%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWC350+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n005.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 0.39s 1.38s
% Output : Proof 0.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWC350+1 : TPTP v8.1.2. Released v2.4.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n005.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 00:58:08 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.39/1.38
% 0.39/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.39/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.39/1.38 %-----------------------------------------------------
% 0.39/1.38 ncf(matrix, plain, [(1978 ^ _232197) ^ [] : [-(ssList(1976 ^ []))], (1981 ^ _232197) ^ [] : [-(ssList(1979 ^ []))], (1984 ^ _232197) ^ [] : [-(ssList(1982 ^ []))], (1987 ^ _232197) ^ [] : [-(ssList(1985 ^ []))], (1989 ^ _232197) ^ [] : [-(1979 ^ [] = 1985 ^ [])], (1991 ^ _232197) ^ [] : [-(1976 ^ [] = 1982 ^ [])], (1993 ^ _232197) ^ [] : [-(neq(1979 ^ [], nil))], (1995 ^ _232197) ^ [] : [-(frontsegP(1985 ^ [], 1982 ^ []))], (1997 ^ _232197) ^ [] : [-(equalelemsP(1982 ^ []))], (2017 ^ _232197) ^ [] : [frontsegP(1979 ^ [], 1976 ^ [])], (1999 ^ _232197) ^ [_301461] : [ssList(_301461), neq(1982 ^ [], _301461), frontsegP(1985 ^ [], _301461), segmentP(_301461, 1982 ^ []), equalelemsP(_301461)], (246 ^ _232197) ^ [_240001, _240003, _240005, _240007] : [-(cons(_240007, _240003) = cons(_240005, _240001)), _240007 = _240005, _240003 = _240001], (256 ^ _232197) ^ [_240332, _240334] : [_240334 = _240332, -(hd(_240334) = hd(_240332))], (272 ^ _232197) ^ [_240889, _240891] : [_240891 = _240889, -(tl(_240891) = tl(_240889))], (262 ^ _232197) ^ [_240578, _240580, _240582, _240584] : [-(app(_240584, _240580) = app(_240582, _240578)), _240584 = _240582, _240580 = _240578], (2 ^ _232197) ^ [_232341] : [-(_232341 = _232341)], (4 ^ _232197) ^ [_232448, _232450] : [_232450 = _232448, -(_232448 = _232450)], (10 ^ _232197) ^ [_232652, _232654, _232656] : [-(_232656 = _232652), _232656 = _232654, _232654 = _232652], (20 ^ _232197) ^ [_232993, _232995, _232997, _232999] : [-(memberP(_232997, _232993)), memberP(_232999, _232995), _232999 = _232997, _232995 = _232993], (34 ^ _232197) ^ [_233409, _233411] : [-(singletonP(_233409)), _233411 = _233409, singletonP(_233411)], (44 ^ _232197) ^ [_233732, _233734, _233736, _233738] : [-(rearsegP(_233736, _233732)), rearsegP(_233738, _233734), _233738 = _233736, _233734 = _233732], (58 ^ _232197) ^ [_234148, _234150] : [-(cyclefreeP(_234148)), _234150 = _234148, cyclefreeP(_234150)], (68 ^ _232197) ^ [_234443, _234445] : [-(totalorderP(_234443)), _234445 = _234443, totalorderP(_234445)], (78 ^ _232197) ^ [_234738, _234740] : [-(strictorderP(_234738)), _234740 = _234738, strictorderP(_234740)], (88 ^ _232197) ^ [_235033, _235035] : [-(totalorderedP(_235033)), _235035 = _235033, totalorderedP(_235035)], (98 ^ _232197) ^ [_235328, _235330] : [-(strictorderedP(_235328)), _235330 = _235328, strictorderedP(_235330)], (108 ^ _232197) ^ [_235623, _235625] : [-(duplicatefreeP(_235623)), _235625 = _235623, duplicatefreeP(_235625)], (118 ^ _232197) ^ [_235946, _235948, _235950, _235952] : [-(geq(_235950, _235946)), geq(_235952, _235948), _235952 = _235950, _235948 = _235946], (132 ^ _232197) ^ [_236390, _236392, _236394, _236396] : [-(lt(_236394, _236390)), lt(_236396, _236392), _236396 = _236394, _236392 = _236390], (146 ^ _232197) ^ [_236834, _236836, _236838, _236840] : [-(leq(_236838, _236834)), leq(_236840, _236836), _236840 = _236838, _236836 = _236834], (160 ^ _232197) ^ [_237250, _237252] : [-(ssItem(_237250)), _237252 = _237250, ssItem(_237252)], (170 ^ _232197) ^ [_237573, _237575, _237577, _237579] : [-(gt(_237577, _237573)), gt(_237579, _237575), _237579 = _237577, _237575 = _237573], (184 ^ _232197) ^ [_237989, _237991] : [-(ssList(_237989)), _237991 = _237989, ssList(_237991)], (194 ^ _232197) ^ [_238312, _238314, _238316, _238318] : [-(neq(_238316, _238312)), neq(_238318, _238314), _238318 = _238316, _238314 = _238312], (208 ^ _232197) ^ [_238756, _238758, _238760, _238762] : [-(segmentP(_238760, _238756)), segmentP(_238762, _238758), _238762 = _238760, _238758 = _238756], (222 ^ _232197) ^ [_239172, _239174] : [-(equalelemsP(_239172)), _239174 = _239172, equalelemsP(_239174)], (232 ^ _232197) ^ [_239475, _239477, _239479, _239481] : [-(frontsegP(_239479, _239475)), frontsegP(_239481, _239477), _239481 = _239479, _239477 = _239475], (278 ^ _232197) ^ [_241111] : [ssItem(_241111), 281 ^ _232197 : [(282 ^ _232197) ^ [_241249] : [ssItem(_241249), 285 ^ _232197 : [(286 ^ _232197) ^ [] : [neq(_241111, _241249), _241111 = _241249], (292 ^ _232197) ^ [] : [-(_241111 = _241249), -(neq(_241111, _241249))]]]]], (299 ^ _232197) ^ [] : [-(ssItem(297 ^ []))], (302 ^ _232197) ^ [] : [-(ssItem(300 ^ []))], (304 ^ _232197) ^ [] : [297 ^ [] = 300 ^ []], (306 ^ _232197) ^ [_241962] : [ssList(_241962), 309 ^ _232197 : [(310 ^ _232197) ^ [_242124] : [ssItem(_242124), 313 ^ _232197 : [(314 ^ _232197) ^ [] : [memberP(_241962, _242124), 318 ^ _232197 : [(319 ^ _232197) ^ [] : [-(ssList(317 ^ [_241962, _242124]))], (322 ^ _232197) ^ [] : [-(ssList(320 ^ [_241962, _242124]))], (324 ^ _232197) ^ [] : [-(app(317 ^ [_241962, _242124], cons(_242124, 320 ^ [_241962, _242124])) = _241962)]]], (326 ^ _232197) ^ [] : [-(memberP(_241962, _242124)), 327 ^ _232197 : [(328 ^ _232197) ^ [_242772] : [ssList(_242772), 331 ^ _232197 : [(332 ^ _232197) ^ [_242920] : [ssList(_242920), app(_242772, cons(_242124, _242920)) = _241962]]]]]]]]], (340 ^ _232197) ^ [_243211] : [ssList(_243211), 343 ^ _232197 : [(344 ^ _232197) ^ [] : [singletonP(_243211), 348 ^ _232197 : [(349 ^ _232197) ^ [] : [-(ssItem(347 ^ [_243211]))], (351 ^ _232197) ^ [] : [-(cons(347 ^ [_243211], nil) = _243211)]]], (353 ^ _232197) ^ [] : [-(singletonP(_243211)), 354 ^ _232197 : [(355 ^ _232197) ^ [_243660] : [ssItem(_243660), cons(_243660, nil) = _243211]]]]], (363 ^ _232197) ^ [_243916] : [ssList(_243916), 366 ^ _232197 : [(367 ^ _232197) ^ [_244065] : [ssList(_244065), 370 ^ _232197 : [(371 ^ _232197) ^ [] : [frontsegP(_243916, _244065), 375 ^ _232197 : [(376 ^ _232197) ^ [] : [-(ssList(374 ^ [_243916, _244065]))], (378 ^ _232197) ^ [] : [-(app(_244065, 374 ^ [_243916, _244065]) = _243916)]]], (380 ^ _232197) ^ [] : [-(frontsegP(_243916, _244065)), 381 ^ _232197 : [(382 ^ _232197) ^ [_244540] : [ssList(_244540), app(_244065, _244540) = _243916]]]]]]], (390 ^ _232197) ^ [_244812] : [ssList(_244812), 393 ^ _232197 : [(394 ^ _232197) ^ [_244961] : [ssList(_244961), 397 ^ _232197 : [(398 ^ _232197) ^ [] : [rearsegP(_244812, _244961), 402 ^ _232197 : [(403 ^ _232197) ^ [] : [-(ssList(401 ^ [_244812, _244961]))], (405 ^ _232197) ^ [] : [-(app(401 ^ [_244812, _244961], _244961) = _244812)]]], (407 ^ _232197) ^ [] : [-(rearsegP(_244812, _244961)), 408 ^ _232197 : [(409 ^ _232197) ^ [_245436] : [ssList(_245436), app(_245436, _244961) = _244812]]]]]]], (417 ^ _232197) ^ [_245708] : [ssList(_245708), 420 ^ _232197 : [(421 ^ _232197) ^ [_245870] : [ssList(_245870), 424 ^ _232197 : [(425 ^ _232197) ^ [] : [segmentP(_245708, _245870), 429 ^ _232197 : [(430 ^ _232197) ^ [] : [-(ssList(428 ^ [_245708, _245870]))], (433 ^ _232197) ^ [] : [-(ssList(431 ^ [_245708, _245870]))], (435 ^ _232197) ^ [] : [-(app(app(428 ^ [_245708, _245870], _245870), 431 ^ [_245708, _245870]) = _245708)]]], (437 ^ _232197) ^ [] : [-(segmentP(_245708, _245870)), 438 ^ _232197 : [(439 ^ _232197) ^ [_246518] : [ssList(_246518), 442 ^ _232197 : [(443 ^ _232197) ^ [_246666] : [ssList(_246666), app(app(_246518, _245870), _246666) = _245708]]]]]]]]], (451 ^ _232197) ^ [_246957] : [ssList(_246957), 454 ^ _232197 : [(489 ^ _232197) ^ [] : [491 ^ _232197 : [(492 ^ _232197) ^ [] : [-(ssItem(490 ^ [_246957]))], (495 ^ _232197) ^ [] : [-(ssItem(493 ^ [_246957]))], (498 ^ _232197) ^ [] : [-(ssList(496 ^ [_246957]))], (501 ^ _232197) ^ [] : [-(ssList(499 ^ [_246957]))], (504 ^ _232197) ^ [] : [-(ssList(502 ^ [_246957]))], (506 ^ _232197) ^ [] : [-(app(app(496 ^ [_246957], cons(490 ^ [_246957], 499 ^ [_246957])), cons(493 ^ [_246957], 502 ^ [_246957])) = _246957)], (508 ^ _232197) ^ [] : [-(leq(490 ^ [_246957], 493 ^ [_246957]))], (510 ^ _232197) ^ [] : [-(leq(493 ^ [_246957], 490 ^ [_246957]))]], -(cyclefreeP(_246957))], (455 ^ _232197) ^ [] : [cyclefreeP(_246957), 458 ^ _232197 : [(459 ^ _232197) ^ [_247261] : [ssItem(_247261), 462 ^ _232197 : [(463 ^ _232197) ^ [_247453] : [ssItem(_247453), 466 ^ _232197 : [(467 ^ _232197) ^ [_247641] : [ssList(_247641), 470 ^ _232197 : [(471 ^ _232197) ^ [_247825] : [ssList(_247825), 474 ^ _232197 : [(475 ^ _232197) ^ [_248005] : [ssList(_248005), app(app(_247641, cons(_247261, _247825)), cons(_247453, _248005)) = _246957, leq(_247261, _247453), leq(_247453, _247261)]]]]]]]]]]]]], (514 ^ _232197) ^ [_249743] : [ssList(_249743), 517 ^ _232197 : [(552 ^ _232197) ^ [] : [554 ^ _232197 : [(555 ^ _232197) ^ [] : [-(ssItem(553 ^ [_249743]))], (558 ^ _232197) ^ [] : [-(ssItem(556 ^ [_249743]))], (561 ^ _232197) ^ [] : [-(ssList(559 ^ [_249743]))], (564 ^ _232197) ^ [] : [-(ssList(562 ^ [_249743]))], (567 ^ _232197) ^ [] : [-(ssList(565 ^ [_249743]))], (569 ^ _232197) ^ [] : [-(app(app(559 ^ [_249743], cons(553 ^ [_249743], 562 ^ [_249743])), cons(556 ^ [_249743], 565 ^ [_249743])) = _249743)], (571 ^ _232197) ^ [] : [leq(553 ^ [_249743], 556 ^ [_249743])], (573 ^ _232197) ^ [] : [leq(556 ^ [_249743], 553 ^ [_249743])]], -(totalorderP(_249743))], (518 ^ _232197) ^ [] : [totalorderP(_249743), 521 ^ _232197 : [(522 ^ _232197) ^ [_250045] : [ssItem(_250045), 525 ^ _232197 : [(526 ^ _232197) ^ [_250235] : [ssItem(_250235), 529 ^ _232197 : [(530 ^ _232197) ^ [_250421] : [ssList(_250421), 533 ^ _232197 : [(534 ^ _232197) ^ [_250603] : [ssList(_250603), 537 ^ _232197 : [(538 ^ _232197) ^ [_250781] : [ssList(_250781), app(app(_250421, cons(_250045, _250603)), cons(_250235, _250781)) = _249743, -(leq(_250045, _250235)), -(leq(_250235, _250045))]]]]]]]]]]]]], (577 ^ _232197) ^ [_252507] : [ssList(_252507), 580 ^ _232197 : [(615 ^ _232197) ^ [] : [617 ^ _232197 : [(618 ^ _232197) ^ [] : [-(ssItem(616 ^ [_252507]))], (621 ^ _232197) ^ [] : [-(ssItem(619 ^ [_252507]))], (624 ^ _232197) ^ [] : [-(ssList(622 ^ [_252507]))], (627 ^ _232197) ^ [] : [-(ssList(625 ^ [_252507]))], (630 ^ _232197) ^ [] : [-(ssList(628 ^ [_252507]))], (632 ^ _232197) ^ [] : [-(app(app(622 ^ [_252507], cons(616 ^ [_252507], 625 ^ [_252507])), cons(619 ^ [_252507], 628 ^ [_252507])) = _252507)], (634 ^ _232197) ^ [] : [lt(616 ^ [_252507], 619 ^ [_252507])], (636 ^ _232197) ^ [] : [lt(619 ^ [_252507], 616 ^ [_252507])]], -(strictorderP(_252507))], (581 ^ _232197) ^ [] : [strictorderP(_252507), 584 ^ _232197 : [(585 ^ _232197) ^ [_252809] : [ssItem(_252809), 588 ^ _232197 : [(589 ^ _232197) ^ [_252999] : [ssItem(_252999), 592 ^ _232197 : [(593 ^ _232197) ^ [_253185] : [ssList(_253185), 596 ^ _232197 : [(597 ^ _232197) ^ [_253367] : [ssList(_253367), 600 ^ _232197 : [(601 ^ _232197) ^ [_253545] : [ssList(_253545), app(app(_253185, cons(_252809, _253367)), cons(_252999, _253545)) = _252507, -(lt(_252809, _252999)), -(lt(_252999, _252809))]]]]]]]]]]]]], (640 ^ _232197) ^ [_255271] : [ssList(_255271), 643 ^ _232197 : [(674 ^ _232197) ^ [] : [676 ^ _232197 : [(677 ^ _232197) ^ [] : [-(ssItem(675 ^ [_255271]))], (680 ^ _232197) ^ [] : [-(ssItem(678 ^ [_255271]))], (683 ^ _232197) ^ [] : [-(ssList(681 ^ [_255271]))], (686 ^ _232197) ^ [] : [-(ssList(684 ^ [_255271]))], (689 ^ _232197) ^ [] : [-(ssList(687 ^ [_255271]))], (691 ^ _232197) ^ [] : [-(app(app(681 ^ [_255271], cons(675 ^ [_255271], 684 ^ [_255271])), cons(678 ^ [_255271], 687 ^ [_255271])) = _255271)], (693 ^ _232197) ^ [] : [leq(675 ^ [_255271], 678 ^ [_255271])]], -(totalorderedP(_255271))], (644 ^ _232197) ^ [] : [totalorderedP(_255271), 647 ^ _232197 : [(648 ^ _232197) ^ [_255567] : [ssItem(_255567), 651 ^ _232197 : [(652 ^ _232197) ^ [_255751] : [ssItem(_255751), 655 ^ _232197 : [(656 ^ _232197) ^ [_255931] : [ssList(_255931), 659 ^ _232197 : [(660 ^ _232197) ^ [_256107] : [ssList(_256107), 663 ^ _232197 : [(664 ^ _232197) ^ [_256279] : [ssList(_256279), app(app(_255931, cons(_255567, _256107)), cons(_255751, _256279)) = _255271, -(leq(_255567, _255751))]]]]]]]]]]]]], (697 ^ _232197) ^ [_257759] : [ssList(_257759), 700 ^ _232197 : [(731 ^ _232197) ^ [] : [733 ^ _232197 : [(734 ^ _232197) ^ [] : [-(ssItem(732 ^ [_257759]))], (737 ^ _232197) ^ [] : [-(ssItem(735 ^ [_257759]))], (740 ^ _232197) ^ [] : [-(ssList(738 ^ [_257759]))], (743 ^ _232197) ^ [] : [-(ssList(741 ^ [_257759]))], (746 ^ _232197) ^ [] : [-(ssList(744 ^ [_257759]))], (748 ^ _232197) ^ [] : [-(app(app(738 ^ [_257759], cons(732 ^ [_257759], 741 ^ [_257759])), cons(735 ^ [_257759], 744 ^ [_257759])) = _257759)], (750 ^ _232197) ^ [] : [lt(732 ^ [_257759], 735 ^ [_257759])]], -(strictorderedP(_257759))], (701 ^ _232197) ^ [] : [strictorderedP(_257759), 704 ^ _232197 : [(705 ^ _232197) ^ [_258055] : [ssItem(_258055), 708 ^ _232197 : [(709 ^ _232197) ^ [_258239] : [ssItem(_258239), 712 ^ _232197 : [(713 ^ _232197) ^ [_258419] : [ssList(_258419), 716 ^ _232197 : [(717 ^ _232197) ^ [_258595] : [ssList(_258595), 720 ^ _232197 : [(721 ^ _232197) ^ [_258767] : [ssList(_258767), app(app(_258419, cons(_258055, _258595)), cons(_258239, _258767)) = _257759, -(lt(_258055, _258239))]]]]]]]]]]]]], (754 ^ _232197) ^ [_260247] : [ssList(_260247), 757 ^ _232197 : [(788 ^ _232197) ^ [] : [790 ^ _232197 : [(791 ^ _232197) ^ [] : [-(ssItem(789 ^ [_260247]))], (794 ^ _232197) ^ [] : [-(ssItem(792 ^ [_260247]))], (797 ^ _232197) ^ [] : [-(ssList(795 ^ [_260247]))], (800 ^ _232197) ^ [] : [-(ssList(798 ^ [_260247]))], (803 ^ _232197) ^ [] : [-(ssList(801 ^ [_260247]))], (805 ^ _232197) ^ [] : [-(app(app(795 ^ [_260247], cons(789 ^ [_260247], 798 ^ [_260247])), cons(792 ^ [_260247], 801 ^ [_260247])) = _260247)], (807 ^ _232197) ^ [] : [-(789 ^ [_260247] = 792 ^ [_260247])]], -(duplicatefreeP(_260247))], (758 ^ _232197) ^ [] : [duplicatefreeP(_260247), 761 ^ _232197 : [(762 ^ _232197) ^ [_260545] : [ssItem(_260545), 765 ^ _232197 : [(766 ^ _232197) ^ [_260731] : [ssItem(_260731), 769 ^ _232197 : [(770 ^ _232197) ^ [_260913] : [ssList(_260913), 773 ^ _232197 : [(774 ^ _232197) ^ [_261091] : [ssList(_261091), 777 ^ _232197 : [(778 ^ _232197) ^ [_261265] : [ssList(_261265), app(app(_260913, cons(_260545, _261091)), cons(_260731, _261265)) = _260247, _260545 = _260731]]]]]]]]]]]]], (811 ^ _232197) ^ [_262757] : [ssList(_262757), 814 ^ _232197 : [(841 ^ _232197) ^ [] : [843 ^ _232197 : [(844 ^ _232197) ^ [] : [-(ssItem(842 ^ [_262757]))], (847 ^ _232197) ^ [] : [-(ssItem(845 ^ [_262757]))], (850 ^ _232197) ^ [] : [-(ssList(848 ^ [_262757]))], (853 ^ _232197) ^ [] : [-(ssList(851 ^ [_262757]))], (855 ^ _232197) ^ [] : [-(app(848 ^ [_262757], cons(842 ^ [_262757], cons(845 ^ [_262757], 851 ^ [_262757]))) = _262757)], (857 ^ _232197) ^ [] : [842 ^ [_262757] = 845 ^ [_262757]]], -(equalelemsP(_262757))], (815 ^ _232197) ^ [] : [equalelemsP(_262757), 818 ^ _232197 : [(819 ^ _232197) ^ [_263040] : [ssItem(_263040), 822 ^ _232197 : [(823 ^ _232197) ^ [_263211] : [ssItem(_263211), 826 ^ _232197 : [(827 ^ _232197) ^ [_263378] : [ssList(_263378), 830 ^ _232197 : [(831 ^ _232197) ^ [_263541] : [ssList(_263541), app(_263378, cons(_263040, cons(_263211, _263541))) = _262757, -(_263040 = _263211)]]]]]]]]]]], (861 ^ _232197) ^ [_264774] : [ssList(_264774), 864 ^ _232197 : [(865 ^ _232197) ^ [_264912] : [ssList(_264912), 868 ^ _232197 : [(869 ^ _232197) ^ [] : [neq(_264774, _264912), _264774 = _264912], (875 ^ _232197) ^ [] : [-(_264774 = _264912), -(neq(_264774, _264912))]]]]], (881 ^ _232197) ^ [_265365] : [ssList(_265365), 884 ^ _232197 : [(885 ^ _232197) ^ [_265497] : [ssItem(_265497), -(ssList(cons(_265497, _265365)))]]], (891 ^ _232197) ^ [] : [-(ssList(nil))], (893 ^ _232197) ^ [_265755] : [ssList(_265755), 896 ^ _232197 : [(897 ^ _232197) ^ [_265890] : [ssItem(_265890), cons(_265890, _265755) = _265755]]], (903 ^ _232197) ^ [_266098] : [ssList(_266098), 906 ^ _232197 : [(907 ^ _232197) ^ [_266266] : [ssList(_266266), 910 ^ _232197 : [(911 ^ _232197) ^ [_266430] : [ssItem(_266430), 914 ^ _232197 : [(915 ^ _232197) ^ [_266590] : [ssItem(_266590), cons(_266430, _266098) = cons(_266590, _266266), 922 ^ _232197 : [(923 ^ _232197) ^ [] : [-(_266430 = _266590)], (925 ^ _232197) ^ [] : [-(_266266 = _266098)]]]]]]]]], (927 ^ _232197) ^ [_267005] : [ssList(_267005), -(nil = _267005), 935 ^ _232197 : [(936 ^ _232197) ^ [] : [-(ssList(934 ^ [_267005]))], (939 ^ _232197) ^ [] : [-(ssItem(937 ^ [_267005]))], (941 ^ _232197) ^ [] : [-(cons(937 ^ [_267005], 934 ^ [_267005]) = _267005)]]], (943 ^ _232197) ^ [_267569] : [ssList(_267569), 946 ^ _232197 : [(947 ^ _232197) ^ [_267704] : [ssItem(_267704), nil = cons(_267704, _267569)]]], (953 ^ _232197) ^ [_267912] : [ssList(_267912), -(nil = _267912), -(ssItem(hd(_267912)))], (963 ^ _232197) ^ [_268190] : [ssList(_268190), 966 ^ _232197 : [(967 ^ _232197) ^ [_268325] : [ssItem(_268325), -(hd(cons(_268325, _268190)) = _268325)]]], (973 ^ _232197) ^ [_268536] : [ssList(_268536), -(nil = _268536), -(ssList(tl(_268536)))], (983 ^ _232197) ^ [_268814] : [ssList(_268814), 986 ^ _232197 : [(987 ^ _232197) ^ [_268949] : [ssItem(_268949), -(tl(cons(_268949, _268814)) = _268814)]]], (993 ^ _232197) ^ [_269160] : [ssList(_269160), 996 ^ _232197 : [(997 ^ _232197) ^ [_269292] : [ssList(_269292), -(ssList(app(_269160, _269292)))]]], (1003 ^ _232197) ^ [_269497] : [ssList(_269497), 1006 ^ _232197 : [(1007 ^ _232197) ^ [_269649] : [ssList(_269649), 1010 ^ _232197 : [(1011 ^ _232197) ^ [_269797] : [ssItem(_269797), -(cons(_269797, app(_269649, _269497)) = app(cons(_269797, _269649), _269497))]]]]], (1017 ^ _232197) ^ [_270035] : [ssList(_270035), -(app(nil, _270035) = _270035)], (1023 ^ _232197) ^ [_270229] : [ssItem(_270229), 1026 ^ _232197 : [(1027 ^ _232197) ^ [_270371] : [ssItem(_270371), -(_270229 = _270371), leq(_270229, _270371), leq(_270371, _270229)]]], (1041 ^ _232197) ^ [_270750] : [ssItem(_270750), 1044 ^ _232197 : [(1045 ^ _232197) ^ [_270902] : [ssItem(_270902), 1048 ^ _232197 : [(1049 ^ _232197) ^ [_271050] : [ssItem(_271050), -(leq(_270750, _271050)), leq(_270750, _270902), leq(_270902, _271050)]]]]], (1063 ^ _232197) ^ [_271450] : [ssItem(_271450), -(leq(_271450, _271450))], (1069 ^ _232197) ^ [_271638] : [ssItem(_271638), 1072 ^ _232197 : [(1073 ^ _232197) ^ [_271774] : [ssItem(_271774), 1076 ^ _232197 : [(1077 ^ _232197) ^ [] : [geq(_271638, _271774), -(leq(_271774, _271638))], (1083 ^ _232197) ^ [] : [leq(_271774, _271638), -(geq(_271638, _271774))]]]]], (1089 ^ _232197) ^ [_272225] : [ssItem(_272225), 1092 ^ _232197 : [(1093 ^ _232197) ^ [_272363] : [ssItem(_272363), lt(_272225, _272363), lt(_272363, _272225)]]], (1103 ^ _232197) ^ [_272654] : [ssItem(_272654), 1106 ^ _232197 : [(1107 ^ _232197) ^ [_272806] : [ssItem(_272806), 1110 ^ _232197 : [(1111 ^ _232197) ^ [_272954] : [ssItem(_272954), -(lt(_272654, _272954)), lt(_272654, _272806), lt(_272806, _272954)]]]]], (1125 ^ _232197) ^ [_273354] : [ssItem(_273354), 1128 ^ _232197 : [(1129 ^ _232197) ^ [_273490] : [ssItem(_273490), 1132 ^ _232197 : [(1133 ^ _232197) ^ [] : [gt(_273354, _273490), -(lt(_273490, _273354))], (1139 ^ _232197) ^ [] : [lt(_273490, _273354), -(gt(_273354, _273490))]]]]], (1145 ^ _232197) ^ [_273941] : [ssItem(_273941), 1148 ^ _232197 : [(1149 ^ _232197) ^ [_274096] : [ssList(_274096), 1152 ^ _232197 : [(1153 ^ _232197) ^ [_274247] : [ssList(_274247), 1156 ^ _232197 : [(1167 ^ _232197) ^ [] : [1168 ^ _232197 : [(1169 ^ _232197) ^ [] : [memberP(_274096, _273941)], (1171 ^ _232197) ^ [] : [memberP(_274247, _273941)]], -(memberP(app(_274096, _274247), _273941))], (1157 ^ _232197) ^ [] : [memberP(app(_274096, _274247), _273941), -(memberP(_274096, _273941)), -(memberP(_274247, _273941))]]]]]]], (1175 ^ _232197) ^ [_274894] : [ssItem(_274894), 1178 ^ _232197 : [(1179 ^ _232197) ^ [_275049] : [ssItem(_275049), 1182 ^ _232197 : [(1183 ^ _232197) ^ [_275200] : [ssList(_275200), 1186 ^ _232197 : [(1197 ^ _232197) ^ [] : [1198 ^ _232197 : [(1199 ^ _232197) ^ [] : [_274894 = _275049], (1201 ^ _232197) ^ [] : [memberP(_275200, _274894)]], -(memberP(cons(_275049, _275200), _274894))], (1187 ^ _232197) ^ [] : [memberP(cons(_275049, _275200), _274894), -(_274894 = _275049), -(memberP(_275200, _274894))]]]]]]], (1205 ^ _232197) ^ [_275847] : [ssItem(_275847), memberP(nil, _275847)], (1211 ^ _232197) ^ [] : [singletonP(nil)], (1213 ^ _232197) ^ [_276088] : [ssList(_276088), 1216 ^ _232197 : [(1217 ^ _232197) ^ [_276240] : [ssList(_276240), 1220 ^ _232197 : [(1221 ^ _232197) ^ [_276388] : [ssList(_276388), -(frontsegP(_276088, _276388)), frontsegP(_276088, _276240), frontsegP(_276240, _276388)]]]]], (1235 ^ _232197) ^ [_276788] : [ssList(_276788), 1238 ^ _232197 : [(1239 ^ _232197) ^ [_276930] : [ssList(_276930), -(_276788 = _276930), frontsegP(_276788, _276930), frontsegP(_276930, _276788)]]], (1253 ^ _232197) ^ [_277309] : [ssList(_277309), -(frontsegP(_277309, _277309))], (1259 ^ _232197) ^ [_277497] : [ssList(_277497), 1262 ^ _232197 : [(1263 ^ _232197) ^ [_277646] : [ssList(_277646), 1266 ^ _232197 : [(1267 ^ _232197) ^ [_277791] : [ssList(_277791), frontsegP(_277497, _277646), -(frontsegP(app(_277497, _277791), _277646))]]]]], (1277 ^ _232197) ^ [_278104] : [ssItem(_278104), 1280 ^ _232197 : [(1281 ^ _232197) ^ [_278272] : [ssItem(_278272), 1284 ^ _232197 : [(1285 ^ _232197) ^ [_278436] : [ssList(_278436), 1288 ^ _232197 : [(1289 ^ _232197) ^ [_278596] : [ssList(_278596), 1292 ^ _232197 : [(1293 ^ _232197) ^ [] : [frontsegP(cons(_278104, _278436), cons(_278272, _278596)), 1296 ^ _232197 : [(1297 ^ _232197) ^ [] : [-(_278104 = _278272)], (1299 ^ _232197) ^ [] : [-(frontsegP(_278436, _278596))]]], (1301 ^ _232197) ^ [] : [-(frontsegP(cons(_278104, _278436), cons(_278272, _278596))), _278104 = _278272, frontsegP(_278436, _278596)]]]]]]]]], (1311 ^ _232197) ^ [_279281] : [ssList(_279281), -(frontsegP(_279281, nil))], (1317 ^ _232197) ^ [_279469] : [ssList(_279469), 1320 ^ _232197 : [(1321 ^ _232197) ^ [] : [frontsegP(nil, _279469), -(nil = _279469)], (1327 ^ _232197) ^ [] : [nil = _279469, -(frontsegP(nil, _279469))]]], (1333 ^ _232197) ^ [_279897] : [ssList(_279897), 1336 ^ _232197 : [(1337 ^ _232197) ^ [_280049] : [ssList(_280049), 1340 ^ _232197 : [(1341 ^ _232197) ^ [_280197] : [ssList(_280197), -(rearsegP(_279897, _280197)), rearsegP(_279897, _280049), rearsegP(_280049, _280197)]]]]], (1355 ^ _232197) ^ [_280597] : [ssList(_280597), 1358 ^ _232197 : [(1359 ^ _232197) ^ [_280739] : [ssList(_280739), -(_280597 = _280739), rearsegP(_280597, _280739), rearsegP(_280739, _280597)]]], (1373 ^ _232197) ^ [_281118] : [ssList(_281118), -(rearsegP(_281118, _281118))], (1379 ^ _232197) ^ [_281306] : [ssList(_281306), 1382 ^ _232197 : [(1383 ^ _232197) ^ [_281455] : [ssList(_281455), 1386 ^ _232197 : [(1387 ^ _232197) ^ [_281600] : [ssList(_281600), rearsegP(_281306, _281455), -(rearsegP(app(_281600, _281306), _281455))]]]]], (1397 ^ _232197) ^ [_281913] : [ssList(_281913), -(rearsegP(_281913, nil))], (1403 ^ _232197) ^ [_282101] : [ssList(_282101), 1406 ^ _232197 : [(1407 ^ _232197) ^ [] : [rearsegP(nil, _282101), -(nil = _282101)], (1413 ^ _232197) ^ [] : [nil = _282101, -(rearsegP(nil, _282101))]]], (1419 ^ _232197) ^ [_282529] : [ssList(_282529), 1422 ^ _232197 : [(1423 ^ _232197) ^ [_282681] : [ssList(_282681), 1426 ^ _232197 : [(1427 ^ _232197) ^ [_282829] : [ssList(_282829), -(segmentP(_282529, _282829)), segmentP(_282529, _282681), segmentP(_282681, _282829)]]]]], (1441 ^ _232197) ^ [_283229] : [ssList(_283229), 1444 ^ _232197 : [(1445 ^ _232197) ^ [_283371] : [ssList(_283371), -(_283229 = _283371), segmentP(_283229, _283371), segmentP(_283371, _283229)]]], (1459 ^ _232197) ^ [_283750] : [ssList(_283750), -(segmentP(_283750, _283750))], (1465 ^ _232197) ^ [_283938] : [ssList(_283938), 1468 ^ _232197 : [(1469 ^ _232197) ^ [_284100] : [ssList(_284100), 1472 ^ _232197 : [(1473 ^ _232197) ^ [_284258] : [ssList(_284258), 1476 ^ _232197 : [(1477 ^ _232197) ^ [_284412] : [ssList(_284412), segmentP(_283938, _284100), -(segmentP(app(app(_284258, _283938), _284412), _284100))]]]]]]], (1487 ^ _232197) ^ [_284748] : [ssList(_284748), -(segmentP(_284748, nil))], (1493 ^ _232197) ^ [_284936] : [ssList(_284936), 1496 ^ _232197 : [(1497 ^ _232197) ^ [] : [segmentP(nil, _284936), -(nil = _284936)], (1503 ^ _232197) ^ [] : [nil = _284936, -(segmentP(nil, _284936))]]], (1509 ^ _232197) ^ [_285364] : [ssItem(_285364), -(cyclefreeP(cons(_285364, nil)))], (1515 ^ _232197) ^ [] : [-(cyclefreeP(nil))], (1517 ^ _232197) ^ [_285609] : [ssItem(_285609), -(totalorderP(cons(_285609, nil)))], (1523 ^ _232197) ^ [] : [-(totalorderP(nil))], (1525 ^ _232197) ^ [_285854] : [ssItem(_285854), -(strictorderP(cons(_285854, nil)))], (1531 ^ _232197) ^ [] : [-(strictorderP(nil))], (1533 ^ _232197) ^ [_286099] : [ssItem(_286099), -(totalorderedP(cons(_286099, nil)))], (1539 ^ _232197) ^ [] : [-(totalorderedP(nil))], (1541 ^ _232197) ^ [_286344] : [ssItem(_286344), 1544 ^ _232197 : [(1545 ^ _232197) ^ [_286503] : [ssList(_286503), 1548 ^ _232197 : [(1549 ^ _232197) ^ [] : [totalorderedP(cons(_286344, _286503)), -(nil = _286503), 1556 ^ _232197 : [(1557 ^ _232197) ^ [] : [nil = _286503], (1559 ^ _232197) ^ [] : [-(totalorderedP(_286503))], (1561 ^ _232197) ^ [] : [-(leq(_286344, hd(_286503)))]]], (1563 ^ _232197) ^ [] : [-(totalorderedP(cons(_286344, _286503))), 1564 ^ _232197 : [(1565 ^ _232197) ^ [] : [nil = _286503], (1567 ^ _232197) ^ [] : [-(nil = _286503), totalorderedP(_286503), leq(_286344, hd(_286503))]]]]]]], (1579 ^ _232197) ^ [_287438] : [ssItem(_287438), -(strictorderedP(cons(_287438, nil)))], (1585 ^ _232197) ^ [] : [-(strictorderedP(nil))], (1587 ^ _232197) ^ [_287683] : [ssItem(_287683), 1590 ^ _232197 : [(1591 ^ _232197) ^ [_287842] : [ssList(_287842), 1594 ^ _232197 : [(1595 ^ _232197) ^ [] : [strictorderedP(cons(_287683, _287842)), -(nil = _287842), 1602 ^ _232197 : [(1603 ^ _232197) ^ [] : [nil = _287842], (1605 ^ _232197) ^ [] : [-(strictorderedP(_287842))], (1607 ^ _232197) ^ [] : [-(lt(_287683, hd(_287842)))]]], (1609 ^ _232197) ^ [] : [-(strictorderedP(cons(_287683, _287842))), 1610 ^ _232197 : [(1611 ^ _232197) ^ [] : [nil = _287842], (1613 ^ _232197) ^ [] : [-(nil = _287842), strictorderedP(_287842), lt(_287683, hd(_287842))]]]]]]], (1625 ^ _232197) ^ [_288777] : [ssItem(_288777), -(duplicatefreeP(cons(_288777, nil)))], (1631 ^ _232197) ^ [] : [-(duplicatefreeP(nil))], (1633 ^ _232197) ^ [_289022] : [ssItem(_289022), -(equalelemsP(cons(_289022, nil)))], (1639 ^ _232197) ^ [] : [-(equalelemsP(nil))], (1641 ^ _232197) ^ [_289267] : [ssList(_289267), -(nil = _289267), 1649 ^ _232197 : [(1650 ^ _232197) ^ [] : [-(ssItem(1648 ^ [_289267]))], (1652 ^ _232197) ^ [] : [-(hd(_289267) = 1648 ^ [_289267])]]], (1654 ^ _232197) ^ [_289681] : [ssList(_289681), -(nil = _289681), 1662 ^ _232197 : [(1663 ^ _232197) ^ [] : [-(ssList(1661 ^ [_289681]))], (1665 ^ _232197) ^ [] : [-(tl(_289681) = 1661 ^ [_289681])]]], (1667 ^ _232197) ^ [_290095] : [ssList(_290095), 1670 ^ _232197 : [(1671 ^ _232197) ^ [_290261] : [ssList(_290261), -(_290261 = _290095), -(nil = _290261), -(nil = _290095), hd(_290261) = hd(_290095), tl(_290261) = tl(_290095)]]], (1693 ^ _232197) ^ [_290840] : [ssList(_290840), -(nil = _290840), -(cons(hd(_290840), tl(_290840)) = _290840)], (1703 ^ _232197) ^ [_291130] : [ssList(_291130), 1706 ^ _232197 : [(1707 ^ _232197) ^ [_291282] : [ssList(_291282), 1710 ^ _232197 : [(1711 ^ _232197) ^ [_291430] : [ssList(_291430), app(_291430, _291282) = app(_291130, _291282), -(_291430 = _291130)]]]]], (1721 ^ _232197) ^ [_291749] : [ssList(_291749), 1724 ^ _232197 : [(1725 ^ _232197) ^ [_291901] : [ssList(_291901), 1728 ^ _232197 : [(1729 ^ _232197) ^ [_292049] : [ssList(_292049), app(_291901, _292049) = app(_291901, _291749), -(_292049 = _291749)]]]]], (1739 ^ _232197) ^ [_292368] : [ssList(_292368), 1742 ^ _232197 : [(1743 ^ _232197) ^ [_292507] : [ssItem(_292507), -(cons(_292507, _292368) = app(cons(_292507, nil), _292368))]]], (1749 ^ _232197) ^ [_292726] : [ssList(_292726), 1752 ^ _232197 : [(1753 ^ _232197) ^ [_292878] : [ssList(_292878), 1756 ^ _232197 : [(1757 ^ _232197) ^ [_293026] : [ssList(_293026), -(app(app(_292726, _292878), _293026) = app(_292726, app(_292878, _293026)))]]]]], (1763 ^ _232197) ^ [_293264] : [ssList(_293264), 1766 ^ _232197 : [(1767 ^ _232197) ^ [_293409] : [ssList(_293409), 1770 ^ _232197 : [(1771 ^ _232197) ^ [] : [nil = app(_293264, _293409), 1774 ^ _232197 : [(1775 ^ _232197) ^ [] : [-(nil = _293409)], (1777 ^ _232197) ^ [] : [-(nil = _293264)]]], (1779 ^ _232197) ^ [] : [-(nil = app(_293264, _293409)), nil = _293409, nil = _293264]]]]], (1789 ^ _232197) ^ [_294027] : [ssList(_294027), -(app(_294027, nil) = _294027)], (1795 ^ _232197) ^ [_294221] : [ssList(_294221), 1798 ^ _232197 : [(1799 ^ _232197) ^ [_294366] : [ssList(_294366), -(nil = _294221), -(hd(app(_294221, _294366)) = hd(_294221))]]], (1809 ^ _232197) ^ [_294673] : [ssList(_294673), 1812 ^ _232197 : [(1813 ^ _232197) ^ [_294821] : [ssList(_294821), -(nil = _294673), -(tl(app(_294673, _294821)) = app(tl(_294673), _294821))]]], (1823 ^ _232197) ^ [_295134] : [ssItem(_295134), 1826 ^ _232197 : [(1827 ^ _232197) ^ [_295276] : [ssItem(_295276), -(_295134 = _295276), geq(_295134, _295276), geq(_295276, _295134)]]], (1841 ^ _232197) ^ [_295655] : [ssItem(_295655), 1844 ^ _232197 : [(1845 ^ _232197) ^ [_295807] : [ssItem(_295807), 1848 ^ _232197 : [(1849 ^ _232197) ^ [_295955] : [ssItem(_295955), -(geq(_295655, _295955)), geq(_295655, _295807), geq(_295807, _295955)]]]]], (1863 ^ _232197) ^ [_296355] : [ssItem(_296355), -(geq(_296355, _296355))], (1869 ^ _232197) ^ [_296543] : [ssItem(_296543), lt(_296543, _296543)], (1875 ^ _232197) ^ [_296732] : [ssItem(_296732), 1878 ^ _232197 : [(1879 ^ _232197) ^ [_296884] : [ssItem(_296884), 1882 ^ _232197 : [(1883 ^ _232197) ^ [_297032] : [ssItem(_297032), -(lt(_296732, _297032)), leq(_296732, _296884), lt(_296884, _297032)]]]]], (1897 ^ _232197) ^ [_297432] : [ssItem(_297432), 1900 ^ _232197 : [(1901 ^ _232197) ^ [_297574] : [ssItem(_297574), leq(_297432, _297574), -(_297432 = _297574), -(lt(_297432, _297574))]]], (1915 ^ _232197) ^ [_297954] : [ssItem(_297954), 1918 ^ _232197 : [(1919 ^ _232197) ^ [_298098] : [ssItem(_298098), 1922 ^ _232197 : [(1923 ^ _232197) ^ [] : [lt(_297954, _298098), 1926 ^ _232197 : [(1927 ^ _232197) ^ [] : [_297954 = _298098], (1929 ^ _232197) ^ [] : [-(leq(_297954, _298098))]]], (1931 ^ _232197) ^ [] : [-(lt(_297954, _298098)), -(_297954 = _298098), leq(_297954, _298098)]]]]], (1941 ^ _232197) ^ [_298709] : [ssItem(_298709), 1944 ^ _232197 : [(1945 ^ _232197) ^ [_298847] : [ssItem(_298847), gt(_298709, _298847), gt(_298847, _298709)]]], (1955 ^ _232197) ^ [_299118] : [ssItem(_299118), 1958 ^ _232197 : [(1959 ^ _232197) ^ [_299270] : [ssItem(_299270), 1962 ^ _232197 : [(1963 ^ _232197) ^ [_299418] : [ssItem(_299418), -(gt(_299118, _299418)), gt(_299118, _299270), gt(_299270, _299418)]]]]]], input).
% 0.39/1.38 ncf('1',plain,[frontsegP(1979 ^ [], 1976 ^ [])],start(2017 ^ 0)).
% 0.39/1.38 ncf('1.1',plain,[-(frontsegP(1979 ^ [], 1976 ^ [])), frontsegP(1985 ^ [], 1982 ^ []), 1985 ^ [] = 1979 ^ [], 1982 ^ [] = 1976 ^ []],extension(232 ^ 1,bind([[_239475, _239477, _239479, _239481], [1976 ^ [], 1982 ^ [], 1979 ^ [], 1985 ^ []]]))).
% 0.39/1.38 ncf('1.1.1',plain,[-(frontsegP(1985 ^ [], 1982 ^ []))],extension(1995 ^ 2)).
% 0.39/1.38 ncf('1.1.2',plain,[-(1985 ^ [] = 1979 ^ []), 1979 ^ [] = 1985 ^ []],extension(4 ^ 2,bind([[_232448, _232450], [1985 ^ [], 1979 ^ []]]))).
% 0.39/1.38 ncf('1.1.2.1',plain,[-(1979 ^ [] = 1985 ^ [])],extension(1989 ^ 3)).
% 0.39/1.38 ncf('1.1.3',plain,[-(1982 ^ [] = 1976 ^ []), 1976 ^ [] = 1982 ^ []],extension(4 ^ 2,bind([[_232448, _232450], [1982 ^ [], 1976 ^ []]]))).
% 0.39/1.38 ncf('1.1.3.1',plain,[-(1976 ^ [] = 1982 ^ [])],extension(1991 ^ 3)).
% 0.39/1.38 %-----------------------------------------------------
% 0.39/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------