============================== Prover9 =============================== Prover9 (64) version Aug-2007, Aug 2007. Process 26266 was started by veroff on titan, Sat Jan 19 14:18:54 2008 The command was "prover9 -f 4.4_alt.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file 4.4_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(assumptions). (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(goals). x -> ((y v x) -> z) = x -> z # label("(4.9)"). x -> (~ x v y) = x -> y # label("(4.10)"). end_of_list. formulas(hints). x -> ((y v x) -> z) = x -> z # label("(4.9)"). x -> (~ x v y) = x -> y # label("(4.10)"). x v y = y v x. x ^ y = y ^ x. x v (x ^ y) = x. 1 => x = x. x * y = y * x. (x * y) => z = x => (y => z). x ^ ((x => y) => y) = x. x -> y = x => (x => y). x => (x => y) = x -> y. ~ x = x => 0. x => 0 = ~ x. x => (x => (x => y)) = x => (x => y). ~ ~ x = x. (x => y) => ((z => x) => (z => y)) = 1. x => (y => z) = y => (x => z). (x => y) ^ (x => z) = x => (y ^ z). (x => y) ^ (z => y) = (x v z) => y. ((x => y) * z) => (x => (y * z)) = 1. (x => y) ^ y = y. (x v y) => y = x => y. x -> (y => z) = y => (x -> z). x = (x ^ y) v x. (x ^ y) v x = x. ~ (x * y) = x => (y => 0). x => (y => 0) = ~ (x * y). x => (x -> y) = x => (x => y). (x => y) => (z => ((z => x) => y)) = 1. (x -> y) ^ (x => z) = x => ((x => y) ^ z). x => ((x => y) ^ z) = (x -> y) ^ (x => z). ~ x ^ (y => 0) = (x v y) => 0. (x * (y => z)) => (y => (z * x)) = 1. x = x ^ (y => x). x ^ (y => x) = x. x -> (y -> z) = y => (x -> (y => z)). x => (y -> (x => z)) = y -> (x -> z). x v (y => x) = y => x. x => ~ y = ~ (x * y). ~ (x * y) = x => ~ y. ~ (x => ~ y) = x * y. ~ (x => ~ y) = (x v ~ y) * y. (x v ~ y) * y = ~ (x => ~ y). x => (x -> y) = x -> y. x => (y -> z) = y => (x => (y -> z)). x => (y => (x -> z)) = y => (x -> z). (x -> y) ^ (z => (x -> y)) = (x v z) => (x -> y). ~ x ^ ~ y = (x v y) => 0. (x v y) => 0 = ~ x ^ ~ y. ~ x ^ ~ y = ~ (x v y). x ^ ~ y = ~ (~ x v y). ~ (~ x v y) = x ^ ~ y. ~ (x v ~ y) = y ^ ~ x. ~ (x v (y => ~ z)) = (y * z) ^ ~ x. (x v ~ y) * y = x * y. x * y = y * (x v ~ y). x * (y v ~ x) = y * x. 1 = x => ((y => z) => ((x => y) => z)). x => ((y => z) => ((x => y) => z)) = 1. 1 = x => ((y * (x => z)) => (z * y)). x => ((y * (x => z)) => (z * y)) = 1. x => (x => (y -> z)) = y -> (x -> z). x => (((x => y) => z) => ((x -> y) => z)) = 1. x => (y => ((x => z) => (z * y))) = 1. x -> (y -> z) = y -> (x -> z). 1 = x -> ((x => y) => (y * x)). x -> ((x => y) => (y * x)) = 1. x -> ((x => y) => (x * y)) = 1. 1 = (x => y) => (x -> (x * y)). (x => y) => (x -> (x * y)) = 1. ~ (x => ~ y) = (x * y) ^ ~ ~ y. (x * y) ^ ~ ~ y = ~ (x => ~ y). (x * y) ^ ~ ~ y = x * y. (x * y) ^ y = x * y. x => (y ^ (x => z)) = (x -> z) ^ (x => y). x => ((x -> y) => (((x => y) => z) => z)) = 1. x => ((x => y) ^ (x => z)) = (x -> z) ^ (x -> y). x => ((x -> y) => (1 => (x -> (x * y)))) = 1. x => ((x -> y) => (x -> (x * y))) = 1. 1 = (x -> y) => (x -> (x * y)). (x -> y) => (x -> (x * y)) = 1. (x -> y) ^ (1 => (x -> (x * y))) = x -> y. (x -> y) ^ (x -> (x * y)) = x -> y. x => (x => (y ^ z)) = (x -> z) ^ (x -> y). (x -> y) ^ (x -> z) = x -> (z ^ y). x -> ((x * y) ^ y) = x -> y. x -> (x * y) = x -> y. x -> (y * x) = x -> (y v ~ x). x -> (y v ~ x) = x -> (y * x). x -> (y v ~ x) = x -> (x * y). x -> (y v ~ x) = x -> y. x -> (~ x v y) = x -> y. x -> y = (x v z) => (x -> y). (x v y) => (x -> z) = x -> z. (x v y) => (x -> z) = (x v y) -> (x -> z). (x v y) -> (x -> z) = (x v y) => (x -> z). (x v y) -> (x -> z) = x -> z. (x v y) -> (y -> z) = y -> z. x -> y = x -> ((z v x) -> y). x -> ((y v x) -> z) = x -> z. end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 x -> ((y v x) -> z) = x -> z # label("(4.9)") # label(non_clause) # label(goal). [goal]. 2 x -> (~ x v y) = x -> y # label("(4.10)") # 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]. (x => y) ^ y = y # label("(3.13)"). [assumption]. (x v y) => y = x => y # label("(4.6)"). [assumption]. x -> (y => z) = y => (x -> z) # label("(4.7)"). [assumption]. x ^ (~ x => y) = x # label("(4.8)"). [assumption]. c1 -> ((c2 v c1) -> c3) != c1 -> c3 # label("(4.9)"). [deny(1)]. c4 -> (~ c4 v c5) != c4 -> c5 # label("(4.10)"). [deny(2)]. end_of_list. formulas(demodulators). end_of_list. % 100 hints input. Auto_denials: % copying label "(4.9)" to answer in negative clause % copying label "(4.10)" to answer in negative clause % assign(max_proofs, 2). % (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. *=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, *, ^, =>, ->, 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=11): 46 c1 -> ((c2 v c1) -> c3) != c1 -> c3 # label("(4.9)") # answer("(4.9)"). [deny(1)]. restricted denial: (wt=10): 47 c4 -> (~ c4 v c5) != c4 -> c5 # label("(4.10)") # answer("(4.10)"). [deny(2)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 46 c1 -> ((c2 v c1) -> c3) != c1 -> c3 # label("(4.9)") # answer("(4.9)"). [deny(1)]. 47 c4 -> (~ c4 v c5) != c4 -> c5 # label("(4.10)") # answer("(4.10)"). [deny(2)]. end_of_list. formulas(sos). 3 (x v y) v z = x v (y v z) # label("(D1)"). [assumption]. 4 (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)"). [assumption]. 5 x v y = y v x # label("(D3)"). [assumption]. 6 x ^ y = y ^ x # label("(D4)"). [assumption]. 7 x v (x ^ y) = x # label("(D5)"). [assumption]. 8 x ^ (x v y) = x # label("(D6)"). [assumption]. 9 (x => y) => ((y => z) => (x => z)) = 1 # label("(BCK1)"). [assumption]. 10 1 => x = x # label("(BCK2)"). [assumption]. 11 x => 1 = 1 # label("(BCK3)"). [assumption]. 12 x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). [assumption]. 13 x * 1 = x # label("(M1)"). [assumption]. 14 x * y = y * x # label("(M2)"). [assumption]. 15 (x * y) * z = x * (y * z) # label("(M3)"). [assumption]. 16 (x * y) => z = x => (y => z) # label("(P)"). [assumption]. 17 x ^ 1 = x # label("(D10)"). [assumption]. 18 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. 19 (x ^ y) => y = 1 # label("(3.11)"). [assumption]. 20 x v 0 = x # label("(D9)"). [assumption]. 22 x => (x => y) = x -> y. [copy(21),flip(a)]. 24 x => 0 = ~ x. [copy(23),flip(a)]. 26 x => (x => 0) = -x. [copy(25),flip(a)]. 27 x => (x => (x => y)) = x => (x => y) # label("(E_2)"). [assumption]. 28 (x v y) ^ (x v z) = x v (y ^ z) # label("(D7)"). [assumption]. 29 (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D8)"). [assumption]. 30 ~ ~ x = x # label("(DN)"). [assumption]. 31 (x -> y) ^ (~ y -> ~ x) = x => y # label("(N)"). [assumption]. 32 (x => y) => ((z => x) => (z => y)) = 1 # label("(BCK1')"). [assumption]. 33 x => ((x => y) => y) = 1 # label("(BCK5)"). [assumption]. 34 x => x = 1 # label("(3.16)"). [assumption]. 35 x => (y => x) = 1 # label("(3.17)"). [assumption]. 36 x => (y => z) = y => (x => z) # label("(3.18)"). [assumption]. 37 (x * y) v (x * z) = x * (y v z) # label("(4.1)"). [assumption]. 38 (x => y) ^ (x => z) = x => (y ^ z) # label("(4.2)"). [assumption]. 39 (x * (x => y)) v y = y # label("(4.3)"). [assumption]. 40 (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). [assumption]. 41 ((x => y) * z) => (x => (y * z)) = 1 # label("(4.5)"). [assumption]. 42 (x => y) ^ y = y # label("(3.13)"). [assumption]. 43 (x v y) => y = x => y # label("(4.6)"). [assumption]. 44 x -> (y => z) = y => (x -> z) # label("(4.7)"). [assumption]. 45 x ^ (~ x => y) = x # label("(4.8)"). [assumption]. end_of_list. formulas(demodulators). end_of_list. % 100 hints processed (25 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=11): 3 (x v y) v z = x v (y v z) # label("(D1)"). [assumption]. given #2 (I,wt=11): 4 (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)"). [assumption]. given #3 (I,wt=7): 5 x v y = y v x # label("(D3)"). [assumption]. given #4 (I,wt=7): 6 x ^ y = y ^ x # label("(D4)"). [assumption]. given #5 (I,wt=7): 7 x v (x ^ y) = x # label("(D5)"). [assumption]. given #6 (I,wt=7): 8 x ^ (x v y) = x # label("(D6)"). [assumption]. given #7 (I,wt=13): 9 (x => y) => ((y => z) => (x => z)) = 1 # label("(BCK1)"). [assumption]. given #8 (I,wt=5): 10 1 => x = x # label("(BCK2)"). [assumption]. given #9 (I,wt=5): 11 x => 1 = 1 # label("(BCK3)"). [assumption]. given #10 (I,wt=13): 12 x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). [assumption]. given #11 (I,wt=5): 13 x * 1 = x # label("(M1)"). [assumption]. given #12 (I,wt=7): 14 x * y = y * x # label("(M2)"). [assumption]. given #13 (I,wt=11): 15 (x * y) * z = x * (y * z) # label("(M3)"). [assumption]. given #14 (I,wt=11): 16 (x * y) => z = x => (y => z) # label("(P)"). [assumption]. given #15 (I,wt=5): 17 x ^ 1 = x # label("(D10)"). [assumption]. given #16 (I,wt=9): 18 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. given #17 (I,wt=7): 19 (x ^ y) => y = 1 # label("(3.11)"). [assumption]. given #18 (I,wt=5): 20 x v 0 = x # label("(D9)"). [assumption]. given #19 (I,wt=9): 22 x => (x => y) = x -> y. [copy(21),flip(a)]. given #20 (I,wt=6): 24 x => 0 = ~ x. [copy(23),flip(a)]. given #21 (I,wt=8): 26 x => (x => 0) = -x. [copy(25),flip(a)]. given #22 (I,wt=13): 27 x => (x => (x => y)) = x => (x => y) # label("(E_2)"). [assumption]. given #23 (I,wt=13): 28 (x v y) ^ (x v z) = x v (y ^ z) # label("(D7)"). [assumption]. given #24 (I,wt=13): 29 (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D8)"). [assumption]. given #25 (I,wt=5): 30 ~ ~ x = x # label("(DN)"). [assumption]. given #26 (I,wt=13): 31 (x -> y) ^ (~ y -> ~ x) = x => y # label("(N)"). [assumption]. given #27 (I,wt=13): 32 (x => y) => ((z => x) => (z => y)) = 1 # label("(BCK1')"). [assumption]. given #28 (I,wt=9): 33 x => ((x => y) => y) = 1 # label("(BCK5)"). [assumption]. given #29 (I,wt=5): 34 x => x = 1 # label("(3.16)"). [assumption]. given #30 (I,wt=7): 35 x => (y => x) = 1 # label("(3.17)"). [assumption]. given #31 (I,wt=11): 36 x => (y => z) = y => (x => z) # label("(3.18)"). [assumption]. given #32 (I,wt=13): 37 (x * y) v (x * z) = x * (y v z) # label("(4.1)"). [assumption]. given #33 (I,wt=13): 38 (x => y) ^ (x => z) = x => (y ^ z) # label("(4.2)"). [assumption]. given #34 (I,wt=9): 39 (x * (x => y)) v y = y # label("(4.3)"). [assumption]. given #35 (I,wt=13): 40 (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). [assumption]. given #36 (I,wt=13): 41 ((x => y) * z) => (x => (y * z)) = 1 # label("(4.5)"). [assumption]. given #37 (I,wt=7): 42 (x => y) ^ y = y # label("(3.13)"). [assumption]. given #38 (I,wt=9): 43 (x v y) => y = x => y # label("(4.6)"). [assumption]. given #39 (I,wt=11): 44 x -> (y => z) = y => (x -> z) # label("(4.7)"). [assumption]. given #40 (I,wt=8): 45 x ^ (~ x => y) = x # label("(4.8)"). [assumption]. given #41 (H,wt=7): 66 (x ^ y) v x = x. [para(7(a,1),5(a,1)),flip(a)]. given #42 (H,wt=7): 579 x ^ (y => x) = x. [para(42(a,1),6(a,1)),flip(a)]. given #43 (H,wt=9): 692 x v (y => x) = y => x. [para(42(a,1),66(a,1,1))]. given #44 (H,wt=10): 149 x => (y => 0) = ~ (x * y). [para(24(a,1),16(a,1)),flip(a)]. given #45 (H,wt=9): 763 ~ (x * y) = x => ~ y. [para(24(a,1),149(a,1,2)),flip(a)]. given #46 (H,wt=9): 804 ~ (x => ~ y) = x * y. [para(763(a,1),30(a,1,1))]. given #47 (H,wt=11): 190 x => (x -> y) = x => (x => y). [para(22(a,1),27(a,1,2))]. given #48 (H,wt=9): 844 x => (x -> y) = x -> y. [para(22(a,1),190(a,2))]. given #49 (H,wt=12): 507 ~ x ^ (y => 0) = (x v y) => 0. [para(24(a,1),40(a,1,1))]. given #50 (H,wt=11): 921 (x v y) => 0 = ~ x ^ ~ y. [para(24(a,1),507(a,1,2)),flip(a)]. given #51 (H,wt=10): 949 ~ x ^ ~ y = ~ (x v y). [para(921(a,1),24(a,1))]. given #52 (H,wt=10): 999 ~ (~ x v y) = x ^ ~ y. [para(30(a,1),949(a,1,1)),flip(a)]. given #53 (H,wt=10): 1012 ~ (x v ~ y) = y ^ ~ x. [para(5(a,1),999(a,1,1))]. given #54 (H,wt=12): 824 (x v ~ y) * y = ~ (x => ~ y). [para(43(a,1),804(a,1,1)),flip(a)]. given #55 (H,wt=10): 1094 (x v ~ y) * y = x * y. [para(804(a,1),824(a,2))]. given #56 (H,wt=10): 1103 x * (y v ~ x) = y * x. [para(1094(a,1),14(a,1)),flip(a)]. given #57 (H,wt=13): 379 (x => y) => (z => ((z => x) => y)) = 1. [para(36(a,1),32(a,1,2))]. given #58 (H,wt=13): 543 (x * (y => z)) => (y => (z * x)) = 1. [para(14(a,1),41(a,1,1))]. given #59 (H,wt=13): 646 x => (y -> (x => z)) = y -> (x -> z). [para(22(a,1),44(a,1,2)),flip(a)]. given #60 (H,wt=13): 894 x => (y => (x -> z)) = y => (x -> z). [para(844(a,1),36(a,1,2)),flip(a)]. given #61 (H,wt=13): 1193 x => ((y => z) => ((x => y) => z)) = 1. [para(379(a,1),36(a,1)),flip(a)]. given #62 (H,wt=13): 1258 x => ((y * (x => z)) => (z * y)) = 1. [para(543(a,1),36(a,1)),flip(a)]. given #63 (H,wt=13): 1330 x => (x => (y -> z)) = y -> (x -> z). [para(44(a,1),646(a,1,2))]. given #64 (H,wt=11): 1559 x -> (y -> z) = y -> (x -> z). [para(1330(a,1),22(a,1))]. given #65 (H,wt=13): 1493 x => (y => ((x => z) => (z * y))) = 1. [para(16(a,1),1258(a,1,2))]. given #66 (H,wt=11): 1628 x -> ((x => y) => (y * x)) = 1. [para(1493(a,1),22(a,1)),flip(a)]. given #67 (H,wt=11): 1690 x -> ((x => y) => (x * y)) = 1. [para(14(a,1),1628(a,1,2,2))]. given #68 (H,wt=11): 1748 (x => y) => (x -> (x * y)) = 1. [para(1690(a,1),44(a,1)),flip(a)]. given #69 (H,wt=14): 1047 ~ (x v (y => ~ z)) = (y * z) ^ ~ x. [para(763(a,1),1012(a,1,1,2))]. given #70 (H,wt=13): 1860 (x * y) ^ ~ ~ y = ~ (x => ~ y). [para(692(a,1),1047(a,1,1)),flip(a)]. given #71 (H,wt=11): 1916 (x * y) ^ ~ ~ y = x * y. [para(804(a,1),1860(a,2))]. given #72 (H,wt=9): 1943 (x * y) ^ y = x * y. [para(30(a,1),1916(a,1,2))]. given #73 (H,wt=15): 431 x => ((x => y) ^ z) = (x -> y) ^ (x => z). [para(22(a,1),38(a,1,1)),flip(a)]. given #74 (H,wt=15): 1409 x => (((x => y) => z) => ((x -> y) => z)) = 1. [para(22(a,1),1193(a,1,2,2,1))]. given #75 (H,wt=15): 1983 x => (y ^ (x => z)) = (x -> z) ^ (x => y). [para(6(a,1),431(a,1,2))]. given #76 (H,wt=15): 2146 x => ((x -> y) => (((x => y) => z) => z)) = 1. [para(36(a,1),1409(a,1,2))]. given #77 (H,wt=15): 2435 x => ((x -> y) => (1 => (x -> (x * y)))) = 1. [para(1748(a,1),2146(a,1,2,2,1))]. given #78 (H,wt=13): 2453 x => ((x -> y) => (x -> (x * y))) = 1. [para(10(a,1),2435(a,1,2,2))]. given #79 (H,wt=11): 2547 (x -> y) => (x -> (x * y)) = 1. [para(2453(a,1),894(a,1)),flip(a)]. given #80 (H,wt=15): 2572 (x -> y) ^ (1 => (x -> (x * y))) = x -> y. [para(2547(a,1),18(a,1,2,1))]. given #81 (H,wt=13): 2622 (x -> y) ^ (x -> (x * y)) = x -> y. [para(10(a,1),2572(a,1,2))]. given #82 (H,wt=17): 898 (x -> y) ^ (z => (x -> y)) = (x v z) => (x -> y). [para(844(a,1),40(a,1,1))]. given #83 (H,wt=11): 2694 (x v y) => (x -> z) = x -> z. [para(898(a,1),579(a,1))]. given #84 (H,wt=15): 2721 (x v y) -> (x -> z) = (x v y) => (x -> z). [para(2694(a,1),22(a,1,2)),flip(a)]. given #85 (H,wt=11): 2819 (x v y) -> (x -> z) = x -> z. [para(2694(a,1),2721(a,2))]. given #86 (H,wt=11): 2823 (x v y) -> (y -> z) = y -> z. [para(5(a,1),2819(a,1,1))]. -------- Proof 1 -------- "(4.9)". ============================== PROOF ================================= % Proof 1 at 0.12 (+ 0.00) seconds: "(4.9)". % Length of proof is 23. % Level of proof is 10. % Maximum clause weight is 17. % Given clauses 86. 1 x -> ((y v x) -> z) = x -> z # label("(4.9)") # label(non_clause) # label(goal). [goal]. 5 x v y = y v x # label("(D3)"). [assumption]. 6 x ^ y = y ^ x # label("(D4)"). [assumption]. 21 x -> y = x => (x => y) # label("(-> def)"). [assumption]. 22 x => (x => y) = x -> y. [copy(21),flip(a)]. 27 x => (x => (x => y)) = x => (x => y) # label("(E_2)"). [assumption]. 40 (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). [assumption]. 42 (x => y) ^ y = y # label("(3.13)"). [assumption]. 44 x -> (y => z) = y => (x -> z) # label("(4.7)"). [assumption]. 46 c1 -> ((c2 v c1) -> c3) != c1 -> c3 # label("(4.9)") # answer("(4.9)"). [deny(1)]. 190 x => (x -> y) = x => (x => y). [para(22(a,1),27(a,1,2))]. 579 x ^ (y => x) = x. [para(42(a,1),6(a,1)),flip(a)]. 646 x => (y -> (x => z)) = y -> (x -> z). [para(22(a,1),44(a,1,2)),flip(a)]. 844 x => (x -> y) = x -> y. [para(22(a,1),190(a,2))]. 898 (x -> y) ^ (z => (x -> y)) = (x v z) => (x -> y). [para(844(a,1),40(a,1,1))]. 1330 x => (x => (y -> z)) = y -> (x -> z). [para(44(a,1),646(a,1,2))]. 1559 x -> (y -> z) = y -> (x -> z). [para(1330(a,1),22(a,1))]. 2694 (x v y) => (x -> z) = x -> z. [para(898(a,1),579(a,1))]. 2721 (x v y) -> (x -> z) = (x v y) => (x -> z). [para(2694(a,1),22(a,1,2)),flip(a)]. 2819 (x v y) -> (x -> z) = x -> z. [para(2694(a,1),2721(a,2))]. 2823 (x v y) -> (y -> z) = y -> z. [para(5(a,1),2819(a,1,1))]. 2892 x -> ((y v x) -> z) = x -> z # label("(4.9)"). [para(2823(a,1),1559(a,1)),flip(a)]. 2893 $F # answer("(4.9)"). [resolve(2892,a,46,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 46 given #87 (H,wt=11): 2892 x -> ((y v x) -> z) = x -> z # label("(4.9)"). [para(2823(a,1),1559(a,1)),flip(a)]. given #88 (H,wt=17): 2233 x => ((x => y) ^ (x => z)) = (x -> z) ^ (x -> y). [para(22(a,1),1983(a,2,2))]. given #89 (H,wt=15): 3028 x => (x => (y ^ z)) = (x -> z) ^ (x -> y). [para(38(a,1),2233(a,1,2))]. given #90 (H,wt=13): 3149 (x -> y) ^ (x -> z) = x -> (z ^ y). [para(3028(a,1),22(a,1))]. given #91 (H,wt=11): 3275 x -> ((x * y) ^ y) = x -> y. [para(3149(a,1),2622(a,1))]. given #92 (H,wt=9): 3312 x -> (x * y) = x -> y. [para(1943(a,1),3275(a,1,2))]. given #93 (H,wt=12): 3360 x -> (y v ~ x) = x -> (y * x). [para(1103(a,1),3312(a,1,2)),flip(a)]. given #94 (H,wt=12): 3411 x -> (y v ~ x) = x -> (x * y). [para(14(a,1),3360(a,2,2))]. given #95 (H,wt=10): 3526 x -> (y v ~ x) = x -> y. [para(3312(a,1),3411(a,2))]. -------- Proof 2 -------- "(4.10)". ============================== PROOF ================================= % Proof 2 at 0.15 (+ 0.00) seconds: "(4.10)". % Length of proof is 70. % Level of proof is 18. % Maximum clause weight is 17. % Given clauses 95. 2 x -> (~ x v y) = x -> y # label("(4.10)") # label(non_clause) # label(goal). [goal]. 5 x v y = y v x # label("(D3)"). [assumption]. 6 x ^ y = y ^ x # label("(D4)"). [assumption]. 7 x v (x ^ y) = x # label("(D5)"). [assumption]. 10 1 => x = x # label("(BCK2)"). [assumption]. 14 x * y = y * x # label("(M2)"). [assumption]. 16 (x * y) => z = x => (y => z) # label("(P)"). [assumption]. 18 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. 21 x -> y = x => (x => y) # label("(-> def)"). [assumption]. 22 x => (x => y) = x -> y. [copy(21),flip(a)]. 23 ~ x = x => 0 # label("(~ def)"). [assumption]. 24 x => 0 = ~ x. [copy(23),flip(a)]. 27 x => (x => (x => y)) = x => (x => y) # label("(E_2)"). [assumption]. 30 ~ ~ x = x # label("(DN)"). [assumption]. 32 (x => y) => ((z => x) => (z => y)) = 1 # label("(BCK1')"). [assumption]. 36 x => (y => z) = y => (x => z) # label("(3.18)"). [assumption]. 38 (x => y) ^ (x => z) = x => (y ^ z) # label("(4.2)"). [assumption]. 40 (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). [assumption]. 41 ((x => y) * z) => (x => (y * z)) = 1 # label("(4.5)"). [assumption]. 42 (x => y) ^ y = y # label("(3.13)"). [assumption]. 43 (x v y) => y = x => y # label("(4.6)"). [assumption]. 44 x -> (y => z) = y => (x -> z) # label("(4.7)"). [assumption]. 47 c4 -> (~ c4 v c5) != c4 -> c5 # label("(4.10)") # answer("(4.10)"). [deny(2)]. 66 (x ^ y) v x = x. [para(7(a,1),5(a,1)),flip(a)]. 149 x => (y => 0) = ~ (x * y). [para(24(a,1),16(a,1)),flip(a)]. 190 x => (x -> y) = x => (x => y). [para(22(a,1),27(a,1,2))]. 379 (x => y) => (z => ((z => x) => y)) = 1. [para(36(a,1),32(a,1,2))]. 431 x => ((x => y) ^ z) = (x -> y) ^ (x => z). [para(22(a,1),38(a,1,1)),flip(a)]. 507 ~ x ^ (y => 0) = (x v y) => 0. [para(24(a,1),40(a,1,1))]. 543 (x * (y => z)) => (y => (z * x)) = 1. [para(14(a,1),41(a,1,1))]. 692 x v (y => x) = y => x. [para(42(a,1),66(a,1,1))]. 763 ~ (x * y) = x => ~ y. [para(24(a,1),149(a,1,2)),flip(a)]. 804 ~ (x => ~ y) = x * y. [para(763(a,1),30(a,1,1))]. 824 (x v ~ y) * y = ~ (x => ~ y). [para(43(a,1),804(a,1,1)),flip(a)]. 844 x => (x -> y) = x -> y. [para(22(a,1),190(a,2))]. 894 x => (y => (x -> z)) = y => (x -> z). [para(844(a,1),36(a,1,2)),flip(a)]. 921 (x v y) => 0 = ~ x ^ ~ y. [para(24(a,1),507(a,1,2)),flip(a)]. 949 ~ x ^ ~ y = ~ (x v y). [para(921(a,1),24(a,1))]. 999 ~ (~ x v y) = x ^ ~ y. [para(30(a,1),949(a,1,1)),flip(a)]. 1012 ~ (x v ~ y) = y ^ ~ x. [para(5(a,1),999(a,1,1))]. 1047 ~ (x v (y => ~ z)) = (y * z) ^ ~ x. [para(763(a,1),1012(a,1,1,2))]. 1094 (x v ~ y) * y = x * y. [para(804(a,1),824(a,2))]. 1103 x * (y v ~ x) = y * x. [para(1094(a,1),14(a,1)),flip(a)]. 1193 x => ((y => z) => ((x => y) => z)) = 1. [para(379(a,1),36(a,1)),flip(a)]. 1258 x => ((y * (x => z)) => (z * y)) = 1. [para(543(a,1),36(a,1)),flip(a)]. 1409 x => (((x => y) => z) => ((x -> y) => z)) = 1. [para(22(a,1),1193(a,1,2,2,1))]. 1493 x => (y => ((x => z) => (z * y))) = 1. [para(16(a,1),1258(a,1,2))]. 1628 x -> ((x => y) => (y * x)) = 1. [para(1493(a,1),22(a,1)),flip(a)]. 1690 x -> ((x => y) => (x * y)) = 1. [para(14(a,1),1628(a,1,2,2))]. 1748 (x => y) => (x -> (x * y)) = 1. [para(1690(a,1),44(a,1)),flip(a)]. 1860 (x * y) ^ ~ ~ y = ~ (x => ~ y). [para(692(a,1),1047(a,1,1)),flip(a)]. 1916 (x * y) ^ ~ ~ y = x * y. [para(804(a,1),1860(a,2))]. 1943 (x * y) ^ y = x * y. [para(30(a,1),1916(a,1,2))]. 1983 x => (y ^ (x => z)) = (x -> z) ^ (x => y). [para(6(a,1),431(a,1,2))]. 2146 x => ((x -> y) => (((x => y) => z) => z)) = 1. [para(36(a,1),1409(a,1,2))]. 2233 x => ((x => y) ^ (x => z)) = (x -> z) ^ (x -> y). [para(22(a,1),1983(a,2,2))]. 2435 x => ((x -> y) => (1 => (x -> (x * y)))) = 1. [para(1748(a,1),2146(a,1,2,2,1))]. 2453 x => ((x -> y) => (x -> (x * y))) = 1. [para(10(a,1),2435(a,1,2,2))]. 2547 (x -> y) => (x -> (x * y)) = 1. [para(2453(a,1),894(a,1)),flip(a)]. 2572 (x -> y) ^ (1 => (x -> (x * y))) = x -> y. [para(2547(a,1),18(a,1,2,1))]. 2622 (x -> y) ^ (x -> (x * y)) = x -> y. [para(10(a,1),2572(a,1,2))]. 3028 x => (x => (y ^ z)) = (x -> z) ^ (x -> y). [para(38(a,1),2233(a,1,2))]. 3149 (x -> y) ^ (x -> z) = x -> (z ^ y). [para(3028(a,1),22(a,1))]. 3275 x -> ((x * y) ^ y) = x -> y. [para(3149(a,1),2622(a,1))]. 3312 x -> (x * y) = x -> y. [para(1943(a,1),3275(a,1,2))]. 3360 x -> (y v ~ x) = x -> (y * x). [para(1103(a,1),3312(a,1,2)),flip(a)]. 3411 x -> (y v ~ x) = x -> (x * y). [para(14(a,1),3360(a,2,2))]. 3526 x -> (y v ~ x) = x -> y. [para(3312(a,1),3411(a,2))]. 3528 x -> (~ x v y) = x -> y # label("(4.10)"). [para(5(a,1),3526(a,1,2))]. 3529 $F # answer("(4.10)"). [resolve(3528,a,47,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=95. Generated=4344. Kept=3522. proofs=2. Usable=96. Sos=3384. Demods=0. Limbo=1, Disabled=82. Hints=100. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=822. Back_subsumed=39. 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=4.86. User_CPU=0.15, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED THEOREM PROVED Exiting with 2 proofs. ------ process 26266 exit (max_proofs) ------  Process 26266 exit (max_proofs) Sat Jan 19 14:18:54 2008