============================== Prover9 =============================== Prover9 (64) version Aug-2007, Aug 2007. Process 26254 was started by veroff on titan, Sat Jan 19 14:18:50 2008 The command was "prover9 -f 4.4.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file 4.4.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). 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(assumptions). A -> ((B v A) -> C) != A -> C | A -> (~ A v B) != A -> B # answer("(Lemma 4.4, 2 parts)"). 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: ============================== 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]. A -> ((B v A) -> C) != A -> C | A -> (~ A v B) != A -> B # answer("(Lemma 4.4, 2 parts)"). [assumption]. end_of_list. formulas(demodulators). end_of_list. WARNING, function symbols not in function_order (lex) command: A, B, C. % 100 hints input. Auto_denials: (no changes). Term ordering decisions: WARNING, function symbols not in function_order (lex) command: A, B, C. Function symbol KB weights: A=1. B=1. C=1. 0=1. 1=1. *=1. ^=1. =>=1. ->=1. v=1. ~=1. -=1. Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ A, B, C, 0, 1, *, ^, =>, ->, 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. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 1 (x v y) v z = x v (y v z) # label("(D1)"). [assumption]. 2 (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)"). [assumption]. 3 x v y = y v x # label("(D3)"). [assumption]. 4 x ^ y = y ^ x # label("(D4)"). [assumption]. 5 x v (x ^ y) = x # label("(D5)"). [assumption]. 6 x ^ (x v y) = x # label("(D6)"). [assumption]. 7 (x => y) => ((y => z) => (x => z)) = 1 # label("(BCK1)"). [assumption]. 8 1 => x = x # label("(BCK2)"). [assumption]. 9 x => 1 = 1 # label("(BCK3)"). [assumption]. 10 x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). [assumption]. 11 x * 1 = x # label("(M1)"). [assumption]. 12 x * y = y * x # label("(M2)"). [assumption]. 13 (x * y) * z = x * (y * z) # label("(M3)"). [assumption]. 14 (x * y) => z = x => (y => z) # label("(P)"). [assumption]. 15 x ^ 1 = x # label("(D10)"). [assumption]. 16 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. 17 (x ^ y) => y = 1 # label("(3.11)"). [assumption]. 18 x v 0 = x # label("(D9)"). [assumption]. 20 x => (x => y) = x -> y. [copy(19),flip(a)]. 22 x => 0 = ~ x. [copy(21),flip(a)]. 24 x => (x => 0) = -x. [copy(23),flip(a)]. 25 x => (x => (x => y)) = x => (x => y) # label("(E_2)"). [assumption]. 26 (x v y) ^ (x v z) = x v (y ^ z) # label("(D7)"). [assumption]. 27 (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D8)"). [assumption]. 28 ~ ~ x = x # label("(DN)"). [assumption]. 29 (x -> y) ^ (~ y -> ~ x) = x => y # label("(N)"). [assumption]. 30 (x => y) => ((z => x) => (z => y)) = 1 # label("(BCK1')"). [assumption]. 31 x => ((x => y) => y) = 1 # label("(BCK5)"). [assumption]. 32 x => x = 1 # label("(3.16)"). [assumption]. 33 x => (y => x) = 1 # label("(3.17)"). [assumption]. 34 x => (y => z) = y => (x => z) # label("(3.18)"). [assumption]. 35 (x * y) v (x * z) = x * (y v z) # label("(4.1)"). [assumption]. 36 (x => y) ^ (x => z) = x => (y ^ z) # label("(4.2)"). [assumption]. 37 (x * (x => y)) v y = y # label("(4.3)"). [assumption]. 38 (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). [assumption]. 39 ((x => y) * z) => (x => (y * z)) = 1 # label("(4.5)"). [assumption]. 40 (x => y) ^ y = y # label("(3.13)"). [assumption]. 41 (x v y) => y = x => y # label("(4.6)"). [assumption]. 42 x -> (y => z) = y => (x -> z) # label("(4.7)"). [assumption]. 43 x ^ (~ x => y) = x # label("(4.8)"). [assumption]. 44 A -> ((B v A) -> C) != A -> C | A -> (~ A v B) != A -> B # answer("(Lemma 4.4, 2 parts)"). [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): 1 (x v y) v z = x v (y v z) # label("(D1)"). [assumption]. given #2 (I,wt=11): 2 (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)"). [assumption]. given #3 (I,wt=7): 3 x v y = y v x # label("(D3)"). [assumption]. given #4 (I,wt=7): 4 x ^ y = y ^ x # label("(D4)"). [assumption]. given #5 (I,wt=7): 5 x v (x ^ y) = x # label("(D5)"). [assumption]. given #6 (I,wt=7): 6 x ^ (x v y) = x # label("(D6)"). [assumption]. given #7 (I,wt=13): 7 (x => y) => ((y => z) => (x => z)) = 1 # label("(BCK1)"). [assumption]. given #8 (I,wt=5): 8 1 => x = x # label("(BCK2)"). [assumption]. given #9 (I,wt=5): 9 x => 1 = 1 # label("(BCK3)"). [assumption]. given #10 (I,wt=13): 10 x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). [assumption]. given #11 (I,wt=5): 11 x * 1 = x # label("(M1)"). [assumption]. given #12 (I,wt=7): 12 x * y = y * x # label("(M2)"). [assumption]. given #13 (I,wt=11): 13 (x * y) * z = x * (y * z) # label("(M3)"). [assumption]. given #14 (I,wt=11): 14 (x * y) => z = x => (y => z) # label("(P)"). [assumption]. given #15 (I,wt=5): 15 x ^ 1 = x # label("(D10)"). [assumption]. given #16 (I,wt=9): 16 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. given #17 (I,wt=7): 17 (x ^ y) => y = 1 # label("(3.11)"). [assumption]. given #18 (I,wt=5): 18 x v 0 = x # label("(D9)"). [assumption]. given #19 (I,wt=9): 20 x => (x => y) = x -> y. [copy(19),flip(a)]. given #20 (I,wt=6): 22 x => 0 = ~ x. [copy(21),flip(a)]. given #21 (I,wt=8): 24 x => (x => 0) = -x. [copy(23),flip(a)]. given #22 (I,wt=13): 25 x => (x => (x => y)) = x => (x => y) # label("(E_2)"). [assumption]. given #23 (I,wt=13): 26 (x v y) ^ (x v z) = x v (y ^ z) # label("(D7)"). [assumption]. given #24 (I,wt=13): 27 (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D8)"). [assumption]. given #25 (I,wt=5): 28 ~ ~ x = x # label("(DN)"). [assumption]. given #26 (I,wt=13): 29 (x -> y) ^ (~ y -> ~ x) = x => y # label("(N)"). [assumption]. given #27 (I,wt=13): 30 (x => y) => ((z => x) => (z => y)) = 1 # label("(BCK1')"). [assumption]. given #28 (I,wt=9): 31 x => ((x => y) => y) = 1 # label("(BCK5)"). [assumption]. given #29 (I,wt=5): 32 x => x = 1 # label("(3.16)"). [assumption]. given #30 (I,wt=7): 33 x => (y => x) = 1 # label("(3.17)"). [assumption]. given #31 (I,wt=11): 34 x => (y => z) = y => (x => z) # label("(3.18)"). [assumption]. given #32 (I,wt=13): 35 (x * y) v (x * z) = x * (y v z) # label("(4.1)"). [assumption]. given #33 (I,wt=13): 36 (x => y) ^ (x => z) = x => (y ^ z) # label("(4.2)"). [assumption]. given #34 (I,wt=9): 37 (x * (x => y)) v y = y # label("(4.3)"). [assumption]. given #35 (I,wt=13): 38 (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). [assumption]. given #36 (I,wt=13): 39 ((x => y) * z) => (x => (y * z)) = 1 # label("(4.5)"). [assumption]. given #37 (I,wt=7): 40 (x => y) ^ y = y # label("(3.13)"). [assumption]. given #38 (I,wt=9): 41 (x v y) => y = x => y # label("(4.6)"). [assumption]. given #39 (I,wt=11): 42 x -> (y => z) = y => (x -> z) # label("(4.7)"). [assumption]. given #40 (I,wt=8): 43 x ^ (~ x => y) = x # label("(4.8)"). [assumption]. given #41 (I,wt=21): 44 A -> ((B v A) -> C) != A -> C | A -> (~ A v B) != A -> B # answer("(Lemma 4.4, 2 parts)"). [assumption]. given #42 (H,wt=7): 63 (x ^ y) v x = x. [para(5(a,1),3(a,1)),flip(a)]. given #43 (H,wt=7): 576 x ^ (y => x) = x. [para(40(a,1),4(a,1)),flip(a)]. given #44 (H,wt=9): 689 x v (y => x) = y => x. [para(40(a,1),63(a,1,1))]. given #45 (H,wt=10): 146 x => (y => 0) = ~ (x * y). [para(22(a,1),14(a,1)),flip(a)]. given #46 (H,wt=9): 760 ~ (x * y) = x => ~ y. [para(22(a,1),146(a,1,2)),flip(a)]. given #47 (H,wt=9): 801 ~ (x => ~ y) = x * y. [para(760(a,1),28(a,1,1))]. given #48 (H,wt=11): 187 x => (x -> y) = x => (x => y). [para(20(a,1),25(a,1,2))]. given #49 (H,wt=9): 841 x => (x -> y) = x -> y. [para(20(a,1),187(a,2))]. given #50 (H,wt=12): 504 ~ x ^ (y => 0) = (x v y) => 0. [para(22(a,1),38(a,1,1))]. given #51 (H,wt=11): 918 (x v y) => 0 = ~ x ^ ~ y. [para(22(a,1),504(a,1,2)),flip(a)]. given #52 (H,wt=10): 946 ~ x ^ ~ y = ~ (x v y). [para(918(a,1),22(a,1))]. given #53 (H,wt=10): 996 ~ (~ x v y) = x ^ ~ y. [para(28(a,1),946(a,1,1)),flip(a)]. given #54 (H,wt=10): 1009 ~ (x v ~ y) = y ^ ~ x. [para(3(a,1),996(a,1,1))]. given #55 (H,wt=12): 821 (x v ~ y) * y = ~ (x => ~ y). [para(41(a,1),801(a,1,1)),flip(a)]. given #56 (H,wt=10): 1091 (x v ~ y) * y = x * y. [para(801(a,1),821(a,2))]. given #57 (H,wt=10): 1100 x * (y v ~ x) = y * x. [para(1091(a,1),12(a,1)),flip(a)]. given #58 (H,wt=13): 376 (x => y) => (z => ((z => x) => y)) = 1. [para(34(a,1),30(a,1,2))]. given #59 (H,wt=13): 540 (x * (y => z)) => (y => (z * x)) = 1. [para(12(a,1),39(a,1,1))]. given #60 (H,wt=13): 643 x => (y -> (x => z)) = y -> (x -> z). [para(20(a,1),42(a,1,2)),flip(a)]. given #61 (H,wt=13): 891 x => (y => (x -> z)) = y => (x -> z). [para(841(a,1),34(a,1,2)),flip(a)]. given #62 (H,wt=13): 1190 x => ((y => z) => ((x => y) => z)) = 1. [para(376(a,1),34(a,1)),flip(a)]. given #63 (H,wt=13): 1255 x => ((y * (x => z)) => (z * y)) = 1. [para(540(a,1),34(a,1)),flip(a)]. given #64 (H,wt=13): 1327 x => (x => (y -> z)) = y -> (x -> z). [para(42(a,1),643(a,1,2))]. given #65 (H,wt=11): 1556 x -> (y -> z) = y -> (x -> z). [para(1327(a,1),20(a,1))]. given #66 (H,wt=13): 1490 x => (y => ((x => z) => (z * y))) = 1. [para(14(a,1),1255(a,1,2))]. given #67 (H,wt=11): 1625 x -> ((x => y) => (y * x)) = 1. [para(1490(a,1),20(a,1)),flip(a)]. given #68 (H,wt=11): 1687 x -> ((x => y) => (x * y)) = 1. [para(12(a,1),1625(a,1,2,2))]. given #69 (H,wt=11): 1745 (x => y) => (x -> (x * y)) = 1. [para(1687(a,1),42(a,1)),flip(a)]. given #70 (H,wt=14): 1044 ~ (x v (y => ~ z)) = (y * z) ^ ~ x. [para(760(a,1),1009(a,1,1,2))]. given #71 (H,wt=13): 1857 (x * y) ^ ~ ~ y = ~ (x => ~ y). [para(689(a,1),1044(a,1,1)),flip(a)]. given #72 (H,wt=11): 1913 (x * y) ^ ~ ~ y = x * y. [para(801(a,1),1857(a,2))]. given #73 (H,wt=9): 1940 (x * y) ^ y = x * y. [para(28(a,1),1913(a,1,2))]. given #74 (H,wt=15): 428 x => ((x => y) ^ z) = (x -> y) ^ (x => z). [para(20(a,1),36(a,1,1)),flip(a)]. given #75 (H,wt=15): 1406 x => (((x => y) => z) => ((x -> y) => z)) = 1. [para(20(a,1),1190(a,1,2,2,1))]. given #76 (H,wt=15): 1980 x => (y ^ (x => z)) = (x -> z) ^ (x => y). [para(4(a,1),428(a,1,2))]. given #77 (H,wt=15): 2143 x => ((x -> y) => (((x => y) => z) => z)) = 1. [para(34(a,1),1406(a,1,2))]. given #78 (H,wt=15): 2432 x => ((x -> y) => (1 => (x -> (x * y)))) = 1. [para(1745(a,1),2143(a,1,2,2,1))]. given #79 (H,wt=13): 2450 x => ((x -> y) => (x -> (x * y))) = 1. [para(8(a,1),2432(a,1,2,2))]. given #80 (H,wt=11): 2544 (x -> y) => (x -> (x * y)) = 1. [para(2450(a,1),891(a,1)),flip(a)]. given #81 (H,wt=15): 2569 (x -> y) ^ (1 => (x -> (x * y))) = x -> y. [para(2544(a,1),16(a,1,2,1))]. given #82 (H,wt=13): 2619 (x -> y) ^ (x -> (x * y)) = x -> y. [para(8(a,1),2569(a,1,2))]. given #83 (H,wt=17): 895 (x -> y) ^ (z => (x -> y)) = (x v z) => (x -> y). [para(841(a,1),38(a,1,1))]. given #84 (H,wt=11): 2691 (x v y) => (x -> z) = x -> z. [para(895(a,1),576(a,1))]. given #85 (H,wt=15): 2718 (x v y) -> (x -> z) = (x v y) => (x -> z). [para(2691(a,1),20(a,1,2)),flip(a)]. given #86 (H,wt=11): 2816 (x v y) -> (x -> z) = x -> z. [para(2691(a,1),2718(a,2))]. given #87 (H,wt=11): 2820 (x v y) -> (y -> z) = y -> z. [para(3(a,1),2816(a,1,1))]. given #88 (H,wt=11): 2889 x -> ((y v x) -> z) = x -> z # label("(4.9)"). [para(2820(a,1),1556(a,1)),flip(a)]. given #89 (H,wt=17): 2230 x => ((x => y) ^ (x => z)) = (x -> z) ^ (x -> y). [para(20(a,1),1980(a,2,2))]. given #90 (H,wt=15): 3024 x => (x => (y ^ z)) = (x -> z) ^ (x -> y). [para(36(a,1),2230(a,1,2))]. given #91 (H,wt=13): 3145 (x -> y) ^ (x -> z) = x -> (z ^ y). [para(3024(a,1),20(a,1))]. given #92 (H,wt=11): 3271 x -> ((x * y) ^ y) = x -> y. [para(3145(a,1),2619(a,1))]. given #93 (H,wt=9): 3308 x -> (x * y) = x -> y. [para(1940(a,1),3271(a,1,2))]. given #94 (H,wt=12): 3356 x -> (y v ~ x) = x -> (y * x). [para(1100(a,1),3308(a,1,2)),flip(a)]. given #95 (H,wt=12): 3407 x -> (y v ~ x) = x -> (x * y). [para(12(a,1),3356(a,2,2))]. given #96 (H,wt=10): 3522 x -> (y v ~ x) = x -> y. [para(3308(a,1),3407(a,2))]. given #97 (H,wt=10): 3524 x -> (~ x v y) = x -> y # label("(4.10)"). [para(3(a,1),3522(a,1,2))]. -------- Proof 1 -------- "(Lemma 4.4, 2 parts)". ============================== PROOF ================================= % Proof 1 at 0.13 (+ 0.01) seconds: "(Lemma 4.4, 2 parts)". % Length of proof is 79. % Level of proof is 18. % Maximum clause weight is 21. % Given clauses 97. 3 x v y = y v x # label("(D3)"). [assumption]. 4 x ^ y = y ^ x # label("(D4)"). [assumption]. 5 x v (x ^ y) = x # label("(D5)"). [assumption]. 8 1 => x = x # label("(BCK2)"). [assumption]. 12 x * y = y * x # label("(M2)"). [assumption]. 14 (x * y) => z = x => (y => z) # label("(P)"). [assumption]. 16 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. 19 x -> y = x => (x => y) # label("(-> def)"). [assumption]. 20 x => (x => y) = x -> y. [copy(19),flip(a)]. 21 ~ x = x => 0 # label("(~ def)"). [assumption]. 22 x => 0 = ~ x. [copy(21),flip(a)]. 25 x => (x => (x => y)) = x => (x => y) # label("(E_2)"). [assumption]. 28 ~ ~ x = x # label("(DN)"). [assumption]. 30 (x => y) => ((z => x) => (z => y)) = 1 # label("(BCK1')"). [assumption]. 34 x => (y => z) = y => (x => z) # label("(3.18)"). [assumption]. 36 (x => y) ^ (x => z) = x => (y ^ z) # label("(4.2)"). [assumption]. 38 (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). [assumption]. 39 ((x => y) * z) => (x => (y * z)) = 1 # label("(4.5)"). [assumption]. 40 (x => y) ^ y = y # label("(3.13)"). [assumption]. 41 (x v y) => y = x => y # label("(4.6)"). [assumption]. 42 x -> (y => z) = y => (x -> z) # label("(4.7)"). [assumption]. 44 A -> ((B v A) -> C) != A -> C | A -> (~ A v B) != A -> B # answer("(Lemma 4.4, 2 parts)"). [assumption]. 63 (x ^ y) v x = x. [para(5(a,1),3(a,1)),flip(a)]. 146 x => (y => 0) = ~ (x * y). [para(22(a,1),14(a,1)),flip(a)]. 187 x => (x -> y) = x => (x => y). [para(20(a,1),25(a,1,2))]. 376 (x => y) => (z => ((z => x) => y)) = 1. [para(34(a,1),30(a,1,2))]. 428 x => ((x => y) ^ z) = (x -> y) ^ (x => z). [para(20(a,1),36(a,1,1)),flip(a)]. 504 ~ x ^ (y => 0) = (x v y) => 0. [para(22(a,1),38(a,1,1))]. 540 (x * (y => z)) => (y => (z * x)) = 1. [para(12(a,1),39(a,1,1))]. 576 x ^ (y => x) = x. [para(40(a,1),4(a,1)),flip(a)]. 643 x => (y -> (x => z)) = y -> (x -> z). [para(20(a,1),42(a,1,2)),flip(a)]. 689 x v (y => x) = y => x. [para(40(a,1),63(a,1,1))]. 760 ~ (x * y) = x => ~ y. [para(22(a,1),146(a,1,2)),flip(a)]. 801 ~ (x => ~ y) = x * y. [para(760(a,1),28(a,1,1))]. 821 (x v ~ y) * y = ~ (x => ~ y). [para(41(a,1),801(a,1,1)),flip(a)]. 841 x => (x -> y) = x -> y. [para(20(a,1),187(a,2))]. 891 x => (y => (x -> z)) = y => (x -> z). [para(841(a,1),34(a,1,2)),flip(a)]. 895 (x -> y) ^ (z => (x -> y)) = (x v z) => (x -> y). [para(841(a,1),38(a,1,1))]. 918 (x v y) => 0 = ~ x ^ ~ y. [para(22(a,1),504(a,1,2)),flip(a)]. 946 ~ x ^ ~ y = ~ (x v y). [para(918(a,1),22(a,1))]. 996 ~ (~ x v y) = x ^ ~ y. [para(28(a,1),946(a,1,1)),flip(a)]. 1009 ~ (x v ~ y) = y ^ ~ x. [para(3(a,1),996(a,1,1))]. 1044 ~ (x v (y => ~ z)) = (y * z) ^ ~ x. [para(760(a,1),1009(a,1,1,2))]. 1091 (x v ~ y) * y = x * y. [para(801(a,1),821(a,2))]. 1100 x * (y v ~ x) = y * x. [para(1091(a,1),12(a,1)),flip(a)]. 1190 x => ((y => z) => ((x => y) => z)) = 1. [para(376(a,1),34(a,1)),flip(a)]. 1255 x => ((y * (x => z)) => (z * y)) = 1. [para(540(a,1),34(a,1)),flip(a)]. 1327 x => (x => (y -> z)) = y -> (x -> z). [para(42(a,1),643(a,1,2))]. 1406 x => (((x => y) => z) => ((x -> y) => z)) = 1. [para(20(a,1),1190(a,1,2,2,1))]. 1490 x => (y => ((x => z) => (z * y))) = 1. [para(14(a,1),1255(a,1,2))]. 1556 x -> (y -> z) = y -> (x -> z). [para(1327(a,1),20(a,1))]. 1625 x -> ((x => y) => (y * x)) = 1. [para(1490(a,1),20(a,1)),flip(a)]. 1687 x -> ((x => y) => (x * y)) = 1. [para(12(a,1),1625(a,1,2,2))]. 1745 (x => y) => (x -> (x * y)) = 1. [para(1687(a,1),42(a,1)),flip(a)]. 1857 (x * y) ^ ~ ~ y = ~ (x => ~ y). [para(689(a,1),1044(a,1,1)),flip(a)]. 1913 (x * y) ^ ~ ~ y = x * y. [para(801(a,1),1857(a,2))]. 1940 (x * y) ^ y = x * y. [para(28(a,1),1913(a,1,2))]. 1980 x => (y ^ (x => z)) = (x -> z) ^ (x => y). [para(4(a,1),428(a,1,2))]. 2143 x => ((x -> y) => (((x => y) => z) => z)) = 1. [para(34(a,1),1406(a,1,2))]. 2230 x => ((x => y) ^ (x => z)) = (x -> z) ^ (x -> y). [para(20(a,1),1980(a,2,2))]. 2432 x => ((x -> y) => (1 => (x -> (x * y)))) = 1. [para(1745(a,1),2143(a,1,2,2,1))]. 2450 x => ((x -> y) => (x -> (x * y))) = 1. [para(8(a,1),2432(a,1,2,2))]. 2544 (x -> y) => (x -> (x * y)) = 1. [para(2450(a,1),891(a,1)),flip(a)]. 2569 (x -> y) ^ (1 => (x -> (x * y))) = x -> y. [para(2544(a,1),16(a,1,2,1))]. 2619 (x -> y) ^ (x -> (x * y)) = x -> y. [para(8(a,1),2569(a,1,2))]. 2691 (x v y) => (x -> z) = x -> z. [para(895(a,1),576(a,1))]. 2718 (x v y) -> (x -> z) = (x v y) => (x -> z). [para(2691(a,1),20(a,1,2)),flip(a)]. 2816 (x v y) -> (x -> z) = x -> z. [para(2691(a,1),2718(a,2))]. 2820 (x v y) -> (y -> z) = y -> z. [para(3(a,1),2816(a,1,1))]. 2889 x -> ((y v x) -> z) = x -> z # label("(4.9)"). [para(2820(a,1),1556(a,1)),flip(a)]. 3024 x => (x => (y ^ z)) = (x -> z) ^ (x -> y). [para(36(a,1),2230(a,1,2))]. 3145 (x -> y) ^ (x -> z) = x -> (z ^ y). [para(3024(a,1),20(a,1))]. 3271 x -> ((x * y) ^ y) = x -> y. [para(3145(a,1),2619(a,1))]. 3308 x -> (x * y) = x -> y. [para(1940(a,1),3271(a,1,2))]. 3356 x -> (y v ~ x) = x -> (y * x). [para(1100(a,1),3308(a,1,2)),flip(a)]. 3407 x -> (y v ~ x) = x -> (x * y). [para(12(a,1),3356(a,2,2))]. 3522 x -> (y v ~ x) = x -> y. [para(3308(a,1),3407(a,2))]. 3524 x -> (~ x v y) = x -> y # label("(4.10)"). [para(3(a,1),3522(a,1,2))]. 3589 $F # answer("(Lemma 4.4, 2 parts)"). [hyper(44,a,2889,a,b,3524,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=97. Generated=4414. Kept=3585. proofs=1. Usable=97. Sos=3449. Demods=0. Limbo=0, Disabled=80. Hints=100. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=828. 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=2. Megabytes=4.93. User_CPU=0.13, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED THEOREM PROVED Exiting with 1 proof. ------ process 26254 exit (max_proofs) ------  Process 26254 exit (max_proofs) Sat Jan 19 14:18:50 2008