%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM544+2 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n001.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 : 300s
% DateTime : Fri May 19 11:44:57 EDT 2023
% Result : Theorem 0.81s 1.37s
% Output : Proof 0.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : NUM544+2 : TPTP v8.1.2. Released v4.0.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n001.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 : 300
% 0.12/0.33 % DateTime : Thu May 18 17:03:49 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.81/1.37
% 0.81/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.81/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.81/1.37 %-----------------------------------------------------
% 0.81/1.37 ncf(matrix, plain, [(1080 ^ _124723) ^ [] : [-(aElementOf0(1078 ^ [], xS))], (1082 ^ _124723) ^ [] : [xS = slcrc0], (1084 ^ _124723) ^ [] : [-(aElementOf0(szmzazxdt0(xS), xS))], (1086 ^ _124723) ^ [_158431] : [aElementOf0(_158431, xS), -(sdtlseqdt0(_158431, szmzazxdt0(xS)))], (1113 ^ _124723) ^ [] : [-(aElementOf0(1111 ^ [], xS))], (1115 ^ _124723) ^ [] : [aElementOf0(1111 ^ [], slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))], (1117 ^ _124723) ^ [] : [aSubsetOf0(xS, slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))], (1092 ^ _124723) ^ [] : [-(aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))], (1094 ^ _124723) ^ [_158705] : [aElementOf0(_158705, slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))), 1097 ^ _124723 : [(1098 ^ _124723) ^ [] : [-(aElementOf0(_158705, szNzAzT0))], (1100 ^ _124723) ^ [] : [-(sdtlseqdt0(szszuzczcdt0(_158705), szszuzczcdt0(szmzazxdt0(xS))))]]], (1102 ^ _124723) ^ [_158938] : [-(aElementOf0(_158938, slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))), aElementOf0(_158938, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_158938), szszuzczcdt0(szmzazxdt0(xS)))], (116 ^ _124723) ^ [_128475, _128477, _128479, _128481] : [-(sdtpldt0(_128481, _128477) = sdtpldt0(_128479, _128475)), _128481 = _128479, _128477 = _128475], (126 ^ _124723) ^ [_128834, _128836, _128838, _128840] : [-(sdtmndt0(_128840, _128836) = sdtmndt0(_128838, _128834)), _128840 = _128838, _128836 = _128834], (136 ^ _124723) ^ [_129165, _129167] : [_129167 = _129165, -(sbrdtbr0(_129167) = sbrdtbr0(_129165))], (142 ^ _124723) ^ [_129383, _129385] : [_129385 = _129383, -(szmzizndt0(_129385) = szmzizndt0(_129383))], (148 ^ _124723) ^ [_129601, _129603] : [_129603 = _129601, -(slbdtrb0(_129603) = slbdtrb0(_129601))], (154 ^ _124723) ^ [_129819, _129821] : [_129821 = _129819, -(szszuzczcdt0(_129821) = szszuzczcdt0(_129819))], (160 ^ _124723) ^ [_130017, _130019] : [_130019 = _130017, -(szmzazxdt0(_130019) = szmzazxdt0(_130017))], (2 ^ _124723) ^ [_124867] : [-(_124867 = _124867)], (4 ^ _124723) ^ [_124974, _124976] : [_124976 = _124974, -(_124974 = _124976)], (10 ^ _124723) ^ [_125178, _125180, _125182] : [-(_125182 = _125178), _125182 = _125180, _125180 = _125178], (20 ^ _124723) ^ [_125491, _125493] : [-(isCountable0(_125491)), _125493 = _125491, isCountable0(_125493)], (30 ^ _124723) ^ [_125814, _125816, _125818, _125820] : [-(iLess0(_125818, _125814)), iLess0(_125820, _125816), _125820 = _125818, _125816 = _125814], (44 ^ _124723) ^ [_126230, _126232] : [-(aElement0(_126230)), _126232 = _126230, aElement0(_126232)], (54 ^ _124723) ^ [_126525, _126527] : [-(isFinite0(_126525)), _126527 = _126525, isFinite0(_126527)], (64 ^ _124723) ^ [_126820, _126822] : [-(aSet0(_126820)), _126822 = _126820, aSet0(_126822)], (74 ^ _124723) ^ [_127143, _127145, _127147, _127149] : [-(sdtlseqdt0(_127147, _127143)), sdtlseqdt0(_127149, _127145), _127149 = _127147, _127145 = _127143], (88 ^ _124723) ^ [_127587, _127589, _127591, _127593] : [-(aElementOf0(_127591, _127587)), aElementOf0(_127593, _127589), _127593 = _127591, _127589 = _127587], (102 ^ _124723) ^ [_128011, _128013, _128015, _128017] : [-(aSubsetOf0(_128015, _128011)), aSubsetOf0(_128017, _128013), _128017 = _128015, _128013 = _128011], (166 ^ _124723) ^ [_130247] : [aSet0(_130247), true___, -(true___)], (176 ^ _124723) ^ [_130502] : [aElement0(_130502), true___, -(true___)], (186 ^ _124723) ^ [_130757] : [aSet0(_130757), 189 ^ _124723 : [(190 ^ _124723) ^ [_130887] : [aElementOf0(_130887, _130757), -(aElement0(_130887))]]], (196 ^ _124723) ^ [_131088] : [aSet0(_131088), isFinite0(_131088), true___, -(true___)], (210 ^ _124723) ^ [_131458] : [_131458 = slcrc0, 213 ^ _124723 : [(214 ^ _124723) ^ [] : [-(aSet0(_131458))], (216 ^ _124723) ^ [_131639] : [aElementOf0(_131639, _131458)]]], (218 ^ _124723) ^ [_131707] : [-(_131707 = slcrc0), aSet0(_131707), -(aElementOf0(223 ^ [_131707], _131707))], (229 ^ _124723) ^ [] : [-(isFinite0(slcrc0))], (231 ^ _124723) ^ [_132089] : [aSet0(_132089), isCountable0(_132089), true___, -(true___)], (245 ^ _124723) ^ [_132430] : [isFinite0(_132430), aSet0(_132430), isCountable0(_132430)], (255 ^ _124723) ^ [_132700] : [_132700 = slcrc0, aSet0(_132700), isCountable0(_132700)], (265 ^ _124723) ^ [_132972] : [aSet0(_132972), 268 ^ _124723 : [(269 ^ _124723) ^ [_133148] : [aSubsetOf0(_133148, _132972), 272 ^ _124723 : [(273 ^ _124723) ^ [] : [-(aSet0(_133148))], (275 ^ _124723) ^ [_133357] : [aElementOf0(_133357, _133148), -(aElementOf0(_133357, _132972))]]], (281 ^ _124723) ^ [_133536] : [-(aSubsetOf0(_133536, _132972)), aSet0(_133536), 287 ^ _124723 : [(288 ^ _124723) ^ [] : [-(aElementOf0(286 ^ [_132972, _133536], _133536))], (290 ^ _124723) ^ [] : [aElementOf0(286 ^ [_132972, _133536], _132972)]]]]], (294 ^ _124723) ^ [_133973] : [aSet0(_133973), isFinite0(_133973), 301 ^ _124723 : [(302 ^ _124723) ^ [_134186] : [aSubsetOf0(_134186, _133973), -(isFinite0(_134186))]]], (308 ^ _124723) ^ [_134389] : [aSet0(_134389), -(aSubsetOf0(_134389, _134389))], (314 ^ _124723) ^ [_134591, _134593] : [aSet0(_134593), aSet0(_134591), -(_134593 = _134591), aSubsetOf0(_134593, _134591), aSubsetOf0(_134591, _134593)], (332 ^ _124723) ^ [_135080, _135082, _135084] : [aSet0(_135084), aSet0(_135082), aSet0(_135080), -(aSubsetOf0(_135084, _135080)), aSubsetOf0(_135084, _135082), aSubsetOf0(_135082, _135080)], (354 ^ _124723) ^ [_135666, _135668] : [aSet0(_135668), aElement0(_135666), 361 ^ _124723 : [(392 ^ _124723) ^ [_136927] : [-(_136927 = sdtpldt0(_135668, _135666)), aSet0(_136927), 400 ^ _124723 : [(401 ^ _124723) ^ [] : [-(aElementOf0(397 ^ [_135666, _135668, _136927], _136927))], (403 ^ _124723) ^ [] : [aElement0(397 ^ [_135666, _135668, _136927]), 406 ^ _124723 : [(407 ^ _124723) ^ [] : [aElementOf0(397 ^ [_135666, _135668, _136927], _135668)], (409 ^ _124723) ^ [] : [397 ^ [_135666, _135668, _136927] = _135666]]]], 410 ^ _124723 : [(419 ^ _124723) ^ [] : [aElementOf0(397 ^ [_135666, _135668, _136927], _136927)], (411 ^ _124723) ^ [] : [-(aElement0(397 ^ [_135666, _135668, _136927]))], (413 ^ _124723) ^ [] : [-(aElementOf0(397 ^ [_135666, _135668, _136927], _135668)), -(397 ^ [_135666, _135668, _136927] = _135666)]]], (362 ^ _124723) ^ [_135947] : [_135947 = sdtpldt0(_135668, _135666), 365 ^ _124723 : [(366 ^ _124723) ^ [] : [-(aSet0(_135947))], (368 ^ _124723) ^ [_136210] : [aElementOf0(_136210, _135947), 371 ^ _124723 : [(372 ^ _124723) ^ [] : [-(aElement0(_136210))], (374 ^ _124723) ^ [] : [-(aElementOf0(_136210, _135668)), -(_136210 = _135666)]]], (380 ^ _124723) ^ [_136565] : [-(aElementOf0(_136565, _135947)), aElement0(_136565), 385 ^ _124723 : [(386 ^ _124723) ^ [] : [aElementOf0(_136565, _135668)], (388 ^ _124723) ^ [] : [_136565 = _135666]]]]]]], (423 ^ _124723) ^ [_137964, _137966] : [aSet0(_137966), aElement0(_137964), 430 ^ _124723 : [(461 ^ _124723) ^ [_139232] : [-(_139232 = sdtmndt0(_137966, _137964)), aSet0(_139232), 481 ^ _124723 : [(482 ^ _124723) ^ [] : [-(aElement0(466 ^ [_137964, _137966, _139232]))], (484 ^ _124723) ^ [] : [-(aElementOf0(466 ^ [_137964, _137966, _139232], _137966))], (486 ^ _124723) ^ [] : [466 ^ [_137964, _137966, _139232] = _137964], (488 ^ _124723) ^ [] : [aElementOf0(466 ^ [_137964, _137966, _139232], _139232)]], 469 ^ _124723 : [(470 ^ _124723) ^ [] : [-(aElementOf0(466 ^ [_137964, _137966, _139232], _139232))], (472 ^ _124723) ^ [] : [aElement0(466 ^ [_137964, _137966, _139232]), aElementOf0(466 ^ [_137964, _137966, _139232], _137966), -(466 ^ [_137964, _137966, _139232] = _137964)]]], (431 ^ _124723) ^ [_138247] : [_138247 = sdtmndt0(_137966, _137964), 434 ^ _124723 : [(435 ^ _124723) ^ [] : [-(aSet0(_138247))], (437 ^ _124723) ^ [_138512] : [aElementOf0(_138512, _138247), 440 ^ _124723 : [(441 ^ _124723) ^ [] : [-(aElement0(_138512))], (443 ^ _124723) ^ [] : [-(aElementOf0(_138512, _137966))], (445 ^ _124723) ^ [] : [_138512 = _137964]]], (447 ^ _124723) ^ [_138848] : [-(aElementOf0(_138848, _138247)), aElement0(_138848), aElementOf0(_138848, _137966), -(_138848 = _137964)]]]]], (492 ^ _124723) ^ [_140262] : [aSet0(_140262), 495 ^ _124723 : [(496 ^ _124723) ^ [_140399] : [aElementOf0(_140399, _140262), -(sdtpldt0(sdtmndt0(_140262, _140399), _140399) = _140262)]]], (502 ^ _124723) ^ [_140628, _140630] : [aElement0(_140630), aSet0(_140628), -(aElementOf0(_140630, _140628)), -(sdtmndt0(sdtpldt0(_140628, _140630), _140630) = _140628)], (516 ^ _124723) ^ [_141015] : [aElement0(_141015), 519 ^ _124723 : [(520 ^ _124723) ^ [_141152] : [-(isCountable0(sdtpldt0(_141152, _141015))), aSet0(_141152), isCountable0(_141152)]]], (530 ^ _124723) ^ [_141444] : [aElement0(_141444), 533 ^ _124723 : [(534 ^ _124723) ^ [_141581] : [-(isCountable0(sdtmndt0(_141581, _141444))), aSet0(_141581), isCountable0(_141581)]]], (544 ^ _124723) ^ [_141873] : [aElement0(_141873), 547 ^ _124723 : [(548 ^ _124723) ^ [_142010] : [-(isFinite0(sdtpldt0(_142010, _141873))), aSet0(_142010), isFinite0(_142010)]]], (558 ^ _124723) ^ [_142302] : [aElement0(_142302), 561 ^ _124723 : [(562 ^ _124723) ^ [_142439] : [-(isFinite0(sdtmndt0(_142439, _142302))), aSet0(_142439), isFinite0(_142439)]]], (572 ^ _124723) ^ [] : [-(aSet0(szNzAzT0))], (574 ^ _124723) ^ [] : [-(isCountable0(szNzAzT0))], (576 ^ _124723) ^ [] : [-(aElementOf0(sz00, szNzAzT0))], (578 ^ _124723) ^ [_142892] : [aElementOf0(_142892, szNzAzT0), 581 ^ _124723 : [(582 ^ _124723) ^ [] : [-(aElementOf0(szszuzczcdt0(_142892), szNzAzT0))], (584 ^ _124723) ^ [] : [szszuzczcdt0(_142892) = sz00]]], (586 ^ _124723) ^ [_143178, _143180] : [aElementOf0(_143180, szNzAzT0), aElementOf0(_143178, szNzAzT0), szszuzczcdt0(_143180) = szszuzczcdt0(_143178), -(_143180 = _143178)], (600 ^ _124723) ^ [_143562] : [aElementOf0(_143562, szNzAzT0), -(_143562 = sz00), 608 ^ _124723 : [(609 ^ _124723) ^ [] : [-(aElementOf0(607 ^ [_143562], szNzAzT0))], (611 ^ _124723) ^ [] : [-(_143562 = szszuzczcdt0(607 ^ [_143562]))]]], (613 ^ _124723) ^ [_143979] : [aElementOf0(_143979, szNzAzT0), _143979 = szszuzczcdt0(_143979)], (619 ^ _124723) ^ [_144188, _144190] : [aElementOf0(_144190, szNzAzT0), aElementOf0(_144188, szNzAzT0), sdtlseqdt0(_144190, _144188), true___, -(true___)], (637 ^ _124723) ^ [_144638] : [aElementOf0(_144638, szNzAzT0), -(sdtlseqdt0(sz00, _144638))], (643 ^ _124723) ^ [_144828] : [aElementOf0(_144828, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_144828), sz00)], (649 ^ _124723) ^ [_145037, _145039] : [aElementOf0(_145039, szNzAzT0), aElementOf0(_145037, szNzAzT0), 656 ^ _124723 : [(657 ^ _124723) ^ [] : [sdtlseqdt0(_145039, _145037), -(sdtlseqdt0(szszuzczcdt0(_145039), szszuzczcdt0(_145037)))], (663 ^ _124723) ^ [] : [sdtlseqdt0(szszuzczcdt0(_145039), szszuzczcdt0(_145037)), -(sdtlseqdt0(_145039, _145037))]]], (669 ^ _124723) ^ [_145586] : [aElementOf0(_145586, szNzAzT0), -(sdtlseqdt0(_145586, szszuzczcdt0(_145586)))], (675 ^ _124723) ^ [_145780] : [aElementOf0(_145780, szNzAzT0), -(sdtlseqdt0(_145780, _145780))], (681 ^ _124723) ^ [_145984, _145986] : [aElementOf0(_145986, szNzAzT0), aElementOf0(_145984, szNzAzT0), -(_145986 = _145984), sdtlseqdt0(_145986, _145984), sdtlseqdt0(_145984, _145986)], (699 ^ _124723) ^ [_146477, _146479, _146481] : [aElementOf0(_146481, szNzAzT0), aElementOf0(_146479, szNzAzT0), aElementOf0(_146477, szNzAzT0), -(sdtlseqdt0(_146481, _146477)), sdtlseqdt0(_146481, _146479), sdtlseqdt0(_146479, _146477)], (721 ^ _124723) ^ [_147069, _147071] : [aElementOf0(_147071, szNzAzT0), aElementOf0(_147069, szNzAzT0), -(sdtlseqdt0(_147071, _147069)), -(sdtlseqdt0(szszuzczcdt0(_147069), _147071))], (735 ^ _124723) ^ [_147464, _147466] : [aElementOf0(_147466, szNzAzT0), aElementOf0(_147464, szNzAzT0), iLess0(_147466, _147464), true___, -(true___)], (753 ^ _124723) ^ [_147914] : [aElementOf0(_147914, szNzAzT0), -(iLess0(_147914, szszuzczcdt0(_147914)))], (759 ^ _124723) ^ [_148108] : [aSet0(_148108), -(aElement0(sbrdtbr0(_148108)))], (765 ^ _124723) ^ [_148298] : [aSet0(_148298), 768 ^ _124723 : [(769 ^ _124723) ^ [] : [aElementOf0(sbrdtbr0(_148298), szNzAzT0), -(isFinite0(_148298))], (775 ^ _124723) ^ [] : [isFinite0(_148298), -(aElementOf0(sbrdtbr0(_148298), szNzAzT0))]]], (781 ^ _124723) ^ [_148729] : [aSet0(_148729), 784 ^ _124723 : [(785 ^ _124723) ^ [] : [sbrdtbr0(_148729) = sz00, -(_148729 = slcrc0)], (791 ^ _124723) ^ [] : [_148729 = slcrc0, -(sbrdtbr0(_148729) = sz00)]]], (797 ^ _124723) ^ [_149163] : [aSet0(_149163), isFinite0(_149163), 804 ^ _124723 : [(805 ^ _124723) ^ [_149393] : [aElement0(_149393), -(aElementOf0(_149393, _149163)), -(sbrdtbr0(sdtpldt0(_149163, _149393)) = szszuzczcdt0(sbrdtbr0(_149163)))]]], (815 ^ _124723) ^ [_149706] : [aSet0(_149706), 818 ^ _124723 : [(819 ^ _124723) ^ [_149851] : [-(szszuzczcdt0(sbrdtbr0(sdtmndt0(_149706, _149851))) = sbrdtbr0(_149706)), isFinite0(_149706), aElementOf0(_149851, _149706)]]], (829 ^ _124723) ^ [_150159] : [aSet0(_150159), 832 ^ _124723 : [(833 ^ _124723) ^ [_150299] : [-(sdtlseqdt0(sbrdtbr0(_150299), sbrdtbr0(_150159))), isFinite0(_150159), aSubsetOf0(_150299, _150159)]]], (843 ^ _124723) ^ [_150611, _150613] : [aSet0(_150613), aElementOf0(_150611, szNzAzT0), 859 ^ _124723 : [(860 ^ _124723) ^ [] : [-(aSubsetOf0(858 ^ [_150611, _150613], _150613))], (862 ^ _124723) ^ [] : [-(sbrdtbr0(858 ^ [_150611, _150613]) = _150611)]], isFinite0(_150613), sdtlseqdt0(_150611, sbrdtbr0(_150613))], (864 ^ _124723) ^ [_151227] : [aSubsetOf0(_151227, szNzAzT0), -(_151227 = slcrc0), 871 ^ _124723 : [(872 ^ _124723) ^ [_151496] : [_151496 = szmzizndt0(_151227), 875 ^ _124723 : [(876 ^ _124723) ^ [] : [-(aElementOf0(_151496, _151227))], (878 ^ _124723) ^ [_151711] : [aElementOf0(_151711, _151227), -(sdtlseqdt0(_151496, _151711))]]], (884 ^ _124723) ^ [_151890] : [-(_151890 = szmzizndt0(_151227)), aElementOf0(_151890, _151227), 890 ^ _124723 : [(891 ^ _124723) ^ [] : [-(aElementOf0(889 ^ [_151227, _151890], _151227))], (893 ^ _124723) ^ [] : [sdtlseqdt0(_151890, 889 ^ [_151227, _151890])]]]]], (897 ^ _124723) ^ [_152335] : [aSubsetOf0(_152335, szNzAzT0), isFinite0(_152335), -(_152335 = slcrc0), 908 ^ _124723 : [(909 ^ _124723) ^ [_152687] : [_152687 = szmzazxdt0(_152335), 912 ^ _124723 : [(913 ^ _124723) ^ [] : [-(aElementOf0(_152687, _152335))], (915 ^ _124723) ^ [_152902] : [aElementOf0(_152902, _152335), -(sdtlseqdt0(_152902, _152687))]]], (921 ^ _124723) ^ [_153081] : [-(_153081 = szmzazxdt0(_152335)), aElementOf0(_153081, _152335), 927 ^ _124723 : [(928 ^ _124723) ^ [] : [-(aElementOf0(926 ^ [_152335, _153081], _152335))], (930 ^ _124723) ^ [] : [sdtlseqdt0(926 ^ [_152335, _153081], _153081)]]]]], (934 ^ _124723) ^ [_153542, _153544] : [-(szmzizndt0(_153544) = szmzizndt0(_153542)), aElementOf0(szmzizndt0(_153544), _153542), aElementOf0(szmzizndt0(_153542), _153544), aSubsetOf0(_153544, szNzAzT0), aSubsetOf0(_153542, szNzAzT0), -(_153544 = slcrc0), -(_153542 = slcrc0)], (960 ^ _124723) ^ [_154209] : [aElementOf0(_154209, szNzAzT0), 963 ^ _124723 : [(988 ^ _124723) ^ [_155178] : [-(_155178 = slbdtrb0(_154209)), aSet0(_155178), 1004 ^ _124723 : [(1005 ^ _124723) ^ [] : [-(aElementOf0(993 ^ [_154209, _155178], szNzAzT0))], (1007 ^ _124723) ^ [] : [-(sdtlseqdt0(szszuzczcdt0(993 ^ [_154209, _155178]), _154209))], (1009 ^ _124723) ^ [] : [aElementOf0(993 ^ [_154209, _155178], _155178)]], 996 ^ _124723 : [(997 ^ _124723) ^ [] : [-(aElementOf0(993 ^ [_154209, _155178], _155178))], (999 ^ _124723) ^ [] : [aElementOf0(993 ^ [_154209, _155178], szNzAzT0), sdtlseqdt0(szszuzczcdt0(993 ^ [_154209, _155178]), _154209)]]], (964 ^ _124723) ^ [_154397] : [_154397 = slbdtrb0(_154209), 967 ^ _124723 : [(968 ^ _124723) ^ [] : [-(aSet0(_154397))], (970 ^ _124723) ^ [_154647] : [aElementOf0(_154647, _154397), 973 ^ _124723 : [(974 ^ _124723) ^ [] : [-(aElementOf0(_154647, szNzAzT0))], (976 ^ _124723) ^ [] : [-(sdtlseqdt0(szszuzczcdt0(_154647), _154209))]]], (978 ^ _124723) ^ [_154900] : [-(aElementOf0(_154900, _154397)), aElementOf0(_154900, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_154900), _154209)]]]]], (1013 ^ _124723) ^ [_155981] : [aElementOf0(_155981, szNzAzT0), -(isFinite0(slbdtrb0(_155981)))], (1019 ^ _124723) ^ [] : [-(slbdtrb0(sz00) = slcrc0)], (1021 ^ _124723) ^ [_156240, _156242] : [aElementOf0(_156242, szNzAzT0), aElementOf0(_156240, szNzAzT0), 1028 ^ _124723 : [(1039 ^ _124723) ^ [] : [1040 ^ _124723 : [(1041 ^ _124723) ^ [] : [aElementOf0(_156242, slbdtrb0(_156240))], (1043 ^ _124723) ^ [] : [_156242 = _156240]], -(aElementOf0(_156242, slbdtrb0(szszuzczcdt0(_156240))))], (1029 ^ _124723) ^ [] : [aElementOf0(_156242, slbdtrb0(szszuzczcdt0(_156240))), -(aElementOf0(_156242, slbdtrb0(_156240))), -(_156242 = _156240)]]], (1067 ^ _124723) ^ [] : [-(aSet0(xS))], (1075 ^ _124723) ^ [] : [-(aSubsetOf0(xS, szNzAzT0))], (1077 ^ _124723) ^ [] : [-(isFinite0(xS))], (1069 ^ _124723) ^ [_157569] : [aElementOf0(_157569, xS), -(aElementOf0(_157569, szNzAzT0))], (1047 ^ _124723) ^ [_156967, _156969] : [aElementOf0(_156969, szNzAzT0), aElementOf0(_156967, szNzAzT0), 1054 ^ _124723 : [(1055 ^ _124723) ^ [] : [sdtlseqdt0(_156969, _156967), -(aSubsetOf0(slbdtrb0(_156969), slbdtrb0(_156967)))], (1061 ^ _124723) ^ [] : [aSubsetOf0(slbdtrb0(_156969), slbdtrb0(_156967)), -(sdtlseqdt0(_156969, _156967))]]]], input).
% 0.81/1.37 ncf('1',plain,[aElementOf0(1111 ^ [], slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))],start(1115 ^ 0)).
% 0.81/1.37 ncf('1.1',plain,[-(aElementOf0(1111 ^ [], slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))), aElementOf0(1111 ^ [], szNzAzT0), sdtlseqdt0(szszuzczcdt0(1111 ^ []), szszuzczcdt0(szmzazxdt0(xS)))],extension(1102 ^ 1,bind([[_158938], [1111 ^ []]]))).
% 0.81/1.37 ncf('1.1.1',plain,[-(aElementOf0(1111 ^ [], szNzAzT0)), 275 : aElementOf0(1111 ^ [], xS), 275 : aSubsetOf0(xS, szNzAzT0), 269 : aSet0(szNzAzT0)],extension(265 ^ 2,bind([[_132972, _133148, _133357], [szNzAzT0, xS, 1111 ^ []]]))).
% 0.81/1.37 ncf('1.1.1.1',plain,[-(aElementOf0(1111 ^ [], xS))],extension(1113 ^ 7)).
% 0.81/1.37 ncf('1.1.1.2',plain,[-(aSubsetOf0(xS, szNzAzT0))],extension(1075 ^ 5)).
% 0.81/1.37 ncf('1.1.1.3',plain,[-(aSet0(szNzAzT0))],extension(572 ^ 3)).
% 0.81/1.37 ncf('1.1.2',plain,[-(sdtlseqdt0(szszuzczcdt0(1111 ^ []), szszuzczcdt0(szmzazxdt0(xS)))), 657 : sdtlseqdt0(1111 ^ [], szmzazxdt0(xS)), 657 : aElementOf0(1111 ^ [], szNzAzT0), 657 : aElementOf0(szmzazxdt0(xS), szNzAzT0)],extension(649 ^ 2,bind([[_145037, _145039], [szmzazxdt0(xS), 1111 ^ []]]))).
% 0.81/1.37 ncf('1.1.2.1',plain,[-(sdtlseqdt0(1111 ^ [], szmzazxdt0(xS))), aElementOf0(1111 ^ [], xS)],extension(1086 ^ 5,bind([[_158431], [1111 ^ []]]))).
% 0.81/1.37 ncf('1.1.2.1.1',plain,[-(aElementOf0(1111 ^ [], xS))],extension(1113 ^ 6)).
% 0.81/1.37 ncf('1.1.2.2',plain,[-(aElementOf0(1111 ^ [], szNzAzT0))],lemmata('[1].x')).
% 0.81/1.37 ncf('1.1.2.3',plain,[-(aElementOf0(szmzazxdt0(xS), szNzAzT0)), 275 : aElementOf0(szmzazxdt0(xS), xS), 275 : aSubsetOf0(xS, szNzAzT0), 269 : aSet0(szNzAzT0)],extension(265 ^ 3,bind([[_132972, _133148, _133357], [szNzAzT0, xS, szmzazxdt0(xS)]]))).
% 0.81/1.37 ncf('1.1.2.3.1',plain,[-(aElementOf0(szmzazxdt0(xS), xS))],extension(1084 ^ 8)).
% 0.81/1.37 ncf('1.1.2.3.2',plain,[-(aSubsetOf0(xS, szNzAzT0))],extension(1075 ^ 6)).
% 0.81/1.37 ncf('1.1.2.3.3',plain,[-(aSet0(szNzAzT0))],extension(572 ^ 4)).
% 0.81/1.37 %-----------------------------------------------------
% 0.81/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------