%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : RNG061+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n028.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:43 EDT 2022
% Result : Theorem 3.18s 3.46s
% Output : Proof 3.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : RNG061+1 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.11/0.32 % Computer : n028.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 600
% 0.11/0.32 % DateTime : Mon May 30 11:01:04 EDT 2022
% 0.11/0.32 % CPUTime :
% 3.18/3.46 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.18/3.47 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.18/3.47
% 3.18/3.47 %-----------------------------------------------------
% 3.18/3.47 fof(m__, conjecture, sdtasdt0(sdtpldt0(xR, smndt0(xS)), sdtpldt0(xR, smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(sdtasdt0(xS, xS), smndt0(xN))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__)).
% 3.18/3.47 fof(mZeroNat, axiom, aNaturalNumber0(sz00), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mZeroNat)).
% 3.18/3.47 fof(mSuccNat, axiom, ! [_86599] : (aNaturalNumber0(_86599) => aNaturalNumber0(szszuzczcdt0(_86599)) & (! szszuzczcdt0(_86599)) = sz00), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mSuccNat)).
% 3.18/3.47 fof(mNatExtr, axiom, ! [_86781] : (aNaturalNumber0(_86781) & (! _86781) = sz00 => ? [_86804] : (aNaturalNumber0(_86804) & _86781 = szszuzczcdt0(_86804))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mNatExtr)).
% 3.18/3.47 fof(mMulSc, axiom, ! [_87001, _87004] : (aScalar0(_87001) & aScalar0(_87004) => aScalar0(sdtasdt0(_87001, _87004))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mMulSc)).
% 3.18/3.47 fof(mNegSc, axiom, ! [_87170] : (aScalar0(_87170) => aScalar0(smndt0(_87170))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mNegSc)).
% 3.18/3.47 fof(mArith, axiom, ! [_87309, _87312, _87315] : (aScalar0(_87309) & aScalar0(_87312) & aScalar0(_87315) => sdtpldt0(sdtpldt0(_87309, _87312), _87315) = sdtpldt0(_87309, sdtpldt0(_87312, _87315)) & sdtpldt0(_87309, _87312) = sdtpldt0(_87312, _87309) & sdtasdt0(sdtasdt0(_87309, _87312), _87315) = sdtasdt0(_87309, sdtasdt0(_87312, _87315)) & sdtasdt0(_87309, _87312) = sdtasdt0(_87312, _87309)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mArith)).
% 3.18/3.47 fof(mElmSc, axiom, ! [_87780, _87783] : (aVector0(_87780) & aNaturalNumber0(_87783) => aScalar0(sdtlbdtrb0(_87780, _87783))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mElmSc)).
% 3.18/3.47 fof(mDefInit, definition, ! [_87949] : (aVector0(_87949) => (! aDimensionOf0(_87949)) = sz00 => ! [_87976] : (_87976 = sziznziztdt0(_87949) <=> aVector0(_87976) & szszuzczcdt0(aDimensionOf0(_87976)) = aDimensionOf0(_87949) & ! [_88019] : (aNaturalNumber0(_88019) => sdtlbdtrb0(_87976, _88019) = sdtlbdtrb0(_87949, _88019)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mDefInit)).
% 3.18/3.47 fof(m__1678, hypothesis, aVector0(xs) & aVector0(xt), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__1678)).
% 3.18/3.47 fof(m__1692, hypothesis, (! aDimensionOf0(xs)) = sz00, file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__1692)).
% 3.18/3.47 fof(m__1930, hypothesis, aScalar0(xS) & xS = sdtasdt0(xF, xD), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__1930)).
% 3.18/3.47 fof(m__1949, hypothesis, aScalar0(xN) & xN = sdtasdt0(xR, xS), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__1949)).
% 3.18/3.47 fof(m__2180, hypothesis, sdtasdt0(sdtpldt0(xR, smndt0(xS)), sdtpldt0(xR, smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(smndt0(xN), sdtasdt0(xS, xS))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2180)).
% 3.18/3.47
% 3.18/3.47 cnf(1, plain, [sdtasdt0(sdtpldt0(xR, smndt0(xS)), sdtpldt0(xR, smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(sdtasdt0(xS, xS), smndt0(xN)))], clausify(m__)).
% 3.18/3.47 cnf(2, plain, [-(sdtpldt0(_33339, _33472) = sdtpldt0(_33406, _33537)), _33339 = _33406, _33472 = _33537], theory(equality)).
% 3.18/3.47 cnf(3, plain, [_34292 = _34341, -(sziznziztdt0(_34292) = sziznziztdt0(_34341))], theory(equality)).
% 3.18/3.47 cnf(4, plain, [-(_27930 = _27930)], theory(equality)).
% 3.18/3.47 cnf(5, plain, [_28083 = _28128, -(_28128 = _28083)], theory(equality)).
% 3.18/3.47 cnf(6, plain, [-(_28362 = _28473), _28362 = _28418, _28418 = _28473], theory(equality)).
% 3.18/3.47 cnf(7, plain, [-(aNaturalNumber0(sz00))], clausify(mZeroNat)).
% 3.18/3.47 cnf(8, plain, [aNaturalNumber0(_35422), -(aNaturalNumber0(szszuzczcdt0(_35422)))], clausify(mSuccNat)).
% 3.18/3.47 cnf(9, plain, [aNaturalNumber0(_35422), szszuzczcdt0(_35422) = sz00], clausify(mSuccNat)).
% 3.18/3.47 cnf(10, plain, [-(aNaturalNumber0(1 ^ [_35766])), aNaturalNumber0(_35766), -(_35766 = sz00)], clausify(mNatExtr)).
% 3.18/3.47 cnf(11, plain, [-(aScalar0(sdtasdt0(_38097, _38148))), aScalar0(_38097), aScalar0(_38148)], clausify(mMulSc)).
% 3.18/3.47 cnf(12, plain, [aScalar0(_38467), -(aScalar0(smndt0(_38467)))], clausify(mNegSc)).
% 3.18/3.47 cnf(13, plain, [-(sdtpldt0(_39812, _39925) = sdtpldt0(_39925, _39812)), aScalar0(_39812), aScalar0(_39925), aScalar0(_40037)], clausify(mArith)).
% 3.18/3.47 cnf(14, plain, [-(aScalar0(sdtlbdtrb0(_50843, _50894))), aVector0(_50843), aNaturalNumber0(_50894)], clausify(mElmSc)).
% 3.18/3.47 cnf(15, plain, [aVector0(_51213), -(aDimensionOf0(_51213) = sz00), _51437 = sziznziztdt0(_51213), -(aVector0(_51437))], clausify(mDefInit)).
% 3.18/3.47 cnf(16, plain, [-(aVector0(xs))], clausify(m__1678)).
% 3.18/3.47 cnf(17, plain, [aDimensionOf0(xs) = sz00], clausify(m__1692)).
% 3.18/3.47 cnf(18, plain, [-(aScalar0(xS))], clausify(m__1930)).
% 3.18/3.47 cnf(19, plain, [-(aScalar0(xN))], clausify(m__1949)).
% 3.18/3.47 cnf(20, plain, [-(sdtasdt0(sdtpldt0(xR, smndt0(xS)), sdtpldt0(xR, smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(smndt0(xN), sdtasdt0(xS, xS))))], clausify(m__2180)).
% 3.18/3.47
% 3.18/3.47 cnf('1',plain,[aNaturalNumber0(sz00), szszuzczcdt0(sz00) = sz00],start(9,bind([[_35422], [sz00]]))).
% 3.18/3.47 cnf('1.1',plain,[-(aNaturalNumber0(sz00))],extension(7)).
% 3.18/3.47 cnf('1.2',plain,[-(szszuzczcdt0(sz00) = sz00), -(aNaturalNumber0(1 ^ [szszuzczcdt0(sz00)])), aNaturalNumber0(szszuzczcdt0(sz00))],extension(10,bind([[_35766], [szszuzczcdt0(sz00)]]))).
% 3.18/3.47 cnf('1.2.1',plain,[aNaturalNumber0(1 ^ [szszuzczcdt0(sz00)]), -(aScalar0(sdtlbdtrb0(sziznziztdt0(xs), 1 ^ [szszuzczcdt0(sz00)]))), aVector0(sziznziztdt0(xs))],extension(14,bind([[_50894, _50843], [1 ^ [szszuzczcdt0(sz00)], sziznziztdt0(xs)]]))).
% 3.18/3.47 cnf('1.2.1.1',plain,[aScalar0(sdtlbdtrb0(sziznziztdt0(xs), 1 ^ [szszuzczcdt0(sz00)])), -(sdtpldt0(smndt0(xN), sdtasdt0(xS, xS)) = sdtpldt0(sdtasdt0(xS, xS), smndt0(xN))), aScalar0(smndt0(xN)), aScalar0(sdtasdt0(xS, xS))],extension(13,bind([[_40037, _39812, _39925], [sdtlbdtrb0(sziznziztdt0(xs), 1 ^ [szszuzczcdt0(sz00)]), smndt0(xN), sdtasdt0(xS, xS)]]))).
% 3.18/3.47 cnf('1.2.1.1.1',plain,[sdtpldt0(smndt0(xN), sdtasdt0(xS, xS)) = sdtpldt0(sdtasdt0(xS, xS), smndt0(xN)), -(sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(smndt0(xN), sdtasdt0(xS, xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(sdtasdt0(xS, xS), smndt0(xN)))), sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)) = sdtpldt0(sdtasdt0(xR, xR), smndt0(xN))],extension(2,bind([[_33472, _33537, _33339, _33406], [sdtpldt0(smndt0(xN), sdtasdt0(xS, xS)), sdtpldt0(sdtasdt0(xS, xS), smndt0(xN)), sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(sdtasdt0(xR, xR), smndt0(xN))]]))).
% 3.18/3.47 cnf('1.2.1.1.1.1',plain,[sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(smndt0(xN), sdtasdt0(xS, xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(sdtasdt0(xS, xS), smndt0(xN))), -(sdtasdt0(sdtpldt0(xR, smndt0(xS)), sdtpldt0(xR, smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(sdtasdt0(xS, xS), smndt0(xN)))), sdtasdt0(sdtpldt0(xR, smndt0(xS)), sdtpldt0(xR, smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(smndt0(xN), sdtasdt0(xS, xS)))],extension(6,bind([[_28473, _28362, _28418], [sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(sdtasdt0(xS, xS), smndt0(xN))), sdtasdt0(sdtpldt0(xR, smndt0(xS)), sdtpldt0(xR, smndt0(xS))), sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(smndt0(xN), sdtasdt0(xS, xS)))]]))).
% 3.18/3.47 cnf('1.2.1.1.1.1.1',plain,[sdtasdt0(sdtpldt0(xR, smndt0(xS)), sdtpldt0(xR, smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(sdtasdt0(xS, xS), smndt0(xN)))],extension(1)).
% 3.18/3.47 cnf('1.2.1.1.1.1.2',plain,[-(sdtasdt0(sdtpldt0(xR, smndt0(xS)), sdtpldt0(xR, smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(smndt0(xN), sdtasdt0(xS, xS))))],extension(20)).
% 3.18/3.47 cnf('1.2.1.1.1.2',plain,[-(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)) = sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)))],extension(4,bind([[_27930], [sdtpldt0(sdtasdt0(xR, xR), smndt0(xN))]]))).
% 3.18/3.47 cnf('1.2.1.1.2',plain,[-(aScalar0(smndt0(xN))), aScalar0(xN)],extension(12,bind([[_38467], [xN]]))).
% 3.18/3.47 cnf('1.2.1.1.2.1',plain,[-(aScalar0(xN))],extension(19)).
% 3.18/3.47 cnf('1.2.1.1.3',plain,[-(aScalar0(sdtasdt0(xS, xS))), aScalar0(xS), aScalar0(xS)],extension(11,bind([[_38097, _38148], [xS, xS]]))).
% 3.18/3.47 cnf('1.2.1.1.3.1',plain,[-(aScalar0(xS))],extension(18)).
% 3.18/3.47 cnf('1.2.1.1.3.2',plain,[-(aScalar0(xS))],extension(18)).
% 3.18/3.47 cnf('1.2.1.2',plain,[-(aVector0(sziznziztdt0(xs))), aVector0(xs), -(aDimensionOf0(xs) = sz00), sziznziztdt0(xs) = sziznziztdt0(xs)],extension(15,bind([[_51437, _51213], [sziznziztdt0(xs), xs]]))).
% 3.18/3.47 cnf('1.2.1.2.1',plain,[-(aVector0(xs))],extension(16)).
% 3.18/3.47 cnf('1.2.1.2.2',plain,[aDimensionOf0(xs) = sz00, -(aDimensionOf0(xs) = aDimensionOf0(xs)), sz00 = aDimensionOf0(xs)],extension(6,bind([[_28362, _28418, _28473], [aDimensionOf0(xs), sz00, aDimensionOf0(xs)]]))).
% 3.18/3.47 cnf('1.2.1.2.2.1',plain,[aDimensionOf0(xs) = aDimensionOf0(xs), -(aDimensionOf0(xs) = sz00), aDimensionOf0(xs) = sz00],extension(6,bind([[_28362, _28418, _28473], [aDimensionOf0(xs), aDimensionOf0(xs), sz00]]))).
% 3.18/3.47 cnf('1.2.1.2.2.1.1',plain,[aDimensionOf0(xs) = sz00],extension(17)).
% 3.18/3.47 cnf('1.2.1.2.2.1.2',plain,[-(aDimensionOf0(xs) = sz00)],reduction('1.2.1.2')).
% 3.18/3.47 cnf('1.2.1.2.2.2',plain,[-(sz00 = aDimensionOf0(xs)), aDimensionOf0(xs) = sz00],extension(5,bind([[_28083, _28128], [aDimensionOf0(xs), sz00]]))).
% 3.18/3.47 cnf('1.2.1.2.2.2.1',plain,[-(aDimensionOf0(xs) = sz00)],reduction('1.2.1.2')).
% 3.18/3.47 cnf('1.2.1.2.3',plain,[-(sziznziztdt0(xs) = sziznziztdt0(xs)), xs = xs],extension(3,bind([[_34292, _34341], [xs, xs]]))).
% 3.18/3.47 cnf('1.2.1.2.3.1',plain,[-(xs = xs)],extension(4,bind([[_27930], [xs]]))).
% 3.18/3.47 cnf('1.2.2',plain,[-(aNaturalNumber0(szszuzczcdt0(sz00))), aNaturalNumber0(sz00)],extension(8,bind([[_35422], [sz00]]))).
% 3.18/3.47 cnf('1.2.2.1',plain,[-(aNaturalNumber0(sz00))],extension(7)).
% 3.18/3.47 %-----------------------------------------------------
% 3.18/3.48
% 3.18/3.48 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------