============================== prooftrans (BV) ======================= Prover9 (64) version Aug-2007, Aug 2007. Process 32400 was started by veroff on io, Mon Jan 21 11:14:49 2008 The command was "prover9 -f 3.4.in". ============================== end of head =========================== op(400,infix,[^,v,"->","=>",*]). op(200,prefix,[~,-]). ============================== end of input ========================== ============================== PROOF ================================= % -------- Comments from original proof -------- % Proof 1 at 0.02 (+ 0.01) seconds: "(BCK5)". % Length of proof is 6. % Level of proof is 2. % Maximum clause weight is 9. % Given clauses 38. 1 x => ((x => y) => y) = 1 # label("(BCK5)") # label(non_clause) # label(goal). [goal]. 35 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. 42 (x ^ y) => y = 1 # label("(3.11)"). [assumption]. 48 c1 => ((c1 => c2) => c2) != 1 # label("(BCK5)") # answer("(BCK5)"). [deny(1)]. 589 x => ((x => y) => y) = 1. [para(35(a,1),42(a,1,1))]. 590 $F # answer("(BCK5)"). [resolve(589,a,48,a)]. ============================== end of proof ==========================