============================== prooftrans (BV) ======================= Prover9 (64) version Aug-2007, Aug 2007. Process 26278 was started by veroff on titan, Sat Jan 19 14:18:57 2008 The command was "prover9 -f 4.5.in". ============================== end of head =========================== op(400,infix,[^,v,"->","=>",*]). op(200,prefix,[~,-]). ============================== end of input ========================== ============================== PROOF ================================= % -------- Comments from original proof -------- % Proof 1 at 0.01 (+ 0.00) seconds: "(N2)". % Length of proof is 7. % Level of proof is 3. % Maximum clause weight is 9. % Given clauses 30. 1 x -> x = 1 # label("(N2)") # label(non_clause) # label(goal). [goal]. 20 x -> y = x => (x => y) # label("(-> def)"). [assumption]. 21 x => (x => y) = x -> y. [copy(20),flip(a)]. 34 x => (y => x) = 1 # label("(3.17)"). [assumption]. 47 c1 -> c1 != 1 # label("(N2)") # answer("(N2)"). [deny(1)]. 344 x -> x = 1. [para(34(a,1),21(a,1)),flip(a)]. 345 $F # answer("(N2)"). [resolve(344,a,47,a)]. ============================== end of proof ==========================