%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : RNG086+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:47 EDT 2022
% Result : Theorem 113.39s 110.07s
% Output : Proof 113.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : RNG086+1 : TPTP v8.1.0. Released v4.0.0.
% 0.11/0.12 % Command : leancop_casc.sh %s %d
% 0.11/0.33 % Computer : n028.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 600
% 0.11/0.33 % DateTime : Mon May 30 10:46:19 EDT 2022
% 0.11/0.33 % CPUTime :
% 113.39/110.07 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 113.39/110.08 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 113.39/110.08
% 113.39/110.08 %-----------------------------------------------------
% 113.39/110.08 fof(m__, conjecture, ? [_56596, _56599] : (aElementOf0(_56596, xI) & aElementOf0(_56599, xJ) & xx = sdtpldt0(_56596, _56599)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__)).
% 113.39/110.08 fof(mDefSSum, definition, ! [_56856, _56859] : (aSet0(_56856) & aSet0(_56859) => ! [_56881] : (_56881 = sdtpldt1(_56856, _56859) <=> aSet0(_56881) & ! [_56909] : (aElementOf0(_56909, _56881) <=> ? [_56927, _56930] : (aElementOf0(_56927, _56856) & aElementOf0(_56930, _56859) & sdtpldt0(_56927, _56930) = _56909)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mDefSSum)).
% 113.39/110.08 fof(m__870, hypothesis, aIdeal0(xI) & aIdeal0(xJ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__870)).
% 113.39/110.08 fof(m__901, hypothesis, aElementOf0(xx, sdtpldt1(xI, xJ)) & aElementOf0(xy, sdtpldt1(xI, xJ)) & aElement0(xz), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__901)).
% 113.39/110.08 fof(mDefIdeal, definition, ! [_57457] : (aIdeal0(_57457) <=> aSet0(_57457) & ! [_57479] : (aElementOf0(_57479, _57457) => ! [_57497] : (aElementOf0(_57497, _57457) => aElementOf0(sdtpldt0(_57479, _57497), _57457)) & ! [_57497] : (aElement0(_57497) => aElementOf0(sdtasdt0(_57497, _57479), _57457)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mDefIdeal)).
% 113.39/110.08
% 113.39/110.08 cnf(1, plain, [aElementOf0(_32927, xI), aElementOf0(_32982, xJ), xx = sdtpldt0(_32927, _32982)], clausify(m__)).
% 113.39/110.08 cnf(2, plain, [-(_14745 = _14745)], theory(equality)).
% 113.39/110.08 cnf(3, plain, [_14898 = _14943, -(_14943 = _14898)], theory(equality)).
% 113.39/110.08 cnf(4, plain, [-(aElementOf0(_16049, _16180)), aElementOf0(_15982, _16115), _15982 = _16049, _16115 = _16180], theory(equality)).
% 113.39/110.08 cnf(5, plain, [aSet0(_29179), aSet0(_29075), _29373 = sdtpldt1(_29075, _29179), aElementOf0(_29599, _29373), -(aElementOf0(3 ^ [_29599, _29373, _29179, _29075], _29075))], clausify(mDefSSum)).
% 113.39/110.08 cnf(6, plain, [aSet0(_29179), aSet0(_29075), _29373 = sdtpldt1(_29075, _29179), aElementOf0(_29599, _29373), -(aElementOf0(4 ^ [_29599, _29373, _29179, _29075], _29179))], clausify(mDefSSum)).
% 113.39/110.08 cnf(7, plain, [aSet0(_29179), aSet0(_29075), _29373 = sdtpldt1(_29075, _29179), aElementOf0(_29599, _29373), -(sdtpldt0(3 ^ [_29599, _29373, _29179, _29075], 4 ^ [_29599, _29373, _29179, _29075]) = _29599)], clausify(mDefSSum)).
% 113.39/110.08 cnf(8, plain, [-(aIdeal0(xI))], clausify(m__870)).
% 113.39/110.08 cnf(9, plain, [-(aIdeal0(xJ))], clausify(m__870)).
% 113.39/110.08 cnf(10, plain, [-(aElementOf0(xx, sdtpldt1(xI, xJ)))], clausify(m__901)).
% 113.39/110.08 cnf(11, plain, [aIdeal0(_31175), -(aSet0(_31175))], clausify(mDefIdeal)).
% 113.39/110.08
% 113.39/110.08 cnf('1',plain,[aElementOf0(3 ^ [xx, sdtpldt1(xI, xJ), xJ, xI], xI), aElementOf0(4 ^ [xx, sdtpldt1(xI, xJ), xJ, xI], xJ), xx = sdtpldt0(3 ^ [xx, sdtpldt1(xI, xJ), xJ, xI], 4 ^ [xx, sdtpldt1(xI, xJ), xJ, xI])],start(1,bind([[_32927, _32982], [3 ^ [xx, sdtpldt1(xI, xJ), xJ, xI], 4 ^ [xx, sdtpldt1(xI, xJ), xJ, xI]]]))).
% 113.39/110.08 cnf('1.1',plain,[-(aElementOf0(3 ^ [xx, sdtpldt1(xI, xJ), xJ, xI], xI)), aElementOf0(3 ^ [xx, sdtpldt1(xI, xJ), xJ, xI], xI), 3 ^ [xx, sdtpldt1(xI, xJ), xJ, xI] = 3 ^ [xx, sdtpldt1(xI, xJ), xJ, xI], xI = xI],extension(4,bind([[_15982, _16049, _16115, _16180], [3 ^ [xx, sdtpldt1(xI, xJ), xJ, xI], 3 ^ [xx, sdtpldt1(xI, xJ), xJ, xI], xI, xI]]))).
% 113.39/110.08 cnf('1.1.1',plain,[-(aElementOf0(3 ^ [xx, sdtpldt1(xI, xJ), xJ, xI], xI)), aSet0(xJ), aSet0(xI), sdtpldt1(xI, xJ) = sdtpldt1(xI, xJ), aElementOf0(xx, sdtpldt1(xI, xJ))],extension(5,bind([[_29075, _29179, _29599, _29373], [xI, xJ, xx, sdtpldt1(xI, xJ)]]))).
% 113.39/110.08 cnf('1.1.1.1',plain,[-(aSet0(xJ)), aIdeal0(xJ)],extension(11,bind([[_31175], [xJ]]))).
% 113.39/110.08 cnf('1.1.1.1.1',plain,[-(aIdeal0(xJ))],extension(9)).
% 113.39/110.08 cnf('1.1.1.2',plain,[-(aSet0(xI)), aIdeal0(xI)],extension(11,bind([[_31175], [xI]]))).
% 113.39/110.08 cnf('1.1.1.2.1',plain,[-(aIdeal0(xI))],extension(8)).
% 113.39/110.08 cnf('1.1.1.3',plain,[-(sdtpldt1(xI, xJ) = sdtpldt1(xI, xJ))],extension(2,bind([[_14745], [sdtpldt1(xI, xJ)]]))).
% 113.39/110.08 cnf('1.1.1.4',plain,[-(aElementOf0(xx, sdtpldt1(xI, xJ)))],extension(10)).
% 113.39/110.08 cnf('1.1.2',plain,[-(3 ^ [xx, sdtpldt1(xI, xJ), xJ, xI] = 3 ^ [xx, sdtpldt1(xI, xJ), xJ, xI])],extension(2,bind([[_14745], [3 ^ [xx, sdtpldt1(xI, xJ), xJ, xI]]]))).
% 113.39/110.08 cnf('1.1.3',plain,[-(xI = xI)],extension(2,bind([[_14745], [xI]]))).
% 113.39/110.08 cnf('1.2',plain,[-(aElementOf0(4 ^ [xx, sdtpldt1(xI, xJ), xJ, xI], xJ)), aElementOf0(4 ^ [xx, sdtpldt1(xI, xJ), xJ, xI], xJ), 4 ^ [xx, sdtpldt1(xI, xJ), xJ, xI] = 4 ^ [xx, sdtpldt1(xI, xJ), xJ, xI], xJ = xJ],extension(4,bind([[_15982, _16049, _16115, _16180], [4 ^ [xx, sdtpldt1(xI, xJ), xJ, xI], 4 ^ [xx, sdtpldt1(xI, xJ), xJ, xI], xJ, xJ]]))).
% 113.39/110.08 cnf('1.2.1',plain,[-(aElementOf0(4 ^ [xx, sdtpldt1(xI, xJ), xJ, xI], xJ)), aSet0(xJ), aSet0(xI), sdtpldt1(xI, xJ) = sdtpldt1(xI, xJ), aElementOf0(xx, sdtpldt1(xI, xJ))],extension(6,bind([[_29075, _29179, _29599, _29373], [xI, xJ, xx, sdtpldt1(xI, xJ)]]))).
% 113.39/110.08 cnf('1.2.1.1',plain,[-(aSet0(xJ)), aIdeal0(xJ)],extension(11,bind([[_31175], [xJ]]))).
% 113.39/110.08 cnf('1.2.1.1.1',plain,[-(aIdeal0(xJ))],extension(9)).
% 113.39/110.08 cnf('1.2.1.2',plain,[-(aSet0(xI)), aIdeal0(xI)],extension(11,bind([[_31175], [xI]]))).
% 113.39/110.08 cnf('1.2.1.2.1',plain,[-(aIdeal0(xI))],extension(8)).
% 113.39/110.08 cnf('1.2.1.3',plain,[-(sdtpldt1(xI, xJ) = sdtpldt1(xI, xJ))],extension(2,bind([[_14745], [sdtpldt1(xI, xJ)]]))).
% 113.39/110.08 cnf('1.2.1.4',plain,[-(aElementOf0(xx, sdtpldt1(xI, xJ)))],extension(10)).
% 113.39/110.08 cnf('1.2.2',plain,[-(4 ^ [xx, sdtpldt1(xI, xJ), xJ, xI] = 4 ^ [xx, sdtpldt1(xI, xJ), xJ, xI])],extension(2,bind([[_14745], [4 ^ [xx, sdtpldt1(xI, xJ), xJ, xI]]]))).
% 113.39/110.08 cnf('1.2.3',plain,[-(xJ = xJ)],extension(2,bind([[_14745], [xJ]]))).
% 113.39/110.08 cnf('1.3',plain,[-(xx = sdtpldt0(3 ^ [xx, sdtpldt1(xI, xJ), xJ, xI], 4 ^ [xx, sdtpldt1(xI, xJ), xJ, xI])), sdtpldt0(3 ^ [xx, sdtpldt1(xI, xJ), xJ, xI], 4 ^ [xx, sdtpldt1(xI, xJ), xJ, xI]) = xx],extension(3,bind([[_14898, _14943], [sdtpldt0(3 ^ [xx, sdtpldt1(xI, xJ), xJ, xI], 4 ^ [xx, sdtpldt1(xI, xJ), xJ, xI]), xx]]))).
% 113.39/110.08 cnf('1.3.1',plain,[-(sdtpldt0(3 ^ [xx, sdtpldt1(xI, xJ), xJ, xI], 4 ^ [xx, sdtpldt1(xI, xJ), xJ, xI]) = xx), aSet0(xJ), aSet0(xI), sdtpldt1(xI, xJ) = sdtpldt1(xI, xJ), aElementOf0(xx, sdtpldt1(xI, xJ))],extension(7,bind([[_29075, _29179, _29599, _29373], [xI, xJ, xx, sdtpldt1(xI, xJ)]]))).
% 113.39/110.08 cnf('1.3.1.1',plain,[-(aSet0(xJ)), aIdeal0(xJ)],extension(11,bind([[_31175], [xJ]]))).
% 113.39/110.08 cnf('1.3.1.1.1',plain,[-(aIdeal0(xJ))],extension(9)).
% 113.39/110.08 cnf('1.3.1.2',plain,[-(aSet0(xI)), aIdeal0(xI)],extension(11,bind([[_31175], [xI]]))).
% 113.39/110.08 cnf('1.3.1.2.1',plain,[-(aIdeal0(xI))],extension(8)).
% 113.39/110.08 cnf('1.3.1.3',plain,[-(sdtpldt1(xI, xJ) = sdtpldt1(xI, xJ))],extension(2,bind([[_14745], [sdtpldt1(xI, xJ)]]))).
% 113.39/110.08 cnf('1.3.1.4',plain,[-(aElementOf0(xx, sdtpldt1(xI, xJ)))],extension(10)).
% 113.39/110.08 %-----------------------------------------------------
% 113.39/110.09
% 113.39/110.09 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------