%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : NUM560+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n020.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:42:01 EDT 2022
% Result : Theorem 118.25s 113.67s
% Output : Proof 118.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM560+1 : TPTP v8.1.0. Released v4.0.0.
% 0.00/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.34 % Computer : n020.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Tue Jul 5 16:47:14 EDT 2022
% 0.12/0.34 % CPUTime :
% 118.25/113.67 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 118.25/113.67 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 118.25/113.68
% 118.25/113.68 %-----------------------------------------------------
% 118.25/113.68 fof(m__, conjecture, aSubsetOf0(sdtlbdtrb0(xF, xy), szDzozmdt0(xF)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__)).
% 118.25/113.68 fof(mDefSub, definition, ! [_115187] : (aSet0(_115187) => ! [_115202] : (aSubsetOf0(_115202, _115187) <=> aSet0(_115202) & ! [_115227] : (aElementOf0(_115227, _115202) => aElementOf0(_115227, _115187)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mDefSub)).
% 118.25/113.68 fof(mDomSet, axiom, ! [_115561] : (aFunction0(_115561) => aSet0(szDzozmdt0(_115561))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mDomSet)).
% 118.25/113.68 fof(m__2693, hypothesis, aFunction0(xF) & aElement0(xy), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2693)).
% 118.25/113.68 fof(mDefPtt, definition, ! [_115758, _115761] : (aFunction0(_115758) & aElement0(_115761) => ! [_115783] : (_115783 = sdtlbdtrb0(_115758, _115761) <=> aSet0(_115783) & ! [_115811] : (aElementOf0(_115811, _115783) <=> aElementOf0(_115811, szDzozmdt0(_115758)) & sdtlpdtrp0(_115758, _115811) = _115761))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mDefPtt)).
% 118.25/113.68
% 118.25/113.68 cnf(1, plain, [aSubsetOf0(sdtlbdtrb0(xF, xy), szDzozmdt0(xF))], clausify(m__)).
% 118.25/113.68 cnf(2, plain, [-(_35592 = _35592)], theory(equality)).
% 118.25/113.68 cnf(3, plain, [aSet0(_48500), -(aSubsetOf0(_48604, _48500)), aSet0(_48604), -(aElementOf0(2 ^ [_48604, _48500], _48604))], clausify(mDefSub)).
% 118.25/113.68 cnf(4, plain, [aSet0(_48500), -(aSubsetOf0(_48604, _48500)), aSet0(_48604), aElementOf0(2 ^ [_48604, _48500], _48500)], clausify(mDefSub)).
% 118.25/113.68 cnf(5, plain, [aFunction0(_75361), -(aSet0(szDzozmdt0(_75361)))], clausify(mDomSet)).
% 118.25/113.68 cnf(6, plain, [-(aFunction0(xF))], clausify(m__2693)).
% 118.25/113.68 cnf(7, plain, [-(aElement0(xy))], clausify(m__2693)).
% 118.25/113.68 cnf(8, plain, [aElement0(_76087), aFunction0(_75997), _76267 = sdtlbdtrb0(_75997, _76087), -(aSet0(_76267))], clausify(mDefPtt)).
% 118.25/113.68 cnf(9, plain, [aElement0(_76087), aFunction0(_75997), _76267 = sdtlbdtrb0(_75997, _76087), aElementOf0(_76479, _76267), -(aElementOf0(_76479, szDzozmdt0(_75997)))], clausify(mDefPtt)).
% 118.25/113.68
% 118.25/113.68 cnf('1',plain,[aSubsetOf0(sdtlbdtrb0(xF, xy), szDzozmdt0(xF))],start(1)).
% 118.25/113.68 cnf('1.1',plain,[-(aSubsetOf0(sdtlbdtrb0(xF, xy), szDzozmdt0(xF))), aSet0(szDzozmdt0(xF)), aSet0(sdtlbdtrb0(xF, xy)), -(aElementOf0(2 ^ [sdtlbdtrb0(xF, xy), szDzozmdt0(xF)], sdtlbdtrb0(xF, xy)))],extension(3,bind([[_48500, _48604], [szDzozmdt0(xF), sdtlbdtrb0(xF, xy)]]))).
% 118.25/113.68 cnf('1.1.1',plain,[-(aSet0(szDzozmdt0(xF))), aFunction0(xF)],extension(5,bind([[_75361], [xF]]))).
% 118.25/113.68 cnf('1.1.1.1',plain,[-(aFunction0(xF))],extension(6)).
% 118.25/113.68 cnf('1.1.2',plain,[-(aSet0(sdtlbdtrb0(xF, xy))), aElement0(xy), aFunction0(xF), sdtlbdtrb0(xF, xy) = sdtlbdtrb0(xF, xy)],extension(8,bind([[_76267, _75997, _76087], [sdtlbdtrb0(xF, xy), xF, xy]]))).
% 118.25/113.68 cnf('1.1.2.1',plain,[-(aElement0(xy))],extension(7)).
% 118.25/113.68 cnf('1.1.2.2',plain,[-(aFunction0(xF))],extension(6)).
% 118.25/113.68 cnf('1.1.2.3',plain,[-(sdtlbdtrb0(xF, xy) = sdtlbdtrb0(xF, xy))],extension(2,bind([[_35592], [sdtlbdtrb0(xF, xy)]]))).
% 118.25/113.68 cnf('1.1.3',plain,[aElementOf0(2 ^ [sdtlbdtrb0(xF, xy), szDzozmdt0(xF)], sdtlbdtrb0(xF, xy)), aElement0(xy), aFunction0(xF), sdtlbdtrb0(xF, xy) = sdtlbdtrb0(xF, xy), -(aElementOf0(2 ^ [sdtlbdtrb0(xF, xy), szDzozmdt0(xF)], szDzozmdt0(xF)))],extension(9,bind([[_76267, _76087, _76479, _75997], [sdtlbdtrb0(xF, xy), xy, 2 ^ [sdtlbdtrb0(xF, xy), szDzozmdt0(xF)], xF]]))).
% 118.25/113.68 cnf('1.1.3.1',plain,[-(aElement0(xy))],extension(7)).
% 118.25/113.68 cnf('1.1.3.2',plain,[-(aFunction0(xF))],extension(6)).
% 118.25/113.68 cnf('1.1.3.3',plain,[-(sdtlbdtrb0(xF, xy) = sdtlbdtrb0(xF, xy))],extension(2,bind([[_35592], [sdtlbdtrb0(xF, xy)]]))).
% 118.25/113.68 cnf('1.1.3.4',plain,[aElementOf0(2 ^ [sdtlbdtrb0(xF, xy), szDzozmdt0(xF)], szDzozmdt0(xF)), aSet0(szDzozmdt0(xF)), -(aSubsetOf0(sdtlbdtrb0(xF, xy), szDzozmdt0(xF))), aSet0(sdtlbdtrb0(xF, xy))],extension(4,bind([[_48500, _48604], [szDzozmdt0(xF), sdtlbdtrb0(xF, xy)]]))).
% 118.25/113.68 cnf('1.1.3.4.1',plain,[-(aSet0(szDzozmdt0(xF)))],lemmata('1.1')).
% 118.25/113.68 cnf('1.1.3.4.2',plain,[aSubsetOf0(sdtlbdtrb0(xF, xy), szDzozmdt0(xF))],extension(1)).
% 118.25/113.68 cnf('1.1.3.4.3',plain,[-(aSet0(sdtlbdtrb0(xF, xy)))],lemmata('1.1')).
% 118.25/113.68 %-----------------------------------------------------
% 118.25/113.69
% 118.25/113.69 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------