Proof of a(p1,x) != a(p2,x)

Proof of `a(p1,x) != a(p2,x) | a(eq,x) = p1.`

Since this is the first OTTER proof presented in this document, I'll explain the procedure I use to get proofs. In OTTER any atomic term beginning with u, v, w, x, y, z is by default treated as a (universally quantified) variable, while any atomic term beginning with any other letter is treated as a constant. Most of the assertions we need to prove are universal, like the present one, which is asserted for all x. We need to refute the negation of this universal assertion. The negation asserts the existence of some constant for which the universal assertion fails. Thus in the set-of-support clauses below, I change x to bad, which, beginning with b, is treated as a constant. The same convention is followed throughout this document: if a clause has only one universally quantified variable, I replace this variable with bad in the clauses to be refuted. If a clause has more than one universally quantified variable, I generally prefix the names of the variables with bad, so x and y become badx and bady.

list(sos).
a(p1,bad) = a(p2,bad).
a(eq,bad) != p1.
end_of_list.

As Art Quaife [4] points out, when the statement to be refuted contains no variables, one can restrict the search tremendously by using a weight template to immediately discard all clauses with variables.

weight_list(pick_and_purge).
weight(x,100).
end_of_list.

The proofs in this document are automatically processed by my Java application which adds a hypertext link from each input clause in a proof (OTTER marks input clauses with the empty justification [ ]) to the place where it was introduced earlier in the input file. This makes it easy to find the proof of each input clause. In the present proof the input clauses are axioms, so the link refers to the section where the axioms of TRC were introduced. Input clauses containing the string "bad" are automatically marked "assumption to refute".

----> UNIT CONFLICT at   0.10 sec ----> 46 [binary,44.1,20.1] $F.

Length of proof is 1.  Level of proof is 1.

Proof



5 [reference] pair(p1 x,p2 x)=x.
15 [reference] x!=y|eq pair(x,y) =p1.
19 [assumption to refute] p1 bad=p2 bad.
20 [assumption to refute] eq bad!=p1.
44 [ur,19,15,demod,5] eq bad=p1.
46 [binary,44.1,20.1] $F.

Proof of a(p1,x) != a(p2,x) | a(eq,x) = p1.

Proof

Proof of `a(p1,x) != a(p2,x) | a(eq,x) = p1.`