%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWC035+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n022.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri May 19 12:12:19 EDT 2023
% Result : Theorem 14.31s 14.84s
% Output : Proof 14.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SWC035+1 : TPTP v8.1.2. Released v2.4.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n022.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:26:16 EDT 2023
% 0.12/0.33 % CPUTime :
% 14.31/14.84
% 14.31/14.84 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 14.31/14.84 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.31/14.84 %-----------------------------------------------------
% 14.31/14.84 ncf(matrix, plain, [(1978 ^ _229850) ^ [] : [-(ssList(1976 ^ []))], (1981 ^ _229850) ^ [] : [-(ssList(1979 ^ []))], (1984 ^ _229850) ^ [] : [-(ssList(1982 ^ []))], (1987 ^ _229850) ^ [] : [-(ssList(1985 ^ []))], (1989 ^ _229850) ^ [] : [-(nil = 1979 ^ [])], (1991 ^ _229850) ^ [] : [-(1979 ^ [] = 1985 ^ [])], (1993 ^ _229850) ^ [] : [-(1976 ^ [] = 1982 ^ [])], (1995 ^ _229850) ^ [] : [-(1985 ^ [] = 1982 ^ [])], (1997 ^ _229850) ^ [] : [nil = 1976 ^ []], (246 ^ _229850) ^ [_237654, _237656, _237658, _237660] : [-(cons(_237660, _237656) = cons(_237658, _237654)), _237660 = _237658, _237656 = _237654], (256 ^ _229850) ^ [_237985, _237987] : [_237987 = _237985, -(hd(_237987) = hd(_237985))], (272 ^ _229850) ^ [_238542, _238544] : [_238544 = _238542, -(tl(_238544) = tl(_238542))], (262 ^ _229850) ^ [_238231, _238233, _238235, _238237] : [-(app(_238237, _238233) = app(_238235, _238231)), _238237 = _238235, _238233 = _238231], (2 ^ _229850) ^ [_229994] : [-(_229994 = _229994)], (4 ^ _229850) ^ [_230101, _230103] : [_230103 = _230101, -(_230101 = _230103)], (10 ^ _229850) ^ [_230305, _230307, _230309] : [-(_230309 = _230305), _230309 = _230307, _230307 = _230305], (20 ^ _229850) ^ [_230646, _230648, _230650, _230652] : [-(neq(_230650, _230646)), neq(_230652, _230648), _230652 = _230650, _230648 = _230646], (34 ^ _229850) ^ [_231090, _231092, _231094, _231096] : [-(memberP(_231094, _231090)), memberP(_231096, _231092), _231096 = _231094, _231092 = _231090], (48 ^ _229850) ^ [_231506, _231508] : [-(singletonP(_231506)), _231508 = _231506, singletonP(_231508)], (58 ^ _229850) ^ [_231829, _231831, _231833, _231835] : [-(frontsegP(_231833, _231829)), frontsegP(_231835, _231831), _231835 = _231833, _231831 = _231829], (72 ^ _229850) ^ [_232273, _232275, _232277, _232279] : [-(rearsegP(_232277, _232273)), rearsegP(_232279, _232275), _232279 = _232277, _232275 = _232273], (86 ^ _229850) ^ [_232717, _232719, _232721, _232723] : [-(segmentP(_232721, _232717)), segmentP(_232723, _232719), _232723 = _232721, _232719 = _232717], (100 ^ _229850) ^ [_233133, _233135] : [-(cyclefreeP(_233133)), _233135 = _233133, cyclefreeP(_233135)], (110 ^ _229850) ^ [_233428, _233430] : [-(totalorderP(_233428)), _233430 = _233428, totalorderP(_233430)], (120 ^ _229850) ^ [_233723, _233725] : [-(strictorderP(_233723)), _233725 = _233723, strictorderP(_233725)], (130 ^ _229850) ^ [_234018, _234020] : [-(totalorderedP(_234018)), _234020 = _234018, totalorderedP(_234020)], (140 ^ _229850) ^ [_234313, _234315] : [-(strictorderedP(_234313)), _234315 = _234313, strictorderedP(_234315)], (150 ^ _229850) ^ [_234608, _234610] : [-(duplicatefreeP(_234608)), _234610 = _234608, duplicatefreeP(_234610)], (160 ^ _229850) ^ [_234903, _234905] : [-(equalelemsP(_234903)), _234905 = _234903, equalelemsP(_234905)], (170 ^ _229850) ^ [_235226, _235228, _235230, _235232] : [-(geq(_235230, _235226)), geq(_235232, _235228), _235232 = _235230, _235228 = _235226], (184 ^ _229850) ^ [_235670, _235672, _235674, _235676] : [-(lt(_235674, _235670)), lt(_235676, _235672), _235676 = _235674, _235672 = _235670], (198 ^ _229850) ^ [_236114, _236116, _236118, _236120] : [-(leq(_236118, _236114)), leq(_236120, _236116), _236120 = _236118, _236116 = _236114], (212 ^ _229850) ^ [_236530, _236532] : [-(ssItem(_236530)), _236532 = _236530, ssItem(_236532)], (236 ^ _229850) ^ [_237249, _237251] : [-(ssList(_237249)), _237251 = _237249, ssList(_237251)], (222 ^ _229850) ^ [_236853, _236855, _236857, _236859] : [-(gt(_236857, _236853)), gt(_236859, _236855), _236859 = _236857, _236855 = _236853], (278 ^ _229850) ^ [_238764] : [ssItem(_238764), 281 ^ _229850 : [(282 ^ _229850) ^ [_238902] : [ssItem(_238902), 285 ^ _229850 : [(286 ^ _229850) ^ [] : [neq(_238764, _238902), _238764 = _238902], (292 ^ _229850) ^ [] : [-(_238764 = _238902), -(neq(_238764, _238902))]]]]], (299 ^ _229850) ^ [] : [-(ssItem(297 ^ []))], (302 ^ _229850) ^ [] : [-(ssItem(300 ^ []))], (304 ^ _229850) ^ [] : [297 ^ [] = 300 ^ []], (306 ^ _229850) ^ [_239615] : [ssList(_239615), 309 ^ _229850 : [(310 ^ _229850) ^ [_239777] : [ssItem(_239777), 313 ^ _229850 : [(314 ^ _229850) ^ [] : [memberP(_239615, _239777), 318 ^ _229850 : [(319 ^ _229850) ^ [] : [-(ssList(317 ^ [_239615, _239777]))], (322 ^ _229850) ^ [] : [-(ssList(320 ^ [_239615, _239777]))], (324 ^ _229850) ^ [] : [-(app(317 ^ [_239615, _239777], cons(_239777, 320 ^ [_239615, _239777])) = _239615)]]], (326 ^ _229850) ^ [] : [-(memberP(_239615, _239777)), 327 ^ _229850 : [(328 ^ _229850) ^ [_240425] : [ssList(_240425), 331 ^ _229850 : [(332 ^ _229850) ^ [_240573] : [ssList(_240573), app(_240425, cons(_239777, _240573)) = _239615]]]]]]]]], (340 ^ _229850) ^ [_240864] : [ssList(_240864), 343 ^ _229850 : [(344 ^ _229850) ^ [] : [singletonP(_240864), 348 ^ _229850 : [(349 ^ _229850) ^ [] : [-(ssItem(347 ^ [_240864]))], (351 ^ _229850) ^ [] : [-(cons(347 ^ [_240864], nil) = _240864)]]], (353 ^ _229850) ^ [] : [-(singletonP(_240864)), 354 ^ _229850 : [(355 ^ _229850) ^ [_241313] : [ssItem(_241313), cons(_241313, nil) = _240864]]]]], (363 ^ _229850) ^ [_241569] : [ssList(_241569), 366 ^ _229850 : [(367 ^ _229850) ^ [_241718] : [ssList(_241718), 370 ^ _229850 : [(371 ^ _229850) ^ [] : [frontsegP(_241569, _241718), 375 ^ _229850 : [(376 ^ _229850) ^ [] : [-(ssList(374 ^ [_241569, _241718]))], (378 ^ _229850) ^ [] : [-(app(_241718, 374 ^ [_241569, _241718]) = _241569)]]], (380 ^ _229850) ^ [] : [-(frontsegP(_241569, _241718)), 381 ^ _229850 : [(382 ^ _229850) ^ [_242193] : [ssList(_242193), app(_241718, _242193) = _241569]]]]]]], (390 ^ _229850) ^ [_242465] : [ssList(_242465), 393 ^ _229850 : [(394 ^ _229850) ^ [_242614] : [ssList(_242614), 397 ^ _229850 : [(398 ^ _229850) ^ [] : [rearsegP(_242465, _242614), 402 ^ _229850 : [(403 ^ _229850) ^ [] : [-(ssList(401 ^ [_242465, _242614]))], (405 ^ _229850) ^ [] : [-(app(401 ^ [_242465, _242614], _242614) = _242465)]]], (407 ^ _229850) ^ [] : [-(rearsegP(_242465, _242614)), 408 ^ _229850 : [(409 ^ _229850) ^ [_243089] : [ssList(_243089), app(_243089, _242614) = _242465]]]]]]], (417 ^ _229850) ^ [_243361] : [ssList(_243361), 420 ^ _229850 : [(421 ^ _229850) ^ [_243523] : [ssList(_243523), 424 ^ _229850 : [(425 ^ _229850) ^ [] : [segmentP(_243361, _243523), 429 ^ _229850 : [(430 ^ _229850) ^ [] : [-(ssList(428 ^ [_243361, _243523]))], (433 ^ _229850) ^ [] : [-(ssList(431 ^ [_243361, _243523]))], (435 ^ _229850) ^ [] : [-(app(app(428 ^ [_243361, _243523], _243523), 431 ^ [_243361, _243523]) = _243361)]]], (437 ^ _229850) ^ [] : [-(segmentP(_243361, _243523)), 438 ^ _229850 : [(439 ^ _229850) ^ [_244171] : [ssList(_244171), 442 ^ _229850 : [(443 ^ _229850) ^ [_244319] : [ssList(_244319), app(app(_244171, _243523), _244319) = _243361]]]]]]]]], (451 ^ _229850) ^ [_244610] : [ssList(_244610), 454 ^ _229850 : [(489 ^ _229850) ^ [] : [491 ^ _229850 : [(492 ^ _229850) ^ [] : [-(ssItem(490 ^ [_244610]))], (495 ^ _229850) ^ [] : [-(ssItem(493 ^ [_244610]))], (498 ^ _229850) ^ [] : [-(ssList(496 ^ [_244610]))], (501 ^ _229850) ^ [] : [-(ssList(499 ^ [_244610]))], (504 ^ _229850) ^ [] : [-(ssList(502 ^ [_244610]))], (506 ^ _229850) ^ [] : [-(app(app(496 ^ [_244610], cons(490 ^ [_244610], 499 ^ [_244610])), cons(493 ^ [_244610], 502 ^ [_244610])) = _244610)], (508 ^ _229850) ^ [] : [-(leq(490 ^ [_244610], 493 ^ [_244610]))], (510 ^ _229850) ^ [] : [-(leq(493 ^ [_244610], 490 ^ [_244610]))]], -(cyclefreeP(_244610))], (455 ^ _229850) ^ [] : [cyclefreeP(_244610), 458 ^ _229850 : [(459 ^ _229850) ^ [_244914] : [ssItem(_244914), 462 ^ _229850 : [(463 ^ _229850) ^ [_245106] : [ssItem(_245106), 466 ^ _229850 : [(467 ^ _229850) ^ [_245294] : [ssList(_245294), 470 ^ _229850 : [(471 ^ _229850) ^ [_245478] : [ssList(_245478), 474 ^ _229850 : [(475 ^ _229850) ^ [_245658] : [ssList(_245658), app(app(_245294, cons(_244914, _245478)), cons(_245106, _245658)) = _244610, leq(_244914, _245106), leq(_245106, _244914)]]]]]]]]]]]]], (514 ^ _229850) ^ [_247396] : [ssList(_247396), 517 ^ _229850 : [(552 ^ _229850) ^ [] : [554 ^ _229850 : [(555 ^ _229850) ^ [] : [-(ssItem(553 ^ [_247396]))], (558 ^ _229850) ^ [] : [-(ssItem(556 ^ [_247396]))], (561 ^ _229850) ^ [] : [-(ssList(559 ^ [_247396]))], (564 ^ _229850) ^ [] : [-(ssList(562 ^ [_247396]))], (567 ^ _229850) ^ [] : [-(ssList(565 ^ [_247396]))], (569 ^ _229850) ^ [] : [-(app(app(559 ^ [_247396], cons(553 ^ [_247396], 562 ^ [_247396])), cons(556 ^ [_247396], 565 ^ [_247396])) = _247396)], (571 ^ _229850) ^ [] : [leq(553 ^ [_247396], 556 ^ [_247396])], (573 ^ _229850) ^ [] : [leq(556 ^ [_247396], 553 ^ [_247396])]], -(totalorderP(_247396))], (518 ^ _229850) ^ [] : [totalorderP(_247396), 521 ^ _229850 : [(522 ^ _229850) ^ [_247698] : [ssItem(_247698), 525 ^ _229850 : [(526 ^ _229850) ^ [_247888] : [ssItem(_247888), 529 ^ _229850 : [(530 ^ _229850) ^ [_248074] : [ssList(_248074), 533 ^ _229850 : [(534 ^ _229850) ^ [_248256] : [ssList(_248256), 537 ^ _229850 : [(538 ^ _229850) ^ [_248434] : [ssList(_248434), app(app(_248074, cons(_247698, _248256)), cons(_247888, _248434)) = _247396, -(leq(_247698, _247888)), -(leq(_247888, _247698))]]]]]]]]]]]]], (577 ^ _229850) ^ [_250160] : [ssList(_250160), 580 ^ _229850 : [(615 ^ _229850) ^ [] : [617 ^ _229850 : [(618 ^ _229850) ^ [] : [-(ssItem(616 ^ [_250160]))], (621 ^ _229850) ^ [] : [-(ssItem(619 ^ [_250160]))], (624 ^ _229850) ^ [] : [-(ssList(622 ^ [_250160]))], (627 ^ _229850) ^ [] : [-(ssList(625 ^ [_250160]))], (630 ^ _229850) ^ [] : [-(ssList(628 ^ [_250160]))], (632 ^ _229850) ^ [] : [-(app(app(622 ^ [_250160], cons(616 ^ [_250160], 625 ^ [_250160])), cons(619 ^ [_250160], 628 ^ [_250160])) = _250160)], (634 ^ _229850) ^ [] : [lt(616 ^ [_250160], 619 ^ [_250160])], (636 ^ _229850) ^ [] : [lt(619 ^ [_250160], 616 ^ [_250160])]], -(strictorderP(_250160))], (581 ^ _229850) ^ [] : [strictorderP(_250160), 584 ^ _229850 : [(585 ^ _229850) ^ [_250462] : [ssItem(_250462), 588 ^ _229850 : [(589 ^ _229850) ^ [_250652] : [ssItem(_250652), 592 ^ _229850 : [(593 ^ _229850) ^ [_250838] : [ssList(_250838), 596 ^ _229850 : [(597 ^ _229850) ^ [_251020] : [ssList(_251020), 600 ^ _229850 : [(601 ^ _229850) ^ [_251198] : [ssList(_251198), app(app(_250838, cons(_250462, _251020)), cons(_250652, _251198)) = _250160, -(lt(_250462, _250652)), -(lt(_250652, _250462))]]]]]]]]]]]]], (640 ^ _229850) ^ [_252924] : [ssList(_252924), 643 ^ _229850 : [(674 ^ _229850) ^ [] : [676 ^ _229850 : [(677 ^ _229850) ^ [] : [-(ssItem(675 ^ [_252924]))], (680 ^ _229850) ^ [] : [-(ssItem(678 ^ [_252924]))], (683 ^ _229850) ^ [] : [-(ssList(681 ^ [_252924]))], (686 ^ _229850) ^ [] : [-(ssList(684 ^ [_252924]))], (689 ^ _229850) ^ [] : [-(ssList(687 ^ [_252924]))], (691 ^ _229850) ^ [] : [-(app(app(681 ^ [_252924], cons(675 ^ [_252924], 684 ^ [_252924])), cons(678 ^ [_252924], 687 ^ [_252924])) = _252924)], (693 ^ _229850) ^ [] : [leq(675 ^ [_252924], 678 ^ [_252924])]], -(totalorderedP(_252924))], (644 ^ _229850) ^ [] : [totalorderedP(_252924), 647 ^ _229850 : [(648 ^ _229850) ^ [_253220] : [ssItem(_253220), 651 ^ _229850 : [(652 ^ _229850) ^ [_253404] : [ssItem(_253404), 655 ^ _229850 : [(656 ^ _229850) ^ [_253584] : [ssList(_253584), 659 ^ _229850 : [(660 ^ _229850) ^ [_253760] : [ssList(_253760), 663 ^ _229850 : [(664 ^ _229850) ^ [_253932] : [ssList(_253932), app(app(_253584, cons(_253220, _253760)), cons(_253404, _253932)) = _252924, -(leq(_253220, _253404))]]]]]]]]]]]]], (697 ^ _229850) ^ [_255412] : [ssList(_255412), 700 ^ _229850 : [(731 ^ _229850) ^ [] : [733 ^ _229850 : [(734 ^ _229850) ^ [] : [-(ssItem(732 ^ [_255412]))], (737 ^ _229850) ^ [] : [-(ssItem(735 ^ [_255412]))], (740 ^ _229850) ^ [] : [-(ssList(738 ^ [_255412]))], (743 ^ _229850) ^ [] : [-(ssList(741 ^ [_255412]))], (746 ^ _229850) ^ [] : [-(ssList(744 ^ [_255412]))], (748 ^ _229850) ^ [] : [-(app(app(738 ^ [_255412], cons(732 ^ [_255412], 741 ^ [_255412])), cons(735 ^ [_255412], 744 ^ [_255412])) = _255412)], (750 ^ _229850) ^ [] : [lt(732 ^ [_255412], 735 ^ [_255412])]], -(strictorderedP(_255412))], (701 ^ _229850) ^ [] : [strictorderedP(_255412), 704 ^ _229850 : [(705 ^ _229850) ^ [_255708] : [ssItem(_255708), 708 ^ _229850 : [(709 ^ _229850) ^ [_255892] : [ssItem(_255892), 712 ^ _229850 : [(713 ^ _229850) ^ [_256072] : [ssList(_256072), 716 ^ _229850 : [(717 ^ _229850) ^ [_256248] : [ssList(_256248), 720 ^ _229850 : [(721 ^ _229850) ^ [_256420] : [ssList(_256420), app(app(_256072, cons(_255708, _256248)), cons(_255892, _256420)) = _255412, -(lt(_255708, _255892))]]]]]]]]]]]]], (754 ^ _229850) ^ [_257900] : [ssList(_257900), 757 ^ _229850 : [(788 ^ _229850) ^ [] : [790 ^ _229850 : [(791 ^ _229850) ^ [] : [-(ssItem(789 ^ [_257900]))], (794 ^ _229850) ^ [] : [-(ssItem(792 ^ [_257900]))], (797 ^ _229850) ^ [] : [-(ssList(795 ^ [_257900]))], (800 ^ _229850) ^ [] : [-(ssList(798 ^ [_257900]))], (803 ^ _229850) ^ [] : [-(ssList(801 ^ [_257900]))], (805 ^ _229850) ^ [] : [-(app(app(795 ^ [_257900], cons(789 ^ [_257900], 798 ^ [_257900])), cons(792 ^ [_257900], 801 ^ [_257900])) = _257900)], (807 ^ _229850) ^ [] : [-(789 ^ [_257900] = 792 ^ [_257900])]], -(duplicatefreeP(_257900))], (758 ^ _229850) ^ [] : [duplicatefreeP(_257900), 761 ^ _229850 : [(762 ^ _229850) ^ [_258198] : [ssItem(_258198), 765 ^ _229850 : [(766 ^ _229850) ^ [_258384] : [ssItem(_258384), 769 ^ _229850 : [(770 ^ _229850) ^ [_258566] : [ssList(_258566), 773 ^ _229850 : [(774 ^ _229850) ^ [_258744] : [ssList(_258744), 777 ^ _229850 : [(778 ^ _229850) ^ [_258918] : [ssList(_258918), app(app(_258566, cons(_258198, _258744)), cons(_258384, _258918)) = _257900, _258198 = _258384]]]]]]]]]]]]], (811 ^ _229850) ^ [_260410] : [ssList(_260410), 814 ^ _229850 : [(841 ^ _229850) ^ [] : [843 ^ _229850 : [(844 ^ _229850) ^ [] : [-(ssItem(842 ^ [_260410]))], (847 ^ _229850) ^ [] : [-(ssItem(845 ^ [_260410]))], (850 ^ _229850) ^ [] : [-(ssList(848 ^ [_260410]))], (853 ^ _229850) ^ [] : [-(ssList(851 ^ [_260410]))], (855 ^ _229850) ^ [] : [-(app(848 ^ [_260410], cons(842 ^ [_260410], cons(845 ^ [_260410], 851 ^ [_260410]))) = _260410)], (857 ^ _229850) ^ [] : [842 ^ [_260410] = 845 ^ [_260410]]], -(equalelemsP(_260410))], (815 ^ _229850) ^ [] : [equalelemsP(_260410), 818 ^ _229850 : [(819 ^ _229850) ^ [_260693] : [ssItem(_260693), 822 ^ _229850 : [(823 ^ _229850) ^ [_260864] : [ssItem(_260864), 826 ^ _229850 : [(827 ^ _229850) ^ [_261031] : [ssList(_261031), 830 ^ _229850 : [(831 ^ _229850) ^ [_261194] : [ssList(_261194), app(_261031, cons(_260693, cons(_260864, _261194))) = _260410, -(_260693 = _260864)]]]]]]]]]]], (861 ^ _229850) ^ [_262427] : [ssList(_262427), 864 ^ _229850 : [(865 ^ _229850) ^ [_262565] : [ssList(_262565), 868 ^ _229850 : [(869 ^ _229850) ^ [] : [neq(_262427, _262565), _262427 = _262565], (875 ^ _229850) ^ [] : [-(_262427 = _262565), -(neq(_262427, _262565))]]]]], (881 ^ _229850) ^ [_263018] : [ssList(_263018), 884 ^ _229850 : [(885 ^ _229850) ^ [_263150] : [ssItem(_263150), -(ssList(cons(_263150, _263018)))]]], (891 ^ _229850) ^ [] : [-(ssList(nil))], (893 ^ _229850) ^ [_263408] : [ssList(_263408), 896 ^ _229850 : [(897 ^ _229850) ^ [_263543] : [ssItem(_263543), cons(_263543, _263408) = _263408]]], (903 ^ _229850) ^ [_263751] : [ssList(_263751), 906 ^ _229850 : [(907 ^ _229850) ^ [_263919] : [ssList(_263919), 910 ^ _229850 : [(911 ^ _229850) ^ [_264083] : [ssItem(_264083), 914 ^ _229850 : [(915 ^ _229850) ^ [_264243] : [ssItem(_264243), cons(_264083, _263751) = cons(_264243, _263919), 922 ^ _229850 : [(923 ^ _229850) ^ [] : [-(_264083 = _264243)], (925 ^ _229850) ^ [] : [-(_263919 = _263751)]]]]]]]]], (927 ^ _229850) ^ [_264658] : [ssList(_264658), -(nil = _264658), 935 ^ _229850 : [(936 ^ _229850) ^ [] : [-(ssList(934 ^ [_264658]))], (939 ^ _229850) ^ [] : [-(ssItem(937 ^ [_264658]))], (941 ^ _229850) ^ [] : [-(cons(937 ^ [_264658], 934 ^ [_264658]) = _264658)]]], (943 ^ _229850) ^ [_265222] : [ssList(_265222), 946 ^ _229850 : [(947 ^ _229850) ^ [_265357] : [ssItem(_265357), nil = cons(_265357, _265222)]]], (953 ^ _229850) ^ [_265565] : [ssList(_265565), -(nil = _265565), -(ssItem(hd(_265565)))], (963 ^ _229850) ^ [_265843] : [ssList(_265843), 966 ^ _229850 : [(967 ^ _229850) ^ [_265978] : [ssItem(_265978), -(hd(cons(_265978, _265843)) = _265978)]]], (973 ^ _229850) ^ [_266189] : [ssList(_266189), -(nil = _266189), -(ssList(tl(_266189)))], (983 ^ _229850) ^ [_266467] : [ssList(_266467), 986 ^ _229850 : [(987 ^ _229850) ^ [_266602] : [ssItem(_266602), -(tl(cons(_266602, _266467)) = _266467)]]], (993 ^ _229850) ^ [_266813] : [ssList(_266813), 996 ^ _229850 : [(997 ^ _229850) ^ [_266945] : [ssList(_266945), -(ssList(app(_266813, _266945)))]]], (1003 ^ _229850) ^ [_267150] : [ssList(_267150), 1006 ^ _229850 : [(1007 ^ _229850) ^ [_267302] : [ssList(_267302), 1010 ^ _229850 : [(1011 ^ _229850) ^ [_267450] : [ssItem(_267450), -(cons(_267450, app(_267302, _267150)) = app(cons(_267450, _267302), _267150))]]]]], (1017 ^ _229850) ^ [_267688] : [ssList(_267688), -(app(nil, _267688) = _267688)], (1023 ^ _229850) ^ [_267882] : [ssItem(_267882), 1026 ^ _229850 : [(1027 ^ _229850) ^ [_268024] : [ssItem(_268024), -(_267882 = _268024), leq(_267882, _268024), leq(_268024, _267882)]]], (1041 ^ _229850) ^ [_268403] : [ssItem(_268403), 1044 ^ _229850 : [(1045 ^ _229850) ^ [_268555] : [ssItem(_268555), 1048 ^ _229850 : [(1049 ^ _229850) ^ [_268703] : [ssItem(_268703), -(leq(_268403, _268703)), leq(_268403, _268555), leq(_268555, _268703)]]]]], (1063 ^ _229850) ^ [_269103] : [ssItem(_269103), -(leq(_269103, _269103))], (1069 ^ _229850) ^ [_269291] : [ssItem(_269291), 1072 ^ _229850 : [(1073 ^ _229850) ^ [_269427] : [ssItem(_269427), 1076 ^ _229850 : [(1077 ^ _229850) ^ [] : [geq(_269291, _269427), -(leq(_269427, _269291))], (1083 ^ _229850) ^ [] : [leq(_269427, _269291), -(geq(_269291, _269427))]]]]], (1089 ^ _229850) ^ [_269878] : [ssItem(_269878), 1092 ^ _229850 : [(1093 ^ _229850) ^ [_270016] : [ssItem(_270016), lt(_269878, _270016), lt(_270016, _269878)]]], (1103 ^ _229850) ^ [_270307] : [ssItem(_270307), 1106 ^ _229850 : [(1107 ^ _229850) ^ [_270459] : [ssItem(_270459), 1110 ^ _229850 : [(1111 ^ _229850) ^ [_270607] : [ssItem(_270607), -(lt(_270307, _270607)), lt(_270307, _270459), lt(_270459, _270607)]]]]], (1125 ^ _229850) ^ [_271007] : [ssItem(_271007), 1128 ^ _229850 : [(1129 ^ _229850) ^ [_271143] : [ssItem(_271143), 1132 ^ _229850 : [(1133 ^ _229850) ^ [] : [gt(_271007, _271143), -(lt(_271143, _271007))], (1139 ^ _229850) ^ [] : [lt(_271143, _271007), -(gt(_271007, _271143))]]]]], (1145 ^ _229850) ^ [_271594] : [ssItem(_271594), 1148 ^ _229850 : [(1149 ^ _229850) ^ [_271749] : [ssList(_271749), 1152 ^ _229850 : [(1153 ^ _229850) ^ [_271900] : [ssList(_271900), 1156 ^ _229850 : [(1167 ^ _229850) ^ [] : [1168 ^ _229850 : [(1169 ^ _229850) ^ [] : [memberP(_271749, _271594)], (1171 ^ _229850) ^ [] : [memberP(_271900, _271594)]], -(memberP(app(_271749, _271900), _271594))], (1157 ^ _229850) ^ [] : [memberP(app(_271749, _271900), _271594), -(memberP(_271749, _271594)), -(memberP(_271900, _271594))]]]]]]], (1175 ^ _229850) ^ [_272547] : [ssItem(_272547), 1178 ^ _229850 : [(1179 ^ _229850) ^ [_272702] : [ssItem(_272702), 1182 ^ _229850 : [(1183 ^ _229850) ^ [_272853] : [ssList(_272853), 1186 ^ _229850 : [(1197 ^ _229850) ^ [] : [1198 ^ _229850 : [(1199 ^ _229850) ^ [] : [_272547 = _272702], (1201 ^ _229850) ^ [] : [memberP(_272853, _272547)]], -(memberP(cons(_272702, _272853), _272547))], (1187 ^ _229850) ^ [] : [memberP(cons(_272702, _272853), _272547), -(_272547 = _272702), -(memberP(_272853, _272547))]]]]]]], (1205 ^ _229850) ^ [_273500] : [ssItem(_273500), memberP(nil, _273500)], (1211 ^ _229850) ^ [] : [singletonP(nil)], (1213 ^ _229850) ^ [_273741] : [ssList(_273741), 1216 ^ _229850 : [(1217 ^ _229850) ^ [_273893] : [ssList(_273893), 1220 ^ _229850 : [(1221 ^ _229850) ^ [_274041] : [ssList(_274041), -(frontsegP(_273741, _274041)), frontsegP(_273741, _273893), frontsegP(_273893, _274041)]]]]], (1235 ^ _229850) ^ [_274441] : [ssList(_274441), 1238 ^ _229850 : [(1239 ^ _229850) ^ [_274583] : [ssList(_274583), -(_274441 = _274583), frontsegP(_274441, _274583), frontsegP(_274583, _274441)]]], (1253 ^ _229850) ^ [_274962] : [ssList(_274962), -(frontsegP(_274962, _274962))], (1259 ^ _229850) ^ [_275150] : [ssList(_275150), 1262 ^ _229850 : [(1263 ^ _229850) ^ [_275299] : [ssList(_275299), 1266 ^ _229850 : [(1267 ^ _229850) ^ [_275444] : [ssList(_275444), frontsegP(_275150, _275299), -(frontsegP(app(_275150, _275444), _275299))]]]]], (1277 ^ _229850) ^ [_275757] : [ssItem(_275757), 1280 ^ _229850 : [(1281 ^ _229850) ^ [_275925] : [ssItem(_275925), 1284 ^ _229850 : [(1285 ^ _229850) ^ [_276089] : [ssList(_276089), 1288 ^ _229850 : [(1289 ^ _229850) ^ [_276249] : [ssList(_276249), 1292 ^ _229850 : [(1293 ^ _229850) ^ [] : [frontsegP(cons(_275757, _276089), cons(_275925, _276249)), 1296 ^ _229850 : [(1297 ^ _229850) ^ [] : [-(_275757 = _275925)], (1299 ^ _229850) ^ [] : [-(frontsegP(_276089, _276249))]]], (1301 ^ _229850) ^ [] : [-(frontsegP(cons(_275757, _276089), cons(_275925, _276249))), _275757 = _275925, frontsegP(_276089, _276249)]]]]]]]]], (1311 ^ _229850) ^ [_276934] : [ssList(_276934), -(frontsegP(_276934, nil))], (1317 ^ _229850) ^ [_277122] : [ssList(_277122), 1320 ^ _229850 : [(1321 ^ _229850) ^ [] : [frontsegP(nil, _277122), -(nil = _277122)], (1327 ^ _229850) ^ [] : [nil = _277122, -(frontsegP(nil, _277122))]]], (1333 ^ _229850) ^ [_277550] : [ssList(_277550), 1336 ^ _229850 : [(1337 ^ _229850) ^ [_277702] : [ssList(_277702), 1340 ^ _229850 : [(1341 ^ _229850) ^ [_277850] : [ssList(_277850), -(rearsegP(_277550, _277850)), rearsegP(_277550, _277702), rearsegP(_277702, _277850)]]]]], (1355 ^ _229850) ^ [_278250] : [ssList(_278250), 1358 ^ _229850 : [(1359 ^ _229850) ^ [_278392] : [ssList(_278392), -(_278250 = _278392), rearsegP(_278250, _278392), rearsegP(_278392, _278250)]]], (1373 ^ _229850) ^ [_278771] : [ssList(_278771), -(rearsegP(_278771, _278771))], (1379 ^ _229850) ^ [_278959] : [ssList(_278959), 1382 ^ _229850 : [(1383 ^ _229850) ^ [_279108] : [ssList(_279108), 1386 ^ _229850 : [(1387 ^ _229850) ^ [_279253] : [ssList(_279253), rearsegP(_278959, _279108), -(rearsegP(app(_279253, _278959), _279108))]]]]], (1397 ^ _229850) ^ [_279566] : [ssList(_279566), -(rearsegP(_279566, nil))], (1403 ^ _229850) ^ [_279754] : [ssList(_279754), 1406 ^ _229850 : [(1407 ^ _229850) ^ [] : [rearsegP(nil, _279754), -(nil = _279754)], (1413 ^ _229850) ^ [] : [nil = _279754, -(rearsegP(nil, _279754))]]], (1419 ^ _229850) ^ [_280182] : [ssList(_280182), 1422 ^ _229850 : [(1423 ^ _229850) ^ [_280334] : [ssList(_280334), 1426 ^ _229850 : [(1427 ^ _229850) ^ [_280482] : [ssList(_280482), -(segmentP(_280182, _280482)), segmentP(_280182, _280334), segmentP(_280334, _280482)]]]]], (1441 ^ _229850) ^ [_280882] : [ssList(_280882), 1444 ^ _229850 : [(1445 ^ _229850) ^ [_281024] : [ssList(_281024), -(_280882 = _281024), segmentP(_280882, _281024), segmentP(_281024, _280882)]]], (1459 ^ _229850) ^ [_281403] : [ssList(_281403), -(segmentP(_281403, _281403))], (1465 ^ _229850) ^ [_281591] : [ssList(_281591), 1468 ^ _229850 : [(1469 ^ _229850) ^ [_281753] : [ssList(_281753), 1472 ^ _229850 : [(1473 ^ _229850) ^ [_281911] : [ssList(_281911), 1476 ^ _229850 : [(1477 ^ _229850) ^ [_282065] : [ssList(_282065), segmentP(_281591, _281753), -(segmentP(app(app(_281911, _281591), _282065), _281753))]]]]]]], (1487 ^ _229850) ^ [_282401] : [ssList(_282401), -(segmentP(_282401, nil))], (1493 ^ _229850) ^ [_282589] : [ssList(_282589), 1496 ^ _229850 : [(1497 ^ _229850) ^ [] : [segmentP(nil, _282589), -(nil = _282589)], (1503 ^ _229850) ^ [] : [nil = _282589, -(segmentP(nil, _282589))]]], (1509 ^ _229850) ^ [_283017] : [ssItem(_283017), -(cyclefreeP(cons(_283017, nil)))], (1515 ^ _229850) ^ [] : [-(cyclefreeP(nil))], (1517 ^ _229850) ^ [_283262] : [ssItem(_283262), -(totalorderP(cons(_283262, nil)))], (1523 ^ _229850) ^ [] : [-(totalorderP(nil))], (1525 ^ _229850) ^ [_283507] : [ssItem(_283507), -(strictorderP(cons(_283507, nil)))], (1531 ^ _229850) ^ [] : [-(strictorderP(nil))], (1533 ^ _229850) ^ [_283752] : [ssItem(_283752), -(totalorderedP(cons(_283752, nil)))], (1539 ^ _229850) ^ [] : [-(totalorderedP(nil))], (1541 ^ _229850) ^ [_283997] : [ssItem(_283997), 1544 ^ _229850 : [(1545 ^ _229850) ^ [_284156] : [ssList(_284156), 1548 ^ _229850 : [(1549 ^ _229850) ^ [] : [totalorderedP(cons(_283997, _284156)), -(nil = _284156), 1556 ^ _229850 : [(1557 ^ _229850) ^ [] : [nil = _284156], (1559 ^ _229850) ^ [] : [-(totalorderedP(_284156))], (1561 ^ _229850) ^ [] : [-(leq(_283997, hd(_284156)))]]], (1563 ^ _229850) ^ [] : [-(totalorderedP(cons(_283997, _284156))), 1564 ^ _229850 : [(1565 ^ _229850) ^ [] : [nil = _284156], (1567 ^ _229850) ^ [] : [-(nil = _284156), totalorderedP(_284156), leq(_283997, hd(_284156))]]]]]]], (1579 ^ _229850) ^ [_285091] : [ssItem(_285091), -(strictorderedP(cons(_285091, nil)))], (1585 ^ _229850) ^ [] : [-(strictorderedP(nil))], (1587 ^ _229850) ^ [_285336] : [ssItem(_285336), 1590 ^ _229850 : [(1591 ^ _229850) ^ [_285495] : [ssList(_285495), 1594 ^ _229850 : [(1595 ^ _229850) ^ [] : [strictorderedP(cons(_285336, _285495)), -(nil = _285495), 1602 ^ _229850 : [(1603 ^ _229850) ^ [] : [nil = _285495], (1605 ^ _229850) ^ [] : [-(strictorderedP(_285495))], (1607 ^ _229850) ^ [] : [-(lt(_285336, hd(_285495)))]]], (1609 ^ _229850) ^ [] : [-(strictorderedP(cons(_285336, _285495))), 1610 ^ _229850 : [(1611 ^ _229850) ^ [] : [nil = _285495], (1613 ^ _229850) ^ [] : [-(nil = _285495), strictorderedP(_285495), lt(_285336, hd(_285495))]]]]]]], (1625 ^ _229850) ^ [_286430] : [ssItem(_286430), -(duplicatefreeP(cons(_286430, nil)))], (1631 ^ _229850) ^ [] : [-(duplicatefreeP(nil))], (1633 ^ _229850) ^ [_286675] : [ssItem(_286675), -(equalelemsP(cons(_286675, nil)))], (1639 ^ _229850) ^ [] : [-(equalelemsP(nil))], (1641 ^ _229850) ^ [_286920] : [ssList(_286920), -(nil = _286920), 1649 ^ _229850 : [(1650 ^ _229850) ^ [] : [-(ssItem(1648 ^ [_286920]))], (1652 ^ _229850) ^ [] : [-(hd(_286920) = 1648 ^ [_286920])]]], (1654 ^ _229850) ^ [_287334] : [ssList(_287334), -(nil = _287334), 1662 ^ _229850 : [(1663 ^ _229850) ^ [] : [-(ssList(1661 ^ [_287334]))], (1665 ^ _229850) ^ [] : [-(tl(_287334) = 1661 ^ [_287334])]]], (1667 ^ _229850) ^ [_287748] : [ssList(_287748), 1670 ^ _229850 : [(1671 ^ _229850) ^ [_287914] : [ssList(_287914), -(_287914 = _287748), -(nil = _287914), -(nil = _287748), hd(_287914) = hd(_287748), tl(_287914) = tl(_287748)]]], (1693 ^ _229850) ^ [_288493] : [ssList(_288493), -(nil = _288493), -(cons(hd(_288493), tl(_288493)) = _288493)], (1703 ^ _229850) ^ [_288783] : [ssList(_288783), 1706 ^ _229850 : [(1707 ^ _229850) ^ [_288935] : [ssList(_288935), 1710 ^ _229850 : [(1711 ^ _229850) ^ [_289083] : [ssList(_289083), app(_289083, _288935) = app(_288783, _288935), -(_289083 = _288783)]]]]], (1721 ^ _229850) ^ [_289402] : [ssList(_289402), 1724 ^ _229850 : [(1725 ^ _229850) ^ [_289554] : [ssList(_289554), 1728 ^ _229850 : [(1729 ^ _229850) ^ [_289702] : [ssList(_289702), app(_289554, _289702) = app(_289554, _289402), -(_289702 = _289402)]]]]], (1739 ^ _229850) ^ [_290021] : [ssList(_290021), 1742 ^ _229850 : [(1743 ^ _229850) ^ [_290160] : [ssItem(_290160), -(cons(_290160, _290021) = app(cons(_290160, nil), _290021))]]], (1749 ^ _229850) ^ [_290379] : [ssList(_290379), 1752 ^ _229850 : [(1753 ^ _229850) ^ [_290531] : [ssList(_290531), 1756 ^ _229850 : [(1757 ^ _229850) ^ [_290679] : [ssList(_290679), -(app(app(_290379, _290531), _290679) = app(_290379, app(_290531, _290679)))]]]]], (1763 ^ _229850) ^ [_290917] : [ssList(_290917), 1766 ^ _229850 : [(1767 ^ _229850) ^ [_291062] : [ssList(_291062), 1770 ^ _229850 : [(1771 ^ _229850) ^ [] : [nil = app(_290917, _291062), 1774 ^ _229850 : [(1775 ^ _229850) ^ [] : [-(nil = _291062)], (1777 ^ _229850) ^ [] : [-(nil = _290917)]]], (1779 ^ _229850) ^ [] : [-(nil = app(_290917, _291062)), nil = _291062, nil = _290917]]]]], (1789 ^ _229850) ^ [_291680] : [ssList(_291680), -(app(_291680, nil) = _291680)], (1795 ^ _229850) ^ [_291874] : [ssList(_291874), 1798 ^ _229850 : [(1799 ^ _229850) ^ [_292019] : [ssList(_292019), -(nil = _291874), -(hd(app(_291874, _292019)) = hd(_291874))]]], (1809 ^ _229850) ^ [_292326] : [ssList(_292326), 1812 ^ _229850 : [(1813 ^ _229850) ^ [_292474] : [ssList(_292474), -(nil = _292326), -(tl(app(_292326, _292474)) = app(tl(_292326), _292474))]]], (1823 ^ _229850) ^ [_292787] : [ssItem(_292787), 1826 ^ _229850 : [(1827 ^ _229850) ^ [_292929] : [ssItem(_292929), -(_292787 = _292929), geq(_292787, _292929), geq(_292929, _292787)]]], (1841 ^ _229850) ^ [_293308] : [ssItem(_293308), 1844 ^ _229850 : [(1845 ^ _229850) ^ [_293460] : [ssItem(_293460), 1848 ^ _229850 : [(1849 ^ _229850) ^ [_293608] : [ssItem(_293608), -(geq(_293308, _293608)), geq(_293308, _293460), geq(_293460, _293608)]]]]], (1863 ^ _229850) ^ [_294008] : [ssItem(_294008), -(geq(_294008, _294008))], (1869 ^ _229850) ^ [_294196] : [ssItem(_294196), lt(_294196, _294196)], (1875 ^ _229850) ^ [_294385] : [ssItem(_294385), 1878 ^ _229850 : [(1879 ^ _229850) ^ [_294537] : [ssItem(_294537), 1882 ^ _229850 : [(1883 ^ _229850) ^ [_294685] : [ssItem(_294685), -(lt(_294385, _294685)), leq(_294385, _294537), lt(_294537, _294685)]]]]], (1897 ^ _229850) ^ [_295085] : [ssItem(_295085), 1900 ^ _229850 : [(1901 ^ _229850) ^ [_295227] : [ssItem(_295227), leq(_295085, _295227), -(_295085 = _295227), -(lt(_295085, _295227))]]], (1915 ^ _229850) ^ [_295607] : [ssItem(_295607), 1918 ^ _229850 : [(1919 ^ _229850) ^ [_295751] : [ssItem(_295751), 1922 ^ _229850 : [(1923 ^ _229850) ^ [] : [lt(_295607, _295751), 1926 ^ _229850 : [(1927 ^ _229850) ^ [] : [_295607 = _295751], (1929 ^ _229850) ^ [] : [-(leq(_295607, _295751))]]], (1931 ^ _229850) ^ [] : [-(lt(_295607, _295751)), -(_295607 = _295751), leq(_295607, _295751)]]]]], (1941 ^ _229850) ^ [_296362] : [ssItem(_296362), 1944 ^ _229850 : [(1945 ^ _229850) ^ [_296500] : [ssItem(_296500), gt(_296362, _296500), gt(_296500, _296362)]]], (1955 ^ _229850) ^ [_296771] : [ssItem(_296771), 1958 ^ _229850 : [(1959 ^ _229850) ^ [_296923] : [ssItem(_296923), 1962 ^ _229850 : [(1963 ^ _229850) ^ [_297071] : [ssItem(_297071), -(gt(_296771, _297071)), gt(_296771, _296923), gt(_296923, _297071)]]]]]], input).
% 14.31/14.84 ncf('1',plain,[nil = 1976 ^ []],start(1997 ^ 0)).
% 14.31/14.84 ncf('1.1',plain,[-(nil = 1976 ^ []), nil = 1979 ^ [], 1979 ^ [] = 1976 ^ []],extension(10 ^ 1,bind([[_230305, _230307, _230309], [1976 ^ [], 1979 ^ [], nil]]))).
% 14.31/14.84 ncf('1.1.1',plain,[-(nil = 1979 ^ [])],extension(1989 ^ 2)).
% 14.31/14.84 ncf('1.1.2',plain,[-(1979 ^ [] = 1976 ^ []), 1979 ^ [] = 1985 ^ [], 1985 ^ [] = 1976 ^ []],extension(10 ^ 2,bind([[_230305, _230307, _230309], [1976 ^ [], 1985 ^ [], 1979 ^ []]]))).
% 14.31/14.84 ncf('1.1.2.1',plain,[-(1979 ^ [] = 1985 ^ [])],extension(1991 ^ 3)).
% 14.31/14.84 ncf('1.1.2.2',plain,[-(1985 ^ [] = 1976 ^ []), 1985 ^ [] = 1982 ^ [], 1982 ^ [] = 1976 ^ []],extension(10 ^ 3,bind([[_230305, _230307, _230309], [1976 ^ [], 1982 ^ [], 1985 ^ []]]))).
% 14.31/14.84 ncf('1.1.2.2.1',plain,[-(1985 ^ [] = 1982 ^ [])],extension(1995 ^ 4)).
% 14.31/14.84 ncf('1.1.2.2.2',plain,[-(1982 ^ [] = 1976 ^ []), 1976 ^ [] = 1982 ^ []],extension(4 ^ 4,bind([[_230101, _230103], [1982 ^ [], 1976 ^ []]]))).
% 14.31/14.84 ncf('1.1.2.2.2.1',plain,[-(1976 ^ [] = 1982 ^ [])],extension(1993 ^ 5)).
% 14.31/14.84 %-----------------------------------------------------
% 14.31/14.84 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------