-------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 0.27 (+ 0.01) seconds. % Length of proof is 25. % Level of proof is 13. % Maximum clause weight is 37.000. % Given clauses 71. 1 x = x * y # label(non_clause) # label(goal). [goal]. 2 x = x * (y * ((z * x) * y)) # label(650). [assumption]. 3 x * (y * ((z * x) * y)) = x. [copy(2),flip(a)]. 4 c1 * c2 != c1. [deny(1)]. 5 (x * ((y * z) * x)) * (u * (z * u)) = x * ((y * z) * x). [para(3(a,1),3(a,1,2,2,1))]. 6 x * ((y * ((z * (u * x)) * y)) * (u * x)) = x. [para(3(a,1),3(a,1,2,2))]. 7 (x * (y * x)) * (z * ((u * ((w * y) * u)) * z)) = x * (y * x). [para(5(a,1),3(a,1,2,2,1))]. 9 ((x * ((y * (z * u)) * x)) * (z * u)) * (w * (u * w)) = (x * ((y * (z * u)) * x)) * (z * u). [para(3(a,1),5(a,1,1,2)),rewrite([3(19)])]. 12 ((x * (y * x)) * (z * ((u * y) * z))) * (w * (((u * y) * z) * w)) = (x * (y * x)) * (z * ((u * y) * z)). [para(5(a,1),5(a,1,1,2)),rewrite([5(19)])]. 16 (x * (y * x)) * (z * (((u * ((w * (v5 * y)) * u)) * (v5 * y)) * z)) = x * (y * x). [para(6(a,1),5(a,1,1,2,1)),rewrite([6(18)])]. 20 (x * y) * ((z * ((u * ((w * x) * u)) * z)) * (y * (x * y))) = x * y. [para(5(a,1),6(a,1,2,1,2,1))]. 25 (x * (y * x)) * ((z * (y * z)) * (u * ((w * y) * u))) = x * (y * x). [para(5(a,1),7(a,1,2,2))]. 31 (x * y) * (((z * (x * z)) * (u * ((w * x) * u))) * (y * (x * y))) = x * y. [para(5(a,1),20(a,1,2,1,2))]. 35 (x * ((y * z) * x)) * (u * (((y * z) * (z * (y * z))) * u)) = x * ((y * z) * x). [para(12(a,1),7(a,1,2,2)),rewrite([5(22)])]. 42 (x * (y * x)) * ((z * (y * z)) * ((u * ((w * (v5 * y)) * u)) * (v5 * y))) = x * (y * x). [para(9(a,1),16(a,1,2,2))]. 43 (x * (y * x)) * (z * ((y * ((u * ((w * y) * u)) * y)) * z)) = x * (y * x). [para(3(a,1),35(a,1,1,2,1)),rewrite([3(6),3(9),3(14)])]. 367 (x * ((y * (z * y)) * x)) * (u * ((y * (z * y)) * u)) = x * ((y * (z * y)) * x). [para(35(a,1),42(a,1,2,2,1)),rewrite([5(24),5(20)])]. 368 ((x * (y * x)) * z) * (u * ((x * (y * x)) * u)) = (x * (y * x)) * z. [para(367(a,1),3(a,1,2,2)),rewrite([367(12)])]. 414 x * ((y * (z * y)) * (u * x)) = x. [para(368(a,1),3(a,1,2))]. 608 (x * (y * x)) * (z * (y * z)) = x * (y * x). [para(414(a,1),25(a,1,2))]. 609 (x * y) * (z * (x * z)) = x * y. [para(414(a,1),31(a,1,2,1)),rewrite([608(6)])]. 617 x * (y * (x * y)) = x. [para(3(a,1),609(a,1,1)),rewrite([3(7)])]. 633 x * (y * x) = x. [para(609(a,1),617(a,1,2))]. 636 x * y = x. [back_rewrite(43),rewrite([633(2),633(3),633(2),633(2),633(3)])]. 637 $F. [resolve(636,a,4,a)]. ============================== end of proof ========================== -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 0.23 (+ 0.01) seconds. % Length of proof is 28. % Level of proof is 14. % Maximum clause weight is 33.000. % Given clauses 67. 1 x = x * y # label(non_clause) # label(goal). [goal]. 2 x = x * (y * ((z * x) * y)) # label(650). [assumption]. 3 x * (y * ((z * x) * y)) = x. [copy(2),flip(a)]. 4 c1 * c2 != c1. [deny(1)]. 5 (x * ((y * z) * x)) * (u * (z * u)) = x * ((y * z) * x). [para(3(a,1),3(a,1,2,2,1))]. 6 x * ((y * ((z * (u * x)) * y)) * (u * x)) = x. [para(3(a,1),3(a,1,2,2))]. 7 (x * (y * x)) * (z * ((u * ((w * y) * u)) * z)) = x * (y * x). [para(5(a,1),3(a,1,2,2,1))]. 8 ((x * y) * z) * ((u * (y * u)) * (z * ((x * y) * z))) = (x * y) * z. [para(5(a,1),3(a,1,2,2))]. 9 ((x * ((y * (z * u)) * x)) * (z * u)) * (w * (u * w)) = (x * ((y * (z * u)) * x)) * (z * u). [para(3(a,1),5(a,1,1,2)),rewrite([3(19)])]. 14 (x * (y * x)) * (z * (((u * ((w * (v5 * y)) * u)) * (v5 * y)) * z)) = x * (y * x). [para(6(a,1),5(a,1,1,2,1)),rewrite([6(18)])]. 16 (x * (y * x)) * ((z * ((u * (w * ((v5 * y) * w))) * z)) * (w * ((v5 * y) * w))) = x * (y * x). [para(5(a,1),6(a,1,2,1,2,1,2)),rewrite([5(14)])]. 17 (x * y) * ((z * ((u * ((w * x) * u)) * z)) * (y * (x * y))) = x * y. [para(5(a,1),6(a,1,2,1,2,1))]. 22 (x * (y * x)) * ((z * (y * z)) * (u * ((w * y) * u))) = x * (y * x). [para(5(a,1),7(a,1,2,2))]. 33 (x * y) * (((z * (x * z)) * (u * ((w * x) * u))) * (y * (x * y))) = x * y. [para(5(a,1),17(a,1,2,1,2))]. 42 (x * (y * x)) * ((z * (y * z)) * ((u * ((w * (v5 * y)) * u)) * (v5 * y))) = x * (y * x). [para(9(a,1),14(a,1,2,2))]. 50 (x * ((y * z) * x)) * (u * (((y * z) * (z * (y * z))) * u)) = x * ((y * z) * x). [para(8(a,1),16(a,1,2,1,2,1)),rewrite([5(22)])]. 66 (x * ((y * (z * y)) * x)) * (u * ((y * (z * y)) * u)) = x * ((y * (z * y)) * x). [para(50(a,1),42(a,1,2,2,1)),rewrite([5(24),5(20)])]. 68 ((x * (y * x)) * z) * (u * ((x * (y * x)) * u)) = (x * (y * x)) * z. [para(66(a,1),3(a,1,2,2)),rewrite([66(12)])]. 124 x * ((y * (z * y)) * (u * x)) = x. [para(68(a,1),3(a,1,2))]. 145 (x * (y * x)) * (z * (y * z)) = x * (y * x). [para(124(a,1),22(a,1,2))]. 152 (x * y) * (z * (x * z)) = x * y. [para(124(a,1),33(a,1,2,1)),rewrite([145(6)])]. 185 x * (y * (z * x)) = x. [para(152(a,1),3(a,1,2))]. 186 x * (y * (x * y)) = x. [para(3(a,1),152(a,1,1)),rewrite([3(7)])]. 200 (x * (y * x)) * (z * (y * u)) = x * (y * x). [para(152(a,1),185(a,1,2,2))]. 206 x * (y * x) = x. [para(152(a,1),186(a,1,2))]. 207 x * (y * z) = x. [para(186(a,1),185(a,1,2,2)),rewrite([206(2),206(4)])]. 209 x * y = x. [back_rewrite(200),rewrite([206(2),207(2),206(3)])]. 210 $F. [resolve(209,a,4,a)]. ============================== end of proof ==========================