============================== Prover9 =============================== Prover9 (64) version 2009-02A, February 2009. Process 9526 was started by veroff on proof, Sat Sep 19 09:10:41 2009 The command was "prover9 -f 2.2a.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file 2.2a.in op(400,infix,[^,v,"=>",*]). op(200,prefix,~). lex([0,1,*,^,=>,v,~]). assign(order,kbo). set(lex_order_vars). set(para_units_only). % set(para_units_only) -> assign(para_lit_limit, 1). clear(back_demod). set(para_from_small). set(para_into_vars). 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 ^ x = x # label("(D3)"). x v x = x # label("(D4)"). x v y = y v x # label("(D5)"). x ^ y = y ^ x # label("(D6)"). x v (x ^ y) = x # label("(D7)"). x ^ (x v y) = x # label("(D8)"). x ^ 0 = 0 # label("(D9)"). x ^ 1 = x # label("(D10)"). x * 1 = x # label("(M1)"). x * y = y * x # label("(M2)"). (x * y) * z = x * (y * z) # label("(M3)"). x * (y v z) = (x * y) v (x * z) # label("(R1)"). x => (y ^ z) = (x => y) ^ (x => z) # label("(R2)"). (x * (x => y)) v y = y # label("(R3)"). (x => (x * y)) ^ y = y # label("(R4)"). x => (x => (x => y)) = x => (x => y) # label("(E_2)"). (x v y) ^ (x v z) = x v (y ^ z) # label("(D11)"). (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D12)"). ~ ~ x = x # label("(I)"). (x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y # label("(N)"). ~ x = x => 0 # label("(~ def)"). end_of_list. formulas(goals). x => ((x => y) => y) = 1 # label("(A1)[= 1]"). (x => y) => ((y => z) => (x => z)) = 1 # label("(A2)[= 1]"). (x ^ y) => x = 1 # label("(A3)[= 1]"). (x ^ y) => y = 1 # label("(A4)[= 1]"). ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]"). x => (x v y) = 1 # label("(A6)[= 1]"). y => (x v y) = 1 # label("(A7)[= 1]"). ((x => z) ^ (y => z)) => ((x v y) => z) = 1 # label("(A8)[= 1]"). (x ^ (y v z)) => ((x ^ y) v z) = 1 # label("(A9)[= 1]"). ~ ~ x => x = 1 # label("(A10)[= 1]"). (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). x => (y => x) = 1 # label("(A12)[= 1]"). ((x => (x => y)) ^ (~ y => (x => y))) => (x => y) = 1 # label("(A13)[= 1]"). end_of_list. formulas(hints). x => ((x => y) => y) = 1. (x => y) => ((y => z) => (x => z)) = 1. (x ^ y) => x = 1. (x ^ y) => y = 1. ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1. x => (x v y) = 1. y => (x v y) = 1. ((x => z) ^ (y => z)) => ((x v y) => z) = 1. (x ^ (y v z)) => ((x ^ y) v z) = 1. ~ ~ x => x = 1. (x => ~ y) => (y => ~ x) = 1. x => (y => x) = 1. ((x => (x => y)) ^ (~ y => (x => y))) => (x => y) = 1. x ^ 1 = x. x * 1 = x. x => (y ^ z) = (x => y) ^ (x => z). (x => y) ^ (x => z) = x => (y ^ z). (x => (x * y)) ^ y = y. 1 = x => (x * 1). x => (x * 1) = 1. x => x = 1. ~ ~ x = x. x ^ y = y ^ x. (x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y. (x => (x => ~ y)) ^ (y => (~ ~ y => ~ x)) = x => ~ y. (x => (x => ~ y)) ^ (y => (y => ~ x)) = x => ~ y. x => ~ y = (y => (y => ~ x)) ^ (x => (x => ~ y)). (x => (x => ~ y)) ^ (y => (y => ~ x)) = y => ~ x. x => ~ y = y => ~ x. x => y = ~ y => ~ x. ~ x => ~ y = y => x. (x => (x => y)) ^ (~ y => (x => y)) = x => y. x ^ (x v y) = x. x = 1 ^ x. 1 ^ x = x. x => (x ^ (x v y)) = 1. 1 ^ (x => y) = x => (x ^ y). x => (x ^ y) = 1 ^ (x => y). x => (x ^ y) = x => y. x v y = y v x. x v (x ^ y) = x. x v (y ^ x) = x. x = (y ^ x) v x. (x ^ y) v y = y. x = (x ^ y) v x. (x ^ y) v x = x. (x v y) ^ (x v z) = x v (y ^ z). (x ^ y) v (x ^ z) = x ^ (y v z). (x v (y ^ z)) => (x v z) = 1. x ^ 0 = 0. x * y = y * x. x * (y v z) = (x * y) v (x * z). (x * y) v (x * z) = x * (y v z). (x * (x => y)) v y = y. ~ x = x => 0. x => 0 = ~ x. x ^ (y v x) = x. x v 0 = x. 1 * x = x. x = x v (y * (y => x)). x v (y * (y => x)) = x. x = x ^ (y => (y * x)). x ^ (y => (y * x)) = x. (x => (y * x)) ^ y = y. ~ x => 0 = x. x * (x => 0) = 0. x = (y v x) ^ x. (x v y) ^ y = y. x * ~ x = 0. 0 = ~ x * x. ~ x * x = 0. x v (y * ~ y) = x. 0 = ~ 1. ~ 1 = 0. x * y = x * (y v ~ x). x * (y v ~ x) = x * y. x * (y v ~ x) = y * x. ~ x * (y v x) = y * ~ x. ~ x * (x v y) = y * ~ x. ~ x * x = (x ^ y) * ~ x. (x ^ y) * ~ x = ~ x * x. (x ^ y) * ~ x = 0. ~ x ^ ((x ^ y) => 0) = ~ x. ~ x ^ ~ (x ^ y) = ~ x. ~ (x v y) ^ ~ y = ~ (x v y). ~ x => y = ~ y => x. ~ 0 = 1. x = ~ 0 => x. ~ 0 => x = x. 1 => x = x. (x => (y ^ z)) => (x => z) = 1. (x => y) => (x => (y v z)) = 1. (x => ~ (y v z)) => (x => ~ z) = 1. ((x v y) => z) => (~ z => ~ y) = 1. ((x v y) => z) => (y => z) = 1. (x => y) => ((x ^ z) => y) = 1. ((x => (y * x)) => z) => (y => z) = 1. 1 => (x => (y => ((x * y) v z))) = 1. 1 => (x => (y => (z v (x * y)))) = 1. 1 = x => (y => (z v (x * y))). x => (y => (z v (x * y))) = 1. x v (x * y) = x * (1 v y). 1 v x = 1. x v (x * y) = x * 1. x v (x * y) = x. (x * y) * z = x * (y * z). x = (x v y) ^ x. (x v y) ^ x = x. x * (y * z) = z * (x * y). x ^ (y => (x * y)) = x. x * (y * z) = y * (x * z). 0 = ~ x * (x ^ y). ~ x * (x ^ y) = 0. x * ~ (x v y) = 0. ~ (x v y) * y = 0. (x * (x => y)) * ~ y = 0. ~ x * (y * (y => x)) = 0. 0 = x * ((x => y) * ~ y). x * ((x => y) * ~ y) = 0. x * (y * (y => ~ x)) = 0. 0 = x * (y * (x => ~ y)). x * (y * (x => ~ y)) = 0. (x * y) * (x => ~ y) = 0. x v (~ y * (~ x => y)) = x. x => (y => (x * y)) = 1. (x * y) => ((x => ~ y) => 0) = 1. (x * y) => ~ (x => ~ y) = 1. (x * ~ y) => ~ (x => y) = 1. 1 = (x => y) => ~ (x * ~ y). (x => y) => ~ (x * ~ y) = 1. 1 => (x => ~ (y * ~ (x * y))) = 1. 1 = x => ~ (y * ~ (x * y)). x => ~ (y * ~ (x * y)) = 1. x v (~ ~ (y * ~ (~ x * y)) * 1) = x. x * (1 * ~ ((x => y) => y)) = 0. x * ~ ((x => y) => y) = 0. x ^ (~ ((x => y) => y) => 0) = x. x ^ ((x => y) => y) = x. (x => y) => (x => ((y => z) => z)) = 1. (x => y) ^ (1 => ~ (x * ~ y)) = x => y. x ^ (1 => (y => (z v (x * y)))) = x. x ^ (y => (z v (x * y))) = x. x = (y => (z v (x * y))) ^ x. (x => (y v (z * x))) ^ z = z. (x => (y v (x * z))) ^ z = z. x v (~ ~ (y * ~ (y * ~ x)) * 1) = x. (x => y) ^ ~ (x * ~ y) = x => y. x v ((y * ~ (y * ~ x)) * 1) = x. x v (y * ~ (y * ~ x)) = x. (x => y) ^ ~ (x * ~ y) = ~ (x * ~ y). ~ (x * ~ y) = x => y. ~ (x * y) = x => ~ y. ~ (x * (y * z)) = (x * y) => ~ z. ~ (x * (y * z)) = z => ~ (x * y). x => ~ (y * z) = y => ~ (z * x). x => ~ (y * z) = z => ~ (x * y). x => (y => ~ z) = z => ~ (x * y). x => ~ (y * z) = y => (z => ~ x). x => (y => z) = y => (~ z => ~ x). x => (~ y => ~ z) = z => (x => y). x => (y => z) = y => (x => z). (x v y) v z = x v (y v z). x v (y v z) = y v (z v x). x v (y v z) = z v (x v y). x v ((x ^ y) v z) = z v x. x v (y v (x ^ z)) = y v x. x v (y v (x ^ z)) = x v y. x => (y => (y * x)) = 1. (x v y) => (~ y => (x * ~ y)) = 1. ((x v y) => z) => (x => z) = 1. (x => y) v (((x v z) => y) * 1) = x => y. ((x => y) => y) v x = (x => y) => y. (((x => y) => y) => z) => (x => z) = 1. 1 => (x => (((x => y) ^ z) => y)) = 1. 1 = x => (((x => y) ^ z) => y). x => (((x => y) ^ z) => y) = 1. x => ((y ^ (x => z)) => z) = 1. x ^ (1 => ((y ^ (x => z)) => z)) = x. x ^ ((y ^ (x => z)) => z) = x. (x => y) v ((x v z) => y) = x => y. (x => y) => z = ~ z => (x * ~ y). ~ x => (y * ~ z) = (y => z) => x. (x v y) => ((x => y) => y) = 1. (x => y) => ((x v y) => y) = 1. ((x v y) => y) v ((x => y) * 1) = (x v y) => y. ((x v y) => y) v (x => y) = (x v y) => y. (x v y) => y = (x => y) v ((x v y) => y). (x => y) v ((x v y) => y) = (x v y) => y. (x v y) => y = x => y. (x v y) => x = y => x. (x v y) => x = (y v (x ^ z)) => x. (x v (y ^ z)) => y = (y v x) => y. (x v (y ^ z)) => y = x => y. (x v (y ^ z)) => z = x => z. (x v y) => ((z ^ (y => u)) => u) = x => ((z ^ (y => u)) => u). (x v y) => (((x => z) ^ (y => z)) => z) = 1. 1 = ((x => y) ^ (z => y)) => ((x v z) => y). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 x => ((x => y) => y) = 1 # label("(A1)[= 1]") # label(non_clause) # label(goal). [goal]. 2 (x => y) => ((y => z) => (x => z)) = 1 # label("(A2)[= 1]") # label(non_clause) # label(goal). [goal]. 3 (x ^ y) => x = 1 # label("(A3)[= 1]") # label(non_clause) # label(goal). [goal]. 4 (x ^ y) => y = 1 # label("(A4)[= 1]") # label(non_clause) # label(goal). [goal]. 5 ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]") # label(non_clause) # label(goal). [goal]. 6 x => (x v y) = 1 # label("(A6)[= 1]") # label(non_clause) # label(goal). [goal]. 7 y => (x v y) = 1 # label("(A7)[= 1]") # label(non_clause) # label(goal). [goal]. 8 ((x => z) ^ (y => z)) => ((x v y) => z) = 1 # label("(A8)[= 1]") # label(non_clause) # label(goal). [goal]. 9 (x ^ (y v z)) => ((x ^ y) v z) = 1 # label("(A9)[= 1]") # label(non_clause) # label(goal). [goal]. 10 ~ ~ x => x = 1 # label("(A10)[= 1]") # label(non_clause) # label(goal). [goal]. 11 (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]") # label(non_clause) # label(goal). [goal]. 12 x => (y => x) = 1 # label("(A12)[= 1]") # label(non_clause) # label(goal). [goal]. 13 ((x => (x => y)) ^ (~ y => (x => y))) => (x => y) = 1 # label("(A13)[= 1]") # 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 ^ x = x # label("(D3)"). [assumption]. x v x = x # label("(D4)"). [assumption]. x v y = y v x # label("(D5)"). [assumption]. x ^ y = y ^ x # label("(D6)"). [assumption]. x v (x ^ y) = x # label("(D7)"). [assumption]. x ^ (x v y) = x # label("(D8)"). [assumption]. x ^ 0 = 0 # label("(D9)"). [assumption]. x ^ 1 = x # label("(D10)"). [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 v z) = (x * y) v (x * z) # label("(R1)"). [assumption]. x => (y ^ z) = (x => y) ^ (x => z) # label("(R2)"). [assumption]. (x * (x => y)) v y = y # label("(R3)"). [assumption]. (x => (x * y)) ^ y = y # label("(R4)"). [assumption]. x => (x => (x => y)) = x => (x => y) # label("(E_2)"). [assumption]. (x v y) ^ (x v z) = x v (y ^ z) # label("(D11)"). [assumption]. (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D12)"). [assumption]. ~ ~ x = x # label("(I)"). [assumption]. (x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y # label("(N)"). [assumption]. ~ x = x => 0 # label("(~ def)"). [assumption]. c1 => ((c1 => c2) => c2) != 1 # label("(A1)[= 1]"). [deny(1)]. (c3 => c4) => ((c4 => c5) => (c3 => c5)) != 1 # label("(A2)[= 1]"). [deny(2)]. (c6 ^ c7) => c6 != 1 # label("(A3)[= 1]"). [deny(3)]. (c8 ^ c9) => c9 != 1 # label("(A4)[= 1]"). [deny(4)]. ((c10 => c11) ^ (c10 => c12)) => (c10 => (c11 ^ c12)) != 1 # label("(A5)[= 1]"). [deny(5)]. c13 => (c13 v c14) != 1 # label("(A6)[= 1]"). [deny(6)]. c15 => (c16 v c15) != 1 # label("(A7)[= 1]"). [deny(7)]. ((c17 => c18) ^ (c19 => c18)) => ((c17 v c19) => c18) != 1 # label("(A8)[= 1]"). [deny(8)]. (c20 ^ (c21 v c22)) => ((c20 ^ c21) v c22) != 1 # label("(A9)[= 1]"). [deny(9)]. ~ ~ c23 => c23 != 1 # label("(A10)[= 1]"). [deny(10)]. (c24 => ~ c25) => (c25 => ~ c24) != 1 # label("(A11)[= 1]"). [deny(11)]. c26 => (c27 => c26) != 1 # label("(A12)[= 1]"). [deny(12)]. ((c28 => (c28 => c29)) ^ (~ c29 => (c28 => c29))) => (c28 => c29) != 1 # label("(A13)[= 1]"). [deny(13)]. end_of_list. formulas(demodulators). end_of_list. % 197 hints input. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination =============  WARNING: denials share constants (see output). Auto_denials: % copying label "(A1)[= 1]" to answer in negative clause % copying label "(A2)[= 1]" to answer in negative clause % copying label "(A3)[= 1]" to answer in negative clause % copying label "(A4)[= 1]" to answer in negative clause % copying label "(A5)[= 1]" to answer in negative clause % copying label "(A6)[= 1]" to answer in negative clause % copying label "(A7)[= 1]" to answer in negative clause % copying label "(A8)[= 1]" to answer in negative clause % copying label "(A9)[= 1]" to answer in negative clause % copying label "(A10)[= 1]" to answer in negative clause % copying label "(A11)[= 1]" to answer in negative clause % copying label "(A12)[= 1]" to answer in negative clause % copying label "(A13)[= 1]" to answer in negative clause % assign(max_proofs, 13). % (Horn set with more than one neg. clause) WARNING, because some of the denials share constants, some of the denials or their descendents may be subsumed, preventing the target number of proofs from being found. The shared constants are: 1. Term ordering decisions: Function symbol KB weights: 0=1. 1=1. c1=1. c2=1. c3=1. c4=1. c5=1. c6=1. c7=1. c8=1. c9=1. c10=1. c11=1. c12=1. c13=1. c14=1. c15=1. c16=1. c17=1. c18=1. c19=1. c20=1. c21=1. c22=1. c23=1. c24=1. c25=1. c26=1. c27=1. c28=1. c29=1. *=1. ^=1. =>=1. v=1. ~=1. Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ 0, 1, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, *, ^, =>, v, ~ ]). Skipping inverse_order, because there is a function_order (lex) command. Skipping unfold_eq, because there is a function_order (lex) command. Auto_inference settings: % set(paramodulation). % (positive equality literals) Auto_process settings: (no changes). kept: 14 (x v y) v z = x v (y v z) # label("(D1)"). [assumption]. kept: 15 (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)"). [assumption]. kept: 16 x ^ x = x # label("(D3)"). [assumption]. kept: 17 x v x = x # label("(D4)"). [assumption]. % Operation v is commutative; C redundancy checks enabled. kept: 18 x v y = y v x # label("(D5)"). [assumption]. % Operation ^ is commutative; C redundancy checks enabled. kept: 19 x ^ y = y ^ x # label("(D6)"). [assumption]. kept: 20 x v (x ^ y) = x # label("(D7)"). [assumption]. kept: 21 x ^ (x v y) = x # label("(D8)"). [assumption]. kept: 22 x ^ 0 = 0 # label("(D9)"). [assumption]. kept: 23 x ^ 1 = x # label("(D10)"). [assumption]. kept: 24 x * 1 = x # label("(M1)"). [assumption]. % Operation * is commutative; C redundancy checks enabled. kept: 25 x * y = y * x # label("(M2)"). [assumption]. kept: 26 (x * y) * z = x * (y * z) # label("(M3)"). [assumption]. 27 x * (y v z) = (x * y) v (x * z) # label("(R1)"). [assumption]. kept: 28 (x * y) v (x * z) = x * (y v z). [copy(27),flip(a)]. 29 x => (y ^ z) = (x => y) ^ (x => z) # label("(R2)"). [assumption]. kept: 30 (x => y) ^ (x => z) = x => (y ^ z). [copy(29),flip(a)]. kept: 31 (x * (x => y)) v y = y # label("(R3)"). [assumption]. kept: 32 (x => (x * y)) ^ y = y # label("(R4)"). [assumption]. kept: 33 x => (x => (x => y)) = x => (x => y) # label("(E_2)"). [assumption]. kept: 34 (x v y) ^ (x v z) = x v (y ^ z) # label("(D11)"). [assumption]. kept: 35 (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D12)"). [assumption]. kept: 36 ~ ~ x = x # label("(I)"). [assumption]. kept: 37 (x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y # label("(N)"). [assumption]. 38 ~ x = x => 0 # label("(~ def)"). [assumption]. kept: 39 x => 0 = ~ x. [copy(38),flip(a)]. kept: 40 c1 => ((c1 => c2) => c2) != 1 # label("(A1)[= 1]") # answer("(A1)[= 1]"). [deny(1)]. kept: 41 (c3 => c4) => ((c4 => c5) => (c3 => c5)) != 1 # label("(A2)[= 1]") # answer("(A2)[= 1]"). [deny(2)]. kept: 42 (c6 ^ c7) => c6 != 1 # label("(A3)[= 1]") # answer("(A3)[= 1]"). [deny(3)]. kept: 43 (c8 ^ c9) => c9 != 1 # label("(A4)[= 1]") # answer("(A4)[= 1]"). [deny(4)]. kept: 44 ((c10 => c11) ^ (c10 => c12)) => (c10 => (c11 ^ c12)) != 1 # label("(A5)[= 1]") # answer("(A5)[= 1]"). [deny(5)]. kept: 45 c13 => (c13 v c14) != 1 # label("(A6)[= 1]") # answer("(A6)[= 1]"). [deny(6)]. kept: 46 c15 => (c16 v c15) != 1 # label("(A7)[= 1]") # answer("(A7)[= 1]"). [deny(7)]. kept: 47 ((c17 => c18) ^ (c19 => c18)) => ((c17 v c19) => c18) != 1 # label("(A8)[= 1]") # answer("(A8)[= 1]"). [deny(8)]. kept: 48 (c20 ^ (c21 v c22)) => ((c20 ^ c21) v c22) != 1 # label("(A9)[= 1]") # answer("(A9)[= 1]"). [deny(9)]. kept: 49 ~ ~ c23 => c23 != 1 # label("(A10)[= 1]") # answer("(A10)[= 1]"). [deny(10)]. kept: 50 (c24 => ~ c25) => (c25 => ~ c24) != 1 # label("(A11)[= 1]") # answer("(A11)[= 1]"). [deny(11)]. kept: 51 c26 => (c27 => c26) != 1 # label("(A12)[= 1]") # answer("(A12)[= 1]"). [deny(12)]. kept: 52 ((c28 => (c28 => c29)) ^ (~ c29 => (c28 => c29))) => (c28 => c29) != 1 # label("(A13)[= 1]") # answer("(A13)[= 1]"). [deny(13)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 40 c1 => ((c1 => c2) => c2) != 1 # label("(A1)[= 1]") # answer("(A1)[= 1]"). [deny(1)]. 41 (c3 => c4) => ((c4 => c5) => (c3 => c5)) != 1 # label("(A2)[= 1]") # answer("(A2)[= 1]"). [deny(2)]. 42 (c6 ^ c7) => c6 != 1 # label("(A3)[= 1]") # answer("(A3)[= 1]"). [deny(3)]. 43 (c8 ^ c9) => c9 != 1 # label("(A4)[= 1]") # answer("(A4)[= 1]"). [deny(4)]. 44 ((c10 => c11) ^ (c10 => c12)) => (c10 => (c11 ^ c12)) != 1 # label("(A5)[= 1]") # answer("(A5)[= 1]"). [deny(5)]. 45 c13 => (c13 v c14) != 1 # label("(A6)[= 1]") # answer("(A6)[= 1]"). [deny(6)]. 46 c15 => (c16 v c15) != 1 # label("(A7)[= 1]") # answer("(A7)[= 1]"). [deny(7)]. 47 ((c17 => c18) ^ (c19 => c18)) => ((c17 v c19) => c18) != 1 # label("(A8)[= 1]") # answer("(A8)[= 1]"). [deny(8)]. 48 (c20 ^ (c21 v c22)) => ((c20 ^ c21) v c22) != 1 # label("(A9)[= 1]") # answer("(A9)[= 1]"). [deny(9)]. 49 ~ ~ c23 => c23 != 1 # label("(A10)[= 1]") # answer("(A10)[= 1]"). [deny(10)]. 50 (c24 => ~ c25) => (c25 => ~ c24) != 1 # label("(A11)[= 1]") # answer("(A11)[= 1]"). [deny(11)]. 51 c26 => (c27 => c26) != 1 # label("(A12)[= 1]") # answer("(A12)[= 1]"). [deny(12)]. 52 ((c28 => (c28 => c29)) ^ (~ c29 => (c28 => c29))) => (c28 => c29) != 1 # label("(A13)[= 1]") # answer("(A13)[= 1]"). [deny(13)]. end_of_list. formulas(sos). 14 (x v y) v z = x v (y v z) # label("(D1)"). [assumption]. 15 (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)"). [assumption]. 16 x ^ x = x # label("(D3)"). [assumption]. 17 x v x = x # label("(D4)"). [assumption]. 18 x v y = y v x # label("(D5)"). [assumption]. 19 x ^ y = y ^ x # label("(D6)"). [assumption]. 20 x v (x ^ y) = x # label("(D7)"). [assumption]. 21 x ^ (x v y) = x # label("(D8)"). [assumption]. 22 x ^ 0 = 0 # label("(D9)"). [assumption]. 23 x ^ 1 = x # label("(D10)"). [assumption]. 24 x * 1 = x # label("(M1)"). [assumption]. 25 x * y = y * x # label("(M2)"). [assumption]. 26 (x * y) * z = x * (y * z) # label("(M3)"). [assumption]. 28 (x * y) v (x * z) = x * (y v z). [copy(27),flip(a)]. 30 (x => y) ^ (x => z) = x => (y ^ z). [copy(29),flip(a)]. 31 (x * (x => y)) v y = y # label("(R3)"). [assumption]. 32 (x => (x * y)) ^ y = y # label("(R4)"). [assumption]. 33 x => (x => (x => y)) = x => (x => y) # label("(E_2)"). [assumption]. 34 (x v y) ^ (x v z) = x v (y ^ z) # label("(D11)"). [assumption]. 35 (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D12)"). [assumption]. 36 ~ ~ x = x # label("(I)"). [assumption]. 37 (x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y # label("(N)"). [assumption]. 39 x => 0 = ~ x. [copy(38),flip(a)]. end_of_list. formulas(demodulators). end_of_list. % 162 hints (197 processed, 35 redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.02 seconds. given #1 (I,wt=11): 14 (x v y) v z = x v (y v z) # label("(D1)"). [assumption]. given #2 (I,wt=11): 15 (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)"). [assumption]. given #3 (I,wt=5): 16 x ^ x = x # label("(D3)"). [assumption]. given #4 (I,wt=5): 17 x v x = x # label("(D4)"). [assumption]. given #5 (I,wt=7): 18 x v y = y v x # label("(D5)"). [assumption]. given #6 (I,wt=7): 19 x ^ y = y ^ x # label("(D6)"). [assumption]. given #7 (I,wt=7): 20 x v (x ^ y) = x # label("(D7)"). [assumption]. given #8 (I,wt=7): 21 x ^ (x v y) = x # label("(D8)"). [assumption]. given #9 (I,wt=5): 22 x ^ 0 = 0 # label("(D9)"). [assumption]. given #10 (I,wt=5): 23 x ^ 1 = x # label("(D10)"). [assumption]. given #11 (I,wt=5): 24 x * 1 = x # label("(M1)"). [assumption]. given #12 (I,wt=7): 25 x * y = y * x # label("(M2)"). [assumption]. given #13 (I,wt=11): 26 (x * y) * z = x * (y * z) # label("(M3)"). [assumption]. given #14 (I,wt=13): 28 (x * y) v (x * z) = x * (y v z). [copy(27),flip(a)]. given #15 (I,wt=13): 30 (x => y) ^ (x => z) = x => (y ^ z). [copy(29),flip(a)]. given #16 (I,wt=9): 31 (x * (x => y)) v y = y # label("(R3)"). [assumption]. given #17 (I,wt=9): 32 (x => (x * y)) ^ y = y # label("(R4)"). [assumption]. given #18 (I,wt=13): 33 x => (x => (x => y)) = x => (x => y) # label("(E_2)"). [assumption]. given #19 (I,wt=13): 34 (x v y) ^ (x v z) = x v (y ^ z) # label("(D11)"). [assumption]. given #20 (I,wt=13): 35 (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D12)"). [assumption]. given #21 (I,wt=5): 36 ~ ~ x = x # label("(I)"). [assumption]. given #22 (I,wt=18): 37 (x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y # label("(N)"). [assumption]. given #23 (I,wt=6): 39 x => 0 = ~ x. [copy(38),flip(a)]. given #24 (H,wt=5): 394 x v 0 = x. [para(22(a,1),20(a,1,2))]. given #25 (H,wt=5): 446 1 ^ x = x. [para(23(a,1),19(a,1)),flip(a)]. given #26 (H,wt=5): 573 1 * x = x. [para(25(a,1),24(a,1))]. given #27 (H,wt=5): 3825 1 v x = 1. [para(446(a,1),20(a,1,2))]. given #28 (H,wt=6): 3534 ~ x => 0 = x. [para(39(a,2),36(a,1))]. given #29 (H,wt=7): 268 (x ^ y) v x = x. [para(20(a,1),18(a,1)),flip(a)]. given #30 (H,wt=7): 277 x v (y ^ x) = x. [para(19(a,1),20(a,1,2))]. given #31 (H,wt=7): 341 x ^ (y v x) = x. [para(18(a,1),21(a,1,2))]. given #32 (H,wt=7): 344 (x v y) ^ x = x. [para(21(a,1),19(a,1)),flip(a)]. given #33 (H,wt=7): 1488 x => (x * 1) = 1. [para(32(a,1),23(a,1)),flip(a)]. given #34 (H,wt=5): 6180 x => x = 1. [para(24(a,1),1488(a,1,2))]. -------- Proof 1 -------- "(A5)[= 1]". ============================== PROOF ================================= % Proof 1 at 0.22 (+ 0.01) seconds: "(A5)[= 1]". % Length of proof is 11. % Level of proof is 4. % Maximum clause weight is 15. % Given clauses 34. 5 ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]") # label(non_clause) # label(goal). [goal]. 23 x ^ 1 = x # label("(D10)"). [assumption]. 24 x * 1 = x # label("(M1)"). [assumption]. 29 x => (y ^ z) = (x => y) ^ (x => z) # label("(R2)"). [assumption]. 30 (x => y) ^ (x => z) = x => (y ^ z). [copy(29),flip(a)]. 32 (x => (x * y)) ^ y = y # label("(R4)"). [assumption]. 44 ((c10 => c11) ^ (c10 => c12)) => (c10 => (c11 ^ c12)) != 1 # label("(A5)[= 1]") # answer("(A5)[= 1]"). [deny(5)]. 1488 x => (x * 1) = 1. [para(32(a,1),23(a,1)),flip(a)]. 6180 x => x = 1. [para(24(a,1),1488(a,1,2))]. 6469 ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1. [para(30(a,1),6180(a,1,2))]. 6470 $F # answer("(A5)[= 1]"). [resolve(6469,a,44,a)]. ============================== end of proof ========================== -------- Proof 2 -------- "(A10)[= 1]". ============================== PROOF ================================= % Proof 2 at 0.22 (+ 0.02) seconds: "(A10)[= 1]". % Length of proof is 10. % Level of proof is 4. % Maximum clause weight is 9. % Given clauses 34. 10 ~ ~ x => x = 1 # label("(A10)[= 1]") # label(non_clause) # label(goal). [goal]. 23 x ^ 1 = x # label("(D10)"). [assumption]. 24 x * 1 = x # label("(M1)"). [assumption]. 32 (x => (x * y)) ^ y = y # label("(R4)"). [assumption]. 36 ~ ~ x = x # label("(I)"). [assumption]. 49 ~ ~ c23 => c23 != 1 # label("(A10)[= 1]") # answer("(A10)[= 1]"). [deny(10)]. 1488 x => (x * 1) = 1. [para(32(a,1),23(a,1)),flip(a)]. 6180 x => x = 1. [para(24(a,1),1488(a,1,2))]. 6532 ~ ~ x => x = 1. [para(36(a,1),6180(a,1,2))]. 6533 $F # answer("(A10)[= 1]"). [resolve(6532,a,49,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 49 44 given #35 (H,wt=4): 6556 ~ 0 = 1. [para(6180(a,1),39(a,1)),flip(a)]. given #36 (H,wt=4): 6733 ~ 1 = 0. [para(6556(a,1),36(a,1,1))]. given #37 (H,wt=7): 3677 x * (x => 0) = 0. [para(394(a,1),31(a,1))]. given #38 (H,wt=6): 7163 x * ~ x = 0. [para(39(a,1),3677(a,1,2))]. given #39 (H,wt=6): 7185 ~ x * x = 0. [para(3534(a,1),3677(a,1,2))]. given #40 (H,wt=7): 4701 (x ^ y) v y = y. [para(19(a,1),268(a,1,1))]. given #41 (H,wt=7): 5418 (x v y) ^ y = y. [para(341(a,1),19(a,1)),flip(a)]. given #42 (H,wt=7): 6532 ~ ~ x => x = 1. [para(36(a,1),6180(a,1,2))]. given #43 (H,wt=8): 7423 x v (y * ~ y) = x. [para(7163(a,2),394(a,1,2))]. given #44 (H,wt=9): 1224 x v (y * (y => x)) = x. [para(31(a,1),18(a,1)),flip(a)]. given #45 (H,wt=9): 1448 x ^ (y => (y * x)) = x. [para(32(a,1),19(a,1)),flip(a)]. given #46 (H,wt=9): 1517 (x => (y * x)) ^ y = y. [para(25(a,1),32(a,1,1,2))]. given #47 (H,wt=9): 6421 x => (x ^ (x v y)) = 1. [para(21(a,1),6180(a,1,1))]. Low Water (keep): wt=37.000, iters=6803 Low Water (keep): wt=36.000, iters=6773 given #48 (H,wt=9): 10120 x ^ (y => (x * y)) = x. [para(25(a,1),1448(a,1,2,2))]. Low Water (keep): wt=25.000, iters=6669 given #49 (H,wt=10): 9081 x * (y v ~ x) = x * y. [para(7423(a,1),28(a,1)),flip(a)]. Low Water (keep): wt=24.000, iters=6892 given #50 (H,wt=10): 12525 x * (y v ~ x) = y * x. [para(9081(a,2),25(a,1))]. Low Water (keep): wt=22.000, iters=6905 Low Water (keep): wt=21.000, iters=6796 given #51 (H,wt=11): 170 x v (y v z) = z v (x v y). [para(18(a,1),14(a,1)),flip(a)]. % Operation v is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 170 x v (y v z) = z v (x v y). [para(18(a,1),14(a,1)),flip(a)]. % back CAC tautology: 13638 (x v y) v (z v u) = z v (u v (y v x)). [para(18(a,1),170(a,1,2,2)),flip(a)]. % back CAC tautology: 13637 x v ((y v z) v u) = u v (x v (z v y)). [para(18(a,1),170(a,1,2,1))]. % back CAC tautology: 13636 (x v y) v (z v u) = u v ((y v x) v z). [para(18(a,1),170(a,1,1))]. % back CAC tautology: 13635 (x v (y v z)) v u = u v (z v (x v y)). [para(170(a,1),18(a,1,2)),flip(a)]. % back CAC tautology: 13634 (x v (y v z)) v u = u v (y v (z v x)). [para(170(a,1),18(a,1,1))]. % back CAC tautology: 13591 x v ((y v z) v u) = u v ((x v y) v z). [para(14(a,2),170(a,2,2))]. % back CAC tautology: 13590 (x v y) v (z v u) = z v ((u v x) v y). [para(14(a,2),170(a,1,2)),flip(a)]. % back CAC tautology: 13589 (x v y) v (z v u) = u v (x v (y v z)). [para(14(a,1),170(a,2,2))]. % back CAC tautology: 13588 x v (((y v z) v u) v w) = w v (x v (y v (z v u))). [para(14(a,1),170(a,2,2,2))]. % back CAC tautology: 13587 ((x v y) v z) v (u v w) = w v ((x v (y v z)) v u). [para(14(a,1),170(a,2,2,1))]. % back CAC tautology: 13586 (x v (y v z)) v (u v w) = u v (w v ((x v y) v z)). [para(14(a,1),170(a,2,1)),flip(a)]. % back CAC tautology: 13585 x v (y v (z v u)) = u v (x v (y v z)). [para(14(a,1),170(a,1,2))]. % back CAC tautology: 13584 ((x v y) v z) v (u v w) = u v (w v (x v (y v z))). [para(14(a,1),170(a,1,2,2)),flip(a)]. % back CAC tautology: 13583 x v ((y v (z v u)) v w) = w v (x v ((y v z) v u)). [para(14(a,1),170(a,1,2,1))]. % back CAC tautology: 13582 (x v (y v z)) v (u v w) = w v (((x v y) v z) v u). [para(14(a,1),170(a,1,1))]. % back CAC tautology: 13581 (x v y) v z = y v (z v x). [para(170(a,2),14(a,2))]. % back CAC tautology: 13580 (x v y) v (z v u) = x v (z v (u v y)). [para(170(a,2),14(a,2,2))]. % back CAC tautology: 13579 x v (y v (z v u)) = z v (u v (x v y)). [para(170(a,2),14(a,1))]. % back CAC tautology: 13578 (x v (y v z)) v u = z v ((x v y) v u). [para(170(a,2),14(a,1,1))]. % back CAC tautology: 13577 (x v y) v (z v u) = x v (u v (y v z)). [para(170(a,1),14(a,2,2))]. % back CAC tautology: 13576 (x v y) v (z v (u v w)) = x v (y v (w v (z v u))). [para(170(a,1),14(a,2,2,2))]. % back CAC tautology: 13575 (x v (y v (z v u))) v w = x v ((u v (y v z)) v w). [para(170(a,1),14(a,2,2,1))]. % back CAC tautology: 13574 ((x v (y v z)) v u) v w = (z v (x v y)) v (u v w). [para(170(a,1),14(a,2,1))]. % back CAC tautology: 13573 x v ((y v z) v u) = y v (z v (u v x)). [para(170(a,1),14(a,1))]. % back CAC tautology: 13572 (x v y) v (z v (u v w)) = x v (y v (u v (w v z))). [para(170(a,1),14(a,1,2))]. % back CAC tautology: 13571 (x v (y v z)) v u = y v ((z v x) v u). [para(170(a,1),14(a,1,1))]. % back CAC tautology: 13570 (x v (y v (z v u))) v w = x v ((z v (u v y)) v w). [para(170(a,1),14(a,1,1,2))]. % back CAC tautology: 13569 ((x v (y v z)) v u) v w = (y v (z v x)) v (u v w). [para(170(a,1),14(a,1,1,1))]. % back CAC tautology: 541 ((x v y) v z) * u = u * (x v (y v z)). [para(14(a,1),25(a,1,2)),flip(a)]. % back CAC tautology: 540 (x v (y v z)) * u = u * ((x v y) v z). [para(14(a,1),25(a,1,1))]. % back CAC tautology: 539 (x v y) v (z * u) = x v (y v (u * z)). [para(25(a,1),14(a,1,2))]. % back CAC tautology: 538 (x v (y * z)) v u = x v ((z * y) v u). [para(25(a,1),14(a,1,1,2))]. % back CAC tautology: 537 ((x * y) v z) v u = (y * x) v (z v u). [para(25(a,1),14(a,1,1,1))]. % back CAC tautology: 194 ((x v y) v z) ^ u = u ^ (x v (y v z)). [para(14(a,1),19(a,1,2)),flip(a)]. % back CAC tautology: 193 (x v (y v z)) ^ u = u ^ ((x v y) v z). [para(14(a,1),19(a,1,1))]. % back CAC tautology: 192 (x v y) v (z ^ u) = x v (y v (u ^ z)). [para(19(a,1),14(a,1,2))]. % back CAC tautology: 191 (x v (y ^ z)) v u = x v ((z ^ y) v u). [para(19(a,1),14(a,1,1,2))]. % back CAC tautology: 190 ((x ^ y) v z) v u = (y ^ x) v (z v u). [para(19(a,1),14(a,1,1,1))]. % back CAC tautology: 174 ((x v y) v z) v u = u v (x v (y v z)). [para(14(a,1),18(a,1,2)),flip(a)]. % back CAC tautology: 173 (x v (y v z)) v u = u v ((x v y) v z). [para(14(a,1),18(a,1,1))]. % back CAC tautology: 172 (x v y) v z = (z v x) v y. [para(18(a,1),14(a,2)),flip(a)]. % back CAC tautology: 171 (x v y) v z = x v (z v y). [para(18(a,1),14(a,2,2))]. % back CAC tautology: 169 (x v y) v (z v u) = x v (y v (u v z)). [para(18(a,1),14(a,1,2))]. % back CAC tautology: 168 (x v y) v z = y v (x v z). [para(18(a,1),14(a,1,1))]. % back CAC tautology: 167 (x v (y v z)) v u = x v ((z v y) v u). [para(18(a,1),14(a,1,1,2))]. % back CAC tautology: 166 ((x v y) v z) v u = (y v x) v (z v u). [para(18(a,1),14(a,1,1,1))]. % back CAC tautology: 63 (x v y) v (z v u) = x v ((y v z) v u). [para(14(a,2),14(a,2,2))]. % back CAC tautology: 62 ((x v y) v z) v u = x v ((y v z) v u). [para(14(a,2),14(a,1,1))]. % back CAC tautology: 61 ((x v y) v z) v u = x v (y v (z v u)). [para(14(a,1),14(a,2))]. % back CAC tautology: 60 (x v (y v z)) v u = x v (y v (z v u)). [para(14(a,1),14(a,2,2))]. % back CAC tautology: 59 (x v y) v ((z v u) v w) = x v (y v (z v (u v w))). [para(14(a,1),14(a,2,2,2))]. % back CAC tautology: 58 (x v ((y v z) v u)) v w = x v ((y v (z v u)) v w). [para(14(a,1),14(a,2,2,1))]. % back CAC tautology: 57 (((x v y) v z) v u) v w = (x v (y v z)) v (u v w). [para(14(a,1),14(a,2,1))]. % back CAC tautology: 56 (x v y) v (z v (u v w)) = x v (y v ((z v u) v w)). [para(14(a,1),14(a,1,2))]. % back CAC tautology: 55 (x v (y v z)) v u = (x v y) v (z v u). [para(14(a,1),14(a,1,1))]. % back CAC tautology: 54 (x v (y v (z v u))) v w = x v (((y v z) v u) v w). [para(14(a,1),14(a,1,1,2))]. % back CAC tautology: 53 ((x v (y v z)) v u) v w = ((x v y) v z) v (u v w). [para(14(a,1),14(a,1,1,1))]. given #52 (H,wt=11): 696 x * (y * z) = z * (x * y). [para(26(a,1),25(a,1))]. Low Water (keep): wt=19.000, iters=6678 % Operation * is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 696 x * (y * z) = z * (x * y). [para(26(a,1),25(a,1))]. % back CAC tautology: 14134 (x * y) * (z * u) = z * (u * (y * x)). [para(25(a,1),696(a,1,2,2)),flip(a)]. % back CAC tautology: 14133 x * ((y * z) * u) = u * (x * (z * y)). [para(25(a,1),696(a,1,2,1))]. % back CAC tautology: 14132 (x * y) * (z * u) = u * ((y * x) * z). [para(25(a,1),696(a,1,1))]. % back CAC tautology: 14131 (x * y) * z = y * (z * x). [para(696(a,1),25(a,1)),flip(a)]. % back CAC tautology: 14130 (x * (y * z)) * u = u * (z * (x * y)). [para(696(a,1),25(a,1,2)),flip(a)]. % back CAC tautology: 14129 (x * (y * z)) * u = u * (y * (z * x)). [para(696(a,1),25(a,1,1))]. % back CAC tautology: 14086 (x ^ y) * (z * u) = z * (u * (y ^ x)). [para(19(a,1),696(a,1,2,2)),flip(a)]. % back CAC tautology: 14085 x * ((y ^ z) * u) = u * (x * (z ^ y)). [para(19(a,1),696(a,1,2,1))]. % back CAC tautology: 14084 (x ^ y) * (z * u) = u * ((y ^ x) * z). [para(19(a,1),696(a,1,1))]. % back CAC tautology: 14083 (x * (y * z)) ^ u = u ^ (z * (x * y)). [para(696(a,1),19(a,1,2)),flip(a)]. % back CAC tautology: 14082 (x * (y * z)) ^ u = u ^ (y * (z * x)). [para(696(a,1),19(a,1,1))]. % back CAC tautology: 14081 (x v y) * (z * u) = z * (u * (y v x)). [para(18(a,1),696(a,1,2,2)),flip(a)]. % back CAC tautology: 14080 x * ((y v z) * u) = u * (x * (z v y)). [para(18(a,1),696(a,1,2,1))]. % back CAC tautology: 14079 (x v y) * (z * u) = u * ((y v x) * z). [para(18(a,1),696(a,1,1))]. % back CAC tautology: 14078 (x * (y * z)) v u = u v (z * (x * y)). [para(696(a,1),18(a,1,2)),flip(a)]. % back CAC tautology: 14077 (x * (y * z)) v u = u v (y * (z * x)). [para(696(a,1),18(a,1,1))]. % back CAC tautology: 13708 x v (((y * z) * u) v w) = w v (x v (y * (z * u))). [para(26(a,1),170(a,2,2,2))]. % back CAC tautology: 13707 ((x * y) * z) v (u v w) = w v ((x * (y * z)) v u). [para(26(a,1),170(a,2,2,1))]. % back CAC tautology: 13706 (x * (y * z)) v (u v w) = u v (w v ((x * y) * z)). [para(26(a,1),170(a,2,1)),flip(a)]. % back CAC tautology: 13705 ((x * y) * z) v (u v w) = u v (w v (x * (y * z))). [para(26(a,1),170(a,1,2,2)),flip(a)]. % back CAC tautology: 13704 x v ((y * (z * u)) v w) = w v (x v ((y * z) * u)). [para(26(a,1),170(a,1,2,1))]. % back CAC tautology: 13703 (x * (y * z)) v (u v w) = w v (((x * y) * z) v u). [para(26(a,1),170(a,1,1))]. % back CAC tautology: 13702 (x * y) * (z v (u v w)) = x * (y * (w v (z v u))). [para(170(a,1),26(a,2,2,2))]. % back CAC tautology: 13701 (x * (y v (z v u))) * w = x * ((u v (y v z)) * w). [para(170(a,1),26(a,2,2,1))]. % back CAC tautology: 13700 ((x v (y v z)) * u) * w = (z v (x v y)) * (u * w). [para(170(a,1),26(a,2,1))]. % back CAC tautology: 13699 (x * y) * (z v (u v w)) = x * (y * (u v (w v z))). [para(170(a,1),26(a,1,2))]. % back CAC tautology: 13698 (x * (y v (z v u))) * w = x * ((z v (u v y)) * w). [para(170(a,1),26(a,1,1,2))]. % back CAC tautology: 13697 ((x v (y v z)) * u) * w = (y v (z v x)) * (u * w). [para(170(a,1),26(a,1,1,1))]. % back CAC tautology: 713 (x * y) * (z * u) = x * ((y * z) * u). [para(26(a,2),26(a,2,2))]. % back CAC tautology: 712 ((x * y) * z) * u = x * ((y * z) * u). [para(26(a,2),26(a,1,1))]. % back CAC tautology: 711 ((x * y) * z) * u = x * (y * (z * u)). [para(26(a,1),26(a,2))]. % back CAC tautology: 710 (x * (y * z)) * u = x * (y * (z * u)). [para(26(a,1),26(a,2,2))]. % back CAC tautology: 709 (x * y) * ((z * u) * w) = x * (y * (z * (u * w))). [para(26(a,1),26(a,2,2,2))]. % back CAC tautology: 708 (x * ((y * z) * u)) * w = x * ((y * (z * u)) * w). [para(26(a,1),26(a,2,2,1))]. % back CAC tautology: 707 (((x * y) * z) * u) * w = (x * (y * z)) * (u * w). [para(26(a,1),26(a,2,1))]. % back CAC tautology: 706 (x * y) * (z * (u * w)) = x * (y * ((z * u) * w)). [para(26(a,1),26(a,1,2))]. % back CAC tautology: 705 (x * (y * z)) * u = (x * y) * (z * u). [para(26(a,1),26(a,1,1))]. % back CAC tautology: 704 (x * (y * (z * u))) * w = x * (((y * z) * u) * w). [para(26(a,1),26(a,1,1,2))]. % back CAC tautology: 703 ((x * (y * z)) * u) * w = ((x * y) * z) * (u * w). [para(26(a,1),26(a,1,1,1))]. % back CAC tautology: 702 (x * y) * z = x * (z * y). [para(25(a,1),26(a,2,2))]. % back CAC tautology: 701 (x * y) * (z * u) = x * (y * (u * z)). [para(25(a,1),26(a,1,2))]. % back CAC tautology: 700 (x * y) * z = y * (x * z). [para(25(a,1),26(a,1,1))]. % back CAC tautology: 699 (x * (y * z)) * u = x * ((z * y) * u). [para(25(a,1),26(a,1,1,2))]. % back CAC tautology: 698 ((x * y) * z) * u = (y * x) * (z * u). [para(25(a,1),26(a,1,1,1))]. % back CAC tautology: 697 (x * y) * z = (z * x) * y. [para(26(a,2),25(a,1)),flip(a)]. % back CAC tautology: 695 ((x * y) * z) * u = u * (x * (y * z)). [para(26(a,1),25(a,1,2)),flip(a)]. % back CAC tautology: 694 (x * (y * z)) * u = u * ((x * y) * z). [para(26(a,1),25(a,1,1))]. % back CAC tautology: 637 (x * y) * (z ^ u) = x * (y * (u ^ z)). [para(19(a,1),26(a,1,2))]. % back CAC tautology: 636 (x * (y ^ z)) * u = x * ((z ^ y) * u). [para(19(a,1),26(a,1,1,2))]. % back CAC tautology: 635 ((x ^ y) * z) * u = (y ^ x) * (z * u). [para(19(a,1),26(a,1,1,1))]. % back CAC tautology: 634 ((x * y) * z) ^ u = u ^ (x * (y * z)). [para(26(a,1),19(a,1,2)),flip(a)]. % back CAC tautology: 633 (x * (y * z)) ^ u = u ^ ((x * y) * z). [para(26(a,1),19(a,1,1))]. % back CAC tautology: 632 (x * y) * (z v u) = x * (y * (u v z)). [para(18(a,1),26(a,1,2))]. % back CAC tautology: 631 (x * (y v z)) * u = x * ((z v y) * u). [para(18(a,1),26(a,1,1,2))]. % back CAC tautology: 630 ((x v y) * z) * u = (y v x) * (z * u). [para(18(a,1),26(a,1,1,1))]. % back CAC tautology: 629 ((x * y) * z) v u = u v (x * (y * z)). [para(26(a,1),18(a,1,2)),flip(a)]. % back CAC tautology: 628 (x * (y * z)) v u = u v ((x * y) * z). [para(26(a,1),18(a,1,1))]. % back CAC tautology: 587 (x * y) * ((z v u) v w) = x * (y * (z v (u v w))). [para(14(a,1),26(a,2,2,2))]. % back CAC tautology: 586 (x * ((y v z) v u)) * w = x * ((y v (z v u)) * w). [para(14(a,1),26(a,2,2,1))]. % back CAC tautology: 585 (((x v y) v z) * u) * w = (x v (y v z)) * (u * w). [para(14(a,1),26(a,2,1))]. % back CAC tautology: 584 (x * y) * (z v (u v w)) = x * (y * ((z v u) v w)). [para(14(a,1),26(a,1,2))]. % back CAC tautology: 583 (x * (y v (z v u))) * w = x * (((y v z) v u) * w). [para(14(a,1),26(a,1,1,2))]. % back CAC tautology: 582 ((x v (y v z)) * u) * w = ((x v y) v z) * (u * w). [para(14(a,1),26(a,1,1,1))]. % back CAC tautology: 581 (x v y) v ((z * u) * w) = x v (y v (z * (u * w))). [para(26(a,1),14(a,2,2,2))]. % back CAC tautology: 580 (x v ((y * z) * u)) v w = x v ((y * (z * u)) v w). [para(26(a,1),14(a,2,2,1))]. % back CAC tautology: 579 (((x * y) * z) v u) v w = (x * (y * z)) v (u v w). [para(26(a,1),14(a,2,1))]. % back CAC tautology: 578 (x v y) v (z * (u * w)) = x v (y v ((z * u) * w)). [para(26(a,1),14(a,1,2))]. % back CAC tautology: 577 (x v (y * (z * u))) v w = x v (((y * z) * u) v w). [para(26(a,1),14(a,1,1,2))]. % back CAC tautology: 576 ((x * (y * z)) v u) v w = ((x * y) * z) v (u v w). [para(26(a,1),14(a,1,1,1))]. given #53 (H,wt=11): 873 x v (x * y) = x * (1 v y). [para(24(a,1),28(a,1,1))]. given #54 (H,wt=9): 14622 x v (x * y) = x * 1. [para(3825(a,1),873(a,2,2))]. given #55 (H,wt=7): 14927 x v (x * y) = x. [para(14622(a,2),24(a,1))]. given #56 (H,wt=11): 6457 x => (x ^ y) = 1 ^ (x => y). [para(6180(a,1),30(a,1,1)),flip(a)]. Low Water (keep): wt=17.000, iters=6701 given #57 (H,wt=9): 15852 x => (x ^ y) = x => y. [para(6457(a,2),446(a,1))]. -------- Proof 3 -------- "(A6)[= 1]". ============================== PROOF ================================= % Proof 3 at 0.64 (+ 0.02) seconds: "(A6)[= 1]". % Length of proof is 17. % Level of proof is 6. % Maximum clause weight is 13. % Given clauses 57. 6 x => (x v y) = 1 # label("(A6)[= 1]") # label(non_clause) # label(goal). [goal]. 19 x ^ y = y ^ x # label("(D6)"). [assumption]. 21 x ^ (x v y) = x # label("(D8)"). [assumption]. 23 x ^ 1 = x # label("(D10)"). [assumption]. 24 x * 1 = x # label("(M1)"). [assumption]. 29 x => (y ^ z) = (x => y) ^ (x => z) # label("(R2)"). [assumption]. 30 (x => y) ^ (x => z) = x => (y ^ z). [copy(29),flip(a)]. 32 (x => (x * y)) ^ y = y # label("(R4)"). [assumption]. 45 c13 => (c13 v c14) != 1 # label("(A6)[= 1]") # answer("(A6)[= 1]"). [deny(6)]. 446 1 ^ x = x. [para(23(a,1),19(a,1)),flip(a)]. 1488 x => (x * 1) = 1. [para(32(a,1),23(a,1)),flip(a)]. 6180 x => x = 1. [para(24(a,1),1488(a,1,2))]. 6421 x => (x ^ (x v y)) = 1. [para(21(a,1),6180(a,1,1))]. 6457 x => (x ^ y) = 1 ^ (x => y). [para(6180(a,1),30(a,1,1)),flip(a)]. 15852 x => (x ^ y) = x => y. [para(6457(a,2),446(a,1))]. 16378 x => (x v y) = 1. [para(15852(a,1),6421(a,1))]. 16379 $F # answer("(A6)[= 1]"). [resolve(16378,a,45,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 45 given #58 (H,wt=7): 16378 x => (x v y) = 1. [para(15852(a,1),6421(a,1))]. -------- Proof 4 -------- "(A7)[= 1]". ============================== PROOF ================================= % Proof 4 at 0.67 (+ 0.02) seconds: "(A7)[= 1]". % Length of proof is 19. % Level of proof is 7. % Maximum clause weight is 13. % Given clauses 58. 7 y => (x v y) = 1 # label("(A7)[= 1]") # label(non_clause) # label(goal). [goal]. 18 x v y = y v x # label("(D5)"). [assumption]. 19 x ^ y = y ^ x # label("(D6)"). [assumption]. 21 x ^ (x v y) = x # label("(D8)"). [assumption]. 23 x ^ 1 = x # label("(D10)"). [assumption]. 24 x * 1 = x # label("(M1)"). [assumption]. 29 x => (y ^ z) = (x => y) ^ (x => z) # label("(R2)"). [assumption]. 30 (x => y) ^ (x => z) = x => (y ^ z). [copy(29),flip(a)]. 32 (x => (x * y)) ^ y = y # label("(R4)"). [assumption]. 46 c15 => (c16 v c15) != 1 # label("(A7)[= 1]") # answer("(A7)[= 1]"). [deny(7)]. 446 1 ^ x = x. [para(23(a,1),19(a,1)),flip(a)]. 1488 x => (x * 1) = 1. [para(32(a,1),23(a,1)),flip(a)]. 6180 x => x = 1. [para(24(a,1),1488(a,1,2))]. 6421 x => (x ^ (x v y)) = 1. [para(21(a,1),6180(a,1,1))]. 6457 x => (x ^ y) = 1 ^ (x => y). [para(6180(a,1),30(a,1,1)),flip(a)]. 15852 x => (x ^ y) = x => y. [para(6457(a,2),446(a,1))]. 16378 x => (x v y) = 1. [para(15852(a,1),6421(a,1))]. 16451 x => (y v x) = 1. [para(18(a,1),16378(a,1,2))]. 16452 $F # answer("(A7)[= 1]"). [resolve(16451,a,46,a)]. ============================== end of proof ========================== -------- Proof 5 -------- "(A3)[= 1]". ============================== PROOF ================================= % Proof 5 at 0.67 (+ 0.02) seconds: "(A3)[= 1]". % Length of proof is 21. % Level of proof is 7. % Maximum clause weight is 13. % Given clauses 58. 3 (x ^ y) => x = 1 # label("(A3)[= 1]") # label(non_clause) # label(goal). [goal]. 18 x v y = y v x # label("(D5)"). [assumption]. 19 x ^ y = y ^ x # label("(D6)"). [assumption]. 20 x v (x ^ y) = x # label("(D7)"). [assumption]. 21 x ^ (x v y) = x # label("(D8)"). [assumption]. 23 x ^ 1 = x # label("(D10)"). [assumption]. 24 x * 1 = x # label("(M1)"). [assumption]. 29 x => (y ^ z) = (x => y) ^ (x => z) # label("(R2)"). [assumption]. 30 (x => y) ^ (x => z) = x => (y ^ z). [copy(29),flip(a)]. 32 (x => (x * y)) ^ y = y # label("(R4)"). [assumption]. 42 (c6 ^ c7) => c6 != 1 # label("(A3)[= 1]") # answer("(A3)[= 1]"). [deny(3)]. 268 (x ^ y) v x = x. [para(20(a,1),18(a,1)),flip(a)]. 446 1 ^ x = x. [para(23(a,1),19(a,1)),flip(a)]. 1488 x => (x * 1) = 1. [para(32(a,1),23(a,1)),flip(a)]. 6180 x => x = 1. [para(24(a,1),1488(a,1,2))]. 6421 x => (x ^ (x v y)) = 1. [para(21(a,1),6180(a,1,1))]. 6457 x => (x ^ y) = 1 ^ (x => y). [para(6180(a,1),30(a,1,1)),flip(a)]. 15852 x => (x ^ y) = x => y. [para(6457(a,2),446(a,1))]. 16378 x => (x v y) = 1. [para(15852(a,1),6421(a,1))]. 16552 (x ^ y) => x = 1. [para(268(a,1),16378(a,1,2))]. 16553 $F # answer("(A3)[= 1]"). [resolve(16552,a,42,a)]. ============================== end of proof ========================== -------- Proof 6 -------- "(A4)[= 1]". ============================== PROOF ================================= % Proof 6 at 0.67 (+ 0.02) seconds: "(A4)[= 1]". % Length of proof is 22. % Level of proof is 7. % Maximum clause weight is 13. % Given clauses 58. 4 (x ^ y) => y = 1 # label("(A4)[= 1]") # label(non_clause) # label(goal). [goal]. 18 x v y = y v x # label("(D5)"). [assumption]. 19 x ^ y = y ^ x # label("(D6)"). [assumption]. 20 x v (x ^ y) = x # label("(D7)"). [assumption]. 21 x ^ (x v y) = x # label("(D8)"). [assumption]. 23 x ^ 1 = x # label("(D10)"). [assumption]. 24 x * 1 = x # label("(M1)"). [assumption]. 29 x => (y ^ z) = (x => y) ^ (x => z) # label("(R2)"). [assumption]. 30 (x => y) ^ (x => z) = x => (y ^ z). [copy(29),flip(a)]. 32 (x => (x * y)) ^ y = y # label("(R4)"). [assumption]. 43 (c8 ^ c9) => c9 != 1 # label("(A4)[= 1]") # answer("(A4)[= 1]"). [deny(4)]. 268 (x ^ y) v x = x. [para(20(a,1),18(a,1)),flip(a)]. 446 1 ^ x = x. [para(23(a,1),19(a,1)),flip(a)]. 1488 x => (x * 1) = 1. [para(32(a,1),23(a,1)),flip(a)]. 4701 (x ^ y) v y = y. [para(19(a,1),268(a,1,1))]. 6180 x => x = 1. [para(24(a,1),1488(a,1,2))]. 6421 x => (x ^ (x v y)) = 1. [para(21(a,1),6180(a,1,1))]. 6457 x => (x ^ y) = 1 ^ (x => y). [para(6180(a,1),30(a,1,1)),flip(a)]. 15852 x => (x ^ y) = x => y. [para(6457(a,2),446(a,1))]. 16378 x => (x v y) = 1. [para(15852(a,1),6421(a,1))]. 16611 (x ^ y) => y = 1. [para(4701(a,1),16378(a,1,2))]. 16612 $F # answer("(A4)[= 1]"). [resolve(16611,a,43,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 43 42 46 given #59 (H,wt=7): 16451 x => (y v x) = 1. [para(18(a,1),16378(a,1,2))]. given #60 (H,wt=7): 16552 (x ^ y) => x = 1. [para(268(a,1),16378(a,1,2))]. given #61 (H,wt=7): 16611 (x ^ y) => y = 1. [para(4701(a,1),16378(a,1,2))]. given #62 (H,wt=9): 17083 x => (y => (y * x)) = 1. [para(32(a,1),16552(a,1,1))]. given #63 (H,wt=9): 17216 x => (y => (x * y)) = 1. [para(1517(a,1),16552(a,1,1))]. Low Water (keep): wt=16.000, iters=6770 given #64 (H,wt=11): 13223 ~ x * (y v x) = y * ~ x. [para(36(a,1),12525(a,1,2,2))]. Low Water (keep): wt=15.000, iters=6666 given #65 (H,wt=11): 13653 x v ((x ^ y) v z) = z v x. [para(20(a,1),170(a,2,2))]. given #66 (H,wt=11): 13825 x v (y v (x ^ z)) = y v x. [para(268(a,1),170(a,1,2)),flip(a)]. given #67 (H,wt=11): 14135 x * (y * z) = y * (x * z). [para(25(a,1),696(a,1,2))]. given #68 (H,wt=11): 17356 (x => (y ^ z)) => (x => z) = 1. [para(30(a,1),16611(a,1,1))]. given #69 (H,wt=11): 17370 (x v (y ^ z)) => (x v z) = 1. [para(34(a,1),16611(a,1,1))]. -------- Proof 7 -------- "(A9)[= 1]". ============================== PROOF ================================= % Proof 7 at 0.82 (+ 0.03) seconds: "(A9)[= 1]". % Length of proof is 26. % Level of proof is 9. % Maximum clause weight is 13. % Given clauses 69. 9 (x ^ (y v z)) => ((x ^ y) v z) = 1 # label("(A9)[= 1]") # label(non_clause) # label(goal). [goal]. 18 x v y = y v x # label("(D5)"). [assumption]. 19 x ^ y = y ^ x # label("(D6)"). [assumption]. 20 x v (x ^ y) = x # label("(D7)"). [assumption]. 21 x ^ (x v y) = x # label("(D8)"). [assumption]. 23 x ^ 1 = x # label("(D10)"). [assumption]. 24 x * 1 = x # label("(M1)"). [assumption]. 29 x => (y ^ z) = (x => y) ^ (x => z) # label("(R2)"). [assumption]. 30 (x => y) ^ (x => z) = x => (y ^ z). [copy(29),flip(a)]. 32 (x => (x * y)) ^ y = y # label("(R4)"). [assumption]. 34 (x v y) ^ (x v z) = x v (y ^ z) # label("(D11)"). [assumption]. 35 (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D12)"). [assumption]. 48 (c20 ^ (c21 v c22)) => ((c20 ^ c21) v c22) != 1 # label("(A9)[= 1]") # answer("(A9)[= 1]"). [deny(9)]. 268 (x ^ y) v x = x. [para(20(a,1),18(a,1)),flip(a)]. 446 1 ^ x = x. [para(23(a,1),19(a,1)),flip(a)]. 1488 x => (x * 1) = 1. [para(32(a,1),23(a,1)),flip(a)]. 4701 (x ^ y) v y = y. [para(19(a,1),268(a,1,1))]. 6180 x => x = 1. [para(24(a,1),1488(a,1,2))]. 6421 x => (x ^ (x v y)) = 1. [para(21(a,1),6180(a,1,1))]. 6457 x => (x ^ y) = 1 ^ (x => y). [para(6180(a,1),30(a,1,1)),flip(a)]. 15852 x => (x ^ y) = x => y. [para(6457(a,2),446(a,1))]. 16378 x => (x v y) = 1. [para(15852(a,1),6421(a,1))]. 16611 (x ^ y) => y = 1. [para(4701(a,1),16378(a,1,2))]. 17370 (x v (y ^ z)) => (x v z) = 1. [para(34(a,1),16611(a,1,1))]. 18917 (x ^ (y v z)) => ((x ^ y) v z) = 1. [para(35(a,1),17370(a,1,1))]. 18918 $F # answer("(A9)[= 1]"). [resolve(18917,a,48,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 48 given #70 (H,wt=11): 18268 ~ x * (x v y) = y * ~ x. [para(18(a,1),13223(a,1,2))]. given #71 (H,wt=11): 18355 (x ^ y) * ~ x = ~ x * x. [para(268(a,1),13223(a,1,2)),flip(a)]. given #72 (H,wt=8): 19297 (x ^ y) * ~ x = 0. [para(18355(a,2),7185(a,1))]. given #73 (H,wt=8): 19364 ~ x * (x ^ y) = 0. [para(19297(a,1),25(a,1)),flip(a)]. given #74 (H,wt=8): 19441 x * ~ (x v y) = 0. [para(344(a,1),19297(a,1,1))]. given #75 (H,wt=8): 19724 ~ (x v y) * y = 0. [para(5418(a,1),19364(a,1,2))]. given #76 (H,wt=10): 19866 (x * (x => y)) * ~ y = 0. [para(31(a,1),19441(a,1,2,1))]. given #77 (H,wt=10): 20215 ~ x * (y * (y => x)) = 0. [para(1224(a,1),19724(a,1,1,1))]. given #78 (H,wt=10): 20371 x * ((x => y) * ~ y) = 0. [para(19866(a,1),26(a,1)),flip(a)]. given #79 (H,wt=10): 20623 x * (y * (y => ~ x)) = 0. [para(36(a,1),20215(a,1,1))]. Low Water (displace): id=3228, wt=67.000 Low Water (displace): id=3348, wt=59.000 Low Water (displace): id=3294, wt=41.000 Low Water (displace): id=21107, wt=14.000 Low Water (displace): id=21124, wt=13.000 given #80 (H,wt=10): 21289 x * (y * (x => ~ y)) = 0. [para(20623(a,1),14135(a,1)),flip(a)]. Low Water (keep): wt=14.000, iters=6680 given #81 (H,wt=10): 21329 (x * y) * (x => ~ y) = 0. [para(21289(a,1),26(a,2))]. Low Water (displace): id=21551, wt=12.000 given #82 (H,wt=11): 18554 x v (y v (x ^ z)) = x v y. [para(13825(a,2),18(a,1))]. given #83 (H,wt=11): 18769 (x => y) => (x => (y v z)) = 1. [para(21(a,1),17356(a,1,1,2))]. given #84 (H,wt=11): 19502 ~ x ^ ((x ^ y) => 0) = ~ x. [para(19297(a,1),1448(a,1,2,2))]. given #85 (H,wt=10): 21817 ~ x ^ ~ (x ^ y) = ~ x. [para(39(a,1),19502(a,1,2))]. Low Water (displace): id=21939, wt=11.000 given #86 (H,wt=12): 21556 (x * y) => ((x => ~ y) => 0) = 1. [para(21329(a,1),17216(a,1,2,2))]. given #87 (H,wt=11): 21986 (x * y) => ~ (x => ~ y) = 1. [para(39(a,1),21556(a,1,2))]. given #88 (H,wt=11): 22050 (x * ~ y) => ~ (x => y) = 1. [para(36(a,1),21986(a,1,2,1,2))]. given #89 (H,wt=12): 21974 ~ (x v y) ^ ~ y = ~ (x v y). [para(5418(a,1),21817(a,1,2,1))]. given #90 (H,wt=13): 18404 (x v y) => (~ y => (x * ~ y)) = 1. [para(13223(a,1),17083(a,1,2,2))]. given #91 (H,wt=13): 18917 (x ^ (y v z)) => ((x ^ y) v z) = 1. [para(35(a,1),17370(a,1,1))]. given #92 (H,wt=13): 22259 (x => ~ (y v z)) => (x => ~ z) = 1. [para(21974(a,1),17356(a,1,1,2))]. given #93 (H,wt=15): 6469 ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1. [para(30(a,1),6180(a,1,2))]. given #94 (H,wt=20): 3322 (x => (x => ~ y)) ^ (y => (~ ~ y => ~ x)) = x => ~ y. [para(36(a,1),37(a,1,2,1))]. given #95 (H,wt=18): 22300 (x => (x => ~ y)) ^ (y => (y => ~ x)) = x => ~ y. [para(36(a,1),3322(a,1,2,2,1))]. given #96 (H,wt=18): 22302 (x => (x => ~ y)) ^ (y => (y => ~ x)) = y => ~ x. [para(22300(a,1),19(a,1)),flip(a)]. given #97 (H,wt=9): 22305 x => ~ y = y => ~ x. [para(22302(a,1),22300(a,1))]. -------- Proof 8 -------- "(A11)[= 1]". ============================== PROOF ================================= % Proof 8 at 1.16 (+ 0.04) seconds: "(A11)[= 1]". % Length of proof is 16. % Level of proof is 6. % Maximum clause weight is 20. % Given clauses 97. 11 (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]") # label(non_clause) # label(goal). [goal]. 19 x ^ y = y ^ x # label("(D6)"). [assumption]. 23 x ^ 1 = x # label("(D10)"). [assumption]. 24 x * 1 = x # label("(M1)"). [assumption]. 32 (x => (x * y)) ^ y = y # label("(R4)"). [assumption]. 36 ~ ~ x = x # label("(I)"). [assumption]. 37 (x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y # label("(N)"). [assumption]. 50 (c24 => ~ c25) => (c25 => ~ c24) != 1 # label("(A11)[= 1]") # answer("(A11)[= 1]"). [deny(11)]. 1488 x => (x * 1) = 1. [para(32(a,1),23(a,1)),flip(a)]. 3322 (x => (x => ~ y)) ^ (y => (~ ~ y => ~ x)) = x => ~ y. [para(36(a,1),37(a,1,2,1))]. 6180 x => x = 1. [para(24(a,1),1488(a,1,2))]. 22300 (x => (x => ~ y)) ^ (y => (y => ~ x)) = x => ~ y. [para(36(a,1),3322(a,1,2,2,1))]. 22302 (x => (x => ~ y)) ^ (y => (y => ~ x)) = y => ~ x. [para(22300(a,1),19(a,1)),flip(a)]. 22305 x => ~ y = y => ~ x. [para(22302(a,1),22300(a,1))]. 22370 (x => ~ y) => (y => ~ x) = 1. [para(22305(a,1),6180(a,1,1))]. 22371 $F # answer("(A11)[= 1]"). [resolve(22370,a,50,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 50 given #98 (H,wt=9): 22336 ~ x => ~ y = y => x. [para(36(a,1),22305(a,1,2)),flip(a)]. given #99 (H,wt=9): 22491 ~ x => y = ~ y => x. [para(36(a,1),22336(a,1,2))]. given #100 (H,wt=6): 22730 ~ 0 => x = x. [para(22491(a,1),3534(a,1))]. given #101 (H,wt=5): 22964 1 => x = x. [para(6556(a,1),22730(a,1,1))]. Low Water (displace): id=23692, wt=10.000 given #102 (H,wt=11): 22370 (x => ~ y) => (y => ~ x) = 1. [para(22305(a,1),6180(a,1,1))]. given #103 (H,wt=11): 22424 (x => y) => ~ (x * ~ y) = 1. [para(22305(a,1),22050(a,1))]. Low Water (keep): wt=13.000, iters=6716 given #104 (H,wt=11): 22766 x v (~ y * (~ x => y)) = x. [para(22491(a,1),1224(a,1,2,2))]. given #105 (H,wt=13): 22675 ((x v y) => z) => (~ z => ~ y) = 1. [para(22336(a,1),22259(a,1,1))]. given #106 (H,wt=11): 24023 ((x v y) => z) => (y => z) = 1. [para(22336(a,1),22675(a,1,2))]. given #107 (H,wt=11): 24025 ((x v y) => z) => (x => z) = 1. [para(18(a,1),24023(a,1,1,1))]. given #108 (H,wt=11): 24026 (x => y) => ((x ^ z) => y) = 1. [para(20(a,1),24023(a,1,1,1))]. given #109 (H,wt=13): 24077 ((x => (y * x)) => z) => (y => z) = 1. [para(1517(a,1),24026(a,1,2,1))]. given #110 (H,wt=13): 24089 1 => (x => (y => ((x * y) v z))) = 1. [para(18769(a,1),24077(a,1,1))]. given #111 (H,wt=13): 24093 1 => (x => ~ (y * ~ (x * y))) = 1. [para(22424(a,1),24077(a,1,1))]. given #112 (H,wt=11): 24109 x => ~ (y * ~ (x * y)) = 1. [para(24093(a,1),22964(a,1)),flip(a)]. given #113 (H,wt=13): 24094 1 => (x => (y => (z v (x * y)))) = 1. [para(18(a,1),24089(a,1,2,2,2))]. given #114 (H,wt=11): 24146 x => (y => (z v (x * y))) = 1. [para(24094(a,1),22964(a,1)),flip(a)]. -------- Proof 9 -------- "(A1)[= 1]". ============================== PROOF ================================= % Proof 9 at 1.42 (+ 0.04) seconds: "(A1)[= 1]". % Length of proof is 70. % Level of proof is 22. % Maximum clause weight is 20. % Given clauses 114. 1 x => ((x => y) => y) = 1 # label("(A1)[= 1]") # label(non_clause) # label(goal). [goal]. 18 x v y = y v x # label("(D5)"). [assumption]. 19 x ^ y = y ^ x # label("(D6)"). [assumption]. 20 x v (x ^ y) = x # label("(D7)"). [assumption]. 21 x ^ (x v y) = x # label("(D8)"). [assumption]. 22 x ^ 0 = 0 # label("(D9)"). [assumption]. 23 x ^ 1 = x # label("(D10)"). [assumption]. 24 x * 1 = x # label("(M1)"). [assumption]. 25 x * y = y * x # label("(M2)"). [assumption]. 27 x * (y v z) = (x * y) v (x * z) # label("(R1)"). [assumption]. 28 (x * y) v (x * z) = x * (y v z). [copy(27),flip(a)]. 29 x => (y ^ z) = (x => y) ^ (x => z) # label("(R2)"). [assumption]. 30 (x => y) ^ (x => z) = x => (y ^ z). [copy(29),flip(a)]. 31 (x * (x => y)) v y = y # label("(R3)"). [assumption]. 32 (x => (x * y)) ^ y = y # label("(R4)"). [assumption]. 36 ~ ~ x = x # label("(I)"). [assumption]. 37 (x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y # label("(N)"). [assumption]. 38 ~ x = x => 0 # label("(~ def)"). [assumption]. 39 x => 0 = ~ x. [copy(38),flip(a)]. 40 c1 => ((c1 => c2) => c2) != 1 # label("(A1)[= 1]") # answer("(A1)[= 1]"). [deny(1)]. 268 (x ^ y) v x = x. [para(20(a,1),18(a,1)),flip(a)]. 341 x ^ (y v x) = x. [para(18(a,1),21(a,1,2))]. 394 x v 0 = x. [para(22(a,1),20(a,1,2))]. 446 1 ^ x = x. [para(23(a,1),19(a,1)),flip(a)]. 1224 x v (y * (y => x)) = x. [para(31(a,1),18(a,1)),flip(a)]. 1448 x ^ (y => (y * x)) = x. [para(32(a,1),19(a,1)),flip(a)]. 1488 x => (x * 1) = 1. [para(32(a,1),23(a,1)),flip(a)]. 1517 (x => (y * x)) ^ y = y. [para(25(a,1),32(a,1,1,2))]. 3322 (x => (x => ~ y)) ^ (y => (~ ~ y => ~ x)) = x => ~ y. [para(36(a,1),37(a,1,2,1))]. 3534 ~ x => 0 = x. [para(39(a,2),36(a,1))]. 3677 x * (x => 0) = 0. [para(394(a,1),31(a,1))]. 4701 (x ^ y) v y = y. [para(19(a,1),268(a,1,1))]. 5418 (x v y) ^ y = y. [para(341(a,1),19(a,1)),flip(a)]. 6180 x => x = 1. [para(24(a,1),1488(a,1,2))]. 6421 x => (x ^ (x v y)) = 1. [para(21(a,1),6180(a,1,1))]. 6457 x => (x ^ y) = 1 ^ (x => y). [para(6180(a,1),30(a,1,1)),flip(a)]. 6556 ~ 0 = 1. [para(6180(a,1),39(a,1)),flip(a)]. 7163 x * ~ x = 0. [para(39(a,1),3677(a,1,2))]. 7185 ~ x * x = 0. [para(3534(a,1),3677(a,1,2))]. 7423 x v (y * ~ y) = x. [para(7163(a,2),394(a,1,2))]. 9081 x * (y v ~ x) = x * y. [para(7423(a,1),28(a,1)),flip(a)]. 12525 x * (y v ~ x) = y * x. [para(9081(a,2),25(a,1))]. 13223 ~ x * (y v x) = y * ~ x. [para(36(a,1),12525(a,1,2,2))]. 15852 x => (x ^ y) = x => y. [para(6457(a,2),446(a,1))]. 16378 x => (x v y) = 1. [para(15852(a,1),6421(a,1))]. 16611 (x ^ y) => y = 1. [para(4701(a,1),16378(a,1,2))]. 17356 (x => (y ^ z)) => (x => z) = 1. [para(30(a,1),16611(a,1,1))]. 18355 (x ^ y) * ~ x = ~ x * x. [para(268(a,1),13223(a,1,2)),flip(a)]. 18769 (x => y) => (x => (y v z)) = 1. [para(21(a,1),17356(a,1,1,2))]. 19297 (x ^ y) * ~ x = 0. [para(18355(a,2),7185(a,1))]. 19502 ~ x ^ ((x ^ y) => 0) = ~ x. [para(19297(a,1),1448(a,1,2,2))]. 21817 ~ x ^ ~ (x ^ y) = ~ x. [para(39(a,1),19502(a,1,2))]. 21974 ~ (x v y) ^ ~ y = ~ (x v y). [para(5418(a,1),21817(a,1,2,1))]. 22259 (x => ~ (y v z)) => (x => ~ z) = 1. [para(21974(a,1),17356(a,1,1,2))]. 22300 (x => (x => ~ y)) ^ (y => (y => ~ x)) = x => ~ y. [para(36(a,1),3322(a,1,2,2,1))]. 22302 (x => (x => ~ y)) ^ (y => (y => ~ x)) = y => ~ x. [para(22300(a,1),19(a,1)),flip(a)]. 22305 x => ~ y = y => ~ x. [para(22302(a,1),22300(a,1))]. 22336 ~ x => ~ y = y => x. [para(36(a,1),22305(a,1,2)),flip(a)]. 22491 ~ x => y = ~ y => x. [para(36(a,1),22336(a,1,2))]. 22675 ((x v y) => z) => (~ z => ~ y) = 1. [para(22336(a,1),22259(a,1,1))]. 22730 ~ 0 => x = x. [para(22491(a,1),3534(a,1))]. 22964 1 => x = x. [para(6556(a,1),22730(a,1,1))]. 24023 ((x v y) => z) => (y => z) = 1. [para(22336(a,1),22675(a,1,2))]. 24026 (x => y) => ((x ^ z) => y) = 1. [para(20(a,1),24023(a,1,1,1))]. 24077 ((x => (y * x)) => z) => (y => z) = 1. [para(1517(a,1),24026(a,1,2,1))]. 24089 1 => (x => (y => ((x * y) v z))) = 1. [para(18769(a,1),24077(a,1,1))]. 24094 1 => (x => (y => (z v (x * y)))) = 1. [para(18(a,1),24089(a,1,2,2,2))]. 24146 x => (y => (z v (x * y))) = 1. [para(24094(a,1),22964(a,1)),flip(a)]. 24163 x => ((x => y) => y) = 1. [para(1224(a,1),24146(a,1,2,2))]. 24164 $F # answer("(A1)[= 1]"). [resolve(24163,a,40,a)]. ============================== end of proof ========================== -------- Proof 10 -------- "(A12)[= 1]". ============================== PROOF ================================= % Proof 10 at 1.43 (+ 0.04) seconds: "(A12)[= 1]". % Length of proof is 73. % Level of proof is 22. % Maximum clause weight is 20. % Given clauses 114. 12 x => (y => x) = 1 # label("(A12)[= 1]") # label(non_clause) # label(goal). [goal]. 18 x v y = y v x # label("(D5)"). [assumption]. 19 x ^ y = y ^ x # label("(D6)"). [assumption]. 20 x v (x ^ y) = x # label("(D7)"). [assumption]. 21 x ^ (x v y) = x # label("(D8)"). [assumption]. 22 x ^ 0 = 0 # label("(D9)"). [assumption]. 23 x ^ 1 = x # label("(D10)"). [assumption]. 24 x * 1 = x # label("(M1)"). [assumption]. 25 x * y = y * x # label("(M2)"). [assumption]. 27 x * (y v z) = (x * y) v (x * z) # label("(R1)"). [assumption]. 28 (x * y) v (x * z) = x * (y v z). [copy(27),flip(a)]. 29 x => (y ^ z) = (x => y) ^ (x => z) # label("(R2)"). [assumption]. 30 (x => y) ^ (x => z) = x => (y ^ z). [copy(29),flip(a)]. 31 (x * (x => y)) v y = y # label("(R3)"). [assumption]. 32 (x => (x * y)) ^ y = y # label("(R4)"). [assumption]. 36 ~ ~ x = x # label("(I)"). [assumption]. 37 (x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y # label("(N)"). [assumption]. 38 ~ x = x => 0 # label("(~ def)"). [assumption]. 39 x => 0 = ~ x. [copy(38),flip(a)]. 51 c26 => (c27 => c26) != 1 # label("(A12)[= 1]") # answer("(A12)[= 1]"). [deny(12)]. 268 (x ^ y) v x = x. [para(20(a,1),18(a,1)),flip(a)]. 341 x ^ (y v x) = x. [para(18(a,1),21(a,1,2))]. 394 x v 0 = x. [para(22(a,1),20(a,1,2))]. 446 1 ^ x = x. [para(23(a,1),19(a,1)),flip(a)]. 873 x v (x * y) = x * (1 v y). [para(24(a,1),28(a,1,1))]. 1448 x ^ (y => (y * x)) = x. [para(32(a,1),19(a,1)),flip(a)]. 1488 x => (x * 1) = 1. [para(32(a,1),23(a,1)),flip(a)]. 1517 (x => (y * x)) ^ y = y. [para(25(a,1),32(a,1,1,2))]. 3322 (x => (x => ~ y)) ^ (y => (~ ~ y => ~ x)) = x => ~ y. [para(36(a,1),37(a,1,2,1))]. 3534 ~ x => 0 = x. [para(39(a,2),36(a,1))]. 3677 x * (x => 0) = 0. [para(394(a,1),31(a,1))]. 3825 1 v x = 1. [para(446(a,1),20(a,1,2))]. 4701 (x ^ y) v y = y. [para(19(a,1),268(a,1,1))]. 5418 (x v y) ^ y = y. [para(341(a,1),19(a,1)),flip(a)]. 6180 x => x = 1. [para(24(a,1),1488(a,1,2))]. 6421 x => (x ^ (x v y)) = 1. [para(21(a,1),6180(a,1,1))]. 6457 x => (x ^ y) = 1 ^ (x => y). [para(6180(a,1),30(a,1,1)),flip(a)]. 6556 ~ 0 = 1. [para(6180(a,1),39(a,1)),flip(a)]. 7163 x * ~ x = 0. [para(39(a,1),3677(a,1,2))]. 7185 ~ x * x = 0. [para(3534(a,1),3677(a,1,2))]. 7423 x v (y * ~ y) = x. [para(7163(a,2),394(a,1,2))]. 9081 x * (y v ~ x) = x * y. [para(7423(a,1),28(a,1)),flip(a)]. 12525 x * (y v ~ x) = y * x. [para(9081(a,2),25(a,1))]. 13223 ~ x * (y v x) = y * ~ x. [para(36(a,1),12525(a,1,2,2))]. 14622 x v (x * y) = x * 1. [para(3825(a,1),873(a,2,2))]. 14927 x v (x * y) = x. [para(14622(a,2),24(a,1))]. 15852 x => (x ^ y) = x => y. [para(6457(a,2),446(a,1))]. 16378 x => (x v y) = 1. [para(15852(a,1),6421(a,1))]. 16611 (x ^ y) => y = 1. [para(4701(a,1),16378(a,1,2))]. 17356 (x => (y ^ z)) => (x => z) = 1. [para(30(a,1),16611(a,1,1))]. 18355 (x ^ y) * ~ x = ~ x * x. [para(268(a,1),13223(a,1,2)),flip(a)]. 18769 (x => y) => (x => (y v z)) = 1. [para(21(a,1),17356(a,1,1,2))]. 19297 (x ^ y) * ~ x = 0. [para(18355(a,2),7185(a,1))]. 19502 ~ x ^ ((x ^ y) => 0) = ~ x. [para(19297(a,1),1448(a,1,2,2))]. 21817 ~ x ^ ~ (x ^ y) = ~ x. [para(39(a,1),19502(a,1,2))]. 21974 ~ (x v y) ^ ~ y = ~ (x v y). [para(5418(a,1),21817(a,1,2,1))]. 22259 (x => ~ (y v z)) => (x => ~ z) = 1. [para(21974(a,1),17356(a,1,1,2))]. 22300 (x => (x => ~ y)) ^ (y => (y => ~ x)) = x => ~ y. [para(36(a,1),3322(a,1,2,2,1))]. 22302 (x => (x => ~ y)) ^ (y => (y => ~ x)) = y => ~ x. [para(22300(a,1),19(a,1)),flip(a)]. 22305 x => ~ y = y => ~ x. [para(22302(a,1),22300(a,1))]. 22336 ~ x => ~ y = y => x. [para(36(a,1),22305(a,1,2)),flip(a)]. 22491 ~ x => y = ~ y => x. [para(36(a,1),22336(a,1,2))]. 22675 ((x v y) => z) => (~ z => ~ y) = 1. [para(22336(a,1),22259(a,1,1))]. 22730 ~ 0 => x = x. [para(22491(a,1),3534(a,1))]. 22964 1 => x = x. [para(6556(a,1),22730(a,1,1))]. 24023 ((x v y) => z) => (y => z) = 1. [para(22336(a,1),22675(a,1,2))]. 24026 (x => y) => ((x ^ z) => y) = 1. [para(20(a,1),24023(a,1,1,1))]. 24077 ((x => (y * x)) => z) => (y => z) = 1. [para(1517(a,1),24026(a,1,2,1))]. 24089 1 => (x => (y => ((x * y) v z))) = 1. [para(18769(a,1),24077(a,1,1))]. 24094 1 => (x => (y => (z v (x * y)))) = 1. [para(18(a,1),24089(a,1,2,2,2))]. 24146 x => (y => (z v (x * y))) = 1. [para(24094(a,1),22964(a,1)),flip(a)]. 24166 x => (y => x) = 1. [para(14927(a,1),24146(a,1,2,2))]. 24167 $F # answer("(A12)[= 1]"). [resolve(24166,a,51,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 51 40 given #115 (H,wt=7): 24166 x => (y => x) = 1. [para(14927(a,1),24146(a,1,2,2))]. given #116 (H,wt=9): 24163 x => ((x => y) => y) = 1. [para(1224(a,1),24146(a,1,2,2))]. given #117 (H,wt=12): 24460 x * (1 * ~ ((x => y) => y)) = 0. [para(24163(a,1),20371(a,1,2,1))]. given #118 (H,wt=10): 24488 x * ~ ((x => y) => y) = 0. [para(573(a,1),24460(a,1,2))]. given #119 (H,wt=12): 24586 x ^ (~ ((x => y) => y) => 0) = x. [para(24488(a,1),10120(a,1,2,2))]. given #120 (H,wt=9): 24616 x ^ ((x => y) => y) = x. [para(3534(a,1),24586(a,1,2))]. given #121 (H,wt=13): 24715 ((x => y) => y) v x = (x => y) => y. [para(24616(a,1),277(a,1,2))]. given #122 (H,wt=13): 24754 (x => y) => (x => ((y => z) => z)) = 1. [para(24616(a,1),17356(a,1,1,2))]. given #123 (H,wt=13): 24779 x ^ (1 => (y => (z v (x * y)))) = x. [para(24146(a,1),24616(a,1,2,1))]. given #124 (H,wt=11): 24804 x ^ (y => (z v (x * y))) = x. [para(22964(a,1),24779(a,1,2))]. given #125 (H,wt=11): 24806 (x => (y v (z * x))) ^ z = z. [para(24804(a,1),19(a,1)),flip(a)]. given #126 (H,wt=11): 24831 (x => (y v (x * z))) ^ z = z. [para(25(a,1),24806(a,1,1,2,2))]. given #127 (H,wt=13): 24789 (((x => y) => y) => z) => (x => z) = 1. [para(24715(a,1),24023(a,1,1,1))]. given #128 (H,wt=13): 24874 1 => (x => (((x => y) ^ z) => y)) = 1. [para(24026(a,1),24789(a,1,1))]. given #129 (H,wt=11): 24880 x => (((x => y) ^ z) => y) = 1. [para(24874(a,1),22964(a,1)),flip(a)]. given #130 (H,wt=11): 24881 x => ((y ^ (x => z)) => z) = 1. [para(19(a,1),24880(a,1,2,1))]. given #131 (H,wt=13): 24915 x ^ (1 => ((y ^ (x => z)) => z)) = x. [para(24881(a,1),24616(a,1,2,1))]. given #132 (H,wt=11): 24919 x ^ ((y ^ (x => z)) => z) = x. [para(22964(a,1),24915(a,1,2))]. given #133 (H,wt=15): 24059 (x => y) v (((x v z) => y) * 1) = x => y. [para(24025(a,1),1224(a,1,2,2))]. given #134 (H,wt=13): 24937 (x => y) v ((x v z) => y) = x => y. [para(24(a,1),24059(a,1,2))]. given #135 (H,wt=15): 24134 x v (~ ~ (y * ~ (~ x * y)) * 1) = x. [para(24109(a,1),22766(a,1,2,2))]. given #136 (H,wt=15): 24778 (x => y) ^ (1 => ~ (x * ~ y)) = x => y. [para(22424(a,1),24616(a,1,2,1))]. given #137 (H,wt=13): 24948 (x => y) ^ ~ (x * ~ y) = x => y. [para(22964(a,1),24778(a,1,2))]. given #138 (H,wt=15): 24945 x v (~ ~ (y * ~ (y * ~ x)) * 1) = x. [para(25(a,1),24134(a,1,2,1,1,1,2,1))]. given #139 (H,wt=13): 24958 x v ((y * ~ (y * ~ x)) * 1) = x. [para(36(a,1),24945(a,1,2,1))]. given #140 (H,wt=11): 24959 x v (y * ~ (y * ~ x)) = x. [para(24(a,1),24958(a,1,2))]. given #141 (H,wt=15): 24987 (x => y) ^ ~ (x * ~ y) = ~ (x * ~ y). [para(24959(a,1),24831(a,1,1,2))]. given #142 (H,wt=9): 24993 ~ (x * ~ y) = x => y. [para(24987(a,1),24948(a,1))]. given #143 (H,wt=9): 25031 ~ (x * y) = x => ~ y. [para(36(a,1),24993(a,1,1,2))]. given #144 (H,wt=13): 25136 ~ x => (y * ~ z) = (y => z) => x. [para(24993(a,1),22491(a,1,1)),flip(a)]. given #145 (H,wt=11): 25340 (x v y) => ((x => y) => y) = 1. [para(25136(a,1),18404(a,1,2))]. given #146 (H,wt=13): 25191 ~ (x * (y * z)) = (x * y) => ~ z. [para(26(a,1),25031(a,1,1))]. given #147 (H,wt=13): 25375 ~ (x * (y * z)) = z => ~ (x * y). [para(25191(a,2),22305(a,1))]. given #148 (H,wt=13): 25395 x => ~ (y * z) = z => ~ (x * y). [para(25375(a,1),25031(a,1)),flip(a)]. given #149 (H,wt=13): 25410 x => ~ (y * z) = y => (z => ~ x). [para(25031(a,1),25395(a,1,2)),flip(a)]. given #150 (H,wt=13): 25428 x => (~ y => ~ z) = z => (x => y). [para(24993(a,1),25410(a,1,2)),flip(a)]. given #151 (H,wt=11): 25436 x => (y => z) = y => (x => z). [para(22336(a,1),25428(a,1,2))]. -------- Proof 11 -------- "(A2)[= 1]". ============================== PROOF ================================= % Proof 11 at 2.07 (+ 0.04) seconds: "(A2)[= 1]". % Length of proof is 119. % Level of proof is 40. % Maximum clause weight is 20. % Given clauses 151. 2 (x => y) => ((y => z) => (x => z)) = 1 # label("(A2)[= 1]") # label(non_clause) # label(goal). [goal]. 18 x v y = y v x # label("(D5)"). [assumption]. 19 x ^ y = y ^ x # label("(D6)"). [assumption]. 20 x v (x ^ y) = x # label("(D7)"). [assumption]. 21 x ^ (x v y) = x # label("(D8)"). [assumption]. 22 x ^ 0 = 0 # label("(D9)"). [assumption]. 23 x ^ 1 = x # label("(D10)"). [assumption]. 24 x * 1 = x # label("(M1)"). [assumption]. 25 x * y = y * x # label("(M2)"). [assumption]. 26 (x * y) * z = x * (y * z) # label("(M3)"). [assumption]. 27 x * (y v z) = (x * y) v (x * z) # label("(R1)"). [assumption]. 28 (x * y) v (x * z) = x * (y v z). [copy(27),flip(a)]. 29 x => (y ^ z) = (x => y) ^ (x => z) # label("(R2)"). [assumption]. 30 (x => y) ^ (x => z) = x => (y ^ z). [copy(29),flip(a)]. 31 (x * (x => y)) v y = y # label("(R3)"). [assumption]. 32 (x => (x * y)) ^ y = y # label("(R4)"). [assumption]. 36 ~ ~ x = x # label("(I)"). [assumption]. 37 (x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y # label("(N)"). [assumption]. 38 ~ x = x => 0 # label("(~ def)"). [assumption]. 39 x => 0 = ~ x. [copy(38),flip(a)]. 41 (c3 => c4) => ((c4 => c5) => (c3 => c5)) != 1 # label("(A2)[= 1]") # answer("(A2)[= 1]"). [deny(2)]. 268 (x ^ y) v x = x. [para(20(a,1),18(a,1)),flip(a)]. 341 x ^ (y v x) = x. [para(18(a,1),21(a,1,2))]. 344 (x v y) ^ x = x. [para(21(a,1),19(a,1)),flip(a)]. 394 x v 0 = x. [para(22(a,1),20(a,1,2))]. 446 1 ^ x = x. [para(23(a,1),19(a,1)),flip(a)]. 573 1 * x = x. [para(25(a,1),24(a,1))]. 696 x * (y * z) = z * (x * y). [para(26(a,1),25(a,1))]. 1224 x v (y * (y => x)) = x. [para(31(a,1),18(a,1)),flip(a)]. 1448 x ^ (y => (y * x)) = x. [para(32(a,1),19(a,1)),flip(a)]. 1488 x => (x * 1) = 1. [para(32(a,1),23(a,1)),flip(a)]. 1517 (x => (y * x)) ^ y = y. [para(25(a,1),32(a,1,1,2))]. 3322 (x => (x => ~ y)) ^ (y => (~ ~ y => ~ x)) = x => ~ y. [para(36(a,1),37(a,1,2,1))]. 3534 ~ x => 0 = x. [para(39(a,2),36(a,1))]. 3677 x * (x => 0) = 0. [para(394(a,1),31(a,1))]. 4701 (x ^ y) v y = y. [para(19(a,1),268(a,1,1))]. 5418 (x v y) ^ y = y. [para(341(a,1),19(a,1)),flip(a)]. 6180 x => x = 1. [para(24(a,1),1488(a,1,2))]. 6421 x => (x ^ (x v y)) = 1. [para(21(a,1),6180(a,1,1))]. 6457 x => (x ^ y) = 1 ^ (x => y). [para(6180(a,1),30(a,1,1)),flip(a)]. 6556 ~ 0 = 1. [para(6180(a,1),39(a,1)),flip(a)]. 7163 x * ~ x = 0. [para(39(a,1),3677(a,1,2))]. 7185 ~ x * x = 0. [para(3534(a,1),3677(a,1,2))]. 7423 x v (y * ~ y) = x. [para(7163(a,2),394(a,1,2))]. 9081 x * (y v ~ x) = x * y. [para(7423(a,1),28(a,1)),flip(a)]. 10120 x ^ (y => (x * y)) = x. [para(25(a,1),1448(a,1,2,2))]. 12525 x * (y v ~ x) = y * x. [para(9081(a,2),25(a,1))]. 13223 ~ x * (y v x) = y * ~ x. [para(36(a,1),12525(a,1,2,2))]. 14135 x * (y * z) = y * (x * z). [para(25(a,1),696(a,1,2))]. 15852 x => (x ^ y) = x => y. [para(6457(a,2),446(a,1))]. 16378 x => (x v y) = 1. [para(15852(a,1),6421(a,1))]. 16552 (x ^ y) => x = 1. [para(268(a,1),16378(a,1,2))]. 16611 (x ^ y) => y = 1. [para(4701(a,1),16378(a,1,2))]. 17216 x => (y => (x * y)) = 1. [para(1517(a,1),16552(a,1,1))]. 17356 (x => (y ^ z)) => (x => z) = 1. [para(30(a,1),16611(a,1,1))]. 18355 (x ^ y) * ~ x = ~ x * x. [para(268(a,1),13223(a,1,2)),flip(a)]. 18769 (x => y) => (x => (y v z)) = 1. [para(21(a,1),17356(a,1,1,2))]. 19297 (x ^ y) * ~ x = 0. [para(18355(a,2),7185(a,1))]. 19364 ~ x * (x ^ y) = 0. [para(19297(a,1),25(a,1)),flip(a)]. 19441 x * ~ (x v y) = 0. [para(344(a,1),19297(a,1,1))]. 19502 ~ x ^ ((x ^ y) => 0) = ~ x. [para(19297(a,1),1448(a,1,2,2))]. 19724 ~ (x v y) * y = 0. [para(5418(a,1),19364(a,1,2))]. 19866 (x * (x => y)) * ~ y = 0. [para(31(a,1),19441(a,1,2,1))]. 20215 ~ x * (y * (y => x)) = 0. [para(1224(a,1),19724(a,1,1,1))]. 20371 x * ((x => y) * ~ y) = 0. [para(19866(a,1),26(a,1)),flip(a)]. 20623 x * (y * (y => ~ x)) = 0. [para(36(a,1),20215(a,1,1))]. 21289 x * (y * (x => ~ y)) = 0. [para(20623(a,1),14135(a,1)),flip(a)]. 21329 (x * y) * (x => ~ y) = 0. [para(21289(a,1),26(a,2))]. 21556 (x * y) => ((x => ~ y) => 0) = 1. [para(21329(a,1),17216(a,1,2,2))]. 21817 ~ x ^ ~ (x ^ y) = ~ x. [para(39(a,1),19502(a,1,2))]. 21974 ~ (x v y) ^ ~ y = ~ (x v y). [para(5418(a,1),21817(a,1,2,1))]. 21986 (x * y) => ~ (x => ~ y) = 1. [para(39(a,1),21556(a,1,2))]. 22050 (x * ~ y) => ~ (x => y) = 1. [para(36(a,1),21986(a,1,2,1,2))]. 22259 (x => ~ (y v z)) => (x => ~ z) = 1. [para(21974(a,1),17356(a,1,1,2))]. 22300 (x => (x => ~ y)) ^ (y => (y => ~ x)) = x => ~ y. [para(36(a,1),3322(a,1,2,2,1))]. 22302 (x => (x => ~ y)) ^ (y => (y => ~ x)) = y => ~ x. [para(22300(a,1),19(a,1)),flip(a)]. 22305 x => ~ y = y => ~ x. [para(22302(a,1),22300(a,1))]. 22336 ~ x => ~ y = y => x. [para(36(a,1),22305(a,1,2)),flip(a)]. 22424 (x => y) => ~ (x * ~ y) = 1. [para(22305(a,1),22050(a,1))]. 22491 ~ x => y = ~ y => x. [para(36(a,1),22336(a,1,2))]. 22675 ((x v y) => z) => (~ z => ~ y) = 1. [para(22336(a,1),22259(a,1,1))]. 22730 ~ 0 => x = x. [para(22491(a,1),3534(a,1))]. 22766 x v (~ y * (~ x => y)) = x. [para(22491(a,1),1224(a,1,2,2))]. 22964 1 => x = x. [para(6556(a,1),22730(a,1,1))]. 24023 ((x v y) => z) => (y => z) = 1. [para(22336(a,1),22675(a,1,2))]. 24026 (x => y) => ((x ^ z) => y) = 1. [para(20(a,1),24023(a,1,1,1))]. 24077 ((x => (y * x)) => z) => (y => z) = 1. [para(1517(a,1),24026(a,1,2,1))]. 24089 1 => (x => (y => ((x * y) v z))) = 1. [para(18769(a,1),24077(a,1,1))]. 24093 1 => (x => ~ (y * ~ (x * y))) = 1. [para(22424(a,1),24077(a,1,1))]. 24094 1 => (x => (y => (z v (x * y)))) = 1. [para(18(a,1),24089(a,1,2,2,2))]. 24109 x => ~ (y * ~ (x * y)) = 1. [para(24093(a,1),22964(a,1)),flip(a)]. 24134 x v (~ ~ (y * ~ (~ x * y)) * 1) = x. [para(24109(a,1),22766(a,1,2,2))]. 24146 x => (y => (z v (x * y))) = 1. [para(24094(a,1),22964(a,1)),flip(a)]. 24163 x => ((x => y) => y) = 1. [para(1224(a,1),24146(a,1,2,2))]. 24460 x * (1 * ~ ((x => y) => y)) = 0. [para(24163(a,1),20371(a,1,2,1))]. 24488 x * ~ ((x => y) => y) = 0. [para(573(a,1),24460(a,1,2))]. 24586 x ^ (~ ((x => y) => y) => 0) = x. [para(24488(a,1),10120(a,1,2,2))]. 24616 x ^ ((x => y) => y) = x. [para(3534(a,1),24586(a,1,2))]. 24754 (x => y) => (x => ((y => z) => z)) = 1. [para(24616(a,1),17356(a,1,1,2))]. 24778 (x => y) ^ (1 => ~ (x * ~ y)) = x => y. [para(22424(a,1),24616(a,1,2,1))]. 24779 x ^ (1 => (y => (z v (x * y)))) = x. [para(24146(a,1),24616(a,1,2,1))]. 24804 x ^ (y => (z v (x * y))) = x. [para(22964(a,1),24779(a,1,2))]. 24806 (x => (y v (z * x))) ^ z = z. [para(24804(a,1),19(a,1)),flip(a)]. 24831 (x => (y v (x * z))) ^ z = z. [para(25(a,1),24806(a,1,1,2,2))]. 24945 x v (~ ~ (y * ~ (y * ~ x)) * 1) = x. [para(25(a,1),24134(a,1,2,1,1,1,2,1))]. 24948 (x => y) ^ ~ (x * ~ y) = x => y. [para(22964(a,1),24778(a,1,2))]. 24958 x v ((y * ~ (y * ~ x)) * 1) = x. [para(36(a,1),24945(a,1,2,1))]. 24959 x v (y * ~ (y * ~ x)) = x. [para(24(a,1),24958(a,1,2))]. 24987 (x => y) ^ ~ (x * ~ y) = ~ (x * ~ y). [para(24959(a,1),24831(a,1,1,2))]. 24993 ~ (x * ~ y) = x => y. [para(24987(a,1),24948(a,1))]. 25031 ~ (x * y) = x => ~ y. [para(36(a,1),24993(a,1,1,2))]. 25191 ~ (x * (y * z)) = (x * y) => ~ z. [para(26(a,1),25031(a,1,1))]. 25375 ~ (x * (y * z)) = z => ~ (x * y). [para(25191(a,2),22305(a,1))]. 25395 x => ~ (y * z) = z => ~ (x * y). [para(25375(a,1),25031(a,1)),flip(a)]. 25410 x => ~ (y * z) = y => (z => ~ x). [para(25031(a,1),25395(a,1,2)),flip(a)]. 25428 x => (~ y => ~ z) = z => (x => y). [para(24993(a,1),25410(a,1,2)),flip(a)]. 25436 x => (y => z) = y => (x => z). [para(22336(a,1),25428(a,1,2))]. 25464 (x => y) => ((y => z) => (x => z)) = 1. [para(25436(a,1),24754(a,1,2))]. 25465 $F # answer("(A2)[= 1]"). [resolve(25464,a,41,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 41 given #152 (H,wt=11): 25466 (x => y) => ((x v y) => y) = 1. [para(25436(a,1),25340(a,1))]. given #153 (H,wt=13): 25464 (x => y) => ((y => z) => (x => z)) = 1. [para(25436(a,1),24754(a,1,2))]. given #154 (H,wt=16): 22494 (x => (x => y)) ^ (~ y => (x => y)) = x => y. [para(22336(a,1),37(a,1,2,2))]. -------- Proof 12 -------- "(A13)[= 1]". ============================== PROOF ================================= % Proof 12 at 2.12 (+ 0.05) seconds: "(A13)[= 1]". % Length of proof is 18. % Level of proof is 8. % Maximum clause weight is 20. % Given clauses 154. 13 ((x => (x => y)) ^ (~ y => (x => y))) => (x => y) = 1 # label("(A13)[= 1]") # label(non_clause) # label(goal). [goal]. 19 x ^ y = y ^ x # label("(D6)"). [assumption]. 23 x ^ 1 = x # label("(D10)"). [assumption]. 24 x * 1 = x # label("(M1)"). [assumption]. 32 (x => (x * y)) ^ y = y # label("(R4)"). [assumption]. 36 ~ ~ x = x # label("(I)"). [assumption]. 37 (x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y # label("(N)"). [assumption]. 52 ((c28 => (c28 => c29)) ^ (~ c29 => (c28 => c29))) => (c28 => c29) != 1 # label("(A13)[= 1]") # answer("(A13)[= 1]"). [deny(13)]. 1488 x => (x * 1) = 1. [para(32(a,1),23(a,1)),flip(a)]. 3322 (x => (x => ~ y)) ^ (y => (~ ~ y => ~ x)) = x => ~ y. [para(36(a,1),37(a,1,2,1))]. 6180 x => x = 1. [para(24(a,1),1488(a,1,2))]. 22300 (x => (x => ~ y)) ^ (y => (y => ~ x)) = x => ~ y. [para(36(a,1),3322(a,1,2,2,1))]. 22302 (x => (x => ~ y)) ^ (y => (y => ~ x)) = y => ~ x. [para(22300(a,1),19(a,1)),flip(a)]. 22305 x => ~ y = y => ~ x. [para(22302(a,1),22300(a,1))]. 22336 ~ x => ~ y = y => x. [para(36(a,1),22305(a,1,2)),flip(a)]. 22494 (x => (x => y)) ^ (~ y => (x => y)) = x => y. [para(22336(a,1),37(a,1,2,2))]. 25492 ((x => (x => y)) ^ (~ y => (x => y))) => (x => y) = 1. [para(22494(a,1),6180(a,1,2))]. 25493 $F # answer("(A13)[= 1]"). [resolve(25492,a,52,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 52 given #155 (H,wt=17): 25481 ((x v y) => y) v ((x => y) * 1) = (x v y) => y. [para(25466(a,1),1224(a,1,2,2))]. given #156 (H,wt=15): 25495 ((x v y) => y) v (x => y) = (x v y) => y. [para(24(a,1),25481(a,1,2))]. given #157 (H,wt=15): 25496 (x => y) v ((x v y) => y) = (x v y) => y. [para(25495(a,1),18(a,1)),flip(a)]. given #158 (H,wt=9): 25499 (x v y) => y = x => y. [para(25496(a,1),24937(a,1))]. given #159 (H,wt=9): 25510 (x v y) => x = y => x. [para(18(a,1),25499(a,1,1))]. given #160 (H,wt=13): 25807 (x v (y ^ z)) => y = (y v x) => y. [para(18554(a,1),25510(a,1,1)),flip(a)]. given #161 (H,wt=11): 25857 (x v (y ^ z)) => y = x => y. [para(25807(a,2),25510(a,1))]. given #162 (H,wt=11): 25859 (x v (y ^ z)) => z = x => z. [para(19(a,1),25857(a,1,1,2))]. given #163 (H,wt=18): 25492 ((x => (x => y)) ^ (~ y => (x => y))) => (x => y) = 1. [para(22494(a,1),6180(a,1,2))]. given #164 (H,wt=21): 25896 (x v y) => ((z ^ (y => u)) => u) = x => ((z ^ (y => u)) => u). [para(24919(a,1),25859(a,1,1,2))]. given #165 (H,wt=15): 25897 (x v y) => (((x => z) ^ (y => z)) => z) = 1. [para(25896(a,2),24880(a,1))]. -------- Proof 13 -------- "(A8)[= 1]". ============================== PROOF ================================= % Proof 13 at 2.43 (+ 0.06) seconds: "(A8)[= 1]". % Length of proof is 148. % Level of proof is 51. % Maximum clause weight is 21. % Given clauses 165. 8 ((x => z) ^ (y => z)) => ((x v y) => z) = 1 # label("(A8)[= 1]") # label(non_clause) # label(goal). [goal]. 14 (x v y) v z = x v (y v z) # label("(D1)"). [assumption]. 18 x v y = y v x # label("(D5)"). [assumption]. 19 x ^ y = y ^ x # label("(D6)"). [assumption]. 20 x v (x ^ y) = x # label("(D7)"). [assumption]. 21 x ^ (x v y) = x # label("(D8)"). [assumption]. 22 x ^ 0 = 0 # label("(D9)"). [assumption]. 23 x ^ 1 = x # label("(D10)"). [assumption]. 24 x * 1 = x # label("(M1)"). [assumption]. 25 x * y = y * x # label("(M2)"). [assumption]. 26 (x * y) * z = x * (y * z) # label("(M3)"). [assumption]. 27 x * (y v z) = (x * y) v (x * z) # label("(R1)"). [assumption]. 28 (x * y) v (x * z) = x * (y v z). [copy(27),flip(a)]. 29 x => (y ^ z) = (x => y) ^ (x => z) # label("(R2)"). [assumption]. 30 (x => y) ^ (x => z) = x => (y ^ z). [copy(29),flip(a)]. 31 (x * (x => y)) v y = y # label("(R3)"). [assumption]. 32 (x => (x * y)) ^ y = y # label("(R4)"). [assumption]. 36 ~ ~ x = x # label("(I)"). [assumption]. 37 (x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y # label("(N)"). [assumption]. 38 ~ x = x => 0 # label("(~ def)"). [assumption]. 39 x => 0 = ~ x. [copy(38),flip(a)]. 47 ((c17 => c18) ^ (c19 => c18)) => ((c17 v c19) => c18) != 1 # label("(A8)[= 1]") # answer("(A8)[= 1]"). [deny(8)]. 170 x v (y v z) = z v (x v y). [para(18(a,1),14(a,1)),flip(a)]. 268 (x ^ y) v x = x. [para(20(a,1),18(a,1)),flip(a)]. 277 x v (y ^ x) = x. [para(19(a,1),20(a,1,2))]. 341 x ^ (y v x) = x. [para(18(a,1),21(a,1,2))]. 344 (x v y) ^ x = x. [para(21(a,1),19(a,1)),flip(a)]. 394 x v 0 = x. [para(22(a,1),20(a,1,2))]. 446 1 ^ x = x. [para(23(a,1),19(a,1)),flip(a)]. 573 1 * x = x. [para(25(a,1),24(a,1))]. 696 x * (y * z) = z * (x * y). [para(26(a,1),25(a,1))]. 1224 x v (y * (y => x)) = x. [para(31(a,1),18(a,1)),flip(a)]. 1448 x ^ (y => (y * x)) = x. [para(32(a,1),19(a,1)),flip(a)]. 1488 x => (x * 1) = 1. [para(32(a,1),23(a,1)),flip(a)]. 1517 (x => (y * x)) ^ y = y. [para(25(a,1),32(a,1,1,2))]. 3322 (x => (x => ~ y)) ^ (y => (~ ~ y => ~ x)) = x => ~ y. [para(36(a,1),37(a,1,2,1))]. 3534 ~ x => 0 = x. [para(39(a,2),36(a,1))]. 3677 x * (x => 0) = 0. [para(394(a,1),31(a,1))]. 4701 (x ^ y) v y = y. [para(19(a,1),268(a,1,1))]. 5418 (x v y) ^ y = y. [para(341(a,1),19(a,1)),flip(a)]. 6180 x => x = 1. [para(24(a,1),1488(a,1,2))]. 6421 x => (x ^ (x v y)) = 1. [para(21(a,1),6180(a,1,1))]. 6457 x => (x ^ y) = 1 ^ (x => y). [para(6180(a,1),30(a,1,1)),flip(a)]. 6556 ~ 0 = 1. [para(6180(a,1),39(a,1)),flip(a)]. 7163 x * ~ x = 0. [para(39(a,1),3677(a,1,2))]. 7185 ~ x * x = 0. [para(3534(a,1),3677(a,1,2))]. 7423 x v (y * ~ y) = x. [para(7163(a,2),394(a,1,2))]. 9081 x * (y v ~ x) = x * y. [para(7423(a,1),28(a,1)),flip(a)]. 10120 x ^ (y => (x * y)) = x. [para(25(a,1),1448(a,1,2,2))]. 12525 x * (y v ~ x) = y * x. [para(9081(a,2),25(a,1))]. 13223 ~ x * (y v x) = y * ~ x. [para(36(a,1),12525(a,1,2,2))]. 13825 x v (y v (x ^ z)) = y v x. [para(268(a,1),170(a,1,2)),flip(a)]. 14135 x * (y * z) = y * (x * z). [para(25(a,1),696(a,1,2))]. 15852 x => (x ^ y) = x => y. [para(6457(a,2),446(a,1))]. 16378 x => (x v y) = 1. [para(15852(a,1),6421(a,1))]. 16552 (x ^ y) => x = 1. [para(268(a,1),16378(a,1,2))]. 16611 (x ^ y) => y = 1. [para(4701(a,1),16378(a,1,2))]. 17083 x => (y => (y * x)) = 1. [para(32(a,1),16552(a,1,1))]. 17216 x => (y => (x * y)) = 1. [para(1517(a,1),16552(a,1,1))]. 17356 (x => (y ^ z)) => (x => z) = 1. [para(30(a,1),16611(a,1,1))]. 18355 (x ^ y) * ~ x = ~ x * x. [para(268(a,1),13223(a,1,2)),flip(a)]. 18404 (x v y) => (~ y => (x * ~ y)) = 1. [para(13223(a,1),17083(a,1,2,2))]. 18554 x v (y v (x ^ z)) = x v y. [para(13825(a,2),18(a,1))]. 18769 (x => y) => (x => (y v z)) = 1. [para(21(a,1),17356(a,1,1,2))]. 19297 (x ^ y) * ~ x = 0. [para(18355(a,2),7185(a,1))]. 19364 ~ x * (x ^ y) = 0. [para(19297(a,1),25(a,1)),flip(a)]. 19441 x * ~ (x v y) = 0. [para(344(a,1),19297(a,1,1))]. 19502 ~ x ^ ((x ^ y) => 0) = ~ x. [para(19297(a,1),1448(a,1,2,2))]. 19724 ~ (x v y) * y = 0. [para(5418(a,1),19364(a,1,2))]. 19866 (x * (x => y)) * ~ y = 0. [para(31(a,1),19441(a,1,2,1))]. 20215 ~ x * (y * (y => x)) = 0. [para(1224(a,1),19724(a,1,1,1))]. 20371 x * ((x => y) * ~ y) = 0. [para(19866(a,1),26(a,1)),flip(a)]. 20623 x * (y * (y => ~ x)) = 0. [para(36(a,1),20215(a,1,1))]. 21289 x * (y * (x => ~ y)) = 0. [para(20623(a,1),14135(a,1)),flip(a)]. 21329 (x * y) * (x => ~ y) = 0. [para(21289(a,1),26(a,2))]. 21556 (x * y) => ((x => ~ y) => 0) = 1. [para(21329(a,1),17216(a,1,2,2))]. 21817 ~ x ^ ~ (x ^ y) = ~ x. [para(39(a,1),19502(a,1,2))]. 21974 ~ (x v y) ^ ~ y = ~ (x v y). [para(5418(a,1),21817(a,1,2,1))]. 21986 (x * y) => ~ (x => ~ y) = 1. [para(39(a,1),21556(a,1,2))]. 22050 (x * ~ y) => ~ (x => y) = 1. [para(36(a,1),21986(a,1,2,1,2))]. 22259 (x => ~ (y v z)) => (x => ~ z) = 1. [para(21974(a,1),17356(a,1,1,2))]. 22300 (x => (x => ~ y)) ^ (y => (y => ~ x)) = x => ~ y. [para(36(a,1),3322(a,1,2,2,1))]. 22302 (x => (x => ~ y)) ^ (y => (y => ~ x)) = y => ~ x. [para(22300(a,1),19(a,1)),flip(a)]. 22305 x => ~ y = y => ~ x. [para(22302(a,1),22300(a,1))]. 22336 ~ x => ~ y = y => x. [para(36(a,1),22305(a,1,2)),flip(a)]. 22424 (x => y) => ~ (x * ~ y) = 1. [para(22305(a,1),22050(a,1))]. 22491 ~ x => y = ~ y => x. [para(36(a,1),22336(a,1,2))]. 22675 ((x v y) => z) => (~ z => ~ y) = 1. [para(22336(a,1),22259(a,1,1))]. 22730 ~ 0 => x = x. [para(22491(a,1),3534(a,1))]. 22766 x v (~ y * (~ x => y)) = x. [para(22491(a,1),1224(a,1,2,2))]. 22964 1 => x = x. [para(6556(a,1),22730(a,1,1))]. 24023 ((x v y) => z) => (y => z) = 1. [para(22336(a,1),22675(a,1,2))]. 24025 ((x v y) => z) => (x => z) = 1. [para(18(a,1),24023(a,1,1,1))]. 24026 (x => y) => ((x ^ z) => y) = 1. [para(20(a,1),24023(a,1,1,1))]. 24059 (x => y) v (((x v z) => y) * 1) = x => y. [para(24025(a,1),1224(a,1,2,2))]. 24077 ((x => (y * x)) => z) => (y => z) = 1. [para(1517(a,1),24026(a,1,2,1))]. 24089 1 => (x => (y => ((x * y) v z))) = 1. [para(18769(a,1),24077(a,1,1))]. 24093 1 => (x => ~ (y * ~ (x * y))) = 1. [para(22424(a,1),24077(a,1,1))]. 24094 1 => (x => (y => (z v (x * y)))) = 1. [para(18(a,1),24089(a,1,2,2,2))]. 24109 x => ~ (y * ~ (x * y)) = 1. [para(24093(a,1),22964(a,1)),flip(a)]. 24134 x v (~ ~ (y * ~ (~ x * y)) * 1) = x. [para(24109(a,1),22766(a,1,2,2))]. 24146 x => (y => (z v (x * y))) = 1. [para(24094(a,1),22964(a,1)),flip(a)]. 24163 x => ((x => y) => y) = 1. [para(1224(a,1),24146(a,1,2,2))]. 24460 x * (1 * ~ ((x => y) => y)) = 0. [para(24163(a,1),20371(a,1,2,1))]. 24488 x * ~ ((x => y) => y) = 0. [para(573(a,1),24460(a,1,2))]. 24586 x ^ (~ ((x => y) => y) => 0) = x. [para(24488(a,1),10120(a,1,2,2))]. 24616 x ^ ((x => y) => y) = x. [para(3534(a,1),24586(a,1,2))]. 24715 ((x => y) => y) v x = (x => y) => y. [para(24616(a,1),277(a,1,2))]. 24778 (x => y) ^ (1 => ~ (x * ~ y)) = x => y. [para(22424(a,1),24616(a,1,2,1))]. 24779 x ^ (1 => (y => (z v (x * y)))) = x. [para(24146(a,1),24616(a,1,2,1))]. 24789 (((x => y) => y) => z) => (x => z) = 1. [para(24715(a,1),24023(a,1,1,1))]. 24804 x ^ (y => (z v (x * y))) = x. [para(22964(a,1),24779(a,1,2))]. 24806 (x => (y v (z * x))) ^ z = z. [para(24804(a,1),19(a,1)),flip(a)]. 24831 (x => (y v (x * z))) ^ z = z. [para(25(a,1),24806(a,1,1,2,2))]. 24874 1 => (x => (((x => y) ^ z) => y)) = 1. [para(24026(a,1),24789(a,1,1))]. 24880 x => (((x => y) ^ z) => y) = 1. [para(24874(a,1),22964(a,1)),flip(a)]. 24881 x => ((y ^ (x => z)) => z) = 1. [para(19(a,1),24880(a,1,2,1))]. 24915 x ^ (1 => ((y ^ (x => z)) => z)) = x. [para(24881(a,1),24616(a,1,2,1))]. 24919 x ^ ((y ^ (x => z)) => z) = x. [para(22964(a,1),24915(a,1,2))]. 24937 (x => y) v ((x v z) => y) = x => y. [para(24(a,1),24059(a,1,2))]. 24945 x v (~ ~ (y * ~ (y * ~ x)) * 1) = x. [para(25(a,1),24134(a,1,2,1,1,1,2,1))]. 24948 (x => y) ^ ~ (x * ~ y) = x => y. [para(22964(a,1),24778(a,1,2))]. 24958 x v ((y * ~ (y * ~ x)) * 1) = x. [para(36(a,1),24945(a,1,2,1))]. 24959 x v (y * ~ (y * ~ x)) = x. [para(24(a,1),24958(a,1,2))]. 24987 (x => y) ^ ~ (x * ~ y) = ~ (x * ~ y). [para(24959(a,1),24831(a,1,1,2))]. 24993 ~ (x * ~ y) = x => y. [para(24987(a,1),24948(a,1))]. 25031 ~ (x * y) = x => ~ y. [para(36(a,1),24993(a,1,1,2))]. 25136 ~ x => (y * ~ z) = (y => z) => x. [para(24993(a,1),22491(a,1,1)),flip(a)]. 25191 ~ (x * (y * z)) = (x * y) => ~ z. [para(26(a,1),25031(a,1,1))]. 25340 (x v y) => ((x => y) => y) = 1. [para(25136(a,1),18404(a,1,2))]. 25375 ~ (x * (y * z)) = z => ~ (x * y). [para(25191(a,2),22305(a,1))]. 25395 x => ~ (y * z) = z => ~ (x * y). [para(25375(a,1),25031(a,1)),flip(a)]. 25410 x => ~ (y * z) = y => (z => ~ x). [para(25031(a,1),25395(a,1,2)),flip(a)]. 25428 x => (~ y => ~ z) = z => (x => y). [para(24993(a,1),25410(a,1,2)),flip(a)]. 25436 x => (y => z) = y => (x => z). [para(22336(a,1),25428(a,1,2))]. 25466 (x => y) => ((x v y) => y) = 1. [para(25436(a,1),25340(a,1))]. 25481 ((x v y) => y) v ((x => y) * 1) = (x v y) => y. [para(25466(a,1),1224(a,1,2,2))]. 25495 ((x v y) => y) v (x => y) = (x v y) => y. [para(24(a,1),25481(a,1,2))]. 25496 (x => y) v ((x v y) => y) = (x v y) => y. [para(25495(a,1),18(a,1)),flip(a)]. 25499 (x v y) => y = x => y. [para(25496(a,1),24937(a,1))]. 25510 (x v y) => x = y => x. [para(18(a,1),25499(a,1,1))]. 25807 (x v (y ^ z)) => y = (y v x) => y. [para(18554(a,1),25510(a,1,1)),flip(a)]. 25857 (x v (y ^ z)) => y = x => y. [para(25807(a,2),25510(a,1))]. 25859 (x v (y ^ z)) => z = x => z. [para(19(a,1),25857(a,1,1,2))]. 25896 (x v y) => ((z ^ (y => u)) => u) = x => ((z ^ (y => u)) => u). [para(24919(a,1),25859(a,1,1,2))]. 25897 (x v y) => (((x => z) ^ (y => z)) => z) = 1. [para(25896(a,2),24880(a,1))]. 25898 ((x => y) ^ (z => y)) => ((x v z) => y) = 1. [para(25897(a,1),25436(a,1)),flip(a)]. 25899 $F # answer("(A8)[= 1]"). [resolve(25898,a,47,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=165. Generated=291667. Kept=25870. proofs=13. Usable=161. Sos=19998. Demods=0. Limbo=0, Disabled=5746. Hints=197. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=27152. Back_subsumed=1217. Sos_limit_deleted=238645. Sos_displaced=4353. 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=0. Megabytes=25.86. User_CPU=2.43, System_CPU=0.06, Wall_clock=3. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED THEOREM PROVED Exiting with 13 proofs. ------ process 9526 exit (max_proofs) ------  Process 9526 exit (max_proofs) Sat Sep 19 09:10:44 2009