============================== prooftrans ============================ Prover9 (32) version Dec-2007, Dec 2007. Process 25184 was started by Papuchino on HISOKA, Thu Nov 28 23:00:31 2024 The command was "/cygdrive/c/Program Files (x86)/Prover9-Mace4/bin-win32/prover9". ============================== end of head =========================== ============================== end of input ========================== ============================== PROOF ================================= % -------- Comments from original proof -------- % Proof 1 at 0.38 (+ 0.25) seconds. % Length of proof is 43. % Level of proof is 16. % Maximum clause weight is 27. % Given clauses 130. 1 x = y * ((((y * y) * x) * z) * (((y * y) * y) * z)) # label(non_clause) # label(goal). [goal]. 2 x = (y * y) * (((x * y) * z) * ((x * (y * x)) * z)). [assumption]. 3 (x * x) * (((y * x) * z) * ((y * (x * y)) * z)) = y. [copy(2),flip(a)]. 4 x * x = y * y. [assumption]. 5 c2 * ((((c2 * c2) * c1) * c3) * (((c2 * c2) * c2) * c3)) != c1. [deny(1)]. 6 (x * x) * (((y * z) * u) * ((y * (z * y)) * u)) = y. [para(4(a,1),3(a,1,1))]. 7 c2 * ((((x * x) * c1) * c3) * (((c2 * c2) * c2) * c3)) != c1. [para(4(a,1),5(a,1,2,1,1,1))]. 8 c2 * ((((x * x) * c1) * c3) * (((y * y) * c2) * c3)) != c1. [para(4(a,1),7(a,1,2,2,1,1))]. 9 (x * x) * (((y * y) * z) * ((u * (u * u)) * z)) = u. [para(4(a,1),6(a,1,2,1,1))]. 10 (x * x) * ((y * y) * ((z * (u * z)) * (z * u))) = z. [para(4(a,1),6(a,1,2,1))]. 11 (x * x) * (((y * z) * (y * (z * y))) * (u * u)) = y. [para(4(a,1),6(a,1,2,2))]. 12 (x * x) * ((y * y) * ((z * (z * z)) * (u * u))) = z. [para(4(a,1),9(a,1,2,1))]. 13 (x * x) * (((y * y) * z) * ((u * (w * w)) * z)) = u. [para(4(a,1),9(a,1,2,2,1,2))]. 14 (x * x) * (y * (z * z)) = (y * u) * (y * (u * y)). [para(11(a,1),11(a,1,2,1))]. 15 (x * y) * (x * (y * x)) = (z * z) * (x * (u * u)). [copy(14),flip(a)]. 16 (x * x) * ((y * y) * ((z * (u * u)) * (w * w))) = z. [para(4(a,1),12(a,1,2,2,1,2))]. 17 (x * x) * (((y * y) * (z * (u * u))) * (w * w)) = z. [para(4(a,1),13(a,1,2,2))]. 18 (x * x) * (y * ((z * (u * u)) * ((w * w) * ((y * (v5 * y)) * (y * v5))))) = z. [para(10(a,1),13(a,1,2,1))]. 19 ((x * x) * y) * ((x * x) * (y * (x * x))) = z * z. [para(15(a,2),4(a,1))]. 20 x * ((y * y) * (((z * z) * ((x * (u * u)) * (w * w))) * (y * y))) = v5 * v5. [para(16(a,1),19(a,1,1))]. 21 x * (x * (y * y)) = z * z. [para(17(a,1),20(a,1,2))]. 22 (x * (x * (y * y))) * ((z * z) * ((u * (w * u)) * (u * w))) = u. [para(21(a,2),10(a,1,1))]. 23 (x * x) * (((y * y) * ((z * (u * u)) * (w * w))) * (v5 * v5)) = z. [para(21(a,1),13(a,1,2,2))]. 24 x * (y * y) = x. [para(17(a,1),23(a,1))]. 25 (x * (x * (y * y))) * (((z * z) * u) * ((w * (v5 * v5)) * u)) = w. [para(21(a,2),13(a,1,1))]. 26 (x * x) * (((z * z) * u) * ((w * (v5 * v5)) * u)) = w. [para(24(a,1),25(a,1,1,2))]. 27 (x * x) * (((y * y) * z) * (u * z)) = u. [para(24(a,1),26(a,1,2,2,1))]. 28 (x * x) * ((y * (y * (z * z))) * ((u * (w * w)) * (v5 * v5))) = u. [para(21(a,2),13(a,1,2,1))]. 29 (x * x) * ((y * y) * ((u * (w * w)) * (v5 * v5))) = u. [para(24(a,1),28(a,1,2,1,2))]. 30 (x * x) * ((y * y) * (u * (v5 * v5))) = u. [para(24(a,1),29(a,1,2,2,1))]. 31 (x * x) * ((y * y) * z) = z. [para(24(a,1),30(a,1,2,2))]. 32 (x * y) * (x * (y * x)) = (z * (z * (u * u))) * (x * (w * w)). [para(21(a,2),15(a,2,1))]. 33 (x * y) * (x * (y * x)) = (z * z) * (x * (w * w)). [para(24(a,1),32(a,2,1,2))]. 34 (x * y) * (x * (y * x)) = (z * z) * x. [para(24(a,1),33(a,2,2))]. 35 (x * x) * ((z * z) * ((u * (w * u)) * (u * w))) = u. [para(24(a,1),22(a,1,1,2))]. 36 (x * (y * x)) * (x * y) = x. [para(31(a,1),35(a,1))]. 37 (x * x) * (y * (z * ((w * w) * ((y * (v5 * y)) * (y * v5))))) = z. [para(24(a,1),18(a,1,2,2,1))]. 38 (x * x) * (y * (z * ((u * u) * y))) = z. [para(36(a,1),37(a,1,2,2,2,2))]. 39 (x * x) * y = ((z * z) * u) * (y * u). [para(27(a,1),31(a,1,2))]. 40 ((x * x) * y) * (z * y) = (u * u) * z. [copy(39),flip(a)]. 41 c2 * ((((c1 * x) * (c1 * (x * c1))) * c3) * (((y * y) * c2) * c3)) != c1. [para(34(a,2),8(a,1,2,1,1))]. 42 (x * x) * y = z * (y * ((u * u) * z)). [para(38(a,1),31(a,1,2))]. 43 ((x * x) * (y * (z * y))) * ((u * u) * y) = (w * w) * (y * z). [para(34(a,1),40(a,1,2))]. 44 c2 * ((((c1 * x) * (c1 * (x * c1))) * c3) * ((((y * y) * z) * (c2 * z)) * c3)) != c1. [para(40(a,2),41(a,1,2,2,1))]. 45 ((x * x) * (y * z)) * ((u * u) * y) = (w * w) * ((v5 * v5) * z). [para(40(a,1),40(a,1,2))]. 46 ((x * x) * (y * z)) * ((u * u) * y) = z. [para(31(a,1),45(a,2))]. 47 z * y = (w * w) * (y * z). [para(46(a,1),43(a,1))]. 48 (x * x) * (y * z) = z * y. [copy(47),flip(a)]. 49 ((x * (y * x)) * z) * ((x * y) * z) = x. [para(48(a,1),6(a,1))]. 50 (x * y) * ((z * z) * y) = x. [para(48(a,1),27(a,1))]. 51 (x * ((y * y) * z)) * z = x. [para(48(a,1),38(a,1))]. 52 (x * (y * z)) * (z * y) = x. [para(48(a,1),50(a,1,2))]. 53 (x * y) * (z * (y * ((u * u) * z))) = x. [para(38(a,1),51(a,1,1,2))]. 54 x * ((y * z) * ((u * u) * x)) = z * y. [para(42(a,1),48(a,1))]. 55 x * (y * (x * z)) = (x * (z * x)) * y. [para(49(a,1),52(a,1,1))]. 56 (x * (y * x)) * z = x * (z * (x * y)). [copy(55),flip(a)]. 57 (x * (y * (z * (y * u)))) * (z * (y * (u * y))) = x. [para(56(a,1),52(a,1,1,2))]. 58 (x * ((y * ((z * z) * x)) * x)) * (u * y) = x * u. [para(53(a,1),56(a,2,2))]. 59 (x * y) * (z * y) = x * z. [para(51(a,1),58(a,1,1,2))]. 60 c2 * ((((c1 * (x * (y * x))) * (c1 * (x * (c1 * (x * y))))) * c3) * ((((z * z) * u) * (c2 * u)) * c3)) != c1. [para(56(a,1),44(a,1,2,1,1,2,2))]. 61 c2 * ((((c1 * (x * (y * x))) * (c1 * (x * (c1 * (x * y))))) * c3) * (((z * z) * c2) * c3)) != c1. [para(59(a,1),60(a,1,2,2,1))]. 62 c2 * (((c1 * (x * (y * x))) * (c1 * (x * (c1 * (x * y))))) * ((z * z) * c2)) != c1. [para(59(a,1),61(a,1,2))]. 63 (c1 * (x * (c1 * (x * y)))) * (c1 * (x * (y * x))) != c1. [para(54(a,1),62(a,1))]. 64 c1 != c1. [para(57(a,1),63(a,1))]. 65 $F. [copy(64),xx(a)]. ============================== end of proof ==========================