%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWC358+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n024.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:20 EDT 2023
% Result : Theorem 10.30s 10.70s
% Output : Proof 10.30s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SWC358+1 : TPTP v8.1.2. Released v2.4.0.
% 0.12/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n024.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 01:10:37 EDT 2023
% 0.12/0.34 % CPUTime :
% 10.30/10.70
% 10.30/10.70 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 10.30/10.70 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.30/10.70 %-----------------------------------------------------
% 10.30/10.70 ncf(matrix, plain, [(1978 ^ _232530) ^ [] : [-(ssList(1976 ^ []))], (1981 ^ _232530) ^ [] : [-(ssList(1979 ^ []))], (1984 ^ _232530) ^ [] : [-(ssList(1982 ^ []))], (1987 ^ _232530) ^ [] : [-(ssList(1985 ^ []))], (1989 ^ _232530) ^ [] : [-(1979 ^ [] = 1985 ^ [])], (1991 ^ _232530) ^ [] : [-(1976 ^ [] = 1982 ^ [])], (1993 ^ _232530) ^ [] : [-(neq(1979 ^ [], nil))], (1995 ^ _232530) ^ [] : [segmentP(1979 ^ [], 1976 ^ [])], (1997 ^ _232530) ^ [] : [1998 ^ _232530 : [(1999 ^ _232530) ^ [] : [-(nil = 1985 ^ [])], (2001 ^ _232530) ^ [] : [-(nil = 1982 ^ [])]], 2002 ^ _232530 : [(2003 ^ _232530) ^ [] : [-(neq(1982 ^ [], nil))], (2005 ^ _232530) ^ [] : [-(segmentP(1985 ^ [], 1982 ^ []))]]], (246 ^ _232530) ^ [_240334, _240336, _240338, _240340] : [-(cons(_240340, _240336) = cons(_240338, _240334)), _240340 = _240338, _240336 = _240334], (256 ^ _232530) ^ [_240665, _240667] : [_240667 = _240665, -(hd(_240667) = hd(_240665))], (272 ^ _232530) ^ [_241222, _241224] : [_241224 = _241222, -(tl(_241224) = tl(_241222))], (262 ^ _232530) ^ [_240911, _240913, _240915, _240917] : [-(app(_240917, _240913) = app(_240915, _240911)), _240917 = _240915, _240913 = _240911], (2 ^ _232530) ^ [_232674] : [-(_232674 = _232674)], (4 ^ _232530) ^ [_232781, _232783] : [_232783 = _232781, -(_232781 = _232783)], (10 ^ _232530) ^ [_232985, _232987, _232989] : [-(_232989 = _232985), _232989 = _232987, _232987 = _232985], (20 ^ _232530) ^ [_233326, _233328, _233330, _233332] : [-(memberP(_233330, _233326)), memberP(_233332, _233328), _233332 = _233330, _233328 = _233326], (34 ^ _232530) ^ [_233742, _233744] : [-(singletonP(_233742)), _233744 = _233742, singletonP(_233744)], (44 ^ _232530) ^ [_234065, _234067, _234069, _234071] : [-(frontsegP(_234069, _234065)), frontsegP(_234071, _234067), _234071 = _234069, _234067 = _234065], (58 ^ _232530) ^ [_234509, _234511, _234513, _234515] : [-(rearsegP(_234513, _234509)), rearsegP(_234515, _234511), _234515 = _234513, _234511 = _234509], (72 ^ _232530) ^ [_234925, _234927] : [-(cyclefreeP(_234925)), _234927 = _234925, cyclefreeP(_234927)], (82 ^ _232530) ^ [_235220, _235222] : [-(totalorderP(_235220)), _235222 = _235220, totalorderP(_235222)], (92 ^ _232530) ^ [_235515, _235517] : [-(strictorderP(_235515)), _235517 = _235515, strictorderP(_235517)], (102 ^ _232530) ^ [_235810, _235812] : [-(totalorderedP(_235810)), _235812 = _235810, totalorderedP(_235812)], (112 ^ _232530) ^ [_236105, _236107] : [-(strictorderedP(_236105)), _236107 = _236105, strictorderedP(_236107)], (122 ^ _232530) ^ [_236400, _236402] : [-(duplicatefreeP(_236400)), _236402 = _236400, duplicatefreeP(_236402)], (132 ^ _232530) ^ [_236695, _236697] : [-(equalelemsP(_236695)), _236697 = _236695, equalelemsP(_236697)], (142 ^ _232530) ^ [_237018, _237020, _237022, _237024] : [-(geq(_237022, _237018)), geq(_237024, _237020), _237024 = _237022, _237020 = _237018], (156 ^ _232530) ^ [_237462, _237464, _237466, _237468] : [-(lt(_237466, _237462)), lt(_237468, _237464), _237468 = _237466, _237464 = _237462], (170 ^ _232530) ^ [_237906, _237908, _237910, _237912] : [-(leq(_237910, _237906)), leq(_237912, _237908), _237912 = _237910, _237908 = _237906], (184 ^ _232530) ^ [_238322, _238324] : [-(ssItem(_238322)), _238324 = _238322, ssItem(_238324)], (194 ^ _232530) ^ [_238645, _238647, _238649, _238651] : [-(gt(_238649, _238645)), gt(_238651, _238647), _238651 = _238649, _238647 = _238645], (208 ^ _232530) ^ [_239061, _239063] : [-(ssList(_239061)), _239063 = _239061, ssList(_239063)], (218 ^ _232530) ^ [_239384, _239386, _239388, _239390] : [-(neq(_239388, _239384)), neq(_239390, _239386), _239390 = _239388, _239386 = _239384], (232 ^ _232530) ^ [_239808, _239810, _239812, _239814] : [-(segmentP(_239812, _239808)), segmentP(_239814, _239810), _239814 = _239812, _239810 = _239808], (278 ^ _232530) ^ [_241444] : [ssItem(_241444), 281 ^ _232530 : [(282 ^ _232530) ^ [_241582] : [ssItem(_241582), 285 ^ _232530 : [(286 ^ _232530) ^ [] : [neq(_241444, _241582), _241444 = _241582], (292 ^ _232530) ^ [] : [-(_241444 = _241582), -(neq(_241444, _241582))]]]]], (299 ^ _232530) ^ [] : [-(ssItem(297 ^ []))], (302 ^ _232530) ^ [] : [-(ssItem(300 ^ []))], (304 ^ _232530) ^ [] : [297 ^ [] = 300 ^ []], (306 ^ _232530) ^ [_242295] : [ssList(_242295), 309 ^ _232530 : [(310 ^ _232530) ^ [_242457] : [ssItem(_242457), 313 ^ _232530 : [(314 ^ _232530) ^ [] : [memberP(_242295, _242457), 318 ^ _232530 : [(319 ^ _232530) ^ [] : [-(ssList(317 ^ [_242295, _242457]))], (322 ^ _232530) ^ [] : [-(ssList(320 ^ [_242295, _242457]))], (324 ^ _232530) ^ [] : [-(app(317 ^ [_242295, _242457], cons(_242457, 320 ^ [_242295, _242457])) = _242295)]]], (326 ^ _232530) ^ [] : [-(memberP(_242295, _242457)), 327 ^ _232530 : [(328 ^ _232530) ^ [_243105] : [ssList(_243105), 331 ^ _232530 : [(332 ^ _232530) ^ [_243253] : [ssList(_243253), app(_243105, cons(_242457, _243253)) = _242295]]]]]]]]], (340 ^ _232530) ^ [_243544] : [ssList(_243544), 343 ^ _232530 : [(344 ^ _232530) ^ [] : [singletonP(_243544), 348 ^ _232530 : [(349 ^ _232530) ^ [] : [-(ssItem(347 ^ [_243544]))], (351 ^ _232530) ^ [] : [-(cons(347 ^ [_243544], nil) = _243544)]]], (353 ^ _232530) ^ [] : [-(singletonP(_243544)), 354 ^ _232530 : [(355 ^ _232530) ^ [_243993] : [ssItem(_243993), cons(_243993, nil) = _243544]]]]], (363 ^ _232530) ^ [_244249] : [ssList(_244249), 366 ^ _232530 : [(367 ^ _232530) ^ [_244398] : [ssList(_244398), 370 ^ _232530 : [(371 ^ _232530) ^ [] : [frontsegP(_244249, _244398), 375 ^ _232530 : [(376 ^ _232530) ^ [] : [-(ssList(374 ^ [_244249, _244398]))], (378 ^ _232530) ^ [] : [-(app(_244398, 374 ^ [_244249, _244398]) = _244249)]]], (380 ^ _232530) ^ [] : [-(frontsegP(_244249, _244398)), 381 ^ _232530 : [(382 ^ _232530) ^ [_244873] : [ssList(_244873), app(_244398, _244873) = _244249]]]]]]], (390 ^ _232530) ^ [_245145] : [ssList(_245145), 393 ^ _232530 : [(394 ^ _232530) ^ [_245294] : [ssList(_245294), 397 ^ _232530 : [(398 ^ _232530) ^ [] : [rearsegP(_245145, _245294), 402 ^ _232530 : [(403 ^ _232530) ^ [] : [-(ssList(401 ^ [_245145, _245294]))], (405 ^ _232530) ^ [] : [-(app(401 ^ [_245145, _245294], _245294) = _245145)]]], (407 ^ _232530) ^ [] : [-(rearsegP(_245145, _245294)), 408 ^ _232530 : [(409 ^ _232530) ^ [_245769] : [ssList(_245769), app(_245769, _245294) = _245145]]]]]]], (417 ^ _232530) ^ [_246041] : [ssList(_246041), 420 ^ _232530 : [(421 ^ _232530) ^ [_246203] : [ssList(_246203), 424 ^ _232530 : [(425 ^ _232530) ^ [] : [segmentP(_246041, _246203), 429 ^ _232530 : [(430 ^ _232530) ^ [] : [-(ssList(428 ^ [_246041, _246203]))], (433 ^ _232530) ^ [] : [-(ssList(431 ^ [_246041, _246203]))], (435 ^ _232530) ^ [] : [-(app(app(428 ^ [_246041, _246203], _246203), 431 ^ [_246041, _246203]) = _246041)]]], (437 ^ _232530) ^ [] : [-(segmentP(_246041, _246203)), 438 ^ _232530 : [(439 ^ _232530) ^ [_246851] : [ssList(_246851), 442 ^ _232530 : [(443 ^ _232530) ^ [_246999] : [ssList(_246999), app(app(_246851, _246203), _246999) = _246041]]]]]]]]], (451 ^ _232530) ^ [_247290] : [ssList(_247290), 454 ^ _232530 : [(489 ^ _232530) ^ [] : [491 ^ _232530 : [(492 ^ _232530) ^ [] : [-(ssItem(490 ^ [_247290]))], (495 ^ _232530) ^ [] : [-(ssItem(493 ^ [_247290]))], (498 ^ _232530) ^ [] : [-(ssList(496 ^ [_247290]))], (501 ^ _232530) ^ [] : [-(ssList(499 ^ [_247290]))], (504 ^ _232530) ^ [] : [-(ssList(502 ^ [_247290]))], (506 ^ _232530) ^ [] : [-(app(app(496 ^ [_247290], cons(490 ^ [_247290], 499 ^ [_247290])), cons(493 ^ [_247290], 502 ^ [_247290])) = _247290)], (508 ^ _232530) ^ [] : [-(leq(490 ^ [_247290], 493 ^ [_247290]))], (510 ^ _232530) ^ [] : [-(leq(493 ^ [_247290], 490 ^ [_247290]))]], -(cyclefreeP(_247290))], (455 ^ _232530) ^ [] : [cyclefreeP(_247290), 458 ^ _232530 : [(459 ^ _232530) ^ [_247594] : [ssItem(_247594), 462 ^ _232530 : [(463 ^ _232530) ^ [_247786] : [ssItem(_247786), 466 ^ _232530 : [(467 ^ _232530) ^ [_247974] : [ssList(_247974), 470 ^ _232530 : [(471 ^ _232530) ^ [_248158] : [ssList(_248158), 474 ^ _232530 : [(475 ^ _232530) ^ [_248338] : [ssList(_248338), app(app(_247974, cons(_247594, _248158)), cons(_247786, _248338)) = _247290, leq(_247594, _247786), leq(_247786, _247594)]]]]]]]]]]]]], (514 ^ _232530) ^ [_250076] : [ssList(_250076), 517 ^ _232530 : [(552 ^ _232530) ^ [] : [554 ^ _232530 : [(555 ^ _232530) ^ [] : [-(ssItem(553 ^ [_250076]))], (558 ^ _232530) ^ [] : [-(ssItem(556 ^ [_250076]))], (561 ^ _232530) ^ [] : [-(ssList(559 ^ [_250076]))], (564 ^ _232530) ^ [] : [-(ssList(562 ^ [_250076]))], (567 ^ _232530) ^ [] : [-(ssList(565 ^ [_250076]))], (569 ^ _232530) ^ [] : [-(app(app(559 ^ [_250076], cons(553 ^ [_250076], 562 ^ [_250076])), cons(556 ^ [_250076], 565 ^ [_250076])) = _250076)], (571 ^ _232530) ^ [] : [leq(553 ^ [_250076], 556 ^ [_250076])], (573 ^ _232530) ^ [] : [leq(556 ^ [_250076], 553 ^ [_250076])]], -(totalorderP(_250076))], (518 ^ _232530) ^ [] : [totalorderP(_250076), 521 ^ _232530 : [(522 ^ _232530) ^ [_250378] : [ssItem(_250378), 525 ^ _232530 : [(526 ^ _232530) ^ [_250568] : [ssItem(_250568), 529 ^ _232530 : [(530 ^ _232530) ^ [_250754] : [ssList(_250754), 533 ^ _232530 : [(534 ^ _232530) ^ [_250936] : [ssList(_250936), 537 ^ _232530 : [(538 ^ _232530) ^ [_251114] : [ssList(_251114), app(app(_250754, cons(_250378, _250936)), cons(_250568, _251114)) = _250076, -(leq(_250378, _250568)), -(leq(_250568, _250378))]]]]]]]]]]]]], (577 ^ _232530) ^ [_252840] : [ssList(_252840), 580 ^ _232530 : [(615 ^ _232530) ^ [] : [617 ^ _232530 : [(618 ^ _232530) ^ [] : [-(ssItem(616 ^ [_252840]))], (621 ^ _232530) ^ [] : [-(ssItem(619 ^ [_252840]))], (624 ^ _232530) ^ [] : [-(ssList(622 ^ [_252840]))], (627 ^ _232530) ^ [] : [-(ssList(625 ^ [_252840]))], (630 ^ _232530) ^ [] : [-(ssList(628 ^ [_252840]))], (632 ^ _232530) ^ [] : [-(app(app(622 ^ [_252840], cons(616 ^ [_252840], 625 ^ [_252840])), cons(619 ^ [_252840], 628 ^ [_252840])) = _252840)], (634 ^ _232530) ^ [] : [lt(616 ^ [_252840], 619 ^ [_252840])], (636 ^ _232530) ^ [] : [lt(619 ^ [_252840], 616 ^ [_252840])]], -(strictorderP(_252840))], (581 ^ _232530) ^ [] : [strictorderP(_252840), 584 ^ _232530 : [(585 ^ _232530) ^ [_253142] : [ssItem(_253142), 588 ^ _232530 : [(589 ^ _232530) ^ [_253332] : [ssItem(_253332), 592 ^ _232530 : [(593 ^ _232530) ^ [_253518] : [ssList(_253518), 596 ^ _232530 : [(597 ^ _232530) ^ [_253700] : [ssList(_253700), 600 ^ _232530 : [(601 ^ _232530) ^ [_253878] : [ssList(_253878), app(app(_253518, cons(_253142, _253700)), cons(_253332, _253878)) = _252840, -(lt(_253142, _253332)), -(lt(_253332, _253142))]]]]]]]]]]]]], (640 ^ _232530) ^ [_255604] : [ssList(_255604), 643 ^ _232530 : [(674 ^ _232530) ^ [] : [676 ^ _232530 : [(677 ^ _232530) ^ [] : [-(ssItem(675 ^ [_255604]))], (680 ^ _232530) ^ [] : [-(ssItem(678 ^ [_255604]))], (683 ^ _232530) ^ [] : [-(ssList(681 ^ [_255604]))], (686 ^ _232530) ^ [] : [-(ssList(684 ^ [_255604]))], (689 ^ _232530) ^ [] : [-(ssList(687 ^ [_255604]))], (691 ^ _232530) ^ [] : [-(app(app(681 ^ [_255604], cons(675 ^ [_255604], 684 ^ [_255604])), cons(678 ^ [_255604], 687 ^ [_255604])) = _255604)], (693 ^ _232530) ^ [] : [leq(675 ^ [_255604], 678 ^ [_255604])]], -(totalorderedP(_255604))], (644 ^ _232530) ^ [] : [totalorderedP(_255604), 647 ^ _232530 : [(648 ^ _232530) ^ [_255900] : [ssItem(_255900), 651 ^ _232530 : [(652 ^ _232530) ^ [_256084] : [ssItem(_256084), 655 ^ _232530 : [(656 ^ _232530) ^ [_256264] : [ssList(_256264), 659 ^ _232530 : [(660 ^ _232530) ^ [_256440] : [ssList(_256440), 663 ^ _232530 : [(664 ^ _232530) ^ [_256612] : [ssList(_256612), app(app(_256264, cons(_255900, _256440)), cons(_256084, _256612)) = _255604, -(leq(_255900, _256084))]]]]]]]]]]]]], (697 ^ _232530) ^ [_258092] : [ssList(_258092), 700 ^ _232530 : [(731 ^ _232530) ^ [] : [733 ^ _232530 : [(734 ^ _232530) ^ [] : [-(ssItem(732 ^ [_258092]))], (737 ^ _232530) ^ [] : [-(ssItem(735 ^ [_258092]))], (740 ^ _232530) ^ [] : [-(ssList(738 ^ [_258092]))], (743 ^ _232530) ^ [] : [-(ssList(741 ^ [_258092]))], (746 ^ _232530) ^ [] : [-(ssList(744 ^ [_258092]))], (748 ^ _232530) ^ [] : [-(app(app(738 ^ [_258092], cons(732 ^ [_258092], 741 ^ [_258092])), cons(735 ^ [_258092], 744 ^ [_258092])) = _258092)], (750 ^ _232530) ^ [] : [lt(732 ^ [_258092], 735 ^ [_258092])]], -(strictorderedP(_258092))], (701 ^ _232530) ^ [] : [strictorderedP(_258092), 704 ^ _232530 : [(705 ^ _232530) ^ [_258388] : [ssItem(_258388), 708 ^ _232530 : [(709 ^ _232530) ^ [_258572] : [ssItem(_258572), 712 ^ _232530 : [(713 ^ _232530) ^ [_258752] : [ssList(_258752), 716 ^ _232530 : [(717 ^ _232530) ^ [_258928] : [ssList(_258928), 720 ^ _232530 : [(721 ^ _232530) ^ [_259100] : [ssList(_259100), app(app(_258752, cons(_258388, _258928)), cons(_258572, _259100)) = _258092, -(lt(_258388, _258572))]]]]]]]]]]]]], (754 ^ _232530) ^ [_260580] : [ssList(_260580), 757 ^ _232530 : [(788 ^ _232530) ^ [] : [790 ^ _232530 : [(791 ^ _232530) ^ [] : [-(ssItem(789 ^ [_260580]))], (794 ^ _232530) ^ [] : [-(ssItem(792 ^ [_260580]))], (797 ^ _232530) ^ [] : [-(ssList(795 ^ [_260580]))], (800 ^ _232530) ^ [] : [-(ssList(798 ^ [_260580]))], (803 ^ _232530) ^ [] : [-(ssList(801 ^ [_260580]))], (805 ^ _232530) ^ [] : [-(app(app(795 ^ [_260580], cons(789 ^ [_260580], 798 ^ [_260580])), cons(792 ^ [_260580], 801 ^ [_260580])) = _260580)], (807 ^ _232530) ^ [] : [-(789 ^ [_260580] = 792 ^ [_260580])]], -(duplicatefreeP(_260580))], (758 ^ _232530) ^ [] : [duplicatefreeP(_260580), 761 ^ _232530 : [(762 ^ _232530) ^ [_260878] : [ssItem(_260878), 765 ^ _232530 : [(766 ^ _232530) ^ [_261064] : [ssItem(_261064), 769 ^ _232530 : [(770 ^ _232530) ^ [_261246] : [ssList(_261246), 773 ^ _232530 : [(774 ^ _232530) ^ [_261424] : [ssList(_261424), 777 ^ _232530 : [(778 ^ _232530) ^ [_261598] : [ssList(_261598), app(app(_261246, cons(_260878, _261424)), cons(_261064, _261598)) = _260580, _260878 = _261064]]]]]]]]]]]]], (811 ^ _232530) ^ [_263090] : [ssList(_263090), 814 ^ _232530 : [(841 ^ _232530) ^ [] : [843 ^ _232530 : [(844 ^ _232530) ^ [] : [-(ssItem(842 ^ [_263090]))], (847 ^ _232530) ^ [] : [-(ssItem(845 ^ [_263090]))], (850 ^ _232530) ^ [] : [-(ssList(848 ^ [_263090]))], (853 ^ _232530) ^ [] : [-(ssList(851 ^ [_263090]))], (855 ^ _232530) ^ [] : [-(app(848 ^ [_263090], cons(842 ^ [_263090], cons(845 ^ [_263090], 851 ^ [_263090]))) = _263090)], (857 ^ _232530) ^ [] : [842 ^ [_263090] = 845 ^ [_263090]]], -(equalelemsP(_263090))], (815 ^ _232530) ^ [] : [equalelemsP(_263090), 818 ^ _232530 : [(819 ^ _232530) ^ [_263373] : [ssItem(_263373), 822 ^ _232530 : [(823 ^ _232530) ^ [_263544] : [ssItem(_263544), 826 ^ _232530 : [(827 ^ _232530) ^ [_263711] : [ssList(_263711), 830 ^ _232530 : [(831 ^ _232530) ^ [_263874] : [ssList(_263874), app(_263711, cons(_263373, cons(_263544, _263874))) = _263090, -(_263373 = _263544)]]]]]]]]]]], (861 ^ _232530) ^ [_265107] : [ssList(_265107), 864 ^ _232530 : [(865 ^ _232530) ^ [_265245] : [ssList(_265245), 868 ^ _232530 : [(869 ^ _232530) ^ [] : [neq(_265107, _265245), _265107 = _265245], (875 ^ _232530) ^ [] : [-(_265107 = _265245), -(neq(_265107, _265245))]]]]], (881 ^ _232530) ^ [_265698] : [ssList(_265698), 884 ^ _232530 : [(885 ^ _232530) ^ [_265830] : [ssItem(_265830), -(ssList(cons(_265830, _265698)))]]], (891 ^ _232530) ^ [] : [-(ssList(nil))], (893 ^ _232530) ^ [_266088] : [ssList(_266088), 896 ^ _232530 : [(897 ^ _232530) ^ [_266223] : [ssItem(_266223), cons(_266223, _266088) = _266088]]], (903 ^ _232530) ^ [_266431] : [ssList(_266431), 906 ^ _232530 : [(907 ^ _232530) ^ [_266599] : [ssList(_266599), 910 ^ _232530 : [(911 ^ _232530) ^ [_266763] : [ssItem(_266763), 914 ^ _232530 : [(915 ^ _232530) ^ [_266923] : [ssItem(_266923), cons(_266763, _266431) = cons(_266923, _266599), 922 ^ _232530 : [(923 ^ _232530) ^ [] : [-(_266763 = _266923)], (925 ^ _232530) ^ [] : [-(_266599 = _266431)]]]]]]]]], (927 ^ _232530) ^ [_267338] : [ssList(_267338), -(nil = _267338), 935 ^ _232530 : [(936 ^ _232530) ^ [] : [-(ssList(934 ^ [_267338]))], (939 ^ _232530) ^ [] : [-(ssItem(937 ^ [_267338]))], (941 ^ _232530) ^ [] : [-(cons(937 ^ [_267338], 934 ^ [_267338]) = _267338)]]], (943 ^ _232530) ^ [_267902] : [ssList(_267902), 946 ^ _232530 : [(947 ^ _232530) ^ [_268037] : [ssItem(_268037), nil = cons(_268037, _267902)]]], (953 ^ _232530) ^ [_268245] : [ssList(_268245), -(nil = _268245), -(ssItem(hd(_268245)))], (963 ^ _232530) ^ [_268523] : [ssList(_268523), 966 ^ _232530 : [(967 ^ _232530) ^ [_268658] : [ssItem(_268658), -(hd(cons(_268658, _268523)) = _268658)]]], (973 ^ _232530) ^ [_268869] : [ssList(_268869), -(nil = _268869), -(ssList(tl(_268869)))], (983 ^ _232530) ^ [_269147] : [ssList(_269147), 986 ^ _232530 : [(987 ^ _232530) ^ [_269282] : [ssItem(_269282), -(tl(cons(_269282, _269147)) = _269147)]]], (993 ^ _232530) ^ [_269493] : [ssList(_269493), 996 ^ _232530 : [(997 ^ _232530) ^ [_269625] : [ssList(_269625), -(ssList(app(_269493, _269625)))]]], (1003 ^ _232530) ^ [_269830] : [ssList(_269830), 1006 ^ _232530 : [(1007 ^ _232530) ^ [_269982] : [ssList(_269982), 1010 ^ _232530 : [(1011 ^ _232530) ^ [_270130] : [ssItem(_270130), -(cons(_270130, app(_269982, _269830)) = app(cons(_270130, _269982), _269830))]]]]], (1017 ^ _232530) ^ [_270368] : [ssList(_270368), -(app(nil, _270368) = _270368)], (1023 ^ _232530) ^ [_270562] : [ssItem(_270562), 1026 ^ _232530 : [(1027 ^ _232530) ^ [_270704] : [ssItem(_270704), -(_270562 = _270704), leq(_270562, _270704), leq(_270704, _270562)]]], (1041 ^ _232530) ^ [_271083] : [ssItem(_271083), 1044 ^ _232530 : [(1045 ^ _232530) ^ [_271235] : [ssItem(_271235), 1048 ^ _232530 : [(1049 ^ _232530) ^ [_271383] : [ssItem(_271383), -(leq(_271083, _271383)), leq(_271083, _271235), leq(_271235, _271383)]]]]], (1063 ^ _232530) ^ [_271783] : [ssItem(_271783), -(leq(_271783, _271783))], (1069 ^ _232530) ^ [_271971] : [ssItem(_271971), 1072 ^ _232530 : [(1073 ^ _232530) ^ [_272107] : [ssItem(_272107), 1076 ^ _232530 : [(1077 ^ _232530) ^ [] : [geq(_271971, _272107), -(leq(_272107, _271971))], (1083 ^ _232530) ^ [] : [leq(_272107, _271971), -(geq(_271971, _272107))]]]]], (1089 ^ _232530) ^ [_272558] : [ssItem(_272558), 1092 ^ _232530 : [(1093 ^ _232530) ^ [_272696] : [ssItem(_272696), lt(_272558, _272696), lt(_272696, _272558)]]], (1103 ^ _232530) ^ [_272987] : [ssItem(_272987), 1106 ^ _232530 : [(1107 ^ _232530) ^ [_273139] : [ssItem(_273139), 1110 ^ _232530 : [(1111 ^ _232530) ^ [_273287] : [ssItem(_273287), -(lt(_272987, _273287)), lt(_272987, _273139), lt(_273139, _273287)]]]]], (1125 ^ _232530) ^ [_273687] : [ssItem(_273687), 1128 ^ _232530 : [(1129 ^ _232530) ^ [_273823] : [ssItem(_273823), 1132 ^ _232530 : [(1133 ^ _232530) ^ [] : [gt(_273687, _273823), -(lt(_273823, _273687))], (1139 ^ _232530) ^ [] : [lt(_273823, _273687), -(gt(_273687, _273823))]]]]], (1145 ^ _232530) ^ [_274274] : [ssItem(_274274), 1148 ^ _232530 : [(1149 ^ _232530) ^ [_274429] : [ssList(_274429), 1152 ^ _232530 : [(1153 ^ _232530) ^ [_274580] : [ssList(_274580), 1156 ^ _232530 : [(1167 ^ _232530) ^ [] : [1168 ^ _232530 : [(1169 ^ _232530) ^ [] : [memberP(_274429, _274274)], (1171 ^ _232530) ^ [] : [memberP(_274580, _274274)]], -(memberP(app(_274429, _274580), _274274))], (1157 ^ _232530) ^ [] : [memberP(app(_274429, _274580), _274274), -(memberP(_274429, _274274)), -(memberP(_274580, _274274))]]]]]]], (1175 ^ _232530) ^ [_275227] : [ssItem(_275227), 1178 ^ _232530 : [(1179 ^ _232530) ^ [_275382] : [ssItem(_275382), 1182 ^ _232530 : [(1183 ^ _232530) ^ [_275533] : [ssList(_275533), 1186 ^ _232530 : [(1197 ^ _232530) ^ [] : [1198 ^ _232530 : [(1199 ^ _232530) ^ [] : [_275227 = _275382], (1201 ^ _232530) ^ [] : [memberP(_275533, _275227)]], -(memberP(cons(_275382, _275533), _275227))], (1187 ^ _232530) ^ [] : [memberP(cons(_275382, _275533), _275227), -(_275227 = _275382), -(memberP(_275533, _275227))]]]]]]], (1205 ^ _232530) ^ [_276180] : [ssItem(_276180), memberP(nil, _276180)], (1211 ^ _232530) ^ [] : [singletonP(nil)], (1213 ^ _232530) ^ [_276421] : [ssList(_276421), 1216 ^ _232530 : [(1217 ^ _232530) ^ [_276573] : [ssList(_276573), 1220 ^ _232530 : [(1221 ^ _232530) ^ [_276721] : [ssList(_276721), -(frontsegP(_276421, _276721)), frontsegP(_276421, _276573), frontsegP(_276573, _276721)]]]]], (1235 ^ _232530) ^ [_277121] : [ssList(_277121), 1238 ^ _232530 : [(1239 ^ _232530) ^ [_277263] : [ssList(_277263), -(_277121 = _277263), frontsegP(_277121, _277263), frontsegP(_277263, _277121)]]], (1253 ^ _232530) ^ [_277642] : [ssList(_277642), -(frontsegP(_277642, _277642))], (1259 ^ _232530) ^ [_277830] : [ssList(_277830), 1262 ^ _232530 : [(1263 ^ _232530) ^ [_277979] : [ssList(_277979), 1266 ^ _232530 : [(1267 ^ _232530) ^ [_278124] : [ssList(_278124), frontsegP(_277830, _277979), -(frontsegP(app(_277830, _278124), _277979))]]]]], (1277 ^ _232530) ^ [_278437] : [ssItem(_278437), 1280 ^ _232530 : [(1281 ^ _232530) ^ [_278605] : [ssItem(_278605), 1284 ^ _232530 : [(1285 ^ _232530) ^ [_278769] : [ssList(_278769), 1288 ^ _232530 : [(1289 ^ _232530) ^ [_278929] : [ssList(_278929), 1292 ^ _232530 : [(1293 ^ _232530) ^ [] : [frontsegP(cons(_278437, _278769), cons(_278605, _278929)), 1296 ^ _232530 : [(1297 ^ _232530) ^ [] : [-(_278437 = _278605)], (1299 ^ _232530) ^ [] : [-(frontsegP(_278769, _278929))]]], (1301 ^ _232530) ^ [] : [-(frontsegP(cons(_278437, _278769), cons(_278605, _278929))), _278437 = _278605, frontsegP(_278769, _278929)]]]]]]]]], (1311 ^ _232530) ^ [_279614] : [ssList(_279614), -(frontsegP(_279614, nil))], (1317 ^ _232530) ^ [_279802] : [ssList(_279802), 1320 ^ _232530 : [(1321 ^ _232530) ^ [] : [frontsegP(nil, _279802), -(nil = _279802)], (1327 ^ _232530) ^ [] : [nil = _279802, -(frontsegP(nil, _279802))]]], (1333 ^ _232530) ^ [_280230] : [ssList(_280230), 1336 ^ _232530 : [(1337 ^ _232530) ^ [_280382] : [ssList(_280382), 1340 ^ _232530 : [(1341 ^ _232530) ^ [_280530] : [ssList(_280530), -(rearsegP(_280230, _280530)), rearsegP(_280230, _280382), rearsegP(_280382, _280530)]]]]], (1355 ^ _232530) ^ [_280930] : [ssList(_280930), 1358 ^ _232530 : [(1359 ^ _232530) ^ [_281072] : [ssList(_281072), -(_280930 = _281072), rearsegP(_280930, _281072), rearsegP(_281072, _280930)]]], (1373 ^ _232530) ^ [_281451] : [ssList(_281451), -(rearsegP(_281451, _281451))], (1379 ^ _232530) ^ [_281639] : [ssList(_281639), 1382 ^ _232530 : [(1383 ^ _232530) ^ [_281788] : [ssList(_281788), 1386 ^ _232530 : [(1387 ^ _232530) ^ [_281933] : [ssList(_281933), rearsegP(_281639, _281788), -(rearsegP(app(_281933, _281639), _281788))]]]]], (1397 ^ _232530) ^ [_282246] : [ssList(_282246), -(rearsegP(_282246, nil))], (1403 ^ _232530) ^ [_282434] : [ssList(_282434), 1406 ^ _232530 : [(1407 ^ _232530) ^ [] : [rearsegP(nil, _282434), -(nil = _282434)], (1413 ^ _232530) ^ [] : [nil = _282434, -(rearsegP(nil, _282434))]]], (1419 ^ _232530) ^ [_282862] : [ssList(_282862), 1422 ^ _232530 : [(1423 ^ _232530) ^ [_283014] : [ssList(_283014), 1426 ^ _232530 : [(1427 ^ _232530) ^ [_283162] : [ssList(_283162), -(segmentP(_282862, _283162)), segmentP(_282862, _283014), segmentP(_283014, _283162)]]]]], (1441 ^ _232530) ^ [_283562] : [ssList(_283562), 1444 ^ _232530 : [(1445 ^ _232530) ^ [_283704] : [ssList(_283704), -(_283562 = _283704), segmentP(_283562, _283704), segmentP(_283704, _283562)]]], (1459 ^ _232530) ^ [_284083] : [ssList(_284083), -(segmentP(_284083, _284083))], (1465 ^ _232530) ^ [_284271] : [ssList(_284271), 1468 ^ _232530 : [(1469 ^ _232530) ^ [_284433] : [ssList(_284433), 1472 ^ _232530 : [(1473 ^ _232530) ^ [_284591] : [ssList(_284591), 1476 ^ _232530 : [(1477 ^ _232530) ^ [_284745] : [ssList(_284745), segmentP(_284271, _284433), -(segmentP(app(app(_284591, _284271), _284745), _284433))]]]]]]], (1487 ^ _232530) ^ [_285081] : [ssList(_285081), -(segmentP(_285081, nil))], (1493 ^ _232530) ^ [_285269] : [ssList(_285269), 1496 ^ _232530 : [(1497 ^ _232530) ^ [] : [segmentP(nil, _285269), -(nil = _285269)], (1503 ^ _232530) ^ [] : [nil = _285269, -(segmentP(nil, _285269))]]], (1509 ^ _232530) ^ [_285697] : [ssItem(_285697), -(cyclefreeP(cons(_285697, nil)))], (1515 ^ _232530) ^ [] : [-(cyclefreeP(nil))], (1517 ^ _232530) ^ [_285942] : [ssItem(_285942), -(totalorderP(cons(_285942, nil)))], (1523 ^ _232530) ^ [] : [-(totalorderP(nil))], (1525 ^ _232530) ^ [_286187] : [ssItem(_286187), -(strictorderP(cons(_286187, nil)))], (1531 ^ _232530) ^ [] : [-(strictorderP(nil))], (1533 ^ _232530) ^ [_286432] : [ssItem(_286432), -(totalorderedP(cons(_286432, nil)))], (1539 ^ _232530) ^ [] : [-(totalorderedP(nil))], (1541 ^ _232530) ^ [_286677] : [ssItem(_286677), 1544 ^ _232530 : [(1545 ^ _232530) ^ [_286836] : [ssList(_286836), 1548 ^ _232530 : [(1549 ^ _232530) ^ [] : [totalorderedP(cons(_286677, _286836)), -(nil = _286836), 1556 ^ _232530 : [(1557 ^ _232530) ^ [] : [nil = _286836], (1559 ^ _232530) ^ [] : [-(totalorderedP(_286836))], (1561 ^ _232530) ^ [] : [-(leq(_286677, hd(_286836)))]]], (1563 ^ _232530) ^ [] : [-(totalorderedP(cons(_286677, _286836))), 1564 ^ _232530 : [(1565 ^ _232530) ^ [] : [nil = _286836], (1567 ^ _232530) ^ [] : [-(nil = _286836), totalorderedP(_286836), leq(_286677, hd(_286836))]]]]]]], (1579 ^ _232530) ^ [_287771] : [ssItem(_287771), -(strictorderedP(cons(_287771, nil)))], (1585 ^ _232530) ^ [] : [-(strictorderedP(nil))], (1587 ^ _232530) ^ [_288016] : [ssItem(_288016), 1590 ^ _232530 : [(1591 ^ _232530) ^ [_288175] : [ssList(_288175), 1594 ^ _232530 : [(1595 ^ _232530) ^ [] : [strictorderedP(cons(_288016, _288175)), -(nil = _288175), 1602 ^ _232530 : [(1603 ^ _232530) ^ [] : [nil = _288175], (1605 ^ _232530) ^ [] : [-(strictorderedP(_288175))], (1607 ^ _232530) ^ [] : [-(lt(_288016, hd(_288175)))]]], (1609 ^ _232530) ^ [] : [-(strictorderedP(cons(_288016, _288175))), 1610 ^ _232530 : [(1611 ^ _232530) ^ [] : [nil = _288175], (1613 ^ _232530) ^ [] : [-(nil = _288175), strictorderedP(_288175), lt(_288016, hd(_288175))]]]]]]], (1625 ^ _232530) ^ [_289110] : [ssItem(_289110), -(duplicatefreeP(cons(_289110, nil)))], (1631 ^ _232530) ^ [] : [-(duplicatefreeP(nil))], (1633 ^ _232530) ^ [_289355] : [ssItem(_289355), -(equalelemsP(cons(_289355, nil)))], (1639 ^ _232530) ^ [] : [-(equalelemsP(nil))], (1641 ^ _232530) ^ [_289600] : [ssList(_289600), -(nil = _289600), 1649 ^ _232530 : [(1650 ^ _232530) ^ [] : [-(ssItem(1648 ^ [_289600]))], (1652 ^ _232530) ^ [] : [-(hd(_289600) = 1648 ^ [_289600])]]], (1654 ^ _232530) ^ [_290014] : [ssList(_290014), -(nil = _290014), 1662 ^ _232530 : [(1663 ^ _232530) ^ [] : [-(ssList(1661 ^ [_290014]))], (1665 ^ _232530) ^ [] : [-(tl(_290014) = 1661 ^ [_290014])]]], (1667 ^ _232530) ^ [_290428] : [ssList(_290428), 1670 ^ _232530 : [(1671 ^ _232530) ^ [_290594] : [ssList(_290594), -(_290594 = _290428), -(nil = _290594), -(nil = _290428), hd(_290594) = hd(_290428), tl(_290594) = tl(_290428)]]], (1693 ^ _232530) ^ [_291173] : [ssList(_291173), -(nil = _291173), -(cons(hd(_291173), tl(_291173)) = _291173)], (1703 ^ _232530) ^ [_291463] : [ssList(_291463), 1706 ^ _232530 : [(1707 ^ _232530) ^ [_291615] : [ssList(_291615), 1710 ^ _232530 : [(1711 ^ _232530) ^ [_291763] : [ssList(_291763), app(_291763, _291615) = app(_291463, _291615), -(_291763 = _291463)]]]]], (1721 ^ _232530) ^ [_292082] : [ssList(_292082), 1724 ^ _232530 : [(1725 ^ _232530) ^ [_292234] : [ssList(_292234), 1728 ^ _232530 : [(1729 ^ _232530) ^ [_292382] : [ssList(_292382), app(_292234, _292382) = app(_292234, _292082), -(_292382 = _292082)]]]]], (1739 ^ _232530) ^ [_292701] : [ssList(_292701), 1742 ^ _232530 : [(1743 ^ _232530) ^ [_292840] : [ssItem(_292840), -(cons(_292840, _292701) = app(cons(_292840, nil), _292701))]]], (1749 ^ _232530) ^ [_293059] : [ssList(_293059), 1752 ^ _232530 : [(1753 ^ _232530) ^ [_293211] : [ssList(_293211), 1756 ^ _232530 : [(1757 ^ _232530) ^ [_293359] : [ssList(_293359), -(app(app(_293059, _293211), _293359) = app(_293059, app(_293211, _293359)))]]]]], (1763 ^ _232530) ^ [_293597] : [ssList(_293597), 1766 ^ _232530 : [(1767 ^ _232530) ^ [_293742] : [ssList(_293742), 1770 ^ _232530 : [(1771 ^ _232530) ^ [] : [nil = app(_293597, _293742), 1774 ^ _232530 : [(1775 ^ _232530) ^ [] : [-(nil = _293742)], (1777 ^ _232530) ^ [] : [-(nil = _293597)]]], (1779 ^ _232530) ^ [] : [-(nil = app(_293597, _293742)), nil = _293742, nil = _293597]]]]], (1789 ^ _232530) ^ [_294360] : [ssList(_294360), -(app(_294360, nil) = _294360)], (1795 ^ _232530) ^ [_294554] : [ssList(_294554), 1798 ^ _232530 : [(1799 ^ _232530) ^ [_294699] : [ssList(_294699), -(nil = _294554), -(hd(app(_294554, _294699)) = hd(_294554))]]], (1809 ^ _232530) ^ [_295006] : [ssList(_295006), 1812 ^ _232530 : [(1813 ^ _232530) ^ [_295154] : [ssList(_295154), -(nil = _295006), -(tl(app(_295006, _295154)) = app(tl(_295006), _295154))]]], (1823 ^ _232530) ^ [_295467] : [ssItem(_295467), 1826 ^ _232530 : [(1827 ^ _232530) ^ [_295609] : [ssItem(_295609), -(_295467 = _295609), geq(_295467, _295609), geq(_295609, _295467)]]], (1841 ^ _232530) ^ [_295988] : [ssItem(_295988), 1844 ^ _232530 : [(1845 ^ _232530) ^ [_296140] : [ssItem(_296140), 1848 ^ _232530 : [(1849 ^ _232530) ^ [_296288] : [ssItem(_296288), -(geq(_295988, _296288)), geq(_295988, _296140), geq(_296140, _296288)]]]]], (1863 ^ _232530) ^ [_296688] : [ssItem(_296688), -(geq(_296688, _296688))], (1869 ^ _232530) ^ [_296876] : [ssItem(_296876), lt(_296876, _296876)], (1875 ^ _232530) ^ [_297065] : [ssItem(_297065), 1878 ^ _232530 : [(1879 ^ _232530) ^ [_297217] : [ssItem(_297217), 1882 ^ _232530 : [(1883 ^ _232530) ^ [_297365] : [ssItem(_297365), -(lt(_297065, _297365)), leq(_297065, _297217), lt(_297217, _297365)]]]]], (1897 ^ _232530) ^ [_297765] : [ssItem(_297765), 1900 ^ _232530 : [(1901 ^ _232530) ^ [_297907] : [ssItem(_297907), leq(_297765, _297907), -(_297765 = _297907), -(lt(_297765, _297907))]]], (1915 ^ _232530) ^ [_298287] : [ssItem(_298287), 1918 ^ _232530 : [(1919 ^ _232530) ^ [_298431] : [ssItem(_298431), 1922 ^ _232530 : [(1923 ^ _232530) ^ [] : [lt(_298287, _298431), 1926 ^ _232530 : [(1927 ^ _232530) ^ [] : [_298287 = _298431], (1929 ^ _232530) ^ [] : [-(leq(_298287, _298431))]]], (1931 ^ _232530) ^ [] : [-(lt(_298287, _298431)), -(_298287 = _298431), leq(_298287, _298431)]]]]], (1941 ^ _232530) ^ [_299042] : [ssItem(_299042), 1944 ^ _232530 : [(1945 ^ _232530) ^ [_299180] : [ssItem(_299180), gt(_299042, _299180), gt(_299180, _299042)]]], (1955 ^ _232530) ^ [_299451] : [ssItem(_299451), 1958 ^ _232530 : [(1959 ^ _232530) ^ [_299603] : [ssItem(_299603), 1962 ^ _232530 : [(1963 ^ _232530) ^ [_299751] : [ssItem(_299751), -(gt(_299451, _299751)), gt(_299451, _299603), gt(_299603, _299751)]]]]]], input).
% 10.30/10.70 ncf('1',plain,[segmentP(1979 ^ [], 1976 ^ [])],start(1995 ^ 0)).
% 10.30/10.70 ncf('1.1',plain,[-(segmentP(1979 ^ [], 1976 ^ [])), segmentP(1985 ^ [], 1982 ^ []), 1985 ^ [] = 1979 ^ [], 1982 ^ [] = 1976 ^ []],extension(232 ^ 1,bind([[_239808, _239810, _239812, _239814], [1976 ^ [], 1982 ^ [], 1979 ^ [], 1985 ^ []]]))).
% 10.30/10.70 ncf('1.1.1',plain,[-(segmentP(1985 ^ [], 1982 ^ [])), 1999 : -(nil = 1985 ^ [])],extension(1997 ^ 2)).
% 10.30/10.70 ncf('1.1.1.1',plain,[nil = 1985 ^ [], -(segmentP(1985 ^ [], 1982 ^ [])), segmentP(nil, nil), nil = 1982 ^ []],extension(232 ^ 5,bind([[_239808, _239810, _239812, _239814], [1982 ^ [], nil, 1985 ^ [], nil]]))).
% 10.30/10.70 ncf('1.1.1.1.1',plain,[segmentP(1985 ^ [], 1982 ^ [])],reduction('1.1')).
% 10.30/10.70 ncf('1.1.1.1.2',plain,[-(segmentP(nil, nil)), ssList(nil)],extension(1459 ^ 6,bind([[_284083], [nil]]))).
% 10.30/10.70 ncf('1.1.1.1.2.1',plain,[-(ssList(nil))],extension(891 ^ 7)).
% 10.30/10.70 ncf('1.1.1.1.3',plain,[-(nil = 1982 ^ [])],extension(2001 ^ 6)).
% 10.30/10.70 ncf('1.1.2',plain,[-(1985 ^ [] = 1979 ^ []), 1979 ^ [] = 1985 ^ []],extension(4 ^ 2,bind([[_232781, _232783], [1985 ^ [], 1979 ^ []]]))).
% 10.30/10.70 ncf('1.1.2.1',plain,[-(1979 ^ [] = 1985 ^ [])],extension(1989 ^ 3)).
% 10.30/10.70 ncf('1.1.3',plain,[-(1982 ^ [] = 1976 ^ []), 1976 ^ [] = 1982 ^ []],extension(4 ^ 2,bind([[_232781, _232783], [1982 ^ [], 1976 ^ []]]))).
% 10.30/10.70 ncf('1.1.3.1',plain,[-(1976 ^ [] = 1982 ^ [])],extension(1991 ^ 3)).
% 10.30/10.70 %-----------------------------------------------------
% 10.30/10.70 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------