%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWC153+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri May 19 12:12:42 EDT 2023
% Result : Theorem 210.25s 203.12s
% Output : Proof 210.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWC153+1 : TPTP v8.1.2. Released v2.4.0.
% 0.00/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n020.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Fri May 19 01:10:32 EDT 2023
% 0.13/0.33 % CPUTime :
% 210.25/203.12
% 210.25/203.12 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 210.25/203.12 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 210.25/203.12 %-----------------------------------------------------
% 210.25/203.12 ncf(matrix, plain, [(2050 ^ _339987) ^ [] : [-(app(app(app(app(2040 ^ [], cons(2034 ^ [], nil)), 2043 ^ []), cons(2037 ^ [], nil)), 2046 ^ []) = 1976 ^ [])], (2052 ^ _339987) ^ [] : [-(leq(2037 ^ [], 2034 ^ []))], (2045 ^ _339987) ^ [] : [-(ssList(2043 ^ []))], (1978 ^ _339987) ^ [] : [-(ssList(1976 ^ []))], (1981 ^ _339987) ^ [] : [-(ssList(1979 ^ []))], (1984 ^ _339987) ^ [] : [-(ssList(1982 ^ []))], (2036 ^ _339987) ^ [] : [-(ssItem(2034 ^ []))], (2048 ^ _339987) ^ [] : [-(ssList(2046 ^ []))], (1993 ^ _339987) ^ [_341285] : [ssItem(_341285), 1996 ^ _339987 : [(1997 ^ _339987) ^ [_341509] : [ssItem(_341509), 2000 ^ _339987 : [(2001 ^ _339987) ^ [_341729] : [ssList(_341729), 2004 ^ _339987 : [(2005 ^ _339987) ^ [_341945] : [ssList(_341945), 2008 ^ _339987 : [(2009 ^ _339987) ^ [_342157] : [ssList(_342157), app(app(app(app(_341729, cons(_341285, nil)), _341945), cons(_341509, nil)), _342157) = 1982 ^ [], leq(_341509, _341285), 2020 ^ _339987 : [(2023 ^ _339987) ^ [_342637] : [ssItem(_342637), memberP(_341945, _342637), 2030 ^ _339987 : [(2033 ^ _339987) ^ [] : [-(leq(_342637, _341509))], (2031 ^ _339987) ^ [] : [-(leq(_341285, _342637))]]], (2021 ^ _339987) ^ [] : [-(leq(_341285, _341509))]]]]]]]]]]], (1991 ^ _339987) ^ [] : [-(1982 ^ [] = 1976 ^ [])], (1987 ^ _339987) ^ [] : [-(ssList(1985 ^ []))], (2042 ^ _339987) ^ [] : [-(ssList(2040 ^ []))], (1989 ^ _339987) ^ [] : [-(1985 ^ [] = 1979 ^ [])], (2039 ^ _339987) ^ [] : [-(ssItem(2037 ^ []))], (2054 ^ _339987) ^ [] : [leq(2034 ^ [], 2037 ^ []), 2056 ^ _339987 : [(2061 ^ _339987) ^ [] : [leq(2055 ^ [], 2037 ^ []), leq(2034 ^ [], 2055 ^ [])], (2059 ^ _339987) ^ [] : [-(memberP(2043 ^ [], 2055 ^ []))], (2057 ^ _339987) ^ [] : [-(ssItem(2055 ^ []))]]], !, (252 ^ _271468) ^ [_279442, _279444] : [_279444 = _279442, -(tl(_279444) = tl(_279442))], (891 ^ _271468) ^ [] : [-(ssList(nil))], (1023 ^ _271468) ^ [_309480] : [ssItem(_309480), 1026 ^ _271468 : [(1027 ^ _271468) ^ [_309622] : [ssItem(_309622), -(_309480 = _309622), leq(_309480, _309622), leq(_309622, _309480)]]], (299 ^ _271468) ^ [] : [-(ssItem(297 ^ []))], (1531 ^ _271468) ^ [] : [-(strictorderP(nil))], (1517 ^ _271468) ^ [_324860] : [ssItem(_324860), -(totalorderP(cons(_324860, nil)))], (1145 ^ _271468) ^ [_313192] : [ssItem(_313192), 1148 ^ _271468 : [(1149 ^ _271468) ^ [_313347] : [ssList(_313347), 1152 ^ _271468 : [(1153 ^ _271468) ^ [_313498] : [ssList(_313498), 1156 ^ _271468 : [(1157 ^ _271468) ^ [] : [memberP(app(_313347, _313498), _313192), -(memberP(_313347, _313192)), -(memberP(_313498, _313192))], (1167 ^ _271468) ^ [] : [1168 ^ _271468 : [(1171 ^ _271468) ^ [] : [memberP(_313498, _313192)], (1169 ^ _271468) ^ [] : [memberP(_313347, _313192)]], -(memberP(app(_313347, _313498), _313192))]]]]]]], (340 ^ _271468) ^ [_282462] : [ssList(_282462), 343 ^ _271468 : [(353 ^ _271468) ^ [] : [-(singletonP(_282462)), 354 ^ _271468 : [(355 ^ _271468) ^ [_282911] : [ssItem(_282911), cons(_282911, nil) = _282462]]], (344 ^ _271468) ^ [] : [singletonP(_282462), 348 ^ _271468 : [(351 ^ _271468) ^ [] : [-(cons(347 ^ [_282462], nil) = _282462)], (349 ^ _271468) ^ [] : [-(ssItem(347 ^ [_282462]))]]]]], (1863 ^ _271468) ^ [_335606] : [ssItem(_335606), -(geq(_335606, _335606))], (304 ^ _271468) ^ [] : [297 ^ [] = 300 ^ []], (306 ^ _271468) ^ [_281213] : [ssList(_281213), 309 ^ _271468 : [(310 ^ _271468) ^ [_281375] : [ssItem(_281375), 313 ^ _271468 : [(326 ^ _271468) ^ [] : [-(memberP(_281213, _281375)), 327 ^ _271468 : [(328 ^ _271468) ^ [_282023] : [ssList(_282023), 331 ^ _271468 : [(332 ^ _271468) ^ [_282171] : [ssList(_282171), app(_282023, cons(_281375, _282171)) = _281213]]]]], (314 ^ _271468) ^ [] : [memberP(_281213, _281375), 318 ^ _271468 : [(324 ^ _271468) ^ [] : [-(app(317 ^ [_281213, _281375], cons(_281375, 320 ^ [_281213, _281375])) = _281213)], (322 ^ _271468) ^ [] : [-(ssList(320 ^ [_281213, _281375]))], (319 ^ _271468) ^ [] : [-(ssList(317 ^ [_281213, _281375]))]]]]]]], (1841 ^ _271468) ^ [_334906] : [ssItem(_334906), 1844 ^ _271468 : [(1845 ^ _271468) ^ [_335058] : [ssItem(_335058), 1848 ^ _271468 : [(1849 ^ _271468) ^ [_335206] : [ssItem(_335206), -(geq(_334906, _335206)), geq(_334906, _335058), geq(_335058, _335206)]]]]], (1441 ^ _271468) ^ [_322480] : [ssList(_322480), 1444 ^ _271468 : [(1445 ^ _271468) ^ [_322622] : [ssList(_322622), -(_322480 = _322622), segmentP(_322480, _322622), segmentP(_322622, _322480)]]], (1459 ^ _271468) ^ [_323001] : [ssList(_323001), -(segmentP(_323001, _323001))], (184 ^ _271468) ^ [_277268, _277270, _277272, _277274] : [-(gt(_277272, _277268)), gt(_277274, _277270), _277274 = _277272, _277270 = _277268], (697 ^ _271468) ^ [_297010] : [ssList(_297010), 700 ^ _271468 : [(701 ^ _271468) ^ [] : [strictorderedP(_297010), 704 ^ _271468 : [(705 ^ _271468) ^ [_297306] : [ssItem(_297306), 708 ^ _271468 : [(709 ^ _271468) ^ [_297490] : [ssItem(_297490), 712 ^ _271468 : [(713 ^ _271468) ^ [_297670] : [ssList(_297670), 716 ^ _271468 : [(717 ^ _271468) ^ [_297846] : [ssList(_297846), 720 ^ _271468 : [(721 ^ _271468) ^ [_298018] : [ssList(_298018), app(app(_297670, cons(_297306, _297846)), cons(_297490, _298018)) = _297010, -(lt(_297306, _297490))]]]]]]]]]]], (731 ^ _271468) ^ [] : [733 ^ _271468 : [(746 ^ _271468) ^ [] : [-(ssList(744 ^ [_297010]))], (737 ^ _271468) ^ [] : [-(ssItem(735 ^ [_297010]))], (734 ^ _271468) ^ [] : [-(ssItem(732 ^ [_297010]))], (740 ^ _271468) ^ [] : [-(ssList(738 ^ [_297010]))], (748 ^ _271468) ^ [] : [-(app(app(738 ^ [_297010], cons(732 ^ [_297010], 741 ^ [_297010])), cons(735 ^ [_297010], 744 ^ [_297010])) = _297010)], (750 ^ _271468) ^ [] : [lt(732 ^ [_297010], 735 ^ [_297010])], (743 ^ _271468) ^ [] : [-(ssList(741 ^ [_297010]))]], -(strictorderedP(_297010))]]], (451 ^ _271468) ^ [_286208] : [ssList(_286208), 454 ^ _271468 : [(455 ^ _271468) ^ [] : [cyclefreeP(_286208), 458 ^ _271468 : [(459 ^ _271468) ^ [_286512] : [ssItem(_286512), 462 ^ _271468 : [(463 ^ _271468) ^ [_286704] : [ssItem(_286704), 466 ^ _271468 : [(467 ^ _271468) ^ [_286892] : [ssList(_286892), 470 ^ _271468 : [(471 ^ _271468) ^ [_287076] : [ssList(_287076), 474 ^ _271468 : [(475 ^ _271468) ^ [_287256] : [ssList(_287256), app(app(_286892, cons(_286512, _287076)), cons(_286704, _287256)) = _286208, leq(_286512, _286704), leq(_286704, _286512)]]]]]]]]]]], (489 ^ _271468) ^ [] : [491 ^ _271468 : [(501 ^ _271468) ^ [] : [-(ssList(499 ^ [_286208]))], (506 ^ _271468) ^ [] : [-(app(app(496 ^ [_286208], cons(490 ^ [_286208], 499 ^ [_286208])), cons(493 ^ [_286208], 502 ^ [_286208])) = _286208)], (504 ^ _271468) ^ [] : [-(ssList(502 ^ [_286208]))], (508 ^ _271468) ^ [] : [-(leq(490 ^ [_286208], 493 ^ [_286208]))], (495 ^ _271468) ^ [] : [-(ssItem(493 ^ [_286208]))], (492 ^ _271468) ^ [] : [-(ssItem(490 ^ [_286208]))], (498 ^ _271468) ^ [] : [-(ssList(496 ^ [_286208]))], (510 ^ _271468) ^ [] : [-(leq(493 ^ [_286208], 490 ^ [_286208]))]], -(cyclefreeP(_286208))]]], (893 ^ _271468) ^ [_305006] : [ssList(_305006), 896 ^ _271468 : [(897 ^ _271468) ^ [_305141] : [ssItem(_305141), cons(_305141, _305006) = _305006]]], (1541 ^ _271468) ^ [_325595] : [ssItem(_325595), 1544 ^ _271468 : [(1545 ^ _271468) ^ [_325754] : [ssList(_325754), 1548 ^ _271468 : [(1563 ^ _271468) ^ [] : [-(totalorderedP(cons(_325595, _325754))), 1564 ^ _271468 : [(1567 ^ _271468) ^ [] : [-(nil = _325754), totalorderedP(_325754), leq(_325595, hd(_325754))], (1565 ^ _271468) ^ [] : [nil = _325754]]], (1549 ^ _271468) ^ [] : [totalorderedP(cons(_325595, _325754)), -(nil = _325754), 1556 ^ _271468 : [(1561 ^ _271468) ^ [] : [-(leq(_325595, hd(_325754)))], (1559 ^ _271468) ^ [] : [-(totalorderedP(_325754))], (1557 ^ _271468) ^ [] : [nil = _325754]]]]]]], (1465 ^ _271468) ^ [_323189] : [ssList(_323189), 1468 ^ _271468 : [(1469 ^ _271468) ^ [_323351] : [ssList(_323351), 1472 ^ _271468 : [(1473 ^ _271468) ^ [_323509] : [ssList(_323509), 1476 ^ _271468 : [(1477 ^ _271468) ^ [_323663] : [ssList(_323663), segmentP(_323189, _323351), -(segmentP(app(app(_323509, _323189), _323663), _323351))]]]]]]], (1587 ^ _271468) ^ [_326934] : [ssItem(_326934), 1590 ^ _271468 : [(1591 ^ _271468) ^ [_327093] : [ssList(_327093), 1594 ^ _271468 : [(1609 ^ _271468) ^ [] : [-(strictorderedP(cons(_326934, _327093))), 1610 ^ _271468 : [(1613 ^ _271468) ^ [] : [-(nil = _327093), strictorderedP(_327093), lt(_326934, hd(_327093))], (1611 ^ _271468) ^ [] : [nil = _327093]]], (1595 ^ _271468) ^ [] : [strictorderedP(cons(_326934, _327093)), -(nil = _327093), 1602 ^ _271468 : [(1607 ^ _271468) ^ [] : [-(lt(_326934, hd(_327093)))], (1605 ^ _271468) ^ [] : [-(strictorderedP(_327093))], (1603 ^ _271468) ^ [] : [nil = _327093]]]]]]], (1311 ^ _271468) ^ [_318532] : [ssList(_318532), -(frontsegP(_318532, nil))], (2 ^ _271468) ^ [_271592] : [-(_271592 = _271592)], (1089 ^ _271468) ^ [_311476] : [ssItem(_311476), 1092 ^ _271468 : [(1093 ^ _271468) ^ [_311614] : [ssItem(_311614), lt(_311476, _311614), lt(_311614, _311476)]]], (1739 ^ _271468) ^ [_331619] : [ssList(_331619), 1742 ^ _271468 : [(1743 ^ _271468) ^ [_331758] : [ssItem(_331758), -(cons(_331758, _331619) = app(cons(_331758, nil), _331619))]]], (4 ^ _271468) ^ [_271699, _271701] : [_271701 = _271699, -(_271699 = _271701)], (1955 ^ _271468) ^ [_338369] : [ssItem(_338369), 1958 ^ _271468 : [(1959 ^ _271468) ^ [_338521] : [ssItem(_338521), 1962 ^ _271468 : [(1963 ^ _271468) ^ [_338669] : [ssItem(_338669), -(gt(_338369, _338669)), gt(_338369, _338521), gt(_338521, _338669)]]]]], (514 ^ _271468) ^ [_288994] : [ssList(_288994), 517 ^ _271468 : [(518 ^ _271468) ^ [] : [totalorderP(_288994), 521 ^ _271468 : [(522 ^ _271468) ^ [_289296] : [ssItem(_289296), 525 ^ _271468 : [(526 ^ _271468) ^ [_289486] : [ssItem(_289486), 529 ^ _271468 : [(530 ^ _271468) ^ [_289672] : [ssList(_289672), 533 ^ _271468 : [(534 ^ _271468) ^ [_289854] : [ssList(_289854), 537 ^ _271468 : [(538 ^ _271468) ^ [_290032] : [ssList(_290032), app(app(_289672, cons(_289296, _289854)), cons(_289486, _290032)) = _288994, -(leq(_289296, _289486)), -(leq(_289486, _289296))]]]]]]]]]]], (552 ^ _271468) ^ [] : [554 ^ _271468 : [(564 ^ _271468) ^ [] : [-(ssList(562 ^ [_288994]))], (569 ^ _271468) ^ [] : [-(app(app(559 ^ [_288994], cons(553 ^ [_288994], 562 ^ [_288994])), cons(556 ^ [_288994], 565 ^ [_288994])) = _288994)], (567 ^ _271468) ^ [] : [-(ssList(565 ^ [_288994]))], (571 ^ _271468) ^ [] : [leq(553 ^ [_288994], 556 ^ [_288994])], (558 ^ _271468) ^ [] : [-(ssItem(556 ^ [_288994]))], (555 ^ _271468) ^ [] : [-(ssItem(553 ^ [_288994]))], (561 ^ _271468) ^ [] : [-(ssList(559 ^ [_288994]))], (573 ^ _271468) ^ [] : [leq(556 ^ [_288994], 553 ^ [_288994])]], -(totalorderP(_288994))]]], (927 ^ _271468) ^ [_306256] : [ssList(_306256), -(nil = _306256), 935 ^ _271468 : [(941 ^ _271468) ^ [] : [-(cons(937 ^ [_306256], 934 ^ [_306256]) = _306256)], (939 ^ _271468) ^ [] : [-(ssItem(937 ^ [_306256]))], (936 ^ _271468) ^ [] : [-(ssList(934 ^ [_306256]))]]], (811 ^ _271468) ^ [_302008] : [ssList(_302008), 814 ^ _271468 : [(815 ^ _271468) ^ [] : [equalelemsP(_302008), 818 ^ _271468 : [(819 ^ _271468) ^ [_302291] : [ssItem(_302291), 822 ^ _271468 : [(823 ^ _271468) ^ [_302462] : [ssItem(_302462), 826 ^ _271468 : [(827 ^ _271468) ^ [_302629] : [ssList(_302629), 830 ^ _271468 : [(831 ^ _271468) ^ [_302792] : [ssList(_302792), app(_302629, cons(_302291, cons(_302462, _302792))) = _302008, -(_302291 = _302462)]]]]]]]]], (841 ^ _271468) ^ [] : [843 ^ _271468 : [(855 ^ _271468) ^ [] : [-(app(848 ^ [_302008], cons(842 ^ [_302008], cons(845 ^ [_302008], 851 ^ [_302008]))) = _302008)], (853 ^ _271468) ^ [] : [-(ssList(851 ^ [_302008]))], (857 ^ _271468) ^ [] : [842 ^ [_302008] = 845 ^ [_302008]], (844 ^ _271468) ^ [] : [-(ssItem(842 ^ [_302008]))], (847 ^ _271468) ^ [] : [-(ssItem(845 ^ [_302008]))], (850 ^ _271468) ^ [] : [-(ssList(848 ^ [_302008]))]], -(equalelemsP(_302008))]]], (1041 ^ _271468) ^ [_310001] : [ssItem(_310001), 1044 ^ _271468 : [(1045 ^ _271468) ^ [_310153] : [ssItem(_310153), 1048 ^ _271468 : [(1049 ^ _271468) ^ [_310301] : [ssItem(_310301), -(leq(_310001, _310301)), leq(_310001, _310153), leq(_310153, _310301)]]]]], (218 ^ _271468) ^ [_278302, _278304, _278306, _278308] : [-(memberP(_278306, _278302)), memberP(_278308, _278304), _278308 = _278306, _278304 = _278302], (208 ^ _271468) ^ [_277979, _277981] : [-(ssItem(_277979)), _277981 = _277979, ssItem(_277981)], (963 ^ _271468) ^ [_307441] : [ssList(_307441), 966 ^ _271468 : [(967 ^ _271468) ^ [_307576] : [ssItem(_307576), -(hd(cons(_307576, _307441)) = _307576)]]], (1355 ^ _271468) ^ [_319848] : [ssList(_319848), 1358 ^ _271468 : [(1359 ^ _271468) ^ [_319990] : [ssList(_319990), -(_319848 = _319990), rearsegP(_319848, _319990), rearsegP(_319990, _319848)]]], (417 ^ _271468) ^ [_284959] : [ssList(_284959), 420 ^ _271468 : [(421 ^ _271468) ^ [_285121] : [ssList(_285121), 424 ^ _271468 : [(437 ^ _271468) ^ [] : [-(segmentP(_284959, _285121)), 438 ^ _271468 : [(439 ^ _271468) ^ [_285769] : [ssList(_285769), 442 ^ _271468 : [(443 ^ _271468) ^ [_285917] : [ssList(_285917), app(app(_285769, _285121), _285917) = _284959]]]]], (425 ^ _271468) ^ [] : [segmentP(_284959, _285121), 429 ^ _271468 : [(435 ^ _271468) ^ [] : [-(app(app(428 ^ [_284959, _285121], _285121), 431 ^ [_284959, _285121]) = _284959)], (433 ^ _271468) ^ [] : [-(ssList(431 ^ [_284959, _285121]))], (430 ^ _271468) ^ [] : [-(ssList(428 ^ [_284959, _285121]))]]]]]]], (1525 ^ _271468) ^ [_325105] : [ssItem(_325105), -(strictorderP(cons(_325105, nil)))], (1017 ^ _271468) ^ [_309286] : [ssList(_309286), -(app(nil, _309286) = _309286)], (1175 ^ _271468) ^ [_314145] : [ssItem(_314145), 1178 ^ _271468 : [(1179 ^ _271468) ^ [_314300] : [ssItem(_314300), 1182 ^ _271468 : [(1183 ^ _271468) ^ [_314451] : [ssList(_314451), 1186 ^ _271468 : [(1187 ^ _271468) ^ [] : [memberP(cons(_314300, _314451), _314145), -(_314145 = _314300), -(memberP(_314451, _314145))], (1197 ^ _271468) ^ [] : [1198 ^ _271468 : [(1201 ^ _271468) ^ [] : [memberP(_314451, _314145)], (1199 ^ _271468) ^ [] : [_314145 = _314300]], -(memberP(cons(_314300, _314451), _314145))]]]]]]], (861 ^ _271468) ^ [_304025] : [ssList(_304025), 864 ^ _271468 : [(865 ^ _271468) ^ [_304163] : [ssList(_304163), 868 ^ _271468 : [(875 ^ _271468) ^ [] : [-(_304025 = _304163), -(neq(_304025, _304163))], (869 ^ _271468) ^ [] : [neq(_304025, _304163), _304025 = _304163]]]]], (170 ^ _271468) ^ [_276824, _276826, _276828, _276830] : [-(lt(_276828, _276824)), lt(_276830, _276826), _276830 = _276828, _276826 = _276824], (640 ^ _271468) ^ [_294522] : [ssList(_294522), 643 ^ _271468 : [(644 ^ _271468) ^ [] : [totalorderedP(_294522), 647 ^ _271468 : [(648 ^ _271468) ^ [_294818] : [ssItem(_294818), 651 ^ _271468 : [(652 ^ _271468) ^ [_295002] : [ssItem(_295002), 655 ^ _271468 : [(656 ^ _271468) ^ [_295182] : [ssList(_295182), 659 ^ _271468 : [(660 ^ _271468) ^ [_295358] : [ssList(_295358), 663 ^ _271468 : [(664 ^ _271468) ^ [_295530] : [ssList(_295530), app(app(_295182, cons(_294818, _295358)), cons(_295002, _295530)) = _294522, -(leq(_294818, _295002))]]]]]]]]]]], (674 ^ _271468) ^ [] : [676 ^ _271468 : [(689 ^ _271468) ^ [] : [-(ssList(687 ^ [_294522]))], (680 ^ _271468) ^ [] : [-(ssItem(678 ^ [_294522]))], (677 ^ _271468) ^ [] : [-(ssItem(675 ^ [_294522]))], (683 ^ _271468) ^ [] : [-(ssList(681 ^ [_294522]))], (691 ^ _271468) ^ [] : [-(app(app(681 ^ [_294522], cons(675 ^ [_294522], 684 ^ [_294522])), cons(678 ^ [_294522], 687 ^ [_294522])) = _294522)], (693 ^ _271468) ^ [] : [leq(675 ^ [_294522], 678 ^ [_294522])], (686 ^ _271468) ^ [] : [-(ssList(684 ^ [_294522]))]], -(totalorderedP(_294522))]]], (1277 ^ _271468) ^ [_317355] : [ssItem(_317355), 1280 ^ _271468 : [(1281 ^ _271468) ^ [_317523] : [ssItem(_317523), 1284 ^ _271468 : [(1285 ^ _271468) ^ [_317687] : [ssList(_317687), 1288 ^ _271468 : [(1289 ^ _271468) ^ [_317847] : [ssList(_317847), 1292 ^ _271468 : [(1301 ^ _271468) ^ [] : [-(frontsegP(cons(_317355, _317687), cons(_317523, _317847))), _317355 = _317523, frontsegP(_317687, _317847)], (1293 ^ _271468) ^ [] : [frontsegP(cons(_317355, _317687), cons(_317523, _317847)), 1296 ^ _271468 : [(1299 ^ _271468) ^ [] : [-(frontsegP(_317687, _317847))], (1297 ^ _271468) ^ [] : [-(_317355 = _317523)]]]]]]]]]]], (1205 ^ _271468) ^ [_315098] : [ssItem(_315098), memberP(nil, _315098)], (1631 ^ _271468) ^ [] : [-(duplicatefreeP(nil))], (10 ^ _271468) ^ [_271903, _271905, _271907] : [-(_271907 = _271903), _271907 = _271905, _271905 = _271903], (1213 ^ _271468) ^ [_315339] : [ssList(_315339), 1216 ^ _271468 : [(1217 ^ _271468) ^ [_315491] : [ssList(_315491), 1220 ^ _271468 : [(1221 ^ _271468) ^ [_315639] : [ssList(_315639), -(frontsegP(_315339, _315639)), frontsegP(_315339, _315491), frontsegP(_315491, _315639)]]]]], (1125 ^ _271468) ^ [_312605] : [ssItem(_312605), 1128 ^ _271468 : [(1129 ^ _271468) ^ [_312741] : [ssItem(_312741), 1132 ^ _271468 : [(1139 ^ _271468) ^ [] : [lt(_312741, _312605), -(gt(_312605, _312741))], (1133 ^ _271468) ^ [] : [gt(_312605, _312741), -(lt(_312741, _312605))]]]]], (246 ^ _271468) ^ [_279224, _279226] : [_279226 = _279224, -(hd(_279226) = hd(_279224))], (1317 ^ _271468) ^ [_318720] : [ssList(_318720), 1320 ^ _271468 : [(1327 ^ _271468) ^ [] : [nil = _318720, -(frontsegP(nil, _318720))], (1321 ^ _271468) ^ [] : [frontsegP(nil, _318720), -(nil = _318720)]]], (1875 ^ _271468) ^ [_335983] : [ssItem(_335983), 1878 ^ _271468 : [(1879 ^ _271468) ^ [_336135] : [ssItem(_336135), 1882 ^ _271468 : [(1883 ^ _271468) ^ [_336283] : [ssItem(_336283), -(lt(_335983, _336283)), leq(_335983, _336135), lt(_336135, _336283)]]]]], (1823 ^ _271468) ^ [_334385] : [ssItem(_334385), 1826 ^ _271468 : [(1827 ^ _271468) ^ [_334527] : [ssItem(_334527), -(_334385 = _334527), geq(_334385, _334527), geq(_334527, _334385)]]], (1373 ^ _271468) ^ [_320369] : [ssList(_320369), -(rearsegP(_320369, _320369))], (302 ^ _271468) ^ [] : [-(ssItem(300 ^ []))], (1693 ^ _271468) ^ [_330091] : [ssList(_330091), -(nil = _330091), -(cons(hd(_330091), tl(_330091)) = _330091)], (1641 ^ _271468) ^ [_328518] : [ssList(_328518), -(nil = _328518), 1649 ^ _271468 : [(1652 ^ _271468) ^ [] : [-(hd(_328518) = 1648 ^ [_328518])], (1650 ^ _271468) ^ [] : [-(ssItem(1648 ^ [_328518]))]]], (1789 ^ _271468) ^ [_333278] : [ssList(_333278), -(app(_333278, nil) = _333278)], (1721 ^ _271468) ^ [_331000] : [ssList(_331000), 1724 ^ _271468 : [(1725 ^ _271468) ^ [_331152] : [ssList(_331152), 1728 ^ _271468 : [(1729 ^ _271468) ^ [_331300] : [ssList(_331300), app(_331152, _331300) = app(_331152, _331000), -(_331300 = _331000)]]]]], (86 ^ _271468) ^ [_274287, _274289] : [-(cyclefreeP(_274287)), _274289 = _274287, cyclefreeP(_274289)], (1211 ^ _271468) ^ [] : [singletonP(nil)], (136 ^ _271468) ^ [_275762, _275764] : [-(duplicatefreeP(_275762)), _275764 = _275762, duplicatefreeP(_275764)], (1795 ^ _271468) ^ [_333472] : [ssList(_333472), 1798 ^ _271468 : [(1799 ^ _271468) ^ [_333617] : [ssList(_333617), -(nil = _333472), -(hd(app(_333472, _333617)) = hd(_333472))]]], (953 ^ _271468) ^ [_307163] : [ssList(_307163), -(nil = _307163), -(ssItem(hd(_307163)))], (44 ^ _271468) ^ [_272983, _272985, _272987, _272989] : [-(frontsegP(_272987, _272983)), frontsegP(_272989, _272985), _272989 = _272987, _272985 = _272983], (20 ^ _271468) ^ [_272244, _272246, _272248, _272250] : [-(neq(_272248, _272244)), neq(_272250, _272246), _272250 = _272248, _272246 = _272244], (34 ^ _271468) ^ [_272660, _272662] : [-(singletonP(_272660)), _272662 = _272660, singletonP(_272662)], (232 ^ _271468) ^ [_278726, _278728, _278730, _278732] : [-(leq(_278730, _278726)), leq(_278732, _278728), _278732 = _278730, _278728 = _278726], (1493 ^ _271468) ^ [_324187] : [ssList(_324187), 1496 ^ _271468 : [(1503 ^ _271468) ^ [] : [nil = _324187, -(segmentP(nil, _324187))], (1497 ^ _271468) ^ [] : [segmentP(nil, _324187), -(nil = _324187)]]], (983 ^ _271468) ^ [_308065] : [ssList(_308065), 986 ^ _271468 : [(987 ^ _271468) ^ [_308200] : [ssItem(_308200), -(tl(cons(_308200, _308065)) = _308065)]]], (1515 ^ _271468) ^ [] : [-(cyclefreeP(nil))], (268 ^ _271468) ^ [_280027, _280029, _280031, _280033] : [-(cons(_280033, _280029) = cons(_280031, _280027)), _280033 = _280031, _280029 = _280027], (1063 ^ _271468) ^ [_310701] : [ssItem(_310701), -(leq(_310701, _310701))], (1633 ^ _271468) ^ [_328273] : [ssItem(_328273), -(equalelemsP(cons(_328273, nil)))], (1419 ^ _271468) ^ [_321780] : [ssList(_321780), 1422 ^ _271468 : [(1423 ^ _271468) ^ [_321932] : [ssList(_321932), 1426 ^ _271468 : [(1427 ^ _271468) ^ [_322080] : [ssList(_322080), -(segmentP(_321780, _322080)), segmentP(_321780, _321932), segmentP(_321932, _322080)]]]]], (1487 ^ _271468) ^ [_323999] : [ssList(_323999), -(segmentP(_323999, nil))], (1235 ^ _271468) ^ [_316039] : [ssList(_316039), 1238 ^ _271468 : [(1239 ^ _271468) ^ [_316181] : [ssList(_316181), -(_316039 = _316181), frontsegP(_316039, _316181), frontsegP(_316181, _316039)]]], (198 ^ _271468) ^ [_277684, _277686] : [-(ssList(_277684)), _277686 = _277684, ssList(_277686)], (258 ^ _271468) ^ [_279688, _279690, _279692, _279694] : [-(app(_279694, _279690) = app(_279692, _279688)), _279694 = _279692, _279690 = _279688], (1941 ^ _271468) ^ [_337960] : [ssItem(_337960), 1944 ^ _271468 : [(1945 ^ _271468) ^ [_338098] : [ssItem(_338098), gt(_337960, _338098), gt(_338098, _337960)]]], (1003 ^ _271468) ^ [_308748] : [ssList(_308748), 1006 ^ _271468 : [(1007 ^ _271468) ^ [_308900] : [ssList(_308900), 1010 ^ _271468 : [(1011 ^ _271468) ^ [_309048] : [ssItem(_309048), -(cons(_309048, app(_308900, _308748)) = app(cons(_309048, _308900), _308748))]]]]], (754 ^ _271468) ^ [_299498] : [ssList(_299498), 757 ^ _271468 : [(758 ^ _271468) ^ [] : [duplicatefreeP(_299498), 761 ^ _271468 : [(762 ^ _271468) ^ [_299796] : [ssItem(_299796), 765 ^ _271468 : [(766 ^ _271468) ^ [_299982] : [ssItem(_299982), 769 ^ _271468 : [(770 ^ _271468) ^ [_300164] : [ssList(_300164), 773 ^ _271468 : [(774 ^ _271468) ^ [_300342] : [ssList(_300342), 777 ^ _271468 : [(778 ^ _271468) ^ [_300516] : [ssList(_300516), app(app(_300164, cons(_299796, _300342)), cons(_299982, _300516)) = _299498, _299796 = _299982]]]]]]]]]]], (788 ^ _271468) ^ [] : [790 ^ _271468 : [(803 ^ _271468) ^ [] : [-(ssList(801 ^ [_299498]))], (794 ^ _271468) ^ [] : [-(ssItem(792 ^ [_299498]))], (791 ^ _271468) ^ [] : [-(ssItem(789 ^ [_299498]))], (797 ^ _271468) ^ [] : [-(ssList(795 ^ [_299498]))], (805 ^ _271468) ^ [] : [-(app(app(795 ^ [_299498], cons(789 ^ [_299498], 798 ^ [_299498])), cons(792 ^ [_299498], 801 ^ [_299498])) = _299498)], (807 ^ _271468) ^ [] : [-(789 ^ [_299498] = 792 ^ [_299498])], (800 ^ _271468) ^ [] : [-(ssList(798 ^ [_299498]))]], -(duplicatefreeP(_299498))]]], (1915 ^ _271468) ^ [_337205] : [ssItem(_337205), 1918 ^ _271468 : [(1919 ^ _271468) ^ [_337349] : [ssItem(_337349), 1922 ^ _271468 : [(1931 ^ _271468) ^ [] : [-(lt(_337205, _337349)), -(_337205 = _337349), leq(_337205, _337349)], (1923 ^ _271468) ^ [] : [lt(_337205, _337349), 1926 ^ _271468 : [(1929 ^ _271468) ^ [] : [-(leq(_337205, _337349))], (1927 ^ _271468) ^ [] : [_337205 = _337349]]]]]]], (993 ^ _271468) ^ [_308411] : [ssList(_308411), 996 ^ _271468 : [(997 ^ _271468) ^ [_308543] : [ssList(_308543), -(ssList(app(_308411, _308543)))]]], (1749 ^ _271468) ^ [_331977] : [ssList(_331977), 1752 ^ _271468 : [(1753 ^ _271468) ^ [_332129] : [ssList(_332129), 1756 ^ _271468 : [(1757 ^ _271468) ^ [_332277] : [ssList(_332277), -(app(app(_331977, _332129), _332277) = app(_331977, app(_332129, _332277)))]]]]], (1103 ^ _271468) ^ [_311905] : [ssItem(_311905), 1106 ^ _271468 : [(1107 ^ _271468) ^ [_312057] : [ssItem(_312057), 1110 ^ _271468 : [(1111 ^ _271468) ^ [_312205] : [ssItem(_312205), -(lt(_311905, _312205)), lt(_311905, _312057), lt(_312057, _312205)]]]]], (156 ^ _271468) ^ [_276380, _276382, _276384, _276386] : [-(geq(_276384, _276380)), geq(_276386, _276382), _276386 = _276384, _276382 = _276380], (1579 ^ _271468) ^ [_326689] : [ssItem(_326689), -(strictorderedP(cons(_326689, nil)))], (96 ^ _271468) ^ [_274582, _274584] : [-(totalorderP(_274582)), _274584 = _274582, totalorderP(_274584)], (1625 ^ _271468) ^ [_328028] : [ssItem(_328028), -(duplicatefreeP(cons(_328028, nil)))], (1333 ^ _271468) ^ [_319148] : [ssList(_319148), 1336 ^ _271468 : [(1337 ^ _271468) ^ [_319300] : [ssList(_319300), 1340 ^ _271468 : [(1341 ^ _271468) ^ [_319448] : [ssList(_319448), -(rearsegP(_319148, _319448)), rearsegP(_319148, _319300), rearsegP(_319300, _319448)]]]]], (1253 ^ _271468) ^ [_316560] : [ssList(_316560), -(frontsegP(_316560, _316560))], (1259 ^ _271468) ^ [_316748] : [ssList(_316748), 1262 ^ _271468 : [(1263 ^ _271468) ^ [_316897] : [ssList(_316897), 1266 ^ _271468 : [(1267 ^ _271468) ^ [_317042] : [ssList(_317042), frontsegP(_316748, _316897), -(frontsegP(app(_316748, _317042), _316897))]]]]], (72 ^ _271468) ^ [_273871, _273873, _273875, _273877] : [-(segmentP(_273875, _273871)), segmentP(_273877, _273873), _273877 = _273875, _273873 = _273871], (1069 ^ _271468) ^ [_310889] : [ssItem(_310889), 1072 ^ _271468 : [(1073 ^ _271468) ^ [_311025] : [ssItem(_311025), 1076 ^ _271468 : [(1083 ^ _271468) ^ [] : [leq(_311025, _310889), -(geq(_310889, _311025))], (1077 ^ _271468) ^ [] : [geq(_310889, _311025), -(leq(_311025, _310889))]]]]], (881 ^ _271468) ^ [_304616] : [ssList(_304616), 884 ^ _271468 : [(885 ^ _271468) ^ [_304748] : [ssItem(_304748), -(ssList(cons(_304748, _304616)))]]], (278 ^ _271468) ^ [_280362] : [ssItem(_280362), 281 ^ _271468 : [(282 ^ _271468) ^ [_280500] : [ssItem(_280500), 285 ^ _271468 : [(292 ^ _271468) ^ [] : [-(_280362 = _280500), -(neq(_280362, _280500))], (286 ^ _271468) ^ [] : [neq(_280362, _280500), _280362 = _280500]]]]], (116 ^ _271468) ^ [_275172, _275174] : [-(totalorderedP(_275172)), _275174 = _275172, totalorderedP(_275174)], (1403 ^ _271468) ^ [_321352] : [ssList(_321352), 1406 ^ _271468 : [(1413 ^ _271468) ^ [] : [nil = _321352, -(rearsegP(nil, _321352))], (1407 ^ _271468) ^ [] : [rearsegP(nil, _321352), -(nil = _321352)]]], (1869 ^ _271468) ^ [_335794] : [ssItem(_335794), lt(_335794, _335794)], (1897 ^ _271468) ^ [_336683] : [ssItem(_336683), 1900 ^ _271468 : [(1901 ^ _271468) ^ [_336825] : [ssItem(_336825), leq(_336683, _336825), -(_336683 = _336825), -(lt(_336683, _336825))]]], (577 ^ _271468) ^ [_291758] : [ssList(_291758), 580 ^ _271468 : [(581 ^ _271468) ^ [] : [strictorderP(_291758), 584 ^ _271468 : [(585 ^ _271468) ^ [_292060] : [ssItem(_292060), 588 ^ _271468 : [(589 ^ _271468) ^ [_292250] : [ssItem(_292250), 592 ^ _271468 : [(593 ^ _271468) ^ [_292436] : [ssList(_292436), 596 ^ _271468 : [(597 ^ _271468) ^ [_292618] : [ssList(_292618), 600 ^ _271468 : [(601 ^ _271468) ^ [_292796] : [ssList(_292796), app(app(_292436, cons(_292060, _292618)), cons(_292250, _292796)) = _291758, -(lt(_292060, _292250)), -(lt(_292250, _292060))]]]]]]]]]]], (615 ^ _271468) ^ [] : [617 ^ _271468 : [(627 ^ _271468) ^ [] : [-(ssList(625 ^ [_291758]))], (632 ^ _271468) ^ [] : [-(app(app(622 ^ [_291758], cons(616 ^ [_291758], 625 ^ [_291758])), cons(619 ^ [_291758], 628 ^ [_291758])) = _291758)], (630 ^ _271468) ^ [] : [-(ssList(628 ^ [_291758]))], (634 ^ _271468) ^ [] : [lt(616 ^ [_291758], 619 ^ [_291758])], (621 ^ _271468) ^ [] : [-(ssItem(619 ^ [_291758]))], (618 ^ _271468) ^ [] : [-(ssItem(616 ^ [_291758]))], (624 ^ _271468) ^ [] : [-(ssList(622 ^ [_291758]))], (636 ^ _271468) ^ [] : [lt(619 ^ [_291758], 616 ^ [_291758])]], -(strictorderP(_291758))]]], (1667 ^ _271468) ^ [_329346] : [ssList(_329346), 1670 ^ _271468 : [(1671 ^ _271468) ^ [_329512] : [ssList(_329512), -(_329512 = _329346), -(nil = _329512), -(nil = _329346), hd(_329512) = hd(_329346), tl(_329512) = tl(_329346)]]], (1703 ^ _271468) ^ [_330381] : [ssList(_330381), 1706 ^ _271468 : [(1707 ^ _271468) ^ [_330533] : [ssList(_330533), 1710 ^ _271468 : [(1711 ^ _271468) ^ [_330681] : [ssList(_330681), app(_330681, _330533) = app(_330381, _330533), -(_330681 = _330381)]]]]], (390 ^ _271468) ^ [_284063] : [ssList(_284063), 393 ^ _271468 : [(394 ^ _271468) ^ [_284212] : [ssList(_284212), 397 ^ _271468 : [(407 ^ _271468) ^ [] : [-(rearsegP(_284063, _284212)), 408 ^ _271468 : [(409 ^ _271468) ^ [_284687] : [ssList(_284687), app(_284687, _284212) = _284063]]], (398 ^ _271468) ^ [] : [rearsegP(_284063, _284212), 402 ^ _271468 : [(405 ^ _271468) ^ [] : [-(app(401 ^ [_284063, _284212], _284212) = _284063)], (403 ^ _271468) ^ [] : [-(ssList(401 ^ [_284063, _284212]))]]]]]]], (973 ^ _271468) ^ [_307787] : [ssList(_307787), -(nil = _307787), -(ssList(tl(_307787)))], (1533 ^ _271468) ^ [_325350] : [ssItem(_325350), -(totalorderedP(cons(_325350, nil)))], (1763 ^ _271468) ^ [_332515] : [ssList(_332515), 1766 ^ _271468 : [(1767 ^ _271468) ^ [_332660] : [ssList(_332660), 1770 ^ _271468 : [(1779 ^ _271468) ^ [] : [-(nil = app(_332515, _332660)), nil = _332660, nil = _332515], (1771 ^ _271468) ^ [] : [nil = app(_332515, _332660), 1774 ^ _271468 : [(1777 ^ _271468) ^ [] : [-(nil = _332515)], (1775 ^ _271468) ^ [] : [-(nil = _332660)]]]]]]], (106 ^ _271468) ^ [_274877, _274879] : [-(strictorderP(_274877)), _274879 = _274877, strictorderP(_274879)], (363 ^ _271468) ^ [_283167] : [ssList(_283167), 366 ^ _271468 : [(367 ^ _271468) ^ [_283316] : [ssList(_283316), 370 ^ _271468 : [(380 ^ _271468) ^ [] : [-(frontsegP(_283167, _283316)), 381 ^ _271468 : [(382 ^ _271468) ^ [_283791] : [ssList(_283791), app(_283316, _283791) = _283167]]], (371 ^ _271468) ^ [] : [frontsegP(_283167, _283316), 375 ^ _271468 : [(378 ^ _271468) ^ [] : [-(app(_283316, 374 ^ [_283167, _283316]) = _283167)], (376 ^ _271468) ^ [] : [-(ssList(374 ^ [_283167, _283316]))]]]]]]], (1654 ^ _271468) ^ [_328932] : [ssList(_328932), -(nil = _328932), 1662 ^ _271468 : [(1665 ^ _271468) ^ [] : [-(tl(_328932) = 1661 ^ [_328932])], (1663 ^ _271468) ^ [] : [-(ssList(1661 ^ [_328932]))]]], (1809 ^ _271468) ^ [_333924] : [ssList(_333924), 1812 ^ _271468 : [(1813 ^ _271468) ^ [_334072] : [ssList(_334072), -(nil = _333924), -(tl(app(_333924, _334072)) = app(tl(_333924), _334072))]]], (1523 ^ _271468) ^ [] : [-(totalorderP(nil))], (1397 ^ _271468) ^ [_321164] : [ssList(_321164), -(rearsegP(_321164, nil))], (1639 ^ _271468) ^ [] : [-(equalelemsP(nil))], (1379 ^ _271468) ^ [_320557] : [ssList(_320557), 1382 ^ _271468 : [(1383 ^ _271468) ^ [_320706] : [ssList(_320706), 1386 ^ _271468 : [(1387 ^ _271468) ^ [_320851] : [ssList(_320851), rearsegP(_320557, _320706), -(rearsegP(app(_320851, _320557), _320706))]]]]], (126 ^ _271468) ^ [_275467, _275469] : [-(strictorderedP(_275467)), _275469 = _275467, strictorderedP(_275469)], (146 ^ _271468) ^ [_276057, _276059] : [-(equalelemsP(_276057)), _276059 = _276057, equalelemsP(_276059)], (1585 ^ _271468) ^ [] : [-(strictorderedP(nil))], (903 ^ _271468) ^ [_305349] : [ssList(_305349), 906 ^ _271468 : [(907 ^ _271468) ^ [_305517] : [ssList(_305517), 910 ^ _271468 : [(911 ^ _271468) ^ [_305681] : [ssItem(_305681), 914 ^ _271468 : [(915 ^ _271468) ^ [_305841] : [ssItem(_305841), cons(_305681, _305349) = cons(_305841, _305517), 922 ^ _271468 : [(925 ^ _271468) ^ [] : [-(_305517 = _305349)], (923 ^ _271468) ^ [] : [-(_305681 = _305841)]]]]]]]]], (58 ^ _271468) ^ [_273427, _273429, _273431, _273433] : [-(rearsegP(_273431, _273427)), rearsegP(_273433, _273429), _273433 = _273431, _273429 = _273427], (1539 ^ _271468) ^ [] : [-(totalorderedP(nil))], (1509 ^ _271468) ^ [_324615] : [ssItem(_324615), -(cyclefreeP(cons(_324615, nil)))], (943 ^ _271468) ^ [_306820] : [ssList(_306820), 946 ^ _271468 : [(947 ^ _271468) ^ [_306955] : [ssItem(_306955), nil = cons(_306955, _306820)]]]], input).
% 210.25/203.12 ncf('1',plain,[-(app(app(app(app(2040 ^ [], cons(2034 ^ [], nil)), 2043 ^ []), cons(2037 ^ [], nil)), 2046 ^ []) = 1976 ^ [])],start(2050 ^ 0)).
% 210.25/203.12 ncf('1.1',plain,[app(app(app(app(2040 ^ [], cons(2034 ^ [], nil)), 2043 ^ []), cons(2037 ^ [], nil)), 2046 ^ []) = 1976 ^ [], -(app(app(app(app(2040 ^ [], cons(2034 ^ [], nil)), 2043 ^ []), cons(2037 ^ [], nil)), 2046 ^ []) = 1982 ^ []), 1976 ^ [] = 1982 ^ []],extension(10 ^ 1,bind([[_271903, _271905, _271907], [1982 ^ [], 1976 ^ [], app(app(app(app(2040 ^ [], cons(2034 ^ [], nil)), 2043 ^ []), cons(2037 ^ [], nil)), 2046 ^ [])]]))).
% 210.25/203.12 ncf('1.1.1',plain,[app(app(app(app(2040 ^ [], cons(2034 ^ [], nil)), 2043 ^ []), cons(2037 ^ [], nil)), 2046 ^ []) = 1982 ^ [], 2009 : ssList(2046 ^ []), 2009 : leq(2037 ^ [], 2034 ^ []), 2021 : -(leq(2034 ^ [], 2037 ^ [])), 2009 : ssList(2043 ^ []), 2005 : ssList(2040 ^ []), 2001 : ssItem(2037 ^ []), 1997 : ssItem(2034 ^ [])],extension(1993 ^ 2,bind([[_341285, _341509, _341729, _341945, _342157], [2034 ^ [], 2037 ^ [], 2040 ^ [], 2043 ^ [], 2046 ^ []]]))).
% 210.25/203.12 ncf('1.1.1.1',plain,[-(ssList(2046 ^ []))],extension(2048 ^ 11)).
% 210.25/203.12 ncf('1.1.1.2',plain,[-(leq(2037 ^ [], 2034 ^ []))],extension(2052 ^ 11)).
% 210.25/203.12 ncf('1.1.1.3',plain,[leq(2034 ^ [], 2037 ^ []), 2061 : leq(2055 ^ [], 2037 ^ []), 2061 : leq(2034 ^ [], 2055 ^ [])],extension(2054 ^ 13)).
% 210.25/203.12 ncf('1.1.1.3.1',plain,[-(leq(2055 ^ [], 2037 ^ [])), ssItem(2055 ^ []), memberP(2043 ^ [], 2055 ^ [])],extension(2023 ^ 16,bind([[_342637], [2055 ^ []]]))).
% 210.25/203.12 ncf('1.1.1.3.1.1',plain,[-(ssItem(2055 ^ []))],extension(2057 ^ 17)).
% 210.25/203.12 ncf('1.1.1.3.1.2',plain,[-(memberP(2043 ^ [], 2055 ^ []))],extension(2059 ^ 17)).
% 210.25/203.12 ncf('1.1.1.3.2',plain,[-(leq(2034 ^ [], 2055 ^ [])), ssItem(2055 ^ []), memberP(2043 ^ [], 2055 ^ [])],extension(2023 ^ 16,bind([[_342637], [2055 ^ []]]))).
% 210.25/203.12 ncf('1.1.1.3.2.1',plain,[-(ssItem(2055 ^ []))],extension(2057 ^ 17)).
% 210.25/203.12 ncf('1.1.1.3.2.2',plain,[-(memberP(2043 ^ [], 2055 ^ []))],extension(2059 ^ 17)).
% 210.25/203.12 ncf('1.1.1.4',plain,[-(ssList(2043 ^ []))],extension(2045 ^ 9)).
% 210.25/203.12 ncf('1.1.1.5',plain,[-(ssList(2040 ^ []))],extension(2042 ^ 7)).
% 210.25/203.12 ncf('1.1.1.6',plain,[-(ssItem(2037 ^ []))],extension(2039 ^ 5)).
% 210.25/203.12 ncf('1.1.1.7',plain,[-(ssItem(2034 ^ []))],extension(2036 ^ 3)).
% 210.25/203.12 ncf('1.1.2',plain,[-(1976 ^ [] = 1982 ^ []), 1982 ^ [] = 1976 ^ []],extension(4 ^ 2,bind([[_271699, _271701], [1976 ^ [], 1982 ^ []]]))).
% 210.25/203.12 ncf('1.1.2.1',plain,[-(1982 ^ [] = 1976 ^ [])],extension(1991 ^ 3)).
% 210.25/203.12 %-----------------------------------------------------
% 210.25/203.12 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------