%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM565+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n032.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:01 EDT 2023
% Result : Theorem 134.38s 130.30s
% Output : Proof 134.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : NUM565+1 : TPTP v8.1.2. Released v4.0.0.
% 0.00/0.10 % Command : nanocop.sh %s %d
% 0.10/0.29 % Computer : n032.cluster.edu
% 0.10/0.29 % Model : x86_64 x86_64
% 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.29 % Memory : 8042.1875MB
% 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.29 % CPULimit : 300
% 0.10/0.29 % WCLimit : 300
% 0.10/0.29 % DateTime : Thu May 18 17:05:19 EDT 2023
% 0.14/0.29 % CPUTime :
% 134.38/130.30
% 134.38/130.30 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 134.38/130.30 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 134.38/130.30 %-----------------------------------------------------
% 134.38/130.30 ncf(matrix, plain, [(1616 ^ _192443) ^ [] : [-(aElementOf0(1614 ^ [], slbdtsldtrb0(xS, sz00)))], (1618 ^ _192443) ^ [] : [sdtlpdtrp0(xc, 1614 ^ []) = sdtlpdtrp0(xc, slcrc0)], (126 ^ _192443) ^ [_196492, _196494, _196496, _196498] : [-(sdtpldt0(_196498, _196494) = sdtpldt0(_196496, _196492)), _196498 = _196496, _196494 = _196492], (136 ^ _192443) ^ [_196851, _196853, _196855, _196857] : [-(sdtmndt0(_196857, _196853) = sdtmndt0(_196855, _196851)), _196857 = _196855, _196853 = _196851], (146 ^ _192443) ^ [_197182, _197184] : [_197184 = _197182, -(szmzazxdt0(_197184) = szmzazxdt0(_197182))], (152 ^ _192443) ^ [_197400, _197402] : [_197402 = _197400, -(szmzizndt0(_197402) = szmzizndt0(_197400))], (158 ^ _192443) ^ [_197618, _197620] : [_197620 = _197618, -(szszuzczcdt0(_197620) = szszuzczcdt0(_197618))], (164 ^ _192443) ^ [_197836, _197838] : [_197838 = _197836, -(slbdtrb0(_197838) = slbdtrb0(_197836))], (170 ^ _192443) ^ [_198054, _198056] : [_198056 = _198054, -(sbrdtbr0(_198056) = sbrdtbr0(_198054))], (176 ^ _192443) ^ [_198300, _198302, _198304, _198306] : [-(sdtexdt0(_198306, _198302) = sdtexdt0(_198304, _198300)), _198306 = _198304, _198302 = _198300], (186 ^ _192443) ^ [_198659, _198661, _198663, _198665] : [-(sdtlbdtrb0(_198665, _198661) = sdtlbdtrb0(_198663, _198659)), _198665 = _198663, _198661 = _198659], (196 ^ _192443) ^ [_198990, _198992] : [_198992 = _198990, -(szDzizrdt0(_198992) = szDzizrdt0(_198990))], (202 ^ _192443) ^ [_199236, _199238, _199240, _199242] : [-(sdtlcdtrc0(_199242, _199238) = sdtlcdtrc0(_199240, _199236)), _199242 = _199240, _199238 = _199236], (212 ^ _192443) ^ [_199567, _199569] : [_199569 = _199567, -(szDzozmdt0(_199569) = szDzozmdt0(_199567))], (218 ^ _192443) ^ [_199813, _199815, _199817, _199819] : [-(slbdtsldtrb0(_199819, _199815) = slbdtsldtrb0(_199817, _199813)), _199819 = _199817, _199815 = _199813], (228 ^ _192443) ^ [_200152, _200154, _200156, _200158] : [-(sdtlpdtrp0(_200158, _200154) = sdtlpdtrp0(_200156, _200152)), _200158 = _200156, _200154 = _200152], (2 ^ _192443) ^ [_192587] : [-(_192587 = _192587)], (4 ^ _192443) ^ [_192694, _192696] : [_192696 = _192694, -(_192694 = _192696)], (10 ^ _192443) ^ [_192898, _192900, _192902] : [-(_192902 = _192898), _192902 = _192900, _192900 = _192898], (20 ^ _192443) ^ [_193239, _193241, _193243, _193245] : [-(sdtlseqdt0(_193243, _193239)), sdtlseqdt0(_193245, _193241), _193245 = _193243, _193241 = _193239], (34 ^ _192443) ^ [_193655, _193657] : [-(aElement0(_193655)), _193657 = _193655, aElement0(_193657)], (44 ^ _192443) ^ [_193950, _193952] : [-(aSet0(_193950)), _193952 = _193950, aSet0(_193952)], (54 ^ _192443) ^ [_194245, _194247] : [-(isFinite0(_194245)), _194247 = _194245, isFinite0(_194247)], (64 ^ _192443) ^ [_194540, _194542] : [-(aFunction0(_194540)), _194542 = _194540, aFunction0(_194542)], (74 ^ _192443) ^ [_194863, _194865, _194867, _194869] : [-(iLess0(_194867, _194863)), iLess0(_194869, _194865), _194869 = _194867, _194865 = _194863], (88 ^ _192443) ^ [_195307, _195309, _195311, _195313] : [-(aSubsetOf0(_195311, _195307)), aSubsetOf0(_195313, _195309), _195313 = _195311, _195309 = _195307], (102 ^ _192443) ^ [_195723, _195725] : [-(isCountable0(_195723)), _195725 = _195723, isCountable0(_195725)], (112 ^ _192443) ^ [_196026, _196028, _196030, _196032] : [-(aElementOf0(_196030, _196026)), aElementOf0(_196032, _196028), _196032 = _196030, _196028 = _196026], (238 ^ _192443) ^ [_200555] : [aSet0(_200555), true___, -(true___)], (248 ^ _192443) ^ [_200810] : [aElement0(_200810), true___, -(true___)], (258 ^ _192443) ^ [_201065] : [aSet0(_201065), 261 ^ _192443 : [(262 ^ _192443) ^ [_201195] : [aElementOf0(_201195, _201065), -(aElement0(_201195))]]], (268 ^ _192443) ^ [_201396] : [aSet0(_201396), isFinite0(_201396), true___, -(true___)], (282 ^ _192443) ^ [_201766] : [_201766 = slcrc0, 285 ^ _192443 : [(286 ^ _192443) ^ [] : [-(aSet0(_201766))], (288 ^ _192443) ^ [_201947] : [aElementOf0(_201947, _201766)]]], (290 ^ _192443) ^ [_202015] : [-(_202015 = slcrc0), aSet0(_202015), -(aElementOf0(295 ^ [_202015], _202015))], (301 ^ _192443) ^ [] : [-(isFinite0(slcrc0))], (303 ^ _192443) ^ [_202397] : [aSet0(_202397), isCountable0(_202397), true___, -(true___)], (317 ^ _192443) ^ [_202738] : [isFinite0(_202738), aSet0(_202738), isCountable0(_202738)], (327 ^ _192443) ^ [_203008] : [_203008 = slcrc0, aSet0(_203008), isCountable0(_203008)], (337 ^ _192443) ^ [_203280] : [aSet0(_203280), 340 ^ _192443 : [(341 ^ _192443) ^ [_203456] : [aSubsetOf0(_203456, _203280), 344 ^ _192443 : [(345 ^ _192443) ^ [] : [-(aSet0(_203456))], (347 ^ _192443) ^ [_203665] : [aElementOf0(_203665, _203456), -(aElementOf0(_203665, _203280))]]], (353 ^ _192443) ^ [_203844] : [-(aSubsetOf0(_203844, _203280)), aSet0(_203844), 359 ^ _192443 : [(360 ^ _192443) ^ [] : [-(aElementOf0(358 ^ [_203280, _203844], _203844))], (362 ^ _192443) ^ [] : [aElementOf0(358 ^ [_203280, _203844], _203280)]]]]], (366 ^ _192443) ^ [_204281] : [aSet0(_204281), isFinite0(_204281), 373 ^ _192443 : [(374 ^ _192443) ^ [_204494] : [aSubsetOf0(_204494, _204281), -(isFinite0(_204494))]]], (380 ^ _192443) ^ [_204697] : [aSet0(_204697), -(aSubsetOf0(_204697, _204697))], (386 ^ _192443) ^ [_204899, _204901] : [aSet0(_204901), aSet0(_204899), -(_204901 = _204899), aSubsetOf0(_204901, _204899), aSubsetOf0(_204899, _204901)], (404 ^ _192443) ^ [_205388, _205390, _205392] : [aSet0(_205392), aSet0(_205390), aSet0(_205388), -(aSubsetOf0(_205392, _205388)), aSubsetOf0(_205392, _205390), aSubsetOf0(_205390, _205388)], (426 ^ _192443) ^ [_205974, _205976] : [aSet0(_205976), aElement0(_205974), 433 ^ _192443 : [(464 ^ _192443) ^ [_207235] : [-(_207235 = sdtpldt0(_205976, _205974)), aSet0(_207235), 472 ^ _192443 : [(473 ^ _192443) ^ [] : [-(aElementOf0(469 ^ [_205974, _205976, _207235], _207235))], (475 ^ _192443) ^ [] : [aElement0(469 ^ [_205974, _205976, _207235]), 478 ^ _192443 : [(479 ^ _192443) ^ [] : [aElementOf0(469 ^ [_205974, _205976, _207235], _205976)], (481 ^ _192443) ^ [] : [469 ^ [_205974, _205976, _207235] = _205974]]]], 482 ^ _192443 : [(491 ^ _192443) ^ [] : [aElementOf0(469 ^ [_205974, _205976, _207235], _207235)], (483 ^ _192443) ^ [] : [-(aElement0(469 ^ [_205974, _205976, _207235]))], (485 ^ _192443) ^ [] : [-(aElementOf0(469 ^ [_205974, _205976, _207235], _205976)), -(469 ^ [_205974, _205976, _207235] = _205974)]]], (434 ^ _192443) ^ [_206255] : [_206255 = sdtpldt0(_205976, _205974), 437 ^ _192443 : [(438 ^ _192443) ^ [] : [-(aSet0(_206255))], (440 ^ _192443) ^ [_206518] : [aElementOf0(_206518, _206255), 443 ^ _192443 : [(444 ^ _192443) ^ [] : [-(aElement0(_206518))], (446 ^ _192443) ^ [] : [-(aElementOf0(_206518, _205976)), -(_206518 = _205974)]]], (452 ^ _192443) ^ [_206873] : [-(aElementOf0(_206873, _206255)), aElement0(_206873), 457 ^ _192443 : [(458 ^ _192443) ^ [] : [aElementOf0(_206873, _205976)], (460 ^ _192443) ^ [] : [_206873 = _205974]]]]]]], (495 ^ _192443) ^ [_208272, _208274] : [aSet0(_208274), aElement0(_208272), 502 ^ _192443 : [(533 ^ _192443) ^ [_209540] : [-(_209540 = sdtmndt0(_208274, _208272)), aSet0(_209540), 553 ^ _192443 : [(554 ^ _192443) ^ [] : [-(aElement0(538 ^ [_208272, _208274, _209540]))], (556 ^ _192443) ^ [] : [-(aElementOf0(538 ^ [_208272, _208274, _209540], _208274))], (558 ^ _192443) ^ [] : [538 ^ [_208272, _208274, _209540] = _208272], (560 ^ _192443) ^ [] : [aElementOf0(538 ^ [_208272, _208274, _209540], _209540)]], 541 ^ _192443 : [(542 ^ _192443) ^ [] : [-(aElementOf0(538 ^ [_208272, _208274, _209540], _209540))], (544 ^ _192443) ^ [] : [aElement0(538 ^ [_208272, _208274, _209540]), aElementOf0(538 ^ [_208272, _208274, _209540], _208274), -(538 ^ [_208272, _208274, _209540] = _208272)]]], (503 ^ _192443) ^ [_208555] : [_208555 = sdtmndt0(_208274, _208272), 506 ^ _192443 : [(507 ^ _192443) ^ [] : [-(aSet0(_208555))], (509 ^ _192443) ^ [_208820] : [aElementOf0(_208820, _208555), 512 ^ _192443 : [(513 ^ _192443) ^ [] : [-(aElement0(_208820))], (515 ^ _192443) ^ [] : [-(aElementOf0(_208820, _208274))], (517 ^ _192443) ^ [] : [_208820 = _208272]]], (519 ^ _192443) ^ [_209156] : [-(aElementOf0(_209156, _208555)), aElement0(_209156), aElementOf0(_209156, _208274), -(_209156 = _208272)]]]]], (564 ^ _192443) ^ [_210570] : [aSet0(_210570), 567 ^ _192443 : [(568 ^ _192443) ^ [_210707] : [aElementOf0(_210707, _210570), -(sdtpldt0(sdtmndt0(_210570, _210707), _210707) = _210570)]]], (574 ^ _192443) ^ [_210936, _210938] : [aElement0(_210938), aSet0(_210936), -(aElementOf0(_210938, _210936)), -(sdtmndt0(sdtpldt0(_210936, _210938), _210938) = _210936)], (588 ^ _192443) ^ [_211323] : [aElement0(_211323), 591 ^ _192443 : [(592 ^ _192443) ^ [_211460] : [-(isCountable0(sdtpldt0(_211460, _211323))), aSet0(_211460), isCountable0(_211460)]]], (602 ^ _192443) ^ [_211752] : [aElement0(_211752), 605 ^ _192443 : [(606 ^ _192443) ^ [_211889] : [-(isCountable0(sdtmndt0(_211889, _211752))), aSet0(_211889), isCountable0(_211889)]]], (616 ^ _192443) ^ [_212181] : [aElement0(_212181), 619 ^ _192443 : [(620 ^ _192443) ^ [_212318] : [-(isFinite0(sdtpldt0(_212318, _212181))), aSet0(_212318), isFinite0(_212318)]]], (630 ^ _192443) ^ [_212610] : [aElement0(_212610), 633 ^ _192443 : [(634 ^ _192443) ^ [_212747] : [-(isFinite0(sdtmndt0(_212747, _212610))), aSet0(_212747), isFinite0(_212747)]]], (644 ^ _192443) ^ [] : [-(aSet0(szNzAzT0))], (646 ^ _192443) ^ [] : [-(isCountable0(szNzAzT0))], (648 ^ _192443) ^ [] : [-(aElementOf0(sz00, szNzAzT0))], (650 ^ _192443) ^ [_213200] : [aElementOf0(_213200, szNzAzT0), 653 ^ _192443 : [(654 ^ _192443) ^ [] : [-(aElementOf0(szszuzczcdt0(_213200), szNzAzT0))], (656 ^ _192443) ^ [] : [szszuzczcdt0(_213200) = sz00]]], (658 ^ _192443) ^ [_213486, _213488] : [aElementOf0(_213488, szNzAzT0), aElementOf0(_213486, szNzAzT0), szszuzczcdt0(_213488) = szszuzczcdt0(_213486), -(_213488 = _213486)], (672 ^ _192443) ^ [_213870] : [aElementOf0(_213870, szNzAzT0), -(_213870 = sz00), 680 ^ _192443 : [(681 ^ _192443) ^ [] : [-(aElementOf0(679 ^ [_213870], szNzAzT0))], (683 ^ _192443) ^ [] : [-(_213870 = szszuzczcdt0(679 ^ [_213870]))]]], (685 ^ _192443) ^ [_214287] : [aElementOf0(_214287, szNzAzT0), _214287 = szszuzczcdt0(_214287)], (691 ^ _192443) ^ [_214496, _214498] : [aElementOf0(_214498, szNzAzT0), aElementOf0(_214496, szNzAzT0), sdtlseqdt0(_214498, _214496), true___, -(true___)], (709 ^ _192443) ^ [_214946] : [aElementOf0(_214946, szNzAzT0), -(sdtlseqdt0(sz00, _214946))], (715 ^ _192443) ^ [_215136] : [aElementOf0(_215136, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_215136), sz00)], (721 ^ _192443) ^ [_215345, _215347] : [aElementOf0(_215347, szNzAzT0), aElementOf0(_215345, szNzAzT0), 728 ^ _192443 : [(729 ^ _192443) ^ [] : [sdtlseqdt0(_215347, _215345), -(sdtlseqdt0(szszuzczcdt0(_215347), szszuzczcdt0(_215345)))], (735 ^ _192443) ^ [] : [sdtlseqdt0(szszuzczcdt0(_215347), szszuzczcdt0(_215345)), -(sdtlseqdt0(_215347, _215345))]]], (741 ^ _192443) ^ [_215894] : [aElementOf0(_215894, szNzAzT0), -(sdtlseqdt0(_215894, szszuzczcdt0(_215894)))], (747 ^ _192443) ^ [_216088] : [aElementOf0(_216088, szNzAzT0), -(sdtlseqdt0(_216088, _216088))], (753 ^ _192443) ^ [_216292, _216294] : [aElementOf0(_216294, szNzAzT0), aElementOf0(_216292, szNzAzT0), -(_216294 = _216292), sdtlseqdt0(_216294, _216292), sdtlseqdt0(_216292, _216294)], (771 ^ _192443) ^ [_216785, _216787, _216789] : [aElementOf0(_216789, szNzAzT0), aElementOf0(_216787, szNzAzT0), aElementOf0(_216785, szNzAzT0), -(sdtlseqdt0(_216789, _216785)), sdtlseqdt0(_216789, _216787), sdtlseqdt0(_216787, _216785)], (793 ^ _192443) ^ [_217377, _217379] : [aElementOf0(_217379, szNzAzT0), aElementOf0(_217377, szNzAzT0), -(sdtlseqdt0(_217379, _217377)), -(sdtlseqdt0(szszuzczcdt0(_217377), _217379))], (807 ^ _192443) ^ [_217772, _217774] : [aElementOf0(_217774, szNzAzT0), aElementOf0(_217772, szNzAzT0), iLess0(_217774, _217772), true___, -(true___)], (825 ^ _192443) ^ [_218222] : [aElementOf0(_218222, szNzAzT0), -(iLess0(_218222, szszuzczcdt0(_218222)))], (831 ^ _192443) ^ [_218416] : [aSet0(_218416), -(aElement0(sbrdtbr0(_218416)))], (837 ^ _192443) ^ [_218606] : [aSet0(_218606), 840 ^ _192443 : [(841 ^ _192443) ^ [] : [aElementOf0(sbrdtbr0(_218606), szNzAzT0), -(isFinite0(_218606))], (847 ^ _192443) ^ [] : [isFinite0(_218606), -(aElementOf0(sbrdtbr0(_218606), szNzAzT0))]]], (853 ^ _192443) ^ [_219037] : [aSet0(_219037), 856 ^ _192443 : [(857 ^ _192443) ^ [] : [sbrdtbr0(_219037) = sz00, -(_219037 = slcrc0)], (863 ^ _192443) ^ [] : [_219037 = slcrc0, -(sbrdtbr0(_219037) = sz00)]]], (869 ^ _192443) ^ [_219471] : [aSet0(_219471), isFinite0(_219471), 876 ^ _192443 : [(877 ^ _192443) ^ [_219701] : [aElement0(_219701), -(aElementOf0(_219701, _219471)), -(sbrdtbr0(sdtpldt0(_219471, _219701)) = szszuzczcdt0(sbrdtbr0(_219471)))]]], (887 ^ _192443) ^ [_220014] : [aSet0(_220014), 890 ^ _192443 : [(891 ^ _192443) ^ [_220159] : [-(szszuzczcdt0(sbrdtbr0(sdtmndt0(_220014, _220159))) = sbrdtbr0(_220014)), isFinite0(_220014), aElementOf0(_220159, _220014)]]], (901 ^ _192443) ^ [_220467] : [aSet0(_220467), 904 ^ _192443 : [(905 ^ _192443) ^ [_220607] : [-(sdtlseqdt0(sbrdtbr0(_220607), sbrdtbr0(_220467))), isFinite0(_220467), aSubsetOf0(_220607, _220467)]]], (915 ^ _192443) ^ [_220919, _220921] : [aSet0(_220921), aElementOf0(_220919, szNzAzT0), 931 ^ _192443 : [(932 ^ _192443) ^ [] : [-(aSubsetOf0(930 ^ [_220919, _220921], _220921))], (934 ^ _192443) ^ [] : [-(sbrdtbr0(930 ^ [_220919, _220921]) = _220919)]], isFinite0(_220921), sdtlseqdt0(_220919, sbrdtbr0(_220921))], (936 ^ _192443) ^ [_221535] : [aSubsetOf0(_221535, szNzAzT0), -(_221535 = slcrc0), 943 ^ _192443 : [(944 ^ _192443) ^ [_221804] : [_221804 = szmzizndt0(_221535), 947 ^ _192443 : [(948 ^ _192443) ^ [] : [-(aElementOf0(_221804, _221535))], (950 ^ _192443) ^ [_222019] : [aElementOf0(_222019, _221535), -(sdtlseqdt0(_221804, _222019))]]], (956 ^ _192443) ^ [_222198] : [-(_222198 = szmzizndt0(_221535)), aElementOf0(_222198, _221535), 962 ^ _192443 : [(963 ^ _192443) ^ [] : [-(aElementOf0(961 ^ [_221535, _222198], _221535))], (965 ^ _192443) ^ [] : [sdtlseqdt0(_222198, 961 ^ [_221535, _222198])]]]]], (969 ^ _192443) ^ [_222643] : [aSubsetOf0(_222643, szNzAzT0), isFinite0(_222643), -(_222643 = slcrc0), 980 ^ _192443 : [(981 ^ _192443) ^ [_222995] : [_222995 = szmzazxdt0(_222643), 984 ^ _192443 : [(985 ^ _192443) ^ [] : [-(aElementOf0(_222995, _222643))], (987 ^ _192443) ^ [_223210] : [aElementOf0(_223210, _222643), -(sdtlseqdt0(_223210, _222995))]]], (993 ^ _192443) ^ [_223389] : [-(_223389 = szmzazxdt0(_222643)), aElementOf0(_223389, _222643), 999 ^ _192443 : [(1000 ^ _192443) ^ [] : [-(aElementOf0(998 ^ [_222643, _223389], _222643))], (1002 ^ _192443) ^ [] : [sdtlseqdt0(998 ^ [_222643, _223389], _223389)]]]]], (1006 ^ _192443) ^ [_223850, _223852] : [-(szmzizndt0(_223852) = szmzizndt0(_223850)), aElementOf0(szmzizndt0(_223852), _223850), aElementOf0(szmzizndt0(_223850), _223852), aSubsetOf0(_223852, szNzAzT0), aSubsetOf0(_223850, szNzAzT0), -(_223852 = slcrc0), -(_223850 = slcrc0)], (1032 ^ _192443) ^ [_224517] : [aElementOf0(_224517, szNzAzT0), 1035 ^ _192443 : [(1060 ^ _192443) ^ [_225486] : [-(_225486 = slbdtrb0(_224517)), aSet0(_225486), 1076 ^ _192443 : [(1077 ^ _192443) ^ [] : [-(aElementOf0(1065 ^ [_224517, _225486], szNzAzT0))], (1079 ^ _192443) ^ [] : [-(sdtlseqdt0(szszuzczcdt0(1065 ^ [_224517, _225486]), _224517))], (1081 ^ _192443) ^ [] : [aElementOf0(1065 ^ [_224517, _225486], _225486)]], 1068 ^ _192443 : [(1069 ^ _192443) ^ [] : [-(aElementOf0(1065 ^ [_224517, _225486], _225486))], (1071 ^ _192443) ^ [] : [aElementOf0(1065 ^ [_224517, _225486], szNzAzT0), sdtlseqdt0(szszuzczcdt0(1065 ^ [_224517, _225486]), _224517)]]], (1036 ^ _192443) ^ [_224705] : [_224705 = slbdtrb0(_224517), 1039 ^ _192443 : [(1040 ^ _192443) ^ [] : [-(aSet0(_224705))], (1042 ^ _192443) ^ [_224955] : [aElementOf0(_224955, _224705), 1045 ^ _192443 : [(1046 ^ _192443) ^ [] : [-(aElementOf0(_224955, szNzAzT0))], (1048 ^ _192443) ^ [] : [-(sdtlseqdt0(szszuzczcdt0(_224955), _224517))]]], (1050 ^ _192443) ^ [_225208] : [-(aElementOf0(_225208, _224705)), aElementOf0(_225208, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_225208), _224517)]]]]], (1085 ^ _192443) ^ [_226289] : [aElementOf0(_226289, szNzAzT0), -(isFinite0(slbdtrb0(_226289)))], (1091 ^ _192443) ^ [] : [-(slbdtrb0(sz00) = slcrc0)], (1093 ^ _192443) ^ [_226548, _226550] : [aElementOf0(_226550, szNzAzT0), aElementOf0(_226548, szNzAzT0), 1100 ^ _192443 : [(1111 ^ _192443) ^ [] : [1112 ^ _192443 : [(1113 ^ _192443) ^ [] : [aElementOf0(_226550, slbdtrb0(_226548))], (1115 ^ _192443) ^ [] : [_226550 = _226548]], -(aElementOf0(_226550, slbdtrb0(szszuzczcdt0(_226548))))], (1101 ^ _192443) ^ [] : [aElementOf0(_226550, slbdtrb0(szszuzczcdt0(_226548))), -(aElementOf0(_226550, slbdtrb0(_226548))), -(_226550 = _226548)]]], (1119 ^ _192443) ^ [_227275, _227277] : [aElementOf0(_227277, szNzAzT0), aElementOf0(_227275, szNzAzT0), 1126 ^ _192443 : [(1127 ^ _192443) ^ [] : [sdtlseqdt0(_227277, _227275), -(aSubsetOf0(slbdtrb0(_227277), slbdtrb0(_227275)))], (1133 ^ _192443) ^ [] : [aSubsetOf0(slbdtrb0(_227277), slbdtrb0(_227275)), -(sdtlseqdt0(_227277, _227275))]]], (1139 ^ _192443) ^ [_227824] : [1147 ^ _192443 : [(1148 ^ _192443) ^ [] : [-(aElementOf0(1146 ^ [_227824], szNzAzT0))], (1150 ^ _192443) ^ [] : [-(aSubsetOf0(_227824, slbdtrb0(1146 ^ [_227824])))]], aSubsetOf0(_227824, szNzAzT0), isFinite0(_227824)], (1152 ^ _192443) ^ [_228238] : [aElementOf0(_228238, szNzAzT0), -(sbrdtbr0(slbdtrb0(_228238)) = _228238)], (1158 ^ _192443) ^ [_228450, _228452] : [aSet0(_228452), aElementOf0(_228450, szNzAzT0), 1165 ^ _192443 : [(1190 ^ _192443) ^ [_229543] : [-(_229543 = slbdtsldtrb0(_228452, _228450)), aSet0(_229543), 1206 ^ _192443 : [(1207 ^ _192443) ^ [] : [-(aSubsetOf0(1195 ^ [_228450, _228452, _229543], _228452))], (1209 ^ _192443) ^ [] : [-(sbrdtbr0(1195 ^ [_228450, _228452, _229543]) = _228450)], (1211 ^ _192443) ^ [] : [aElementOf0(1195 ^ [_228450, _228452, _229543], _229543)]], 1198 ^ _192443 : [(1199 ^ _192443) ^ [] : [-(aElementOf0(1195 ^ [_228450, _228452, _229543], _229543))], (1201 ^ _192443) ^ [] : [aSubsetOf0(1195 ^ [_228450, _228452, _229543], _228452), sbrdtbr0(1195 ^ [_228450, _228452, _229543]) = _228450]]], (1166 ^ _192443) ^ [_228730] : [_228730 = slbdtsldtrb0(_228452, _228450), 1169 ^ _192443 : [(1170 ^ _192443) ^ [] : [-(aSet0(_228730))], (1172 ^ _192443) ^ [_228990] : [aElementOf0(_228990, _228730), 1175 ^ _192443 : [(1176 ^ _192443) ^ [] : [-(aSubsetOf0(_228990, _228452))], (1178 ^ _192443) ^ [] : [-(sbrdtbr0(_228990) = _228450)]]], (1180 ^ _192443) ^ [_229253] : [-(aElementOf0(_229253, _228730)), aSubsetOf0(_229253, _228452), sbrdtbr0(_229253) = _228450]]]]], (1215 ^ _192443) ^ [_230392] : [aSet0(_230392), isFinite0(_230392), 1222 ^ _192443 : [(1223 ^ _192443) ^ [_230608] : [aElementOf0(_230608, szNzAzT0), -(isFinite0(slbdtsldtrb0(_230392, _230608)))]]], (1229 ^ _192443) ^ [_230817] : [aSet0(_230817), -(isFinite0(_230817)), 1236 ^ _192443 : [(1237 ^ _192443) ^ [_231039] : [aElementOf0(_231039, szNzAzT0), slbdtsldtrb0(_230817, _231039) = slcrc0]]], (1243 ^ _192443) ^ [_231251] : [aSet0(_231251), isCountable0(_231251), 1250 ^ _192443 : [(1251 ^ _192443) ^ [_231475] : [-(isCountable0(slbdtsldtrb0(_231251, _231475))), aElementOf0(_231475, szNzAzT0), -(_231475 = sz00)]]], (1261 ^ _192443) ^ [_231776] : [aElementOf0(_231776, szNzAzT0), 1264 ^ _192443 : [(1265 ^ _192443) ^ [_231963, _231965] : [aSet0(_231965), aSet0(_231963), -(_231776 = sz00), -(aSubsetOf0(_231965, _231963)), aSubsetOf0(slbdtsldtrb0(_231965, _231776), slbdtsldtrb0(_231963, _231776)), -(slbdtsldtrb0(_231965, _231776) = slcrc0)]]], (1287 ^ _192443) ^ [_232582, _232584] : [aSet0(_232584), aElementOf0(_232582, szNzAzT0), 1294 ^ _192443 : [(1295 ^ _192443) ^ [_232833] : [1303 ^ _192443 : [(1304 ^ _192443) ^ [] : [-(aSubsetOf0(1302 ^ [_232582, _232584, _232833], _232584))], (1306 ^ _192443) ^ [] : [-(isFinite0(1302 ^ [_232582, _232584, _232833]))], (1308 ^ _192443) ^ [] : [-(aSubsetOf0(_232833, slbdtsldtrb0(1302 ^ [_232582, _232584, _232833], _232582)))]], aSubsetOf0(_232833, slbdtsldtrb0(_232584, _232582)), isFinite0(_232833)]]], (1310 ^ _192443) ^ [_233395] : [aFunction0(_233395), true___, -(true___)], (1320 ^ _192443) ^ [_233650] : [aFunction0(_233650), -(aSet0(szDzozmdt0(_233650)))], (1326 ^ _192443) ^ [_233840] : [aFunction0(_233840), 1329 ^ _192443 : [(1330 ^ _192443) ^ [_233975] : [aElementOf0(_233975, szDzozmdt0(_233840)), -(aElement0(sdtlpdtrp0(_233840, _233975)))]]], (1336 ^ _192443) ^ [_234200, _234202] : [aFunction0(_234202), aElement0(_234200), 1343 ^ _192443 : [(1368 ^ _192443) ^ [_235309] : [-(_235309 = sdtlbdtrb0(_234202, _234200)), aSet0(_235309), 1384 ^ _192443 : [(1385 ^ _192443) ^ [] : [-(aElementOf0(1373 ^ [_234200, _234202, _235309], szDzozmdt0(_234202)))], (1387 ^ _192443) ^ [] : [-(sdtlpdtrp0(_234202, 1373 ^ [_234200, _234202, _235309]) = _234200)], (1389 ^ _192443) ^ [] : [aElementOf0(1373 ^ [_234200, _234202, _235309], _235309)]], 1376 ^ _192443 : [(1377 ^ _192443) ^ [] : [-(aElementOf0(1373 ^ [_234200, _234202, _235309], _235309))], (1379 ^ _192443) ^ [] : [aElementOf0(1373 ^ [_234200, _234202, _235309], szDzozmdt0(_234202)), sdtlpdtrp0(_234202, 1373 ^ [_234200, _234202, _235309]) = _234200]]], (1344 ^ _192443) ^ [_234481] : [_234481 = sdtlbdtrb0(_234202, _234200), 1347 ^ _192443 : [(1348 ^ _192443) ^ [] : [-(aSet0(_234481))], (1350 ^ _192443) ^ [_234744] : [aElementOf0(_234744, _234481), 1353 ^ _192443 : [(1354 ^ _192443) ^ [] : [-(aElementOf0(_234744, szDzozmdt0(_234202)))], (1356 ^ _192443) ^ [] : [-(sdtlpdtrp0(_234202, _234744) = _234200)]]], (1358 ^ _192443) ^ [_235013] : [-(aElementOf0(_235013, _234481)), aElementOf0(_235013, szDzozmdt0(_234202)), sdtlpdtrp0(_234202, _235013) = _234200]]]]], (1393 ^ _192443) ^ [_236184, _236186] : [-(aSubsetOf0(sdtlbdtrb0(_236186, _236184), szDzozmdt0(_236186))), aFunction0(_236186), aElement0(_236184)], (1403 ^ _192443) ^ [_236475] : [aFunction0(_236475), 1406 ^ _192443 : [(1407 ^ _192443) ^ [_236652] : [aSubsetOf0(_236652, szDzozmdt0(_236475)), 1410 ^ _192443 : [(1436 ^ _192443) ^ [_237839] : [-(_237839 = sdtlcdtrc0(_236475, _236652)), aSet0(_237839), 1453 ^ _192443 : [(1454 ^ _192443) ^ [] : [-(aElementOf0(1452 ^ [_236475, _236652, _237839], _236652))], (1456 ^ _192443) ^ [] : [-(sdtlpdtrp0(_236475, 1452 ^ [_236475, _236652, _237839]) = 1441 ^ [_236475, _236652, _237839])], (1458 ^ _192443) ^ [] : [aElementOf0(1441 ^ [_236475, _236652, _237839], _237839)]], 1444 ^ _192443 : [(1445 ^ _192443) ^ [] : [-(aElementOf0(1441 ^ [_236475, _236652, _237839], _237839))], (1447 ^ _192443) ^ [_238232] : [aElementOf0(_238232, _236652), sdtlpdtrp0(_236475, _238232) = 1441 ^ [_236475, _236652, _237839]]]], (1411 ^ _192443) ^ [_236857] : [_236857 = sdtlcdtrc0(_236475, _236652), 1414 ^ _192443 : [(1415 ^ _192443) ^ [] : [-(aSet0(_236857))], (1417 ^ _192443) ^ [_237123] : [aElementOf0(_237123, _236857), 1421 ^ _192443 : [(1422 ^ _192443) ^ [] : [-(aElementOf0(1420 ^ [_236475, _236652, _236857, _237123], _236652))], (1424 ^ _192443) ^ [] : [-(sdtlpdtrp0(_236475, 1420 ^ [_236475, _236652, _236857, _237123]) = _237123)]]], (1426 ^ _192443) ^ [_237477] : [-(aElementOf0(_237477, _236857)), 1427 ^ _192443 : [(1428 ^ _192443) ^ [_237582] : [aElementOf0(_237582, _236652), sdtlpdtrp0(_236475, _237582) = _237477]]]]]]]]], (1462 ^ _192443) ^ [_238843] : [aFunction0(_238843), 1465 ^ _192443 : [(1466 ^ _192443) ^ [_238984] : [aElementOf0(_238984, szDzozmdt0(_238843)), -(aElementOf0(sdtlpdtrp0(_238843, _238984), sdtlcdtrc0(_238843, szDzozmdt0(_238843))))]]], (1472 ^ _192443) ^ [_239207] : [aFunction0(_239207), 1475 ^ _192443 : [(1476 ^ _192443) ^ [_239384] : [aSubsetOf0(_239384, szDzozmdt0(_239207)), 1479 ^ _192443 : [(1480 ^ _192443) ^ [_239589] : [_239589 = sdtexdt0(_239207, _239384), 1483 ^ _192443 : [(1484 ^ _192443) ^ [] : [-(aFunction0(_239589))], (1486 ^ _192443) ^ [] : [-(szDzozmdt0(_239589) = _239384)], (1488 ^ _192443) ^ [_239896] : [aElementOf0(_239896, _239384), -(sdtlpdtrp0(_239589, _239896) = sdtlpdtrp0(_239207, _239896))]]], (1494 ^ _192443) ^ [_240097] : [-(_240097 = sdtexdt0(_239207, _239384)), aFunction0(_240097), szDzozmdt0(_240097) = _239384, 1504 ^ _192443 : [(1505 ^ _192443) ^ [] : [-(aElementOf0(1503 ^ [_239207, _239384, _240097], _239384))], (1507 ^ _192443) ^ [] : [sdtlpdtrp0(_240097, 1503 ^ [_239207, _239384, _240097]) = sdtlpdtrp0(_239207, 1503 ^ [_239207, _239384, _240097])]]]]]]], (1511 ^ _192443) ^ [_240691] : [aFunction0(_240691), 1514 ^ _192443 : [(1515 ^ _192443) ^ [_240879] : [aSubsetOf0(_240879, szDzozmdt0(_240691)), isCountable0(_240879), 1526 ^ _192443 : [(1527 ^ _192443) ^ [] : [-(aElementOf0(1524 ^ [_240691, _240879], szDzozmdt0(_240691)))], (1529 ^ _192443) ^ [] : [-(aElementOf0(1525 ^ [_240691, _240879], szDzozmdt0(_240691)))], (1531 ^ _192443) ^ [] : [1524 ^ [_240691, _240879] = 1525 ^ [_240691, _240879]], (1533 ^ _192443) ^ [] : [-(sdtlpdtrp0(_240691, 1524 ^ [_240691, _240879]) = sdtlpdtrp0(_240691, 1525 ^ [_240691, _240879]))]], -(isCountable0(sdtlcdtrc0(_240691, _240879)))]]], (1537 ^ _192443) ^ [_241751] : [aFunction0(_241751), 1548 ^ _192443 : [(1549 ^ _192443) ^ [] : [-(aElement0(szDzizrdt0(_241751)))], (1551 ^ _192443) ^ [] : [-(isCountable0(sdtlbdtrb0(_241751, szDzizrdt0(_241751))))]], isCountable0(szDzozmdt0(_241751)), isFinite0(sdtlcdtrc0(_241751, szDzozmdt0(_241751)))], (1553 ^ _192443) ^ [] : [-(aSet0(xT))], (1555 ^ _192443) ^ [] : [-(isFinite0(xT))], (1557 ^ _192443) ^ [] : [-(aElementOf0(xK, szNzAzT0))], (1559 ^ _192443) ^ [] : [-(aSubsetOf0(xS, szNzAzT0))], (1561 ^ _192443) ^ [] : [-(isCountable0(xS))], (1563 ^ _192443) ^ [] : [-(aFunction0(xc))], (1565 ^ _192443) ^ [] : [-(szDzozmdt0(xc) = slbdtsldtrb0(xS, xK))], (1567 ^ _192443) ^ [] : [-(aSubsetOf0(sdtlcdtrc0(xc, szDzozmdt0(xc)), xT))], (1611 ^ _192443) ^ [] : [-(xK = sz00)], (1613 ^ _192443) ^ [] : [-(aElementOf0(slcrc0, slbdtsldtrb0(xS, sz00)))], (1569 ^ _192443) ^ [_242634] : [aElementOf0(_242634, szNzAzT0), 1572 ^ _192443 : [(1573 ^ _192443) ^ [_242854] : [aSubsetOf0(_242854, szNzAzT0), isCountable0(_242854), 1580 ^ _192443 : [(1581 ^ _192443) ^ [_243151] : [aFunction0(_243151), szDzozmdt0(_243151) = slbdtsldtrb0(_242854, _242634), aSubsetOf0(sdtlcdtrc0(_243151, szDzozmdt0(_243151)), xT), iLess0(_242634, xK), 1597 ^ _192443 : [(1598 ^ _192443) ^ [] : [-(aElementOf0(1596 ^ [_242634, _242854, _243151], xT))], (1601 ^ _192443) ^ [] : [-(aSubsetOf0(1599 ^ [_242634, _242854, _243151], _242854))], (1603 ^ _192443) ^ [] : [-(isCountable0(1599 ^ [_242634, _242854, _243151]))], (1605 ^ _192443) ^ [_244026] : [aElementOf0(_244026, slbdtsldtrb0(1599 ^ [_242634, _242854, _243151], _242634)), -(sdtlpdtrp0(_243151, _244026) = 1596 ^ [_242634, _242854, _243151])]]]]]]]], input).
% 134.38/130.30 ncf('1',plain,[sdtlpdtrp0(xc, 1614 ^ []) = sdtlpdtrp0(xc, slcrc0)],start(1618 ^ 0)).
% 134.38/130.30 ncf('1.1',plain,[-(sdtlpdtrp0(xc, 1614 ^ []) = sdtlpdtrp0(xc, slcrc0)), xc = xc, 1614 ^ [] = slcrc0],extension(228 ^ 1,bind([[_200152, _200154, _200156, _200158], [slcrc0, 1614 ^ [], xc, xc]]))).
% 134.38/130.30 ncf('1.1.1',plain,[-(xc = xc)],extension(2 ^ 2,bind([[_192587], [xc]]))).
% 134.38/130.30 ncf('1.1.2',plain,[-(1614 ^ [] = slcrc0), 857 : sbrdtbr0(1614 ^ []) = sz00, 857 : aSet0(1614 ^ [])],extension(853 ^ 2,bind([[_219037], [1614 ^ []]]))).
% 134.38/130.30 ncf('1.1.2.1',plain,[-(sbrdtbr0(1614 ^ []) = sz00), 1172 : aElementOf0(1614 ^ [], slbdtsldtrb0(xS, sz00)), 1172 : slbdtsldtrb0(xS, sz00) = slbdtsldtrb0(xS, sz00), 1166 : aSet0(xS), 1166 : aElementOf0(sz00, szNzAzT0)],extension(1158 ^ 5,bind([[_228450, _228452, _228730, _228990], [sz00, xS, slbdtsldtrb0(xS, sz00), 1614 ^ []]]))).
% 134.38/130.30 ncf('1.1.2.1.1',plain,[-(aElementOf0(1614 ^ [], slbdtsldtrb0(xS, sz00)))],extension(1616 ^ 10)).
% 134.38/130.30 ncf('1.1.2.1.2',plain,[-(slbdtsldtrb0(xS, sz00) = slbdtsldtrb0(xS, sz00)), xS = xS, sz00 = sz00],extension(218 ^ 8,bind([[_199813, _199815, _199817, _199819], [sz00, sz00, xS, xS]]))).
% 134.38/130.30 ncf('1.1.2.1.2.1',plain,[-(xS = xS)],extension(2 ^ 9,bind([[_192587], [xS]]))).
% 134.38/130.30 ncf('1.1.2.1.2.2',plain,[-(sz00 = sz00)],extension(2 ^ 9,bind([[_192587], [sz00]]))).
% 134.38/130.30 ncf('1.1.2.1.3',plain,[-(aSet0(xS)), 341 : aSubsetOf0(xS, szNzAzT0), 341 : aSet0(szNzAzT0)],extension(337 ^ 6,bind([[_203280, _203456], [szNzAzT0, xS]]))).
% 134.38/130.30 ncf('1.1.2.1.3.1',plain,[-(aSubsetOf0(xS, szNzAzT0))],extension(1559 ^ 9)).
% 134.38/130.30 ncf('1.1.2.1.3.2',plain,[-(aSet0(szNzAzT0))],extension(644 ^ 7)).
% 134.38/130.30 ncf('1.1.2.1.4',plain,[-(aElementOf0(sz00, szNzAzT0)), 347 : aElementOf0(sz00, szNzAzT0), 347 : aSubsetOf0(szNzAzT0, szNzAzT0), 341 : aSet0(szNzAzT0)],extension(337 ^ 6,bind([[_203280, _203456, _203665], [szNzAzT0, szNzAzT0, sz00]]))).
% 134.38/130.30 ncf('1.1.2.1.4.1',plain,[-(aElementOf0(sz00, szNzAzT0))],extension(648 ^ 11)).
% 134.38/130.30 ncf('1.1.2.1.4.2',plain,[-(aSubsetOf0(szNzAzT0, szNzAzT0)), aSet0(szNzAzT0)],extension(380 ^ 9,bind([[_204697], [szNzAzT0]]))).
% 134.38/130.30 ncf('1.1.2.1.4.2.1',plain,[-(aSet0(szNzAzT0))],extension(644 ^ 10)).
% 134.38/130.30 ncf('1.1.2.1.4.3',plain,[-(aSet0(szNzAzT0))],extension(644 ^ 7)).
% 134.38/130.30 ncf('1.1.2.2',plain,[-(aSet0(1614 ^ [])), 341 : aSubsetOf0(1614 ^ [], xS), 341 : aSet0(xS)],extension(337 ^ 3,bind([[_203280, _203456], [xS, 1614 ^ []]]))).
% 134.38/130.30 ncf('1.1.2.2.1',plain,[-(aSubsetOf0(1614 ^ [], xS)), 1172 : aElementOf0(1614 ^ [], slbdtsldtrb0(xS, sz00)), 1172 : slbdtsldtrb0(xS, sz00) = slbdtsldtrb0(xS, sz00), 1166 : aSet0(xS), 1166 : aElementOf0(sz00, szNzAzT0)],extension(1158 ^ 6,bind([[_228450, _228452, _228730, _228990], [sz00, xS, slbdtsldtrb0(xS, sz00), 1614 ^ []]]))).
% 134.38/130.30 ncf('1.1.2.2.1.1',plain,[-(aElementOf0(1614 ^ [], slbdtsldtrb0(xS, sz00)))],extension(1616 ^ 11)).
% 134.38/130.30 ncf('1.1.2.2.1.2',plain,[-(slbdtsldtrb0(xS, sz00) = slbdtsldtrb0(xS, sz00))],extension(2 ^ 9,bind([[_192587], [slbdtsldtrb0(xS, sz00)]]))).
% 134.38/130.30 ncf('1.1.2.2.1.3',plain,[-(aSet0(xS)), 341 : aSubsetOf0(xS, szNzAzT0), 341 : aSet0(szNzAzT0)],extension(337 ^ 7,bind([[_203280, _203456], [szNzAzT0, xS]]))).
% 134.38/130.30 ncf('1.1.2.2.1.3.1',plain,[-(aSubsetOf0(xS, szNzAzT0))],extension(1559 ^ 10)).
% 134.38/130.30 ncf('1.1.2.2.1.3.2',plain,[-(aSet0(szNzAzT0))],extension(644 ^ 8)).
% 134.38/130.30 ncf('1.1.2.2.1.4',plain,[-(aElementOf0(sz00, szNzAzT0))],extension(648 ^ 7)).
% 134.38/130.30 ncf('1.1.2.2.2',plain,[-(aSet0(xS)), 341 : aSubsetOf0(xS, szNzAzT0), 341 : aSet0(szNzAzT0)],extension(337 ^ 4,bind([[_203280, _203456], [szNzAzT0, xS]]))).
% 134.38/130.30 ncf('1.1.2.2.2.1',plain,[-(aSubsetOf0(xS, szNzAzT0))],extension(1559 ^ 7)).
% 134.38/130.30 ncf('1.1.2.2.2.2',plain,[-(aSet0(szNzAzT0))],extension(644 ^ 5)).
% 134.38/130.30 %-----------------------------------------------------
% 134.38/130.30 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------