%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : RNG005-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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 12:34:44 PM UTC 2026
% Result : Unsatisfiable 189.55s 24.34s
% Output : Proof 190.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG005-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n026.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 23:00:56 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 189.55/24.34 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
% 189.55/24.34
% 189.55/24.34 % SZS status Unsatisfiable
% 189.55/24.34
% 189.55/24.39 % SZS output start Proof
% 189.55/24.39 Axiom 1 (additive_identity2): sum(X, additive_identity, X) = true.
% 189.55/24.39 Axiom 2 (additive_identity1): sum(additive_identity, X, X) = true.
% 189.55/24.39 Axiom 3 (left_inverse): sum(additive_inverse(X), X, additive_identity) = true.
% 189.55/24.39 Axiom 4 (a_times_b): product(a, b, d) = true.
% 189.55/24.39 Axiom 5 (a_inverse_times_b): product(additive_inverse(a), b, c) = true.
% 189.55/24.39 Axiom 6 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 189.55/24.39 Axiom 7 (ifeq_axiom): ifeq2(X, X, Y, Z) = Y.
% 189.55/24.39 Axiom 8 (closure_of_addition): sum(X, Y, add(X, Y)) = true.
% 189.55/24.39 Axiom 9 (closure_of_multiplication): product(X, Y, multiply(X, Y)) = true.
% 189.55/24.39 Axiom 10 (commutativity_of_addition): ifeq(sum(X, Y, Z), true, sum(Y, X, Z), true) = true.
% 189.55/24.39 Axiom 11 (addition_is_well_defined): ifeq2(sum(X, Y, Z), true, ifeq2(sum(X, Y, W), true, W, Z), Z) = Z.
% 189.55/24.39 Axiom 12 (multiplication_is_well_defined): ifeq2(product(X, Y, Z), true, ifeq2(product(X, Y, W), true, W, Z), Z) = Z.
% 189.55/24.39 Axiom 13 (associativity_of_addition1): ifeq(sum(X, Y, Z), true, ifeq(sum(W, Y, V), true, ifeq(sum(U, W, X), true, sum(U, V, Z), true), true), true) = true.
% 189.55/24.39 Axiom 14 (associativity_of_addition2): ifeq(sum(X, Y, Z), true, ifeq(sum(W, Z, V), true, ifeq(sum(W, X, U), true, sum(U, Y, V), true), true), true) = true.
% 189.55/24.39 Axiom 15 (distributivity4): ifeq(product(X, Y, Z), true, ifeq(product(W, Y, V), true, ifeq(sum(V, Z, U), true, ifeq(sum(W, X, T), true, product(T, Y, U), true), true), true), true) = true.
% 189.55/24.39
% 189.55/24.39 Lemma 16: ifeq2(sum(X, Y, Z), true, add(X, Y), Z) = Z.
% 189.55/24.39 Proof:
% 189.55/24.39 ifeq2(sum(X, Y, Z), true, add(X, Y), Z)
% 189.55/24.39 = { by axiom 7 (ifeq_axiom) R->L }
% 189.55/24.39 ifeq2(sum(X, Y, Z), true, ifeq2(true, true, add(X, Y), Z), Z)
% 189.55/24.39 = { by axiom 8 (closure_of_addition) R->L }
% 189.55/24.39 ifeq2(sum(X, Y, Z), true, ifeq2(sum(X, Y, add(X, Y)), true, add(X, Y), Z), Z)
% 189.55/24.39 = { by axiom 11 (addition_is_well_defined) }
% 189.55/24.39 Z
% 189.55/24.39
% 189.55/24.39 Lemma 17: add(X, Y) = add(Y, X).
% 189.55/24.39 Proof:
% 189.55/24.39 add(X, Y)
% 189.55/24.39 = { by lemma 16 R->L }
% 189.55/24.39 ifeq2(sum(Y, X, add(X, Y)), true, add(Y, X), add(X, Y))
% 189.55/24.40 = { by axiom 6 (ifeq_axiom) R->L }
% 189.55/24.40 ifeq2(ifeq(true, true, sum(Y, X, add(X, Y)), true), true, add(Y, X), add(X, Y))
% 189.55/24.40 = { by axiom 8 (closure_of_addition) R->L }
% 189.55/24.40 ifeq2(ifeq(sum(X, Y, add(X, Y)), true, sum(Y, X, add(X, Y)), true), true, add(Y, X), add(X, Y))
% 189.55/24.40 = { by axiom 10 (commutativity_of_addition) }
% 189.55/24.40 ifeq2(true, true, add(Y, X), add(X, Y))
% 189.55/24.40 = { by axiom 7 (ifeq_axiom) }
% 189.55/24.40 add(Y, X)
% 189.55/24.40
% 189.55/24.40 Goal 1 (prove_sum_is_additive_id): sum(c, d, additive_identity) = true.
% 189.55/24.40 Proof:
% 189.55/24.40 sum(c, d, additive_identity)
% 189.55/24.40 = { by axiom 6 (ifeq_axiom) R->L }
% 189.55/24.40 ifeq(true, true, sum(c, d, additive_identity), true)
% 189.55/24.40 = { by axiom 2 (additive_identity1) R->L }
% 189.55/24.40 ifeq(sum(additive_identity, additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 189.55/24.40 = { by axiom 7 (ifeq_axiom) R->L }
% 189.55/24.40 ifeq(sum(ifeq2(true, true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 189.55/24.40 = { by axiom 14 (associativity_of_addition2) R->L }
% 189.55/24.40 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), d), true, ifeq(sum(add(additive_identity, additive_inverse(d)), d, add(add(additive_identity, additive_inverse(d)), d)), true, ifeq(sum(add(additive_identity, additive_inverse(d)), d, additive_identity), true, sum(additive_identity, multiply(additive_identity, b), add(add(additive_identity, additive_inverse(d)), d)), true), true), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 189.55/24.40 = { by axiom 8 (closure_of_addition) }
% 189.55/24.40 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), d), true, ifeq(true, true, ifeq(sum(add(additive_identity, additive_inverse(d)), d, additive_identity), true, sum(additive_identity, multiply(additive_identity, b), add(add(additive_identity, additive_inverse(d)), d)), true), true), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 189.55/24.40 = { by axiom 6 (ifeq_axiom) }
% 189.55/24.40 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), d), true, ifeq(sum(add(additive_identity, additive_inverse(d)), d, additive_identity), true, sum(additive_identity, multiply(additive_identity, b), add(add(additive_identity, additive_inverse(d)), d)), true), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 189.55/24.40 = { by lemma 17 }
% 189.55/24.40 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), d), true, ifeq(sum(add(additive_identity, additive_inverse(d)), d, additive_identity), true, sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 189.55/24.40 = { by axiom 6 (ifeq_axiom) R->L }
% 189.55/24.40 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), d), true, ifeq(ifeq(true, true, sum(add(additive_identity, additive_inverse(d)), d, additive_identity), true), true, sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 189.55/24.40 = { by axiom 8 (closure_of_addition) R->L }
% 189.55/24.40 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), d), true, ifeq(ifeq(sum(additive_identity, additive_inverse(d), add(additive_identity, additive_inverse(d))), true, sum(add(additive_identity, additive_inverse(d)), d, additive_identity), true), true, sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 189.55/24.40 = { by axiom 6 (ifeq_axiom) R->L }
% 189.55/24.40 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), d), true, ifeq(ifeq(true, true, ifeq(sum(additive_identity, additive_inverse(d), add(additive_identity, additive_inverse(d))), true, sum(add(additive_identity, additive_inverse(d)), d, additive_identity), true), true), true, sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 189.55/24.40 = { by axiom 3 (left_inverse) R->L }
% 190.36/24.40 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), d), true, ifeq(ifeq(sum(additive_inverse(d), d, additive_identity), true, ifeq(sum(additive_identity, additive_inverse(d), add(additive_identity, additive_inverse(d))), true, sum(add(additive_identity, additive_inverse(d)), d, additive_identity), true), true), true, sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.40 = { by axiom 6 (ifeq_axiom) R->L }
% 190.36/24.40 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), d), true, ifeq(ifeq(sum(additive_inverse(d), d, additive_identity), true, ifeq(true, true, ifeq(sum(additive_identity, additive_inverse(d), add(additive_identity, additive_inverse(d))), true, sum(add(additive_identity, additive_inverse(d)), d, additive_identity), true), true), true), true, sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.40 = { by axiom 1 (additive_identity2) R->L }
% 190.36/24.40 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), d), true, ifeq(ifeq(sum(additive_inverse(d), d, additive_identity), true, ifeq(sum(additive_identity, additive_identity, additive_identity), true, ifeq(sum(additive_identity, additive_inverse(d), add(additive_identity, additive_inverse(d))), true, sum(add(additive_identity, additive_inverse(d)), d, additive_identity), true), true), true), true, sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.41 = { by axiom 14 (associativity_of_addition2) }
% 190.36/24.41 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), d), true, ifeq(true, true, sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.41 = { by axiom 6 (ifeq_axiom) }
% 190.36/24.41 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), d), true, sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.41 = { by axiom 7 (ifeq_axiom) R->L }
% 190.36/24.41 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), ifeq2(true, true, d, add(d, multiply(additive_identity, b)))), true, sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.41 = { by axiom 15 (distributivity4) R->L }
% 190.36/24.41 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), ifeq2(ifeq(product(additive_identity, b, multiply(additive_identity, b)), true, ifeq(product(a, b, d), true, ifeq(sum(d, multiply(additive_identity, b), add(d, multiply(additive_identity, b))), true, ifeq(sum(a, additive_identity, a), true, product(a, b, add(d, multiply(additive_identity, b))), true), true), true), true), true, d, add(d, multiply(additive_identity, b)))), true, sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.41 = { by axiom 1 (additive_identity2) }
% 190.36/24.41 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), ifeq2(ifeq(product(additive_identity, b, multiply(additive_identity, b)), true, ifeq(product(a, b, d), true, ifeq(sum(d, multiply(additive_identity, b), add(d, multiply(additive_identity, b))), true, ifeq(true, true, product(a, b, add(d, multiply(additive_identity, b))), true), true), true), true), true, d, add(d, multiply(additive_identity, b)))), true, sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.41 = { by axiom 6 (ifeq_axiom) }
% 190.36/24.41 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), ifeq2(ifeq(product(additive_identity, b, multiply(additive_identity, b)), true, ifeq(product(a, b, d), true, ifeq(sum(d, multiply(additive_identity, b), add(d, multiply(additive_identity, b))), true, product(a, b, add(d, multiply(additive_identity, b))), true), true), true), true, d, add(d, multiply(additive_identity, b)))), true, sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.41 = { by axiom 4 (a_times_b) }
% 190.36/24.41 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), ifeq2(ifeq(product(additive_identity, b, multiply(additive_identity, b)), true, ifeq(true, true, ifeq(sum(d, multiply(additive_identity, b), add(d, multiply(additive_identity, b))), true, product(a, b, add(d, multiply(additive_identity, b))), true), true), true), true, d, add(d, multiply(additive_identity, b)))), true, sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.41 = { by axiom 6 (ifeq_axiom) }
% 190.36/24.41 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), ifeq2(ifeq(product(additive_identity, b, multiply(additive_identity, b)), true, ifeq(sum(d, multiply(additive_identity, b), add(d, multiply(additive_identity, b))), true, product(a, b, add(d, multiply(additive_identity, b))), true), true), true, d, add(d, multiply(additive_identity, b)))), true, sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.41 = { by axiom 8 (closure_of_addition) }
% 190.36/24.41 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), ifeq2(ifeq(product(additive_identity, b, multiply(additive_identity, b)), true, ifeq(true, true, product(a, b, add(d, multiply(additive_identity, b))), true), true), true, d, add(d, multiply(additive_identity, b)))), true, sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.41 = { by axiom 6 (ifeq_axiom) }
% 190.36/24.41 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), ifeq2(ifeq(product(additive_identity, b, multiply(additive_identity, b)), true, product(a, b, add(d, multiply(additive_identity, b))), true), true, d, add(d, multiply(additive_identity, b)))), true, sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.41 = { by lemma 17 }
% 190.36/24.41 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), ifeq2(ifeq(product(additive_identity, b, multiply(additive_identity, b)), true, product(a, b, add(multiply(additive_identity, b), d)), true), true, d, add(d, multiply(additive_identity, b)))), true, sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.41 = { by axiom 9 (closure_of_multiplication) }
% 190.36/24.41 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), ifeq2(ifeq(true, true, product(a, b, add(multiply(additive_identity, b), d)), true), true, d, add(d, multiply(additive_identity, b)))), true, sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.41 = { by axiom 6 (ifeq_axiom) }
% 190.36/24.41 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), ifeq2(product(a, b, add(multiply(additive_identity, b), d)), true, d, add(d, multiply(additive_identity, b)))), true, sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.41 = { by lemma 17 }
% 190.36/24.41 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), ifeq2(product(a, b, add(d, multiply(additive_identity, b))), true, d, add(d, multiply(additive_identity, b)))), true, sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.41 = { by axiom 7 (ifeq_axiom) R->L }
% 190.36/24.41 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), ifeq2(product(a, b, add(d, multiply(additive_identity, b))), true, ifeq2(true, true, d, add(d, multiply(additive_identity, b))), add(d, multiply(additive_identity, b)))), true, sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.41 = { by axiom 4 (a_times_b) R->L }
% 190.36/24.41 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), ifeq2(product(a, b, add(d, multiply(additive_identity, b))), true, ifeq2(product(a, b, d), true, d, add(d, multiply(additive_identity, b))), add(d, multiply(additive_identity, b)))), true, sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.41 = { by axiom 12 (multiplication_is_well_defined) }
% 190.36/24.41 ifeq(sum(ifeq2(ifeq(sum(d, multiply(additive_identity, b), add(d, multiply(additive_identity, b))), true, sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.41 = { by axiom 8 (closure_of_addition) }
% 190.36/24.41 ifeq(sum(ifeq2(ifeq(true, true, sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.41 = { by axiom 6 (ifeq_axiom) }
% 190.36/24.41 ifeq(sum(ifeq2(sum(additive_identity, multiply(additive_identity, b), add(d, add(additive_identity, additive_inverse(d)))), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.41 = { by lemma 17 R->L }
% 190.36/24.42 ifeq(sum(ifeq2(sum(additive_identity, multiply(additive_identity, b), add(add(additive_identity, additive_inverse(d)), d)), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by axiom 7 (ifeq_axiom) R->L }
% 190.36/24.42 ifeq(sum(ifeq2(sum(additive_identity, multiply(additive_identity, b), ifeq2(true, true, add(add(additive_identity, additive_inverse(d)), d), additive_identity)), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by axiom 14 (associativity_of_addition2) R->L }
% 190.36/24.42 ifeq(sum(ifeq2(sum(additive_identity, multiply(additive_identity, b), ifeq2(ifeq(sum(additive_inverse(d), d, additive_identity), true, ifeq(sum(additive_identity, additive_identity, additive_identity), true, ifeq(sum(additive_identity, additive_inverse(d), add(additive_identity, additive_inverse(d))), true, sum(add(additive_identity, additive_inverse(d)), d, additive_identity), true), true), true), true, add(add(additive_identity, additive_inverse(d)), d), additive_identity)), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by axiom 1 (additive_identity2) }
% 190.36/24.42 ifeq(sum(ifeq2(sum(additive_identity, multiply(additive_identity, b), ifeq2(ifeq(sum(additive_inverse(d), d, additive_identity), true, ifeq(true, true, ifeq(sum(additive_identity, additive_inverse(d), add(additive_identity, additive_inverse(d))), true, sum(add(additive_identity, additive_inverse(d)), d, additive_identity), true), true), true), true, add(add(additive_identity, additive_inverse(d)), d), additive_identity)), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by axiom 6 (ifeq_axiom) }
% 190.36/24.42 ifeq(sum(ifeq2(sum(additive_identity, multiply(additive_identity, b), ifeq2(ifeq(sum(additive_inverse(d), d, additive_identity), true, ifeq(sum(additive_identity, additive_inverse(d), add(additive_identity, additive_inverse(d))), true, sum(add(additive_identity, additive_inverse(d)), d, additive_identity), true), true), true, add(add(additive_identity, additive_inverse(d)), d), additive_identity)), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by axiom 3 (left_inverse) }
% 190.36/24.42 ifeq(sum(ifeq2(sum(additive_identity, multiply(additive_identity, b), ifeq2(ifeq(true, true, ifeq(sum(additive_identity, additive_inverse(d), add(additive_identity, additive_inverse(d))), true, sum(add(additive_identity, additive_inverse(d)), d, additive_identity), true), true), true, add(add(additive_identity, additive_inverse(d)), d), additive_identity)), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by axiom 6 (ifeq_axiom) }
% 190.36/24.42 ifeq(sum(ifeq2(sum(additive_identity, multiply(additive_identity, b), ifeq2(ifeq(sum(additive_identity, additive_inverse(d), add(additive_identity, additive_inverse(d))), true, sum(add(additive_identity, additive_inverse(d)), d, additive_identity), true), true, add(add(additive_identity, additive_inverse(d)), d), additive_identity)), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by axiom 8 (closure_of_addition) }
% 190.36/24.42 ifeq(sum(ifeq2(sum(additive_identity, multiply(additive_identity, b), ifeq2(ifeq(true, true, sum(add(additive_identity, additive_inverse(d)), d, additive_identity), true), true, add(add(additive_identity, additive_inverse(d)), d), additive_identity)), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by axiom 6 (ifeq_axiom) }
% 190.36/24.42 ifeq(sum(ifeq2(sum(additive_identity, multiply(additive_identity, b), ifeq2(sum(add(additive_identity, additive_inverse(d)), d, additive_identity), true, add(add(additive_identity, additive_inverse(d)), d), additive_identity)), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by lemma 16 }
% 190.36/24.42 ifeq(sum(ifeq2(sum(additive_identity, multiply(additive_identity, b), additive_identity), true, additive_identity, multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by axiom 7 (ifeq_axiom) R->L }
% 190.36/24.42 ifeq(sum(ifeq2(true, true, ifeq2(sum(additive_identity, multiply(additive_identity, b), additive_identity), true, additive_identity, multiply(additive_identity, b)), multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by axiom 2 (additive_identity1) R->L }
% 190.36/24.42 ifeq(sum(ifeq2(sum(additive_identity, multiply(additive_identity, b), multiply(additive_identity, b)), true, ifeq2(sum(additive_identity, multiply(additive_identity, b), additive_identity), true, additive_identity, multiply(additive_identity, b)), multiply(additive_identity, b)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by axiom 11 (addition_is_well_defined) }
% 190.36/24.42 ifeq(sum(multiply(additive_identity, b), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by axiom 7 (ifeq_axiom) R->L }
% 190.36/24.42 ifeq(sum(ifeq2(true, true, multiply(additive_identity, b), add(d, c)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by axiom 15 (distributivity4) R->L }
% 190.36/24.42 ifeq(sum(ifeq2(ifeq(product(a, b, d), true, ifeq(product(additive_inverse(a), b, c), true, ifeq(sum(c, d, add(c, d)), true, ifeq(sum(additive_inverse(a), a, additive_identity), true, product(additive_identity, b, add(c, d)), true), true), true), true), true, multiply(additive_identity, b), add(d, c)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by axiom 4 (a_times_b) }
% 190.36/24.42 ifeq(sum(ifeq2(ifeq(true, true, ifeq(product(additive_inverse(a), b, c), true, ifeq(sum(c, d, add(c, d)), true, ifeq(sum(additive_inverse(a), a, additive_identity), true, product(additive_identity, b, add(c, d)), true), true), true), true), true, multiply(additive_identity, b), add(d, c)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by axiom 6 (ifeq_axiom) }
% 190.36/24.42 ifeq(sum(ifeq2(ifeq(product(additive_inverse(a), b, c), true, ifeq(sum(c, d, add(c, d)), true, ifeq(sum(additive_inverse(a), a, additive_identity), true, product(additive_identity, b, add(c, d)), true), true), true), true, multiply(additive_identity, b), add(d, c)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by axiom 3 (left_inverse) }
% 190.36/24.42 ifeq(sum(ifeq2(ifeq(product(additive_inverse(a), b, c), true, ifeq(sum(c, d, add(c, d)), true, ifeq(true, true, product(additive_identity, b, add(c, d)), true), true), true), true, multiply(additive_identity, b), add(d, c)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by axiom 6 (ifeq_axiom) }
% 190.36/24.42 ifeq(sum(ifeq2(ifeq(product(additive_inverse(a), b, c), true, ifeq(sum(c, d, add(c, d)), true, product(additive_identity, b, add(c, d)), true), true), true, multiply(additive_identity, b), add(d, c)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by axiom 5 (a_inverse_times_b) }
% 190.36/24.42 ifeq(sum(ifeq2(ifeq(true, true, ifeq(sum(c, d, add(c, d)), true, product(additive_identity, b, add(c, d)), true), true), true, multiply(additive_identity, b), add(d, c)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by axiom 6 (ifeq_axiom) }
% 190.36/24.42 ifeq(sum(ifeq2(ifeq(sum(c, d, add(c, d)), true, product(additive_identity, b, add(c, d)), true), true, multiply(additive_identity, b), add(d, c)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by axiom 8 (closure_of_addition) }
% 190.36/24.42 ifeq(sum(ifeq2(ifeq(true, true, product(additive_identity, b, add(c, d)), true), true, multiply(additive_identity, b), add(d, c)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by axiom 6 (ifeq_axiom) }
% 190.36/24.42 ifeq(sum(ifeq2(product(additive_identity, b, add(c, d)), true, multiply(additive_identity, b), add(d, c)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by lemma 17 }
% 190.36/24.42 ifeq(sum(ifeq2(product(additive_identity, b, add(d, c)), true, multiply(additive_identity, b), add(d, c)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by axiom 7 (ifeq_axiom) R->L }
% 190.36/24.42 ifeq(sum(ifeq2(product(additive_identity, b, add(d, c)), true, ifeq2(true, true, multiply(additive_identity, b), add(d, c)), add(d, c)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by axiom 9 (closure_of_multiplication) R->L }
% 190.36/24.42 ifeq(sum(ifeq2(product(additive_identity, b, add(d, c)), true, ifeq2(product(additive_identity, b, multiply(additive_identity, b)), true, multiply(additive_identity, b), add(d, c)), add(d, c)), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by axiom 12 (multiplication_is_well_defined) }
% 190.36/24.42 ifeq(sum(add(d, c), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by lemma 17 R->L }
% 190.36/24.42 ifeq(sum(add(c, d), additive_identity, additive_identity), true, sum(c, d, additive_identity), true)
% 190.36/24.42 = { by axiom 6 (ifeq_axiom) R->L }
% 190.36/24.42 ifeq(sum(add(c, d), additive_identity, additive_identity), true, ifeq(true, true, sum(c, d, additive_identity), true), true)
% 190.36/24.42 = { by axiom 8 (closure_of_addition) R->L }
% 190.36/24.42 ifeq(sum(add(c, d), additive_identity, additive_identity), true, ifeq(sum(c, d, add(c, d)), true, sum(c, d, additive_identity), true), true)
% 190.36/24.42 = { by axiom 6 (ifeq_axiom) R->L }
% 190.36/24.42 ifeq(sum(add(c, d), additive_identity, additive_identity), true, ifeq(true, true, ifeq(sum(c, d, add(c, d)), true, sum(c, d, additive_identity), true), true), true)
% 190.36/24.42 = { by axiom 1 (additive_identity2) R->L }
% 190.36/24.42 ifeq(sum(add(c, d), additive_identity, additive_identity), true, ifeq(sum(d, additive_identity, d), true, ifeq(sum(c, d, add(c, d)), true, sum(c, d, additive_identity), true), true), true)
% 190.36/24.42 = { by axiom 13 (associativity_of_addition1) }
% 190.36/24.42 true
% 190.36/24.42 % SZS output end Proof
% 190.36/24.42
% 190.36/24.42 RESULT: Unsatisfiable (the axioms are contradictory).
%------------------------------------------------------------------------------