%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWC096+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:12:30 EDT 2023
% Result : Theorem 94.57s 91.40s
% Output : Proof 94.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWC096+1 : TPTP v8.1.2. Released v2.4.0.
% 0.07/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 00:59:51 EDT 2023
% 0.12/0.34 % CPUTime :
% 94.57/91.40
% 94.57/91.40 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 94.57/91.40 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 94.57/91.40 %-----------------------------------------------------
% 94.57/91.40 ncf(matrix, plain, [(1984 ^ _326718) ^ [] : [-(ssList(1982 ^ []))], (1991 ^ _326718) ^ [] : [-(1976 ^ [] = 1982 ^ [])], (1993 ^ _326718) ^ [] : [2020 ^ _326718 : [(2023 ^ _326718) ^ [] : [neq(1985 ^ [], nil)], (2021 ^ _326718) ^ [] : [-(neq(1979 ^ [], nil))]], 1994 ^ _326718 : [(2012 ^ _326718) ^ [] : [-(ssItem(2010 ^ []))], (1995 ^ _326718) ^ [] : [-(neq(1979 ^ [], nil))], (1997 ^ _326718) ^ [_327695] : [ssItem(_327695), 2000 ^ _326718 : [(2001 ^ _326718) ^ [_327840] : [ssList(_327840), cons(_327695, nil) = 1976 ^ [], app(_327840, cons(_327695, nil)) = 1979 ^ []]]], (2017 ^ _326718) ^ [] : [-(cons(2010 ^ [], nil) = 1982 ^ [])], (2019 ^ _326718) ^ [] : [-(app(2013 ^ [], cons(2010 ^ [], nil)) = 1985 ^ [])], (2015 ^ _326718) ^ [] : [-(ssList(2013 ^ []))]]], (1987 ^ _326718) ^ [] : [-(ssList(1985 ^ []))], (1978 ^ _326718) ^ [] : [-(ssList(1976 ^ []))], (1981 ^ _326718) ^ [] : [-(ssList(1979 ^ []))], (1989 ^ _326718) ^ [] : [-(1979 ^ [] = 1985 ^ [])], !, (861 ^ _258327) ^ [_290884] : [ssList(_290884), 864 ^ _258327 : [(865 ^ _258327) ^ [_291022] : [ssList(_291022), 868 ^ _258327 : [(875 ^ _258327) ^ [] : [-(_290884 = _291022), -(neq(_290884, _291022))], (869 ^ _258327) ^ [] : [neq(_290884, _291022), _290884 = _291022]]]]], (252 ^ _258327) ^ [_266301, _266303] : [_266303 = _266301, -(tl(_266303) = tl(_266301))], (72 ^ _258327) ^ [_260730, _260732, _260734, _260736] : [-(segmentP(_260734, _260730)), segmentP(_260736, _260732), _260736 = _260734, _260732 = _260730], (1355 ^ _258327) ^ [_306707] : [ssList(_306707), 1358 ^ _258327 : [(1359 ^ _258327) ^ [_306849] : [ssList(_306849), -(_306707 = _306849), rearsegP(_306707, _306849), rearsegP(_306849, _306707)]]], (1459 ^ _258327) ^ [_309860] : [ssList(_309860), -(segmentP(_309860, _309860))], (106 ^ _258327) ^ [_261736, _261738] : [-(strictorderP(_261736)), _261738 = _261736, strictorderP(_261738)], (58 ^ _258327) ^ [_260286, _260288, _260290, _260292] : [-(rearsegP(_260290, _260286)), rearsegP(_260292, _260288), _260292 = _260290, _260288 = _260286], (943 ^ _258327) ^ [_293679] : [ssList(_293679), 946 ^ _258327 : [(947 ^ _258327) ^ [_293814] : [ssItem(_293814), nil = cons(_293814, _293679)]]], (1869 ^ _258327) ^ [_322653] : [ssItem(_322653), lt(_322653, _322653)], (136 ^ _258327) ^ [_262621, _262623] : [-(duplicatefreeP(_262621)), _262623 = _262621, duplicatefreeP(_262623)], (232 ^ _258327) ^ [_265585, _265587, _265589, _265591] : [-(neq(_265589, _265585)), neq(_265591, _265587), _265591 = _265589, _265587 = _265585], (2 ^ _258327) ^ [_258451] : [-(_258451 = _258451)], (1633 ^ _258327) ^ [_315132] : [ssItem(_315132), -(equalelemsP(cons(_315132, nil)))], (268 ^ _258327) ^ [_266886, _266888, _266890, _266892] : [-(cons(_266892, _266888) = cons(_266890, _266886)), _266892 = _266890, _266888 = _266886], (1145 ^ _258327) ^ [_300051] : [ssItem(_300051), 1148 ^ _258327 : [(1149 ^ _258327) ^ [_300206] : [ssList(_300206), 1152 ^ _258327 : [(1153 ^ _258327) ^ [_300357] : [ssList(_300357), 1156 ^ _258327 : [(1157 ^ _258327) ^ [] : [memberP(app(_300206, _300357), _300051), -(memberP(_300206, _300051)), -(memberP(_300357, _300051))], (1167 ^ _258327) ^ [] : [1168 ^ _258327 : [(1171 ^ _258327) ^ [] : [memberP(_300357, _300051)], (1169 ^ _258327) ^ [] : [memberP(_300206, _300051)]], -(memberP(app(_300206, _300357), _300051))]]]]]]], (278 ^ _258327) ^ [_267221] : [ssItem(_267221), 281 ^ _258327 : [(282 ^ _258327) ^ [_267359] : [ssItem(_267359), 285 ^ _258327 : [(292 ^ _258327) ^ [] : [-(_267221 = _267359), -(neq(_267221, _267359))], (286 ^ _258327) ^ [] : [neq(_267221, _267359), _267221 = _267359]]]]], (1213 ^ _258327) ^ [_302198] : [ssList(_302198), 1216 ^ _258327 : [(1217 ^ _258327) ^ [_302350] : [ssList(_302350), 1220 ^ _258327 : [(1221 ^ _258327) ^ [_302498] : [ssList(_302498), -(frontsegP(_302198, _302498)), frontsegP(_302198, _302350), frontsegP(_302350, _302498)]]]]], (390 ^ _258327) ^ [_270922] : [ssList(_270922), 393 ^ _258327 : [(394 ^ _258327) ^ [_271071] : [ssList(_271071), 397 ^ _258327 : [(407 ^ _258327) ^ [] : [-(rearsegP(_270922, _271071)), 408 ^ _258327 : [(409 ^ _258327) ^ [_271546] : [ssList(_271546), app(_271546, _271071) = _270922]]], (398 ^ _258327) ^ [] : [rearsegP(_270922, _271071), 402 ^ _258327 : [(405 ^ _258327) ^ [] : [-(app(401 ^ [_270922, _271071], _271071) = _270922)], (403 ^ _258327) ^ [] : [-(ssList(401 ^ [_270922, _271071]))]]]]]]], (1017 ^ _258327) ^ [_296145] : [ssList(_296145), -(app(nil, _296145) = _296145)], (1063 ^ _258327) ^ [_297560] : [ssItem(_297560), -(leq(_297560, _297560))], (1749 ^ _258327) ^ [_318836] : [ssList(_318836), 1752 ^ _258327 : [(1753 ^ _258327) ^ [_318988] : [ssList(_318988), 1756 ^ _258327 : [(1757 ^ _258327) ^ [_319136] : [ssList(_319136), -(app(app(_318836, _318988), _319136) = app(_318836, app(_318988, _319136)))]]]]], (1465 ^ _258327) ^ [_310048] : [ssList(_310048), 1468 ^ _258327 : [(1469 ^ _258327) ^ [_310210] : [ssList(_310210), 1472 ^ _258327 : [(1473 ^ _258327) ^ [_310368] : [ssList(_310368), 1476 ^ _258327 : [(1477 ^ _258327) ^ [_310522] : [ssList(_310522), segmentP(_310048, _310210), -(segmentP(app(app(_310368, _310048), _310522), _310210))]]]]]]], (1809 ^ _258327) ^ [_320783] : [ssList(_320783), 1812 ^ _258327 : [(1813 ^ _258327) ^ [_320931] : [ssList(_320931), -(nil = _320783), -(tl(app(_320783, _320931)) = app(tl(_320783), _320931))]]], (1211 ^ _258327) ^ [] : [singletonP(nil)], (1379 ^ _258327) ^ [_307416] : [ssList(_307416), 1382 ^ _258327 : [(1383 ^ _258327) ^ [_307565] : [ssList(_307565), 1386 ^ _258327 : [(1387 ^ _258327) ^ [_307710] : [ssList(_307710), rearsegP(_307416, _307565), -(rearsegP(app(_307710, _307416), _307565))]]]]], (993 ^ _258327) ^ [_295270] : [ssList(_295270), 996 ^ _258327 : [(997 ^ _258327) ^ [_295402] : [ssList(_295402), -(ssList(app(_295270, _295402)))]]], (1517 ^ _258327) ^ [_311719] : [ssItem(_311719), -(totalorderP(cons(_311719, nil)))], (1253 ^ _258327) ^ [_303419] : [ssList(_303419), -(frontsegP(_303419, _303419))], (1487 ^ _258327) ^ [_310858] : [ssList(_310858), -(segmentP(_310858, nil))], (34 ^ _258327) ^ [_259519, _259521] : [-(singletonP(_259519)), _259521 = _259519, singletonP(_259521)], (1311 ^ _258327) ^ [_305391] : [ssList(_305391), -(frontsegP(_305391, nil))], (1023 ^ _258327) ^ [_296339] : [ssItem(_296339), 1026 ^ _258327 : [(1027 ^ _258327) ^ [_296481] : [ssItem(_296481), -(_296339 = _296481), leq(_296339, _296481), leq(_296481, _296339)]]], (1403 ^ _258327) ^ [_308211] : [ssList(_308211), 1406 ^ _258327 : [(1413 ^ _258327) ^ [] : [nil = _308211, -(rearsegP(nil, _308211))], (1407 ^ _258327) ^ [] : [rearsegP(nil, _308211), -(nil = _308211)]]], (1579 ^ _258327) ^ [_313548] : [ssItem(_313548), -(strictorderedP(cons(_313548, nil)))], (184 ^ _258327) ^ [_264127, _264129, _264131, _264133] : [-(leq(_264131, _264127)), leq(_264133, _264129), _264133 = _264131, _264129 = _264127], (754 ^ _258327) ^ [_286357] : [ssList(_286357), 757 ^ _258327 : [(758 ^ _258327) ^ [] : [duplicatefreeP(_286357), 761 ^ _258327 : [(762 ^ _258327) ^ [_286655] : [ssItem(_286655), 765 ^ _258327 : [(766 ^ _258327) ^ [_286841] : [ssItem(_286841), 769 ^ _258327 : [(770 ^ _258327) ^ [_287023] : [ssList(_287023), 773 ^ _258327 : [(774 ^ _258327) ^ [_287201] : [ssList(_287201), 777 ^ _258327 : [(778 ^ _258327) ^ [_287375] : [ssList(_287375), app(app(_287023, cons(_286655, _287201)), cons(_286841, _287375)) = _286357, _286655 = _286841]]]]]]]]]]], (788 ^ _258327) ^ [] : [790 ^ _258327 : [(797 ^ _258327) ^ [] : [-(ssList(795 ^ [_286357]))], (805 ^ _258327) ^ [] : [-(app(app(795 ^ [_286357], cons(789 ^ [_286357], 798 ^ [_286357])), cons(792 ^ [_286357], 801 ^ [_286357])) = _286357)], (807 ^ _258327) ^ [] : [-(789 ^ [_286357] = 792 ^ [_286357])], (800 ^ _258327) ^ [] : [-(ssList(798 ^ [_286357]))], (791 ^ _258327) ^ [] : [-(ssItem(789 ^ [_286357]))], (794 ^ _258327) ^ [] : [-(ssItem(792 ^ [_286357]))], (803 ^ _258327) ^ [] : [-(ssList(801 ^ [_286357]))]], -(duplicatefreeP(_286357))]]], (963 ^ _258327) ^ [_294300] : [ssList(_294300), 966 ^ _258327 : [(967 ^ _258327) ^ [_294435] : [ssItem(_294435), -(hd(cons(_294435, _294300)) = _294435)]]], (1089 ^ _258327) ^ [_298335] : [ssItem(_298335), 1092 ^ _258327 : [(1093 ^ _258327) ^ [_298473] : [ssItem(_298473), lt(_298335, _298473), lt(_298473, _298335)]]], (1739 ^ _258327) ^ [_318478] : [ssList(_318478), 1742 ^ _258327 : [(1743 ^ _258327) ^ [_318617] : [ssItem(_318617), -(cons(_318617, _318478) = app(cons(_318617, nil), _318478))]]], (1441 ^ _258327) ^ [_309339] : [ssList(_309339), 1444 ^ _258327 : [(1445 ^ _258327) ^ [_309481] : [ssList(_309481), -(_309339 = _309481), segmentP(_309339, _309481), segmentP(_309481, _309339)]]], (1259 ^ _258327) ^ [_303607] : [ssList(_303607), 1262 ^ _258327 : [(1263 ^ _258327) ^ [_303756] : [ssList(_303756), 1266 ^ _258327 : [(1267 ^ _258327) ^ [_303901] : [ssList(_303901), frontsegP(_303607, _303756), -(frontsegP(app(_303607, _303901), _303756))]]]]], (1875 ^ _258327) ^ [_322842] : [ssItem(_322842), 1878 ^ _258327 : [(1879 ^ _258327) ^ [_322994] : [ssItem(_322994), 1882 ^ _258327 : [(1883 ^ _258327) ^ [_323142] : [ssItem(_323142), -(lt(_322842, _323142)), leq(_322842, _322994), lt(_322994, _323142)]]]]], (1541 ^ _258327) ^ [_312454] : [ssItem(_312454), 1544 ^ _258327 : [(1545 ^ _258327) ^ [_312613] : [ssList(_312613), 1548 ^ _258327 : [(1563 ^ _258327) ^ [] : [-(totalorderedP(cons(_312454, _312613))), 1564 ^ _258327 : [(1567 ^ _258327) ^ [] : [-(nil = _312613), totalorderedP(_312613), leq(_312454, hd(_312613))], (1565 ^ _258327) ^ [] : [nil = _312613]]], (1549 ^ _258327) ^ [] : [totalorderedP(cons(_312454, _312613)), -(nil = _312613), 1556 ^ _258327 : [(1561 ^ _258327) ^ [] : [-(leq(_312454, hd(_312613)))], (1559 ^ _258327) ^ [] : [-(totalorderedP(_312613))], (1557 ^ _258327) ^ [] : [nil = _312613]]]]]]], (1721 ^ _258327) ^ [_317859] : [ssList(_317859), 1724 ^ _258327 : [(1725 ^ _258327) ^ [_318011] : [ssList(_318011), 1728 ^ _258327 : [(1729 ^ _258327) ^ [_318159] : [ssList(_318159), app(_318011, _318159) = app(_318011, _317859), -(_318159 = _317859)]]]]], (340 ^ _258327) ^ [_269321] : [ssList(_269321), 343 ^ _258327 : [(353 ^ _258327) ^ [] : [-(singletonP(_269321)), 354 ^ _258327 : [(355 ^ _258327) ^ [_269770] : [ssItem(_269770), cons(_269770, nil) = _269321]]], (344 ^ _258327) ^ [] : [singletonP(_269321), 348 ^ _258327 : [(351 ^ _258327) ^ [] : [-(cons(347 ^ [_269321], nil) = _269321)], (349 ^ _258327) ^ [] : [-(ssItem(347 ^ [_269321]))]]]]], (1041 ^ _258327) ^ [_296860] : [ssItem(_296860), 1044 ^ _258327 : [(1045 ^ _258327) ^ [_297012] : [ssItem(_297012), 1048 ^ _258327 : [(1049 ^ _258327) ^ [_297160] : [ssItem(_297160), -(leq(_296860, _297160)), leq(_296860, _297012), leq(_297012, _297160)]]]]], (246 ^ _258327) ^ [_266083, _266085] : [_266085 = _266083, -(hd(_266085) = hd(_266083))], (1533 ^ _258327) ^ [_312209] : [ssItem(_312209), -(totalorderedP(cons(_312209, nil)))], (927 ^ _258327) ^ [_293115] : [ssList(_293115), -(nil = _293115), 935 ^ _258327 : [(941 ^ _258327) ^ [] : [-(cons(937 ^ [_293115], 934 ^ [_293115]) = _293115)], (939 ^ _258327) ^ [] : [-(ssItem(937 ^ [_293115]))], (936 ^ _258327) ^ [] : [-(ssList(934 ^ [_293115]))]]], (1493 ^ _258327) ^ [_311046] : [ssList(_311046), 1496 ^ _258327 : [(1503 ^ _258327) ^ [] : [nil = _311046, -(segmentP(nil, _311046))], (1497 ^ _258327) ^ [] : [segmentP(nil, _311046), -(nil = _311046)]]], (363 ^ _258327) ^ [_270026] : [ssList(_270026), 366 ^ _258327 : [(367 ^ _258327) ^ [_270175] : [ssList(_270175), 370 ^ _258327 : [(380 ^ _258327) ^ [] : [-(frontsegP(_270026, _270175)), 381 ^ _258327 : [(382 ^ _258327) ^ [_270650] : [ssList(_270650), app(_270175, _270650) = _270026]]], (371 ^ _258327) ^ [] : [frontsegP(_270026, _270175), 375 ^ _258327 : [(378 ^ _258327) ^ [] : [-(app(_270175, 374 ^ [_270026, _270175]) = _270026)], (376 ^ _258327) ^ [] : [-(ssList(374 ^ [_270026, _270175]))]]]]]]], (306 ^ _258327) ^ [_268072] : [ssList(_268072), 309 ^ _258327 : [(310 ^ _258327) ^ [_268234] : [ssItem(_268234), 313 ^ _258327 : [(326 ^ _258327) ^ [] : [-(memberP(_268072, _268234)), 327 ^ _258327 : [(328 ^ _258327) ^ [_268882] : [ssList(_268882), 331 ^ _258327 : [(332 ^ _258327) ^ [_269030] : [ssList(_269030), app(_268882, cons(_268234, _269030)) = _268072]]]]], (314 ^ _258327) ^ [] : [memberP(_268072, _268234), 318 ^ _258327 : [(324 ^ _258327) ^ [] : [-(app(317 ^ [_268072, _268234], cons(_268234, 320 ^ [_268072, _268234])) = _268072)], (322 ^ _258327) ^ [] : [-(ssList(320 ^ [_268072, _268234]))], (319 ^ _258327) ^ [] : [-(ssList(317 ^ [_268072, _268234]))]]]]]]], (1693 ^ _258327) ^ [_316950] : [ssList(_316950), -(nil = _316950), -(cons(hd(_316950), tl(_316950)) = _316950)], (811 ^ _258327) ^ [_288867] : [ssList(_288867), 814 ^ _258327 : [(815 ^ _258327) ^ [] : [equalelemsP(_288867), 818 ^ _258327 : [(819 ^ _258327) ^ [_289150] : [ssItem(_289150), 822 ^ _258327 : [(823 ^ _258327) ^ [_289321] : [ssItem(_289321), 826 ^ _258327 : [(827 ^ _258327) ^ [_289488] : [ssList(_289488), 830 ^ _258327 : [(831 ^ _258327) ^ [_289651] : [ssList(_289651), app(_289488, cons(_289150, cons(_289321, _289651))) = _288867, -(_289150 = _289321)]]]]]]]]], (841 ^ _258327) ^ [] : [843 ^ _258327 : [(847 ^ _258327) ^ [] : [-(ssItem(845 ^ [_288867]))], (844 ^ _258327) ^ [] : [-(ssItem(842 ^ [_288867]))], (857 ^ _258327) ^ [] : [842 ^ [_288867] = 845 ^ [_288867]], (853 ^ _258327) ^ [] : [-(ssList(851 ^ [_288867]))], (855 ^ _258327) ^ [] : [-(app(848 ^ [_288867], cons(842 ^ [_288867], cons(845 ^ [_288867], 851 ^ [_288867]))) = _288867)], (850 ^ _258327) ^ [] : [-(ssList(848 ^ [_288867]))]], -(equalelemsP(_288867))]]], (1125 ^ _258327) ^ [_299464] : [ssItem(_299464), 1128 ^ _258327 : [(1129 ^ _258327) ^ [_299600] : [ssItem(_299600), 1132 ^ _258327 : [(1139 ^ _258327) ^ [] : [lt(_299600, _299464), -(gt(_299464, _299600))], (1133 ^ _258327) ^ [] : [gt(_299464, _299600), -(lt(_299600, _299464))]]]]], (973 ^ _258327) ^ [_294646] : [ssList(_294646), -(nil = _294646), -(ssList(tl(_294646)))], (1823 ^ _258327) ^ [_321244] : [ssItem(_321244), 1826 ^ _258327 : [(1827 ^ _258327) ^ [_321386] : [ssItem(_321386), -(_321244 = _321386), geq(_321244, _321386), geq(_321386, _321244)]]], (953 ^ _258327) ^ [_294022] : [ssList(_294022), -(nil = _294022), -(ssItem(hd(_294022)))], (1667 ^ _258327) ^ [_316205] : [ssList(_316205), 1670 ^ _258327 : [(1671 ^ _258327) ^ [_316371] : [ssList(_316371), -(_316371 = _316205), -(nil = _316371), -(nil = _316205), hd(_316371) = hd(_316205), tl(_316371) = tl(_316205)]]], (1841 ^ _258327) ^ [_321765] : [ssItem(_321765), 1844 ^ _258327 : [(1845 ^ _258327) ^ [_321917] : [ssItem(_321917), 1848 ^ _258327 : [(1849 ^ _258327) ^ [_322065] : [ssItem(_322065), -(geq(_321765, _322065)), geq(_321765, _321917), geq(_321917, _322065)]]]]], (1897 ^ _258327) ^ [_323542] : [ssItem(_323542), 1900 ^ _258327 : [(1901 ^ _258327) ^ [_323684] : [ssItem(_323684), leq(_323542, _323684), -(_323542 = _323684), -(lt(_323542, _323684))]]], (1639 ^ _258327) ^ [] : [-(equalelemsP(nil))], (1863 ^ _258327) ^ [_322465] : [ssItem(_322465), -(geq(_322465, _322465))], (1625 ^ _258327) ^ [_314887] : [ssItem(_314887), -(duplicatefreeP(cons(_314887, nil)))], (577 ^ _258327) ^ [_278617] : [ssList(_278617), 580 ^ _258327 : [(581 ^ _258327) ^ [] : [strictorderP(_278617), 584 ^ _258327 : [(585 ^ _258327) ^ [_278919] : [ssItem(_278919), 588 ^ _258327 : [(589 ^ _258327) ^ [_279109] : [ssItem(_279109), 592 ^ _258327 : [(593 ^ _258327) ^ [_279295] : [ssList(_279295), 596 ^ _258327 : [(597 ^ _258327) ^ [_279477] : [ssList(_279477), 600 ^ _258327 : [(601 ^ _258327) ^ [_279655] : [ssList(_279655), app(app(_279295, cons(_278919, _279477)), cons(_279109, _279655)) = _278617, -(lt(_278919, _279109)), -(lt(_279109, _278919))]]]]]]]]]]], (615 ^ _258327) ^ [] : [617 ^ _258327 : [(624 ^ _258327) ^ [] : [-(ssList(622 ^ [_278617]))], (632 ^ _258327) ^ [] : [-(app(app(622 ^ [_278617], cons(616 ^ [_278617], 625 ^ [_278617])), cons(619 ^ [_278617], 628 ^ [_278617])) = _278617)], (618 ^ _258327) ^ [] : [-(ssItem(616 ^ [_278617]))], (634 ^ _258327) ^ [] : [lt(616 ^ [_278617], 619 ^ [_278617])], (627 ^ _258327) ^ [] : [-(ssList(625 ^ [_278617]))], (630 ^ _258327) ^ [] : [-(ssList(628 ^ [_278617]))], (636 ^ _258327) ^ [] : [lt(619 ^ [_278617], 616 ^ [_278617])], (621 ^ _258327) ^ [] : [-(ssItem(619 ^ [_278617]))]], -(strictorderP(_278617))]]], (44 ^ _258327) ^ [_259842, _259844, _259846, _259848] : [-(frontsegP(_259846, _259842)), frontsegP(_259848, _259844), _259848 = _259846, _259844 = _259842], (1795 ^ _258327) ^ [_320331] : [ssList(_320331), 1798 ^ _258327 : [(1799 ^ _258327) ^ [_320476] : [ssList(_320476), -(nil = _320331), -(hd(app(_320331, _320476)) = hd(_320331))]]], (20 ^ _258327) ^ [_259103, _259105, _259107, _259109] : [-(memberP(_259107, _259103)), memberP(_259109, _259105), _259109 = _259107, _259105 = _259103], (1523 ^ _258327) ^ [] : [-(totalorderP(nil))], (1789 ^ _258327) ^ [_320137] : [ssList(_320137), -(app(_320137, nil) = _320137)], (697 ^ _258327) ^ [_283869] : [ssList(_283869), 700 ^ _258327 : [(701 ^ _258327) ^ [] : [strictorderedP(_283869), 704 ^ _258327 : [(705 ^ _258327) ^ [_284165] : [ssItem(_284165), 708 ^ _258327 : [(709 ^ _258327) ^ [_284349] : [ssItem(_284349), 712 ^ _258327 : [(713 ^ _258327) ^ [_284529] : [ssList(_284529), 716 ^ _258327 : [(717 ^ _258327) ^ [_284705] : [ssList(_284705), 720 ^ _258327 : [(721 ^ _258327) ^ [_284877] : [ssList(_284877), app(app(_284529, cons(_284165, _284705)), cons(_284349, _284877)) = _283869, -(lt(_284165, _284349))]]]]]]]]]]], (731 ^ _258327) ^ [] : [733 ^ _258327 : [(740 ^ _258327) ^ [] : [-(ssList(738 ^ [_283869]))], (748 ^ _258327) ^ [] : [-(app(app(738 ^ [_283869], cons(732 ^ [_283869], 741 ^ [_283869])), cons(735 ^ [_283869], 744 ^ [_283869])) = _283869)], (750 ^ _258327) ^ [] : [lt(732 ^ [_283869], 735 ^ [_283869])], (743 ^ _258327) ^ [] : [-(ssList(741 ^ [_283869]))], (734 ^ _258327) ^ [] : [-(ssItem(732 ^ [_283869]))], (737 ^ _258327) ^ [] : [-(ssItem(735 ^ [_283869]))], (746 ^ _258327) ^ [] : [-(ssList(744 ^ [_283869]))]], -(strictorderedP(_283869))]]], (198 ^ _258327) ^ [_264571, _264573, _264575, _264577] : [-(gt(_264575, _264571)), gt(_264577, _264573), _264577 = _264575, _264573 = _264571], (1373 ^ _258327) ^ [_307228] : [ssList(_307228), -(rearsegP(_307228, _307228))], (116 ^ _258327) ^ [_262031, _262033] : [-(totalorderedP(_262031)), _262033 = _262031, totalorderedP(_262033)], (10 ^ _258327) ^ [_258762, _258764, _258766] : [-(_258766 = _258762), _258766 = _258764, _258764 = _258762], (1941 ^ _258327) ^ [_324819] : [ssItem(_324819), 1944 ^ _258327 : [(1945 ^ _258327) ^ [_324957] : [ssItem(_324957), gt(_324819, _324957), gt(_324957, _324819)]]], (1587 ^ _258327) ^ [_313793] : [ssItem(_313793), 1590 ^ _258327 : [(1591 ^ _258327) ^ [_313952] : [ssList(_313952), 1594 ^ _258327 : [(1609 ^ _258327) ^ [] : [-(strictorderedP(cons(_313793, _313952))), 1610 ^ _258327 : [(1613 ^ _258327) ^ [] : [-(nil = _313952), strictorderedP(_313952), lt(_313793, hd(_313952))], (1611 ^ _258327) ^ [] : [nil = _313952]]], (1595 ^ _258327) ^ [] : [strictorderedP(cons(_313793, _313952)), -(nil = _313952), 1602 ^ _258327 : [(1607 ^ _258327) ^ [] : [-(lt(_313793, hd(_313952)))], (1605 ^ _258327) ^ [] : [-(strictorderedP(_313952))], (1603 ^ _258327) ^ [] : [nil = _313952]]]]]]], (299 ^ _258327) ^ [] : [-(ssItem(297 ^ []))], (451 ^ _258327) ^ [_273067] : [ssList(_273067), 454 ^ _258327 : [(455 ^ _258327) ^ [] : [cyclefreeP(_273067), 458 ^ _258327 : [(459 ^ _258327) ^ [_273371] : [ssItem(_273371), 462 ^ _258327 : [(463 ^ _258327) ^ [_273563] : [ssItem(_273563), 466 ^ _258327 : [(467 ^ _258327) ^ [_273751] : [ssList(_273751), 470 ^ _258327 : [(471 ^ _258327) ^ [_273935] : [ssList(_273935), 474 ^ _258327 : [(475 ^ _258327) ^ [_274115] : [ssList(_274115), app(app(_273751, cons(_273371, _273935)), cons(_273563, _274115)) = _273067, leq(_273371, _273563), leq(_273563, _273371)]]]]]]]]]]], (489 ^ _258327) ^ [] : [491 ^ _258327 : [(498 ^ _258327) ^ [] : [-(ssList(496 ^ [_273067]))], (506 ^ _258327) ^ [] : [-(app(app(496 ^ [_273067], cons(490 ^ [_273067], 499 ^ [_273067])), cons(493 ^ [_273067], 502 ^ [_273067])) = _273067)], (492 ^ _258327) ^ [] : [-(ssItem(490 ^ [_273067]))], (508 ^ _258327) ^ [] : [-(leq(490 ^ [_273067], 493 ^ [_273067]))], (501 ^ _258327) ^ [] : [-(ssList(499 ^ [_273067]))], (504 ^ _258327) ^ [] : [-(ssList(502 ^ [_273067]))], (510 ^ _258327) ^ [] : [-(leq(493 ^ [_273067], 490 ^ [_273067]))], (495 ^ _258327) ^ [] : [-(ssItem(493 ^ [_273067]))]], -(cyclefreeP(_273067))]]], (1515 ^ _258327) ^ [] : [-(cyclefreeP(nil))], (1333 ^ _258327) ^ [_306007] : [ssList(_306007), 1336 ^ _258327 : [(1337 ^ _258327) ^ [_306159] : [ssList(_306159), 1340 ^ _258327 : [(1341 ^ _258327) ^ [_306307] : [ssList(_306307), -(rearsegP(_306007, _306307)), rearsegP(_306007, _306159), rearsegP(_306159, _306307)]]]]], (302 ^ _258327) ^ [] : [-(ssItem(300 ^ []))], (170 ^ _258327) ^ [_263683, _263685, _263687, _263689] : [-(lt(_263687, _263683)), lt(_263689, _263685), _263689 = _263687, _263685 = _263683], (1103 ^ _258327) ^ [_298764] : [ssItem(_298764), 1106 ^ _258327 : [(1107 ^ _258327) ^ [_298916] : [ssItem(_298916), 1110 ^ _258327 : [(1111 ^ _258327) ^ [_299064] : [ssItem(_299064), -(lt(_298764, _299064)), lt(_298764, _298916), lt(_298916, _299064)]]]]], (1955 ^ _258327) ^ [_325228] : [ssItem(_325228), 1958 ^ _258327 : [(1959 ^ _258327) ^ [_325380] : [ssItem(_325380), 1962 ^ _258327 : [(1963 ^ _258327) ^ [_325528] : [ssItem(_325528), -(gt(_325228, _325528)), gt(_325228, _325380), gt(_325380, _325528)]]]]], (893 ^ _258327) ^ [_291865] : [ssList(_291865), 896 ^ _258327 : [(897 ^ _258327) ^ [_292000] : [ssItem(_292000), cons(_292000, _291865) = _291865]]], (1205 ^ _258327) ^ [_301957] : [ssItem(_301957), memberP(nil, _301957)], (640 ^ _258327) ^ [_281381] : [ssList(_281381), 643 ^ _258327 : [(644 ^ _258327) ^ [] : [totalorderedP(_281381), 647 ^ _258327 : [(648 ^ _258327) ^ [_281677] : [ssItem(_281677), 651 ^ _258327 : [(652 ^ _258327) ^ [_281861] : [ssItem(_281861), 655 ^ _258327 : [(656 ^ _258327) ^ [_282041] : [ssList(_282041), 659 ^ _258327 : [(660 ^ _258327) ^ [_282217] : [ssList(_282217), 663 ^ _258327 : [(664 ^ _258327) ^ [_282389] : [ssList(_282389), app(app(_282041, cons(_281677, _282217)), cons(_281861, _282389)) = _281381, -(leq(_281677, _281861))]]]]]]]]]]], (674 ^ _258327) ^ [] : [676 ^ _258327 : [(683 ^ _258327) ^ [] : [-(ssList(681 ^ [_281381]))], (691 ^ _258327) ^ [] : [-(app(app(681 ^ [_281381], cons(675 ^ [_281381], 684 ^ [_281381])), cons(678 ^ [_281381], 687 ^ [_281381])) = _281381)], (693 ^ _258327) ^ [] : [leq(675 ^ [_281381], 678 ^ [_281381])], (686 ^ _258327) ^ [] : [-(ssList(684 ^ [_281381]))], (677 ^ _258327) ^ [] : [-(ssItem(675 ^ [_281381]))], (680 ^ _258327) ^ [] : [-(ssItem(678 ^ [_281381]))], (689 ^ _258327) ^ [] : [-(ssList(687 ^ [_281381]))]], -(totalorderedP(_281381))]]], (1654 ^ _258327) ^ [_315791] : [ssList(_315791), -(nil = _315791), 1662 ^ _258327 : [(1665 ^ _258327) ^ [] : [-(tl(_315791) = 1661 ^ [_315791])], (1663 ^ _258327) ^ [] : [-(ssList(1661 ^ [_315791]))]]], (4 ^ _258327) ^ [_258558, _258560] : [_258560 = _258558, -(_258558 = _258560)], (417 ^ _258327) ^ [_271818] : [ssList(_271818), 420 ^ _258327 : [(421 ^ _258327) ^ [_271980] : [ssList(_271980), 424 ^ _258327 : [(437 ^ _258327) ^ [] : [-(segmentP(_271818, _271980)), 438 ^ _258327 : [(439 ^ _258327) ^ [_272628] : [ssList(_272628), 442 ^ _258327 : [(443 ^ _258327) ^ [_272776] : [ssList(_272776), app(app(_272628, _271980), _272776) = _271818]]]]], (425 ^ _258327) ^ [] : [segmentP(_271818, _271980), 429 ^ _258327 : [(435 ^ _258327) ^ [] : [-(app(app(428 ^ [_271818, _271980], _271980), 431 ^ [_271818, _271980]) = _271818)], (433 ^ _258327) ^ [] : [-(ssList(431 ^ [_271818, _271980]))], (430 ^ _258327) ^ [] : [-(ssList(428 ^ [_271818, _271980]))]]]]]]], (1069 ^ _258327) ^ [_297748] : [ssItem(_297748), 1072 ^ _258327 : [(1073 ^ _258327) ^ [_297884] : [ssItem(_297884), 1076 ^ _258327 : [(1083 ^ _258327) ^ [] : [leq(_297884, _297748), -(geq(_297748, _297884))], (1077 ^ _258327) ^ [] : [geq(_297748, _297884), -(leq(_297884, _297748))]]]]], (212 ^ _258327) ^ [_264987, _264989] : [-(ssItem(_264987)), _264989 = _264987, ssItem(_264989)], (1175 ^ _258327) ^ [_301004] : [ssItem(_301004), 1178 ^ _258327 : [(1179 ^ _258327) ^ [_301159] : [ssItem(_301159), 1182 ^ _258327 : [(1183 ^ _258327) ^ [_301310] : [ssList(_301310), 1186 ^ _258327 : [(1187 ^ _258327) ^ [] : [memberP(cons(_301159, _301310), _301004), -(_301004 = _301159), -(memberP(_301310, _301004))], (1197 ^ _258327) ^ [] : [1198 ^ _258327 : [(1201 ^ _258327) ^ [] : [memberP(_301310, _301004)], (1199 ^ _258327) ^ [] : [_301004 = _301159]], -(memberP(cons(_301159, _301310), _301004))]]]]]]], (258 ^ _258327) ^ [_266547, _266549, _266551, _266553] : [-(app(_266553, _266549) = app(_266551, _266547)), _266553 = _266551, _266549 = _266547], (1531 ^ _258327) ^ [] : [-(strictorderP(nil))], (1763 ^ _258327) ^ [_319374] : [ssList(_319374), 1766 ^ _258327 : [(1767 ^ _258327) ^ [_319519] : [ssList(_319519), 1770 ^ _258327 : [(1779 ^ _258327) ^ [] : [-(nil = app(_319374, _319519)), nil = _319519, nil = _319374], (1771 ^ _258327) ^ [] : [nil = app(_319374, _319519), 1774 ^ _258327 : [(1777 ^ _258327) ^ [] : [-(nil = _319374)], (1775 ^ _258327) ^ [] : [-(nil = _319519)]]]]]]], (1003 ^ _258327) ^ [_295607] : [ssList(_295607), 1006 ^ _258327 : [(1007 ^ _258327) ^ [_295759] : [ssList(_295759), 1010 ^ _258327 : [(1011 ^ _258327) ^ [_295907] : [ssItem(_295907), -(cons(_295907, app(_295759, _295607)) = app(cons(_295907, _295759), _295607))]]]]], (1509 ^ _258327) ^ [_311474] : [ssItem(_311474), -(cyclefreeP(cons(_311474, nil)))], (1539 ^ _258327) ^ [] : [-(totalorderedP(nil))], (1317 ^ _258327) ^ [_305579] : [ssList(_305579), 1320 ^ _258327 : [(1327 ^ _258327) ^ [] : [nil = _305579, -(frontsegP(nil, _305579))], (1321 ^ _258327) ^ [] : [frontsegP(nil, _305579), -(nil = _305579)]]], (1397 ^ _258327) ^ [_308023] : [ssList(_308023), -(rearsegP(_308023, nil))], (1585 ^ _258327) ^ [] : [-(strictorderedP(nil))], (96 ^ _258327) ^ [_261441, _261443] : [-(totalorderP(_261441)), _261443 = _261441, totalorderP(_261443)], (146 ^ _258327) ^ [_262916, _262918] : [-(equalelemsP(_262916)), _262918 = _262916, equalelemsP(_262918)], (881 ^ _258327) ^ [_291475] : [ssList(_291475), 884 ^ _258327 : [(885 ^ _258327) ^ [_291607] : [ssItem(_291607), -(ssList(cons(_291607, _291475)))]]], (1235 ^ _258327) ^ [_302898] : [ssList(_302898), 1238 ^ _258327 : [(1239 ^ _258327) ^ [_303040] : [ssList(_303040), -(_302898 = _303040), frontsegP(_302898, _303040), frontsegP(_303040, _302898)]]], (1915 ^ _258327) ^ [_324064] : [ssItem(_324064), 1918 ^ _258327 : [(1919 ^ _258327) ^ [_324208] : [ssItem(_324208), 1922 ^ _258327 : [(1931 ^ _258327) ^ [] : [-(lt(_324064, _324208)), -(_324064 = _324208), leq(_324064, _324208)], (1923 ^ _258327) ^ [] : [lt(_324064, _324208), 1926 ^ _258327 : [(1929 ^ _258327) ^ [] : [-(leq(_324064, _324208))], (1927 ^ _258327) ^ [] : [_324064 = _324208]]]]]]], (903 ^ _258327) ^ [_292208] : [ssList(_292208), 906 ^ _258327 : [(907 ^ _258327) ^ [_292376] : [ssList(_292376), 910 ^ _258327 : [(911 ^ _258327) ^ [_292540] : [ssItem(_292540), 914 ^ _258327 : [(915 ^ _258327) ^ [_292700] : [ssItem(_292700), cons(_292540, _292208) = cons(_292700, _292376), 922 ^ _258327 : [(925 ^ _258327) ^ [] : [-(_292376 = _292208)], (923 ^ _258327) ^ [] : [-(_292540 = _292700)]]]]]]]]], (304 ^ _258327) ^ [] : [297 ^ [] = 300 ^ []], (1631 ^ _258327) ^ [] : [-(duplicatefreeP(nil))], (1525 ^ _258327) ^ [_311964] : [ssItem(_311964), -(strictorderP(cons(_311964, nil)))], (156 ^ _258327) ^ [_263239, _263241, _263243, _263245] : [-(geq(_263243, _263239)), geq(_263245, _263241), _263245 = _263243, _263241 = _263239], (891 ^ _258327) ^ [] : [-(ssList(nil))], (983 ^ _258327) ^ [_294924] : [ssList(_294924), 986 ^ _258327 : [(987 ^ _258327) ^ [_295059] : [ssItem(_295059), -(tl(cons(_295059, _294924)) = _294924)]]], (86 ^ _258327) ^ [_261146, _261148] : [-(cyclefreeP(_261146)), _261148 = _261146, cyclefreeP(_261148)], (1277 ^ _258327) ^ [_304214] : [ssItem(_304214), 1280 ^ _258327 : [(1281 ^ _258327) ^ [_304382] : [ssItem(_304382), 1284 ^ _258327 : [(1285 ^ _258327) ^ [_304546] : [ssList(_304546), 1288 ^ _258327 : [(1289 ^ _258327) ^ [_304706] : [ssList(_304706), 1292 ^ _258327 : [(1301 ^ _258327) ^ [] : [-(frontsegP(cons(_304214, _304546), cons(_304382, _304706))), _304214 = _304382, frontsegP(_304546, _304706)], (1293 ^ _258327) ^ [] : [frontsegP(cons(_304214, _304546), cons(_304382, _304706)), 1296 ^ _258327 : [(1299 ^ _258327) ^ [] : [-(frontsegP(_304546, _304706))], (1297 ^ _258327) ^ [] : [-(_304214 = _304382)]]]]]]]]]]], (1703 ^ _258327) ^ [_317240] : [ssList(_317240), 1706 ^ _258327 : [(1707 ^ _258327) ^ [_317392] : [ssList(_317392), 1710 ^ _258327 : [(1711 ^ _258327) ^ [_317540] : [ssList(_317540), app(_317540, _317392) = app(_317240, _317392), -(_317540 = _317240)]]]]], (514 ^ _258327) ^ [_275853] : [ssList(_275853), 517 ^ _258327 : [(518 ^ _258327) ^ [] : [totalorderP(_275853), 521 ^ _258327 : [(522 ^ _258327) ^ [_276155] : [ssItem(_276155), 525 ^ _258327 : [(526 ^ _258327) ^ [_276345] : [ssItem(_276345), 529 ^ _258327 : [(530 ^ _258327) ^ [_276531] : [ssList(_276531), 533 ^ _258327 : [(534 ^ _258327) ^ [_276713] : [ssList(_276713), 537 ^ _258327 : [(538 ^ _258327) ^ [_276891] : [ssList(_276891), app(app(_276531, cons(_276155, _276713)), cons(_276345, _276891)) = _275853, -(leq(_276155, _276345)), -(leq(_276345, _276155))]]]]]]]]]]], (552 ^ _258327) ^ [] : [554 ^ _258327 : [(561 ^ _258327) ^ [] : [-(ssList(559 ^ [_275853]))], (569 ^ _258327) ^ [] : [-(app(app(559 ^ [_275853], cons(553 ^ [_275853], 562 ^ [_275853])), cons(556 ^ [_275853], 565 ^ [_275853])) = _275853)], (555 ^ _258327) ^ [] : [-(ssItem(553 ^ [_275853]))], (571 ^ _258327) ^ [] : [leq(553 ^ [_275853], 556 ^ [_275853])], (564 ^ _258327) ^ [] : [-(ssList(562 ^ [_275853]))], (567 ^ _258327) ^ [] : [-(ssList(565 ^ [_275853]))], (573 ^ _258327) ^ [] : [leq(556 ^ [_275853], 553 ^ [_275853])], (558 ^ _258327) ^ [] : [-(ssItem(556 ^ [_275853]))]], -(totalorderP(_275853))]]], (1419 ^ _258327) ^ [_308639] : [ssList(_308639), 1422 ^ _258327 : [(1423 ^ _258327) ^ [_308791] : [ssList(_308791), 1426 ^ _258327 : [(1427 ^ _258327) ^ [_308939] : [ssList(_308939), -(segmentP(_308639, _308939)), segmentP(_308639, _308791), segmentP(_308791, _308939)]]]]], (1641 ^ _258327) ^ [_315377] : [ssList(_315377), -(nil = _315377), 1649 ^ _258327 : [(1652 ^ _258327) ^ [] : [-(hd(_315377) = 1648 ^ [_315377])], (1650 ^ _258327) ^ [] : [-(ssItem(1648 ^ [_315377]))]]], (222 ^ _258327) ^ [_265282, _265284] : [-(ssList(_265282)), _265284 = _265282, ssList(_265284)], (126 ^ _258327) ^ [_262326, _262328] : [-(strictorderedP(_262326)), _262328 = _262326, strictorderedP(_262328)]], input).
% 94.57/91.40 ncf('1',plain,[2023 : neq(1985 ^ [], nil), 2015 : -(ssList(2013 ^ []))],start(1993 ^ 0)).
% 94.57/91.40 ncf('1.1',plain,[-(neq(1985 ^ [], nil)), 875 : -(1985 ^ [] = nil), 875 : ssList(nil), 865 : ssList(1985 ^ [])],extension(861 ^ 3,bind([[_290884, _291022], [1985 ^ [], nil]]))).
% 94.57/91.40 ncf('1.1.1',plain,[1985 ^ [] = nil, -(1979 ^ [] = nil), 1979 ^ [] = 1985 ^ []],extension(10 ^ 8,bind([[_258762, _258764, _258766], [nil, 1985 ^ [], 1979 ^ []]]))).
% 94.57/91.40 ncf('1.1.1.1',plain,[1979 ^ [] = nil, 869 : neq(1979 ^ [], nil), 869 : ssList(nil), 865 : ssList(1979 ^ [])],extension(861 ^ 9,bind([[_290884, _291022], [1979 ^ [], nil]]))).
% 94.57/91.40 ncf('1.1.1.1.1',plain,[-(neq(1979 ^ [], nil))],extension(2021 ^ 14)).
% 94.57/91.40 ncf('1.1.1.1.2',plain,[-(ssList(nil))],extension(891 ^ 12)).
% 94.57/91.40 ncf('1.1.1.1.3',plain,[-(ssList(1979 ^ []))],extension(1981 ^ 10)).
% 94.57/91.40 ncf('1.1.1.2',plain,[-(1979 ^ [] = 1985 ^ [])],extension(1989 ^ 9)).
% 94.57/91.40 ncf('1.1.2',plain,[-(ssList(nil))],extension(891 ^ 6)).
% 94.57/91.40 ncf('1.1.3',plain,[-(ssList(1985 ^ []))],extension(1987 ^ 4)).
% 94.57/91.40 ncf('1.2',plain,[ssList(2013 ^ []), 2001 : cons(2010 ^ [], nil) = 1976 ^ [], 2001 : app(2013 ^ [], cons(2010 ^ [], nil)) = 1979 ^ [], 2001 : ssItem(2010 ^ [])],extension(1997 ^ 3,bind([[_327695, _327840], [2010 ^ [], 2013 ^ []]]))).
% 94.57/91.40 ncf('1.2.1',plain,[-(cons(2010 ^ [], nil) = 1976 ^ []), cons(2010 ^ [], nil) = 1982 ^ [], 1982 ^ [] = 1976 ^ []],extension(10 ^ 6,bind([[_258762, _258764, _258766], [1976 ^ [], 1982 ^ [], cons(2010 ^ [], nil)]]))).
% 94.57/91.40 ncf('1.2.1.1',plain,[-(cons(2010 ^ [], nil) = 1982 ^ [])],extension(2017 ^ 7)).
% 94.57/91.40 ncf('1.2.1.2',plain,[-(1982 ^ [] = 1976 ^ []), 1976 ^ [] = 1982 ^ []],extension(4 ^ 7,bind([[_258558, _258560], [1982 ^ [], 1976 ^ []]]))).
% 94.57/91.40 ncf('1.2.1.2.1',plain,[-(1976 ^ [] = 1982 ^ [])],extension(1991 ^ 8)).
% 94.57/91.40 ncf('1.2.2',plain,[-(app(2013 ^ [], cons(2010 ^ [], nil)) = 1979 ^ []), app(2013 ^ [], cons(2010 ^ [], nil)) = 1985 ^ [], 1985 ^ [] = 1979 ^ []],extension(10 ^ 6,bind([[_258762, _258764, _258766], [1979 ^ [], 1985 ^ [], app(2013 ^ [], cons(2010 ^ [], nil))]]))).
% 94.57/91.40 ncf('1.2.2.1',plain,[-(app(2013 ^ [], cons(2010 ^ [], nil)) = 1985 ^ [])],extension(2019 ^ 7)).
% 94.57/91.40 ncf('1.2.2.2',plain,[-(1985 ^ [] = 1979 ^ []), 1979 ^ [] = 1985 ^ []],extension(4 ^ 7,bind([[_258558, _258560], [1985 ^ [], 1979 ^ []]]))).
% 94.57/91.40 ncf('1.2.2.2.1',plain,[-(1979 ^ [] = 1985 ^ [])],extension(1989 ^ 8)).
% 94.57/91.40 ncf('1.2.3',plain,[-(ssItem(2010 ^ []))],extension(2012 ^ 4)).
% 94.57/91.40 %-----------------------------------------------------
% 94.57/91.40 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------