%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : RNG079+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 116.19s 112.28s
% Output : Proof 116.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : RNG079+1 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.32 % Computer : n032.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 600
% 0.12/0.32 % DateTime : Mon May 30 11:50:12 EDT 2022
% 0.12/0.32 % CPUTime :
% 116.19/112.28 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 116.19/112.28 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 116.19/112.29
% 116.19/112.29 %-----------------------------------------------------
% 116.19/112.29 fof(m__, conjecture, sdtlseqdt0(sdtasdt0(sdtpldt0(xE, xH), sdtpldt0(xE, xH)), sdtasdt0(sdtpldt0(xC, xF), sdtpldt0(xD, xG))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__)).
% 116.19/112.29 fof(mDistr2, axiom, ! [_85329, _85332, _85335, _85338] : (aScalar0(_85329) & aScalar0(_85332) & aScalar0(_85335) & aScalar0(_85338) => sdtasdt0(sdtpldt0(_85329, _85332), sdtpldt0(_85335, _85338)) = sdtpldt0(sdtpldt0(sdtasdt0(_85329, _85335), sdtasdt0(_85329, _85338)), sdtpldt0(sdtasdt0(_85332, _85335), sdtasdt0(_85332, _85338)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mDistr2)).
% 116.19/112.29 fof(m__1783, hypothesis, aScalar0(xC) & xC = sdtasasdt0(xp, xp), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__1783)).
% 116.19/112.29 fof(m__1800, hypothesis, aScalar0(xD) & xD = sdtasasdt0(xq, xq), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__1800)).
% 116.19/112.29 fof(m__1820, hypothesis, aScalar0(xE) & xE = sdtasasdt0(xp, xq), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__1820)).
% 116.19/112.29 fof(m__1837, hypothesis, aScalar0(xF) & xF = sdtasdt0(xA, xA), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__1837)).
% 116.19/112.29 fof(m__1854, hypothesis, aScalar0(xG) & xG = sdtasdt0(xB, xB), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__1854)).
% 116.19/112.29 fof(m__1873, hypothesis, aScalar0(xH) & xH = sdtasdt0(xA, xB), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__1873)).
% 116.19/112.29 fof(m__2905, hypothesis, sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xE, xE), sdtasdt0(xE, xH)), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH))), sdtpldt0(sdtpldt0(sdtasdt0(xC, xD), sdtasdt0(xC, xG)), sdtpldt0(sdtasdt0(xF, xD), sdtasdt0(xF, xG)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__2905)).
% 116.19/112.29
% 116.19/112.29 cnf(1, plain, [sdtlseqdt0(sdtasdt0(sdtpldt0(xE, xH), sdtpldt0(xE, xH)), sdtasdt0(sdtpldt0(xC, xF), sdtpldt0(xD, xG)))], clausify(m__)).
% 116.19/112.29 cnf(2, plain, [-(_28118 = _28118)], theory(equality)).
% 116.19/112.29 cnf(3, plain, [_28271 = _28316, -(_28316 = _28271)], theory(equality)).
% 116.19/112.29 cnf(4, plain, [-(sdtlseqdt0(_30694, _30825)), sdtlseqdt0(_30627, _30760), _30627 = _30694, _30760 = _30825], theory(equality)).
% 116.19/112.29 cnf(5, plain, [-(sdtasdt0(sdtpldt0(_42354, _42453), sdtpldt0(_42551, _42648)) = sdtpldt0(sdtpldt0(sdtasdt0(_42354, _42551), sdtasdt0(_42354, _42648)), sdtpldt0(sdtasdt0(_42453, _42551), sdtasdt0(_42453, _42648)))), aScalar0(_42354), aScalar0(_42453), aScalar0(_42551), aScalar0(_42648)], clausify(mDistr2)).
% 116.19/112.29 cnf(6, plain, [-(aScalar0(xC))], clausify(m__1783)).
% 116.19/112.29 cnf(7, plain, [-(aScalar0(xD))], clausify(m__1800)).
% 116.19/112.29 cnf(8, plain, [-(aScalar0(xE))], clausify(m__1820)).
% 116.19/112.29 cnf(9, plain, [-(aScalar0(xF))], clausify(m__1837)).
% 116.19/112.29 cnf(10, plain, [-(aScalar0(xG))], clausify(m__1854)).
% 116.19/112.29 cnf(11, plain, [-(aScalar0(xH))], clausify(m__1873)).
% 116.19/112.29 cnf(12, plain, [-(sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xE, xE), sdtasdt0(xE, xH)), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH))), sdtpldt0(sdtpldt0(sdtasdt0(xC, xD), sdtasdt0(xC, xG)), sdtpldt0(sdtasdt0(xF, xD), sdtasdt0(xF, xG)))))], clausify(m__2905)).
% 116.19/112.29
% 116.19/112.29 cnf('1',plain,[sdtlseqdt0(sdtasdt0(sdtpldt0(xE, xH), sdtpldt0(xE, xH)), sdtasdt0(sdtpldt0(xC, xF), sdtpldt0(xD, xG)))],start(1)).
% 116.19/112.29 cnf('1.1',plain,[-(sdtlseqdt0(sdtasdt0(sdtpldt0(xE, xH), sdtpldt0(xE, xH)), sdtasdt0(sdtpldt0(xC, xF), sdtpldt0(xD, xG)))), sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xE, xE), sdtasdt0(xE, xH)), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH))), sdtpldt0(sdtpldt0(sdtasdt0(xC, xD), sdtasdt0(xC, xG)), sdtpldt0(sdtasdt0(xF, xD), sdtasdt0(xF, xG)))), sdtpldt0(sdtpldt0(sdtasdt0(xE, xE), sdtasdt0(xE, xH)), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH))) = sdtasdt0(sdtpldt0(xE, xH), sdtpldt0(xE, xH)), sdtpldt0(sdtpldt0(sdtasdt0(xC, xD), sdtasdt0(xC, xG)), sdtpldt0(sdtasdt0(xF, xD), sdtasdt0(xF, xG))) = sdtasdt0(sdtpldt0(xC, xF), sdtpldt0(xD, xG))],extension(4,bind([[_30627, _30694, _30760, _30825], [sdtpldt0(sdtpldt0(sdtasdt0(xE, xE), sdtasdt0(xE, xH)), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH))), sdtasdt0(sdtpldt0(xE, xH), sdtpldt0(xE, xH)), sdtpldt0(sdtpldt0(sdtasdt0(xC, xD), sdtasdt0(xC, xG)), sdtpldt0(sdtasdt0(xF, xD), sdtasdt0(xF, xG))), sdtasdt0(sdtpldt0(xC, xF), sdtpldt0(xD, xG))]]))).
% 116.19/112.29 cnf('1.1.1',plain,[-(sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xE, xE), sdtasdt0(xE, xH)), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH))), sdtpldt0(sdtpldt0(sdtasdt0(xC, xD), sdtasdt0(xC, xG)), sdtpldt0(sdtasdt0(xF, xD), sdtasdt0(xF, xG))))), sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xE, xE), sdtasdt0(xE, xH)), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH))), sdtpldt0(sdtpldt0(sdtasdt0(xC, xD), sdtasdt0(xC, xG)), sdtpldt0(sdtasdt0(xF, xD), sdtasdt0(xF, xG)))), sdtpldt0(sdtpldt0(sdtasdt0(xE, xE), sdtasdt0(xE, xH)), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH))) = sdtpldt0(sdtpldt0(sdtasdt0(xE, xE), sdtasdt0(xE, xH)), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH))), sdtpldt0(sdtpldt0(sdtasdt0(xC, xD), sdtasdt0(xC, xG)), sdtpldt0(sdtasdt0(xF, xD), sdtasdt0(xF, xG))) = sdtpldt0(sdtpldt0(sdtasdt0(xC, xD), sdtasdt0(xC, xG)), sdtpldt0(sdtasdt0(xF, xD), sdtasdt0(xF, xG)))],extension(4,bind([[_30627, _30694, _30760, _30825], [sdtpldt0(sdtpldt0(sdtasdt0(xE, xE), sdtasdt0(xE, xH)), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH))), sdtpldt0(sdtpldt0(sdtasdt0(xE, xE), sdtasdt0(xE, xH)), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH))), sdtpldt0(sdtpldt0(sdtasdt0(xC, xD), sdtasdt0(xC, xG)), sdtpldt0(sdtasdt0(xF, xD), sdtasdt0(xF, xG))), sdtpldt0(sdtpldt0(sdtasdt0(xC, xD), sdtasdt0(xC, xG)), sdtpldt0(sdtasdt0(xF, xD), sdtasdt0(xF, xG)))]]))).
% 116.19/112.29 cnf('1.1.1.1',plain,[-(sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xE, xE), sdtasdt0(xE, xH)), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH))), sdtpldt0(sdtpldt0(sdtasdt0(xC, xD), sdtasdt0(xC, xG)), sdtpldt0(sdtasdt0(xF, xD), sdtasdt0(xF, xG)))))],extension(12)).
% 116.19/112.29 cnf('1.1.1.2',plain,[-(sdtpldt0(sdtpldt0(sdtasdt0(xE, xE), sdtasdt0(xE, xH)), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH))) = sdtpldt0(sdtpldt0(sdtasdt0(xE, xE), sdtasdt0(xE, xH)), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH))))],extension(2,bind([[_28118], [sdtpldt0(sdtpldt0(sdtasdt0(xE, xE), sdtasdt0(xE, xH)), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH)))]]))).
% 116.19/112.29 cnf('1.1.1.3',plain,[-(sdtpldt0(sdtpldt0(sdtasdt0(xC, xD), sdtasdt0(xC, xG)), sdtpldt0(sdtasdt0(xF, xD), sdtasdt0(xF, xG))) = sdtpldt0(sdtpldt0(sdtasdt0(xC, xD), sdtasdt0(xC, xG)), sdtpldt0(sdtasdt0(xF, xD), sdtasdt0(xF, xG))))],extension(2,bind([[_28118], [sdtpldt0(sdtpldt0(sdtasdt0(xC, xD), sdtasdt0(xC, xG)), sdtpldt0(sdtasdt0(xF, xD), sdtasdt0(xF, xG)))]]))).
% 116.19/112.29 cnf('1.1.2',plain,[-(sdtpldt0(sdtpldt0(sdtasdt0(xE, xE), sdtasdt0(xE, xH)), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH))) = sdtasdt0(sdtpldt0(xE, xH), sdtpldt0(xE, xH))), sdtasdt0(sdtpldt0(xE, xH), sdtpldt0(xE, xH)) = sdtpldt0(sdtpldt0(sdtasdt0(xE, xE), sdtasdt0(xE, xH)), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH)))],extension(3,bind([[_28271, _28316], [sdtasdt0(sdtpldt0(xE, xH), sdtpldt0(xE, xH)), sdtpldt0(sdtpldt0(sdtasdt0(xE, xE), sdtasdt0(xE, xH)), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH)))]]))).
% 116.19/112.29 cnf('1.1.2.1',plain,[-(sdtasdt0(sdtpldt0(xE, xH), sdtpldt0(xE, xH)) = sdtpldt0(sdtpldt0(sdtasdt0(xE, xE), sdtasdt0(xE, xH)), sdtpldt0(sdtasdt0(xH, xE), sdtasdt0(xH, xH)))), aScalar0(xE), aScalar0(xH), aScalar0(xE), aScalar0(xH)],extension(5,bind([[_42354, _42453, _42551, _42648], [xE, xH, xE, xH]]))).
% 116.19/112.29 cnf('1.1.2.1.1',plain,[-(aScalar0(xE))],extension(8)).
% 116.19/112.29 cnf('1.1.2.1.2',plain,[-(aScalar0(xH))],extension(11)).
% 116.19/112.29 cnf('1.1.2.1.3',plain,[-(aScalar0(xE))],extension(8)).
% 116.19/112.29 cnf('1.1.2.1.4',plain,[-(aScalar0(xH))],extension(11)).
% 116.19/112.29 cnf('1.1.3',plain,[-(sdtpldt0(sdtpldt0(sdtasdt0(xC, xD), sdtasdt0(xC, xG)), sdtpldt0(sdtasdt0(xF, xD), sdtasdt0(xF, xG))) = sdtasdt0(sdtpldt0(xC, xF), sdtpldt0(xD, xG))), sdtasdt0(sdtpldt0(xC, xF), sdtpldt0(xD, xG)) = sdtpldt0(sdtpldt0(sdtasdt0(xC, xD), sdtasdt0(xC, xG)), sdtpldt0(sdtasdt0(xF, xD), sdtasdt0(xF, xG)))],extension(3,bind([[_28271, _28316], [sdtasdt0(sdtpldt0(xC, xF), sdtpldt0(xD, xG)), sdtpldt0(sdtpldt0(sdtasdt0(xC, xD), sdtasdt0(xC, xG)), sdtpldt0(sdtasdt0(xF, xD), sdtasdt0(xF, xG)))]]))).
% 116.19/112.29 cnf('1.1.3.1',plain,[-(sdtasdt0(sdtpldt0(xC, xF), sdtpldt0(xD, xG)) = sdtpldt0(sdtpldt0(sdtasdt0(xC, xD), sdtasdt0(xC, xG)), sdtpldt0(sdtasdt0(xF, xD), sdtasdt0(xF, xG)))), aScalar0(xC), aScalar0(xF), aScalar0(xD), aScalar0(xG)],extension(5,bind([[_42354, _42453, _42551, _42648], [xC, xF, xD, xG]]))).
% 116.19/112.29 cnf('1.1.3.1.1',plain,[-(aScalar0(xC))],extension(6)).
% 116.19/112.29 cnf('1.1.3.1.2',plain,[-(aScalar0(xF))],extension(9)).
% 116.19/112.29 cnf('1.1.3.1.3',plain,[-(aScalar0(xD))],extension(7)).
% 116.19/112.29 cnf('1.1.3.1.4',plain,[-(aScalar0(xG))],extension(10)).
% 116.19/112.29 %-----------------------------------------------------
% 116.19/112.29
% 116.19/112.29 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------