%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : NUM537+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n029.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:48 EDT 2022
% Result : Theorem 0.67s 1.42s
% Output : Proof 0.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : NUM537+1 : TPTP v8.1.0. Released v4.0.0.
% 0.04/0.13 % Command : leancop_casc.sh %s %d
% 0.12/0.34 % Computer : n029.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 23:34:27 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.67/1.42 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.67/1.43 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.67/1.43
% 0.67/1.43 %-----------------------------------------------------
% 0.67/1.43 fof(m__, conjecture, aSubsetOf0(xS, sdtmndt0(sdtpldt0(xS, xx), xx)) & aSubsetOf0(sdtmndt0(sdtpldt0(xS, xx), xx), xS), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__)).
% 0.67/1.43 fof(mEOfElem, axiom, ! [_66497] : (aSet0(_66497) => ! [_66512] : (aElementOf0(_66512, _66497) => aElement0(_66512))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mEOfElem)).
% 0.67/1.43 fof(mDefSub, definition, ! [_66682] : (aSet0(_66682) => ! [_66697] : (aSubsetOf0(_66697, _66682) <=> aSet0(_66697) & ! [_66722] : (aElementOf0(_66722, _66697) => aElementOf0(_66722, _66682)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mDefSub)).
% 0.67/1.43 fof(mSubRefl, axiom, ! [_66951] : (aSet0(_66951) => aSubsetOf0(_66951, _66951)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mSubRefl)).
% 0.67/1.43 fof(mDefCons, definition, ! [_67081, _67084] : (aSet0(_67081) & aElement0(_67084) => ! [_67106] : (_67106 = sdtpldt0(_67081, _67084) <=> aSet0(_67106) & ! [_67134] : (aElementOf0(_67134, _67106) <=> aElement0(_67134) & (aElementOf0(_67134, _67081) | _67134 = _67084)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mDefCons)).
% 0.67/1.43 fof(m__679, hypothesis, aElement0(xx) & aSet0(xS), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__679)).
% 0.67/1.43 fof(m__679_02, hypothesis, ~ aElementOf0(xx, xS), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__679_02)).
% 0.67/1.43 fof(mDefDiff, definition, ! [_67590, _67593] : (aSet0(_67590) & aElement0(_67593) => ! [_67615] : (_67615 = sdtmndt0(_67590, _67593) <=> aSet0(_67615) & ! [_67643] : (aElementOf0(_67643, _67615) <=> aElement0(_67643) & aElementOf0(_67643, _67590) & (! _67643) = _67593))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mDefDiff)).
% 0.67/1.43
% 0.67/1.43 cnf(1, plain, [aSubsetOf0(xS, sdtmndt0(sdtpldt0(xS, xx), xx)), aSubsetOf0(sdtmndt0(sdtpldt0(xS, xx), xx), xS)], clausify(m__)).
% 0.67/1.43 cnf(2, plain, [-(_10668 = _10668)], theory(equality)).
% 0.67/1.43 cnf(3, plain, [-(aElementOf0(_11972, _12103)), aElementOf0(_11905, _12038), _11905 = _11972, _12038 = _12103], theory(equality)).
% 0.67/1.43 cnf(4, plain, [-(aSubsetOf0(_12925, _13056)), aSubsetOf0(_12858, _12991), _12858 = _12925, _12991 = _13056], theory(equality)).
% 0.67/1.43 cnf(5, plain, [aSet0(_15967), aElementOf0(_16054, _15967), -(aElement0(_16054))], clausify(mEOfElem)).
% 0.67/1.43 cnf(6, plain, [aSet0(_17973), aSubsetOf0(_18077, _17973), -(aSet0(_18077))], clausify(mDefSub)).
% 0.67/1.43 cnf(7, plain, [aSet0(_18958), -(aSubsetOf0(_18958, _18958))], clausify(mSubRefl)).
% 0.67/1.43 cnf(8, plain, [aElement0(_20473), aSet0(_20383), _20653 = sdtpldt0(_20383, _20473), -(aSet0(_20653))], clausify(mDefCons)).
% 0.67/1.43 cnf(9, plain, [aElement0(_20473), aSet0(_20383), _20653 = sdtpldt0(_20383, _20473), aElementOf0(_20865, _20653), -(aElementOf0(_20865, _20383)), -(_20865 = _20473)], clausify(mDefCons)).
% 0.67/1.43 cnf(10, plain, [aElement0(_20473), aSet0(_20383), _20653 = sdtpldt0(_20383, _20473), -(aElementOf0(_20865, _20653)), aElement0(_20865), aElementOf0(_20865, _20383)], clausify(mDefCons)).
% 0.67/1.43 cnf(11, plain, [-(aElement0(xx))], clausify(m__679)).
% 0.67/1.43 cnf(12, plain, [-(aSet0(xS))], clausify(m__679)).
% 0.67/1.43 cnf(13, plain, [aElementOf0(xx, xS)], clausify(m__679_02)).
% 0.67/1.43 cnf(14, plain, [aElement0(_21427), aSet0(_21335), -(_21609 = sdtmndt0(_21335, _21427)), aSet0(_21609), -(aElementOf0(4 ^ [_21609, _21427, _21335], _21609)), -(aElementOf0(4 ^ [_21609, _21427, _21335], _21335))], clausify(mDefDiff)).
% 0.67/1.43 cnf(15, plain, [aElement0(_21427), aSet0(_21335), -(_21609 = sdtmndt0(_21335, _21427)), aSet0(_21609), -(aElementOf0(4 ^ [_21609, _21427, _21335], _21609)), 4 ^ [_21609, _21427, _21335] = _21427], clausify(mDefDiff)).
% 0.67/1.43 cnf(16, plain, [aElement0(_21427), aSet0(_21335), -(_21609 = sdtmndt0(_21335, _21427)), aSet0(_21609), aElementOf0(4 ^ [_21609, _21427, _21335], _21609), aElement0(4 ^ [_21609, _21427, _21335]), aElementOf0(4 ^ [_21609, _21427, _21335], _21335), -(4 ^ [_21609, _21427, _21335] = _21427)], clausify(mDefDiff)).
% 0.67/1.43
% 0.67/1.43 cnf('1',plain,[aSubsetOf0(xS, sdtmndt0(sdtpldt0(xS, xx), xx)), aSubsetOf0(sdtmndt0(sdtpldt0(xS, xx), xx), xS)],start(1)).
% 0.67/1.43 cnf('1.1',plain,[-(aSubsetOf0(xS, sdtmndt0(sdtpldt0(xS, xx), xx))), aSubsetOf0(xS, xS), xS = xS, xS = sdtmndt0(sdtpldt0(xS, xx), xx)],extension(4,bind([[_12858, _12925, _12991, _13056], [xS, xS, xS, sdtmndt0(sdtpldt0(xS, xx), xx)]]))).
% 0.67/1.43 cnf('1.1.1',plain,[-(aSubsetOf0(xS, xS)), aSubsetOf0(xS, xS), xS = xS, xS = xS],extension(4,bind([[_12858, _12925, _12991, _13056], [xS, xS, xS, xS]]))).
% 0.67/1.43 cnf('1.1.1.1',plain,[-(aSubsetOf0(xS, xS)), aSubsetOf0(xS, xS), xS = xS, xS = xS],extension(4,bind([[_12858, _12925, _12991, _13056], [xS, xS, xS, xS]]))).
% 0.67/1.43 cnf('1.1.1.1.1',plain,[-(aSubsetOf0(xS, xS)), aSet0(xS)],extension(7,bind([[_18958], [xS]]))).
% 0.67/1.43 cnf('1.1.1.1.1.1',plain,[-(aSet0(xS))],extension(12)).
% 0.67/1.43 cnf('1.1.1.1.2',plain,[-(xS = xS)],extension(2,bind([[_10668], [xS]]))).
% 0.67/1.43 cnf('1.1.1.1.3',plain,[-(xS = xS)],extension(2,bind([[_10668], [xS]]))).
% 0.67/1.43 cnf('1.1.1.2',plain,[-(xS = xS)],extension(2,bind([[_10668], [xS]]))).
% 0.67/1.43 cnf('1.1.1.3',plain,[-(xS = xS)],extension(2,bind([[_10668], [xS]]))).
% 0.67/1.43 cnf('1.1.2',plain,[-(xS = xS)],extension(2,bind([[_10668], [xS]]))).
% 0.67/1.43 cnf('1.1.3',plain,[-(xS = sdtmndt0(sdtpldt0(xS, xx), xx)), aElement0(xx), aSet0(sdtpldt0(xS, xx)), aSet0(xS), aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], xS), aElement0(4 ^ [xS, xx, sdtpldt0(xS, xx)]), aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], sdtpldt0(xS, xx)), -(4 ^ [xS, xx, sdtpldt0(xS, xx)] = xx)],extension(16,bind([[_21609, _21335, _21427], [xS, sdtpldt0(xS, xx), xx]]))).
% 0.67/1.43 cnf('1.1.3.1',plain,[-(aElement0(xx))],extension(11)).
% 0.67/1.43 cnf('1.1.3.2',plain,[-(aSet0(sdtpldt0(xS, xx))), aElement0(xx), aSet0(xS), sdtpldt0(xS, xx) = sdtpldt0(xS, xx)],extension(8,bind([[_20653, _20383, _20473], [sdtpldt0(xS, xx), xS, xx]]))).
% 0.67/1.43 cnf('1.1.3.2.1',plain,[-(aElement0(xx))],extension(11)).
% 0.67/1.43 cnf('1.1.3.2.2',plain,[-(aSet0(xS))],extension(12)).
% 0.67/1.43 cnf('1.1.3.2.3',plain,[-(sdtpldt0(xS, xx) = sdtpldt0(xS, xx))],extension(2,bind([[_10668], [sdtpldt0(xS, xx)]]))).
% 0.67/1.43 cnf('1.1.3.3',plain,[-(aSet0(xS)), aSet0(xS), aSubsetOf0(xS, xS)],extension(6,bind([[_18077, _17973], [xS, xS]]))).
% 0.67/1.43 cnf('1.1.3.3.1',plain,[-(aSet0(xS))],extension(12)).
% 0.67/1.43 cnf('1.1.3.3.2',plain,[-(aSubsetOf0(xS, xS))],lemmata('1.1')).
% 0.67/1.43 cnf('1.1.3.4',plain,[-(aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], xS)), aElement0(xx), aSet0(xS), sdtpldt0(xS, xx) = sdtpldt0(xS, xx), aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], sdtpldt0(xS, xx)), -(4 ^ [xS, xx, sdtpldt0(xS, xx)] = xx)],extension(9,bind([[_20383, _20653, _20865, _20473], [xS, sdtpldt0(xS, xx), 4 ^ [xS, xx, sdtpldt0(xS, xx)], xx]]))).
% 0.67/1.43 cnf('1.1.3.4.1',plain,[-(aElement0(xx))],extension(11)).
% 0.67/1.43 cnf('1.1.3.4.2',plain,[-(aSet0(xS))],extension(12)).
% 0.67/1.43 cnf('1.1.3.4.3',plain,[-(sdtpldt0(xS, xx) = sdtpldt0(xS, xx))],extension(2,bind([[_10668], [sdtpldt0(xS, xx)]]))).
% 0.67/1.43 cnf('1.1.3.4.4',plain,[-(aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], sdtpldt0(xS, xx))), aElement0(xx), aSet0(sdtpldt0(xS, xx)), -(xS = sdtmndt0(sdtpldt0(xS, xx), xx)), aSet0(xS), -(aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], xS))],extension(14,bind([[_21427, _21335, _21609], [xx, sdtpldt0(xS, xx), xS]]))).
% 0.67/1.43 cnf('1.1.3.4.4.1',plain,[-(aElement0(xx))],extension(11)).
% 0.67/1.43 cnf('1.1.3.4.4.2',plain,[-(aSet0(sdtpldt0(xS, xx)))],lemmata('1.1.3')).
% 0.67/1.43 cnf('1.1.3.4.4.3',plain,[xS = sdtmndt0(sdtpldt0(xS, xx), xx)],reduction('1.1')).
% 0.67/1.43 cnf('1.1.3.4.4.4',plain,[-(aSet0(xS))],extension(12)).
% 0.67/1.43 cnf('1.1.3.4.4.5',plain,[aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], xS)],reduction('1.1.3')).
% 0.67/1.43 cnf('1.1.3.4.5',plain,[4 ^ [xS, xx, sdtpldt0(xS, xx)] = xx, aElement0(xx), aSet0(sdtpldt0(xS, xx)), -(xS = sdtmndt0(sdtpldt0(xS, xx), xx)), aSet0(xS), -(aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], xS))],extension(15,bind([[_21427, _21335, _21609], [xx, sdtpldt0(xS, xx), xS]]))).
% 0.67/1.43 cnf('1.1.3.4.5.1',plain,[-(aElement0(xx))],extension(11)).
% 0.67/1.43 cnf('1.1.3.4.5.2',plain,[-(aSet0(sdtpldt0(xS, xx)))],lemmata('1.1.3')).
% 0.67/1.43 cnf('1.1.3.4.5.3',plain,[xS = sdtmndt0(sdtpldt0(xS, xx), xx)],reduction('1.1')).
% 0.67/1.43 cnf('1.1.3.4.5.4',plain,[-(aSet0(xS))],extension(12)).
% 0.67/1.43 cnf('1.1.3.4.5.5',plain,[aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], xS)],reduction('1.1.3')).
% 0.67/1.43 cnf('1.1.3.5',plain,[-(aElement0(4 ^ [xS, xx, sdtpldt0(xS, xx)])), aSet0(xS), aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], xS)],extension(5,bind([[_16054, _15967], [4 ^ [xS, xx, sdtpldt0(xS, xx)], xS]]))).
% 0.67/1.43 cnf('1.1.3.5.1',plain,[-(aSet0(xS))],extension(12)).
% 0.67/1.43 cnf('1.1.3.5.2',plain,[-(aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], xS))],lemmata('1.1.3')).
% 0.67/1.43 cnf('1.1.3.6',plain,[-(aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], sdtpldt0(xS, xx))), aElement0(xx), aSet0(xS), sdtpldt0(xS, xx) = sdtpldt0(xS, xx), aElement0(4 ^ [xS, xx, sdtpldt0(xS, xx)]), aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], xS)],extension(10,bind([[_20653, _20473, _20865, _20383], [sdtpldt0(xS, xx), xx, 4 ^ [xS, xx, sdtpldt0(xS, xx)], xS]]))).
% 0.67/1.43 cnf('1.1.3.6.1',plain,[-(aElement0(xx))],extension(11)).
% 0.67/1.43 cnf('1.1.3.6.2',plain,[-(aSet0(xS))],extension(12)).
% 0.67/1.43 cnf('1.1.3.6.3',plain,[-(sdtpldt0(xS, xx) = sdtpldt0(xS, xx))],extension(2,bind([[_10668], [sdtpldt0(xS, xx)]]))).
% 0.67/1.43 cnf('1.1.3.6.4',plain,[-(aElement0(4 ^ [xS, xx, sdtpldt0(xS, xx)]))],lemmata('1.1.3')).
% 0.67/1.43 cnf('1.1.3.6.5',plain,[-(aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], xS))],lemmata('1.1.3')).
% 0.67/1.43 cnf('1.1.3.7',plain,[4 ^ [xS, xx, sdtpldt0(xS, xx)] = xx, -(aElementOf0(xx, xS)), aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], xS), xS = xS],extension(3,bind([[_11972, _11905, _12038, _12103], [xx, 4 ^ [xS, xx, sdtpldt0(xS, xx)], xS, xS]]))).
% 0.67/1.43 cnf('1.1.3.7.1',plain,[aElementOf0(xx, xS)],extension(13)).
% 0.67/1.43 cnf('1.1.3.7.2',plain,[-(aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], xS)), aElement0(xx), aSet0(sdtpldt0(xS, xx)), -(xS = sdtmndt0(sdtpldt0(xS, xx), xx)), aSet0(xS), 4 ^ [xS, xx, sdtpldt0(xS, xx)] = xx],extension(15,bind([[_21609, _21335, _21427], [xS, sdtpldt0(xS, xx), xx]]))).
% 0.67/1.43 cnf('1.1.3.7.2.1',plain,[-(aElement0(xx))],extension(11)).
% 0.67/1.43 cnf('1.1.3.7.2.2',plain,[-(aSet0(sdtpldt0(xS, xx)))],lemmata('1.1.3')).
% 0.67/1.43 cnf('1.1.3.7.2.3',plain,[xS = sdtmndt0(sdtpldt0(xS, xx), xx)],reduction('1.1')).
% 0.67/1.43 cnf('1.1.3.7.2.4',plain,[-(aSet0(xS))],extension(12)).
% 0.67/1.43 cnf('1.1.3.7.2.5',plain,[-(4 ^ [xS, xx, sdtpldt0(xS, xx)] = xx)],reduction('1.1.3')).
% 0.67/1.43 cnf('1.1.3.7.3',plain,[-(xS = xS)],extension(2,bind([[_10668], [xS]]))).
% 0.67/1.43 cnf('1.2',plain,[-(aSubsetOf0(sdtmndt0(sdtpldt0(xS, xx), xx), xS)), aSubsetOf0(xS, xS), xS = sdtmndt0(sdtpldt0(xS, xx), xx), xS = xS],extension(4,bind([[_12858, _12925, _12991, _13056], [xS, sdtmndt0(sdtpldt0(xS, xx), xx), xS, xS]]))).
% 0.67/1.43 cnf('1.2.1',plain,[-(aSubsetOf0(xS, xS)), aSubsetOf0(xS, xS), xS = xS, xS = xS],extension(4,bind([[_12858, _12925, _12991, _13056], [xS, xS, xS, xS]]))).
% 0.67/1.43 cnf('1.2.1.1',plain,[-(aSubsetOf0(xS, xS)), aSubsetOf0(xS, xS), xS = xS, xS = xS],extension(4,bind([[_12858, _12925, _12991, _13056], [xS, xS, xS, xS]]))).
% 0.67/1.43 cnf('1.2.1.1.1',plain,[-(aSubsetOf0(xS, xS)), aSet0(xS)],extension(7,bind([[_18958], [xS]]))).
% 0.67/1.43 cnf('1.2.1.1.1.1',plain,[-(aSet0(xS))],extension(12)).
% 0.67/1.43 cnf('1.2.1.1.2',plain,[-(xS = xS)],extension(2,bind([[_10668], [xS]]))).
% 0.67/1.43 cnf('1.2.1.1.3',plain,[-(xS = xS)],extension(2,bind([[_10668], [xS]]))).
% 0.67/1.43 cnf('1.2.1.2',plain,[-(xS = xS)],extension(2,bind([[_10668], [xS]]))).
% 0.67/1.43 cnf('1.2.1.3',plain,[-(xS = xS)],extension(2,bind([[_10668], [xS]]))).
% 0.67/1.43 cnf('1.2.2',plain,[-(xS = sdtmndt0(sdtpldt0(xS, xx), xx)), aElement0(xx), aSet0(sdtpldt0(xS, xx)), aSet0(xS), aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], xS), aElement0(4 ^ [xS, xx, sdtpldt0(xS, xx)]), aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], sdtpldt0(xS, xx)), -(4 ^ [xS, xx, sdtpldt0(xS, xx)] = xx)],extension(16,bind([[_21609, _21335, _21427], [xS, sdtpldt0(xS, xx), xx]]))).
% 0.67/1.43 cnf('1.2.2.1',plain,[-(aElement0(xx))],extension(11)).
% 0.67/1.43 cnf('1.2.2.2',plain,[-(aSet0(sdtpldt0(xS, xx))), aElement0(xx), aSet0(xS), sdtpldt0(xS, xx) = sdtpldt0(xS, xx)],extension(8,bind([[_20653, _20383, _20473], [sdtpldt0(xS, xx), xS, xx]]))).
% 0.67/1.43 cnf('1.2.2.2.1',plain,[-(aElement0(xx))],extension(11)).
% 0.67/1.43 cnf('1.2.2.2.2',plain,[-(aSet0(xS))],extension(12)).
% 0.67/1.43 cnf('1.2.2.2.3',plain,[-(sdtpldt0(xS, xx) = sdtpldt0(xS, xx))],extension(2,bind([[_10668], [sdtpldt0(xS, xx)]]))).
% 0.67/1.43 cnf('1.2.2.3',plain,[-(aSet0(xS)), aSet0(xS), aSubsetOf0(xS, xS)],extension(6,bind([[_18077, _17973], [xS, xS]]))).
% 0.67/1.43 cnf('1.2.2.3.1',plain,[-(aSet0(xS))],extension(12)).
% 0.67/1.43 cnf('1.2.2.3.2',plain,[-(aSubsetOf0(xS, xS))],lemmata('1.2')).
% 0.67/1.43 cnf('1.2.2.4',plain,[-(aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], xS)), aElement0(xx), aSet0(xS), sdtpldt0(xS, xx) = sdtpldt0(xS, xx), aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], sdtpldt0(xS, xx)), -(4 ^ [xS, xx, sdtpldt0(xS, xx)] = xx)],extension(9,bind([[_20383, _20653, _20865, _20473], [xS, sdtpldt0(xS, xx), 4 ^ [xS, xx, sdtpldt0(xS, xx)], xx]]))).
% 0.67/1.43 cnf('1.2.2.4.1',plain,[-(aElement0(xx))],extension(11)).
% 0.67/1.43 cnf('1.2.2.4.2',plain,[-(aSet0(xS))],extension(12)).
% 0.67/1.43 cnf('1.2.2.4.3',plain,[-(sdtpldt0(xS, xx) = sdtpldt0(xS, xx))],extension(2,bind([[_10668], [sdtpldt0(xS, xx)]]))).
% 0.67/1.43 cnf('1.2.2.4.4',plain,[-(aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], sdtpldt0(xS, xx))), aElement0(xx), aSet0(sdtpldt0(xS, xx)), -(xS = sdtmndt0(sdtpldt0(xS, xx), xx)), aSet0(xS), -(aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], xS))],extension(14,bind([[_21427, _21335, _21609], [xx, sdtpldt0(xS, xx), xS]]))).
% 0.67/1.43 cnf('1.2.2.4.4.1',plain,[-(aElement0(xx))],extension(11)).
% 0.67/1.43 cnf('1.2.2.4.4.2',plain,[-(aSet0(sdtpldt0(xS, xx)))],lemmata('1.2.2')).
% 0.67/1.43 cnf('1.2.2.4.4.3',plain,[xS = sdtmndt0(sdtpldt0(xS, xx), xx)],reduction('1.2')).
% 0.67/1.43 cnf('1.2.2.4.4.4',plain,[-(aSet0(xS))],extension(12)).
% 0.67/1.43 cnf('1.2.2.4.4.5',plain,[aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], xS)],reduction('1.2.2')).
% 0.67/1.43 cnf('1.2.2.4.5',plain,[4 ^ [xS, xx, sdtpldt0(xS, xx)] = xx, aElement0(xx), aSet0(sdtpldt0(xS, xx)), -(xS = sdtmndt0(sdtpldt0(xS, xx), xx)), aSet0(xS), -(aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], xS))],extension(15,bind([[_21427, _21335, _21609], [xx, sdtpldt0(xS, xx), xS]]))).
% 0.67/1.43 cnf('1.2.2.4.5.1',plain,[-(aElement0(xx))],extension(11)).
% 0.67/1.43 cnf('1.2.2.4.5.2',plain,[-(aSet0(sdtpldt0(xS, xx)))],lemmata('1.2.2')).
% 0.67/1.43 cnf('1.2.2.4.5.3',plain,[xS = sdtmndt0(sdtpldt0(xS, xx), xx)],reduction('1.2')).
% 0.67/1.43 cnf('1.2.2.4.5.4',plain,[-(aSet0(xS))],extension(12)).
% 0.67/1.43 cnf('1.2.2.4.5.5',plain,[aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], xS)],reduction('1.2.2')).
% 0.67/1.43 cnf('1.2.2.5',plain,[-(aElement0(4 ^ [xS, xx, sdtpldt0(xS, xx)])), aSet0(xS), aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], xS)],extension(5,bind([[_16054, _15967], [4 ^ [xS, xx, sdtpldt0(xS, xx)], xS]]))).
% 0.67/1.43 cnf('1.2.2.5.1',plain,[-(aSet0(xS))],extension(12)).
% 0.67/1.43 cnf('1.2.2.5.2',plain,[-(aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], xS))],lemmata('1.2.2')).
% 0.67/1.43 cnf('1.2.2.6',plain,[-(aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], sdtpldt0(xS, xx))), aElement0(xx), aSet0(xS), sdtpldt0(xS, xx) = sdtpldt0(xS, xx), aElement0(4 ^ [xS, xx, sdtpldt0(xS, xx)]), aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], xS)],extension(10,bind([[_20653, _20473, _20865, _20383], [sdtpldt0(xS, xx), xx, 4 ^ [xS, xx, sdtpldt0(xS, xx)], xS]]))).
% 0.67/1.43 cnf('1.2.2.6.1',plain,[-(aElement0(xx))],extension(11)).
% 0.67/1.43 cnf('1.2.2.6.2',plain,[-(aSet0(xS))],extension(12)).
% 0.67/1.43 cnf('1.2.2.6.3',plain,[-(sdtpldt0(xS, xx) = sdtpldt0(xS, xx))],extension(2,bind([[_10668], [sdtpldt0(xS, xx)]]))).
% 0.67/1.43 cnf('1.2.2.6.4',plain,[-(aElement0(4 ^ [xS, xx, sdtpldt0(xS, xx)]))],lemmata('1.2.2')).
% 0.67/1.43 cnf('1.2.2.6.5',plain,[-(aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], xS))],lemmata('1.2.2')).
% 0.67/1.43 cnf('1.2.2.7',plain,[4 ^ [xS, xx, sdtpldt0(xS, xx)] = xx, -(aElementOf0(xx, xS)), aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], xS), xS = xS],extension(3,bind([[_11972, _11905, _12038, _12103], [xx, 4 ^ [xS, xx, sdtpldt0(xS, xx)], xS, xS]]))).
% 0.67/1.43 cnf('1.2.2.7.1',plain,[aElementOf0(xx, xS)],extension(13)).
% 0.67/1.43 cnf('1.2.2.7.2',plain,[-(aElementOf0(4 ^ [xS, xx, sdtpldt0(xS, xx)], xS)), aElement0(xx), aSet0(sdtpldt0(xS, xx)), -(xS = sdtmndt0(sdtpldt0(xS, xx), xx)), aSet0(xS), 4 ^ [xS, xx, sdtpldt0(xS, xx)] = xx],extension(15,bind([[_21609, _21335, _21427], [xS, sdtpldt0(xS, xx), xx]]))).
% 0.67/1.43 cnf('1.2.2.7.2.1',plain,[-(aElement0(xx))],extension(11)).
% 0.67/1.43 cnf('1.2.2.7.2.2',plain,[-(aSet0(sdtpldt0(xS, xx)))],lemmata('1.2.2')).
% 0.67/1.43 cnf('1.2.2.7.2.3',plain,[xS = sdtmndt0(sdtpldt0(xS, xx), xx)],reduction('1.2')).
% 0.67/1.43 cnf('1.2.2.7.2.4',plain,[-(aSet0(xS))],extension(12)).
% 0.67/1.43 cnf('1.2.2.7.2.5',plain,[-(4 ^ [xS, xx, sdtpldt0(xS, xx)] = xx)],reduction('1.2.2')).
% 0.67/1.43 cnf('1.2.2.7.3',plain,[-(xS = xS)],extension(2,bind([[_10668], [xS]]))).
% 0.67/1.43 cnf('1.2.3',plain,[-(xS = xS)],extension(2,bind([[_10668], [xS]]))).
% 0.67/1.43 %-----------------------------------------------------
% 0.67/1.44
% 0.67/1.44 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------