%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : RNG077+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n032.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Mon Jul 18 20:33:46 EDT 2022
% Result : Theorem 238.52s 230.88s
% Output : Proof 238.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.08 % Problem : RNG077+1 : TPTP v8.1.0. Released v4.0.0.
% 0.04/0.08 % Command : leancop_casc.sh %s %d
% 0.07/0.26 % Computer : n032.cluster.edu
% 0.07/0.26 % Model : x86_64 x86_64
% 0.07/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.26 % Memory : 8042.1875MB
% 0.07/0.26 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.26 % CPULimit : 300
% 0.07/0.26 % WCLimit : 600
% 0.07/0.26 % DateTime : Mon May 30 22:17:28 EDT 2022
% 0.07/0.26 % CPUTime :
% 238.52/230.88 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 238.52/230.89 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 238.52/230.89
% 238.52/230.89 %-----------------------------------------------------
% 238.52/230.89 fof(mArith, axiom, ! [_119540, _119543, _119546] : (aScalar0(_119540) & aScalar0(_119543) & aScalar0(_119546) => sdtpldt0(sdtpldt0(_119540, _119543), _119546) = sdtpldt0(_119540, sdtpldt0(_119543, _119546)) & sdtpldt0(_119540, _119543) = sdtpldt0(_119543, _119540) & sdtasdt0(sdtasdt0(_119540, _119543), _119546) = sdtasdt0(_119540, sdtasdt0(_119543, _119546)) & sdtasdt0(_119540, _119543) = sdtasdt0(_119543, _119540)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mArith)).
% 238.52/230.89 fof(mZeroNat, axiom, aNaturalNumber0(sz00), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mZeroNat)).
% 238.52/230.89 fof(mElmSc, axiom, ! [_120046, _120049] : (aVector0(_120046) & aNaturalNumber0(_120049) => aScalar0(sdtlbdtrb0(_120046, _120049))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mElmSc)).
% 238.52/230.89 fof(mSZeroSc, axiom, aScalar0(sz0z00), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mSZeroSc)).
% 238.52/230.89 fof(m__, conjecture, sdtpldt0(sdtpldt0(xP, xP), sdtasdt0(xH, xH)) = sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__)).
% 238.52/230.89 fof(mMulSc, axiom, ! [_120393, _120396] : (aScalar0(_120393) & aScalar0(_120396) => aScalar0(sdtasdt0(_120393, _120396))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mMulSc)).
% 238.52/230.89 fof(m__1873, hypothesis, aScalar0(xH) & xH = sdtasdt0(xA, xB), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__1873)).
% 238.52/230.89 fof(m__1911, hypothesis, aScalar0(xP) & xP = sdtasdt0(xE, xH), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__1911)).
% 238.52/230.89 fof(m__1678, hypothesis, aVector0(xs) & aVector0(xt), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__1678)).
% 238.52/230.89 fof(m__1820, hypothesis, aScalar0(xE) & xE = sdtasasdt0(xp, xq), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__1820)).
% 238.52/230.89
% 238.52/230.89 cnf(1, plain, [-(sdtasdt0(_39228, _39341) = sdtasdt0(_39341, _39228)), aScalar0(_39228), aScalar0(_39341), aScalar0(_39453)], clausify(mArith)).
% 238.52/230.89 cnf(2, plain, [-(aNaturalNumber0(sz00))], clausify(mZeroNat)).
% 238.52/230.89 cnf(3, plain, [-(aScalar0(sdtlbdtrb0(_50259, _50310))), aVector0(_50259), aNaturalNumber0(_50310)], clausify(mElmSc)).
% 238.52/230.89 cnf(4, plain, [-(aScalar0(sz0z00))], clausify(mSZeroSc)).
% 238.52/230.89 cnf(5, plain, [sdtpldt0(sdtpldt0(xP, xP), sdtasdt0(xH, xH)) = sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH)))], clausify(m__)).
% 238.52/230.89 cnf(6, plain, [-(aScalar0(sdtasdt0(_37513, _37564))), aScalar0(_37513), aScalar0(_37564)], clausify(mMulSc)).
% 238.52/230.89 cnf(7, plain, [-(aScalar0(xH))], clausify(m__1873)).
% 238.52/230.89 cnf(8, plain, [-(_27778 = _27889), _27778 = _27834, _27834 = _27889], theory(equality)).
% 238.52/230.89 cnf(9, plain, [-(sdtpldt0(sdtpldt0(_39228, _39341), _39453) = sdtpldt0(_39228, sdtpldt0(_39341, _39453))), aScalar0(_39228), aScalar0(_39341), aScalar0(_39453)], clausify(mArith)).
% 238.52/230.89 cnf(10, plain, [-(aScalar0(xP))], clausify(m__1911)).
% 238.52/230.89 cnf(11, plain, [-(aVector0(xs))], clausify(m__1678)).
% 238.52/230.89 cnf(12, plain, [-(xP = sdtasdt0(xE, xH))], clausify(m__1911)).
% 238.52/230.89 cnf(13, plain, [-(sdtpldt0(_32755, _32888) = sdtpldt0(_32822, _32953)), _32755 = _32822, _32888 = _32953], theory(equality)).
% 238.52/230.89 cnf(14, plain, [-(_27346 = _27346)], theory(equality)).
% 238.52/230.89 cnf(15, plain, [-(aScalar0(xE))], clausify(m__1820)).
% 238.52/230.89
% 238.52/230.89 cnf('1',plain,[sdtpldt0(sdtpldt0(xP, xP), sdtasdt0(xH, xH)) = sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH)))],start(5)).
% 238.52/230.89 cnf('1.1',plain,[-(sdtpldt0(sdtpldt0(xP, xP), sdtasdt0(xH, xH)) = sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH)))), sdtpldt0(sdtpldt0(xP, xP), sdtasdt0(xH, xH)) = sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH))), sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH))) = sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH)))],extension(8,bind([[_27778, _27834, _27889], [sdtpldt0(sdtpldt0(xP, xP), sdtasdt0(xH, xH)), sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH))), sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH)))]]))).
% 238.52/230.89 cnf('1.1.1',plain,[-(sdtpldt0(sdtpldt0(xP, xP), sdtasdt0(xH, xH)) = sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH)))), sdtpldt0(sdtpldt0(xP, xP), sdtasdt0(xH, xH)) = sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH))), sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH))) = sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH)))],extension(8,bind([[_27778, _27834, _27889], [sdtpldt0(sdtpldt0(xP, xP), sdtasdt0(xH, xH)), sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH))), sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH)))]]))).
% 238.52/230.89 cnf('1.1.1.1',plain,[-(sdtpldt0(sdtpldt0(xP, xP), sdtasdt0(xH, xH)) = sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH)))), sdtpldt0(sdtpldt0(xP, xP), sdtasdt0(xH, xH)) = sdtpldt0(xP, sdtpldt0(xP, sdtasdt0(xH, xH))), sdtpldt0(xP, sdtpldt0(xP, sdtasdt0(xH, xH))) = sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH)))],extension(8,bind([[_27778, _27834, _27889], [sdtpldt0(sdtpldt0(xP, xP), sdtasdt0(xH, xH)), sdtpldt0(xP, sdtpldt0(xP, sdtasdt0(xH, xH))), sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH)))]]))).
% 238.52/230.89 cnf('1.1.1.1.1',plain,[-(sdtpldt0(sdtpldt0(xP, xP), sdtasdt0(xH, xH)) = sdtpldt0(xP, sdtpldt0(xP, sdtasdt0(xH, xH)))), aScalar0(xP), aScalar0(xP), aScalar0(sdtasdt0(xH, xH))],extension(9,bind([[_39228, _39341, _39453], [xP, xP, sdtasdt0(xH, xH)]]))).
% 238.52/230.89 cnf('1.1.1.1.1.1',plain,[-(aScalar0(xP))],extension(10)).
% 238.52/230.89 cnf('1.1.1.1.1.2',plain,[-(aScalar0(xP))],extension(10)).
% 238.52/230.89 cnf('1.1.1.1.1.3',plain,[-(aScalar0(sdtasdt0(xH, xH))), aScalar0(xH), aScalar0(xH)],extension(6,bind([[_37513, _37564], [xH, xH]]))).
% 238.52/230.89 cnf('1.1.1.1.1.3.1',plain,[-(aScalar0(xH))],extension(7)).
% 238.52/230.89 cnf('1.1.1.1.1.3.2',plain,[-(aScalar0(xH))],extension(7)).
% 238.52/230.89 cnf('1.1.1.1.2',plain,[-(sdtpldt0(xP, sdtpldt0(xP, sdtasdt0(xH, xH))) = sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH)))), xP = sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH)) = sdtpldt0(xP, sdtasdt0(xH, xH))],extension(13,bind([[_32755, _32822, _32888, _32953], [xP, sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH)), sdtpldt0(xP, sdtasdt0(xH, xH))]]))).
% 238.52/230.89 cnf('1.1.1.1.2.1',plain,[-(xP = sdtasdt0(xE, xH))],extension(12)).
% 238.52/230.89 cnf('1.1.1.1.2.2',plain,[-(sdtpldt0(xP, sdtasdt0(xH, xH)) = sdtpldt0(xP, sdtasdt0(xH, xH)))],extension(14,bind([[_27346], [sdtpldt0(xP, sdtasdt0(xH, xH))]]))).
% 238.52/230.89 cnf('1.1.1.2',plain,[-(sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH))) = sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH)))), sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH))) = sdtpldt0(sdtasdt0(xH, xE), sdtpldt0(xP, sdtasdt0(xH, xH))), sdtpldt0(sdtasdt0(xH, xE), sdtpldt0(xP, sdtasdt0(xH, xH))) = sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH)))],extension(8,bind([[_27778, _27834, _27889], [sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH))), sdtpldt0(sdtasdt0(xH, xE), sdtpldt0(xP, sdtasdt0(xH, xH))), sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH)))]]))).
% 238.52/230.89 cnf('1.1.1.2.1',plain,[-(sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH))) = sdtpldt0(sdtasdt0(xH, xE), sdtpldt0(xP, sdtasdt0(xH, xH)))), sdtasdt0(xE, xH) = sdtasdt0(xH, xE), sdtpldt0(xP, sdtasdt0(xH, xH)) = sdtpldt0(xP, sdtasdt0(xH, xH))],extension(13,bind([[_32755, _32822, _32888, _32953], [sdtasdt0(xE, xH), sdtasdt0(xH, xE), sdtpldt0(xP, sdtasdt0(xH, xH)), sdtpldt0(xP, sdtasdt0(xH, xH))]]))).
% 238.52/230.89 cnf('1.1.1.2.1.1',plain,[-(sdtasdt0(xE, xH) = sdtasdt0(xH, xE)), aScalar0(xE), aScalar0(xH), aScalar0(sz0z00)],extension(1,bind([[_39228, _39341, _39453], [xE, xH, sz0z00]]))).
% 238.52/230.89 cnf('1.1.1.2.1.1.1',plain,[-(aScalar0(xE))],extension(15)).
% 238.52/230.89 cnf('1.1.1.2.1.1.2',plain,[-(aScalar0(xH))],extension(7)).
% 238.52/230.89 cnf('1.1.1.2.1.1.3',plain,[-(aScalar0(sz0z00))],extension(4)).
% 238.52/230.89 cnf('1.1.1.2.1.2',plain,[-(sdtpldt0(xP, sdtasdt0(xH, xH)) = sdtpldt0(xP, sdtasdt0(xH, xH)))],extension(14,bind([[_27346], [sdtpldt0(xP, sdtasdt0(xH, xH))]]))).
% 238.52/230.89 cnf('1.1.1.2.2',plain,[-(sdtpldt0(sdtasdt0(xH, xE), sdtpldt0(xP, sdtasdt0(xH, xH))) = sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH)))), sdtasdt0(xH, xE) = sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH)) = sdtpldt0(xP, sdtasdt0(xH, xH))],extension(13,bind([[_32755, _32822, _32888, _32953], [sdtasdt0(xH, xE), sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH)), sdtpldt0(xP, sdtasdt0(xH, xH))]]))).
% 238.52/230.89 cnf('1.1.1.2.2.1',plain,[-(sdtasdt0(xH, xE) = sdtasdt0(xE, xH)), aScalar0(xH), aScalar0(xE), aScalar0(sz0z00)],extension(1,bind([[_39228, _39341, _39453], [xH, xE, sz0z00]]))).
% 238.52/230.89 cnf('1.1.1.2.2.1.1',plain,[-(aScalar0(xH))],extension(7)).
% 238.52/230.89 cnf('1.1.1.2.2.1.2',plain,[-(aScalar0(xE))],extension(15)).
% 238.52/230.89 cnf('1.1.1.2.2.1.3',plain,[-(aScalar0(sz0z00))],extension(4)).
% 238.52/230.89 cnf('1.1.1.2.2.2',plain,[-(sdtpldt0(xP, sdtasdt0(xH, xH)) = sdtpldt0(xP, sdtasdt0(xH, xH)))],extension(14,bind([[_27346], [sdtpldt0(xP, sdtasdt0(xH, xH))]]))).
% 238.52/230.89 cnf('1.1.2',plain,[-(sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH))) = sdtpldt0(sdtasdt0(xE, xH), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH)))), sdtasdt0(xE, xH) = sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH)) = sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH))],extension(13,bind([[_32755, _32822, _32888, _32953], [sdtasdt0(xE, xH), sdtasdt0(xE, xH), sdtpldt0(xP, sdtasdt0(xH, xH)), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH))]]))).
% 238.52/230.89 cnf('1.1.2.1',plain,[-(sdtasdt0(xE, xH) = sdtasdt0(xE, xH)), sdtasdt0(xE, xH) = sdtasdt0(xH, xE), sdtasdt0(xH, xE) = sdtasdt0(xE, xH)],extension(8,bind([[_27778, _27834, _27889], [sdtasdt0(xE, xH), sdtasdt0(xH, xE), sdtasdt0(xE, xH)]]))).
% 238.52/230.89 cnf('1.1.2.1.1',plain,[-(sdtasdt0(xE, xH) = sdtasdt0(xH, xE)), aScalar0(xE), aScalar0(xH), aScalar0(sdtlbdtrb0(xs, sz00))],extension(1,bind([[_39228, _39341, _39453], [xE, xH, sdtlbdtrb0(xs, sz00)]]))).
% 238.52/230.89 cnf('1.1.2.1.1.1',plain,[-(aScalar0(xE))],extension(15)).
% 238.52/230.89 cnf('1.1.2.1.1.2',plain,[-(aScalar0(xH))],extension(7)).
% 238.52/230.89 cnf('1.1.2.1.1.3',plain,[-(aScalar0(sdtlbdtrb0(xs, sz00))), aVector0(xs), aNaturalNumber0(sz00)],extension(3,bind([[_50259, _50310], [xs, sz00]]))).
% 238.52/230.89 cnf('1.1.2.1.1.3.1',plain,[-(aVector0(xs))],extension(11)).
% 238.52/230.89 cnf('1.1.2.1.1.3.2',plain,[-(aNaturalNumber0(sz00))],extension(2)).
% 238.52/230.89 cnf('1.1.2.1.2',plain,[-(sdtasdt0(xH, xE) = sdtasdt0(xE, xH)), aScalar0(xH), aScalar0(xE), aScalar0(sdtlbdtrb0(xs, sz00))],extension(1,bind([[_39228, _39341, _39453], [xH, xE, sdtlbdtrb0(xs, sz00)]]))).
% 238.52/230.89 cnf('1.1.2.1.2.1',plain,[-(aScalar0(xH))],extension(7)).
% 238.52/230.89 cnf('1.1.2.1.2.2',plain,[-(aScalar0(xE))],extension(15)).
% 238.52/230.89 cnf('1.1.2.1.2.3',plain,[-(aScalar0(sdtlbdtrb0(xs, sz00))), aVector0(xs), aNaturalNumber0(sz00)],extension(3,bind([[_50259, _50310], [xs, sz00]]))).
% 238.52/230.89 cnf('1.1.2.1.2.3.1',plain,[-(aVector0(xs))],extension(11)).
% 238.52/230.89 cnf('1.1.2.1.2.3.2',plain,[-(aNaturalNumber0(sz00))],extension(2)).
% 238.52/230.89 cnf('1.1.2.2',plain,[-(sdtpldt0(xP, sdtasdt0(xH, xH)) = sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH))), sdtpldt0(xP, sdtasdt0(xH, xH)) = sdtpldt0(sdtasdt0(xE, xH), sdtasdt0(xH, xH)), sdtpldt0(sdtasdt0(xE, xH), sdtasdt0(xH, xH)) = sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH))],extension(8,bind([[_27778, _27834, _27889], [sdtpldt0(xP, sdtasdt0(xH, xH)), sdtpldt0(sdtasdt0(xE, xH), sdtasdt0(xH, xH)), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH))]]))).
% 238.52/230.89 cnf('1.1.2.2.1',plain,[-(sdtpldt0(xP, sdtasdt0(xH, xH)) = sdtpldt0(sdtasdt0(xE, xH), sdtasdt0(xH, xH))), xP = sdtasdt0(xE, xH), sdtasdt0(xH, xH) = sdtasdt0(xH, xH)],extension(13,bind([[_32755, _32822, _32888, _32953], [xP, sdtasdt0(xE, xH), sdtasdt0(xH, xH), sdtasdt0(xH, xH)]]))).
% 238.52/230.89 cnf('1.1.2.2.1.1',plain,[-(xP = sdtasdt0(xE, xH))],extension(12)).
% 238.52/230.89 cnf('1.1.2.2.1.2',plain,[-(sdtasdt0(xH, xH) = sdtasdt0(xH, xH)), aScalar0(xH), aScalar0(xH), aScalar0(sz0z00)],extension(1,bind([[_39228, _39341, _39453], [xH, xH, sz0z00]]))).
% 238.52/230.89 cnf('1.1.2.2.1.2.1',plain,[-(aScalar0(xH))],extension(7)).
% 238.52/230.89 cnf('1.1.2.2.1.2.2',plain,[-(aScalar0(xH))],extension(7)).
% 238.52/230.89 cnf('1.1.2.2.1.2.3',plain,[-(aScalar0(sz0z00))],extension(4)).
% 238.52/230.89 cnf('1.1.2.2.2',plain,[-(sdtpldt0(sdtasdt0(xE, xH), sdtasdt0(xH, xH)) = sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH))), sdtasdt0(xE, xH) = sdtasdt0(xH, xE), sdtasdt0(xH, xH) = sdtasdt0(xH, xH)],extension(13,bind([[_32755, _32822, _32888, _32953], [sdtasdt0(xE, xH), sdtasdt0(xH, xE), sdtasdt0(xH, xH), sdtasdt0(xH, xH)]]))).
% 238.52/230.89 cnf('1.1.2.2.2.1',plain,[-(sdtasdt0(xE, xH) = sdtasdt0(xH, xE)), aScalar0(xE), aScalar0(xH), aScalar0(sz0z00)],extension(1,bind([[_39228, _39341, _39453], [xE, xH, sz0z00]]))).
% 238.52/230.89 cnf('1.1.2.2.2.1.1',plain,[-(aScalar0(xE))],extension(15)).
% 238.52/230.89 cnf('1.1.2.2.2.1.2',plain,[-(aScalar0(xH))],extension(7)).
% 238.52/230.89 cnf('1.1.2.2.2.1.3',plain,[-(aScalar0(sz0z00))],extension(4)).
% 238.52/230.89 cnf('1.1.2.2.2.2',plain,[-(sdtasdt0(xH, xH) = sdtasdt0(xH, xH)), aScalar0(xH), aScalar0(xH), aScalar0(sz0z00)],extension(1,bind([[_39228, _39341, _39453], [xH, xH, sz0z00]]))).
% 238.52/230.89 cnf('1.1.2.2.2.2.1',plain,[-(aScalar0(xH))],extension(7)).
% 238.52/230.89 cnf('1.1.2.2.2.2.2',plain,[-(aScalar0(xH))],extension(7)).
% 238.52/230.89 cnf('1.1.2.2.2.2.3',plain,[-(aScalar0(sz0z00))],extension(4)).
% 238.52/230.89 %-----------------------------------------------------
% 238.52/230.90
% 238.52/230.90 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------