%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : BOO007-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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:35:21 AM UTC 2026
% Result : Unsatisfiable 128.24s 16.40s
% Output : Proof 129.86s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : BOO007-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.02 % Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.00/0.11 % Computer : n012.cluster.edu
% 0.00/0.11 % Model : x86_64 x86_64
% 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.11 % Memory : 8046.5625MB
% 0.00/0.11 % OS : Linux 6.8.0-71-generic
% 0.00/0.11 % CPULimit : 300
% 0.00/0.11 % WCLimit : 300
% 0.00/0.11 % DateTime : Mon Sep 28 21:03:04 UTC 2026
% 0.00/0.11 % CPUTime :
% 0.00/0.11 Running run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 128.24/16.40 Command-line arguments: --lhs-weight 1 --flip-ordering --normalise-queue-percent 10 --cp-renormalise-threshold 10 --complete-subsets --ground-joining-incomplete-limit 15 --flatten-regeneralise
% 128.24/16.40
% 128.24/16.40 % SZS status Unsatisfiable
% 128.24/16.40
% 129.04/16.49 % SZS output start Proof
% 129.04/16.49 Axiom 1 (multiplicative_identity2): product(X, multiplicative_identity, X) = true.
% 129.04/16.49 Axiom 2 (multiplicative_inverse2): product(X, inverse(X), additive_identity) = true.
% 129.04/16.49 Axiom 3 (multiplicative_identity1): product(multiplicative_identity, X, X) = true.
% 129.04/16.49 Axiom 4 (y_times_z): product(y, z, y_times_z) = true.
% 129.04/16.49 Axiom 5 (x_times__y_times_z): product(x, y_times_z, x_times__y_times_z) = true.
% 129.04/16.49 Axiom 6 (x_times_y): product(x, y, x_times_y) = true.
% 129.04/16.49 Axiom 7 (x_times_y__times_z): product(x_times_y, z, x_times_y__times_z) = true.
% 129.04/16.49 Axiom 8 (multiplicative_inverse1): product(inverse(X), X, additive_identity) = true.
% 129.04/16.49 Axiom 9 (additive_identity2): sum(X, additive_identity, X) = true.
% 129.04/16.49 Axiom 10 (additive_inverse2): sum(X, inverse(X), multiplicative_identity) = true.
% 129.04/16.49 Axiom 11 (additive_identity1): sum(additive_identity, X, X) = true.
% 129.04/16.49 Axiom 12 (additive_inverse1): sum(inverse(X), X, multiplicative_identity) = true.
% 129.04/16.49 Axiom 13 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 129.04/16.49 Axiom 14 (ifeq_axiom): ifeq2(X, X, Y, Z) = Y.
% 129.04/16.49 Axiom 15 (closure_of_multiplication): product(X, Y, multiply(X, Y)) = true.
% 129.04/16.49 Axiom 16 (closure_of_addition): sum(X, Y, add(X, Y)) = true.
% 129.04/16.49 Axiom 17 (commutativity_of_multiplication): ifeq(product(X, Y, Z), true, product(Y, X, Z), true) = true.
% 129.04/16.49 Axiom 18 (commutativity_of_addition): ifeq(sum(X, Y, Z), true, sum(Y, X, Z), true) = true.
% 129.04/16.49 Axiom 19 (multiplication_is_well_defined): ifeq2(product(X, Y, Z), true, ifeq2(product(X, Y, W), true, W, Z), Z) = Z.
% 129.04/16.49 Axiom 20 (addition_is_well_defined): ifeq2(sum(X, Y, Z), true, ifeq2(sum(X, Y, W), true, W, Z), Z) = Z.
% 129.04/16.49 Axiom 21 (distributivity1): ifeq(product(X, Y, Z), true, ifeq(product(X, W, V), true, ifeq(product(X, U, T), true, ifeq(sum(U, W, Y), true, sum(T, V, Z), true), true), true), true) = true.
% 129.04/16.49 Axiom 22 (distributivity2): ifeq(product(X, Y, Z), true, ifeq(product(X, W, V), true, ifeq(sum(V, Z, U), true, ifeq(sum(W, Y, T), true, product(X, T, U), true), true), true), true) = true.
% 129.04/16.49 Axiom 23 (distributivity8): ifeq(product(X, Y, Z), true, ifeq(product(W, V, U), true, ifeq(sum(V, T, Y), true, ifeq(sum(W, T, X), true, sum(U, T, Z), true), true), true), true) = true.
% 129.04/16.49
% 129.04/16.49 Lemma 24: add(X, Y) = add(Y, X).
% 129.04/16.49 Proof:
% 129.04/16.49 add(X, Y)
% 129.04/16.49 = { by axiom 20 (addition_is_well_defined) R->L }
% 129.04/16.49 ifeq2(sum(Y, X, add(X, Y)), true, ifeq2(sum(Y, X, add(Y, X)), true, add(Y, X), add(X, Y)), add(X, Y))
% 129.04/16.49 = { by axiom 16 (closure_of_addition) }
% 129.04/16.49 ifeq2(sum(Y, X, add(X, Y)), true, ifeq2(true, true, add(Y, X), add(X, Y)), add(X, Y))
% 129.04/16.49 = { by axiom 14 (ifeq_axiom) }
% 129.04/16.49 ifeq2(sum(Y, X, add(X, Y)), true, add(Y, X), add(X, Y))
% 129.04/16.49 = { by axiom 13 (ifeq_axiom) R->L }
% 129.04/16.49 ifeq2(ifeq(true, true, sum(Y, X, add(X, Y)), true), true, add(Y, X), add(X, Y))
% 129.04/16.49 = { by axiom 16 (closure_of_addition) R->L }
% 129.04/16.49 ifeq2(ifeq(sum(X, Y, add(X, Y)), true, sum(Y, X, add(X, Y)), true), true, add(Y, X), add(X, Y))
% 129.04/16.49 = { by axiom 18 (commutativity_of_addition) }
% 129.04/16.49 ifeq2(true, true, add(Y, X), add(X, Y))
% 129.04/16.49 = { by axiom 14 (ifeq_axiom) }
% 129.04/16.49 add(Y, X)
% 129.04/16.49
% 129.04/16.49 Lemma 25: add(X, multiplicative_identity) = multiplicative_identity.
% 129.04/16.49 Proof:
% 129.04/16.49 add(X, multiplicative_identity)
% 129.04/16.49 = { by axiom 20 (addition_is_well_defined) R->L }
% 129.04/16.49 ifeq2(sum(inverse(X), X, add(X, multiplicative_identity)), true, ifeq2(sum(inverse(X), X, multiplicative_identity), true, multiplicative_identity, add(X, multiplicative_identity)), add(X, multiplicative_identity))
% 129.04/16.49 = { by axiom 12 (additive_inverse1) }
% 129.04/16.49 ifeq2(sum(inverse(X), X, add(X, multiplicative_identity)), true, ifeq2(true, true, multiplicative_identity, add(X, multiplicative_identity)), add(X, multiplicative_identity))
% 129.04/16.49 = { by axiom 14 (ifeq_axiom) }
% 129.04/16.49 ifeq2(sum(inverse(X), X, add(X, multiplicative_identity)), true, multiplicative_identity, add(X, multiplicative_identity))
% 129.04/16.49 = { by lemma 24 R->L }
% 129.04/16.49 ifeq2(sum(inverse(X), X, add(multiplicative_identity, X)), true, multiplicative_identity, add(X, multiplicative_identity))
% 129.04/16.49 = { by axiom 13 (ifeq_axiom) R->L }
% 129.04/16.49 ifeq2(ifeq(true, true, sum(inverse(X), X, add(multiplicative_identity, X)), true), true, multiplicative_identity, add(X, multiplicative_identity))
% 129.04/16.49 = { by axiom 16 (closure_of_addition) R->L }
% 129.04/16.49 ifeq2(ifeq(sum(multiplicative_identity, X, add(multiplicative_identity, X)), true, sum(inverse(X), X, add(multiplicative_identity, X)), true), true, multiplicative_identity, add(X, multiplicative_identity))
% 129.04/16.49 = { by axiom 13 (ifeq_axiom) R->L }
% 129.04/16.49 ifeq2(ifeq(sum(multiplicative_identity, X, add(multiplicative_identity, X)), true, ifeq(true, true, sum(inverse(X), X, add(multiplicative_identity, X)), true), true), true, multiplicative_identity, add(X, multiplicative_identity))
% 129.04/16.49 = { by axiom 12 (additive_inverse1) R->L }
% 129.04/16.49 ifeq2(ifeq(sum(multiplicative_identity, X, add(multiplicative_identity, X)), true, ifeq(sum(inverse(X), X, multiplicative_identity), true, sum(inverse(X), X, add(multiplicative_identity, X)), true), true), true, multiplicative_identity, add(X, multiplicative_identity))
% 129.04/16.49 = { by axiom 13 (ifeq_axiom) R->L }
% 129.04/16.49 ifeq2(ifeq(true, true, ifeq(sum(multiplicative_identity, X, add(multiplicative_identity, X)), true, ifeq(sum(inverse(X), X, multiplicative_identity), true, sum(inverse(X), X, add(multiplicative_identity, X)), true), true), true), true, multiplicative_identity, add(X, multiplicative_identity))
% 129.04/16.49 = { by axiom 3 (multiplicative_identity1) R->L }
% 129.04/16.49 ifeq2(ifeq(product(multiplicative_identity, add(multiplicative_identity, X), add(multiplicative_identity, X)), true, ifeq(sum(multiplicative_identity, X, add(multiplicative_identity, X)), true, ifeq(sum(inverse(X), X, multiplicative_identity), true, sum(inverse(X), X, add(multiplicative_identity, X)), true), true), true), true, multiplicative_identity, add(X, multiplicative_identity))
% 129.04/16.49 = { by axiom 13 (ifeq_axiom) R->L }
% 129.04/16.49 ifeq2(ifeq(product(multiplicative_identity, add(multiplicative_identity, X), add(multiplicative_identity, X)), true, ifeq(true, true, ifeq(sum(multiplicative_identity, X, add(multiplicative_identity, X)), true, ifeq(sum(inverse(X), X, multiplicative_identity), true, sum(inverse(X), X, add(multiplicative_identity, X)), true), true), true), true), true, multiplicative_identity, add(X, multiplicative_identity))
% 129.04/16.49 = { by axiom 1 (multiplicative_identity2) R->L }
% 129.04/16.49 ifeq2(ifeq(product(multiplicative_identity, add(multiplicative_identity, X), add(multiplicative_identity, X)), true, ifeq(product(inverse(X), multiplicative_identity, inverse(X)), true, ifeq(sum(multiplicative_identity, X, add(multiplicative_identity, X)), true, ifeq(sum(inverse(X), X, multiplicative_identity), true, sum(inverse(X), X, add(multiplicative_identity, X)), true), true), true), true), true, multiplicative_identity, add(X, multiplicative_identity))
% 129.04/16.49 = { by axiom 23 (distributivity8) }
% 129.04/16.49 ifeq2(true, true, multiplicative_identity, add(X, multiplicative_identity))
% 129.04/16.49 = { by axiom 14 (ifeq_axiom) }
% 129.04/16.49 multiplicative_identity
% 129.04/16.49
% 129.04/16.49 Lemma 26: multiply(X, Y) = multiply(Y, X).
% 129.04/16.49 Proof:
% 129.04/16.49 multiply(X, Y)
% 129.04/16.49 = { by axiom 19 (multiplication_is_well_defined) R->L }
% 129.04/16.49 ifeq2(product(Y, X, multiply(X, Y)), true, ifeq2(product(Y, X, multiply(Y, X)), true, multiply(Y, X), multiply(X, Y)), multiply(X, Y))
% 129.04/16.49 = { by axiom 15 (closure_of_multiplication) }
% 129.04/16.49 ifeq2(product(Y, X, multiply(X, Y)), true, ifeq2(true, true, multiply(Y, X), multiply(X, Y)), multiply(X, Y))
% 129.04/16.50 = { by axiom 14 (ifeq_axiom) }
% 129.04/16.50 ifeq2(product(Y, X, multiply(X, Y)), true, multiply(Y, X), multiply(X, Y))
% 129.04/16.50 = { by axiom 13 (ifeq_axiom) R->L }
% 129.04/16.50 ifeq2(ifeq(true, true, product(Y, X, multiply(X, Y)), true), true, multiply(Y, X), multiply(X, Y))
% 129.04/16.50 = { by axiom 15 (closure_of_multiplication) R->L }
% 129.04/16.50 ifeq2(ifeq(product(X, Y, multiply(X, Y)), true, product(Y, X, multiply(X, Y)), true), true, multiply(Y, X), multiply(X, Y))
% 129.04/16.50 = { by axiom 17 (commutativity_of_multiplication) }
% 129.04/16.50 ifeq2(true, true, multiply(Y, X), multiply(X, Y))
% 129.04/16.50 = { by axiom 14 (ifeq_axiom) }
% 129.04/16.50 multiply(Y, X)
% 129.04/16.50
% 129.04/16.50 Lemma 27: ifeq2(product(inverse(X), X, Y), true, additive_identity, Y) = Y.
% 129.04/16.50 Proof:
% 129.04/16.50 ifeq2(product(inverse(X), X, Y), true, additive_identity, Y)
% 129.04/16.50 = { by axiom 14 (ifeq_axiom) R->L }
% 129.04/16.50 ifeq2(product(inverse(X), X, Y), true, ifeq2(true, true, additive_identity, Y), Y)
% 129.04/16.50 = { by axiom 8 (multiplicative_inverse1) R->L }
% 129.04/16.50 ifeq2(product(inverse(X), X, Y), true, ifeq2(product(inverse(X), X, additive_identity), true, additive_identity, Y), Y)
% 129.04/16.50 = { by axiom 19 (multiplication_is_well_defined) }
% 129.04/16.50 Y
% 129.04/16.50
% 129.04/16.50 Lemma 28: multiply(y_times_z, inverse(y)) = additive_identity.
% 129.04/16.50 Proof:
% 129.04/16.50 multiply(y_times_z, inverse(y))
% 129.04/16.50 = { by lemma 27 R->L }
% 129.04/16.50 ifeq2(product(inverse(y), y, multiply(y_times_z, inverse(y))), true, additive_identity, multiply(y_times_z, inverse(y)))
% 129.04/16.50 = { by axiom 13 (ifeq_axiom) R->L }
% 129.04/16.50 ifeq2(ifeq(true, true, product(inverse(y), y, multiply(y_times_z, inverse(y))), true), true, additive_identity, multiply(y_times_z, inverse(y)))
% 129.04/16.50 = { by axiom 21 (distributivity1) R->L }
% 129.04/16.50 ifeq2(ifeq(ifeq(product(y, multiplicative_identity, y), true, ifeq(product(y, multiplicative_identity, y), true, ifeq(product(y, z, y_times_z), true, ifeq(sum(z, multiplicative_identity, multiplicative_identity), true, sum(y_times_z, y, y), true), true), true), true), true, product(inverse(y), y, multiply(y_times_z, inverse(y))), true), true, additive_identity, multiply(y_times_z, inverse(y)))
% 129.04/16.50 = { by axiom 1 (multiplicative_identity2) }
% 129.04/16.50 ifeq2(ifeq(ifeq(true, true, ifeq(product(y, multiplicative_identity, y), true, ifeq(product(y, z, y_times_z), true, ifeq(sum(z, multiplicative_identity, multiplicative_identity), true, sum(y_times_z, y, y), true), true), true), true), true, product(inverse(y), y, multiply(y_times_z, inverse(y))), true), true, additive_identity, multiply(y_times_z, inverse(y)))
% 129.04/16.50 = { by axiom 13 (ifeq_axiom) }
% 129.04/16.50 ifeq2(ifeq(ifeq(product(y, multiplicative_identity, y), true, ifeq(product(y, z, y_times_z), true, ifeq(sum(z, multiplicative_identity, multiplicative_identity), true, sum(y_times_z, y, y), true), true), true), true, product(inverse(y), y, multiply(y_times_z, inverse(y))), true), true, additive_identity, multiply(y_times_z, inverse(y)))
% 129.04/16.50 = { by axiom 1 (multiplicative_identity2) }
% 129.04/16.50 ifeq2(ifeq(ifeq(true, true, ifeq(product(y, z, y_times_z), true, ifeq(sum(z, multiplicative_identity, multiplicative_identity), true, sum(y_times_z, y, y), true), true), true), true, product(inverse(y), y, multiply(y_times_z, inverse(y))), true), true, additive_identity, multiply(y_times_z, inverse(y)))
% 129.04/16.50 = { by axiom 13 (ifeq_axiom) }
% 129.04/16.50 ifeq2(ifeq(ifeq(product(y, z, y_times_z), true, ifeq(sum(z, multiplicative_identity, multiplicative_identity), true, sum(y_times_z, y, y), true), true), true, product(inverse(y), y, multiply(y_times_z, inverse(y))), true), true, additive_identity, multiply(y_times_z, inverse(y)))
% 129.04/16.50 = { by lemma 25 R->L }
% 129.04/16.50 ifeq2(ifeq(ifeq(product(y, z, y_times_z), true, ifeq(sum(z, multiplicative_identity, add(z, multiplicative_identity)), true, sum(y_times_z, y, y), true), true), true, product(inverse(y), y, multiply(y_times_z, inverse(y))), true), true, additive_identity, multiply(y_times_z, inverse(y)))
% 129.04/16.50 = { by axiom 16 (closure_of_addition) }
% 129.04/16.50 ifeq2(ifeq(ifeq(product(y, z, y_times_z), true, ifeq(true, true, sum(y_times_z, y, y), true), true), true, product(inverse(y), y, multiply(y_times_z, inverse(y))), true), true, additive_identity, multiply(y_times_z, inverse(y)))
% 129.04/16.50 = { by axiom 13 (ifeq_axiom) }
% 129.04/16.50 ifeq2(ifeq(ifeq(product(y, z, y_times_z), true, sum(y_times_z, y, y), true), true, product(inverse(y), y, multiply(y_times_z, inverse(y))), true), true, additive_identity, multiply(y_times_z, inverse(y)))
% 129.04/16.50 = { by axiom 4 (y_times_z) }
% 129.04/16.50 ifeq2(ifeq(ifeq(true, true, sum(y_times_z, y, y), true), true, product(inverse(y), y, multiply(y_times_z, inverse(y))), true), true, additive_identity, multiply(y_times_z, inverse(y)))
% 129.04/16.50 = { by axiom 13 (ifeq_axiom) }
% 129.04/16.50 ifeq2(ifeq(sum(y_times_z, y, y), true, product(inverse(y), y, multiply(y_times_z, inverse(y))), true), true, additive_identity, multiply(y_times_z, inverse(y)))
% 129.04/16.50 = { by lemma 26 R->L }
% 129.04/16.50 ifeq2(ifeq(sum(y_times_z, y, y), true, product(inverse(y), y, multiply(inverse(y), y_times_z)), true), true, additive_identity, multiply(y_times_z, inverse(y)))
% 129.86/16.50 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.50 ifeq2(ifeq(true, true, ifeq(sum(y_times_z, y, y), true, product(inverse(y), y, multiply(inverse(y), y_times_z)), true), true), true, additive_identity, multiply(y_times_z, inverse(y)))
% 129.86/16.50 = { by axiom 15 (closure_of_multiplication) R->L }
% 129.86/16.50 ifeq2(ifeq(product(inverse(y), y_times_z, multiply(inverse(y), y_times_z)), true, ifeq(sum(y_times_z, y, y), true, product(inverse(y), y, multiply(inverse(y), y_times_z)), true), true), true, additive_identity, multiply(y_times_z, inverse(y)))
% 129.86/16.50 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.50 ifeq2(ifeq(true, true, ifeq(product(inverse(y), y_times_z, multiply(inverse(y), y_times_z)), true, ifeq(sum(y_times_z, y, y), true, product(inverse(y), y, multiply(inverse(y), y_times_z)), true), true), true), true, additive_identity, multiply(y_times_z, inverse(y)))
% 129.86/16.50 = { by axiom 8 (multiplicative_inverse1) R->L }
% 129.86/16.50 ifeq2(ifeq(product(inverse(y), y, additive_identity), true, ifeq(product(inverse(y), y_times_z, multiply(inverse(y), y_times_z)), true, ifeq(sum(y_times_z, y, y), true, product(inverse(y), y, multiply(inverse(y), y_times_z)), true), true), true), true, additive_identity, multiply(y_times_z, inverse(y)))
% 129.86/16.50 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.50 ifeq2(ifeq(product(inverse(y), y, additive_identity), true, ifeq(product(inverse(y), y_times_z, multiply(inverse(y), y_times_z)), true, ifeq(true, true, ifeq(sum(y_times_z, y, y), true, product(inverse(y), y, multiply(inverse(y), y_times_z)), true), true), true), true), true, additive_identity, multiply(y_times_z, inverse(y)))
% 129.86/16.50 = { by axiom 9 (additive_identity2) R->L }
% 129.86/16.50 ifeq2(ifeq(product(inverse(y), y, additive_identity), true, ifeq(product(inverse(y), y_times_z, multiply(inverse(y), y_times_z)), true, ifeq(sum(multiply(inverse(y), y_times_z), additive_identity, multiply(inverse(y), y_times_z)), true, ifeq(sum(y_times_z, y, y), true, product(inverse(y), y, multiply(inverse(y), y_times_z)), true), true), true), true), true, additive_identity, multiply(y_times_z, inverse(y)))
% 129.86/16.50 = { by axiom 22 (distributivity2) }
% 129.86/16.50 ifeq2(true, true, additive_identity, multiply(y_times_z, inverse(y)))
% 129.86/16.50 = { by axiom 14 (ifeq_axiom) }
% 129.86/16.50 additive_identity
% 129.86/16.50
% 129.86/16.50 Lemma 29: multiply(x_times_y, inverse(y)) = additive_identity.
% 129.86/16.50 Proof:
% 129.86/16.50 multiply(x_times_y, inverse(y))
% 129.86/16.50 = { by lemma 27 R->L }
% 129.86/16.50 ifeq2(product(inverse(y), y, multiply(x_times_y, inverse(y))), true, additive_identity, multiply(x_times_y, inverse(y)))
% 129.86/16.50 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.50 ifeq2(ifeq(true, true, product(inverse(y), y, multiply(x_times_y, inverse(y))), true), true, additive_identity, multiply(x_times_y, inverse(y)))
% 129.86/16.50 = { by axiom 21 (distributivity1) R->L }
% 129.86/16.50 ifeq2(ifeq(ifeq(product(y, multiplicative_identity, y), true, ifeq(product(y, multiplicative_identity, y), true, ifeq(product(y, x, x_times_y), true, ifeq(sum(x, multiplicative_identity, multiplicative_identity), true, sum(x_times_y, y, y), true), true), true), true), true, product(inverse(y), y, multiply(x_times_y, inverse(y))), true), true, additive_identity, multiply(x_times_y, inverse(y)))
% 129.86/16.50 = { by axiom 1 (multiplicative_identity2) }
% 129.86/16.50 ifeq2(ifeq(ifeq(true, true, ifeq(product(y, multiplicative_identity, y), true, ifeq(product(y, x, x_times_y), true, ifeq(sum(x, multiplicative_identity, multiplicative_identity), true, sum(x_times_y, y, y), true), true), true), true), true, product(inverse(y), y, multiply(x_times_y, inverse(y))), true), true, additive_identity, multiply(x_times_y, inverse(y)))
% 129.86/16.50 = { by axiom 13 (ifeq_axiom) }
% 129.86/16.50 ifeq2(ifeq(ifeq(product(y, multiplicative_identity, y), true, ifeq(product(y, x, x_times_y), true, ifeq(sum(x, multiplicative_identity, multiplicative_identity), true, sum(x_times_y, y, y), true), true), true), true, product(inverse(y), y, multiply(x_times_y, inverse(y))), true), true, additive_identity, multiply(x_times_y, inverse(y)))
% 129.86/16.50 = { by axiom 1 (multiplicative_identity2) }
% 129.86/16.50 ifeq2(ifeq(ifeq(true, true, ifeq(product(y, x, x_times_y), true, ifeq(sum(x, multiplicative_identity, multiplicative_identity), true, sum(x_times_y, y, y), true), true), true), true, product(inverse(y), y, multiply(x_times_y, inverse(y))), true), true, additive_identity, multiply(x_times_y, inverse(y)))
% 129.86/16.50 = { by axiom 13 (ifeq_axiom) }
% 129.86/16.50 ifeq2(ifeq(ifeq(product(y, x, x_times_y), true, ifeq(sum(x, multiplicative_identity, multiplicative_identity), true, sum(x_times_y, y, y), true), true), true, product(inverse(y), y, multiply(x_times_y, inverse(y))), true), true, additive_identity, multiply(x_times_y, inverse(y)))
% 129.86/16.50 = { by lemma 25 R->L }
% 129.86/16.50 ifeq2(ifeq(ifeq(product(y, x, x_times_y), true, ifeq(sum(x, multiplicative_identity, add(x, multiplicative_identity)), true, sum(x_times_y, y, y), true), true), true, product(inverse(y), y, multiply(x_times_y, inverse(y))), true), true, additive_identity, multiply(x_times_y, inverse(y)))
% 129.86/16.50 = { by axiom 16 (closure_of_addition) }
% 129.86/16.50 ifeq2(ifeq(ifeq(product(y, x, x_times_y), true, ifeq(true, true, sum(x_times_y, y, y), true), true), true, product(inverse(y), y, multiply(x_times_y, inverse(y))), true), true, additive_identity, multiply(x_times_y, inverse(y)))
% 129.86/16.50 = { by axiom 13 (ifeq_axiom) }
% 129.86/16.50 ifeq2(ifeq(ifeq(product(y, x, x_times_y), true, sum(x_times_y, y, y), true), true, product(inverse(y), y, multiply(x_times_y, inverse(y))), true), true, additive_identity, multiply(x_times_y, inverse(y)))
% 129.86/16.50 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.50 ifeq2(ifeq(ifeq(ifeq(true, true, product(y, x, x_times_y), true), true, sum(x_times_y, y, y), true), true, product(inverse(y), y, multiply(x_times_y, inverse(y))), true), true, additive_identity, multiply(x_times_y, inverse(y)))
% 129.86/16.50 = { by axiom 6 (x_times_y) R->L }
% 129.86/16.50 ifeq2(ifeq(ifeq(ifeq(product(x, y, x_times_y), true, product(y, x, x_times_y), true), true, sum(x_times_y, y, y), true), true, product(inverse(y), y, multiply(x_times_y, inverse(y))), true), true, additive_identity, multiply(x_times_y, inverse(y)))
% 129.86/16.50 = { by axiom 17 (commutativity_of_multiplication) }
% 129.86/16.50 ifeq2(ifeq(ifeq(true, true, sum(x_times_y, y, y), true), true, product(inverse(y), y, multiply(x_times_y, inverse(y))), true), true, additive_identity, multiply(x_times_y, inverse(y)))
% 129.86/16.50 = { by axiom 13 (ifeq_axiom) }
% 129.86/16.50 ifeq2(ifeq(sum(x_times_y, y, y), true, product(inverse(y), y, multiply(x_times_y, inverse(y))), true), true, additive_identity, multiply(x_times_y, inverse(y)))
% 129.86/16.50 = { by lemma 26 R->L }
% 129.86/16.50 ifeq2(ifeq(sum(x_times_y, y, y), true, product(inverse(y), y, multiply(inverse(y), x_times_y)), true), true, additive_identity, multiply(x_times_y, inverse(y)))
% 129.86/16.50 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.50 ifeq2(ifeq(true, true, ifeq(sum(x_times_y, y, y), true, product(inverse(y), y, multiply(inverse(y), x_times_y)), true), true), true, additive_identity, multiply(x_times_y, inverse(y)))
% 129.86/16.50 = { by axiom 15 (closure_of_multiplication) R->L }
% 129.86/16.50 ifeq2(ifeq(product(inverse(y), x_times_y, multiply(inverse(y), x_times_y)), true, ifeq(sum(x_times_y, y, y), true, product(inverse(y), y, multiply(inverse(y), x_times_y)), true), true), true, additive_identity, multiply(x_times_y, inverse(y)))
% 129.86/16.50 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.50 ifeq2(ifeq(true, true, ifeq(product(inverse(y), x_times_y, multiply(inverse(y), x_times_y)), true, ifeq(sum(x_times_y, y, y), true, product(inverse(y), y, multiply(inverse(y), x_times_y)), true), true), true), true, additive_identity, multiply(x_times_y, inverse(y)))
% 129.86/16.50 = { by axiom 8 (multiplicative_inverse1) R->L }
% 129.86/16.50 ifeq2(ifeq(product(inverse(y), y, additive_identity), true, ifeq(product(inverse(y), x_times_y, multiply(inverse(y), x_times_y)), true, ifeq(sum(x_times_y, y, y), true, product(inverse(y), y, multiply(inverse(y), x_times_y)), true), true), true), true, additive_identity, multiply(x_times_y, inverse(y)))
% 129.86/16.50 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.50 ifeq2(ifeq(product(inverse(y), y, additive_identity), true, ifeq(product(inverse(y), x_times_y, multiply(inverse(y), x_times_y)), true, ifeq(true, true, ifeq(sum(x_times_y, y, y), true, product(inverse(y), y, multiply(inverse(y), x_times_y)), true), true), true), true), true, additive_identity, multiply(x_times_y, inverse(y)))
% 129.86/16.50 = { by axiom 9 (additive_identity2) R->L }
% 129.86/16.50 ifeq2(ifeq(product(inverse(y), y, additive_identity), true, ifeq(product(inverse(y), x_times_y, multiply(inverse(y), x_times_y)), true, ifeq(sum(multiply(inverse(y), x_times_y), additive_identity, multiply(inverse(y), x_times_y)), true, ifeq(sum(x_times_y, y, y), true, product(inverse(y), y, multiply(inverse(y), x_times_y)), true), true), true), true), true, additive_identity, multiply(x_times_y, inverse(y)))
% 129.86/16.50 = { by axiom 22 (distributivity2) }
% 129.86/16.50 ifeq2(true, true, additive_identity, multiply(x_times_y, inverse(y)))
% 129.86/16.50 = { by axiom 14 (ifeq_axiom) }
% 129.86/16.50 additive_identity
% 129.86/16.50
% 129.86/16.50 Lemma 30: multiply(X, add(Y, X)) = X.
% 129.86/16.50 Proof:
% 129.86/16.50 multiply(X, add(Y, X))
% 129.86/16.50 = { by lemma 24 R->L }
% 129.86/16.50 multiply(X, add(X, Y))
% 129.86/16.50 = { by axiom 14 (ifeq_axiom) R->L }
% 129.86/16.50 ifeq2(true, true, multiply(X, add(X, Y)), X)
% 129.86/16.50 = { by axiom 23 (distributivity8) R->L }
% 129.86/16.50 ifeq2(ifeq(product(X, add(Y, X), multiply(X, add(Y, X))), true, ifeq(product(additive_identity, Y, multiply(additive_identity, Y)), true, ifeq(sum(Y, X, add(Y, X)), true, ifeq(sum(additive_identity, X, X), true, sum(multiply(additive_identity, Y), X, multiply(X, add(Y, X))), true), true), true), true), true, multiply(X, add(X, Y)), X)
% 129.86/16.50 = { by axiom 11 (additive_identity1) }
% 129.86/16.50 ifeq2(ifeq(product(X, add(Y, X), multiply(X, add(Y, X))), true, ifeq(product(additive_identity, Y, multiply(additive_identity, Y)), true, ifeq(sum(Y, X, add(Y, X)), true, ifeq(true, true, sum(multiply(additive_identity, Y), X, multiply(X, add(Y, X))), true), true), true), true), true, multiply(X, add(X, Y)), X)
% 129.86/16.50 = { by axiom 13 (ifeq_axiom) }
% 129.86/16.50 ifeq2(ifeq(product(X, add(Y, X), multiply(X, add(Y, X))), true, ifeq(product(additive_identity, Y, multiply(additive_identity, Y)), true, ifeq(sum(Y, X, add(Y, X)), true, sum(multiply(additive_identity, Y), X, multiply(X, add(Y, X))), true), true), true), true, multiply(X, add(X, Y)), X)
% 129.86/16.51 = { by axiom 15 (closure_of_multiplication) }
% 129.86/16.51 ifeq2(ifeq(product(X, add(Y, X), multiply(X, add(Y, X))), true, ifeq(true, true, ifeq(sum(Y, X, add(Y, X)), true, sum(multiply(additive_identity, Y), X, multiply(X, add(Y, X))), true), true), true), true, multiply(X, add(X, Y)), X)
% 129.86/16.51 = { by axiom 13 (ifeq_axiom) }
% 129.86/16.51 ifeq2(ifeq(product(X, add(Y, X), multiply(X, add(Y, X))), true, ifeq(sum(Y, X, add(Y, X)), true, sum(multiply(additive_identity, Y), X, multiply(X, add(Y, X))), true), true), true, multiply(X, add(X, Y)), X)
% 129.86/16.51 = { by lemma 26 R->L }
% 129.86/16.51 ifeq2(ifeq(product(X, add(Y, X), multiply(X, add(Y, X))), true, ifeq(sum(Y, X, add(Y, X)), true, sum(multiply(Y, additive_identity), X, multiply(X, add(Y, X))), true), true), true, multiply(X, add(X, Y)), X)
% 129.86/16.51 = { by axiom 19 (multiplication_is_well_defined) R->L }
% 129.86/16.51 ifeq2(ifeq(product(X, add(Y, X), multiply(X, add(Y, X))), true, ifeq(sum(Y, X, add(Y, X)), true, sum(ifeq2(product(Y, inverse(Y), multiply(Y, additive_identity)), true, ifeq2(product(Y, inverse(Y), additive_identity), true, additive_identity, multiply(Y, additive_identity)), multiply(Y, additive_identity)), X, multiply(X, add(Y, X))), true), true), true, multiply(X, add(X, Y)), X)
% 129.86/16.51 = { by axiom 2 (multiplicative_inverse2) }
% 129.86/16.51 ifeq2(ifeq(product(X, add(Y, X), multiply(X, add(Y, X))), true, ifeq(sum(Y, X, add(Y, X)), true, sum(ifeq2(product(Y, inverse(Y), multiply(Y, additive_identity)), true, ifeq2(true, true, additive_identity, multiply(Y, additive_identity)), multiply(Y, additive_identity)), X, multiply(X, add(Y, X))), true), true), true, multiply(X, add(X, Y)), X)
% 129.86/16.51 = { by axiom 14 (ifeq_axiom) }
% 129.86/16.51 ifeq2(ifeq(product(X, add(Y, X), multiply(X, add(Y, X))), true, ifeq(sum(Y, X, add(Y, X)), true, sum(ifeq2(product(Y, inverse(Y), multiply(Y, additive_identity)), true, additive_identity, multiply(Y, additive_identity)), X, multiply(X, add(Y, X))), true), true), true, multiply(X, add(X, Y)), X)
% 129.86/16.51 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.51 ifeq2(ifeq(product(X, add(Y, X), multiply(X, add(Y, X))), true, ifeq(sum(Y, X, add(Y, X)), true, sum(ifeq2(ifeq(true, true, product(Y, inverse(Y), multiply(Y, additive_identity)), true), true, additive_identity, multiply(Y, additive_identity)), X, multiply(X, add(Y, X))), true), true), true, multiply(X, add(X, Y)), X)
% 129.86/16.51 = { by axiom 15 (closure_of_multiplication) R->L }
% 129.86/16.51 ifeq2(ifeq(product(X, add(Y, X), multiply(X, add(Y, X))), true, ifeq(sum(Y, X, add(Y, X)), true, sum(ifeq2(ifeq(product(Y, additive_identity, multiply(Y, additive_identity)), true, product(Y, inverse(Y), multiply(Y, additive_identity)), true), true, additive_identity, multiply(Y, additive_identity)), X, multiply(X, add(Y, X))), true), true), true, multiply(X, add(X, Y)), X)
% 129.86/16.51 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.51 ifeq2(ifeq(product(X, add(Y, X), multiply(X, add(Y, X))), true, ifeq(sum(Y, X, add(Y, X)), true, sum(ifeq2(ifeq(true, true, ifeq(product(Y, additive_identity, multiply(Y, additive_identity)), true, product(Y, inverse(Y), multiply(Y, additive_identity)), true), true), true, additive_identity, multiply(Y, additive_identity)), X, multiply(X, add(Y, X))), true), true), true, multiply(X, add(X, Y)), X)
% 129.86/16.51 = { by axiom 2 (multiplicative_inverse2) R->L }
% 129.86/16.51 ifeq2(ifeq(product(X, add(Y, X), multiply(X, add(Y, X))), true, ifeq(sum(Y, X, add(Y, X)), true, sum(ifeq2(ifeq(product(Y, inverse(Y), additive_identity), true, ifeq(product(Y, additive_identity, multiply(Y, additive_identity)), true, product(Y, inverse(Y), multiply(Y, additive_identity)), true), true), true, additive_identity, multiply(Y, additive_identity)), X, multiply(X, add(Y, X))), true), true), true, multiply(X, add(X, Y)), X)
% 129.86/16.51 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.51 ifeq2(ifeq(product(X, add(Y, X), multiply(X, add(Y, X))), true, ifeq(sum(Y, X, add(Y, X)), true, sum(ifeq2(ifeq(product(Y, inverse(Y), additive_identity), true, ifeq(product(Y, additive_identity, multiply(Y, additive_identity)), true, ifeq(true, true, product(Y, inverse(Y), multiply(Y, additive_identity)), true), true), true), true, additive_identity, multiply(Y, additive_identity)), X, multiply(X, add(Y, X))), true), true), true, multiply(X, add(X, Y)), X)
% 129.86/16.51 = { by axiom 11 (additive_identity1) R->L }
% 129.86/16.51 ifeq2(ifeq(product(X, add(Y, X), multiply(X, add(Y, X))), true, ifeq(sum(Y, X, add(Y, X)), true, sum(ifeq2(ifeq(product(Y, inverse(Y), additive_identity), true, ifeq(product(Y, additive_identity, multiply(Y, additive_identity)), true, ifeq(sum(additive_identity, inverse(Y), inverse(Y)), true, product(Y, inverse(Y), multiply(Y, additive_identity)), true), true), true), true, additive_identity, multiply(Y, additive_identity)), X, multiply(X, add(Y, X))), true), true), true, multiply(X, add(X, Y)), X)
% 129.86/16.51 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.51 ifeq2(ifeq(product(X, add(Y, X), multiply(X, add(Y, X))), true, ifeq(sum(Y, X, add(Y, X)), true, sum(ifeq2(ifeq(product(Y, inverse(Y), additive_identity), true, ifeq(product(Y, additive_identity, multiply(Y, additive_identity)), true, ifeq(true, true, ifeq(sum(additive_identity, inverse(Y), inverse(Y)), true, product(Y, inverse(Y), multiply(Y, additive_identity)), true), true), true), true), true, additive_identity, multiply(Y, additive_identity)), X, multiply(X, add(Y, X))), true), true), true, multiply(X, add(X, Y)), X)
% 129.86/16.51 = { by axiom 9 (additive_identity2) R->L }
% 129.86/16.51 ifeq2(ifeq(product(X, add(Y, X), multiply(X, add(Y, X))), true, ifeq(sum(Y, X, add(Y, X)), true, sum(ifeq2(ifeq(product(Y, inverse(Y), additive_identity), true, ifeq(product(Y, additive_identity, multiply(Y, additive_identity)), true, ifeq(sum(multiply(Y, additive_identity), additive_identity, multiply(Y, additive_identity)), true, ifeq(sum(additive_identity, inverse(Y), inverse(Y)), true, product(Y, inverse(Y), multiply(Y, additive_identity)), true), true), true), true), true, additive_identity, multiply(Y, additive_identity)), X, multiply(X, add(Y, X))), true), true), true, multiply(X, add(X, Y)), X)
% 129.86/16.51 = { by axiom 22 (distributivity2) }
% 129.86/16.51 ifeq2(ifeq(product(X, add(Y, X), multiply(X, add(Y, X))), true, ifeq(sum(Y, X, add(Y, X)), true, sum(ifeq2(true, true, additive_identity, multiply(Y, additive_identity)), X, multiply(X, add(Y, X))), true), true), true, multiply(X, add(X, Y)), X)
% 129.86/16.51 = { by axiom 14 (ifeq_axiom) }
% 129.86/16.51 ifeq2(ifeq(product(X, add(Y, X), multiply(X, add(Y, X))), true, ifeq(sum(Y, X, add(Y, X)), true, sum(additive_identity, X, multiply(X, add(Y, X))), true), true), true, multiply(X, add(X, Y)), X)
% 129.86/16.51 = { by axiom 15 (closure_of_multiplication) }
% 129.86/16.51 ifeq2(ifeq(true, true, ifeq(sum(Y, X, add(Y, X)), true, sum(additive_identity, X, multiply(X, add(Y, X))), true), true), true, multiply(X, add(X, Y)), X)
% 129.86/16.51 = { by axiom 13 (ifeq_axiom) }
% 129.86/16.51 ifeq2(ifeq(sum(Y, X, add(Y, X)), true, sum(additive_identity, X, multiply(X, add(Y, X))), true), true, multiply(X, add(X, Y)), X)
% 129.86/16.51 = { by axiom 16 (closure_of_addition) }
% 129.86/16.51 ifeq2(ifeq(true, true, sum(additive_identity, X, multiply(X, add(Y, X))), true), true, multiply(X, add(X, Y)), X)
% 129.86/16.51 = { by axiom 13 (ifeq_axiom) }
% 129.86/16.51 ifeq2(sum(additive_identity, X, multiply(X, add(Y, X))), true, multiply(X, add(X, Y)), X)
% 129.86/16.51 = { by lemma 24 }
% 129.86/16.51 ifeq2(sum(additive_identity, X, multiply(X, add(X, Y))), true, multiply(X, add(X, Y)), X)
% 129.86/16.51 = { by axiom 14 (ifeq_axiom) R->L }
% 129.86/16.51 ifeq2(true, true, ifeq2(sum(additive_identity, X, multiply(X, add(X, Y))), true, multiply(X, add(X, Y)), X), X)
% 129.86/16.51 = { by axiom 11 (additive_identity1) R->L }
% 129.86/16.51 ifeq2(sum(additive_identity, X, X), true, ifeq2(sum(additive_identity, X, multiply(X, add(X, Y))), true, multiply(X, add(X, Y)), X), X)
% 129.86/16.51 = { by axiom 20 (addition_is_well_defined) }
% 129.86/16.51 X
% 129.86/16.51
% 129.86/16.51 Lemma 31: ifeq2(sum(X, Y, Z), true, Z, add(X, Y)) = add(X, Y).
% 129.86/16.51 Proof:
% 129.86/16.51 ifeq2(sum(X, Y, Z), true, Z, add(X, Y))
% 129.86/16.51 = { by axiom 14 (ifeq_axiom) R->L }
% 129.86/16.51 ifeq2(true, true, ifeq2(sum(X, Y, Z), true, Z, add(X, Y)), add(X, Y))
% 129.86/16.51 = { by axiom 16 (closure_of_addition) R->L }
% 129.86/16.51 ifeq2(sum(X, Y, add(X, Y)), true, ifeq2(sum(X, Y, Z), true, Z, add(X, Y)), add(X, Y))
% 129.86/16.51 = { by axiom 20 (addition_is_well_defined) }
% 129.86/16.51 add(X, Y)
% 129.86/16.51
% 129.86/16.51 Lemma 32: ifeq2(product(X, Y, Z), true, Z, multiply(X, Y)) = multiply(X, Y).
% 129.86/16.51 Proof:
% 129.86/16.51 ifeq2(product(X, Y, Z), true, Z, multiply(X, Y))
% 129.86/16.51 = { by axiom 14 (ifeq_axiom) R->L }
% 129.86/16.51 ifeq2(true, true, ifeq2(product(X, Y, Z), true, Z, multiply(X, Y)), multiply(X, Y))
% 129.86/16.51 = { by axiom 15 (closure_of_multiplication) R->L }
% 129.86/16.51 ifeq2(product(X, Y, multiply(X, Y)), true, ifeq2(product(X, Y, Z), true, Z, multiply(X, Y)), multiply(X, Y))
% 129.86/16.51 = { by axiom 19 (multiplication_is_well_defined) }
% 129.86/16.51 multiply(X, Y)
% 129.86/16.51
% 129.86/16.51 Goal 1 (prove_equality): x_times__y_times_z = x_times_y__times_z.
% 129.86/16.51 Proof:
% 129.86/16.51 x_times__y_times_z
% 129.86/16.51 = { by axiom 14 (ifeq_axiom) R->L }
% 129.86/16.51 ifeq2(true, true, x_times__y_times_z, multiply(y_times_z, add(x, inverse(y))))
% 129.86/16.51 = { by axiom 22 (distributivity2) R->L }
% 129.86/16.51 ifeq2(ifeq(product(y_times_z, inverse(y), additive_identity), true, ifeq(product(y_times_z, x, x_times__y_times_z), true, ifeq(sum(x_times__y_times_z, additive_identity, x_times__y_times_z), true, ifeq(sum(x, inverse(y), add(x, inverse(y))), true, product(y_times_z, add(x, inverse(y)), x_times__y_times_z), true), true), true), true), true, x_times__y_times_z, multiply(y_times_z, add(x, inverse(y))))
% 129.86/16.51 = { by axiom 9 (additive_identity2) }
% 129.86/16.51 ifeq2(ifeq(product(y_times_z, inverse(y), additive_identity), true, ifeq(product(y_times_z, x, x_times__y_times_z), true, ifeq(true, true, ifeq(sum(x, inverse(y), add(x, inverse(y))), true, product(y_times_z, add(x, inverse(y)), x_times__y_times_z), true), true), true), true), true, x_times__y_times_z, multiply(y_times_z, add(x, inverse(y))))
% 129.86/16.51 = { by axiom 13 (ifeq_axiom) }
% 129.86/16.51 ifeq2(ifeq(product(y_times_z, inverse(y), additive_identity), true, ifeq(product(y_times_z, x, x_times__y_times_z), true, ifeq(sum(x, inverse(y), add(x, inverse(y))), true, product(y_times_z, add(x, inverse(y)), x_times__y_times_z), true), true), true), true, x_times__y_times_z, multiply(y_times_z, add(x, inverse(y))))
% 129.86/16.51 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.51 ifeq2(ifeq(product(y_times_z, inverse(y), additive_identity), true, ifeq(ifeq(true, true, product(y_times_z, x, x_times__y_times_z), true), true, ifeq(sum(x, inverse(y), add(x, inverse(y))), true, product(y_times_z, add(x, inverse(y)), x_times__y_times_z), true), true), true), true, x_times__y_times_z, multiply(y_times_z, add(x, inverse(y))))
% 129.86/16.51 = { by axiom 5 (x_times__y_times_z) R->L }
% 129.86/16.51 ifeq2(ifeq(product(y_times_z, inverse(y), additive_identity), true, ifeq(ifeq(product(x, y_times_z, x_times__y_times_z), true, product(y_times_z, x, x_times__y_times_z), true), true, ifeq(sum(x, inverse(y), add(x, inverse(y))), true, product(y_times_z, add(x, inverse(y)), x_times__y_times_z), true), true), true), true, x_times__y_times_z, multiply(y_times_z, add(x, inverse(y))))
% 129.86/16.51 = { by axiom 17 (commutativity_of_multiplication) }
% 129.86/16.51 ifeq2(ifeq(product(y_times_z, inverse(y), additive_identity), true, ifeq(true, true, ifeq(sum(x, inverse(y), add(x, inverse(y))), true, product(y_times_z, add(x, inverse(y)), x_times__y_times_z), true), true), true), true, x_times__y_times_z, multiply(y_times_z, add(x, inverse(y))))
% 129.86/16.51 = { by axiom 13 (ifeq_axiom) }
% 129.86/16.51 ifeq2(ifeq(product(y_times_z, inverse(y), additive_identity), true, ifeq(sum(x, inverse(y), add(x, inverse(y))), true, product(y_times_z, add(x, inverse(y)), x_times__y_times_z), true), true), true, x_times__y_times_z, multiply(y_times_z, add(x, inverse(y))))
% 129.86/16.51 = { by axiom 16 (closure_of_addition) }
% 129.86/16.52 ifeq2(ifeq(product(y_times_z, inverse(y), additive_identity), true, ifeq(true, true, product(y_times_z, add(x, inverse(y)), x_times__y_times_z), true), true), true, x_times__y_times_z, multiply(y_times_z, add(x, inverse(y))))
% 129.86/16.52 = { by axiom 13 (ifeq_axiom) }
% 129.86/16.52 ifeq2(ifeq(product(y_times_z, inverse(y), additive_identity), true, product(y_times_z, add(x, inverse(y)), x_times__y_times_z), true), true, x_times__y_times_z, multiply(y_times_z, add(x, inverse(y))))
% 129.86/16.52 = { by lemma 24 }
% 129.86/16.52 ifeq2(ifeq(product(y_times_z, inverse(y), additive_identity), true, product(y_times_z, add(inverse(y), x), x_times__y_times_z), true), true, x_times__y_times_z, multiply(y_times_z, add(x, inverse(y))))
% 129.86/16.52 = { by lemma 28 R->L }
% 129.86/16.52 ifeq2(ifeq(product(y_times_z, inverse(y), multiply(y_times_z, inverse(y))), true, product(y_times_z, add(inverse(y), x), x_times__y_times_z), true), true, x_times__y_times_z, multiply(y_times_z, add(x, inverse(y))))
% 129.86/16.52 = { by axiom 15 (closure_of_multiplication) }
% 129.86/16.52 ifeq2(ifeq(true, true, product(y_times_z, add(inverse(y), x), x_times__y_times_z), true), true, x_times__y_times_z, multiply(y_times_z, add(x, inverse(y))))
% 129.86/16.52 = { by axiom 13 (ifeq_axiom) }
% 129.86/16.52 ifeq2(product(y_times_z, add(inverse(y), x), x_times__y_times_z), true, x_times__y_times_z, multiply(y_times_z, add(x, inverse(y))))
% 129.86/16.52 = { by lemma 24 }
% 129.86/16.52 ifeq2(product(y_times_z, add(x, inverse(y)), x_times__y_times_z), true, x_times__y_times_z, multiply(y_times_z, add(x, inverse(y))))
% 129.86/16.52 = { by lemma 32 }
% 129.86/16.52 multiply(y_times_z, add(x, inverse(y)))
% 129.86/16.52 = { by axiom 14 (ifeq_axiom) R->L }
% 129.86/16.52 multiply(y_times_z, ifeq2(true, true, add(x, inverse(y)), add(x_times_y, inverse(y))))
% 129.86/16.52 = { by axiom 21 (distributivity1) R->L }
% 129.86/16.52 multiply(y_times_z, ifeq2(ifeq(product(add(x, inverse(y)), multiplicative_identity, add(x, inverse(y))), true, ifeq(product(add(x, inverse(y)), inverse(y), multiply(add(x, inverse(y)), inverse(y))), true, ifeq(product(add(x, inverse(y)), y, x_times_y), true, ifeq(sum(y, inverse(y), multiplicative_identity), true, sum(x_times_y, multiply(add(x, inverse(y)), inverse(y)), add(x, inverse(y))), true), true), true), true), true, add(x, inverse(y)), add(x_times_y, inverse(y))))
% 129.86/16.52 = { by axiom 1 (multiplicative_identity2) }
% 129.86/16.52 multiply(y_times_z, ifeq2(ifeq(true, true, ifeq(product(add(x, inverse(y)), inverse(y), multiply(add(x, inverse(y)), inverse(y))), true, ifeq(product(add(x, inverse(y)), y, x_times_y), true, ifeq(sum(y, inverse(y), multiplicative_identity), true, sum(x_times_y, multiply(add(x, inverse(y)), inverse(y)), add(x, inverse(y))), true), true), true), true), true, add(x, inverse(y)), add(x_times_y, inverse(y))))
% 129.86/16.52 = { by axiom 13 (ifeq_axiom) }
% 129.86/16.52 multiply(y_times_z, ifeq2(ifeq(product(add(x, inverse(y)), inverse(y), multiply(add(x, inverse(y)), inverse(y))), true, ifeq(product(add(x, inverse(y)), y, x_times_y), true, ifeq(sum(y, inverse(y), multiplicative_identity), true, sum(x_times_y, multiply(add(x, inverse(y)), inverse(y)), add(x, inverse(y))), true), true), true), true, add(x, inverse(y)), add(x_times_y, inverse(y))))
% 129.86/16.52 = { by axiom 10 (additive_inverse2) }
% 129.86/16.52 multiply(y_times_z, ifeq2(ifeq(product(add(x, inverse(y)), inverse(y), multiply(add(x, inverse(y)), inverse(y))), true, ifeq(product(add(x, inverse(y)), y, x_times_y), true, ifeq(true, true, sum(x_times_y, multiply(add(x, inverse(y)), inverse(y)), add(x, inverse(y))), true), true), true), true, add(x, inverse(y)), add(x_times_y, inverse(y))))
% 129.86/16.52 = { by axiom 13 (ifeq_axiom) }
% 129.86/16.52 multiply(y_times_z, ifeq2(ifeq(product(add(x, inverse(y)), inverse(y), multiply(add(x, inverse(y)), inverse(y))), true, ifeq(product(add(x, inverse(y)), y, x_times_y), true, sum(x_times_y, multiply(add(x, inverse(y)), inverse(y)), add(x, inverse(y))), true), true), true, add(x, inverse(y)), add(x_times_y, inverse(y))))
% 129.86/16.52 = { by axiom 15 (closure_of_multiplication) }
% 129.86/16.52 multiply(y_times_z, ifeq2(ifeq(true, true, ifeq(product(add(x, inverse(y)), y, x_times_y), true, sum(x_times_y, multiply(add(x, inverse(y)), inverse(y)), add(x, inverse(y))), true), true), true, add(x, inverse(y)), add(x_times_y, inverse(y))))
% 129.86/16.52 = { by axiom 13 (ifeq_axiom) }
% 129.86/16.52 multiply(y_times_z, ifeq2(ifeq(product(add(x, inverse(y)), y, x_times_y), true, sum(x_times_y, multiply(add(x, inverse(y)), inverse(y)), add(x, inverse(y))), true), true, add(x, inverse(y)), add(x_times_y, inverse(y))))
% 129.86/16.52 = { by lemma 26 }
% 129.86/16.52 multiply(y_times_z, ifeq2(ifeq(product(add(x, inverse(y)), y, x_times_y), true, sum(x_times_y, multiply(inverse(y), add(x, inverse(y))), add(x, inverse(y))), true), true, add(x, inverse(y)), add(x_times_y, inverse(y))))
% 129.86/16.52 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.52 multiply(y_times_z, ifeq2(ifeq(ifeq(true, true, product(add(x, inverse(y)), y, x_times_y), true), true, sum(x_times_y, multiply(inverse(y), add(x, inverse(y))), add(x, inverse(y))), true), true, add(x, inverse(y)), add(x_times_y, inverse(y))))
% 129.86/16.52 = { by axiom 22 (distributivity2) R->L }
% 129.86/16.52 multiply(y_times_z, ifeq2(ifeq(ifeq(ifeq(product(y, inverse(y), additive_identity), true, ifeq(product(y, x, x_times_y), true, ifeq(sum(x_times_y, additive_identity, x_times_y), true, ifeq(sum(x, inverse(y), add(x, inverse(y))), true, product(y, add(x, inverse(y)), x_times_y), true), true), true), true), true, product(add(x, inverse(y)), y, x_times_y), true), true, sum(x_times_y, multiply(inverse(y), add(x, inverse(y))), add(x, inverse(y))), true), true, add(x, inverse(y)), add(x_times_y, inverse(y))))
% 129.86/16.52 = { by axiom 9 (additive_identity2) }
% 129.86/16.52 multiply(y_times_z, ifeq2(ifeq(ifeq(ifeq(product(y, inverse(y), additive_identity), true, ifeq(product(y, x, x_times_y), true, ifeq(true, true, ifeq(sum(x, inverse(y), add(x, inverse(y))), true, product(y, add(x, inverse(y)), x_times_y), true), true), true), true), true, product(add(x, inverse(y)), y, x_times_y), true), true, sum(x_times_y, multiply(inverse(y), add(x, inverse(y))), add(x, inverse(y))), true), true, add(x, inverse(y)), add(x_times_y, inverse(y))))
% 129.86/16.52 = { by axiom 13 (ifeq_axiom) }
% 129.86/16.52 multiply(y_times_z, ifeq2(ifeq(ifeq(ifeq(product(y, inverse(y), additive_identity), true, ifeq(product(y, x, x_times_y), true, ifeq(sum(x, inverse(y), add(x, inverse(y))), true, product(y, add(x, inverse(y)), x_times_y), true), true), true), true, product(add(x, inverse(y)), y, x_times_y), true), true, sum(x_times_y, multiply(inverse(y), add(x, inverse(y))), add(x, inverse(y))), true), true, add(x, inverse(y)), add(x_times_y, inverse(y))))
% 129.86/16.52 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.52 multiply(y_times_z, ifeq2(ifeq(ifeq(ifeq(product(y, inverse(y), additive_identity), true, ifeq(ifeq(true, true, product(y, x, x_times_y), true), true, ifeq(sum(x, inverse(y), add(x, inverse(y))), true, product(y, add(x, inverse(y)), x_times_y), true), true), true), true, product(add(x, inverse(y)), y, x_times_y), true), true, sum(x_times_y, multiply(inverse(y), add(x, inverse(y))), add(x, inverse(y))), true), true, add(x, inverse(y)), add(x_times_y, inverse(y))))
% 129.86/16.52 = { by axiom 6 (x_times_y) R->L }
% 129.86/16.52 multiply(y_times_z, ifeq2(ifeq(ifeq(ifeq(product(y, inverse(y), additive_identity), true, ifeq(ifeq(product(x, y, x_times_y), true, product(y, x, x_times_y), true), true, ifeq(sum(x, inverse(y), add(x, inverse(y))), true, product(y, add(x, inverse(y)), x_times_y), true), true), true), true, product(add(x, inverse(y)), y, x_times_y), true), true, sum(x_times_y, multiply(inverse(y), add(x, inverse(y))), add(x, inverse(y))), true), true, add(x, inverse(y)), add(x_times_y, inverse(y))))
% 129.86/16.52 = { by axiom 17 (commutativity_of_multiplication) }
% 129.86/16.52 multiply(y_times_z, ifeq2(ifeq(ifeq(ifeq(product(y, inverse(y), additive_identity), true, ifeq(true, true, ifeq(sum(x, inverse(y), add(x, inverse(y))), true, product(y, add(x, inverse(y)), x_times_y), true), true), true), true, product(add(x, inverse(y)), y, x_times_y), true), true, sum(x_times_y, multiply(inverse(y), add(x, inverse(y))), add(x, inverse(y))), true), true, add(x, inverse(y)), add(x_times_y, inverse(y))))
% 129.86/16.52 = { by axiom 13 (ifeq_axiom) }
% 129.86/16.52 multiply(y_times_z, ifeq2(ifeq(ifeq(ifeq(product(y, inverse(y), additive_identity), true, ifeq(sum(x, inverse(y), add(x, inverse(y))), true, product(y, add(x, inverse(y)), x_times_y), true), true), true, product(add(x, inverse(y)), y, x_times_y), true), true, sum(x_times_y, multiply(inverse(y), add(x, inverse(y))), add(x, inverse(y))), true), true, add(x, inverse(y)), add(x_times_y, inverse(y))))
% 129.86/16.52 = { by axiom 2 (multiplicative_inverse2) }
% 129.86/16.52 multiply(y_times_z, ifeq2(ifeq(ifeq(ifeq(true, true, ifeq(sum(x, inverse(y), add(x, inverse(y))), true, product(y, add(x, inverse(y)), x_times_y), true), true), true, product(add(x, inverse(y)), y, x_times_y), true), true, sum(x_times_y, multiply(inverse(y), add(x, inverse(y))), add(x, inverse(y))), true), true, add(x, inverse(y)), add(x_times_y, inverse(y))))
% 129.86/16.52 = { by axiom 13 (ifeq_axiom) }
% 129.86/16.52 multiply(y_times_z, ifeq2(ifeq(ifeq(ifeq(sum(x, inverse(y), add(x, inverse(y))), true, product(y, add(x, inverse(y)), x_times_y), true), true, product(add(x, inverse(y)), y, x_times_y), true), true, sum(x_times_y, multiply(inverse(y), add(x, inverse(y))), add(x, inverse(y))), true), true, add(x, inverse(y)), add(x_times_y, inverse(y))))
% 129.86/16.52 = { by axiom 16 (closure_of_addition) }
% 129.86/16.52 multiply(y_times_z, ifeq2(ifeq(ifeq(ifeq(true, true, product(y, add(x, inverse(y)), x_times_y), true), true, product(add(x, inverse(y)), y, x_times_y), true), true, sum(x_times_y, multiply(inverse(y), add(x, inverse(y))), add(x, inverse(y))), true), true, add(x, inverse(y)), add(x_times_y, inverse(y))))
% 129.86/16.52 = { by axiom 13 (ifeq_axiom) }
% 129.86/16.53 multiply(y_times_z, ifeq2(ifeq(ifeq(product(y, add(x, inverse(y)), x_times_y), true, product(add(x, inverse(y)), y, x_times_y), true), true, sum(x_times_y, multiply(inverse(y), add(x, inverse(y))), add(x, inverse(y))), true), true, add(x, inverse(y)), add(x_times_y, inverse(y))))
% 129.86/16.53 = { by axiom 17 (commutativity_of_multiplication) }
% 129.86/16.53 multiply(y_times_z, ifeq2(ifeq(true, true, sum(x_times_y, multiply(inverse(y), add(x, inverse(y))), add(x, inverse(y))), true), true, add(x, inverse(y)), add(x_times_y, inverse(y))))
% 129.86/16.53 = { by axiom 13 (ifeq_axiom) }
% 129.86/16.53 multiply(y_times_z, ifeq2(sum(x_times_y, multiply(inverse(y), add(x, inverse(y))), add(x, inverse(y))), true, add(x, inverse(y)), add(x_times_y, inverse(y))))
% 129.86/16.53 = { by lemma 30 }
% 129.86/16.53 multiply(y_times_z, ifeq2(sum(x_times_y, inverse(y), add(x, inverse(y))), true, add(x, inverse(y)), add(x_times_y, inverse(y))))
% 129.86/16.53 = { by lemma 31 }
% 129.86/16.53 multiply(y_times_z, add(x_times_y, inverse(y)))
% 129.86/16.53 = { by lemma 32 R->L }
% 129.86/16.53 ifeq2(product(y_times_z, add(x_times_y, inverse(y)), multiply(x_times_y, y_times_z)), true, multiply(x_times_y, y_times_z), multiply(y_times_z, add(x_times_y, inverse(y))))
% 129.86/16.53 = { by lemma 24 R->L }
% 129.86/16.53 ifeq2(product(y_times_z, add(inverse(y), x_times_y), multiply(x_times_y, y_times_z)), true, multiply(x_times_y, y_times_z), multiply(y_times_z, add(x_times_y, inverse(y))))
% 129.86/16.53 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.53 ifeq2(ifeq(true, true, product(y_times_z, add(inverse(y), x_times_y), multiply(x_times_y, y_times_z)), true), true, multiply(x_times_y, y_times_z), multiply(y_times_z, add(x_times_y, inverse(y))))
% 129.86/16.53 = { by axiom 15 (closure_of_multiplication) R->L }
% 129.86/16.53 ifeq2(ifeq(product(y_times_z, inverse(y), multiply(y_times_z, inverse(y))), true, product(y_times_z, add(inverse(y), x_times_y), multiply(x_times_y, y_times_z)), true), true, multiply(x_times_y, y_times_z), multiply(y_times_z, add(x_times_y, inverse(y))))
% 129.86/16.53 = { by lemma 28 }
% 129.86/16.53 ifeq2(ifeq(product(y_times_z, inverse(y), additive_identity), true, product(y_times_z, add(inverse(y), x_times_y), multiply(x_times_y, y_times_z)), true), true, multiply(x_times_y, y_times_z), multiply(y_times_z, add(x_times_y, inverse(y))))
% 129.86/16.53 = { by lemma 26 R->L }
% 129.86/16.53 ifeq2(ifeq(product(y_times_z, inverse(y), additive_identity), true, product(y_times_z, add(inverse(y), x_times_y), multiply(y_times_z, x_times_y)), true), true, multiply(x_times_y, y_times_z), multiply(y_times_z, add(x_times_y, inverse(y))))
% 129.86/16.53 = { by lemma 24 R->L }
% 129.86/16.53 ifeq2(ifeq(product(y_times_z, inverse(y), additive_identity), true, product(y_times_z, add(x_times_y, inverse(y)), multiply(y_times_z, x_times_y)), true), true, multiply(x_times_y, y_times_z), multiply(y_times_z, add(x_times_y, inverse(y))))
% 129.86/16.53 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.53 ifeq2(ifeq(product(y_times_z, inverse(y), additive_identity), true, ifeq(true, true, product(y_times_z, add(x_times_y, inverse(y)), multiply(y_times_z, x_times_y)), true), true), true, multiply(x_times_y, y_times_z), multiply(y_times_z, add(x_times_y, inverse(y))))
% 129.86/16.53 = { by axiom 16 (closure_of_addition) R->L }
% 129.86/16.53 ifeq2(ifeq(product(y_times_z, inverse(y), additive_identity), true, ifeq(sum(x_times_y, inverse(y), add(x_times_y, inverse(y))), true, product(y_times_z, add(x_times_y, inverse(y)), multiply(y_times_z, x_times_y)), true), true), true, multiply(x_times_y, y_times_z), multiply(y_times_z, add(x_times_y, inverse(y))))
% 129.86/16.53 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.53 ifeq2(ifeq(product(y_times_z, inverse(y), additive_identity), true, ifeq(true, true, ifeq(sum(x_times_y, inverse(y), add(x_times_y, inverse(y))), true, product(y_times_z, add(x_times_y, inverse(y)), multiply(y_times_z, x_times_y)), true), true), true), true, multiply(x_times_y, y_times_z), multiply(y_times_z, add(x_times_y, inverse(y))))
% 129.86/16.53 = { by axiom 15 (closure_of_multiplication) R->L }
% 129.86/16.53 ifeq2(ifeq(product(y_times_z, inverse(y), additive_identity), true, ifeq(product(y_times_z, x_times_y, multiply(y_times_z, x_times_y)), true, ifeq(sum(x_times_y, inverse(y), add(x_times_y, inverse(y))), true, product(y_times_z, add(x_times_y, inverse(y)), multiply(y_times_z, x_times_y)), true), true), true), true, multiply(x_times_y, y_times_z), multiply(y_times_z, add(x_times_y, inverse(y))))
% 129.86/16.53 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.53 ifeq2(ifeq(product(y_times_z, inverse(y), additive_identity), true, ifeq(product(y_times_z, x_times_y, multiply(y_times_z, x_times_y)), true, ifeq(true, true, ifeq(sum(x_times_y, inverse(y), add(x_times_y, inverse(y))), true, product(y_times_z, add(x_times_y, inverse(y)), multiply(y_times_z, x_times_y)), true), true), true), true), true, multiply(x_times_y, y_times_z), multiply(y_times_z, add(x_times_y, inverse(y))))
% 129.86/16.53 = { by axiom 9 (additive_identity2) R->L }
% 129.86/16.53 ifeq2(ifeq(product(y_times_z, inverse(y), additive_identity), true, ifeq(product(y_times_z, x_times_y, multiply(y_times_z, x_times_y)), true, ifeq(sum(multiply(y_times_z, x_times_y), additive_identity, multiply(y_times_z, x_times_y)), true, ifeq(sum(x_times_y, inverse(y), add(x_times_y, inverse(y))), true, product(y_times_z, add(x_times_y, inverse(y)), multiply(y_times_z, x_times_y)), true), true), true), true), true, multiply(x_times_y, y_times_z), multiply(y_times_z, add(x_times_y, inverse(y))))
% 129.86/16.53 = { by axiom 22 (distributivity2) }
% 129.86/16.53 ifeq2(true, true, multiply(x_times_y, y_times_z), multiply(y_times_z, add(x_times_y, inverse(y))))
% 129.86/16.53 = { by axiom 14 (ifeq_axiom) }
% 129.86/16.53 multiply(x_times_y, y_times_z)
% 129.86/16.53 = { by lemma 26 }
% 129.86/16.53 multiply(y_times_z, x_times_y)
% 129.86/16.53 = { by axiom 14 (ifeq_axiom) R->L }
% 129.86/16.53 ifeq2(true, true, multiply(y_times_z, x_times_y), multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by axiom 22 (distributivity2) R->L }
% 129.86/16.53 ifeq2(ifeq(product(x_times_y, inverse(y), additive_identity), true, ifeq(product(x_times_y, y_times_z, multiply(x_times_y, y_times_z)), true, ifeq(sum(multiply(x_times_y, y_times_z), additive_identity, multiply(x_times_y, y_times_z)), true, ifeq(sum(y_times_z, inverse(y), add(y_times_z, inverse(y))), true, product(x_times_y, add(y_times_z, inverse(y)), multiply(x_times_y, y_times_z)), true), true), true), true), true, multiply(y_times_z, x_times_y), multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by axiom 9 (additive_identity2) }
% 129.86/16.53 ifeq2(ifeq(product(x_times_y, inverse(y), additive_identity), true, ifeq(product(x_times_y, y_times_z, multiply(x_times_y, y_times_z)), true, ifeq(true, true, ifeq(sum(y_times_z, inverse(y), add(y_times_z, inverse(y))), true, product(x_times_y, add(y_times_z, inverse(y)), multiply(x_times_y, y_times_z)), true), true), true), true), true, multiply(y_times_z, x_times_y), multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by axiom 13 (ifeq_axiom) }
% 129.86/16.53 ifeq2(ifeq(product(x_times_y, inverse(y), additive_identity), true, ifeq(product(x_times_y, y_times_z, multiply(x_times_y, y_times_z)), true, ifeq(sum(y_times_z, inverse(y), add(y_times_z, inverse(y))), true, product(x_times_y, add(y_times_z, inverse(y)), multiply(x_times_y, y_times_z)), true), true), true), true, multiply(y_times_z, x_times_y), multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by axiom 15 (closure_of_multiplication) }
% 129.86/16.53 ifeq2(ifeq(product(x_times_y, inverse(y), additive_identity), true, ifeq(true, true, ifeq(sum(y_times_z, inverse(y), add(y_times_z, inverse(y))), true, product(x_times_y, add(y_times_z, inverse(y)), multiply(x_times_y, y_times_z)), true), true), true), true, multiply(y_times_z, x_times_y), multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by axiom 13 (ifeq_axiom) }
% 129.86/16.53 ifeq2(ifeq(product(x_times_y, inverse(y), additive_identity), true, ifeq(sum(y_times_z, inverse(y), add(y_times_z, inverse(y))), true, product(x_times_y, add(y_times_z, inverse(y)), multiply(x_times_y, y_times_z)), true), true), true, multiply(y_times_z, x_times_y), multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by axiom 16 (closure_of_addition) }
% 129.86/16.53 ifeq2(ifeq(product(x_times_y, inverse(y), additive_identity), true, ifeq(true, true, product(x_times_y, add(y_times_z, inverse(y)), multiply(x_times_y, y_times_z)), true), true), true, multiply(y_times_z, x_times_y), multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by axiom 13 (ifeq_axiom) }
% 129.86/16.53 ifeq2(ifeq(product(x_times_y, inverse(y), additive_identity), true, product(x_times_y, add(y_times_z, inverse(y)), multiply(x_times_y, y_times_z)), true), true, multiply(y_times_z, x_times_y), multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by lemma 24 }
% 129.86/16.53 ifeq2(ifeq(product(x_times_y, inverse(y), additive_identity), true, product(x_times_y, add(inverse(y), y_times_z), multiply(x_times_y, y_times_z)), true), true, multiply(y_times_z, x_times_y), multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by lemma 26 }
% 129.86/16.53 ifeq2(ifeq(product(x_times_y, inverse(y), additive_identity), true, product(x_times_y, add(inverse(y), y_times_z), multiply(y_times_z, x_times_y)), true), true, multiply(y_times_z, x_times_y), multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by lemma 29 R->L }
% 129.86/16.53 ifeq2(ifeq(product(x_times_y, inverse(y), multiply(x_times_y, inverse(y))), true, product(x_times_y, add(inverse(y), y_times_z), multiply(y_times_z, x_times_y)), true), true, multiply(y_times_z, x_times_y), multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by axiom 15 (closure_of_multiplication) }
% 129.86/16.53 ifeq2(ifeq(true, true, product(x_times_y, add(inverse(y), y_times_z), multiply(y_times_z, x_times_y)), true), true, multiply(y_times_z, x_times_y), multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by axiom 13 (ifeq_axiom) }
% 129.86/16.53 ifeq2(product(x_times_y, add(inverse(y), y_times_z), multiply(y_times_z, x_times_y)), true, multiply(y_times_z, x_times_y), multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by lemma 24 }
% 129.86/16.53 ifeq2(product(x_times_y, add(y_times_z, inverse(y)), multiply(y_times_z, x_times_y)), true, multiply(y_times_z, x_times_y), multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by lemma 32 }
% 129.86/16.53 multiply(x_times_y, add(y_times_z, inverse(y)))
% 129.86/16.53 = { by lemma 32 R->L }
% 129.86/16.53 ifeq2(product(x_times_y, add(y_times_z, inverse(y)), x_times_y__times_z), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by lemma 31 R->L }
% 129.86/16.53 ifeq2(product(x_times_y, ifeq2(sum(y_times_z, inverse(y), add(z, inverse(y))), true, add(z, inverse(y)), add(y_times_z, inverse(y))), x_times_y__times_z), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by lemma 30 R->L }
% 129.86/16.53 ifeq2(product(x_times_y, ifeq2(sum(y_times_z, multiply(inverse(y), add(z, inverse(y))), add(z, inverse(y))), true, add(z, inverse(y)), add(y_times_z, inverse(y))), x_times_y__times_z), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.53 ifeq2(product(x_times_y, ifeq2(ifeq(true, true, sum(y_times_z, multiply(inverse(y), add(z, inverse(y))), add(z, inverse(y))), true), true, add(z, inverse(y)), add(y_times_z, inverse(y))), x_times_y__times_z), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by axiom 17 (commutativity_of_multiplication) R->L }
% 129.86/16.53 ifeq2(product(x_times_y, ifeq2(ifeq(ifeq(product(y, add(z, inverse(y)), y_times_z), true, product(add(z, inverse(y)), y, y_times_z), true), true, sum(y_times_z, multiply(inverse(y), add(z, inverse(y))), add(z, inverse(y))), true), true, add(z, inverse(y)), add(y_times_z, inverse(y))), x_times_y__times_z), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.53 ifeq2(product(x_times_y, ifeq2(ifeq(ifeq(ifeq(true, true, product(y, add(z, inverse(y)), y_times_z), true), true, product(add(z, inverse(y)), y, y_times_z), true), true, sum(y_times_z, multiply(inverse(y), add(z, inverse(y))), add(z, inverse(y))), true), true, add(z, inverse(y)), add(y_times_z, inverse(y))), x_times_y__times_z), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by axiom 16 (closure_of_addition) R->L }
% 129.86/16.53 ifeq2(product(x_times_y, ifeq2(ifeq(ifeq(ifeq(sum(z, inverse(y), add(z, inverse(y))), true, product(y, add(z, inverse(y)), y_times_z), true), true, product(add(z, inverse(y)), y, y_times_z), true), true, sum(y_times_z, multiply(inverse(y), add(z, inverse(y))), add(z, inverse(y))), true), true, add(z, inverse(y)), add(y_times_z, inverse(y))), x_times_y__times_z), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.53 ifeq2(product(x_times_y, ifeq2(ifeq(ifeq(ifeq(true, true, ifeq(sum(z, inverse(y), add(z, inverse(y))), true, product(y, add(z, inverse(y)), y_times_z), true), true), true, product(add(z, inverse(y)), y, y_times_z), true), true, sum(y_times_z, multiply(inverse(y), add(z, inverse(y))), add(z, inverse(y))), true), true, add(z, inverse(y)), add(y_times_z, inverse(y))), x_times_y__times_z), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by axiom 2 (multiplicative_inverse2) R->L }
% 129.86/16.53 ifeq2(product(x_times_y, ifeq2(ifeq(ifeq(ifeq(product(y, inverse(y), additive_identity), true, ifeq(sum(z, inverse(y), add(z, inverse(y))), true, product(y, add(z, inverse(y)), y_times_z), true), true), true, product(add(z, inverse(y)), y, y_times_z), true), true, sum(y_times_z, multiply(inverse(y), add(z, inverse(y))), add(z, inverse(y))), true), true, add(z, inverse(y)), add(y_times_z, inverse(y))), x_times_y__times_z), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.53 ifeq2(product(x_times_y, ifeq2(ifeq(ifeq(ifeq(product(y, inverse(y), additive_identity), true, ifeq(true, true, ifeq(sum(z, inverse(y), add(z, inverse(y))), true, product(y, add(z, inverse(y)), y_times_z), true), true), true), true, product(add(z, inverse(y)), y, y_times_z), true), true, sum(y_times_z, multiply(inverse(y), add(z, inverse(y))), add(z, inverse(y))), true), true, add(z, inverse(y)), add(y_times_z, inverse(y))), x_times_y__times_z), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by axiom 4 (y_times_z) R->L }
% 129.86/16.53 ifeq2(product(x_times_y, ifeq2(ifeq(ifeq(ifeq(product(y, inverse(y), additive_identity), true, ifeq(product(y, z, y_times_z), true, ifeq(sum(z, inverse(y), add(z, inverse(y))), true, product(y, add(z, inverse(y)), y_times_z), true), true), true), true, product(add(z, inverse(y)), y, y_times_z), true), true, sum(y_times_z, multiply(inverse(y), add(z, inverse(y))), add(z, inverse(y))), true), true, add(z, inverse(y)), add(y_times_z, inverse(y))), x_times_y__times_z), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.53 ifeq2(product(x_times_y, ifeq2(ifeq(ifeq(ifeq(product(y, inverse(y), additive_identity), true, ifeq(product(y, z, y_times_z), true, ifeq(true, true, ifeq(sum(z, inverse(y), add(z, inverse(y))), true, product(y, add(z, inverse(y)), y_times_z), true), true), true), true), true, product(add(z, inverse(y)), y, y_times_z), true), true, sum(y_times_z, multiply(inverse(y), add(z, inverse(y))), add(z, inverse(y))), true), true, add(z, inverse(y)), add(y_times_z, inverse(y))), x_times_y__times_z), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by axiom 9 (additive_identity2) R->L }
% 129.86/16.53 ifeq2(product(x_times_y, ifeq2(ifeq(ifeq(ifeq(product(y, inverse(y), additive_identity), true, ifeq(product(y, z, y_times_z), true, ifeq(sum(y_times_z, additive_identity, y_times_z), true, ifeq(sum(z, inverse(y), add(z, inverse(y))), true, product(y, add(z, inverse(y)), y_times_z), true), true), true), true), true, product(add(z, inverse(y)), y, y_times_z), true), true, sum(y_times_z, multiply(inverse(y), add(z, inverse(y))), add(z, inverse(y))), true), true, add(z, inverse(y)), add(y_times_z, inverse(y))), x_times_y__times_z), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by axiom 22 (distributivity2) }
% 129.86/16.53 ifeq2(product(x_times_y, ifeq2(ifeq(ifeq(true, true, product(add(z, inverse(y)), y, y_times_z), true), true, sum(y_times_z, multiply(inverse(y), add(z, inverse(y))), add(z, inverse(y))), true), true, add(z, inverse(y)), add(y_times_z, inverse(y))), x_times_y__times_z), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by axiom 13 (ifeq_axiom) }
% 129.86/16.53 ifeq2(product(x_times_y, ifeq2(ifeq(product(add(z, inverse(y)), y, y_times_z), true, sum(y_times_z, multiply(inverse(y), add(z, inverse(y))), add(z, inverse(y))), true), true, add(z, inverse(y)), add(y_times_z, inverse(y))), x_times_y__times_z), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by lemma 26 R->L }
% 129.86/16.53 ifeq2(product(x_times_y, ifeq2(ifeq(product(add(z, inverse(y)), y, y_times_z), true, sum(y_times_z, multiply(add(z, inverse(y)), inverse(y)), add(z, inverse(y))), true), true, add(z, inverse(y)), add(y_times_z, inverse(y))), x_times_y__times_z), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.53 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.54 ifeq2(product(x_times_y, ifeq2(ifeq(true, true, ifeq(product(add(z, inverse(y)), y, y_times_z), true, sum(y_times_z, multiply(add(z, inverse(y)), inverse(y)), add(z, inverse(y))), true), true), true, add(z, inverse(y)), add(y_times_z, inverse(y))), x_times_y__times_z), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.54 = { by axiom 15 (closure_of_multiplication) R->L }
% 129.86/16.54 ifeq2(product(x_times_y, ifeq2(ifeq(product(add(z, inverse(y)), inverse(y), multiply(add(z, inverse(y)), inverse(y))), true, ifeq(product(add(z, inverse(y)), y, y_times_z), true, sum(y_times_z, multiply(add(z, inverse(y)), inverse(y)), add(z, inverse(y))), true), true), true, add(z, inverse(y)), add(y_times_z, inverse(y))), x_times_y__times_z), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.54 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.54 ifeq2(product(x_times_y, ifeq2(ifeq(product(add(z, inverse(y)), inverse(y), multiply(add(z, inverse(y)), inverse(y))), true, ifeq(product(add(z, inverse(y)), y, y_times_z), true, ifeq(true, true, sum(y_times_z, multiply(add(z, inverse(y)), inverse(y)), add(z, inverse(y))), true), true), true), true, add(z, inverse(y)), add(y_times_z, inverse(y))), x_times_y__times_z), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.54 = { by axiom 10 (additive_inverse2) R->L }
% 129.86/16.54 ifeq2(product(x_times_y, ifeq2(ifeq(product(add(z, inverse(y)), inverse(y), multiply(add(z, inverse(y)), inverse(y))), true, ifeq(product(add(z, inverse(y)), y, y_times_z), true, ifeq(sum(y, inverse(y), multiplicative_identity), true, sum(y_times_z, multiply(add(z, inverse(y)), inverse(y)), add(z, inverse(y))), true), true), true), true, add(z, inverse(y)), add(y_times_z, inverse(y))), x_times_y__times_z), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.54 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.54 ifeq2(product(x_times_y, ifeq2(ifeq(true, true, ifeq(product(add(z, inverse(y)), inverse(y), multiply(add(z, inverse(y)), inverse(y))), true, ifeq(product(add(z, inverse(y)), y, y_times_z), true, ifeq(sum(y, inverse(y), multiplicative_identity), true, sum(y_times_z, multiply(add(z, inverse(y)), inverse(y)), add(z, inverse(y))), true), true), true), true), true, add(z, inverse(y)), add(y_times_z, inverse(y))), x_times_y__times_z), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.54 = { by axiom 1 (multiplicative_identity2) R->L }
% 129.86/16.54 ifeq2(product(x_times_y, ifeq2(ifeq(product(add(z, inverse(y)), multiplicative_identity, add(z, inverse(y))), true, ifeq(product(add(z, inverse(y)), inverse(y), multiply(add(z, inverse(y)), inverse(y))), true, ifeq(product(add(z, inverse(y)), y, y_times_z), true, ifeq(sum(y, inverse(y), multiplicative_identity), true, sum(y_times_z, multiply(add(z, inverse(y)), inverse(y)), add(z, inverse(y))), true), true), true), true), true, add(z, inverse(y)), add(y_times_z, inverse(y))), x_times_y__times_z), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.54 = { by axiom 21 (distributivity1) }
% 129.86/16.54 ifeq2(product(x_times_y, ifeq2(true, true, add(z, inverse(y)), add(y_times_z, inverse(y))), x_times_y__times_z), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.54 = { by axiom 14 (ifeq_axiom) }
% 129.86/16.54 ifeq2(product(x_times_y, add(z, inverse(y)), x_times_y__times_z), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.54 = { by lemma 24 R->L }
% 129.86/16.54 ifeq2(product(x_times_y, add(inverse(y), z), x_times_y__times_z), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.54 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.54 ifeq2(ifeq(true, true, product(x_times_y, add(inverse(y), z), x_times_y__times_z), true), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.54 = { by axiom 15 (closure_of_multiplication) R->L }
% 129.86/16.54 ifeq2(ifeq(product(x_times_y, inverse(y), multiply(x_times_y, inverse(y))), true, product(x_times_y, add(inverse(y), z), x_times_y__times_z), true), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.54 = { by lemma 29 }
% 129.86/16.54 ifeq2(ifeq(product(x_times_y, inverse(y), additive_identity), true, product(x_times_y, add(inverse(y), z), x_times_y__times_z), true), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.54 = { by lemma 24 R->L }
% 129.86/16.54 ifeq2(ifeq(product(x_times_y, inverse(y), additive_identity), true, product(x_times_y, add(z, inverse(y)), x_times_y__times_z), true), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.54 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.54 ifeq2(ifeq(product(x_times_y, inverse(y), additive_identity), true, ifeq(true, true, product(x_times_y, add(z, inverse(y)), x_times_y__times_z), true), true), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.54 = { by axiom 16 (closure_of_addition) R->L }
% 129.86/16.54 ifeq2(ifeq(product(x_times_y, inverse(y), additive_identity), true, ifeq(sum(z, inverse(y), add(z, inverse(y))), true, product(x_times_y, add(z, inverse(y)), x_times_y__times_z), true), true), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.54 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.54 ifeq2(ifeq(product(x_times_y, inverse(y), additive_identity), true, ifeq(true, true, ifeq(sum(z, inverse(y), add(z, inverse(y))), true, product(x_times_y, add(z, inverse(y)), x_times_y__times_z), true), true), true), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.54 = { by axiom 7 (x_times_y__times_z) R->L }
% 129.86/16.54 ifeq2(ifeq(product(x_times_y, inverse(y), additive_identity), true, ifeq(product(x_times_y, z, x_times_y__times_z), true, ifeq(sum(z, inverse(y), add(z, inverse(y))), true, product(x_times_y, add(z, inverse(y)), x_times_y__times_z), true), true), true), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.54 = { by axiom 13 (ifeq_axiom) R->L }
% 129.86/16.54 ifeq2(ifeq(product(x_times_y, inverse(y), additive_identity), true, ifeq(product(x_times_y, z, x_times_y__times_z), true, ifeq(true, true, ifeq(sum(z, inverse(y), add(z, inverse(y))), true, product(x_times_y, add(z, inverse(y)), x_times_y__times_z), true), true), true), true), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.54 = { by axiom 9 (additive_identity2) R->L }
% 129.86/16.54 ifeq2(ifeq(product(x_times_y, inverse(y), additive_identity), true, ifeq(product(x_times_y, z, x_times_y__times_z), true, ifeq(sum(x_times_y__times_z, additive_identity, x_times_y__times_z), true, ifeq(sum(z, inverse(y), add(z, inverse(y))), true, product(x_times_y, add(z, inverse(y)), x_times_y__times_z), true), true), true), true), true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.54 = { by axiom 22 (distributivity2) }
% 129.86/16.54 ifeq2(true, true, x_times_y__times_z, multiply(x_times_y, add(y_times_z, inverse(y))))
% 129.86/16.54 = { by axiom 14 (ifeq_axiom) }
% 129.86/16.54 x_times_y__times_z
% 129.86/16.54 % SZS output end Proof
% 129.86/16.54
% 129.86/16.54 RESULT: Unsatisfiable (the axioms are contradictory).
%------------------------------------------------------------------------------