%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM560+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.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 : 300s
% DateTime : Fri May 19 11:45:00 EDT 2023
% Result : Theorem 0.56s 1.38s
% Output : Proof 0.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM560+1 : TPTP v8.1.2. Released v4.0.0.
% 0.00/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n007.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 16:37:07 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.56/1.38
% 0.56/1.38 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.56/1.38 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.56/1.38 %-----------------------------------------------------
% 0.56/1.38 ncf(matrix, plain, [(1371 ^ _155334) ^ [] : [aSubsetOf0(sdtlbdtrb0(xF, xy), szDzozmdt0(xF))], (126 ^ _155334) ^ [_159383, _159385, _159387, _159389] : [-(sdtpldt0(_159389, _159385) = sdtpldt0(_159387, _159383)), _159389 = _159387, _159385 = _159383], (136 ^ _155334) ^ [_159742, _159744, _159746, _159748] : [-(sdtmndt0(_159748, _159744) = sdtmndt0(_159746, _159742)), _159748 = _159746, _159744 = _159742], (146 ^ _155334) ^ [_160073, _160075] : [_160075 = _160073, -(szmzazxdt0(_160075) = szmzazxdt0(_160073))], (152 ^ _155334) ^ [_160291, _160293] : [_160293 = _160291, -(szmzizndt0(_160293) = szmzizndt0(_160291))], (158 ^ _155334) ^ [_160509, _160511] : [_160511 = _160509, -(szszuzczcdt0(_160511) = szszuzczcdt0(_160509))], (164 ^ _155334) ^ [_160727, _160729] : [_160729 = _160727, -(slbdtrb0(_160729) = slbdtrb0(_160727))], (170 ^ _155334) ^ [_160945, _160947] : [_160947 = _160945, -(sbrdtbr0(_160947) = sbrdtbr0(_160945))], (176 ^ _155334) ^ [_161191, _161193, _161195, _161197] : [-(slbdtsldtrb0(_161197, _161193) = slbdtsldtrb0(_161195, _161191)), _161197 = _161195, _161193 = _161191], (186 ^ _155334) ^ [_161550, _161552, _161554, _161556] : [-(sdtlpdtrp0(_161556, _161552) = sdtlpdtrp0(_161554, _161550)), _161556 = _161554, _161552 = _161550], (206 ^ _155334) ^ [_162220, _162222] : [_162222 = _162220, -(szDzozmdt0(_162222) = szDzozmdt0(_162220))], (196 ^ _155334) ^ [_161909, _161911, _161913, _161915] : [-(sdtlbdtrb0(_161915, _161911) = sdtlbdtrb0(_161913, _161909)), _161915 = _161913, _161911 = _161909], (2 ^ _155334) ^ [_155478] : [-(_155478 = _155478)], (4 ^ _155334) ^ [_155585, _155587] : [_155587 = _155585, -(_155585 = _155587)], (10 ^ _155334) ^ [_155789, _155791, _155793] : [-(_155793 = _155789), _155793 = _155791, _155791 = _155789], (20 ^ _155334) ^ [_156130, _156132, _156134, _156136] : [-(iLess0(_156134, _156130)), iLess0(_156136, _156132), _156136 = _156134, _156132 = _156130], (34 ^ _155334) ^ [_156574, _156576, _156578, _156580] : [-(sdtlseqdt0(_156578, _156574)), sdtlseqdt0(_156580, _156576), _156580 = _156578, _156576 = _156574], (48 ^ _155334) ^ [_156990, _156992] : [-(isCountable0(_156990)), _156992 = _156990, isCountable0(_156992)], (58 ^ _155334) ^ [_157285, _157287] : [-(isFinite0(_157285)), _157287 = _157285, isFinite0(_157287)], (68 ^ _155334) ^ [_157580, _157582] : [-(aSet0(_157580)), _157582 = _157580, aSet0(_157582)], (78 ^ _155334) ^ [_157903, _157905, _157907, _157909] : [-(aElementOf0(_157907, _157903)), aElementOf0(_157909, _157905), _157909 = _157907, _157905 = _157903], (92 ^ _155334) ^ [_158319, _158321] : [-(aFunction0(_158319)), _158321 = _158319, aFunction0(_158321)], (102 ^ _155334) ^ [_158614, _158616] : [-(aElement0(_158614)), _158616 = _158614, aElement0(_158616)], (112 ^ _155334) ^ [_158917, _158919, _158921, _158923] : [-(aSubsetOf0(_158921, _158917)), aSubsetOf0(_158923, _158919), _158923 = _158921, _158919 = _158917], (212 ^ _155334) ^ [_162498] : [aSet0(_162498), true___, -(true___)], (222 ^ _155334) ^ [_162753] : [aElement0(_162753), true___, -(true___)], (232 ^ _155334) ^ [_163008] : [aSet0(_163008), 235 ^ _155334 : [(236 ^ _155334) ^ [_163138] : [aElementOf0(_163138, _163008), -(aElement0(_163138))]]], (242 ^ _155334) ^ [_163339] : [aSet0(_163339), isFinite0(_163339), true___, -(true___)], (256 ^ _155334) ^ [_163709] : [_163709 = slcrc0, 259 ^ _155334 : [(260 ^ _155334) ^ [] : [-(aSet0(_163709))], (262 ^ _155334) ^ [_163890] : [aElementOf0(_163890, _163709)]]], (264 ^ _155334) ^ [_163958] : [-(_163958 = slcrc0), aSet0(_163958), -(aElementOf0(269 ^ [_163958], _163958))], (275 ^ _155334) ^ [] : [-(isFinite0(slcrc0))], (277 ^ _155334) ^ [_164340] : [aSet0(_164340), isCountable0(_164340), true___, -(true___)], (291 ^ _155334) ^ [_164681] : [isFinite0(_164681), aSet0(_164681), isCountable0(_164681)], (301 ^ _155334) ^ [_164951] : [_164951 = slcrc0, aSet0(_164951), isCountable0(_164951)], (311 ^ _155334) ^ [_165223] : [aSet0(_165223), 314 ^ _155334 : [(315 ^ _155334) ^ [_165399] : [aSubsetOf0(_165399, _165223), 318 ^ _155334 : [(319 ^ _155334) ^ [] : [-(aSet0(_165399))], (321 ^ _155334) ^ [_165608] : [aElementOf0(_165608, _165399), -(aElementOf0(_165608, _165223))]]], (327 ^ _155334) ^ [_165787] : [-(aSubsetOf0(_165787, _165223)), aSet0(_165787), 333 ^ _155334 : [(334 ^ _155334) ^ [] : [-(aElementOf0(332 ^ [_165223, _165787], _165787))], (336 ^ _155334) ^ [] : [aElementOf0(332 ^ [_165223, _165787], _165223)]]]]], (340 ^ _155334) ^ [_166224] : [aSet0(_166224), isFinite0(_166224), 347 ^ _155334 : [(348 ^ _155334) ^ [_166437] : [aSubsetOf0(_166437, _166224), -(isFinite0(_166437))]]], (354 ^ _155334) ^ [_166640] : [aSet0(_166640), -(aSubsetOf0(_166640, _166640))], (360 ^ _155334) ^ [_166842, _166844] : [aSet0(_166844), aSet0(_166842), -(_166844 = _166842), aSubsetOf0(_166844, _166842), aSubsetOf0(_166842, _166844)], (378 ^ _155334) ^ [_167331, _167333, _167335] : [aSet0(_167335), aSet0(_167333), aSet0(_167331), -(aSubsetOf0(_167335, _167331)), aSubsetOf0(_167335, _167333), aSubsetOf0(_167333, _167331)], (400 ^ _155334) ^ [_167917, _167919] : [aSet0(_167919), aElement0(_167917), 407 ^ _155334 : [(438 ^ _155334) ^ [_169178] : [-(_169178 = sdtpldt0(_167919, _167917)), aSet0(_169178), 446 ^ _155334 : [(447 ^ _155334) ^ [] : [-(aElementOf0(443 ^ [_167917, _167919, _169178], _169178))], (449 ^ _155334) ^ [] : [aElement0(443 ^ [_167917, _167919, _169178]), 452 ^ _155334 : [(453 ^ _155334) ^ [] : [aElementOf0(443 ^ [_167917, _167919, _169178], _167919)], (455 ^ _155334) ^ [] : [443 ^ [_167917, _167919, _169178] = _167917]]]], 456 ^ _155334 : [(465 ^ _155334) ^ [] : [aElementOf0(443 ^ [_167917, _167919, _169178], _169178)], (457 ^ _155334) ^ [] : [-(aElement0(443 ^ [_167917, _167919, _169178]))], (459 ^ _155334) ^ [] : [-(aElementOf0(443 ^ [_167917, _167919, _169178], _167919)), -(443 ^ [_167917, _167919, _169178] = _167917)]]], (408 ^ _155334) ^ [_168198] : [_168198 = sdtpldt0(_167919, _167917), 411 ^ _155334 : [(412 ^ _155334) ^ [] : [-(aSet0(_168198))], (414 ^ _155334) ^ [_168461] : [aElementOf0(_168461, _168198), 417 ^ _155334 : [(418 ^ _155334) ^ [] : [-(aElement0(_168461))], (420 ^ _155334) ^ [] : [-(aElementOf0(_168461, _167919)), -(_168461 = _167917)]]], (426 ^ _155334) ^ [_168816] : [-(aElementOf0(_168816, _168198)), aElement0(_168816), 431 ^ _155334 : [(432 ^ _155334) ^ [] : [aElementOf0(_168816, _167919)], (434 ^ _155334) ^ [] : [_168816 = _167917]]]]]]], (469 ^ _155334) ^ [_170215, _170217] : [aSet0(_170217), aElement0(_170215), 476 ^ _155334 : [(507 ^ _155334) ^ [_171483] : [-(_171483 = sdtmndt0(_170217, _170215)), aSet0(_171483), 527 ^ _155334 : [(528 ^ _155334) ^ [] : [-(aElement0(512 ^ [_170215, _170217, _171483]))], (530 ^ _155334) ^ [] : [-(aElementOf0(512 ^ [_170215, _170217, _171483], _170217))], (532 ^ _155334) ^ [] : [512 ^ [_170215, _170217, _171483] = _170215], (534 ^ _155334) ^ [] : [aElementOf0(512 ^ [_170215, _170217, _171483], _171483)]], 515 ^ _155334 : [(516 ^ _155334) ^ [] : [-(aElementOf0(512 ^ [_170215, _170217, _171483], _171483))], (518 ^ _155334) ^ [] : [aElement0(512 ^ [_170215, _170217, _171483]), aElementOf0(512 ^ [_170215, _170217, _171483], _170217), -(512 ^ [_170215, _170217, _171483] = _170215)]]], (477 ^ _155334) ^ [_170498] : [_170498 = sdtmndt0(_170217, _170215), 480 ^ _155334 : [(481 ^ _155334) ^ [] : [-(aSet0(_170498))], (483 ^ _155334) ^ [_170763] : [aElementOf0(_170763, _170498), 486 ^ _155334 : [(487 ^ _155334) ^ [] : [-(aElement0(_170763))], (489 ^ _155334) ^ [] : [-(aElementOf0(_170763, _170217))], (491 ^ _155334) ^ [] : [_170763 = _170215]]], (493 ^ _155334) ^ [_171099] : [-(aElementOf0(_171099, _170498)), aElement0(_171099), aElementOf0(_171099, _170217), -(_171099 = _170215)]]]]], (538 ^ _155334) ^ [_172513] : [aSet0(_172513), 541 ^ _155334 : [(542 ^ _155334) ^ [_172650] : [aElementOf0(_172650, _172513), -(sdtpldt0(sdtmndt0(_172513, _172650), _172650) = _172513)]]], (548 ^ _155334) ^ [_172879, _172881] : [aElement0(_172881), aSet0(_172879), -(aElementOf0(_172881, _172879)), -(sdtmndt0(sdtpldt0(_172879, _172881), _172881) = _172879)], (562 ^ _155334) ^ [_173266] : [aElement0(_173266), 565 ^ _155334 : [(566 ^ _155334) ^ [_173403] : [-(isCountable0(sdtpldt0(_173403, _173266))), aSet0(_173403), isCountable0(_173403)]]], (576 ^ _155334) ^ [_173695] : [aElement0(_173695), 579 ^ _155334 : [(580 ^ _155334) ^ [_173832] : [-(isCountable0(sdtmndt0(_173832, _173695))), aSet0(_173832), isCountable0(_173832)]]], (590 ^ _155334) ^ [_174124] : [aElement0(_174124), 593 ^ _155334 : [(594 ^ _155334) ^ [_174261] : [-(isFinite0(sdtpldt0(_174261, _174124))), aSet0(_174261), isFinite0(_174261)]]], (604 ^ _155334) ^ [_174553] : [aElement0(_174553), 607 ^ _155334 : [(608 ^ _155334) ^ [_174690] : [-(isFinite0(sdtmndt0(_174690, _174553))), aSet0(_174690), isFinite0(_174690)]]], (618 ^ _155334) ^ [] : [-(aSet0(szNzAzT0))], (620 ^ _155334) ^ [] : [-(isCountable0(szNzAzT0))], (622 ^ _155334) ^ [] : [-(aElementOf0(sz00, szNzAzT0))], (624 ^ _155334) ^ [_175143] : [aElementOf0(_175143, szNzAzT0), 627 ^ _155334 : [(628 ^ _155334) ^ [] : [-(aElementOf0(szszuzczcdt0(_175143), szNzAzT0))], (630 ^ _155334) ^ [] : [szszuzczcdt0(_175143) = sz00]]], (632 ^ _155334) ^ [_175429, _175431] : [aElementOf0(_175431, szNzAzT0), aElementOf0(_175429, szNzAzT0), szszuzczcdt0(_175431) = szszuzczcdt0(_175429), -(_175431 = _175429)], (646 ^ _155334) ^ [_175813] : [aElementOf0(_175813, szNzAzT0), -(_175813 = sz00), 654 ^ _155334 : [(655 ^ _155334) ^ [] : [-(aElementOf0(653 ^ [_175813], szNzAzT0))], (657 ^ _155334) ^ [] : [-(_175813 = szszuzczcdt0(653 ^ [_175813]))]]], (659 ^ _155334) ^ [_176230] : [aElementOf0(_176230, szNzAzT0), _176230 = szszuzczcdt0(_176230)], (665 ^ _155334) ^ [_176439, _176441] : [aElementOf0(_176441, szNzAzT0), aElementOf0(_176439, szNzAzT0), sdtlseqdt0(_176441, _176439), true___, -(true___)], (683 ^ _155334) ^ [_176889] : [aElementOf0(_176889, szNzAzT0), -(sdtlseqdt0(sz00, _176889))], (689 ^ _155334) ^ [_177079] : [aElementOf0(_177079, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_177079), sz00)], (695 ^ _155334) ^ [_177288, _177290] : [aElementOf0(_177290, szNzAzT0), aElementOf0(_177288, szNzAzT0), 702 ^ _155334 : [(703 ^ _155334) ^ [] : [sdtlseqdt0(_177290, _177288), -(sdtlseqdt0(szszuzczcdt0(_177290), szszuzczcdt0(_177288)))], (709 ^ _155334) ^ [] : [sdtlseqdt0(szszuzczcdt0(_177290), szszuzczcdt0(_177288)), -(sdtlseqdt0(_177290, _177288))]]], (715 ^ _155334) ^ [_177837] : [aElementOf0(_177837, szNzAzT0), -(sdtlseqdt0(_177837, szszuzczcdt0(_177837)))], (721 ^ _155334) ^ [_178031] : [aElementOf0(_178031, szNzAzT0), -(sdtlseqdt0(_178031, _178031))], (727 ^ _155334) ^ [_178235, _178237] : [aElementOf0(_178237, szNzAzT0), aElementOf0(_178235, szNzAzT0), -(_178237 = _178235), sdtlseqdt0(_178237, _178235), sdtlseqdt0(_178235, _178237)], (745 ^ _155334) ^ [_178728, _178730, _178732] : [aElementOf0(_178732, szNzAzT0), aElementOf0(_178730, szNzAzT0), aElementOf0(_178728, szNzAzT0), -(sdtlseqdt0(_178732, _178728)), sdtlseqdt0(_178732, _178730), sdtlseqdt0(_178730, _178728)], (767 ^ _155334) ^ [_179320, _179322] : [aElementOf0(_179322, szNzAzT0), aElementOf0(_179320, szNzAzT0), -(sdtlseqdt0(_179322, _179320)), -(sdtlseqdt0(szszuzczcdt0(_179320), _179322))], (781 ^ _155334) ^ [_179715, _179717] : [aElementOf0(_179717, szNzAzT0), aElementOf0(_179715, szNzAzT0), iLess0(_179717, _179715), true___, -(true___)], (799 ^ _155334) ^ [_180165] : [aElementOf0(_180165, szNzAzT0), -(iLess0(_180165, szszuzczcdt0(_180165)))], (805 ^ _155334) ^ [_180359] : [aSet0(_180359), -(aElement0(sbrdtbr0(_180359)))], (811 ^ _155334) ^ [_180549] : [aSet0(_180549), 814 ^ _155334 : [(815 ^ _155334) ^ [] : [aElementOf0(sbrdtbr0(_180549), szNzAzT0), -(isFinite0(_180549))], (821 ^ _155334) ^ [] : [isFinite0(_180549), -(aElementOf0(sbrdtbr0(_180549), szNzAzT0))]]], (827 ^ _155334) ^ [_180980] : [aSet0(_180980), 830 ^ _155334 : [(831 ^ _155334) ^ [] : [sbrdtbr0(_180980) = sz00, -(_180980 = slcrc0)], (837 ^ _155334) ^ [] : [_180980 = slcrc0, -(sbrdtbr0(_180980) = sz00)]]], (843 ^ _155334) ^ [_181414] : [aSet0(_181414), isFinite0(_181414), 850 ^ _155334 : [(851 ^ _155334) ^ [_181644] : [aElement0(_181644), -(aElementOf0(_181644, _181414)), -(sbrdtbr0(sdtpldt0(_181414, _181644)) = szszuzczcdt0(sbrdtbr0(_181414)))]]], (861 ^ _155334) ^ [_181957] : [aSet0(_181957), 864 ^ _155334 : [(865 ^ _155334) ^ [_182102] : [-(szszuzczcdt0(sbrdtbr0(sdtmndt0(_181957, _182102))) = sbrdtbr0(_181957)), isFinite0(_181957), aElementOf0(_182102, _181957)]]], (875 ^ _155334) ^ [_182410] : [aSet0(_182410), 878 ^ _155334 : [(879 ^ _155334) ^ [_182550] : [-(sdtlseqdt0(sbrdtbr0(_182550), sbrdtbr0(_182410))), isFinite0(_182410), aSubsetOf0(_182550, _182410)]]], (889 ^ _155334) ^ [_182862, _182864] : [aSet0(_182864), aElementOf0(_182862, szNzAzT0), 905 ^ _155334 : [(906 ^ _155334) ^ [] : [-(aSubsetOf0(904 ^ [_182862, _182864], _182864))], (908 ^ _155334) ^ [] : [-(sbrdtbr0(904 ^ [_182862, _182864]) = _182862)]], isFinite0(_182864), sdtlseqdt0(_182862, sbrdtbr0(_182864))], (910 ^ _155334) ^ [_183478] : [aSubsetOf0(_183478, szNzAzT0), -(_183478 = slcrc0), 917 ^ _155334 : [(918 ^ _155334) ^ [_183747] : [_183747 = szmzizndt0(_183478), 921 ^ _155334 : [(922 ^ _155334) ^ [] : [-(aElementOf0(_183747, _183478))], (924 ^ _155334) ^ [_183962] : [aElementOf0(_183962, _183478), -(sdtlseqdt0(_183747, _183962))]]], (930 ^ _155334) ^ [_184141] : [-(_184141 = szmzizndt0(_183478)), aElementOf0(_184141, _183478), 936 ^ _155334 : [(937 ^ _155334) ^ [] : [-(aElementOf0(935 ^ [_183478, _184141], _183478))], (939 ^ _155334) ^ [] : [sdtlseqdt0(_184141, 935 ^ [_183478, _184141])]]]]], (943 ^ _155334) ^ [_184586] : [aSubsetOf0(_184586, szNzAzT0), isFinite0(_184586), -(_184586 = slcrc0), 954 ^ _155334 : [(955 ^ _155334) ^ [_184938] : [_184938 = szmzazxdt0(_184586), 958 ^ _155334 : [(959 ^ _155334) ^ [] : [-(aElementOf0(_184938, _184586))], (961 ^ _155334) ^ [_185153] : [aElementOf0(_185153, _184586), -(sdtlseqdt0(_185153, _184938))]]], (967 ^ _155334) ^ [_185332] : [-(_185332 = szmzazxdt0(_184586)), aElementOf0(_185332, _184586), 973 ^ _155334 : [(974 ^ _155334) ^ [] : [-(aElementOf0(972 ^ [_184586, _185332], _184586))], (976 ^ _155334) ^ [] : [sdtlseqdt0(972 ^ [_184586, _185332], _185332)]]]]], (980 ^ _155334) ^ [_185793, _185795] : [-(szmzizndt0(_185795) = szmzizndt0(_185793)), aElementOf0(szmzizndt0(_185795), _185793), aElementOf0(szmzizndt0(_185793), _185795), aSubsetOf0(_185795, szNzAzT0), aSubsetOf0(_185793, szNzAzT0), -(_185795 = slcrc0), -(_185793 = slcrc0)], (1006 ^ _155334) ^ [_186460] : [aElementOf0(_186460, szNzAzT0), 1009 ^ _155334 : [(1034 ^ _155334) ^ [_187429] : [-(_187429 = slbdtrb0(_186460)), aSet0(_187429), 1050 ^ _155334 : [(1051 ^ _155334) ^ [] : [-(aElementOf0(1039 ^ [_186460, _187429], szNzAzT0))], (1053 ^ _155334) ^ [] : [-(sdtlseqdt0(szszuzczcdt0(1039 ^ [_186460, _187429]), _186460))], (1055 ^ _155334) ^ [] : [aElementOf0(1039 ^ [_186460, _187429], _187429)]], 1042 ^ _155334 : [(1043 ^ _155334) ^ [] : [-(aElementOf0(1039 ^ [_186460, _187429], _187429))], (1045 ^ _155334) ^ [] : [aElementOf0(1039 ^ [_186460, _187429], szNzAzT0), sdtlseqdt0(szszuzczcdt0(1039 ^ [_186460, _187429]), _186460)]]], (1010 ^ _155334) ^ [_186648] : [_186648 = slbdtrb0(_186460), 1013 ^ _155334 : [(1014 ^ _155334) ^ [] : [-(aSet0(_186648))], (1016 ^ _155334) ^ [_186898] : [aElementOf0(_186898, _186648), 1019 ^ _155334 : [(1020 ^ _155334) ^ [] : [-(aElementOf0(_186898, szNzAzT0))], (1022 ^ _155334) ^ [] : [-(sdtlseqdt0(szszuzczcdt0(_186898), _186460))]]], (1024 ^ _155334) ^ [_187151] : [-(aElementOf0(_187151, _186648)), aElementOf0(_187151, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_187151), _186460)]]]]], (1059 ^ _155334) ^ [_188232] : [aElementOf0(_188232, szNzAzT0), -(isFinite0(slbdtrb0(_188232)))], (1065 ^ _155334) ^ [] : [-(slbdtrb0(sz00) = slcrc0)], (1067 ^ _155334) ^ [_188491, _188493] : [aElementOf0(_188493, szNzAzT0), aElementOf0(_188491, szNzAzT0), 1074 ^ _155334 : [(1085 ^ _155334) ^ [] : [1086 ^ _155334 : [(1087 ^ _155334) ^ [] : [aElementOf0(_188493, slbdtrb0(_188491))], (1089 ^ _155334) ^ [] : [_188493 = _188491]], -(aElementOf0(_188493, slbdtrb0(szszuzczcdt0(_188491))))], (1075 ^ _155334) ^ [] : [aElementOf0(_188493, slbdtrb0(szszuzczcdt0(_188491))), -(aElementOf0(_188493, slbdtrb0(_188491))), -(_188493 = _188491)]]], (1093 ^ _155334) ^ [_189218, _189220] : [aElementOf0(_189220, szNzAzT0), aElementOf0(_189218, szNzAzT0), 1100 ^ _155334 : [(1101 ^ _155334) ^ [] : [sdtlseqdt0(_189220, _189218), -(aSubsetOf0(slbdtrb0(_189220), slbdtrb0(_189218)))], (1107 ^ _155334) ^ [] : [aSubsetOf0(slbdtrb0(_189220), slbdtrb0(_189218)), -(sdtlseqdt0(_189220, _189218))]]], (1113 ^ _155334) ^ [_189767] : [1121 ^ _155334 : [(1122 ^ _155334) ^ [] : [-(aElementOf0(1120 ^ [_189767], szNzAzT0))], (1124 ^ _155334) ^ [] : [-(aSubsetOf0(_189767, slbdtrb0(1120 ^ [_189767])))]], aSubsetOf0(_189767, szNzAzT0), isFinite0(_189767)], (1126 ^ _155334) ^ [_190181] : [aElementOf0(_190181, szNzAzT0), -(sbrdtbr0(slbdtrb0(_190181)) = _190181)], (1132 ^ _155334) ^ [_190393, _190395] : [aSet0(_190395), aElementOf0(_190393, szNzAzT0), 1139 ^ _155334 : [(1164 ^ _155334) ^ [_191486] : [-(_191486 = slbdtsldtrb0(_190395, _190393)), aSet0(_191486), 1180 ^ _155334 : [(1181 ^ _155334) ^ [] : [-(aSubsetOf0(1169 ^ [_190393, _190395, _191486], _190395))], (1183 ^ _155334) ^ [] : [-(sbrdtbr0(1169 ^ [_190393, _190395, _191486]) = _190393)], (1185 ^ _155334) ^ [] : [aElementOf0(1169 ^ [_190393, _190395, _191486], _191486)]], 1172 ^ _155334 : [(1173 ^ _155334) ^ [] : [-(aElementOf0(1169 ^ [_190393, _190395, _191486], _191486))], (1175 ^ _155334) ^ [] : [aSubsetOf0(1169 ^ [_190393, _190395, _191486], _190395), sbrdtbr0(1169 ^ [_190393, _190395, _191486]) = _190393]]], (1140 ^ _155334) ^ [_190673] : [_190673 = slbdtsldtrb0(_190395, _190393), 1143 ^ _155334 : [(1144 ^ _155334) ^ [] : [-(aSet0(_190673))], (1146 ^ _155334) ^ [_190933] : [aElementOf0(_190933, _190673), 1149 ^ _155334 : [(1150 ^ _155334) ^ [] : [-(aSubsetOf0(_190933, _190395))], (1152 ^ _155334) ^ [] : [-(sbrdtbr0(_190933) = _190393)]]], (1154 ^ _155334) ^ [_191196] : [-(aElementOf0(_191196, _190673)), aSubsetOf0(_191196, _190395), sbrdtbr0(_191196) = _190393]]]]], (1189 ^ _155334) ^ [_192335] : [aSet0(_192335), isFinite0(_192335), 1196 ^ _155334 : [(1197 ^ _155334) ^ [_192551] : [aElementOf0(_192551, szNzAzT0), -(isFinite0(slbdtsldtrb0(_192335, _192551)))]]], (1203 ^ _155334) ^ [_192760] : [aSet0(_192760), -(isFinite0(_192760)), 1210 ^ _155334 : [(1211 ^ _155334) ^ [_192982] : [aElementOf0(_192982, szNzAzT0), slbdtsldtrb0(_192760, _192982) = slcrc0]]], (1217 ^ _155334) ^ [_193194] : [aSet0(_193194), isCountable0(_193194), 1224 ^ _155334 : [(1225 ^ _155334) ^ [_193418] : [-(isCountable0(slbdtsldtrb0(_193194, _193418))), aElementOf0(_193418, szNzAzT0), -(_193418 = sz00)]]], (1235 ^ _155334) ^ [_193719] : [aElementOf0(_193719, szNzAzT0), 1238 ^ _155334 : [(1239 ^ _155334) ^ [_193906, _193908] : [aSet0(_193908), aSet0(_193906), -(_193719 = sz00), -(aSubsetOf0(_193908, _193906)), aSubsetOf0(slbdtsldtrb0(_193908, _193719), slbdtsldtrb0(_193906, _193719)), -(slbdtsldtrb0(_193908, _193719) = slcrc0)]]], (1261 ^ _155334) ^ [_194525, _194527] : [aSet0(_194527), aElementOf0(_194525, szNzAzT0), 1268 ^ _155334 : [(1269 ^ _155334) ^ [_194776] : [1277 ^ _155334 : [(1278 ^ _155334) ^ [] : [-(aSubsetOf0(1276 ^ [_194525, _194527, _194776], _194527))], (1280 ^ _155334) ^ [] : [-(isFinite0(1276 ^ [_194525, _194527, _194776]))], (1282 ^ _155334) ^ [] : [-(aSubsetOf0(_194776, slbdtsldtrb0(1276 ^ [_194525, _194527, _194776], _194525)))]], aSubsetOf0(_194776, slbdtsldtrb0(_194527, _194525)), isFinite0(_194776)]]], (1284 ^ _155334) ^ [_195338] : [aFunction0(_195338), true___, -(true___)], (1294 ^ _155334) ^ [_195593] : [aFunction0(_195593), -(aSet0(szDzozmdt0(_195593)))], (1300 ^ _155334) ^ [_195783] : [aFunction0(_195783), 1303 ^ _155334 : [(1304 ^ _155334) ^ [_195918] : [aElementOf0(_195918, szDzozmdt0(_195783)), -(aElement0(sdtlpdtrp0(_195783, _195918)))]]], (1367 ^ _155334) ^ [] : [-(aFunction0(xF))], (1369 ^ _155334) ^ [] : [-(aElement0(xy))], (1310 ^ _155334) ^ [_196143, _196145] : [aFunction0(_196145), aElement0(_196143), 1317 ^ _155334 : [(1342 ^ _155334) ^ [_197252] : [-(_197252 = sdtlbdtrb0(_196145, _196143)), aSet0(_197252), 1358 ^ _155334 : [(1359 ^ _155334) ^ [] : [-(aElementOf0(1347 ^ [_196143, _196145, _197252], szDzozmdt0(_196145)))], (1361 ^ _155334) ^ [] : [-(sdtlpdtrp0(_196145, 1347 ^ [_196143, _196145, _197252]) = _196143)], (1363 ^ _155334) ^ [] : [aElementOf0(1347 ^ [_196143, _196145, _197252], _197252)]], 1350 ^ _155334 : [(1351 ^ _155334) ^ [] : [-(aElementOf0(1347 ^ [_196143, _196145, _197252], _197252))], (1353 ^ _155334) ^ [] : [aElementOf0(1347 ^ [_196143, _196145, _197252], szDzozmdt0(_196145)), sdtlpdtrp0(_196145, 1347 ^ [_196143, _196145, _197252]) = _196143]]], (1318 ^ _155334) ^ [_196424] : [_196424 = sdtlbdtrb0(_196145, _196143), 1321 ^ _155334 : [(1322 ^ _155334) ^ [] : [-(aSet0(_196424))], (1324 ^ _155334) ^ [_196687] : [aElementOf0(_196687, _196424), 1327 ^ _155334 : [(1328 ^ _155334) ^ [] : [-(aElementOf0(_196687, szDzozmdt0(_196145)))], (1330 ^ _155334) ^ [] : [-(sdtlpdtrp0(_196145, _196687) = _196143)]]], (1332 ^ _155334) ^ [_196956] : [-(aElementOf0(_196956, _196424)), aElementOf0(_196956, szDzozmdt0(_196145)), sdtlpdtrp0(_196145, _196956) = _196143]]]]]], input).
% 0.56/1.38 ncf('1',plain,[aSubsetOf0(sdtlbdtrb0(xF, xy), szDzozmdt0(xF))],start(1371 ^ 0)).
% 0.56/1.38 ncf('1.1',plain,[-(aSubsetOf0(sdtlbdtrb0(xF, xy), szDzozmdt0(xF))), 327 : aSet0(sdtlbdtrb0(xF, xy)), 334 : -(aElementOf0(332 ^ [szDzozmdt0(xF), sdtlbdtrb0(xF, xy)], sdtlbdtrb0(xF, xy))), 327 : aSet0(szDzozmdt0(xF))],extension(311 ^ 1,bind([[_165223, _165787], [szDzozmdt0(xF), sdtlbdtrb0(xF, xy)]]))).
% 0.56/1.38 ncf('1.1.1',plain,[-(aSet0(sdtlbdtrb0(xF, xy))), 1318 : sdtlbdtrb0(xF, xy) = sdtlbdtrb0(xF, xy), 1318 : aFunction0(xF), 1318 : aElement0(xy)],extension(1310 ^ 4,bind([[_196143, _196145, _196424], [xy, xF, sdtlbdtrb0(xF, xy)]]))).
% 0.56/1.38 ncf('1.1.1.1',plain,[-(sdtlbdtrb0(xF, xy) = sdtlbdtrb0(xF, xy))],extension(2 ^ 7,bind([[_155478], [sdtlbdtrb0(xF, xy)]]))).
% 0.56/1.38 ncf('1.1.1.2',plain,[-(aFunction0(xF))],extension(1367 ^ 5)).
% 0.56/1.38 ncf('1.1.1.3',plain,[-(aElement0(xy))],extension(1369 ^ 5)).
% 0.56/1.38 ncf('1.1.2',plain,[aElementOf0(332 ^ [szDzozmdt0(xF), sdtlbdtrb0(xF, xy)], sdtlbdtrb0(xF, xy)), 1328 : -(aElementOf0(332 ^ [szDzozmdt0(xF), sdtlbdtrb0(xF, xy)], szDzozmdt0(xF))), 1324 : sdtlbdtrb0(xF, xy) = sdtlbdtrb0(xF, xy), 1318 : aFunction0(xF), 1318 : aElement0(xy)],extension(1310 ^ 6,bind([[_196143, _196145, _196424, _196687], [xy, xF, sdtlbdtrb0(xF, xy), 332 ^ [szDzozmdt0(xF), sdtlbdtrb0(xF, xy)]]]))).
% 0.56/1.38 ncf('1.1.2.1',plain,[aElementOf0(332 ^ [szDzozmdt0(xF), sdtlbdtrb0(xF, xy)], szDzozmdt0(xF))],extension(336 ^ 13)).
% 0.56/1.38 ncf('1.1.2.2',plain,[-(sdtlbdtrb0(xF, xy) = sdtlbdtrb0(xF, xy))],extension(2 ^ 9,bind([[_155478], [sdtlbdtrb0(xF, xy)]]))).
% 0.56/1.38 ncf('1.1.2.3',plain,[-(aFunction0(xF))],extension(1367 ^ 7)).
% 0.56/1.38 ncf('1.1.2.4',plain,[-(aElement0(xy))],extension(1369 ^ 7)).
% 0.56/1.38 ncf('1.1.3',plain,[-(aSet0(szDzozmdt0(xF))), aFunction0(xF)],extension(1294 ^ 2,bind([[_195593], [xF]]))).
% 0.56/1.38 ncf('1.1.3.1',plain,[-(aFunction0(xF))],extension(1367 ^ 3)).
% 0.56/1.38 %-----------------------------------------------------
% 0.56/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------