%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWC269+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n007.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:03 EDT 2023
% Result : Theorem 11.42s 11.72s
% Output : Proof 11.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWC269+1 : TPTP v8.1.2. Released v2.4.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n007.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Fri May 19 00:49:53 EDT 2023
% 0.12/0.34 % CPUTime :
% 11.42/11.72
% 11.42/11.72 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 11.42/11.72 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.42/11.72 %-----------------------------------------------------
% 11.42/11.72 ncf(matrix, plain, [(1978 ^ _232593) ^ [] : [-(ssList(1976 ^ []))], (1981 ^ _232593) ^ [] : [-(ssList(1979 ^ []))], (1984 ^ _232593) ^ [] : [-(ssList(1982 ^ []))], (1987 ^ _232593) ^ [] : [-(ssList(1985 ^ []))], (1989 ^ _232593) ^ [] : [-(1979 ^ [] = 1985 ^ [])], (1991 ^ _232593) ^ [] : [-(1976 ^ [] = 1982 ^ [])], (1993 ^ _232593) ^ [] : [-(frontsegP(1985 ^ [], 1982 ^ []))], (1995 ^ _232593) ^ [] : [-(totalorderedP(1982 ^ []))], (2015 ^ _232593) ^ [] : [totalorderedP(1976 ^ [])], (1997 ^ _232593) ^ [_301778] : [ssList(_301778), neq(1982 ^ [], _301778), frontsegP(1985 ^ [], _301778), segmentP(_301778, 1982 ^ []), totalorderedP(_301778)], (246 ^ _232593) ^ [_240397, _240399, _240401, _240403] : [-(cons(_240403, _240399) = cons(_240401, _240397)), _240403 = _240401, _240399 = _240397], (256 ^ _232593) ^ [_240728, _240730] : [_240730 = _240728, -(hd(_240730) = hd(_240728))], (272 ^ _232593) ^ [_241285, _241287] : [_241287 = _241285, -(tl(_241287) = tl(_241285))], (262 ^ _232593) ^ [_240974, _240976, _240978, _240980] : [-(app(_240980, _240976) = app(_240978, _240974)), _240980 = _240978, _240976 = _240974], (2 ^ _232593) ^ [_232737] : [-(_232737 = _232737)], (4 ^ _232593) ^ [_232844, _232846] : [_232846 = _232844, -(_232844 = _232846)], (10 ^ _232593) ^ [_233048, _233050, _233052] : [-(_233052 = _233048), _233052 = _233050, _233050 = _233048], (20 ^ _232593) ^ [_233389, _233391, _233393, _233395] : [-(memberP(_233393, _233389)), memberP(_233395, _233391), _233395 = _233393, _233391 = _233389], (34 ^ _232593) ^ [_233805, _233807] : [-(singletonP(_233805)), _233807 = _233805, singletonP(_233807)], (44 ^ _232593) ^ [_234128, _234130, _234132, _234134] : [-(rearsegP(_234132, _234128)), rearsegP(_234134, _234130), _234134 = _234132, _234130 = _234128], (58 ^ _232593) ^ [_234544, _234546] : [-(cyclefreeP(_234544)), _234546 = _234544, cyclefreeP(_234546)], (68 ^ _232593) ^ [_234839, _234841] : [-(totalorderP(_234839)), _234841 = _234839, totalorderP(_234841)], (78 ^ _232593) ^ [_235134, _235136] : [-(strictorderP(_235134)), _235136 = _235134, strictorderP(_235136)], (88 ^ _232593) ^ [_235429, _235431] : [-(strictorderedP(_235429)), _235431 = _235429, strictorderedP(_235431)], (98 ^ _232593) ^ [_235724, _235726] : [-(duplicatefreeP(_235724)), _235726 = _235724, duplicatefreeP(_235726)], (108 ^ _232593) ^ [_236019, _236021] : [-(equalelemsP(_236019)), _236021 = _236019, equalelemsP(_236021)], (118 ^ _232593) ^ [_236342, _236344, _236346, _236348] : [-(geq(_236346, _236342)), geq(_236348, _236344), _236348 = _236346, _236344 = _236342], (132 ^ _232593) ^ [_236786, _236788, _236790, _236792] : [-(lt(_236790, _236786)), lt(_236792, _236788), _236792 = _236790, _236788 = _236786], (146 ^ _232593) ^ [_237230, _237232, _237234, _237236] : [-(leq(_237234, _237230)), leq(_237236, _237232), _237236 = _237234, _237232 = _237230], (160 ^ _232593) ^ [_237646, _237648] : [-(ssItem(_237646)), _237648 = _237646, ssItem(_237648)], (170 ^ _232593) ^ [_237969, _237971, _237973, _237975] : [-(gt(_237973, _237969)), gt(_237975, _237971), _237975 = _237973, _237971 = _237969], (184 ^ _232593) ^ [_238385, _238387] : [-(ssList(_238385)), _238387 = _238385, ssList(_238387)], (194 ^ _232593) ^ [_238708, _238710, _238712, _238714] : [-(neq(_238712, _238708)), neq(_238714, _238710), _238714 = _238712, _238710 = _238708], (208 ^ _232593) ^ [_239152, _239154, _239156, _239158] : [-(frontsegP(_239156, _239152)), frontsegP(_239158, _239154), _239158 = _239156, _239154 = _239152], (236 ^ _232593) ^ [_239992, _239994] : [-(totalorderedP(_239992)), _239994 = _239992, totalorderedP(_239994)], (222 ^ _232593) ^ [_239596, _239598, _239600, _239602] : [-(segmentP(_239600, _239596)), segmentP(_239602, _239598), _239602 = _239600, _239598 = _239596], (278 ^ _232593) ^ [_241507] : [ssItem(_241507), 281 ^ _232593 : [(282 ^ _232593) ^ [_241645] : [ssItem(_241645), 285 ^ _232593 : [(286 ^ _232593) ^ [] : [neq(_241507, _241645), _241507 = _241645], (292 ^ _232593) ^ [] : [-(_241507 = _241645), -(neq(_241507, _241645))]]]]], (299 ^ _232593) ^ [] : [-(ssItem(297 ^ []))], (302 ^ _232593) ^ [] : [-(ssItem(300 ^ []))], (304 ^ _232593) ^ [] : [297 ^ [] = 300 ^ []], (306 ^ _232593) ^ [_242358] : [ssList(_242358), 309 ^ _232593 : [(310 ^ _232593) ^ [_242520] : [ssItem(_242520), 313 ^ _232593 : [(314 ^ _232593) ^ [] : [memberP(_242358, _242520), 318 ^ _232593 : [(319 ^ _232593) ^ [] : [-(ssList(317 ^ [_242358, _242520]))], (322 ^ _232593) ^ [] : [-(ssList(320 ^ [_242358, _242520]))], (324 ^ _232593) ^ [] : [-(app(317 ^ [_242358, _242520], cons(_242520, 320 ^ [_242358, _242520])) = _242358)]]], (326 ^ _232593) ^ [] : [-(memberP(_242358, _242520)), 327 ^ _232593 : [(328 ^ _232593) ^ [_243168] : [ssList(_243168), 331 ^ _232593 : [(332 ^ _232593) ^ [_243316] : [ssList(_243316), app(_243168, cons(_242520, _243316)) = _242358]]]]]]]]], (340 ^ _232593) ^ [_243607] : [ssList(_243607), 343 ^ _232593 : [(344 ^ _232593) ^ [] : [singletonP(_243607), 348 ^ _232593 : [(349 ^ _232593) ^ [] : [-(ssItem(347 ^ [_243607]))], (351 ^ _232593) ^ [] : [-(cons(347 ^ [_243607], nil) = _243607)]]], (353 ^ _232593) ^ [] : [-(singletonP(_243607)), 354 ^ _232593 : [(355 ^ _232593) ^ [_244056] : [ssItem(_244056), cons(_244056, nil) = _243607]]]]], (363 ^ _232593) ^ [_244312] : [ssList(_244312), 366 ^ _232593 : [(367 ^ _232593) ^ [_244461] : [ssList(_244461), 370 ^ _232593 : [(371 ^ _232593) ^ [] : [frontsegP(_244312, _244461), 375 ^ _232593 : [(376 ^ _232593) ^ [] : [-(ssList(374 ^ [_244312, _244461]))], (378 ^ _232593) ^ [] : [-(app(_244461, 374 ^ [_244312, _244461]) = _244312)]]], (380 ^ _232593) ^ [] : [-(frontsegP(_244312, _244461)), 381 ^ _232593 : [(382 ^ _232593) ^ [_244936] : [ssList(_244936), app(_244461, _244936) = _244312]]]]]]], (390 ^ _232593) ^ [_245208] : [ssList(_245208), 393 ^ _232593 : [(394 ^ _232593) ^ [_245357] : [ssList(_245357), 397 ^ _232593 : [(398 ^ _232593) ^ [] : [rearsegP(_245208, _245357), 402 ^ _232593 : [(403 ^ _232593) ^ [] : [-(ssList(401 ^ [_245208, _245357]))], (405 ^ _232593) ^ [] : [-(app(401 ^ [_245208, _245357], _245357) = _245208)]]], (407 ^ _232593) ^ [] : [-(rearsegP(_245208, _245357)), 408 ^ _232593 : [(409 ^ _232593) ^ [_245832] : [ssList(_245832), app(_245832, _245357) = _245208]]]]]]], (417 ^ _232593) ^ [_246104] : [ssList(_246104), 420 ^ _232593 : [(421 ^ _232593) ^ [_246266] : [ssList(_246266), 424 ^ _232593 : [(425 ^ _232593) ^ [] : [segmentP(_246104, _246266), 429 ^ _232593 : [(430 ^ _232593) ^ [] : [-(ssList(428 ^ [_246104, _246266]))], (433 ^ _232593) ^ [] : [-(ssList(431 ^ [_246104, _246266]))], (435 ^ _232593) ^ [] : [-(app(app(428 ^ [_246104, _246266], _246266), 431 ^ [_246104, _246266]) = _246104)]]], (437 ^ _232593) ^ [] : [-(segmentP(_246104, _246266)), 438 ^ _232593 : [(439 ^ _232593) ^ [_246914] : [ssList(_246914), 442 ^ _232593 : [(443 ^ _232593) ^ [_247062] : [ssList(_247062), app(app(_246914, _246266), _247062) = _246104]]]]]]]]], (451 ^ _232593) ^ [_247353] : [ssList(_247353), 454 ^ _232593 : [(489 ^ _232593) ^ [] : [491 ^ _232593 : [(492 ^ _232593) ^ [] : [-(ssItem(490 ^ [_247353]))], (495 ^ _232593) ^ [] : [-(ssItem(493 ^ [_247353]))], (498 ^ _232593) ^ [] : [-(ssList(496 ^ [_247353]))], (501 ^ _232593) ^ [] : [-(ssList(499 ^ [_247353]))], (504 ^ _232593) ^ [] : [-(ssList(502 ^ [_247353]))], (506 ^ _232593) ^ [] : [-(app(app(496 ^ [_247353], cons(490 ^ [_247353], 499 ^ [_247353])), cons(493 ^ [_247353], 502 ^ [_247353])) = _247353)], (508 ^ _232593) ^ [] : [-(leq(490 ^ [_247353], 493 ^ [_247353]))], (510 ^ _232593) ^ [] : [-(leq(493 ^ [_247353], 490 ^ [_247353]))]], -(cyclefreeP(_247353))], (455 ^ _232593) ^ [] : [cyclefreeP(_247353), 458 ^ _232593 : [(459 ^ _232593) ^ [_247657] : [ssItem(_247657), 462 ^ _232593 : [(463 ^ _232593) ^ [_247849] : [ssItem(_247849), 466 ^ _232593 : [(467 ^ _232593) ^ [_248037] : [ssList(_248037), 470 ^ _232593 : [(471 ^ _232593) ^ [_248221] : [ssList(_248221), 474 ^ _232593 : [(475 ^ _232593) ^ [_248401] : [ssList(_248401), app(app(_248037, cons(_247657, _248221)), cons(_247849, _248401)) = _247353, leq(_247657, _247849), leq(_247849, _247657)]]]]]]]]]]]]], (514 ^ _232593) ^ [_250139] : [ssList(_250139), 517 ^ _232593 : [(552 ^ _232593) ^ [] : [554 ^ _232593 : [(555 ^ _232593) ^ [] : [-(ssItem(553 ^ [_250139]))], (558 ^ _232593) ^ [] : [-(ssItem(556 ^ [_250139]))], (561 ^ _232593) ^ [] : [-(ssList(559 ^ [_250139]))], (564 ^ _232593) ^ [] : [-(ssList(562 ^ [_250139]))], (567 ^ _232593) ^ [] : [-(ssList(565 ^ [_250139]))], (569 ^ _232593) ^ [] : [-(app(app(559 ^ [_250139], cons(553 ^ [_250139], 562 ^ [_250139])), cons(556 ^ [_250139], 565 ^ [_250139])) = _250139)], (571 ^ _232593) ^ [] : [leq(553 ^ [_250139], 556 ^ [_250139])], (573 ^ _232593) ^ [] : [leq(556 ^ [_250139], 553 ^ [_250139])]], -(totalorderP(_250139))], (518 ^ _232593) ^ [] : [totalorderP(_250139), 521 ^ _232593 : [(522 ^ _232593) ^ [_250441] : [ssItem(_250441), 525 ^ _232593 : [(526 ^ _232593) ^ [_250631] : [ssItem(_250631), 529 ^ _232593 : [(530 ^ _232593) ^ [_250817] : [ssList(_250817), 533 ^ _232593 : [(534 ^ _232593) ^ [_250999] : [ssList(_250999), 537 ^ _232593 : [(538 ^ _232593) ^ [_251177] : [ssList(_251177), app(app(_250817, cons(_250441, _250999)), cons(_250631, _251177)) = _250139, -(leq(_250441, _250631)), -(leq(_250631, _250441))]]]]]]]]]]]]], (577 ^ _232593) ^ [_252903] : [ssList(_252903), 580 ^ _232593 : [(615 ^ _232593) ^ [] : [617 ^ _232593 : [(618 ^ _232593) ^ [] : [-(ssItem(616 ^ [_252903]))], (621 ^ _232593) ^ [] : [-(ssItem(619 ^ [_252903]))], (624 ^ _232593) ^ [] : [-(ssList(622 ^ [_252903]))], (627 ^ _232593) ^ [] : [-(ssList(625 ^ [_252903]))], (630 ^ _232593) ^ [] : [-(ssList(628 ^ [_252903]))], (632 ^ _232593) ^ [] : [-(app(app(622 ^ [_252903], cons(616 ^ [_252903], 625 ^ [_252903])), cons(619 ^ [_252903], 628 ^ [_252903])) = _252903)], (634 ^ _232593) ^ [] : [lt(616 ^ [_252903], 619 ^ [_252903])], (636 ^ _232593) ^ [] : [lt(619 ^ [_252903], 616 ^ [_252903])]], -(strictorderP(_252903))], (581 ^ _232593) ^ [] : [strictorderP(_252903), 584 ^ _232593 : [(585 ^ _232593) ^ [_253205] : [ssItem(_253205), 588 ^ _232593 : [(589 ^ _232593) ^ [_253395] : [ssItem(_253395), 592 ^ _232593 : [(593 ^ _232593) ^ [_253581] : [ssList(_253581), 596 ^ _232593 : [(597 ^ _232593) ^ [_253763] : [ssList(_253763), 600 ^ _232593 : [(601 ^ _232593) ^ [_253941] : [ssList(_253941), app(app(_253581, cons(_253205, _253763)), cons(_253395, _253941)) = _252903, -(lt(_253205, _253395)), -(lt(_253395, _253205))]]]]]]]]]]]]], (640 ^ _232593) ^ [_255667] : [ssList(_255667), 643 ^ _232593 : [(674 ^ _232593) ^ [] : [676 ^ _232593 : [(677 ^ _232593) ^ [] : [-(ssItem(675 ^ [_255667]))], (680 ^ _232593) ^ [] : [-(ssItem(678 ^ [_255667]))], (683 ^ _232593) ^ [] : [-(ssList(681 ^ [_255667]))], (686 ^ _232593) ^ [] : [-(ssList(684 ^ [_255667]))], (689 ^ _232593) ^ [] : [-(ssList(687 ^ [_255667]))], (691 ^ _232593) ^ [] : [-(app(app(681 ^ [_255667], cons(675 ^ [_255667], 684 ^ [_255667])), cons(678 ^ [_255667], 687 ^ [_255667])) = _255667)], (693 ^ _232593) ^ [] : [leq(675 ^ [_255667], 678 ^ [_255667])]], -(totalorderedP(_255667))], (644 ^ _232593) ^ [] : [totalorderedP(_255667), 647 ^ _232593 : [(648 ^ _232593) ^ [_255963] : [ssItem(_255963), 651 ^ _232593 : [(652 ^ _232593) ^ [_256147] : [ssItem(_256147), 655 ^ _232593 : [(656 ^ _232593) ^ [_256327] : [ssList(_256327), 659 ^ _232593 : [(660 ^ _232593) ^ [_256503] : [ssList(_256503), 663 ^ _232593 : [(664 ^ _232593) ^ [_256675] : [ssList(_256675), app(app(_256327, cons(_255963, _256503)), cons(_256147, _256675)) = _255667, -(leq(_255963, _256147))]]]]]]]]]]]]], (697 ^ _232593) ^ [_258155] : [ssList(_258155), 700 ^ _232593 : [(731 ^ _232593) ^ [] : [733 ^ _232593 : [(734 ^ _232593) ^ [] : [-(ssItem(732 ^ [_258155]))], (737 ^ _232593) ^ [] : [-(ssItem(735 ^ [_258155]))], (740 ^ _232593) ^ [] : [-(ssList(738 ^ [_258155]))], (743 ^ _232593) ^ [] : [-(ssList(741 ^ [_258155]))], (746 ^ _232593) ^ [] : [-(ssList(744 ^ [_258155]))], (748 ^ _232593) ^ [] : [-(app(app(738 ^ [_258155], cons(732 ^ [_258155], 741 ^ [_258155])), cons(735 ^ [_258155], 744 ^ [_258155])) = _258155)], (750 ^ _232593) ^ [] : [lt(732 ^ [_258155], 735 ^ [_258155])]], -(strictorderedP(_258155))], (701 ^ _232593) ^ [] : [strictorderedP(_258155), 704 ^ _232593 : [(705 ^ _232593) ^ [_258451] : [ssItem(_258451), 708 ^ _232593 : [(709 ^ _232593) ^ [_258635] : [ssItem(_258635), 712 ^ _232593 : [(713 ^ _232593) ^ [_258815] : [ssList(_258815), 716 ^ _232593 : [(717 ^ _232593) ^ [_258991] : [ssList(_258991), 720 ^ _232593 : [(721 ^ _232593) ^ [_259163] : [ssList(_259163), app(app(_258815, cons(_258451, _258991)), cons(_258635, _259163)) = _258155, -(lt(_258451, _258635))]]]]]]]]]]]]], (754 ^ _232593) ^ [_260643] : [ssList(_260643), 757 ^ _232593 : [(788 ^ _232593) ^ [] : [790 ^ _232593 : [(791 ^ _232593) ^ [] : [-(ssItem(789 ^ [_260643]))], (794 ^ _232593) ^ [] : [-(ssItem(792 ^ [_260643]))], (797 ^ _232593) ^ [] : [-(ssList(795 ^ [_260643]))], (800 ^ _232593) ^ [] : [-(ssList(798 ^ [_260643]))], (803 ^ _232593) ^ [] : [-(ssList(801 ^ [_260643]))], (805 ^ _232593) ^ [] : [-(app(app(795 ^ [_260643], cons(789 ^ [_260643], 798 ^ [_260643])), cons(792 ^ [_260643], 801 ^ [_260643])) = _260643)], (807 ^ _232593) ^ [] : [-(789 ^ [_260643] = 792 ^ [_260643])]], -(duplicatefreeP(_260643))], (758 ^ _232593) ^ [] : [duplicatefreeP(_260643), 761 ^ _232593 : [(762 ^ _232593) ^ [_260941] : [ssItem(_260941), 765 ^ _232593 : [(766 ^ _232593) ^ [_261127] : [ssItem(_261127), 769 ^ _232593 : [(770 ^ _232593) ^ [_261309] : [ssList(_261309), 773 ^ _232593 : [(774 ^ _232593) ^ [_261487] : [ssList(_261487), 777 ^ _232593 : [(778 ^ _232593) ^ [_261661] : [ssList(_261661), app(app(_261309, cons(_260941, _261487)), cons(_261127, _261661)) = _260643, _260941 = _261127]]]]]]]]]]]]], (811 ^ _232593) ^ [_263153] : [ssList(_263153), 814 ^ _232593 : [(841 ^ _232593) ^ [] : [843 ^ _232593 : [(844 ^ _232593) ^ [] : [-(ssItem(842 ^ [_263153]))], (847 ^ _232593) ^ [] : [-(ssItem(845 ^ [_263153]))], (850 ^ _232593) ^ [] : [-(ssList(848 ^ [_263153]))], (853 ^ _232593) ^ [] : [-(ssList(851 ^ [_263153]))], (855 ^ _232593) ^ [] : [-(app(848 ^ [_263153], cons(842 ^ [_263153], cons(845 ^ [_263153], 851 ^ [_263153]))) = _263153)], (857 ^ _232593) ^ [] : [842 ^ [_263153] = 845 ^ [_263153]]], -(equalelemsP(_263153))], (815 ^ _232593) ^ [] : [equalelemsP(_263153), 818 ^ _232593 : [(819 ^ _232593) ^ [_263436] : [ssItem(_263436), 822 ^ _232593 : [(823 ^ _232593) ^ [_263607] : [ssItem(_263607), 826 ^ _232593 : [(827 ^ _232593) ^ [_263774] : [ssList(_263774), 830 ^ _232593 : [(831 ^ _232593) ^ [_263937] : [ssList(_263937), app(_263774, cons(_263436, cons(_263607, _263937))) = _263153, -(_263436 = _263607)]]]]]]]]]]], (861 ^ _232593) ^ [_265170] : [ssList(_265170), 864 ^ _232593 : [(865 ^ _232593) ^ [_265308] : [ssList(_265308), 868 ^ _232593 : [(869 ^ _232593) ^ [] : [neq(_265170, _265308), _265170 = _265308], (875 ^ _232593) ^ [] : [-(_265170 = _265308), -(neq(_265170, _265308))]]]]], (881 ^ _232593) ^ [_265761] : [ssList(_265761), 884 ^ _232593 : [(885 ^ _232593) ^ [_265893] : [ssItem(_265893), -(ssList(cons(_265893, _265761)))]]], (891 ^ _232593) ^ [] : [-(ssList(nil))], (893 ^ _232593) ^ [_266151] : [ssList(_266151), 896 ^ _232593 : [(897 ^ _232593) ^ [_266286] : [ssItem(_266286), cons(_266286, _266151) = _266151]]], (903 ^ _232593) ^ [_266494] : [ssList(_266494), 906 ^ _232593 : [(907 ^ _232593) ^ [_266662] : [ssList(_266662), 910 ^ _232593 : [(911 ^ _232593) ^ [_266826] : [ssItem(_266826), 914 ^ _232593 : [(915 ^ _232593) ^ [_266986] : [ssItem(_266986), cons(_266826, _266494) = cons(_266986, _266662), 922 ^ _232593 : [(923 ^ _232593) ^ [] : [-(_266826 = _266986)], (925 ^ _232593) ^ [] : [-(_266662 = _266494)]]]]]]]]], (927 ^ _232593) ^ [_267401] : [ssList(_267401), -(nil = _267401), 935 ^ _232593 : [(936 ^ _232593) ^ [] : [-(ssList(934 ^ [_267401]))], (939 ^ _232593) ^ [] : [-(ssItem(937 ^ [_267401]))], (941 ^ _232593) ^ [] : [-(cons(937 ^ [_267401], 934 ^ [_267401]) = _267401)]]], (943 ^ _232593) ^ [_267965] : [ssList(_267965), 946 ^ _232593 : [(947 ^ _232593) ^ [_268100] : [ssItem(_268100), nil = cons(_268100, _267965)]]], (953 ^ _232593) ^ [_268308] : [ssList(_268308), -(nil = _268308), -(ssItem(hd(_268308)))], (963 ^ _232593) ^ [_268586] : [ssList(_268586), 966 ^ _232593 : [(967 ^ _232593) ^ [_268721] : [ssItem(_268721), -(hd(cons(_268721, _268586)) = _268721)]]], (973 ^ _232593) ^ [_268932] : [ssList(_268932), -(nil = _268932), -(ssList(tl(_268932)))], (983 ^ _232593) ^ [_269210] : [ssList(_269210), 986 ^ _232593 : [(987 ^ _232593) ^ [_269345] : [ssItem(_269345), -(tl(cons(_269345, _269210)) = _269210)]]], (993 ^ _232593) ^ [_269556] : [ssList(_269556), 996 ^ _232593 : [(997 ^ _232593) ^ [_269688] : [ssList(_269688), -(ssList(app(_269556, _269688)))]]], (1003 ^ _232593) ^ [_269893] : [ssList(_269893), 1006 ^ _232593 : [(1007 ^ _232593) ^ [_270045] : [ssList(_270045), 1010 ^ _232593 : [(1011 ^ _232593) ^ [_270193] : [ssItem(_270193), -(cons(_270193, app(_270045, _269893)) = app(cons(_270193, _270045), _269893))]]]]], (1017 ^ _232593) ^ [_270431] : [ssList(_270431), -(app(nil, _270431) = _270431)], (1023 ^ _232593) ^ [_270625] : [ssItem(_270625), 1026 ^ _232593 : [(1027 ^ _232593) ^ [_270767] : [ssItem(_270767), -(_270625 = _270767), leq(_270625, _270767), leq(_270767, _270625)]]], (1041 ^ _232593) ^ [_271146] : [ssItem(_271146), 1044 ^ _232593 : [(1045 ^ _232593) ^ [_271298] : [ssItem(_271298), 1048 ^ _232593 : [(1049 ^ _232593) ^ [_271446] : [ssItem(_271446), -(leq(_271146, _271446)), leq(_271146, _271298), leq(_271298, _271446)]]]]], (1063 ^ _232593) ^ [_271846] : [ssItem(_271846), -(leq(_271846, _271846))], (1069 ^ _232593) ^ [_272034] : [ssItem(_272034), 1072 ^ _232593 : [(1073 ^ _232593) ^ [_272170] : [ssItem(_272170), 1076 ^ _232593 : [(1077 ^ _232593) ^ [] : [geq(_272034, _272170), -(leq(_272170, _272034))], (1083 ^ _232593) ^ [] : [leq(_272170, _272034), -(geq(_272034, _272170))]]]]], (1089 ^ _232593) ^ [_272621] : [ssItem(_272621), 1092 ^ _232593 : [(1093 ^ _232593) ^ [_272759] : [ssItem(_272759), lt(_272621, _272759), lt(_272759, _272621)]]], (1103 ^ _232593) ^ [_273050] : [ssItem(_273050), 1106 ^ _232593 : [(1107 ^ _232593) ^ [_273202] : [ssItem(_273202), 1110 ^ _232593 : [(1111 ^ _232593) ^ [_273350] : [ssItem(_273350), -(lt(_273050, _273350)), lt(_273050, _273202), lt(_273202, _273350)]]]]], (1125 ^ _232593) ^ [_273750] : [ssItem(_273750), 1128 ^ _232593 : [(1129 ^ _232593) ^ [_273886] : [ssItem(_273886), 1132 ^ _232593 : [(1133 ^ _232593) ^ [] : [gt(_273750, _273886), -(lt(_273886, _273750))], (1139 ^ _232593) ^ [] : [lt(_273886, _273750), -(gt(_273750, _273886))]]]]], (1145 ^ _232593) ^ [_274337] : [ssItem(_274337), 1148 ^ _232593 : [(1149 ^ _232593) ^ [_274492] : [ssList(_274492), 1152 ^ _232593 : [(1153 ^ _232593) ^ [_274643] : [ssList(_274643), 1156 ^ _232593 : [(1167 ^ _232593) ^ [] : [1168 ^ _232593 : [(1169 ^ _232593) ^ [] : [memberP(_274492, _274337)], (1171 ^ _232593) ^ [] : [memberP(_274643, _274337)]], -(memberP(app(_274492, _274643), _274337))], (1157 ^ _232593) ^ [] : [memberP(app(_274492, _274643), _274337), -(memberP(_274492, _274337)), -(memberP(_274643, _274337))]]]]]]], (1175 ^ _232593) ^ [_275290] : [ssItem(_275290), 1178 ^ _232593 : [(1179 ^ _232593) ^ [_275445] : [ssItem(_275445), 1182 ^ _232593 : [(1183 ^ _232593) ^ [_275596] : [ssList(_275596), 1186 ^ _232593 : [(1197 ^ _232593) ^ [] : [1198 ^ _232593 : [(1199 ^ _232593) ^ [] : [_275290 = _275445], (1201 ^ _232593) ^ [] : [memberP(_275596, _275290)]], -(memberP(cons(_275445, _275596), _275290))], (1187 ^ _232593) ^ [] : [memberP(cons(_275445, _275596), _275290), -(_275290 = _275445), -(memberP(_275596, _275290))]]]]]]], (1205 ^ _232593) ^ [_276243] : [ssItem(_276243), memberP(nil, _276243)], (1211 ^ _232593) ^ [] : [singletonP(nil)], (1213 ^ _232593) ^ [_276484] : [ssList(_276484), 1216 ^ _232593 : [(1217 ^ _232593) ^ [_276636] : [ssList(_276636), 1220 ^ _232593 : [(1221 ^ _232593) ^ [_276784] : [ssList(_276784), -(frontsegP(_276484, _276784)), frontsegP(_276484, _276636), frontsegP(_276636, _276784)]]]]], (1235 ^ _232593) ^ [_277184] : [ssList(_277184), 1238 ^ _232593 : [(1239 ^ _232593) ^ [_277326] : [ssList(_277326), -(_277184 = _277326), frontsegP(_277184, _277326), frontsegP(_277326, _277184)]]], (1253 ^ _232593) ^ [_277705] : [ssList(_277705), -(frontsegP(_277705, _277705))], (1259 ^ _232593) ^ [_277893] : [ssList(_277893), 1262 ^ _232593 : [(1263 ^ _232593) ^ [_278042] : [ssList(_278042), 1266 ^ _232593 : [(1267 ^ _232593) ^ [_278187] : [ssList(_278187), frontsegP(_277893, _278042), -(frontsegP(app(_277893, _278187), _278042))]]]]], (1277 ^ _232593) ^ [_278500] : [ssItem(_278500), 1280 ^ _232593 : [(1281 ^ _232593) ^ [_278668] : [ssItem(_278668), 1284 ^ _232593 : [(1285 ^ _232593) ^ [_278832] : [ssList(_278832), 1288 ^ _232593 : [(1289 ^ _232593) ^ [_278992] : [ssList(_278992), 1292 ^ _232593 : [(1293 ^ _232593) ^ [] : [frontsegP(cons(_278500, _278832), cons(_278668, _278992)), 1296 ^ _232593 : [(1297 ^ _232593) ^ [] : [-(_278500 = _278668)], (1299 ^ _232593) ^ [] : [-(frontsegP(_278832, _278992))]]], (1301 ^ _232593) ^ [] : [-(frontsegP(cons(_278500, _278832), cons(_278668, _278992))), _278500 = _278668, frontsegP(_278832, _278992)]]]]]]]]], (1311 ^ _232593) ^ [_279677] : [ssList(_279677), -(frontsegP(_279677, nil))], (1317 ^ _232593) ^ [_279865] : [ssList(_279865), 1320 ^ _232593 : [(1321 ^ _232593) ^ [] : [frontsegP(nil, _279865), -(nil = _279865)], (1327 ^ _232593) ^ [] : [nil = _279865, -(frontsegP(nil, _279865))]]], (1333 ^ _232593) ^ [_280293] : [ssList(_280293), 1336 ^ _232593 : [(1337 ^ _232593) ^ [_280445] : [ssList(_280445), 1340 ^ _232593 : [(1341 ^ _232593) ^ [_280593] : [ssList(_280593), -(rearsegP(_280293, _280593)), rearsegP(_280293, _280445), rearsegP(_280445, _280593)]]]]], (1355 ^ _232593) ^ [_280993] : [ssList(_280993), 1358 ^ _232593 : [(1359 ^ _232593) ^ [_281135] : [ssList(_281135), -(_280993 = _281135), rearsegP(_280993, _281135), rearsegP(_281135, _280993)]]], (1373 ^ _232593) ^ [_281514] : [ssList(_281514), -(rearsegP(_281514, _281514))], (1379 ^ _232593) ^ [_281702] : [ssList(_281702), 1382 ^ _232593 : [(1383 ^ _232593) ^ [_281851] : [ssList(_281851), 1386 ^ _232593 : [(1387 ^ _232593) ^ [_281996] : [ssList(_281996), rearsegP(_281702, _281851), -(rearsegP(app(_281996, _281702), _281851))]]]]], (1397 ^ _232593) ^ [_282309] : [ssList(_282309), -(rearsegP(_282309, nil))], (1403 ^ _232593) ^ [_282497] : [ssList(_282497), 1406 ^ _232593 : [(1407 ^ _232593) ^ [] : [rearsegP(nil, _282497), -(nil = _282497)], (1413 ^ _232593) ^ [] : [nil = _282497, -(rearsegP(nil, _282497))]]], (1419 ^ _232593) ^ [_282925] : [ssList(_282925), 1422 ^ _232593 : [(1423 ^ _232593) ^ [_283077] : [ssList(_283077), 1426 ^ _232593 : [(1427 ^ _232593) ^ [_283225] : [ssList(_283225), -(segmentP(_282925, _283225)), segmentP(_282925, _283077), segmentP(_283077, _283225)]]]]], (1441 ^ _232593) ^ [_283625] : [ssList(_283625), 1444 ^ _232593 : [(1445 ^ _232593) ^ [_283767] : [ssList(_283767), -(_283625 = _283767), segmentP(_283625, _283767), segmentP(_283767, _283625)]]], (1459 ^ _232593) ^ [_284146] : [ssList(_284146), -(segmentP(_284146, _284146))], (1465 ^ _232593) ^ [_284334] : [ssList(_284334), 1468 ^ _232593 : [(1469 ^ _232593) ^ [_284496] : [ssList(_284496), 1472 ^ _232593 : [(1473 ^ _232593) ^ [_284654] : [ssList(_284654), 1476 ^ _232593 : [(1477 ^ _232593) ^ [_284808] : [ssList(_284808), segmentP(_284334, _284496), -(segmentP(app(app(_284654, _284334), _284808), _284496))]]]]]]], (1487 ^ _232593) ^ [_285144] : [ssList(_285144), -(segmentP(_285144, nil))], (1493 ^ _232593) ^ [_285332] : [ssList(_285332), 1496 ^ _232593 : [(1497 ^ _232593) ^ [] : [segmentP(nil, _285332), -(nil = _285332)], (1503 ^ _232593) ^ [] : [nil = _285332, -(segmentP(nil, _285332))]]], (1509 ^ _232593) ^ [_285760] : [ssItem(_285760), -(cyclefreeP(cons(_285760, nil)))], (1515 ^ _232593) ^ [] : [-(cyclefreeP(nil))], (1517 ^ _232593) ^ [_286005] : [ssItem(_286005), -(totalorderP(cons(_286005, nil)))], (1523 ^ _232593) ^ [] : [-(totalorderP(nil))], (1525 ^ _232593) ^ [_286250] : [ssItem(_286250), -(strictorderP(cons(_286250, nil)))], (1531 ^ _232593) ^ [] : [-(strictorderP(nil))], (1533 ^ _232593) ^ [_286495] : [ssItem(_286495), -(totalorderedP(cons(_286495, nil)))], (1539 ^ _232593) ^ [] : [-(totalorderedP(nil))], (1541 ^ _232593) ^ [_286740] : [ssItem(_286740), 1544 ^ _232593 : [(1545 ^ _232593) ^ [_286899] : [ssList(_286899), 1548 ^ _232593 : [(1549 ^ _232593) ^ [] : [totalorderedP(cons(_286740, _286899)), -(nil = _286899), 1556 ^ _232593 : [(1557 ^ _232593) ^ [] : [nil = _286899], (1559 ^ _232593) ^ [] : [-(totalorderedP(_286899))], (1561 ^ _232593) ^ [] : [-(leq(_286740, hd(_286899)))]]], (1563 ^ _232593) ^ [] : [-(totalorderedP(cons(_286740, _286899))), 1564 ^ _232593 : [(1565 ^ _232593) ^ [] : [nil = _286899], (1567 ^ _232593) ^ [] : [-(nil = _286899), totalorderedP(_286899), leq(_286740, hd(_286899))]]]]]]], (1579 ^ _232593) ^ [_287834] : [ssItem(_287834), -(strictorderedP(cons(_287834, nil)))], (1585 ^ _232593) ^ [] : [-(strictorderedP(nil))], (1587 ^ _232593) ^ [_288079] : [ssItem(_288079), 1590 ^ _232593 : [(1591 ^ _232593) ^ [_288238] : [ssList(_288238), 1594 ^ _232593 : [(1595 ^ _232593) ^ [] : [strictorderedP(cons(_288079, _288238)), -(nil = _288238), 1602 ^ _232593 : [(1603 ^ _232593) ^ [] : [nil = _288238], (1605 ^ _232593) ^ [] : [-(strictorderedP(_288238))], (1607 ^ _232593) ^ [] : [-(lt(_288079, hd(_288238)))]]], (1609 ^ _232593) ^ [] : [-(strictorderedP(cons(_288079, _288238))), 1610 ^ _232593 : [(1611 ^ _232593) ^ [] : [nil = _288238], (1613 ^ _232593) ^ [] : [-(nil = _288238), strictorderedP(_288238), lt(_288079, hd(_288238))]]]]]]], (1625 ^ _232593) ^ [_289173] : [ssItem(_289173), -(duplicatefreeP(cons(_289173, nil)))], (1631 ^ _232593) ^ [] : [-(duplicatefreeP(nil))], (1633 ^ _232593) ^ [_289418] : [ssItem(_289418), -(equalelemsP(cons(_289418, nil)))], (1639 ^ _232593) ^ [] : [-(equalelemsP(nil))], (1641 ^ _232593) ^ [_289663] : [ssList(_289663), -(nil = _289663), 1649 ^ _232593 : [(1650 ^ _232593) ^ [] : [-(ssItem(1648 ^ [_289663]))], (1652 ^ _232593) ^ [] : [-(hd(_289663) = 1648 ^ [_289663])]]], (1654 ^ _232593) ^ [_290077] : [ssList(_290077), -(nil = _290077), 1662 ^ _232593 : [(1663 ^ _232593) ^ [] : [-(ssList(1661 ^ [_290077]))], (1665 ^ _232593) ^ [] : [-(tl(_290077) = 1661 ^ [_290077])]]], (1667 ^ _232593) ^ [_290491] : [ssList(_290491), 1670 ^ _232593 : [(1671 ^ _232593) ^ [_290657] : [ssList(_290657), -(_290657 = _290491), -(nil = _290657), -(nil = _290491), hd(_290657) = hd(_290491), tl(_290657) = tl(_290491)]]], (1693 ^ _232593) ^ [_291236] : [ssList(_291236), -(nil = _291236), -(cons(hd(_291236), tl(_291236)) = _291236)], (1703 ^ _232593) ^ [_291526] : [ssList(_291526), 1706 ^ _232593 : [(1707 ^ _232593) ^ [_291678] : [ssList(_291678), 1710 ^ _232593 : [(1711 ^ _232593) ^ [_291826] : [ssList(_291826), app(_291826, _291678) = app(_291526, _291678), -(_291826 = _291526)]]]]], (1721 ^ _232593) ^ [_292145] : [ssList(_292145), 1724 ^ _232593 : [(1725 ^ _232593) ^ [_292297] : [ssList(_292297), 1728 ^ _232593 : [(1729 ^ _232593) ^ [_292445] : [ssList(_292445), app(_292297, _292445) = app(_292297, _292145), -(_292445 = _292145)]]]]], (1739 ^ _232593) ^ [_292764] : [ssList(_292764), 1742 ^ _232593 : [(1743 ^ _232593) ^ [_292903] : [ssItem(_292903), -(cons(_292903, _292764) = app(cons(_292903, nil), _292764))]]], (1749 ^ _232593) ^ [_293122] : [ssList(_293122), 1752 ^ _232593 : [(1753 ^ _232593) ^ [_293274] : [ssList(_293274), 1756 ^ _232593 : [(1757 ^ _232593) ^ [_293422] : [ssList(_293422), -(app(app(_293122, _293274), _293422) = app(_293122, app(_293274, _293422)))]]]]], (1763 ^ _232593) ^ [_293660] : [ssList(_293660), 1766 ^ _232593 : [(1767 ^ _232593) ^ [_293805] : [ssList(_293805), 1770 ^ _232593 : [(1771 ^ _232593) ^ [] : [nil = app(_293660, _293805), 1774 ^ _232593 : [(1775 ^ _232593) ^ [] : [-(nil = _293805)], (1777 ^ _232593) ^ [] : [-(nil = _293660)]]], (1779 ^ _232593) ^ [] : [-(nil = app(_293660, _293805)), nil = _293805, nil = _293660]]]]], (1789 ^ _232593) ^ [_294423] : [ssList(_294423), -(app(_294423, nil) = _294423)], (1795 ^ _232593) ^ [_294617] : [ssList(_294617), 1798 ^ _232593 : [(1799 ^ _232593) ^ [_294762] : [ssList(_294762), -(nil = _294617), -(hd(app(_294617, _294762)) = hd(_294617))]]], (1809 ^ _232593) ^ [_295069] : [ssList(_295069), 1812 ^ _232593 : [(1813 ^ _232593) ^ [_295217] : [ssList(_295217), -(nil = _295069), -(tl(app(_295069, _295217)) = app(tl(_295069), _295217))]]], (1823 ^ _232593) ^ [_295530] : [ssItem(_295530), 1826 ^ _232593 : [(1827 ^ _232593) ^ [_295672] : [ssItem(_295672), -(_295530 = _295672), geq(_295530, _295672), geq(_295672, _295530)]]], (1841 ^ _232593) ^ [_296051] : [ssItem(_296051), 1844 ^ _232593 : [(1845 ^ _232593) ^ [_296203] : [ssItem(_296203), 1848 ^ _232593 : [(1849 ^ _232593) ^ [_296351] : [ssItem(_296351), -(geq(_296051, _296351)), geq(_296051, _296203), geq(_296203, _296351)]]]]], (1863 ^ _232593) ^ [_296751] : [ssItem(_296751), -(geq(_296751, _296751))], (1869 ^ _232593) ^ [_296939] : [ssItem(_296939), lt(_296939, _296939)], (1875 ^ _232593) ^ [_297128] : [ssItem(_297128), 1878 ^ _232593 : [(1879 ^ _232593) ^ [_297280] : [ssItem(_297280), 1882 ^ _232593 : [(1883 ^ _232593) ^ [_297428] : [ssItem(_297428), -(lt(_297128, _297428)), leq(_297128, _297280), lt(_297280, _297428)]]]]], (1897 ^ _232593) ^ [_297828] : [ssItem(_297828), 1900 ^ _232593 : [(1901 ^ _232593) ^ [_297970] : [ssItem(_297970), leq(_297828, _297970), -(_297828 = _297970), -(lt(_297828, _297970))]]], (1915 ^ _232593) ^ [_298350] : [ssItem(_298350), 1918 ^ _232593 : [(1919 ^ _232593) ^ [_298494] : [ssItem(_298494), 1922 ^ _232593 : [(1923 ^ _232593) ^ [] : [lt(_298350, _298494), 1926 ^ _232593 : [(1927 ^ _232593) ^ [] : [_298350 = _298494], (1929 ^ _232593) ^ [] : [-(leq(_298350, _298494))]]], (1931 ^ _232593) ^ [] : [-(lt(_298350, _298494)), -(_298350 = _298494), leq(_298350, _298494)]]]]], (1941 ^ _232593) ^ [_299105] : [ssItem(_299105), 1944 ^ _232593 : [(1945 ^ _232593) ^ [_299243] : [ssItem(_299243), gt(_299105, _299243), gt(_299243, _299105)]]], (1955 ^ _232593) ^ [_299514] : [ssItem(_299514), 1958 ^ _232593 : [(1959 ^ _232593) ^ [_299666] : [ssItem(_299666), 1962 ^ _232593 : [(1963 ^ _232593) ^ [_299814] : [ssItem(_299814), -(gt(_299514, _299814)), gt(_299514, _299666), gt(_299666, _299814)]]]]]], input).
% 11.42/11.72 ncf('1',plain,[ssList(1976 ^ []), 865 : ssList(1976 ^ []), 869 : neq(1976 ^ [], 1976 ^ []), 869 : 1976 ^ [] = 1976 ^ []],start(861 ^ 0,bind([[_265170, _265308], [1976 ^ [], 1976 ^ []]]))).
% 11.42/11.72 ncf('1.1',plain,[-(ssList(1976 ^ []))],extension(1978 ^ 1)).
% 11.42/11.72 ncf('1.2',plain,[-(ssList(1976 ^ []))],extension(1978 ^ 3)).
% 11.42/11.72 ncf('1.3',plain,[-(neq(1976 ^ [], 1976 ^ [])), -(1976 ^ [] = 1976 ^ [])],extension(875 ^ 5)).
% 11.42/11.72 ncf('1.3.1',plain,[1976 ^ [] = 1976 ^ [], -(1982 ^ [] = 1976 ^ []), 1982 ^ [] = 1976 ^ []],extension(10 ^ 6,bind([[_233048, _233050, _233052], [1976 ^ [], 1976 ^ [], 1982 ^ []]]))).
% 11.42/11.72 ncf('1.3.1.1',plain,[1982 ^ [] = 1976 ^ [], -(totalorderedP(1976 ^ [])), totalorderedP(1982 ^ [])],extension(236 ^ 7,bind([[_239992, _239994], [1976 ^ [], 1982 ^ []]]))).
% 11.42/11.72 ncf('1.3.1.1.1',plain,[totalorderedP(1976 ^ [])],extension(2015 ^ 8)).
% 11.42/11.72 ncf('1.3.1.1.2',plain,[-(totalorderedP(1982 ^ []))],extension(1995 ^ 8)).
% 11.42/11.72 ncf('1.3.1.2',plain,[-(1982 ^ [] = 1976 ^ []), 1976 ^ [] = 1982 ^ []],extension(4 ^ 7,bind([[_232844, _232846], [1982 ^ [], 1976 ^ []]]))).
% 11.42/11.72 ncf('1.3.1.2.1',plain,[-(1976 ^ [] = 1982 ^ [])],extension(1991 ^ 8)).
% 11.42/11.72 ncf('1.4',plain,[-(1976 ^ [] = 1976 ^ [])],extension(2 ^ 5,bind([[_232737], [1976 ^ []]]))).
% 11.42/11.72 %-----------------------------------------------------
% 11.42/11.72 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------