%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : NUM539+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n007.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 11:41:49 EDT 2022
% Result : Theorem 179.60s 172.90s
% Output : Proof 179.69s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : NUM539+1 : TPTP v8.1.0. Released v4.0.0.
% 0.11/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n007.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Thu Jul 7 01:14:44 EDT 2022
% 0.13/0.34 % CPUTime :
% 179.60/172.90 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 179.60/172.91 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 179.69/172.92
% 179.69/172.92 %-----------------------------------------------------
% 179.69/172.92 fof(mDefMin, definition, ! [_85079] : (aSubsetOf0(_85079, szNzAzT0) & (! _85079) = slcrc0 => ! [_85105] : (_85105 = szmzizndt0(_85079) <=> aElementOf0(_85105, _85079) & ! [_85133] : (aElementOf0(_85133, _85079) => sdtlseqdt0(_85105, _85133)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mDefMin)).
% 179.69/172.92 fof(mDefSub, definition, ! [_85451] : (aSet0(_85451) => ! [_85466] : (aSubsetOf0(_85466, _85451) <=> aSet0(_85466) & ! [_85491] : (aElementOf0(_85491, _85466) => aElementOf0(_85491, _85451)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mDefSub)).
% 179.69/172.92 fof(m__, conjecture, szmzizndt0(xS) = szmzizndt0(xT), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__)).
% 179.69/172.92 fof(mNATSet, axiom, aSet0(szNzAzT0) & isCountable0(szNzAzT0), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mNATSet)).
% 179.69/172.92 fof(mLessASymm, axiom, ! [_85920, _85923] : (aElementOf0(_85920, szNzAzT0) & aElementOf0(_85923, szNzAzT0) => sdtlseqdt0(_85920, _85923) & sdtlseqdt0(_85923, _85920) => _85920 = _85923), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mLessASymm)).
% 179.69/172.92 fof(m__1779, hypothesis, aSubsetOf0(xS, szNzAzT0) & aSubsetOf0(xT, szNzAzT0) & (! xS) = slcrc0 & (! xT) = slcrc0, file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__1779)).
% 179.69/172.92 fof(m__1802, hypothesis, aElementOf0(szmzizndt0(xS), xT) & aElementOf0(szmzizndt0(xT), xS), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__1802)).
% 179.69/172.92
% 179.69/172.92 cnf(1, plain, [-(29 ^ [_52002, _51775]), aElementOf0(_52199, _51775), -(sdtlseqdt0(_52002, _52199))], clausify(mDefMin)).
% 179.69/172.92 cnf(2, plain, [-(32 ^ [_51775]), _52002 = szmzizndt0(_51775), 29 ^ [_52002, _51775]], clausify(mDefMin)).
% 179.69/172.92 cnf(3, plain, [-(3 ^ [_35016, _34912]), aElementOf0(_35173, _35016), -(aElementOf0(_35173, _34912))], clausify(mDefSub)).
% 179.69/172.92 cnf(4, plain, [-(6 ^ [_34912]), aSubsetOf0(_35016, _34912), 3 ^ [_35016, _34912]], clausify(mDefSub)).
% 179.69/172.92 cnf(5, plain, [szmzizndt0(xS) = szmzizndt0(xT)], clausify(m__)).
% 179.69/172.92 cnf(6, plain, [-(_24953 = _24953)], theory(equality)).
% 179.69/172.92 cnf(7, plain, [-(aElementOf0(_26257, _26388)), aElementOf0(_26190, _26323), _26190 = _26257, _26323 = _26388], theory(equality)).
% 179.69/172.92 cnf(8, plain, [aSet0(_34912), 6 ^ [_34912]], clausify(mDefSub)).
% 179.69/172.92 cnf(9, plain, [-(aSet0(szNzAzT0))], clausify(mNATSet)).
% 179.69/172.92 cnf(10, plain, [aElementOf0(_46078, szNzAzT0), aElementOf0(_46015, szNzAzT0), -(_46015 = _46078), sdtlseqdt0(_46015, _46078), sdtlseqdt0(_46078, _46015)], clausify(mLessASymm)).
% 179.69/172.92 cnf(11, plain, [-(_51775 = slcrc0), aSubsetOf0(_51775, szNzAzT0), 32 ^ [_51775]], clausify(mDefMin)).
% 179.69/172.92 cnf(12, plain, [-(aSubsetOf0(xS, szNzAzT0))], clausify(m__1779)).
% 179.69/172.92 cnf(13, plain, [-(aSubsetOf0(xT, szNzAzT0))], clausify(m__1779)).
% 179.69/172.92 cnf(14, plain, [xS = slcrc0], clausify(m__1779)).
% 179.69/172.92 cnf(15, plain, [xT = slcrc0], clausify(m__1779)).
% 179.69/172.92 cnf(16, plain, [-(aElementOf0(szmzizndt0(xS), xT))], clausify(m__1802)).
% 179.69/172.92 cnf(17, plain, [-(aElementOf0(szmzizndt0(xT), xS))], clausify(m__1802)).
% 179.69/172.92
% 179.69/172.92 cnf('1',plain,[szmzizndt0(xS) = szmzizndt0(xT)],start(5)).
% 179.69/172.92 cnf('1.1',plain,[-(szmzizndt0(xS) = szmzizndt0(xT)), aElementOf0(szmzizndt0(xT), szNzAzT0), aElementOf0(szmzizndt0(xS), szNzAzT0), sdtlseqdt0(szmzizndt0(xS), szmzizndt0(xT)), sdtlseqdt0(szmzizndt0(xT), szmzizndt0(xS))],extension(10,bind([[_46078, _46015], [szmzizndt0(xT), szmzizndt0(xS)]]))).
% 179.69/172.92 cnf('1.1.1',plain,[-(aElementOf0(szmzizndt0(xT), szNzAzT0)), -(3 ^ [xS, szNzAzT0]), aElementOf0(szmzizndt0(xT), xS)],extension(3,bind([[_34912, _35173, _35016], [szNzAzT0, szmzizndt0(xT), xS]]))).
% 179.69/172.92 cnf('1.1.1.1',plain,[3 ^ [xS, szNzAzT0], -(6 ^ [szNzAzT0]), aSubsetOf0(xS, szNzAzT0)],extension(4,bind([[_35016, _34912], [xS, szNzAzT0]]))).
% 179.69/172.92 cnf('1.1.1.1.1',plain,[6 ^ [szNzAzT0], aSet0(szNzAzT0)],extension(8,bind([[_34912], [szNzAzT0]]))).
% 179.69/172.92 cnf('1.1.1.1.1.1',plain,[-(aSet0(szNzAzT0))],extension(9)).
% 179.69/172.92 cnf('1.1.1.1.2',plain,[-(aSubsetOf0(xS, szNzAzT0))],extension(12)).
% 179.69/172.92 cnf('1.1.1.2',plain,[-(aElementOf0(szmzizndt0(xT), xS)), aElementOf0(szmzizndt0(xT), xS), szmzizndt0(xT) = szmzizndt0(xT), xS = xS],extension(7,bind([[_26190, _26257, _26323, _26388], [szmzizndt0(xT), szmzizndt0(xT), xS, xS]]))).
% 179.69/172.92 cnf('1.1.1.2.1',plain,[-(aElementOf0(szmzizndt0(xT), xS))],extension(17)).
% 179.69/172.92 cnf('1.1.1.2.2',plain,[-(szmzizndt0(xT) = szmzizndt0(xT))],extension(6,bind([[_24953], [szmzizndt0(xT)]]))).
% 179.69/172.92 cnf('1.1.1.2.3',plain,[-(xS = xS)],extension(6,bind([[_24953], [xS]]))).
% 179.69/172.92 cnf('1.1.2',plain,[-(aElementOf0(szmzizndt0(xS), szNzAzT0)), -(3 ^ [xT, szNzAzT0]), aElementOf0(szmzizndt0(xS), xT)],extension(3,bind([[_34912, _35173, _35016], [szNzAzT0, szmzizndt0(xS), xT]]))).
% 179.69/172.92 cnf('1.1.2.1',plain,[3 ^ [xT, szNzAzT0], -(6 ^ [szNzAzT0]), aSubsetOf0(xT, szNzAzT0)],extension(4,bind([[_35016, _34912], [xT, szNzAzT0]]))).
% 179.69/172.92 cnf('1.1.2.1.1',plain,[6 ^ [szNzAzT0], aSet0(szNzAzT0)],extension(8,bind([[_34912], [szNzAzT0]]))).
% 179.69/172.92 cnf('1.1.2.1.1.1',plain,[-(aSet0(szNzAzT0))],extension(9)).
% 179.69/172.92 cnf('1.1.2.1.2',plain,[-(aSubsetOf0(xT, szNzAzT0))],extension(13)).
% 179.69/172.92 cnf('1.1.2.2',plain,[-(aElementOf0(szmzizndt0(xS), xT)), aElementOf0(szmzizndt0(xS), xT), szmzizndt0(xS) = szmzizndt0(xS), xT = xT],extension(7,bind([[_26190, _26257, _26323, _26388], [szmzizndt0(xS), szmzizndt0(xS), xT, xT]]))).
% 179.69/172.92 cnf('1.1.2.2.1',plain,[-(aElementOf0(szmzizndt0(xS), xT))],extension(16)).
% 179.69/172.92 cnf('1.1.2.2.2',plain,[-(szmzizndt0(xS) = szmzizndt0(xS))],extension(6,bind([[_24953], [szmzizndt0(xS)]]))).
% 179.69/172.92 cnf('1.1.2.2.3',plain,[-(xT = xT)],extension(6,bind([[_24953], [xT]]))).
% 179.69/172.92 cnf('1.1.3',plain,[-(sdtlseqdt0(szmzizndt0(xS), szmzizndt0(xT))), -(29 ^ [szmzizndt0(xS), xS]), aElementOf0(szmzizndt0(xT), xS)],extension(1,bind([[_52002, _52199, _51775], [szmzizndt0(xS), szmzizndt0(xT), xS]]))).
% 179.69/172.92 cnf('1.1.3.1',plain,[29 ^ [szmzizndt0(xS), xS], -(32 ^ [xS]), szmzizndt0(xS) = szmzizndt0(xS)],extension(2,bind([[_52002, _51775], [szmzizndt0(xS), xS]]))).
% 179.69/172.92 cnf('1.1.3.1.1',plain,[32 ^ [xS], -(xS = slcrc0), aSubsetOf0(xS, szNzAzT0)],extension(11,bind([[_51775], [xS]]))).
% 179.69/172.92 cnf('1.1.3.1.1.1',plain,[xS = slcrc0],extension(14)).
% 179.69/172.92 cnf('1.1.3.1.1.2',plain,[-(aSubsetOf0(xS, szNzAzT0))],extension(12)).
% 179.69/172.92 cnf('1.1.3.1.2',plain,[-(szmzizndt0(xS) = szmzizndt0(xS))],extension(6,bind([[_24953], [szmzizndt0(xS)]]))).
% 179.69/172.92 cnf('1.1.3.2',plain,[-(aElementOf0(szmzizndt0(xT), xS)), aElementOf0(szmzizndt0(xT), xS), szmzizndt0(xT) = szmzizndt0(xT), xS = xS],extension(7,bind([[_26190, _26257, _26323, _26388], [szmzizndt0(xT), szmzizndt0(xT), xS, xS]]))).
% 179.69/172.92 cnf('1.1.3.2.1',plain,[-(aElementOf0(szmzizndt0(xT), xS))],extension(17)).
% 179.69/172.92 cnf('1.1.3.2.2',plain,[-(szmzizndt0(xT) = szmzizndt0(xT))],extension(6,bind([[_24953], [szmzizndt0(xT)]]))).
% 179.69/172.92 cnf('1.1.3.2.3',plain,[-(xS = xS)],extension(6,bind([[_24953], [xS]]))).
% 179.69/172.92 cnf('1.1.4',plain,[-(sdtlseqdt0(szmzizndt0(xT), szmzizndt0(xS))), -(29 ^ [szmzizndt0(xT), xT]), aElementOf0(szmzizndt0(xS), xT)],extension(1,bind([[_52002, _52199, _51775], [szmzizndt0(xT), szmzizndt0(xS), xT]]))).
% 179.69/172.92 cnf('1.1.4.1',plain,[29 ^ [szmzizndt0(xT), xT], -(32 ^ [xT]), szmzizndt0(xT) = szmzizndt0(xT)],extension(2,bind([[_52002, _51775], [szmzizndt0(xT), xT]]))).
% 179.69/172.92 cnf('1.1.4.1.1',plain,[32 ^ [xT], -(xT = slcrc0), aSubsetOf0(xT, szNzAzT0)],extension(11,bind([[_51775], [xT]]))).
% 179.69/172.92 cnf('1.1.4.1.1.1',plain,[xT = slcrc0],extension(15)).
% 179.69/172.92 cnf('1.1.4.1.1.2',plain,[-(aSubsetOf0(xT, szNzAzT0))],extension(13)).
% 179.69/172.92 cnf('1.1.4.1.2',plain,[-(szmzizndt0(xT) = szmzizndt0(xT))],extension(6,bind([[_24953], [szmzizndt0(xT)]]))).
% 179.69/172.92 cnf('1.1.4.2',plain,[-(aElementOf0(szmzizndt0(xS), xT)), aElementOf0(szmzizndt0(xS), xT), szmzizndt0(xS) = szmzizndt0(xS), xT = xT],extension(7,bind([[_26190, _26257, _26323, _26388], [szmzizndt0(xS), szmzizndt0(xS), xT, xT]]))).
% 179.69/172.92 cnf('1.1.4.2.1',plain,[-(aElementOf0(szmzizndt0(xS), xT))],extension(16)).
% 179.69/172.92 cnf('1.1.4.2.2',plain,[-(szmzizndt0(xS) = szmzizndt0(xS))],extension(6,bind([[_24953], [szmzizndt0(xS)]]))).
% 179.69/172.92 cnf('1.1.4.2.3',plain,[-(xT = xT)],extension(6,bind([[_24953], [xT]]))).
% 179.69/172.92 %-----------------------------------------------------
% 179.69/172.92
% 179.69/172.92 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------