%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM551+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.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 : 300s
% DateTime : Fri May 19 11:44:58 EDT 2023
% Result : Theorem 0.37s 1.38s
% Output : Proof 0.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUM551+3 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n029.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 18 17:04:13 EDT 2023
% 0.13/0.34 % CPUTime :
% 0.37/1.38
% 0.37/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.37/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/1.38 %-----------------------------------------------------
% 0.37/1.38 ncf(matrix, plain, [(1356 ^ _155632) ^ [_198040] : [aElement0(_198040), aElementOf0(_198040, xQ)], (116 ^ _155632) ^ [_159384, _159386, _159388, _159390] : [-(sdtpldt0(_159390, _159386) = sdtpldt0(_159388, _159384)), _159390 = _159388, _159386 = _159384], (126 ^ _155632) ^ [_159743, _159745, _159747, _159749] : [-(sdtmndt0(_159749, _159745) = sdtmndt0(_159747, _159743)), _159749 = _159747, _159745 = _159743], (136 ^ _155632) ^ [_160074, _160076] : [_160076 = _160074, -(szmzazxdt0(_160076) = szmzazxdt0(_160074))], (142 ^ _155632) ^ [_160292, _160294] : [_160294 = _160292, -(szmzizndt0(_160294) = szmzizndt0(_160292))], (148 ^ _155632) ^ [_160510, _160512] : [_160512 = _160510, -(szszuzczcdt0(_160512) = szszuzczcdt0(_160510))], (154 ^ _155632) ^ [_160728, _160730] : [_160730 = _160728, -(slbdtrb0(_160730) = slbdtrb0(_160728))], (170 ^ _155632) ^ [_161285, _161287] : [_161287 = _161285, -(sbrdtbr0(_161287) = sbrdtbr0(_161285))], (160 ^ _155632) ^ [_160974, _160976, _160978, _160980] : [-(slbdtsldtrb0(_160980, _160976) = slbdtsldtrb0(_160978, _160974)), _160980 = _160978, _160976 = _160974], (2 ^ _155632) ^ [_155776] : [-(_155776 = _155776)], (4 ^ _155632) ^ [_155883, _155885] : [_155885 = _155883, -(_155883 = _155885)], (10 ^ _155632) ^ [_156087, _156089, _156091] : [-(_156091 = _156087), _156091 = _156089, _156089 = _156087], (20 ^ _155632) ^ [_156428, _156430, _156432, _156434] : [-(iLess0(_156432, _156428)), iLess0(_156434, _156430), _156434 = _156432, _156430 = _156428], (34 ^ _155632) ^ [_156872, _156874, _156876, _156878] : [-(sdtlseqdt0(_156876, _156872)), sdtlseqdt0(_156878, _156874), _156878 = _156876, _156874 = _156872], (48 ^ _155632) ^ [_157288, _157290] : [-(isCountable0(_157288)), _157290 = _157288, isCountable0(_157290)], (58 ^ _155632) ^ [_157611, _157613, _157615, _157617] : [-(aSubsetOf0(_157615, _157611)), aSubsetOf0(_157617, _157613), _157617 = _157615, _157613 = _157611], (72 ^ _155632) ^ [_158027, _158029] : [-(aSet0(_158027)), _158029 = _158027, aSet0(_158029)], (82 ^ _155632) ^ [_158322, _158324] : [-(isFinite0(_158322)), _158324 = _158322, isFinite0(_158324)], (92 ^ _155632) ^ [_158617, _158619] : [-(aElement0(_158617)), _158619 = _158617, aElement0(_158619)], (102 ^ _155632) ^ [_158920, _158922, _158924, _158926] : [-(aElementOf0(_158924, _158920)), aElementOf0(_158926, _158922), _158926 = _158924, _158922 = _158920], (176 ^ _155632) ^ [_161519] : [aSet0(_161519), true___, -(true___)], (186 ^ _155632) ^ [_161774] : [aElement0(_161774), true___, -(true___)], (196 ^ _155632) ^ [_162029] : [aSet0(_162029), 199 ^ _155632 : [(200 ^ _155632) ^ [_162159] : [aElementOf0(_162159, _162029), -(aElement0(_162159))]]], (206 ^ _155632) ^ [_162360] : [aSet0(_162360), isFinite0(_162360), true___, -(true___)], (220 ^ _155632) ^ [_162730] : [_162730 = slcrc0, 223 ^ _155632 : [(224 ^ _155632) ^ [] : [-(aSet0(_162730))], (226 ^ _155632) ^ [_162911] : [aElementOf0(_162911, _162730)]]], (228 ^ _155632) ^ [_162979] : [-(_162979 = slcrc0), aSet0(_162979), -(aElementOf0(233 ^ [_162979], _162979))], (239 ^ _155632) ^ [] : [-(isFinite0(slcrc0))], (241 ^ _155632) ^ [_163361] : [aSet0(_163361), isCountable0(_163361), true___, -(true___)], (255 ^ _155632) ^ [_163702] : [isFinite0(_163702), aSet0(_163702), isCountable0(_163702)], (265 ^ _155632) ^ [_163972] : [_163972 = slcrc0, aSet0(_163972), isCountable0(_163972)], (275 ^ _155632) ^ [_164244] : [aSet0(_164244), 278 ^ _155632 : [(279 ^ _155632) ^ [_164420] : [aSubsetOf0(_164420, _164244), 282 ^ _155632 : [(283 ^ _155632) ^ [] : [-(aSet0(_164420))], (285 ^ _155632) ^ [_164629] : [aElementOf0(_164629, _164420), -(aElementOf0(_164629, _164244))]]], (291 ^ _155632) ^ [_164808] : [-(aSubsetOf0(_164808, _164244)), aSet0(_164808), 297 ^ _155632 : [(298 ^ _155632) ^ [] : [-(aElementOf0(296 ^ [_164244, _164808], _164808))], (300 ^ _155632) ^ [] : [aElementOf0(296 ^ [_164244, _164808], _164244)]]]]], (304 ^ _155632) ^ [_165245] : [aSet0(_165245), isFinite0(_165245), 311 ^ _155632 : [(312 ^ _155632) ^ [_165458] : [aSubsetOf0(_165458, _165245), -(isFinite0(_165458))]]], (318 ^ _155632) ^ [_165661] : [aSet0(_165661), -(aSubsetOf0(_165661, _165661))], (324 ^ _155632) ^ [_165863, _165865] : [aSet0(_165865), aSet0(_165863), -(_165865 = _165863), aSubsetOf0(_165865, _165863), aSubsetOf0(_165863, _165865)], (342 ^ _155632) ^ [_166352, _166354, _166356] : [aSet0(_166356), aSet0(_166354), aSet0(_166352), -(aSubsetOf0(_166356, _166352)), aSubsetOf0(_166356, _166354), aSubsetOf0(_166354, _166352)], (364 ^ _155632) ^ [_166938, _166940] : [aSet0(_166940), aElement0(_166938), 371 ^ _155632 : [(402 ^ _155632) ^ [_168199] : [-(_168199 = sdtpldt0(_166940, _166938)), aSet0(_168199), 410 ^ _155632 : [(411 ^ _155632) ^ [] : [-(aElementOf0(407 ^ [_166938, _166940, _168199], _168199))], (413 ^ _155632) ^ [] : [aElement0(407 ^ [_166938, _166940, _168199]), 416 ^ _155632 : [(417 ^ _155632) ^ [] : [aElementOf0(407 ^ [_166938, _166940, _168199], _166940)], (419 ^ _155632) ^ [] : [407 ^ [_166938, _166940, _168199] = _166938]]]], 420 ^ _155632 : [(429 ^ _155632) ^ [] : [aElementOf0(407 ^ [_166938, _166940, _168199], _168199)], (421 ^ _155632) ^ [] : [-(aElement0(407 ^ [_166938, _166940, _168199]))], (423 ^ _155632) ^ [] : [-(aElementOf0(407 ^ [_166938, _166940, _168199], _166940)), -(407 ^ [_166938, _166940, _168199] = _166938)]]], (372 ^ _155632) ^ [_167219] : [_167219 = sdtpldt0(_166940, _166938), 375 ^ _155632 : [(376 ^ _155632) ^ [] : [-(aSet0(_167219))], (378 ^ _155632) ^ [_167482] : [aElementOf0(_167482, _167219), 381 ^ _155632 : [(382 ^ _155632) ^ [] : [-(aElement0(_167482))], (384 ^ _155632) ^ [] : [-(aElementOf0(_167482, _166940)), -(_167482 = _166938)]]], (390 ^ _155632) ^ [_167837] : [-(aElementOf0(_167837, _167219)), aElement0(_167837), 395 ^ _155632 : [(396 ^ _155632) ^ [] : [aElementOf0(_167837, _166940)], (398 ^ _155632) ^ [] : [_167837 = _166938]]]]]]], (433 ^ _155632) ^ [_169236, _169238] : [aSet0(_169238), aElement0(_169236), 440 ^ _155632 : [(471 ^ _155632) ^ [_170504] : [-(_170504 = sdtmndt0(_169238, _169236)), aSet0(_170504), 491 ^ _155632 : [(492 ^ _155632) ^ [] : [-(aElement0(476 ^ [_169236, _169238, _170504]))], (494 ^ _155632) ^ [] : [-(aElementOf0(476 ^ [_169236, _169238, _170504], _169238))], (496 ^ _155632) ^ [] : [476 ^ [_169236, _169238, _170504] = _169236], (498 ^ _155632) ^ [] : [aElementOf0(476 ^ [_169236, _169238, _170504], _170504)]], 479 ^ _155632 : [(480 ^ _155632) ^ [] : [-(aElementOf0(476 ^ [_169236, _169238, _170504], _170504))], (482 ^ _155632) ^ [] : [aElement0(476 ^ [_169236, _169238, _170504]), aElementOf0(476 ^ [_169236, _169238, _170504], _169238), -(476 ^ [_169236, _169238, _170504] = _169236)]]], (441 ^ _155632) ^ [_169519] : [_169519 = sdtmndt0(_169238, _169236), 444 ^ _155632 : [(445 ^ _155632) ^ [] : [-(aSet0(_169519))], (447 ^ _155632) ^ [_169784] : [aElementOf0(_169784, _169519), 450 ^ _155632 : [(451 ^ _155632) ^ [] : [-(aElement0(_169784))], (453 ^ _155632) ^ [] : [-(aElementOf0(_169784, _169238))], (455 ^ _155632) ^ [] : [_169784 = _169236]]], (457 ^ _155632) ^ [_170120] : [-(aElementOf0(_170120, _169519)), aElement0(_170120), aElementOf0(_170120, _169238), -(_170120 = _169236)]]]]], (502 ^ _155632) ^ [_171534] : [aSet0(_171534), 505 ^ _155632 : [(506 ^ _155632) ^ [_171671] : [aElementOf0(_171671, _171534), -(sdtpldt0(sdtmndt0(_171534, _171671), _171671) = _171534)]]], (512 ^ _155632) ^ [_171900, _171902] : [aElement0(_171902), aSet0(_171900), -(aElementOf0(_171902, _171900)), -(sdtmndt0(sdtpldt0(_171900, _171902), _171902) = _171900)], (526 ^ _155632) ^ [_172287] : [aElement0(_172287), 529 ^ _155632 : [(530 ^ _155632) ^ [_172424] : [-(isCountable0(sdtpldt0(_172424, _172287))), aSet0(_172424), isCountable0(_172424)]]], (540 ^ _155632) ^ [_172716] : [aElement0(_172716), 543 ^ _155632 : [(544 ^ _155632) ^ [_172853] : [-(isCountable0(sdtmndt0(_172853, _172716))), aSet0(_172853), isCountable0(_172853)]]], (554 ^ _155632) ^ [_173145] : [aElement0(_173145), 557 ^ _155632 : [(558 ^ _155632) ^ [_173282] : [-(isFinite0(sdtpldt0(_173282, _173145))), aSet0(_173282), isFinite0(_173282)]]], (568 ^ _155632) ^ [_173574] : [aElement0(_173574), 571 ^ _155632 : [(572 ^ _155632) ^ [_173711] : [-(isFinite0(sdtmndt0(_173711, _173574))), aSet0(_173711), isFinite0(_173711)]]], (582 ^ _155632) ^ [] : [-(aSet0(szNzAzT0))], (584 ^ _155632) ^ [] : [-(isCountable0(szNzAzT0))], (586 ^ _155632) ^ [] : [-(aElementOf0(sz00, szNzAzT0))], (588 ^ _155632) ^ [_174164] : [aElementOf0(_174164, szNzAzT0), 591 ^ _155632 : [(592 ^ _155632) ^ [] : [-(aElementOf0(szszuzczcdt0(_174164), szNzAzT0))], (594 ^ _155632) ^ [] : [szszuzczcdt0(_174164) = sz00]]], (596 ^ _155632) ^ [_174450, _174452] : [aElementOf0(_174452, szNzAzT0), aElementOf0(_174450, szNzAzT0), szszuzczcdt0(_174452) = szszuzczcdt0(_174450), -(_174452 = _174450)], (610 ^ _155632) ^ [_174834] : [aElementOf0(_174834, szNzAzT0), -(_174834 = sz00), 618 ^ _155632 : [(619 ^ _155632) ^ [] : [-(aElementOf0(617 ^ [_174834], szNzAzT0))], (621 ^ _155632) ^ [] : [-(_174834 = szszuzczcdt0(617 ^ [_174834]))]]], (623 ^ _155632) ^ [_175251] : [aElementOf0(_175251, szNzAzT0), _175251 = szszuzczcdt0(_175251)], (629 ^ _155632) ^ [_175460, _175462] : [aElementOf0(_175462, szNzAzT0), aElementOf0(_175460, szNzAzT0), sdtlseqdt0(_175462, _175460), true___, -(true___)], (647 ^ _155632) ^ [_175910] : [aElementOf0(_175910, szNzAzT0), -(sdtlseqdt0(sz00, _175910))], (653 ^ _155632) ^ [_176100] : [aElementOf0(_176100, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_176100), sz00)], (659 ^ _155632) ^ [_176309, _176311] : [aElementOf0(_176311, szNzAzT0), aElementOf0(_176309, szNzAzT0), 666 ^ _155632 : [(667 ^ _155632) ^ [] : [sdtlseqdt0(_176311, _176309), -(sdtlseqdt0(szszuzczcdt0(_176311), szszuzczcdt0(_176309)))], (673 ^ _155632) ^ [] : [sdtlseqdt0(szszuzczcdt0(_176311), szszuzczcdt0(_176309)), -(sdtlseqdt0(_176311, _176309))]]], (679 ^ _155632) ^ [_176858] : [aElementOf0(_176858, szNzAzT0), -(sdtlseqdt0(_176858, szszuzczcdt0(_176858)))], (685 ^ _155632) ^ [_177052] : [aElementOf0(_177052, szNzAzT0), -(sdtlseqdt0(_177052, _177052))], (691 ^ _155632) ^ [_177256, _177258] : [aElementOf0(_177258, szNzAzT0), aElementOf0(_177256, szNzAzT0), -(_177258 = _177256), sdtlseqdt0(_177258, _177256), sdtlseqdt0(_177256, _177258)], (709 ^ _155632) ^ [_177749, _177751, _177753] : [aElementOf0(_177753, szNzAzT0), aElementOf0(_177751, szNzAzT0), aElementOf0(_177749, szNzAzT0), -(sdtlseqdt0(_177753, _177749)), sdtlseqdt0(_177753, _177751), sdtlseqdt0(_177751, _177749)], (731 ^ _155632) ^ [_178341, _178343] : [aElementOf0(_178343, szNzAzT0), aElementOf0(_178341, szNzAzT0), -(sdtlseqdt0(_178343, _178341)), -(sdtlseqdt0(szszuzczcdt0(_178341), _178343))], (745 ^ _155632) ^ [_178736, _178738] : [aElementOf0(_178738, szNzAzT0), aElementOf0(_178736, szNzAzT0), iLess0(_178738, _178736), true___, -(true___)], (763 ^ _155632) ^ [_179186] : [aElementOf0(_179186, szNzAzT0), -(iLess0(_179186, szszuzczcdt0(_179186)))], (769 ^ _155632) ^ [_179380] : [aSet0(_179380), -(aElement0(sbrdtbr0(_179380)))], (775 ^ _155632) ^ [_179570] : [aSet0(_179570), 778 ^ _155632 : [(779 ^ _155632) ^ [] : [aElementOf0(sbrdtbr0(_179570), szNzAzT0), -(isFinite0(_179570))], (785 ^ _155632) ^ [] : [isFinite0(_179570), -(aElementOf0(sbrdtbr0(_179570), szNzAzT0))]]], (791 ^ _155632) ^ [_180001] : [aSet0(_180001), 794 ^ _155632 : [(795 ^ _155632) ^ [] : [sbrdtbr0(_180001) = sz00, -(_180001 = slcrc0)], (801 ^ _155632) ^ [] : [_180001 = slcrc0, -(sbrdtbr0(_180001) = sz00)]]], (807 ^ _155632) ^ [_180435] : [aSet0(_180435), isFinite0(_180435), 814 ^ _155632 : [(815 ^ _155632) ^ [_180665] : [aElement0(_180665), -(aElementOf0(_180665, _180435)), -(sbrdtbr0(sdtpldt0(_180435, _180665)) = szszuzczcdt0(sbrdtbr0(_180435)))]]], (825 ^ _155632) ^ [_180978] : [aSet0(_180978), 828 ^ _155632 : [(829 ^ _155632) ^ [_181123] : [-(szszuzczcdt0(sbrdtbr0(sdtmndt0(_180978, _181123))) = sbrdtbr0(_180978)), isFinite0(_180978), aElementOf0(_181123, _180978)]]], (839 ^ _155632) ^ [_181431] : [aSet0(_181431), 842 ^ _155632 : [(843 ^ _155632) ^ [_181571] : [-(sdtlseqdt0(sbrdtbr0(_181571), sbrdtbr0(_181431))), isFinite0(_181431), aSubsetOf0(_181571, _181431)]]], (853 ^ _155632) ^ [_181883, _181885] : [aSet0(_181885), aElementOf0(_181883, szNzAzT0), 869 ^ _155632 : [(870 ^ _155632) ^ [] : [-(aSubsetOf0(868 ^ [_181883, _181885], _181885))], (872 ^ _155632) ^ [] : [-(sbrdtbr0(868 ^ [_181883, _181885]) = _181883)]], isFinite0(_181885), sdtlseqdt0(_181883, sbrdtbr0(_181885))], (874 ^ _155632) ^ [_182499] : [aSubsetOf0(_182499, szNzAzT0), -(_182499 = slcrc0), 881 ^ _155632 : [(882 ^ _155632) ^ [_182768] : [_182768 = szmzizndt0(_182499), 885 ^ _155632 : [(886 ^ _155632) ^ [] : [-(aElementOf0(_182768, _182499))], (888 ^ _155632) ^ [_182983] : [aElementOf0(_182983, _182499), -(sdtlseqdt0(_182768, _182983))]]], (894 ^ _155632) ^ [_183162] : [-(_183162 = szmzizndt0(_182499)), aElementOf0(_183162, _182499), 900 ^ _155632 : [(901 ^ _155632) ^ [] : [-(aElementOf0(899 ^ [_182499, _183162], _182499))], (903 ^ _155632) ^ [] : [sdtlseqdt0(_183162, 899 ^ [_182499, _183162])]]]]], (907 ^ _155632) ^ [_183607] : [aSubsetOf0(_183607, szNzAzT0), isFinite0(_183607), -(_183607 = slcrc0), 918 ^ _155632 : [(919 ^ _155632) ^ [_183959] : [_183959 = szmzazxdt0(_183607), 922 ^ _155632 : [(923 ^ _155632) ^ [] : [-(aElementOf0(_183959, _183607))], (925 ^ _155632) ^ [_184174] : [aElementOf0(_184174, _183607), -(sdtlseqdt0(_184174, _183959))]]], (931 ^ _155632) ^ [_184353] : [-(_184353 = szmzazxdt0(_183607)), aElementOf0(_184353, _183607), 937 ^ _155632 : [(938 ^ _155632) ^ [] : [-(aElementOf0(936 ^ [_183607, _184353], _183607))], (940 ^ _155632) ^ [] : [sdtlseqdt0(936 ^ [_183607, _184353], _184353)]]]]], (944 ^ _155632) ^ [_184814, _184816] : [-(szmzizndt0(_184816) = szmzizndt0(_184814)), aElementOf0(szmzizndt0(_184816), _184814), aElementOf0(szmzizndt0(_184814), _184816), aSubsetOf0(_184816, szNzAzT0), aSubsetOf0(_184814, szNzAzT0), -(_184816 = slcrc0), -(_184814 = slcrc0)], (970 ^ _155632) ^ [_185481] : [aElementOf0(_185481, szNzAzT0), 973 ^ _155632 : [(998 ^ _155632) ^ [_186450] : [-(_186450 = slbdtrb0(_185481)), aSet0(_186450), 1014 ^ _155632 : [(1015 ^ _155632) ^ [] : [-(aElementOf0(1003 ^ [_185481, _186450], szNzAzT0))], (1017 ^ _155632) ^ [] : [-(sdtlseqdt0(szszuzczcdt0(1003 ^ [_185481, _186450]), _185481))], (1019 ^ _155632) ^ [] : [aElementOf0(1003 ^ [_185481, _186450], _186450)]], 1006 ^ _155632 : [(1007 ^ _155632) ^ [] : [-(aElementOf0(1003 ^ [_185481, _186450], _186450))], (1009 ^ _155632) ^ [] : [aElementOf0(1003 ^ [_185481, _186450], szNzAzT0), sdtlseqdt0(szszuzczcdt0(1003 ^ [_185481, _186450]), _185481)]]], (974 ^ _155632) ^ [_185669] : [_185669 = slbdtrb0(_185481), 977 ^ _155632 : [(978 ^ _155632) ^ [] : [-(aSet0(_185669))], (980 ^ _155632) ^ [_185919] : [aElementOf0(_185919, _185669), 983 ^ _155632 : [(984 ^ _155632) ^ [] : [-(aElementOf0(_185919, szNzAzT0))], (986 ^ _155632) ^ [] : [-(sdtlseqdt0(szszuzczcdt0(_185919), _185481))]]], (988 ^ _155632) ^ [_186172] : [-(aElementOf0(_186172, _185669)), aElementOf0(_186172, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_186172), _185481)]]]]], (1023 ^ _155632) ^ [_187253] : [aElementOf0(_187253, szNzAzT0), -(isFinite0(slbdtrb0(_187253)))], (1029 ^ _155632) ^ [] : [-(slbdtrb0(sz00) = slcrc0)], (1031 ^ _155632) ^ [_187512, _187514] : [aElementOf0(_187514, szNzAzT0), aElementOf0(_187512, szNzAzT0), 1038 ^ _155632 : [(1049 ^ _155632) ^ [] : [1050 ^ _155632 : [(1051 ^ _155632) ^ [] : [aElementOf0(_187514, slbdtrb0(_187512))], (1053 ^ _155632) ^ [] : [_187514 = _187512]], -(aElementOf0(_187514, slbdtrb0(szszuzczcdt0(_187512))))], (1039 ^ _155632) ^ [] : [aElementOf0(_187514, slbdtrb0(szszuzczcdt0(_187512))), -(aElementOf0(_187514, slbdtrb0(_187512))), -(_187514 = _187512)]]], (1057 ^ _155632) ^ [_188239, _188241] : [aElementOf0(_188241, szNzAzT0), aElementOf0(_188239, szNzAzT0), 1064 ^ _155632 : [(1065 ^ _155632) ^ [] : [sdtlseqdt0(_188241, _188239), -(aSubsetOf0(slbdtrb0(_188241), slbdtrb0(_188239)))], (1071 ^ _155632) ^ [] : [aSubsetOf0(slbdtrb0(_188241), slbdtrb0(_188239)), -(sdtlseqdt0(_188241, _188239))]]], (1077 ^ _155632) ^ [_188788] : [1085 ^ _155632 : [(1086 ^ _155632) ^ [] : [-(aElementOf0(1084 ^ [_188788], szNzAzT0))], (1088 ^ _155632) ^ [] : [-(aSubsetOf0(_188788, slbdtrb0(1084 ^ [_188788])))]], aSubsetOf0(_188788, szNzAzT0), isFinite0(_188788)], (1090 ^ _155632) ^ [_189202] : [aElementOf0(_189202, szNzAzT0), -(sbrdtbr0(slbdtrb0(_189202)) = _189202)], (1096 ^ _155632) ^ [_189414, _189416] : [aSet0(_189416), aElementOf0(_189414, szNzAzT0), 1103 ^ _155632 : [(1128 ^ _155632) ^ [_190507] : [-(_190507 = slbdtsldtrb0(_189416, _189414)), aSet0(_190507), 1144 ^ _155632 : [(1145 ^ _155632) ^ [] : [-(aSubsetOf0(1133 ^ [_189414, _189416, _190507], _189416))], (1147 ^ _155632) ^ [] : [-(sbrdtbr0(1133 ^ [_189414, _189416, _190507]) = _189414)], (1149 ^ _155632) ^ [] : [aElementOf0(1133 ^ [_189414, _189416, _190507], _190507)]], 1136 ^ _155632 : [(1137 ^ _155632) ^ [] : [-(aElementOf0(1133 ^ [_189414, _189416, _190507], _190507))], (1139 ^ _155632) ^ [] : [aSubsetOf0(1133 ^ [_189414, _189416, _190507], _189416), sbrdtbr0(1133 ^ [_189414, _189416, _190507]) = _189414]]], (1104 ^ _155632) ^ [_189694] : [_189694 = slbdtsldtrb0(_189416, _189414), 1107 ^ _155632 : [(1108 ^ _155632) ^ [] : [-(aSet0(_189694))], (1110 ^ _155632) ^ [_189954] : [aElementOf0(_189954, _189694), 1113 ^ _155632 : [(1114 ^ _155632) ^ [] : [-(aSubsetOf0(_189954, _189416))], (1116 ^ _155632) ^ [] : [-(sbrdtbr0(_189954) = _189414)]]], (1118 ^ _155632) ^ [_190217] : [-(aElementOf0(_190217, _189694)), aSubsetOf0(_190217, _189416), sbrdtbr0(_190217) = _189414]]]]], (1153 ^ _155632) ^ [_191356] : [aSet0(_191356), isFinite0(_191356), 1160 ^ _155632 : [(1161 ^ _155632) ^ [_191572] : [aElementOf0(_191572, szNzAzT0), -(isFinite0(slbdtsldtrb0(_191356, _191572)))]]], (1167 ^ _155632) ^ [_191781] : [aSet0(_191781), -(isFinite0(_191781)), 1174 ^ _155632 : [(1175 ^ _155632) ^ [_192003] : [aElementOf0(_192003, szNzAzT0), slbdtsldtrb0(_191781, _192003) = slcrc0]]], (1181 ^ _155632) ^ [_192215] : [aSet0(_192215), isCountable0(_192215), 1188 ^ _155632 : [(1189 ^ _155632) ^ [_192439] : [-(isCountable0(slbdtsldtrb0(_192215, _192439))), aElementOf0(_192439, szNzAzT0), -(_192439 = sz00)]]], (1199 ^ _155632) ^ [] : [-(aElementOf0(xk, szNzAzT0))], (1201 ^ _155632) ^ [] : [-(aSet0(xS))], (1203 ^ _155632) ^ [] : [-(aSet0(xT))], (1205 ^ _155632) ^ [] : [xk = sz00], (1329 ^ _155632) ^ [] : [-(aElementOf0(xx, xS))], (1345 ^ _155632) ^ [] : [-(aSet0(xQ))], (1347 ^ _155632) ^ [] : [-(isFinite0(xQ))], (1349 ^ _155632) ^ [] : [-(sbrdtbr0(xQ) = xk)], (1352 ^ _155632) ^ [] : [-(aElementOf0(1350 ^ [], xQ))], (1354 ^ _155632) ^ [] : [xQ = slcrc0], (1331 ^ _155632) ^ [] : [-(aSet0(xQ))], (1339 ^ _155632) ^ [] : [-(aSubsetOf0(xQ, xS))], (1341 ^ _155632) ^ [] : [-(sbrdtbr0(xQ) = xk)], (1343 ^ _155632) ^ [] : [-(aElementOf0(xQ, slbdtsldtrb0(xS, xk)))], (1333 ^ _155632) ^ [_196933] : [aElementOf0(_196933, xQ), -(aElementOf0(_196933, xS))], (1207 ^ _155632) ^ [] : [-(aSet0(slbdtsldtrb0(xS, xk)))], (1209 ^ _155632) ^ [_193048] : [aElementOf0(_193048, slbdtsldtrb0(xS, xk)), 1212 ^ _155632 : [(1213 ^ _155632) ^ [] : [-(aSet0(_193048))], (1221 ^ _155632) ^ [] : [-(aSubsetOf0(_193048, xS))], (1223 ^ _155632) ^ [] : [-(sbrdtbr0(_193048) = xk)], (1215 ^ _155632) ^ [_193283] : [aElementOf0(_193283, _193048), -(aElementOf0(_193283, xS))]]], (1225 ^ _155632) ^ [_193570] : [-(aElementOf0(_193570, slbdtsldtrb0(xS, xk))), sbrdtbr0(_193570) = xk, 1228 ^ _155632 : [(1238 ^ _155632) ^ [] : [aSubsetOf0(_193570, xS)], (1229 ^ _155632) ^ [] : [aSet0(_193570), 1233 ^ _155632 : [(1234 ^ _155632) ^ [] : [-(aElementOf0(1232 ^ [_193570], _193570))], (1236 ^ _155632) ^ [] : [aElementOf0(1232 ^ [_193570], xS)]]]]], (1244 ^ _155632) ^ [] : [-(aSet0(slbdtsldtrb0(xT, xk)))], (1246 ^ _155632) ^ [_194214] : [aElementOf0(_194214, slbdtsldtrb0(xT, xk)), 1249 ^ _155632 : [(1250 ^ _155632) ^ [] : [-(aSet0(_194214))], (1258 ^ _155632) ^ [] : [-(aSubsetOf0(_194214, xT))], (1260 ^ _155632) ^ [] : [-(sbrdtbr0(_194214) = xk)], (1252 ^ _155632) ^ [_194449] : [aElementOf0(_194449, _194214), -(aElementOf0(_194449, xT))]]], (1262 ^ _155632) ^ [_194736] : [-(aElementOf0(_194736, slbdtsldtrb0(xT, xk))), sbrdtbr0(_194736) = xk, 1265 ^ _155632 : [(1275 ^ _155632) ^ [] : [aSubsetOf0(_194736, xT)], (1266 ^ _155632) ^ [] : [aSet0(_194736), 1270 ^ _155632 : [(1271 ^ _155632) ^ [] : [-(aElementOf0(1269 ^ [_194736], _194736))], (1273 ^ _155632) ^ [] : [aElementOf0(1269 ^ [_194736], xT)]]]]], (1281 ^ _155632) ^ [_195307] : [aElementOf0(_195307, slbdtsldtrb0(xS, xk)), -(aElementOf0(_195307, slbdtsldtrb0(xT, xk)))], (1287 ^ _155632) ^ [] : [-(aSubsetOf0(slbdtsldtrb0(xS, xk), slbdtsldtrb0(xT, xk)))], (1325 ^ _155632) ^ [] : [-(aElementOf0(1323 ^ [], slbdtsldtrb0(xS, xk)))], (1327 ^ _155632) ^ [] : [slbdtsldtrb0(xS, xk) = slcrc0], (1289 ^ _155632) ^ [_195570] : [aElementOf0(_195570, slbdtsldtrb0(xS, xk)), 1292 ^ _155632 : [(1293 ^ _155632) ^ [] : [-(aSet0(_195570))], (1301 ^ _155632) ^ [] : [-(aSubsetOf0(_195570, xS))], (1303 ^ _155632) ^ [] : [-(sbrdtbr0(_195570) = xk)], (1295 ^ _155632) ^ [_195805] : [aElementOf0(_195805, _195570), -(aElementOf0(_195805, xS))]]], (1305 ^ _155632) ^ [_196092] : [-(aElementOf0(_196092, slbdtsldtrb0(xS, xk))), sbrdtbr0(_196092) = xk, 1308 ^ _155632 : [(1318 ^ _155632) ^ [] : [aSubsetOf0(_196092, xS)], (1309 ^ _155632) ^ [] : [aSet0(_196092), 1313 ^ _155632 : [(1314 ^ _155632) ^ [] : [-(aElementOf0(1312 ^ [_196092], _196092))], (1316 ^ _155632) ^ [] : [aElementOf0(1312 ^ [_196092], xS)]]]]]], input).
% 0.37/1.38 ncf('1',plain,[aElement0(233 ^ [xQ]), aElementOf0(233 ^ [xQ], xQ)],start(1356 ^ 0,bind([[_198040], [233 ^ [xQ]]]))).
% 0.37/1.38 ncf('1.1',plain,[-(aElement0(233 ^ [xQ])), 200 : aElementOf0(233 ^ [xQ], xQ), 200 : aSet0(xQ)],extension(196 ^ 1,bind([[_162029, _162159], [xQ, 233 ^ [xQ]]]))).
% 0.37/1.38 ncf('1.1.1',plain,[-(aElementOf0(233 ^ [xQ], xQ)), -(xQ = slcrc0), aSet0(xQ)],extension(228 ^ 4,bind([[_162979], [xQ]]))).
% 0.37/1.38 ncf('1.1.1.1',plain,[xQ = slcrc0],extension(1354 ^ 5)).
% 0.37/1.38 ncf('1.1.1.2',plain,[-(aSet0(xQ))],extension(1345 ^ 5)).
% 0.37/1.38 ncf('1.1.2',plain,[-(aSet0(xQ)), 279 : aSubsetOf0(xQ, xS), 279 : aSet0(xS)],extension(275 ^ 2,bind([[_164244, _164420], [xS, xQ]]))).
% 0.37/1.38 ncf('1.1.2.1',plain,[-(aSubsetOf0(xQ, xS))],extension(1339 ^ 5)).
% 0.37/1.38 ncf('1.1.2.2',plain,[-(aSet0(xS))],extension(1201 ^ 3)).
% 0.37/1.38 ncf('1.2',plain,[-(aElementOf0(233 ^ [xQ], xQ)), aElementOf0(233 ^ [xQ], xQ), 233 ^ [xQ] = 233 ^ [xQ], xQ = xQ],extension(102 ^ 1,bind([[_158920, _158922, _158924, _158926], [xQ, xQ, 233 ^ [xQ], 233 ^ [xQ]]]))).
% 0.37/1.38 ncf('1.2.1',plain,[-(aElementOf0(233 ^ [xQ], xQ)), -(xQ = slcrc0), aSet0(xQ)],extension(228 ^ 2,bind([[_162979], [xQ]]))).
% 0.37/1.38 ncf('1.2.1.1',plain,[xQ = slcrc0],extension(1354 ^ 3)).
% 0.37/1.38 ncf('1.2.1.2',plain,[-(aSet0(xQ))],extension(1345 ^ 3)).
% 0.37/1.38 ncf('1.2.2',plain,[-(233 ^ [xQ] = 233 ^ [xQ])],extension(2 ^ 2,bind([[_155776], [233 ^ [xQ]]]))).
% 0.37/1.38 ncf('1.2.3',plain,[-(xQ = xQ)],extension(2 ^ 2,bind([[_155776], [xQ]]))).
% 0.37/1.38 %-----------------------------------------------------
% 0.37/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------