%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWC040+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri May 19 12:12:20 EDT 2023
% Result : Theorem 47.01s 45.87s
% Output : Proof 47.01s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SWC040+1 : TPTP v8.1.2. Released v2.4.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n007.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri May 19 00:47:53 EDT 2023
% 0.12/0.33 % CPUTime :
% 47.01/45.87
% 47.01/45.87 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 47.01/45.87 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 47.01/45.87 %-----------------------------------------------------
% 47.01/45.87 ncf(matrix, plain, [(1987 ^ _319663) ^ [] : [-(ssList(1985 ^ []))], (2003 ^ _319663) ^ [] : [2005 ^ _319663 : [(2009 ^ _319663) ^ [] : [-(ssList(2007 ^ []))], (2011 ^ _319663) ^ [] : [-(app(cons(2004 ^ [], nil), 2007 ^ []) = 1982 ^ [])], (2013 ^ _319663) ^ [] : [-(app(2007 ^ [], cons(2004 ^ [], nil)) = 1985 ^ [])], (2006 ^ _319663) ^ [] : [-(ssItem(2004 ^ []))]], neq(1985 ^ [], nil)], (1981 ^ _319663) ^ [] : [-(ssList(1979 ^ []))], (1978 ^ _319663) ^ [] : [-(ssList(1976 ^ []))], (1991 ^ _319663) ^ [] : [-(1979 ^ [] = 1985 ^ [])], (1997 ^ _319663) ^ [] : [-(nil = 1982 ^ []), nil = 1985 ^ []], (1984 ^ _319663) ^ [] : [-(ssList(1982 ^ []))], (1995 ^ _319663) ^ [] : [nil = 1976 ^ []], (1989 ^ _319663) ^ [] : [-(nil = 1979 ^ [])], (1993 ^ _319663) ^ [] : [-(1976 ^ [] = 1982 ^ [])], !, (861 ^ _251302) ^ [_283859] : [ssList(_283859), 864 ^ _251302 : [(865 ^ _251302) ^ [_283997] : [ssList(_283997), 868 ^ _251302 : [(875 ^ _251302) ^ [] : [-(_283859 = _283997), -(neq(_283859, _283997))], (869 ^ _251302) ^ [] : [neq(_283859, _283997), _283859 = _283997]]]]], (252 ^ _251302) ^ [_259276, _259278] : [_259278 = _259276, -(tl(_259278) = tl(_259276))], (72 ^ _251302) ^ [_253705, _253707, _253709, _253711] : [-(segmentP(_253709, _253705)), segmentP(_253711, _253707), _253711 = _253709, _253707 = _253705], (1355 ^ _251302) ^ [_299682] : [ssList(_299682), 1358 ^ _251302 : [(1359 ^ _251302) ^ [_299824] : [ssList(_299824), -(_299682 = _299824), rearsegP(_299682, _299824), rearsegP(_299824, _299682)]]], (1459 ^ _251302) ^ [_302835] : [ssList(_302835), -(segmentP(_302835, _302835))], (106 ^ _251302) ^ [_254711, _254713] : [-(strictorderP(_254711)), _254713 = _254711, strictorderP(_254713)], (58 ^ _251302) ^ [_253261, _253263, _253265, _253267] : [-(rearsegP(_253265, _253261)), rearsegP(_253267, _253263), _253267 = _253265, _253263 = _253261], (943 ^ _251302) ^ [_286654] : [ssList(_286654), 946 ^ _251302 : [(947 ^ _251302) ^ [_286789] : [ssItem(_286789), nil = cons(_286789, _286654)]]], (1869 ^ _251302) ^ [_315628] : [ssItem(_315628), lt(_315628, _315628)], (136 ^ _251302) ^ [_255596, _255598] : [-(duplicatefreeP(_255596)), _255598 = _255596, duplicatefreeP(_255598)], (232 ^ _251302) ^ [_258560, _258562, _258564, _258566] : [-(neq(_258564, _258560)), neq(_258566, _258562), _258566 = _258564, _258562 = _258560], (2 ^ _251302) ^ [_251426] : [-(_251426 = _251426)], (1633 ^ _251302) ^ [_308107] : [ssItem(_308107), -(equalelemsP(cons(_308107, nil)))], (268 ^ _251302) ^ [_259861, _259863, _259865, _259867] : [-(cons(_259867, _259863) = cons(_259865, _259861)), _259867 = _259865, _259863 = _259861], (1145 ^ _251302) ^ [_293026] : [ssItem(_293026), 1148 ^ _251302 : [(1149 ^ _251302) ^ [_293181] : [ssList(_293181), 1152 ^ _251302 : [(1153 ^ _251302) ^ [_293332] : [ssList(_293332), 1156 ^ _251302 : [(1157 ^ _251302) ^ [] : [memberP(app(_293181, _293332), _293026), -(memberP(_293181, _293026)), -(memberP(_293332, _293026))], (1167 ^ _251302) ^ [] : [1168 ^ _251302 : [(1171 ^ _251302) ^ [] : [memberP(_293332, _293026)], (1169 ^ _251302) ^ [] : [memberP(_293181, _293026)]], -(memberP(app(_293181, _293332), _293026))]]]]]]], (278 ^ _251302) ^ [_260196] : [ssItem(_260196), 281 ^ _251302 : [(282 ^ _251302) ^ [_260334] : [ssItem(_260334), 285 ^ _251302 : [(292 ^ _251302) ^ [] : [-(_260196 = _260334), -(neq(_260196, _260334))], (286 ^ _251302) ^ [] : [neq(_260196, _260334), _260196 = _260334]]]]], (1213 ^ _251302) ^ [_295173] : [ssList(_295173), 1216 ^ _251302 : [(1217 ^ _251302) ^ [_295325] : [ssList(_295325), 1220 ^ _251302 : [(1221 ^ _251302) ^ [_295473] : [ssList(_295473), -(frontsegP(_295173, _295473)), frontsegP(_295173, _295325), frontsegP(_295325, _295473)]]]]], (390 ^ _251302) ^ [_263897] : [ssList(_263897), 393 ^ _251302 : [(394 ^ _251302) ^ [_264046] : [ssList(_264046), 397 ^ _251302 : [(407 ^ _251302) ^ [] : [-(rearsegP(_263897, _264046)), 408 ^ _251302 : [(409 ^ _251302) ^ [_264521] : [ssList(_264521), app(_264521, _264046) = _263897]]], (398 ^ _251302) ^ [] : [rearsegP(_263897, _264046), 402 ^ _251302 : [(405 ^ _251302) ^ [] : [-(app(401 ^ [_263897, _264046], _264046) = _263897)], (403 ^ _251302) ^ [] : [-(ssList(401 ^ [_263897, _264046]))]]]]]]], (1017 ^ _251302) ^ [_289120] : [ssList(_289120), -(app(nil, _289120) = _289120)], (1063 ^ _251302) ^ [_290535] : [ssItem(_290535), -(leq(_290535, _290535))], (1749 ^ _251302) ^ [_311811] : [ssList(_311811), 1752 ^ _251302 : [(1753 ^ _251302) ^ [_311963] : [ssList(_311963), 1756 ^ _251302 : [(1757 ^ _251302) ^ [_312111] : [ssList(_312111), -(app(app(_311811, _311963), _312111) = app(_311811, app(_311963, _312111)))]]]]], (1465 ^ _251302) ^ [_303023] : [ssList(_303023), 1468 ^ _251302 : [(1469 ^ _251302) ^ [_303185] : [ssList(_303185), 1472 ^ _251302 : [(1473 ^ _251302) ^ [_303343] : [ssList(_303343), 1476 ^ _251302 : [(1477 ^ _251302) ^ [_303497] : [ssList(_303497), segmentP(_303023, _303185), -(segmentP(app(app(_303343, _303023), _303497), _303185))]]]]]]], (1809 ^ _251302) ^ [_313758] : [ssList(_313758), 1812 ^ _251302 : [(1813 ^ _251302) ^ [_313906] : [ssList(_313906), -(nil = _313758), -(tl(app(_313758, _313906)) = app(tl(_313758), _313906))]]], (1211 ^ _251302) ^ [] : [singletonP(nil)], (1379 ^ _251302) ^ [_300391] : [ssList(_300391), 1382 ^ _251302 : [(1383 ^ _251302) ^ [_300540] : [ssList(_300540), 1386 ^ _251302 : [(1387 ^ _251302) ^ [_300685] : [ssList(_300685), rearsegP(_300391, _300540), -(rearsegP(app(_300685, _300391), _300540))]]]]], (993 ^ _251302) ^ [_288245] : [ssList(_288245), 996 ^ _251302 : [(997 ^ _251302) ^ [_288377] : [ssList(_288377), -(ssList(app(_288245, _288377)))]]], (1517 ^ _251302) ^ [_304694] : [ssItem(_304694), -(totalorderP(cons(_304694, nil)))], (1253 ^ _251302) ^ [_296394] : [ssList(_296394), -(frontsegP(_296394, _296394))], (1487 ^ _251302) ^ [_303833] : [ssList(_303833), -(segmentP(_303833, nil))], (34 ^ _251302) ^ [_252494, _252496] : [-(singletonP(_252494)), _252496 = _252494, singletonP(_252496)], (1311 ^ _251302) ^ [_298366] : [ssList(_298366), -(frontsegP(_298366, nil))], (1023 ^ _251302) ^ [_289314] : [ssItem(_289314), 1026 ^ _251302 : [(1027 ^ _251302) ^ [_289456] : [ssItem(_289456), -(_289314 = _289456), leq(_289314, _289456), leq(_289456, _289314)]]], (1403 ^ _251302) ^ [_301186] : [ssList(_301186), 1406 ^ _251302 : [(1413 ^ _251302) ^ [] : [nil = _301186, -(rearsegP(nil, _301186))], (1407 ^ _251302) ^ [] : [rearsegP(nil, _301186), -(nil = _301186)]]], (1579 ^ _251302) ^ [_306523] : [ssItem(_306523), -(strictorderedP(cons(_306523, nil)))], (184 ^ _251302) ^ [_257102, _257104, _257106, _257108] : [-(leq(_257106, _257102)), leq(_257108, _257104), _257108 = _257106, _257104 = _257102], (754 ^ _251302) ^ [_279332] : [ssList(_279332), 757 ^ _251302 : [(758 ^ _251302) ^ [] : [duplicatefreeP(_279332), 761 ^ _251302 : [(762 ^ _251302) ^ [_279630] : [ssItem(_279630), 765 ^ _251302 : [(766 ^ _251302) ^ [_279816] : [ssItem(_279816), 769 ^ _251302 : [(770 ^ _251302) ^ [_279998] : [ssList(_279998), 773 ^ _251302 : [(774 ^ _251302) ^ [_280176] : [ssList(_280176), 777 ^ _251302 : [(778 ^ _251302) ^ [_280350] : [ssList(_280350), app(app(_279998, cons(_279630, _280176)), cons(_279816, _280350)) = _279332, _279630 = _279816]]]]]]]]]]], (788 ^ _251302) ^ [] : [790 ^ _251302 : [(797 ^ _251302) ^ [] : [-(ssList(795 ^ [_279332]))], (805 ^ _251302) ^ [] : [-(app(app(795 ^ [_279332], cons(789 ^ [_279332], 798 ^ [_279332])), cons(792 ^ [_279332], 801 ^ [_279332])) = _279332)], (807 ^ _251302) ^ [] : [-(789 ^ [_279332] = 792 ^ [_279332])], (800 ^ _251302) ^ [] : [-(ssList(798 ^ [_279332]))], (791 ^ _251302) ^ [] : [-(ssItem(789 ^ [_279332]))], (794 ^ _251302) ^ [] : [-(ssItem(792 ^ [_279332]))], (803 ^ _251302) ^ [] : [-(ssList(801 ^ [_279332]))]], -(duplicatefreeP(_279332))]]], (963 ^ _251302) ^ [_287275] : [ssList(_287275), 966 ^ _251302 : [(967 ^ _251302) ^ [_287410] : [ssItem(_287410), -(hd(cons(_287410, _287275)) = _287410)]]], (1089 ^ _251302) ^ [_291310] : [ssItem(_291310), 1092 ^ _251302 : [(1093 ^ _251302) ^ [_291448] : [ssItem(_291448), lt(_291310, _291448), lt(_291448, _291310)]]], (1739 ^ _251302) ^ [_311453] : [ssList(_311453), 1742 ^ _251302 : [(1743 ^ _251302) ^ [_311592] : [ssItem(_311592), -(cons(_311592, _311453) = app(cons(_311592, nil), _311453))]]], (1441 ^ _251302) ^ [_302314] : [ssList(_302314), 1444 ^ _251302 : [(1445 ^ _251302) ^ [_302456] : [ssList(_302456), -(_302314 = _302456), segmentP(_302314, _302456), segmentP(_302456, _302314)]]], (1259 ^ _251302) ^ [_296582] : [ssList(_296582), 1262 ^ _251302 : [(1263 ^ _251302) ^ [_296731] : [ssList(_296731), 1266 ^ _251302 : [(1267 ^ _251302) ^ [_296876] : [ssList(_296876), frontsegP(_296582, _296731), -(frontsegP(app(_296582, _296876), _296731))]]]]], (1875 ^ _251302) ^ [_315817] : [ssItem(_315817), 1878 ^ _251302 : [(1879 ^ _251302) ^ [_315969] : [ssItem(_315969), 1882 ^ _251302 : [(1883 ^ _251302) ^ [_316117] : [ssItem(_316117), -(lt(_315817, _316117)), leq(_315817, _315969), lt(_315969, _316117)]]]]], (1541 ^ _251302) ^ [_305429] : [ssItem(_305429), 1544 ^ _251302 : [(1545 ^ _251302) ^ [_305588] : [ssList(_305588), 1548 ^ _251302 : [(1563 ^ _251302) ^ [] : [-(totalorderedP(cons(_305429, _305588))), 1564 ^ _251302 : [(1567 ^ _251302) ^ [] : [-(nil = _305588), totalorderedP(_305588), leq(_305429, hd(_305588))], (1565 ^ _251302) ^ [] : [nil = _305588]]], (1549 ^ _251302) ^ [] : [totalorderedP(cons(_305429, _305588)), -(nil = _305588), 1556 ^ _251302 : [(1561 ^ _251302) ^ [] : [-(leq(_305429, hd(_305588)))], (1559 ^ _251302) ^ [] : [-(totalorderedP(_305588))], (1557 ^ _251302) ^ [] : [nil = _305588]]]]]]], (1721 ^ _251302) ^ [_310834] : [ssList(_310834), 1724 ^ _251302 : [(1725 ^ _251302) ^ [_310986] : [ssList(_310986), 1728 ^ _251302 : [(1729 ^ _251302) ^ [_311134] : [ssList(_311134), app(_310986, _311134) = app(_310986, _310834), -(_311134 = _310834)]]]]], (340 ^ _251302) ^ [_262296] : [ssList(_262296), 343 ^ _251302 : [(353 ^ _251302) ^ [] : [-(singletonP(_262296)), 354 ^ _251302 : [(355 ^ _251302) ^ [_262745] : [ssItem(_262745), cons(_262745, nil) = _262296]]], (344 ^ _251302) ^ [] : [singletonP(_262296), 348 ^ _251302 : [(351 ^ _251302) ^ [] : [-(cons(347 ^ [_262296], nil) = _262296)], (349 ^ _251302) ^ [] : [-(ssItem(347 ^ [_262296]))]]]]], (1041 ^ _251302) ^ [_289835] : [ssItem(_289835), 1044 ^ _251302 : [(1045 ^ _251302) ^ [_289987] : [ssItem(_289987), 1048 ^ _251302 : [(1049 ^ _251302) ^ [_290135] : [ssItem(_290135), -(leq(_289835, _290135)), leq(_289835, _289987), leq(_289987, _290135)]]]]], (246 ^ _251302) ^ [_259058, _259060] : [_259060 = _259058, -(hd(_259060) = hd(_259058))], (1533 ^ _251302) ^ [_305184] : [ssItem(_305184), -(totalorderedP(cons(_305184, nil)))], (927 ^ _251302) ^ [_286090] : [ssList(_286090), -(nil = _286090), 935 ^ _251302 : [(941 ^ _251302) ^ [] : [-(cons(937 ^ [_286090], 934 ^ [_286090]) = _286090)], (939 ^ _251302) ^ [] : [-(ssItem(937 ^ [_286090]))], (936 ^ _251302) ^ [] : [-(ssList(934 ^ [_286090]))]]], (1493 ^ _251302) ^ [_304021] : [ssList(_304021), 1496 ^ _251302 : [(1503 ^ _251302) ^ [] : [nil = _304021, -(segmentP(nil, _304021))], (1497 ^ _251302) ^ [] : [segmentP(nil, _304021), -(nil = _304021)]]], (363 ^ _251302) ^ [_263001] : [ssList(_263001), 366 ^ _251302 : [(367 ^ _251302) ^ [_263150] : [ssList(_263150), 370 ^ _251302 : [(380 ^ _251302) ^ [] : [-(frontsegP(_263001, _263150)), 381 ^ _251302 : [(382 ^ _251302) ^ [_263625] : [ssList(_263625), app(_263150, _263625) = _263001]]], (371 ^ _251302) ^ [] : [frontsegP(_263001, _263150), 375 ^ _251302 : [(378 ^ _251302) ^ [] : [-(app(_263150, 374 ^ [_263001, _263150]) = _263001)], (376 ^ _251302) ^ [] : [-(ssList(374 ^ [_263001, _263150]))]]]]]]], (306 ^ _251302) ^ [_261047] : [ssList(_261047), 309 ^ _251302 : [(310 ^ _251302) ^ [_261209] : [ssItem(_261209), 313 ^ _251302 : [(326 ^ _251302) ^ [] : [-(memberP(_261047, _261209)), 327 ^ _251302 : [(328 ^ _251302) ^ [_261857] : [ssList(_261857), 331 ^ _251302 : [(332 ^ _251302) ^ [_262005] : [ssList(_262005), app(_261857, cons(_261209, _262005)) = _261047]]]]], (314 ^ _251302) ^ [] : [memberP(_261047, _261209), 318 ^ _251302 : [(324 ^ _251302) ^ [] : [-(app(317 ^ [_261047, _261209], cons(_261209, 320 ^ [_261047, _261209])) = _261047)], (322 ^ _251302) ^ [] : [-(ssList(320 ^ [_261047, _261209]))], (319 ^ _251302) ^ [] : [-(ssList(317 ^ [_261047, _261209]))]]]]]]], (1693 ^ _251302) ^ [_309925] : [ssList(_309925), -(nil = _309925), -(cons(hd(_309925), tl(_309925)) = _309925)], (811 ^ _251302) ^ [_281842] : [ssList(_281842), 814 ^ _251302 : [(815 ^ _251302) ^ [] : [equalelemsP(_281842), 818 ^ _251302 : [(819 ^ _251302) ^ [_282125] : [ssItem(_282125), 822 ^ _251302 : [(823 ^ _251302) ^ [_282296] : [ssItem(_282296), 826 ^ _251302 : [(827 ^ _251302) ^ [_282463] : [ssList(_282463), 830 ^ _251302 : [(831 ^ _251302) ^ [_282626] : [ssList(_282626), app(_282463, cons(_282125, cons(_282296, _282626))) = _281842, -(_282125 = _282296)]]]]]]]]], (841 ^ _251302) ^ [] : [843 ^ _251302 : [(847 ^ _251302) ^ [] : [-(ssItem(845 ^ [_281842]))], (844 ^ _251302) ^ [] : [-(ssItem(842 ^ [_281842]))], (857 ^ _251302) ^ [] : [842 ^ [_281842] = 845 ^ [_281842]], (853 ^ _251302) ^ [] : [-(ssList(851 ^ [_281842]))], (855 ^ _251302) ^ [] : [-(app(848 ^ [_281842], cons(842 ^ [_281842], cons(845 ^ [_281842], 851 ^ [_281842]))) = _281842)], (850 ^ _251302) ^ [] : [-(ssList(848 ^ [_281842]))]], -(equalelemsP(_281842))]]], (1125 ^ _251302) ^ [_292439] : [ssItem(_292439), 1128 ^ _251302 : [(1129 ^ _251302) ^ [_292575] : [ssItem(_292575), 1132 ^ _251302 : [(1139 ^ _251302) ^ [] : [lt(_292575, _292439), -(gt(_292439, _292575))], (1133 ^ _251302) ^ [] : [gt(_292439, _292575), -(lt(_292575, _292439))]]]]], (973 ^ _251302) ^ [_287621] : [ssList(_287621), -(nil = _287621), -(ssList(tl(_287621)))], (1823 ^ _251302) ^ [_314219] : [ssItem(_314219), 1826 ^ _251302 : [(1827 ^ _251302) ^ [_314361] : [ssItem(_314361), -(_314219 = _314361), geq(_314219, _314361), geq(_314361, _314219)]]], (953 ^ _251302) ^ [_286997] : [ssList(_286997), -(nil = _286997), -(ssItem(hd(_286997)))], (1667 ^ _251302) ^ [_309180] : [ssList(_309180), 1670 ^ _251302 : [(1671 ^ _251302) ^ [_309346] : [ssList(_309346), -(_309346 = _309180), -(nil = _309346), -(nil = _309180), hd(_309346) = hd(_309180), tl(_309346) = tl(_309180)]]], (1841 ^ _251302) ^ [_314740] : [ssItem(_314740), 1844 ^ _251302 : [(1845 ^ _251302) ^ [_314892] : [ssItem(_314892), 1848 ^ _251302 : [(1849 ^ _251302) ^ [_315040] : [ssItem(_315040), -(geq(_314740, _315040)), geq(_314740, _314892), geq(_314892, _315040)]]]]], (1897 ^ _251302) ^ [_316517] : [ssItem(_316517), 1900 ^ _251302 : [(1901 ^ _251302) ^ [_316659] : [ssItem(_316659), leq(_316517, _316659), -(_316517 = _316659), -(lt(_316517, _316659))]]], (1639 ^ _251302) ^ [] : [-(equalelemsP(nil))], (1863 ^ _251302) ^ [_315440] : [ssItem(_315440), -(geq(_315440, _315440))], (1625 ^ _251302) ^ [_307862] : [ssItem(_307862), -(duplicatefreeP(cons(_307862, nil)))], (577 ^ _251302) ^ [_271592] : [ssList(_271592), 580 ^ _251302 : [(581 ^ _251302) ^ [] : [strictorderP(_271592), 584 ^ _251302 : [(585 ^ _251302) ^ [_271894] : [ssItem(_271894), 588 ^ _251302 : [(589 ^ _251302) ^ [_272084] : [ssItem(_272084), 592 ^ _251302 : [(593 ^ _251302) ^ [_272270] : [ssList(_272270), 596 ^ _251302 : [(597 ^ _251302) ^ [_272452] : [ssList(_272452), 600 ^ _251302 : [(601 ^ _251302) ^ [_272630] : [ssList(_272630), app(app(_272270, cons(_271894, _272452)), cons(_272084, _272630)) = _271592, -(lt(_271894, _272084)), -(lt(_272084, _271894))]]]]]]]]]]], (615 ^ _251302) ^ [] : [617 ^ _251302 : [(624 ^ _251302) ^ [] : [-(ssList(622 ^ [_271592]))], (632 ^ _251302) ^ [] : [-(app(app(622 ^ [_271592], cons(616 ^ [_271592], 625 ^ [_271592])), cons(619 ^ [_271592], 628 ^ [_271592])) = _271592)], (618 ^ _251302) ^ [] : [-(ssItem(616 ^ [_271592]))], (634 ^ _251302) ^ [] : [lt(616 ^ [_271592], 619 ^ [_271592])], (627 ^ _251302) ^ [] : [-(ssList(625 ^ [_271592]))], (630 ^ _251302) ^ [] : [-(ssList(628 ^ [_271592]))], (636 ^ _251302) ^ [] : [lt(619 ^ [_271592], 616 ^ [_271592])], (621 ^ _251302) ^ [] : [-(ssItem(619 ^ [_271592]))]], -(strictorderP(_271592))]]], (44 ^ _251302) ^ [_252817, _252819, _252821, _252823] : [-(frontsegP(_252821, _252817)), frontsegP(_252823, _252819), _252823 = _252821, _252819 = _252817], (1795 ^ _251302) ^ [_313306] : [ssList(_313306), 1798 ^ _251302 : [(1799 ^ _251302) ^ [_313451] : [ssList(_313451), -(nil = _313306), -(hd(app(_313306, _313451)) = hd(_313306))]]], (20 ^ _251302) ^ [_252078, _252080, _252082, _252084] : [-(memberP(_252082, _252078)), memberP(_252084, _252080), _252084 = _252082, _252080 = _252078], (1523 ^ _251302) ^ [] : [-(totalorderP(nil))], (1789 ^ _251302) ^ [_313112] : [ssList(_313112), -(app(_313112, nil) = _313112)], (697 ^ _251302) ^ [_276844] : [ssList(_276844), 700 ^ _251302 : [(701 ^ _251302) ^ [] : [strictorderedP(_276844), 704 ^ _251302 : [(705 ^ _251302) ^ [_277140] : [ssItem(_277140), 708 ^ _251302 : [(709 ^ _251302) ^ [_277324] : [ssItem(_277324), 712 ^ _251302 : [(713 ^ _251302) ^ [_277504] : [ssList(_277504), 716 ^ _251302 : [(717 ^ _251302) ^ [_277680] : [ssList(_277680), 720 ^ _251302 : [(721 ^ _251302) ^ [_277852] : [ssList(_277852), app(app(_277504, cons(_277140, _277680)), cons(_277324, _277852)) = _276844, -(lt(_277140, _277324))]]]]]]]]]]], (731 ^ _251302) ^ [] : [733 ^ _251302 : [(740 ^ _251302) ^ [] : [-(ssList(738 ^ [_276844]))], (748 ^ _251302) ^ [] : [-(app(app(738 ^ [_276844], cons(732 ^ [_276844], 741 ^ [_276844])), cons(735 ^ [_276844], 744 ^ [_276844])) = _276844)], (750 ^ _251302) ^ [] : [lt(732 ^ [_276844], 735 ^ [_276844])], (743 ^ _251302) ^ [] : [-(ssList(741 ^ [_276844]))], (734 ^ _251302) ^ [] : [-(ssItem(732 ^ [_276844]))], (737 ^ _251302) ^ [] : [-(ssItem(735 ^ [_276844]))], (746 ^ _251302) ^ [] : [-(ssList(744 ^ [_276844]))]], -(strictorderedP(_276844))]]], (198 ^ _251302) ^ [_257546, _257548, _257550, _257552] : [-(gt(_257550, _257546)), gt(_257552, _257548), _257552 = _257550, _257548 = _257546], (1373 ^ _251302) ^ [_300203] : [ssList(_300203), -(rearsegP(_300203, _300203))], (116 ^ _251302) ^ [_255006, _255008] : [-(totalorderedP(_255006)), _255008 = _255006, totalorderedP(_255008)], (10 ^ _251302) ^ [_251737, _251739, _251741] : [-(_251741 = _251737), _251741 = _251739, _251739 = _251737], (1941 ^ _251302) ^ [_317794] : [ssItem(_317794), 1944 ^ _251302 : [(1945 ^ _251302) ^ [_317932] : [ssItem(_317932), gt(_317794, _317932), gt(_317932, _317794)]]], (1587 ^ _251302) ^ [_306768] : [ssItem(_306768), 1590 ^ _251302 : [(1591 ^ _251302) ^ [_306927] : [ssList(_306927), 1594 ^ _251302 : [(1609 ^ _251302) ^ [] : [-(strictorderedP(cons(_306768, _306927))), 1610 ^ _251302 : [(1613 ^ _251302) ^ [] : [-(nil = _306927), strictorderedP(_306927), lt(_306768, hd(_306927))], (1611 ^ _251302) ^ [] : [nil = _306927]]], (1595 ^ _251302) ^ [] : [strictorderedP(cons(_306768, _306927)), -(nil = _306927), 1602 ^ _251302 : [(1607 ^ _251302) ^ [] : [-(lt(_306768, hd(_306927)))], (1605 ^ _251302) ^ [] : [-(strictorderedP(_306927))], (1603 ^ _251302) ^ [] : [nil = _306927]]]]]]], (299 ^ _251302) ^ [] : [-(ssItem(297 ^ []))], (451 ^ _251302) ^ [_266042] : [ssList(_266042), 454 ^ _251302 : [(455 ^ _251302) ^ [] : [cyclefreeP(_266042), 458 ^ _251302 : [(459 ^ _251302) ^ [_266346] : [ssItem(_266346), 462 ^ _251302 : [(463 ^ _251302) ^ [_266538] : [ssItem(_266538), 466 ^ _251302 : [(467 ^ _251302) ^ [_266726] : [ssList(_266726), 470 ^ _251302 : [(471 ^ _251302) ^ [_266910] : [ssList(_266910), 474 ^ _251302 : [(475 ^ _251302) ^ [_267090] : [ssList(_267090), app(app(_266726, cons(_266346, _266910)), cons(_266538, _267090)) = _266042, leq(_266346, _266538), leq(_266538, _266346)]]]]]]]]]]], (489 ^ _251302) ^ [] : [491 ^ _251302 : [(498 ^ _251302) ^ [] : [-(ssList(496 ^ [_266042]))], (506 ^ _251302) ^ [] : [-(app(app(496 ^ [_266042], cons(490 ^ [_266042], 499 ^ [_266042])), cons(493 ^ [_266042], 502 ^ [_266042])) = _266042)], (492 ^ _251302) ^ [] : [-(ssItem(490 ^ [_266042]))], (508 ^ _251302) ^ [] : [-(leq(490 ^ [_266042], 493 ^ [_266042]))], (501 ^ _251302) ^ [] : [-(ssList(499 ^ [_266042]))], (504 ^ _251302) ^ [] : [-(ssList(502 ^ [_266042]))], (510 ^ _251302) ^ [] : [-(leq(493 ^ [_266042], 490 ^ [_266042]))], (495 ^ _251302) ^ [] : [-(ssItem(493 ^ [_266042]))]], -(cyclefreeP(_266042))]]], (1515 ^ _251302) ^ [] : [-(cyclefreeP(nil))], (1333 ^ _251302) ^ [_298982] : [ssList(_298982), 1336 ^ _251302 : [(1337 ^ _251302) ^ [_299134] : [ssList(_299134), 1340 ^ _251302 : [(1341 ^ _251302) ^ [_299282] : [ssList(_299282), -(rearsegP(_298982, _299282)), rearsegP(_298982, _299134), rearsegP(_299134, _299282)]]]]], (302 ^ _251302) ^ [] : [-(ssItem(300 ^ []))], (170 ^ _251302) ^ [_256658, _256660, _256662, _256664] : [-(lt(_256662, _256658)), lt(_256664, _256660), _256664 = _256662, _256660 = _256658], (1103 ^ _251302) ^ [_291739] : [ssItem(_291739), 1106 ^ _251302 : [(1107 ^ _251302) ^ [_291891] : [ssItem(_291891), 1110 ^ _251302 : [(1111 ^ _251302) ^ [_292039] : [ssItem(_292039), -(lt(_291739, _292039)), lt(_291739, _291891), lt(_291891, _292039)]]]]], (1955 ^ _251302) ^ [_318203] : [ssItem(_318203), 1958 ^ _251302 : [(1959 ^ _251302) ^ [_318355] : [ssItem(_318355), 1962 ^ _251302 : [(1963 ^ _251302) ^ [_318503] : [ssItem(_318503), -(gt(_318203, _318503)), gt(_318203, _318355), gt(_318355, _318503)]]]]], (893 ^ _251302) ^ [_284840] : [ssList(_284840), 896 ^ _251302 : [(897 ^ _251302) ^ [_284975] : [ssItem(_284975), cons(_284975, _284840) = _284840]]], (1205 ^ _251302) ^ [_294932] : [ssItem(_294932), memberP(nil, _294932)], (640 ^ _251302) ^ [_274356] : [ssList(_274356), 643 ^ _251302 : [(644 ^ _251302) ^ [] : [totalorderedP(_274356), 647 ^ _251302 : [(648 ^ _251302) ^ [_274652] : [ssItem(_274652), 651 ^ _251302 : [(652 ^ _251302) ^ [_274836] : [ssItem(_274836), 655 ^ _251302 : [(656 ^ _251302) ^ [_275016] : [ssList(_275016), 659 ^ _251302 : [(660 ^ _251302) ^ [_275192] : [ssList(_275192), 663 ^ _251302 : [(664 ^ _251302) ^ [_275364] : [ssList(_275364), app(app(_275016, cons(_274652, _275192)), cons(_274836, _275364)) = _274356, -(leq(_274652, _274836))]]]]]]]]]]], (674 ^ _251302) ^ [] : [676 ^ _251302 : [(683 ^ _251302) ^ [] : [-(ssList(681 ^ [_274356]))], (691 ^ _251302) ^ [] : [-(app(app(681 ^ [_274356], cons(675 ^ [_274356], 684 ^ [_274356])), cons(678 ^ [_274356], 687 ^ [_274356])) = _274356)], (693 ^ _251302) ^ [] : [leq(675 ^ [_274356], 678 ^ [_274356])], (686 ^ _251302) ^ [] : [-(ssList(684 ^ [_274356]))], (677 ^ _251302) ^ [] : [-(ssItem(675 ^ [_274356]))], (680 ^ _251302) ^ [] : [-(ssItem(678 ^ [_274356]))], (689 ^ _251302) ^ [] : [-(ssList(687 ^ [_274356]))]], -(totalorderedP(_274356))]]], (1654 ^ _251302) ^ [_308766] : [ssList(_308766), -(nil = _308766), 1662 ^ _251302 : [(1665 ^ _251302) ^ [] : [-(tl(_308766) = 1661 ^ [_308766])], (1663 ^ _251302) ^ [] : [-(ssList(1661 ^ [_308766]))]]], (4 ^ _251302) ^ [_251533, _251535] : [_251535 = _251533, -(_251533 = _251535)], (417 ^ _251302) ^ [_264793] : [ssList(_264793), 420 ^ _251302 : [(421 ^ _251302) ^ [_264955] : [ssList(_264955), 424 ^ _251302 : [(437 ^ _251302) ^ [] : [-(segmentP(_264793, _264955)), 438 ^ _251302 : [(439 ^ _251302) ^ [_265603] : [ssList(_265603), 442 ^ _251302 : [(443 ^ _251302) ^ [_265751] : [ssList(_265751), app(app(_265603, _264955), _265751) = _264793]]]]], (425 ^ _251302) ^ [] : [segmentP(_264793, _264955), 429 ^ _251302 : [(435 ^ _251302) ^ [] : [-(app(app(428 ^ [_264793, _264955], _264955), 431 ^ [_264793, _264955]) = _264793)], (433 ^ _251302) ^ [] : [-(ssList(431 ^ [_264793, _264955]))], (430 ^ _251302) ^ [] : [-(ssList(428 ^ [_264793, _264955]))]]]]]]], (1069 ^ _251302) ^ [_290723] : [ssItem(_290723), 1072 ^ _251302 : [(1073 ^ _251302) ^ [_290859] : [ssItem(_290859), 1076 ^ _251302 : [(1083 ^ _251302) ^ [] : [leq(_290859, _290723), -(geq(_290723, _290859))], (1077 ^ _251302) ^ [] : [geq(_290723, _290859), -(leq(_290859, _290723))]]]]], (212 ^ _251302) ^ [_257962, _257964] : [-(ssItem(_257962)), _257964 = _257962, ssItem(_257964)], (1175 ^ _251302) ^ [_293979] : [ssItem(_293979), 1178 ^ _251302 : [(1179 ^ _251302) ^ [_294134] : [ssItem(_294134), 1182 ^ _251302 : [(1183 ^ _251302) ^ [_294285] : [ssList(_294285), 1186 ^ _251302 : [(1187 ^ _251302) ^ [] : [memberP(cons(_294134, _294285), _293979), -(_293979 = _294134), -(memberP(_294285, _293979))], (1197 ^ _251302) ^ [] : [1198 ^ _251302 : [(1201 ^ _251302) ^ [] : [memberP(_294285, _293979)], (1199 ^ _251302) ^ [] : [_293979 = _294134]], -(memberP(cons(_294134, _294285), _293979))]]]]]]], (258 ^ _251302) ^ [_259522, _259524, _259526, _259528] : [-(app(_259528, _259524) = app(_259526, _259522)), _259528 = _259526, _259524 = _259522], (1531 ^ _251302) ^ [] : [-(strictorderP(nil))], (1763 ^ _251302) ^ [_312349] : [ssList(_312349), 1766 ^ _251302 : [(1767 ^ _251302) ^ [_312494] : [ssList(_312494), 1770 ^ _251302 : [(1779 ^ _251302) ^ [] : [-(nil = app(_312349, _312494)), nil = _312494, nil = _312349], (1771 ^ _251302) ^ [] : [nil = app(_312349, _312494), 1774 ^ _251302 : [(1777 ^ _251302) ^ [] : [-(nil = _312349)], (1775 ^ _251302) ^ [] : [-(nil = _312494)]]]]]]], (1003 ^ _251302) ^ [_288582] : [ssList(_288582), 1006 ^ _251302 : [(1007 ^ _251302) ^ [_288734] : [ssList(_288734), 1010 ^ _251302 : [(1011 ^ _251302) ^ [_288882] : [ssItem(_288882), -(cons(_288882, app(_288734, _288582)) = app(cons(_288882, _288734), _288582))]]]]], (1509 ^ _251302) ^ [_304449] : [ssItem(_304449), -(cyclefreeP(cons(_304449, nil)))], (1539 ^ _251302) ^ [] : [-(totalorderedP(nil))], (1317 ^ _251302) ^ [_298554] : [ssList(_298554), 1320 ^ _251302 : [(1327 ^ _251302) ^ [] : [nil = _298554, -(frontsegP(nil, _298554))], (1321 ^ _251302) ^ [] : [frontsegP(nil, _298554), -(nil = _298554)]]], (1397 ^ _251302) ^ [_300998] : [ssList(_300998), -(rearsegP(_300998, nil))], (1585 ^ _251302) ^ [] : [-(strictorderedP(nil))], (96 ^ _251302) ^ [_254416, _254418] : [-(totalorderP(_254416)), _254418 = _254416, totalorderP(_254418)], (146 ^ _251302) ^ [_255891, _255893] : [-(equalelemsP(_255891)), _255893 = _255891, equalelemsP(_255893)], (881 ^ _251302) ^ [_284450] : [ssList(_284450), 884 ^ _251302 : [(885 ^ _251302) ^ [_284582] : [ssItem(_284582), -(ssList(cons(_284582, _284450)))]]], (1235 ^ _251302) ^ [_295873] : [ssList(_295873), 1238 ^ _251302 : [(1239 ^ _251302) ^ [_296015] : [ssList(_296015), -(_295873 = _296015), frontsegP(_295873, _296015), frontsegP(_296015, _295873)]]], (1915 ^ _251302) ^ [_317039] : [ssItem(_317039), 1918 ^ _251302 : [(1919 ^ _251302) ^ [_317183] : [ssItem(_317183), 1922 ^ _251302 : [(1931 ^ _251302) ^ [] : [-(lt(_317039, _317183)), -(_317039 = _317183), leq(_317039, _317183)], (1923 ^ _251302) ^ [] : [lt(_317039, _317183), 1926 ^ _251302 : [(1929 ^ _251302) ^ [] : [-(leq(_317039, _317183))], (1927 ^ _251302) ^ [] : [_317039 = _317183]]]]]]], (903 ^ _251302) ^ [_285183] : [ssList(_285183), 906 ^ _251302 : [(907 ^ _251302) ^ [_285351] : [ssList(_285351), 910 ^ _251302 : [(911 ^ _251302) ^ [_285515] : [ssItem(_285515), 914 ^ _251302 : [(915 ^ _251302) ^ [_285675] : [ssItem(_285675), cons(_285515, _285183) = cons(_285675, _285351), 922 ^ _251302 : [(925 ^ _251302) ^ [] : [-(_285351 = _285183)], (923 ^ _251302) ^ [] : [-(_285515 = _285675)]]]]]]]]], (304 ^ _251302) ^ [] : [297 ^ [] = 300 ^ []], (1631 ^ _251302) ^ [] : [-(duplicatefreeP(nil))], (1525 ^ _251302) ^ [_304939] : [ssItem(_304939), -(strictorderP(cons(_304939, nil)))], (156 ^ _251302) ^ [_256214, _256216, _256218, _256220] : [-(geq(_256218, _256214)), geq(_256220, _256216), _256220 = _256218, _256216 = _256214], (891 ^ _251302) ^ [] : [-(ssList(nil))], (983 ^ _251302) ^ [_287899] : [ssList(_287899), 986 ^ _251302 : [(987 ^ _251302) ^ [_288034] : [ssItem(_288034), -(tl(cons(_288034, _287899)) = _287899)]]], (86 ^ _251302) ^ [_254121, _254123] : [-(cyclefreeP(_254121)), _254123 = _254121, cyclefreeP(_254123)], (1277 ^ _251302) ^ [_297189] : [ssItem(_297189), 1280 ^ _251302 : [(1281 ^ _251302) ^ [_297357] : [ssItem(_297357), 1284 ^ _251302 : [(1285 ^ _251302) ^ [_297521] : [ssList(_297521), 1288 ^ _251302 : [(1289 ^ _251302) ^ [_297681] : [ssList(_297681), 1292 ^ _251302 : [(1301 ^ _251302) ^ [] : [-(frontsegP(cons(_297189, _297521), cons(_297357, _297681))), _297189 = _297357, frontsegP(_297521, _297681)], (1293 ^ _251302) ^ [] : [frontsegP(cons(_297189, _297521), cons(_297357, _297681)), 1296 ^ _251302 : [(1299 ^ _251302) ^ [] : [-(frontsegP(_297521, _297681))], (1297 ^ _251302) ^ [] : [-(_297189 = _297357)]]]]]]]]]]], (1703 ^ _251302) ^ [_310215] : [ssList(_310215), 1706 ^ _251302 : [(1707 ^ _251302) ^ [_310367] : [ssList(_310367), 1710 ^ _251302 : [(1711 ^ _251302) ^ [_310515] : [ssList(_310515), app(_310515, _310367) = app(_310215, _310367), -(_310515 = _310215)]]]]], (514 ^ _251302) ^ [_268828] : [ssList(_268828), 517 ^ _251302 : [(518 ^ _251302) ^ [] : [totalorderP(_268828), 521 ^ _251302 : [(522 ^ _251302) ^ [_269130] : [ssItem(_269130), 525 ^ _251302 : [(526 ^ _251302) ^ [_269320] : [ssItem(_269320), 529 ^ _251302 : [(530 ^ _251302) ^ [_269506] : [ssList(_269506), 533 ^ _251302 : [(534 ^ _251302) ^ [_269688] : [ssList(_269688), 537 ^ _251302 : [(538 ^ _251302) ^ [_269866] : [ssList(_269866), app(app(_269506, cons(_269130, _269688)), cons(_269320, _269866)) = _268828, -(leq(_269130, _269320)), -(leq(_269320, _269130))]]]]]]]]]]], (552 ^ _251302) ^ [] : [554 ^ _251302 : [(561 ^ _251302) ^ [] : [-(ssList(559 ^ [_268828]))], (569 ^ _251302) ^ [] : [-(app(app(559 ^ [_268828], cons(553 ^ [_268828], 562 ^ [_268828])), cons(556 ^ [_268828], 565 ^ [_268828])) = _268828)], (555 ^ _251302) ^ [] : [-(ssItem(553 ^ [_268828]))], (571 ^ _251302) ^ [] : [leq(553 ^ [_268828], 556 ^ [_268828])], (564 ^ _251302) ^ [] : [-(ssList(562 ^ [_268828]))], (567 ^ _251302) ^ [] : [-(ssList(565 ^ [_268828]))], (573 ^ _251302) ^ [] : [leq(556 ^ [_268828], 553 ^ [_268828])], (558 ^ _251302) ^ [] : [-(ssItem(556 ^ [_268828]))]], -(totalorderP(_268828))]]], (1419 ^ _251302) ^ [_301614] : [ssList(_301614), 1422 ^ _251302 : [(1423 ^ _251302) ^ [_301766] : [ssList(_301766), 1426 ^ _251302 : [(1427 ^ _251302) ^ [_301914] : [ssList(_301914), -(segmentP(_301614, _301914)), segmentP(_301614, _301766), segmentP(_301766, _301914)]]]]], (1641 ^ _251302) ^ [_308352] : [ssList(_308352), -(nil = _308352), 1649 ^ _251302 : [(1652 ^ _251302) ^ [] : [-(hd(_308352) = 1648 ^ [_308352])], (1650 ^ _251302) ^ [] : [-(ssItem(1648 ^ [_308352]))]]], (222 ^ _251302) ^ [_258257, _258259] : [-(ssList(_258257)), _258259 = _258257, ssList(_258259)], (126 ^ _251302) ^ [_255301, _255303] : [-(strictorderedP(_255301)), _255303 = _255301, strictorderedP(_255303)]], input).
% 47.01/45.87 ncf('1',plain,[-(nil = 1982 ^ []), nil = 1985 ^ []],start(1997 ^ 0)).
% 47.01/45.87 ncf('1.1',plain,[nil = 1982 ^ [], -(nil = 1976 ^ []), 1982 ^ [] = 1976 ^ []],extension(10 ^ 1,bind([[_251737, _251739, _251741], [1976 ^ [], 1982 ^ [], nil]]))).
% 47.01/45.87 ncf('1.1.1',plain,[nil = 1976 ^ []],extension(1995 ^ 2)).
% 47.01/45.87 ncf('1.1.2',plain,[-(1982 ^ [] = 1976 ^ []), 1976 ^ [] = 1982 ^ []],extension(4 ^ 2,bind([[_251533, _251535], [1982 ^ [], 1976 ^ []]]))).
% 47.01/45.87 ncf('1.1.2.1',plain,[-(1976 ^ [] = 1982 ^ [])],extension(1993 ^ 3)).
% 47.01/45.87 ncf('1.2',plain,[-(nil = 1985 ^ []), nil = 1979 ^ [], 1979 ^ [] = 1985 ^ []],extension(10 ^ 1,bind([[_251737, _251739, _251741], [1985 ^ [], 1979 ^ [], nil]]))).
% 47.01/45.87 ncf('1.2.1',plain,[-(nil = 1979 ^ [])],extension(1989 ^ 2)).
% 47.01/45.87 ncf('1.2.2',plain,[-(1979 ^ [] = 1985 ^ [])],extension(1991 ^ 2)).
% 47.01/45.87 %-----------------------------------------------------
% 47.01/45.87 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------