============================== Prover9 =============================== Prover9 (64) version Aug-2007, Aug 2007. Process 32388 was started by veroff on io, Mon Jan 21 11:14:45 2008 The command was "prover9 -f 3.3.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file 3.3.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 v y) ^ (x v z) = x v (y ^ z) # label("(D7)"). (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D8)"). x v 0 = x # label("(D9)"). x ^ 1 = x # label("(D10)"). x ^ 0 = 0 # label("(2.1)"). ~ x v ~ y = ~ (x ^ y) # label("(DM1)"). ~ x ^ ~ y = ~ (x v y) # label("(DM2)"). ~ ~ x = x # label("(DN)"). ~ 1 = 0 # label("(2.2)"). (x ^ ~ x) ^ (y v ~ y) = x ^ ~ x # label("(N1)"). x -> x = 1 # label("(N2)"). (x -> y) ^ (~ x v y) = ~ x v y # label("(N3)"). x ^ (~ x v y) = x ^ (x -> y) # label("(N4)"). (x -> y) ^ (x -> z) = x -> (y ^ z) # label("(N5)"). (x ^ y) -> z = x -> (y -> z) # label("(N6)"). -x = x -> 0 # label("(N7)"). x * y = ~ (x -> ~ y) v ~ (y -> ~ x) # label("(* def)"). x => y = (x -> y) ^ (~ y -> ~ x) # label("(=> def)"). x -> 1 = 1 # label("(3.1)"). 1 -> x = x # label("(3.2)"). (x -> y) -> (x -> z) = x -> (y -> z) # label("(3.3)"). x -> (y -> z) = y -> (x -> z) # label("(3.4)"). x -> (x -> y) = x -> y # label("(3.5)"). (x -> y) ^ (z -> y) = (x v z) -> y # label("(3.6)"). x ^ ((x => y) => y) = x # label("(3.7)"). x -> ~ (x -> y) = x -> ~ y # label("(3.8)"). ~ (x -> y) -> z = x -> (~ y -> z) # label("(3.9)"). 1 => x = x # label("(BCK2)"). x => 1 = 1 # label("(BCK3)"). x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). end_of_list. formulas(assumptions). (x ^ y) -> y = 1 # label("(3.10)"). (x ^ y) => y = 1 # label("(3.11)"). ~ x => ~ y = y => x # label("(3.12)"). (x => y) ^ y = y # label("(3.13)"). x => (x ^ y) = x => y # label("(3.14)"). x => (x => y) = x -> y # label("(3.15)"). end_of_list. formulas(goals). (x => y) => ((z => x) => (z => y)) = 1 # label("(BCK1')"). end_of_list. formulas(hints). x = (x ^ y) v x. (x ^ y) v x = x. x v (y ^ x) = x. x ^ (y v x) = x. ~ (x v y) -> z = ~ x -> (~ y -> z). ~ x -> (~ y -> z) = ~ (x v y) -> z. (x -> (y -> z)) ^ (x -> (~ z -> ~ y)) = x -> (y => z). x -> (y -> y) = 1. (x -> (y -> z)) ^ (~ (x -> z) -> ~ y) = y => (x -> z). x ^ y = x ^ (((x => z) => z) ^ y). x ^ (((x => y) => y) ^ z) = x ^ z. (x ^ (y ^ z)) => z = 1. (x ^ y) => x = 1. x = x ^ (y => x). x ^ (y => x) = x. x => (x -> y) = x -> (x => y). x -> (x => y) = x => (x -> y). x v (y => x) = y => x. (x -> y) v (x -> (z ^ y)) = x -> y. x -> (y v x) = 1. 1 = x -> (y -> x). x -> (y -> x) = 1. (x => y) => (x -> y) = 1. x => (y => x) = 1. ~ x -> ~ (y ^ x) = 1. (x ^ y) => (z v y) = 1. (x => (x -> y)) => (x -> y) = 1. x -> 1 = ~ y -> (x -> ~ (z ^ y)). ~ x -> (y -> ~ (z ^ x)) = y -> 1. (x => y) => y != 1 | y = x => y. x -> y = x => (x -> y). x => (x -> y) = x -> y. x -> (x => y) = x -> y. x -> ~ (x -> y) = x -> ~ (x => y). ~ x -> (y => x) = ~ x -> ~ y. ~ (~ x -> ~ y) -> z = ~ x -> (~ (y => x) -> z). ~ x -> (~ (y => x) -> z) = ~ (~ x -> ~ y) -> z. x ^ ((x => y) => y) = x ^ (z => ((x => y) => y)). x ^ (y => ((x => z) => z)) = x ^ ((x => z) => z). ~ x -> (y -> ~ (z ^ x)) = 1. x -> ~ (x => y) = x -> ~ y. x -> ~ (x => ~ y) = x -> y. ~ (x -> ~ y) -> z = x -> (~ ~ (x => y) -> z). x -> (~ ~ (x => y) -> z) = ~ (x -> ~ y) -> z. ~ x -> ~ (y => x) = ~ x -> y. x ^ (y => ((x => z) => z)) = x. x ^ ((x => y) -> y) = x. x => (y v ((x => z) -> z)) = 1. x => ((x => (y ^ z)) -> z) = 1. x -> (~ ~ (x => y) -> z) = x -> (~ ~ y -> z). x -> (~ ~ (x => y) -> z) = x -> (y -> z). x -> ((x => y) -> z) = x -> (y -> z). ~ x -> (~ (y => x) -> z) = ~ x -> (~ ~ y -> z). ~ x -> (~ (y => x) -> z) = ~ x -> (y -> z). ~ x -> (y -> z) = ~ (x v (y => x)) -> z. ~ (x v (y => x)) -> z = ~ x -> (y -> z). ~ (x => y) -> z = ~ y -> (x -> z). ~ (x => y) -> z = x -> (~ y -> z). (x -> (y -> z)) ^ (x -> (~ z -> ~ y)) = y => (x -> z). x => (y -> z) = y -> (x => z). x -> (y => z) = y => (x -> z). (x => (y -> z)) ^ (~ (x => z) -> ~ y) = y => (x => z). (x => (y ^ z)) -> (x => z) = 1. 1 ^ (~ (x => y) -> ~ (x => (z ^ y))) = (x => (z ^ y)) => (x => y). (x => (y -> z)) ^ (x -> (~ z -> ~ y)) = y => (x => z). (x => (y => (z -> u))) ^ (x -> (~ (y => u) -> ~ z)) = z => (x => (y => u)). 1 ^ (~ x -> (y -> ~ (y => (z ^ x)))) = (y => (z ^ x)) => (y => x). 1 ^ (~ x -> (y -> ~ (z ^ x))) = (y => (z ^ x)) => (y => x). (x => (y ^ z)) => (x => z) = 1 ^ (~ z -> (x -> ~ (y ^ z))). (x => (y ^ z)) => (x => z) = 1 ^ 1. (x => (y ^ z)) => (x => z) = 1. (x => y) => (x => ((y => z) -> z)) = 1. (x => (y => (z -> u))) ^ (x -> (y -> (~ u -> ~ z))) = z => (x => (y => u)). 1 ^ ((x => y) -> (x -> (~ z -> ~ (y => z)))) = (y => z) => ((x => y) => (x => z)). 1 ^ ((x => y) -> (x -> (~ z -> y))) = (y => z) => ((x => y) => (x => z)). (x => y) => ((z => x) => (z => y)) = 1 ^ ((z => x) -> (z -> (~ y -> x))). (x => y) => ((z => x) => (z => y)) = 1 ^ (z -> ((z => x) -> (~ y -> x))). (x => y) => ((z => x) => (z => y)) = 1 ^ (z -> (x -> (~ y -> x))). (x => y) => ((z => x) => (z => y)) = 1 ^ (z -> 1). 1 ^ (x -> 1) = 1. end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (x => y) => ((z => x) => (z => y)) = 1 # label("(BCK1')") # 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 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 v 0 = x # label("(D9)"). [assumption]. x ^ 1 = x # label("(D10)"). [assumption]. x ^ 0 = 0 # label("(2.1)"). [assumption]. ~ x v ~ y = ~ (x ^ y) # label("(DM1)"). [assumption]. ~ x ^ ~ y = ~ (x v y) # label("(DM2)"). [assumption]. ~ ~ x = x # label("(DN)"). [assumption]. ~ 1 = 0 # label("(2.2)"). [assumption]. (x ^ ~ x) ^ (y v ~ y) = x ^ ~ x # label("(N1)"). [assumption]. x -> x = 1 # label("(N2)"). [assumption]. (x -> y) ^ (~ x v y) = ~ x v y # label("(N3)"). [assumption]. x ^ (~ x v y) = x ^ (x -> y) # label("(N4)"). [assumption]. (x -> y) ^ (x -> z) = x -> (y ^ z) # label("(N5)"). [assumption]. (x ^ y) -> z = x -> (y -> z) # label("(N6)"). [assumption]. -x = x -> 0 # label("(N7)"). [assumption]. x * y = ~ (x -> ~ y) v ~ (y -> ~ x) # label("(* def)"). [assumption]. x => y = (x -> y) ^ (~ y -> ~ x) # label("(=> def)"). [assumption]. x -> 1 = 1 # label("(3.1)"). [assumption]. 1 -> x = x # label("(3.2)"). [assumption]. (x -> y) -> (x -> z) = x -> (y -> z) # label("(3.3)"). [assumption]. x -> (y -> z) = y -> (x -> z) # label("(3.4)"). [assumption]. x -> (x -> y) = x -> y # label("(3.5)"). [assumption]. (x -> y) ^ (z -> y) = (x v z) -> y # label("(3.6)"). [assumption]. x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. x -> ~ (x -> y) = x -> ~ y # label("(3.8)"). [assumption]. ~ (x -> y) -> z = x -> (~ y -> z) # label("(3.9)"). [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 ^ y) -> y = 1 # label("(3.10)"). [assumption]. (x ^ y) => y = 1 # label("(3.11)"). [assumption]. ~ x => ~ y = y => x # label("(3.12)"). [assumption]. (x => y) ^ y = y # label("(3.13)"). [assumption]. x => (x ^ y) = x => y # label("(3.14)"). [assumption]. x => (x => y) = x -> y # label("(3.15)"). [assumption]. (c1 => c2) => ((c3 => c1) => (c3 => c2)) != 1 # label("(BCK1')"). [deny(1)]. end_of_list. formulas(demodulators). end_of_list. % 80 hints input. Auto_denials: % copying label "(BCK1')" to answer in negative clause Term ordering decisions: Function symbol KB weights: 0=1. 1=1. c1=1. c2=1. c3=1. *=1. ^=1. =>=1. ->=1. v=1. ~=1. -=1. Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ 0, 1, c1, c2, c3, *, ^, =>, ->, 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. restricted denial: (wt=13): 47 (c1 => c2) => ((c3 => c1) => (c3 => c2)) != 1 # label("(BCK1')") # answer("(BCK1')"). [deny(1)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 47 (c1 => c2) => ((c3 => c1) => (c3 => c2)) != 1 # label("(BCK1')") # answer("(BCK1')"). [deny(1)]. end_of_list. formulas(sos). 2 (x v y) v z = x v (y v z) # label("(D1)"). [assumption]. 3 (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)"). [assumption]. 4 x v y = y v x # label("(D3)"). [assumption]. 5 x ^ y = y ^ x # label("(D4)"). [assumption]. 6 x v (x ^ y) = x # label("(D5)"). [assumption]. 7 x ^ (x v y) = x # label("(D6)"). [assumption]. 8 (x v y) ^ (x v z) = x v (y ^ z) # label("(D7)"). [assumption]. 9 (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D8)"). [assumption]. 10 x v 0 = x # label("(D9)"). [assumption]. 11 x ^ 1 = x # label("(D10)"). [assumption]. 12 x ^ 0 = 0 # label("(2.1)"). [assumption]. 13 ~ x v ~ y = ~ (x ^ y) # label("(DM1)"). [assumption]. 14 ~ x ^ ~ y = ~ (x v y) # label("(DM2)"). [assumption]. 15 ~ ~ x = x # label("(DN)"). [assumption]. 16 ~ 1 = 0 # label("(2.2)"). [assumption]. 17 (x ^ ~ x) ^ (y v ~ y) = x ^ ~ x # label("(N1)"). [assumption]. 18 x -> x = 1 # label("(N2)"). [assumption]. 19 (x -> y) ^ (~ x v y) = ~ x v y # label("(N3)"). [assumption]. 20 x ^ (~ x v y) = x ^ (x -> y) # label("(N4)"). [assumption]. 21 (x -> y) ^ (x -> z) = x -> (y ^ z) # label("(N5)"). [assumption]. 22 (x ^ y) -> z = x -> (y -> z) # label("(N6)"). [assumption]. 24 x -> 0 = -x. [copy(23),flip(a)]. 26 ~ (x -> ~ y) v ~ (y -> ~ x) = x * y. [copy(25),flip(a)]. 28 (x -> y) ^ (~ y -> ~ x) = x => y. [copy(27),flip(a)]. 29 x -> 1 = 1 # label("(3.1)"). [assumption]. 30 1 -> x = x # label("(3.2)"). [assumption]. 31 (x -> y) -> (x -> z) = x -> (y -> z) # label("(3.3)"). [assumption]. 32 x -> (y -> z) = y -> (x -> z) # label("(3.4)"). [assumption]. 33 x -> (x -> y) = x -> y # label("(3.5)"). [assumption]. 34 (x -> y) ^ (z -> y) = (x v z) -> y # label("(3.6)"). [assumption]. 35 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. 36 x -> ~ (x -> y) = x -> ~ y # label("(3.8)"). [assumption]. 37 ~ (x -> y) -> z = x -> (~ y -> z) # label("(3.9)"). [assumption]. 38 1 => x = x # label("(BCK2)"). [assumption]. 39 x => 1 = 1 # label("(BCK3)"). [assumption]. 40 x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). [assumption]. 41 (x ^ y) -> y = 1 # label("(3.10)"). [assumption]. 42 (x ^ y) => y = 1 # label("(3.11)"). [assumption]. 43 ~ x => ~ y = y => x # label("(3.12)"). [assumption]. 44 (x => y) ^ y = y # label("(3.13)"). [assumption]. 45 x => (x ^ y) = x => y # label("(3.14)"). [assumption]. 46 x => (x => y) = x -> y # label("(3.15)"). [assumption]. end_of_list. formulas(demodulators). end_of_list. % 80 hints processed (15 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=11): 2 (x v y) v z = x v (y v z) # label("(D1)"). [assumption]. given #2 (I,wt=11): 3 (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)"). [assumption]. given #3 (I,wt=7): 4 x v y = y v x # label("(D3)"). [assumption]. given #4 (I,wt=7): 5 x ^ y = y ^ x # label("(D4)"). [assumption]. given #5 (I,wt=7): 6 x v (x ^ y) = x # label("(D5)"). [assumption]. given #6 (I,wt=7): 7 x ^ (x v y) = x # label("(D6)"). [assumption]. given #7 (I,wt=13): 8 (x v y) ^ (x v z) = x v (y ^ z) # label("(D7)"). [assumption]. given #8 (I,wt=13): 9 (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D8)"). [assumption]. given #9 (I,wt=5): 10 x v 0 = x # label("(D9)"). [assumption]. given #10 (I,wt=5): 11 x ^ 1 = x # label("(D10)"). [assumption]. given #11 (I,wt=5): 12 x ^ 0 = 0 # label("(2.1)"). [assumption]. given #12 (I,wt=10): 13 ~ x v ~ y = ~ (x ^ y) # label("(DM1)"). [assumption]. given #13 (I,wt=10): 14 ~ x ^ ~ y = ~ (x v y) # label("(DM2)"). [assumption]. given #14 (I,wt=5): 15 ~ ~ x = x # label("(DN)"). [assumption]. given #15 (I,wt=4): 16 ~ 1 = 0 # label("(2.2)"). [assumption]. given #16 (I,wt=14): 17 (x ^ ~ x) ^ (y v ~ y) = x ^ ~ x # label("(N1)"). [assumption]. given #17 (I,wt=5): 18 x -> x = 1 # label("(N2)"). [assumption]. given #18 (I,wt=13): 19 (x -> y) ^ (~ x v y) = ~ x v y # label("(N3)"). [assumption]. given #19 (I,wt=12): 20 x ^ (~ x v y) = x ^ (x -> y) # label("(N4)"). [assumption]. given #20 (I,wt=13): 21 (x -> y) ^ (x -> z) = x -> (y ^ z) # label("(N5)"). [assumption]. given #21 (I,wt=11): 22 (x ^ y) -> z = x -> (y -> z) # label("(N6)"). [assumption]. given #22 (I,wt=6): 24 x -> 0 = -x. [copy(23),flip(a)]. given #23 (I,wt=15): 26 ~ (x -> ~ y) v ~ (y -> ~ x) = x * y. [copy(25),flip(a)]. given #24 (I,wt=13): 28 (x -> y) ^ (~ y -> ~ x) = x => y. [copy(27),flip(a)]. given #25 (I,wt=5): 29 x -> 1 = 1 # label("(3.1)"). [assumption]. given #26 (I,wt=5): 30 1 -> x = x # label("(3.2)"). [assumption]. given #27 (I,wt=13): 31 (x -> y) -> (x -> z) = x -> (y -> z) # label("(3.3)"). [assumption]. given #28 (I,wt=11): 32 x -> (y -> z) = y -> (x -> z) # label("(3.4)"). [assumption]. given #29 (I,wt=9): 33 x -> (x -> y) = x -> y # label("(3.5)"). [assumption]. given #30 (I,wt=13): 34 (x -> y) ^ (z -> y) = (x v z) -> y # label("(3.6)"). [assumption]. given #31 (I,wt=9): 35 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. given #32 (I,wt=11): 36 x -> ~ (x -> y) = x -> ~ y # label("(3.8)"). [assumption]. given #33 (I,wt=13): 37 ~ (x -> y) -> z = x -> (~ y -> z) # label("(3.9)"). [assumption]. given #34 (I,wt=5): 38 1 => x = x # label("(BCK2)"). [assumption]. given #35 (I,wt=5): 39 x => 1 = 1 # label("(BCK3)"). [assumption]. given #36 (I,wt=13): 40 x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). [assumption]. given #37 (I,wt=7): 41 (x ^ y) -> y = 1 # label("(3.10)"). [assumption]. given #38 (I,wt=7): 42 (x ^ y) => y = 1 # label("(3.11)"). [assumption]. given #39 (I,wt=9): 43 ~ x => ~ y = y => x # label("(3.12)"). [assumption]. given #40 (I,wt=7): 44 (x => y) ^ y = y # label("(3.13)"). [assumption]. given #41 (I,wt=9): 45 x => (x ^ y) = x => y # label("(3.14)"). [assumption]. given #42 (I,wt=9): 46 x => (x => y) = x -> y # label("(3.15)"). [assumption]. given #43 (H,wt=7): 66 (x ^ y) v x = x. [para(6(a,1),4(a,1)),flip(a)]. given #44 (H,wt=7): 67 x v (y ^ x) = x. [para(5(a,1),6(a,1,2))]. given #45 (H,wt=7): 72 x ^ (y v x) = x. [para(4(a,1),7(a,1,2))]. given #46 (H,wt=7): 331 x -> (y -> y) = 1. [para(31(a,1),18(a,1))]. given #47 (H,wt=7): 575 (x ^ y) => x = 1. [para(5(a,1),42(a,1,1))]. given #48 (H,wt=7): 602 x ^ (y => x) = x. [para(44(a,1),5(a,1)),flip(a)]. given #49 (H,wt=7): 714 x -> (y v x) = 1. [para(72(a,1),41(a,1,1))]. given #50 (H,wt=7): 729 x -> (y -> x) = 1. [para(331(a,1),31(a,1)),flip(a)]. given #51 (H,wt=7): 754 x => (y => x) = 1. [para(44(a,1),575(a,1,1))]. given #52 (H,wt=9): 574 (x ^ (y ^ z)) => z = 1. [para(3(a,1),42(a,1,1))]. given #53 (H,wt=9): 674 x v (y => x) = y => x. [para(44(a,1),66(a,1,1))]. given #54 (H,wt=9): 750 (x => y) => (x -> y) = 1. [para(28(a,1),575(a,1,1))]. given #55 (H,wt=9): 773 ~ x -> ~ (y ^ x) = 1. [para(13(a,1),714(a,1,2))]. given #56 (H,wt=9): 844 (x ^ y) => (z v y) = 1. [para(72(a,1),574(a,1,1,2))]. given #57 (H,wt=11): 656 x -> (x => y) = x => (x -> y). [para(46(a,1),46(a,1,2)),flip(a)]. given #58 (H,wt=11): 879 (x => (x -> y)) => (x -> y) = 1. [para(33(a,1),750(a,1,2))]. given #59 (H,wt=9): 1009 x => (x -> y) = x -> y. [hyper(40,a,754,a,b,879,a),flip(a)]. given #60 (H,wt=9): 1075 x -> (x => y) = x -> y. [para(1009(a,1),656(a,2))]. given #61 (H,wt=12): 1108 ~ x -> (y => x) = ~ x -> ~ y. [para(43(a,1),1075(a,1,2))]. given #62 (H,wt=13): 441 x ^ (((x => y) => y) ^ z) = x ^ z. [para(35(a,1),3(a,1,1)),flip(a)]. given #63 (H,wt=13): 694 (x -> y) v (x -> (z ^ y)) = x -> y. [para(21(a,1),67(a,1,2))]. given #64 (H,wt=13): 919 ~ x -> (y -> ~ (z ^ x)) = y -> 1. [para(773(a,1),32(a,1,2)),flip(a)]. given #65 (H,wt=11): 1320 ~ x -> (y -> ~ (z ^ x)) = 1. [para(29(a,1),919(a,2))]. given #66 (H,wt=13): 1101 x -> ~ (x -> y) = x -> ~ (x => y). [para(1075(a,1),36(a,1,2,1))]. given #67 (H,wt=11): 1431 x -> ~ (x => y) = x -> ~ y. [para(1101(a,1),36(a,1))]. given #68 (H,wt=11): 1471 x -> ~ (x => ~ y) = x -> y. [para(15(a,1),1431(a,2,2))]. given #69 (H,wt=12): 1565 ~ x -> ~ (y => x) = ~ x -> y. [para(43(a,1),1471(a,1,2,1))]. given #70 (H,wt=14): 253 ~ x -> (~ y -> z) = ~ (x v y) -> z. [para(14(a,1),22(a,1,1)),flip(a)]. given #71 (H,wt=17): 1220 x ^ (y => ((x => z) => z)) = x ^ ((x => z) => z). [para(602(a,1),441(a,1,2)),flip(a)]. given #72 (H,wt=11): 1772 x ^ (y => ((x => z) => z)) = x. [para(35(a,1),1220(a,2))]. given #73 (H,wt=9): 1836 x ^ ((x => y) -> y) = x. [para(46(a,1),1772(a,1,2))]. given #74 (H,wt=11): 1882 x => (y v ((x => z) -> z)) = 1. [para(1836(a,1),844(a,1,1))]. given #75 (H,wt=11): 1921 x => ((x => (y ^ z)) -> z) = 1. [para(694(a,1),1882(a,1,2))]. given #76 (H,wt=17): 1499 x -> (~ ~ (x => y) -> z) = ~ (x -> ~ y) -> z. [para(1431(a,1),37(a,1,1,1)),flip(a)]. given #77 (H,wt=17): 2016 x -> (~ ~ (x => y) -> z) = x -> (~ ~ y -> z). [para(37(a,1),1499(a,2))]. given #78 (H,wt=15): 2083 x -> (~ ~ (x => y) -> z) = x -> (y -> z). [para(15(a,1),2016(a,2,2,1))]. given #79 (H,wt=13): 2196 x -> ((x => y) -> z) = x -> (y -> z). [para(15(a,1),2083(a,1,2,1))]. given #80 (H,wt=18): 1151 ~ x -> (~ (y => x) -> z) = ~ (~ x -> ~ y) -> z. [para(1108(a,1),37(a,1,1,1)),flip(a)]. given #81 (H,wt=18): 2481 ~ x -> (~ (y => x) -> z) = ~ x -> (~ ~ y -> z). [para(37(a,1),1151(a,2))]. given #82 (H,wt=16): 2568 ~ x -> (~ (y => x) -> z) = ~ x -> (y -> z). [para(15(a,1),2481(a,2,2,1))]. given #83 (H,wt=15): 2795 ~ (x v (y => x)) -> z = ~ x -> (y -> z). [para(2568(a,1),253(a,1)),flip(a)]. given #84 (H,wt=13): 2898 ~ (x => y) -> z = ~ y -> (x -> z). [para(674(a,1),2795(a,1,1,1))]. given #85 (H,wt=13): 3008 ~ (x => y) -> z = x -> (~ y -> z). [para(32(a,1),2898(a,2))]. given #86 (H,wt=19): 310 (x -> (y -> z)) ^ (x -> (~ z -> ~ y)) = x -> (y => z). [para(28(a,1),21(a,2,2))]. given #87 (H,wt=19): 369 (x -> (y -> z)) ^ (~ (x -> z) -> ~ y) = y => (x -> z). [para(32(a,1),28(a,1,1))]. given #88 (H,wt=19): 3466 (x -> (y -> z)) ^ (x -> (~ z -> ~ y)) = y => (x -> z). [para(37(a,1),369(a,1,2))]. given #89 (H,wt=11): 3724 x -> (y => z) = y => (x -> z). [para(3466(a,1),310(a,1)),flip(a)]. given #90 (H,wt=11): 3809 (x => (y ^ z)) -> (x => z) = 1. [para(1921(a,1),3724(a,2))]. given #91 (H,wt=19): 3734 (x => (y -> z)) ^ (~ (x => z) -> ~ y) = y => (x => z). [para(3724(a,1),28(a,1,1))]. given #92 (H,wt=19): 4009 (x => (y -> z)) ^ (x -> (~ z -> ~ y)) = y => (x => z). [para(3008(a,1),3734(a,1,2))]. given #93 (H,wt=23): 3860 1 ^ (~ (x => y) -> ~ (x => (z ^ y))) = (x => (z ^ y)) => (x => y). [para(3809(a,1),28(a,1,1))]. given #94 (H,wt=23): 4227 1 ^ (~ x -> (y -> ~ (y => (z ^ x)))) = (y => (z ^ x)) => (y => x). [para(2898(a,1),3860(a,1,2))]. given #95 (H,wt=21): 4325 (x => (y ^ z)) => (x => z) = 1 ^ (~ z -> (x -> ~ (y ^ z))). [para(1431(a,1),4227(a,1,2,2)),flip(a)]. given #96 (H,wt=13): 4467 (x => (y ^ z)) => (x => z) = 1 ^ 1. [para(1320(a,1),4325(a,2,2))]. given #97 (H,wt=11): 4551 (x => (y ^ z)) => (x => z) = 1. [para(11(a,1),4467(a,2))]. given #98 (H,wt=13): 4681 (x => y) => (x => ((y => z) -> z)) = 1. [para(1836(a,1),4551(a,1,1,2))]. given #99 (H,wt=25): 4132 (x => (y => (z -> u))) ^ (x -> (~ (y => u) -> ~ z)) = z => (x => (y => u)). [para(3724(a,1),4009(a,1,1,2))]. given #100 (H,wt=25): 4927 (x => (y => (z -> u))) ^ (x -> (y -> (~ u -> ~ z))) = z => (x => (y => u)). [para(3008(a,1),4132(a,1,2,2))]. given #101 (H,wt=27): 5132 1 ^ ((x => y) -> (x -> (~ z -> ~ (y => z)))) = (y => z) => ((x => y) => (x => z)). [para(4681(a,1),4927(a,1,1))]. given #102 (H,wt=24): 5230 (x => y) => ((z => x) => (z => y)) = 1 ^ ((z => x) -> (z -> (~ y -> x))). [para(1565(a,1),5132(a,1,2,2,2)),flip(a)]. given #103 (H,wt=24): 5305 (x => y) => ((z => x) => (z => y)) = 1 ^ (z -> ((z => x) -> (~ y -> x))). [para(32(a,1),5230(a,2,2))]. given #104 (H,wt=22): 5667 (x => y) => ((z => x) => (z => y)) = 1 ^ (z -> (x -> (~ y -> x))). [para(2196(a,1),5305(a,2,2))]. given #105 (H,wt=17): 5811 (x => y) => ((z => x) => (z => y)) = 1 ^ (z -> 1). [para(729(a,1),5667(a,2,2,2))]. given #106 (H,wt=7): 6009 1 ^ (x -> 1) = 1. [para(5811(a,1),754(a,1))]. -------- Proof 1 -------- "(BCK1')". ============================== PROOF ================================= % Proof 1 at 0.32 (+ 0.01) seconds: "(BCK1')". % Length of proof is 95. % Level of proof is 24. % Maximum clause weight is 27. % Given clauses 106. 1 (x => y) => ((z => x) => (z => y)) = 1 # label("(BCK1')") # label(non_clause) # label(goal). [goal]. 3 (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)"). [assumption]. 4 x v y = y v x # label("(D3)"). [assumption]. 5 x ^ y = y ^ x # label("(D4)"). [assumption]. 6 x v (x ^ y) = x # label("(D5)"). [assumption]. 7 x ^ (x v y) = x # label("(D6)"). [assumption]. 11 x ^ 1 = x # label("(D10)"). [assumption]. 13 ~ x v ~ y = ~ (x ^ y) # label("(DM1)"). [assumption]. 14 ~ x ^ ~ y = ~ (x v y) # label("(DM2)"). [assumption]. 15 ~ ~ x = x # label("(DN)"). [assumption]. 18 x -> x = 1 # label("(N2)"). [assumption]. 21 (x -> y) ^ (x -> z) = x -> (y ^ z) # label("(N5)"). [assumption]. 22 (x ^ y) -> z = x -> (y -> z) # label("(N6)"). [assumption]. 27 x => y = (x -> y) ^ (~ y -> ~ x) # label("(=> def)"). [assumption]. 28 (x -> y) ^ (~ y -> ~ x) = x => y. [copy(27),flip(a)]. 29 x -> 1 = 1 # label("(3.1)"). [assumption]. 31 (x -> y) -> (x -> z) = x -> (y -> z) # label("(3.3)"). [assumption]. 32 x -> (y -> z) = y -> (x -> z) # label("(3.4)"). [assumption]. 33 x -> (x -> y) = x -> y # label("(3.5)"). [assumption]. 35 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. 36 x -> ~ (x -> y) = x -> ~ y # label("(3.8)"). [assumption]. 37 ~ (x -> y) -> z = x -> (~ y -> z) # label("(3.9)"). [assumption]. 40 x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). [assumption]. 41 (x ^ y) -> y = 1 # label("(3.10)"). [assumption]. 42 (x ^ y) => y = 1 # label("(3.11)"). [assumption]. 43 ~ x => ~ y = y => x # label("(3.12)"). [assumption]. 44 (x => y) ^ y = y # label("(3.13)"). [assumption]. 46 x => (x => y) = x -> y # label("(3.15)"). [assumption]. 47 (c1 => c2) => ((c3 => c1) => (c3 => c2)) != 1 # label("(BCK1')") # answer("(BCK1')"). [deny(1)]. 66 (x ^ y) v x = x. [para(6(a,1),4(a,1)),flip(a)]. 67 x v (y ^ x) = x. [para(5(a,1),6(a,1,2))]. 72 x ^ (y v x) = x. [para(4(a,1),7(a,1,2))]. 253 ~ x -> (~ y -> z) = ~ (x v y) -> z. [para(14(a,1),22(a,1,1)),flip(a)]. 310 (x -> (y -> z)) ^ (x -> (~ z -> ~ y)) = x -> (y => z). [para(28(a,1),21(a,2,2))]. 331 x -> (y -> y) = 1. [para(31(a,1),18(a,1))]. 369 (x -> (y -> z)) ^ (~ (x -> z) -> ~ y) = y => (x -> z). [para(32(a,1),28(a,1,1))]. 441 x ^ (((x => y) => y) ^ z) = x ^ z. [para(35(a,1),3(a,1,1)),flip(a)]. 574 (x ^ (y ^ z)) => z = 1. [para(3(a,1),42(a,1,1))]. 575 (x ^ y) => x = 1. [para(5(a,1),42(a,1,1))]. 602 x ^ (y => x) = x. [para(44(a,1),5(a,1)),flip(a)]. 656 x -> (x => y) = x => (x -> y). [para(46(a,1),46(a,1,2)),flip(a)]. 674 x v (y => x) = y => x. [para(44(a,1),66(a,1,1))]. 694 (x -> y) v (x -> (z ^ y)) = x -> y. [para(21(a,1),67(a,1,2))]. 714 x -> (y v x) = 1. [para(72(a,1),41(a,1,1))]. 729 x -> (y -> x) = 1. [para(331(a,1),31(a,1)),flip(a)]. 750 (x => y) => (x -> y) = 1. [para(28(a,1),575(a,1,1))]. 754 x => (y => x) = 1. [para(44(a,1),575(a,1,1))]. 773 ~ x -> ~ (y ^ x) = 1. [para(13(a,1),714(a,1,2))]. 844 (x ^ y) => (z v y) = 1. [para(72(a,1),574(a,1,1,2))]. 879 (x => (x -> y)) => (x -> y) = 1. [para(33(a,1),750(a,1,2))]. 919 ~ x -> (y -> ~ (z ^ x)) = y -> 1. [para(773(a,1),32(a,1,2)),flip(a)]. 1009 x => (x -> y) = x -> y. [hyper(40,a,754,a,b,879,a),flip(a)]. 1075 x -> (x => y) = x -> y. [para(1009(a,1),656(a,2))]. 1101 x -> ~ (x -> y) = x -> ~ (x => y). [para(1075(a,1),36(a,1,2,1))]. 1108 ~ x -> (y => x) = ~ x -> ~ y. [para(43(a,1),1075(a,1,2))]. 1151 ~ x -> (~ (y => x) -> z) = ~ (~ x -> ~ y) -> z. [para(1108(a,1),37(a,1,1,1)),flip(a)]. 1220 x ^ (y => ((x => z) => z)) = x ^ ((x => z) => z). [para(602(a,1),441(a,1,2)),flip(a)]. 1320 ~ x -> (y -> ~ (z ^ x)) = 1. [para(29(a,1),919(a,2))]. 1431 x -> ~ (x => y) = x -> ~ y. [para(1101(a,1),36(a,1))]. 1471 x -> ~ (x => ~ y) = x -> y. [para(15(a,1),1431(a,2,2))]. 1499 x -> (~ ~ (x => y) -> z) = ~ (x -> ~ y) -> z. [para(1431(a,1),37(a,1,1,1)),flip(a)]. 1565 ~ x -> ~ (y => x) = ~ x -> y. [para(43(a,1),1471(a,1,2,1))]. 1772 x ^ (y => ((x => z) => z)) = x. [para(35(a,1),1220(a,2))]. 1836 x ^ ((x => y) -> y) = x. [para(46(a,1),1772(a,1,2))]. 1882 x => (y v ((x => z) -> z)) = 1. [para(1836(a,1),844(a,1,1))]. 1921 x => ((x => (y ^ z)) -> z) = 1. [para(694(a,1),1882(a,1,2))]. 2016 x -> (~ ~ (x => y) -> z) = x -> (~ ~ y -> z). [para(37(a,1),1499(a,2))]. 2083 x -> (~ ~ (x => y) -> z) = x -> (y -> z). [para(15(a,1),2016(a,2,2,1))]. 2196 x -> ((x => y) -> z) = x -> (y -> z). [para(15(a,1),2083(a,1,2,1))]. 2481 ~ x -> (~ (y => x) -> z) = ~ x -> (~ ~ y -> z). [para(37(a,1),1151(a,2))]. 2568 ~ x -> (~ (y => x) -> z) = ~ x -> (y -> z). [para(15(a,1),2481(a,2,2,1))]. 2795 ~ (x v (y => x)) -> z = ~ x -> (y -> z). [para(2568(a,1),253(a,1)),flip(a)]. 2898 ~ (x => y) -> z = ~ y -> (x -> z). [para(674(a,1),2795(a,1,1,1))]. 3008 ~ (x => y) -> z = x -> (~ y -> z). [para(32(a,1),2898(a,2))]. 3466 (x -> (y -> z)) ^ (x -> (~ z -> ~ y)) = y => (x -> z). [para(37(a,1),369(a,1,2))]. 3724 x -> (y => z) = y => (x -> z). [para(3466(a,1),310(a,1)),flip(a)]. 3734 (x => (y -> z)) ^ (~ (x => z) -> ~ y) = y => (x => z). [para(3724(a,1),28(a,1,1))]. 3809 (x => (y ^ z)) -> (x => z) = 1. [para(1921(a,1),3724(a,2))]. 3860 1 ^ (~ (x => y) -> ~ (x => (z ^ y))) = (x => (z ^ y)) => (x => y). [para(3809(a,1),28(a,1,1))]. 4009 (x => (y -> z)) ^ (x -> (~ z -> ~ y)) = y => (x => z). [para(3008(a,1),3734(a,1,2))]. 4132 (x => (y => (z -> u))) ^ (x -> (~ (y => u) -> ~ z)) = z => (x => (y => u)). [para(3724(a,1),4009(a,1,1,2))]. 4227 1 ^ (~ x -> (y -> ~ (y => (z ^ x)))) = (y => (z ^ x)) => (y => x). [para(2898(a,1),3860(a,1,2))]. 4325 (x => (y ^ z)) => (x => z) = 1 ^ (~ z -> (x -> ~ (y ^ z))). [para(1431(a,1),4227(a,1,2,2)),flip(a)]. 4467 (x => (y ^ z)) => (x => z) = 1 ^ 1. [para(1320(a,1),4325(a,2,2))]. 4551 (x => (y ^ z)) => (x => z) = 1. [para(11(a,1),4467(a,2))]. 4681 (x => y) => (x => ((y => z) -> z)) = 1. [para(1836(a,1),4551(a,1,1,2))]. 4927 (x => (y => (z -> u))) ^ (x -> (y -> (~ u -> ~ z))) = z => (x => (y => u)). [para(3008(a,1),4132(a,1,2,2))]. 5132 1 ^ ((x => y) -> (x -> (~ z -> ~ (y => z)))) = (y => z) => ((x => y) => (x => z)). [para(4681(a,1),4927(a,1,1))]. 5230 (x => y) => ((z => x) => (z => y)) = 1 ^ ((z => x) -> (z -> (~ y -> x))). [para(1565(a,1),5132(a,1,2,2,2)),flip(a)]. 5305 (x => y) => ((z => x) => (z => y)) = 1 ^ (z -> ((z => x) -> (~ y -> x))). [para(32(a,1),5230(a,2,2))]. 5667 (x => y) => ((z => x) => (z => y)) = 1 ^ (z -> (x -> (~ y -> x))). [para(2196(a,1),5305(a,2,2))]. 5811 (x => y) => ((z => x) => (z => y)) = 1 ^ (z -> 1). [para(729(a,1),5667(a,2,2,2))]. 6009 1 ^ (x -> 1) = 1. [para(5811(a,1),754(a,1))]. 6163 (x => y) => ((z => x) => (z => y)) = 1. [para(6009(a,1),5811(a,2))]. 6164 $F # answer("(BCK1')"). [resolve(6163,a,47,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=106. Generated=7172. Kept=6159. proofs=1. Usable=106. Sos=5871. Demods=0. Limbo=27, Disabled=197. Hints=80. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=1013. Back_subsumed=154. 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=9.70. User_CPU=0.32, System_CPU=0.01, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED THEOREM PROVED Exiting with 1 proof. ------ process 32388 exit (max_proofs) ------  Process 32388 exit (max_proofs) Mon Jan 21 11:14:46 2008