%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWC375+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n032.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri May 19 12:13:23 EDT 2023
% Result : Theorem 14.17s 14.67s
% Output : Proof 14.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.09 % Problem : SWC375+1 : TPTP v8.1.2. Released v2.4.0.
% 0.05/0.09 % Command : nanocop.sh %s %d
% 0.08/0.27 % Computer : n032.cluster.edu
% 0.08/0.27 % Model : x86_64 x86_64
% 0.08/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.27 % Memory : 8042.1875MB
% 0.08/0.27 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.27 % CPULimit : 300
% 0.08/0.27 % WCLimit : 300
% 0.08/0.27 % DateTime : Fri May 19 00:57:50 EDT 2023
% 0.08/0.27 % CPUTime :
% 14.17/14.67
% 14.17/14.67 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 14.17/14.67 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.17/14.67 %-----------------------------------------------------
% 14.17/14.67 ncf(matrix, plain, [(1978 ^ _232996) ^ [] : [-(ssList(1976 ^ []))], (1981 ^ _232996) ^ [] : [-(ssList(1979 ^ []))], (1984 ^ _232996) ^ [] : [-(ssList(1982 ^ []))], (1987 ^ _232996) ^ [] : [-(ssList(1985 ^ []))], (1989 ^ _232996) ^ [] : [-(1979 ^ [] = 1985 ^ [])], (1991 ^ _232996) ^ [] : [-(1976 ^ [] = 1982 ^ [])], (1993 ^ _232996) ^ [] : [-(1985 ^ [] = 1982 ^ [])], (1996 ^ _232996) ^ [] : [-(ssItem(1994 ^ []))], (1998 ^ _232996) ^ [] : [-(memberP(1979 ^ [], 1994 ^ [])), -(memberP(1976 ^ [], 1994 ^ []))], (2004 ^ _232996) ^ [] : [memberP(1979 ^ [], 1994 ^ []), memberP(1976 ^ [], 1994 ^ [])], (246 ^ _232996) ^ [_240800, _240802, _240804, _240806] : [-(cons(_240806, _240802) = cons(_240804, _240800)), _240806 = _240804, _240802 = _240800], (256 ^ _232996) ^ [_241131, _241133] : [_241133 = _241131, -(hd(_241133) = hd(_241131))], (272 ^ _232996) ^ [_241688, _241690] : [_241690 = _241688, -(tl(_241690) = tl(_241688))], (262 ^ _232996) ^ [_241377, _241379, _241381, _241383] : [-(app(_241383, _241379) = app(_241381, _241377)), _241383 = _241381, _241379 = _241377], (2 ^ _232996) ^ [_233140] : [-(_233140 = _233140)], (4 ^ _232996) ^ [_233247, _233249] : [_233249 = _233247, -(_233247 = _233249)], (10 ^ _232996) ^ [_233451, _233453, _233455] : [-(_233455 = _233451), _233455 = _233453, _233453 = _233451], (20 ^ _232996) ^ [_233792, _233794, _233796, _233798] : [-(neq(_233796, _233792)), neq(_233798, _233794), _233798 = _233796, _233794 = _233792], (34 ^ _232996) ^ [_234208, _234210] : [-(singletonP(_234208)), _234210 = _234208, singletonP(_234210)], (44 ^ _232996) ^ [_234531, _234533, _234535, _234537] : [-(frontsegP(_234535, _234531)), frontsegP(_234537, _234533), _234537 = _234535, _234533 = _234531], (58 ^ _232996) ^ [_234975, _234977, _234979, _234981] : [-(rearsegP(_234979, _234975)), rearsegP(_234981, _234977), _234981 = _234979, _234977 = _234975], (72 ^ _232996) ^ [_235419, _235421, _235423, _235425] : [-(segmentP(_235423, _235419)), segmentP(_235425, _235421), _235425 = _235423, _235421 = _235419], (86 ^ _232996) ^ [_235835, _235837] : [-(cyclefreeP(_235835)), _235837 = _235835, cyclefreeP(_235837)], (96 ^ _232996) ^ [_236130, _236132] : [-(totalorderP(_236130)), _236132 = _236130, totalorderP(_236132)], (106 ^ _232996) ^ [_236425, _236427] : [-(strictorderP(_236425)), _236427 = _236425, strictorderP(_236427)], (116 ^ _232996) ^ [_236720, _236722] : [-(totalorderedP(_236720)), _236722 = _236720, totalorderedP(_236722)], (126 ^ _232996) ^ [_237015, _237017] : [-(strictorderedP(_237015)), _237017 = _237015, strictorderedP(_237017)], (136 ^ _232996) ^ [_237310, _237312] : [-(duplicatefreeP(_237310)), _237312 = _237310, duplicatefreeP(_237312)], (146 ^ _232996) ^ [_237605, _237607] : [-(equalelemsP(_237605)), _237607 = _237605, equalelemsP(_237607)], (156 ^ _232996) ^ [_237928, _237930, _237932, _237934] : [-(geq(_237932, _237928)), geq(_237934, _237930), _237934 = _237932, _237930 = _237928], (170 ^ _232996) ^ [_238372, _238374, _238376, _238378] : [-(lt(_238376, _238372)), lt(_238378, _238374), _238378 = _238376, _238374 = _238372], (184 ^ _232996) ^ [_238816, _238818, _238820, _238822] : [-(leq(_238820, _238816)), leq(_238822, _238818), _238822 = _238820, _238818 = _238816], (198 ^ _232996) ^ [_239260, _239262, _239264, _239266] : [-(gt(_239264, _239260)), gt(_239266, _239262), _239266 = _239264, _239262 = _239260], (212 ^ _232996) ^ [_239676, _239678] : [-(ssList(_239676)), _239678 = _239676, ssList(_239678)], (222 ^ _232996) ^ [_239971, _239973] : [-(ssItem(_239971)), _239973 = _239971, ssItem(_239973)], (232 ^ _232996) ^ [_240274, _240276, _240278, _240280] : [-(memberP(_240278, _240274)), memberP(_240280, _240276), _240280 = _240278, _240276 = _240274], (278 ^ _232996) ^ [_241910] : [ssItem(_241910), 281 ^ _232996 : [(282 ^ _232996) ^ [_242048] : [ssItem(_242048), 285 ^ _232996 : [(286 ^ _232996) ^ [] : [neq(_241910, _242048), _241910 = _242048], (292 ^ _232996) ^ [] : [-(_241910 = _242048), -(neq(_241910, _242048))]]]]], (299 ^ _232996) ^ [] : [-(ssItem(297 ^ []))], (302 ^ _232996) ^ [] : [-(ssItem(300 ^ []))], (304 ^ _232996) ^ [] : [297 ^ [] = 300 ^ []], (306 ^ _232996) ^ [_242761] : [ssList(_242761), 309 ^ _232996 : [(310 ^ _232996) ^ [_242923] : [ssItem(_242923), 313 ^ _232996 : [(314 ^ _232996) ^ [] : [memberP(_242761, _242923), 318 ^ _232996 : [(319 ^ _232996) ^ [] : [-(ssList(317 ^ [_242761, _242923]))], (322 ^ _232996) ^ [] : [-(ssList(320 ^ [_242761, _242923]))], (324 ^ _232996) ^ [] : [-(app(317 ^ [_242761, _242923], cons(_242923, 320 ^ [_242761, _242923])) = _242761)]]], (326 ^ _232996) ^ [] : [-(memberP(_242761, _242923)), 327 ^ _232996 : [(328 ^ _232996) ^ [_243571] : [ssList(_243571), 331 ^ _232996 : [(332 ^ _232996) ^ [_243719] : [ssList(_243719), app(_243571, cons(_242923, _243719)) = _242761]]]]]]]]], (340 ^ _232996) ^ [_244010] : [ssList(_244010), 343 ^ _232996 : [(344 ^ _232996) ^ [] : [singletonP(_244010), 348 ^ _232996 : [(349 ^ _232996) ^ [] : [-(ssItem(347 ^ [_244010]))], (351 ^ _232996) ^ [] : [-(cons(347 ^ [_244010], nil) = _244010)]]], (353 ^ _232996) ^ [] : [-(singletonP(_244010)), 354 ^ _232996 : [(355 ^ _232996) ^ [_244459] : [ssItem(_244459), cons(_244459, nil) = _244010]]]]], (363 ^ _232996) ^ [_244715] : [ssList(_244715), 366 ^ _232996 : [(367 ^ _232996) ^ [_244864] : [ssList(_244864), 370 ^ _232996 : [(371 ^ _232996) ^ [] : [frontsegP(_244715, _244864), 375 ^ _232996 : [(376 ^ _232996) ^ [] : [-(ssList(374 ^ [_244715, _244864]))], (378 ^ _232996) ^ [] : [-(app(_244864, 374 ^ [_244715, _244864]) = _244715)]]], (380 ^ _232996) ^ [] : [-(frontsegP(_244715, _244864)), 381 ^ _232996 : [(382 ^ _232996) ^ [_245339] : [ssList(_245339), app(_244864, _245339) = _244715]]]]]]], (390 ^ _232996) ^ [_245611] : [ssList(_245611), 393 ^ _232996 : [(394 ^ _232996) ^ [_245760] : [ssList(_245760), 397 ^ _232996 : [(398 ^ _232996) ^ [] : [rearsegP(_245611, _245760), 402 ^ _232996 : [(403 ^ _232996) ^ [] : [-(ssList(401 ^ [_245611, _245760]))], (405 ^ _232996) ^ [] : [-(app(401 ^ [_245611, _245760], _245760) = _245611)]]], (407 ^ _232996) ^ [] : [-(rearsegP(_245611, _245760)), 408 ^ _232996 : [(409 ^ _232996) ^ [_246235] : [ssList(_246235), app(_246235, _245760) = _245611]]]]]]], (417 ^ _232996) ^ [_246507] : [ssList(_246507), 420 ^ _232996 : [(421 ^ _232996) ^ [_246669] : [ssList(_246669), 424 ^ _232996 : [(425 ^ _232996) ^ [] : [segmentP(_246507, _246669), 429 ^ _232996 : [(430 ^ _232996) ^ [] : [-(ssList(428 ^ [_246507, _246669]))], (433 ^ _232996) ^ [] : [-(ssList(431 ^ [_246507, _246669]))], (435 ^ _232996) ^ [] : [-(app(app(428 ^ [_246507, _246669], _246669), 431 ^ [_246507, _246669]) = _246507)]]], (437 ^ _232996) ^ [] : [-(segmentP(_246507, _246669)), 438 ^ _232996 : [(439 ^ _232996) ^ [_247317] : [ssList(_247317), 442 ^ _232996 : [(443 ^ _232996) ^ [_247465] : [ssList(_247465), app(app(_247317, _246669), _247465) = _246507]]]]]]]]], (451 ^ _232996) ^ [_247756] : [ssList(_247756), 454 ^ _232996 : [(489 ^ _232996) ^ [] : [491 ^ _232996 : [(492 ^ _232996) ^ [] : [-(ssItem(490 ^ [_247756]))], (495 ^ _232996) ^ [] : [-(ssItem(493 ^ [_247756]))], (498 ^ _232996) ^ [] : [-(ssList(496 ^ [_247756]))], (501 ^ _232996) ^ [] : [-(ssList(499 ^ [_247756]))], (504 ^ _232996) ^ [] : [-(ssList(502 ^ [_247756]))], (506 ^ _232996) ^ [] : [-(app(app(496 ^ [_247756], cons(490 ^ [_247756], 499 ^ [_247756])), cons(493 ^ [_247756], 502 ^ [_247756])) = _247756)], (508 ^ _232996) ^ [] : [-(leq(490 ^ [_247756], 493 ^ [_247756]))], (510 ^ _232996) ^ [] : [-(leq(493 ^ [_247756], 490 ^ [_247756]))]], -(cyclefreeP(_247756))], (455 ^ _232996) ^ [] : [cyclefreeP(_247756), 458 ^ _232996 : [(459 ^ _232996) ^ [_248060] : [ssItem(_248060), 462 ^ _232996 : [(463 ^ _232996) ^ [_248252] : [ssItem(_248252), 466 ^ _232996 : [(467 ^ _232996) ^ [_248440] : [ssList(_248440), 470 ^ _232996 : [(471 ^ _232996) ^ [_248624] : [ssList(_248624), 474 ^ _232996 : [(475 ^ _232996) ^ [_248804] : [ssList(_248804), app(app(_248440, cons(_248060, _248624)), cons(_248252, _248804)) = _247756, leq(_248060, _248252), leq(_248252, _248060)]]]]]]]]]]]]], (514 ^ _232996) ^ [_250542] : [ssList(_250542), 517 ^ _232996 : [(552 ^ _232996) ^ [] : [554 ^ _232996 : [(555 ^ _232996) ^ [] : [-(ssItem(553 ^ [_250542]))], (558 ^ _232996) ^ [] : [-(ssItem(556 ^ [_250542]))], (561 ^ _232996) ^ [] : [-(ssList(559 ^ [_250542]))], (564 ^ _232996) ^ [] : [-(ssList(562 ^ [_250542]))], (567 ^ _232996) ^ [] : [-(ssList(565 ^ [_250542]))], (569 ^ _232996) ^ [] : [-(app(app(559 ^ [_250542], cons(553 ^ [_250542], 562 ^ [_250542])), cons(556 ^ [_250542], 565 ^ [_250542])) = _250542)], (571 ^ _232996) ^ [] : [leq(553 ^ [_250542], 556 ^ [_250542])], (573 ^ _232996) ^ [] : [leq(556 ^ [_250542], 553 ^ [_250542])]], -(totalorderP(_250542))], (518 ^ _232996) ^ [] : [totalorderP(_250542), 521 ^ _232996 : [(522 ^ _232996) ^ [_250844] : [ssItem(_250844), 525 ^ _232996 : [(526 ^ _232996) ^ [_251034] : [ssItem(_251034), 529 ^ _232996 : [(530 ^ _232996) ^ [_251220] : [ssList(_251220), 533 ^ _232996 : [(534 ^ _232996) ^ [_251402] : [ssList(_251402), 537 ^ _232996 : [(538 ^ _232996) ^ [_251580] : [ssList(_251580), app(app(_251220, cons(_250844, _251402)), cons(_251034, _251580)) = _250542, -(leq(_250844, _251034)), -(leq(_251034, _250844))]]]]]]]]]]]]], (577 ^ _232996) ^ [_253306] : [ssList(_253306), 580 ^ _232996 : [(615 ^ _232996) ^ [] : [617 ^ _232996 : [(618 ^ _232996) ^ [] : [-(ssItem(616 ^ [_253306]))], (621 ^ _232996) ^ [] : [-(ssItem(619 ^ [_253306]))], (624 ^ _232996) ^ [] : [-(ssList(622 ^ [_253306]))], (627 ^ _232996) ^ [] : [-(ssList(625 ^ [_253306]))], (630 ^ _232996) ^ [] : [-(ssList(628 ^ [_253306]))], (632 ^ _232996) ^ [] : [-(app(app(622 ^ [_253306], cons(616 ^ [_253306], 625 ^ [_253306])), cons(619 ^ [_253306], 628 ^ [_253306])) = _253306)], (634 ^ _232996) ^ [] : [lt(616 ^ [_253306], 619 ^ [_253306])], (636 ^ _232996) ^ [] : [lt(619 ^ [_253306], 616 ^ [_253306])]], -(strictorderP(_253306))], (581 ^ _232996) ^ [] : [strictorderP(_253306), 584 ^ _232996 : [(585 ^ _232996) ^ [_253608] : [ssItem(_253608), 588 ^ _232996 : [(589 ^ _232996) ^ [_253798] : [ssItem(_253798), 592 ^ _232996 : [(593 ^ _232996) ^ [_253984] : [ssList(_253984), 596 ^ _232996 : [(597 ^ _232996) ^ [_254166] : [ssList(_254166), 600 ^ _232996 : [(601 ^ _232996) ^ [_254344] : [ssList(_254344), app(app(_253984, cons(_253608, _254166)), cons(_253798, _254344)) = _253306, -(lt(_253608, _253798)), -(lt(_253798, _253608))]]]]]]]]]]]]], (640 ^ _232996) ^ [_256070] : [ssList(_256070), 643 ^ _232996 : [(674 ^ _232996) ^ [] : [676 ^ _232996 : [(677 ^ _232996) ^ [] : [-(ssItem(675 ^ [_256070]))], (680 ^ _232996) ^ [] : [-(ssItem(678 ^ [_256070]))], (683 ^ _232996) ^ [] : [-(ssList(681 ^ [_256070]))], (686 ^ _232996) ^ [] : [-(ssList(684 ^ [_256070]))], (689 ^ _232996) ^ [] : [-(ssList(687 ^ [_256070]))], (691 ^ _232996) ^ [] : [-(app(app(681 ^ [_256070], cons(675 ^ [_256070], 684 ^ [_256070])), cons(678 ^ [_256070], 687 ^ [_256070])) = _256070)], (693 ^ _232996) ^ [] : [leq(675 ^ [_256070], 678 ^ [_256070])]], -(totalorderedP(_256070))], (644 ^ _232996) ^ [] : [totalorderedP(_256070), 647 ^ _232996 : [(648 ^ _232996) ^ [_256366] : [ssItem(_256366), 651 ^ _232996 : [(652 ^ _232996) ^ [_256550] : [ssItem(_256550), 655 ^ _232996 : [(656 ^ _232996) ^ [_256730] : [ssList(_256730), 659 ^ _232996 : [(660 ^ _232996) ^ [_256906] : [ssList(_256906), 663 ^ _232996 : [(664 ^ _232996) ^ [_257078] : [ssList(_257078), app(app(_256730, cons(_256366, _256906)), cons(_256550, _257078)) = _256070, -(leq(_256366, _256550))]]]]]]]]]]]]], (697 ^ _232996) ^ [_258558] : [ssList(_258558), 700 ^ _232996 : [(731 ^ _232996) ^ [] : [733 ^ _232996 : [(734 ^ _232996) ^ [] : [-(ssItem(732 ^ [_258558]))], (737 ^ _232996) ^ [] : [-(ssItem(735 ^ [_258558]))], (740 ^ _232996) ^ [] : [-(ssList(738 ^ [_258558]))], (743 ^ _232996) ^ [] : [-(ssList(741 ^ [_258558]))], (746 ^ _232996) ^ [] : [-(ssList(744 ^ [_258558]))], (748 ^ _232996) ^ [] : [-(app(app(738 ^ [_258558], cons(732 ^ [_258558], 741 ^ [_258558])), cons(735 ^ [_258558], 744 ^ [_258558])) = _258558)], (750 ^ _232996) ^ [] : [lt(732 ^ [_258558], 735 ^ [_258558])]], -(strictorderedP(_258558))], (701 ^ _232996) ^ [] : [strictorderedP(_258558), 704 ^ _232996 : [(705 ^ _232996) ^ [_258854] : [ssItem(_258854), 708 ^ _232996 : [(709 ^ _232996) ^ [_259038] : [ssItem(_259038), 712 ^ _232996 : [(713 ^ _232996) ^ [_259218] : [ssList(_259218), 716 ^ _232996 : [(717 ^ _232996) ^ [_259394] : [ssList(_259394), 720 ^ _232996 : [(721 ^ _232996) ^ [_259566] : [ssList(_259566), app(app(_259218, cons(_258854, _259394)), cons(_259038, _259566)) = _258558, -(lt(_258854, _259038))]]]]]]]]]]]]], (754 ^ _232996) ^ [_261046] : [ssList(_261046), 757 ^ _232996 : [(788 ^ _232996) ^ [] : [790 ^ _232996 : [(791 ^ _232996) ^ [] : [-(ssItem(789 ^ [_261046]))], (794 ^ _232996) ^ [] : [-(ssItem(792 ^ [_261046]))], (797 ^ _232996) ^ [] : [-(ssList(795 ^ [_261046]))], (800 ^ _232996) ^ [] : [-(ssList(798 ^ [_261046]))], (803 ^ _232996) ^ [] : [-(ssList(801 ^ [_261046]))], (805 ^ _232996) ^ [] : [-(app(app(795 ^ [_261046], cons(789 ^ [_261046], 798 ^ [_261046])), cons(792 ^ [_261046], 801 ^ [_261046])) = _261046)], (807 ^ _232996) ^ [] : [-(789 ^ [_261046] = 792 ^ [_261046])]], -(duplicatefreeP(_261046))], (758 ^ _232996) ^ [] : [duplicatefreeP(_261046), 761 ^ _232996 : [(762 ^ _232996) ^ [_261344] : [ssItem(_261344), 765 ^ _232996 : [(766 ^ _232996) ^ [_261530] : [ssItem(_261530), 769 ^ _232996 : [(770 ^ _232996) ^ [_261712] : [ssList(_261712), 773 ^ _232996 : [(774 ^ _232996) ^ [_261890] : [ssList(_261890), 777 ^ _232996 : [(778 ^ _232996) ^ [_262064] : [ssList(_262064), app(app(_261712, cons(_261344, _261890)), cons(_261530, _262064)) = _261046, _261344 = _261530]]]]]]]]]]]]], (811 ^ _232996) ^ [_263556] : [ssList(_263556), 814 ^ _232996 : [(841 ^ _232996) ^ [] : [843 ^ _232996 : [(844 ^ _232996) ^ [] : [-(ssItem(842 ^ [_263556]))], (847 ^ _232996) ^ [] : [-(ssItem(845 ^ [_263556]))], (850 ^ _232996) ^ [] : [-(ssList(848 ^ [_263556]))], (853 ^ _232996) ^ [] : [-(ssList(851 ^ [_263556]))], (855 ^ _232996) ^ [] : [-(app(848 ^ [_263556], cons(842 ^ [_263556], cons(845 ^ [_263556], 851 ^ [_263556]))) = _263556)], (857 ^ _232996) ^ [] : [842 ^ [_263556] = 845 ^ [_263556]]], -(equalelemsP(_263556))], (815 ^ _232996) ^ [] : [equalelemsP(_263556), 818 ^ _232996 : [(819 ^ _232996) ^ [_263839] : [ssItem(_263839), 822 ^ _232996 : [(823 ^ _232996) ^ [_264010] : [ssItem(_264010), 826 ^ _232996 : [(827 ^ _232996) ^ [_264177] : [ssList(_264177), 830 ^ _232996 : [(831 ^ _232996) ^ [_264340] : [ssList(_264340), app(_264177, cons(_263839, cons(_264010, _264340))) = _263556, -(_263839 = _264010)]]]]]]]]]]], (861 ^ _232996) ^ [_265573] : [ssList(_265573), 864 ^ _232996 : [(865 ^ _232996) ^ [_265711] : [ssList(_265711), 868 ^ _232996 : [(869 ^ _232996) ^ [] : [neq(_265573, _265711), _265573 = _265711], (875 ^ _232996) ^ [] : [-(_265573 = _265711), -(neq(_265573, _265711))]]]]], (881 ^ _232996) ^ [_266164] : [ssList(_266164), 884 ^ _232996 : [(885 ^ _232996) ^ [_266296] : [ssItem(_266296), -(ssList(cons(_266296, _266164)))]]], (891 ^ _232996) ^ [] : [-(ssList(nil))], (893 ^ _232996) ^ [_266554] : [ssList(_266554), 896 ^ _232996 : [(897 ^ _232996) ^ [_266689] : [ssItem(_266689), cons(_266689, _266554) = _266554]]], (903 ^ _232996) ^ [_266897] : [ssList(_266897), 906 ^ _232996 : [(907 ^ _232996) ^ [_267065] : [ssList(_267065), 910 ^ _232996 : [(911 ^ _232996) ^ [_267229] : [ssItem(_267229), 914 ^ _232996 : [(915 ^ _232996) ^ [_267389] : [ssItem(_267389), cons(_267229, _266897) = cons(_267389, _267065), 922 ^ _232996 : [(923 ^ _232996) ^ [] : [-(_267229 = _267389)], (925 ^ _232996) ^ [] : [-(_267065 = _266897)]]]]]]]]], (927 ^ _232996) ^ [_267804] : [ssList(_267804), -(nil = _267804), 935 ^ _232996 : [(936 ^ _232996) ^ [] : [-(ssList(934 ^ [_267804]))], (939 ^ _232996) ^ [] : [-(ssItem(937 ^ [_267804]))], (941 ^ _232996) ^ [] : [-(cons(937 ^ [_267804], 934 ^ [_267804]) = _267804)]]], (943 ^ _232996) ^ [_268368] : [ssList(_268368), 946 ^ _232996 : [(947 ^ _232996) ^ [_268503] : [ssItem(_268503), nil = cons(_268503, _268368)]]], (953 ^ _232996) ^ [_268711] : [ssList(_268711), -(nil = _268711), -(ssItem(hd(_268711)))], (963 ^ _232996) ^ [_268989] : [ssList(_268989), 966 ^ _232996 : [(967 ^ _232996) ^ [_269124] : [ssItem(_269124), -(hd(cons(_269124, _268989)) = _269124)]]], (973 ^ _232996) ^ [_269335] : [ssList(_269335), -(nil = _269335), -(ssList(tl(_269335)))], (983 ^ _232996) ^ [_269613] : [ssList(_269613), 986 ^ _232996 : [(987 ^ _232996) ^ [_269748] : [ssItem(_269748), -(tl(cons(_269748, _269613)) = _269613)]]], (993 ^ _232996) ^ [_269959] : [ssList(_269959), 996 ^ _232996 : [(997 ^ _232996) ^ [_270091] : [ssList(_270091), -(ssList(app(_269959, _270091)))]]], (1003 ^ _232996) ^ [_270296] : [ssList(_270296), 1006 ^ _232996 : [(1007 ^ _232996) ^ [_270448] : [ssList(_270448), 1010 ^ _232996 : [(1011 ^ _232996) ^ [_270596] : [ssItem(_270596), -(cons(_270596, app(_270448, _270296)) = app(cons(_270596, _270448), _270296))]]]]], (1017 ^ _232996) ^ [_270834] : [ssList(_270834), -(app(nil, _270834) = _270834)], (1023 ^ _232996) ^ [_271028] : [ssItem(_271028), 1026 ^ _232996 : [(1027 ^ _232996) ^ [_271170] : [ssItem(_271170), -(_271028 = _271170), leq(_271028, _271170), leq(_271170, _271028)]]], (1041 ^ _232996) ^ [_271549] : [ssItem(_271549), 1044 ^ _232996 : [(1045 ^ _232996) ^ [_271701] : [ssItem(_271701), 1048 ^ _232996 : [(1049 ^ _232996) ^ [_271849] : [ssItem(_271849), -(leq(_271549, _271849)), leq(_271549, _271701), leq(_271701, _271849)]]]]], (1063 ^ _232996) ^ [_272249] : [ssItem(_272249), -(leq(_272249, _272249))], (1069 ^ _232996) ^ [_272437] : [ssItem(_272437), 1072 ^ _232996 : [(1073 ^ _232996) ^ [_272573] : [ssItem(_272573), 1076 ^ _232996 : [(1077 ^ _232996) ^ [] : [geq(_272437, _272573), -(leq(_272573, _272437))], (1083 ^ _232996) ^ [] : [leq(_272573, _272437), -(geq(_272437, _272573))]]]]], (1089 ^ _232996) ^ [_273024] : [ssItem(_273024), 1092 ^ _232996 : [(1093 ^ _232996) ^ [_273162] : [ssItem(_273162), lt(_273024, _273162), lt(_273162, _273024)]]], (1103 ^ _232996) ^ [_273453] : [ssItem(_273453), 1106 ^ _232996 : [(1107 ^ _232996) ^ [_273605] : [ssItem(_273605), 1110 ^ _232996 : [(1111 ^ _232996) ^ [_273753] : [ssItem(_273753), -(lt(_273453, _273753)), lt(_273453, _273605), lt(_273605, _273753)]]]]], (1125 ^ _232996) ^ [_274153] : [ssItem(_274153), 1128 ^ _232996 : [(1129 ^ _232996) ^ [_274289] : [ssItem(_274289), 1132 ^ _232996 : [(1133 ^ _232996) ^ [] : [gt(_274153, _274289), -(lt(_274289, _274153))], (1139 ^ _232996) ^ [] : [lt(_274289, _274153), -(gt(_274153, _274289))]]]]], (1145 ^ _232996) ^ [_274740] : [ssItem(_274740), 1148 ^ _232996 : [(1149 ^ _232996) ^ [_274895] : [ssList(_274895), 1152 ^ _232996 : [(1153 ^ _232996) ^ [_275046] : [ssList(_275046), 1156 ^ _232996 : [(1167 ^ _232996) ^ [] : [1168 ^ _232996 : [(1169 ^ _232996) ^ [] : [memberP(_274895, _274740)], (1171 ^ _232996) ^ [] : [memberP(_275046, _274740)]], -(memberP(app(_274895, _275046), _274740))], (1157 ^ _232996) ^ [] : [memberP(app(_274895, _275046), _274740), -(memberP(_274895, _274740)), -(memberP(_275046, _274740))]]]]]]], (1175 ^ _232996) ^ [_275693] : [ssItem(_275693), 1178 ^ _232996 : [(1179 ^ _232996) ^ [_275848] : [ssItem(_275848), 1182 ^ _232996 : [(1183 ^ _232996) ^ [_275999] : [ssList(_275999), 1186 ^ _232996 : [(1197 ^ _232996) ^ [] : [1198 ^ _232996 : [(1199 ^ _232996) ^ [] : [_275693 = _275848], (1201 ^ _232996) ^ [] : [memberP(_275999, _275693)]], -(memberP(cons(_275848, _275999), _275693))], (1187 ^ _232996) ^ [] : [memberP(cons(_275848, _275999), _275693), -(_275693 = _275848), -(memberP(_275999, _275693))]]]]]]], (1205 ^ _232996) ^ [_276646] : [ssItem(_276646), memberP(nil, _276646)], (1211 ^ _232996) ^ [] : [singletonP(nil)], (1213 ^ _232996) ^ [_276887] : [ssList(_276887), 1216 ^ _232996 : [(1217 ^ _232996) ^ [_277039] : [ssList(_277039), 1220 ^ _232996 : [(1221 ^ _232996) ^ [_277187] : [ssList(_277187), -(frontsegP(_276887, _277187)), frontsegP(_276887, _277039), frontsegP(_277039, _277187)]]]]], (1235 ^ _232996) ^ [_277587] : [ssList(_277587), 1238 ^ _232996 : [(1239 ^ _232996) ^ [_277729] : [ssList(_277729), -(_277587 = _277729), frontsegP(_277587, _277729), frontsegP(_277729, _277587)]]], (1253 ^ _232996) ^ [_278108] : [ssList(_278108), -(frontsegP(_278108, _278108))], (1259 ^ _232996) ^ [_278296] : [ssList(_278296), 1262 ^ _232996 : [(1263 ^ _232996) ^ [_278445] : [ssList(_278445), 1266 ^ _232996 : [(1267 ^ _232996) ^ [_278590] : [ssList(_278590), frontsegP(_278296, _278445), -(frontsegP(app(_278296, _278590), _278445))]]]]], (1277 ^ _232996) ^ [_278903] : [ssItem(_278903), 1280 ^ _232996 : [(1281 ^ _232996) ^ [_279071] : [ssItem(_279071), 1284 ^ _232996 : [(1285 ^ _232996) ^ [_279235] : [ssList(_279235), 1288 ^ _232996 : [(1289 ^ _232996) ^ [_279395] : [ssList(_279395), 1292 ^ _232996 : [(1293 ^ _232996) ^ [] : [frontsegP(cons(_278903, _279235), cons(_279071, _279395)), 1296 ^ _232996 : [(1297 ^ _232996) ^ [] : [-(_278903 = _279071)], (1299 ^ _232996) ^ [] : [-(frontsegP(_279235, _279395))]]], (1301 ^ _232996) ^ [] : [-(frontsegP(cons(_278903, _279235), cons(_279071, _279395))), _278903 = _279071, frontsegP(_279235, _279395)]]]]]]]]], (1311 ^ _232996) ^ [_280080] : [ssList(_280080), -(frontsegP(_280080, nil))], (1317 ^ _232996) ^ [_280268] : [ssList(_280268), 1320 ^ _232996 : [(1321 ^ _232996) ^ [] : [frontsegP(nil, _280268), -(nil = _280268)], (1327 ^ _232996) ^ [] : [nil = _280268, -(frontsegP(nil, _280268))]]], (1333 ^ _232996) ^ [_280696] : [ssList(_280696), 1336 ^ _232996 : [(1337 ^ _232996) ^ [_280848] : [ssList(_280848), 1340 ^ _232996 : [(1341 ^ _232996) ^ [_280996] : [ssList(_280996), -(rearsegP(_280696, _280996)), rearsegP(_280696, _280848), rearsegP(_280848, _280996)]]]]], (1355 ^ _232996) ^ [_281396] : [ssList(_281396), 1358 ^ _232996 : [(1359 ^ _232996) ^ [_281538] : [ssList(_281538), -(_281396 = _281538), rearsegP(_281396, _281538), rearsegP(_281538, _281396)]]], (1373 ^ _232996) ^ [_281917] : [ssList(_281917), -(rearsegP(_281917, _281917))], (1379 ^ _232996) ^ [_282105] : [ssList(_282105), 1382 ^ _232996 : [(1383 ^ _232996) ^ [_282254] : [ssList(_282254), 1386 ^ _232996 : [(1387 ^ _232996) ^ [_282399] : [ssList(_282399), rearsegP(_282105, _282254), -(rearsegP(app(_282399, _282105), _282254))]]]]], (1397 ^ _232996) ^ [_282712] : [ssList(_282712), -(rearsegP(_282712, nil))], (1403 ^ _232996) ^ [_282900] : [ssList(_282900), 1406 ^ _232996 : [(1407 ^ _232996) ^ [] : [rearsegP(nil, _282900), -(nil = _282900)], (1413 ^ _232996) ^ [] : [nil = _282900, -(rearsegP(nil, _282900))]]], (1419 ^ _232996) ^ [_283328] : [ssList(_283328), 1422 ^ _232996 : [(1423 ^ _232996) ^ [_283480] : [ssList(_283480), 1426 ^ _232996 : [(1427 ^ _232996) ^ [_283628] : [ssList(_283628), -(segmentP(_283328, _283628)), segmentP(_283328, _283480), segmentP(_283480, _283628)]]]]], (1441 ^ _232996) ^ [_284028] : [ssList(_284028), 1444 ^ _232996 : [(1445 ^ _232996) ^ [_284170] : [ssList(_284170), -(_284028 = _284170), segmentP(_284028, _284170), segmentP(_284170, _284028)]]], (1459 ^ _232996) ^ [_284549] : [ssList(_284549), -(segmentP(_284549, _284549))], (1465 ^ _232996) ^ [_284737] : [ssList(_284737), 1468 ^ _232996 : [(1469 ^ _232996) ^ [_284899] : [ssList(_284899), 1472 ^ _232996 : [(1473 ^ _232996) ^ [_285057] : [ssList(_285057), 1476 ^ _232996 : [(1477 ^ _232996) ^ [_285211] : [ssList(_285211), segmentP(_284737, _284899), -(segmentP(app(app(_285057, _284737), _285211), _284899))]]]]]]], (1487 ^ _232996) ^ [_285547] : [ssList(_285547), -(segmentP(_285547, nil))], (1493 ^ _232996) ^ [_285735] : [ssList(_285735), 1496 ^ _232996 : [(1497 ^ _232996) ^ [] : [segmentP(nil, _285735), -(nil = _285735)], (1503 ^ _232996) ^ [] : [nil = _285735, -(segmentP(nil, _285735))]]], (1509 ^ _232996) ^ [_286163] : [ssItem(_286163), -(cyclefreeP(cons(_286163, nil)))], (1515 ^ _232996) ^ [] : [-(cyclefreeP(nil))], (1517 ^ _232996) ^ [_286408] : [ssItem(_286408), -(totalorderP(cons(_286408, nil)))], (1523 ^ _232996) ^ [] : [-(totalorderP(nil))], (1525 ^ _232996) ^ [_286653] : [ssItem(_286653), -(strictorderP(cons(_286653, nil)))], (1531 ^ _232996) ^ [] : [-(strictorderP(nil))], (1533 ^ _232996) ^ [_286898] : [ssItem(_286898), -(totalorderedP(cons(_286898, nil)))], (1539 ^ _232996) ^ [] : [-(totalorderedP(nil))], (1541 ^ _232996) ^ [_287143] : [ssItem(_287143), 1544 ^ _232996 : [(1545 ^ _232996) ^ [_287302] : [ssList(_287302), 1548 ^ _232996 : [(1549 ^ _232996) ^ [] : [totalorderedP(cons(_287143, _287302)), -(nil = _287302), 1556 ^ _232996 : [(1557 ^ _232996) ^ [] : [nil = _287302], (1559 ^ _232996) ^ [] : [-(totalorderedP(_287302))], (1561 ^ _232996) ^ [] : [-(leq(_287143, hd(_287302)))]]], (1563 ^ _232996) ^ [] : [-(totalorderedP(cons(_287143, _287302))), 1564 ^ _232996 : [(1565 ^ _232996) ^ [] : [nil = _287302], (1567 ^ _232996) ^ [] : [-(nil = _287302), totalorderedP(_287302), leq(_287143, hd(_287302))]]]]]]], (1579 ^ _232996) ^ [_288237] : [ssItem(_288237), -(strictorderedP(cons(_288237, nil)))], (1585 ^ _232996) ^ [] : [-(strictorderedP(nil))], (1587 ^ _232996) ^ [_288482] : [ssItem(_288482), 1590 ^ _232996 : [(1591 ^ _232996) ^ [_288641] : [ssList(_288641), 1594 ^ _232996 : [(1595 ^ _232996) ^ [] : [strictorderedP(cons(_288482, _288641)), -(nil = _288641), 1602 ^ _232996 : [(1603 ^ _232996) ^ [] : [nil = _288641], (1605 ^ _232996) ^ [] : [-(strictorderedP(_288641))], (1607 ^ _232996) ^ [] : [-(lt(_288482, hd(_288641)))]]], (1609 ^ _232996) ^ [] : [-(strictorderedP(cons(_288482, _288641))), 1610 ^ _232996 : [(1611 ^ _232996) ^ [] : [nil = _288641], (1613 ^ _232996) ^ [] : [-(nil = _288641), strictorderedP(_288641), lt(_288482, hd(_288641))]]]]]]], (1625 ^ _232996) ^ [_289576] : [ssItem(_289576), -(duplicatefreeP(cons(_289576, nil)))], (1631 ^ _232996) ^ [] : [-(duplicatefreeP(nil))], (1633 ^ _232996) ^ [_289821] : [ssItem(_289821), -(equalelemsP(cons(_289821, nil)))], (1639 ^ _232996) ^ [] : [-(equalelemsP(nil))], (1641 ^ _232996) ^ [_290066] : [ssList(_290066), -(nil = _290066), 1649 ^ _232996 : [(1650 ^ _232996) ^ [] : [-(ssItem(1648 ^ [_290066]))], (1652 ^ _232996) ^ [] : [-(hd(_290066) = 1648 ^ [_290066])]]], (1654 ^ _232996) ^ [_290480] : [ssList(_290480), -(nil = _290480), 1662 ^ _232996 : [(1663 ^ _232996) ^ [] : [-(ssList(1661 ^ [_290480]))], (1665 ^ _232996) ^ [] : [-(tl(_290480) = 1661 ^ [_290480])]]], (1667 ^ _232996) ^ [_290894] : [ssList(_290894), 1670 ^ _232996 : [(1671 ^ _232996) ^ [_291060] : [ssList(_291060), -(_291060 = _290894), -(nil = _291060), -(nil = _290894), hd(_291060) = hd(_290894), tl(_291060) = tl(_290894)]]], (1693 ^ _232996) ^ [_291639] : [ssList(_291639), -(nil = _291639), -(cons(hd(_291639), tl(_291639)) = _291639)], (1703 ^ _232996) ^ [_291929] : [ssList(_291929), 1706 ^ _232996 : [(1707 ^ _232996) ^ [_292081] : [ssList(_292081), 1710 ^ _232996 : [(1711 ^ _232996) ^ [_292229] : [ssList(_292229), app(_292229, _292081) = app(_291929, _292081), -(_292229 = _291929)]]]]], (1721 ^ _232996) ^ [_292548] : [ssList(_292548), 1724 ^ _232996 : [(1725 ^ _232996) ^ [_292700] : [ssList(_292700), 1728 ^ _232996 : [(1729 ^ _232996) ^ [_292848] : [ssList(_292848), app(_292700, _292848) = app(_292700, _292548), -(_292848 = _292548)]]]]], (1739 ^ _232996) ^ [_293167] : [ssList(_293167), 1742 ^ _232996 : [(1743 ^ _232996) ^ [_293306] : [ssItem(_293306), -(cons(_293306, _293167) = app(cons(_293306, nil), _293167))]]], (1749 ^ _232996) ^ [_293525] : [ssList(_293525), 1752 ^ _232996 : [(1753 ^ _232996) ^ [_293677] : [ssList(_293677), 1756 ^ _232996 : [(1757 ^ _232996) ^ [_293825] : [ssList(_293825), -(app(app(_293525, _293677), _293825) = app(_293525, app(_293677, _293825)))]]]]], (1763 ^ _232996) ^ [_294063] : [ssList(_294063), 1766 ^ _232996 : [(1767 ^ _232996) ^ [_294208] : [ssList(_294208), 1770 ^ _232996 : [(1771 ^ _232996) ^ [] : [nil = app(_294063, _294208), 1774 ^ _232996 : [(1775 ^ _232996) ^ [] : [-(nil = _294208)], (1777 ^ _232996) ^ [] : [-(nil = _294063)]]], (1779 ^ _232996) ^ [] : [-(nil = app(_294063, _294208)), nil = _294208, nil = _294063]]]]], (1789 ^ _232996) ^ [_294826] : [ssList(_294826), -(app(_294826, nil) = _294826)], (1795 ^ _232996) ^ [_295020] : [ssList(_295020), 1798 ^ _232996 : [(1799 ^ _232996) ^ [_295165] : [ssList(_295165), -(nil = _295020), -(hd(app(_295020, _295165)) = hd(_295020))]]], (1809 ^ _232996) ^ [_295472] : [ssList(_295472), 1812 ^ _232996 : [(1813 ^ _232996) ^ [_295620] : [ssList(_295620), -(nil = _295472), -(tl(app(_295472, _295620)) = app(tl(_295472), _295620))]]], (1823 ^ _232996) ^ [_295933] : [ssItem(_295933), 1826 ^ _232996 : [(1827 ^ _232996) ^ [_296075] : [ssItem(_296075), -(_295933 = _296075), geq(_295933, _296075), geq(_296075, _295933)]]], (1841 ^ _232996) ^ [_296454] : [ssItem(_296454), 1844 ^ _232996 : [(1845 ^ _232996) ^ [_296606] : [ssItem(_296606), 1848 ^ _232996 : [(1849 ^ _232996) ^ [_296754] : [ssItem(_296754), -(geq(_296454, _296754)), geq(_296454, _296606), geq(_296606, _296754)]]]]], (1863 ^ _232996) ^ [_297154] : [ssItem(_297154), -(geq(_297154, _297154))], (1869 ^ _232996) ^ [_297342] : [ssItem(_297342), lt(_297342, _297342)], (1875 ^ _232996) ^ [_297531] : [ssItem(_297531), 1878 ^ _232996 : [(1879 ^ _232996) ^ [_297683] : [ssItem(_297683), 1882 ^ _232996 : [(1883 ^ _232996) ^ [_297831] : [ssItem(_297831), -(lt(_297531, _297831)), leq(_297531, _297683), lt(_297683, _297831)]]]]], (1897 ^ _232996) ^ [_298231] : [ssItem(_298231), 1900 ^ _232996 : [(1901 ^ _232996) ^ [_298373] : [ssItem(_298373), leq(_298231, _298373), -(_298231 = _298373), -(lt(_298231, _298373))]]], (1915 ^ _232996) ^ [_298753] : [ssItem(_298753), 1918 ^ _232996 : [(1919 ^ _232996) ^ [_298897] : [ssItem(_298897), 1922 ^ _232996 : [(1923 ^ _232996) ^ [] : [lt(_298753, _298897), 1926 ^ _232996 : [(1927 ^ _232996) ^ [] : [_298753 = _298897], (1929 ^ _232996) ^ [] : [-(leq(_298753, _298897))]]], (1931 ^ _232996) ^ [] : [-(lt(_298753, _298897)), -(_298753 = _298897), leq(_298753, _298897)]]]]], (1941 ^ _232996) ^ [_299508] : [ssItem(_299508), 1944 ^ _232996 : [(1945 ^ _232996) ^ [_299646] : [ssItem(_299646), gt(_299508, _299646), gt(_299646, _299508)]]], (1955 ^ _232996) ^ [_299917] : [ssItem(_299917), 1958 ^ _232996 : [(1959 ^ _232996) ^ [_300069] : [ssItem(_300069), 1962 ^ _232996 : [(1963 ^ _232996) ^ [_300217] : [ssItem(_300217), -(gt(_299917, _300217)), gt(_299917, _300069), gt(_300069, _300217)]]]]]], input).
% 14.17/14.67 ncf('1',plain,[memberP(1979 ^ [], 1994 ^ []), memberP(1976 ^ [], 1994 ^ [])],start(2004 ^ 0)).
% 14.17/14.67 ncf('1.1',plain,[-(memberP(1979 ^ [], 1994 ^ [])), memberP(1976 ^ [], 1994 ^ []), 1976 ^ [] = 1979 ^ [], 1994 ^ [] = 1994 ^ []],extension(232 ^ 1,bind([[_240274, _240276, _240278, _240280], [1994 ^ [], 1994 ^ [], 1979 ^ [], 1976 ^ []]]))).
% 14.17/14.67 ncf('1.1.1',plain,[-(memberP(1976 ^ [], 1994 ^ [])), -(memberP(1979 ^ [], 1994 ^ []))],extension(1998 ^ 2)).
% 14.17/14.67 ncf('1.1.1.1',plain,[memberP(1979 ^ [], 1994 ^ [])],reduction('1')).
% 14.17/14.67 ncf('1.1.2',plain,[-(1976 ^ [] = 1979 ^ []), 1976 ^ [] = 1982 ^ [], 1982 ^ [] = 1979 ^ []],extension(10 ^ 2,bind([[_233451, _233453, _233455], [1979 ^ [], 1982 ^ [], 1976 ^ []]]))).
% 14.17/14.67 ncf('1.1.2.1',plain,[-(1976 ^ [] = 1982 ^ [])],extension(1991 ^ 3)).
% 14.17/14.67 ncf('1.1.2.2',plain,[-(1982 ^ [] = 1979 ^ []), 1979 ^ [] = 1982 ^ []],extension(4 ^ 3,bind([[_233247, _233249], [1982 ^ [], 1979 ^ []]]))).
% 14.17/14.67 ncf('1.1.2.2.1',plain,[-(1979 ^ [] = 1982 ^ []), 1979 ^ [] = 1985 ^ [], 1985 ^ [] = 1982 ^ []],extension(10 ^ 4,bind([[_233451, _233453, _233455], [1982 ^ [], 1985 ^ [], 1979 ^ []]]))).
% 14.17/14.67 ncf('1.1.2.2.1.1',plain,[-(1979 ^ [] = 1985 ^ [])],extension(1989 ^ 5)).
% 14.17/14.67 ncf('1.1.2.2.1.2',plain,[-(1985 ^ [] = 1982 ^ [])],extension(1993 ^ 5)).
% 14.17/14.67 ncf('1.1.3',plain,[-(1994 ^ [] = 1994 ^ [])],extension(2 ^ 2,bind([[_233140], [1994 ^ []]]))).
% 14.17/14.67 ncf('1.2',plain,[-(memberP(1976 ^ [], 1994 ^ [])), memberP(1979 ^ [], 1994 ^ []), 1979 ^ [] = 1976 ^ [], 1994 ^ [] = 1994 ^ []],extension(232 ^ 1,bind([[_240274, _240276, _240278, _240280], [1994 ^ [], 1994 ^ [], 1976 ^ [], 1979 ^ []]]))).
% 14.17/14.67 ncf('1.2.1',plain,[-(memberP(1979 ^ [], 1994 ^ [])), -(memberP(1976 ^ [], 1994 ^ []))],extension(1998 ^ 2)).
% 14.17/14.67 ncf('1.2.1.1',plain,[memberP(1976 ^ [], 1994 ^ [])],reduction('1')).
% 14.17/14.67 ncf('1.2.2',plain,[-(1979 ^ [] = 1976 ^ []), 1979 ^ [] = 1985 ^ [], 1985 ^ [] = 1976 ^ []],extension(10 ^ 2,bind([[_233451, _233453, _233455], [1976 ^ [], 1985 ^ [], 1979 ^ []]]))).
% 14.17/14.67 ncf('1.2.2.1',plain,[-(1979 ^ [] = 1985 ^ [])],extension(1989 ^ 3)).
% 14.17/14.67 ncf('1.2.2.2',plain,[-(1985 ^ [] = 1976 ^ []), 1985 ^ [] = 1982 ^ [], 1982 ^ [] = 1976 ^ []],extension(10 ^ 3,bind([[_233451, _233453, _233455], [1976 ^ [], 1982 ^ [], 1985 ^ []]]))).
% 14.17/14.67 ncf('1.2.2.2.1',plain,[-(1985 ^ [] = 1982 ^ [])],extension(1993 ^ 4)).
% 14.17/14.67 ncf('1.2.2.2.2',plain,[-(1982 ^ [] = 1976 ^ []), 1976 ^ [] = 1982 ^ []],extension(4 ^ 4,bind([[_233247, _233249], [1982 ^ [], 1976 ^ []]]))).
% 14.17/14.67 ncf('1.2.2.2.2.1',plain,[-(1976 ^ [] = 1982 ^ [])],extension(1991 ^ 5)).
% 14.17/14.67 ncf('1.2.3',plain,[-(1994 ^ [] = 1994 ^ [])],extension(2 ^ 2,bind([[_233140], [1994 ^ []]]))).
% 14.17/14.67 %-----------------------------------------------------
% 14.17/14.67 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------