%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM634+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n012.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:13 EDT 2023
% Result : Theorem 0.36s 1.38s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM634+1 : TPTP v8.1.2. Released v4.0.0.
% 0.12/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n012.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 18 17:25:17 EDT 2023
% 0.12/0.34 % CPUTime :
% 0.36/1.38
% 0.36/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.36/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.38 %-----------------------------------------------------
% 0.36/1.38 ncf(matrix, plain, [(1615 ^ _184986) ^ [_237493] : [aElementOf0(_237493, xT), 1618 ^ _184986 : [(1619 ^ _184986) ^ [_237648] : [aSubsetOf0(_237648, xS), isCountable0(_237648), 1627 ^ _184986 : [(1628 ^ _184986) ^ [] : [-(aElementOf0(1626 ^ [_237493, _237648], slbdtsldtrb0(_237648, xK)))], (1630 ^ _184986) ^ [] : [sdtlpdtrp0(xc, 1626 ^ [_237493, _237648]) = _237493]]]]], (126 ^ _184986) ^ [_189035, _189037, _189039, _189041] : [-(sdtpldt0(_189041, _189037) = sdtpldt0(_189039, _189035)), _189041 = _189039, _189037 = _189035], (136 ^ _184986) ^ [_189394, _189396, _189398, _189400] : [-(sdtmndt0(_189400, _189396) = sdtmndt0(_189398, _189394)), _189400 = _189398, _189396 = _189394], (146 ^ _184986) ^ [_189725, _189727] : [_189727 = _189725, -(szmzazxdt0(_189727) = szmzazxdt0(_189725))], (152 ^ _184986) ^ [_189943, _189945] : [_189945 = _189943, -(szmzizndt0(_189945) = szmzizndt0(_189943))], (158 ^ _184986) ^ [_190161, _190163] : [_190163 = _190161, -(szszuzczcdt0(_190163) = szszuzczcdt0(_190161))], (164 ^ _184986) ^ [_190379, _190381] : [_190381 = _190379, -(slbdtrb0(_190381) = slbdtrb0(_190379))], (170 ^ _184986) ^ [_190597, _190599] : [_190599 = _190597, -(sbrdtbr0(_190599) = sbrdtbr0(_190597))], (176 ^ _184986) ^ [_190843, _190845, _190847, _190849] : [-(sdtexdt0(_190849, _190845) = sdtexdt0(_190847, _190843)), _190849 = _190847, _190845 = _190843], (186 ^ _184986) ^ [_191202, _191204, _191206, _191208] : [-(sdtlbdtrb0(_191208, _191204) = sdtlbdtrb0(_191206, _191202)), _191208 = _191206, _191204 = _191202], (196 ^ _184986) ^ [_191533, _191535] : [_191535 = _191533, -(szDzizrdt0(_191535) = szDzizrdt0(_191533))], (202 ^ _184986) ^ [_191779, _191781, _191783, _191785] : [-(sdtlcdtrc0(_191785, _191781) = sdtlcdtrc0(_191783, _191779)), _191785 = _191783, _191781 = _191779], (212 ^ _184986) ^ [_192110, _192112] : [_192112 = _192110, -(szDzozmdt0(_192112) = szDzozmdt0(_192110))], (218 ^ _184986) ^ [_192356, _192358, _192360, _192362] : [-(slbdtsldtrb0(_192362, _192358) = slbdtsldtrb0(_192360, _192356)), _192362 = _192360, _192358 = _192356], (228 ^ _184986) ^ [_192695, _192697, _192699, _192701] : [-(sdtlpdtrp0(_192701, _192697) = sdtlpdtrp0(_192699, _192695)), _192701 = _192699, _192697 = _192695], (2 ^ _184986) ^ [_185130] : [-(_185130 = _185130)], (4 ^ _184986) ^ [_185237, _185239] : [_185239 = _185237, -(_185237 = _185239)], (10 ^ _184986) ^ [_185441, _185443, _185445] : [-(_185445 = _185441), _185445 = _185443, _185443 = _185441], (20 ^ _184986) ^ [_185782, _185784, _185786, _185788] : [-(sdtlseqdt0(_185786, _185782)), sdtlseqdt0(_185788, _185784), _185788 = _185786, _185784 = _185782], (34 ^ _184986) ^ [_186198, _186200] : [-(aElement0(_186198)), _186200 = _186198, aElement0(_186200)], (44 ^ _184986) ^ [_186493, _186495] : [-(aSet0(_186493)), _186495 = _186493, aSet0(_186495)], (54 ^ _184986) ^ [_186788, _186790] : [-(isFinite0(_186788)), _186790 = _186788, isFinite0(_186790)], (64 ^ _184986) ^ [_187083, _187085] : [-(aFunction0(_187083)), _187085 = _187083, aFunction0(_187085)], (74 ^ _184986) ^ [_187406, _187408, _187410, _187412] : [-(iLess0(_187410, _187406)), iLess0(_187412, _187408), _187412 = _187410, _187408 = _187406], (88 ^ _184986) ^ [_187850, _187852, _187854, _187856] : [-(aSubsetOf0(_187854, _187850)), aSubsetOf0(_187856, _187852), _187856 = _187854, _187852 = _187850], (102 ^ _184986) ^ [_188266, _188268] : [-(isCountable0(_188266)), _188268 = _188266, isCountable0(_188268)], (112 ^ _184986) ^ [_188569, _188571, _188573, _188575] : [-(aElementOf0(_188573, _188569)), aElementOf0(_188575, _188571), _188575 = _188573, _188571 = _188569], (238 ^ _184986) ^ [_193098] : [aSet0(_193098), true___, -(true___)], (248 ^ _184986) ^ [_193353] : [aElement0(_193353), true___, -(true___)], (258 ^ _184986) ^ [_193608] : [aSet0(_193608), 261 ^ _184986 : [(262 ^ _184986) ^ [_193738] : [aElementOf0(_193738, _193608), -(aElement0(_193738))]]], (268 ^ _184986) ^ [_193939] : [aSet0(_193939), isFinite0(_193939), true___, -(true___)], (282 ^ _184986) ^ [_194309] : [_194309 = slcrc0, 285 ^ _184986 : [(286 ^ _184986) ^ [] : [-(aSet0(_194309))], (288 ^ _184986) ^ [_194490] : [aElementOf0(_194490, _194309)]]], (290 ^ _184986) ^ [_194558] : [-(_194558 = slcrc0), aSet0(_194558), -(aElementOf0(295 ^ [_194558], _194558))], (301 ^ _184986) ^ [] : [-(isFinite0(slcrc0))], (303 ^ _184986) ^ [_194940] : [aSet0(_194940), isCountable0(_194940), true___, -(true___)], (317 ^ _184986) ^ [_195281] : [isFinite0(_195281), aSet0(_195281), isCountable0(_195281)], (327 ^ _184986) ^ [_195551] : [_195551 = slcrc0, aSet0(_195551), isCountable0(_195551)], (337 ^ _184986) ^ [_195823] : [aSet0(_195823), 340 ^ _184986 : [(341 ^ _184986) ^ [_195999] : [aSubsetOf0(_195999, _195823), 344 ^ _184986 : [(345 ^ _184986) ^ [] : [-(aSet0(_195999))], (347 ^ _184986) ^ [_196208] : [aElementOf0(_196208, _195999), -(aElementOf0(_196208, _195823))]]], (353 ^ _184986) ^ [_196387] : [-(aSubsetOf0(_196387, _195823)), aSet0(_196387), 359 ^ _184986 : [(360 ^ _184986) ^ [] : [-(aElementOf0(358 ^ [_195823, _196387], _196387))], (362 ^ _184986) ^ [] : [aElementOf0(358 ^ [_195823, _196387], _195823)]]]]], (366 ^ _184986) ^ [_196824] : [aSet0(_196824), isFinite0(_196824), 373 ^ _184986 : [(374 ^ _184986) ^ [_197037] : [aSubsetOf0(_197037, _196824), -(isFinite0(_197037))]]], (380 ^ _184986) ^ [_197240] : [aSet0(_197240), -(aSubsetOf0(_197240, _197240))], (386 ^ _184986) ^ [_197442, _197444] : [aSet0(_197444), aSet0(_197442), -(_197444 = _197442), aSubsetOf0(_197444, _197442), aSubsetOf0(_197442, _197444)], (404 ^ _184986) ^ [_197931, _197933, _197935] : [aSet0(_197935), aSet0(_197933), aSet0(_197931), -(aSubsetOf0(_197935, _197931)), aSubsetOf0(_197935, _197933), aSubsetOf0(_197933, _197931)], (426 ^ _184986) ^ [_198517, _198519] : [aSet0(_198519), aElement0(_198517), 433 ^ _184986 : [(464 ^ _184986) ^ [_199778] : [-(_199778 = sdtpldt0(_198519, _198517)), aSet0(_199778), 472 ^ _184986 : [(473 ^ _184986) ^ [] : [-(aElementOf0(469 ^ [_198517, _198519, _199778], _199778))], (475 ^ _184986) ^ [] : [aElement0(469 ^ [_198517, _198519, _199778]), 478 ^ _184986 : [(479 ^ _184986) ^ [] : [aElementOf0(469 ^ [_198517, _198519, _199778], _198519)], (481 ^ _184986) ^ [] : [469 ^ [_198517, _198519, _199778] = _198517]]]], 482 ^ _184986 : [(491 ^ _184986) ^ [] : [aElementOf0(469 ^ [_198517, _198519, _199778], _199778)], (483 ^ _184986) ^ [] : [-(aElement0(469 ^ [_198517, _198519, _199778]))], (485 ^ _184986) ^ [] : [-(aElementOf0(469 ^ [_198517, _198519, _199778], _198519)), -(469 ^ [_198517, _198519, _199778] = _198517)]]], (434 ^ _184986) ^ [_198798] : [_198798 = sdtpldt0(_198519, _198517), 437 ^ _184986 : [(438 ^ _184986) ^ [] : [-(aSet0(_198798))], (440 ^ _184986) ^ [_199061] : [aElementOf0(_199061, _198798), 443 ^ _184986 : [(444 ^ _184986) ^ [] : [-(aElement0(_199061))], (446 ^ _184986) ^ [] : [-(aElementOf0(_199061, _198519)), -(_199061 = _198517)]]], (452 ^ _184986) ^ [_199416] : [-(aElementOf0(_199416, _198798)), aElement0(_199416), 457 ^ _184986 : [(458 ^ _184986) ^ [] : [aElementOf0(_199416, _198519)], (460 ^ _184986) ^ [] : [_199416 = _198517]]]]]]], (495 ^ _184986) ^ [_200815, _200817] : [aSet0(_200817), aElement0(_200815), 502 ^ _184986 : [(533 ^ _184986) ^ [_202083] : [-(_202083 = sdtmndt0(_200817, _200815)), aSet0(_202083), 553 ^ _184986 : [(554 ^ _184986) ^ [] : [-(aElement0(538 ^ [_200815, _200817, _202083]))], (556 ^ _184986) ^ [] : [-(aElementOf0(538 ^ [_200815, _200817, _202083], _200817))], (558 ^ _184986) ^ [] : [538 ^ [_200815, _200817, _202083] = _200815], (560 ^ _184986) ^ [] : [aElementOf0(538 ^ [_200815, _200817, _202083], _202083)]], 541 ^ _184986 : [(542 ^ _184986) ^ [] : [-(aElementOf0(538 ^ [_200815, _200817, _202083], _202083))], (544 ^ _184986) ^ [] : [aElement0(538 ^ [_200815, _200817, _202083]), aElementOf0(538 ^ [_200815, _200817, _202083], _200817), -(538 ^ [_200815, _200817, _202083] = _200815)]]], (503 ^ _184986) ^ [_201098] : [_201098 = sdtmndt0(_200817, _200815), 506 ^ _184986 : [(507 ^ _184986) ^ [] : [-(aSet0(_201098))], (509 ^ _184986) ^ [_201363] : [aElementOf0(_201363, _201098), 512 ^ _184986 : [(513 ^ _184986) ^ [] : [-(aElement0(_201363))], (515 ^ _184986) ^ [] : [-(aElementOf0(_201363, _200817))], (517 ^ _184986) ^ [] : [_201363 = _200815]]], (519 ^ _184986) ^ [_201699] : [-(aElementOf0(_201699, _201098)), aElement0(_201699), aElementOf0(_201699, _200817), -(_201699 = _200815)]]]]], (564 ^ _184986) ^ [_203113] : [aSet0(_203113), 567 ^ _184986 : [(568 ^ _184986) ^ [_203250] : [aElementOf0(_203250, _203113), -(sdtpldt0(sdtmndt0(_203113, _203250), _203250) = _203113)]]], (574 ^ _184986) ^ [_203479, _203481] : [aElement0(_203481), aSet0(_203479), -(aElementOf0(_203481, _203479)), -(sdtmndt0(sdtpldt0(_203479, _203481), _203481) = _203479)], (588 ^ _184986) ^ [_203866] : [aElement0(_203866), 591 ^ _184986 : [(592 ^ _184986) ^ [_204003] : [-(isCountable0(sdtpldt0(_204003, _203866))), aSet0(_204003), isCountable0(_204003)]]], (602 ^ _184986) ^ [_204295] : [aElement0(_204295), 605 ^ _184986 : [(606 ^ _184986) ^ [_204432] : [-(isCountable0(sdtmndt0(_204432, _204295))), aSet0(_204432), isCountable0(_204432)]]], (616 ^ _184986) ^ [_204724] : [aElement0(_204724), 619 ^ _184986 : [(620 ^ _184986) ^ [_204861] : [-(isFinite0(sdtpldt0(_204861, _204724))), aSet0(_204861), isFinite0(_204861)]]], (630 ^ _184986) ^ [_205153] : [aElement0(_205153), 633 ^ _184986 : [(634 ^ _184986) ^ [_205290] : [-(isFinite0(sdtmndt0(_205290, _205153))), aSet0(_205290), isFinite0(_205290)]]], (644 ^ _184986) ^ [] : [-(aSet0(szNzAzT0))], (646 ^ _184986) ^ [] : [-(isCountable0(szNzAzT0))], (648 ^ _184986) ^ [] : [-(aElementOf0(sz00, szNzAzT0))], (650 ^ _184986) ^ [_205743] : [aElementOf0(_205743, szNzAzT0), 653 ^ _184986 : [(654 ^ _184986) ^ [] : [-(aElementOf0(szszuzczcdt0(_205743), szNzAzT0))], (656 ^ _184986) ^ [] : [szszuzczcdt0(_205743) = sz00]]], (658 ^ _184986) ^ [_206029, _206031] : [aElementOf0(_206031, szNzAzT0), aElementOf0(_206029, szNzAzT0), szszuzczcdt0(_206031) = szszuzczcdt0(_206029), -(_206031 = _206029)], (672 ^ _184986) ^ [_206413] : [aElementOf0(_206413, szNzAzT0), -(_206413 = sz00), 680 ^ _184986 : [(681 ^ _184986) ^ [] : [-(aElementOf0(679 ^ [_206413], szNzAzT0))], (683 ^ _184986) ^ [] : [-(_206413 = szszuzczcdt0(679 ^ [_206413]))]]], (685 ^ _184986) ^ [_206830] : [aElementOf0(_206830, szNzAzT0), _206830 = szszuzczcdt0(_206830)], (691 ^ _184986) ^ [_207039, _207041] : [aElementOf0(_207041, szNzAzT0), aElementOf0(_207039, szNzAzT0), sdtlseqdt0(_207041, _207039), true___, -(true___)], (709 ^ _184986) ^ [_207489] : [aElementOf0(_207489, szNzAzT0), -(sdtlseqdt0(sz00, _207489))], (715 ^ _184986) ^ [_207679] : [aElementOf0(_207679, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_207679), sz00)], (721 ^ _184986) ^ [_207888, _207890] : [aElementOf0(_207890, szNzAzT0), aElementOf0(_207888, szNzAzT0), 728 ^ _184986 : [(729 ^ _184986) ^ [] : [sdtlseqdt0(_207890, _207888), -(sdtlseqdt0(szszuzczcdt0(_207890), szszuzczcdt0(_207888)))], (735 ^ _184986) ^ [] : [sdtlseqdt0(szszuzczcdt0(_207890), szszuzczcdt0(_207888)), -(sdtlseqdt0(_207890, _207888))]]], (741 ^ _184986) ^ [_208437] : [aElementOf0(_208437, szNzAzT0), -(sdtlseqdt0(_208437, szszuzczcdt0(_208437)))], (747 ^ _184986) ^ [_208631] : [aElementOf0(_208631, szNzAzT0), -(sdtlseqdt0(_208631, _208631))], (753 ^ _184986) ^ [_208835, _208837] : [aElementOf0(_208837, szNzAzT0), aElementOf0(_208835, szNzAzT0), -(_208837 = _208835), sdtlseqdt0(_208837, _208835), sdtlseqdt0(_208835, _208837)], (771 ^ _184986) ^ [_209328, _209330, _209332] : [aElementOf0(_209332, szNzAzT0), aElementOf0(_209330, szNzAzT0), aElementOf0(_209328, szNzAzT0), -(sdtlseqdt0(_209332, _209328)), sdtlseqdt0(_209332, _209330), sdtlseqdt0(_209330, _209328)], (793 ^ _184986) ^ [_209920, _209922] : [aElementOf0(_209922, szNzAzT0), aElementOf0(_209920, szNzAzT0), -(sdtlseqdt0(_209922, _209920)), -(sdtlseqdt0(szszuzczcdt0(_209920), _209922))], (807 ^ _184986) ^ [_210315, _210317] : [aElementOf0(_210317, szNzAzT0), aElementOf0(_210315, szNzAzT0), iLess0(_210317, _210315), true___, -(true___)], (825 ^ _184986) ^ [_210765] : [aElementOf0(_210765, szNzAzT0), -(iLess0(_210765, szszuzczcdt0(_210765)))], (831 ^ _184986) ^ [_210959] : [aSet0(_210959), -(aElement0(sbrdtbr0(_210959)))], (837 ^ _184986) ^ [_211149] : [aSet0(_211149), 840 ^ _184986 : [(841 ^ _184986) ^ [] : [aElementOf0(sbrdtbr0(_211149), szNzAzT0), -(isFinite0(_211149))], (847 ^ _184986) ^ [] : [isFinite0(_211149), -(aElementOf0(sbrdtbr0(_211149), szNzAzT0))]]], (853 ^ _184986) ^ [_211580] : [aSet0(_211580), 856 ^ _184986 : [(857 ^ _184986) ^ [] : [sbrdtbr0(_211580) = sz00, -(_211580 = slcrc0)], (863 ^ _184986) ^ [] : [_211580 = slcrc0, -(sbrdtbr0(_211580) = sz00)]]], (869 ^ _184986) ^ [_212014] : [aSet0(_212014), isFinite0(_212014), 876 ^ _184986 : [(877 ^ _184986) ^ [_212244] : [aElement0(_212244), -(aElementOf0(_212244, _212014)), -(sbrdtbr0(sdtpldt0(_212014, _212244)) = szszuzczcdt0(sbrdtbr0(_212014)))]]], (887 ^ _184986) ^ [_212557] : [aSet0(_212557), 890 ^ _184986 : [(891 ^ _184986) ^ [_212702] : [-(szszuzczcdt0(sbrdtbr0(sdtmndt0(_212557, _212702))) = sbrdtbr0(_212557)), isFinite0(_212557), aElementOf0(_212702, _212557)]]], (901 ^ _184986) ^ [_213010] : [aSet0(_213010), 904 ^ _184986 : [(905 ^ _184986) ^ [_213150] : [-(sdtlseqdt0(sbrdtbr0(_213150), sbrdtbr0(_213010))), isFinite0(_213010), aSubsetOf0(_213150, _213010)]]], (915 ^ _184986) ^ [_213462, _213464] : [aSet0(_213464), aElementOf0(_213462, szNzAzT0), 931 ^ _184986 : [(932 ^ _184986) ^ [] : [-(aSubsetOf0(930 ^ [_213462, _213464], _213464))], (934 ^ _184986) ^ [] : [-(sbrdtbr0(930 ^ [_213462, _213464]) = _213462)]], isFinite0(_213464), sdtlseqdt0(_213462, sbrdtbr0(_213464))], (936 ^ _184986) ^ [_214078] : [aSubsetOf0(_214078, szNzAzT0), -(_214078 = slcrc0), 943 ^ _184986 : [(944 ^ _184986) ^ [_214347] : [_214347 = szmzizndt0(_214078), 947 ^ _184986 : [(948 ^ _184986) ^ [] : [-(aElementOf0(_214347, _214078))], (950 ^ _184986) ^ [_214562] : [aElementOf0(_214562, _214078), -(sdtlseqdt0(_214347, _214562))]]], (956 ^ _184986) ^ [_214741] : [-(_214741 = szmzizndt0(_214078)), aElementOf0(_214741, _214078), 962 ^ _184986 : [(963 ^ _184986) ^ [] : [-(aElementOf0(961 ^ [_214078, _214741], _214078))], (965 ^ _184986) ^ [] : [sdtlseqdt0(_214741, 961 ^ [_214078, _214741])]]]]], (969 ^ _184986) ^ [_215186] : [aSubsetOf0(_215186, szNzAzT0), isFinite0(_215186), -(_215186 = slcrc0), 980 ^ _184986 : [(981 ^ _184986) ^ [_215538] : [_215538 = szmzazxdt0(_215186), 984 ^ _184986 : [(985 ^ _184986) ^ [] : [-(aElementOf0(_215538, _215186))], (987 ^ _184986) ^ [_215753] : [aElementOf0(_215753, _215186), -(sdtlseqdt0(_215753, _215538))]]], (993 ^ _184986) ^ [_215932] : [-(_215932 = szmzazxdt0(_215186)), aElementOf0(_215932, _215186), 999 ^ _184986 : [(1000 ^ _184986) ^ [] : [-(aElementOf0(998 ^ [_215186, _215932], _215186))], (1002 ^ _184986) ^ [] : [sdtlseqdt0(998 ^ [_215186, _215932], _215932)]]]]], (1006 ^ _184986) ^ [_216393, _216395] : [-(szmzizndt0(_216395) = szmzizndt0(_216393)), aElementOf0(szmzizndt0(_216395), _216393), aElementOf0(szmzizndt0(_216393), _216395), aSubsetOf0(_216395, szNzAzT0), aSubsetOf0(_216393, szNzAzT0), -(_216395 = slcrc0), -(_216393 = slcrc0)], (1032 ^ _184986) ^ [_217060] : [aElementOf0(_217060, szNzAzT0), 1035 ^ _184986 : [(1060 ^ _184986) ^ [_218029] : [-(_218029 = slbdtrb0(_217060)), aSet0(_218029), 1076 ^ _184986 : [(1077 ^ _184986) ^ [] : [-(aElementOf0(1065 ^ [_217060, _218029], szNzAzT0))], (1079 ^ _184986) ^ [] : [-(sdtlseqdt0(szszuzczcdt0(1065 ^ [_217060, _218029]), _217060))], (1081 ^ _184986) ^ [] : [aElementOf0(1065 ^ [_217060, _218029], _218029)]], 1068 ^ _184986 : [(1069 ^ _184986) ^ [] : [-(aElementOf0(1065 ^ [_217060, _218029], _218029))], (1071 ^ _184986) ^ [] : [aElementOf0(1065 ^ [_217060, _218029], szNzAzT0), sdtlseqdt0(szszuzczcdt0(1065 ^ [_217060, _218029]), _217060)]]], (1036 ^ _184986) ^ [_217248] : [_217248 = slbdtrb0(_217060), 1039 ^ _184986 : [(1040 ^ _184986) ^ [] : [-(aSet0(_217248))], (1042 ^ _184986) ^ [_217498] : [aElementOf0(_217498, _217248), 1045 ^ _184986 : [(1046 ^ _184986) ^ [] : [-(aElementOf0(_217498, szNzAzT0))], (1048 ^ _184986) ^ [] : [-(sdtlseqdt0(szszuzczcdt0(_217498), _217060))]]], (1050 ^ _184986) ^ [_217751] : [-(aElementOf0(_217751, _217248)), aElementOf0(_217751, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_217751), _217060)]]]]], (1085 ^ _184986) ^ [_218832] : [aElementOf0(_218832, szNzAzT0), -(isFinite0(slbdtrb0(_218832)))], (1091 ^ _184986) ^ [] : [-(slbdtrb0(sz00) = slcrc0)], (1093 ^ _184986) ^ [_219091, _219093] : [aElementOf0(_219093, szNzAzT0), aElementOf0(_219091, szNzAzT0), 1100 ^ _184986 : [(1111 ^ _184986) ^ [] : [1112 ^ _184986 : [(1113 ^ _184986) ^ [] : [aElementOf0(_219093, slbdtrb0(_219091))], (1115 ^ _184986) ^ [] : [_219093 = _219091]], -(aElementOf0(_219093, slbdtrb0(szszuzczcdt0(_219091))))], (1101 ^ _184986) ^ [] : [aElementOf0(_219093, slbdtrb0(szszuzczcdt0(_219091))), -(aElementOf0(_219093, slbdtrb0(_219091))), -(_219093 = _219091)]]], (1119 ^ _184986) ^ [_219818, _219820] : [aElementOf0(_219820, szNzAzT0), aElementOf0(_219818, szNzAzT0), 1126 ^ _184986 : [(1127 ^ _184986) ^ [] : [sdtlseqdt0(_219820, _219818), -(aSubsetOf0(slbdtrb0(_219820), slbdtrb0(_219818)))], (1133 ^ _184986) ^ [] : [aSubsetOf0(slbdtrb0(_219820), slbdtrb0(_219818)), -(sdtlseqdt0(_219820, _219818))]]], (1139 ^ _184986) ^ [_220367] : [1147 ^ _184986 : [(1148 ^ _184986) ^ [] : [-(aElementOf0(1146 ^ [_220367], szNzAzT0))], (1150 ^ _184986) ^ [] : [-(aSubsetOf0(_220367, slbdtrb0(1146 ^ [_220367])))]], aSubsetOf0(_220367, szNzAzT0), isFinite0(_220367)], (1152 ^ _184986) ^ [_220781] : [aElementOf0(_220781, szNzAzT0), -(sbrdtbr0(slbdtrb0(_220781)) = _220781)], (1158 ^ _184986) ^ [_220993, _220995] : [aSet0(_220995), aElementOf0(_220993, szNzAzT0), 1165 ^ _184986 : [(1190 ^ _184986) ^ [_222086] : [-(_222086 = slbdtsldtrb0(_220995, _220993)), aSet0(_222086), 1206 ^ _184986 : [(1207 ^ _184986) ^ [] : [-(aSubsetOf0(1195 ^ [_220993, _220995, _222086], _220995))], (1209 ^ _184986) ^ [] : [-(sbrdtbr0(1195 ^ [_220993, _220995, _222086]) = _220993)], (1211 ^ _184986) ^ [] : [aElementOf0(1195 ^ [_220993, _220995, _222086], _222086)]], 1198 ^ _184986 : [(1199 ^ _184986) ^ [] : [-(aElementOf0(1195 ^ [_220993, _220995, _222086], _222086))], (1201 ^ _184986) ^ [] : [aSubsetOf0(1195 ^ [_220993, _220995, _222086], _220995), sbrdtbr0(1195 ^ [_220993, _220995, _222086]) = _220993]]], (1166 ^ _184986) ^ [_221273] : [_221273 = slbdtsldtrb0(_220995, _220993), 1169 ^ _184986 : [(1170 ^ _184986) ^ [] : [-(aSet0(_221273))], (1172 ^ _184986) ^ [_221533] : [aElementOf0(_221533, _221273), 1175 ^ _184986 : [(1176 ^ _184986) ^ [] : [-(aSubsetOf0(_221533, _220995))], (1178 ^ _184986) ^ [] : [-(sbrdtbr0(_221533) = _220993)]]], (1180 ^ _184986) ^ [_221796] : [-(aElementOf0(_221796, _221273)), aSubsetOf0(_221796, _220995), sbrdtbr0(_221796) = _220993]]]]], (1215 ^ _184986) ^ [_222935] : [aSet0(_222935), isFinite0(_222935), 1222 ^ _184986 : [(1223 ^ _184986) ^ [_223151] : [aElementOf0(_223151, szNzAzT0), -(isFinite0(slbdtsldtrb0(_222935, _223151)))]]], (1229 ^ _184986) ^ [_223360] : [aSet0(_223360), -(isFinite0(_223360)), 1236 ^ _184986 : [(1237 ^ _184986) ^ [_223582] : [aElementOf0(_223582, szNzAzT0), slbdtsldtrb0(_223360, _223582) = slcrc0]]], (1243 ^ _184986) ^ [_223794] : [aSet0(_223794), isCountable0(_223794), 1250 ^ _184986 : [(1251 ^ _184986) ^ [_224018] : [-(isCountable0(slbdtsldtrb0(_223794, _224018))), aElementOf0(_224018, szNzAzT0), -(_224018 = sz00)]]], (1261 ^ _184986) ^ [_224319] : [aElementOf0(_224319, szNzAzT0), 1264 ^ _184986 : [(1265 ^ _184986) ^ [_224506, _224508] : [aSet0(_224508), aSet0(_224506), -(_224319 = sz00), -(aSubsetOf0(_224508, _224506)), aSubsetOf0(slbdtsldtrb0(_224508, _224319), slbdtsldtrb0(_224506, _224319)), -(slbdtsldtrb0(_224508, _224319) = slcrc0)]]], (1287 ^ _184986) ^ [_225125, _225127] : [aSet0(_225127), aElementOf0(_225125, szNzAzT0), 1294 ^ _184986 : [(1295 ^ _184986) ^ [_225376] : [1303 ^ _184986 : [(1304 ^ _184986) ^ [] : [-(aSubsetOf0(1302 ^ [_225125, _225127, _225376], _225127))], (1306 ^ _184986) ^ [] : [-(isFinite0(1302 ^ [_225125, _225127, _225376]))], (1308 ^ _184986) ^ [] : [-(aSubsetOf0(_225376, slbdtsldtrb0(1302 ^ [_225125, _225127, _225376], _225125)))]], aSubsetOf0(_225376, slbdtsldtrb0(_225127, _225125)), isFinite0(_225376)]]], (1310 ^ _184986) ^ [_225938] : [aFunction0(_225938), true___, -(true___)], (1320 ^ _184986) ^ [_226193] : [aFunction0(_226193), -(aSet0(szDzozmdt0(_226193)))], (1326 ^ _184986) ^ [_226383] : [aFunction0(_226383), 1329 ^ _184986 : [(1330 ^ _184986) ^ [_226518] : [aElementOf0(_226518, szDzozmdt0(_226383)), -(aElement0(sdtlpdtrp0(_226383, _226518)))]]], (1336 ^ _184986) ^ [_226743, _226745] : [aFunction0(_226745), aElement0(_226743), 1343 ^ _184986 : [(1368 ^ _184986) ^ [_227852] : [-(_227852 = sdtlbdtrb0(_226745, _226743)), aSet0(_227852), 1384 ^ _184986 : [(1385 ^ _184986) ^ [] : [-(aElementOf0(1373 ^ [_226743, _226745, _227852], szDzozmdt0(_226745)))], (1387 ^ _184986) ^ [] : [-(sdtlpdtrp0(_226745, 1373 ^ [_226743, _226745, _227852]) = _226743)], (1389 ^ _184986) ^ [] : [aElementOf0(1373 ^ [_226743, _226745, _227852], _227852)]], 1376 ^ _184986 : [(1377 ^ _184986) ^ [] : [-(aElementOf0(1373 ^ [_226743, _226745, _227852], _227852))], (1379 ^ _184986) ^ [] : [aElementOf0(1373 ^ [_226743, _226745, _227852], szDzozmdt0(_226745)), sdtlpdtrp0(_226745, 1373 ^ [_226743, _226745, _227852]) = _226743]]], (1344 ^ _184986) ^ [_227024] : [_227024 = sdtlbdtrb0(_226745, _226743), 1347 ^ _184986 : [(1348 ^ _184986) ^ [] : [-(aSet0(_227024))], (1350 ^ _184986) ^ [_227287] : [aElementOf0(_227287, _227024), 1353 ^ _184986 : [(1354 ^ _184986) ^ [] : [-(aElementOf0(_227287, szDzozmdt0(_226745)))], (1356 ^ _184986) ^ [] : [-(sdtlpdtrp0(_226745, _227287) = _226743)]]], (1358 ^ _184986) ^ [_227556] : [-(aElementOf0(_227556, _227024)), aElementOf0(_227556, szDzozmdt0(_226745)), sdtlpdtrp0(_226745, _227556) = _226743]]]]], (1393 ^ _184986) ^ [_228727, _228729] : [-(aSubsetOf0(sdtlbdtrb0(_228729, _228727), szDzozmdt0(_228729))), aFunction0(_228729), aElement0(_228727)], (1403 ^ _184986) ^ [_229018] : [aFunction0(_229018), 1406 ^ _184986 : [(1407 ^ _184986) ^ [_229195] : [aSubsetOf0(_229195, szDzozmdt0(_229018)), 1410 ^ _184986 : [(1436 ^ _184986) ^ [_230382] : [-(_230382 = sdtlcdtrc0(_229018, _229195)), aSet0(_230382), 1453 ^ _184986 : [(1454 ^ _184986) ^ [] : [-(aElementOf0(1452 ^ [_229018, _229195, _230382], _229195))], (1456 ^ _184986) ^ [] : [-(sdtlpdtrp0(_229018, 1452 ^ [_229018, _229195, _230382]) = 1441 ^ [_229018, _229195, _230382])], (1458 ^ _184986) ^ [] : [aElementOf0(1441 ^ [_229018, _229195, _230382], _230382)]], 1444 ^ _184986 : [(1445 ^ _184986) ^ [] : [-(aElementOf0(1441 ^ [_229018, _229195, _230382], _230382))], (1447 ^ _184986) ^ [_230775] : [aElementOf0(_230775, _229195), sdtlpdtrp0(_229018, _230775) = 1441 ^ [_229018, _229195, _230382]]]], (1411 ^ _184986) ^ [_229400] : [_229400 = sdtlcdtrc0(_229018, _229195), 1414 ^ _184986 : [(1415 ^ _184986) ^ [] : [-(aSet0(_229400))], (1417 ^ _184986) ^ [_229666] : [aElementOf0(_229666, _229400), 1421 ^ _184986 : [(1422 ^ _184986) ^ [] : [-(aElementOf0(1420 ^ [_229018, _229195, _229400, _229666], _229195))], (1424 ^ _184986) ^ [] : [-(sdtlpdtrp0(_229018, 1420 ^ [_229018, _229195, _229400, _229666]) = _229666)]]], (1426 ^ _184986) ^ [_230020] : [-(aElementOf0(_230020, _229400)), 1427 ^ _184986 : [(1428 ^ _184986) ^ [_230125] : [aElementOf0(_230125, _229195), sdtlpdtrp0(_229018, _230125) = _230020]]]]]]]]], (1462 ^ _184986) ^ [_231386] : [aFunction0(_231386), 1465 ^ _184986 : [(1466 ^ _184986) ^ [_231527] : [aElementOf0(_231527, szDzozmdt0(_231386)), -(aElementOf0(sdtlpdtrp0(_231386, _231527), sdtlcdtrc0(_231386, szDzozmdt0(_231386))))]]], (1472 ^ _184986) ^ [_231750] : [aFunction0(_231750), 1475 ^ _184986 : [(1476 ^ _184986) ^ [_231927] : [aSubsetOf0(_231927, szDzozmdt0(_231750)), 1479 ^ _184986 : [(1480 ^ _184986) ^ [_232132] : [_232132 = sdtexdt0(_231750, _231927), 1483 ^ _184986 : [(1484 ^ _184986) ^ [] : [-(aFunction0(_232132))], (1486 ^ _184986) ^ [] : [-(szDzozmdt0(_232132) = _231927)], (1488 ^ _184986) ^ [_232439] : [aElementOf0(_232439, _231927), -(sdtlpdtrp0(_232132, _232439) = sdtlpdtrp0(_231750, _232439))]]], (1494 ^ _184986) ^ [_232640] : [-(_232640 = sdtexdt0(_231750, _231927)), aFunction0(_232640), szDzozmdt0(_232640) = _231927, 1504 ^ _184986 : [(1505 ^ _184986) ^ [] : [-(aElementOf0(1503 ^ [_231750, _231927, _232640], _231927))], (1507 ^ _184986) ^ [] : [sdtlpdtrp0(_232640, 1503 ^ [_231750, _231927, _232640]) = sdtlpdtrp0(_231750, 1503 ^ [_231750, _231927, _232640])]]]]]]], (1511 ^ _184986) ^ [_233234] : [aFunction0(_233234), 1514 ^ _184986 : [(1515 ^ _184986) ^ [_233422] : [aSubsetOf0(_233422, szDzozmdt0(_233234)), isCountable0(_233422), 1526 ^ _184986 : [(1527 ^ _184986) ^ [] : [-(aElementOf0(1524 ^ [_233234, _233422], szDzozmdt0(_233234)))], (1529 ^ _184986) ^ [] : [-(aElementOf0(1525 ^ [_233234, _233422], szDzozmdt0(_233234)))], (1531 ^ _184986) ^ [] : [1524 ^ [_233234, _233422] = 1525 ^ [_233234, _233422]], (1533 ^ _184986) ^ [] : [-(sdtlpdtrp0(_233234, 1524 ^ [_233234, _233422]) = sdtlpdtrp0(_233234, 1525 ^ [_233234, _233422]))]], -(isCountable0(sdtlcdtrc0(_233234, _233422)))]]], (1537 ^ _184986) ^ [_234294] : [aFunction0(_234294), 1548 ^ _184986 : [(1549 ^ _184986) ^ [] : [-(aElement0(szDzizrdt0(_234294)))], (1551 ^ _184986) ^ [] : [-(isCountable0(sdtlbdtrb0(_234294, szDzizrdt0(_234294))))]], isCountable0(szDzozmdt0(_234294)), isFinite0(sdtlcdtrc0(_234294, szDzozmdt0(_234294)))], (1553 ^ _184986) ^ [] : [-(aSet0(xT))], (1555 ^ _184986) ^ [] : [-(isFinite0(xT))], (1557 ^ _184986) ^ [] : [-(aElementOf0(xK, szNzAzT0))], (1559 ^ _184986) ^ [] : [-(aSubsetOf0(xS, szNzAzT0))], (1561 ^ _184986) ^ [] : [-(isCountable0(xS))], (1563 ^ _184986) ^ [] : [-(aFunction0(xc))], (1565 ^ _184986) ^ [] : [-(szDzozmdt0(xc) = slbdtsldtrb0(xS, xK))], (1567 ^ _184986) ^ [] : [-(aSubsetOf0(sdtlcdtrc0(xc, szDzozmdt0(xc)), xT))], (1611 ^ _184986) ^ [] : [xK = sz00], (1613 ^ _184986) ^ [] : [-(xK = sz00)], (1569 ^ _184986) ^ [_235177] : [aElementOf0(_235177, szNzAzT0), 1572 ^ _184986 : [(1573 ^ _184986) ^ [_235397] : [aSubsetOf0(_235397, szNzAzT0), isCountable0(_235397), 1580 ^ _184986 : [(1581 ^ _184986) ^ [_235694] : [aFunction0(_235694), szDzozmdt0(_235694) = slbdtsldtrb0(_235397, _235177), aSubsetOf0(sdtlcdtrc0(_235694, szDzozmdt0(_235694)), xT), iLess0(_235177, xK), 1597 ^ _184986 : [(1598 ^ _184986) ^ [] : [-(aElementOf0(1596 ^ [_235177, _235397, _235694], xT))], (1601 ^ _184986) ^ [] : [-(aSubsetOf0(1599 ^ [_235177, _235397, _235694], _235397))], (1603 ^ _184986) ^ [] : [-(isCountable0(1599 ^ [_235177, _235397, _235694]))], (1605 ^ _184986) ^ [_236569] : [aElementOf0(_236569, slbdtsldtrb0(1599 ^ [_235177, _235397, _235694], _235177)), -(sdtlpdtrp0(_235694, _236569) = 1596 ^ [_235177, _235397, _235694])]]]]]]]], input).
% 0.36/1.38 ncf('1',plain,[xK = sz00],start(1611 ^ 0)).
% 0.36/1.38 ncf('1.1',plain,[-(xK = sz00)],extension(1613 ^ 1)).
% 0.36/1.38 %-----------------------------------------------------
% 0.36/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------