============================== Prover9 =============================== Prover9 (64) version Aug-2007, Aug 2007. Process 26338 was started by veroff on titan, Sat Jan 19 14:19:12 2008 The command was "prover9 -f 4.11.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file 4.11.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)"). x -> ((y v x) -> z) = x -> z # label("(4.9)"). x -> (~ x v y) = x -> y # label("(4.10)"). x -> x = 1 # label("(N2)"). (x -> y) ^ (x -> z) = x -> (y ^ z) # label("(N5)"). (x -> y) ^ (~ x v y) = ~ x v y # label("(N3)"). (x ^ y) -> z = x -> (y -> z) # label("(N6)"). x ^ (~ x v y) = x ^ (x -> y) # label("(N4)"). end_of_list. formulas(goals). (x ^ ~ x) ^ (y v ~ y) = x ^ ~ x # label("(N1)"). end_of_list. formulas(hints). x v x = x. (x ^ y) => x = 1. (x * x) => y = x -> y. (x * y) => (x => (y => z)) = (x * y) -> z. ~ x => 0 = x. x => ((y ^ (x => z)) => z) = 1. x => (y -> z) = y => (x => (y => z)). x => (y => (x => z)) = y => (x -> z). x => (y => (z => u)) = z => (x => (y => u)). ~ x ^ (y => 0) = (x v y) => 0. (x v y) => x = y => x. (x ^ y) -> z = y -> (x -> z). x -> y = x -> ((z => x) -> y). x -> ((y => x) -> z) = x -> z. x ^ (y v ~ x) = x ^ (x -> y). x ^ ~ x = x ^ (x -> 0). x ^ (x -> 0) = x ^ ~ x. x v y = x v (x v y). x v (x v y) = x v y. x ^ (y => 0) = (~ x v y) => 0. (~ x v y) => 0 = x ^ (y => 0). (x => (y ^ z)) => (x => y) = 1. (x -> y) ^ y = y. x v ((y -> x) ^ z) = (y -> x) ^ (x v z). (x v y) => (y => x) = (x v y) -> x. (x v y) ^ (x v z) = x v (y ^ (x v z)). x v (y ^ (x v z)) = (x v y) ^ (x v z). x ^ (1 => ((y ^ (x => z)) => z)) = x. x -> y = (x v z) -> (x -> y). (x v y) -> (x -> z) = x -> z. x -> (y -> z) = y -> (x -> z). 1 = x => ((x => (y ^ z)) => y). x => ((x => (y ^ z)) => y) = 1. x -> ((y * (y => x)) -> z) = (y * (y => x)) -> z. ~ 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 ^ ~ y) => 0 = ~ x v y. (~ x v y) => (x ^ (y => 0)) = (~ x v y) -> 0. (x v y) -> x = y => ((x v y) => x). x => ((y v x) => y) = (y v x) -> y. x ^ ((y ^ (x => z)) => z) = x. x ^ (((y v x) => z) => z) = x. x ^ (1 => (((y v x) => (z ^ u)) => z)) = x. x => (x => y) = (y v x) -> y. (x v y) -> x = y -> x. (x * y) -> z = x => (y => (x => (y => z))). x => (y => (x => (y => z))) = (x * y) -> z. x => (y => ((z ^ (y => (x => u))) => u)) = 1. x => (y => (~ z v u)) = (z ^ ~ u) => (x => (y => 0)). (x ^ ~ y) => (z => (u => 0)) = z => (u => (~ x v y)). x v (y ^ (z -> x)) = (z -> x) ^ (x v y). x v (y ^ (x v z)) = x v (y ^ z). x v (y ^ (y -> x)) = x v (y ^ ~ y). x ^ (((y v x) => (z ^ u)) => z) = x. x => (x => (y -> z)) = (x * y) -> z. (x * y) -> z = x -> (y -> z). (x -> y) ^ (y v x) = y v (x ^ ~ x). x -> (y -> ((y => x) -> z)) = (y * (y => x)) -> z. x ^ (((~ y v x) -> 0) => y) = x. x => (((~ (x => y) v z) -> 0) => (z => y)) = 1. x => (((y v ~ (x => z)) -> 0) => (y => z)) = 1. x => (y => (((y v ~ (x => z)) -> 0) => z)) = 1. x => (y => (((y v ~ ~ x) -> 0) => 0)) = 1. x => (y => (((y v x) -> 0) => 0)) = 1. x => (y => ~ ((y v x) -> 0)) = 1. (x * (x => y)) -> z = x -> (y -> ((x => y) -> z)). x -> (y -> ((x => y) -> z)) = (x * (x => y)) -> z. x -> (y -> z) = (x * (x => y)) -> z. (x * (x => y)) -> z = x -> (y -> z). (x * (x -> y)) -> z = x -> ((x => y) -> z). x -> (y -> z) = x -> ((x => y) -> z). x -> ((x => y) -> z) = x -> (y -> z). (x * (x -> y)) -> z = x -> (y -> z). x -> (y -> z) = x -> ((x -> y) -> z). x -> ((x -> y) -> z) = x -> (y -> z). (x v y) -> (((x v y) -> x) -> z) = x -> z. (x v y) -> ((y -> x) -> z) = x -> z. ((x -> y) ^ (y v x)) -> z = y -> z. (x v (y ^ ~ y)) -> z = x -> z. (x ^ ~ x) => (y => ~ (y -> 0)) = 1. (x ^ ~ y) => (z => ~ u) = z => (u => (~ x v y)). x => ((x -> 0) => (~ y v y)) = 1. x => ((x -> 0) => (y v ~ y)) = 1. (x ^ y) => ((x -> (y -> 0)) => (z v ~ z)) = 1. ((x -> 0) ^ x) => (1 => (y v ~ y)) = 1. (x ^ (x -> 0)) => (1 => (y v ~ y)) = 1. (x ^ ~ x) => (1 => (y v ~ y)) = 1. (x ^ ~ x) => (y v ~ y) = 1. (x ^ ~ x) ^ (1 => (y v ~ y)) = x ^ ~ x. end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (x ^ ~ x) ^ (y v ~ y) = x ^ ~ x # label("(N1)") # 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]. x -> ((y v x) -> z) = x -> z # label("(4.9)"). [assumption]. x -> (~ x v y) = x -> y # label("(4.10)"). [assumption]. x -> x = 1 # label("(N2)"). [assumption]. (x -> y) ^ (x -> z) = x -> (y ^ z) # label("(N5)"). [assumption]. (x -> y) ^ (~ x v y) = ~ x v y # label("(N3)"). [assumption]. (x ^ y) -> z = x -> (y -> z) # label("(N6)"). [assumption]. x ^ (~ x v y) = x ^ (x -> y) # label("(N4)"). [assumption]. (c1 ^ ~ c1) ^ (c2 v ~ c2) != c1 ^ ~ c1 # label("(N1)"). [deny(1)]. end_of_list. formulas(demodulators). end_of_list. % 92 hints input. Auto_denials: % copying label "(N1)" to answer in negative clause Term ordering decisions: Function symbol KB weights: 0=1. 1=1. c1=1. c2=1. *=1. ^=1. =>=1. ->=1. v=1. ~=1. -=1. Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ 0, 1, c1, c2, *, ^, =>, ->, 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=14): 52 (c1 ^ ~ c1) ^ (c2 v ~ c2) != c1 ^ ~ c1 # label("(N1)") # answer("(N1)"). [deny(1)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 52 (c1 ^ ~ c1) ^ (c2 v ~ c2) != c1 ^ ~ c1 # label("(N1)") # answer("(N1)"). [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 => y) => ((y => z) => (x => z)) = 1 # label("(BCK1)"). [assumption]. 9 1 => x = x # label("(BCK2)"). [assumption]. 10 x => 1 = 1 # label("(BCK3)"). [assumption]. 11 x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). [assumption]. 12 x * 1 = x # label("(M1)"). [assumption]. 13 x * y = y * x # label("(M2)"). [assumption]. 14 (x * y) * z = x * (y * z) # label("(M3)"). [assumption]. 15 (x * y) => z = x => (y => z) # label("(P)"). [assumption]. 16 x ^ 1 = x # label("(D10)"). [assumption]. 17 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. 18 (x ^ y) => y = 1 # label("(3.11)"). [assumption]. 19 x v 0 = x # label("(D9)"). [assumption]. 21 x => (x => y) = x -> y. [copy(20),flip(a)]. 23 x => 0 = ~ x. [copy(22),flip(a)]. 25 x => (x => 0) = -x. [copy(24),flip(a)]. 26 x => (x => (x => y)) = x => (x => y) # label("(E_2)"). [assumption]. 27 (x v y) ^ (x v z) = x v (y ^ z) # label("(D7)"). [assumption]. 28 (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D8)"). [assumption]. 29 ~ ~ x = x # label("(DN)"). [assumption]. 30 (x -> y) ^ (~ y -> ~ x) = x => y # label("(N)"). [assumption]. 31 (x => y) => ((z => x) => (z => y)) = 1 # label("(BCK1')"). [assumption]. 32 x => ((x => y) => y) = 1 # label("(BCK5)"). [assumption]. 33 x => x = 1 # label("(3.16)"). [assumption]. 34 x => (y => x) = 1 # label("(3.17)"). [assumption]. 35 x => (y => z) = y => (x => z) # label("(3.18)"). [assumption]. 36 (x * y) v (x * z) = x * (y v z) # label("(4.1)"). [assumption]. 37 (x => y) ^ (x => z) = x => (y ^ z) # label("(4.2)"). [assumption]. 38 (x * (x => y)) v y = y # label("(4.3)"). [assumption]. 39 (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). [assumption]. 40 ((x => y) * z) => (x => (y * z)) = 1 # label("(4.5)"). [assumption]. 41 (x => y) ^ y = y # label("(3.13)"). [assumption]. 42 (x v y) => y = x => y # label("(4.6)"). [assumption]. 43 x -> (y => z) = y => (x -> z) # label("(4.7)"). [assumption]. 44 x ^ (~ x => y) = x # label("(4.8)"). [assumption]. 45 x -> ((y v x) -> z) = x -> z # label("(4.9)"). [assumption]. 46 x -> (~ x v y) = x -> y # label("(4.10)"). [assumption]. 47 x -> x = 1 # label("(N2)"). [assumption]. 48 (x -> y) ^ (x -> z) = x -> (y ^ z) # label("(N5)"). [assumption]. 49 (x -> y) ^ (~ x v y) = ~ x v y # label("(N3)"). [assumption]. 50 (x ^ y) -> z = x -> (y -> z) # label("(N6)"). [assumption]. 51 x ^ (~ x v y) = x ^ (x -> y) # label("(N4)"). [assumption]. end_of_list. formulas(demodulators). end_of_list. % 92 hints processed (17 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 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 => y) => ((y => z) => (x => z)) = 1 # label("(BCK1)"). [assumption]. given #8 (I,wt=5): 9 1 => x = x # label("(BCK2)"). [assumption]. given #9 (I,wt=5): 10 x => 1 = 1 # label("(BCK3)"). [assumption]. given #10 (I,wt=13): 11 x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). [assumption]. given #11 (I,wt=5): 12 x * 1 = x # label("(M1)"). [assumption]. given #12 (I,wt=7): 13 x * y = y * x # label("(M2)"). [assumption]. given #13 (I,wt=11): 14 (x * y) * z = x * (y * z) # label("(M3)"). [assumption]. given #14 (I,wt=11): 15 (x * y) => z = x => (y => z) # label("(P)"). [assumption]. given #15 (I,wt=5): 16 x ^ 1 = x # label("(D10)"). [assumption]. given #16 (I,wt=9): 17 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. given #17 (I,wt=7): 18 (x ^ y) => y = 1 # label("(3.11)"). [assumption]. given #18 (I,wt=5): 19 x v 0 = x # label("(D9)"). [assumption]. given #19 (I,wt=9): 21 x => (x => y) = x -> y. [copy(20),flip(a)]. given #20 (I,wt=6): 23 x => 0 = ~ x. [copy(22),flip(a)]. given #21 (I,wt=8): 25 x => (x => 0) = -x. [copy(24),flip(a)]. given #22 (I,wt=13): 26 x => (x => (x => y)) = x => (x => y) # label("(E_2)"). [assumption]. given #23 (I,wt=13): 27 (x v y) ^ (x v z) = x v (y ^ z) # label("(D7)"). [assumption]. given #24 (I,wt=13): 28 (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D8)"). [assumption]. given #25 (I,wt=5): 29 ~ ~ x = x # label("(DN)"). [assumption]. given #26 (I,wt=13): 30 (x -> y) ^ (~ y -> ~ x) = x => y # label("(N)"). [assumption]. given #27 (I,wt=13): 31 (x => y) => ((z => x) => (z => y)) = 1 # label("(BCK1')"). [assumption]. given #28 (I,wt=9): 32 x => ((x => y) => y) = 1 # label("(BCK5)"). [assumption]. given #29 (I,wt=5): 33 x => x = 1 # label("(3.16)"). [assumption]. given #30 (I,wt=7): 34 x => (y => x) = 1 # label("(3.17)"). [assumption]. given #31 (I,wt=11): 35 x => (y => z) = y => (x => z) # label("(3.18)"). [assumption]. given #32 (I,wt=13): 36 (x * y) v (x * z) = x * (y v z) # label("(4.1)"). [assumption]. given #33 (I,wt=13): 37 (x => y) ^ (x => z) = x => (y ^ z) # label("(4.2)"). [assumption]. given #34 (I,wt=9): 38 (x * (x => y)) v y = y # label("(4.3)"). [assumption]. given #35 (I,wt=13): 39 (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). [assumption]. given #36 (I,wt=13): 40 ((x => y) * z) => (x => (y * z)) = 1 # label("(4.5)"). [assumption]. given #37 (I,wt=7): 41 (x => y) ^ y = y # label("(3.13)"). [assumption]. given #38 (I,wt=9): 42 (x v y) => y = x => y # label("(4.6)"). [assumption]. given #39 (I,wt=11): 43 x -> (y => z) = y => (x -> z) # label("(4.7)"). [assumption]. given #40 (I,wt=8): 44 x ^ (~ x => y) = x # label("(4.8)"). [assumption]. given #41 (I,wt=11): 45 x -> ((y v x) -> z) = x -> z # label("(4.9)"). [assumption]. given #42 (I,wt=10): 46 x -> (~ x v y) = x -> y # label("(4.10)"). [assumption]. given #43 (I,wt=5): 47 x -> x = 1 # label("(N2)"). [assumption]. given #44 (I,wt=13): 48 (x -> y) ^ (x -> z) = x -> (y ^ z) # label("(N5)"). [assumption]. given #45 (I,wt=13): 49 (x -> y) ^ (~ x v y) = ~ x v y # label("(N3)"). [assumption]. given #46 (I,wt=11): 50 (x ^ y) -> z = x -> (y -> z) # label("(N6)"). [assumption]. given #47 (I,wt=12): 51 x ^ (~ x v y) = x ^ (x -> y) # label("(N4)"). [assumption]. given #48 (H,wt=5): 79 x v x = x. [para(7(a,1),6(a,1,2))]. given #49 (H,wt=6): 251 ~ x => 0 = x. [para(29(a,1),23(a,2))]. given #50 (H,wt=7): 126 (x ^ y) => x = 1. [para(5(a,1),18(a,1,1))]. given #51 (H,wt=9): 145 (x * x) => y = x -> y. [para(21(a,1),15(a,2))]. given #52 (H,wt=7): 925 (x -> y) ^ y = y. [para(145(a,1),41(a,1,1))]. given #53 (H,wt=9): 595 (x v y) => x = y => x. [para(4(a,1),42(a,1,1))]. given #54 (H,wt=9): 819 x v (x v y) = x v y. [para(79(a,1),2(a,1,1)),flip(a)]. given #55 (H,wt=10): 805 x ^ (x -> 0) = x ^ ~ x. [para(19(a,1),51(a,1,2)),flip(a)]. given #56 (H,wt=11): 369 x => ((y ^ (x => z)) => z) = 1. [para(35(a,1),18(a,1))]. given #57 (H,wt=11): 764 (x ^ y) -> z = y -> (x -> z). [para(5(a,1),50(a,1,1))]. given #58 (H,wt=11): 876 (x => (y ^ z)) => (x => y) = 1. [para(37(a,1),126(a,1,1))]. given #59 (H,wt=11): 1097 (x v y) -> (x -> z) = x -> z. [para(7(a,1),764(a,1,1)),flip(a)]. given #60 (H,wt=11): 1106 x -> ((y => x) -> z) = x -> z. [para(41(a,1),764(a,1,1)),flip(a)]. given #61 (H,wt=11): 1127 x -> (y -> z) = y -> (x -> z). [para(764(a,1),50(a,1))]. given #62 (H,wt=11): 1164 x => ((x => (y ^ z)) => y) = 1. [para(876(a,1),35(a,1)),flip(a)]. given #63 (H,wt=12): 510 ~ x ^ (y => 0) = (x v y) => 0. [para(23(a,1),39(a,1,1))]. given #64 (H,wt=11): 1342 (x v y) => 0 = ~ x ^ ~ y. [para(23(a,1),510(a,1,2)),flip(a)]. given #65 (H,wt=10): 1377 ~ x ^ ~ y = ~ (x v y). [para(1342(a,1),23(a,1))]. given #66 (H,wt=10): 1420 ~ (~ x v y) = x ^ ~ y. [para(29(a,1),1377(a,1,1)),flip(a)]. given #67 (H,wt=11): 1449 (x ^ ~ y) => 0 = ~ x v y. [para(1420(a,1),251(a,1,1))]. given #68 (H,wt=12): 800 x ^ (y v ~ x) = x ^ (x -> y). [para(4(a,1),51(a,1,2))]. given #69 (H,wt=12): 849 (~ x v y) => 0 = x ^ (y => 0). [para(251(a,1),39(a,1,1)),flip(a)]. given #70 (H,wt=13): 372 x => (y => (x => z)) = y => (x -> z). [para(21(a,1),35(a,1,2)),flip(a)]. given #71 (H,wt=13): 960 (x v y) => (y => x) = (x v y) -> x. [para(595(a,1),21(a,1,2))]. given #72 (H,wt=13): 1056 x ^ (1 => ((y ^ (x => z)) => z)) = x. [para(369(a,1),17(a,1,2,1))]. given #73 (H,wt=11): 1773 x ^ ((y ^ (x => z)) => z) = x. [para(9(a,1),1056(a,1,2))]. given #74 (H,wt=11): 1843 x ^ (((y v x) => z) => z) = x. [para(39(a,1),1773(a,1,2,1))]. given #75 (H,wt=13): 1723 x => ((y v x) => y) = (y v x) -> y. [para(960(a,1),35(a,1)),flip(a)]. given #76 (H,wt=11): 1947 x => (x => y) = (y v x) -> y. [para(595(a,1),1723(a,1,2))]. given #77 (H,wt=9): 1975 (x v y) -> x = y -> x. [para(1947(a,1),21(a,1))]. given #78 (H,wt=15): 146 (x * y) => (x => (y => z)) = (x * y) -> z. [para(15(a,1),21(a,1,2))]. given #79 (H,wt=15): 391 x => (y => (z => u)) = z => (x => (y => u)). [para(35(a,1),35(a,1,2))]. given #80 (H,wt=15): 938 x v ((y -> x) ^ z) = (y -> x) ^ (x v z). [para(925(a,1),28(a,1,1))]. given #81 (H,wt=15): 1014 x v (y ^ (x v z)) = (x v y) ^ (x v z). [para(819(a,1),27(a,1,2)),flip(a)]. given #82 (H,wt=13): 2538 x v (y ^ (x v z)) = x v (y ^ z). [para(27(a,1),1014(a,2))]. given #83 (H,wt=14): 2653 x v (y ^ (y -> x)) = x v (y ^ ~ y). [para(800(a,1),2538(a,1,2))]. given #84 (H,wt=15): 1893 x ^ (1 => (((y v x) => (z ^ u)) => z)) = x. [para(1164(a,1),1843(a,1,2,1))]. given #85 (H,wt=13): 2748 x ^ (((y v x) => (z ^ u)) => z) = x. [para(9(a,1),1893(a,1,2))]. given #86 (H,wt=15): 2115 x => (y => (x => (y => z))) = (x * y) -> z. [para(146(a,1),15(a,1)),flip(a)]. given #87 (H,wt=13): 2940 x => (x => (y -> z)) = (x * y) -> z. [para(372(a,1),2115(a,1,2))]. given #88 (H,wt=11): 2983 (x * y) -> z = x -> (y -> z). [para(2940(a,1),21(a,1))]. given #89 (H,wt=15): 2347 x => (y => ((z ^ (y => (x => u))) => u)) = 1. [para(391(a,1),369(a,1))]. given #90 (H,wt=15): 2437 x v (y ^ (z -> x)) = (z -> x) ^ (x v y). [para(5(a,1),938(a,1,2))]. given #91 (H,wt=14): 3309 (x -> y) ^ (y v x) = y v (x ^ ~ x). [para(2437(a,1),2653(a,1))]. given #92 (H,wt=17): 1195 x -> ((y * (y => x)) -> z) = (y * (y => x)) -> z. [para(38(a,1),1097(a,1,1))]. given #93 (H,wt=17): 1548 (~ x v y) => (x ^ (y => 0)) = (~ x v y) -> 0. [para(849(a,1),21(a,1,2))]. given #94 (H,wt=12): 3589 x ^ (((~ y v x) -> 0) => y) = x. [para(1548(a,1),2748(a,1,2,1))]. given #95 (H,wt=16): 3632 x => (((~ (x => y) v z) -> 0) => (z => y)) = 1. [para(3589(a,1),2347(a,1,2,2,1))]. given #96 (H,wt=16): 3636 x => (((y v ~ (x => z)) -> 0) => (y => z)) = 1. [para(4(a,1),3632(a,1,2,1,1))]. given #97 (H,wt=16): 3796 x => (y => (((y v ~ (x => z)) -> 0) => z)) = 1. [para(35(a,1),3636(a,1,2))]. given #98 (H,wt=15): 3896 x => (y => (((y v ~ ~ x) -> 0) => 0)) = 1. [para(23(a,1),3796(a,1,2,2,1,1,2,1))]. given #99 (H,wt=13): 4000 x => (y => (((y v x) -> 0) => 0)) = 1. [para(29(a,1),3896(a,1,2,2,1,1,2))]. given #100 (H,wt=12): 4064 x => (y => ~ ((y v x) -> 0)) = 1. [para(23(a,1),4000(a,1,2,2))]. given #101 (H,wt=17): 3494 x -> (y -> ((y => x) -> z)) = (y * (y => x)) -> z. [para(2983(a,1),1195(a,1,2))]. given #102 (H,wt=17): 4280 x -> (y -> ((x => y) -> z)) = (x * (x => y)) -> z. [para(3494(a,1),1127(a,1)),flip(a)]. given #103 (H,wt=13): 4427 (x * (x => y)) -> z = x -> (y -> z). [para(1106(a,1),4280(a,1,2)),flip(a)]. given #104 (H,wt=13): 4596 x -> ((x => y) -> z) = x -> (y -> z). [para(4427(a,1),2983(a,1)),flip(a)]. given #105 (H,wt=15): 4512 (x * (x -> y)) -> z = x -> ((x => y) -> z). [para(21(a,1),4427(a,1,1,2))]. given #106 (H,wt=13): 4885 (x * (x -> y)) -> z = x -> (y -> z). [para(4596(a,1),4512(a,2))]. given #107 (H,wt=13): 4955 x -> ((x -> y) -> z) = x -> (y -> z). [para(4885(a,1),2983(a,1)),flip(a)]. given #108 (H,wt=15): 5035 (x v y) -> (((x v y) -> x) -> z) = x -> z. [para(1097(a,1),4955(a,2))]. given #109 (H,wt=13): 5177 (x v y) -> ((y -> x) -> z) = x -> z. [para(1975(a,1),5035(a,1,2,1))]. given #110 (H,wt=13): 5257 ((x -> y) ^ (y v x)) -> z = y -> z. [para(5177(a,1),764(a,2))]. given #111 (H,wt=12): 5405 (x v (y ^ ~ y)) -> z = x -> z. [para(3309(a,1),5257(a,1,1))]. given #112 (H,wt=13): 5517 (x ^ ~ x) => (y => ~ (y -> 0)) = 1. [para(5405(a,1),4064(a,1,2,2,1))]. given #113 (H,wt=19): 2370 (x ^ ~ y) => (z => (u => 0)) = z => (u => (~ x v y)). [para(1449(a,1),391(a,1,2,2)),flip(a)]. given #114 (H,wt=18): 5653 (x ^ ~ y) => (z => ~ u) = z => (u => (~ x v y)). [para(23(a,1),2370(a,1,2,2))]. given #115 (H,wt=12): 5906 x => ((x -> 0) => (~ y v y)) = 1. [para(5653(a,1),5517(a,1))]. given #116 (H,wt=12): 5908 x => ((x -> 0) => (y v ~ y)) = 1. [para(4(a,1),5906(a,1,2,2))]. given #117 (H,wt=16): 6003 (x ^ y) => ((x -> (y -> 0)) => (z v ~ z)) = 1. [para(50(a,1),5908(a,1,2,1))]. given #118 (H,wt=14): 6083 ((x -> 0) ^ x) => (1 => (y v ~ y)) = 1. [para(47(a,1),6003(a,1,2,1))]. given #119 (H,wt=14): 6161 (x ^ (x -> 0)) => (1 => (y v ~ y)) = 1. [para(5(a,1),6083(a,1,1))]. given #120 (H,wt=13): 6258 (x ^ ~ x) => (1 => (y v ~ y)) = 1. [para(805(a,1),6161(a,1,1))]. given #121 (H,wt=11): 6306 (x ^ ~ x) => (y v ~ y) = 1. [para(9(a,1),6258(a,1,2))]. given #122 (H,wt=16): 6369 (x ^ ~ x) ^ (1 => (y v ~ y)) = x ^ ~ x. [para(6306(a,1),17(a,1,2,1))]. -------- Proof 1 -------- "(N1)". ============================== PROOF ================================= % Proof 1 at 0.26 (+ 0.02) seconds: "(N1)". % Length of proof is 105. % Level of proof is 26. % Maximum clause weight is 19. % Given clauses 122. 1 (x ^ ~ x) ^ (y v ~ y) = x ^ ~ x # label("(N1)") # label(non_clause) # label(goal). [goal]. 2 (x v y) v z = x v (y v z) # label("(D1)"). [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]. 9 1 => x = x # label("(BCK2)"). [assumption]. 15 (x * y) => z = x => (y => z) # label("(P)"). [assumption]. 17 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. 18 (x ^ y) => y = 1 # label("(3.11)"). [assumption]. 19 x v 0 = x # label("(D9)"). [assumption]. 20 x -> y = x => (x => y) # label("(-> def)"). [assumption]. 21 x => (x => y) = x -> y. [copy(20),flip(a)]. 22 ~ x = x => 0 # label("(~ def)"). [assumption]. 23 x => 0 = ~ x. [copy(22),flip(a)]. 27 (x v y) ^ (x v z) = x v (y ^ z) # label("(D7)"). [assumption]. 28 (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D8)"). [assumption]. 29 ~ ~ x = x # label("(DN)"). [assumption]. 35 x => (y => z) = y => (x => z) # label("(3.18)"). [assumption]. 37 (x => y) ^ (x => z) = x => (y ^ z) # label("(4.2)"). [assumption]. 38 (x * (x => y)) v y = y # label("(4.3)"). [assumption]. 39 (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). [assumption]. 41 (x => y) ^ y = y # label("(3.13)"). [assumption]. 42 (x v y) => y = x => y # label("(4.6)"). [assumption]. 47 x -> x = 1 # label("(N2)"). [assumption]. 50 (x ^ y) -> z = x -> (y -> z) # label("(N6)"). [assumption]. 51 x ^ (~ x v y) = x ^ (x -> y) # label("(N4)"). [assumption]. 52 (c1 ^ ~ c1) ^ (c2 v ~ c2) != c1 ^ ~ c1 # label("(N1)") # answer("(N1)"). [deny(1)]. 79 x v x = x. [para(7(a,1),6(a,1,2))]. 126 (x ^ y) => x = 1. [para(5(a,1),18(a,1,1))]. 145 (x * x) => y = x -> y. [para(21(a,1),15(a,2))]. 146 (x * y) => (x => (y => z)) = (x * y) -> z. [para(15(a,1),21(a,1,2))]. 251 ~ x => 0 = x. [para(29(a,1),23(a,2))]. 369 x => ((y ^ (x => z)) => z) = 1. [para(35(a,1),18(a,1))]. 372 x => (y => (x => z)) = y => (x -> z). [para(21(a,1),35(a,1,2)),flip(a)]. 391 x => (y => (z => u)) = z => (x => (y => u)). [para(35(a,1),35(a,1,2))]. 510 ~ x ^ (y => 0) = (x v y) => 0. [para(23(a,1),39(a,1,1))]. 595 (x v y) => x = y => x. [para(4(a,1),42(a,1,1))]. 764 (x ^ y) -> z = y -> (x -> z). [para(5(a,1),50(a,1,1))]. 800 x ^ (y v ~ x) = x ^ (x -> y). [para(4(a,1),51(a,1,2))]. 805 x ^ (x -> 0) = x ^ ~ x. [para(19(a,1),51(a,1,2)),flip(a)]. 819 x v (x v y) = x v y. [para(79(a,1),2(a,1,1)),flip(a)]. 849 (~ x v y) => 0 = x ^ (y => 0). [para(251(a,1),39(a,1,1)),flip(a)]. 876 (x => (y ^ z)) => (x => y) = 1. [para(37(a,1),126(a,1,1))]. 925 (x -> y) ^ y = y. [para(145(a,1),41(a,1,1))]. 938 x v ((y -> x) ^ z) = (y -> x) ^ (x v z). [para(925(a,1),28(a,1,1))]. 960 (x v y) => (y => x) = (x v y) -> x. [para(595(a,1),21(a,1,2))]. 1014 x v (y ^ (x v z)) = (x v y) ^ (x v z). [para(819(a,1),27(a,1,2)),flip(a)]. 1056 x ^ (1 => ((y ^ (x => z)) => z)) = x. [para(369(a,1),17(a,1,2,1))]. 1097 (x v y) -> (x -> z) = x -> z. [para(7(a,1),764(a,1,1)),flip(a)]. 1106 x -> ((y => x) -> z) = x -> z. [para(41(a,1),764(a,1,1)),flip(a)]. 1127 x -> (y -> z) = y -> (x -> z). [para(764(a,1),50(a,1))]. 1164 x => ((x => (y ^ z)) => y) = 1. [para(876(a,1),35(a,1)),flip(a)]. 1195 x -> ((y * (y => x)) -> z) = (y * (y => x)) -> z. [para(38(a,1),1097(a,1,1))]. 1342 (x v y) => 0 = ~ x ^ ~ y. [para(23(a,1),510(a,1,2)),flip(a)]. 1377 ~ x ^ ~ y = ~ (x v y). [para(1342(a,1),23(a,1))]. 1420 ~ (~ x v y) = x ^ ~ y. [para(29(a,1),1377(a,1,1)),flip(a)]. 1449 (x ^ ~ y) => 0 = ~ x v y. [para(1420(a,1),251(a,1,1))]. 1548 (~ x v y) => (x ^ (y => 0)) = (~ x v y) -> 0. [para(849(a,1),21(a,1,2))]. 1723 x => ((y v x) => y) = (y v x) -> y. [para(960(a,1),35(a,1)),flip(a)]. 1773 x ^ ((y ^ (x => z)) => z) = x. [para(9(a,1),1056(a,1,2))]. 1843 x ^ (((y v x) => z) => z) = x. [para(39(a,1),1773(a,1,2,1))]. 1893 x ^ (1 => (((y v x) => (z ^ u)) => z)) = x. [para(1164(a,1),1843(a,1,2,1))]. 1947 x => (x => y) = (y v x) -> y. [para(595(a,1),1723(a,1,2))]. 1975 (x v y) -> x = y -> x. [para(1947(a,1),21(a,1))]. 2115 x => (y => (x => (y => z))) = (x * y) -> z. [para(146(a,1),15(a,1)),flip(a)]. 2347 x => (y => ((z ^ (y => (x => u))) => u)) = 1. [para(391(a,1),369(a,1))]. 2370 (x ^ ~ y) => (z => (u => 0)) = z => (u => (~ x v y)). [para(1449(a,1),391(a,1,2,2)),flip(a)]. 2437 x v (y ^ (z -> x)) = (z -> x) ^ (x v y). [para(5(a,1),938(a,1,2))]. 2538 x v (y ^ (x v z)) = x v (y ^ z). [para(27(a,1),1014(a,2))]. 2653 x v (y ^ (y -> x)) = x v (y ^ ~ y). [para(800(a,1),2538(a,1,2))]. 2748 x ^ (((y v x) => (z ^ u)) => z) = x. [para(9(a,1),1893(a,1,2))]. 2940 x => (x => (y -> z)) = (x * y) -> z. [para(372(a,1),2115(a,1,2))]. 2983 (x * y) -> z = x -> (y -> z). [para(2940(a,1),21(a,1))]. 3309 (x -> y) ^ (y v x) = y v (x ^ ~ x). [para(2437(a,1),2653(a,1))]. 3494 x -> (y -> ((y => x) -> z)) = (y * (y => x)) -> z. [para(2983(a,1),1195(a,1,2))]. 3589 x ^ (((~ y v x) -> 0) => y) = x. [para(1548(a,1),2748(a,1,2,1))]. 3632 x => (((~ (x => y) v z) -> 0) => (z => y)) = 1. [para(3589(a,1),2347(a,1,2,2,1))]. 3636 x => (((y v ~ (x => z)) -> 0) => (y => z)) = 1. [para(4(a,1),3632(a,1,2,1,1))]. 3796 x => (y => (((y v ~ (x => z)) -> 0) => z)) = 1. [para(35(a,1),3636(a,1,2))]. 3896 x => (y => (((y v ~ ~ x) -> 0) => 0)) = 1. [para(23(a,1),3796(a,1,2,2,1,1,2,1))]. 4000 x => (y => (((y v x) -> 0) => 0)) = 1. [para(29(a,1),3896(a,1,2,2,1,1,2))]. 4064 x => (y => ~ ((y v x) -> 0)) = 1. [para(23(a,1),4000(a,1,2,2))]. 4280 x -> (y -> ((x => y) -> z)) = (x * (x => y)) -> z. [para(3494(a,1),1127(a,1)),flip(a)]. 4427 (x * (x => y)) -> z = x -> (y -> z). [para(1106(a,1),4280(a,1,2)),flip(a)]. 4512 (x * (x -> y)) -> z = x -> ((x => y) -> z). [para(21(a,1),4427(a,1,1,2))]. 4596 x -> ((x => y) -> z) = x -> (y -> z). [para(4427(a,1),2983(a,1)),flip(a)]. 4885 (x * (x -> y)) -> z = x -> (y -> z). [para(4596(a,1),4512(a,2))]. 4955 x -> ((x -> y) -> z) = x -> (y -> z). [para(4885(a,1),2983(a,1)),flip(a)]. 5035 (x v y) -> (((x v y) -> x) -> z) = x -> z. [para(1097(a,1),4955(a,2))]. 5177 (x v y) -> ((y -> x) -> z) = x -> z. [para(1975(a,1),5035(a,1,2,1))]. 5257 ((x -> y) ^ (y v x)) -> z = y -> z. [para(5177(a,1),764(a,2))]. 5405 (x v (y ^ ~ y)) -> z = x -> z. [para(3309(a,1),5257(a,1,1))]. 5517 (x ^ ~ x) => (y => ~ (y -> 0)) = 1. [para(5405(a,1),4064(a,1,2,2,1))]. 5653 (x ^ ~ y) => (z => ~ u) = z => (u => (~ x v y)). [para(23(a,1),2370(a,1,2,2))]. 5906 x => ((x -> 0) => (~ y v y)) = 1. [para(5653(a,1),5517(a,1))]. 5908 x => ((x -> 0) => (y v ~ y)) = 1. [para(4(a,1),5906(a,1,2,2))]. 6003 (x ^ y) => ((x -> (y -> 0)) => (z v ~ z)) = 1. [para(50(a,1),5908(a,1,2,1))]. 6083 ((x -> 0) ^ x) => (1 => (y v ~ y)) = 1. [para(47(a,1),6003(a,1,2,1))]. 6161 (x ^ (x -> 0)) => (1 => (y v ~ y)) = 1. [para(5(a,1),6083(a,1,1))]. 6258 (x ^ ~ x) => (1 => (y v ~ y)) = 1. [para(805(a,1),6161(a,1,1))]. 6306 (x ^ ~ x) => (y v ~ y) = 1. [para(9(a,1),6258(a,1,2))]. 6369 (x ^ ~ x) ^ (1 => (y v ~ y)) = x ^ ~ x. [para(6306(a,1),17(a,1,2,1))]. 6424 (x ^ ~ x) ^ (y v ~ y) = x ^ ~ x. [para(9(a,1),6369(a,1,2))]. 6425 $F # answer("(N1)"). [resolve(6424,a,52,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=122. Generated=7792. Kept=6420. proofs=1. Usable=123. Sos=6229. Demods=0. Limbo=10, Disabled=105. Hints=92. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=1372. Back_subsumed=57. 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.15. User_CPU=0.26, System_CPU=0.02, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED THEOREM PROVED Exiting with 1 proof. ------ process 26338 exit (max_proofs) ------  Process 26338 exit (max_proofs) Sat Jan 19 14:19:13 2008