%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM455+6 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n006.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:40 EDT 2023
% Result : Theorem 0.34s 1.37s
% Output : Proof 0.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM455+6 : TPTP v8.1.2. Released v4.0.0.
% 0.00/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n006.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 18 17:10:51 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.34/1.37
% 0.34/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.34/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.34/1.37 %-----------------------------------------------------
% 0.34/1.37 ncf(matrix, plain, [(1609 ^ _200304) ^ [_253688] : [1626 ^ _200304 : [(1633 ^ _200304) ^ [] : [-(aElementOf0(_253688, cS2200))], (1627 ^ _200304) ^ [] : [-(_253688 = sz10), -(_253688 = smndt0(sz10))]], 1610 ^ _200304 : [(1625 ^ _200304) ^ [] : [aElementOf0(_253688, szAzrzSzezqlpdtcmdtrp0(sz10, xp))], (1611 ^ _200304) ^ [] : [aInteger0(_253688), 1614 ^ _200304 : [(1621 ^ _200304) ^ [] : [aDivisorOf0(xp, sdtpldt0(_253688, smndt0(sz10)))], (1623 ^ _200304) ^ [] : [sdteqdtlpzmzozddtrp0(_253688, sz10, xp)], (1615 ^ _200304) ^ [_253938] : [aInteger0(_253938), sdtasdt0(xp, _253938) = sdtpldt0(_253688, smndt0(sz10))]]]]], (140 ^ _200304) ^ [_204815, _204817, _204819, _204821] : [-(sdtslmnbsdt0(_204821, _204817) = sdtslmnbsdt0(_204819, _204815)), _204821 = _204819, _204817 = _204815], (150 ^ _200304) ^ [_205174, _205176, _205178, _205180] : [-(sdtbsmnsldt0(_205180, _205176) = sdtbsmnsldt0(_205178, _205174)), _205180 = _205178, _205176 = _205174], (160 ^ _200304) ^ [_205505, _205507] : [_205507 = _205505, -(stldt0(_205507) = stldt0(_205505))], (166 ^ _200304) ^ [_205723, _205725] : [_205725 = _205723, -(sbsmnsldt0(_205725) = sbsmnsldt0(_205723))], (172 ^ _200304) ^ [_205969, _205971, _205973, _205975] : [-(sdtasdt0(_205975, _205971) = sdtasdt0(_205973, _205969)), _205975 = _205973, _205971 = _205969], (182 ^ _200304) ^ [_206328, _206330, _206332, _206334] : [-(sdtpldt0(_206334, _206330) = sdtpldt0(_206332, _206328)), _206334 = _206332, _206330 = _206328], (202 ^ _200304) ^ [_206998, _207000] : [_207000 = _206998, -(smndt0(_207000) = smndt0(_206998))], (192 ^ _200304) ^ [_206687, _206689, _206691, _206693] : [-(szAzrzSzezqlpdtcmdtrp0(_206693, _206689) = szAzrzSzezqlpdtcmdtrp0(_206691, _206687)), _206693 = _206691, _206689 = _206687], (2 ^ _200304) ^ [_200448] : [-(_200448 = _200448)], (4 ^ _200304) ^ [_200555, _200557] : [_200557 = _200555, -(_200555 = _200557)], (10 ^ _200304) ^ [_200759, _200761, _200763] : [-(_200763 = _200759), _200763 = _200761, _200761 = _200759], (20 ^ _200304) ^ [_201072, _201074] : [-(isPrime0(_201072)), _201074 = _201072, isPrime0(_201074)], (30 ^ _200304) ^ [_201367, _201369] : [-(isFinite0(_201367)), _201369 = _201367, isFinite0(_201369)], (40 ^ _200304) ^ [_201662, _201664] : [-(isOpen0(_201662)), _201664 = _201662, isOpen0(_201664)], (50 ^ _200304) ^ [_201957, _201959] : [-(isClosed0(_201957)), _201959 = _201957, isClosed0(_201959)], (60 ^ _200304) ^ [_202252, _202254] : [-(aSet0(_202252)), _202254 = _202252, aSet0(_202254)], (70 ^ _200304) ^ [_202575, _202577, _202579, _202581] : [-(aSubsetOf0(_202579, _202575)), aSubsetOf0(_202581, _202577), _202581 = _202579, _202577 = _202575], (84 ^ _200304) ^ [_202991, _202993] : [-(aInteger0(_202991)), _202993 = _202991, aInteger0(_202993)], (94 ^ _200304) ^ [_203314, _203316, _203318, _203320] : [-(aDivisorOf0(_203318, _203314)), aDivisorOf0(_203320, _203316), _203320 = _203318, _203316 = _203314], (126 ^ _200304) ^ [_204347, _204349, _204351, _204353] : [-(aElementOf0(_204351, _204347)), aElementOf0(_204353, _204349), _204353 = _204351, _204349 = _204347], (108 ^ _200304) ^ [_203786, _203788, _203790, _203792, _203794, _203796] : [-(sdteqdtlpzmzozddtrp0(_203794, _203790, _203786)), sdteqdtlpzmzozddtrp0(_203796, _203792, _203788), _203796 = _203794, _203792 = _203790, _203788 = _203786], (208 ^ _200304) ^ [_207264] : [aInteger0(_207264), true___, -(true___)], (218 ^ _200304) ^ [] : [-(aInteger0(sz00))], (220 ^ _200304) ^ [] : [-(aInteger0(sz10))], (222 ^ _200304) ^ [_207625] : [aInteger0(_207625), -(aInteger0(smndt0(_207625)))], (228 ^ _200304) ^ [_207829, _207831] : [-(aInteger0(sdtpldt0(_207831, _207829))), aInteger0(_207831), aInteger0(_207829)], (238 ^ _200304) ^ [_208128, _208130] : [-(aInteger0(sdtasdt0(_208130, _208128))), aInteger0(_208130), aInteger0(_208128)], (248 ^ _200304) ^ [_208441, _208443, _208445] : [-(sdtpldt0(_208445, sdtpldt0(_208443, _208441)) = sdtpldt0(sdtpldt0(_208445, _208443), _208441)), aInteger0(_208445), aInteger0(_208443), aInteger0(_208441)], (262 ^ _200304) ^ [_208861, _208863] : [-(sdtpldt0(_208863, _208861) = sdtpldt0(_208861, _208863)), aInteger0(_208863), aInteger0(_208861)], (272 ^ _200304) ^ [_209154] : [aInteger0(_209154), 275 ^ _200304 : [(276 ^ _200304) ^ [] : [-(sdtpldt0(_209154, sz00) = _209154)], (278 ^ _200304) ^ [] : [-(_209154 = sdtpldt0(sz00, _209154))]]], (280 ^ _200304) ^ [_209427] : [aInteger0(_209427), 283 ^ _200304 : [(284 ^ _200304) ^ [] : [-(sdtpldt0(_209427, smndt0(_209427)) = sz00)], (286 ^ _200304) ^ [] : [-(sz00 = sdtpldt0(smndt0(_209427), _209427))]]], (288 ^ _200304) ^ [_209736, _209738, _209740] : [-(sdtasdt0(_209740, sdtasdt0(_209738, _209736)) = sdtasdt0(sdtasdt0(_209740, _209738), _209736)), aInteger0(_209740), aInteger0(_209738), aInteger0(_209736)], (302 ^ _200304) ^ [_210156, _210158] : [-(sdtasdt0(_210158, _210156) = sdtasdt0(_210156, _210158)), aInteger0(_210158), aInteger0(_210156)], (312 ^ _200304) ^ [_210449] : [aInteger0(_210449), 315 ^ _200304 : [(316 ^ _200304) ^ [] : [-(sdtasdt0(_210449, sz10) = _210449)], (318 ^ _200304) ^ [] : [-(_210449 = sdtasdt0(sz10, _210449))]]], (320 ^ _200304) ^ [_210750, _210752, _210754] : [331 ^ _200304 : [(332 ^ _200304) ^ [] : [-(sdtasdt0(_210754, sdtpldt0(_210752, _210750)) = sdtpldt0(sdtasdt0(_210754, _210752), sdtasdt0(_210754, _210750)))], (334 ^ _200304) ^ [] : [-(sdtasdt0(sdtpldt0(_210754, _210752), _210750) = sdtpldt0(sdtasdt0(_210754, _210750), sdtasdt0(_210752, _210750)))]], aInteger0(_210754), aInteger0(_210752), aInteger0(_210750)], (336 ^ _200304) ^ [_211269] : [aInteger0(_211269), 339 ^ _200304 : [(340 ^ _200304) ^ [] : [-(sdtasdt0(_211269, sz00) = sz00)], (342 ^ _200304) ^ [] : [-(sz00 = sdtasdt0(sz00, _211269))]]], (344 ^ _200304) ^ [_211542] : [aInteger0(_211542), 347 ^ _200304 : [(348 ^ _200304) ^ [] : [-(sdtasdt0(smndt0(sz10), _211542) = smndt0(_211542))], (350 ^ _200304) ^ [] : [-(smndt0(_211542) = sdtasdt0(_211542, smndt0(sz10)))]]], (352 ^ _200304) ^ [_211837, _211839] : [aInteger0(_211839), aInteger0(_211837), sdtasdt0(_211839, _211837) = sz00, -(_211839 = sz00), -(_211837 = sz00)], (370 ^ _200304) ^ [_212305] : [aInteger0(_212305), 373 ^ _200304 : [(374 ^ _200304) ^ [_212491] : [aDivisorOf0(_212491, _212305), 377 ^ _200304 : [(378 ^ _200304) ^ [] : [-(aInteger0(_212491))], (380 ^ _200304) ^ [] : [_212491 = sz00], (383 ^ _200304) ^ [] : [-(aInteger0(381 ^ [_212305, _212491]))], (385 ^ _200304) ^ [] : [-(sdtasdt0(_212491, 381 ^ [_212305, _212491]) = _212305)]]], (387 ^ _200304) ^ [_212953] : [-(aDivisorOf0(_212953, _212305)), aInteger0(_212953), -(_212953 = sz00), 396 ^ _200304 : [(397 ^ _200304) ^ [_213220] : [aInteger0(_213220), sdtasdt0(_212953, _213220) = _212305]]]]], (405 ^ _200304) ^ [_213523, _213525, _213527] : [aInteger0(_213527), aInteger0(_213525), aInteger0(_213523), -(_213523 = sz00), 420 ^ _200304 : [(421 ^ _200304) ^ [] : [sdteqdtlpzmzozddtrp0(_213527, _213525, _213523), -(aDivisorOf0(_213523, sdtpldt0(_213527, smndt0(_213525))))], (427 ^ _200304) ^ [] : [aDivisorOf0(_213523, sdtpldt0(_213527, smndt0(_213525))), -(sdteqdtlpzmzozddtrp0(_213527, _213525, _213523))]]], (433 ^ _200304) ^ [_214299, _214301] : [-(sdteqdtlpzmzozddtrp0(_214301, _214301, _214299)), aInteger0(_214301), aInteger0(_214299), -(_214299 = sz00)], (447 ^ _200304) ^ [_214702, _214704, _214706] : [sdteqdtlpzmzozddtrp0(_214706, _214704, _214702), -(sdteqdtlpzmzozddtrp0(_214704, _214706, _214702)), aInteger0(_214706), aInteger0(_214704), aInteger0(_214702), -(_214702 = sz00)], (469 ^ _200304) ^ [_215321, _215323, _215325, _215327] : [-(sdteqdtlpzmzozddtrp0(_215327, _215321, _215323)), sdteqdtlpzmzozddtrp0(_215327, _215325, _215323), sdteqdtlpzmzozddtrp0(_215325, _215321, _215323), aInteger0(_215327), aInteger0(_215325), aInteger0(_215323), -(_215323 = sz00), aInteger0(_215321)], (499 ^ _200304) ^ [_216158, _216160, _216162, _216164] : [sdteqdtlpzmzozddtrp0(_216164, _216162, sdtasdt0(_216160, _216158)), 526 ^ _200304 : [(527 ^ _200304) ^ [] : [-(sdteqdtlpzmzozddtrp0(_216164, _216162, _216160))], (529 ^ _200304) ^ [] : [-(sdteqdtlpzmzozddtrp0(_216164, _216162, _216158))]], aInteger0(_216164), aInteger0(_216162), aInteger0(_216160), -(_216160 = sz00), aInteger0(_216158), -(_216158 = sz00)], (531 ^ _200304) ^ [_217039] : [aInteger0(_217039), -(_217039 = sz00), isPrime0(_217039), true___, -(true___)], (549 ^ _200304) ^ [_217470] : [aInteger0(_217470), 552 ^ _200304 : [(553 ^ _200304) ^ [] : [560 ^ _200304 : [(561 ^ _200304) ^ [] : [_217470 = sz10], (563 ^ _200304) ^ [] : [_217470 = smndt0(sz10)]], 554 ^ _200304 : [(555 ^ _200304) ^ [_217677] : [aDivisorOf0(_217677, _217470), isPrime0(_217677)]]], (565 ^ _200304) ^ [] : [573 ^ _200304 : [(574 ^ _200304) ^ [] : [-(aDivisorOf0(572 ^ [_217470], _217470))], (576 ^ _200304) ^ [] : [-(isPrime0(572 ^ [_217470]))]], -(_217470 = sz10), -(_217470 = smndt0(sz10))]]], (578 ^ _200304) ^ [_218319] : [aSet0(_218319), true___, -(true___)], (588 ^ _200304) ^ [_218574] : [aSet0(_218574), 591 ^ _200304 : [(592 ^ _200304) ^ [_218702] : [aElementOf0(_218702, _218574), true___, -(true___)]]], (602 ^ _200304) ^ [_218979] : [aSet0(_218979), 605 ^ _200304 : [(606 ^ _200304) ^ [_219155] : [aSubsetOf0(_219155, _218979), 609 ^ _200304 : [(610 ^ _200304) ^ [] : [-(aSet0(_219155))], (612 ^ _200304) ^ [_219364] : [aElementOf0(_219364, _219155), -(aElementOf0(_219364, _218979))]]], (618 ^ _200304) ^ [_219543] : [-(aSubsetOf0(_219543, _218979)), aSet0(_219543), 624 ^ _200304 : [(625 ^ _200304) ^ [] : [-(aElementOf0(623 ^ [_218979, _219543], _219543))], (627 ^ _200304) ^ [] : [aElementOf0(623 ^ [_218979, _219543], _218979)]]]]], (631 ^ _200304) ^ [_219980] : [aSet0(_219980), isFinite0(_219980), true___, -(true___)], (645 ^ _200304) ^ [_220335, _220337] : [aSubsetOf0(_220337, cS1395), aSubsetOf0(_220335, cS1395), 652 ^ _200304 : [(683 ^ _200304) ^ [_221600] : [-(_221600 = sdtbsmnsldt0(_220337, _220335)), aSet0(_221600), 691 ^ _200304 : [(692 ^ _200304) ^ [] : [-(aElementOf0(688 ^ [_220335, _220337, _221600], _221600))], (694 ^ _200304) ^ [] : [aInteger0(688 ^ [_220335, _220337, _221600]), 697 ^ _200304 : [(698 ^ _200304) ^ [] : [aElementOf0(688 ^ [_220335, _220337, _221600], _220337)], (700 ^ _200304) ^ [] : [aElementOf0(688 ^ [_220335, _220337, _221600], _220335)]]]], 701 ^ _200304 : [(710 ^ _200304) ^ [] : [aElementOf0(688 ^ [_220335, _220337, _221600], _221600)], (702 ^ _200304) ^ [] : [-(aInteger0(688 ^ [_220335, _220337, _221600]))], (704 ^ _200304) ^ [] : [-(aElementOf0(688 ^ [_220335, _220337, _221600], _220337)), -(aElementOf0(688 ^ [_220335, _220337, _221600], _220335))]]], (653 ^ _200304) ^ [_220620] : [_220620 = sdtbsmnsldt0(_220337, _220335), 656 ^ _200304 : [(657 ^ _200304) ^ [] : [-(aSet0(_220620))], (659 ^ _200304) ^ [_220883] : [aElementOf0(_220883, _220620), 662 ^ _200304 : [(663 ^ _200304) ^ [] : [-(aInteger0(_220883))], (665 ^ _200304) ^ [] : [-(aElementOf0(_220883, _220337)), -(aElementOf0(_220883, _220335))]]], (671 ^ _200304) ^ [_221238] : [-(aElementOf0(_221238, _220620)), aInteger0(_221238), 676 ^ _200304 : [(677 ^ _200304) ^ [] : [aElementOf0(_221238, _220337)], (679 ^ _200304) ^ [] : [aElementOf0(_221238, _220335)]]]]]]], (714 ^ _200304) ^ [_222637, _222639] : [aSubsetOf0(_222639, cS1395), aSubsetOf0(_222637, cS1395), 721 ^ _200304 : [(752 ^ _200304) ^ [_223901] : [-(_223901 = sdtslmnbsdt0(_222639, _222637)), aSet0(_223901), 772 ^ _200304 : [(773 ^ _200304) ^ [] : [-(aInteger0(757 ^ [_222637, _222639, _223901]))], (775 ^ _200304) ^ [] : [-(aElementOf0(757 ^ [_222637, _222639, _223901], _222639))], (777 ^ _200304) ^ [] : [-(aElementOf0(757 ^ [_222637, _222639, _223901], _222637))], (779 ^ _200304) ^ [] : [aElementOf0(757 ^ [_222637, _222639, _223901], _223901)]], 760 ^ _200304 : [(761 ^ _200304) ^ [] : [-(aElementOf0(757 ^ [_222637, _222639, _223901], _223901))], (763 ^ _200304) ^ [] : [aInteger0(757 ^ [_222637, _222639, _223901]), aElementOf0(757 ^ [_222637, _222639, _223901], _222639), aElementOf0(757 ^ [_222637, _222639, _223901], _222637)]]], (722 ^ _200304) ^ [_222922] : [_222922 = sdtslmnbsdt0(_222639, _222637), 725 ^ _200304 : [(726 ^ _200304) ^ [] : [-(aSet0(_222922))], (728 ^ _200304) ^ [_223185] : [aElementOf0(_223185, _222922), 731 ^ _200304 : [(732 ^ _200304) ^ [] : [-(aInteger0(_223185))], (734 ^ _200304) ^ [] : [-(aElementOf0(_223185, _222639))], (736 ^ _200304) ^ [] : [-(aElementOf0(_223185, _222637))]]], (738 ^ _200304) ^ [_223520] : [-(aElementOf0(_223520, _222922)), aInteger0(_223520), aElementOf0(_223520, _222639), aElementOf0(_223520, _222637)]]]]], (783 ^ _200304) ^ [_224927] : [aSet0(_224927), 789 ^ _200304 : [(790 ^ _200304) ^ [] : [-(aElementOf0(788 ^ [_224927], _224927))], (792 ^ _200304) ^ [] : [aSubsetOf0(788 ^ [_224927], cS1395)]], 793 ^ _200304 : [(825 ^ _200304) ^ [_226430] : [-(_226430 = sbsmnsldt0(_224927)), aSet0(_226430), 845 ^ _200304 : [(846 ^ _200304) ^ [] : [-(aInteger0(830 ^ [_224927, _226430]))], (849 ^ _200304) ^ [] : [-(aElementOf0(847 ^ [_224927, _226430], _224927))], (851 ^ _200304) ^ [] : [-(aElementOf0(830 ^ [_224927, _226430], 847 ^ [_224927, _226430]))], (853 ^ _200304) ^ [] : [aElementOf0(830 ^ [_224927, _226430], _226430)]], 833 ^ _200304 : [(834 ^ _200304) ^ [] : [-(aElementOf0(830 ^ [_224927, _226430], _226430))], (836 ^ _200304) ^ [] : [aInteger0(830 ^ [_224927, _226430]), 839 ^ _200304 : [(840 ^ _200304) ^ [_226893] : [aElementOf0(_226893, _224927), aElementOf0(830 ^ [_224927, _226430], _226893)]]]]], (794 ^ _200304) ^ [_225341] : [_225341 = sbsmnsldt0(_224927), 797 ^ _200304 : [(798 ^ _200304) ^ [] : [-(aSet0(_225341))], (800 ^ _200304) ^ [_225599] : [aElementOf0(_225599, _225341), 803 ^ _200304 : [(804 ^ _200304) ^ [] : [-(aInteger0(_225599))], (807 ^ _200304) ^ [] : [-(aElementOf0(805 ^ [_224927, _225341, _225599], _224927))], (809 ^ _200304) ^ [] : [-(aElementOf0(_225599, 805 ^ [_224927, _225341, _225599]))]]], (811 ^ _200304) ^ [_226000] : [-(aElementOf0(_226000, _225341)), aInteger0(_226000), 816 ^ _200304 : [(817 ^ _200304) ^ [_226185] : [aElementOf0(_226185, _224927), aElementOf0(_226000, _226185)]]]]]]], (857 ^ _200304) ^ [_227535] : [aSubsetOf0(_227535, cS1395), 860 ^ _200304 : [(885 ^ _200304) ^ [_228494] : [-(_228494 = stldt0(_227535)), aSet0(_228494), 901 ^ _200304 : [(902 ^ _200304) ^ [] : [-(aInteger0(890 ^ [_227535, _228494]))], (904 ^ _200304) ^ [] : [aElementOf0(890 ^ [_227535, _228494], _227535)], (906 ^ _200304) ^ [] : [aElementOf0(890 ^ [_227535, _228494], _228494)]], 893 ^ _200304 : [(894 ^ _200304) ^ [] : [-(aElementOf0(890 ^ [_227535, _228494], _228494))], (896 ^ _200304) ^ [] : [aInteger0(890 ^ [_227535, _228494]), -(aElementOf0(890 ^ [_227535, _228494], _227535))]]], (861 ^ _200304) ^ [_227722] : [_227722 = stldt0(_227535), 864 ^ _200304 : [(865 ^ _200304) ^ [] : [-(aSet0(_227722))], (867 ^ _200304) ^ [_227971] : [aElementOf0(_227971, _227722), 870 ^ _200304 : [(871 ^ _200304) ^ [] : [-(aInteger0(_227971))], (873 ^ _200304) ^ [] : [aElementOf0(_227971, _227535)]]], (875 ^ _200304) ^ [_228219] : [-(aElementOf0(_228219, _227722)), aInteger0(_228219), -(aElementOf0(_228219, _227535))]]]]], (910 ^ _200304) ^ [_229303, _229305] : [aInteger0(_229305), aInteger0(_229303), -(_229303 = sz00), 921 ^ _200304 : [(946 ^ _200304) ^ [_230474] : [-(_230474 = szAzrzSzezqlpdtcmdtrp0(_229305, _229303)), aSet0(_230474), 962 ^ _200304 : [(963 ^ _200304) ^ [] : [-(aInteger0(951 ^ [_229303, _229305, _230474]))], (965 ^ _200304) ^ [] : [-(sdteqdtlpzmzozddtrp0(951 ^ [_229303, _229305, _230474], _229305, _229303))], (967 ^ _200304) ^ [] : [aElementOf0(951 ^ [_229303, _229305, _230474], _230474)]], 954 ^ _200304 : [(955 ^ _200304) ^ [] : [-(aElementOf0(951 ^ [_229303, _229305, _230474], _230474))], (957 ^ _200304) ^ [] : [aInteger0(951 ^ [_229303, _229305, _230474]), sdteqdtlpzmzozddtrp0(951 ^ [_229303, _229305, _230474], _229305, _229303)]]], (922 ^ _200304) ^ [_229671] : [_229671 = szAzrzSzezqlpdtcmdtrp0(_229305, _229303), 925 ^ _200304 : [(926 ^ _200304) ^ [] : [-(aSet0(_229671))], (928 ^ _200304) ^ [_229929] : [aElementOf0(_229929, _229671), 931 ^ _200304 : [(932 ^ _200304) ^ [] : [-(aInteger0(_229929))], (934 ^ _200304) ^ [] : [-(sdteqdtlpzmzozddtrp0(_229929, _229305, _229303))]]], (936 ^ _200304) ^ [_230188] : [-(aElementOf0(_230188, _229671)), aInteger0(_230188), sdteqdtlpzmzozddtrp0(_230188, _229305, _229303)]]]]], (971 ^ _200304) ^ [_231317] : [aSubsetOf0(_231317, cS1395), 974 ^ _200304 : [(975 ^ _200304) ^ [] : [isOpen0(_231317), 978 ^ _200304 : [(979 ^ _200304) ^ [_231579] : [aElementOf0(_231579, _231317), 983 ^ _200304 : [(984 ^ _200304) ^ [] : [-(aInteger0(982 ^ [_231317, _231579]))], (986 ^ _200304) ^ [] : [982 ^ [_231317, _231579] = sz00], (988 ^ _200304) ^ [] : [-(aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(_231579, 982 ^ [_231317, _231579]), _231317))]]]]], (990 ^ _200304) ^ [] : [-(isOpen0(_231317)), 992 ^ _200304 : [(993 ^ _200304) ^ [] : [-(aElementOf0(991 ^ [_231317], _231317))], (995 ^ _200304) ^ [_232172] : [aInteger0(_232172), -(_232172 = sz00), aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(991 ^ [_231317], _232172), _231317)]]]]], (1007 ^ _200304) ^ [_232532] : [aSubsetOf0(_232532, cS1395), 1010 ^ _200304 : [(1011 ^ _200304) ^ [] : [isClosed0(_232532), -(isOpen0(stldt0(_232532)))], (1017 ^ _200304) ^ [] : [isOpen0(stldt0(_232532)), -(isClosed0(_232532))]]], (1023 ^ _200304) ^ [_232962] : [-(isOpen0(sbsmnsldt0(_232962))), aSet0(_232962), 1029 ^ _200304 : [(1030 ^ _200304) ^ [] : [-(aElementOf0(1028 ^ [_232962], _232962))], (1032 ^ _200304) ^ [] : [aSubsetOf0(1028 ^ [_232962], cS1395), isOpen0(1028 ^ [_232962])]]], (1040 ^ _200304) ^ [_233479, _233481] : [-(isOpen0(sdtslmnbsdt0(_233481, _233479))), aSubsetOf0(_233481, cS1395), aSubsetOf0(_233479, cS1395), isOpen0(_233481), isOpen0(_233479)], (1058 ^ _200304) ^ [_233956, _233958] : [-(isClosed0(sdtbsmnsldt0(_233958, _233956))), aSubsetOf0(_233958, cS1395), aSubsetOf0(_233956, cS1395), isClosed0(_233958), isClosed0(_233956)], (1076 ^ _200304) ^ [_234419] : [-(isClosed0(sbsmnsldt0(_234419))), aSet0(_234419), isFinite0(_234419), 1086 ^ _200304 : [(1087 ^ _200304) ^ [] : [-(aElementOf0(1085 ^ [_234419], _234419))], (1089 ^ _200304) ^ [] : [aSubsetOf0(1085 ^ [_234419], cS1395), isClosed0(1085 ^ [_234419])]]], (1097 ^ _200304) ^ [_235019, _235021] : [1108 ^ _200304 : [(1109 ^ _200304) ^ [] : [-(aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(_235021, _235019), cS1395))], (1111 ^ _200304) ^ [] : [-(isClosed0(szAzrzSzezqlpdtcmdtrp0(_235021, _235019)))]], aInteger0(_235021), aInteger0(_235019), -(_235019 = sz00)], (1113 ^ _200304) ^ [] : [-(aSet0(xS))], (1216 ^ _200304) ^ [] : [-(xS = cS2043)], (1115 ^ _200304) ^ [_235570] : [aElementOf0(_235570, xS), 1119 ^ _200304 : [(1120 ^ _200304) ^ [] : [-(aInteger0(1118 ^ [_235570]))], (1122 ^ _200304) ^ [] : [1118 ^ [_235570] = sz00], (1124 ^ _200304) ^ [] : [-(isPrime0(1118 ^ [_235570]))], (1126 ^ _200304) ^ [] : [-(aSet0(szAzrzSzezqlpdtcmdtrp0(sz00, 1118 ^ [_235570])))], (1161 ^ _200304) ^ [] : [-(szAzrzSzezqlpdtcmdtrp0(sz00, 1118 ^ [_235570]) = _235570)], (1128 ^ _200304) ^ [_236329] : [aElementOf0(_236329, szAzrzSzezqlpdtcmdtrp0(sz00, 1118 ^ [_235570])), 1131 ^ _200304 : [(1132 ^ _200304) ^ [] : [-(aInteger0(_236329))], (1135 ^ _200304) ^ [] : [-(aInteger0(1133 ^ [_235570, _236329]))], (1137 ^ _200304) ^ [] : [-(sdtasdt0(1118 ^ [_235570], 1133 ^ [_235570, _236329]) = sdtpldt0(_236329, smndt0(sz00)))], (1139 ^ _200304) ^ [] : [-(aDivisorOf0(1118 ^ [_235570], sdtpldt0(_236329, smndt0(sz00))))], (1141 ^ _200304) ^ [] : [-(sdteqdtlpzmzozddtrp0(_236329, sz00, 1118 ^ [_235570]))]]], (1143 ^ _200304) ^ [_236934] : [-(aElementOf0(_236934, szAzrzSzezqlpdtcmdtrp0(sz00, 1118 ^ [_235570]))), aInteger0(_236934), 1148 ^ _200304 : [(1155 ^ _200304) ^ [] : [aDivisorOf0(1118 ^ [_235570], sdtpldt0(_236934, smndt0(sz00)))], (1157 ^ _200304) ^ [] : [sdteqdtlpzmzozddtrp0(_236934, sz00, 1118 ^ [_235570])], (1149 ^ _200304) ^ [_237175] : [aInteger0(_237175), sdtasdt0(1118 ^ [_235570], _237175) = sdtpldt0(_236934, smndt0(sz00))]]]]], (1163 ^ _200304) ^ [_237628] : [-(aElementOf0(_237628, xS)), 1164 ^ _200304 : [(1165 ^ _200304) ^ [_237850] : [aInteger0(_237850), -(_237850 = sz00), isPrime0(_237850), 1176 ^ _200304 : [(1212 ^ _200304) ^ [] : [szAzrzSzezqlpdtcmdtrp0(sz00, _237850) = _237628], (1177 ^ _200304) ^ [] : [-(aSet0(szAzrzSzezqlpdtcmdtrp0(sz00, _237850)))], (1179 ^ _200304) ^ [_238375] : [aElementOf0(_238375, szAzrzSzezqlpdtcmdtrp0(sz00, _237850)), 1182 ^ _200304 : [(1183 ^ _200304) ^ [] : [-(aInteger0(_238375))], (1186 ^ _200304) ^ [] : [-(aInteger0(1184 ^ [_237628, _237850, _238375]))], (1188 ^ _200304) ^ [] : [-(sdtasdt0(_237850, 1184 ^ [_237628, _237850, _238375]) = sdtpldt0(_238375, smndt0(sz00)))], (1190 ^ _200304) ^ [] : [-(aDivisorOf0(_237850, sdtpldt0(_238375, smndt0(sz00))))], (1192 ^ _200304) ^ [] : [-(sdteqdtlpzmzozddtrp0(_238375, sz00, _237850))]]], (1194 ^ _200304) ^ [_238959] : [-(aElementOf0(_238959, szAzrzSzezqlpdtcmdtrp0(sz00, _237850))), aInteger0(_238959), 1199 ^ _200304 : [(1206 ^ _200304) ^ [] : [aDivisorOf0(_237850, sdtpldt0(_238959, smndt0(sz00)))], (1208 ^ _200304) ^ [] : [sdteqdtlpzmzozddtrp0(_238959, sz00, _237850)], (1200 ^ _200304) ^ [_239188] : [aInteger0(_239188), sdtasdt0(_237850, _239188) = sdtpldt0(_238959, smndt0(sz00))]]]]]]], (1218 ^ _200304) ^ [] : [-(aSet0(sbsmnsldt0(xS)))], (1220 ^ _200304) ^ [_239852] : [aElementOf0(_239852, sbsmnsldt0(xS)), 1223 ^ _200304 : [(1224 ^ _200304) ^ [] : [-(aInteger0(_239852))], (1227 ^ _200304) ^ [] : [-(aElementOf0(1225 ^ [_239852], xS))], (1229 ^ _200304) ^ [] : [-(aElementOf0(_239852, 1225 ^ [_239852]))]]], (1231 ^ _200304) ^ [_240213] : [-(aElementOf0(_240213, sbsmnsldt0(xS))), aInteger0(_240213), 1236 ^ _200304 : [(1237 ^ _200304) ^ [_240382] : [aElementOf0(_240382, xS), aElementOf0(_240213, _240382)]]], (1245 ^ _200304) ^ [] : [-(aSet0(stldt0(sbsmnsldt0(xS))))], (1247 ^ _200304) ^ [_240716] : [aElementOf0(_240716, stldt0(sbsmnsldt0(xS))), 1250 ^ _200304 : [(1251 ^ _200304) ^ [] : [-(aInteger0(_240716))], (1253 ^ _200304) ^ [] : [aElementOf0(_240716, sbsmnsldt0(xS))]]], (1255 ^ _200304) ^ [_240944] : [-(aElementOf0(_240944, stldt0(sbsmnsldt0(xS)))), aInteger0(_240944), -(aElementOf0(_240944, sbsmnsldt0(xS)))], (1283 ^ _200304) ^ [] : [-(stldt0(sbsmnsldt0(xS)) = cS2076)], (1275 ^ _200304) ^ [_241493] : [1276 ^ _200304 : [(1277 ^ _200304) ^ [] : [_241493 = sz10], (1279 ^ _200304) ^ [] : [_241493 = smndt0(sz10)]], -(aElementOf0(_241493, stldt0(sbsmnsldt0(xS))))], (1265 ^ _200304) ^ [_241251] : [aElementOf0(_241251, stldt0(sbsmnsldt0(xS))), -(_241251 = sz10), -(_241251 = smndt0(sz10))], (1285 ^ _200304) ^ [] : [-(isFinite0(xS))], (1578 ^ _200304) ^ [] : [-(aInteger0(1576 ^ []))], (1580 ^ _200304) ^ [] : [-(sdtasdt0(xp, 1576 ^ []) = sdtpldt0(sdtpldt0(sz10, xp), smndt0(sz10)))], (1582 ^ _200304) ^ [] : [-(aDivisorOf0(xp, sdtpldt0(sdtpldt0(sz10, xp), smndt0(sz10))))], (1584 ^ _200304) ^ [] : [-(sdteqdtlpzmzozddtrp0(sdtpldt0(sz10, xp), sz10, xp))], (1586 ^ _200304) ^ [] : [-(aElementOf0(sdtpldt0(sz10, xp), szAzrzSzezqlpdtcmdtrp0(sz10, xp)))], (1589 ^ _200304) ^ [] : [-(aInteger0(1587 ^ []))], (1591 ^ _200304) ^ [] : [-(sdtasdt0(xp, 1587 ^ []) = sdtpldt0(sdtpldt0(sz10, smndt0(xp)), smndt0(sz10)))], (1593 ^ _200304) ^ [] : [-(aDivisorOf0(xp, sdtpldt0(sdtpldt0(sz10, smndt0(xp)), smndt0(sz10))))], (1595 ^ _200304) ^ [] : [-(sdteqdtlpzmzozddtrp0(sdtpldt0(sz10, smndt0(xp)), sz10, xp))], (1597 ^ _200304) ^ [] : [-(aElementOf0(sdtpldt0(sz10, smndt0(xp)), szAzrzSzezqlpdtcmdtrp0(sz10, xp)))], (1599 ^ _200304) ^ [] : [sdtpldt0(sz10, xp) = sz10], (1601 ^ _200304) ^ [] : [sdtpldt0(sz10, smndt0(xp)) = sz10], (1603 ^ _200304) ^ [] : [sdtpldt0(sz10, xp) = smndt0(sz10), sdtpldt0(sz10, smndt0(xp)) = smndt0(sz10)], (1485 ^ _200304) ^ [] : [-(aInteger0(xp))], (1487 ^ _200304) ^ [] : [xp = sz00], (1489 ^ _200304) ^ [] : [-(aSet0(szAzrzSzezqlpdtcmdtrp0(sz10, xp)))], (1491 ^ _200304) ^ [_249597] : [aElementOf0(_249597, szAzrzSzezqlpdtcmdtrp0(sz10, xp)), 1494 ^ _200304 : [(1495 ^ _200304) ^ [] : [-(aInteger0(_249597))], (1498 ^ _200304) ^ [] : [-(aInteger0(1496 ^ [_249597]))], (1500 ^ _200304) ^ [] : [-(sdtasdt0(xp, 1496 ^ [_249597]) = sdtpldt0(_249597, smndt0(sz10)))], (1502 ^ _200304) ^ [] : [-(aDivisorOf0(xp, sdtpldt0(_249597, smndt0(sz10))))], (1504 ^ _200304) ^ [] : [-(sdteqdtlpzmzozddtrp0(_249597, sz10, xp))]]], (1506 ^ _200304) ^ [_250127] : [-(aElementOf0(_250127, szAzrzSzezqlpdtcmdtrp0(sz10, xp))), aInteger0(_250127), 1511 ^ _200304 : [(1518 ^ _200304) ^ [] : [aDivisorOf0(xp, sdtpldt0(_250127, smndt0(sz10)))], (1520 ^ _200304) ^ [] : [sdteqdtlpzmzozddtrp0(_250127, sz10, xp)], (1512 ^ _200304) ^ [_250337] : [aInteger0(_250337), sdtasdt0(xp, _250337) = sdtpldt0(_250127, smndt0(sz10))]]], (1524 ^ _200304) ^ [] : [-(aSet0(sbsmnsldt0(xS)))], (1526 ^ _200304) ^ [_250797] : [aElementOf0(_250797, sbsmnsldt0(xS)), 1529 ^ _200304 : [(1530 ^ _200304) ^ [] : [-(aInteger0(_250797))], (1533 ^ _200304) ^ [] : [-(aElementOf0(1531 ^ [_250797], xS))], (1535 ^ _200304) ^ [] : [-(aElementOf0(_250797, 1531 ^ [_250797]))]]], (1537 ^ _200304) ^ [_251158] : [-(aElementOf0(_251158, sbsmnsldt0(xS))), aInteger0(_251158), 1542 ^ _200304 : [(1543 ^ _200304) ^ [_251327] : [aElementOf0(_251327, xS), aElementOf0(_251158, _251327)]]], (1575 ^ _200304) ^ [] : [-(aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10, xp), stldt0(sbsmnsldt0(xS))))], (1569 ^ _200304) ^ [_252114] : [aElementOf0(_252114, szAzrzSzezqlpdtcmdtrp0(sz10, xp)), -(aElementOf0(_252114, stldt0(sbsmnsldt0(xS))))], (1551 ^ _200304) ^ [_251608] : [aElementOf0(_251608, stldt0(sbsmnsldt0(xS))), 1554 ^ _200304 : [(1555 ^ _200304) ^ [] : [-(aInteger0(_251608))], (1557 ^ _200304) ^ [] : [aElementOf0(_251608, sbsmnsldt0(xS))]]], (1559 ^ _200304) ^ [_251836] : [-(aElementOf0(_251836, stldt0(sbsmnsldt0(xS)))), aInteger0(_251836), -(aElementOf0(_251836, sbsmnsldt0(xS)))], (1287 ^ _200304) ^ [] : [-(aSet0(sbsmnsldt0(xS)))], (1289 ^ _200304) ^ [_241959] : [aElementOf0(_241959, sbsmnsldt0(xS)), 1292 ^ _200304 : [(1293 ^ _200304) ^ [] : [-(aInteger0(_241959))], (1296 ^ _200304) ^ [] : [-(aElementOf0(1294 ^ [_241959], xS))], (1298 ^ _200304) ^ [] : [-(aElementOf0(_241959, 1294 ^ [_241959]))]]], (1300 ^ _200304) ^ [_242320] : [-(aElementOf0(_242320, sbsmnsldt0(xS))), aInteger0(_242320), 1305 ^ _200304 : [(1306 ^ _200304) ^ [_242489] : [aElementOf0(_242489, xS), aElementOf0(_242320, _242489)]]], (1314 ^ _200304) ^ [_242770] : [aElementOf0(_242770, stldt0(sbsmnsldt0(xS))), 1317 ^ _200304 : [(1318 ^ _200304) ^ [] : [-(aInteger0(_242770))], (1320 ^ _200304) ^ [] : [aElementOf0(_242770, sbsmnsldt0(xS))]]], (1322 ^ _200304) ^ [_242998] : [-(aElementOf0(_242998, stldt0(sbsmnsldt0(xS)))), aInteger0(_242998), -(aElementOf0(_242998, sbsmnsldt0(xS)))], (1332 ^ _200304) ^ [_243276] : [aElementOf0(_243276, stldt0(sbsmnsldt0(xS))), 1336 ^ _200304 : [(1337 ^ _200304) ^ [] : [-(aInteger0(1335 ^ [_243276]))], (1339 ^ _200304) ^ [] : [1335 ^ [_243276] = sz00], (1341 ^ _200304) ^ [] : [-(aSet0(szAzrzSzezqlpdtcmdtrp0(_243276, 1335 ^ [_243276])))], (1382 ^ _200304) ^ [] : [-(aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(_243276, 1335 ^ [_243276]), stldt0(sbsmnsldt0(xS))))], (1376 ^ _200304) ^ [_245299] : [aElementOf0(_245299, szAzrzSzezqlpdtcmdtrp0(_243276, 1335 ^ [_243276])), -(aElementOf0(_245299, stldt0(sbsmnsldt0(xS))))], (1343 ^ _200304) ^ [_244013] : [aElementOf0(_244013, szAzrzSzezqlpdtcmdtrp0(_243276, 1335 ^ [_243276])), 1346 ^ _200304 : [(1347 ^ _200304) ^ [] : [-(aInteger0(_244013))], (1350 ^ _200304) ^ [] : [-(aInteger0(1348 ^ [_243276, _244013]))], (1352 ^ _200304) ^ [] : [-(sdtasdt0(1335 ^ [_243276], 1348 ^ [_243276, _244013]) = sdtpldt0(_244013, smndt0(_243276)))], (1354 ^ _200304) ^ [] : [-(aDivisorOf0(1335 ^ [_243276], sdtpldt0(_244013, smndt0(_243276))))], (1356 ^ _200304) ^ [] : [-(sdteqdtlpzmzozddtrp0(_244013, _243276, 1335 ^ [_243276]))]]], (1358 ^ _200304) ^ [_244628] : [-(aElementOf0(_244628, szAzrzSzezqlpdtcmdtrp0(_243276, 1335 ^ [_243276]))), aInteger0(_244628), 1363 ^ _200304 : [(1370 ^ _200304) ^ [] : [aDivisorOf0(1335 ^ [_243276], sdtpldt0(_244628, smndt0(_243276)))], (1372 ^ _200304) ^ [] : [sdteqdtlpzmzozddtrp0(_244628, _243276, 1335 ^ [_243276])], (1364 ^ _200304) ^ [_244873] : [aInteger0(_244873), sdtasdt0(1335 ^ [_243276], _244873) = sdtpldt0(_244628, smndt0(_243276))]]]]], (1384 ^ _200304) ^ [] : [-(isOpen0(stldt0(sbsmnsldt0(xS))))], (1386 ^ _200304) ^ [] : [-(isClosed0(sbsmnsldt0(xS)))], (1388 ^ _200304) ^ [] : [-(aSet0(sbsmnsldt0(xS)))], (1390 ^ _200304) ^ [_245770] : [aElementOf0(_245770, sbsmnsldt0(xS)), 1393 ^ _200304 : [(1394 ^ _200304) ^ [] : [-(aInteger0(_245770))], (1397 ^ _200304) ^ [] : [-(aElementOf0(1395 ^ [_245770], xS))], (1399 ^ _200304) ^ [] : [-(aElementOf0(_245770, 1395 ^ [_245770]))]]], (1401 ^ _200304) ^ [_246131] : [-(aElementOf0(_246131, sbsmnsldt0(xS))), aInteger0(_246131), 1406 ^ _200304 : [(1407 ^ _200304) ^ [_246300] : [aElementOf0(_246300, xS), aElementOf0(_246131, _246300)]]], (1415 ^ _200304) ^ [_246581] : [aElementOf0(_246581, stldt0(sbsmnsldt0(xS))), 1418 ^ _200304 : [(1419 ^ _200304) ^ [] : [-(aInteger0(_246581))], (1421 ^ _200304) ^ [] : [aElementOf0(_246581, sbsmnsldt0(xS))]]], (1423 ^ _200304) ^ [_246809] : [-(aElementOf0(_246809, stldt0(sbsmnsldt0(xS)))), aInteger0(_246809), -(aElementOf0(_246809, sbsmnsldt0(xS)))], (1433 ^ _200304) ^ [_247067] : [aElementOf0(_247067, stldt0(sbsmnsldt0(xS))), 1437 ^ _200304 : [(1438 ^ _200304) ^ [] : [-(aInteger0(1436 ^ [_247067]))], (1440 ^ _200304) ^ [] : [1436 ^ [_247067] = sz00], (1442 ^ _200304) ^ [] : [-(aSet0(szAzrzSzezqlpdtcmdtrp0(_247067, 1436 ^ [_247067])))], (1483 ^ _200304) ^ [] : [-(aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(_247067, 1436 ^ [_247067]), stldt0(sbsmnsldt0(xS))))], (1477 ^ _200304) ^ [_249090] : [aElementOf0(_249090, szAzrzSzezqlpdtcmdtrp0(_247067, 1436 ^ [_247067])), -(aElementOf0(_249090, stldt0(sbsmnsldt0(xS))))], (1444 ^ _200304) ^ [_247804] : [aElementOf0(_247804, szAzrzSzezqlpdtcmdtrp0(_247067, 1436 ^ [_247067])), 1447 ^ _200304 : [(1448 ^ _200304) ^ [] : [-(aInteger0(_247804))], (1451 ^ _200304) ^ [] : [-(aInteger0(1449 ^ [_247067, _247804]))], (1453 ^ _200304) ^ [] : [-(sdtasdt0(1436 ^ [_247067], 1449 ^ [_247067, _247804]) = sdtpldt0(_247804, smndt0(_247067)))], (1455 ^ _200304) ^ [] : [-(aDivisorOf0(1436 ^ [_247067], sdtpldt0(_247804, smndt0(_247067))))], (1457 ^ _200304) ^ [] : [-(sdteqdtlpzmzozddtrp0(_247804, _247067, 1436 ^ [_247067]))]]], (1459 ^ _200304) ^ [_248419] : [-(aElementOf0(_248419, szAzrzSzezqlpdtcmdtrp0(_247067, 1436 ^ [_247067]))), aInteger0(_248419), 1464 ^ _200304 : [(1471 ^ _200304) ^ [] : [aDivisorOf0(1436 ^ [_247067], sdtpldt0(_248419, smndt0(_247067)))], (1473 ^ _200304) ^ [] : [sdteqdtlpzmzozddtrp0(_248419, _247067, 1436 ^ [_247067])], (1465 ^ _200304) ^ [_248664] : [aInteger0(_248664), sdtasdt0(1436 ^ [_247067], _248664) = sdtpldt0(_248419, smndt0(_247067))]]]]]], input).
% 0.34/1.37 ncf('1',plain,[sdtpldt0(sz10, xp) = smndt0(sz10), sdtpldt0(sz10, smndt0(xp)) = smndt0(sz10)],start(1603 ^ 0)).
% 0.34/1.37 ncf('1.1',plain,[-(sdtpldt0(sz10, xp) = smndt0(sz10)), 1627 : -(sdtpldt0(sz10, xp) = sz10), 1625 : aElementOf0(sdtpldt0(sz10, xp), szAzrzSzezqlpdtcmdtrp0(sz10, xp))],extension(1609 ^ 1,bind([[_253688], [sdtpldt0(sz10, xp)]]))).
% 0.34/1.37 ncf('1.1.1',plain,[sdtpldt0(sz10, xp) = sz10],extension(1599 ^ 4)).
% 0.34/1.37 ncf('1.1.2',plain,[-(aElementOf0(sdtpldt0(sz10, xp), szAzrzSzezqlpdtcmdtrp0(sz10, xp)))],extension(1586 ^ 4)).
% 0.34/1.37 ncf('1.2',plain,[-(sdtpldt0(sz10, smndt0(xp)) = smndt0(sz10)), 1627 : -(sdtpldt0(sz10, smndt0(xp)) = sz10), 1625 : aElementOf0(sdtpldt0(sz10, smndt0(xp)), szAzrzSzezqlpdtcmdtrp0(sz10, xp))],extension(1609 ^ 1,bind([[_253688], [sdtpldt0(sz10, smndt0(xp))]]))).
% 0.34/1.37 ncf('1.2.1',plain,[sdtpldt0(sz10, smndt0(xp)) = sz10],extension(1601 ^ 4)).
% 0.34/1.37 ncf('1.2.2',plain,[-(aElementOf0(sdtpldt0(sz10, smndt0(xp)), szAzrzSzezqlpdtcmdtrp0(sz10, xp)))],extension(1597 ^ 4)).
% 0.34/1.37 %-----------------------------------------------------
% 0.34/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------