%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : RNG083+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox/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 12:34:57 PM UTC 2026
% Result : Theorem 0.83s 0.51s
% Output : Proof 0.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : RNG083+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.31 % CPULimit : 300
% 0.03/0.31 % WCLimit : 300
% 0.03/0.31 % DateTime : Sun Sep 27 23:10:49 UTC 2026
% 0.03/0.31 % CPUTime :
% 0.03/0.31 Running run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.83/0.51 Command-line arguments: --no-flatten-goal
% 0.83/0.51
% 0.83/0.51 % SZS status Theorem
% 0.83/0.51
% 0.83/0.53 % SZS output start Proof
% 0.83/0.53 Axiom 1 (m__468): aElement0(xx) = true.
% 0.83/0.53 Axiom 2 (mSortsC_01): aElement0(sz10) = true.
% 0.83/0.53 Axiom 3 (mSortsC): aElement0(sz00) = true.
% 0.83/0.53 Axiom 4 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 0.83/0.53 Axiom 5 (ifeq_axiom): ifeq2(X, X, Y, Z) = Y.
% 0.83/0.53 Axiom 6 (mSortsU): ifeq(aElement0(X), true, aElement0(smndt0(X)), true) = true.
% 0.83/0.53 Axiom 7 (mAddZero): ifeq2(aElement0(X), true, sdtpldt0(X, sz00), X) = X.
% 0.83/0.53 Axiom 8 (mAddZero_1): ifeq2(aElement0(X), true, sdtpldt0(sz00, X), X) = X.
% 0.83/0.53 Axiom 9 (mAddInvr): ifeq2(aElement0(X), true, sdtpldt0(X, smndt0(X)), sz00) = sz00.
% 0.83/0.53 Axiom 10 (mMulMnOne_1): ifeq2(aElement0(X), true, sdtasdt0(smndt0(sz10), X), smndt0(X)) = smndt0(X).
% 0.83/0.53 Axiom 11 (mSortsB_02): ifeq(aElement0(X), true, ifeq(aElement0(Y), true, aElement0(sdtasdt0(Y, X)), true), true) = true.
% 0.83/0.53 Axiom 12 (mMulComm): ifeq2(aElement0(X), true, ifeq2(aElement0(Y), true, sdtasdt0(Y, X), sdtasdt0(X, Y)), sdtasdt0(X, Y)) = sdtasdt0(X, Y).
% 0.83/0.53 Axiom 13 (mMulAsso): ifeq2(aElement0(X), true, ifeq2(aElement0(Y), true, ifeq2(aElement0(Z), true, sdtasdt0(sdtasdt0(Z, Y), X), sdtasdt0(Z, sdtasdt0(Y, X))), sdtasdt0(Z, sdtasdt0(Y, X))), sdtasdt0(Z, sdtasdt0(Y, X))) = sdtasdt0(Z, sdtasdt0(Y, X)).
% 0.83/0.53 Axiom 14 (mAMDistr_1): ifeq2(aElement0(X), true, ifeq2(aElement0(Y), true, ifeq2(aElement0(Z), true, sdtpldt0(sdtasdt0(Y, Z), sdtasdt0(X, Z)), sdtasdt0(sdtpldt0(Y, X), Z)), sdtasdt0(sdtpldt0(Y, X), Z)), sdtasdt0(sdtpldt0(Y, X), Z)) = sdtasdt0(sdtpldt0(Y, X), Z).
% 0.83/0.53
% 0.83/0.53 Lemma 15: sdtasdt0(smndt0(sz10), sdtasdt0(sz00, xx)) = smndt0(sdtasdt0(sz00, xx)).
% 0.83/0.53 Proof:
% 0.83/0.53 sdtasdt0(smndt0(sz10), sdtasdt0(sz00, xx))
% 0.83/0.53 = { by axiom 5 (ifeq_axiom) R->L }
% 0.83/0.53 ifeq2(true, true, sdtasdt0(smndt0(sz10), sdtasdt0(sz00, xx)), smndt0(sdtasdt0(sz00, xx)))
% 0.83/0.53 = { by axiom 11 (mSortsB_02) R->L }
% 0.83/0.53 ifeq2(ifeq(aElement0(xx), true, ifeq(aElement0(sz00), true, aElement0(sdtasdt0(sz00, xx)), true), true), true, sdtasdt0(smndt0(sz10), sdtasdt0(sz00, xx)), smndt0(sdtasdt0(sz00, xx)))
% 0.83/0.53 = { by axiom 1 (m__468) }
% 0.83/0.53 ifeq2(ifeq(true, true, ifeq(aElement0(sz00), true, aElement0(sdtasdt0(sz00, xx)), true), true), true, sdtasdt0(smndt0(sz10), sdtasdt0(sz00, xx)), smndt0(sdtasdt0(sz00, xx)))
% 0.83/0.53 = { by axiom 4 (ifeq_axiom) }
% 0.83/0.53 ifeq2(ifeq(aElement0(sz00), true, aElement0(sdtasdt0(sz00, xx)), true), true, sdtasdt0(smndt0(sz10), sdtasdt0(sz00, xx)), smndt0(sdtasdt0(sz00, xx)))
% 0.83/0.53 = { by axiom 3 (mSortsC) }
% 0.83/0.53 ifeq2(ifeq(true, true, aElement0(sdtasdt0(sz00, xx)), true), true, sdtasdt0(smndt0(sz10), sdtasdt0(sz00, xx)), smndt0(sdtasdt0(sz00, xx)))
% 0.83/0.53 = { by axiom 4 (ifeq_axiom) }
% 0.83/0.53 ifeq2(aElement0(sdtasdt0(sz00, xx)), true, sdtasdt0(smndt0(sz10), sdtasdt0(sz00, xx)), smndt0(sdtasdt0(sz00, xx)))
% 0.83/0.53 = { by axiom 10 (mMulMnOne_1) }
% 0.83/0.53 smndt0(sdtasdt0(sz00, xx))
% 0.83/0.53
% 0.83/0.53 Lemma 16: sdtasdt0(sz00, xx) = sz00.
% 0.83/0.53 Proof:
% 0.83/0.54 sdtasdt0(sz00, xx)
% 0.83/0.54 = { by axiom 7 (mAddZero) R->L }
% 0.83/0.54 sdtasdt0(ifeq2(aElement0(sz00), true, sdtpldt0(sz00, sz00), sz00), xx)
% 0.83/0.54 = { by axiom 3 (mSortsC) }
% 0.83/0.54 sdtasdt0(ifeq2(true, true, sdtpldt0(sz00, sz00), sz00), xx)
% 0.83/0.54 = { by axiom 5 (ifeq_axiom) }
% 0.83/0.54 sdtasdt0(sdtpldt0(sz00, sz00), xx)
% 0.83/0.54 = { by axiom 14 (mAMDistr_1) R->L }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, sdtpldt0(sdtasdt0(sz00, xx), sdtasdt0(sz00, xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 5 (ifeq_axiom) R->L }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(true, true, sdtpldt0(sdtasdt0(sz00, xx), sdtasdt0(sz00, xx)), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 11 (mSortsB_02) R->L }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(ifeq(aElement0(xx), true, ifeq(aElement0(sz00), true, aElement0(sdtasdt0(sz00, xx)), true), true), true, sdtpldt0(sdtasdt0(sz00, xx), sdtasdt0(sz00, xx)), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 1 (m__468) }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(ifeq(true, true, ifeq(aElement0(sz00), true, aElement0(sdtasdt0(sz00, xx)), true), true), true, sdtpldt0(sdtasdt0(sz00, xx), sdtasdt0(sz00, xx)), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 4 (ifeq_axiom) }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(ifeq(aElement0(sz00), true, aElement0(sdtasdt0(sz00, xx)), true), true, sdtpldt0(sdtasdt0(sz00, xx), sdtasdt0(sz00, xx)), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 3 (mSortsC) }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(ifeq(true, true, aElement0(sdtasdt0(sz00, xx)), true), true, sdtpldt0(sdtasdt0(sz00, xx), sdtasdt0(sz00, xx)), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 4 (ifeq_axiom) }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(aElement0(sdtasdt0(sz00, xx)), true, sdtpldt0(sdtasdt0(sz00, xx), sdtasdt0(sz00, xx)), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 5 (ifeq_axiom) R->L }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(aElement0(sdtasdt0(sz00, xx)), true, sdtpldt0(sdtasdt0(sz00, xx), sdtasdt0(ifeq2(true, true, sz00, smndt0(sz00)), xx)), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 6 (mSortsU) R->L }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(aElement0(sdtasdt0(sz00, xx)), true, sdtpldt0(sdtasdt0(sz00, xx), sdtasdt0(ifeq2(ifeq(aElement0(sz00), true, aElement0(smndt0(sz00)), true), true, sz00, smndt0(sz00)), xx)), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 3 (mSortsC) }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(aElement0(sdtasdt0(sz00, xx)), true, sdtpldt0(sdtasdt0(sz00, xx), sdtasdt0(ifeq2(ifeq(true, true, aElement0(smndt0(sz00)), true), true, sz00, smndt0(sz00)), xx)), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 4 (ifeq_axiom) }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(aElement0(sdtasdt0(sz00, xx)), true, sdtpldt0(sdtasdt0(sz00, xx), sdtasdt0(ifeq2(aElement0(smndt0(sz00)), true, sz00, smndt0(sz00)), xx)), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 9 (mAddInvr) R->L }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(aElement0(sdtasdt0(sz00, xx)), true, sdtpldt0(sdtasdt0(sz00, xx), sdtasdt0(ifeq2(aElement0(smndt0(sz00)), true, ifeq2(aElement0(sz00), true, sdtpldt0(sz00, smndt0(sz00)), sz00), smndt0(sz00)), xx)), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 3 (mSortsC) }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(aElement0(sdtasdt0(sz00, xx)), true, sdtpldt0(sdtasdt0(sz00, xx), sdtasdt0(ifeq2(aElement0(smndt0(sz00)), true, ifeq2(true, true, sdtpldt0(sz00, smndt0(sz00)), sz00), smndt0(sz00)), xx)), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 5 (ifeq_axiom) }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(aElement0(sdtasdt0(sz00, xx)), true, sdtpldt0(sdtasdt0(sz00, xx), sdtasdt0(ifeq2(aElement0(smndt0(sz00)), true, sdtpldt0(sz00, smndt0(sz00)), smndt0(sz00)), xx)), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 8 (mAddZero_1) }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(aElement0(sdtasdt0(sz00, xx)), true, sdtpldt0(sdtasdt0(sz00, xx), sdtasdt0(smndt0(sz00), xx)), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 10 (mMulMnOne_1) R->L }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(aElement0(sdtasdt0(sz00, xx)), true, sdtpldt0(sdtasdt0(sz00, xx), sdtasdt0(ifeq2(aElement0(sz00), true, sdtasdt0(smndt0(sz10), sz00), smndt0(sz00)), xx)), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 3 (mSortsC) }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(aElement0(sdtasdt0(sz00, xx)), true, sdtpldt0(sdtasdt0(sz00, xx), sdtasdt0(ifeq2(true, true, sdtasdt0(smndt0(sz10), sz00), smndt0(sz00)), xx)), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 5 (ifeq_axiom) }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(aElement0(sdtasdt0(sz00, xx)), true, sdtpldt0(sdtasdt0(sz00, xx), sdtasdt0(sdtasdt0(smndt0(sz10), sz00), xx)), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 5 (ifeq_axiom) R->L }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(aElement0(sdtasdt0(sz00, xx)), true, sdtpldt0(sdtasdt0(sz00, xx), ifeq2(true, true, sdtasdt0(sdtasdt0(smndt0(sz10), sz00), xx), smndt0(sdtasdt0(sz00, xx)))), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 6 (mSortsU) R->L }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(aElement0(sdtasdt0(sz00, xx)), true, sdtpldt0(sdtasdt0(sz00, xx), ifeq2(ifeq(aElement0(sz10), true, aElement0(smndt0(sz10)), true), true, sdtasdt0(sdtasdt0(smndt0(sz10), sz00), xx), smndt0(sdtasdt0(sz00, xx)))), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 2 (mSortsC_01) }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(aElement0(sdtasdt0(sz00, xx)), true, sdtpldt0(sdtasdt0(sz00, xx), ifeq2(ifeq(true, true, aElement0(smndt0(sz10)), true), true, sdtasdt0(sdtasdt0(smndt0(sz10), sz00), xx), smndt0(sdtasdt0(sz00, xx)))), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 4 (ifeq_axiom) }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(aElement0(sdtasdt0(sz00, xx)), true, sdtpldt0(sdtasdt0(sz00, xx), ifeq2(aElement0(smndt0(sz10)), true, sdtasdt0(sdtasdt0(smndt0(sz10), sz00), xx), smndt0(sdtasdt0(sz00, xx)))), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 5 (ifeq_axiom) R->L }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(aElement0(sdtasdt0(sz00, xx)), true, sdtpldt0(sdtasdt0(sz00, xx), ifeq2(true, true, ifeq2(aElement0(smndt0(sz10)), true, sdtasdt0(sdtasdt0(smndt0(sz10), sz00), xx), smndt0(sdtasdt0(sz00, xx))), sdtasdt0(smndt0(sz10), sdtasdt0(sz00, xx)))), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 3 (mSortsC) R->L }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(aElement0(sdtasdt0(sz00, xx)), true, sdtpldt0(sdtasdt0(sz00, xx), ifeq2(aElement0(sz00), true, ifeq2(aElement0(smndt0(sz10)), true, sdtasdt0(sdtasdt0(smndt0(sz10), sz00), xx), smndt0(sdtasdt0(sz00, xx))), sdtasdt0(smndt0(sz10), sdtasdt0(sz00, xx)))), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 5 (ifeq_axiom) R->L }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(aElement0(sdtasdt0(sz00, xx)), true, sdtpldt0(sdtasdt0(sz00, xx), ifeq2(true, true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(smndt0(sz10)), true, sdtasdt0(sdtasdt0(smndt0(sz10), sz00), xx), smndt0(sdtasdt0(sz00, xx))), sdtasdt0(smndt0(sz10), sdtasdt0(sz00, xx))), sdtasdt0(smndt0(sz10), sdtasdt0(sz00, xx)))), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 1 (m__468) R->L }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(aElement0(sdtasdt0(sz00, xx)), true, sdtpldt0(sdtasdt0(sz00, xx), ifeq2(aElement0(xx), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(smndt0(sz10)), true, sdtasdt0(sdtasdt0(smndt0(sz10), sz00), xx), smndt0(sdtasdt0(sz00, xx))), sdtasdt0(smndt0(sz10), sdtasdt0(sz00, xx))), sdtasdt0(smndt0(sz10), sdtasdt0(sz00, xx)))), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by lemma 15 R->L }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(aElement0(sdtasdt0(sz00, xx)), true, sdtpldt0(sdtasdt0(sz00, xx), ifeq2(aElement0(xx), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(smndt0(sz10)), true, sdtasdt0(sdtasdt0(smndt0(sz10), sz00), xx), sdtasdt0(smndt0(sz10), sdtasdt0(sz00, xx))), sdtasdt0(smndt0(sz10), sdtasdt0(sz00, xx))), sdtasdt0(smndt0(sz10), sdtasdt0(sz00, xx)))), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 13 (mMulAsso) }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(aElement0(sdtasdt0(sz00, xx)), true, sdtpldt0(sdtasdt0(sz00, xx), sdtasdt0(smndt0(sz10), sdtasdt0(sz00, xx))), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by lemma 15 }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, ifeq2(aElement0(sdtasdt0(sz00, xx)), true, sdtpldt0(sdtasdt0(sz00, xx), smndt0(sdtasdt0(sz00, xx))), sz00), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 9 (mAddInvr) }
% 0.83/0.54 ifeq2(aElement0(sz00), true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, sz00, sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 3 (mSortsC) }
% 0.83/0.54 ifeq2(true, true, ifeq2(aElement0(sz00), true, ifeq2(aElement0(xx), true, sz00, sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 3 (mSortsC) }
% 0.83/0.54 ifeq2(true, true, ifeq2(true, true, ifeq2(aElement0(xx), true, sz00, sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 5 (ifeq_axiom) }
% 0.83/0.54 ifeq2(true, true, ifeq2(aElement0(xx), true, sz00, sdtasdt0(sdtpldt0(sz00, sz00), xx)), sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.54 = { by axiom 5 (ifeq_axiom) }
% 0.83/0.55 ifeq2(aElement0(xx), true, sz00, sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.55 = { by axiom 1 (m__468) }
% 0.83/0.55 ifeq2(true, true, sz00, sdtasdt0(sdtpldt0(sz00, sz00), xx))
% 0.83/0.55 = { by axiom 5 (ifeq_axiom) }
% 0.83/0.55 sz00
% 0.83/0.55
% 0.83/0.55 Goal 1 (m__): tuple(sz00, sdtasdt0(xx, sz00)) = tuple(sdtasdt0(sz00, xx), sz00).
% 0.83/0.55 Proof:
% 0.83/0.55 tuple(sz00, sdtasdt0(xx, sz00))
% 0.83/0.55 = { by axiom 12 (mMulComm) R->L }
% 0.83/0.55 tuple(sz00, ifeq2(aElement0(xx), true, ifeq2(aElement0(sz00), true, sdtasdt0(sz00, xx), sdtasdt0(xx, sz00)), sdtasdt0(xx, sz00)))
% 0.83/0.55 = { by lemma 16 }
% 0.83/0.55 tuple(sz00, ifeq2(aElement0(xx), true, ifeq2(aElement0(sz00), true, sz00, sdtasdt0(xx, sz00)), sdtasdt0(xx, sz00)))
% 0.83/0.55 = { by axiom 1 (m__468) }
% 0.83/0.55 tuple(sz00, ifeq2(true, true, ifeq2(aElement0(sz00), true, sz00, sdtasdt0(xx, sz00)), sdtasdt0(xx, sz00)))
% 0.83/0.55 = { by axiom 5 (ifeq_axiom) }
% 0.83/0.55 tuple(sz00, ifeq2(aElement0(sz00), true, sz00, sdtasdt0(xx, sz00)))
% 0.83/0.55 = { by axiom 3 (mSortsC) }
% 0.83/0.55 tuple(sz00, ifeq2(true, true, sz00, sdtasdt0(xx, sz00)))
% 0.83/0.55 = { by axiom 5 (ifeq_axiom) }
% 0.83/0.55 tuple(sz00, sz00)
% 0.83/0.55 = { by lemma 16 R->L }
% 0.83/0.55 tuple(sdtasdt0(sz00, xx), sz00)
% 0.83/0.55 % SZS output end Proof
% 0.83/0.55
% 0.83/0.55 RESULT: Theorem (the conjecture is true).
%------------------------------------------------------------------------------