%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWC352+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n022.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 12:13:18 EDT 2023
% Result : Theorem 139.48s 134.92s
% Output : Proof 139.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SWC352+1 : TPTP v8.1.2. Released v2.4.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n022.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Fri May 19 00:54:16 EDT 2023
% 0.13/0.35 % CPUTime :
% 139.48/134.92
% 139.48/134.92 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 139.48/134.92 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 139.48/134.92 %-----------------------------------------------------
% 139.48/134.92 ncf(matrix, plain, [(1978 ^ _233007) ^ [] : [-(ssList(1976 ^ []))], (1981 ^ _233007) ^ [] : [-(ssList(1979 ^ []))], (1984 ^ _233007) ^ [] : [-(ssList(1982 ^ []))], (1987 ^ _233007) ^ [] : [-(ssList(1985 ^ []))], (1989 ^ _233007) ^ [] : [-(1979 ^ [] = 1985 ^ [])], (1991 ^ _233007) ^ [] : [-(1976 ^ [] = 1982 ^ [])], (1993 ^ _233007) ^ [] : [frontsegP(1979 ^ [], 1976 ^ [])], (1995 ^ _233007) ^ [] : [-(nil = 1982 ^ []), nil = 1985 ^ []], (2001 ^ _233007) ^ [] : [neq(1985 ^ [], nil), 2004 ^ _233007 : [(2005 ^ _233007) ^ [] : [-(neq(1982 ^ [], nil))], (2007 ^ _233007) ^ [] : [-(frontsegP(1985 ^ [], 1982 ^ []))]]], (246 ^ _233007) ^ [_240811, _240813, _240815, _240817] : [-(cons(_240817, _240813) = cons(_240815, _240811)), _240817 = _240815, _240813 = _240811], (256 ^ _233007) ^ [_241142, _241144] : [_241144 = _241142, -(hd(_241144) = hd(_241142))], (272 ^ _233007) ^ [_241699, _241701] : [_241701 = _241699, -(tl(_241701) = tl(_241699))], (262 ^ _233007) ^ [_241388, _241390, _241392, _241394] : [-(app(_241394, _241390) = app(_241392, _241388)), _241394 = _241392, _241390 = _241388], (2 ^ _233007) ^ [_233151] : [-(_233151 = _233151)], (4 ^ _233007) ^ [_233258, _233260] : [_233260 = _233258, -(_233258 = _233260)], (10 ^ _233007) ^ [_233462, _233464, _233466] : [-(_233466 = _233462), _233466 = _233464, _233464 = _233462], (20 ^ _233007) ^ [_233803, _233805, _233807, _233809] : [-(memberP(_233807, _233803)), memberP(_233809, _233805), _233809 = _233807, _233805 = _233803], (34 ^ _233007) ^ [_234219, _234221] : [-(singletonP(_234219)), _234221 = _234219, singletonP(_234221)], (44 ^ _233007) ^ [_234542, _234544, _234546, _234548] : [-(rearsegP(_234546, _234542)), rearsegP(_234548, _234544), _234548 = _234546, _234544 = _234542], (58 ^ _233007) ^ [_234986, _234988, _234990, _234992] : [-(segmentP(_234990, _234986)), segmentP(_234992, _234988), _234992 = _234990, _234988 = _234986], (72 ^ _233007) ^ [_235402, _235404] : [-(cyclefreeP(_235402)), _235404 = _235402, cyclefreeP(_235404)], (82 ^ _233007) ^ [_235697, _235699] : [-(totalorderP(_235697)), _235699 = _235697, totalorderP(_235699)], (92 ^ _233007) ^ [_235992, _235994] : [-(strictorderP(_235992)), _235994 = _235992, strictorderP(_235994)], (102 ^ _233007) ^ [_236287, _236289] : [-(totalorderedP(_236287)), _236289 = _236287, totalorderedP(_236289)], (112 ^ _233007) ^ [_236582, _236584] : [-(strictorderedP(_236582)), _236584 = _236582, strictorderedP(_236584)], (122 ^ _233007) ^ [_236877, _236879] : [-(duplicatefreeP(_236877)), _236879 = _236877, duplicatefreeP(_236879)], (132 ^ _233007) ^ [_237172, _237174] : [-(equalelemsP(_237172)), _237174 = _237172, equalelemsP(_237174)], (142 ^ _233007) ^ [_237495, _237497, _237499, _237501] : [-(geq(_237499, _237495)), geq(_237501, _237497), _237501 = _237499, _237497 = _237495], (156 ^ _233007) ^ [_237939, _237941, _237943, _237945] : [-(lt(_237943, _237939)), lt(_237945, _237941), _237945 = _237943, _237941 = _237939], (170 ^ _233007) ^ [_238383, _238385, _238387, _238389] : [-(leq(_238387, _238383)), leq(_238389, _238385), _238389 = _238387, _238385 = _238383], (184 ^ _233007) ^ [_238799, _238801] : [-(ssItem(_238799)), _238801 = _238799, ssItem(_238801)], (194 ^ _233007) ^ [_239122, _239124, _239126, _239128] : [-(gt(_239126, _239122)), gt(_239128, _239124), _239128 = _239126, _239124 = _239122], (208 ^ _233007) ^ [_239538, _239540] : [-(ssList(_239538)), _239540 = _239538, ssList(_239540)], (218 ^ _233007) ^ [_239861, _239863, _239865, _239867] : [-(neq(_239865, _239861)), neq(_239867, _239863), _239867 = _239865, _239863 = _239861], (232 ^ _233007) ^ [_240285, _240287, _240289, _240291] : [-(frontsegP(_240289, _240285)), frontsegP(_240291, _240287), _240291 = _240289, _240287 = _240285], (278 ^ _233007) ^ [_241921] : [ssItem(_241921), 281 ^ _233007 : [(282 ^ _233007) ^ [_242059] : [ssItem(_242059), 285 ^ _233007 : [(286 ^ _233007) ^ [] : [neq(_241921, _242059), _241921 = _242059], (292 ^ _233007) ^ [] : [-(_241921 = _242059), -(neq(_241921, _242059))]]]]], (299 ^ _233007) ^ [] : [-(ssItem(297 ^ []))], (302 ^ _233007) ^ [] : [-(ssItem(300 ^ []))], (304 ^ _233007) ^ [] : [297 ^ [] = 300 ^ []], (306 ^ _233007) ^ [_242772] : [ssList(_242772), 309 ^ _233007 : [(310 ^ _233007) ^ [_242934] : [ssItem(_242934), 313 ^ _233007 : [(314 ^ _233007) ^ [] : [memberP(_242772, _242934), 318 ^ _233007 : [(319 ^ _233007) ^ [] : [-(ssList(317 ^ [_242772, _242934]))], (322 ^ _233007) ^ [] : [-(ssList(320 ^ [_242772, _242934]))], (324 ^ _233007) ^ [] : [-(app(317 ^ [_242772, _242934], cons(_242934, 320 ^ [_242772, _242934])) = _242772)]]], (326 ^ _233007) ^ [] : [-(memberP(_242772, _242934)), 327 ^ _233007 : [(328 ^ _233007) ^ [_243582] : [ssList(_243582), 331 ^ _233007 : [(332 ^ _233007) ^ [_243730] : [ssList(_243730), app(_243582, cons(_242934, _243730)) = _242772]]]]]]]]], (340 ^ _233007) ^ [_244021] : [ssList(_244021), 343 ^ _233007 : [(344 ^ _233007) ^ [] : [singletonP(_244021), 348 ^ _233007 : [(349 ^ _233007) ^ [] : [-(ssItem(347 ^ [_244021]))], (351 ^ _233007) ^ [] : [-(cons(347 ^ [_244021], nil) = _244021)]]], (353 ^ _233007) ^ [] : [-(singletonP(_244021)), 354 ^ _233007 : [(355 ^ _233007) ^ [_244470] : [ssItem(_244470), cons(_244470, nil) = _244021]]]]], (363 ^ _233007) ^ [_244726] : [ssList(_244726), 366 ^ _233007 : [(367 ^ _233007) ^ [_244875] : [ssList(_244875), 370 ^ _233007 : [(371 ^ _233007) ^ [] : [frontsegP(_244726, _244875), 375 ^ _233007 : [(376 ^ _233007) ^ [] : [-(ssList(374 ^ [_244726, _244875]))], (378 ^ _233007) ^ [] : [-(app(_244875, 374 ^ [_244726, _244875]) = _244726)]]], (380 ^ _233007) ^ [] : [-(frontsegP(_244726, _244875)), 381 ^ _233007 : [(382 ^ _233007) ^ [_245350] : [ssList(_245350), app(_244875, _245350) = _244726]]]]]]], (390 ^ _233007) ^ [_245622] : [ssList(_245622), 393 ^ _233007 : [(394 ^ _233007) ^ [_245771] : [ssList(_245771), 397 ^ _233007 : [(398 ^ _233007) ^ [] : [rearsegP(_245622, _245771), 402 ^ _233007 : [(403 ^ _233007) ^ [] : [-(ssList(401 ^ [_245622, _245771]))], (405 ^ _233007) ^ [] : [-(app(401 ^ [_245622, _245771], _245771) = _245622)]]], (407 ^ _233007) ^ [] : [-(rearsegP(_245622, _245771)), 408 ^ _233007 : [(409 ^ _233007) ^ [_246246] : [ssList(_246246), app(_246246, _245771) = _245622]]]]]]], (417 ^ _233007) ^ [_246518] : [ssList(_246518), 420 ^ _233007 : [(421 ^ _233007) ^ [_246680] : [ssList(_246680), 424 ^ _233007 : [(425 ^ _233007) ^ [] : [segmentP(_246518, _246680), 429 ^ _233007 : [(430 ^ _233007) ^ [] : [-(ssList(428 ^ [_246518, _246680]))], (433 ^ _233007) ^ [] : [-(ssList(431 ^ [_246518, _246680]))], (435 ^ _233007) ^ [] : [-(app(app(428 ^ [_246518, _246680], _246680), 431 ^ [_246518, _246680]) = _246518)]]], (437 ^ _233007) ^ [] : [-(segmentP(_246518, _246680)), 438 ^ _233007 : [(439 ^ _233007) ^ [_247328] : [ssList(_247328), 442 ^ _233007 : [(443 ^ _233007) ^ [_247476] : [ssList(_247476), app(app(_247328, _246680), _247476) = _246518]]]]]]]]], (451 ^ _233007) ^ [_247767] : [ssList(_247767), 454 ^ _233007 : [(489 ^ _233007) ^ [] : [491 ^ _233007 : [(492 ^ _233007) ^ [] : [-(ssItem(490 ^ [_247767]))], (495 ^ _233007) ^ [] : [-(ssItem(493 ^ [_247767]))], (498 ^ _233007) ^ [] : [-(ssList(496 ^ [_247767]))], (501 ^ _233007) ^ [] : [-(ssList(499 ^ [_247767]))], (504 ^ _233007) ^ [] : [-(ssList(502 ^ [_247767]))], (506 ^ _233007) ^ [] : [-(app(app(496 ^ [_247767], cons(490 ^ [_247767], 499 ^ [_247767])), cons(493 ^ [_247767], 502 ^ [_247767])) = _247767)], (508 ^ _233007) ^ [] : [-(leq(490 ^ [_247767], 493 ^ [_247767]))], (510 ^ _233007) ^ [] : [-(leq(493 ^ [_247767], 490 ^ [_247767]))]], -(cyclefreeP(_247767))], (455 ^ _233007) ^ [] : [cyclefreeP(_247767), 458 ^ _233007 : [(459 ^ _233007) ^ [_248071] : [ssItem(_248071), 462 ^ _233007 : [(463 ^ _233007) ^ [_248263] : [ssItem(_248263), 466 ^ _233007 : [(467 ^ _233007) ^ [_248451] : [ssList(_248451), 470 ^ _233007 : [(471 ^ _233007) ^ [_248635] : [ssList(_248635), 474 ^ _233007 : [(475 ^ _233007) ^ [_248815] : [ssList(_248815), app(app(_248451, cons(_248071, _248635)), cons(_248263, _248815)) = _247767, leq(_248071, _248263), leq(_248263, _248071)]]]]]]]]]]]]], (514 ^ _233007) ^ [_250553] : [ssList(_250553), 517 ^ _233007 : [(552 ^ _233007) ^ [] : [554 ^ _233007 : [(555 ^ _233007) ^ [] : [-(ssItem(553 ^ [_250553]))], (558 ^ _233007) ^ [] : [-(ssItem(556 ^ [_250553]))], (561 ^ _233007) ^ [] : [-(ssList(559 ^ [_250553]))], (564 ^ _233007) ^ [] : [-(ssList(562 ^ [_250553]))], (567 ^ _233007) ^ [] : [-(ssList(565 ^ [_250553]))], (569 ^ _233007) ^ [] : [-(app(app(559 ^ [_250553], cons(553 ^ [_250553], 562 ^ [_250553])), cons(556 ^ [_250553], 565 ^ [_250553])) = _250553)], (571 ^ _233007) ^ [] : [leq(553 ^ [_250553], 556 ^ [_250553])], (573 ^ _233007) ^ [] : [leq(556 ^ [_250553], 553 ^ [_250553])]], -(totalorderP(_250553))], (518 ^ _233007) ^ [] : [totalorderP(_250553), 521 ^ _233007 : [(522 ^ _233007) ^ [_250855] : [ssItem(_250855), 525 ^ _233007 : [(526 ^ _233007) ^ [_251045] : [ssItem(_251045), 529 ^ _233007 : [(530 ^ _233007) ^ [_251231] : [ssList(_251231), 533 ^ _233007 : [(534 ^ _233007) ^ [_251413] : [ssList(_251413), 537 ^ _233007 : [(538 ^ _233007) ^ [_251591] : [ssList(_251591), app(app(_251231, cons(_250855, _251413)), cons(_251045, _251591)) = _250553, -(leq(_250855, _251045)), -(leq(_251045, _250855))]]]]]]]]]]]]], (577 ^ _233007) ^ [_253317] : [ssList(_253317), 580 ^ _233007 : [(615 ^ _233007) ^ [] : [617 ^ _233007 : [(618 ^ _233007) ^ [] : [-(ssItem(616 ^ [_253317]))], (621 ^ _233007) ^ [] : [-(ssItem(619 ^ [_253317]))], (624 ^ _233007) ^ [] : [-(ssList(622 ^ [_253317]))], (627 ^ _233007) ^ [] : [-(ssList(625 ^ [_253317]))], (630 ^ _233007) ^ [] : [-(ssList(628 ^ [_253317]))], (632 ^ _233007) ^ [] : [-(app(app(622 ^ [_253317], cons(616 ^ [_253317], 625 ^ [_253317])), cons(619 ^ [_253317], 628 ^ [_253317])) = _253317)], (634 ^ _233007) ^ [] : [lt(616 ^ [_253317], 619 ^ [_253317])], (636 ^ _233007) ^ [] : [lt(619 ^ [_253317], 616 ^ [_253317])]], -(strictorderP(_253317))], (581 ^ _233007) ^ [] : [strictorderP(_253317), 584 ^ _233007 : [(585 ^ _233007) ^ [_253619] : [ssItem(_253619), 588 ^ _233007 : [(589 ^ _233007) ^ [_253809] : [ssItem(_253809), 592 ^ _233007 : [(593 ^ _233007) ^ [_253995] : [ssList(_253995), 596 ^ _233007 : [(597 ^ _233007) ^ [_254177] : [ssList(_254177), 600 ^ _233007 : [(601 ^ _233007) ^ [_254355] : [ssList(_254355), app(app(_253995, cons(_253619, _254177)), cons(_253809, _254355)) = _253317, -(lt(_253619, _253809)), -(lt(_253809, _253619))]]]]]]]]]]]]], (640 ^ _233007) ^ [_256081] : [ssList(_256081), 643 ^ _233007 : [(674 ^ _233007) ^ [] : [676 ^ _233007 : [(677 ^ _233007) ^ [] : [-(ssItem(675 ^ [_256081]))], (680 ^ _233007) ^ [] : [-(ssItem(678 ^ [_256081]))], (683 ^ _233007) ^ [] : [-(ssList(681 ^ [_256081]))], (686 ^ _233007) ^ [] : [-(ssList(684 ^ [_256081]))], (689 ^ _233007) ^ [] : [-(ssList(687 ^ [_256081]))], (691 ^ _233007) ^ [] : [-(app(app(681 ^ [_256081], cons(675 ^ [_256081], 684 ^ [_256081])), cons(678 ^ [_256081], 687 ^ [_256081])) = _256081)], (693 ^ _233007) ^ [] : [leq(675 ^ [_256081], 678 ^ [_256081])]], -(totalorderedP(_256081))], (644 ^ _233007) ^ [] : [totalorderedP(_256081), 647 ^ _233007 : [(648 ^ _233007) ^ [_256377] : [ssItem(_256377), 651 ^ _233007 : [(652 ^ _233007) ^ [_256561] : [ssItem(_256561), 655 ^ _233007 : [(656 ^ _233007) ^ [_256741] : [ssList(_256741), 659 ^ _233007 : [(660 ^ _233007) ^ [_256917] : [ssList(_256917), 663 ^ _233007 : [(664 ^ _233007) ^ [_257089] : [ssList(_257089), app(app(_256741, cons(_256377, _256917)), cons(_256561, _257089)) = _256081, -(leq(_256377, _256561))]]]]]]]]]]]]], (697 ^ _233007) ^ [_258569] : [ssList(_258569), 700 ^ _233007 : [(731 ^ _233007) ^ [] : [733 ^ _233007 : [(734 ^ _233007) ^ [] : [-(ssItem(732 ^ [_258569]))], (737 ^ _233007) ^ [] : [-(ssItem(735 ^ [_258569]))], (740 ^ _233007) ^ [] : [-(ssList(738 ^ [_258569]))], (743 ^ _233007) ^ [] : [-(ssList(741 ^ [_258569]))], (746 ^ _233007) ^ [] : [-(ssList(744 ^ [_258569]))], (748 ^ _233007) ^ [] : [-(app(app(738 ^ [_258569], cons(732 ^ [_258569], 741 ^ [_258569])), cons(735 ^ [_258569], 744 ^ [_258569])) = _258569)], (750 ^ _233007) ^ [] : [lt(732 ^ [_258569], 735 ^ [_258569])]], -(strictorderedP(_258569))], (701 ^ _233007) ^ [] : [strictorderedP(_258569), 704 ^ _233007 : [(705 ^ _233007) ^ [_258865] : [ssItem(_258865), 708 ^ _233007 : [(709 ^ _233007) ^ [_259049] : [ssItem(_259049), 712 ^ _233007 : [(713 ^ _233007) ^ [_259229] : [ssList(_259229), 716 ^ _233007 : [(717 ^ _233007) ^ [_259405] : [ssList(_259405), 720 ^ _233007 : [(721 ^ _233007) ^ [_259577] : [ssList(_259577), app(app(_259229, cons(_258865, _259405)), cons(_259049, _259577)) = _258569, -(lt(_258865, _259049))]]]]]]]]]]]]], (754 ^ _233007) ^ [_261057] : [ssList(_261057), 757 ^ _233007 : [(788 ^ _233007) ^ [] : [790 ^ _233007 : [(791 ^ _233007) ^ [] : [-(ssItem(789 ^ [_261057]))], (794 ^ _233007) ^ [] : [-(ssItem(792 ^ [_261057]))], (797 ^ _233007) ^ [] : [-(ssList(795 ^ [_261057]))], (800 ^ _233007) ^ [] : [-(ssList(798 ^ [_261057]))], (803 ^ _233007) ^ [] : [-(ssList(801 ^ [_261057]))], (805 ^ _233007) ^ [] : [-(app(app(795 ^ [_261057], cons(789 ^ [_261057], 798 ^ [_261057])), cons(792 ^ [_261057], 801 ^ [_261057])) = _261057)], (807 ^ _233007) ^ [] : [-(789 ^ [_261057] = 792 ^ [_261057])]], -(duplicatefreeP(_261057))], (758 ^ _233007) ^ [] : [duplicatefreeP(_261057), 761 ^ _233007 : [(762 ^ _233007) ^ [_261355] : [ssItem(_261355), 765 ^ _233007 : [(766 ^ _233007) ^ [_261541] : [ssItem(_261541), 769 ^ _233007 : [(770 ^ _233007) ^ [_261723] : [ssList(_261723), 773 ^ _233007 : [(774 ^ _233007) ^ [_261901] : [ssList(_261901), 777 ^ _233007 : [(778 ^ _233007) ^ [_262075] : [ssList(_262075), app(app(_261723, cons(_261355, _261901)), cons(_261541, _262075)) = _261057, _261355 = _261541]]]]]]]]]]]]], (811 ^ _233007) ^ [_263567] : [ssList(_263567), 814 ^ _233007 : [(841 ^ _233007) ^ [] : [843 ^ _233007 : [(844 ^ _233007) ^ [] : [-(ssItem(842 ^ [_263567]))], (847 ^ _233007) ^ [] : [-(ssItem(845 ^ [_263567]))], (850 ^ _233007) ^ [] : [-(ssList(848 ^ [_263567]))], (853 ^ _233007) ^ [] : [-(ssList(851 ^ [_263567]))], (855 ^ _233007) ^ [] : [-(app(848 ^ [_263567], cons(842 ^ [_263567], cons(845 ^ [_263567], 851 ^ [_263567]))) = _263567)], (857 ^ _233007) ^ [] : [842 ^ [_263567] = 845 ^ [_263567]]], -(equalelemsP(_263567))], (815 ^ _233007) ^ [] : [equalelemsP(_263567), 818 ^ _233007 : [(819 ^ _233007) ^ [_263850] : [ssItem(_263850), 822 ^ _233007 : [(823 ^ _233007) ^ [_264021] : [ssItem(_264021), 826 ^ _233007 : [(827 ^ _233007) ^ [_264188] : [ssList(_264188), 830 ^ _233007 : [(831 ^ _233007) ^ [_264351] : [ssList(_264351), app(_264188, cons(_263850, cons(_264021, _264351))) = _263567, -(_263850 = _264021)]]]]]]]]]]], (861 ^ _233007) ^ [_265584] : [ssList(_265584), 864 ^ _233007 : [(865 ^ _233007) ^ [_265722] : [ssList(_265722), 868 ^ _233007 : [(869 ^ _233007) ^ [] : [neq(_265584, _265722), _265584 = _265722], (875 ^ _233007) ^ [] : [-(_265584 = _265722), -(neq(_265584, _265722))]]]]], (881 ^ _233007) ^ [_266175] : [ssList(_266175), 884 ^ _233007 : [(885 ^ _233007) ^ [_266307] : [ssItem(_266307), -(ssList(cons(_266307, _266175)))]]], (891 ^ _233007) ^ [] : [-(ssList(nil))], (893 ^ _233007) ^ [_266565] : [ssList(_266565), 896 ^ _233007 : [(897 ^ _233007) ^ [_266700] : [ssItem(_266700), cons(_266700, _266565) = _266565]]], (903 ^ _233007) ^ [_266908] : [ssList(_266908), 906 ^ _233007 : [(907 ^ _233007) ^ [_267076] : [ssList(_267076), 910 ^ _233007 : [(911 ^ _233007) ^ [_267240] : [ssItem(_267240), 914 ^ _233007 : [(915 ^ _233007) ^ [_267400] : [ssItem(_267400), cons(_267240, _266908) = cons(_267400, _267076), 922 ^ _233007 : [(923 ^ _233007) ^ [] : [-(_267240 = _267400)], (925 ^ _233007) ^ [] : [-(_267076 = _266908)]]]]]]]]], (927 ^ _233007) ^ [_267815] : [ssList(_267815), -(nil = _267815), 935 ^ _233007 : [(936 ^ _233007) ^ [] : [-(ssList(934 ^ [_267815]))], (939 ^ _233007) ^ [] : [-(ssItem(937 ^ [_267815]))], (941 ^ _233007) ^ [] : [-(cons(937 ^ [_267815], 934 ^ [_267815]) = _267815)]]], (943 ^ _233007) ^ [_268379] : [ssList(_268379), 946 ^ _233007 : [(947 ^ _233007) ^ [_268514] : [ssItem(_268514), nil = cons(_268514, _268379)]]], (953 ^ _233007) ^ [_268722] : [ssList(_268722), -(nil = _268722), -(ssItem(hd(_268722)))], (963 ^ _233007) ^ [_269000] : [ssList(_269000), 966 ^ _233007 : [(967 ^ _233007) ^ [_269135] : [ssItem(_269135), -(hd(cons(_269135, _269000)) = _269135)]]], (973 ^ _233007) ^ [_269346] : [ssList(_269346), -(nil = _269346), -(ssList(tl(_269346)))], (983 ^ _233007) ^ [_269624] : [ssList(_269624), 986 ^ _233007 : [(987 ^ _233007) ^ [_269759] : [ssItem(_269759), -(tl(cons(_269759, _269624)) = _269624)]]], (993 ^ _233007) ^ [_269970] : [ssList(_269970), 996 ^ _233007 : [(997 ^ _233007) ^ [_270102] : [ssList(_270102), -(ssList(app(_269970, _270102)))]]], (1003 ^ _233007) ^ [_270307] : [ssList(_270307), 1006 ^ _233007 : [(1007 ^ _233007) ^ [_270459] : [ssList(_270459), 1010 ^ _233007 : [(1011 ^ _233007) ^ [_270607] : [ssItem(_270607), -(cons(_270607, app(_270459, _270307)) = app(cons(_270607, _270459), _270307))]]]]], (1017 ^ _233007) ^ [_270845] : [ssList(_270845), -(app(nil, _270845) = _270845)], (1023 ^ _233007) ^ [_271039] : [ssItem(_271039), 1026 ^ _233007 : [(1027 ^ _233007) ^ [_271181] : [ssItem(_271181), -(_271039 = _271181), leq(_271039, _271181), leq(_271181, _271039)]]], (1041 ^ _233007) ^ [_271560] : [ssItem(_271560), 1044 ^ _233007 : [(1045 ^ _233007) ^ [_271712] : [ssItem(_271712), 1048 ^ _233007 : [(1049 ^ _233007) ^ [_271860] : [ssItem(_271860), -(leq(_271560, _271860)), leq(_271560, _271712), leq(_271712, _271860)]]]]], (1063 ^ _233007) ^ [_272260] : [ssItem(_272260), -(leq(_272260, _272260))], (1069 ^ _233007) ^ [_272448] : [ssItem(_272448), 1072 ^ _233007 : [(1073 ^ _233007) ^ [_272584] : [ssItem(_272584), 1076 ^ _233007 : [(1077 ^ _233007) ^ [] : [geq(_272448, _272584), -(leq(_272584, _272448))], (1083 ^ _233007) ^ [] : [leq(_272584, _272448), -(geq(_272448, _272584))]]]]], (1089 ^ _233007) ^ [_273035] : [ssItem(_273035), 1092 ^ _233007 : [(1093 ^ _233007) ^ [_273173] : [ssItem(_273173), lt(_273035, _273173), lt(_273173, _273035)]]], (1103 ^ _233007) ^ [_273464] : [ssItem(_273464), 1106 ^ _233007 : [(1107 ^ _233007) ^ [_273616] : [ssItem(_273616), 1110 ^ _233007 : [(1111 ^ _233007) ^ [_273764] : [ssItem(_273764), -(lt(_273464, _273764)), lt(_273464, _273616), lt(_273616, _273764)]]]]], (1125 ^ _233007) ^ [_274164] : [ssItem(_274164), 1128 ^ _233007 : [(1129 ^ _233007) ^ [_274300] : [ssItem(_274300), 1132 ^ _233007 : [(1133 ^ _233007) ^ [] : [gt(_274164, _274300), -(lt(_274300, _274164))], (1139 ^ _233007) ^ [] : [lt(_274300, _274164), -(gt(_274164, _274300))]]]]], (1145 ^ _233007) ^ [_274751] : [ssItem(_274751), 1148 ^ _233007 : [(1149 ^ _233007) ^ [_274906] : [ssList(_274906), 1152 ^ _233007 : [(1153 ^ _233007) ^ [_275057] : [ssList(_275057), 1156 ^ _233007 : [(1167 ^ _233007) ^ [] : [1168 ^ _233007 : [(1169 ^ _233007) ^ [] : [memberP(_274906, _274751)], (1171 ^ _233007) ^ [] : [memberP(_275057, _274751)]], -(memberP(app(_274906, _275057), _274751))], (1157 ^ _233007) ^ [] : [memberP(app(_274906, _275057), _274751), -(memberP(_274906, _274751)), -(memberP(_275057, _274751))]]]]]]], (1175 ^ _233007) ^ [_275704] : [ssItem(_275704), 1178 ^ _233007 : [(1179 ^ _233007) ^ [_275859] : [ssItem(_275859), 1182 ^ _233007 : [(1183 ^ _233007) ^ [_276010] : [ssList(_276010), 1186 ^ _233007 : [(1197 ^ _233007) ^ [] : [1198 ^ _233007 : [(1199 ^ _233007) ^ [] : [_275704 = _275859], (1201 ^ _233007) ^ [] : [memberP(_276010, _275704)]], -(memberP(cons(_275859, _276010), _275704))], (1187 ^ _233007) ^ [] : [memberP(cons(_275859, _276010), _275704), -(_275704 = _275859), -(memberP(_276010, _275704))]]]]]]], (1205 ^ _233007) ^ [_276657] : [ssItem(_276657), memberP(nil, _276657)], (1211 ^ _233007) ^ [] : [singletonP(nil)], (1213 ^ _233007) ^ [_276898] : [ssList(_276898), 1216 ^ _233007 : [(1217 ^ _233007) ^ [_277050] : [ssList(_277050), 1220 ^ _233007 : [(1221 ^ _233007) ^ [_277198] : [ssList(_277198), -(frontsegP(_276898, _277198)), frontsegP(_276898, _277050), frontsegP(_277050, _277198)]]]]], (1235 ^ _233007) ^ [_277598] : [ssList(_277598), 1238 ^ _233007 : [(1239 ^ _233007) ^ [_277740] : [ssList(_277740), -(_277598 = _277740), frontsegP(_277598, _277740), frontsegP(_277740, _277598)]]], (1253 ^ _233007) ^ [_278119] : [ssList(_278119), -(frontsegP(_278119, _278119))], (1259 ^ _233007) ^ [_278307] : [ssList(_278307), 1262 ^ _233007 : [(1263 ^ _233007) ^ [_278456] : [ssList(_278456), 1266 ^ _233007 : [(1267 ^ _233007) ^ [_278601] : [ssList(_278601), frontsegP(_278307, _278456), -(frontsegP(app(_278307, _278601), _278456))]]]]], (1277 ^ _233007) ^ [_278914] : [ssItem(_278914), 1280 ^ _233007 : [(1281 ^ _233007) ^ [_279082] : [ssItem(_279082), 1284 ^ _233007 : [(1285 ^ _233007) ^ [_279246] : [ssList(_279246), 1288 ^ _233007 : [(1289 ^ _233007) ^ [_279406] : [ssList(_279406), 1292 ^ _233007 : [(1293 ^ _233007) ^ [] : [frontsegP(cons(_278914, _279246), cons(_279082, _279406)), 1296 ^ _233007 : [(1297 ^ _233007) ^ [] : [-(_278914 = _279082)], (1299 ^ _233007) ^ [] : [-(frontsegP(_279246, _279406))]]], (1301 ^ _233007) ^ [] : [-(frontsegP(cons(_278914, _279246), cons(_279082, _279406))), _278914 = _279082, frontsegP(_279246, _279406)]]]]]]]]], (1311 ^ _233007) ^ [_280091] : [ssList(_280091), -(frontsegP(_280091, nil))], (1317 ^ _233007) ^ [_280279] : [ssList(_280279), 1320 ^ _233007 : [(1321 ^ _233007) ^ [] : [frontsegP(nil, _280279), -(nil = _280279)], (1327 ^ _233007) ^ [] : [nil = _280279, -(frontsegP(nil, _280279))]]], (1333 ^ _233007) ^ [_280707] : [ssList(_280707), 1336 ^ _233007 : [(1337 ^ _233007) ^ [_280859] : [ssList(_280859), 1340 ^ _233007 : [(1341 ^ _233007) ^ [_281007] : [ssList(_281007), -(rearsegP(_280707, _281007)), rearsegP(_280707, _280859), rearsegP(_280859, _281007)]]]]], (1355 ^ _233007) ^ [_281407] : [ssList(_281407), 1358 ^ _233007 : [(1359 ^ _233007) ^ [_281549] : [ssList(_281549), -(_281407 = _281549), rearsegP(_281407, _281549), rearsegP(_281549, _281407)]]], (1373 ^ _233007) ^ [_281928] : [ssList(_281928), -(rearsegP(_281928, _281928))], (1379 ^ _233007) ^ [_282116] : [ssList(_282116), 1382 ^ _233007 : [(1383 ^ _233007) ^ [_282265] : [ssList(_282265), 1386 ^ _233007 : [(1387 ^ _233007) ^ [_282410] : [ssList(_282410), rearsegP(_282116, _282265), -(rearsegP(app(_282410, _282116), _282265))]]]]], (1397 ^ _233007) ^ [_282723] : [ssList(_282723), -(rearsegP(_282723, nil))], (1403 ^ _233007) ^ [_282911] : [ssList(_282911), 1406 ^ _233007 : [(1407 ^ _233007) ^ [] : [rearsegP(nil, _282911), -(nil = _282911)], (1413 ^ _233007) ^ [] : [nil = _282911, -(rearsegP(nil, _282911))]]], (1419 ^ _233007) ^ [_283339] : [ssList(_283339), 1422 ^ _233007 : [(1423 ^ _233007) ^ [_283491] : [ssList(_283491), 1426 ^ _233007 : [(1427 ^ _233007) ^ [_283639] : [ssList(_283639), -(segmentP(_283339, _283639)), segmentP(_283339, _283491), segmentP(_283491, _283639)]]]]], (1441 ^ _233007) ^ [_284039] : [ssList(_284039), 1444 ^ _233007 : [(1445 ^ _233007) ^ [_284181] : [ssList(_284181), -(_284039 = _284181), segmentP(_284039, _284181), segmentP(_284181, _284039)]]], (1459 ^ _233007) ^ [_284560] : [ssList(_284560), -(segmentP(_284560, _284560))], (1465 ^ _233007) ^ [_284748] : [ssList(_284748), 1468 ^ _233007 : [(1469 ^ _233007) ^ [_284910] : [ssList(_284910), 1472 ^ _233007 : [(1473 ^ _233007) ^ [_285068] : [ssList(_285068), 1476 ^ _233007 : [(1477 ^ _233007) ^ [_285222] : [ssList(_285222), segmentP(_284748, _284910), -(segmentP(app(app(_285068, _284748), _285222), _284910))]]]]]]], (1487 ^ _233007) ^ [_285558] : [ssList(_285558), -(segmentP(_285558, nil))], (1493 ^ _233007) ^ [_285746] : [ssList(_285746), 1496 ^ _233007 : [(1497 ^ _233007) ^ [] : [segmentP(nil, _285746), -(nil = _285746)], (1503 ^ _233007) ^ [] : [nil = _285746, -(segmentP(nil, _285746))]]], (1509 ^ _233007) ^ [_286174] : [ssItem(_286174), -(cyclefreeP(cons(_286174, nil)))], (1515 ^ _233007) ^ [] : [-(cyclefreeP(nil))], (1517 ^ _233007) ^ [_286419] : [ssItem(_286419), -(totalorderP(cons(_286419, nil)))], (1523 ^ _233007) ^ [] : [-(totalorderP(nil))], (1525 ^ _233007) ^ [_286664] : [ssItem(_286664), -(strictorderP(cons(_286664, nil)))], (1531 ^ _233007) ^ [] : [-(strictorderP(nil))], (1533 ^ _233007) ^ [_286909] : [ssItem(_286909), -(totalorderedP(cons(_286909, nil)))], (1539 ^ _233007) ^ [] : [-(totalorderedP(nil))], (1541 ^ _233007) ^ [_287154] : [ssItem(_287154), 1544 ^ _233007 : [(1545 ^ _233007) ^ [_287313] : [ssList(_287313), 1548 ^ _233007 : [(1549 ^ _233007) ^ [] : [totalorderedP(cons(_287154, _287313)), -(nil = _287313), 1556 ^ _233007 : [(1557 ^ _233007) ^ [] : [nil = _287313], (1559 ^ _233007) ^ [] : [-(totalorderedP(_287313))], (1561 ^ _233007) ^ [] : [-(leq(_287154, hd(_287313)))]]], (1563 ^ _233007) ^ [] : [-(totalorderedP(cons(_287154, _287313))), 1564 ^ _233007 : [(1565 ^ _233007) ^ [] : [nil = _287313], (1567 ^ _233007) ^ [] : [-(nil = _287313), totalorderedP(_287313), leq(_287154, hd(_287313))]]]]]]], (1579 ^ _233007) ^ [_288248] : [ssItem(_288248), -(strictorderedP(cons(_288248, nil)))], (1585 ^ _233007) ^ [] : [-(strictorderedP(nil))], (1587 ^ _233007) ^ [_288493] : [ssItem(_288493), 1590 ^ _233007 : [(1591 ^ _233007) ^ [_288652] : [ssList(_288652), 1594 ^ _233007 : [(1595 ^ _233007) ^ [] : [strictorderedP(cons(_288493, _288652)), -(nil = _288652), 1602 ^ _233007 : [(1603 ^ _233007) ^ [] : [nil = _288652], (1605 ^ _233007) ^ [] : [-(strictorderedP(_288652))], (1607 ^ _233007) ^ [] : [-(lt(_288493, hd(_288652)))]]], (1609 ^ _233007) ^ [] : [-(strictorderedP(cons(_288493, _288652))), 1610 ^ _233007 : [(1611 ^ _233007) ^ [] : [nil = _288652], (1613 ^ _233007) ^ [] : [-(nil = _288652), strictorderedP(_288652), lt(_288493, hd(_288652))]]]]]]], (1625 ^ _233007) ^ [_289587] : [ssItem(_289587), -(duplicatefreeP(cons(_289587, nil)))], (1631 ^ _233007) ^ [] : [-(duplicatefreeP(nil))], (1633 ^ _233007) ^ [_289832] : [ssItem(_289832), -(equalelemsP(cons(_289832, nil)))], (1639 ^ _233007) ^ [] : [-(equalelemsP(nil))], (1641 ^ _233007) ^ [_290077] : [ssList(_290077), -(nil = _290077), 1649 ^ _233007 : [(1650 ^ _233007) ^ [] : [-(ssItem(1648 ^ [_290077]))], (1652 ^ _233007) ^ [] : [-(hd(_290077) = 1648 ^ [_290077])]]], (1654 ^ _233007) ^ [_290491] : [ssList(_290491), -(nil = _290491), 1662 ^ _233007 : [(1663 ^ _233007) ^ [] : [-(ssList(1661 ^ [_290491]))], (1665 ^ _233007) ^ [] : [-(tl(_290491) = 1661 ^ [_290491])]]], (1667 ^ _233007) ^ [_290905] : [ssList(_290905), 1670 ^ _233007 : [(1671 ^ _233007) ^ [_291071] : [ssList(_291071), -(_291071 = _290905), -(nil = _291071), -(nil = _290905), hd(_291071) = hd(_290905), tl(_291071) = tl(_290905)]]], (1693 ^ _233007) ^ [_291650] : [ssList(_291650), -(nil = _291650), -(cons(hd(_291650), tl(_291650)) = _291650)], (1703 ^ _233007) ^ [_291940] : [ssList(_291940), 1706 ^ _233007 : [(1707 ^ _233007) ^ [_292092] : [ssList(_292092), 1710 ^ _233007 : [(1711 ^ _233007) ^ [_292240] : [ssList(_292240), app(_292240, _292092) = app(_291940, _292092), -(_292240 = _291940)]]]]], (1721 ^ _233007) ^ [_292559] : [ssList(_292559), 1724 ^ _233007 : [(1725 ^ _233007) ^ [_292711] : [ssList(_292711), 1728 ^ _233007 : [(1729 ^ _233007) ^ [_292859] : [ssList(_292859), app(_292711, _292859) = app(_292711, _292559), -(_292859 = _292559)]]]]], (1739 ^ _233007) ^ [_293178] : [ssList(_293178), 1742 ^ _233007 : [(1743 ^ _233007) ^ [_293317] : [ssItem(_293317), -(cons(_293317, _293178) = app(cons(_293317, nil), _293178))]]], (1749 ^ _233007) ^ [_293536] : [ssList(_293536), 1752 ^ _233007 : [(1753 ^ _233007) ^ [_293688] : [ssList(_293688), 1756 ^ _233007 : [(1757 ^ _233007) ^ [_293836] : [ssList(_293836), -(app(app(_293536, _293688), _293836) = app(_293536, app(_293688, _293836)))]]]]], (1763 ^ _233007) ^ [_294074] : [ssList(_294074), 1766 ^ _233007 : [(1767 ^ _233007) ^ [_294219] : [ssList(_294219), 1770 ^ _233007 : [(1771 ^ _233007) ^ [] : [nil = app(_294074, _294219), 1774 ^ _233007 : [(1775 ^ _233007) ^ [] : [-(nil = _294219)], (1777 ^ _233007) ^ [] : [-(nil = _294074)]]], (1779 ^ _233007) ^ [] : [-(nil = app(_294074, _294219)), nil = _294219, nil = _294074]]]]], (1789 ^ _233007) ^ [_294837] : [ssList(_294837), -(app(_294837, nil) = _294837)], (1795 ^ _233007) ^ [_295031] : [ssList(_295031), 1798 ^ _233007 : [(1799 ^ _233007) ^ [_295176] : [ssList(_295176), -(nil = _295031), -(hd(app(_295031, _295176)) = hd(_295031))]]], (1809 ^ _233007) ^ [_295483] : [ssList(_295483), 1812 ^ _233007 : [(1813 ^ _233007) ^ [_295631] : [ssList(_295631), -(nil = _295483), -(tl(app(_295483, _295631)) = app(tl(_295483), _295631))]]], (1823 ^ _233007) ^ [_295944] : [ssItem(_295944), 1826 ^ _233007 : [(1827 ^ _233007) ^ [_296086] : [ssItem(_296086), -(_295944 = _296086), geq(_295944, _296086), geq(_296086, _295944)]]], (1841 ^ _233007) ^ [_296465] : [ssItem(_296465), 1844 ^ _233007 : [(1845 ^ _233007) ^ [_296617] : [ssItem(_296617), 1848 ^ _233007 : [(1849 ^ _233007) ^ [_296765] : [ssItem(_296765), -(geq(_296465, _296765)), geq(_296465, _296617), geq(_296617, _296765)]]]]], (1863 ^ _233007) ^ [_297165] : [ssItem(_297165), -(geq(_297165, _297165))], (1869 ^ _233007) ^ [_297353] : [ssItem(_297353), lt(_297353, _297353)], (1875 ^ _233007) ^ [_297542] : [ssItem(_297542), 1878 ^ _233007 : [(1879 ^ _233007) ^ [_297694] : [ssItem(_297694), 1882 ^ _233007 : [(1883 ^ _233007) ^ [_297842] : [ssItem(_297842), -(lt(_297542, _297842)), leq(_297542, _297694), lt(_297694, _297842)]]]]], (1897 ^ _233007) ^ [_298242] : [ssItem(_298242), 1900 ^ _233007 : [(1901 ^ _233007) ^ [_298384] : [ssItem(_298384), leq(_298242, _298384), -(_298242 = _298384), -(lt(_298242, _298384))]]], (1915 ^ _233007) ^ [_298764] : [ssItem(_298764), 1918 ^ _233007 : [(1919 ^ _233007) ^ [_298908] : [ssItem(_298908), 1922 ^ _233007 : [(1923 ^ _233007) ^ [] : [lt(_298764, _298908), 1926 ^ _233007 : [(1927 ^ _233007) ^ [] : [_298764 = _298908], (1929 ^ _233007) ^ [] : [-(leq(_298764, _298908))]]], (1931 ^ _233007) ^ [] : [-(lt(_298764, _298908)), -(_298764 = _298908), leq(_298764, _298908)]]]]], (1941 ^ _233007) ^ [_299519] : [ssItem(_299519), 1944 ^ _233007 : [(1945 ^ _233007) ^ [_299657] : [ssItem(_299657), gt(_299519, _299657), gt(_299657, _299519)]]], (1955 ^ _233007) ^ [_299928] : [ssItem(_299928), 1958 ^ _233007 : [(1959 ^ _233007) ^ [_300080] : [ssItem(_300080), 1962 ^ _233007 : [(1963 ^ _233007) ^ [_300228] : [ssItem(_300228), -(gt(_299928, _300228)), gt(_299928, _300080), gt(_300080, _300228)]]]]]], input).
% 139.48/134.92 ncf('1',plain,[frontsegP(1979 ^ [], 1976 ^ [])],start(1993 ^ 0)).
% 139.48/134.92 ncf('1.1',plain,[-(frontsegP(1979 ^ [], 1976 ^ [])), frontsegP(1985 ^ [], 1982 ^ []), 1985 ^ [] = 1979 ^ [], 1982 ^ [] = 1976 ^ []],extension(232 ^ 1,bind([[_240285, _240287, _240289, _240291], [1976 ^ [], 1982 ^ [], 1979 ^ [], 1985 ^ []]]))).
% 139.48/134.92 ncf('1.1.1',plain,[-(frontsegP(1985 ^ [], 1982 ^ [])), neq(1985 ^ [], nil)],extension(2001 ^ 2)).
% 139.48/134.92 ncf('1.1.1.1',plain,[-(neq(1985 ^ [], nil)), 875 : -(1985 ^ [] = nil), 875 : ssList(nil), 865 : ssList(1985 ^ [])],extension(861 ^ 3,bind([[_265584, _265722], [1985 ^ [], nil]]))).
% 139.48/134.92 ncf('1.1.1.1.1',plain,[1985 ^ [] = nil, -(nil = 1985 ^ [])],extension(4 ^ 8,bind([[_233258, _233260], [nil, 1985 ^ []]]))).
% 139.48/134.92 ncf('1.1.1.1.1.1',plain,[nil = 1985 ^ [], -(frontsegP(1985 ^ [], 1982 ^ [])), frontsegP(nil, nil), nil = 1982 ^ []],extension(232 ^ 9,bind([[_240285, _240287, _240289, _240291], [1982 ^ [], nil, 1985 ^ [], nil]]))).
% 139.48/134.92 ncf('1.1.1.1.1.1.1',plain,[frontsegP(1985 ^ [], 1982 ^ [])],reduction('1.1')).
% 139.48/134.92 ncf('1.1.1.1.1.1.2',plain,[-(frontsegP(nil, nil)), ssList(nil)],extension(1253 ^ 10,bind([[_278119], [nil]]))).
% 139.48/134.92 ncf('1.1.1.1.1.1.2.1',plain,[-(ssList(nil))],extension(891 ^ 11)).
% 139.48/134.92 ncf('1.1.1.1.1.1.3',plain,[-(nil = 1982 ^ []), nil = 1985 ^ []],extension(1995 ^ 10)).
% 139.48/134.92 ncf('1.1.1.1.1.1.3.1',plain,[-(nil = 1985 ^ [])],reduction('1.1.1.1.1')).
% 139.48/134.92 ncf('1.1.1.1.2',plain,[-(ssList(nil))],extension(891 ^ 6)).
% 139.48/134.92 ncf('1.1.1.1.3',plain,[-(ssList(1985 ^ []))],extension(1987 ^ 4)).
% 139.48/134.92 ncf('1.1.2',plain,[-(1985 ^ [] = 1979 ^ []), 1979 ^ [] = 1985 ^ []],extension(4 ^ 2,bind([[_233258, _233260], [1985 ^ [], 1979 ^ []]]))).
% 139.48/134.92 ncf('1.1.2.1',plain,[-(1979 ^ [] = 1985 ^ [])],extension(1989 ^ 3)).
% 139.48/134.92 ncf('1.1.3',plain,[-(1982 ^ [] = 1976 ^ []), 1976 ^ [] = 1982 ^ []],extension(4 ^ 2,bind([[_233258, _233260], [1982 ^ [], 1976 ^ []]]))).
% 139.48/134.92 ncf('1.1.3.1',plain,[-(1976 ^ [] = 1982 ^ [])],extension(1991 ^ 3)).
% 139.48/134.92 %-----------------------------------------------------
% 139.48/134.92 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------