============================== prooftrans ============================ Prover9 (64) version 2009-02A, February 2009. Process 9548 was started by veroff on proof, Sat Sep 19 09:10:52 2009 The command was "prover9 -f 2.2c.in". ============================== end of head =========================== op(400,infix,[^,v,"=>",*]). op(200,prefix,~). ============================== end of input ========================== ============================== PROOF ================================= % -------- Comments from original proof -------- % Proof 1 at 0.10 (+ 0.01) seconds: "(4)". % Length of proof is 9. % Level of proof is 4. % Maximum clause weight is 5. % Given clauses 27. 1 (all x all y (x = 1 & y = 1 -> x ^ y = 1)) # label("(4)") # label(non_clause) # label(goal). [goal]. 4 x ^ x = x # label("(D3)"). [assumption]. 28 c1 = 1 # label("(4)"). [deny(1)]. 29 c2 = 1 # label("(4)"). [deny(1)]. 30 c1 ^ c2 != 1 # label("(4)") # answer("(4)"). [deny(1)]. 3551 c1 ^ c1 = 1. [para(28(a,1),4(a,2))]. 3815 c2 = c1. [para(29(a,2),28(a,2)),flip(a)]. 4114 c1 ^ c2 = 1. [para(3815(a,2),3551(a,1,2))]. 4115 $F # answer("(4)"). [resolve(4114,a,30,a)]. ============================== end of proof ==========================