Again, by applying inference rules, we obtain the following sets of premises P and subgoals G: Here, the two sub-goals G 5 and G 6 do not match any of the premises, so the attempted proof of B ′ ⇒ A ′ fails.
we therefore attempt to inject additional axioms, but in this case no predicate in P shares the argument x 2 of the predicates bar(x 2 ) and in(e 1 , x 2 ) in G. no axiom can be generated.