-------- Proof 1 -------- 432. ============================== PROOF ================================= % Proof 1 at 1.95 (+ 0.02) seconds: 432. % Length of proof is 16. % Level of proof is 13. % Maximum clause weight is 35.000. % Given clauses 138. 3 x = x * (y * (x * (z * x))) # label(432) # label(non_clause) # label(goal). [goal]. 4 x = x * (y * (z * (y * x))) # label(450). [assumption]. 5 x * (y * (z * (y * x))) = x. [copy(4),flip(a)]. 8 c5 * (c6 * (c5 * (c7 * c5))) != c5 # label(432) # answer(432). [deny(3)]. 9 (x * (y * (x * z))) * (z * (u * z)) = x * (y * (x * z)). [para(5(a,1),5(a,1,2,2,2))]. 14 x * ((y * x) * (z * (y * x))) = x. [para(5(a,1),9(a,1,1)),rewrite([5(9)])]. 17 (x * (y * x)) * (((z * x) * (u * (z * x))) * (w * ((z * x) * (u * (z * x))))) = x * (y * x). [para(14(a,1),9(a,1,1,2,2)),rewrite([14(18)])]. 56 (x * (y * x)) * (((z * x) * (u * (z * x))) * (w * (v5 * (w * (z * x))))) = x * (y * x). [para(9(a,1),17(a,1,2,2))]. 103 (x * ((y * (z * y)) * (u * y))) * (y * (z * y)) = x * ((y * (z * y)) * (u * y)). [para(56(a,1),5(a,1,2))]. 107 (x * y) * (y * (z * ((y * (x * y)) * (u * y)))) = x * y. [para(103(a,1),5(a,1,2,2))]. 113 ((x * (y * x)) * (z * x)) * (y * x) = (x * (y * x)) * (z * x). [para(107(a,1),5(a,1,2))]. 116 x * (y * ((x * (y * x)) * (z * x))) = x. [para(113(a,1),5(a,1,2,2))]. 147 (x * (y * x)) * (z * (((x * (y * x)) * (z * (x * (y * x)))) * (u * (w * (u * x))))) = x * (y * x). [para(9(a,1),116(a,1,2,2,2))]. 177 (x * (y * x)) * (z * x) = x * (y * x). [para(5(a,1),147(a,1,2))]. 182 x * (y * (x * (z * x))) = x. [para(177(a,1),5(a,1,2,2))]. 183 $F # answer(432). [resolve(182,a,8,a)]. ============================== end of proof ========================== -------- Proof 2 -------- 426. ============================== PROOF ================================= % Proof 2 at 1.95 (+ 0.02) seconds: 426. % Length of proof is 16. % Level of proof is 13. % Maximum clause weight is 35.000. % Given clauses 138. 2 x = x * (y * (x * (x * x))) # label(426) # label(non_clause) # label(goal). [goal]. 4 x = x * (y * (z * (y * x))) # label(450). [assumption]. 5 x * (y * (z * (y * x))) = x. [copy(4),flip(a)]. 7 c3 * (c4 * (c3 * (c3 * c3))) != c3 # label(426) # answer(426). [deny(2)]. 9 (x * (y * (x * z))) * (z * (u * z)) = x * (y * (x * z)). [para(5(a,1),5(a,1,2,2,2))]. 14 x * ((y * x) * (z * (y * x))) = x. [para(5(a,1),9(a,1,1)),rewrite([5(9)])]. 17 (x * (y * x)) * (((z * x) * (u * (z * x))) * (w * ((z * x) * (u * (z * x))))) = x * (y * x). [para(14(a,1),9(a,1,1,2,2)),rewrite([14(18)])]. 56 (x * (y * x)) * (((z * x) * (u * (z * x))) * (w * (v5 * (w * (z * x))))) = x * (y * x). [para(9(a,1),17(a,1,2,2))]. 103 (x * ((y * (z * y)) * (u * y))) * (y * (z * y)) = x * ((y * (z * y)) * (u * y)). [para(56(a,1),5(a,1,2))]. 107 (x * y) * (y * (z * ((y * (x * y)) * (u * y)))) = x * y. [para(103(a,1),5(a,1,2,2))]. 113 ((x * (y * x)) * (z * x)) * (y * x) = (x * (y * x)) * (z * x). [para(107(a,1),5(a,1,2))]. 116 x * (y * ((x * (y * x)) * (z * x))) = x. [para(113(a,1),5(a,1,2,2))]. 147 (x * (y * x)) * (z * (((x * (y * x)) * (z * (x * (y * x)))) * (u * (w * (u * x))))) = x * (y * x). [para(9(a,1),116(a,1,2,2,2))]. 177 (x * (y * x)) * (z * x) = x * (y * x). [para(5(a,1),147(a,1,2))]. 182 x * (y * (x * (z * x))) = x. [para(177(a,1),5(a,1,2,2))]. 184 $F # answer(426). [resolve(182,a,7,a)]. ============================== end of proof ========================== -------- Proof 3 -------- 413. ============================== PROOF ================================= % Proof 3 at 1.95 (+ 0.02) seconds: 413. % Length of proof is 16. % Level of proof is 13. % Maximum clause weight is 35.000. % Given clauses 138. 1 x = x * (x * (x * (y * x))) # label(413) # label(non_clause) # label(goal). [goal]. 4 x = x * (y * (z * (y * x))) # label(450). [assumption]. 5 x * (y * (z * (y * x))) = x. [copy(4),flip(a)]. 6 c1 * (c1 * (c1 * (c2 * c1))) != c1 # label(413) # answer(413). [deny(1)]. 9 (x * (y * (x * z))) * (z * (u * z)) = x * (y * (x * z)). [para(5(a,1),5(a,1,2,2,2))]. 14 x * ((y * x) * (z * (y * x))) = x. [para(5(a,1),9(a,1,1)),rewrite([5(9)])]. 17 (x * (y * x)) * (((z * x) * (u * (z * x))) * (w * ((z * x) * (u * (z * x))))) = x * (y * x). [para(14(a,1),9(a,1,1,2,2)),rewrite([14(18)])]. 56 (x * (y * x)) * (((z * x) * (u * (z * x))) * (w * (v5 * (w * (z * x))))) = x * (y * x). [para(9(a,1),17(a,1,2,2))]. 103 (x * ((y * (z * y)) * (u * y))) * (y * (z * y)) = x * ((y * (z * y)) * (u * y)). [para(56(a,1),5(a,1,2))]. 107 (x * y) * (y * (z * ((y * (x * y)) * (u * y)))) = x * y. [para(103(a,1),5(a,1,2,2))]. 113 ((x * (y * x)) * (z * x)) * (y * x) = (x * (y * x)) * (z * x). [para(107(a,1),5(a,1,2))]. 116 x * (y * ((x * (y * x)) * (z * x))) = x. [para(113(a,1),5(a,1,2,2))]. 147 (x * (y * x)) * (z * (((x * (y * x)) * (z * (x * (y * x)))) * (u * (w * (u * x))))) = x * (y * x). [para(9(a,1),116(a,1,2,2,2))]. 177 (x * (y * x)) * (z * x) = x * (y * x). [para(5(a,1),147(a,1,2))]. 182 x * (y * (x * (z * x))) = x. [para(177(a,1),5(a,1,2,2))]. 185 $F # answer(413). [resolve(182,a,6,a)]. ============================== end of proof ==========================