============================== Prover9 =============================== Prover9 (64) version Aug-2007, Aug 2007. Process 26411 was started by veroff on titan, Sat Jan 19 14:40:38 2008 The command was "prover9 -f 4.3_alt.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file 4.3_alt.in clear(auto). % clear(auto) -> clear(auto_inference). % clear(auto_inference) -> clear(predicate_elim). % clear(auto_inference) -> assign(eq_defs, pass). % clear(auto) -> clear(auto_limits). % clear(auto_limits) -> assign(max_weight, 2147483647). % clear(auto_limits) -> assign(sos_limit, -1). % clear(auto) -> clear(auto_denials). % clear(auto) -> clear(auto_process). op(400,infix,[^,v,"->","=>",*]). op(200,prefix,[~,-]). lex([0,1,*,^,=>,->,v,~,-]). assign(order,kbo). set(lex_order_vars). set(paramodulation). % set(paramodulation) -> set(back_demod). set(para_units_only). % set(para_units_only) -> assign(para_lit_limit, 1). clear(back_demod). set(hyper_resolution). % set(hyper_resolution) -> set(pos_hyper_resolution). set(auto_denials). set(restrict_denials). formulas(assumptions). (x v y) v z = x v (y v z) # label("(D1)"). (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)"). x v y = y v x # label("(D3)"). x ^ y = y ^ x # label("(D4)"). x v (x ^ y) = x # label("(D5)"). x ^ (x v y) = x # label("(D6)"). (x => y) => ((y => z) => (x => z)) = 1 # label("(BCK1)"). 1 => x = x # label("(BCK2)"). x => 1 = 1 # label("(BCK3)"). x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). x * 1 = x # label("(M1)"). x * y = y * x # label("(M2)"). (x * y) * z = x * (y * z) # label("(M3)"). (x * y) => z = x => (y => z) # label("(P)"). x ^ 1 = x # label("(D10)"). x ^ ((x => y) => y) = x # label("(3.7)"). (x ^ y) => y = 1 # label("(3.11)"). x v 0 = x # label("(D9)"). x -> y = x => (x => y) # label("(-> def)"). ~ x = x => 0 # label("(~ def)"). -x = x => (x => 0) # label("(- def)"). x => (x => (x => y)) = x => (x => y) # label("(E_2)"). (x v y) ^ (x v z) = x v (y ^ z) # label("(D7)"). (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D8)"). ~ ~ x = x # label("(DN)"). (x -> y) ^ (~ y -> ~ x) = x => y # label("(N)"). (x => y) => ((z => x) => (z => y)) = 1 # label("(BCK1')"). x => ((x => y) => y) = 1 # label("(BCK5)"). x => x = 1 # label("(3.16)"). x => (y => x) = 1 # label("(3.17)"). x => (y => z) = y => (x => z) # label("(3.18)"). (x * y) v (x * z) = x * (y v z) # label("(4.1)"). (x => y) ^ (x => z) = x => (y ^ z) # label("(4.2)"). (x * (x => y)) v y = y # label("(4.3)"). (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). ((x => y) * z) => (x => (y * z)) = 1 # label("(4.5)"). end_of_list. formulas(goals). (x => y) ^ y = y # label("(3.13)"). (x v y) => y = x => y # label("(4.6)"). x -> (y => z) = y => (x -> z) # label("(4.7)"). x ^ (~ x => y) = x # label("(4.8)"). end_of_list. formulas(hints). (x => y) ^ y = y # label("(3.13)"). (x v y) => y = x => y # label("(4.6)"). x -> (y => z) = y => (x -> z) # label("(4.7)"). x ^ (~ x => y) = x # label("(4.8)"). x v y = y v x. x ^ y = y ^ x. 1 => x = x. x ^ 1 = x. x ^ ((x => y) => y) = x. x -> y = x => (x => y). x => (x => y) = x -> y. ~ x = x => 0. x => 0 = ~ x. ~ ~ x = x. x => x = 1. x => (y => x) = 1. x => (y => z) = y => (x => z). (x => y) ^ (z => y) = (x v z) => y. x = 1 ^ x. 1 ^ x = x. ~ x => 0 = x. x => (y -> z) = y => (x => (y => z)). x => (y => (x => z)) = y => (x -> z). x => ~ y = y => (x => 0). x => (y => 0) = y => ~ x. 1 ^ (x => y) = (y v x) => y. (x v y) => x = 1 ^ (y => x). x => y = ~ y => ~ x. ~ x => ~ y = y => x. ~ x => y = ~ y => x. x => (~ x => y) = 1. x ^ (1 => (~ x => y)) = x. x ^ (~ x => y) = x. x ^ (y => x) = x. x = (y => x) ^ x. (x => y) ^ y = y. (x v y) => x = y => x. (x v y) => y = x => y. x => (x => (y => z)) = y => (x -> z). x => (y -> z) = y -> (x => z). x -> (y => z) = y => (x -> z). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (x => y) ^ y = y # label("(3.13)") # label(non_clause) # label(goal). [goal]. 2 (x v y) => y = x => y # label("(4.6)") # label(non_clause) # label(goal). [goal]. 3 x -> (y => z) = y => (x -> z) # label("(4.7)") # label(non_clause) # label(goal). [goal]. 4 x ^ (~ x => y) = x # label("(4.8)") # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). (x v y) v z = x v (y v z) # label("(D1)"). [assumption]. (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)"). [assumption]. x v y = y v x # label("(D3)"). [assumption]. x ^ y = y ^ x # label("(D4)"). [assumption]. x v (x ^ y) = x # label("(D5)"). [assumption]. x ^ (x v y) = x # label("(D6)"). [assumption]. (x => y) => ((y => z) => (x => z)) = 1 # label("(BCK1)"). [assumption]. 1 => x = x # label("(BCK2)"). [assumption]. x => 1 = 1 # label("(BCK3)"). [assumption]. x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). [assumption]. x * 1 = x # label("(M1)"). [assumption]. x * y = y * x # label("(M2)"). [assumption]. (x * y) * z = x * (y * z) # label("(M3)"). [assumption]. (x * y) => z = x => (y => z) # label("(P)"). [assumption]. x ^ 1 = x # label("(D10)"). [assumption]. x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. (x ^ y) => y = 1 # label("(3.11)"). [assumption]. x v 0 = x # label("(D9)"). [assumption]. x -> y = x => (x => y) # label("(-> def)"). [assumption]. ~ x = x => 0 # label("(~ def)"). [assumption]. -x = x => (x => 0) # label("(- def)"). [assumption]. x => (x => (x => y)) = x => (x => y) # label("(E_2)"). [assumption]. (x v y) ^ (x v z) = x v (y ^ z) # label("(D7)"). [assumption]. (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D8)"). [assumption]. ~ ~ x = x # label("(DN)"). [assumption]. (x -> y) ^ (~ y -> ~ x) = x => y # label("(N)"). [assumption]. (x => y) => ((z => x) => (z => y)) = 1 # label("(BCK1')"). [assumption]. x => ((x => y) => y) = 1 # label("(BCK5)"). [assumption]. x => x = 1 # label("(3.16)"). [assumption]. x => (y => x) = 1 # label("(3.17)"). [assumption]. x => (y => z) = y => (x => z) # label("(3.18)"). [assumption]. (x * y) v (x * z) = x * (y v z) # label("(4.1)"). [assumption]. (x => y) ^ (x => z) = x => (y ^ z) # label("(4.2)"). [assumption]. (x * (x => y)) v y = y # label("(4.3)"). [assumption]. (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). [assumption]. ((x => y) * z) => (x => (y * z)) = 1 # label("(4.5)"). [assumption]. (c1 => c2) ^ c2 != c2 # label("(3.13)"). [deny(1)]. (c3 v c4) => c4 != c3 => c4 # label("(4.6)"). [deny(2)]. c6 => (c5 -> c7) != c5 -> (c6 => c7) # label("(4.7)"). [deny(3)]. c8 ^ (~ c8 => c9) != c8 # label("(4.8)"). [deny(4)]. end_of_list. formulas(demodulators). end_of_list. % 41 hints input. Auto_denials: % copying label "(3.13)" to answer in negative clause % copying label "(4.6)" to answer in negative clause % copying label "(4.7)" to answer in negative clause % copying label "(4.8)" to answer in negative clause % assign(max_proofs, 4). % (Horn set with more than one neg. clause) Term ordering decisions: Function symbol KB weights: 0=1. 1=1. c1=1. c2=1. c3=1. c4=1. c5=1. c6=1. c7=1. c8=1. c9=1. *=1. ^=1. =>=1. ->=1. v=1. ~=1. -=1. Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ 0, 1, c1, c2, c3, c4, c5, c6, c7, c8, c9, *, ^, =>, ->, v, ~, - ]). Skipping inverse_order, because there is a function_order (lex) command. % Operation v is commutative; C redundancy checks enabled. % Operation ^ is commutative; C redundancy checks enabled. % Operation * is commutative; C redundancy checks enabled. restricted denial: (wt=7): 44 (c1 => c2) ^ c2 != c2 # label("(3.13)") # answer("(3.13)"). [deny(1)]. restricted denial: (wt=9): 45 (c3 v c4) => c4 != c3 => c4 # label("(4.6)") # answer("(4.6)"). [deny(2)]. restricted denial: (wt=11): 47 c5 -> (c6 => c7) != c6 => (c5 -> c7) # answer("(4.7)"). [copy(46),flip(a)]. restricted denial: (wt=8): 48 c8 ^ (~ c8 => c9) != c8 # label("(4.8)") # answer("(4.8)"). [deny(4)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 44 (c1 => c2) ^ c2 != c2 # label("(3.13)") # answer("(3.13)"). [deny(1)]. 45 (c3 v c4) => c4 != c3 => c4 # label("(4.6)") # answer("(4.6)"). [deny(2)]. 47 c5 -> (c6 => c7) != c6 => (c5 -> c7) # answer("(4.7)"). [copy(46),flip(a)]. 48 c8 ^ (~ c8 => c9) != c8 # label("(4.8)") # answer("(4.8)"). [deny(4)]. end_of_list. formulas(sos). 5 (x v y) v z = x v (y v z) # label("(D1)"). [assumption]. 6 (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)"). [assumption]. 7 x v y = y v x # label("(D3)"). [assumption]. 8 x ^ y = y ^ x # label("(D4)"). [assumption]. 9 x v (x ^ y) = x # label("(D5)"). [assumption]. 10 x ^ (x v y) = x # label("(D6)"). [assumption]. 11 (x => y) => ((y => z) => (x => z)) = 1 # label("(BCK1)"). [assumption]. 12 1 => x = x # label("(BCK2)"). [assumption]. 13 x => 1 = 1 # label("(BCK3)"). [assumption]. 14 x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). [assumption]. 15 x * 1 = x # label("(M1)"). [assumption]. 16 x * y = y * x # label("(M2)"). [assumption]. 17 (x * y) * z = x * (y * z) # label("(M3)"). [assumption]. 18 (x * y) => z = x => (y => z) # label("(P)"). [assumption]. 19 x ^ 1 = x # label("(D10)"). [assumption]. 20 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. 21 (x ^ y) => y = 1 # label("(3.11)"). [assumption]. 22 x v 0 = x # label("(D9)"). [assumption]. 24 x => (x => y) = x -> y. [copy(23),flip(a)]. 26 x => 0 = ~ x. [copy(25),flip(a)]. 28 x => (x => 0) = -x. [copy(27),flip(a)]. 29 x => (x => (x => y)) = x => (x => y) # label("(E_2)"). [assumption]. 30 (x v y) ^ (x v z) = x v (y ^ z) # label("(D7)"). [assumption]. 31 (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D8)"). [assumption]. 32 ~ ~ x = x # label("(DN)"). [assumption]. 33 (x -> y) ^ (~ y -> ~ x) = x => y # label("(N)"). [assumption]. 34 (x => y) => ((z => x) => (z => y)) = 1 # label("(BCK1')"). [assumption]. 35 x => ((x => y) => y) = 1 # label("(BCK5)"). [assumption]. 36 x => x = 1 # label("(3.16)"). [assumption]. 37 x => (y => x) = 1 # label("(3.17)"). [assumption]. 38 x => (y => z) = y => (x => z) # label("(3.18)"). [assumption]. 39 (x * y) v (x * z) = x * (y v z) # label("(4.1)"). [assumption]. 40 (x => y) ^ (x => z) = x => (y ^ z) # label("(4.2)"). [assumption]. 41 (x * (x => y)) v y = y # label("(4.3)"). [assumption]. 42 (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). [assumption]. 43 ((x => y) * z) => (x => (y * z)) = 1 # label("(4.5)"). [assumption]. end_of_list. formulas(demodulators). end_of_list. % 41 hints processed (13 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=11): 5 (x v y) v z = x v (y v z) # label("(D1)"). [assumption]. given #2 (I,wt=11): 6 (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)"). [assumption]. given #3 (I,wt=7): 7 x v y = y v x # label("(D3)"). [assumption]. given #4 (I,wt=7): 8 x ^ y = y ^ x # label("(D4)"). [assumption]. given #5 (I,wt=7): 9 x v (x ^ y) = x # label("(D5)"). [assumption]. given #6 (I,wt=7): 10 x ^ (x v y) = x # label("(D6)"). [assumption]. given #7 (I,wt=13): 11 (x => y) => ((y => z) => (x => z)) = 1 # label("(BCK1)"). [assumption]. given #8 (I,wt=5): 12 1 => x = x # label("(BCK2)"). [assumption]. given #9 (I,wt=5): 13 x => 1 = 1 # label("(BCK3)"). [assumption]. given #10 (I,wt=13): 14 x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). [assumption]. given #11 (I,wt=5): 15 x * 1 = x # label("(M1)"). [assumption]. given #12 (I,wt=7): 16 x * y = y * x # label("(M2)"). [assumption]. given #13 (I,wt=11): 17 (x * y) * z = x * (y * z) # label("(M3)"). [assumption]. given #14 (I,wt=11): 18 (x * y) => z = x => (y => z) # label("(P)"). [assumption]. given #15 (I,wt=5): 19 x ^ 1 = x # label("(D10)"). [assumption]. given #16 (I,wt=9): 20 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. given #17 (I,wt=7): 21 (x ^ y) => y = 1 # label("(3.11)"). [assumption]. given #18 (I,wt=5): 22 x v 0 = x # label("(D9)"). [assumption]. given #19 (I,wt=9): 24 x => (x => y) = x -> y. [copy(23),flip(a)]. given #20 (I,wt=6): 26 x => 0 = ~ x. [copy(25),flip(a)]. given #21 (I,wt=8): 28 x => (x => 0) = -x. [copy(27),flip(a)]. given #22 (I,wt=13): 29 x => (x => (x => y)) = x => (x => y) # label("(E_2)"). [assumption]. given #23 (I,wt=13): 30 (x v y) ^ (x v z) = x v (y ^ z) # label("(D7)"). [assumption]. given #24 (I,wt=13): 31 (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D8)"). [assumption]. given #25 (I,wt=5): 32 ~ ~ x = x # label("(DN)"). [assumption]. given #26 (I,wt=13): 33 (x -> y) ^ (~ y -> ~ x) = x => y # label("(N)"). [assumption]. given #27 (I,wt=13): 34 (x => y) => ((z => x) => (z => y)) = 1 # label("(BCK1')"). [assumption]. given #28 (I,wt=9): 35 x => ((x => y) => y) = 1 # label("(BCK5)"). [assumption]. given #29 (I,wt=5): 36 x => x = 1 # label("(3.16)"). [assumption]. given #30 (I,wt=7): 37 x => (y => x) = 1 # label("(3.17)"). [assumption]. given #31 (I,wt=11): 38 x => (y => z) = y => (x => z) # label("(3.18)"). [assumption]. given #32 (I,wt=13): 39 (x * y) v (x * z) = x * (y v z) # label("(4.1)"). [assumption]. given #33 (I,wt=13): 40 (x => y) ^ (x => z) = x => (y ^ z) # label("(4.2)"). [assumption]. given #34 (I,wt=9): 41 (x * (x => y)) v y = y # label("(4.3)"). [assumption]. given #35 (I,wt=13): 42 (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). [assumption]. given #36 (I,wt=13): 43 ((x => y) * z) => (x => (y * z)) = 1 # label("(4.5)"). [assumption]. given #37 (H,wt=5): 112 1 ^ x = x. [para(19(a,1),8(a,1)),flip(a)]. given #38 (H,wt=6): 250 ~ x => 0 = x. [para(32(a,1),26(a,2))]. given #39 (H,wt=10): 373 x => (y => 0) = y => ~ x. [para(26(a,1),38(a,1,2)),flip(a)]. given #40 (H,wt=9): 649 ~ x => ~ y = y => x. [para(250(a,1),373(a,1,2)),flip(a)]. given #41 (H,wt=9): 667 ~ x => y = ~ y => x. [para(32(a,1),649(a,1,2))]. given #42 (H,wt=8): 714 x => (~ x => y) = 1. [para(667(a,1),37(a,1,2))]. given #43 (H,wt=10): 737 x ^ (1 => (~ x => y)) = x. [para(714(a,1),20(a,1,2,1))]. -------- Proof 1 -------- "(4.8)". ============================== PROOF ================================= % Proof 1 at 0.03 (+ 0.00) seconds: "(4.8)". % Length of proof is 17. % Level of proof is 8. % Maximum clause weight is 11. % Given clauses 43. 4 x ^ (~ x => y) = x # label("(4.8)") # label(non_clause) # label(goal). [goal]. 12 1 => x = x # label("(BCK2)"). [assumption]. 20 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. 25 ~ x = x => 0 # label("(~ def)"). [assumption]. 26 x => 0 = ~ x. [copy(25),flip(a)]. 32 ~ ~ x = x # label("(DN)"). [assumption]. 37 x => (y => x) = 1 # label("(3.17)"). [assumption]. 38 x => (y => z) = y => (x => z) # label("(3.18)"). [assumption]. 48 c8 ^ (~ c8 => c9) != c8 # label("(4.8)") # answer("(4.8)"). [deny(4)]. 250 ~ x => 0 = x. [para(32(a,1),26(a,2))]. 373 x => (y => 0) = y => ~ x. [para(26(a,1),38(a,1,2)),flip(a)]. 649 ~ x => ~ y = y => x. [para(250(a,1),373(a,1,2)),flip(a)]. 667 ~ x => y = ~ y => x. [para(32(a,1),649(a,1,2))]. 714 x => (~ x => y) = 1. [para(667(a,1),37(a,1,2))]. 737 x ^ (1 => (~ x => y)) = x. [para(714(a,1),20(a,1,2,1))]. 764 x ^ (~ x => y) = x # label("(4.8)"). [para(12(a,1),737(a,1,2))]. 765 $F # answer("(4.8)"). [resolve(764,a,48,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 48 given #44 (H,wt=8): 764 x ^ (~ x => y) = x # label("(4.8)"). [para(12(a,1),737(a,1,2))]. given #45 (H,wt=7): 792 x ^ (y => x) = x. [para(649(a,1),764(a,1,2))]. -------- Proof 2 -------- "(3.13)". ============================== PROOF ================================= % Proof 2 at 0.04 (+ 0.00) seconds: "(3.13)". % Length of proof is 20. % Level of proof is 10. % Maximum clause weight is 11. % Given clauses 45. 1 (x => y) ^ y = y # label("(3.13)") # label(non_clause) # label(goal). [goal]. 8 x ^ y = y ^ x # label("(D4)"). [assumption]. 12 1 => x = x # label("(BCK2)"). [assumption]. 20 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. 25 ~ x = x => 0 # label("(~ def)"). [assumption]. 26 x => 0 = ~ x. [copy(25),flip(a)]. 32 ~ ~ x = x # label("(DN)"). [assumption]. 37 x => (y => x) = 1 # label("(3.17)"). [assumption]. 38 x => (y => z) = y => (x => z) # label("(3.18)"). [assumption]. 44 (c1 => c2) ^ c2 != c2 # label("(3.13)") # answer("(3.13)"). [deny(1)]. 250 ~ x => 0 = x. [para(32(a,1),26(a,2))]. 373 x => (y => 0) = y => ~ x. [para(26(a,1),38(a,1,2)),flip(a)]. 649 ~ x => ~ y = y => x. [para(250(a,1),373(a,1,2)),flip(a)]. 667 ~ x => y = ~ y => x. [para(32(a,1),649(a,1,2))]. 714 x => (~ x => y) = 1. [para(667(a,1),37(a,1,2))]. 737 x ^ (1 => (~ x => y)) = x. [para(714(a,1),20(a,1,2,1))]. 764 x ^ (~ x => y) = x # label("(4.8)"). [para(12(a,1),737(a,1,2))]. 792 x ^ (y => x) = x. [para(649(a,1),764(a,1,2))]. 796 (x => y) ^ y = y # label("(3.13)"). [para(792(a,1),8(a,1)),flip(a)]. 797 $F # answer("(3.13)"). [resolve(796,a,44,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 44 given #46 (H,wt=7): 796 (x => y) ^ y = y # label("(3.13)"). [para(792(a,1),8(a,1)),flip(a)]. given #47 (H,wt=11): 528 (x v y) => x = 1 ^ (y => x). [para(36(a,1),42(a,1,1)),flip(a)]. given #48 (H,wt=9): 883 (x v y) => x = y => x. [para(528(a,2),112(a,1))]. -------- Proof 3 -------- "(4.6)". ============================== PROOF ================================= % Proof 3 at 0.04 (+ 0.00) seconds: "(4.6)". % Length of proof is 12. % Level of proof is 4. % Maximum clause weight is 13. % Given clauses 48. 2 (x v y) => y = x => y # label("(4.6)") # label(non_clause) # label(goal). [goal]. 7 x v y = y v x # label("(D3)"). [assumption]. 8 x ^ y = y ^ x # label("(D4)"). [assumption]. 19 x ^ 1 = x # label("(D10)"). [assumption]. 36 x => x = 1 # label("(3.16)"). [assumption]. 42 (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). [assumption]. 45 (c3 v c4) => c4 != c3 => c4 # label("(4.6)") # answer("(4.6)"). [deny(2)]. 112 1 ^ x = x. [para(19(a,1),8(a,1)),flip(a)]. 528 (x v y) => x = 1 ^ (y => x). [para(36(a,1),42(a,1,1)),flip(a)]. 883 (x v y) => x = y => x. [para(528(a,2),112(a,1))]. 898 (x v y) => y = x => y # label("(4.6)"). [para(7(a,1),883(a,1,1))]. 899 $F # answer("(4.6)"). [resolve(898,a,45,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 45 given #49 (H,wt=9): 898 (x v y) => y = x => y # label("(4.6)"). [para(7(a,1),883(a,1,1))]. given #50 (H,wt=13): 372 x => (y => (x => z)) = y => (x -> z). [para(24(a,1),38(a,1,2)),flip(a)]. given #51 (H,wt=13): 1061 x => (x => (y => z)) = y => (x -> z). [para(38(a,1),372(a,1,2))]. -------- Proof 4 -------- "(4.7)". ============================== PROOF ================================= % Proof 4 at 0.05 (+ 0.00) seconds: "(4.7)". % Length of proof is 10. % Level of proof is 5. % Maximum clause weight is 13. % Given clauses 51. 3 x -> (y => z) = y => (x -> z) # label("(4.7)") # label(non_clause) # label(goal). [goal]. 23 x -> y = x => (x => y) # label("(-> def)"). [assumption]. 24 x => (x => y) = x -> y. [copy(23),flip(a)]. 38 x => (y => z) = y => (x => z) # label("(3.18)"). [assumption]. 46 c6 => (c5 -> c7) != c5 -> (c6 => c7) # label("(4.7)") # answer("(4.7)"). [deny(3)]. 47 c5 -> (c6 => c7) != c6 => (c5 -> c7) # answer("(4.7)"). [copy(46),flip(a)]. 372 x => (y => (x => z)) = y => (x -> z). [para(24(a,1),38(a,1,2)),flip(a)]. 1061 x => (x => (y => z)) = y => (x -> z). [para(38(a,1),372(a,1,2))]. 1120 x -> (y => z) = y => (x -> z) # label("(4.7)"). [para(1061(a,1),24(a,1)),flip(a)]. 1121 $F # answer("(4.7)"). [resolve(1120,a,47,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=51. Generated=1536. Kept=1109. proofs=4. Usable=51. Sos=1001. Demods=0. Limbo=19, Disabled=77. Hints=41. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=427. Back_subsumed=34. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=1. Megabytes=1.40. User_CPU=0.05, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED THEOREM PROVED Exiting with 4 proofs. ------ process 26411 exit (max_proofs) ------  Process 26411 exit (max_proofs) Sat Jan 19 14:40:38 2008