%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : ALG010-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:06:54 AM UTC 2026
% Result : Unsatisfiable 5.28s 0.95s
% Output : Proof 6.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG010-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.18 % Computer : n005.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 19:17:01 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.28/0.95 Command-line arguments: --lhs-weight 9 --flip-ordering --complete-subsets --normalise-queue-percent 10 --cp-renormalise-threshold 10
% 5.28/0.95
% 5.28/0.95 % SZS status Unsatisfiable
% 5.28/0.95
% 6.32/1.05 % SZS output start Proof
% 6.32/1.05 Axiom 1 (m8): multiply(X, X) = one.
% 6.32/1.05 Axiom 2 (m3): multiply(X, one) = one.
% 6.32/1.06 Axiom 3 (m4): multiply(one, X) = X.
% 6.32/1.06 Axiom 4 (m9): multiply(X, multiply(Y, Z)) = multiply(Y, multiply(X, Z)).
% 6.32/1.06 Axiom 5 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 6.32/1.06 Axiom 6 (h): multiply(multiply(X, Y), multiply(X, Z)) = multiply(multiply(Y, X), multiply(Y, Z)).
% 6.32/1.06 Axiom 7 (m5): multiply(multiply(X, Y), multiply(multiply(Z, X), multiply(Z, Y))) = one.
% 6.32/1.06 Axiom 8 (m7): ifeq(multiply(X, Y), one, ifeq(multiply(Y, X), one, Y, X), X) = X.
% 6.32/1.06
% 6.32/1.06 Lemma 9: multiply(X, multiply(Y, X)) = one.
% 6.32/1.06 Proof:
% 6.32/1.06 multiply(X, multiply(Y, X))
% 6.32/1.06 = { by axiom 4 (m9) R->L }
% 6.32/1.06 multiply(Y, multiply(X, X))
% 6.32/1.06 = { by axiom 1 (m8) }
% 6.32/1.06 multiply(Y, one)
% 6.32/1.06 = { by axiom 2 (m3) }
% 6.32/1.06 one
% 6.32/1.06
% 6.32/1.06 Lemma 10: multiply(X, multiply(Y, multiply(Z, W))) = multiply(Y, multiply(Z, multiply(X, W))).
% 6.32/1.06 Proof:
% 6.32/1.06 multiply(X, multiply(Y, multiply(Z, W)))
% 6.32/1.06 = { by axiom 4 (m9) R->L }
% 6.32/1.06 multiply(Y, multiply(X, multiply(Z, W)))
% 6.32/1.06 = { by axiom 4 (m9) R->L }
% 6.32/1.06 multiply(Y, multiply(Z, multiply(X, W)))
% 6.32/1.06
% 6.32/1.06 Lemma 11: multiply(X, multiply(multiply(X, Y), Y)) = one.
% 6.32/1.06 Proof:
% 6.32/1.06 multiply(X, multiply(multiply(X, Y), Y))
% 6.32/1.06 = { by axiom 4 (m9) R->L }
% 6.32/1.06 multiply(multiply(X, Y), multiply(X, Y))
% 6.32/1.06 = { by axiom 1 (m8) }
% 6.32/1.06 one
% 6.32/1.06
% 6.32/1.06 Lemma 12: multiply(Y, multiply(multiply(Y, X), Z)) = multiply(X, multiply(multiply(X, Y), Z)).
% 6.32/1.06 Proof:
% 6.32/1.06 multiply(Y, multiply(multiply(Y, X), Z))
% 6.32/1.06 = { by axiom 4 (m9) R->L }
% 6.32/1.06 multiply(multiply(Y, X), multiply(Y, Z))
% 6.32/1.06 = { by axiom 6 (h) R->L }
% 6.32/1.06 multiply(multiply(X, Y), multiply(X, Z))
% 6.32/1.06 = { by axiom 4 (m9) }
% 6.32/1.06 multiply(X, multiply(multiply(X, Y), Z))
% 6.32/1.06
% 6.32/1.06 Lemma 13: multiply(multiply(Y, X), multiply(Y, Z)) = multiply(X, multiply(multiply(X, Y), Z)).
% 6.32/1.06 Proof:
% 6.32/1.06 multiply(multiply(Y, X), multiply(Y, Z))
% 6.32/1.06 = { by axiom 4 (m9) }
% 6.32/1.06 multiply(Y, multiply(multiply(Y, X), Z))
% 6.32/1.06 = { by lemma 12 R->L }
% 6.32/1.06 multiply(X, multiply(multiply(X, Y), Z))
% 6.32/1.06
% 6.32/1.06 Lemma 14: multiply(multiply(multiply(X, Y), Y), Y) = multiply(X, Y).
% 6.32/1.06 Proof:
% 6.32/1.06 multiply(multiply(multiply(X, Y), Y), Y)
% 6.32/1.06 = { by axiom 8 (m7) R->L }
% 6.32/1.06 ifeq(multiply(multiply(multiply(multiply(X, Y), Y), Y), multiply(X, Y)), one, ifeq(multiply(multiply(X, Y), multiply(multiply(multiply(X, Y), Y), Y)), one, multiply(X, Y), multiply(multiply(multiply(X, Y), Y), Y)), multiply(multiply(multiply(X, Y), Y), Y))
% 6.32/1.06 = { by axiom 3 (m4) R->L }
% 6.32/1.06 ifeq(multiply(multiply(multiply(multiply(X, Y), Y), Y), multiply(X, multiply(one, Y))), one, ifeq(multiply(multiply(X, Y), multiply(multiply(multiply(X, Y), Y), Y)), one, multiply(X, Y), multiply(multiply(multiply(X, Y), Y), Y)), multiply(multiply(multiply(X, Y), Y), Y))
% 6.32/1.06 = { by lemma 11 R->L }
% 6.32/1.06 ifeq(multiply(multiply(multiply(multiply(X, Y), Y), Y), multiply(X, multiply(multiply(X, multiply(multiply(X, Y), Y)), Y))), one, ifeq(multiply(multiply(X, Y), multiply(multiply(multiply(X, Y), Y), Y)), one, multiply(X, Y), multiply(multiply(multiply(X, Y), Y), Y)), multiply(multiply(multiply(X, Y), Y), Y))
% 6.32/1.06 = { by axiom 4 (m9) R->L }
% 6.32/1.06 ifeq(multiply(multiply(multiply(multiply(X, Y), Y), Y), multiply(multiply(X, multiply(multiply(X, Y), Y)), multiply(X, Y))), one, ifeq(multiply(multiply(X, Y), multiply(multiply(multiply(X, Y), Y), Y)), one, multiply(X, Y), multiply(multiply(multiply(X, Y), Y), Y)), multiply(multiply(multiply(X, Y), Y), Y))
% 6.32/1.06 = { by axiom 7 (m5) }
% 6.32/1.06 ifeq(one, one, ifeq(multiply(multiply(X, Y), multiply(multiply(multiply(X, Y), Y), Y)), one, multiply(X, Y), multiply(multiply(multiply(X, Y), Y), Y)), multiply(multiply(multiply(X, Y), Y), Y))
% 6.32/1.06 = { by axiom 5 (ifeq_axiom) }
% 6.32/1.06 ifeq(multiply(multiply(X, Y), multiply(multiply(multiply(X, Y), Y), Y)), one, multiply(X, Y), multiply(multiply(multiply(X, Y), Y), Y))
% 6.32/1.06 = { by axiom 4 (m9) R->L }
% 6.32/1.06 ifeq(multiply(multiply(multiply(X, Y), Y), multiply(multiply(X, Y), Y)), one, multiply(X, Y), multiply(multiply(multiply(X, Y), Y), Y))
% 6.32/1.06 = { by axiom 1 (m8) }
% 6.32/1.06 ifeq(one, one, multiply(X, Y), multiply(multiply(multiply(X, Y), Y), Y))
% 6.32/1.06 = { by axiom 5 (ifeq_axiom) }
% 6.32/1.06 multiply(X, Y)
% 6.32/1.06
% 6.32/1.06 Lemma 15: multiply(X, multiply(Y, multiply(multiply(X, Z), Z))) = one.
% 6.32/1.06 Proof:
% 6.32/1.06 multiply(X, multiply(Y, multiply(multiply(X, Z), Z)))
% 6.32/1.06 = { by axiom 4 (m9) R->L }
% 6.32/1.06 multiply(Y, multiply(X, multiply(multiply(X, Z), Z)))
% 6.32/1.06 = { by lemma 11 }
% 6.32/1.06 multiply(Y, one)
% 6.32/1.06 = { by axiom 2 (m3) }
% 6.32/1.06 one
% 6.32/1.06
% 6.32/1.06 Lemma 16: multiply(multiply(multiply(Y, Z), Z), multiply(X, Z)) = multiply(X, multiply(Y, Z)).
% 6.32/1.06 Proof:
% 6.32/1.06 multiply(multiply(multiply(Y, Z), Z), multiply(X, Z))
% 6.32/1.06 = { by axiom 4 (m9) }
% 6.32/1.06 multiply(X, multiply(multiply(multiply(Y, Z), Z), Z))
% 6.32/1.06 = { by lemma 14 }
% 6.32/1.06 multiply(X, multiply(Y, Z))
% 6.32/1.06
% 6.32/1.06 Lemma 17: multiply(multiply(multiply(X, Z), Z), multiply(Y, Z)) = multiply(X, multiply(Y, Z)).
% 6.32/1.06 Proof:
% 6.32/1.06 multiply(multiply(multiply(X, Z), Z), multiply(Y, Z))
% 6.32/1.06 = { by lemma 16 }
% 6.32/1.06 multiply(Y, multiply(X, Z))
% 6.32/1.06 = { by axiom 4 (m9) R->L }
% 6.32/1.06 multiply(X, multiply(Y, Z))
% 6.32/1.06
% 6.32/1.06 Lemma 18: multiply(multiply(multiply(X, Y), Y), multiply(multiply(X, Y), Z)) = multiply(Y, Z).
% 6.32/1.06 Proof:
% 6.32/1.06 multiply(multiply(multiply(X, Y), Y), multiply(multiply(X, Y), Z))
% 6.32/1.06 = { by axiom 4 (m9) R->L }
% 6.32/1.06 multiply(multiply(X, Y), multiply(multiply(multiply(X, Y), Y), Z))
% 6.32/1.06 = { by lemma 12 }
% 6.32/1.06 multiply(Y, multiply(multiply(Y, multiply(X, Y)), Z))
% 6.32/1.06 = { by lemma 9 }
% 6.32/1.06 multiply(Y, multiply(one, Z))
% 6.32/1.06 = { by axiom 3 (m4) }
% 6.32/1.06 multiply(Y, Z)
% 6.32/1.06
% 6.32/1.06 Lemma 19: multiply(X, multiply(multiply(multiply(multiply(Y, X), X), Z), Z)) = one.
% 6.32/1.06 Proof:
% 6.32/1.06 multiply(X, multiply(multiply(multiply(multiply(Y, X), X), Z), Z))
% 6.32/1.06 = { by lemma 18 R->L }
% 6.32/1.06 multiply(multiply(multiply(Y, X), X), multiply(multiply(Y, X), multiply(multiply(multiply(multiply(Y, X), X), Z), Z)))
% 6.32/1.06 = { by lemma 15 }
% 6.32/1.06 one
% 6.32/1.06
% 6.32/1.06 Lemma 20: multiply(Y, multiply(multiply(multiply(X, W), W), multiply(Z, W))) = multiply(X, multiply(Y, multiply(Z, W))).
% 6.32/1.06 Proof:
% 6.32/1.06 multiply(Y, multiply(multiply(multiply(X, W), W), multiply(Z, W)))
% 6.32/1.06 = { by lemma 17 }
% 6.32/1.06 multiply(Y, multiply(X, multiply(Z, W)))
% 6.32/1.06 = { by axiom 4 (m9) }
% 6.32/1.06 multiply(X, multiply(Y, multiply(Z, W)))
% 6.32/1.06
% 6.32/1.06 Lemma 21: multiply(multiply(X, Y), multiply(multiply(multiply(X, Y), Y), Z)) = multiply(Y, Z).
% 6.32/1.06 Proof:
% 6.32/1.06 multiply(multiply(X, Y), multiply(multiply(multiply(X, Y), Y), Z))
% 6.32/1.06 = { by axiom 4 (m9) }
% 6.32/1.06 multiply(multiply(multiply(X, Y), Y), multiply(multiply(X, Y), Z))
% 6.32/1.06 = { by lemma 18 }
% 6.32/1.06 multiply(Y, Z)
% 6.32/1.06
% 6.32/1.06 Lemma 22: multiply(multiply(multiply(X, W), W), multiply(Y, multiply(Z, W))) = multiply(X, multiply(Y, multiply(Z, W))).
% 6.32/1.06 Proof:
% 6.32/1.06 multiply(multiply(multiply(X, W), W), multiply(Y, multiply(Z, W)))
% 6.32/1.06 = { by axiom 4 (m9) R->L }
% 6.32/1.06 multiply(Y, multiply(multiply(multiply(X, W), W), multiply(Z, W)))
% 6.32/1.06 = { by lemma 20 }
% 6.32/1.06 multiply(X, multiply(Y, multiply(Z, W)))
% 6.32/1.06
% 6.32/1.06 Lemma 23: multiply(multiply(multiply(Z, W), W), multiply(Y, multiply(X, W))) = multiply(X, multiply(Y, multiply(Z, W))).
% 6.32/1.06 Proof:
% 6.32/1.06 multiply(multiply(multiply(Z, W), W), multiply(Y, multiply(X, W)))
% 6.32/1.06 = { by axiom 4 (m9) R->L }
% 6.32/1.06 multiply(Y, multiply(multiply(multiply(Z, W), W), multiply(X, W)))
% 6.32/1.06 = { by lemma 16 }
% 6.32/1.06 multiply(Y, multiply(X, multiply(Z, W)))
% 6.32/1.06 = { by axiom 4 (m9) }
% 6.32/1.06 multiply(X, multiply(Y, multiply(Z, W)))
% 6.32/1.06
% 6.32/1.06 Lemma 24: multiply(multiply(multiply(multiply(X, Y), Y), X), multiply(X, Y)) = multiply(X, Y).
% 6.32/1.06 Proof:
% 6.32/1.06 multiply(multiply(multiply(multiply(X, Y), Y), X), multiply(X, Y))
% 6.32/1.06 = { by lemma 14 R->L }
% 6.32/1.06 multiply(multiply(multiply(multiply(X, Y), Y), X), multiply(multiply(multiply(X, Y), Y), Y))
% 6.32/1.06 = { by axiom 4 (m9) R->L }
% 6.32/1.06 multiply(multiply(multiply(X, Y), Y), multiply(multiply(multiply(multiply(X, Y), Y), X), Y))
% 6.32/1.06 = { by lemma 12 }
% 6.32/1.06 multiply(X, multiply(multiply(X, multiply(multiply(X, Y), Y)), Y))
% 6.32/1.06 = { by lemma 11 }
% 6.32/1.06 multiply(X, multiply(one, Y))
% 6.32/1.06 = { by axiom 3 (m4) }
% 6.32/1.06 multiply(X, Y)
% 6.32/1.06
% 6.32/1.06 Lemma 25: multiply(multiply(multiply(multiply(X, Y), Y), X), multiply(Z, multiply(X, Y))) = multiply(Z, multiply(X, Y)).
% 6.32/1.06 Proof:
% 6.32/1.06 multiply(multiply(multiply(multiply(X, Y), Y), X), multiply(Z, multiply(X, Y)))
% 6.32/1.06 = { by axiom 4 (m9) R->L }
% 6.32/1.06 multiply(Z, multiply(multiply(multiply(multiply(X, Y), Y), X), multiply(X, Y)))
% 6.32/1.06 = { by lemma 24 }
% 6.32/1.06 multiply(Z, multiply(X, Y))
% 6.32/1.06
% 6.32/1.06 Lemma 26: multiply(multiply(multiply(multiply(X, Y), Y), X), multiply(multiply(X, Y), Z)) = multiply(multiply(X, Y), multiply(multiply(Y, X), Z)).
% 6.32/1.06 Proof:
% 6.32/1.06 multiply(multiply(multiply(multiply(X, Y), Y), X), multiply(multiply(X, Y), Z))
% 6.32/1.06 = { by lemma 24 R->L }
% 6.32/1.06 multiply(multiply(multiply(multiply(X, Y), Y), X), multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), multiply(X, Y)), Z))
% 6.32/1.06 = { by lemma 12 R->L }
% 6.32/1.06 multiply(multiply(X, Y), multiply(multiply(multiply(X, Y), multiply(multiply(multiply(X, Y), Y), X)), Z))
% 6.32/1.06 = { by lemma 21 }
% 6.32/1.06 multiply(multiply(X, Y), multiply(multiply(Y, X), Z))
% 6.32/1.06
% 6.32/1.06 Lemma 27: multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(Y, X), Z)) = multiply(multiply(X, Y), multiply(multiply(Y, X), Z)).
% 6.32/1.06 Proof:
% 6.32/1.06 multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(Y, X), Z))
% 6.32/1.06 = { by lemma 26 }
% 6.32/1.06 multiply(multiply(Y, X), multiply(multiply(X, Y), Z))
% 6.32/1.06 = { by axiom 4 (m9) R->L }
% 6.32/1.06 multiply(multiply(X, Y), multiply(multiply(Y, X), Z))
% 6.32/1.06
% 6.32/1.06 Lemma 28: multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(Y, X), Z)) = multiply(multiply(X, Y), multiply(multiply(multiply(multiply(X, Y), Y), X), Z)).
% 6.32/1.06 Proof:
% 6.32/1.06 multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(Y, X), Z))
% 6.32/1.06 = { by lemma 24 R->L }
% 6.32/1.06 multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(Y, X)), Z))
% 6.32/1.06 = { by lemma 12 R->L }
% 6.32/1.06 multiply(multiply(Y, X), multiply(multiply(multiply(Y, X), multiply(multiply(multiply(Y, X), X), Y)), Z))
% 6.32/1.06 = { by lemma 21 }
% 6.32/1.06 multiply(multiply(Y, X), multiply(multiply(X, Y), Z))
% 6.32/1.06 = { by axiom 4 (m9) }
% 6.32/1.06 multiply(multiply(X, Y), multiply(multiply(Y, X), Z))
% 6.32/1.06 = { by lemma 26 R->L }
% 6.32/1.06 multiply(multiply(multiply(multiply(X, Y), Y), X), multiply(multiply(X, Y), Z))
% 6.32/1.06 = { by axiom 4 (m9) R->L }
% 6.32/1.06 multiply(multiply(X, Y), multiply(multiply(multiply(multiply(X, Y), Y), X), Z))
% 6.32/1.06
% 6.32/1.06 Lemma 29: multiply(X, multiply(multiply(X, multiply(multiply(multiply(Y, Z), Z), W)), multiply(Z, W))) = one.
% 6.32/1.06 Proof:
% 6.32/1.06 multiply(X, multiply(multiply(X, multiply(multiply(multiply(Y, Z), Z), W)), multiply(Z, W)))
% 6.32/1.06 = { by lemma 10 R->L }
% 6.32/1.06 multiply(Z, multiply(X, multiply(multiply(X, multiply(multiply(multiply(Y, Z), Z), W)), W)))
% 6.32/1.06 = { by lemma 13 R->L }
% 6.32/1.06 multiply(Z, multiply(multiply(multiply(multiply(multiply(Y, Z), Z), W), X), multiply(multiply(multiply(multiply(Y, Z), Z), W), W)))
% 6.32/1.06 = { by axiom 4 (m9) R->L }
% 6.32/1.06 multiply(multiply(multiply(multiply(multiply(Y, Z), Z), W), X), multiply(Z, multiply(multiply(multiply(multiply(Y, Z), Z), W), W)))
% 6.32/1.06 = { by lemma 19 }
% 6.32/1.06 multiply(multiply(multiply(multiply(multiply(Y, Z), Z), W), X), one)
% 6.32/1.06 = { by axiom 2 (m3) }
% 6.32/1.06 one
% 6.32/1.06
% 6.32/1.06 Lemma 30: multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(Z, multiply(multiply(Y, X), W))) = multiply(multiply(X, Y), multiply(Z, multiply(multiply(Y, X), W))).
% 6.32/1.06 Proof:
% 6.32/1.06 multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(Z, multiply(multiply(Y, X), W)))
% 6.32/1.06 = { by axiom 4 (m9) R->L }
% 6.32/1.06 multiply(Z, multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(Y, X), W)))
% 6.32/1.06 = { by lemma 27 }
% 6.32/1.06 multiply(Z, multiply(multiply(X, Y), multiply(multiply(Y, X), W)))
% 6.32/1.06 = { by axiom 4 (m9) }
% 6.32/1.06 multiply(multiply(X, Y), multiply(Z, multiply(multiply(Y, X), W)))
% 6.32/1.06
% 6.32/1.06 Lemma 31: multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), Z), Z), multiply(multiply(Y, Z), Z)), multiply(multiply(Y, Z), W)) = multiply(multiply(multiply(multiply(X, Y), Y), Z), W).
% 6.32/1.06 Proof:
% 6.32/1.06 multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), Z), Z), multiply(multiply(Y, Z), Z)), multiply(multiply(Y, Z), W))
% 6.32/1.06 = { by lemma 16 }
% 6.32/1.06 multiply(multiply(multiply(Y, Z), multiply(multiply(multiply(X, Y), Y), Z)), multiply(multiply(Y, Z), W))
% 6.32/1.06 = { by lemma 13 }
% 6.32/1.06 multiply(multiply(multiply(multiply(X, Y), Y), Z), multiply(multiply(multiply(multiply(multiply(X, Y), Y), Z), multiply(Y, Z)), W))
% 6.32/1.06 = { by axiom 4 (m9) }
% 6.32/1.06 multiply(multiply(multiply(multiply(X, Y), Y), Z), multiply(multiply(Y, multiply(multiply(multiply(multiply(X, Y), Y), Z), Z)), W))
% 6.32/1.06 = { by axiom 4 (m9) R->L }
% 6.32/1.06 multiply(multiply(Y, multiply(multiply(multiply(multiply(X, Y), Y), Z), Z)), multiply(multiply(multiply(multiply(X, Y), Y), Z), W))
% 6.32/1.06 = { by lemma 19 }
% 6.32/1.06 multiply(one, multiply(multiply(multiply(multiply(X, Y), Y), Z), W))
% 6.32/1.06 = { by axiom 3 (m4) }
% 6.32/1.06 multiply(multiply(multiply(multiply(X, Y), Y), Z), W)
% 6.32/1.06
% 6.32/1.06 Lemma 32: multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(Y, X), X), Y), Y)) = one.
% 6.32/1.06 Proof:
% 6.32/1.06 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(Y, X), X), Y), Y))
% 6.32/1.06 = { by axiom 3 (m4) R->L }
% 6.32/1.06 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(one, multiply(multiply(multiply(multiply(Y, X), X), Y), Y)))
% 6.32/1.06 = { by axiom 2 (m3) R->L }
% 6.32/1.06 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), one), multiply(multiply(multiply(multiply(Y, X), X), Y), Y)))
% 6.32/1.06 = { by axiom 1 (m8) R->L }
% 6.32/1.06 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(X, Y), Y), X), X))), multiply(multiply(multiply(multiply(Y, X), X), Y), Y)))
% 6.32/1.06 = { by axiom 4 (m9) R->L }
% 6.32/1.06 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(multiply(multiply(X, Y), Y), X), X))), multiply(multiply(multiply(multiply(Y, X), X), Y), Y)))
% 6.32/1.06 = { by lemma 31 R->L }
% 6.32/1.06 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(Y, X), X)))), multiply(multiply(multiply(multiply(Y, X), X), Y), Y)))
% 6.32/1.06 = { by lemma 30 }
% 6.32/1.06 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(X, Y), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(Y, X), X)))), multiply(multiply(multiply(multiply(Y, X), X), Y), Y)))
% 6.32/1.06 = { by lemma 31 }
% 6.32/1.07 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(X, Y), multiply(multiply(multiply(multiply(X, Y), Y), X), X))), multiply(multiply(multiply(multiply(Y, X), X), Y), Y)))
% 6.32/1.07 = { by lemma 28 R->L }
% 6.32/1.07 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(Y, X), X))), multiply(multiply(multiply(multiply(Y, X), X), Y), Y)))
% 6.32/1.07 = { by lemma 27 }
% 6.32/1.07 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(X, Y), multiply(multiply(Y, X), X))), multiply(multiply(multiply(multiply(Y, X), X), Y), Y)))
% 6.32/1.07 = { by axiom 4 (m9) R->L }
% 6.32/1.07 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(X, Y), multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X))), multiply(multiply(multiply(multiply(Y, X), X), Y), Y)))
% 6.32/1.07 = { by lemma 30 R->L }
% 6.32/1.07 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X))), multiply(multiply(multiply(multiply(Y, X), X), Y), Y)))
% 6.32/1.07 = { by axiom 4 (m9) }
% 6.32/1.07 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X))), Y)))
% 6.32/1.07 = { by lemma 12 }
% 6.32/1.07 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(Y, X), X), Y)), Y)))
% 6.32/1.07 = { by axiom 3 (m4) R->L }
% 6.32/1.07 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(Y, X), X), Y)), multiply(one, Y))))
% 6.32/1.07 = { by axiom 2 (m3) R->L }
% 6.32/1.07 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(Y, X), X), Y)), multiply(multiply(multiply(Y, X), one), Y))))
% 6.32/1.07 = { by lemma 29 R->L }
% 6.32/1.07 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(Y, X), X), Y)), multiply(multiply(multiply(Y, X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(Y, X), X), Y)), multiply(X, Y)))), Y))))
% 6.32/1.07 = { by lemma 17 }
% 6.32/1.07 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(Y, X), X), Y)), multiply(multiply(multiply(Y, X), multiply(multiply(multiply(multiply(X, Y), Y), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(Y, X), X), Y)), multiply(X, Y)))), Y))))
% 6.32/1.07 = { by axiom 4 (m9) }
% 6.32/1.07 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(Y, X), X), Y)), multiply(multiply(multiply(Y, X), multiply(multiply(multiply(Y, X), multiply(multiply(multiply(X, Y), Y), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(Y, X), X), Y)), multiply(X, Y)))), Y))))
% 6.32/1.08 = { by lemma 12 R->L }
% 6.32/1.08 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(Y, X), X), Y)), multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), multiply(Y, X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(Y, X), X), Y)), multiply(X, Y)))), Y))))
% 6.32/1.08 = { by axiom 4 (m9) }
% 6.32/1.08 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(Y, X), X), Y)), multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), multiply(multiply(Y, multiply(multiply(multiply(multiply(X, Y), Y), X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(Y, X), X), Y)), multiply(X, Y)))), Y))))
% 6.32/1.08 = { by lemma 19 }
% 6.32/1.08 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(Y, X), X), Y)), multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), multiply(one, multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(Y, X), X), Y)), multiply(X, Y)))), Y))))
% 6.32/1.08 = { by axiom 3 (m4) }
% 6.32/1.08 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(Y, X), X), Y)), multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(Y, X), X), Y)), multiply(X, Y))), Y))))
% 6.32/1.08 = { by lemma 25 }
% 6.32/1.08 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(Y, X), X), Y)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(Y, X), X), Y)), multiply(X, Y)), Y))))
% 6.32/1.08 = { by lemma 13 R->L }
% 6.32/1.08 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(X, Y), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(Y, X), X), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.08 = { by lemma 23 R->L }
% 6.32/1.09 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), Y), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(X, Y), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.09 = { by lemma 22 }
% 6.32/1.09 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(Y, X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(X, Y), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.09 = { by lemma 20 R->L }
% 6.32/1.09 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), Y), multiply(multiply(X, Y), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.09 = { by lemma 16 }
% 6.32/1.09 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(X, Y), multiply(multiply(multiply(Y, X), X), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.09 = { by lemma 14 R->L }
% 6.32/1.09 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(X, Y), Y), Y), multiply(multiply(multiply(Y, X), X), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.09 = { by axiom 3 (m4) R->L }
% 6.32/1.09 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(X, Y), Y), multiply(one, Y)), multiply(multiply(multiply(Y, X), X), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.09 = { by lemma 9 R->L }
% 6.32/1.09 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(X, Y), Y), multiply(multiply(multiply(multiply(X, Y), Y), multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), Y), multiply(multiply(X, Y), Y))), Y)), multiply(multiply(multiply(Y, X), X), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.09 = { by lemma 12 }
% 6.32/1.09 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), Y), multiply(multiply(X, Y), Y)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), Y), multiply(multiply(X, Y), Y)), multiply(multiply(X, Y), Y)), Y)), multiply(multiply(multiply(Y, X), X), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.09 = { by lemma 31 }
% 6.32/1.09 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), Y), multiply(multiply(X, Y), Y)), multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), Y), Y)), multiply(multiply(multiply(Y, X), X), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.09 = { by axiom 4 (m9) }
% 6.32/1.09 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), Y), multiply(multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), Y), multiply(multiply(X, Y), Y)), Y)), multiply(multiply(multiply(Y, X), X), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.09 = { by lemma 16 }
% 6.32/1.09 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), Y), multiply(multiply(X, Y), Y)), multiply(multiply(multiply(Y, X), X), Y)), multiply(multiply(multiply(Y, X), X), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.09 = { by lemma 17 }
% 6.32/1.10 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(Y, X), X), multiply(multiply(X, Y), Y)), multiply(multiply(multiply(Y, X), X), Y)), multiply(multiply(multiply(Y, X), X), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.10 = { by lemma 13 }
% 6.32/1.10 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(X, Y), Y), multiply(multiply(multiply(multiply(X, Y), Y), multiply(multiply(Y, X), X)), Y)), multiply(multiply(multiply(Y, X), X), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.10 = { by lemma 16 }
% 6.32/1.10 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(X, Y), Y), multiply(multiply(Y, X), X)), multiply(X, Y)), multiply(multiply(multiply(Y, X), X), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.10 = { by lemma 17 R->L }
% 6.32/1.10 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(X, Y)), multiply(multiply(multiply(Y, X), X), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.10 = { by lemma 17 }
% 6.32/1.10 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(X, Y), Y), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(X, Y)), multiply(multiply(multiply(Y, X), X), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.10 = { by lemma 17 }
% 6.32/1.10 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(X, Y), Y), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(X, Y), Y), multiply(multiply(Y, X), X)), multiply(X, Y)), multiply(multiply(multiply(Y, X), X), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.10 = { by lemma 10 R->L }
% 6.32/1.10 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(Y, X), X), multiply(multiply(multiply(multiply(X, Y), Y), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(X, Y), Y), multiply(multiply(Y, X), X)), multiply(X, Y)), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.10 = { by lemma 13 R->L }
% 6.32/1.10 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(Y, X), X), multiply(multiply(multiply(X, Y), multiply(multiply(multiply(X, Y), Y), multiply(multiply(Y, X), X))), multiply(multiply(X, Y), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.10 = { by lemma 22 R->L }
% 6.32/1.10 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), Y), multiply(multiply(multiply(X, Y), multiply(multiply(multiply(X, Y), Y), multiply(multiply(Y, X), X))), multiply(multiply(X, Y), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.10 = { by lemma 10 R->L }
% 6.32/1.10 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), Y), multiply(multiply(multiply(Y, X), multiply(multiply(X, Y), multiply(multiply(multiply(X, Y), Y), X))), multiply(multiply(X, Y), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.10 = { by lemma 26 R->L }
% 6.32/1.10 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), Y), multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(Y, X), multiply(multiply(multiply(X, Y), Y), X))), multiply(multiply(X, Y), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.11 = { by axiom 4 (m9) R->L }
% 6.32/1.11 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), Y), multiply(multiply(multiply(Y, X), multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(multiply(X, Y), Y), X))), multiply(multiply(X, Y), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.11 = { by axiom 8 (m7) R->L }
% 6.32/1.11 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), Y), multiply(multiply(multiply(Y, X), ifeq(multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(multiply(X, Y), Y), X)), multiply(Y, X)), one, ifeq(multiply(multiply(Y, X), multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(multiply(X, Y), Y), X))), one, multiply(Y, X), multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(multiply(X, Y), Y), X))), multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(multiply(X, Y), Y), X)))), multiply(multiply(X, Y), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.11 = { by lemma 25 R->L }
% 6.32/1.11 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), Y), multiply(multiply(multiply(Y, X), ifeq(multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(multiply(X, Y), Y), X)), multiply(Y, X))), one, ifeq(multiply(multiply(Y, X), multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(multiply(X, Y), Y), X))), one, multiply(Y, X), multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(multiply(X, Y), Y), X))), multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(multiply(X, Y), Y), X)))), multiply(multiply(X, Y), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.11 = { by lemma 29 }
% 6.32/1.11 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), Y), multiply(multiply(multiply(Y, X), ifeq(one, one, ifeq(multiply(multiply(Y, X), multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(multiply(X, Y), Y), X))), one, multiply(Y, X), multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(multiply(X, Y), Y), X))), multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(multiply(X, Y), Y), X)))), multiply(multiply(X, Y), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.11 = { by axiom 5 (ifeq_axiom) }
% 6.32/1.11 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), Y), multiply(multiply(multiply(Y, X), ifeq(multiply(multiply(Y, X), multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(multiply(X, Y), Y), X))), one, multiply(Y, X), multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(multiply(X, Y), Y), X)))), multiply(multiply(X, Y), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.11 = { by lemma 23 R->L }
% 6.32/1.11 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), Y), multiply(multiply(multiply(Y, X), ifeq(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(Y, X), X))), one, multiply(Y, X), multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(multiply(X, Y), Y), X)))), multiply(multiply(X, Y), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.11 = { by lemma 28 }
% 6.32/1.11 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), Y), multiply(multiply(multiply(Y, X), ifeq(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(X, Y), multiply(multiply(multiply(multiply(X, Y), Y), X), X))), one, multiply(Y, X), multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(multiply(X, Y), Y), X)))), multiply(multiply(X, Y), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.11 = { by lemma 9 }
% 6.32/1.11 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), Y), multiply(multiply(multiply(Y, X), ifeq(one, one, multiply(Y, X), multiply(multiply(multiply(multiply(Y, X), X), Y), multiply(multiply(multiply(X, Y), Y), X)))), multiply(multiply(X, Y), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.11 = { by axiom 5 (ifeq_axiom) }
% 6.32/1.12 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), Y), multiply(multiply(multiply(Y, X), multiply(Y, X)), multiply(multiply(X, Y), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.12 = { by axiom 1 (m8) }
% 6.32/1.12 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), Y), multiply(one, multiply(multiply(X, Y), Y))), multiply(multiply(X, Y), Y))))
% 6.32/1.12 = { by axiom 3 (m4) }
% 6.32/1.12 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(multiply(multiply(Y, X), X), Y), Y), multiply(multiply(X, Y), Y)), multiply(multiply(X, Y), Y))))
% 6.32/1.12 = { by lemma 31 }
% 6.32/1.12 multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(multiply(multiply(multiply(multiply(X, Y), Y), X), X), multiply(multiply(Y, X), X)), multiply(multiply(multiply(multiply(Y, X), X), Y), Y)))
% 6.32/1.12 = { by lemma 12 R->L }
% 6.32/1.12 multiply(multiply(multiply(Y, X), X), multiply(multiply(multiply(multiply(Y, X), X), multiply(multiply(multiply(multiply(X, Y), Y), X), X)), multiply(multiply(multiply(multiply(Y, X), X), Y), Y)))
% 6.32/1.12 = { by lemma 15 }
% 6.32/1.12 one
% 6.32/1.12
% 6.32/1.12 Goal 1 (prove_j): multiply(multiply(multiply(multiply(a, b), b), a), a) = multiply(multiply(multiply(multiply(b, a), a), b), b).
% 6.32/1.12 Proof:
% 6.32/1.12 multiply(multiply(multiply(multiply(a, b), b), a), a)
% 6.32/1.12 = { by axiom 8 (m7) R->L }
% 6.32/1.12 ifeq(multiply(multiply(multiply(multiply(multiply(a, b), b), a), a), multiply(multiply(multiply(multiply(b, a), a), b), b)), one, ifeq(multiply(multiply(multiply(multiply(multiply(b, a), a), b), b), multiply(multiply(multiply(multiply(a, b), b), a), a)), one, multiply(multiply(multiply(multiply(b, a), a), b), b), multiply(multiply(multiply(multiply(a, b), b), a), a)), multiply(multiply(multiply(multiply(a, b), b), a), a))
% 6.32/1.12 = { by lemma 32 }
% 6.32/1.12 ifeq(one, one, ifeq(multiply(multiply(multiply(multiply(multiply(b, a), a), b), b), multiply(multiply(multiply(multiply(a, b), b), a), a)), one, multiply(multiply(multiply(multiply(b, a), a), b), b), multiply(multiply(multiply(multiply(a, b), b), a), a)), multiply(multiply(multiply(multiply(a, b), b), a), a))
% 6.32/1.12 = { by axiom 5 (ifeq_axiom) }
% 6.32/1.12 ifeq(multiply(multiply(multiply(multiply(multiply(b, a), a), b), b), multiply(multiply(multiply(multiply(a, b), b), a), a)), one, multiply(multiply(multiply(multiply(b, a), a), b), b), multiply(multiply(multiply(multiply(a, b), b), a), a))
% 6.32/1.12 = { by lemma 32 }
% 6.32/1.12 ifeq(one, one, multiply(multiply(multiply(multiply(b, a), a), b), b), multiply(multiply(multiply(multiply(a, b), b), a), a))
% 6.32/1.12 = { by axiom 5 (ifeq_axiom) }
% 6.32/1.12 multiply(multiply(multiply(multiply(b, a), a), b), b)
% 6.32/1.12 % SZS output end Proof
% 6.32/1.12
% 6.32/1.12 RESULT: Unsatisfiable (the axioms are contradictory).
%------------------------------------------------------------------------------