%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : NUM534+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n004.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:45 EDT 2022
% Result : Theorem 230.25s 222.06s
% Output : Proof 230.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : NUM534+1 : TPTP v8.1.0. Released v4.0.0.
% 0.06/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n004.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Thu Jul 7 12:55:37 EDT 2022
% 0.12/0.33 % CPUTime :
% 230.25/222.06 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 230.31/222.07 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 230.31/222.08
% 230.31/222.08 %-----------------------------------------------------
% 230.31/222.08 fof(mDefSub, definition, ! [_88361] : (aSet0(_88361) => ! [_88376] : (aSubsetOf0(_88376, _88361) <=> aSet0(_88376) & ! [_88401] : (aElementOf0(_88401, _88376) => aElementOf0(_88401, _88361)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mDefSub)).
% 230.31/222.08 fof(mDefDiff, definition, ! [_88637, _88640] : (aSet0(_88637) & aElement0(_88640) => ! [_88662] : (_88662 = sdtmndt0(_88637, _88640) <=> aSet0(_88662) & ! [_88690] : (aElementOf0(_88690, _88662) <=> aElement0(_88690) & aElementOf0(_88690, _88637) & (! _88690) = _88640))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mDefDiff)).
% 230.31/222.08 fof(m__617, hypothesis, aSet0(xS), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__617)).
% 230.31/222.08 fof(mDefCons, definition, ! [_89071, _89074] : (aSet0(_89071) & aElement0(_89074) => ! [_89096] : (_89096 = sdtpldt0(_89071, _89074) <=> aSet0(_89096) & ! [_89124] : (aElementOf0(_89124, _89096) <=> aElement0(_89124) & (aElementOf0(_89124, _89071) | _89124 = _89074)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mDefCons)).
% 230.31/222.08 fof(m__, conjecture, sdtpldt0(sdtmndt0(xS, xx), xx) = xS, file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__)).
% 230.31/222.08 fof(mEOfElem, axiom, ! [_89594] : (aSet0(_89594) => ! [_89609] : (aElementOf0(_89609, _89594) => aElement0(_89609))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mEOfElem)).
% 230.31/222.08 fof(mSubRefl, axiom, ! [_89817] : (aSet0(_89817) => aSubsetOf0(_89817, _89817)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mSubRefl)).
% 230.31/222.08 fof(m__617_02, hypothesis, aElementOf0(xx, xS), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__617_02)).
% 230.31/222.08
% 230.31/222.08 cnf(1, plain, [-(_10459 = _10570), _10459 = _10515, _10515 = _10570], theory(equality)).
% 230.31/222.08 cnf(2, plain, [-(6 ^ [_17332]), -(aSubsetOf0(_17436, _17332)), aSet0(_17436), 5 ^ [_17436, _17332]], clausify(mDefSub)).
% 230.31/222.08 cnf(3, plain, [-(3 ^ [_17436, _17332]), -(aSet0(_17436))], clausify(mDefSub)).
% 230.31/222.08 cnf(4, plain, [-(15 ^ [_21182, _20968, _20786, _20694]), -(aElementOf0(_21182, _20694))], clausify(mDefDiff)).
% 230.31/222.08 cnf(5, plain, [-(aSet0(xS))], clausify(m__617)).
% 230.31/222.08 cnf(6, plain, [-(5 ^ [_17436, _17332]), aElementOf0(4 ^ [_17436, _17332], _17332)], clausify(mDefSub)).
% 230.31/222.08 cnf(7, plain, [-(16 ^ [_20968, _20786, _20694]), -(aElementOf0(_21182, _20968)), aElement0(_21182), aElementOf0(_21182, _20694), -(_21182 = _20786)], clausify(mDefDiff)).
% 230.31/222.08 cnf(8, plain, [-(14 ^ [_19832, _19742]), -(_20012 = sdtpldt0(_19742, _19832)), aSet0(_20012), 12 ^ [_20012, _19832, _19742], 13 ^ [_20012, _19832, _19742]], clausify(mDefCons)).
% 230.31/222.08 cnf(9, plain, [-(11 ^ [_20012, _19832, _19742]), aElementOf0(10 ^ [_20012, _19832, _19742], _19742)], clausify(mDefCons)).
% 230.31/222.08 cnf(10, plain, [sdtpldt0(sdtmndt0(xS, xx), xx) = xS], clausify(m__)).
% 230.31/222.08 cnf(11, plain, [-(12 ^ [_20012, _19832, _19742]), aElement0(10 ^ [_20012, _19832, _19742]), 11 ^ [_20012, _19832, _19742]], clausify(mDefCons)).
% 230.31/222.08 cnf(12, plain, [aElement0(_19832), aSet0(_19742), 14 ^ [_19832, _19742]], clausify(mDefCons)).
% 230.31/222.08 cnf(13, plain, [-(6 ^ [_17332]), aSubsetOf0(_17436, _17332), 3 ^ [_17436, _17332]], clausify(mDefSub)).
% 230.31/222.08 cnf(14, plain, [-(aSubsetOf0(_12284, _12415)), aSubsetOf0(_12217, _12350), _12217 = _12284, _12350 = _12415], theory(equality)).
% 230.31/222.08 cnf(15, plain, [-(16 ^ [_20968, _20786, _20694]), -(aSet0(_20968))], clausify(mDefDiff)).
% 230.31/222.08 cnf(16, plain, [-(_10027 = _10027)], theory(equality)).
% 230.31/222.08 cnf(17, plain, [-(5 ^ [_17436, _17332]), -(aElementOf0(4 ^ [_17436, _17332], _17436))], clausify(mDefSub)).
% 230.31/222.08 cnf(18, plain, [-(15 ^ [_21182, _20968, _20786, _20694]), _21182 = _20786], clausify(mDefDiff)).
% 230.31/222.08 cnf(19, plain, [aSet0(_15326), aElementOf0(_15413, _15326), -(aElement0(_15413))], clausify(mEOfElem)).
% 230.31/222.08 cnf(20, plain, [-(16 ^ [_20968, _20786, _20694]), aElementOf0(_21182, _20968), 15 ^ [_21182, _20968, _20786, _20694]], clausify(mDefDiff)).
% 230.31/222.08 cnf(21, plain, [aSet0(_17332), 6 ^ [_17332]], clausify(mDefSub)).
% 230.31/222.08 cnf(22, plain, [-(13 ^ [_20012, _19832, _19742]), -(aElementOf0(10 ^ [_20012, _19832, _19742], _19742)), -(10 ^ [_20012, _19832, _19742] = _19832)], clausify(mDefCons)).
% 230.31/222.08 cnf(23, plain, [aSet0(_18317), -(aSubsetOf0(_18317, _18317))], clausify(mSubRefl)).
% 230.31/222.08 cnf(24, plain, [-(11 ^ [_20012, _19832, _19742]), 10 ^ [_20012, _19832, _19742] = _19832], clausify(mDefCons)).
% 230.31/222.08 cnf(25, plain, [-(12 ^ [_20012, _19832, _19742]), -(aElementOf0(10 ^ [_20012, _19832, _19742], _20012))], clausify(mDefCons)).
% 230.31/222.08 cnf(26, plain, [_10180 = _10225, -(_10225 = _10180)], theory(equality)).
% 230.31/222.08 cnf(27, plain, [-(aElementOf0(_11331, _11462)), aElementOf0(_11264, _11397), _11264 = _11331, _11397 = _11462], theory(equality)).
% 230.31/222.08 cnf(28, plain, [-(aElementOf0(xx, xS))], clausify(m__617_02)).
% 230.31/222.08 cnf(29, plain, [aElement0(_20786), aSet0(_20694), 20 ^ [_20786, _20694]], clausify(mDefDiff)).
% 230.31/222.08 cnf(30, plain, [-(aElement0(_10984)), _10935 = _10984, aElement0(_10935)], theory(equality)).
% 230.31/222.08 cnf(31, plain, [-(13 ^ [_20012, _19832, _19742]), aElementOf0(10 ^ [_20012, _19832, _19742], _20012)], clausify(mDefCons)).
% 230.31/222.08 cnf(32, plain, [-(20 ^ [_20786, _20694]), _20968 = sdtmndt0(_20694, _20786), 16 ^ [_20968, _20786, _20694]], clausify(mDefDiff)).
% 230.31/222.08
% 230.31/222.08 cnf('1',plain,[sdtpldt0(sdtmndt0(xS, xx), xx) = xS],start(10)).
% 230.31/222.08 cnf('1.1',plain,[-(sdtpldt0(sdtmndt0(xS, xx), xx) = xS), xS = sdtpldt0(sdtmndt0(xS, xx), xx)],extension(26,bind([[_10180, _10225], [xS, sdtpldt0(sdtmndt0(xS, xx), xx)]]))).
% 230.31/222.08 cnf('1.1.1',plain,[-(xS = sdtpldt0(sdtmndt0(xS, xx), xx)), -(14 ^ [xx, sdtmndt0(xS, xx)]), aSet0(xS), 12 ^ [xS, xx, sdtmndt0(xS, xx)], 13 ^ [xS, xx, sdtmndt0(xS, xx)]],extension(8,bind([[_20012, _19832, _19742], [xS, xx, sdtmndt0(xS, xx)]]))).
% 230.31/222.08 cnf('1.1.1.1',plain,[14 ^ [xx, sdtmndt0(xS, xx)], aElement0(xx), aSet0(sdtmndt0(xS, xx))],extension(12,bind([[_19832, _19742], [xx, sdtmndt0(xS, xx)]]))).
% 230.31/222.08 cnf('1.1.1.1.1',plain,[-(aElement0(xx)), aSet0(xS), aElementOf0(xx, xS)],extension(19,bind([[_15413, _15326], [xx, xS]]))).
% 230.31/222.08 cnf('1.1.1.1.1.1',plain,[-(aSet0(xS)), -(3 ^ [xS, xS])],extension(3,bind([[_17436, _17332], [xS, xS]]))).
% 230.31/222.08 cnf('1.1.1.1.1.1.1',plain,[3 ^ [xS, xS], -(6 ^ [xS]), aSubsetOf0(xS, xS)],extension(13,bind([[_17436, _17332], [xS, xS]]))).
% 230.31/222.08 cnf('1.1.1.1.1.1.1.1',plain,[6 ^ [xS], aSet0(xS)],extension(21,bind([[_17332], [xS]]))).
% 230.31/222.08 cnf('1.1.1.1.1.1.1.1.1',plain,[-(aSet0(xS))],extension(5)).
% 230.31/222.08 cnf('1.1.1.1.1.1.1.2',plain,[-(aSubsetOf0(xS, xS)), aSubsetOf0(xS, xS), xS = xS, xS = xS],extension(14,bind([[_12217, _12284, _12350, _12415], [xS, xS, xS, xS]]))).
% 230.31/222.08 cnf('1.1.1.1.1.1.1.2.1',plain,[-(aSubsetOf0(xS, xS)), aSet0(xS)],extension(23,bind([[_18317], [xS]]))).
% 230.31/222.08 cnf('1.1.1.1.1.1.1.2.1.1',plain,[-(aSet0(xS))],extension(5)).
% 230.31/222.08 cnf('1.1.1.1.1.1.1.2.2',plain,[-(xS = xS)],extension(16,bind([[_10027], [xS]]))).
% 230.31/222.08 cnf('1.1.1.1.1.1.1.2.3',plain,[-(xS = xS)],extension(16,bind([[_10027], [xS]]))).
% 230.31/222.08 cnf('1.1.1.1.1.2',plain,[-(aElementOf0(xx, xS))],extension(28)).
% 230.31/222.08 cnf('1.1.1.1.2',plain,[-(aSet0(sdtmndt0(xS, xx))), -(16 ^ [sdtmndt0(xS, xx), xx, xS])],extension(15,bind([[_20968, _20786, _20694], [sdtmndt0(xS, xx), xx, xS]]))).
% 230.31/222.08 cnf('1.1.1.1.2.1',plain,[16 ^ [sdtmndt0(xS, xx), xx, xS], -(20 ^ [xx, xS]), sdtmndt0(xS, xx) = sdtmndt0(xS, xx)],extension(32,bind([[_20968, _20694, _20786], [sdtmndt0(xS, xx), xS, xx]]))).
% 230.31/222.08 cnf('1.1.1.1.2.1.1',plain,[20 ^ [xx, xS], aElement0(xx), aSet0(xS)],extension(29,bind([[_20786, _20694], [xx, xS]]))).
% 230.31/222.08 cnf('1.1.1.1.2.1.1.1',plain,[-(aElement0(xx)), aSet0(xS), aElementOf0(xx, xS)],extension(19,bind([[_15413, _15326], [xx, xS]]))).
% 230.31/222.08 cnf('1.1.1.1.2.1.1.1.1',plain,[-(aSet0(xS))],extension(5)).
% 230.31/222.08 cnf('1.1.1.1.2.1.1.1.2',plain,[-(aElementOf0(xx, xS))],extension(28)).
% 230.31/222.08 cnf('1.1.1.1.2.1.1.2',plain,[-(aSet0(xS))],extension(5)).
% 230.31/222.08 cnf('1.1.1.1.2.1.2',plain,[-(sdtmndt0(xS, xx) = sdtmndt0(xS, xx))],extension(16,bind([[_10027], [sdtmndt0(xS, xx)]]))).
% 230.31/222.08 cnf('1.1.1.2',plain,[-(aSet0(xS)), -(3 ^ [xS, xS])],extension(3,bind([[_17436, _17332], [xS, xS]]))).
% 230.31/222.08 cnf('1.1.1.2.1',plain,[3 ^ [xS, xS], -(6 ^ [xS]), aSubsetOf0(xS, xS)],extension(13,bind([[_17436, _17332], [xS, xS]]))).
% 230.31/222.08 cnf('1.1.1.2.1.1',plain,[6 ^ [xS], aSet0(xS)],extension(21,bind([[_17332], [xS]]))).
% 230.31/222.08 cnf('1.1.1.2.1.1.1',plain,[-(aSet0(xS))],extension(5)).
% 230.31/222.08 cnf('1.1.1.2.1.2',plain,[-(aSubsetOf0(xS, xS)), aSubsetOf0(xS, xS), xS = xS, xS = xS],extension(14,bind([[_12217, _12284, _12350, _12415], [xS, xS, xS, xS]]))).
% 230.31/222.08 cnf('1.1.1.2.1.2.1',plain,[-(aSubsetOf0(xS, xS)), -(6 ^ [xS]), aSet0(xS), 5 ^ [xS, xS]],extension(2,bind([[_17436, _17332], [xS, xS]]))).
% 230.31/222.08 cnf('1.1.1.2.1.2.1.1',plain,[6 ^ [xS], aSet0(xS)],extension(21,bind([[_17332], [xS]]))).
% 230.31/222.08 cnf('1.1.1.2.1.2.1.1.1',plain,[-(aSet0(xS))],extension(5)).
% 230.31/222.08 cnf('1.1.1.2.1.2.1.2',plain,[-(aSet0(xS))],extension(5)).
% 230.31/222.08 cnf('1.1.1.2.1.2.1.3',plain,[-(5 ^ [xS, xS]), aElementOf0(4 ^ [xS, xS], xS)],extension(6,bind([[_17436, _17332], [xS, xS]]))).
% 230.31/222.08 cnf('1.1.1.2.1.2.1.3.1',plain,[-(aElementOf0(4 ^ [xS, xS], xS)), -(5 ^ [xS, xS])],extension(17,bind([[_17436, _17332], [xS, xS]]))).
% 230.31/222.08 cnf('1.1.1.2.1.2.1.3.1.1',plain,[5 ^ [xS, xS]],reduction('1.1.1.2.1.2.1')).
% 230.31/222.08 cnf('1.1.1.2.1.2.2',plain,[-(xS = xS)],extension(16,bind([[_10027], [xS]]))).
% 230.31/222.08 cnf('1.1.1.2.1.2.3',plain,[-(xS = xS)],extension(16,bind([[_10027], [xS]]))).
% 230.31/222.08 cnf('1.1.1.3',plain,[-(12 ^ [xS, xx, sdtmndt0(xS, xx)]), aElement0(10 ^ [xS, xx, sdtmndt0(xS, xx)]), 11 ^ [xS, xx, sdtmndt0(xS, xx)]],extension(11,bind([[_20012, _19832, _19742], [xS, xx, sdtmndt0(xS, xx)]]))).
% 230.31/222.08 cnf('1.1.1.3.1',plain,[-(aElement0(10 ^ [xS, xx, sdtmndt0(xS, xx)])), aSet0(xS), aElementOf0(10 ^ [xS, xx, sdtmndt0(xS, xx)], xS)],extension(19,bind([[_15413, _15326], [10 ^ [xS, xx, sdtmndt0(xS, xx)], xS]]))).
% 230.31/222.08 cnf('1.1.1.3.1.1',plain,[-(aSet0(xS)), -(3 ^ [xS, xS])],extension(3,bind([[_17436, _17332], [xS, xS]]))).
% 230.31/222.08 cnf('1.1.1.3.1.1.1',plain,[3 ^ [xS, xS], -(6 ^ [xS]), aSubsetOf0(xS, xS)],extension(13,bind([[_17436, _17332], [xS, xS]]))).
% 230.31/222.08 cnf('1.1.1.3.1.1.1.1',plain,[6 ^ [xS], aSet0(xS)],extension(21,bind([[_17332], [xS]]))).
% 230.31/222.08 cnf('1.1.1.3.1.1.1.1.1',plain,[-(aSet0(xS))],extension(5)).
% 230.31/222.08 cnf('1.1.1.3.1.1.1.2',plain,[-(aSubsetOf0(xS, xS)), aSubsetOf0(xS, xS), xS = xS, xS = xS],extension(14,bind([[_12217, _12284, _12350, _12415], [xS, xS, xS, xS]]))).
% 230.31/222.08 cnf('1.1.1.3.1.1.1.2.1',plain,[-(aSubsetOf0(xS, xS)), aSet0(xS)],extension(23,bind([[_18317], [xS]]))).
% 230.31/222.08 cnf('1.1.1.3.1.1.1.2.1.1',plain,[-(aSet0(xS))],extension(5)).
% 230.31/222.08 cnf('1.1.1.3.1.1.1.2.2',plain,[-(xS = xS)],extension(16,bind([[_10027], [xS]]))).
% 230.31/222.08 cnf('1.1.1.3.1.1.1.2.3',plain,[-(xS = xS)],extension(16,bind([[_10027], [xS]]))).
% 230.31/222.08 cnf('1.1.1.3.1.2',plain,[-(aElementOf0(10 ^ [xS, xx, sdtmndt0(xS, xx)], xS)), -(12 ^ [xS, xx, sdtmndt0(xS, xx)])],extension(25,bind([[_20012, _19832, _19742], [xS, xx, sdtmndt0(xS, xx)]]))).
% 230.31/222.08 cnf('1.1.1.3.1.2.1',plain,[12 ^ [xS, xx, sdtmndt0(xS, xx)]],reduction('1.1.1')).
% 230.31/222.08 cnf('1.1.1.3.2',plain,[-(11 ^ [xS, xx, sdtmndt0(xS, xx)]), aElementOf0(10 ^ [xS, xx, sdtmndt0(xS, xx)], sdtmndt0(xS, xx))],extension(9,bind([[_20012, _19832, _19742], [xS, xx, sdtmndt0(xS, xx)]]))).
% 230.31/222.08 cnf('1.1.1.3.2.1',plain,[-(aElementOf0(10 ^ [xS, xx, sdtmndt0(xS, xx)], sdtmndt0(xS, xx))), -(16 ^ [sdtmndt0(xS, xx), xx, xS]), aElement0(10 ^ [xS, xx, sdtmndt0(xS, xx)]), aElementOf0(10 ^ [xS, xx, sdtmndt0(xS, xx)], xS), -(10 ^ [xS, xx, sdtmndt0(xS, xx)] = xx)],extension(7,bind([[_20968, _20694, _21182, _20786], [sdtmndt0(xS, xx), xS, 10 ^ [xS, xx, sdtmndt0(xS, xx)], xx]]))).
% 230.31/222.08 cnf('1.1.1.3.2.1.1',plain,[16 ^ [sdtmndt0(xS, xx), xx, xS], -(20 ^ [xx, xS]), sdtmndt0(xS, xx) = sdtmndt0(xS, xx)],extension(32,bind([[_20968, _20694, _20786], [sdtmndt0(xS, xx), xS, xx]]))).
% 230.31/222.08 cnf('1.1.1.3.2.1.1.1',plain,[20 ^ [xx, xS], aElement0(xx), aSet0(xS)],extension(29,bind([[_20786, _20694], [xx, xS]]))).
% 230.31/222.08 cnf('1.1.1.3.2.1.1.1.1',plain,[-(aElement0(xx)), aSet0(xS), aElementOf0(xx, xS)],extension(19,bind([[_15413, _15326], [xx, xS]]))).
% 230.31/222.08 cnf('1.1.1.3.2.1.1.1.1.1',plain,[-(aSet0(xS))],extension(5)).
% 230.31/222.08 cnf('1.1.1.3.2.1.1.1.1.2',plain,[-(aElementOf0(xx, xS))],extension(28)).
% 230.31/222.08 cnf('1.1.1.3.2.1.1.1.2',plain,[-(aSet0(xS))],extension(5)).
% 230.31/222.08 cnf('1.1.1.3.2.1.1.2',plain,[-(sdtmndt0(xS, xx) = sdtmndt0(xS, xx))],extension(16,bind([[_10027], [sdtmndt0(xS, xx)]]))).
% 230.31/222.08 cnf('1.1.1.3.2.1.2',plain,[-(aElement0(10 ^ [xS, xx, sdtmndt0(xS, xx)]))],lemmata('1.1.1.3')).
% 230.31/222.08 cnf('1.1.1.3.2.1.3',plain,[-(aElementOf0(10 ^ [xS, xx, sdtmndt0(xS, xx)], xS)), -(12 ^ [xS, xx, sdtmndt0(xS, xx)])],extension(25,bind([[_20012, _19832, _19742], [xS, xx, sdtmndt0(xS, xx)]]))).
% 230.31/222.08 cnf('1.1.1.3.2.1.3.1',plain,[12 ^ [xS, xx, sdtmndt0(xS, xx)]],reduction('1.1.1')).
% 230.31/222.08 cnf('1.1.1.3.2.1.4',plain,[10 ^ [xS, xx, sdtmndt0(xS, xx)] = xx, -(10 ^ [xS, xx, sdtmndt0(xS, xx)] = 10 ^ [xS, xx, sdtmndt0(xS, xx)]), xx = 10 ^ [xS, xx, sdtmndt0(xS, xx)]],extension(1,bind([[_10459, _10515, _10570], [10 ^ [xS, xx, sdtmndt0(xS, xx)], xx, 10 ^ [xS, xx, sdtmndt0(xS, xx)]]]))).
% 230.31/222.08 cnf('1.1.1.3.2.1.4.1',plain,[10 ^ [xS, xx, sdtmndt0(xS, xx)] = 10 ^ [xS, xx, sdtmndt0(xS, xx)], -(10 ^ [xS, xx, sdtmndt0(xS, xx)] = xx), 10 ^ [xS, xx, sdtmndt0(xS, xx)] = xx],extension(1,bind([[_10459, _10515, _10570], [10 ^ [xS, xx, sdtmndt0(xS, xx)], 10 ^ [xS, xx, sdtmndt0(xS, xx)], xx]]))).
% 230.31/222.08 cnf('1.1.1.3.2.1.4.1.1',plain,[10 ^ [xS, xx, sdtmndt0(xS, xx)] = xx, -(11 ^ [xS, xx, sdtmndt0(xS, xx)])],extension(24,bind([[_20012, _19832, _19742], [xS, xx, sdtmndt0(xS, xx)]]))).
% 230.31/222.08 cnf('1.1.1.3.2.1.4.1.1.1',plain,[11 ^ [xS, xx, sdtmndt0(xS, xx)]],reduction('1.1.1.3')).
% 230.31/222.08 cnf('1.1.1.3.2.1.4.1.2',plain,[-(10 ^ [xS, xx, sdtmndt0(xS, xx)] = xx)],reduction('1.1.1.3.2.1')).
% 230.31/222.08 cnf('1.1.1.3.2.1.4.2',plain,[-(xx = 10 ^ [xS, xx, sdtmndt0(xS, xx)]), 10 ^ [xS, xx, sdtmndt0(xS, xx)] = xx],extension(26,bind([[_10180, _10225], [10 ^ [xS, xx, sdtmndt0(xS, xx)], xx]]))).
% 230.31/222.08 cnf('1.1.1.3.2.1.4.2.1',plain,[-(10 ^ [xS, xx, sdtmndt0(xS, xx)] = xx)],reduction('1.1.1.3.2.1')).
% 230.31/222.08 cnf('1.1.1.4',plain,[-(13 ^ [xS, xx, sdtmndt0(xS, xx)]), -(aElementOf0(10 ^ [xS, xx, sdtmndt0(xS, xx)], sdtmndt0(xS, xx))), -(10 ^ [xS, xx, sdtmndt0(xS, xx)] = xx)],extension(22,bind([[_20012, _19742, _19832], [xS, sdtmndt0(xS, xx), xx]]))).
% 230.31/222.08 cnf('1.1.1.4.1',plain,[aElementOf0(10 ^ [xS, xx, sdtmndt0(xS, xx)], sdtmndt0(xS, xx)), -(16 ^ [sdtmndt0(xS, xx), xx, xS]), 15 ^ [10 ^ [xS, xx, sdtmndt0(xS, xx)], sdtmndt0(xS, xx), xx, xS]],extension(20,bind([[_21182, _20968, _20786, _20694], [10 ^ [xS, xx, sdtmndt0(xS, xx)], sdtmndt0(xS, xx), xx, xS]]))).
% 230.31/222.08 cnf('1.1.1.4.1.1',plain,[16 ^ [sdtmndt0(xS, xx), xx, xS], -(20 ^ [xx, xS]), sdtmndt0(xS, xx) = sdtmndt0(xS, xx)],extension(32,bind([[_20968, _20694, _20786], [sdtmndt0(xS, xx), xS, xx]]))).
% 230.31/222.08 cnf('1.1.1.4.1.1.1',plain,[20 ^ [xx, xS], aElement0(xx), aSet0(xS)],extension(29,bind([[_20786, _20694], [xx, xS]]))).
% 230.31/222.08 cnf('1.1.1.4.1.1.1.1',plain,[-(aElement0(xx)), aSet0(xS), aElementOf0(xx, xS)],extension(19,bind([[_15413, _15326], [xx, xS]]))).
% 230.31/222.08 cnf('1.1.1.4.1.1.1.1.1',plain,[-(aSet0(xS))],extension(5)).
% 230.31/222.08 cnf('1.1.1.4.1.1.1.1.2',plain,[-(aElementOf0(xx, xS))],extension(28)).
% 230.31/222.08 cnf('1.1.1.4.1.1.1.2',plain,[-(aSet0(xS))],extension(5)).
% 230.31/222.08 cnf('1.1.1.4.1.1.2',plain,[-(sdtmndt0(xS, xx) = sdtmndt0(xS, xx))],extension(16,bind([[_10027], [sdtmndt0(xS, xx)]]))).
% 230.31/222.08 cnf('1.1.1.4.1.2',plain,[-(15 ^ [10 ^ [xS, xx, sdtmndt0(xS, xx)], sdtmndt0(xS, xx), xx, xS]), -(aElementOf0(10 ^ [xS, xx, sdtmndt0(xS, xx)], xS))],extension(4,bind([[_20968, _20786, _21182, _20694], [sdtmndt0(xS, xx), xx, 10 ^ [xS, xx, sdtmndt0(xS, xx)], xS]]))).
% 230.31/222.08 cnf('1.1.1.4.1.2.1',plain,[aElementOf0(10 ^ [xS, xx, sdtmndt0(xS, xx)], xS), -(aElementOf0(10 ^ [xS, xx, sdtmndt0(xS, xx)], xS)), 10 ^ [xS, xx, sdtmndt0(xS, xx)] = 10 ^ [xS, xx, sdtmndt0(xS, xx)], xS = xS],extension(27,bind([[_11264, _11331, _11397, _11462], [10 ^ [xS, xx, sdtmndt0(xS, xx)], 10 ^ [xS, xx, sdtmndt0(xS, xx)], xS, xS]]))).
% 230.31/222.08 cnf('1.1.1.4.1.2.1.1',plain,[aElementOf0(10 ^ [xS, xx, sdtmndt0(xS, xx)], xS), -(aElementOf0(10 ^ [xS, xx, sdtmndt0(xS, xx)], xS)), 10 ^ [xS, xx, sdtmndt0(xS, xx)] = 10 ^ [xS, xx, sdtmndt0(xS, xx)], xS = xS],extension(27,bind([[_11264, _11331, _11397, _11462], [10 ^ [xS, xx, sdtmndt0(xS, xx)], 10 ^ [xS, xx, sdtmndt0(xS, xx)], xS, xS]]))).
% 230.31/222.08 cnf('1.1.1.4.1.2.1.1.1',plain,[aElementOf0(10 ^ [xS, xx, sdtmndt0(xS, xx)], xS), -(13 ^ [xS, xx, sdtmndt0(xS, xx)])],extension(31,bind([[_20012, _19832, _19742], [xS, xx, sdtmndt0(xS, xx)]]))).
% 230.31/222.08 cnf('1.1.1.4.1.2.1.1.1.1',plain,[13 ^ [xS, xx, sdtmndt0(xS, xx)]],reduction('1.1.1')).
% 230.31/222.08 cnf('1.1.1.4.1.2.1.1.2',plain,[-(10 ^ [xS, xx, sdtmndt0(xS, xx)] = 10 ^ [xS, xx, sdtmndt0(xS, xx)])],extension(16,bind([[_10027], [10 ^ [xS, xx, sdtmndt0(xS, xx)]]]))).
% 230.31/222.08 cnf('1.1.1.4.1.2.1.1.3',plain,[-(xS = xS)],extension(16,bind([[_10027], [xS]]))).
% 230.31/222.08 cnf('1.1.1.4.1.2.1.2',plain,[-(10 ^ [xS, xx, sdtmndt0(xS, xx)] = 10 ^ [xS, xx, sdtmndt0(xS, xx)])],extension(16,bind([[_10027], [10 ^ [xS, xx, sdtmndt0(xS, xx)]]]))).
% 230.31/222.08 cnf('1.1.1.4.1.2.1.3',plain,[-(xS = xS)],extension(16,bind([[_10027], [xS]]))).
% 230.31/222.08 cnf('1.1.1.4.2',plain,[10 ^ [xS, xx, sdtmndt0(xS, xx)] = xx, -(aElement0(xx)), aElement0(10 ^ [xS, xx, sdtmndt0(xS, xx)])],extension(30,bind([[_10984, _10935], [xx, 10 ^ [xS, xx, sdtmndt0(xS, xx)]]]))).
% 230.31/222.08 cnf('1.1.1.4.2.1',plain,[aElement0(xx), -(16 ^ [sdtmndt0(xS, xx), xx, xS]), -(aElementOf0(xx, sdtmndt0(xS, xx))), aElementOf0(xx, xS), -(xx = xx)],extension(7,bind([[_20968, _20694, _21182, _20786], [sdtmndt0(xS, xx), xS, xx, xx]]))).
% 230.31/222.08 cnf('1.1.1.4.2.1.1',plain,[16 ^ [sdtmndt0(xS, xx), xx, xS], -(20 ^ [xx, xS]), sdtmndt0(xS, xx) = sdtmndt0(xS, xx)],extension(32,bind([[_20968, _20694, _20786], [sdtmndt0(xS, xx), xS, xx]]))).
% 230.31/222.08 cnf('1.1.1.4.2.1.1.1',plain,[20 ^ [xx, xS], aElement0(xx), aSet0(xS)],extension(29,bind([[_20786, _20694], [xx, xS]]))).
% 230.31/222.08 cnf('1.1.1.4.2.1.1.1.1',plain,[-(aElement0(xx))],reduction('1.1.1.4.2')).
% 230.31/222.08 cnf('1.1.1.4.2.1.1.1.2',plain,[-(aSet0(xS))],extension(5)).
% 230.31/222.08 cnf('1.1.1.4.2.1.1.2',plain,[-(sdtmndt0(xS, xx) = sdtmndt0(xS, xx))],extension(16,bind([[_10027], [sdtmndt0(xS, xx)]]))).
% 230.31/222.08 cnf('1.1.1.4.2.1.2',plain,[aElementOf0(xx, sdtmndt0(xS, xx)), -(16 ^ [sdtmndt0(xS, xx), xx, xS]), 15 ^ [xx, sdtmndt0(xS, xx), xx, xS]],extension(20,bind([[_21182, _20968, _20786, _20694], [xx, sdtmndt0(xS, xx), xx, xS]]))).
% 230.31/222.08 cnf('1.1.1.4.2.1.2.1',plain,[16 ^ [sdtmndt0(xS, xx), xx, xS], -(20 ^ [xx, xS]), sdtmndt0(xS, xx) = sdtmndt0(xS, xx)],extension(32,bind([[_20968, _20694, _20786], [sdtmndt0(xS, xx), xS, xx]]))).
% 230.31/222.08 cnf('1.1.1.4.2.1.2.1.1',plain,[20 ^ [xx, xS], aElement0(xx), aSet0(xS)],extension(29,bind([[_20786, _20694], [xx, xS]]))).
% 230.31/222.08 cnf('1.1.1.4.2.1.2.1.1.1',plain,[-(aElement0(xx))],reduction('1.1.1.4.2')).
% 230.31/222.08 cnf('1.1.1.4.2.1.2.1.1.2',plain,[-(aSet0(xS))],extension(5)).
% 230.31/222.08 cnf('1.1.1.4.2.1.2.1.2',plain,[-(sdtmndt0(xS, xx) = sdtmndt0(xS, xx))],extension(16,bind([[_10027], [sdtmndt0(xS, xx)]]))).
% 230.31/222.08 cnf('1.1.1.4.2.1.2.2',plain,[-(15 ^ [xx, sdtmndt0(xS, xx), xx, xS]), xx = xx],extension(18,bind([[_20968, _20694, _21182, _20786], [sdtmndt0(xS, xx), xS, xx, xx]]))).
% 230.31/222.08 cnf('1.1.1.4.2.1.2.2.1',plain,[-(xx = xx)],extension(16,bind([[_10027], [xx]]))).
% 230.31/222.08 cnf('1.1.1.4.2.1.3',plain,[-(aElementOf0(xx, xS)), aElementOf0(xx, xS), xx = xx, xS = xS],extension(27,bind([[_11264, _11331, _11397, _11462], [xx, xx, xS, xS]]))).
% 230.31/222.08 cnf('1.1.1.4.2.1.3.1',plain,[-(aElementOf0(xx, xS)), aElementOf0(xx, xS), xx = xx, xS = xS],extension(27,bind([[_11264, _11331, _11397, _11462], [xx, xx, xS, xS]]))).
% 230.31/222.08 cnf('1.1.1.4.2.1.3.1.1',plain,[-(aElementOf0(xx, xS))],extension(28)).
% 230.31/222.08 cnf('1.1.1.4.2.1.3.1.2',plain,[-(xx = xx)],extension(16,bind([[_10027], [xx]]))).
% 230.31/222.08 cnf('1.1.1.4.2.1.3.1.3',plain,[-(xS = xS)],extension(16,bind([[_10027], [xS]]))).
% 230.31/222.08 cnf('1.1.1.4.2.1.3.2',plain,[-(xx = xx)],extension(16,bind([[_10027], [xx]]))).
% 230.31/222.08 cnf('1.1.1.4.2.1.3.3',plain,[-(xS = xS)],extension(16,bind([[_10027], [xS]]))).
% 230.31/222.08 cnf('1.1.1.4.2.1.4',plain,[xx = xx, -(xx = 10 ^ [xS, xx, sdtmndt0(xS, xx)]), xx = 10 ^ [xS, xx, sdtmndt0(xS, xx)]],extension(1,bind([[_10459, _10515, _10570], [xx, xx, 10 ^ [xS, xx, sdtmndt0(xS, xx)]]]))).
% 230.31/222.08 cnf('1.1.1.4.2.1.4.1',plain,[xx = 10 ^ [xS, xx, sdtmndt0(xS, xx)], -(aElementOf0(10 ^ [xS, xx, sdtmndt0(xS, xx)], xS)), aElementOf0(xx, xS), xS = xS],extension(27,bind([[_11331, _11264, _11397, _11462], [10 ^ [xS, xx, sdtmndt0(xS, xx)], xx, xS, xS]]))).
% 230.31/222.08 cnf('1.1.1.4.2.1.4.1.1',plain,[aElementOf0(10 ^ [xS, xx, sdtmndt0(xS, xx)], xS), -(13 ^ [xS, xx, sdtmndt0(xS, xx)])],extension(31,bind([[_20012, _19832, _19742], [xS, xx, sdtmndt0(xS, xx)]]))).
% 230.31/222.08 cnf('1.1.1.4.2.1.4.1.1.1',plain,[13 ^ [xS, xx, sdtmndt0(xS, xx)]],reduction('1.1.1')).
% 230.31/222.08 cnf('1.1.1.4.2.1.4.1.2',plain,[-(aElementOf0(xx, xS))],extension(28)).
% 230.31/222.08 cnf('1.1.1.4.2.1.4.1.3',plain,[-(xS = xS)],extension(16,bind([[_10027], [xS]]))).
% 230.31/222.08 cnf('1.1.1.4.2.1.4.2',plain,[-(xx = 10 ^ [xS, xx, sdtmndt0(xS, xx)]), 10 ^ [xS, xx, sdtmndt0(xS, xx)] = xx],extension(26,bind([[_10180, _10225], [10 ^ [xS, xx, sdtmndt0(xS, xx)], xx]]))).
% 230.31/222.08 cnf('1.1.1.4.2.1.4.2.1',plain,[-(10 ^ [xS, xx, sdtmndt0(xS, xx)] = xx)],reduction('1.1.1.4')).
% 230.31/222.08 cnf('1.1.1.4.2.2',plain,[-(aElement0(10 ^ [xS, xx, sdtmndt0(xS, xx)])), aSet0(xS), aElementOf0(10 ^ [xS, xx, sdtmndt0(xS, xx)], xS)],extension(19,bind([[_15413, _15326], [10 ^ [xS, xx, sdtmndt0(xS, xx)], xS]]))).
% 230.31/222.08 cnf('1.1.1.4.2.2.1',plain,[-(aSet0(xS))],extension(5)).
% 230.31/222.08 cnf('1.1.1.4.2.2.2',plain,[-(aElementOf0(10 ^ [xS, xx, sdtmndt0(xS, xx)], xS)), aElementOf0(xx, xS), xx = 10 ^ [xS, xx, sdtmndt0(xS, xx)], xS = xS],extension(27,bind([[_11264, _11331, _11397, _11462], [xx, 10 ^ [xS, xx, sdtmndt0(xS, xx)], xS, xS]]))).
% 230.31/222.08 cnf('1.1.1.4.2.2.2.1',plain,[-(aElementOf0(xx, xS)), aElementOf0(xx, xS), xx = xx, xS = xS],extension(27,bind([[_11264, _11331, _11397, _11462], [xx, xx, xS, xS]]))).
% 230.31/222.08 cnf('1.1.1.4.2.2.2.1.1',plain,[-(aElementOf0(xx, xS))],extension(28)).
% 230.31/222.08 cnf('1.1.1.4.2.2.2.1.2',plain,[-(xx = xx)],extension(16,bind([[_10027], [xx]]))).
% 230.31/222.08 cnf('1.1.1.4.2.2.2.1.3',plain,[-(xS = xS)],extension(16,bind([[_10027], [xS]]))).
% 230.31/222.08 cnf('1.1.1.4.2.2.2.2',plain,[-(xx = 10 ^ [xS, xx, sdtmndt0(xS, xx)]), 10 ^ [xS, xx, sdtmndt0(xS, xx)] = xx],extension(26,bind([[_10180, _10225], [10 ^ [xS, xx, sdtmndt0(xS, xx)], xx]]))).
% 230.31/222.08 cnf('1.1.1.4.2.2.2.2.1',plain,[-(10 ^ [xS, xx, sdtmndt0(xS, xx)] = xx)],reduction('1.1.1.4')).
% 230.31/222.08 cnf('1.1.1.4.2.2.2.3',plain,[-(xS = xS)],extension(16,bind([[_10027], [xS]]))).
% 230.31/222.08 %-----------------------------------------------------
% 230.31/222.08
% 230.31/222.08 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------