%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWC151+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n011.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:12:42 EDT 2023
% Result : Theorem 0.33s 1.37s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SWC151+1 : TPTP v8.1.2. Released v2.4.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n011.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 : Fri May 19 01:03:33 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.33/1.37
% 0.33/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.33/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.33/1.37 %-----------------------------------------------------
% 0.33/1.37 ncf(matrix, plain, [(1978 ^ _228672) ^ [] : [-(ssList(1976 ^ []))], (1981 ^ _228672) ^ [] : [-(ssList(1979 ^ []))], (1984 ^ _228672) ^ [] : [-(ssList(1982 ^ []))], (1987 ^ _228672) ^ [] : [-(ssList(1985 ^ []))], (1989 ^ _228672) ^ [] : [-(1979 ^ [] = 1985 ^ [])], (1991 ^ _228672) ^ [] : [-(1976 ^ [] = 1982 ^ [])], (1993 ^ _228672) ^ [] : [-(totalorderP(1979 ^ []))], (1995 ^ _228672) ^ [] : [totalorderP(1985 ^ [])], (246 ^ _228672) ^ [_236476, _236478, _236480, _236482] : [-(cons(_236482, _236478) = cons(_236480, _236476)), _236482 = _236480, _236478 = _236476], (256 ^ _228672) ^ [_236807, _236809] : [_236809 = _236807, -(hd(_236809) = hd(_236807))], (272 ^ _228672) ^ [_237364, _237366] : [_237366 = _237364, -(tl(_237366) = tl(_237364))], (262 ^ _228672) ^ [_237053, _237055, _237057, _237059] : [-(app(_237059, _237055) = app(_237057, _237053)), _237059 = _237057, _237055 = _237053], (2 ^ _228672) ^ [_228816] : [-(_228816 = _228816)], (4 ^ _228672) ^ [_228923, _228925] : [_228925 = _228923, -(_228923 = _228925)], (10 ^ _228672) ^ [_229127, _229129, _229131] : [-(_229131 = _229127), _229131 = _229129, _229129 = _229127], (20 ^ _228672) ^ [_229468, _229470, _229472, _229474] : [-(neq(_229472, _229468)), neq(_229474, _229470), _229474 = _229472, _229470 = _229468], (34 ^ _228672) ^ [_229912, _229914, _229916, _229918] : [-(memberP(_229916, _229912)), memberP(_229918, _229914), _229918 = _229916, _229914 = _229912], (48 ^ _228672) ^ [_230328, _230330] : [-(singletonP(_230328)), _230330 = _230328, singletonP(_230330)], (58 ^ _228672) ^ [_230651, _230653, _230655, _230657] : [-(frontsegP(_230655, _230651)), frontsegP(_230657, _230653), _230657 = _230655, _230653 = _230651], (72 ^ _228672) ^ [_231095, _231097, _231099, _231101] : [-(rearsegP(_231099, _231095)), rearsegP(_231101, _231097), _231101 = _231099, _231097 = _231095], (86 ^ _228672) ^ [_231539, _231541, _231543, _231545] : [-(segmentP(_231543, _231539)), segmentP(_231545, _231541), _231545 = _231543, _231541 = _231539], (100 ^ _228672) ^ [_231955, _231957] : [-(cyclefreeP(_231955)), _231957 = _231955, cyclefreeP(_231957)], (110 ^ _228672) ^ [_232250, _232252] : [-(strictorderP(_232250)), _232252 = _232250, strictorderP(_232252)], (120 ^ _228672) ^ [_232545, _232547] : [-(totalorderedP(_232545)), _232547 = _232545, totalorderedP(_232547)], (130 ^ _228672) ^ [_232840, _232842] : [-(strictorderedP(_232840)), _232842 = _232840, strictorderedP(_232842)], (140 ^ _228672) ^ [_233135, _233137] : [-(duplicatefreeP(_233135)), _233137 = _233135, duplicatefreeP(_233137)], (150 ^ _228672) ^ [_233430, _233432] : [-(equalelemsP(_233430)), _233432 = _233430, equalelemsP(_233432)], (160 ^ _228672) ^ [_233753, _233755, _233757, _233759] : [-(geq(_233757, _233753)), geq(_233759, _233755), _233759 = _233757, _233755 = _233753], (174 ^ _228672) ^ [_234197, _234199, _234201, _234203] : [-(lt(_234201, _234197)), lt(_234203, _234199), _234203 = _234201, _234199 = _234197], (188 ^ _228672) ^ [_234641, _234643, _234645, _234647] : [-(leq(_234645, _234641)), leq(_234647, _234643), _234647 = _234645, _234643 = _234641], (202 ^ _228672) ^ [_235057, _235059] : [-(ssItem(_235057)), _235059 = _235057, ssItem(_235059)], (212 ^ _228672) ^ [_235380, _235382, _235384, _235386] : [-(gt(_235384, _235380)), gt(_235386, _235382), _235386 = _235384, _235382 = _235380], (226 ^ _228672) ^ [_235796, _235798] : [-(ssList(_235796)), _235798 = _235796, ssList(_235798)], (236 ^ _228672) ^ [_236071, _236073] : [-(totalorderP(_236071)), _236073 = _236071, totalorderP(_236073)], (278 ^ _228672) ^ [_237586] : [ssItem(_237586), 281 ^ _228672 : [(282 ^ _228672) ^ [_237724] : [ssItem(_237724), 285 ^ _228672 : [(286 ^ _228672) ^ [] : [neq(_237586, _237724), _237586 = _237724], (292 ^ _228672) ^ [] : [-(_237586 = _237724), -(neq(_237586, _237724))]]]]], (299 ^ _228672) ^ [] : [-(ssItem(297 ^ []))], (302 ^ _228672) ^ [] : [-(ssItem(300 ^ []))], (304 ^ _228672) ^ [] : [297 ^ [] = 300 ^ []], (306 ^ _228672) ^ [_238437] : [ssList(_238437), 309 ^ _228672 : [(310 ^ _228672) ^ [_238599] : [ssItem(_238599), 313 ^ _228672 : [(314 ^ _228672) ^ [] : [memberP(_238437, _238599), 318 ^ _228672 : [(319 ^ _228672) ^ [] : [-(ssList(317 ^ [_238437, _238599]))], (322 ^ _228672) ^ [] : [-(ssList(320 ^ [_238437, _238599]))], (324 ^ _228672) ^ [] : [-(app(317 ^ [_238437, _238599], cons(_238599, 320 ^ [_238437, _238599])) = _238437)]]], (326 ^ _228672) ^ [] : [-(memberP(_238437, _238599)), 327 ^ _228672 : [(328 ^ _228672) ^ [_239247] : [ssList(_239247), 331 ^ _228672 : [(332 ^ _228672) ^ [_239395] : [ssList(_239395), app(_239247, cons(_238599, _239395)) = _238437]]]]]]]]], (340 ^ _228672) ^ [_239686] : [ssList(_239686), 343 ^ _228672 : [(344 ^ _228672) ^ [] : [singletonP(_239686), 348 ^ _228672 : [(349 ^ _228672) ^ [] : [-(ssItem(347 ^ [_239686]))], (351 ^ _228672) ^ [] : [-(cons(347 ^ [_239686], nil) = _239686)]]], (353 ^ _228672) ^ [] : [-(singletonP(_239686)), 354 ^ _228672 : [(355 ^ _228672) ^ [_240135] : [ssItem(_240135), cons(_240135, nil) = _239686]]]]], (363 ^ _228672) ^ [_240391] : [ssList(_240391), 366 ^ _228672 : [(367 ^ _228672) ^ [_240540] : [ssList(_240540), 370 ^ _228672 : [(371 ^ _228672) ^ [] : [frontsegP(_240391, _240540), 375 ^ _228672 : [(376 ^ _228672) ^ [] : [-(ssList(374 ^ [_240391, _240540]))], (378 ^ _228672) ^ [] : [-(app(_240540, 374 ^ [_240391, _240540]) = _240391)]]], (380 ^ _228672) ^ [] : [-(frontsegP(_240391, _240540)), 381 ^ _228672 : [(382 ^ _228672) ^ [_241015] : [ssList(_241015), app(_240540, _241015) = _240391]]]]]]], (390 ^ _228672) ^ [_241287] : [ssList(_241287), 393 ^ _228672 : [(394 ^ _228672) ^ [_241436] : [ssList(_241436), 397 ^ _228672 : [(398 ^ _228672) ^ [] : [rearsegP(_241287, _241436), 402 ^ _228672 : [(403 ^ _228672) ^ [] : [-(ssList(401 ^ [_241287, _241436]))], (405 ^ _228672) ^ [] : [-(app(401 ^ [_241287, _241436], _241436) = _241287)]]], (407 ^ _228672) ^ [] : [-(rearsegP(_241287, _241436)), 408 ^ _228672 : [(409 ^ _228672) ^ [_241911] : [ssList(_241911), app(_241911, _241436) = _241287]]]]]]], (417 ^ _228672) ^ [_242183] : [ssList(_242183), 420 ^ _228672 : [(421 ^ _228672) ^ [_242345] : [ssList(_242345), 424 ^ _228672 : [(425 ^ _228672) ^ [] : [segmentP(_242183, _242345), 429 ^ _228672 : [(430 ^ _228672) ^ [] : [-(ssList(428 ^ [_242183, _242345]))], (433 ^ _228672) ^ [] : [-(ssList(431 ^ [_242183, _242345]))], (435 ^ _228672) ^ [] : [-(app(app(428 ^ [_242183, _242345], _242345), 431 ^ [_242183, _242345]) = _242183)]]], (437 ^ _228672) ^ [] : [-(segmentP(_242183, _242345)), 438 ^ _228672 : [(439 ^ _228672) ^ [_242993] : [ssList(_242993), 442 ^ _228672 : [(443 ^ _228672) ^ [_243141] : [ssList(_243141), app(app(_242993, _242345), _243141) = _242183]]]]]]]]], (451 ^ _228672) ^ [_243432] : [ssList(_243432), 454 ^ _228672 : [(489 ^ _228672) ^ [] : [491 ^ _228672 : [(492 ^ _228672) ^ [] : [-(ssItem(490 ^ [_243432]))], (495 ^ _228672) ^ [] : [-(ssItem(493 ^ [_243432]))], (498 ^ _228672) ^ [] : [-(ssList(496 ^ [_243432]))], (501 ^ _228672) ^ [] : [-(ssList(499 ^ [_243432]))], (504 ^ _228672) ^ [] : [-(ssList(502 ^ [_243432]))], (506 ^ _228672) ^ [] : [-(app(app(496 ^ [_243432], cons(490 ^ [_243432], 499 ^ [_243432])), cons(493 ^ [_243432], 502 ^ [_243432])) = _243432)], (508 ^ _228672) ^ [] : [-(leq(490 ^ [_243432], 493 ^ [_243432]))], (510 ^ _228672) ^ [] : [-(leq(493 ^ [_243432], 490 ^ [_243432]))]], -(cyclefreeP(_243432))], (455 ^ _228672) ^ [] : [cyclefreeP(_243432), 458 ^ _228672 : [(459 ^ _228672) ^ [_243736] : [ssItem(_243736), 462 ^ _228672 : [(463 ^ _228672) ^ [_243928] : [ssItem(_243928), 466 ^ _228672 : [(467 ^ _228672) ^ [_244116] : [ssList(_244116), 470 ^ _228672 : [(471 ^ _228672) ^ [_244300] : [ssList(_244300), 474 ^ _228672 : [(475 ^ _228672) ^ [_244480] : [ssList(_244480), app(app(_244116, cons(_243736, _244300)), cons(_243928, _244480)) = _243432, leq(_243736, _243928), leq(_243928, _243736)]]]]]]]]]]]]], (514 ^ _228672) ^ [_246218] : [ssList(_246218), 517 ^ _228672 : [(552 ^ _228672) ^ [] : [554 ^ _228672 : [(555 ^ _228672) ^ [] : [-(ssItem(553 ^ [_246218]))], (558 ^ _228672) ^ [] : [-(ssItem(556 ^ [_246218]))], (561 ^ _228672) ^ [] : [-(ssList(559 ^ [_246218]))], (564 ^ _228672) ^ [] : [-(ssList(562 ^ [_246218]))], (567 ^ _228672) ^ [] : [-(ssList(565 ^ [_246218]))], (569 ^ _228672) ^ [] : [-(app(app(559 ^ [_246218], cons(553 ^ [_246218], 562 ^ [_246218])), cons(556 ^ [_246218], 565 ^ [_246218])) = _246218)], (571 ^ _228672) ^ [] : [leq(553 ^ [_246218], 556 ^ [_246218])], (573 ^ _228672) ^ [] : [leq(556 ^ [_246218], 553 ^ [_246218])]], -(totalorderP(_246218))], (518 ^ _228672) ^ [] : [totalorderP(_246218), 521 ^ _228672 : [(522 ^ _228672) ^ [_246520] : [ssItem(_246520), 525 ^ _228672 : [(526 ^ _228672) ^ [_246710] : [ssItem(_246710), 529 ^ _228672 : [(530 ^ _228672) ^ [_246896] : [ssList(_246896), 533 ^ _228672 : [(534 ^ _228672) ^ [_247078] : [ssList(_247078), 537 ^ _228672 : [(538 ^ _228672) ^ [_247256] : [ssList(_247256), app(app(_246896, cons(_246520, _247078)), cons(_246710, _247256)) = _246218, -(leq(_246520, _246710)), -(leq(_246710, _246520))]]]]]]]]]]]]], (577 ^ _228672) ^ [_248982] : [ssList(_248982), 580 ^ _228672 : [(615 ^ _228672) ^ [] : [617 ^ _228672 : [(618 ^ _228672) ^ [] : [-(ssItem(616 ^ [_248982]))], (621 ^ _228672) ^ [] : [-(ssItem(619 ^ [_248982]))], (624 ^ _228672) ^ [] : [-(ssList(622 ^ [_248982]))], (627 ^ _228672) ^ [] : [-(ssList(625 ^ [_248982]))], (630 ^ _228672) ^ [] : [-(ssList(628 ^ [_248982]))], (632 ^ _228672) ^ [] : [-(app(app(622 ^ [_248982], cons(616 ^ [_248982], 625 ^ [_248982])), cons(619 ^ [_248982], 628 ^ [_248982])) = _248982)], (634 ^ _228672) ^ [] : [lt(616 ^ [_248982], 619 ^ [_248982])], (636 ^ _228672) ^ [] : [lt(619 ^ [_248982], 616 ^ [_248982])]], -(strictorderP(_248982))], (581 ^ _228672) ^ [] : [strictorderP(_248982), 584 ^ _228672 : [(585 ^ _228672) ^ [_249284] : [ssItem(_249284), 588 ^ _228672 : [(589 ^ _228672) ^ [_249474] : [ssItem(_249474), 592 ^ _228672 : [(593 ^ _228672) ^ [_249660] : [ssList(_249660), 596 ^ _228672 : [(597 ^ _228672) ^ [_249842] : [ssList(_249842), 600 ^ _228672 : [(601 ^ _228672) ^ [_250020] : [ssList(_250020), app(app(_249660, cons(_249284, _249842)), cons(_249474, _250020)) = _248982, -(lt(_249284, _249474)), -(lt(_249474, _249284))]]]]]]]]]]]]], (640 ^ _228672) ^ [_251746] : [ssList(_251746), 643 ^ _228672 : [(674 ^ _228672) ^ [] : [676 ^ _228672 : [(677 ^ _228672) ^ [] : [-(ssItem(675 ^ [_251746]))], (680 ^ _228672) ^ [] : [-(ssItem(678 ^ [_251746]))], (683 ^ _228672) ^ [] : [-(ssList(681 ^ [_251746]))], (686 ^ _228672) ^ [] : [-(ssList(684 ^ [_251746]))], (689 ^ _228672) ^ [] : [-(ssList(687 ^ [_251746]))], (691 ^ _228672) ^ [] : [-(app(app(681 ^ [_251746], cons(675 ^ [_251746], 684 ^ [_251746])), cons(678 ^ [_251746], 687 ^ [_251746])) = _251746)], (693 ^ _228672) ^ [] : [leq(675 ^ [_251746], 678 ^ [_251746])]], -(totalorderedP(_251746))], (644 ^ _228672) ^ [] : [totalorderedP(_251746), 647 ^ _228672 : [(648 ^ _228672) ^ [_252042] : [ssItem(_252042), 651 ^ _228672 : [(652 ^ _228672) ^ [_252226] : [ssItem(_252226), 655 ^ _228672 : [(656 ^ _228672) ^ [_252406] : [ssList(_252406), 659 ^ _228672 : [(660 ^ _228672) ^ [_252582] : [ssList(_252582), 663 ^ _228672 : [(664 ^ _228672) ^ [_252754] : [ssList(_252754), app(app(_252406, cons(_252042, _252582)), cons(_252226, _252754)) = _251746, -(leq(_252042, _252226))]]]]]]]]]]]]], (697 ^ _228672) ^ [_254234] : [ssList(_254234), 700 ^ _228672 : [(731 ^ _228672) ^ [] : [733 ^ _228672 : [(734 ^ _228672) ^ [] : [-(ssItem(732 ^ [_254234]))], (737 ^ _228672) ^ [] : [-(ssItem(735 ^ [_254234]))], (740 ^ _228672) ^ [] : [-(ssList(738 ^ [_254234]))], (743 ^ _228672) ^ [] : [-(ssList(741 ^ [_254234]))], (746 ^ _228672) ^ [] : [-(ssList(744 ^ [_254234]))], (748 ^ _228672) ^ [] : [-(app(app(738 ^ [_254234], cons(732 ^ [_254234], 741 ^ [_254234])), cons(735 ^ [_254234], 744 ^ [_254234])) = _254234)], (750 ^ _228672) ^ [] : [lt(732 ^ [_254234], 735 ^ [_254234])]], -(strictorderedP(_254234))], (701 ^ _228672) ^ [] : [strictorderedP(_254234), 704 ^ _228672 : [(705 ^ _228672) ^ [_254530] : [ssItem(_254530), 708 ^ _228672 : [(709 ^ _228672) ^ [_254714] : [ssItem(_254714), 712 ^ _228672 : [(713 ^ _228672) ^ [_254894] : [ssList(_254894), 716 ^ _228672 : [(717 ^ _228672) ^ [_255070] : [ssList(_255070), 720 ^ _228672 : [(721 ^ _228672) ^ [_255242] : [ssList(_255242), app(app(_254894, cons(_254530, _255070)), cons(_254714, _255242)) = _254234, -(lt(_254530, _254714))]]]]]]]]]]]]], (754 ^ _228672) ^ [_256722] : [ssList(_256722), 757 ^ _228672 : [(788 ^ _228672) ^ [] : [790 ^ _228672 : [(791 ^ _228672) ^ [] : [-(ssItem(789 ^ [_256722]))], (794 ^ _228672) ^ [] : [-(ssItem(792 ^ [_256722]))], (797 ^ _228672) ^ [] : [-(ssList(795 ^ [_256722]))], (800 ^ _228672) ^ [] : [-(ssList(798 ^ [_256722]))], (803 ^ _228672) ^ [] : [-(ssList(801 ^ [_256722]))], (805 ^ _228672) ^ [] : [-(app(app(795 ^ [_256722], cons(789 ^ [_256722], 798 ^ [_256722])), cons(792 ^ [_256722], 801 ^ [_256722])) = _256722)], (807 ^ _228672) ^ [] : [-(789 ^ [_256722] = 792 ^ [_256722])]], -(duplicatefreeP(_256722))], (758 ^ _228672) ^ [] : [duplicatefreeP(_256722), 761 ^ _228672 : [(762 ^ _228672) ^ [_257020] : [ssItem(_257020), 765 ^ _228672 : [(766 ^ _228672) ^ [_257206] : [ssItem(_257206), 769 ^ _228672 : [(770 ^ _228672) ^ [_257388] : [ssList(_257388), 773 ^ _228672 : [(774 ^ _228672) ^ [_257566] : [ssList(_257566), 777 ^ _228672 : [(778 ^ _228672) ^ [_257740] : [ssList(_257740), app(app(_257388, cons(_257020, _257566)), cons(_257206, _257740)) = _256722, _257020 = _257206]]]]]]]]]]]]], (811 ^ _228672) ^ [_259232] : [ssList(_259232), 814 ^ _228672 : [(841 ^ _228672) ^ [] : [843 ^ _228672 : [(844 ^ _228672) ^ [] : [-(ssItem(842 ^ [_259232]))], (847 ^ _228672) ^ [] : [-(ssItem(845 ^ [_259232]))], (850 ^ _228672) ^ [] : [-(ssList(848 ^ [_259232]))], (853 ^ _228672) ^ [] : [-(ssList(851 ^ [_259232]))], (855 ^ _228672) ^ [] : [-(app(848 ^ [_259232], cons(842 ^ [_259232], cons(845 ^ [_259232], 851 ^ [_259232]))) = _259232)], (857 ^ _228672) ^ [] : [842 ^ [_259232] = 845 ^ [_259232]]], -(equalelemsP(_259232))], (815 ^ _228672) ^ [] : [equalelemsP(_259232), 818 ^ _228672 : [(819 ^ _228672) ^ [_259515] : [ssItem(_259515), 822 ^ _228672 : [(823 ^ _228672) ^ [_259686] : [ssItem(_259686), 826 ^ _228672 : [(827 ^ _228672) ^ [_259853] : [ssList(_259853), 830 ^ _228672 : [(831 ^ _228672) ^ [_260016] : [ssList(_260016), app(_259853, cons(_259515, cons(_259686, _260016))) = _259232, -(_259515 = _259686)]]]]]]]]]]], (861 ^ _228672) ^ [_261249] : [ssList(_261249), 864 ^ _228672 : [(865 ^ _228672) ^ [_261387] : [ssList(_261387), 868 ^ _228672 : [(869 ^ _228672) ^ [] : [neq(_261249, _261387), _261249 = _261387], (875 ^ _228672) ^ [] : [-(_261249 = _261387), -(neq(_261249, _261387))]]]]], (881 ^ _228672) ^ [_261840] : [ssList(_261840), 884 ^ _228672 : [(885 ^ _228672) ^ [_261972] : [ssItem(_261972), -(ssList(cons(_261972, _261840)))]]], (891 ^ _228672) ^ [] : [-(ssList(nil))], (893 ^ _228672) ^ [_262230] : [ssList(_262230), 896 ^ _228672 : [(897 ^ _228672) ^ [_262365] : [ssItem(_262365), cons(_262365, _262230) = _262230]]], (903 ^ _228672) ^ [_262573] : [ssList(_262573), 906 ^ _228672 : [(907 ^ _228672) ^ [_262741] : [ssList(_262741), 910 ^ _228672 : [(911 ^ _228672) ^ [_262905] : [ssItem(_262905), 914 ^ _228672 : [(915 ^ _228672) ^ [_263065] : [ssItem(_263065), cons(_262905, _262573) = cons(_263065, _262741), 922 ^ _228672 : [(923 ^ _228672) ^ [] : [-(_262905 = _263065)], (925 ^ _228672) ^ [] : [-(_262741 = _262573)]]]]]]]]], (927 ^ _228672) ^ [_263480] : [ssList(_263480), -(nil = _263480), 935 ^ _228672 : [(936 ^ _228672) ^ [] : [-(ssList(934 ^ [_263480]))], (939 ^ _228672) ^ [] : [-(ssItem(937 ^ [_263480]))], (941 ^ _228672) ^ [] : [-(cons(937 ^ [_263480], 934 ^ [_263480]) = _263480)]]], (943 ^ _228672) ^ [_264044] : [ssList(_264044), 946 ^ _228672 : [(947 ^ _228672) ^ [_264179] : [ssItem(_264179), nil = cons(_264179, _264044)]]], (953 ^ _228672) ^ [_264387] : [ssList(_264387), -(nil = _264387), -(ssItem(hd(_264387)))], (963 ^ _228672) ^ [_264665] : [ssList(_264665), 966 ^ _228672 : [(967 ^ _228672) ^ [_264800] : [ssItem(_264800), -(hd(cons(_264800, _264665)) = _264800)]]], (973 ^ _228672) ^ [_265011] : [ssList(_265011), -(nil = _265011), -(ssList(tl(_265011)))], (983 ^ _228672) ^ [_265289] : [ssList(_265289), 986 ^ _228672 : [(987 ^ _228672) ^ [_265424] : [ssItem(_265424), -(tl(cons(_265424, _265289)) = _265289)]]], (993 ^ _228672) ^ [_265635] : [ssList(_265635), 996 ^ _228672 : [(997 ^ _228672) ^ [_265767] : [ssList(_265767), -(ssList(app(_265635, _265767)))]]], (1003 ^ _228672) ^ [_265972] : [ssList(_265972), 1006 ^ _228672 : [(1007 ^ _228672) ^ [_266124] : [ssList(_266124), 1010 ^ _228672 : [(1011 ^ _228672) ^ [_266272] : [ssItem(_266272), -(cons(_266272, app(_266124, _265972)) = app(cons(_266272, _266124), _265972))]]]]], (1017 ^ _228672) ^ [_266510] : [ssList(_266510), -(app(nil, _266510) = _266510)], (1023 ^ _228672) ^ [_266704] : [ssItem(_266704), 1026 ^ _228672 : [(1027 ^ _228672) ^ [_266846] : [ssItem(_266846), -(_266704 = _266846), leq(_266704, _266846), leq(_266846, _266704)]]], (1041 ^ _228672) ^ [_267225] : [ssItem(_267225), 1044 ^ _228672 : [(1045 ^ _228672) ^ [_267377] : [ssItem(_267377), 1048 ^ _228672 : [(1049 ^ _228672) ^ [_267525] : [ssItem(_267525), -(leq(_267225, _267525)), leq(_267225, _267377), leq(_267377, _267525)]]]]], (1063 ^ _228672) ^ [_267925] : [ssItem(_267925), -(leq(_267925, _267925))], (1069 ^ _228672) ^ [_268113] : [ssItem(_268113), 1072 ^ _228672 : [(1073 ^ _228672) ^ [_268249] : [ssItem(_268249), 1076 ^ _228672 : [(1077 ^ _228672) ^ [] : [geq(_268113, _268249), -(leq(_268249, _268113))], (1083 ^ _228672) ^ [] : [leq(_268249, _268113), -(geq(_268113, _268249))]]]]], (1089 ^ _228672) ^ [_268700] : [ssItem(_268700), 1092 ^ _228672 : [(1093 ^ _228672) ^ [_268838] : [ssItem(_268838), lt(_268700, _268838), lt(_268838, _268700)]]], (1103 ^ _228672) ^ [_269129] : [ssItem(_269129), 1106 ^ _228672 : [(1107 ^ _228672) ^ [_269281] : [ssItem(_269281), 1110 ^ _228672 : [(1111 ^ _228672) ^ [_269429] : [ssItem(_269429), -(lt(_269129, _269429)), lt(_269129, _269281), lt(_269281, _269429)]]]]], (1125 ^ _228672) ^ [_269829] : [ssItem(_269829), 1128 ^ _228672 : [(1129 ^ _228672) ^ [_269965] : [ssItem(_269965), 1132 ^ _228672 : [(1133 ^ _228672) ^ [] : [gt(_269829, _269965), -(lt(_269965, _269829))], (1139 ^ _228672) ^ [] : [lt(_269965, _269829), -(gt(_269829, _269965))]]]]], (1145 ^ _228672) ^ [_270416] : [ssItem(_270416), 1148 ^ _228672 : [(1149 ^ _228672) ^ [_270571] : [ssList(_270571), 1152 ^ _228672 : [(1153 ^ _228672) ^ [_270722] : [ssList(_270722), 1156 ^ _228672 : [(1167 ^ _228672) ^ [] : [1168 ^ _228672 : [(1169 ^ _228672) ^ [] : [memberP(_270571, _270416)], (1171 ^ _228672) ^ [] : [memberP(_270722, _270416)]], -(memberP(app(_270571, _270722), _270416))], (1157 ^ _228672) ^ [] : [memberP(app(_270571, _270722), _270416), -(memberP(_270571, _270416)), -(memberP(_270722, _270416))]]]]]]], (1175 ^ _228672) ^ [_271369] : [ssItem(_271369), 1178 ^ _228672 : [(1179 ^ _228672) ^ [_271524] : [ssItem(_271524), 1182 ^ _228672 : [(1183 ^ _228672) ^ [_271675] : [ssList(_271675), 1186 ^ _228672 : [(1197 ^ _228672) ^ [] : [1198 ^ _228672 : [(1199 ^ _228672) ^ [] : [_271369 = _271524], (1201 ^ _228672) ^ [] : [memberP(_271675, _271369)]], -(memberP(cons(_271524, _271675), _271369))], (1187 ^ _228672) ^ [] : [memberP(cons(_271524, _271675), _271369), -(_271369 = _271524), -(memberP(_271675, _271369))]]]]]]], (1205 ^ _228672) ^ [_272322] : [ssItem(_272322), memberP(nil, _272322)], (1211 ^ _228672) ^ [] : [singletonP(nil)], (1213 ^ _228672) ^ [_272563] : [ssList(_272563), 1216 ^ _228672 : [(1217 ^ _228672) ^ [_272715] : [ssList(_272715), 1220 ^ _228672 : [(1221 ^ _228672) ^ [_272863] : [ssList(_272863), -(frontsegP(_272563, _272863)), frontsegP(_272563, _272715), frontsegP(_272715, _272863)]]]]], (1235 ^ _228672) ^ [_273263] : [ssList(_273263), 1238 ^ _228672 : [(1239 ^ _228672) ^ [_273405] : [ssList(_273405), -(_273263 = _273405), frontsegP(_273263, _273405), frontsegP(_273405, _273263)]]], (1253 ^ _228672) ^ [_273784] : [ssList(_273784), -(frontsegP(_273784, _273784))], (1259 ^ _228672) ^ [_273972] : [ssList(_273972), 1262 ^ _228672 : [(1263 ^ _228672) ^ [_274121] : [ssList(_274121), 1266 ^ _228672 : [(1267 ^ _228672) ^ [_274266] : [ssList(_274266), frontsegP(_273972, _274121), -(frontsegP(app(_273972, _274266), _274121))]]]]], (1277 ^ _228672) ^ [_274579] : [ssItem(_274579), 1280 ^ _228672 : [(1281 ^ _228672) ^ [_274747] : [ssItem(_274747), 1284 ^ _228672 : [(1285 ^ _228672) ^ [_274911] : [ssList(_274911), 1288 ^ _228672 : [(1289 ^ _228672) ^ [_275071] : [ssList(_275071), 1292 ^ _228672 : [(1293 ^ _228672) ^ [] : [frontsegP(cons(_274579, _274911), cons(_274747, _275071)), 1296 ^ _228672 : [(1297 ^ _228672) ^ [] : [-(_274579 = _274747)], (1299 ^ _228672) ^ [] : [-(frontsegP(_274911, _275071))]]], (1301 ^ _228672) ^ [] : [-(frontsegP(cons(_274579, _274911), cons(_274747, _275071))), _274579 = _274747, frontsegP(_274911, _275071)]]]]]]]]], (1311 ^ _228672) ^ [_275756] : [ssList(_275756), -(frontsegP(_275756, nil))], (1317 ^ _228672) ^ [_275944] : [ssList(_275944), 1320 ^ _228672 : [(1321 ^ _228672) ^ [] : [frontsegP(nil, _275944), -(nil = _275944)], (1327 ^ _228672) ^ [] : [nil = _275944, -(frontsegP(nil, _275944))]]], (1333 ^ _228672) ^ [_276372] : [ssList(_276372), 1336 ^ _228672 : [(1337 ^ _228672) ^ [_276524] : [ssList(_276524), 1340 ^ _228672 : [(1341 ^ _228672) ^ [_276672] : [ssList(_276672), -(rearsegP(_276372, _276672)), rearsegP(_276372, _276524), rearsegP(_276524, _276672)]]]]], (1355 ^ _228672) ^ [_277072] : [ssList(_277072), 1358 ^ _228672 : [(1359 ^ _228672) ^ [_277214] : [ssList(_277214), -(_277072 = _277214), rearsegP(_277072, _277214), rearsegP(_277214, _277072)]]], (1373 ^ _228672) ^ [_277593] : [ssList(_277593), -(rearsegP(_277593, _277593))], (1379 ^ _228672) ^ [_277781] : [ssList(_277781), 1382 ^ _228672 : [(1383 ^ _228672) ^ [_277930] : [ssList(_277930), 1386 ^ _228672 : [(1387 ^ _228672) ^ [_278075] : [ssList(_278075), rearsegP(_277781, _277930), -(rearsegP(app(_278075, _277781), _277930))]]]]], (1397 ^ _228672) ^ [_278388] : [ssList(_278388), -(rearsegP(_278388, nil))], (1403 ^ _228672) ^ [_278576] : [ssList(_278576), 1406 ^ _228672 : [(1407 ^ _228672) ^ [] : [rearsegP(nil, _278576), -(nil = _278576)], (1413 ^ _228672) ^ [] : [nil = _278576, -(rearsegP(nil, _278576))]]], (1419 ^ _228672) ^ [_279004] : [ssList(_279004), 1422 ^ _228672 : [(1423 ^ _228672) ^ [_279156] : [ssList(_279156), 1426 ^ _228672 : [(1427 ^ _228672) ^ [_279304] : [ssList(_279304), -(segmentP(_279004, _279304)), segmentP(_279004, _279156), segmentP(_279156, _279304)]]]]], (1441 ^ _228672) ^ [_279704] : [ssList(_279704), 1444 ^ _228672 : [(1445 ^ _228672) ^ [_279846] : [ssList(_279846), -(_279704 = _279846), segmentP(_279704, _279846), segmentP(_279846, _279704)]]], (1459 ^ _228672) ^ [_280225] : [ssList(_280225), -(segmentP(_280225, _280225))], (1465 ^ _228672) ^ [_280413] : [ssList(_280413), 1468 ^ _228672 : [(1469 ^ _228672) ^ [_280575] : [ssList(_280575), 1472 ^ _228672 : [(1473 ^ _228672) ^ [_280733] : [ssList(_280733), 1476 ^ _228672 : [(1477 ^ _228672) ^ [_280887] : [ssList(_280887), segmentP(_280413, _280575), -(segmentP(app(app(_280733, _280413), _280887), _280575))]]]]]]], (1487 ^ _228672) ^ [_281223] : [ssList(_281223), -(segmentP(_281223, nil))], (1493 ^ _228672) ^ [_281411] : [ssList(_281411), 1496 ^ _228672 : [(1497 ^ _228672) ^ [] : [segmentP(nil, _281411), -(nil = _281411)], (1503 ^ _228672) ^ [] : [nil = _281411, -(segmentP(nil, _281411))]]], (1509 ^ _228672) ^ [_281839] : [ssItem(_281839), -(cyclefreeP(cons(_281839, nil)))], (1515 ^ _228672) ^ [] : [-(cyclefreeP(nil))], (1517 ^ _228672) ^ [_282084] : [ssItem(_282084), -(totalorderP(cons(_282084, nil)))], (1523 ^ _228672) ^ [] : [-(totalorderP(nil))], (1525 ^ _228672) ^ [_282329] : [ssItem(_282329), -(strictorderP(cons(_282329, nil)))], (1531 ^ _228672) ^ [] : [-(strictorderP(nil))], (1533 ^ _228672) ^ [_282574] : [ssItem(_282574), -(totalorderedP(cons(_282574, nil)))], (1539 ^ _228672) ^ [] : [-(totalorderedP(nil))], (1541 ^ _228672) ^ [_282819] : [ssItem(_282819), 1544 ^ _228672 : [(1545 ^ _228672) ^ [_282978] : [ssList(_282978), 1548 ^ _228672 : [(1549 ^ _228672) ^ [] : [totalorderedP(cons(_282819, _282978)), -(nil = _282978), 1556 ^ _228672 : [(1557 ^ _228672) ^ [] : [nil = _282978], (1559 ^ _228672) ^ [] : [-(totalorderedP(_282978))], (1561 ^ _228672) ^ [] : [-(leq(_282819, hd(_282978)))]]], (1563 ^ _228672) ^ [] : [-(totalorderedP(cons(_282819, _282978))), 1564 ^ _228672 : [(1565 ^ _228672) ^ [] : [nil = _282978], (1567 ^ _228672) ^ [] : [-(nil = _282978), totalorderedP(_282978), leq(_282819, hd(_282978))]]]]]]], (1579 ^ _228672) ^ [_283913] : [ssItem(_283913), -(strictorderedP(cons(_283913, nil)))], (1585 ^ _228672) ^ [] : [-(strictorderedP(nil))], (1587 ^ _228672) ^ [_284158] : [ssItem(_284158), 1590 ^ _228672 : [(1591 ^ _228672) ^ [_284317] : [ssList(_284317), 1594 ^ _228672 : [(1595 ^ _228672) ^ [] : [strictorderedP(cons(_284158, _284317)), -(nil = _284317), 1602 ^ _228672 : [(1603 ^ _228672) ^ [] : [nil = _284317], (1605 ^ _228672) ^ [] : [-(strictorderedP(_284317))], (1607 ^ _228672) ^ [] : [-(lt(_284158, hd(_284317)))]]], (1609 ^ _228672) ^ [] : [-(strictorderedP(cons(_284158, _284317))), 1610 ^ _228672 : [(1611 ^ _228672) ^ [] : [nil = _284317], (1613 ^ _228672) ^ [] : [-(nil = _284317), strictorderedP(_284317), lt(_284158, hd(_284317))]]]]]]], (1625 ^ _228672) ^ [_285252] : [ssItem(_285252), -(duplicatefreeP(cons(_285252, nil)))], (1631 ^ _228672) ^ [] : [-(duplicatefreeP(nil))], (1633 ^ _228672) ^ [_285497] : [ssItem(_285497), -(equalelemsP(cons(_285497, nil)))], (1639 ^ _228672) ^ [] : [-(equalelemsP(nil))], (1641 ^ _228672) ^ [_285742] : [ssList(_285742), -(nil = _285742), 1649 ^ _228672 : [(1650 ^ _228672) ^ [] : [-(ssItem(1648 ^ [_285742]))], (1652 ^ _228672) ^ [] : [-(hd(_285742) = 1648 ^ [_285742])]]], (1654 ^ _228672) ^ [_286156] : [ssList(_286156), -(nil = _286156), 1662 ^ _228672 : [(1663 ^ _228672) ^ [] : [-(ssList(1661 ^ [_286156]))], (1665 ^ _228672) ^ [] : [-(tl(_286156) = 1661 ^ [_286156])]]], (1667 ^ _228672) ^ [_286570] : [ssList(_286570), 1670 ^ _228672 : [(1671 ^ _228672) ^ [_286736] : [ssList(_286736), -(_286736 = _286570), -(nil = _286736), -(nil = _286570), hd(_286736) = hd(_286570), tl(_286736) = tl(_286570)]]], (1693 ^ _228672) ^ [_287315] : [ssList(_287315), -(nil = _287315), -(cons(hd(_287315), tl(_287315)) = _287315)], (1703 ^ _228672) ^ [_287605] : [ssList(_287605), 1706 ^ _228672 : [(1707 ^ _228672) ^ [_287757] : [ssList(_287757), 1710 ^ _228672 : [(1711 ^ _228672) ^ [_287905] : [ssList(_287905), app(_287905, _287757) = app(_287605, _287757), -(_287905 = _287605)]]]]], (1721 ^ _228672) ^ [_288224] : [ssList(_288224), 1724 ^ _228672 : [(1725 ^ _228672) ^ [_288376] : [ssList(_288376), 1728 ^ _228672 : [(1729 ^ _228672) ^ [_288524] : [ssList(_288524), app(_288376, _288524) = app(_288376, _288224), -(_288524 = _288224)]]]]], (1739 ^ _228672) ^ [_288843] : [ssList(_288843), 1742 ^ _228672 : [(1743 ^ _228672) ^ [_288982] : [ssItem(_288982), -(cons(_288982, _288843) = app(cons(_288982, nil), _288843))]]], (1749 ^ _228672) ^ [_289201] : [ssList(_289201), 1752 ^ _228672 : [(1753 ^ _228672) ^ [_289353] : [ssList(_289353), 1756 ^ _228672 : [(1757 ^ _228672) ^ [_289501] : [ssList(_289501), -(app(app(_289201, _289353), _289501) = app(_289201, app(_289353, _289501)))]]]]], (1763 ^ _228672) ^ [_289739] : [ssList(_289739), 1766 ^ _228672 : [(1767 ^ _228672) ^ [_289884] : [ssList(_289884), 1770 ^ _228672 : [(1771 ^ _228672) ^ [] : [nil = app(_289739, _289884), 1774 ^ _228672 : [(1775 ^ _228672) ^ [] : [-(nil = _289884)], (1777 ^ _228672) ^ [] : [-(nil = _289739)]]], (1779 ^ _228672) ^ [] : [-(nil = app(_289739, _289884)), nil = _289884, nil = _289739]]]]], (1789 ^ _228672) ^ [_290502] : [ssList(_290502), -(app(_290502, nil) = _290502)], (1795 ^ _228672) ^ [_290696] : [ssList(_290696), 1798 ^ _228672 : [(1799 ^ _228672) ^ [_290841] : [ssList(_290841), -(nil = _290696), -(hd(app(_290696, _290841)) = hd(_290696))]]], (1809 ^ _228672) ^ [_291148] : [ssList(_291148), 1812 ^ _228672 : [(1813 ^ _228672) ^ [_291296] : [ssList(_291296), -(nil = _291148), -(tl(app(_291148, _291296)) = app(tl(_291148), _291296))]]], (1823 ^ _228672) ^ [_291609] : [ssItem(_291609), 1826 ^ _228672 : [(1827 ^ _228672) ^ [_291751] : [ssItem(_291751), -(_291609 = _291751), geq(_291609, _291751), geq(_291751, _291609)]]], (1841 ^ _228672) ^ [_292130] : [ssItem(_292130), 1844 ^ _228672 : [(1845 ^ _228672) ^ [_292282] : [ssItem(_292282), 1848 ^ _228672 : [(1849 ^ _228672) ^ [_292430] : [ssItem(_292430), -(geq(_292130, _292430)), geq(_292130, _292282), geq(_292282, _292430)]]]]], (1863 ^ _228672) ^ [_292830] : [ssItem(_292830), -(geq(_292830, _292830))], (1869 ^ _228672) ^ [_293018] : [ssItem(_293018), lt(_293018, _293018)], (1875 ^ _228672) ^ [_293207] : [ssItem(_293207), 1878 ^ _228672 : [(1879 ^ _228672) ^ [_293359] : [ssItem(_293359), 1882 ^ _228672 : [(1883 ^ _228672) ^ [_293507] : [ssItem(_293507), -(lt(_293207, _293507)), leq(_293207, _293359), lt(_293359, _293507)]]]]], (1897 ^ _228672) ^ [_293907] : [ssItem(_293907), 1900 ^ _228672 : [(1901 ^ _228672) ^ [_294049] : [ssItem(_294049), leq(_293907, _294049), -(_293907 = _294049), -(lt(_293907, _294049))]]], (1915 ^ _228672) ^ [_294429] : [ssItem(_294429), 1918 ^ _228672 : [(1919 ^ _228672) ^ [_294573] : [ssItem(_294573), 1922 ^ _228672 : [(1923 ^ _228672) ^ [] : [lt(_294429, _294573), 1926 ^ _228672 : [(1927 ^ _228672) ^ [] : [_294429 = _294573], (1929 ^ _228672) ^ [] : [-(leq(_294429, _294573))]]], (1931 ^ _228672) ^ [] : [-(lt(_294429, _294573)), -(_294429 = _294573), leq(_294429, _294573)]]]]], (1941 ^ _228672) ^ [_295184] : [ssItem(_295184), 1944 ^ _228672 : [(1945 ^ _228672) ^ [_295322] : [ssItem(_295322), gt(_295184, _295322), gt(_295322, _295184)]]], (1955 ^ _228672) ^ [_295593] : [ssItem(_295593), 1958 ^ _228672 : [(1959 ^ _228672) ^ [_295745] : [ssItem(_295745), 1962 ^ _228672 : [(1963 ^ _228672) ^ [_295893] : [ssItem(_295893), -(gt(_295593, _295893)), gt(_295593, _295745), gt(_295745, _295893)]]]]]], input).
% 0.33/1.37 ncf('1',plain,[totalorderP(1985 ^ [])],start(1995 ^ 0)).
% 0.33/1.37 ncf('1.1',plain,[-(totalorderP(1985 ^ [])), 1979 ^ [] = 1985 ^ [], totalorderP(1979 ^ [])],extension(236 ^ 1,bind([[_236071, _236073], [1985 ^ [], 1979 ^ []]]))).
% 0.33/1.37 ncf('1.1.1',plain,[-(1979 ^ [] = 1985 ^ [])],extension(1989 ^ 2)).
% 0.33/1.37 ncf('1.1.2',plain,[-(totalorderP(1979 ^ []))],extension(1993 ^ 2)).
% 0.33/1.37 %-----------------------------------------------------
% 0.33/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------