%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : RNG061+2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n027.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.54s 4.53s
% Output : Proof 3.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : RNG061+2 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.13 % Command : leancop_casc.sh %s %d
% 0.14/0.34 % Computer : n027.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.35 % WCLimit : 600
% 0.14/0.35 % DateTime : Mon May 30 16:47:31 EDT 2022
% 0.14/0.35 % CPUTime :
% 3.54/4.53 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.54/4.54 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.56/4.54
% 3.56/4.54 %-----------------------------------------------------
% 3.56/4.54 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/sandbox/benchmark/theBenchmark.p', m__)).
% 3.56/4.54 fof(mZeroNat, axiom, aNaturalNumber0(sz00), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mZeroNat)).
% 3.56/4.54 fof(mSuccNat, axiom, ! [_88749] : (aNaturalNumber0(_88749) => aNaturalNumber0(szszuzczcdt0(_88749)) & (! szszuzczcdt0(_88749)) = sz00), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mSuccNat)).
% 3.56/4.54 fof(mNatExtr, axiom, ! [_88931] : (aNaturalNumber0(_88931) & (! _88931) = sz00 => ? [_88954] : (aNaturalNumber0(_88954) & _88931 = szszuzczcdt0(_88954))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mNatExtr)).
% 3.56/4.54 fof(mMulSc, axiom, ! [_89151, _89154] : (aScalar0(_89151) & aScalar0(_89154) => aScalar0(sdtasdt0(_89151, _89154))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mMulSc)).
% 3.56/4.54 fof(mNegSc, axiom, ! [_89320] : (aScalar0(_89320) => aScalar0(smndt0(_89320))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mNegSc)).
% 3.56/4.54 fof(mArith, axiom, ! [_89459, _89462, _89465] : (aScalar0(_89459) & aScalar0(_89462) & aScalar0(_89465) => sdtpldt0(sdtpldt0(_89459, _89462), _89465) = sdtpldt0(_89459, sdtpldt0(_89462, _89465)) & sdtpldt0(_89459, _89462) = sdtpldt0(_89462, _89459) & sdtasdt0(sdtasdt0(_89459, _89462), _89465) = sdtasdt0(_89459, sdtasdt0(_89462, _89465)) & sdtasdt0(_89459, _89462) = sdtasdt0(_89462, _89459)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mArith)).
% 3.56/4.54 fof(mElmSc, axiom, ! [_89930, _89933] : (aVector0(_89930) & aNaturalNumber0(_89933) => aScalar0(sdtlbdtrb0(_89930, _89933))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mElmSc)).
% 3.56/4.54 fof(mDefInit, definition, ! [_90099] : (aVector0(_90099) => (! aDimensionOf0(_90099)) = sz00 => ! [_90126] : (_90126 = sziznziztdt0(_90099) <=> aVector0(_90126) & szszuzczcdt0(aDimensionOf0(_90126)) = aDimensionOf0(_90099) & ! [_90169] : (aNaturalNumber0(_90169) => sdtlbdtrb0(_90126, _90169) = sdtlbdtrb0(_90099, _90169)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mDefInit)).
% 3.56/4.54 fof(m__1678, hypothesis, aVector0(xs) & aVector0(xt), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__1678)).
% 3.56/4.54 fof(m__1692, hypothesis, (! aDimensionOf0(xs)) = sz00, file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__1692)).
% 3.56/4.54 fof(m__1930, hypothesis, aScalar0(xS) & xS = sdtasdt0(xF, xD), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__1930)).
% 3.56/4.54 fof(m__1949, hypothesis, aScalar0(xN) & xN = sdtasdt0(xR, xS), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__1949)).
% 3.56/4.54 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/sandbox/benchmark/theBenchmark.p', m__2180)).
% 3.56/4.54
% 3.56/4.54 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.56/4.54 cnf(2, plain, [-(sdtpldt0(_34302, _34435) = sdtpldt0(_34369, _34500)), _34302 = _34369, _34435 = _34500], theory(equality)).
% 3.56/4.54 cnf(3, plain, [_35255 = _35304, -(sziznziztdt0(_35255) = sziznziztdt0(_35304))], theory(equality)).
% 3.56/4.54 cnf(4, plain, [-(_28893 = _28893)], theory(equality)).
% 3.56/4.54 cnf(5, plain, [_29046 = _29091, -(_29091 = _29046)], theory(equality)).
% 3.56/4.54 cnf(6, plain, [-(_29325 = _29436), _29325 = _29381, _29381 = _29436], theory(equality)).
% 3.56/4.54 cnf(7, plain, [-(aNaturalNumber0(sz00))], clausify(mZeroNat)).
% 3.56/4.54 cnf(8, plain, [aNaturalNumber0(_36385), -(aNaturalNumber0(szszuzczcdt0(_36385)))], clausify(mSuccNat)).
% 3.56/4.54 cnf(9, plain, [aNaturalNumber0(_36385), szszuzczcdt0(_36385) = sz00], clausify(mSuccNat)).
% 3.56/4.54 cnf(10, plain, [-(aNaturalNumber0(1 ^ [_36729])), aNaturalNumber0(_36729), -(_36729 = sz00)], clausify(mNatExtr)).
% 3.56/4.54 cnf(11, plain, [-(aScalar0(sdtasdt0(_39060, _39111))), aScalar0(_39060), aScalar0(_39111)], clausify(mMulSc)).
% 3.56/4.54 cnf(12, plain, [aScalar0(_39430), -(aScalar0(smndt0(_39430)))], clausify(mNegSc)).
% 3.56/4.54 cnf(13, plain, [-(sdtpldt0(_40775, _40888) = sdtpldt0(_40888, _40775)), aScalar0(_40775), aScalar0(_40888), aScalar0(_41000)], clausify(mArith)).
% 3.56/4.54 cnf(14, plain, [-(aScalar0(sdtlbdtrb0(_51806, _51857))), aVector0(_51806), aNaturalNumber0(_51857)], clausify(mElmSc)).
% 3.56/4.54 cnf(15, plain, [aVector0(_52176), -(aDimensionOf0(_52176) = sz00), _52400 = sziznziztdt0(_52176), -(aVector0(_52400))], clausify(mDefInit)).
% 3.56/4.54 cnf(16, plain, [-(aVector0(xs))], clausify(m__1678)).
% 3.56/4.54 cnf(17, plain, [aDimensionOf0(xs) = sz00], clausify(m__1692)).
% 3.56/4.54 cnf(18, plain, [-(aScalar0(xS))], clausify(m__1930)).
% 3.56/4.54 cnf(19, plain, [-(aScalar0(xN))], clausify(m__1949)).
% 3.56/4.54 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.56/4.54
% 3.56/4.54 cnf('1',plain,[aNaturalNumber0(sz00), szszuzczcdt0(sz00) = sz00],start(9,bind([[_36385], [sz00]]))).
% 3.56/4.54 cnf('1.1',plain,[-(aNaturalNumber0(sz00))],extension(7)).
% 3.56/4.54 cnf('1.2',plain,[-(szszuzczcdt0(sz00) = sz00), -(aNaturalNumber0(1 ^ [szszuzczcdt0(sz00)])), aNaturalNumber0(szszuzczcdt0(sz00))],extension(10,bind([[_36729], [szszuzczcdt0(sz00)]]))).
% 3.56/4.54 cnf('1.2.1',plain,[aNaturalNumber0(1 ^ [szszuzczcdt0(sz00)]), -(aScalar0(sdtlbdtrb0(sziznziztdt0(xs), 1 ^ [szszuzczcdt0(sz00)]))), aVector0(sziznziztdt0(xs))],extension(14,bind([[_51857, _51806], [1 ^ [szszuzczcdt0(sz00)], sziznziztdt0(xs)]]))).
% 3.56/4.54 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([[_41000, _40775, _40888], [sdtlbdtrb0(sziznziztdt0(xs), 1 ^ [szszuzczcdt0(sz00)]), smndt0(xN), sdtasdt0(xS, xS)]]))).
% 3.56/4.54 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([[_34435, _34500, _34302, _34369], [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.56/4.54 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([[_29436, _29325, _29381], [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.56/4.54 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.56/4.54 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.56/4.54 cnf('1.2.1.1.1.2',plain,[-(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)) = sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)))],extension(4,bind([[_28893], [sdtpldt0(sdtasdt0(xR, xR), smndt0(xN))]]))).
% 3.56/4.54 cnf('1.2.1.1.2',plain,[-(aScalar0(smndt0(xN))), aScalar0(xN)],extension(12,bind([[_39430], [xN]]))).
% 3.56/4.54 cnf('1.2.1.1.2.1',plain,[-(aScalar0(xN))],extension(19)).
% 3.56/4.54 cnf('1.2.1.1.3',plain,[-(aScalar0(sdtasdt0(xS, xS))), aScalar0(xS), aScalar0(xS)],extension(11,bind([[_39060, _39111], [xS, xS]]))).
% 3.56/4.54 cnf('1.2.1.1.3.1',plain,[-(aScalar0(xS))],extension(18)).
% 3.56/4.54 cnf('1.2.1.1.3.2',plain,[-(aScalar0(xS))],extension(18)).
% 3.56/4.54 cnf('1.2.1.2',plain,[-(aVector0(sziznziztdt0(xs))), aVector0(xs), -(aDimensionOf0(xs) = sz00), sziznziztdt0(xs) = sziznziztdt0(xs)],extension(15,bind([[_52400, _52176], [sziznziztdt0(xs), xs]]))).
% 3.56/4.54 cnf('1.2.1.2.1',plain,[-(aVector0(xs))],extension(16)).
% 3.56/4.54 cnf('1.2.1.2.2',plain,[aDimensionOf0(xs) = sz00, -(aDimensionOf0(xs) = aDimensionOf0(xs)), sz00 = aDimensionOf0(xs)],extension(6,bind([[_29325, _29381, _29436], [aDimensionOf0(xs), sz00, aDimensionOf0(xs)]]))).
% 3.56/4.54 cnf('1.2.1.2.2.1',plain,[aDimensionOf0(xs) = aDimensionOf0(xs), -(aDimensionOf0(xs) = sz00), aDimensionOf0(xs) = sz00],extension(6,bind([[_29325, _29381, _29436], [aDimensionOf0(xs), aDimensionOf0(xs), sz00]]))).
% 3.56/4.54 cnf('1.2.1.2.2.1.1',plain,[aDimensionOf0(xs) = sz00],extension(17)).
% 3.56/4.54 cnf('1.2.1.2.2.1.2',plain,[-(aDimensionOf0(xs) = sz00)],reduction('1.2.1.2')).
% 3.56/4.54 cnf('1.2.1.2.2.2',plain,[-(sz00 = aDimensionOf0(xs)), aDimensionOf0(xs) = sz00],extension(5,bind([[_29046, _29091], [aDimensionOf0(xs), sz00]]))).
% 3.56/4.54 cnf('1.2.1.2.2.2.1',plain,[-(aDimensionOf0(xs) = sz00)],reduction('1.2.1.2')).
% 3.56/4.54 cnf('1.2.1.2.3',plain,[-(sziznziztdt0(xs) = sziznziztdt0(xs)), xs = xs],extension(3,bind([[_35255, _35304], [xs, xs]]))).
% 3.56/4.54 cnf('1.2.1.2.3.1',plain,[-(xs = xs)],extension(4,bind([[_28893], [xs]]))).
% 3.56/4.54 cnf('1.2.2',plain,[-(aNaturalNumber0(szszuzczcdt0(sz00))), aNaturalNumber0(sz00)],extension(8,bind([[_36385], [sz00]]))).
% 3.56/4.54 cnf('1.2.2.1',plain,[-(aNaturalNumber0(sz00))],extension(7)).
% 3.56/4.54 %-----------------------------------------------------
% 3.56/4.55
% 3.56/4.55 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------