============================== Prover9 =============================== Prover9 (64) version 2009-02A, February 2009. Process 9581 was started by veroff on proof, Sat Sep 19 09:11:03 2009 The command was "prover9 -f 2.4.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file 2.4.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(restrict_denials). formulas(assumptions). 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]"). (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)"). (all x all y (x = 1 & y = 1 -> x ^ y = 1)) # label("(4)"). (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)"). x * y = ~ (x => ~ y) # label("(* def)"). 0 = ~ (x => x) # label("(0 def)"). 1 = x => x # label("(1 def)"). end_of_list. formulas(goals). (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)"). end_of_list. formulas(hints). (x v y) v z = x v (y v z). (x ^ y) ^ z = x ^ (y ^ z). x ^ x = x. x v x = x. x v y = y v x. x ^ y = y ^ x. x v (x ^ y) = x. x ^ (x v y) = x. x ^ 0 = 0. x ^ 1 = x. x * 1 = x. x * y = y * x. (x * y) * z = x * (y * z). x * (y v z) = (x * y) v (x * z). x => (y ^ z) = (x => y) ^ (x => z). (x * (x => y)) v y = y. (x => (x * y)) ^ y = y. x => (x => (x => y)) = x => (x => y). (x v y) ^ (x v z) = x v (y ^ z). (x ^ y) v (x ^ z) = x ^ (y v z). ~ ~ x = x. (x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y. ~ ~ x => x = 1. (x => ~ y) => (y => ~ x) = 1. 1 = x => x. x => x = 1. 1 = x => ~ ~ x. x => ~ ~ x = 1. x = ~ ~ x. x => ((x => y) => y) = 1. (x ^ y) => x = 1. (x ^ y) => y = 1. x => (y => x) = 1. 0 = ~ (x => x). ~ (x => x) = 0. 1 = (1 => x) => x. (1 => x) => x = 1. x => ~ y = y => ~ x. ~ 1 = 0. 1 => x = x. x => ~ 1 = ~ x. x => 0 = ~ x. ~ (0 ^ x) = 1. ~ 1 = 0 ^ x. 0 ^ x = ~ 1. 0 ^ x = 0. 0 => x = 1. 0 = x ^ 0. x * y = ~ (x => ~ y). ~ (x => ~ y) = x * y. ~ ~ x = x * 1. x => (y v x) = 1. ((x => y) ^ (z => y)) => ((x v z) => y) = 1. (x => x) ^ (y => y) = 1. 1 = (x v x) => x. (x v x) => x = 1. ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1. 1 = x => (x ^ x). x => (x ^ x) = 1. x = x ^ x. x => 1 = 1. (x => x) ^ (y => 1) = 1. 1 = x => (x ^ 1). x => (x ^ 1) = 1. x = x ^ 1. ~ (x => ~ y) = y * x. x => (x v y) = 1. (x => x) ^ (y => (y v z)) = 1. 1 = x => (x ^ (x v y)). x => (x ^ (x v y)) = 1. x = x ^ (x v y). (x => x) ^ ((y ^ z) => y) = 1. 1 = (x v (x ^ y)) => x. (x v (x ^ y)) => x = 1. ((x => y) ^ 1) => (x => (y ^ x)) = 1. x => (y => ~ (x => ~ y)) = 1. x => (y => (y * x)) = 1. (x => y) => (x => (y ^ x)) = 1. 1 = x => ((y => (y * x)) ^ x). x => ((y => (y * x)) ^ x) = 1. x = (y => (y * x)) ^ x. ((x => y) ^ 1) => ((x v y) => y) = 1. ~ (x * y) = x => ~ y. x => ((y => ~ x) => ~ y) = 1. x => y = ~ y => ~ x. ~ x => ~ y = y => x. ~ (x * y) = y => ~ x. x => ~ (y * (y => ~ x)) = 1. ~ x => ~ (y * (y => x)) = 1. 1 = (x * (x => y)) => y. (x * (x => y)) => y = 1. (x => y) => ((x v y) => y) = 1. 1 = ((x * (x => y)) v y) => y. ((x * (x => y)) v y) => y = 1. (x => y) => ((y => z) => (x => z)) = 1. (1 ^ ((x ^ y) => z)) => ((x ^ y) => (x ^ z)) = 1. 1 = (x => y) => ((z ^ x) => y). (x => y) => ((z ^ x) => y) = 1. ~ (x => y) = x * ~ y. ~ 1 = (x ^ y) * ~ y. (x ^ y) * ~ y = ~ 1. (x ^ y) * ~ y = 0. 0 = ~ x * (y ^ x). ~ x * (y ^ x) = 0. 1 = (x ^ (y ^ z)) => y. (x ^ (y ^ z)) => y = 1. 1 = x => ((y => x) ^ x). x => ((y => x) ^ x) = 1. x = (y => x) ^ x. (x => y) ^ y = y. 1 ^ x = x. (~ x => 0) ^ (y ^ x) = y ^ x. ~ ~ x ^ (y ^ x) = y ^ x. x ^ (y ^ x) = y ^ x. (1 ^ 1) => ((x ^ (y ^ z)) => (x ^ y)) = 1. 1 = (x ^ (y ^ z)) => (x ^ y). (x ^ (y ^ z)) => (x ^ y) = 1. (x ^ y) => (y ^ x) = 1. ((x => (x => y)) ^ (~ y => (x => y))) => (x => y) = 1. 1 = (x ^ y) => (z => y). (x ^ y) => (z => y) = 1. (1 ^ 1) => ((x ^ y) => (x ^ (z => y))) = 1. 1 = (x ^ y) => (x ^ (z => y)). (x ^ y) => (x ^ (z => y)) = 1. x => ((y => x) ^ (z => x)) = 1. x => y = (x => (x => y)) ^ (~ y => (x => y)). (x => (x => y)) ^ (~ y => (x => y)) = x => y. (1 ^ (x => (y v z))) => ((z v x) => (y v z)) = 1. (1 ^ 1) => ((x v y) => (y v x)) = 1. 1 = (x v y) => (y v x). (x v y) => (y v x) = 1. 1 = (((x => y) => (z => y)) => u) => ((z => x) => u). (((x => y) => (z => y)) => u) => ((z => x) => u) = 1. 1 = (((x => y) => y) => z) => (x => z). (((x => y) => y) => z) => (x => z) = 1. 1 = (x => (y => z)) => (y => (x => z)). (x => (y => z)) => (y => (x => z)) = 1. x => (y => z) = y => (x => z). ~ (x => (y => z)) = y * ~ (x => z). x * ~ (y => z) = y * ~ (x => z). x * (y * ~ z) = y * ~ (x => z). x * ~ (y => z) = y * (x * ~ z). x * (y * z) = y * (x * ~ ~ z). x * (y * ~ ~ z) = y * (x * z). x * (y * z) = y * (x * z). x * (y * z) = z * (x * y). x * (y * z) = (x * y) * z. (~ x => (~ x => x)) => (~ x => x) = 1. ~ x => (y => ~ z) = (y * z) => x. ~ x => (~ x => x) = ~ x => x. ~ ~ x => (x => ~ ~ ~ x) = ~ ~ x => ~ x. x => (~ y => ~ z) = (x * z) => y. x => (y => z) = (x * y) => z. (x * y) => z = x => (y => z). x => (x => ~ ~ ~ x) = ~ ~ x => ~ x. x => (x => ~ x) = ~ ~ x => ~ x. ~ ~ x => ~ x = x => (x => ~ x). x => ~ x = x => (x => ~ x). x => (x => ~ x) = x => ~ x. ~ (x => ~ x) = x * ~ (x => ~ x). x * ~ (x => ~ x) = ~ (x => ~ x). x * ~ (x => ~ x) = x * x. x * (x * x) = x * x. (x * x) => y = x => ((x * x) => y). x => ((x * x) => y) = (x * x) => y. x => ((x * x) => y) = x => (x => y). (x => (y ^ z)) => (1 => (x => y)) = 1. (x => (y ^ z)) => (1 => (x => z)) = 1. (x => (y ^ z)) => (x => y) = 1. (x => (y ^ z)) => (x => z) = 1. ((x => (y ^ z)) => (x => y)) ^ ((u => (w ^ v5)) => (u => v5)) = 1. 1 = (x => (y ^ z)) => ((x => y) ^ (x => z)). (x => (y ^ z)) => ((x => y) ^ (x => z)) = 1. (x => y) ^ (x => z) = x => (y ^ z). (x ^ (y v z)) => ((x ^ y) v z) = 1. ~ 1 = (x ^ (y v z)) * ~ ((x ^ y) v z). (x ^ (y v z)) * ~ ((x ^ y) v z) = ~ 1. 1 = (x ^ y) => (y v z). (x ^ y) => (y v z) = 1. 1 = x => ((x v y) ^ x). x => ((x v y) ^ x) = 1. 1 = (x ^ y) => (x ^ (x ^ y)). (x ^ y) => (x ^ (x ^ y)) = 1. 1 = x => (((x => y) => y) ^ x). x => (((x => y) => y) ^ x) = 1. x = (x v y) ^ x. (x v y) ^ x = x. (x => (y * x)) ^ y = y. x ^ y = x ^ (x ^ y). x ^ (x ^ y) = x ^ y. x v (y ^ x) = x. (x * (x => y)) ^ y = x * (x => y). x v (y * (y => x)) = x. (x ^ (y v z)) * ~ ((x ^ y) v z) = 0. (1 ^ 1) => ((x ^ y) => (x ^ (y v z))) = 1. 1 = (x ^ y) => (x ^ (y v z)). (x ^ y) => (x ^ (y v z)) = 1. (x ^ y) v ((x ^ (y ^ z)) * 1) = x ^ y. x ^ (y => (x * y)) = x. x => (x ^ ((x => y) => y)) = 1. x = x ^ ((x => y) => y). x ^ ((x => y) => y) = x. (x ^ y) ^ (1 => (x ^ (y v z))) = x ^ y. (x ^ y) v (x ^ (y ^ z)) = x ^ y. (x ^ y) ^ (x ^ (y v z)) = x ^ y. (x ^ y) ^ (x ^ ((x ^ y) v z)) = x ^ (x ^ y). (x v y) ^ y = y. (x ^ (y v z)) * ~ (z v (x ^ y)) = 0. (x ^ (y v z)) v (x ^ z) = x ^ (y v z). (x ^ (y v z)) ^ (~ (z v (x ^ y)) => 0) = x ^ (y v z). (x ^ (y v z)) v (z ^ x) = x ^ (y v z). (x ^ y) ^ (x ^ (z v (x ^ y))) = x ^ (x ^ y). (x ^ y) ^ (x ^ (z v (x ^ y))) = x ^ y. (x ^ (y v z)) ^ ~ ~ (z v (x ^ y)) = x ^ (y v z). (x ^ (y v z)) ^ (z v (x ^ y)) = x ^ (y v z). (x ^ ((y ^ z) v (x ^ y))) ^ (x ^ y) = x ^ ((y ^ z) v (x ^ y)). x ^ ((y ^ z) v (x ^ y)) = (x ^ y) ^ (x ^ ((y ^ z) v (x ^ y))). (x ^ y) ^ (x ^ ((y ^ z) v (x ^ y))) = x ^ ((y ^ z) v (x ^ y)). x ^ ((y ^ z) v (x ^ y)) = x ^ y. x ^ (y ^ (z v x)) = x ^ y. x ^ (y ^ (z v x)) = y ^ x. (x ^ y) ^ (z ^ x) = z ^ (x ^ y). x ^ (y ^ z) = (x ^ y) ^ (y ^ z). (x ^ y) ^ (y ^ z) = x ^ (y ^ z). (x ^ y) ^ (x ^ z) = z ^ (x ^ y). (x ^ y) ^ (x ^ z) = y ^ (x ^ z). x ^ (y ^ z) = z ^ (y ^ x). x ^ (y ^ z) = (y ^ x) ^ z. (x ^ y) ^ z = y ^ (x ^ z). x => ~ ~ (y v x) = 1. (~ x ^ (y => 0)) => ((x v y) => 0) = 1. 1 = ~ (x v y) => ~ y. ~ (x v y) => ~ y = 1. ~ 1 = x * ~ ((x => y) => y). x * ~ ((x => y) => y) = ~ 1. ~ 1 = (x ^ y) * ~ x. (x ^ y) * ~ x = ~ 1. (x ^ y) * ~ x = 0. x * ~ (x v y) = 0. x * ~ ((x => y) => y) = 0. x * (y * (x => ~ y)) = 0. ~ (x v y) * (y * 1) = 0. ~ (x v y) * y = 0. 0 = x * ~ (y v x). x * ~ (y v x) = 0. (x => 0) ^ ~ (x v y) = ~ (x v y). ~ x ^ ~ (x v y) = ~ (x v y). (~ x ^ ~ y) => ((x v y) => 0) = 1. (~ x ^ ~ y) => ~ (x v y) = 1. ~ 1 = (x v y) * (~ x ^ ~ y). (x v y) * (~ x ^ ~ y) = ~ 1. (x v y) * (~ x ^ ~ y) = 0. ((x v y) => 0) ^ (~ x ^ ~ y) = ~ x ^ ~ y. x ^ (y => (y * x)) = x. ~ x ^ ((x ^ y) => 0) = ~ x. ~ (x v y) ^ (y => 0) = ~ (x v y). ~ x ^ ~ (x ^ y) = ~ x. ~ x = ~ (x ^ y) ^ ~ x. ~ (x ^ y) ^ ~ x = ~ x. ~ (x v y) ^ ~ y = ~ (x v y). ~ (x v y) = ~ y ^ ~ (x v y). ~ x ^ ~ (y v x) = ~ (y v x). ~ (x v y) ^ (~ x ^ ~ y) = ~ x ^ ~ y. ~ x ^ (~ y ^ ~ (y v x)) = ~ y ^ ~ x. ~ x ^ y = ~ x ^ (~ (x ^ z) ^ y). ~ x ^ (~ (x ^ y) ^ z) = ~ x ^ z. ~ x ^ (y ^ ~ (x ^ z)) = ~ x ^ y. ~ x ^ ~ (y v x) = ~ y ^ ~ x. ~ x ^ ~ y = ~ (x v y). ~ x ^ ~ (y v (x ^ z)) = ~ x ^ ~ y. ~ x ^ ~ y = ~ (x v (y v (x ^ z))). ~ (x v (y v (x ^ z))) = ~ x ^ ~ y. ~ (x v (y v (x ^ z))) = ~ (x v y). ~ ~ (x v y) = x v (y v (x ^ z)). x v (y v (x ^ z)) = ~ ~ (x v y). x v (y v (x ^ z)) = x v y. (x v y) v (z v x) = (x v y) v z. (x v y) v (z v y) = (x v y) v z. (x v y) v (x v z) = (x v y) v z. (x v y) v (y v z) = (x v y) v z. (x v y) v (x v z) = z v (x v y). x v (y v z) = (y v x) v (y v z). (x v y) v (x v z) = y v (x v z). (x v y) v (y v z) = x v (y v z). x v (y v z) = (x v y) v z. (x ^ (y v z)) v (x ^ y) = x ^ (y v z). (x ^ (y ^ z)) v (x ^ y) = x ^ y. (x ^ y) v (x ^ (y v z)) = x ^ (y v z). (x ^ y) v (x ^ (z v y)) = x ^ (z v y). (x ^ y) v (x ^ (z v (x ^ y))) = x ^ (z v (x ^ y)). (x v (y ^ z)) v (y ^ (z v x)) = x v (y ^ z). x ^ (y v (x ^ (y v z))) = x ^ (y v z). x v ((y ^ z) v (y ^ (z v x))) = x v (y ^ z). x v (y ^ (z v x)) = x v (y ^ z). x v (y ^ (x v z)) = x v (y ^ z). (x ^ y) v (x ^ z) = x ^ (z v (x ^ y)). x ^ (y v (x ^ z)) = x ^ (y v z). x ^ (y v (x ^ z)) = x ^ (z v y). 1 = (x => y) => ((x ^ z) => y). (x => y) => ((x ^ z) => y) = 1. ~ ~ x = 1 * x. 1 * x = x. 1 = (x ^ y) => (x v z). (x ^ y) => (x v z) = 1. x * ((x => y) * ~ y) = 0. (x v y) v x = x v y. (1 ^ 1) => ((x v (y ^ z)) => (y v x)) = 1. x v (x v y) = x v y. 1 = (x v (y ^ z)) => (y v x). (x v (y ^ z)) => (y v x) = 1. (x v (y ^ z)) * (1 * ~ (y v x)) = 0. (x v (y ^ z)) * ~ (y v x) = 0. (x v (y ^ z)) ^ (~ (y v x) => 0) = x v (y ^ z). (x v (y ^ z)) ^ (~ (x v y) => 0) = x v (y ^ z). (x v (y ^ z)) ^ ~ ~ (x v y) = x v (y ^ z). (x v (y ^ z)) ^ (x v y) = x v (y ^ z). x v (y ^ z) = (x v y) ^ (x v (y ^ z)). (x v y) ^ (x v (y ^ z)) = x v (y ^ z). (x v y) ^ (x v ((x v y) ^ z)) = x v ((x v y) ^ z). (x v y) ^ (x v (z ^ (x v y))) = x v ((x v y) ^ z). (x v y) ^ (x v (z ^ (x v y))) = x v (z ^ (x v y)). x ^ (y v (z ^ x)) = x ^ (y v z). (x v y) ^ (x v z) = x v (z ^ (x v y)). x v (y ^ (x v z)) = (x v z) ^ (x v y). (x v y) ^ (x v z) = x v (z ^ y). x v (y ^ z) = (x v y) ^ (x v z). (x => ~ y) ^ (y => z) = y => (~ x ^ z). (x => ~ y) ^ (y => z) = y => (z ^ ~ x). x ^ ~ y = ~ (~ x v y). ~ (~ x v y) = x ^ ~ y. ~ (x v ~ y) = y ^ ~ x. ~ (x ^ ~ y) = y v ~ x. ~ (x ^ (y => ~ z)) = (y * z) v ~ x. ~ (x => (~ y ^ ~ z)) = (x * y) v ~ (z => ~ x). (x * y) v ~ (z => ~ x) = ~ (x => (~ y ^ ~ z)). (x * y) v ~ (z => ~ x) = ~ (x => ~ (y v z)). (x * y) v ~ (z => ~ x) = x * (y v z). (x * y) v (x * z) = x * (y v z). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 2 (all x all y (x = 1 & y = 1 -> x ^ y = 1)) # label("(4)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 4 (x v y) v z = x v (y v z) # label("(D1)") # label(non_clause) # label(goal). [goal]. 5 (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)") # label(non_clause) # label(goal). [goal]. 6 x ^ x = x # label("(D3)") # label(non_clause) # label(goal). [goal]. 7 x v x = x # label("(D4)") # label(non_clause) # label(goal). [goal]. 8 x v y = y v x # label("(D5)") # label(non_clause) # label(goal). [goal]. 9 x ^ y = y ^ x # label("(D6)") # label(non_clause) # label(goal). [goal]. 10 x v (x ^ y) = x # label("(D7)") # label(non_clause) # label(goal). [goal]. 11 x ^ (x v y) = x # label("(D8)") # label(non_clause) # label(goal). [goal]. 12 x ^ 0 = 0 # label("(D9)") # label(non_clause) # label(goal). [goal]. 13 x ^ 1 = x # label("(D10)") # label(non_clause) # label(goal). [goal]. 14 x * 1 = x # label("(M1)") # label(non_clause) # label(goal). [goal]. 15 x * y = y * x # label("(M2)") # label(non_clause) # label(goal). [goal]. 16 (x * y) * z = x * (y * z) # label("(M3)") # label(non_clause) # label(goal). [goal]. 17 x * (y v z) = (x * y) v (x * z) # label("(R1)") # label(non_clause) # label(goal). [goal]. 18 x => (y ^ z) = (x => y) ^ (x => z) # label("(R2)") # label(non_clause) # label(goal). [goal]. 19 (x * (x => y)) v y = y # label("(R3)") # label(non_clause) # label(goal). [goal]. 20 (x => (x * y)) ^ y = y # label("(R4)") # label(non_clause) # label(goal). [goal]. 21 x => (x => (x => y)) = x => (x => y) # label("(E_2)") # label(non_clause) # label(goal). [goal]. 22 (x v y) ^ (x v z) = x v (y ^ z) # label("(D11)") # label(non_clause) # label(goal). [goal]. 23 (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D12)") # label(non_clause) # label(goal). [goal]. 24 ~ ~ x = x # label("(I)") # label(non_clause) # label(goal). [goal]. 25 (x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y # label("(N)") # 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 => ((x => y) => y) = 1 # label("(A1)[= 1]"). [assumption]. (x => y) => ((y => z) => (x => z)) = 1 # label("(A2)[= 1]"). [assumption]. (x ^ y) => x = 1 # label("(A3)[= 1]"). [assumption]. (x ^ y) => y = 1 # label("(A4)[= 1]"). [assumption]. ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]"). [assumption]. x => (x v y) = 1 # label("(A6)[= 1]"). [assumption]. x => (y v x) = 1 # label("(A7)[= 1]"). [assumption]. ((x => y) ^ (z => y)) => ((x v z) => y) = 1 # label("(A8)[= 1]"). [assumption]. (x ^ (y v z)) => ((x ^ y) v z) = 1 # label("(A9)[= 1]"). [assumption]. ~ ~ x => x = 1 # label("(A10)[= 1]"). [assumption]. (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). [assumption]. x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. ((x => (x => y)) ^ (~ y => (x => y))) => (x => y) = 1 # label("(A13)[= 1]"). [assumption]. x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. x != 1 | y != 1 | x ^ y = 1 # label("(4)"). [clausify(2)]. x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. x * y = ~ (x => ~ y) # label("(* def)"). [assumption]. 0 = ~ (x => x) # label("(0 def)"). [assumption]. 1 = x => x # label("(1 def)"). [assumption]. (c1 v c2) v c3 != c1 v (c2 v c3) # label("(D1)"). [deny(4)]. (c4 ^ c5) ^ c6 != c4 ^ (c5 ^ c6) # label("(D2)"). [deny(5)]. c7 ^ c7 != c7 # label("(D3)"). [deny(6)]. c8 v c8 != c8 # label("(D4)"). [deny(7)]. c10 v c9 != c9 v c10 # label("(D5)"). [deny(8)]. c12 ^ c11 != c11 ^ c12 # label("(D6)"). [deny(9)]. c13 v (c13 ^ c14) != c13 # label("(D7)"). [deny(10)]. c15 ^ (c15 v c16) != c15 # label("(D8)"). [deny(11)]. c17 ^ 0 != 0 # label("(D9)"). [deny(12)]. c18 ^ 1 != c18 # label("(D10)"). [deny(13)]. c19 * 1 != c19 # label("(M1)"). [deny(14)]. c21 * c20 != c20 * c21 # label("(M2)"). [deny(15)]. (c22 * c23) * c24 != c22 * (c23 * c24) # label("(M3)"). [deny(16)]. (c25 * c26) v (c25 * c27) != c25 * (c26 v c27) # label("(R1)"). [deny(17)]. c28 => (c29 ^ c30) != (c28 => c29) ^ (c28 => c30) # label("(R2)"). [deny(18)]. (c31 * (c31 => c32)) v c32 != c32 # label("(R3)"). [deny(19)]. (c33 => (c33 * c34)) ^ c34 != c34 # label("(R4)"). [deny(20)]. c35 => (c35 => (c35 => c36)) != c35 => (c35 => c36) # label("(E_2)"). [deny(21)]. c37 v (c38 ^ c39) != (c37 v c38) ^ (c37 v c39) # label("(D11)"). [deny(22)]. (c40 ^ c41) v (c40 ^ c42) != c40 ^ (c41 v c42) # label("(D12)"). [deny(23)]. ~ ~ c43 != c43 # label("(I)"). [deny(24)]. c44 => c45 != (c44 => (c44 => c45)) ^ (~ c45 => (~ c45 => ~ c44)) # label("(N)"). [deny(25)]. end_of_list. formulas(demodulators). end_of_list. % 338 hints input. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination =============  WARNING: denials share constants (see output). Auto_denials: % copying label "(D1)" to answer in negative clause % copying label "(D2)" to answer in negative clause % copying label "(D3)" to answer in negative clause % copying label "(D4)" to answer in negative clause % copying label "(D5)" to answer in negative clause % copying label "(D6)" to answer in negative clause % copying label "(D7)" to answer in negative clause % copying label "(D8)" to answer in negative clause % copying label "(D9)" to answer in negative clause % copying label "(D10)" to answer in negative clause % copying label "(M1)" to answer in negative clause % copying label "(M2)" to answer in negative clause % copying label "(M3)" to answer in negative clause % copying label "(R1)" to answer in negative clause % copying label "(R2)" to answer in negative clause % copying label "(R3)" to answer in negative clause % copying label "(R4)" to answer in negative clause % copying label "(E_2)" to answer in negative clause % copying label "(D11)" to answer in negative clause % copying label "(D12)" to answer in negative clause % copying label "(I)" to answer in negative clause % copying label "(N)" to answer in negative clause % assign(max_proofs, 22). % (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. c30=1. c31=1. c32=1. c33=1. c34=1. c35=1. c36=1. c37=1. c38=1. c39=1. c40=1. c41=1. c42=1. c43=1. c44=1. c45=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, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, *, ^, =>, 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) % set(hyper_resolution). % (nonunit Horn with equality) % set(hyper_resolution) -> set(pos_hyper_resolution). % set(neg_ur_resolution). % (nonunit Horn with equality) Auto_process settings: (no changes). kept: 26 x => ((x => y) => y) = 1 # label("(A1)[= 1]"). [assumption]. kept: 27 (x => y) => ((y => z) => (x => z)) = 1 # label("(A2)[= 1]"). [assumption]. kept: 28 (x ^ y) => x = 1 # label("(A3)[= 1]"). [assumption]. kept: 29 (x ^ y) => y = 1 # label("(A4)[= 1]"). [assumption]. kept: 30 ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]"). [assumption]. kept: 31 x => (x v y) = 1 # label("(A6)[= 1]"). [assumption]. kept: 32 x => (y v x) = 1 # label("(A7)[= 1]"). [assumption]. kept: 33 ((x => y) ^ (z => y)) => ((x v z) => y) = 1 # label("(A8)[= 1]"). [assumption]. kept: 34 (x ^ (y v z)) => ((x ^ y) v z) = 1 # label("(A9)[= 1]"). [assumption]. kept: 35 ~ ~ x => x = 1 # label("(A10)[= 1]"). [assumption]. kept: 36 (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). [assumption]. kept: 37 x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. kept: 38 ((x => (x => y)) ^ (~ y => (x => y))) => (x => y) = 1 # label("(A13)[= 1]"). [assumption]. 39 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. kept: 40 1 != x | x => y != 1 | 1 = y. [copy(39),flip(a),flip(c)]. 41 x != 1 | y != 1 | x ^ y = 1 # label("(4)"). [clausify(2)]. kept: 42 1 != x | 1 != y | x ^ y = 1. [copy(41),flip(a),flip(b)]. kept: 43 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 44 x * y = ~ (x => ~ y) # label("(* def)"). [assumption]. kept: 45 ~ (x => ~ y) = x * y. [copy(44),flip(a)]. 46 0 = ~ (x => x) # label("(0 def)"). [assumption]. kept: 47 ~ (x => x) = 0. [copy(46),flip(a)]. 48 1 = x => x # label("(1 def)"). [assumption]. kept: 49 x => x = 1. [copy(48),flip(a)]. kept: 50 (c1 v c2) v c3 != c1 v (c2 v c3) # label("(D1)") # answer("(D1)"). [deny(4)]. kept: 51 (c4 ^ c5) ^ c6 != c4 ^ (c5 ^ c6) # label("(D2)") # answer("(D2)"). [deny(5)]. kept: 52 c7 ^ c7 != c7 # label("(D3)") # answer("(D3)"). [deny(6)]. kept: 53 c8 v c8 != c8 # label("(D4)") # answer("(D4)"). [deny(7)]. kept: 54 c10 v c9 != c9 v c10 # label("(D5)") # answer("(D5)"). [deny(8)]. kept: 55 c12 ^ c11 != c11 ^ c12 # label("(D6)") # answer("(D6)"). [deny(9)]. kept: 56 c13 v (c13 ^ c14) != c13 # label("(D7)") # answer("(D7)"). [deny(10)]. kept: 57 c15 ^ (c15 v c16) != c15 # label("(D8)") # answer("(D8)"). [deny(11)]. kept: 58 c17 ^ 0 != 0 # label("(D9)") # answer("(D9)"). [deny(12)]. kept: 59 c18 ^ 1 != c18 # label("(D10)") # answer("(D10)"). [deny(13)]. kept: 60 c19 * 1 != c19 # label("(M1)") # answer("(M1)"). [deny(14)]. kept: 61 c21 * c20 != c20 * c21 # label("(M2)") # answer("(M2)"). [deny(15)]. kept: 62 (c22 * c23) * c24 != c22 * (c23 * c24) # label("(M3)") # answer("(M3)"). [deny(16)]. kept: 63 (c25 * c26) v (c25 * c27) != c25 * (c26 v c27) # label("(R1)") # answer("(R1)"). [deny(17)]. 64 c28 => (c29 ^ c30) != (c28 => c29) ^ (c28 => c30) # label("(R2)") # answer("(R2)"). [deny(18)]. kept: 65 (c28 => c29) ^ (c28 => c30) != c28 => (c29 ^ c30) # answer("(R2)"). [copy(64),flip(a)]. kept: 66 (c31 * (c31 => c32)) v c32 != c32 # label("(R3)") # answer("(R3)"). [deny(19)]. kept: 67 (c33 => (c33 * c34)) ^ c34 != c34 # label("(R4)") # answer("(R4)"). [deny(20)]. kept: 68 c35 => (c35 => (c35 => c36)) != c35 => (c35 => c36) # label("(E_2)") # answer("(E_2)"). [deny(21)]. 69 c37 v (c38 ^ c39) != (c37 v c38) ^ (c37 v c39) # label("(D11)") # answer("(D11)"). [deny(22)]. kept: 70 (c37 v c38) ^ (c37 v c39) != c37 v (c38 ^ c39) # answer("(D11)"). [copy(69),flip(a)]. kept: 71 (c40 ^ c41) v (c40 ^ c42) != c40 ^ (c41 v c42) # label("(D12)") # answer("(D12)"). [deny(23)]. kept: 72 ~ ~ c43 != c43 # label("(I)") # answer("(I)"). [deny(24)]. 73 c44 => c45 != (c44 => (c44 => c45)) ^ (~ c45 => (~ c45 => ~ c44)) # label("(N)") # answer("(N)"). [deny(25)]. kept: 74 (c44 => (c44 => c45)) ^ (~ c45 => (~ c45 => ~ c44)) != c44 => c45 # answer("(N)"). [copy(73),flip(a)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 50 (c1 v c2) v c3 != c1 v (c2 v c3) # label("(D1)") # answer("(D1)"). [deny(4)]. 51 (c4 ^ c5) ^ c6 != c4 ^ (c5 ^ c6) # label("(D2)") # answer("(D2)"). [deny(5)]. 52 c7 ^ c7 != c7 # label("(D3)") # answer("(D3)"). [deny(6)]. 53 c8 v c8 != c8 # label("(D4)") # answer("(D4)"). [deny(7)]. 54 c10 v c9 != c9 v c10 # label("(D5)") # answer("(D5)"). [deny(8)]. 55 c12 ^ c11 != c11 ^ c12 # label("(D6)") # answer("(D6)"). [deny(9)]. 56 c13 v (c13 ^ c14) != c13 # label("(D7)") # answer("(D7)"). [deny(10)]. 57 c15 ^ (c15 v c16) != c15 # label("(D8)") # answer("(D8)"). [deny(11)]. 58 c17 ^ 0 != 0 # label("(D9)") # answer("(D9)"). [deny(12)]. 59 c18 ^ 1 != c18 # label("(D10)") # answer("(D10)"). [deny(13)]. 60 c19 * 1 != c19 # label("(M1)") # answer("(M1)"). [deny(14)]. 61 c21 * c20 != c20 * c21 # label("(M2)") # answer("(M2)"). [deny(15)]. 62 (c22 * c23) * c24 != c22 * (c23 * c24) # label("(M3)") # answer("(M3)"). [deny(16)]. 63 (c25 * c26) v (c25 * c27) != c25 * (c26 v c27) # label("(R1)") # answer("(R1)"). [deny(17)]. 65 (c28 => c29) ^ (c28 => c30) != c28 => (c29 ^ c30) # answer("(R2)"). [copy(64),flip(a)]. 66 (c31 * (c31 => c32)) v c32 != c32 # label("(R3)") # answer("(R3)"). [deny(19)]. 67 (c33 => (c33 * c34)) ^ c34 != c34 # label("(R4)") # answer("(R4)"). [deny(20)]. 68 c35 => (c35 => (c35 => c36)) != c35 => (c35 => c36) # label("(E_2)") # answer("(E_2)"). [deny(21)]. 70 (c37 v c38) ^ (c37 v c39) != c37 v (c38 ^ c39) # answer("(D11)"). [copy(69),flip(a)]. 71 (c40 ^ c41) v (c40 ^ c42) != c40 ^ (c41 v c42) # label("(D12)") # answer("(D12)"). [deny(23)]. 72 ~ ~ c43 != c43 # label("(I)") # answer("(I)"). [deny(24)]. 74 (c44 => (c44 => c45)) ^ (~ c45 => (~ c45 => ~ c44)) != c44 => c45 # answer("(N)"). [copy(73),flip(a)]. end_of_list. formulas(sos). 26 x => ((x => y) => y) = 1 # label("(A1)[= 1]"). [assumption]. 27 (x => y) => ((y => z) => (x => z)) = 1 # label("(A2)[= 1]"). [assumption]. 28 (x ^ y) => x = 1 # label("(A3)[= 1]"). [assumption]. 29 (x ^ y) => y = 1 # label("(A4)[= 1]"). [assumption]. 30 ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]"). [assumption]. 31 x => (x v y) = 1 # label("(A6)[= 1]"). [assumption]. 32 x => (y v x) = 1 # label("(A7)[= 1]"). [assumption]. 33 ((x => y) ^ (z => y)) => ((x v z) => y) = 1 # label("(A8)[= 1]"). [assumption]. 34 (x ^ (y v z)) => ((x ^ y) v z) = 1 # label("(A9)[= 1]"). [assumption]. 35 ~ ~ x => x = 1 # label("(A10)[= 1]"). [assumption]. 36 (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). [assumption]. 37 x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. 38 ((x => (x => y)) ^ (~ y => (x => y))) => (x => y) = 1 # label("(A13)[= 1]"). [assumption]. 40 1 != x | x => y != 1 | 1 = y. [copy(39),flip(a),flip(c)]. 42 1 != x | 1 != y | x ^ y = 1. [copy(41),flip(a),flip(b)]. 43 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 45 ~ (x => ~ y) = x * y. [copy(44),flip(a)]. 47 ~ (x => x) = 0. [copy(46),flip(a)]. 49 x => x = 1. [copy(48),flip(a)]. end_of_list. formulas(demodulators). end_of_list. % 260 hints (338 processed, 78 redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.02 seconds. given #1 (I,wt=9): 26 x => ((x => y) => y) = 1 # label("(A1)[= 1]"). [assumption]. given #2 (I,wt=13): 27 (x => y) => ((y => z) => (x => z)) = 1 # label("(A2)[= 1]"). [assumption]. given #3 (I,wt=7): 28 (x ^ y) => x = 1 # label("(A3)[= 1]"). [assumption]. given #4 (I,wt=7): 29 (x ^ y) => y = 1 # label("(A4)[= 1]"). [assumption]. given #5 (I,wt=15): 30 ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]"). [assumption]. given #6 (I,wt=7): 31 x => (x v y) = 1 # label("(A6)[= 1]"). [assumption]. given #7 (I,wt=7): 32 x => (y v x) = 1 # label("(A7)[= 1]"). [assumption]. given #8 (I,wt=15): 33 ((x => y) ^ (z => y)) => ((x v z) => y) = 1 # label("(A8)[= 1]"). [assumption]. given #9 (I,wt=13): 34 (x ^ (y v z)) => ((x ^ y) v z) = 1 # label("(A9)[= 1]"). [assumption]. given #10 (I,wt=7): 35 ~ ~ x => x = 1 # label("(A10)[= 1]"). [assumption]. given #11 (I,wt=11): 36 (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). [assumption]. given #12 (I,wt=7): 37 x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. given #13 (I,wt=18): 38 ((x => (x => y)) ^ (~ y => (x => y))) => (x => y) = 1 # label("(A13)[= 1]"). [assumption]. given #14 (I,wt=11): 40 1 != x | x => y != 1 | 1 = y. [copy(39),flip(a),flip(c)]. given #15 (I,wt=11): 42 1 != x | 1 != y | x ^ y = 1. [copy(41),flip(a),flip(b)]. given #16 (I,wt=13): 43 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. given #17 (I,wt=9): 45 ~ (x => ~ y) = x * y. [copy(44),flip(a)]. given #18 (I,wt=6): 47 ~ (x => x) = 0. [copy(46),flip(a)]. given #19 (I,wt=5): 49 x => x = 1. [copy(48),flip(a)]. given #20 (H,wt=4): 595 ~ 1 = 0. [para(36(a,1),47(a,1,1))]. given #21 (H,wt=5): 252 x => 1 = 1. [para(28(a,1),37(a,1,2))]. given #22 (H,wt=7): 386 (1 => x) => x = 1. [hyper(40,a,xx,b,26,a),flip(a)]. given #23 (H,wt=5): 728 1 => x = x. [hyper(43,a,37,a,b,386,a)]. given #24 (H,wt=7): 630 x => ~ ~ x = 1. [hyper(40,a,49,a(flip),b,36,a),flip(a)]. -------- Proof 1 -------- "(I)". ============================== PROOF ================================= % Proof 1 at 0.05 (+ 0.00) seconds: "(I)". % Length of proof is 14. % Level of proof is 5. % Maximum clause weight is 13. % Given clauses 24. 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 24 ~ ~ x = x # label("(I)") # label(non_clause) # label(goal). [goal]. 35 ~ ~ x => x = 1 # label("(A10)[= 1]"). [assumption]. 36 (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). [assumption]. 39 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. 40 1 != x | x => y != 1 | 1 = y. [copy(39),flip(a),flip(c)]. 43 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 48 1 = x => x # label("(1 def)"). [assumption]. 49 x => x = 1. [copy(48),flip(a)]. 72 ~ ~ c43 != c43 # label("(I)") # answer("(I)"). [deny(24)]. 630 x => ~ ~ x = 1. [hyper(40,a,49,a(flip),b,36,a),flip(a)]. 861 ~ ~ x = x. [hyper(43,a,35,a,b,630,a),flip(a)]. 862 $F # answer("(I)"). [resolve(861,a,72,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 72 given #25 (H,wt=5): 861 ~ ~ x = x. [hyper(43,a,35,a,b,630,a),flip(a)]. given #26 (H,wt=7): 845 ~ ~ x = 1 * x. [para(728(a,1),45(a,1,1))]. given #27 (H,wt=5): 1100 1 * x = x. [para(845(a,1),861(a,1))]. given #28 (H,wt=9): 583 x => ~ y = y => ~ x. [hyper(43,a,36,a,b,36,a)]. given #29 (H,wt=7): 1281 x => ~ 1 = ~ x. [para(583(a,1),728(a,1))]. given #30 (H,wt=6): 1326 x => 0 = ~ x. [para(595(a,1),1281(a,1,2))]. given #31 (H,wt=6): 1343 ~ (0 ^ x) = 1. [para(1326(a,1),28(a,1))]. given #32 (H,wt=6): 1448 0 ^ x = ~ 1. [para(1343(a,1),861(a,1,1)),flip(a)]. given #33 (H,wt=5): 1479 0 ^ x = 0. [para(1448(a,2),595(a,1))]. given #34 (H,wt=5): 1496 0 => x = 1. [para(1479(a,1),29(a,1,1))]. -------- Proof 2 -------- "(D9)". ============================== PROOF ================================= % Proof 2 at 0.06 (+ 0.00) seconds: "(D9)". % Length of proof is 31. % Level of proof is 12. % Maximum clause weight is 13. % Given clauses 34. 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 12 x ^ 0 = 0 # label("(D9)") # label(non_clause) # label(goal). [goal]. 26 x => ((x => y) => y) = 1 # label("(A1)[= 1]"). [assumption]. 28 (x ^ y) => x = 1 # label("(A3)[= 1]"). [assumption]. 29 (x ^ y) => y = 1 # label("(A4)[= 1]"). [assumption]. 35 ~ ~ x => x = 1 # label("(A10)[= 1]"). [assumption]. 36 (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). [assumption]. 37 x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. 39 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. 40 1 != x | x => y != 1 | 1 = y. [copy(39),flip(a),flip(c)]. 43 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 46 0 = ~ (x => x) # label("(0 def)"). [assumption]. 47 ~ (x => x) = 0. [copy(46),flip(a)]. 48 1 = x => x # label("(1 def)"). [assumption]. 49 x => x = 1. [copy(48),flip(a)]. 58 c17 ^ 0 != 0 # label("(D9)") # answer("(D9)"). [deny(12)]. 386 (1 => x) => x = 1. [hyper(40,a,xx,b,26,a),flip(a)]. 583 x => ~ y = y => ~ x. [hyper(43,a,36,a,b,36,a)]. 595 ~ 1 = 0. [para(36(a,1),47(a,1,1))]. 630 x => ~ ~ x = 1. [hyper(40,a,49,a(flip),b,36,a),flip(a)]. 728 1 => x = x. [hyper(43,a,37,a,b,386,a)]. 861 ~ ~ x = x. [hyper(43,a,35,a,b,630,a),flip(a)]. 1281 x => ~ 1 = ~ x. [para(583(a,1),728(a,1))]. 1326 x => 0 = ~ x. [para(595(a,1),1281(a,1,2))]. 1343 ~ (0 ^ x) = 1. [para(1326(a,1),28(a,1))]. 1448 0 ^ x = ~ 1. [para(1343(a,1),861(a,1,1)),flip(a)]. 1479 0 ^ x = 0. [para(1448(a,2),595(a,1))]. 1496 0 => x = 1. [para(1479(a,1),29(a,1,1))]. 1506 x ^ 0 = 0. [hyper(43,a,29,a,b,1496,a),flip(a)]. 1507 $F # answer("(D9)"). [resolve(1506,a,58,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 58 given #35 (H,wt=5): 1506 x ^ 0 = 0. [hyper(43,a,29,a,b,1496,a),flip(a)]. given #36 (H,wt=7): 1321 ~ ~ x = x * 1. [para(1281(a,1),45(a,1,1))]. -------- Proof 3 -------- "(M1)". ============================== PROOF ================================= % Proof 3 at 0.07 (+ 0.00) seconds: "(M1)". % Length of proof is 24. % Level of proof is 8. % Maximum clause weight is 13. % Given clauses 36. 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 14 x * 1 = x # label("(M1)") # label(non_clause) # label(goal). [goal]. 26 x => ((x => y) => y) = 1 # label("(A1)[= 1]"). [assumption]. 35 ~ ~ x => x = 1 # label("(A10)[= 1]"). [assumption]. 36 (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). [assumption]. 37 x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. 39 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. 40 1 != x | x => y != 1 | 1 = y. [copy(39),flip(a),flip(c)]. 43 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 44 x * y = ~ (x => ~ y) # label("(* def)"). [assumption]. 45 ~ (x => ~ y) = x * y. [copy(44),flip(a)]. 48 1 = x => x # label("(1 def)"). [assumption]. 49 x => x = 1. [copy(48),flip(a)]. 60 c19 * 1 != c19 # label("(M1)") # answer("(M1)"). [deny(14)]. 386 (1 => x) => x = 1. [hyper(40,a,xx,b,26,a),flip(a)]. 583 x => ~ y = y => ~ x. [hyper(43,a,36,a,b,36,a)]. 630 x => ~ ~ x = 1. [hyper(40,a,49,a(flip),b,36,a),flip(a)]. 728 1 => x = x. [hyper(43,a,37,a,b,386,a)]. 861 ~ ~ x = x. [hyper(43,a,35,a,b,630,a),flip(a)]. 1281 x => ~ 1 = ~ x. [para(583(a,1),728(a,1))]. 1321 ~ ~ x = x * 1. [para(1281(a,1),45(a,1,1))]. 1640 x * 1 = x. [para(1321(a,1),861(a,1))]. 1641 $F # answer("(M1)"). [resolve(1640,a,60,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 60 given #37 (H,wt=5): 1640 x * 1 = x. [para(1321(a,1),861(a,1))]. given #38 (H,wt=9): 600 (x => x) ^ (y => y) = 1. [hyper(42,a,49,a(flip),b,49,a(flip))]. given #39 (H,wt=7): 1805 (x v x) => x = 1. [hyper(40,a,600,a(flip),b,33,a),flip(a)]. -------- Proof 4 -------- "(D4)". ============================== PROOF ================================= % Proof 4 at 0.08 (+ 0.00) seconds: "(D4)". % Length of proof is 18. % Level of proof is 6. % Maximum clause weight is 15. % Given clauses 39. 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 2 (all x all y (x = 1 & y = 1 -> x ^ y = 1)) # label("(4)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 7 x v x = x # label("(D4)") # label(non_clause) # label(goal). [goal]. 32 x => (y v x) = 1 # label("(A7)[= 1]"). [assumption]. 33 ((x => y) ^ (z => y)) => ((x v z) => y) = 1 # label("(A8)[= 1]"). [assumption]. 39 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. 40 1 != x | x => y != 1 | 1 = y. [copy(39),flip(a),flip(c)]. 41 x != 1 | y != 1 | x ^ y = 1 # label("(4)"). [clausify(2)]. 42 1 != x | 1 != y | x ^ y = 1. [copy(41),flip(a),flip(b)]. 43 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 48 1 = x => x # label("(1 def)"). [assumption]. 49 x => x = 1. [copy(48),flip(a)]. 53 c8 v c8 != c8 # label("(D4)") # answer("(D4)"). [deny(7)]. 600 (x => x) ^ (y => y) = 1. [hyper(42,a,49,a(flip),b,49,a(flip))]. 1805 (x v x) => x = 1. [hyper(40,a,600,a(flip),b,33,a),flip(a)]. 1852 x v x = x. [hyper(43,a,32,a,b,1805,a)]. 1853 $F # answer("(D4)"). [resolve(1852,a,53,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 53 given #40 (H,wt=5): 1852 x v x = x. [hyper(43,a,32,a,b,1805,a)]. given #41 (H,wt=7): 1808 x => (x ^ x) = 1. [hyper(40,a,600,a(flip),b,30,a),flip(a)]. -------- Proof 5 -------- "(D3)". ============================== PROOF ================================= % Proof 5 at 0.08 (+ 0.00) seconds: "(D3)". % Length of proof is 18. % Level of proof is 6. % Maximum clause weight is 15. % Given clauses 41. 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 2 (all x all y (x = 1 & y = 1 -> x ^ y = 1)) # label("(4)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 6 x ^ x = x # label("(D3)") # label(non_clause) # label(goal). [goal]. 29 (x ^ y) => y = 1 # label("(A4)[= 1]"). [assumption]. 30 ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]"). [assumption]. 39 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. 40 1 != x | x => y != 1 | 1 = y. [copy(39),flip(a),flip(c)]. 41 x != 1 | y != 1 | x ^ y = 1 # label("(4)"). [clausify(2)]. 42 1 != x | 1 != y | x ^ y = 1. [copy(41),flip(a),flip(b)]. 43 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 48 1 = x => x # label("(1 def)"). [assumption]. 49 x => x = 1. [copy(48),flip(a)]. 52 c7 ^ c7 != c7 # label("(D3)") # answer("(D3)"). [deny(6)]. 600 (x => x) ^ (y => y) = 1. [hyper(42,a,49,a(flip),b,49,a(flip))]. 1808 x => (x ^ x) = 1. [hyper(40,a,600,a(flip),b,30,a),flip(a)]. 2124 x ^ x = x. [hyper(43,a,29,a,b,1808,a),flip(a)]. 2125 $F # answer("(D3)"). [resolve(2124,a,52,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 52 given #42 (H,wt=5): 2124 x ^ x = x. [hyper(43,a,29,a,b,1808,a),flip(a)]. given #43 (H,wt=9): 674 (x => x) ^ (y => 1) = 1. [hyper(42,a,49,a(flip),b,252,a(flip))]. given #44 (H,wt=7): 2448 x => (x ^ 1) = 1. [hyper(40,a,674,a(flip),b,30,a),flip(a)]. -------- Proof 6 -------- "(D10)". ============================== PROOF ================================= % Proof 6 at 0.10 (+ 0.00) seconds: "(D10)". % Length of proof is 20. % Level of proof is 6. % Maximum clause weight is 15. % Given clauses 44. 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 2 (all x all y (x = 1 & y = 1 -> x ^ y = 1)) # label("(4)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 13 x ^ 1 = x # label("(D10)") # label(non_clause) # label(goal). [goal]. 28 (x ^ y) => x = 1 # label("(A3)[= 1]"). [assumption]. 30 ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]"). [assumption]. 37 x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. 39 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. 40 1 != x | x => y != 1 | 1 = y. [copy(39),flip(a),flip(c)]. 41 x != 1 | y != 1 | x ^ y = 1 # label("(4)"). [clausify(2)]. 42 1 != x | 1 != y | x ^ y = 1. [copy(41),flip(a),flip(b)]. 43 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 48 1 = x => x # label("(1 def)"). [assumption]. 49 x => x = 1. [copy(48),flip(a)]. 59 c18 ^ 1 != c18 # label("(D10)") # answer("(D10)"). [deny(13)]. 252 x => 1 = 1. [para(28(a,1),37(a,1,2))]. 674 (x => x) ^ (y => 1) = 1. [hyper(42,a,49,a(flip),b,252,a(flip))]. 2448 x => (x ^ 1) = 1. [hyper(40,a,674,a(flip),b,30,a),flip(a)]. 2521 x ^ 1 = x. [hyper(43,a,28,a,b,2448,a),flip(a)]. 2522 $F # answer("(D10)"). [resolve(2521,a,59,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 59 given #45 (H,wt=5): 2521 x ^ 1 = x. [hyper(43,a,28,a,b,2448,a),flip(a)]. given #46 (H,wt=9): 1017 x => ~ ~ (y v x) = 1. [para(861(a,2),32(a,1,2))]. given #47 (H,wt=9): 1050 ~ (x => y) = x * ~ y. [para(861(a,1),45(a,1,1,2))]. given #48 (H,wt=9): 1054 ~ (x * y) = x => ~ y. [para(45(a,1),861(a,1,1))]. given #49 (H,wt=9): 1277 ~ (x => ~ y) = y * x. [para(583(a,1),45(a,1,1))]. % Operation * is commutative; C redundancy checks enabled. -------- Proof 7 -------- "(M2)". ============================== PROOF ================================= % Proof 7 at 0.11 (+ 0.00) seconds: "(M2)". % Length of proof is 11. % Level of proof is 5. % Maximum clause weight is 13. % Given clauses 49. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 15 x * y = y * x # label("(M2)") # label(non_clause) # label(goal). [goal]. 36 (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). [assumption]. 43 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 44 x * y = ~ (x => ~ y) # label("(* def)"). [assumption]. 45 ~ (x => ~ y) = x * y. [copy(44),flip(a)]. 61 c21 * c20 != c20 * c21 # label("(M2)") # answer("(M2)"). [deny(15)]. 583 x => ~ y = y => ~ x. [hyper(43,a,36,a,b,36,a)]. 1277 ~ (x => ~ y) = y * x. [para(583(a,1),45(a,1,1))]. 3064 x * y = y * x. [para(1277(a,1),45(a,1))]. 3065 $F # answer("(M2)"). [resolve(3064,a,61,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 61 given #50 (H,wt=7): 3064 x * y = y * x. [para(1277(a,1),45(a,1))]. given #51 (H,wt=9): 1283 ~ x => ~ y = y => x. [para(861(a,1),583(a,1,2)),flip(a)]. given #52 (H,wt=9): 2860 ~ (x v y) => ~ y = 1. [hyper(40,a,1017,a(flip),b,36,a),flip(a)]. given #53 (H,wt=9): 2934 (x ^ y) * ~ x = ~ 1. [para(28(a,1),1050(a,1,1)),flip(a)]. given #54 (H,wt=8): 3369 (x ^ y) * ~ x = 0. [para(2934(a,2),595(a,1))]. given #55 (H,wt=9): 2935 (x ^ y) * ~ y = ~ 1. [para(29(a,1),1050(a,1,1)),flip(a)]. given #56 (H,wt=8): 3491 (x ^ y) * ~ y = 0. [para(2935(a,2),595(a,1))]. given #57 (H,wt=8): 3596 ~ x * (y ^ x) = 0. [para(3491(a,1),3064(a,1)),flip(a)]. given #58 (H,wt=9): 3031 ~ (x * y) = y => ~ x. [para(1054(a,2),583(a,1))]. given #59 (H,wt=11): 366 (x => y) => ((z ^ x) => y) = 1. [hyper(40,a,29,a(flip),b,27,a),flip(a)]. given #60 (H,wt=9): 3730 (x ^ y) => (z => y) = 1. [hyper(40,a,37,a(flip),b,366,a),flip(a)]. given #61 (H,wt=9): 3736 (x ^ y) => (y v z) = 1. [hyper(40,a,31,a(flip),b,366,a),flip(a)]. given #62 (H,wt=9): 3739 (x ^ (y ^ z)) => y = 1. [hyper(40,a,28,a(flip),b,366,a),flip(a)]. given #63 (H,wt=11): 372 (x => y) => ((x ^ z) => y) = 1. [hyper(40,a,28,a(flip),b,27,a),flip(a)]. given #64 (H,wt=9): 4381 (x ^ y) => (x v z) = 1. [hyper(40,a,31,a(flip),b,372,a),flip(a)]. given #65 (H,wt=11): 622 (x => x) ^ (y => (y v z)) = 1. [hyper(42,a,49,a(flip),b,31,a(flip))]. given #66 (H,wt=9): 4812 x => (x ^ (x v y)) = 1. [hyper(40,a,622,a(flip),b,30,a),flip(a)]. -------- Proof 8 -------- "(D8)". ============================== PROOF ================================= % Proof 8 at 0.19 (+ 0.00) seconds: "(D8)". % Length of proof is 19. % Level of proof is 6. % Maximum clause weight is 15. % Given clauses 66. 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 2 (all x all y (x = 1 & y = 1 -> x ^ y = 1)) # label("(4)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 11 x ^ (x v y) = x # label("(D8)") # label(non_clause) # label(goal). [goal]. 28 (x ^ y) => x = 1 # label("(A3)[= 1]"). [assumption]. 30 ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]"). [assumption]. 31 x => (x v y) = 1 # label("(A6)[= 1]"). [assumption]. 39 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. 40 1 != x | x => y != 1 | 1 = y. [copy(39),flip(a),flip(c)]. 41 x != 1 | y != 1 | x ^ y = 1 # label("(4)"). [clausify(2)]. 42 1 != x | 1 != y | x ^ y = 1. [copy(41),flip(a),flip(b)]. 43 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 48 1 = x => x # label("(1 def)"). [assumption]. 49 x => x = 1. [copy(48),flip(a)]. 57 c15 ^ (c15 v c16) != c15 # label("(D8)") # answer("(D8)"). [deny(11)]. 622 (x => x) ^ (y => (y v z)) = 1. [hyper(42,a,49,a(flip),b,31,a(flip))]. 4812 x => (x ^ (x v y)) = 1. [hyper(40,a,622,a(flip),b,30,a),flip(a)]. 4893 x ^ (x v y) = x. [hyper(43,a,28,a,b,4812,a),flip(a)]. 4894 $F # answer("(D8)"). [resolve(4893,a,57,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 57 given #67 (H,wt=7): 4893 x ^ (x v y) = x. [hyper(43,a,28,a,b,4812,a),flip(a)]. given #68 (H,wt=8): 5322 x * ~ (x v y) = 0. [para(4893(a,1),3491(a,1,1))]. given #69 (H,wt=11): 625 (x => x) ^ ((y ^ z) => y) = 1. [hyper(42,a,49,a(flip),b,28,a(flip))]. given #70 (H,wt=9): 5480 (x v (x ^ y)) => x = 1. [hyper(40,a,625,a(flip),b,33,a),flip(a)]. -------- Proof 9 -------- "(D7)". ============================== PROOF ================================= % Proof 9 at 0.22 (+ 0.00) seconds: "(D7)". % Length of proof is 19. % Level of proof is 6. % Maximum clause weight is 15. % Given clauses 70. 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 2 (all x all y (x = 1 & y = 1 -> x ^ y = 1)) # label("(4)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 10 x v (x ^ y) = x # label("(D7)") # label(non_clause) # label(goal). [goal]. 28 (x ^ y) => x = 1 # label("(A3)[= 1]"). [assumption]. 31 x => (x v y) = 1 # label("(A6)[= 1]"). [assumption]. 33 ((x => y) ^ (z => y)) => ((x v z) => y) = 1 # label("(A8)[= 1]"). [assumption]. 39 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. 40 1 != x | x => y != 1 | 1 = y. [copy(39),flip(a),flip(c)]. 41 x != 1 | y != 1 | x ^ y = 1 # label("(4)"). [clausify(2)]. 42 1 != x | 1 != y | x ^ y = 1. [copy(41),flip(a),flip(b)]. 43 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 48 1 = x => x # label("(1 def)"). [assumption]. 49 x => x = 1. [copy(48),flip(a)]. 56 c13 v (c13 ^ c14) != c13 # label("(D7)") # answer("(D7)"). [deny(10)]. 625 (x => x) ^ ((y ^ z) => y) = 1. [hyper(42,a,49,a(flip),b,28,a(flip))]. 5480 (x v (x ^ y)) => x = 1. [hyper(40,a,625,a(flip),b,33,a),flip(a)]. 5572 x v (x ^ y) = x. [hyper(43,a,31,a,b,5480,a)]. 5573 $F # answer("(D7)"). [resolve(5572,a,56,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 56 given #71 (H,wt=7): 5572 x v (x ^ y) = x. [hyper(43,a,31,a,b,5480,a)]. given #72 (H,wt=11): 1263 x => ((y => ~ x) => ~ y) = 1. [para(583(a,1),26(a,1,2,1))]. given #73 (H,wt=11): 1264 x => (y => ~ (x => ~ y)) = 1. [para(583(a,1),26(a,1,2))]. given #74 (H,wt=9): 6588 x => (y => (y * x)) = 1. [para(1277(a,1),1264(a,1,2,2))]. given #75 (H,wt=11): 2932 x * ~ ((x => y) => y) = ~ 1. [para(26(a,1),1050(a,1,1)),flip(a)]. given #76 (H,wt=10): 6888 x * ~ ((x => y) => y) = 0. [para(2932(a,2),595(a,1))]. given #77 (H,wt=10): 7068 x * ((x => y) * ~ y) = 0. [para(1050(a,1),6888(a,1,2))]. given #78 (H,wt=10): 7073 x * (y * (x => ~ y)) = 0. [para(1277(a,1),6888(a,1,2))]. given #79 (H,wt=10): 7267 ~ (x v y) * (y * 1) = 0. [para(2860(a,1),7073(a,1,2,2))]. given #80 (H,wt=8): 7336 ~ (x v y) * y = 0. [para(1640(a,1),7267(a,1,2))]. given #81 (H,wt=8): 7422 x * ~ (y v x) = 0. [para(7336(a,1),3064(a,1)),flip(a)]. given #82 (H,wt=11): 6326 x => ~ (y * (y => ~ x)) = 1. [para(3031(a,2),1263(a,1,2))]. given #83 (H,wt=11): 7667 ~ x => ~ (y * (y => x)) = 1. [para(861(a,1),6326(a,1,2,1,2,2))]. given #84 (H,wt=9): 7991 (x * (x => y)) => y = 1. [para(7667(a,1),1283(a,1)),flip(a)]. given #85 (H,wt=13): 90 (x => (y ^ z)) => (1 => (x => y)) = 1. [para(28(a,1),27(a,1,2,1))]. given #86 (H,wt=11): 8436 (x => (y ^ z)) => (x => y) = 1. [para(728(a,1),90(a,1,2))]. given #87 (H,wt=13): 97 (x => (y ^ z)) => (1 => (x => z)) = 1. [para(29(a,1),27(a,1,2,1))]. given #88 (H,wt=11): 8959 (x => (y ^ z)) => (x => z) = 1. [para(728(a,1),97(a,1,2))]. given #89 (H,wt=13): 382 (((x => y) => y) => z) => (x => z) = 1. [hyper(40,a,26,a(flip),b,27,a),flip(a)]. given #90 (H,wt=13): 640 ((x => y) ^ 1) => (x => (y ^ x)) = 1. [para(49(a,1),30(a,1,1,2))]. given #91 (H,wt=11): 9898 (x => y) => (x => (y ^ x)) = 1. [para(2521(a,1),640(a,1,1))]. given #92 (H,wt=9): 10031 x => ((y => x) ^ x) = 1. [hyper(40,a,37,a(flip),b,9898,a),flip(a)]. given #93 (H,wt=7): 10326 (x => y) ^ y = y. [hyper(43,a,29,a,b,10031,a),flip(a)]. given #94 (H,wt=5): 10753 1 ^ x = x. [para(28(a,1),10326(a,1,1))]. given #95 (H,wt=9): 10037 x => ((x v y) ^ x) = 1. [hyper(40,a,31,a(flip),b,9898,a),flip(a)]. given #96 (H,wt=7): 11287 (x v y) ^ x = x. [hyper(43,a,29,a,b,10037,a),flip(a)]. Low Water (keep): wt=27.000, iters=6781 Low Water (keep): wt=25.000, iters=6714 given #97 (H,wt=9): 11894 (x v y) v x = x v y. [para(11287(a,1),5572(a,1,2))]. given #98 (H,wt=11): 10006 x => ((y => (y * x)) ^ x) = 1. [hyper(40,a,6588,a(flip),b,9898,a),flip(a)]. -------- Proof 10 -------- "(R4)". ============================== PROOF ================================= % Proof 10 at 0.50 (+ 0.00) seconds: "(R4)". % Length of proof is 33. % Level of proof is 9. % Maximum clause weight is 15. % Given clauses 98. 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 2 (all x all y (x = 1 & y = 1 -> x ^ y = 1)) # label("(4)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 20 (x => (x * y)) ^ y = y # label("(R4)") # label(non_clause) # label(goal). [goal]. 26 x => ((x => y) => y) = 1 # label("(A1)[= 1]"). [assumption]. 28 (x ^ y) => x = 1 # label("(A3)[= 1]"). [assumption]. 29 (x ^ y) => y = 1 # label("(A4)[= 1]"). [assumption]. 30 ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]"). [assumption]. 36 (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). [assumption]. 37 x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. 39 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. 40 1 != x | x => y != 1 | 1 = y. [copy(39),flip(a),flip(c)]. 41 x != 1 | y != 1 | x ^ y = 1 # label("(4)"). [clausify(2)]. 42 1 != x | 1 != y | x ^ y = 1. [copy(41),flip(a),flip(b)]. 43 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 44 x * y = ~ (x => ~ y) # label("(* def)"). [assumption]. 45 ~ (x => ~ y) = x * y. [copy(44),flip(a)]. 48 1 = x => x # label("(1 def)"). [assumption]. 49 x => x = 1. [copy(48),flip(a)]. 67 (c33 => (c33 * c34)) ^ c34 != c34 # label("(R4)") # answer("(R4)"). [deny(20)]. 252 x => 1 = 1. [para(28(a,1),37(a,1,2))]. 583 x => ~ y = y => ~ x. [hyper(43,a,36,a,b,36,a)]. 640 ((x => y) ^ 1) => (x => (y ^ x)) = 1. [para(49(a,1),30(a,1,1,2))]. 674 (x => x) ^ (y => 1) = 1. [hyper(42,a,49,a(flip),b,252,a(flip))]. 1264 x => (y => ~ (x => ~ y)) = 1. [para(583(a,1),26(a,1,2))]. 1277 ~ (x => ~ y) = y * x. [para(583(a,1),45(a,1,1))]. 2448 x => (x ^ 1) = 1. [hyper(40,a,674,a(flip),b,30,a),flip(a)]. 2521 x ^ 1 = x. [hyper(43,a,28,a,b,2448,a),flip(a)]. 6588 x => (y => (y * x)) = 1. [para(1277(a,1),1264(a,1,2,2))]. 9898 (x => y) => (x => (y ^ x)) = 1. [para(2521(a,1),640(a,1,1))]. 10006 x => ((y => (y * x)) ^ x) = 1. [hyper(40,a,6588,a(flip),b,9898,a),flip(a)]. 12015 (x => (x * y)) ^ y = y. [hyper(43,a,29,a,b,10006,a),flip(a)]. 12016 $F # answer("(R4)"). [resolve(12015,a,67,a)]. ============================== end of proof ========================== Low Water (keep): wt=23.000, iters=6845 % Disable descendants (x means already disabled): 67 given #99 (H,wt=9): 12015 (x => (x * y)) ^ y = y. [hyper(43,a,29,a,b,10006,a),flip(a)]. Low Water (keep): wt=21.000, iters=6772 given #100 (H,wt=9): 12549 (x => (y * x)) ^ y = y. [para(3064(a,1),12015(a,1,1,2))]. given #101 (H,wt=11): 10040 (x ^ y) => (x ^ (x ^ y)) = 1. [hyper(40,a,28,a(flip),b,9898,a),flip(a)]. Low Water (keep): wt=19.000, iters=6747 given #102 (H,wt=9): 13097 x ^ (x ^ y) = x ^ y. [hyper(43,a,29,a,b,10040,a),flip(a)]. given #103 (H,wt=11): 10042 x => (((x => y) => y) ^ x) = 1. [hyper(40,a,26,a(flip),b,9898,a),flip(a)]. given #104 (H,wt=12): 12578 (~ x => 0) ^ (y ^ x) = y ^ x. [para(3596(a,1),12015(a,1,1,2))]. given #105 (H,wt=11): 13528 ~ ~ x ^ (y ^ x) = y ^ x. [para(1326(a,1),12578(a,1,1))]. given #106 (H,wt=9): 13639 x ^ (y ^ x) = y ^ x. [para(861(a,1),13528(a,1,1))]. given #107 (H,wt=7): 13776 x v (y ^ x) = x. [para(13639(a,1),5572(a,1,2))]. given #108 (H,wt=13): 645 ((x => y) ^ 1) => ((x v y) => y) = 1. [para(49(a,1),33(a,1,1,2))]. given #109 (H,wt=11): 14367 (x => y) => ((x v y) => y) = 1. [para(2521(a,1),645(a,1,1))]. Low Water (keep): wt=18.000, iters=6753 given #110 (H,wt=11): 14410 ((x * (x => y)) v y) => y = 1. [hyper(40,a,7991,a(flip),b,14367,a),flip(a)]. -------- Proof 11 -------- "(R3)". ============================== PROOF ================================= % Proof 11 at 0.62 (+ 0.00) seconds: "(R3)". % Length of proof is 41. % Level of proof is 12. % Maximum clause weight is 15. % Given clauses 110. 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 2 (all x all y (x = 1 & y = 1 -> x ^ y = 1)) # label("(4)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 19 (x * (x => y)) v y = y # label("(R3)") # label(non_clause) # label(goal). [goal]. 26 x => ((x => y) => y) = 1 # label("(A1)[= 1]"). [assumption]. 28 (x ^ y) => x = 1 # label("(A3)[= 1]"). [assumption]. 30 ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]"). [assumption]. 32 x => (y v x) = 1 # label("(A7)[= 1]"). [assumption]. 33 ((x => y) ^ (z => y)) => ((x v z) => y) = 1 # label("(A8)[= 1]"). [assumption]. 35 ~ ~ x => x = 1 # label("(A10)[= 1]"). [assumption]. 36 (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). [assumption]. 37 x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. 39 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. 40 1 != x | x => y != 1 | 1 = y. [copy(39),flip(a),flip(c)]. 41 x != 1 | y != 1 | x ^ y = 1 # label("(4)"). [clausify(2)]. 42 1 != x | 1 != y | x ^ y = 1. [copy(41),flip(a),flip(b)]. 43 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 44 x * y = ~ (x => ~ y) # label("(* def)"). [assumption]. 45 ~ (x => ~ y) = x * y. [copy(44),flip(a)]. 48 1 = x => x # label("(1 def)"). [assumption]. 49 x => x = 1. [copy(48),flip(a)]. 66 (c31 * (c31 => c32)) v c32 != c32 # label("(R3)") # answer("(R3)"). [deny(19)]. 252 x => 1 = 1. [para(28(a,1),37(a,1,2))]. 583 x => ~ y = y => ~ x. [hyper(43,a,36,a,b,36,a)]. 630 x => ~ ~ x = 1. [hyper(40,a,49,a(flip),b,36,a),flip(a)]. 645 ((x => y) ^ 1) => ((x v y) => y) = 1. [para(49(a,1),33(a,1,1,2))]. 674 (x => x) ^ (y => 1) = 1. [hyper(42,a,49,a(flip),b,252,a(flip))]. 861 ~ ~ x = x. [hyper(43,a,35,a,b,630,a),flip(a)]. 1054 ~ (x * y) = x => ~ y. [para(45(a,1),861(a,1,1))]. 1263 x => ((y => ~ x) => ~ y) = 1. [para(583(a,1),26(a,1,2,1))]. 1283 ~ x => ~ y = y => x. [para(861(a,1),583(a,1,2)),flip(a)]. 2448 x => (x ^ 1) = 1. [hyper(40,a,674,a(flip),b,30,a),flip(a)]. 2521 x ^ 1 = x. [hyper(43,a,28,a,b,2448,a),flip(a)]. 3031 ~ (x * y) = y => ~ x. [para(1054(a,2),583(a,1))]. 6326 x => ~ (y * (y => ~ x)) = 1. [para(3031(a,2),1263(a,1,2))]. 7667 ~ x => ~ (y * (y => x)) = 1. [para(861(a,1),6326(a,1,2,1,2,2))]. 7991 (x * (x => y)) => y = 1. [para(7667(a,1),1283(a,1)),flip(a)]. 14367 (x => y) => ((x v y) => y) = 1. [para(2521(a,1),645(a,1,1))]. 14410 ((x * (x => y)) v y) => y = 1. [hyper(40,a,7991,a(flip),b,14367,a),flip(a)]. 14629 (x * (x => y)) v y = y. [hyper(43,a,32,a,b,14410,a)]. 14630 $F # answer("(R3)"). [resolve(14629,a,66,a)]. ============================== end of proof ========================== Low Water (keep): wt=17.000, iters=6775 % Disable descendants (x means already disabled): 66 given #111 (H,wt=9): 14629 (x * (x => y)) v y = y. [hyper(43,a,32,a,b,14410,a)]. given #112 (H,wt=13): 3197 ~ x => (y => ~ z) = (y * z) => x. [para(1054(a,1),1283(a,1,2))]. given #113 (H,wt=13): 12606 (x => 0) ^ ~ (x v y) = ~ (x v y). [para(5322(a,1),12015(a,1,1,2))]. given #114 (H,wt=12): 15170 ~ x ^ ~ (x v y) = ~ (x v y). [para(1326(a,1),12606(a,1,1))]. given #115 (H,wt=13): 14979 (x * (x => y)) ^ y = x * (x => y). [para(14629(a,1),4893(a,1,2))]. given #116 (H,wt=9): 15370 x v (y * (y => x)) = x. [para(14979(a,1),13776(a,1,2))]. given #117 (H,wt=14): 1347 (~ x ^ (y => 0)) => ((x v y) => 0) = 1. [para(1326(a,1),33(a,1,1,1))]. given #118 (H,wt=13): 15670 (~ x ^ ~ y) => ((x v y) => 0) = 1. [para(1326(a,1),1347(a,1,1,2))]. given #119 (H,wt=12): 15750 (~ x ^ ~ y) => ~ (x v y) = 1. [para(1326(a,1),15670(a,1,2))]. given #120 (H,wt=12): 15901 (x v y) * (~ x ^ ~ y) = ~ 1. [para(15750(a,1),1277(a,1,1)),flip(a)]. given #121 (H,wt=11): 15944 (x v y) * (~ x ^ ~ y) = 0. [para(15901(a,2),595(a,1))]. given #122 (H,wt=14): 2332 (~ x => (~ x => x)) => (~ x => x) = 1. [para(2124(a,1),38(a,1,1))]. given #123 (H,wt=12): 16148 ~ x => (~ x => x) = ~ x => x. [hyper(43,a,37,a,b,2332,a)]. given #124 (H,wt=15): 2939 (x ^ (y v z)) * ~ ((x ^ y) v z) = ~ 1. [para(34(a,1),1050(a,1,1)),flip(a)]. given #125 (H,wt=14): 16296 (x ^ (y v z)) * ~ ((x ^ y) v z) = 0. [para(2939(a,2),595(a,1))]. given #126 (H,wt=17): 113 (1 ^ ((x ^ y) => z)) => ((x ^ y) => (x ^ z)) = 1. [para(28(a,1),30(a,1,1,1))]. given #127 (H,wt=15): 16377 (1 ^ 1) => ((x ^ y) => (x ^ (z => y))) = 1. [para(3730(a,1),113(a,1,1,2))]. given #128 (H,wt=11): 16384 (x ^ y) => (x ^ (z => y)) = 1. [hyper(40,a,10753,a(flip),b,16377,a),flip(a)]. given #129 (H,wt=11): 16496 x => ((y => x) ^ (z => x)) = 1. [para(10326(a,1),16384(a,1,1))]. given #130 (H,wt=15): 16378 (1 ^ 1) => ((x ^ y) => (x ^ (y v z))) = 1. [para(3736(a,1),113(a,1,1,2))]. given #131 (H,wt=11): 16629 (x ^ y) => (x ^ (y v z)) = 1. [hyper(40,a,10753,a(flip),b,16378,a),flip(a)]. given #132 (H,wt=15): 16379 (1 ^ 1) => ((x ^ (y ^ z)) => (x ^ y)) = 1. [para(3739(a,1),113(a,1,1,2))]. Low Water (keep): wt=16.000, iters=6692 given #133 (H,wt=11): 16751 (x ^ (y ^ z)) => (x ^ y) = 1. [hyper(40,a,10753,a(flip),b,16379,a),flip(a)]. given #134 (H,wt=9): 16862 (x ^ y) => (y ^ x) = 1. [para(13639(a,1),16751(a,1,1))]. % Operation ^ is commutative; C redundancy checks enabled. -------- Proof 12 -------- "(D6)". ============================== PROOF ================================= % Proof 12 at 0.78 (+ 0.01) seconds: "(D6)". % Length of proof is 62. % Level of proof is 14. % Maximum clause weight is 17. % Given clauses 134. 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 2 (all x all y (x = 1 & y = 1 -> x ^ y = 1)) # label("(4)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 9 x ^ y = y ^ x # label("(D6)") # label(non_clause) # label(goal). [goal]. 26 x => ((x => y) => y) = 1 # label("(A1)[= 1]"). [assumption]. 27 (x => y) => ((y => z) => (x => z)) = 1 # label("(A2)[= 1]"). [assumption]. 28 (x ^ y) => x = 1 # label("(A3)[= 1]"). [assumption]. 29 (x ^ y) => y = 1 # label("(A4)[= 1]"). [assumption]. 30 ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]"). [assumption]. 35 ~ ~ x => x = 1 # label("(A10)[= 1]"). [assumption]. 36 (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). [assumption]. 37 x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. 39 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. 40 1 != x | x => y != 1 | 1 = y. [copy(39),flip(a),flip(c)]. 41 x != 1 | y != 1 | x ^ y = 1 # label("(4)"). [clausify(2)]. 42 1 != x | 1 != y | x ^ y = 1. [copy(41),flip(a),flip(b)]. 43 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 44 x * y = ~ (x => ~ y) # label("(* def)"). [assumption]. 45 ~ (x => ~ y) = x * y. [copy(44),flip(a)]. 46 0 = ~ (x => x) # label("(0 def)"). [assumption]. 47 ~ (x => x) = 0. [copy(46),flip(a)]. 48 1 = x => x # label("(1 def)"). [assumption]. 49 x => x = 1. [copy(48),flip(a)]. 55 c12 ^ c11 != c11 ^ c12 # label("(D6)") # answer("(D6)"). [deny(9)]. 113 (1 ^ ((x ^ y) => z)) => ((x ^ y) => (x ^ z)) = 1. [para(28(a,1),30(a,1,1,1))]. 252 x => 1 = 1. [para(28(a,1),37(a,1,2))]. 366 (x => y) => ((z ^ x) => y) = 1. [hyper(40,a,29,a(flip),b,27,a),flip(a)]. 386 (1 => x) => x = 1. [hyper(40,a,xx,b,26,a),flip(a)]. 583 x => ~ y = y => ~ x. [hyper(43,a,36,a,b,36,a)]. 595 ~ 1 = 0. [para(36(a,1),47(a,1,1))]. 630 x => ~ ~ x = 1. [hyper(40,a,49,a(flip),b,36,a),flip(a)]. 640 ((x => y) ^ 1) => (x => (y ^ x)) = 1. [para(49(a,1),30(a,1,1,2))]. 674 (x => x) ^ (y => 1) = 1. [hyper(42,a,49,a(flip),b,252,a(flip))]. 728 1 => x = x. [hyper(43,a,37,a,b,386,a)]. 861 ~ ~ x = x. [hyper(43,a,35,a,b,630,a),flip(a)]. 1050 ~ (x => y) = x * ~ y. [para(861(a,1),45(a,1,1,2))]. 1264 x => (y => ~ (x => ~ y)) = 1. [para(583(a,1),26(a,1,2))]. 1277 ~ (x => ~ y) = y * x. [para(583(a,1),45(a,1,1))]. 1281 x => ~ 1 = ~ x. [para(583(a,1),728(a,1))]. 1326 x => 0 = ~ x. [para(595(a,1),1281(a,1,2))]. 2448 x => (x ^ 1) = 1. [hyper(40,a,674,a(flip),b,30,a),flip(a)]. 2521 x ^ 1 = x. [hyper(43,a,28,a,b,2448,a),flip(a)]. 2935 (x ^ y) * ~ y = ~ 1. [para(29(a,1),1050(a,1,1)),flip(a)]. 3064 x * y = y * x. [para(1277(a,1),45(a,1))]. 3491 (x ^ y) * ~ y = 0. [para(2935(a,2),595(a,1))]. 3596 ~ x * (y ^ x) = 0. [para(3491(a,1),3064(a,1)),flip(a)]. 3739 (x ^ (y ^ z)) => y = 1. [hyper(40,a,28,a(flip),b,366,a),flip(a)]. 6588 x => (y => (y * x)) = 1. [para(1277(a,1),1264(a,1,2,2))]. 9898 (x => y) => (x => (y ^ x)) = 1. [para(2521(a,1),640(a,1,1))]. 10006 x => ((y => (y * x)) ^ x) = 1. [hyper(40,a,6588,a(flip),b,9898,a),flip(a)]. 10031 x => ((y => x) ^ x) = 1. [hyper(40,a,37,a(flip),b,9898,a),flip(a)]. 10326 (x => y) ^ y = y. [hyper(43,a,29,a,b,10031,a),flip(a)]. 10753 1 ^ x = x. [para(28(a,1),10326(a,1,1))]. 12015 (x => (x * y)) ^ y = y. [hyper(43,a,29,a,b,10006,a),flip(a)]. 12578 (~ x => 0) ^ (y ^ x) = y ^ x. [para(3596(a,1),12015(a,1,1,2))]. 13528 ~ ~ x ^ (y ^ x) = y ^ x. [para(1326(a,1),12578(a,1,1))]. 13639 x ^ (y ^ x) = y ^ x. [para(861(a,1),13528(a,1,1))]. 16379 (1 ^ 1) => ((x ^ (y ^ z)) => (x ^ y)) = 1. [para(3739(a,1),113(a,1,1,2))]. 16751 (x ^ (y ^ z)) => (x ^ y) = 1. [hyper(40,a,10753,a(flip),b,16379,a),flip(a)]. 16862 (x ^ y) => (y ^ x) = 1. [para(13639(a,1),16751(a,1,1))]. 16869 x ^ y = y ^ x. [hyper(43,a,16862,a,b,16862,a)]. 16870 $F # answer("(D6)"). [resolve(16869,a,55,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 55 given #135 (H,wt=7): 16869 x ^ y = y ^ x. [hyper(43,a,16862,a,b,16862,a)]. given #136 (H,wt=9): 17043 x ^ (y => (y * x)) = x. [para(16869(a,1),12015(a,1))]. given #137 (H,wt=9): 17044 x ^ (y => (x * y)) = x. [para(16869(a,1),12549(a,1))]. given #138 (H,wt=11): 17048 x => (x ^ ((x => y) => y)) = 1. [para(16869(a,1),10042(a,1,2))]. given #139 (H,wt=9): 17466 x ^ ((x => y) => y) = x. [hyper(43,a,28,a,b,17048,a),flip(a)]. Low Water (keep): wt=15.000, iters=6744 given #140 (H,wt=11): 17224 ~ x ^ ((x ^ y) => 0) = ~ x. [para(3369(a,1),17043(a,1,2,2))]. given #141 (H,wt=10): 17755 ~ x ^ ~ (x ^ y) = ~ x. [para(1326(a,1),17224(a,1,2))]. given #142 (H,wt=10): 17877 ~ (x ^ y) ^ ~ x = ~ x. [para(17755(a,1),16869(a,1)),flip(a)]. given #143 (H,wt=13): 17245 ~ (x v y) ^ (y => 0) = ~ (x v y). [para(7422(a,1),17043(a,1,2,2))]. given #144 (H,wt=12): 17962 ~ (x v y) ^ ~ y = ~ (x v y). [para(1326(a,1),17245(a,1,2))]. given #145 (H,wt=12): 18032 ~ x ^ ~ (y v x) = ~ (y v x). [para(17962(a,1),16869(a,1)),flip(a)]. given #146 (H,wt=15): 16868 (x ^ y) v ((x ^ (y ^ z)) * 1) = x ^ y. [para(16751(a,1),15370(a,1,2,2))]. given #147 (H,wt=13): 18097 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(1640(a,1),16868(a,1,2))]. given #148 (H,wt=15): 17726 (x ^ y) ^ (1 => (x ^ (y v z))) = x ^ y. [para(16629(a,1),17466(a,1,2,1))]. given #149 (H,wt=13): 18142 (x ^ y) ^ (x ^ (y v z)) = x ^ y. [para(728(a,1),17726(a,1,2))]. given #150 (H,wt=15): 18134 (x ^ (y v z)) v (x ^ y) = x ^ (y v z). [para(11287(a,1),18097(a,1,2,2))]. given #151 (H,wt=16): 16513 (x => (x => y)) ^ (~ y => (x => y)) = x => y. [hyper(43,a,38,a,b,16496,a),flip(a)]. -------- Proof 13 -------- "(N)". ============================== PROOF ================================= % Proof 13 at 0.90 (+ 0.01) seconds: "(N)". % Length of proof is 43. % Level of proof is 14. % Maximum clause weight is 18. % Given clauses 151. 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 2 (all x all y (x = 1 & y = 1 -> x ^ y = 1)) # label("(4)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 25 (x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y # label("(N)") # label(non_clause) # label(goal). [goal]. 27 (x => y) => ((y => z) => (x => z)) = 1 # label("(A2)[= 1]"). [assumption]. 28 (x ^ y) => x = 1 # label("(A3)[= 1]"). [assumption]. 29 (x ^ y) => y = 1 # label("(A4)[= 1]"). [assumption]. 30 ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]"). [assumption]. 35 ~ ~ x => x = 1 # label("(A10)[= 1]"). [assumption]. 36 (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). [assumption]. 37 x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. 38 ((x => (x => y)) ^ (~ y => (x => y))) => (x => y) = 1 # label("(A13)[= 1]"). [assumption]. 39 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. 40 1 != x | x => y != 1 | 1 = y. [copy(39),flip(a),flip(c)]. 41 x != 1 | y != 1 | x ^ y = 1 # label("(4)"). [clausify(2)]. 42 1 != x | 1 != y | x ^ y = 1. [copy(41),flip(a),flip(b)]. 43 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 48 1 = x => x # label("(1 def)"). [assumption]. 49 x => x = 1. [copy(48),flip(a)]. 73 c44 => c45 != (c44 => (c44 => c45)) ^ (~ c45 => (~ c45 => ~ c44)) # label("(N)") # answer("(N)"). [deny(25)]. 74 (c44 => (c44 => c45)) ^ (~ c45 => (~ c45 => ~ c44)) != c44 => c45 # answer("(N)"). [copy(73),flip(a)]. 113 (1 ^ ((x ^ y) => z)) => ((x ^ y) => (x ^ z)) = 1. [para(28(a,1),30(a,1,1,1))]. 252 x => 1 = 1. [para(28(a,1),37(a,1,2))]. 366 (x => y) => ((z ^ x) => y) = 1. [hyper(40,a,29,a(flip),b,27,a),flip(a)]. 583 x => ~ y = y => ~ x. [hyper(43,a,36,a,b,36,a)]. 630 x => ~ ~ x = 1. [hyper(40,a,49,a(flip),b,36,a),flip(a)]. 640 ((x => y) ^ 1) => (x => (y ^ x)) = 1. [para(49(a,1),30(a,1,1,2))]. 674 (x => x) ^ (y => 1) = 1. [hyper(42,a,49,a(flip),b,252,a(flip))]. 861 ~ ~ x = x. [hyper(43,a,35,a,b,630,a),flip(a)]. 1283 ~ x => ~ y = y => x. [para(861(a,1),583(a,1,2)),flip(a)]. 2448 x => (x ^ 1) = 1. [hyper(40,a,674,a(flip),b,30,a),flip(a)]. 2521 x ^ 1 = x. [hyper(43,a,28,a,b,2448,a),flip(a)]. 3730 (x ^ y) => (z => y) = 1. [hyper(40,a,37,a(flip),b,366,a),flip(a)]. 9898 (x => y) => (x => (y ^ x)) = 1. [para(2521(a,1),640(a,1,1))]. 10031 x => ((y => x) ^ x) = 1. [hyper(40,a,37,a(flip),b,9898,a),flip(a)]. 10326 (x => y) ^ y = y. [hyper(43,a,29,a,b,10031,a),flip(a)]. 10753 1 ^ x = x. [para(28(a,1),10326(a,1,1))]. 16377 (1 ^ 1) => ((x ^ y) => (x ^ (z => y))) = 1. [para(3730(a,1),113(a,1,1,2))]. 16384 (x ^ y) => (x ^ (z => y)) = 1. [hyper(40,a,10753,a(flip),b,16377,a),flip(a)]. 16496 x => ((y => x) ^ (z => x)) = 1. [para(10326(a,1),16384(a,1,1))]. 16513 (x => (x => y)) ^ (~ y => (x => y)) = x => y. [hyper(43,a,38,a,b,16496,a),flip(a)]. 18204 (x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y. [para(1283(a,2),16513(a,1,2,2))]. 18205 $F # answer("(N)"). [resolve(18204,a,74,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 73x 74 given #152 (H,wt=17): 175 (1 ^ (x => (y v z))) => ((z v x) => (y v z)) = 1. [para(32(a,1),33(a,1,1,1))]. given #153 (H,wt=13): 18209 (1 ^ 1) => ((x v y) => (y v x)) = 1. [para(31(a,1),175(a,1,1,2))]. given #154 (H,wt=9): 18213 (x v y) => (y v x) = 1. [hyper(40,a,10753,a(flip),b,18209,a),flip(a)]. % Operation v is commutative; C redundancy checks enabled. -------- Proof 14 -------- "(D5)". ============================== PROOF ================================= % Proof 14 at 0.92 (+ 0.01) seconds: "(D5)". % Length of proof is 33. % Level of proof is 12. % Maximum clause weight is 17. % Given clauses 154. 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 2 (all x all y (x = 1 & y = 1 -> x ^ y = 1)) # label("(4)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 8 x v y = y v x # label("(D5)") # label(non_clause) # label(goal). [goal]. 28 (x ^ y) => x = 1 # label("(A3)[= 1]"). [assumption]. 29 (x ^ y) => y = 1 # label("(A4)[= 1]"). [assumption]. 30 ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]"). [assumption]. 31 x => (x v y) = 1 # label("(A6)[= 1]"). [assumption]. 32 x => (y v x) = 1 # label("(A7)[= 1]"). [assumption]. 33 ((x => y) ^ (z => y)) => ((x v z) => y) = 1 # label("(A8)[= 1]"). [assumption]. 37 x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. 39 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. 40 1 != x | x => y != 1 | 1 = y. [copy(39),flip(a),flip(c)]. 41 x != 1 | y != 1 | x ^ y = 1 # label("(4)"). [clausify(2)]. 42 1 != x | 1 != y | x ^ y = 1. [copy(41),flip(a),flip(b)]. 43 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 48 1 = x => x # label("(1 def)"). [assumption]. 49 x => x = 1. [copy(48),flip(a)]. 54 c10 v c9 != c9 v c10 # label("(D5)") # answer("(D5)"). [deny(8)]. 175 (1 ^ (x => (y v z))) => ((z v x) => (y v z)) = 1. [para(32(a,1),33(a,1,1,1))]. 252 x => 1 = 1. [para(28(a,1),37(a,1,2))]. 640 ((x => y) ^ 1) => (x => (y ^ x)) = 1. [para(49(a,1),30(a,1,1,2))]. 674 (x => x) ^ (y => 1) = 1. [hyper(42,a,49,a(flip),b,252,a(flip))]. 2448 x => (x ^ 1) = 1. [hyper(40,a,674,a(flip),b,30,a),flip(a)]. 2521 x ^ 1 = x. [hyper(43,a,28,a,b,2448,a),flip(a)]. 9898 (x => y) => (x => (y ^ x)) = 1. [para(2521(a,1),640(a,1,1))]. 10031 x => ((y => x) ^ x) = 1. [hyper(40,a,37,a(flip),b,9898,a),flip(a)]. 10326 (x => y) ^ y = y. [hyper(43,a,29,a,b,10031,a),flip(a)]. 10753 1 ^ x = x. [para(28(a,1),10326(a,1,1))]. 18209 (1 ^ 1) => ((x v y) => (y v x)) = 1. [para(31(a,1),175(a,1,1,2))]. 18213 (x v y) => (y v x) = 1. [hyper(40,a,10753,a(flip),b,18209,a),flip(a)]. 18216 x v y = y v x. [hyper(43,a,18213,a,b,18213,a)]. 18217 $F # answer("(D5)"). [resolve(18216,a,54,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 54 given #155 (H,wt=7): 18216 x v y = y v x. [hyper(43,a,18213,a,b,18213,a)]. given #156 (H,wt=7): 18308 (x v y) ^ y = y. [para(18216(a,1),11287(a,1,1))]. given #157 (H,wt=9): 18310 x v (x v y) = x v y. [para(18216(a,1),11894(a,1))]. given #158 (H,wt=13): 18326 (x ^ (y ^ z)) v (x ^ y) = x ^ y. [para(18216(a,1),18097(a,1))]. given #159 (H,wt=14): 18320 (x ^ (y v z)) * ~ (z v (x ^ y)) = 0. [para(18216(a,1),16296(a,1,2,1))]. given #160 (H,wt=15): 18212 (1 ^ 1) => ((x v (y ^ z)) => (y v x)) = 1. [para(4381(a,1),175(a,1,1,2))]. given #161 (H,wt=11): 18632 (x v (y ^ z)) => (y v x) = 1. [hyper(40,a,10753,a(flip),b,18212,a),flip(a)]. given #162 (H,wt=14): 18675 (x v (y ^ z)) * (1 * ~ (y v x)) = 0. [para(18632(a,1),7068(a,1,2,1))]. given #163 (H,wt=12): 18704 (x v (y ^ z)) * ~ (y v x) = 0. [para(1100(a,1),18675(a,1,2))]. given #164 (H,wt=15): 18328 (x ^ y) v (x ^ (y v z)) = x ^ (y v z). [para(18216(a,1),18134(a,1))]. given #165 (H,wt=15): 18535 (x ^ (y v z)) v (x ^ z) = x ^ (y v z). [para(18308(a,1),18097(a,1,2,2))]. given #166 (H,wt=15): 18611 (x ^ y) v (x ^ (z v y)) = x ^ (z v y). [para(18308(a,1),18326(a,1,1,2))]. given #167 (H,wt=15): 18818 (x ^ (y v z)) v (z ^ x) = x ^ (y v z). [para(16869(a,1),18535(a,1,2))]. given #168 (H,wt=17): 377 (((x => y) => (z => y)) => u) => ((z => x) => u) = 1. [hyper(40,a,27,a(flip),b,27,a),flip(a)]. given #169 (H,wt=13): 18860 (x => (y => z)) => (y => (x => z)) = 1. [hyper(40,a,382,a(flip),b,377,a),flip(a)]. given #170 (H,wt=11): 18862 x => (y => z) = y => (x => z). [hyper(43,a,18860,a,b,18860,a)]. given #171 (H,wt=13): 18909 ~ (x => (y => z)) = y * ~ (x => z). [para(18862(a,1),1050(a,1,1))]. given #172 (H,wt=13): 18935 x => (~ y => ~ z) = (x * z) => y. [para(18862(a,1),3197(a,1))]. given #173 (H,wt=11): 19047 (x * y) => z = x => (y => z). [para(1283(a,1),18935(a,1,2)),flip(a)]. given #174 (H,wt=13): 18984 x * ~ (y => z) = y * ~ (x => z). [para(18909(a,1),1050(a,1))]. given #175 (H,wt=13): 19232 x * ~ (y => z) = y * (x * ~ z). [para(1050(a,1),18984(a,1,2)),flip(a)]. given #176 (H,wt=13): 19244 x * (y * ~ ~ z) = y * (x * z). [para(45(a,1),19232(a,1,2)),flip(a)]. given #177 (H,wt=11): 19290 x * (y * z) = y * (x * z). [para(861(a,1),19244(a,1,2,2))]. given #178 (H,wt=11): 19340 x * (y * z) = z * (x * y). [para(3064(a,1),19290(a,1,2))]. % Operation * is associative-commutative; CAC redundancy checks enabled. -------- Proof 15 -------- "(M3)". ============================== PROOF ================================= % Proof 15 at 1.05 (+ 0.01) seconds: "(M3)". % Length of proof is 33. % Level of proof is 13. % Maximum clause weight is 17. % Given clauses 178. 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 16 (x * y) * z = x * (y * z) # label("(M3)") # label(non_clause) # label(goal). [goal]. 26 x => ((x => y) => y) = 1 # label("(A1)[= 1]"). [assumption]. 27 (x => y) => ((y => z) => (x => z)) = 1 # label("(A2)[= 1]"). [assumption]. 35 ~ ~ x => x = 1 # label("(A10)[= 1]"). [assumption]. 36 (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). [assumption]. 39 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. 40 1 != x | x => y != 1 | 1 = y. [copy(39),flip(a),flip(c)]. 43 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 44 x * y = ~ (x => ~ y) # label("(* def)"). [assumption]. 45 ~ (x => ~ y) = x * y. [copy(44),flip(a)]. 48 1 = x => x # label("(1 def)"). [assumption]. 49 x => x = 1. [copy(48),flip(a)]. 62 (c22 * c23) * c24 != c22 * (c23 * c24) # label("(M3)") # answer("(M3)"). [deny(16)]. 377 (((x => y) => (z => y)) => u) => ((z => x) => u) = 1. [hyper(40,a,27,a(flip),b,27,a),flip(a)]. 382 (((x => y) => y) => z) => (x => z) = 1. [hyper(40,a,26,a(flip),b,27,a),flip(a)]. 583 x => ~ y = y => ~ x. [hyper(43,a,36,a,b,36,a)]. 630 x => ~ ~ x = 1. [hyper(40,a,49,a(flip),b,36,a),flip(a)]. 861 ~ ~ x = x. [hyper(43,a,35,a,b,630,a),flip(a)]. 1050 ~ (x => y) = x * ~ y. [para(861(a,1),45(a,1,1,2))]. 1277 ~ (x => ~ y) = y * x. [para(583(a,1),45(a,1,1))]. 3064 x * y = y * x. [para(1277(a,1),45(a,1))]. 18860 (x => (y => z)) => (y => (x => z)) = 1. [hyper(40,a,382,a(flip),b,377,a),flip(a)]. 18862 x => (y => z) = y => (x => z). [hyper(43,a,18860,a,b,18860,a)]. 18909 ~ (x => (y => z)) = y * ~ (x => z). [para(18862(a,1),1050(a,1,1))]. 18984 x * ~ (y => z) = y * ~ (x => z). [para(18909(a,1),1050(a,1))]. 19232 x * ~ (y => z) = y * (x * ~ z). [para(1050(a,1),18984(a,1,2)),flip(a)]. 19244 x * (y * ~ ~ z) = y * (x * z). [para(45(a,1),19232(a,1,2)),flip(a)]. 19290 x * (y * z) = y * (x * z). [para(861(a,1),19244(a,1,2,2))]. 19340 x * (y * z) = z * (x * y). [para(3064(a,1),19290(a,1,2))]. 19385 (x * y) * z = x * (y * z). [para(19340(a,2),3064(a,1)),flip(a)]. 19386 $F # answer("(M3)"). [resolve(19385,a,62,a)]. ============================== end of proof ========================== % back CAC tautology: 19340 x * (y * z) = z * (x * y). [para(3064(a,1),19290(a,1,2))]. % back CAC tautology: 19384 (x * y) * z = y * (z * x). [para(19340(a,1),3064(a,1)),flip(a)]. % back CAC tautology: 19339 (x * y) * z = x * (z * y). [para(19290(a,1),3064(a,1)),flip(a)]. % Disable descendants (x means already disabled): 62 given #179 (H,wt=11): 19385 (x * y) * z = x * (y * z). [para(19340(a,2),3064(a,1)),flip(a)]. given #180 (H,wt=17): 16138 ((x v y) => 0) ^ (~ x ^ ~ y) = ~ x ^ ~ y. [para(15944(a,1),12015(a,1,1,2))]. given #181 (H,wt=16): 19503 ~ (x v y) ^ (~ x ^ ~ y) = ~ x ^ ~ y. [para(1326(a,1),16138(a,1,1))]. given #182 (H,wt=17): 16231 ~ ~ x => (x => ~ ~ ~ x) = ~ ~ x => ~ x. [para(583(a,1),16148(a,1,2))]. given #183 (H,wt=15): 19511 x => (x => ~ ~ ~ x) = ~ ~ x => ~ x. [para(861(a,1),16231(a,1,1))]. given #184 (H,wt=13): 19516 ~ ~ x => ~ x = x => (x => ~ x). [para(861(a,1),19511(a,1,2,2,1)),flip(a)]. given #185 (H,wt=11): 19523 x => (x => ~ x) = x => ~ x. [para(861(a,1),19516(a,1,1)),flip(a)]. given #186 (H,wt=13): 19568 x * ~ (x => ~ x) = ~ (x => ~ x). [para(19523(a,1),1050(a,1,1)),flip(a)]. given #187 (H,wt=11): 19590 x * ~ (x => ~ x) = x * x. [para(19568(a,2),45(a,1))]. given #188 (H,wt=9): 19610 x * (x * x) = x * x. [para(45(a,1),19590(a,1,2))]. given #189 (H,wt=13): 19672 x => ((x * x) => y) = (x * x) => y. [para(19610(a,1),19047(a,1,1)),flip(a)]. given #190 (H,wt=13): 19694 x => ((x * x) => y) = x => (x => y). [para(19672(a,2),19047(a,1))]. -------- Proof 16 -------- "(E_2)". ============================== PROOF ================================= % Proof 16 at 1.10 (+ 0.01) seconds: "(E_2)". % Length of proof is 51. % Level of proof is 18. % Maximum clause weight is 18. % Given clauses 190. 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 2 (all x all y (x = 1 & y = 1 -> x ^ y = 1)) # label("(4)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 21 x => (x => (x => y)) = x => (x => y) # label("(E_2)") # label(non_clause) # label(goal). [goal]. 26 x => ((x => y) => y) = 1 # label("(A1)[= 1]"). [assumption]. 27 (x => y) => ((y => z) => (x => z)) = 1 # label("(A2)[= 1]"). [assumption]. 29 (x ^ y) => y = 1 # label("(A4)[= 1]"). [assumption]. 30 ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]"). [assumption]. 35 ~ ~ x => x = 1 # label("(A10)[= 1]"). [assumption]. 36 (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). [assumption]. 37 x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. 38 ((x => (x => y)) ^ (~ y => (x => y))) => (x => y) = 1 # label("(A13)[= 1]"). [assumption]. 39 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. 40 1 != x | x => y != 1 | 1 = y. [copy(39),flip(a),flip(c)]. 41 x != 1 | y != 1 | x ^ y = 1 # label("(4)"). [clausify(2)]. 42 1 != x | 1 != y | x ^ y = 1. [copy(41),flip(a),flip(b)]. 43 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 44 x * y = ~ (x => ~ y) # label("(* def)"). [assumption]. 45 ~ (x => ~ y) = x * y. [copy(44),flip(a)]. 48 1 = x => x # label("(1 def)"). [assumption]. 49 x => x = 1. [copy(48),flip(a)]. 68 c35 => (c35 => (c35 => c36)) != c35 => (c35 => c36) # label("(E_2)") # answer("(E_2)"). [deny(21)]. 377 (((x => y) => (z => y)) => u) => ((z => x) => u) = 1. [hyper(40,a,27,a(flip),b,27,a),flip(a)]. 382 (((x => y) => y) => z) => (x => z) = 1. [hyper(40,a,26,a(flip),b,27,a),flip(a)]. 583 x => ~ y = y => ~ x. [hyper(43,a,36,a,b,36,a)]. 600 (x => x) ^ (y => y) = 1. [hyper(42,a,49,a(flip),b,49,a(flip))]. 630 x => ~ ~ x = 1. [hyper(40,a,49,a(flip),b,36,a),flip(a)]. 861 ~ ~ x = x. [hyper(43,a,35,a,b,630,a),flip(a)]. 1050 ~ (x => y) = x * ~ y. [para(861(a,1),45(a,1,1,2))]. 1054 ~ (x * y) = x => ~ y. [para(45(a,1),861(a,1,1))]. 1283 ~ x => ~ y = y => x. [para(861(a,1),583(a,1,2)),flip(a)]. 1808 x => (x ^ x) = 1. [hyper(40,a,600,a(flip),b,30,a),flip(a)]. 2124 x ^ x = x. [hyper(43,a,29,a,b,1808,a),flip(a)]. 2332 (~ x => (~ x => x)) => (~ x => x) = 1. [para(2124(a,1),38(a,1,1))]. 3197 ~ x => (y => ~ z) = (y * z) => x. [para(1054(a,1),1283(a,1,2))]. 16148 ~ x => (~ x => x) = ~ x => x. [hyper(43,a,37,a,b,2332,a)]. 16231 ~ ~ x => (x => ~ ~ ~ x) = ~ ~ x => ~ x. [para(583(a,1),16148(a,1,2))]. 18860 (x => (y => z)) => (y => (x => z)) = 1. [hyper(40,a,382,a(flip),b,377,a),flip(a)]. 18862 x => (y => z) = y => (x => z). [hyper(43,a,18860,a,b,18860,a)]. 18935 x => (~ y => ~ z) = (x * z) => y. [para(18862(a,1),3197(a,1))]. 19047 (x * y) => z = x => (y => z). [para(1283(a,1),18935(a,1,2)),flip(a)]. 19511 x => (x => ~ ~ ~ x) = ~ ~ x => ~ x. [para(861(a,1),16231(a,1,1))]. 19516 ~ ~ x => ~ x = x => (x => ~ x). [para(861(a,1),19511(a,1,2,2,1)),flip(a)]. 19523 x => (x => ~ x) = x => ~ x. [para(861(a,1),19516(a,1,1)),flip(a)]. 19568 x * ~ (x => ~ x) = ~ (x => ~ x). [para(19523(a,1),1050(a,1,1)),flip(a)]. 19590 x * ~ (x => ~ x) = x * x. [para(19568(a,2),45(a,1))]. 19610 x * (x * x) = x * x. [para(45(a,1),19590(a,1,2))]. 19672 x => ((x * x) => y) = (x * x) => y. [para(19610(a,1),19047(a,1,1)),flip(a)]. 19694 x => ((x * x) => y) = x => (x => y). [para(19672(a,2),19047(a,1))]. 19718 x => (x => (x => y)) = x => (x => y). [para(19047(a,1),19694(a,1,2))]. 19719 $F # answer("(E_2)"). [resolve(19718,a,68,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 68 given #191 (H,wt=13): 19718 x => (x => (x => y)) = x => (x => y). [para(19047(a,1),19694(a,1,2))]. given #192 (H,wt=17): 18171 (x ^ y) ^ (x ^ ((x ^ y) v z)) = x ^ (x ^ y). [para(13097(a,1),18142(a,1,1))]. given #193 (H,wt=17): 19735 (x ^ y) ^ (x ^ (z v (x ^ y))) = x ^ (x ^ y). [para(18216(a,1),18171(a,1,2,2))]. given #194 (H,wt=15): 19737 (x ^ y) ^ (x ^ (z v (x ^ y))) = x ^ y. [para(19735(a,2),13097(a,1))]. given #195 (H,wt=18): 18204 (x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y. [para(1283(a,2),16513(a,1,2,2))]. given #196 (H,wt=18): 18774 (x v (y ^ z)) ^ (~ (y v x) => 0) = x v (y ^ z). [para(18704(a,1),17044(a,1,2,2))]. given #197 (H,wt=18): 19761 (x v (y ^ z)) ^ (~ (x v y) => 0) = x v (y ^ z). [para(18216(a,1),18774(a,1,2,1,1))]. given #198 (H,wt=17): 19763 (x v (y ^ z)) ^ ~ ~ (x v y) = x v (y ^ z). [para(1326(a,1),19761(a,1,2))]. given #199 (H,wt=15): 19767 (x v (y ^ z)) ^ (x v y) = x v (y ^ z). [para(861(a,1),19763(a,1,2))]. given #200 (H,wt=15): 19798 (x v y) ^ (x v (y ^ z)) = x v (y ^ z). [para(19767(a,1),16869(a,1)),flip(a)]. given #201 (H,wt=19): 18837 (x ^ y) v (x ^ (z v (x ^ y))) = x ^ (z v (x ^ y)). [para(13097(a,1),18611(a,1,1))]. given #202 (H,wt=19): 19817 (x v y) ^ (x v ((x v y) ^ z)) = x v ((x v y) ^ z). [para(18310(a,1),19798(a,1,1))]. given #203 (H,wt=19): 19827 (x v y) ^ (x v (z ^ (x v y))) = x v ((x v y) ^ z). [para(16869(a,1),19817(a,1,2,2))]. given #204 (H,wt=19): 19829 (x v y) ^ (x v (z ^ (x v y))) = x v (z ^ (x v y)). [para(16869(a,1),19827(a,2,2))]. given #205 (H,wt=20): 18629 (x ^ (y v z)) ^ (~ (z v (x ^ y)) => 0) = x ^ (y v z). [para(18320(a,1),17044(a,1,2,2))]. given #206 (H,wt=19): 19833 (x ^ (y v z)) ^ ~ ~ (z v (x ^ y)) = x ^ (y v z). [para(1326(a,1),18629(a,1,2))]. given #207 (H,wt=17): 19834 (x ^ (y v z)) ^ (z v (x ^ y)) = x ^ (y v z). [para(861(a,1),19833(a,1,2))]. given #208 (H,wt=17): 19838 (x v (y ^ z)) v (y ^ (z v x)) = x v (y ^ z). [para(19834(a,1),13776(a,1,2))]. given #209 (H,wt=21): 9096 ((x => (y ^ z)) => (x => y)) ^ ((u => (w ^ v5)) => (u => v5)) = 1. [hyper(42,a,8436,a(flip),b,8959,a(flip))]. given #210 (H,wt=15): 19846 (x => (y ^ z)) => ((x => y) ^ (x => z)) = 1. [hyper(40,a,9096,a(flip),b,30,a),flip(a)]. -------- Proof 17 -------- "(R2)". ============================== PROOF ================================= % Proof 17 at 1.19 (+ 0.01) seconds: "(R2)". % Length of proof is 27. % Level of proof is 9. % Maximum clause weight is 21. % Given clauses 210. 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 2 (all x all y (x = 1 & y = 1 -> x ^ y = 1)) # label("(4)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 18 x => (y ^ z) = (x => y) ^ (x => z) # label("(R2)") # label(non_clause) # label(goal). [goal]. 26 x => ((x => y) => y) = 1 # label("(A1)[= 1]"). [assumption]. 27 (x => y) => ((y => z) => (x => z)) = 1 # label("(A2)[= 1]"). [assumption]. 28 (x ^ y) => x = 1 # label("(A3)[= 1]"). [assumption]. 29 (x ^ y) => y = 1 # label("(A4)[= 1]"). [assumption]. 30 ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]"). [assumption]. 37 x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. 39 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. 40 1 != x | x => y != 1 | 1 = y. [copy(39),flip(a),flip(c)]. 41 x != 1 | y != 1 | x ^ y = 1 # label("(4)"). [clausify(2)]. 42 1 != x | 1 != y | x ^ y = 1. [copy(41),flip(a),flip(b)]. 43 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 64 c28 => (c29 ^ c30) != (c28 => c29) ^ (c28 => c30) # label("(R2)") # answer("(R2)"). [deny(18)]. 65 (c28 => c29) ^ (c28 => c30) != c28 => (c29 ^ c30) # answer("(R2)"). [copy(64),flip(a)]. 90 (x => (y ^ z)) => (1 => (x => y)) = 1. [para(28(a,1),27(a,1,2,1))]. 97 (x => (y ^ z)) => (1 => (x => z)) = 1. [para(29(a,1),27(a,1,2,1))]. 386 (1 => x) => x = 1. [hyper(40,a,xx,b,26,a),flip(a)]. 728 1 => x = x. [hyper(43,a,37,a,b,386,a)]. 8436 (x => (y ^ z)) => (x => y) = 1. [para(728(a,1),90(a,1,2))]. 8959 (x => (y ^ z)) => (x => z) = 1. [para(728(a,1),97(a,1,2))]. 9096 ((x => (y ^ z)) => (x => y)) ^ ((u => (w ^ v5)) => (u => v5)) = 1. [hyper(42,a,8436,a(flip),b,8959,a(flip))]. 19846 (x => (y ^ z)) => ((x => y) ^ (x => z)) = 1. [hyper(40,a,9096,a(flip),b,30,a),flip(a)]. 19850 (x => y) ^ (x => z) = x => (y ^ z). [hyper(43,a,30,a,b,19846,a),flip(a)]. 19851 $F # answer("(R2)"). [resolve(19850,a,65,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 64x 65 given #211 (H,wt=13): 19850 (x => y) ^ (x => z) = x => (y ^ z). [hyper(43,a,30,a,b,19846,a),flip(a)]. given #212 (H,wt=15): 19880 (x => ~ y) ^ (y => z) = y => (~ x ^ z). [para(583(a,1),19850(a,1,1))]. given #213 (H,wt=15): 19930 (x => ~ y) ^ (y => z) = y => (z ^ ~ x). [para(16869(a,1),19880(a,2,2))]. given #214 (H,wt=23): 19840 (x ^ ((y ^ z) v (x ^ y))) ^ (x ^ y) = x ^ ((y ^ z) v (x ^ y)). [para(18097(a,1),19834(a,1,2))]. given #215 (H,wt=23): 19950 (x ^ y) ^ (x ^ ((y ^ z) v (x ^ y))) = x ^ ((y ^ z) v (x ^ y)). [para(19840(a,1),16869(a,1)),flip(a)]. given #216 (H,wt=13): 19951 x ^ ((y ^ z) v (x ^ y)) = x ^ y. [para(19950(a,1),19737(a,1))]. given #217 (H,wt=11): 19979 x ^ (y ^ (z v x)) = x ^ y. [para(18818(a,1),19951(a,1,2))]. given #218 (H,wt=11): 20029 x ^ (y ^ (z v x)) = y ^ x. [para(19979(a,2),16869(a,1))]. given #219 (H,wt=13): 20053 (x ^ y) ^ (z ^ x) = z ^ (x ^ y). [para(5572(a,1),20029(a,1,2,2))]. given #220 (H,wt=13): 20110 (x ^ y) ^ (y ^ z) = x ^ (y ^ z). [para(20053(a,1),16869(a,1)),flip(a)]. given #221 (H,wt=13): 20112 (x ^ y) ^ (x ^ z) = z ^ (x ^ y). [para(16869(a,1),20053(a,1,2))]. given #222 (H,wt=13): 20151 (x ^ y) ^ (x ^ z) = y ^ (x ^ z). [para(16869(a,1),20110(a,1,1))]. given #223 (H,wt=11): 20232 x ^ (y ^ z) = z ^ (y ^ x). [para(20151(a,1),20112(a,1))]. given #224 (H,wt=11): 20276 (x ^ y) ^ z = y ^ (x ^ z). [para(20232(a,1),16869(a,1)),flip(a)]. -------- Proof 18 -------- "(D2)". ============================== PROOF ================================= % Proof 18 at 1.30 (+ 0.02) seconds: "(D2)". % Length of proof is 132. % Level of proof is 30. % Maximum clause weight is 23. % Given clauses 224. 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 2 (all x all y (x = 1 & y = 1 -> x ^ y = 1)) # label("(4)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 5 (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)") # label(non_clause) # label(goal). [goal]. 26 x => ((x => y) => y) = 1 # label("(A1)[= 1]"). [assumption]. 27 (x => y) => ((y => z) => (x => z)) = 1 # label("(A2)[= 1]"). [assumption]. 28 (x ^ y) => x = 1 # label("(A3)[= 1]"). [assumption]. 29 (x ^ y) => y = 1 # label("(A4)[= 1]"). [assumption]. 30 ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]"). [assumption]. 31 x => (x v y) = 1 # label("(A6)[= 1]"). [assumption]. 32 x => (y v x) = 1 # label("(A7)[= 1]"). [assumption]. 33 ((x => y) ^ (z => y)) => ((x v z) => y) = 1 # label("(A8)[= 1]"). [assumption]. 34 (x ^ (y v z)) => ((x ^ y) v z) = 1 # label("(A9)[= 1]"). [assumption]. 35 ~ ~ x => x = 1 # label("(A10)[= 1]"). [assumption]. 36 (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). [assumption]. 37 x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. 39 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. 40 1 != x | x => y != 1 | 1 = y. [copy(39),flip(a),flip(c)]. 41 x != 1 | y != 1 | x ^ y = 1 # label("(4)"). [clausify(2)]. 42 1 != x | 1 != y | x ^ y = 1. [copy(41),flip(a),flip(b)]. 43 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 44 x * y = ~ (x => ~ y) # label("(* def)"). [assumption]. 45 ~ (x => ~ y) = x * y. [copy(44),flip(a)]. 46 0 = ~ (x => x) # label("(0 def)"). [assumption]. 47 ~ (x => x) = 0. [copy(46),flip(a)]. 48 1 = x => x # label("(1 def)"). [assumption]. 49 x => x = 1. [copy(48),flip(a)]. 51 (c4 ^ c5) ^ c6 != c4 ^ (c5 ^ c6) # label("(D2)") # answer("(D2)"). [deny(5)]. 113 (1 ^ ((x ^ y) => z)) => ((x ^ y) => (x ^ z)) = 1. [para(28(a,1),30(a,1,1,1))]. 175 (1 ^ (x => (y v z))) => ((z v x) => (y v z)) = 1. [para(32(a,1),33(a,1,1,1))]. 252 x => 1 = 1. [para(28(a,1),37(a,1,2))]. 366 (x => y) => ((z ^ x) => y) = 1. [hyper(40,a,29,a(flip),b,27,a),flip(a)]. 386 (1 => x) => x = 1. [hyper(40,a,xx,b,26,a),flip(a)]. 583 x => ~ y = y => ~ x. [hyper(43,a,36,a,b,36,a)]. 595 ~ 1 = 0. [para(36(a,1),47(a,1,1))]. 622 (x => x) ^ (y => (y v z)) = 1. [hyper(42,a,49,a(flip),b,31,a(flip))]. 625 (x => x) ^ ((y ^ z) => y) = 1. [hyper(42,a,49,a(flip),b,28,a(flip))]. 630 x => ~ ~ x = 1. [hyper(40,a,49,a(flip),b,36,a),flip(a)]. 640 ((x => y) ^ 1) => (x => (y ^ x)) = 1. [para(49(a,1),30(a,1,1,2))]. 645 ((x => y) ^ 1) => ((x v y) => y) = 1. [para(49(a,1),33(a,1,1,2))]. 674 (x => x) ^ (y => 1) = 1. [hyper(42,a,49,a(flip),b,252,a(flip))]. 728 1 => x = x. [hyper(43,a,37,a,b,386,a)]. 861 ~ ~ x = x. [hyper(43,a,35,a,b,630,a),flip(a)]. 1050 ~ (x => y) = x * ~ y. [para(861(a,1),45(a,1,1,2))]. 1054 ~ (x * y) = x => ~ y. [para(45(a,1),861(a,1,1))]. 1263 x => ((y => ~ x) => ~ y) = 1. [para(583(a,1),26(a,1,2,1))]. 1264 x => (y => ~ (x => ~ y)) = 1. [para(583(a,1),26(a,1,2))]. 1277 ~ (x => ~ y) = y * x. [para(583(a,1),45(a,1,1))]. 1281 x => ~ 1 = ~ x. [para(583(a,1),728(a,1))]. 1283 ~ x => ~ y = y => x. [para(861(a,1),583(a,1,2)),flip(a)]. 1321 ~ ~ x = x * 1. [para(1281(a,1),45(a,1,1))]. 1326 x => 0 = ~ x. [para(595(a,1),1281(a,1,2))]. 1640 x * 1 = x. [para(1321(a,1),861(a,1))]. 2448 x => (x ^ 1) = 1. [hyper(40,a,674,a(flip),b,30,a),flip(a)]. 2521 x ^ 1 = x. [hyper(43,a,28,a,b,2448,a),flip(a)]. 2935 (x ^ y) * ~ y = ~ 1. [para(29(a,1),1050(a,1,1)),flip(a)]. 2939 (x ^ (y v z)) * ~ ((x ^ y) v z) = ~ 1. [para(34(a,1),1050(a,1,1)),flip(a)]. 3031 ~ (x * y) = y => ~ x. [para(1054(a,2),583(a,1))]. 3064 x * y = y * x. [para(1277(a,1),45(a,1))]. 3491 (x ^ y) * ~ y = 0. [para(2935(a,2),595(a,1))]. 3596 ~ x * (y ^ x) = 0. [para(3491(a,1),3064(a,1)),flip(a)]. 3736 (x ^ y) => (y v z) = 1. [hyper(40,a,31,a(flip),b,366,a),flip(a)]. 3739 (x ^ (y ^ z)) => y = 1. [hyper(40,a,28,a(flip),b,366,a),flip(a)]. 4812 x => (x ^ (x v y)) = 1. [hyper(40,a,622,a(flip),b,30,a),flip(a)]. 4893 x ^ (x v y) = x. [hyper(43,a,28,a,b,4812,a),flip(a)]. 5480 (x v (x ^ y)) => x = 1. [hyper(40,a,625,a(flip),b,33,a),flip(a)]. 5572 x v (x ^ y) = x. [hyper(43,a,31,a,b,5480,a)]. 6326 x => ~ (y * (y => ~ x)) = 1. [para(3031(a,2),1263(a,1,2))]. 6588 x => (y => (y * x)) = 1. [para(1277(a,1),1264(a,1,2,2))]. 7667 ~ x => ~ (y * (y => x)) = 1. [para(861(a,1),6326(a,1,2,1,2,2))]. 7991 (x * (x => y)) => y = 1. [para(7667(a,1),1283(a,1)),flip(a)]. 9898 (x => y) => (x => (y ^ x)) = 1. [para(2521(a,1),640(a,1,1))]. 10006 x => ((y => (y * x)) ^ x) = 1. [hyper(40,a,6588,a(flip),b,9898,a),flip(a)]. 10031 x => ((y => x) ^ x) = 1. [hyper(40,a,37,a(flip),b,9898,a),flip(a)]. 10037 x => ((x v y) ^ x) = 1. [hyper(40,a,31,a(flip),b,9898,a),flip(a)]. 10040 (x ^ y) => (x ^ (x ^ y)) = 1. [hyper(40,a,28,a(flip),b,9898,a),flip(a)]. 10042 x => (((x => y) => y) ^ x) = 1. [hyper(40,a,26,a(flip),b,9898,a),flip(a)]. 10326 (x => y) ^ y = y. [hyper(43,a,29,a,b,10031,a),flip(a)]. 10753 1 ^ x = x. [para(28(a,1),10326(a,1,1))]. 11287 (x v y) ^ x = x. [hyper(43,a,29,a,b,10037,a),flip(a)]. 12015 (x => (x * y)) ^ y = y. [hyper(43,a,29,a,b,10006,a),flip(a)]. 12549 (x => (y * x)) ^ y = y. [para(3064(a,1),12015(a,1,1,2))]. 12578 (~ x => 0) ^ (y ^ x) = y ^ x. [para(3596(a,1),12015(a,1,1,2))]. 13097 x ^ (x ^ y) = x ^ y. [hyper(43,a,29,a,b,10040,a),flip(a)]. 13528 ~ ~ x ^ (y ^ x) = y ^ x. [para(1326(a,1),12578(a,1,1))]. 13639 x ^ (y ^ x) = y ^ x. [para(861(a,1),13528(a,1,1))]. 13776 x v (y ^ x) = x. [para(13639(a,1),5572(a,1,2))]. 14367 (x => y) => ((x v y) => y) = 1. [para(2521(a,1),645(a,1,1))]. 14410 ((x * (x => y)) v y) => y = 1. [hyper(40,a,7991,a(flip),b,14367,a),flip(a)]. 14629 (x * (x => y)) v y = y. [hyper(43,a,32,a,b,14410,a)]. 14979 (x * (x => y)) ^ y = x * (x => y). [para(14629(a,1),4893(a,1,2))]. 15370 x v (y * (y => x)) = x. [para(14979(a,1),13776(a,1,2))]. 16296 (x ^ (y v z)) * ~ ((x ^ y) v z) = 0. [para(2939(a,2),595(a,1))]. 16378 (1 ^ 1) => ((x ^ y) => (x ^ (y v z))) = 1. [para(3736(a,1),113(a,1,1,2))]. 16379 (1 ^ 1) => ((x ^ (y ^ z)) => (x ^ y)) = 1. [para(3739(a,1),113(a,1,1,2))]. 16629 (x ^ y) => (x ^ (y v z)) = 1. [hyper(40,a,10753,a(flip),b,16378,a),flip(a)]. 16751 (x ^ (y ^ z)) => (x ^ y) = 1. [hyper(40,a,10753,a(flip),b,16379,a),flip(a)]. 16862 (x ^ y) => (y ^ x) = 1. [para(13639(a,1),16751(a,1,1))]. 16868 (x ^ y) v ((x ^ (y ^ z)) * 1) = x ^ y. [para(16751(a,1),15370(a,1,2,2))]. 16869 x ^ y = y ^ x. [hyper(43,a,16862,a,b,16862,a)]. 17044 x ^ (y => (x * y)) = x. [para(16869(a,1),12549(a,1))]. 17048 x => (x ^ ((x => y) => y)) = 1. [para(16869(a,1),10042(a,1,2))]. 17466 x ^ ((x => y) => y) = x. [hyper(43,a,28,a,b,17048,a),flip(a)]. 17726 (x ^ y) ^ (1 => (x ^ (y v z))) = x ^ y. [para(16629(a,1),17466(a,1,2,1))]. 18097 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(1640(a,1),16868(a,1,2))]. 18142 (x ^ y) ^ (x ^ (y v z)) = x ^ y. [para(728(a,1),17726(a,1,2))]. 18171 (x ^ y) ^ (x ^ ((x ^ y) v z)) = x ^ (x ^ y). [para(13097(a,1),18142(a,1,1))]. 18209 (1 ^ 1) => ((x v y) => (y v x)) = 1. [para(31(a,1),175(a,1,1,2))]. 18213 (x v y) => (y v x) = 1. [hyper(40,a,10753,a(flip),b,18209,a),flip(a)]. 18216 x v y = y v x. [hyper(43,a,18213,a,b,18213,a)]. 18308 (x v y) ^ y = y. [para(18216(a,1),11287(a,1,1))]. 18320 (x ^ (y v z)) * ~ (z v (x ^ y)) = 0. [para(18216(a,1),16296(a,1,2,1))]. 18535 (x ^ (y v z)) v (x ^ z) = x ^ (y v z). [para(18308(a,1),18097(a,1,2,2))]. 18629 (x ^ (y v z)) ^ (~ (z v (x ^ y)) => 0) = x ^ (y v z). [para(18320(a,1),17044(a,1,2,2))]. 18818 (x ^ (y v z)) v (z ^ x) = x ^ (y v z). [para(16869(a,1),18535(a,1,2))]. 19735 (x ^ y) ^ (x ^ (z v (x ^ y))) = x ^ (x ^ y). [para(18216(a,1),18171(a,1,2,2))]. 19737 (x ^ y) ^ (x ^ (z v (x ^ y))) = x ^ y. [para(19735(a,2),13097(a,1))]. 19833 (x ^ (y v z)) ^ ~ ~ (z v (x ^ y)) = x ^ (y v z). [para(1326(a,1),18629(a,1,2))]. 19834 (x ^ (y v z)) ^ (z v (x ^ y)) = x ^ (y v z). [para(861(a,1),19833(a,1,2))]. 19840 (x ^ ((y ^ z) v (x ^ y))) ^ (x ^ y) = x ^ ((y ^ z) v (x ^ y)). [para(18097(a,1),19834(a,1,2))]. 19950 (x ^ y) ^ (x ^ ((y ^ z) v (x ^ y))) = x ^ ((y ^ z) v (x ^ y)). [para(19840(a,1),16869(a,1)),flip(a)]. 19951 x ^ ((y ^ z) v (x ^ y)) = x ^ y. [para(19950(a,1),19737(a,1))]. 19979 x ^ (y ^ (z v x)) = x ^ y. [para(18818(a,1),19951(a,1,2))]. 20029 x ^ (y ^ (z v x)) = y ^ x. [para(19979(a,2),16869(a,1))]. 20053 (x ^ y) ^ (z ^ x) = z ^ (x ^ y). [para(5572(a,1),20029(a,1,2,2))]. 20110 (x ^ y) ^ (y ^ z) = x ^ (y ^ z). [para(20053(a,1),16869(a,1)),flip(a)]. 20112 (x ^ y) ^ (x ^ z) = z ^ (x ^ y). [para(16869(a,1),20053(a,1,2))]. 20151 (x ^ y) ^ (x ^ z) = y ^ (x ^ z). [para(16869(a,1),20110(a,1,1))]. 20232 x ^ (y ^ z) = z ^ (y ^ x). [para(20151(a,1),20112(a,1))]. 20276 (x ^ y) ^ z = y ^ (x ^ z). [para(20232(a,1),16869(a,1)),flip(a)]. 20370 (x ^ y) ^ z = x ^ (y ^ z). [para(16869(a,1),20276(a,1,1))]. 20371 $F # answer("(D2)"). [resolve(20370,a,51,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 51 given #225 (H,wt=11): 20370 (x ^ y) ^ z = x ^ (y ^ z). [para(16869(a,1),20276(a,1,1))]. % Operation ^ is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 20276 (x ^ y) ^ z = y ^ (x ^ z). [para(20232(a,1),16869(a,1)),flip(a)]. % back CAC tautology: 20232 x ^ (y ^ z) = z ^ (y ^ x). [para(20151(a,1),20112(a,1))]. % back CAC tautology: 20464 (x ^ y) ^ z = x ^ (z ^ y). [para(16869(a,1),20370(a,2,2))]. % back CAC tautology: 20463 (x ^ y) ^ z = (z ^ x) ^ y. [para(20370(a,2),16869(a,1)),flip(a)]. % back CAC tautology: 20372 (x ^ y) ^ z = y ^ (z ^ x). [para(16869(a,1),20276(a,2,2))]. % back CAC tautology: 20369 (x ^ y) ^ z = (x ^ z) ^ y. [para(20276(a,2),16869(a,1))]. % back CAC tautology: 20277 x ^ (y ^ z) = z ^ (x ^ y). [para(16869(a,1),20232(a,1,2)),flip(a)]. % back CAC tautology: 20085 0 ^ (x ^ y) = x ^ (y ^ 0). [para(1506(a,1),20053(a,1,1))]. given #226 (H,wt=14): 20384 ~ x ^ (~ (x ^ y) ^ z) = ~ x ^ z. [para(17877(a,1),20276(a,1,1)),flip(a)]. given #227 (H,wt=14): 20506 ~ x ^ (y ^ ~ (x ^ z)) = ~ x ^ y. [para(16869(a,1),20384(a,1,2))]. given #228 (H,wt=15): 19971 x ^ (y v (x ^ (y v z))) = x ^ (y v z). [para(11287(a,1),19951(a,1,2,1))]. given #229 (H,wt=16): 20291 ~ x ^ (~ y ^ ~ (y v x)) = ~ y ^ ~ x. [para(20232(a,1),19503(a,1))]. given #230 (H,wt=13): 20531 ~ x ^ ~ (y v x) = ~ y ^ ~ x. [para(15170(a,1),20291(a,1,2))]. given #231 (H,wt=10): 20561 ~ x ^ ~ y = ~ (x v y). [para(20531(a,1),18032(a,1))]. given #232 (H,wt=10): 20575 ~ (~ x v y) = x ^ ~ y. [para(861(a,1),20561(a,1,1)),flip(a)]. given #233 (H,wt=10): 20790 ~ (x v ~ y) = y ^ ~ x. [para(18216(a,1),20575(a,1,1))]. given #234 (H,wt=10): 20817 ~ (x ^ ~ y) = y v ~ x. [para(20790(a,1),861(a,1,1))]. given #235 (H,wt=14): 20999 ~ (x ^ (y => ~ z)) = (y * z) v ~ x. [para(1054(a,1),20817(a,1,1,2))]. given #236 (H,wt=15): 20666 ~ x ^ ~ (y v (x ^ z)) = ~ x ^ ~ y. [para(20561(a,1),20506(a,1,2))]. given #237 (H,wt=14): 21103 ~ (x v (y v (x ^ z))) = ~ x ^ ~ y. [para(20666(a,1),20561(a,1)),flip(a)]. given #238 (H,wt=13): 21128 ~ (x v (y v (x ^ z))) = ~ (x v y). [para(21103(a,2),20561(a,1))]. given #239 (H,wt=13): 21129 x v (y v (x ^ z)) = ~ ~ (x v y). [para(21128(a,1),861(a,1,1)),flip(a)]. given #240 (H,wt=11): 21151 x v (y v (x ^ z)) = x v y. [para(21129(a,2),861(a,1))]. given #241 (H,wt=13): 21192 (x v y) v (z v x) = (x v y) v z. [para(11287(a,1),21151(a,1,2,2))]. given #242 (H,wt=13): 21209 (x v y) v (z v y) = (x v y) v z. [para(18308(a,1),21151(a,1,2,2))]. Low Water (keep): wt=14.000, iters=6679 given #243 (H,wt=13): 21240 (x v y) v (x v z) = (x v y) v z. [para(18216(a,1),21192(a,1,2))]. given #244 (H,wt=13): 21256 (x v y) v (y v z) = (x v y) v z. [para(18216(a,1),21209(a,1,2))]. given #245 (H,wt=13): 21279 (x v y) v (x v z) = z v (x v y). [para(21240(a,2),18216(a,1))]. given #246 (H,wt=13): 21323 (x v y) v (x v z) = y v (x v z). [para(21279(a,1),18216(a,1)),flip(a)]. given #247 (H,wt=13): 21348 (x v y) v (y v z) = x v (y v z). [para(18216(a,1),21323(a,1,1))]. -------- Proof 19 -------- "(D1)". ============================== PROOF ================================= % Proof 19 at 1.43 (+ 0.02) seconds: "(D1)". % Length of proof is 176. % Level of proof is 42. % Maximum clause weight is 23. % Given clauses 247. 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 2 (all x all y (x = 1 & y = 1 -> x ^ y = 1)) # label("(4)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 4 (x v y) v z = x v (y v z) # label("(D1)") # label(non_clause) # label(goal). [goal]. 26 x => ((x => y) => y) = 1 # label("(A1)[= 1]"). [assumption]. 27 (x => y) => ((y => z) => (x => z)) = 1 # label("(A2)[= 1]"). [assumption]. 28 (x ^ y) => x = 1 # label("(A3)[= 1]"). [assumption]. 29 (x ^ y) => y = 1 # label("(A4)[= 1]"). [assumption]. 30 ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]"). [assumption]. 31 x => (x v y) = 1 # label("(A6)[= 1]"). [assumption]. 32 x => (y v x) = 1 # label("(A7)[= 1]"). [assumption]. 33 ((x => y) ^ (z => y)) => ((x v z) => y) = 1 # label("(A8)[= 1]"). [assumption]. 34 (x ^ (y v z)) => ((x ^ y) v z) = 1 # label("(A9)[= 1]"). [assumption]. 35 ~ ~ x => x = 1 # label("(A10)[= 1]"). [assumption]. 36 (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). [assumption]. 37 x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. 39 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. 40 1 != x | x => y != 1 | 1 = y. [copy(39),flip(a),flip(c)]. 41 x != 1 | y != 1 | x ^ y = 1 # label("(4)"). [clausify(2)]. 42 1 != x | 1 != y | x ^ y = 1. [copy(41),flip(a),flip(b)]. 43 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 44 x * y = ~ (x => ~ y) # label("(* def)"). [assumption]. 45 ~ (x => ~ y) = x * y. [copy(44),flip(a)]. 46 0 = ~ (x => x) # label("(0 def)"). [assumption]. 47 ~ (x => x) = 0. [copy(46),flip(a)]. 48 1 = x => x # label("(1 def)"). [assumption]. 49 x => x = 1. [copy(48),flip(a)]. 50 (c1 v c2) v c3 != c1 v (c2 v c3) # label("(D1)") # answer("(D1)"). [deny(4)]. 113 (1 ^ ((x ^ y) => z)) => ((x ^ y) => (x ^ z)) = 1. [para(28(a,1),30(a,1,1,1))]. 175 (1 ^ (x => (y v z))) => ((z v x) => (y v z)) = 1. [para(32(a,1),33(a,1,1,1))]. 252 x => 1 = 1. [para(28(a,1),37(a,1,2))]. 366 (x => y) => ((z ^ x) => y) = 1. [hyper(40,a,29,a(flip),b,27,a),flip(a)]. 386 (1 => x) => x = 1. [hyper(40,a,xx,b,26,a),flip(a)]. 583 x => ~ y = y => ~ x. [hyper(43,a,36,a,b,36,a)]. 595 ~ 1 = 0. [para(36(a,1),47(a,1,1))]. 622 (x => x) ^ (y => (y v z)) = 1. [hyper(42,a,49,a(flip),b,31,a(flip))]. 625 (x => x) ^ ((y ^ z) => y) = 1. [hyper(42,a,49,a(flip),b,28,a(flip))]. 630 x => ~ ~ x = 1. [hyper(40,a,49,a(flip),b,36,a),flip(a)]. 640 ((x => y) ^ 1) => (x => (y ^ x)) = 1. [para(49(a,1),30(a,1,1,2))]. 645 ((x => y) ^ 1) => ((x v y) => y) = 1. [para(49(a,1),33(a,1,1,2))]. 674 (x => x) ^ (y => 1) = 1. [hyper(42,a,49,a(flip),b,252,a(flip))]. 728 1 => x = x. [hyper(43,a,37,a,b,386,a)]. 861 ~ ~ x = x. [hyper(43,a,35,a,b,630,a),flip(a)]. 1017 x => ~ ~ (y v x) = 1. [para(861(a,2),32(a,1,2))]. 1050 ~ (x => y) = x * ~ y. [para(861(a,1),45(a,1,1,2))]. 1054 ~ (x * y) = x => ~ y. [para(45(a,1),861(a,1,1))]. 1263 x => ((y => ~ x) => ~ y) = 1. [para(583(a,1),26(a,1,2,1))]. 1264 x => (y => ~ (x => ~ y)) = 1. [para(583(a,1),26(a,1,2))]. 1277 ~ (x => ~ y) = y * x. [para(583(a,1),45(a,1,1))]. 1281 x => ~ 1 = ~ x. [para(583(a,1),728(a,1))]. 1283 ~ x => ~ y = y => x. [para(861(a,1),583(a,1,2)),flip(a)]. 1321 ~ ~ x = x * 1. [para(1281(a,1),45(a,1,1))]. 1326 x => 0 = ~ x. [para(595(a,1),1281(a,1,2))]. 1347 (~ x ^ (y => 0)) => ((x v y) => 0) = 1. [para(1326(a,1),33(a,1,1,1))]. 1640 x * 1 = x. [para(1321(a,1),861(a,1))]. 2448 x => (x ^ 1) = 1. [hyper(40,a,674,a(flip),b,30,a),flip(a)]. 2521 x ^ 1 = x. [hyper(43,a,28,a,b,2448,a),flip(a)]. 2860 ~ (x v y) => ~ y = 1. [hyper(40,a,1017,a(flip),b,36,a),flip(a)]. 2932 x * ~ ((x => y) => y) = ~ 1. [para(26(a,1),1050(a,1,1)),flip(a)]. 2934 (x ^ y) * ~ x = ~ 1. [para(28(a,1),1050(a,1,1)),flip(a)]. 2935 (x ^ y) * ~ y = ~ 1. [para(29(a,1),1050(a,1,1)),flip(a)]. 2939 (x ^ (y v z)) * ~ ((x ^ y) v z) = ~ 1. [para(34(a,1),1050(a,1,1)),flip(a)]. 3031 ~ (x * y) = y => ~ x. [para(1054(a,2),583(a,1))]. 3064 x * y = y * x. [para(1277(a,1),45(a,1))]. 3369 (x ^ y) * ~ x = 0. [para(2934(a,2),595(a,1))]. 3491 (x ^ y) * ~ y = 0. [para(2935(a,2),595(a,1))]. 3596 ~ x * (y ^ x) = 0. [para(3491(a,1),3064(a,1)),flip(a)]. 3736 (x ^ y) => (y v z) = 1. [hyper(40,a,31,a(flip),b,366,a),flip(a)]. 3739 (x ^ (y ^ z)) => y = 1. [hyper(40,a,28,a(flip),b,366,a),flip(a)]. 4812 x => (x ^ (x v y)) = 1. [hyper(40,a,622,a(flip),b,30,a),flip(a)]. 4893 x ^ (x v y) = x. [hyper(43,a,28,a,b,4812,a),flip(a)]. 5322 x * ~ (x v y) = 0. [para(4893(a,1),3491(a,1,1))]. 5480 (x v (x ^ y)) => x = 1. [hyper(40,a,625,a(flip),b,33,a),flip(a)]. 5572 x v (x ^ y) = x. [hyper(43,a,31,a,b,5480,a)]. 6326 x => ~ (y * (y => ~ x)) = 1. [para(3031(a,2),1263(a,1,2))]. 6588 x => (y => (y * x)) = 1. [para(1277(a,1),1264(a,1,2,2))]. 6888 x * ~ ((x => y) => y) = 0. [para(2932(a,2),595(a,1))]. 7073 x * (y * (x => ~ y)) = 0. [para(1277(a,1),6888(a,1,2))]. 7267 ~ (x v y) * (y * 1) = 0. [para(2860(a,1),7073(a,1,2,2))]. 7336 ~ (x v y) * y = 0. [para(1640(a,1),7267(a,1,2))]. 7422 x * ~ (y v x) = 0. [para(7336(a,1),3064(a,1)),flip(a)]. 7667 ~ x => ~ (y * (y => x)) = 1. [para(861(a,1),6326(a,1,2,1,2,2))]. 7991 (x * (x => y)) => y = 1. [para(7667(a,1),1283(a,1)),flip(a)]. 9898 (x => y) => (x => (y ^ x)) = 1. [para(2521(a,1),640(a,1,1))]. 10006 x => ((y => (y * x)) ^ x) = 1. [hyper(40,a,6588,a(flip),b,9898,a),flip(a)]. 10031 x => ((y => x) ^ x) = 1. [hyper(40,a,37,a(flip),b,9898,a),flip(a)]. 10037 x => ((x v y) ^ x) = 1. [hyper(40,a,31,a(flip),b,9898,a),flip(a)]. 10040 (x ^ y) => (x ^ (x ^ y)) = 1. [hyper(40,a,28,a(flip),b,9898,a),flip(a)]. 10042 x => (((x => y) => y) ^ x) = 1. [hyper(40,a,26,a(flip),b,9898,a),flip(a)]. 10326 (x => y) ^ y = y. [hyper(43,a,29,a,b,10031,a),flip(a)]. 10753 1 ^ x = x. [para(28(a,1),10326(a,1,1))]. 11287 (x v y) ^ x = x. [hyper(43,a,29,a,b,10037,a),flip(a)]. 12015 (x => (x * y)) ^ y = y. [hyper(43,a,29,a,b,10006,a),flip(a)]. 12549 (x => (y * x)) ^ y = y. [para(3064(a,1),12015(a,1,1,2))]. 12578 (~ x => 0) ^ (y ^ x) = y ^ x. [para(3596(a,1),12015(a,1,1,2))]. 12606 (x => 0) ^ ~ (x v y) = ~ (x v y). [para(5322(a,1),12015(a,1,1,2))]. 13097 x ^ (x ^ y) = x ^ y. [hyper(43,a,29,a,b,10040,a),flip(a)]. 13528 ~ ~ x ^ (y ^ x) = y ^ x. [para(1326(a,1),12578(a,1,1))]. 13639 x ^ (y ^ x) = y ^ x. [para(861(a,1),13528(a,1,1))]. 13776 x v (y ^ x) = x. [para(13639(a,1),5572(a,1,2))]. 14367 (x => y) => ((x v y) => y) = 1. [para(2521(a,1),645(a,1,1))]. 14410 ((x * (x => y)) v y) => y = 1. [hyper(40,a,7991,a(flip),b,14367,a),flip(a)]. 14629 (x * (x => y)) v y = y. [hyper(43,a,32,a,b,14410,a)]. 14979 (x * (x => y)) ^ y = x * (x => y). [para(14629(a,1),4893(a,1,2))]. 15170 ~ x ^ ~ (x v y) = ~ (x v y). [para(1326(a,1),12606(a,1,1))]. 15370 x v (y * (y => x)) = x. [para(14979(a,1),13776(a,1,2))]. 15670 (~ x ^ ~ y) => ((x v y) => 0) = 1. [para(1326(a,1),1347(a,1,1,2))]. 15750 (~ x ^ ~ y) => ~ (x v y) = 1. [para(1326(a,1),15670(a,1,2))]. 15901 (x v y) * (~ x ^ ~ y) = ~ 1. [para(15750(a,1),1277(a,1,1)),flip(a)]. 15944 (x v y) * (~ x ^ ~ y) = 0. [para(15901(a,2),595(a,1))]. 16138 ((x v y) => 0) ^ (~ x ^ ~ y) = ~ x ^ ~ y. [para(15944(a,1),12015(a,1,1,2))]. 16296 (x ^ (y v z)) * ~ ((x ^ y) v z) = 0. [para(2939(a,2),595(a,1))]. 16378 (1 ^ 1) => ((x ^ y) => (x ^ (y v z))) = 1. [para(3736(a,1),113(a,1,1,2))]. 16379 (1 ^ 1) => ((x ^ (y ^ z)) => (x ^ y)) = 1. [para(3739(a,1),113(a,1,1,2))]. 16629 (x ^ y) => (x ^ (y v z)) = 1. [hyper(40,a,10753,a(flip),b,16378,a),flip(a)]. 16751 (x ^ (y ^ z)) => (x ^ y) = 1. [hyper(40,a,10753,a(flip),b,16379,a),flip(a)]. 16862 (x ^ y) => (y ^ x) = 1. [para(13639(a,1),16751(a,1,1))]. 16868 (x ^ y) v ((x ^ (y ^ z)) * 1) = x ^ y. [para(16751(a,1),15370(a,1,2,2))]. 16869 x ^ y = y ^ x. [hyper(43,a,16862,a,b,16862,a)]. 17043 x ^ (y => (y * x)) = x. [para(16869(a,1),12015(a,1))]. 17044 x ^ (y => (x * y)) = x. [para(16869(a,1),12549(a,1))]. 17048 x => (x ^ ((x => y) => y)) = 1. [para(16869(a,1),10042(a,1,2))]. 17224 ~ x ^ ((x ^ y) => 0) = ~ x. [para(3369(a,1),17043(a,1,2,2))]. 17245 ~ (x v y) ^ (y => 0) = ~ (x v y). [para(7422(a,1),17043(a,1,2,2))]. 17466 x ^ ((x => y) => y) = x. [hyper(43,a,28,a,b,17048,a),flip(a)]. 17726 (x ^ y) ^ (1 => (x ^ (y v z))) = x ^ y. [para(16629(a,1),17466(a,1,2,1))]. 17755 ~ x ^ ~ (x ^ y) = ~ x. [para(1326(a,1),17224(a,1,2))]. 17877 ~ (x ^ y) ^ ~ x = ~ x. [para(17755(a,1),16869(a,1)),flip(a)]. 17962 ~ (x v y) ^ ~ y = ~ (x v y). [para(1326(a,1),17245(a,1,2))]. 18032 ~ x ^ ~ (y v x) = ~ (y v x). [para(17962(a,1),16869(a,1)),flip(a)]. 18097 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(1640(a,1),16868(a,1,2))]. 18142 (x ^ y) ^ (x ^ (y v z)) = x ^ y. [para(728(a,1),17726(a,1,2))]. 18171 (x ^ y) ^ (x ^ ((x ^ y) v z)) = x ^ (x ^ y). [para(13097(a,1),18142(a,1,1))]. 18209 (1 ^ 1) => ((x v y) => (y v x)) = 1. [para(31(a,1),175(a,1,1,2))]. 18213 (x v y) => (y v x) = 1. [hyper(40,a,10753,a(flip),b,18209,a),flip(a)]. 18216 x v y = y v x. [hyper(43,a,18213,a,b,18213,a)]. 18308 (x v y) ^ y = y. [para(18216(a,1),11287(a,1,1))]. 18320 (x ^ (y v z)) * ~ (z v (x ^ y)) = 0. [para(18216(a,1),16296(a,1,2,1))]. 18535 (x ^ (y v z)) v (x ^ z) = x ^ (y v z). [para(18308(a,1),18097(a,1,2,2))]. 18629 (x ^ (y v z)) ^ (~ (z v (x ^ y)) => 0) = x ^ (y v z). [para(18320(a,1),17044(a,1,2,2))]. 18818 (x ^ (y v z)) v (z ^ x) = x ^ (y v z). [para(16869(a,1),18535(a,1,2))]. 19503 ~ (x v y) ^ (~ x ^ ~ y) = ~ x ^ ~ y. [para(1326(a,1),16138(a,1,1))]. 19735 (x ^ y) ^ (x ^ (z v (x ^ y))) = x ^ (x ^ y). [para(18216(a,1),18171(a,1,2,2))]. 19737 (x ^ y) ^ (x ^ (z v (x ^ y))) = x ^ y. [para(19735(a,2),13097(a,1))]. 19833 (x ^ (y v z)) ^ ~ ~ (z v (x ^ y)) = x ^ (y v z). [para(1326(a,1),18629(a,1,2))]. 19834 (x ^ (y v z)) ^ (z v (x ^ y)) = x ^ (y v z). [para(861(a,1),19833(a,1,2))]. 19840 (x ^ ((y ^ z) v (x ^ y))) ^ (x ^ y) = x ^ ((y ^ z) v (x ^ y)). [para(18097(a,1),19834(a,1,2))]. 19950 (x ^ y) ^ (x ^ ((y ^ z) v (x ^ y))) = x ^ ((y ^ z) v (x ^ y)). [para(19840(a,1),16869(a,1)),flip(a)]. 19951 x ^ ((y ^ z) v (x ^ y)) = x ^ y. [para(19950(a,1),19737(a,1))]. 19979 x ^ (y ^ (z v x)) = x ^ y. [para(18818(a,1),19951(a,1,2))]. 20029 x ^ (y ^ (z v x)) = y ^ x. [para(19979(a,2),16869(a,1))]. 20053 (x ^ y) ^ (z ^ x) = z ^ (x ^ y). [para(5572(a,1),20029(a,1,2,2))]. 20110 (x ^ y) ^ (y ^ z) = x ^ (y ^ z). [para(20053(a,1),16869(a,1)),flip(a)]. 20112 (x ^ y) ^ (x ^ z) = z ^ (x ^ y). [para(16869(a,1),20053(a,1,2))]. 20151 (x ^ y) ^ (x ^ z) = y ^ (x ^ z). [para(16869(a,1),20110(a,1,1))]. 20232 x ^ (y ^ z) = z ^ (y ^ x). [para(20151(a,1),20112(a,1))]. 20276 (x ^ y) ^ z = y ^ (x ^ z). [para(20232(a,1),16869(a,1)),flip(a)]. 20291 ~ x ^ (~ y ^ ~ (y v x)) = ~ y ^ ~ x. [para(20232(a,1),19503(a,1))]. 20384 ~ x ^ (~ (x ^ y) ^ z) = ~ x ^ z. [para(17877(a,1),20276(a,1,1)),flip(a)]. 20506 ~ x ^ (y ^ ~ (x ^ z)) = ~ x ^ y. [para(16869(a,1),20384(a,1,2))]. 20531 ~ x ^ ~ (y v x) = ~ y ^ ~ x. [para(15170(a,1),20291(a,1,2))]. 20561 ~ x ^ ~ y = ~ (x v y). [para(20531(a,1),18032(a,1))]. 20666 ~ x ^ ~ (y v (x ^ z)) = ~ x ^ ~ y. [para(20561(a,1),20506(a,1,2))]. 21103 ~ (x v (y v (x ^ z))) = ~ x ^ ~ y. [para(20666(a,1),20561(a,1)),flip(a)]. 21128 ~ (x v (y v (x ^ z))) = ~ (x v y). [para(21103(a,2),20561(a,1))]. 21129 x v (y v (x ^ z)) = ~ ~ (x v y). [para(21128(a,1),861(a,1,1)),flip(a)]. 21151 x v (y v (x ^ z)) = x v y. [para(21129(a,2),861(a,1))]. 21192 (x v y) v (z v x) = (x v y) v z. [para(11287(a,1),21151(a,1,2,2))]. 21209 (x v y) v (z v y) = (x v y) v z. [para(18308(a,1),21151(a,1,2,2))]. 21240 (x v y) v (x v z) = (x v y) v z. [para(18216(a,1),21192(a,1,2))]. 21256 (x v y) v (y v z) = (x v y) v z. [para(18216(a,1),21209(a,1,2))]. 21279 (x v y) v (x v z) = z v (x v y). [para(21240(a,2),18216(a,1))]. 21323 (x v y) v (x v z) = y v (x v z). [para(21279(a,1),18216(a,1)),flip(a)]. 21348 (x v y) v (y v z) = x v (y v z). [para(18216(a,1),21323(a,1,1))]. 21376 (x v y) v z = x v (y v z). [para(21348(a,1),21256(a,1)),flip(a)]. 21377 $F # answer("(D1)"). [resolve(21376,a,50,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 50 given #248 (H,wt=11): 21376 (x v y) v z = x v (y v z). [para(21348(a,1),21256(a,1)),flip(a)]. given #249 (H,wt=17): 21436 x v ((y ^ z) v (y ^ (z v x))) = x v (y ^ z). [para(21376(a,1),19838(a,1))]. given #250 (H,wt=13): 21460 x v (y ^ (z v x)) = x v (y ^ z). [para(18328(a,1),21436(a,1,2))]. given #251 (H,wt=13): 21479 x v (y ^ (x v z)) = x v (y ^ z). [para(18216(a,1),21460(a,1,2,2))]. given #252 (H,wt=13): 21499 x ^ (y v (x ^ z)) = x ^ (y v z). [para(21479(a,1),19971(a,1,2))]. given #253 (H,wt=13): 21511 x ^ (y v (z ^ x)) = x ^ (y v z). [para(16869(a,1),21499(a,1,2,2))]. Low Water (displace): id=11333, wt=37.000 Low Water (displace): id=21526, wt=13.000 given #254 (H,wt=13): 21513 x ^ (y v (x ^ z)) = x ^ (z v y). [para(18216(a,1),21499(a,2,2))]. Low Water (displace): id=21538, wt=9.000 given #255 (H,wt=15): 21481 (x ^ y) v (x ^ z) = x ^ (z v (x ^ y)). [para(21460(a,1),18837(a,1))]. -------- Proof 20 -------- "(D12)". ============================== PROOF ================================= % Proof 20 at 1.48 (+ 0.02) seconds: "(D12)". % Length of proof is 190. % Level of proof is 48. % Maximum clause weight is 23. % Given clauses 255. 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 2 (all x all y (x = 1 & y = 1 -> x ^ y = 1)) # label("(4)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 23 (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D12)") # label(non_clause) # label(goal). [goal]. 26 x => ((x => y) => y) = 1 # label("(A1)[= 1]"). [assumption]. 27 (x => y) => ((y => z) => (x => z)) = 1 # label("(A2)[= 1]"). [assumption]. 28 (x ^ y) => x = 1 # label("(A3)[= 1]"). [assumption]. 29 (x ^ y) => y = 1 # label("(A4)[= 1]"). [assumption]. 30 ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]"). [assumption]. 31 x => (x v y) = 1 # label("(A6)[= 1]"). [assumption]. 32 x => (y v x) = 1 # label("(A7)[= 1]"). [assumption]. 33 ((x => y) ^ (z => y)) => ((x v z) => y) = 1 # label("(A8)[= 1]"). [assumption]. 34 (x ^ (y v z)) => ((x ^ y) v z) = 1 # label("(A9)[= 1]"). [assumption]. 35 ~ ~ x => x = 1 # label("(A10)[= 1]"). [assumption]. 36 (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). [assumption]. 37 x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. 39 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. 40 1 != x | x => y != 1 | 1 = y. [copy(39),flip(a),flip(c)]. 41 x != 1 | y != 1 | x ^ y = 1 # label("(4)"). [clausify(2)]. 42 1 != x | 1 != y | x ^ y = 1. [copy(41),flip(a),flip(b)]. 43 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 44 x * y = ~ (x => ~ y) # label("(* def)"). [assumption]. 45 ~ (x => ~ y) = x * y. [copy(44),flip(a)]. 46 0 = ~ (x => x) # label("(0 def)"). [assumption]. 47 ~ (x => x) = 0. [copy(46),flip(a)]. 48 1 = x => x # label("(1 def)"). [assumption]. 49 x => x = 1. [copy(48),flip(a)]. 71 (c40 ^ c41) v (c40 ^ c42) != c40 ^ (c41 v c42) # label("(D12)") # answer("(D12)"). [deny(23)]. 113 (1 ^ ((x ^ y) => z)) => ((x ^ y) => (x ^ z)) = 1. [para(28(a,1),30(a,1,1,1))]. 175 (1 ^ (x => (y v z))) => ((z v x) => (y v z)) = 1. [para(32(a,1),33(a,1,1,1))]. 252 x => 1 = 1. [para(28(a,1),37(a,1,2))]. 366 (x => y) => ((z ^ x) => y) = 1. [hyper(40,a,29,a(flip),b,27,a),flip(a)]. 386 (1 => x) => x = 1. [hyper(40,a,xx,b,26,a),flip(a)]. 583 x => ~ y = y => ~ x. [hyper(43,a,36,a,b,36,a)]. 595 ~ 1 = 0. [para(36(a,1),47(a,1,1))]. 622 (x => x) ^ (y => (y v z)) = 1. [hyper(42,a,49,a(flip),b,31,a(flip))]. 625 (x => x) ^ ((y ^ z) => y) = 1. [hyper(42,a,49,a(flip),b,28,a(flip))]. 630 x => ~ ~ x = 1. [hyper(40,a,49,a(flip),b,36,a),flip(a)]. 640 ((x => y) ^ 1) => (x => (y ^ x)) = 1. [para(49(a,1),30(a,1,1,2))]. 645 ((x => y) ^ 1) => ((x v y) => y) = 1. [para(49(a,1),33(a,1,1,2))]. 674 (x => x) ^ (y => 1) = 1. [hyper(42,a,49,a(flip),b,252,a(flip))]. 728 1 => x = x. [hyper(43,a,37,a,b,386,a)]. 861 ~ ~ x = x. [hyper(43,a,35,a,b,630,a),flip(a)]. 1017 x => ~ ~ (y v x) = 1. [para(861(a,2),32(a,1,2))]. 1050 ~ (x => y) = x * ~ y. [para(861(a,1),45(a,1,1,2))]. 1054 ~ (x * y) = x => ~ y. [para(45(a,1),861(a,1,1))]. 1263 x => ((y => ~ x) => ~ y) = 1. [para(583(a,1),26(a,1,2,1))]. 1264 x => (y => ~ (x => ~ y)) = 1. [para(583(a,1),26(a,1,2))]. 1277 ~ (x => ~ y) = y * x. [para(583(a,1),45(a,1,1))]. 1281 x => ~ 1 = ~ x. [para(583(a,1),728(a,1))]. 1283 ~ x => ~ y = y => x. [para(861(a,1),583(a,1,2)),flip(a)]. 1321 ~ ~ x = x * 1. [para(1281(a,1),45(a,1,1))]. 1326 x => 0 = ~ x. [para(595(a,1),1281(a,1,2))]. 1347 (~ x ^ (y => 0)) => ((x v y) => 0) = 1. [para(1326(a,1),33(a,1,1,1))]. 1640 x * 1 = x. [para(1321(a,1),861(a,1))]. 2448 x => (x ^ 1) = 1. [hyper(40,a,674,a(flip),b,30,a),flip(a)]. 2521 x ^ 1 = x. [hyper(43,a,28,a,b,2448,a),flip(a)]. 2860 ~ (x v y) => ~ y = 1. [hyper(40,a,1017,a(flip),b,36,a),flip(a)]. 2932 x * ~ ((x => y) => y) = ~ 1. [para(26(a,1),1050(a,1,1)),flip(a)]. 2934 (x ^ y) * ~ x = ~ 1. [para(28(a,1),1050(a,1,1)),flip(a)]. 2935 (x ^ y) * ~ y = ~ 1. [para(29(a,1),1050(a,1,1)),flip(a)]. 2939 (x ^ (y v z)) * ~ ((x ^ y) v z) = ~ 1. [para(34(a,1),1050(a,1,1)),flip(a)]. 3031 ~ (x * y) = y => ~ x. [para(1054(a,2),583(a,1))]. 3064 x * y = y * x. [para(1277(a,1),45(a,1))]. 3369 (x ^ y) * ~ x = 0. [para(2934(a,2),595(a,1))]. 3491 (x ^ y) * ~ y = 0. [para(2935(a,2),595(a,1))]. 3596 ~ x * (y ^ x) = 0. [para(3491(a,1),3064(a,1)),flip(a)]. 3736 (x ^ y) => (y v z) = 1. [hyper(40,a,31,a(flip),b,366,a),flip(a)]. 3739 (x ^ (y ^ z)) => y = 1. [hyper(40,a,28,a(flip),b,366,a),flip(a)]. 4812 x => (x ^ (x v y)) = 1. [hyper(40,a,622,a(flip),b,30,a),flip(a)]. 4893 x ^ (x v y) = x. [hyper(43,a,28,a,b,4812,a),flip(a)]. 5322 x * ~ (x v y) = 0. [para(4893(a,1),3491(a,1,1))]. 5480 (x v (x ^ y)) => x = 1. [hyper(40,a,625,a(flip),b,33,a),flip(a)]. 5572 x v (x ^ y) = x. [hyper(43,a,31,a,b,5480,a)]. 6326 x => ~ (y * (y => ~ x)) = 1. [para(3031(a,2),1263(a,1,2))]. 6588 x => (y => (y * x)) = 1. [para(1277(a,1),1264(a,1,2,2))]. 6888 x * ~ ((x => y) => y) = 0. [para(2932(a,2),595(a,1))]. 7073 x * (y * (x => ~ y)) = 0. [para(1277(a,1),6888(a,1,2))]. 7267 ~ (x v y) * (y * 1) = 0. [para(2860(a,1),7073(a,1,2,2))]. 7336 ~ (x v y) * y = 0. [para(1640(a,1),7267(a,1,2))]. 7422 x * ~ (y v x) = 0. [para(7336(a,1),3064(a,1)),flip(a)]. 7667 ~ x => ~ (y * (y => x)) = 1. [para(861(a,1),6326(a,1,2,1,2,2))]. 7991 (x * (x => y)) => y = 1. [para(7667(a,1),1283(a,1)),flip(a)]. 9898 (x => y) => (x => (y ^ x)) = 1. [para(2521(a,1),640(a,1,1))]. 10006 x => ((y => (y * x)) ^ x) = 1. [hyper(40,a,6588,a(flip),b,9898,a),flip(a)]. 10031 x => ((y => x) ^ x) = 1. [hyper(40,a,37,a(flip),b,9898,a),flip(a)]. 10037 x => ((x v y) ^ x) = 1. [hyper(40,a,31,a(flip),b,9898,a),flip(a)]. 10040 (x ^ y) => (x ^ (x ^ y)) = 1. [hyper(40,a,28,a(flip),b,9898,a),flip(a)]. 10042 x => (((x => y) => y) ^ x) = 1. [hyper(40,a,26,a(flip),b,9898,a),flip(a)]. 10326 (x => y) ^ y = y. [hyper(43,a,29,a,b,10031,a),flip(a)]. 10753 1 ^ x = x. [para(28(a,1),10326(a,1,1))]. 11287 (x v y) ^ x = x. [hyper(43,a,29,a,b,10037,a),flip(a)]. 12015 (x => (x * y)) ^ y = y. [hyper(43,a,29,a,b,10006,a),flip(a)]. 12549 (x => (y * x)) ^ y = y. [para(3064(a,1),12015(a,1,1,2))]. 12578 (~ x => 0) ^ (y ^ x) = y ^ x. [para(3596(a,1),12015(a,1,1,2))]. 12606 (x => 0) ^ ~ (x v y) = ~ (x v y). [para(5322(a,1),12015(a,1,1,2))]. 13097 x ^ (x ^ y) = x ^ y. [hyper(43,a,29,a,b,10040,a),flip(a)]. 13528 ~ ~ x ^ (y ^ x) = y ^ x. [para(1326(a,1),12578(a,1,1))]. 13639 x ^ (y ^ x) = y ^ x. [para(861(a,1),13528(a,1,1))]. 13776 x v (y ^ x) = x. [para(13639(a,1),5572(a,1,2))]. 14367 (x => y) => ((x v y) => y) = 1. [para(2521(a,1),645(a,1,1))]. 14410 ((x * (x => y)) v y) => y = 1. [hyper(40,a,7991,a(flip),b,14367,a),flip(a)]. 14629 (x * (x => y)) v y = y. [hyper(43,a,32,a,b,14410,a)]. 14979 (x * (x => y)) ^ y = x * (x => y). [para(14629(a,1),4893(a,1,2))]. 15170 ~ x ^ ~ (x v y) = ~ (x v y). [para(1326(a,1),12606(a,1,1))]. 15370 x v (y * (y => x)) = x. [para(14979(a,1),13776(a,1,2))]. 15670 (~ x ^ ~ y) => ((x v y) => 0) = 1. [para(1326(a,1),1347(a,1,1,2))]. 15750 (~ x ^ ~ y) => ~ (x v y) = 1. [para(1326(a,1),15670(a,1,2))]. 15901 (x v y) * (~ x ^ ~ y) = ~ 1. [para(15750(a,1),1277(a,1,1)),flip(a)]. 15944 (x v y) * (~ x ^ ~ y) = 0. [para(15901(a,2),595(a,1))]. 16138 ((x v y) => 0) ^ (~ x ^ ~ y) = ~ x ^ ~ y. [para(15944(a,1),12015(a,1,1,2))]. 16296 (x ^ (y v z)) * ~ ((x ^ y) v z) = 0. [para(2939(a,2),595(a,1))]. 16378 (1 ^ 1) => ((x ^ y) => (x ^ (y v z))) = 1. [para(3736(a,1),113(a,1,1,2))]. 16379 (1 ^ 1) => ((x ^ (y ^ z)) => (x ^ y)) = 1. [para(3739(a,1),113(a,1,1,2))]. 16629 (x ^ y) => (x ^ (y v z)) = 1. [hyper(40,a,10753,a(flip),b,16378,a),flip(a)]. 16751 (x ^ (y ^ z)) => (x ^ y) = 1. [hyper(40,a,10753,a(flip),b,16379,a),flip(a)]. 16862 (x ^ y) => (y ^ x) = 1. [para(13639(a,1),16751(a,1,1))]. 16868 (x ^ y) v ((x ^ (y ^ z)) * 1) = x ^ y. [para(16751(a,1),15370(a,1,2,2))]. 16869 x ^ y = y ^ x. [hyper(43,a,16862,a,b,16862,a)]. 17043 x ^ (y => (y * x)) = x. [para(16869(a,1),12015(a,1))]. 17044 x ^ (y => (x * y)) = x. [para(16869(a,1),12549(a,1))]. 17048 x => (x ^ ((x => y) => y)) = 1. [para(16869(a,1),10042(a,1,2))]. 17224 ~ x ^ ((x ^ y) => 0) = ~ x. [para(3369(a,1),17043(a,1,2,2))]. 17245 ~ (x v y) ^ (y => 0) = ~ (x v y). [para(7422(a,1),17043(a,1,2,2))]. 17466 x ^ ((x => y) => y) = x. [hyper(43,a,28,a,b,17048,a),flip(a)]. 17726 (x ^ y) ^ (1 => (x ^ (y v z))) = x ^ y. [para(16629(a,1),17466(a,1,2,1))]. 17755 ~ x ^ ~ (x ^ y) = ~ x. [para(1326(a,1),17224(a,1,2))]. 17877 ~ (x ^ y) ^ ~ x = ~ x. [para(17755(a,1),16869(a,1)),flip(a)]. 17962 ~ (x v y) ^ ~ y = ~ (x v y). [para(1326(a,1),17245(a,1,2))]. 18032 ~ x ^ ~ (y v x) = ~ (y v x). [para(17962(a,1),16869(a,1)),flip(a)]. 18097 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(1640(a,1),16868(a,1,2))]. 18134 (x ^ (y v z)) v (x ^ y) = x ^ (y v z). [para(11287(a,1),18097(a,1,2,2))]. 18142 (x ^ y) ^ (x ^ (y v z)) = x ^ y. [para(728(a,1),17726(a,1,2))]. 18171 (x ^ y) ^ (x ^ ((x ^ y) v z)) = x ^ (x ^ y). [para(13097(a,1),18142(a,1,1))]. 18209 (1 ^ 1) => ((x v y) => (y v x)) = 1. [para(31(a,1),175(a,1,1,2))]. 18213 (x v y) => (y v x) = 1. [hyper(40,a,10753,a(flip),b,18209,a),flip(a)]. 18216 x v y = y v x. [hyper(43,a,18213,a,b,18213,a)]. 18308 (x v y) ^ y = y. [para(18216(a,1),11287(a,1,1))]. 18320 (x ^ (y v z)) * ~ (z v (x ^ y)) = 0. [para(18216(a,1),16296(a,1,2,1))]. 18326 (x ^ (y ^ z)) v (x ^ y) = x ^ y. [para(18216(a,1),18097(a,1))]. 18328 (x ^ y) v (x ^ (y v z)) = x ^ (y v z). [para(18216(a,1),18134(a,1))]. 18535 (x ^ (y v z)) v (x ^ z) = x ^ (y v z). [para(18308(a,1),18097(a,1,2,2))]. 18611 (x ^ y) v (x ^ (z v y)) = x ^ (z v y). [para(18308(a,1),18326(a,1,1,2))]. 18629 (x ^ (y v z)) ^ (~ (z v (x ^ y)) => 0) = x ^ (y v z). [para(18320(a,1),17044(a,1,2,2))]. 18818 (x ^ (y v z)) v (z ^ x) = x ^ (y v z). [para(16869(a,1),18535(a,1,2))]. 18837 (x ^ y) v (x ^ (z v (x ^ y))) = x ^ (z v (x ^ y)). [para(13097(a,1),18611(a,1,1))]. 19503 ~ (x v y) ^ (~ x ^ ~ y) = ~ x ^ ~ y. [para(1326(a,1),16138(a,1,1))]. 19735 (x ^ y) ^ (x ^ (z v (x ^ y))) = x ^ (x ^ y). [para(18216(a,1),18171(a,1,2,2))]. 19737 (x ^ y) ^ (x ^ (z v (x ^ y))) = x ^ y. [para(19735(a,2),13097(a,1))]. 19833 (x ^ (y v z)) ^ ~ ~ (z v (x ^ y)) = x ^ (y v z). [para(1326(a,1),18629(a,1,2))]. 19834 (x ^ (y v z)) ^ (z v (x ^ y)) = x ^ (y v z). [para(861(a,1),19833(a,1,2))]. 19838 (x v (y ^ z)) v (y ^ (z v x)) = x v (y ^ z). [para(19834(a,1),13776(a,1,2))]. 19840 (x ^ ((y ^ z) v (x ^ y))) ^ (x ^ y) = x ^ ((y ^ z) v (x ^ y)). [para(18097(a,1),19834(a,1,2))]. 19950 (x ^ y) ^ (x ^ ((y ^ z) v (x ^ y))) = x ^ ((y ^ z) v (x ^ y)). [para(19840(a,1),16869(a,1)),flip(a)]. 19951 x ^ ((y ^ z) v (x ^ y)) = x ^ y. [para(19950(a,1),19737(a,1))]. 19971 x ^ (y v (x ^ (y v z))) = x ^ (y v z). [para(11287(a,1),19951(a,1,2,1))]. 19979 x ^ (y ^ (z v x)) = x ^ y. [para(18818(a,1),19951(a,1,2))]. 20029 x ^ (y ^ (z v x)) = y ^ x. [para(19979(a,2),16869(a,1))]. 20053 (x ^ y) ^ (z ^ x) = z ^ (x ^ y). [para(5572(a,1),20029(a,1,2,2))]. 20110 (x ^ y) ^ (y ^ z) = x ^ (y ^ z). [para(20053(a,1),16869(a,1)),flip(a)]. 20112 (x ^ y) ^ (x ^ z) = z ^ (x ^ y). [para(16869(a,1),20053(a,1,2))]. 20151 (x ^ y) ^ (x ^ z) = y ^ (x ^ z). [para(16869(a,1),20110(a,1,1))]. 20232 x ^ (y ^ z) = z ^ (y ^ x). [para(20151(a,1),20112(a,1))]. 20276 (x ^ y) ^ z = y ^ (x ^ z). [para(20232(a,1),16869(a,1)),flip(a)]. 20291 ~ x ^ (~ y ^ ~ (y v x)) = ~ y ^ ~ x. [para(20232(a,1),19503(a,1))]. 20384 ~ x ^ (~ (x ^ y) ^ z) = ~ x ^ z. [para(17877(a,1),20276(a,1,1)),flip(a)]. 20506 ~ x ^ (y ^ ~ (x ^ z)) = ~ x ^ y. [para(16869(a,1),20384(a,1,2))]. 20531 ~ x ^ ~ (y v x) = ~ y ^ ~ x. [para(15170(a,1),20291(a,1,2))]. 20561 ~ x ^ ~ y = ~ (x v y). [para(20531(a,1),18032(a,1))]. 20666 ~ x ^ ~ (y v (x ^ z)) = ~ x ^ ~ y. [para(20561(a,1),20506(a,1,2))]. 21103 ~ (x v (y v (x ^ z))) = ~ x ^ ~ y. [para(20666(a,1),20561(a,1)),flip(a)]. 21128 ~ (x v (y v (x ^ z))) = ~ (x v y). [para(21103(a,2),20561(a,1))]. 21129 x v (y v (x ^ z)) = ~ ~ (x v y). [para(21128(a,1),861(a,1,1)),flip(a)]. 21151 x v (y v (x ^ z)) = x v y. [para(21129(a,2),861(a,1))]. 21192 (x v y) v (z v x) = (x v y) v z. [para(11287(a,1),21151(a,1,2,2))]. 21209 (x v y) v (z v y) = (x v y) v z. [para(18308(a,1),21151(a,1,2,2))]. 21240 (x v y) v (x v z) = (x v y) v z. [para(18216(a,1),21192(a,1,2))]. 21256 (x v y) v (y v z) = (x v y) v z. [para(18216(a,1),21209(a,1,2))]. 21279 (x v y) v (x v z) = z v (x v y). [para(21240(a,2),18216(a,1))]. 21323 (x v y) v (x v z) = y v (x v z). [para(21279(a,1),18216(a,1)),flip(a)]. 21348 (x v y) v (y v z) = x v (y v z). [para(18216(a,1),21323(a,1,1))]. 21376 (x v y) v z = x v (y v z). [para(21348(a,1),21256(a,1)),flip(a)]. 21436 x v ((y ^ z) v (y ^ (z v x))) = x v (y ^ z). [para(21376(a,1),19838(a,1))]. 21460 x v (y ^ (z v x)) = x v (y ^ z). [para(18328(a,1),21436(a,1,2))]. 21479 x v (y ^ (x v z)) = x v (y ^ z). [para(18216(a,1),21460(a,1,2,2))]. 21481 (x ^ y) v (x ^ z) = x ^ (z v (x ^ y)). [para(21460(a,1),18837(a,1))]. 21499 x ^ (y v (x ^ z)) = x ^ (y v z). [para(21479(a,1),19971(a,1,2))]. 21513 x ^ (y v (x ^ z)) = x ^ (z v y). [para(18216(a,1),21499(a,2,2))]. 21571 (x ^ y) v (x ^ z) = x ^ (y v z). [para(21481(a,2),21513(a,1))]. 21572 $F # answer("(D12)"). [resolve(21571,a,71,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 71 given #256 (H,wt=13): 21571 (x ^ y) v (x ^ z) = x ^ (y v z). [para(21481(a,2),21513(a,1))]. given #257 (H,wt=15): 21531 x v (y ^ (x v z)) = (x v z) ^ (x v y). [para(21511(a,1),19829(a,1)),flip(a)]. given #258 (H,wt=13): 21608 (x v y) ^ (x v z) = x v (z ^ y). [para(21531(a,1),21479(a,1))]. -------- Proof 21 -------- "(D11)". ============================== PROOF ================================= % Proof 21 at 1.50 (+ 0.02) seconds: "(D11)". % Length of proof is 208. % Level of proof is 50. % Maximum clause weight is 23. % Given clauses 258. 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 2 (all x all y (x = 1 & y = 1 -> x ^ y = 1)) # label("(4)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 22 (x v y) ^ (x v z) = x v (y ^ z) # label("(D11)") # label(non_clause) # label(goal). [goal]. 26 x => ((x => y) => y) = 1 # label("(A1)[= 1]"). [assumption]. 27 (x => y) => ((y => z) => (x => z)) = 1 # label("(A2)[= 1]"). [assumption]. 28 (x ^ y) => x = 1 # label("(A3)[= 1]"). [assumption]. 29 (x ^ y) => y = 1 # label("(A4)[= 1]"). [assumption]. 30 ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]"). [assumption]. 31 x => (x v y) = 1 # label("(A6)[= 1]"). [assumption]. 32 x => (y v x) = 1 # label("(A7)[= 1]"). [assumption]. 33 ((x => y) ^ (z => y)) => ((x v z) => y) = 1 # label("(A8)[= 1]"). [assumption]. 34 (x ^ (y v z)) => ((x ^ y) v z) = 1 # label("(A9)[= 1]"). [assumption]. 35 ~ ~ x => x = 1 # label("(A10)[= 1]"). [assumption]. 36 (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). [assumption]. 37 x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. 39 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. 40 1 != x | x => y != 1 | 1 = y. [copy(39),flip(a),flip(c)]. 41 x != 1 | y != 1 | x ^ y = 1 # label("(4)"). [clausify(2)]. 42 1 != x | 1 != y | x ^ y = 1. [copy(41),flip(a),flip(b)]. 43 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 44 x * y = ~ (x => ~ y) # label("(* def)"). [assumption]. 45 ~ (x => ~ y) = x * y. [copy(44),flip(a)]. 46 0 = ~ (x => x) # label("(0 def)"). [assumption]. 47 ~ (x => x) = 0. [copy(46),flip(a)]. 48 1 = x => x # label("(1 def)"). [assumption]. 49 x => x = 1. [copy(48),flip(a)]. 69 c37 v (c38 ^ c39) != (c37 v c38) ^ (c37 v c39) # label("(D11)") # answer("(D11)"). [deny(22)]. 70 (c37 v c38) ^ (c37 v c39) != c37 v (c38 ^ c39) # answer("(D11)"). [copy(69),flip(a)]. 113 (1 ^ ((x ^ y) => z)) => ((x ^ y) => (x ^ z)) = 1. [para(28(a,1),30(a,1,1,1))]. 175 (1 ^ (x => (y v z))) => ((z v x) => (y v z)) = 1. [para(32(a,1),33(a,1,1,1))]. 252 x => 1 = 1. [para(28(a,1),37(a,1,2))]. 366 (x => y) => ((z ^ x) => y) = 1. [hyper(40,a,29,a(flip),b,27,a),flip(a)]. 372 (x => y) => ((x ^ z) => y) = 1. [hyper(40,a,28,a(flip),b,27,a),flip(a)]. 386 (1 => x) => x = 1. [hyper(40,a,xx,b,26,a),flip(a)]. 583 x => ~ y = y => ~ x. [hyper(43,a,36,a,b,36,a)]. 595 ~ 1 = 0. [para(36(a,1),47(a,1,1))]. 622 (x => x) ^ (y => (y v z)) = 1. [hyper(42,a,49,a(flip),b,31,a(flip))]. 625 (x => x) ^ ((y ^ z) => y) = 1. [hyper(42,a,49,a(flip),b,28,a(flip))]. 630 x => ~ ~ x = 1. [hyper(40,a,49,a(flip),b,36,a),flip(a)]. 640 ((x => y) ^ 1) => (x => (y ^ x)) = 1. [para(49(a,1),30(a,1,1,2))]. 645 ((x => y) ^ 1) => ((x v y) => y) = 1. [para(49(a,1),33(a,1,1,2))]. 674 (x => x) ^ (y => 1) = 1. [hyper(42,a,49,a(flip),b,252,a(flip))]. 728 1 => x = x. [hyper(43,a,37,a,b,386,a)]. 845 ~ ~ x = 1 * x. [para(728(a,1),45(a,1,1))]. 861 ~ ~ x = x. [hyper(43,a,35,a,b,630,a),flip(a)]. 1017 x => ~ ~ (y v x) = 1. [para(861(a,2),32(a,1,2))]. 1050 ~ (x => y) = x * ~ y. [para(861(a,1),45(a,1,1,2))]. 1054 ~ (x * y) = x => ~ y. [para(45(a,1),861(a,1,1))]. 1100 1 * x = x. [para(845(a,1),861(a,1))]. 1263 x => ((y => ~ x) => ~ y) = 1. [para(583(a,1),26(a,1,2,1))]. 1264 x => (y => ~ (x => ~ y)) = 1. [para(583(a,1),26(a,1,2))]. 1277 ~ (x => ~ y) = y * x. [para(583(a,1),45(a,1,1))]. 1281 x => ~ 1 = ~ x. [para(583(a,1),728(a,1))]. 1283 ~ x => ~ y = y => x. [para(861(a,1),583(a,1,2)),flip(a)]. 1321 ~ ~ x = x * 1. [para(1281(a,1),45(a,1,1))]. 1326 x => 0 = ~ x. [para(595(a,1),1281(a,1,2))]. 1347 (~ x ^ (y => 0)) => ((x v y) => 0) = 1. [para(1326(a,1),33(a,1,1,1))]. 1640 x * 1 = x. [para(1321(a,1),861(a,1))]. 2448 x => (x ^ 1) = 1. [hyper(40,a,674,a(flip),b,30,a),flip(a)]. 2521 x ^ 1 = x. [hyper(43,a,28,a,b,2448,a),flip(a)]. 2860 ~ (x v y) => ~ y = 1. [hyper(40,a,1017,a(flip),b,36,a),flip(a)]. 2932 x * ~ ((x => y) => y) = ~ 1. [para(26(a,1),1050(a,1,1)),flip(a)]. 2934 (x ^ y) * ~ x = ~ 1. [para(28(a,1),1050(a,1,1)),flip(a)]. 2935 (x ^ y) * ~ y = ~ 1. [para(29(a,1),1050(a,1,1)),flip(a)]. 2939 (x ^ (y v z)) * ~ ((x ^ y) v z) = ~ 1. [para(34(a,1),1050(a,1,1)),flip(a)]. 3031 ~ (x * y) = y => ~ x. [para(1054(a,2),583(a,1))]. 3064 x * y = y * x. [para(1277(a,1),45(a,1))]. 3369 (x ^ y) * ~ x = 0. [para(2934(a,2),595(a,1))]. 3491 (x ^ y) * ~ y = 0. [para(2935(a,2),595(a,1))]. 3596 ~ x * (y ^ x) = 0. [para(3491(a,1),3064(a,1)),flip(a)]. 3736 (x ^ y) => (y v z) = 1. [hyper(40,a,31,a(flip),b,366,a),flip(a)]. 3739 (x ^ (y ^ z)) => y = 1. [hyper(40,a,28,a(flip),b,366,a),flip(a)]. 4381 (x ^ y) => (x v z) = 1. [hyper(40,a,31,a(flip),b,372,a),flip(a)]. 4812 x => (x ^ (x v y)) = 1. [hyper(40,a,622,a(flip),b,30,a),flip(a)]. 4893 x ^ (x v y) = x. [hyper(43,a,28,a,b,4812,a),flip(a)]. 5322 x * ~ (x v y) = 0. [para(4893(a,1),3491(a,1,1))]. 5480 (x v (x ^ y)) => x = 1. [hyper(40,a,625,a(flip),b,33,a),flip(a)]. 5572 x v (x ^ y) = x. [hyper(43,a,31,a,b,5480,a)]. 6326 x => ~ (y * (y => ~ x)) = 1. [para(3031(a,2),1263(a,1,2))]. 6588 x => (y => (y * x)) = 1. [para(1277(a,1),1264(a,1,2,2))]. 6888 x * ~ ((x => y) => y) = 0. [para(2932(a,2),595(a,1))]. 7068 x * ((x => y) * ~ y) = 0. [para(1050(a,1),6888(a,1,2))]. 7073 x * (y * (x => ~ y)) = 0. [para(1277(a,1),6888(a,1,2))]. 7267 ~ (x v y) * (y * 1) = 0. [para(2860(a,1),7073(a,1,2,2))]. 7336 ~ (x v y) * y = 0. [para(1640(a,1),7267(a,1,2))]. 7422 x * ~ (y v x) = 0. [para(7336(a,1),3064(a,1)),flip(a)]. 7667 ~ x => ~ (y * (y => x)) = 1. [para(861(a,1),6326(a,1,2,1,2,2))]. 7991 (x * (x => y)) => y = 1. [para(7667(a,1),1283(a,1)),flip(a)]. 9898 (x => y) => (x => (y ^ x)) = 1. [para(2521(a,1),640(a,1,1))]. 10006 x => ((y => (y * x)) ^ x) = 1. [hyper(40,a,6588,a(flip),b,9898,a),flip(a)]. 10031 x => ((y => x) ^ x) = 1. [hyper(40,a,37,a(flip),b,9898,a),flip(a)]. 10037 x => ((x v y) ^ x) = 1. [hyper(40,a,31,a(flip),b,9898,a),flip(a)]. 10040 (x ^ y) => (x ^ (x ^ y)) = 1. [hyper(40,a,28,a(flip),b,9898,a),flip(a)]. 10042 x => (((x => y) => y) ^ x) = 1. [hyper(40,a,26,a(flip),b,9898,a),flip(a)]. 10326 (x => y) ^ y = y. [hyper(43,a,29,a,b,10031,a),flip(a)]. 10753 1 ^ x = x. [para(28(a,1),10326(a,1,1))]. 11287 (x v y) ^ x = x. [hyper(43,a,29,a,b,10037,a),flip(a)]. 11894 (x v y) v x = x v y. [para(11287(a,1),5572(a,1,2))]. 12015 (x => (x * y)) ^ y = y. [hyper(43,a,29,a,b,10006,a),flip(a)]. 12549 (x => (y * x)) ^ y = y. [para(3064(a,1),12015(a,1,1,2))]. 12578 (~ x => 0) ^ (y ^ x) = y ^ x. [para(3596(a,1),12015(a,1,1,2))]. 12606 (x => 0) ^ ~ (x v y) = ~ (x v y). [para(5322(a,1),12015(a,1,1,2))]. 13097 x ^ (x ^ y) = x ^ y. [hyper(43,a,29,a,b,10040,a),flip(a)]. 13528 ~ ~ x ^ (y ^ x) = y ^ x. [para(1326(a,1),12578(a,1,1))]. 13639 x ^ (y ^ x) = y ^ x. [para(861(a,1),13528(a,1,1))]. 13776 x v (y ^ x) = x. [para(13639(a,1),5572(a,1,2))]. 14367 (x => y) => ((x v y) => y) = 1. [para(2521(a,1),645(a,1,1))]. 14410 ((x * (x => y)) v y) => y = 1. [hyper(40,a,7991,a(flip),b,14367,a),flip(a)]. 14629 (x * (x => y)) v y = y. [hyper(43,a,32,a,b,14410,a)]. 14979 (x * (x => y)) ^ y = x * (x => y). [para(14629(a,1),4893(a,1,2))]. 15170 ~ x ^ ~ (x v y) = ~ (x v y). [para(1326(a,1),12606(a,1,1))]. 15370 x v (y * (y => x)) = x. [para(14979(a,1),13776(a,1,2))]. 15670 (~ x ^ ~ y) => ((x v y) => 0) = 1. [para(1326(a,1),1347(a,1,1,2))]. 15750 (~ x ^ ~ y) => ~ (x v y) = 1. [para(1326(a,1),15670(a,1,2))]. 15901 (x v y) * (~ x ^ ~ y) = ~ 1. [para(15750(a,1),1277(a,1,1)),flip(a)]. 15944 (x v y) * (~ x ^ ~ y) = 0. [para(15901(a,2),595(a,1))]. 16138 ((x v y) => 0) ^ (~ x ^ ~ y) = ~ x ^ ~ y. [para(15944(a,1),12015(a,1,1,2))]. 16296 (x ^ (y v z)) * ~ ((x ^ y) v z) = 0. [para(2939(a,2),595(a,1))]. 16378 (1 ^ 1) => ((x ^ y) => (x ^ (y v z))) = 1. [para(3736(a,1),113(a,1,1,2))]. 16379 (1 ^ 1) => ((x ^ (y ^ z)) => (x ^ y)) = 1. [para(3739(a,1),113(a,1,1,2))]. 16629 (x ^ y) => (x ^ (y v z)) = 1. [hyper(40,a,10753,a(flip),b,16378,a),flip(a)]. 16751 (x ^ (y ^ z)) => (x ^ y) = 1. [hyper(40,a,10753,a(flip),b,16379,a),flip(a)]. 16862 (x ^ y) => (y ^ x) = 1. [para(13639(a,1),16751(a,1,1))]. 16868 (x ^ y) v ((x ^ (y ^ z)) * 1) = x ^ y. [para(16751(a,1),15370(a,1,2,2))]. 16869 x ^ y = y ^ x. [hyper(43,a,16862,a,b,16862,a)]. 17043 x ^ (y => (y * x)) = x. [para(16869(a,1),12015(a,1))]. 17044 x ^ (y => (x * y)) = x. [para(16869(a,1),12549(a,1))]. 17048 x => (x ^ ((x => y) => y)) = 1. [para(16869(a,1),10042(a,1,2))]. 17224 ~ x ^ ((x ^ y) => 0) = ~ x. [para(3369(a,1),17043(a,1,2,2))]. 17245 ~ (x v y) ^ (y => 0) = ~ (x v y). [para(7422(a,1),17043(a,1,2,2))]. 17466 x ^ ((x => y) => y) = x. [hyper(43,a,28,a,b,17048,a),flip(a)]. 17726 (x ^ y) ^ (1 => (x ^ (y v z))) = x ^ y. [para(16629(a,1),17466(a,1,2,1))]. 17755 ~ x ^ ~ (x ^ y) = ~ x. [para(1326(a,1),17224(a,1,2))]. 17877 ~ (x ^ y) ^ ~ x = ~ x. [para(17755(a,1),16869(a,1)),flip(a)]. 17962 ~ (x v y) ^ ~ y = ~ (x v y). [para(1326(a,1),17245(a,1,2))]. 18032 ~ x ^ ~ (y v x) = ~ (y v x). [para(17962(a,1),16869(a,1)),flip(a)]. 18097 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(1640(a,1),16868(a,1,2))]. 18134 (x ^ (y v z)) v (x ^ y) = x ^ (y v z). [para(11287(a,1),18097(a,1,2,2))]. 18142 (x ^ y) ^ (x ^ (y v z)) = x ^ y. [para(728(a,1),17726(a,1,2))]. 18171 (x ^ y) ^ (x ^ ((x ^ y) v z)) = x ^ (x ^ y). [para(13097(a,1),18142(a,1,1))]. 18209 (1 ^ 1) => ((x v y) => (y v x)) = 1. [para(31(a,1),175(a,1,1,2))]. 18212 (1 ^ 1) => ((x v (y ^ z)) => (y v x)) = 1. [para(4381(a,1),175(a,1,1,2))]. 18213 (x v y) => (y v x) = 1. [hyper(40,a,10753,a(flip),b,18209,a),flip(a)]. 18216 x v y = y v x. [hyper(43,a,18213,a,b,18213,a)]. 18308 (x v y) ^ y = y. [para(18216(a,1),11287(a,1,1))]. 18310 x v (x v y) = x v y. [para(18216(a,1),11894(a,1))]. 18320 (x ^ (y v z)) * ~ (z v (x ^ y)) = 0. [para(18216(a,1),16296(a,1,2,1))]. 18328 (x ^ y) v (x ^ (y v z)) = x ^ (y v z). [para(18216(a,1),18134(a,1))]. 18535 (x ^ (y v z)) v (x ^ z) = x ^ (y v z). [para(18308(a,1),18097(a,1,2,2))]. 18629 (x ^ (y v z)) ^ (~ (z v (x ^ y)) => 0) = x ^ (y v z). [para(18320(a,1),17044(a,1,2,2))]. 18632 (x v (y ^ z)) => (y v x) = 1. [hyper(40,a,10753,a(flip),b,18212,a),flip(a)]. 18675 (x v (y ^ z)) * (1 * ~ (y v x)) = 0. [para(18632(a,1),7068(a,1,2,1))]. 18704 (x v (y ^ z)) * ~ (y v x) = 0. [para(1100(a,1),18675(a,1,2))]. 18774 (x v (y ^ z)) ^ (~ (y v x) => 0) = x v (y ^ z). [para(18704(a,1),17044(a,1,2,2))]. 18818 (x ^ (y v z)) v (z ^ x) = x ^ (y v z). [para(16869(a,1),18535(a,1,2))]. 19503 ~ (x v y) ^ (~ x ^ ~ y) = ~ x ^ ~ y. [para(1326(a,1),16138(a,1,1))]. 19735 (x ^ y) ^ (x ^ (z v (x ^ y))) = x ^ (x ^ y). [para(18216(a,1),18171(a,1,2,2))]. 19737 (x ^ y) ^ (x ^ (z v (x ^ y))) = x ^ y. [para(19735(a,2),13097(a,1))]. 19761 (x v (y ^ z)) ^ (~ (x v y) => 0) = x v (y ^ z). [para(18216(a,1),18774(a,1,2,1,1))]. 19763 (x v (y ^ z)) ^ ~ ~ (x v y) = x v (y ^ z). [para(1326(a,1),19761(a,1,2))]. 19767 (x v (y ^ z)) ^ (x v y) = x v (y ^ z). [para(861(a,1),19763(a,1,2))]. 19798 (x v y) ^ (x v (y ^ z)) = x v (y ^ z). [para(19767(a,1),16869(a,1)),flip(a)]. 19817 (x v y) ^ (x v ((x v y) ^ z)) = x v ((x v y) ^ z). [para(18310(a,1),19798(a,1,1))]. 19827 (x v y) ^ (x v (z ^ (x v y))) = x v ((x v y) ^ z). [para(16869(a,1),19817(a,1,2,2))]. 19829 (x v y) ^ (x v (z ^ (x v y))) = x v (z ^ (x v y)). [para(16869(a,1),19827(a,2,2))]. 19833 (x ^ (y v z)) ^ ~ ~ (z v (x ^ y)) = x ^ (y v z). [para(1326(a,1),18629(a,1,2))]. 19834 (x ^ (y v z)) ^ (z v (x ^ y)) = x ^ (y v z). [para(861(a,1),19833(a,1,2))]. 19838 (x v (y ^ z)) v (y ^ (z v x)) = x v (y ^ z). [para(19834(a,1),13776(a,1,2))]. 19840 (x ^ ((y ^ z) v (x ^ y))) ^ (x ^ y) = x ^ ((y ^ z) v (x ^ y)). [para(18097(a,1),19834(a,1,2))]. 19950 (x ^ y) ^ (x ^ ((y ^ z) v (x ^ y))) = x ^ ((y ^ z) v (x ^ y)). [para(19840(a,1),16869(a,1)),flip(a)]. 19951 x ^ ((y ^ z) v (x ^ y)) = x ^ y. [para(19950(a,1),19737(a,1))]. 19971 x ^ (y v (x ^ (y v z))) = x ^ (y v z). [para(11287(a,1),19951(a,1,2,1))]. 19979 x ^ (y ^ (z v x)) = x ^ y. [para(18818(a,1),19951(a,1,2))]. 20029 x ^ (y ^ (z v x)) = y ^ x. [para(19979(a,2),16869(a,1))]. 20053 (x ^ y) ^ (z ^ x) = z ^ (x ^ y). [para(5572(a,1),20029(a,1,2,2))]. 20110 (x ^ y) ^ (y ^ z) = x ^ (y ^ z). [para(20053(a,1),16869(a,1)),flip(a)]. 20112 (x ^ y) ^ (x ^ z) = z ^ (x ^ y). [para(16869(a,1),20053(a,1,2))]. 20151 (x ^ y) ^ (x ^ z) = y ^ (x ^ z). [para(16869(a,1),20110(a,1,1))]. 20232 x ^ (y ^ z) = z ^ (y ^ x). [para(20151(a,1),20112(a,1))]. 20276 (x ^ y) ^ z = y ^ (x ^ z). [para(20232(a,1),16869(a,1)),flip(a)]. 20291 ~ x ^ (~ y ^ ~ (y v x)) = ~ y ^ ~ x. [para(20232(a,1),19503(a,1))]. 20384 ~ x ^ (~ (x ^ y) ^ z) = ~ x ^ z. [para(17877(a,1),20276(a,1,1)),flip(a)]. 20506 ~ x ^ (y ^ ~ (x ^ z)) = ~ x ^ y. [para(16869(a,1),20384(a,1,2))]. 20531 ~ x ^ ~ (y v x) = ~ y ^ ~ x. [para(15170(a,1),20291(a,1,2))]. 20561 ~ x ^ ~ y = ~ (x v y). [para(20531(a,1),18032(a,1))]. 20666 ~ x ^ ~ (y v (x ^ z)) = ~ x ^ ~ y. [para(20561(a,1),20506(a,1,2))]. 21103 ~ (x v (y v (x ^ z))) = ~ x ^ ~ y. [para(20666(a,1),20561(a,1)),flip(a)]. 21128 ~ (x v (y v (x ^ z))) = ~ (x v y). [para(21103(a,2),20561(a,1))]. 21129 x v (y v (x ^ z)) = ~ ~ (x v y). [para(21128(a,1),861(a,1,1)),flip(a)]. 21151 x v (y v (x ^ z)) = x v y. [para(21129(a,2),861(a,1))]. 21192 (x v y) v (z v x) = (x v y) v z. [para(11287(a,1),21151(a,1,2,2))]. 21209 (x v y) v (z v y) = (x v y) v z. [para(18308(a,1),21151(a,1,2,2))]. 21240 (x v y) v (x v z) = (x v y) v z. [para(18216(a,1),21192(a,1,2))]. 21256 (x v y) v (y v z) = (x v y) v z. [para(18216(a,1),21209(a,1,2))]. 21279 (x v y) v (x v z) = z v (x v y). [para(21240(a,2),18216(a,1))]. 21323 (x v y) v (x v z) = y v (x v z). [para(21279(a,1),18216(a,1)),flip(a)]. 21348 (x v y) v (y v z) = x v (y v z). [para(18216(a,1),21323(a,1,1))]. 21376 (x v y) v z = x v (y v z). [para(21348(a,1),21256(a,1)),flip(a)]. 21436 x v ((y ^ z) v (y ^ (z v x))) = x v (y ^ z). [para(21376(a,1),19838(a,1))]. 21460 x v (y ^ (z v x)) = x v (y ^ z). [para(18328(a,1),21436(a,1,2))]. 21479 x v (y ^ (x v z)) = x v (y ^ z). [para(18216(a,1),21460(a,1,2,2))]. 21499 x ^ (y v (x ^ z)) = x ^ (y v z). [para(21479(a,1),19971(a,1,2))]. 21511 x ^ (y v (z ^ x)) = x ^ (y v z). [para(16869(a,1),21499(a,1,2,2))]. 21531 x v (y ^ (x v z)) = (x v z) ^ (x v y). [para(21511(a,1),19829(a,1)),flip(a)]. 21608 (x v y) ^ (x v z) = x v (z ^ y). [para(21531(a,1),21479(a,1))]. 21627 (x v y) ^ (x v z) = x v (y ^ z). [para(21608(a,1),16869(a,1)),flip(a)]. 21628 $F # answer("(D11)"). [resolve(21627,a,70,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 69x 70 given #259 (H,wt=13): 21627 (x v y) ^ (x v z) = x v (y ^ z). [para(21608(a,1),16869(a,1)),flip(a)]. given #260 (H,wt=18): 21093 (x * y) v ~ (z => ~ x) = ~ (x => (~ y ^ ~ z)). [para(19930(a,1),20999(a,1,1)),flip(a)]. given #261 (H,wt=17): 21656 (x * y) v ~ (z => ~ x) = ~ (x => ~ (y v z)). [para(20561(a,1),21093(a,2,1,2))]. given #262 (H,wt=15): 21658 (x * y) v ~ (z => ~ x) = x * (y v z). [para(21656(a,2),45(a,1))]. -------- Proof 22 -------- "(R1)". ============================== PROOF ================================= % Proof 22 at 1.53 (+ 0.02) seconds: "(R1)". % Length of proof is 172. % Level of proof is 39. % Maximum clause weight is 23. % Given clauses 262. 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 2 (all x all y (x = 1 & y = 1 -> x ^ y = 1)) # label("(4)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 17 x * (y v z) = (x * y) v (x * z) # label("(R1)") # label(non_clause) # label(goal). [goal]. 26 x => ((x => y) => y) = 1 # label("(A1)[= 1]"). [assumption]. 27 (x => y) => ((y => z) => (x => z)) = 1 # label("(A2)[= 1]"). [assumption]. 28 (x ^ y) => x = 1 # label("(A3)[= 1]"). [assumption]. 29 (x ^ y) => y = 1 # label("(A4)[= 1]"). [assumption]. 30 ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]"). [assumption]. 31 x => (x v y) = 1 # label("(A6)[= 1]"). [assumption]. 32 x => (y v x) = 1 # label("(A7)[= 1]"). [assumption]. 33 ((x => y) ^ (z => y)) => ((x v z) => y) = 1 # label("(A8)[= 1]"). [assumption]. 34 (x ^ (y v z)) => ((x ^ y) v z) = 1 # label("(A9)[= 1]"). [assumption]. 35 ~ ~ x => x = 1 # label("(A10)[= 1]"). [assumption]. 36 (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). [assumption]. 37 x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. 39 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. 40 1 != x | x => y != 1 | 1 = y. [copy(39),flip(a),flip(c)]. 41 x != 1 | y != 1 | x ^ y = 1 # label("(4)"). [clausify(2)]. 42 1 != x | 1 != y | x ^ y = 1. [copy(41),flip(a),flip(b)]. 43 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 44 x * y = ~ (x => ~ y) # label("(* def)"). [assumption]. 45 ~ (x => ~ y) = x * y. [copy(44),flip(a)]. 46 0 = ~ (x => x) # label("(0 def)"). [assumption]. 47 ~ (x => x) = 0. [copy(46),flip(a)]. 48 1 = x => x # label("(1 def)"). [assumption]. 49 x => x = 1. [copy(48),flip(a)]. 63 (c25 * c26) v (c25 * c27) != c25 * (c26 v c27) # label("(R1)") # answer("(R1)"). [deny(17)]. 90 (x => (y ^ z)) => (1 => (x => y)) = 1. [para(28(a,1),27(a,1,2,1))]. 97 (x => (y ^ z)) => (1 => (x => z)) = 1. [para(29(a,1),27(a,1,2,1))]. 113 (1 ^ ((x ^ y) => z)) => ((x ^ y) => (x ^ z)) = 1. [para(28(a,1),30(a,1,1,1))]. 175 (1 ^ (x => (y v z))) => ((z v x) => (y v z)) = 1. [para(32(a,1),33(a,1,1,1))]. 252 x => 1 = 1. [para(28(a,1),37(a,1,2))]. 366 (x => y) => ((z ^ x) => y) = 1. [hyper(40,a,29,a(flip),b,27,a),flip(a)]. 386 (1 => x) => x = 1. [hyper(40,a,xx,b,26,a),flip(a)]. 583 x => ~ y = y => ~ x. [hyper(43,a,36,a,b,36,a)]. 595 ~ 1 = 0. [para(36(a,1),47(a,1,1))]. 622 (x => x) ^ (y => (y v z)) = 1. [hyper(42,a,49,a(flip),b,31,a(flip))]. 625 (x => x) ^ ((y ^ z) => y) = 1. [hyper(42,a,49,a(flip),b,28,a(flip))]. 630 x => ~ ~ x = 1. [hyper(40,a,49,a(flip),b,36,a),flip(a)]. 640 ((x => y) ^ 1) => (x => (y ^ x)) = 1. [para(49(a,1),30(a,1,1,2))]. 645 ((x => y) ^ 1) => ((x v y) => y) = 1. [para(49(a,1),33(a,1,1,2))]. 674 (x => x) ^ (y => 1) = 1. [hyper(42,a,49,a(flip),b,252,a(flip))]. 728 1 => x = x. [hyper(43,a,37,a,b,386,a)]. 861 ~ ~ x = x. [hyper(43,a,35,a,b,630,a),flip(a)]. 1017 x => ~ ~ (y v x) = 1. [para(861(a,2),32(a,1,2))]. 1050 ~ (x => y) = x * ~ y. [para(861(a,1),45(a,1,1,2))]. 1054 ~ (x * y) = x => ~ y. [para(45(a,1),861(a,1,1))]. 1263 x => ((y => ~ x) => ~ y) = 1. [para(583(a,1),26(a,1,2,1))]. 1264 x => (y => ~ (x => ~ y)) = 1. [para(583(a,1),26(a,1,2))]. 1277 ~ (x => ~ y) = y * x. [para(583(a,1),45(a,1,1))]. 1281 x => ~ 1 = ~ x. [para(583(a,1),728(a,1))]. 1283 ~ x => ~ y = y => x. [para(861(a,1),583(a,1,2)),flip(a)]. 1321 ~ ~ x = x * 1. [para(1281(a,1),45(a,1,1))]. 1326 x => 0 = ~ x. [para(595(a,1),1281(a,1,2))]. 1347 (~ x ^ (y => 0)) => ((x v y) => 0) = 1. [para(1326(a,1),33(a,1,1,1))]. 1640 x * 1 = x. [para(1321(a,1),861(a,1))]. 2448 x => (x ^ 1) = 1. [hyper(40,a,674,a(flip),b,30,a),flip(a)]. 2521 x ^ 1 = x. [hyper(43,a,28,a,b,2448,a),flip(a)]. 2860 ~ (x v y) => ~ y = 1. [hyper(40,a,1017,a(flip),b,36,a),flip(a)]. 2932 x * ~ ((x => y) => y) = ~ 1. [para(26(a,1),1050(a,1,1)),flip(a)]. 2935 (x ^ y) * ~ y = ~ 1. [para(29(a,1),1050(a,1,1)),flip(a)]. 2939 (x ^ (y v z)) * ~ ((x ^ y) v z) = ~ 1. [para(34(a,1),1050(a,1,1)),flip(a)]. 3031 ~ (x * y) = y => ~ x. [para(1054(a,2),583(a,1))]. 3064 x * y = y * x. [para(1277(a,1),45(a,1))]. 3491 (x ^ y) * ~ y = 0. [para(2935(a,2),595(a,1))]. 3596 ~ x * (y ^ x) = 0. [para(3491(a,1),3064(a,1)),flip(a)]. 3736 (x ^ y) => (y v z) = 1. [hyper(40,a,31,a(flip),b,366,a),flip(a)]. 3739 (x ^ (y ^ z)) => y = 1. [hyper(40,a,28,a(flip),b,366,a),flip(a)]. 4812 x => (x ^ (x v y)) = 1. [hyper(40,a,622,a(flip),b,30,a),flip(a)]. 4893 x ^ (x v y) = x. [hyper(43,a,28,a,b,4812,a),flip(a)]. 5322 x * ~ (x v y) = 0. [para(4893(a,1),3491(a,1,1))]. 5480 (x v (x ^ y)) => x = 1. [hyper(40,a,625,a(flip),b,33,a),flip(a)]. 5572 x v (x ^ y) = x. [hyper(43,a,31,a,b,5480,a)]. 6326 x => ~ (y * (y => ~ x)) = 1. [para(3031(a,2),1263(a,1,2))]. 6588 x => (y => (y * x)) = 1. [para(1277(a,1),1264(a,1,2,2))]. 6888 x * ~ ((x => y) => y) = 0. [para(2932(a,2),595(a,1))]. 7073 x * (y * (x => ~ y)) = 0. [para(1277(a,1),6888(a,1,2))]. 7267 ~ (x v y) * (y * 1) = 0. [para(2860(a,1),7073(a,1,2,2))]. 7336 ~ (x v y) * y = 0. [para(1640(a,1),7267(a,1,2))]. 7422 x * ~ (y v x) = 0. [para(7336(a,1),3064(a,1)),flip(a)]. 7667 ~ x => ~ (y * (y => x)) = 1. [para(861(a,1),6326(a,1,2,1,2,2))]. 7991 (x * (x => y)) => y = 1. [para(7667(a,1),1283(a,1)),flip(a)]. 8436 (x => (y ^ z)) => (x => y) = 1. [para(728(a,1),90(a,1,2))]. 8959 (x => (y ^ z)) => (x => z) = 1. [para(728(a,1),97(a,1,2))]. 9096 ((x => (y ^ z)) => (x => y)) ^ ((u => (w ^ v5)) => (u => v5)) = 1. [hyper(42,a,8436,a(flip),b,8959,a(flip))]. 9898 (x => y) => (x => (y ^ x)) = 1. [para(2521(a,1),640(a,1,1))]. 10006 x => ((y => (y * x)) ^ x) = 1. [hyper(40,a,6588,a(flip),b,9898,a),flip(a)]. 10031 x => ((y => x) ^ x) = 1. [hyper(40,a,37,a(flip),b,9898,a),flip(a)]. 10037 x => ((x v y) ^ x) = 1. [hyper(40,a,31,a(flip),b,9898,a),flip(a)]. 10040 (x ^ y) => (x ^ (x ^ y)) = 1. [hyper(40,a,28,a(flip),b,9898,a),flip(a)]. 10042 x => (((x => y) => y) ^ x) = 1. [hyper(40,a,26,a(flip),b,9898,a),flip(a)]. 10326 (x => y) ^ y = y. [hyper(43,a,29,a,b,10031,a),flip(a)]. 10753 1 ^ x = x. [para(28(a,1),10326(a,1,1))]. 11287 (x v y) ^ x = x. [hyper(43,a,29,a,b,10037,a),flip(a)]. 12015 (x => (x * y)) ^ y = y. [hyper(43,a,29,a,b,10006,a),flip(a)]. 12549 (x => (y * x)) ^ y = y. [para(3064(a,1),12015(a,1,1,2))]. 12578 (~ x => 0) ^ (y ^ x) = y ^ x. [para(3596(a,1),12015(a,1,1,2))]. 12606 (x => 0) ^ ~ (x v y) = ~ (x v y). [para(5322(a,1),12015(a,1,1,2))]. 13097 x ^ (x ^ y) = x ^ y. [hyper(43,a,29,a,b,10040,a),flip(a)]. 13528 ~ ~ x ^ (y ^ x) = y ^ x. [para(1326(a,1),12578(a,1,1))]. 13639 x ^ (y ^ x) = y ^ x. [para(861(a,1),13528(a,1,1))]. 13776 x v (y ^ x) = x. [para(13639(a,1),5572(a,1,2))]. 14367 (x => y) => ((x v y) => y) = 1. [para(2521(a,1),645(a,1,1))]. 14410 ((x * (x => y)) v y) => y = 1. [hyper(40,a,7991,a(flip),b,14367,a),flip(a)]. 14629 (x * (x => y)) v y = y. [hyper(43,a,32,a,b,14410,a)]. 14979 (x * (x => y)) ^ y = x * (x => y). [para(14629(a,1),4893(a,1,2))]. 15170 ~ x ^ ~ (x v y) = ~ (x v y). [para(1326(a,1),12606(a,1,1))]. 15370 x v (y * (y => x)) = x. [para(14979(a,1),13776(a,1,2))]. 15670 (~ x ^ ~ y) => ((x v y) => 0) = 1. [para(1326(a,1),1347(a,1,1,2))]. 15750 (~ x ^ ~ y) => ~ (x v y) = 1. [para(1326(a,1),15670(a,1,2))]. 15901 (x v y) * (~ x ^ ~ y) = ~ 1. [para(15750(a,1),1277(a,1,1)),flip(a)]. 15944 (x v y) * (~ x ^ ~ y) = 0. [para(15901(a,2),595(a,1))]. 16138 ((x v y) => 0) ^ (~ x ^ ~ y) = ~ x ^ ~ y. [para(15944(a,1),12015(a,1,1,2))]. 16296 (x ^ (y v z)) * ~ ((x ^ y) v z) = 0. [para(2939(a,2),595(a,1))]. 16378 (1 ^ 1) => ((x ^ y) => (x ^ (y v z))) = 1. [para(3736(a,1),113(a,1,1,2))]. 16379 (1 ^ 1) => ((x ^ (y ^ z)) => (x ^ y)) = 1. [para(3739(a,1),113(a,1,1,2))]. 16629 (x ^ y) => (x ^ (y v z)) = 1. [hyper(40,a,10753,a(flip),b,16378,a),flip(a)]. 16751 (x ^ (y ^ z)) => (x ^ y) = 1. [hyper(40,a,10753,a(flip),b,16379,a),flip(a)]. 16862 (x ^ y) => (y ^ x) = 1. [para(13639(a,1),16751(a,1,1))]. 16868 (x ^ y) v ((x ^ (y ^ z)) * 1) = x ^ y. [para(16751(a,1),15370(a,1,2,2))]. 16869 x ^ y = y ^ x. [hyper(43,a,16862,a,b,16862,a)]. 17043 x ^ (y => (y * x)) = x. [para(16869(a,1),12015(a,1))]. 17044 x ^ (y => (x * y)) = x. [para(16869(a,1),12549(a,1))]. 17048 x => (x ^ ((x => y) => y)) = 1. [para(16869(a,1),10042(a,1,2))]. 17245 ~ (x v y) ^ (y => 0) = ~ (x v y). [para(7422(a,1),17043(a,1,2,2))]. 17466 x ^ ((x => y) => y) = x. [hyper(43,a,28,a,b,17048,a),flip(a)]. 17726 (x ^ y) ^ (1 => (x ^ (y v z))) = x ^ y. [para(16629(a,1),17466(a,1,2,1))]. 17962 ~ (x v y) ^ ~ y = ~ (x v y). [para(1326(a,1),17245(a,1,2))]. 18032 ~ x ^ ~ (y v x) = ~ (y v x). [para(17962(a,1),16869(a,1)),flip(a)]. 18097 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(1640(a,1),16868(a,1,2))]. 18142 (x ^ y) ^ (x ^ (y v z)) = x ^ y. [para(728(a,1),17726(a,1,2))]. 18171 (x ^ y) ^ (x ^ ((x ^ y) v z)) = x ^ (x ^ y). [para(13097(a,1),18142(a,1,1))]. 18209 (1 ^ 1) => ((x v y) => (y v x)) = 1. [para(31(a,1),175(a,1,1,2))]. 18213 (x v y) => (y v x) = 1. [hyper(40,a,10753,a(flip),b,18209,a),flip(a)]. 18216 x v y = y v x. [hyper(43,a,18213,a,b,18213,a)]. 18308 (x v y) ^ y = y. [para(18216(a,1),11287(a,1,1))]. 18320 (x ^ (y v z)) * ~ (z v (x ^ y)) = 0. [para(18216(a,1),16296(a,1,2,1))]. 18535 (x ^ (y v z)) v (x ^ z) = x ^ (y v z). [para(18308(a,1),18097(a,1,2,2))]. 18629 (x ^ (y v z)) ^ (~ (z v (x ^ y)) => 0) = x ^ (y v z). [para(18320(a,1),17044(a,1,2,2))]. 18818 (x ^ (y v z)) v (z ^ x) = x ^ (y v z). [para(16869(a,1),18535(a,1,2))]. 19503 ~ (x v y) ^ (~ x ^ ~ y) = ~ x ^ ~ y. [para(1326(a,1),16138(a,1,1))]. 19735 (x ^ y) ^ (x ^ (z v (x ^ y))) = x ^ (x ^ y). [para(18216(a,1),18171(a,1,2,2))]. 19737 (x ^ y) ^ (x ^ (z v (x ^ y))) = x ^ y. [para(19735(a,2),13097(a,1))]. 19833 (x ^ (y v z)) ^ ~ ~ (z v (x ^ y)) = x ^ (y v z). [para(1326(a,1),18629(a,1,2))]. 19834 (x ^ (y v z)) ^ (z v (x ^ y)) = x ^ (y v z). [para(861(a,1),19833(a,1,2))]. 19840 (x ^ ((y ^ z) v (x ^ y))) ^ (x ^ y) = x ^ ((y ^ z) v (x ^ y)). [para(18097(a,1),19834(a,1,2))]. 19846 (x => (y ^ z)) => ((x => y) ^ (x => z)) = 1. [hyper(40,a,9096,a(flip),b,30,a),flip(a)]. 19850 (x => y) ^ (x => z) = x => (y ^ z). [hyper(43,a,30,a,b,19846,a),flip(a)]. 19880 (x => ~ y) ^ (y => z) = y => (~ x ^ z). [para(583(a,1),19850(a,1,1))]. 19930 (x => ~ y) ^ (y => z) = y => (z ^ ~ x). [para(16869(a,1),19880(a,2,2))]. 19950 (x ^ y) ^ (x ^ ((y ^ z) v (x ^ y))) = x ^ ((y ^ z) v (x ^ y)). [para(19840(a,1),16869(a,1)),flip(a)]. 19951 x ^ ((y ^ z) v (x ^ y)) = x ^ y. [para(19950(a,1),19737(a,1))]. 19979 x ^ (y ^ (z v x)) = x ^ y. [para(18818(a,1),19951(a,1,2))]. 20029 x ^ (y ^ (z v x)) = y ^ x. [para(19979(a,2),16869(a,1))]. 20053 (x ^ y) ^ (z ^ x) = z ^ (x ^ y). [para(5572(a,1),20029(a,1,2,2))]. 20110 (x ^ y) ^ (y ^ z) = x ^ (y ^ z). [para(20053(a,1),16869(a,1)),flip(a)]. 20112 (x ^ y) ^ (x ^ z) = z ^ (x ^ y). [para(16869(a,1),20053(a,1,2))]. 20151 (x ^ y) ^ (x ^ z) = y ^ (x ^ z). [para(16869(a,1),20110(a,1,1))]. 20232 x ^ (y ^ z) = z ^ (y ^ x). [para(20151(a,1),20112(a,1))]. 20291 ~ x ^ (~ y ^ ~ (y v x)) = ~ y ^ ~ x. [para(20232(a,1),19503(a,1))]. 20531 ~ x ^ ~ (y v x) = ~ y ^ ~ x. [para(15170(a,1),20291(a,1,2))]. 20561 ~ x ^ ~ y = ~ (x v y). [para(20531(a,1),18032(a,1))]. 20575 ~ (~ x v y) = x ^ ~ y. [para(861(a,1),20561(a,1,1)),flip(a)]. 20790 ~ (x v ~ y) = y ^ ~ x. [para(18216(a,1),20575(a,1,1))]. 20817 ~ (x ^ ~ y) = y v ~ x. [para(20790(a,1),861(a,1,1))]. 20999 ~ (x ^ (y => ~ z)) = (y * z) v ~ x. [para(1054(a,1),20817(a,1,1,2))]. 21093 (x * y) v ~ (z => ~ x) = ~ (x => (~ y ^ ~ z)). [para(19930(a,1),20999(a,1,1)),flip(a)]. 21656 (x * y) v ~ (z => ~ x) = ~ (x => ~ (y v z)). [para(20561(a,1),21093(a,2,1,2))]. 21658 (x * y) v ~ (z => ~ x) = x * (y v z). [para(21656(a,2),45(a,1))]. 21672 (x * y) v (x * z) = x * (y v z). [para(1277(a,1),21658(a,1,2))]. 21673 $F # answer("(R1)"). [resolve(21672,a,63,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=262. Generated=97241. Kept=21618. proofs=22. Usable=249. Sos=19999. Demods=0. Limbo=12, Disabled=1398. Hints=338. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=10902. Back_subsumed=1267. Sos_limit_deleted=64721. Sos_displaced=58. 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=4. Megabytes=23.12. User_CPU=1.53, System_CPU=0.02, Wall_clock=3. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED THEOREM PROVED Exiting with 22 proofs. ------ process 9581 exit (max_proofs) ------  Process 9581 exit (max_proofs) Sat Sep 19 09:11:06 2009