%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWX035+1 : TPTP v9.1.0. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n005.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 : Tue Apr 1 02:15:13 AM UTC 2025
% Result : Theorem 10.83s 10.70s
% Output : Proof 10.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : SWX035+1 : TPTP v9.1.0. Released v9.1.0.
% 0.10/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n005.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 : Mon Mar 31 14:28:44 EDT 2025
% 0.12/0.34 % CPUTime :
% 10.83/10.70
% 10.83/10.70 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 10.83/10.70 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.83/10.70 %-----------------------------------------------------
% 10.83/10.70 ncf(matrix, plain, [(1371 ^ _170730) ^ [] : [-(nat_succeeds(1368 ^ []))], (1373 ^ _170730) ^ [] : [-(nat_succeeds(1369 ^ []))], (1375 ^ _170730) ^ [] : [@*(s(1368 ^ []), 1369 ^ []) = @+(1369 ^ [], @*(1368 ^ [], 1369 ^ []))], (252 ^ _170730) ^ [_179048, _179050] : [_179050 = _179048, -(s(_179050) = s(_179048))], (258 ^ _170730) ^ [_179294, _179296, _179298, _179300] : [-(@+(_179300, _179296) = @+(_179298, _179294)), _179300 = _179298, _179296 = _179294], (268 ^ _170730) ^ [_179633, _179635, _179637, _179639] : [-(@*(_179639, _179635) = @*(_179637, _179633)), _179639 = _179637, _179635 = _179633], (2 ^ _170730) ^ [_170874] : [-(_170874 = _170874)], (4 ^ _170730) ^ [_170981, _170983] : [_170983 = _170981, -(_170981 = _170983)], (10 ^ _170730) ^ [_171185, _171187, _171189] : [-(_171189 = _171185), _171189 = _171187, _171187 = _171185], (20 ^ _170730) ^ [_171554, _171556, _171558, _171560, _171562, _171564] : [-(times_fails(_171562, _171558, _171554)), times_fails(_171564, _171560, _171556), _171564 = _171562, _171560 = _171558, _171556 = _171554], (38 ^ _170730) ^ [_172163, _172165, _172167, _172169, _172171, _172173] : [-(plus_fails(_172171, _172167, _172163)), plus_fails(_172173, _172169, _172165), _172173 = _172171, _172169 = _172167, _172165 = _172163], (56 ^ _170730) ^ [_172744, _172746, _172748, _172750] : [-('@=<_succeeds'(_172748, _172744)), '@=<_succeeds'(_172750, _172746), _172750 = _172748, _172746 = _172744], (70 ^ _170730) ^ [_173188, _173190, _173192, _173194] : [-('@=<_fails'(_173192, _173188)), '@=<_fails'(_173194, _173190), _173194 = _173192, _173190 = _173188], (84 ^ _170730) ^ [_173632, _173634, _173636, _173638] : [-('@=<_terminates'(_173636, _173632)), '@=<_terminates'(_173638, _173634), _173638 = _173636, _173634 = _173632], (98 ^ _170730) ^ [_174076, _174078, _174080, _174082] : [-('@<_succeeds'(_174080, _174076)), '@<_succeeds'(_174082, _174078), _174082 = _174080, _174078 = _174076], (112 ^ _170730) ^ [_174520, _174522, _174524, _174526] : [-('@<_fails'(_174524, _174520)), '@<_fails'(_174526, _174522), _174526 = _174524, _174522 = _174520], (126 ^ _170730) ^ [_174964, _174966, _174968, _174970] : [-('@<_terminates'(_174968, _174964)), '@<_terminates'(_174970, _174966), _174970 = _174968, _174966 = _174964], (140 ^ _170730) ^ [_175380, _175382] : [-(nat_fails(_175380)), _175382 = _175380, nat_fails(_175382)], (150 ^ _170730) ^ [_175675, _175677] : [-(nat_terminates(_175675)), _175677 = _175675, nat_terminates(_175677)], (160 ^ _170730) ^ [_176026, _176028, _176030, _176032, _176034, _176036] : [-(plus_terminates(_176034, _176030, _176026)), plus_terminates(_176036, _176032, _176028), _176036 = _176034, _176032 = _176030, _176028 = _176026], (178 ^ _170730) ^ [_176635, _176637, _176639, _176641, _176643, _176645] : [-(plus_succeeds(_176643, _176639, _176635)), plus_succeeds(_176645, _176641, _176637), _176645 = _176643, _176641 = _176639, _176637 = _176635], (196 ^ _170730) ^ [_177188, _177190] : [-(gr(_177188)), _177190 = _177188, gr(_177190)], (206 ^ _170730) ^ [_177539, _177541, _177543, _177545, _177547, _177549] : [-(times_terminates(_177547, _177543, _177539)), times_terminates(_177549, _177545, _177541), _177549 = _177547, _177545 = _177543, _177541 = _177539], (242 ^ _170730) ^ [_178681, _178683] : [-(nat_succeeds(_178681)), _178683 = _178681, nat_succeeds(_178683)], (224 ^ _170730) ^ [_178148, _178150, _178152, _178154, _178156, _178158] : [-(times_succeeds(_178156, _178152, _178148)), times_succeeds(_178158, _178154, _178150), _178158 = _178156, _178154 = _178152, _178150 = _178148], (278 ^ _170730) ^ [_179948] : ['0' = s(_179948)], (280 ^ _170730) ^ [_180057, _180059] : [s(_180059) = s(_180057), -(_180059 = _180057)], (286 ^ _170730) ^ [] : [-(gr('0'))], (288 ^ _170730) ^ [_180343] : [gr(_180343), -(gr(s(_180343)))], (294 ^ _170730) ^ [_180499] : [gr(s(_180499)), -(gr(_180499))], (300 ^ _170730) ^ [_180719, _180721, _180723] : [times_succeeds(_180723, _180721, _180719), times_fails(_180723, _180721, _180719)], (306 ^ _170730) ^ [_180952, _180954, _180956] : [times_terminates(_180956, _180954, _180952), -(times_succeeds(_180956, _180954, _180952)), -(times_fails(_180956, _180954, _180952))], (316 ^ _170730) ^ [_181282, _181284, _181286] : [plus_succeeds(_181286, _181284, _181282), plus_fails(_181286, _181284, _181282)], (322 ^ _170730) ^ [_181515, _181517, _181519] : [plus_terminates(_181519, _181517, _181515), -(plus_succeeds(_181519, _181517, _181515)), -(plus_fails(_181519, _181517, _181515))], (332 ^ _170730) ^ [_181831, _181833] : ['@=<_succeeds'(_181833, _181831), '@=<_fails'(_181833, _181831)], (338 ^ _170730) ^ [_182040, _182042] : ['@=<_terminates'(_182042, _182040), -('@=<_succeeds'(_182042, _182040)), -('@=<_fails'(_182042, _182040))], (348 ^ _170730) ^ [_182340, _182342] : ['@<_succeeds'(_182342, _182340), '@<_fails'(_182342, _182340)], (354 ^ _170730) ^ [_182549, _182551] : ['@<_terminates'(_182551, _182549), -('@<_succeeds'(_182551, _182549)), -('@<_fails'(_182551, _182549))], (364 ^ _170730) ^ [_182835] : [nat_succeeds(_182835), nat_fails(_182835)], (370 ^ _170730) ^ [_183020] : [nat_terminates(_183020), -(nat_succeeds(_183020)), -(nat_fails(_183020))], (380 ^ _170730) ^ [_183347, _183349, _183351] : [times_succeeds(_183351, _183349, _183347), 387 ^ _170730 : [(388 ^ _170730) ^ [] : [-(_183351 = s(385 ^ [_183347, _183349, _183351]))], (390 ^ _170730) ^ [] : [-(times_succeeds(385 ^ [_183347, _183349, _183351], _183349, 386 ^ [_183347, _183349, _183351]))], (392 ^ _170730) ^ [] : [-(plus_succeeds(_183349, 386 ^ [_183347, _183349, _183351], _183347))]], 393 ^ _170730 : [(394 ^ _170730) ^ [] : [-(_183351 = '0')], (396 ^ _170730) ^ [] : [-(_183347 = '0')]]], (398 ^ _170730) ^ [_184048, _184050, _184052] : [-(times_succeeds(_184052, _184050, _184048)), 399 ^ _170730 : [(410 ^ _170730) ^ [] : [_184052 = '0', _184048 = '0'], (400 ^ _170730) ^ [_184204, _184206] : [_184052 = s(_184206), times_succeeds(_184206, _184050, _184204), plus_succeeds(_184050, _184204, _184048)]]], (438 ^ _170730) ^ [_185430, _185432, _185434] : [-(times_fails(_185434, _185432, _185430)), 443 ^ _170730 : [(444 ^ _170730) ^ [] : [-(_185434 = s(441 ^ [_185430, _185432, _185434]))], (446 ^ _170730) ^ [] : [times_fails(441 ^ [_185430, _185432, _185434], _185432, 442 ^ [_185430, _185432, _185434])], (448 ^ _170730) ^ [] : [plus_fails(_185432, 442 ^ [_185430, _185432, _185434], _185430)]], 449 ^ _170730 : [(450 ^ _170730) ^ [] : [-(_185434 = '0')], (452 ^ _170730) ^ [] : [-(_185430 = '0')]]], (418 ^ _170730) ^ [_184781, _184783, _184785] : [times_fails(_184785, _184783, _184781), 421 ^ _170730 : [(432 ^ _170730) ^ [] : [_184785 = '0', _184781 = '0'], (422 ^ _170730) ^ [_184991, _184993] : [_184785 = s(_184993), -(times_fails(_184993, _184783, _184991)), -(plus_fails(_184783, _184991, _184781))]]], (494 ^ _170730) ^ [_187404, _187406, _187408] : [-(times_terminates(_187408, _187406, _187404)), 517 ^ _170730 : [(518 ^ _170730) ^ [] : [-(true___)], (520 ^ _170730) ^ [] : [true___]], 521 ^ _170730 : [(522 ^ _170730) ^ [] : [-(_187408 = '0')], (524 ^ _170730) ^ [] : [-(true___)], (526 ^ _170730) ^ [] : [true___]], 501 ^ _170730 : [(502 ^ _170730) ^ [] : [-(true___)], (504 ^ _170730) ^ [] : [true___]], 505 ^ _170730 : [(506 ^ _170730) ^ [] : [-(_187408 = s(497 ^ [_187404, _187406, _187408]))], (508 ^ _170730) ^ [] : [times_terminates(497 ^ [_187404, _187406, _187408], _187406, 498 ^ [_187404, _187406, _187408]), 511 ^ _170730 : [(512 ^ _170730) ^ [] : [times_fails(497 ^ [_187404, _187406, _187408], _187406, 498 ^ [_187404, _187406, _187408])], (514 ^ _170730) ^ [] : [plus_terminates(_187406, 498 ^ [_187404, _187406, _187408], _187404)]]]]], (456 ^ _170730) ^ [_186233, _186235, _186237] : [times_terminates(_186237, _186235, _186233), 459 ^ _170730 : [(460 ^ _170730) ^ [_186471, _186473] : [true___, -(true___)], (466 ^ _170730) ^ [_186645, _186647] : [_186237 = s(_186647), 469 ^ _170730 : [(470 ^ _170730) ^ [] : [-(times_terminates(_186647, _186235, _186645))], (472 ^ _170730) ^ [] : [-(times_fails(_186647, _186235, _186645)), -(plus_terminates(_186235, _186645, _186233))]]], (478 ^ _170730) ^ [] : [true___, -(true___)], (484 ^ _170730) ^ [] : [_186237 = '0', true___, -(true___)]]], (530 ^ _170730) ^ [_188720, _188722, _188724] : [plus_succeeds(_188724, _188722, _188720), 537 ^ _170730 : [(538 ^ _170730) ^ [] : [-(_188724 = s(535 ^ [_188720, _188722, _188724]))], (540 ^ _170730) ^ [] : [-(_188720 = s(536 ^ [_188720, _188722, _188724]))], (542 ^ _170730) ^ [] : [-(plus_succeeds(535 ^ [_188720, _188722, _188724], _188722, 536 ^ [_188720, _188722, _188724]))]], 543 ^ _170730 : [(544 ^ _170730) ^ [] : [-(_188724 = '0')], (546 ^ _170730) ^ [] : [-(_188720 = _188722)]]], (548 ^ _170730) ^ [_189425, _189427, _189429] : [-(plus_succeeds(_189429, _189427, _189425)), 549 ^ _170730 : [(560 ^ _170730) ^ [] : [_189429 = '0', _189425 = _189427], (550 ^ _170730) ^ [_189582, _189584] : [_189429 = s(_189584), _189425 = s(_189582), plus_succeeds(_189584, _189427, _189582)]]], (588 ^ _170730) ^ [_190816, _190818, _190820] : [-(plus_fails(_190820, _190818, _190816)), 593 ^ _170730 : [(594 ^ _170730) ^ [] : [-(_190820 = s(591 ^ [_190816, _190818, _190820]))], (596 ^ _170730) ^ [] : [-(_190816 = s(592 ^ [_190816, _190818, _190820]))], (598 ^ _170730) ^ [] : [plus_fails(591 ^ [_190816, _190818, _190820], _190818, 592 ^ [_190816, _190818, _190820])]], 599 ^ _170730 : [(600 ^ _170730) ^ [] : [-(_190820 = '0')], (602 ^ _170730) ^ [] : [-(_190816 = _190818)]]], (568 ^ _170730) ^ [_190161, _190163, _190165] : [plus_fails(_190165, _190163, _190161), 571 ^ _170730 : [(582 ^ _170730) ^ [] : [_190165 = '0', _190161 = _190163], (572 ^ _170730) ^ [_190374, _190376] : [_190165 = s(_190376), _190161 = s(_190374), -(plus_fails(_190376, _190163, _190374))]]], (648 ^ _170730) ^ [_192887, _192889, _192891] : [-(plus_terminates(_192891, _192889, _192887)), 673 ^ _170730 : [(674 ^ _170730) ^ [] : [-(true___)], (676 ^ _170730) ^ [] : [true___]], 677 ^ _170730 : [(678 ^ _170730) ^ [] : [-(_192891 = '0')], (680 ^ _170730) ^ [] : [-(true___)], (682 ^ _170730) ^ [] : [true___]], 655 ^ _170730 : [(656 ^ _170730) ^ [] : [-(true___)], (658 ^ _170730) ^ [] : [true___]], 659 ^ _170730 : [(660 ^ _170730) ^ [] : [-(_192891 = s(651 ^ [_192887, _192889, _192891]))], (662 ^ _170730) ^ [] : [663 ^ _170730 : [(664 ^ _170730) ^ [] : [-(true___)], (666 ^ _170730) ^ [] : [true___]], 667 ^ _170730 : [(668 ^ _170730) ^ [] : [-(_192887 = s(652 ^ [_192887, _192889, _192891]))], (670 ^ _170730) ^ [] : [plus_terminates(651 ^ [_192887, _192889, _192891], _192889, 652 ^ [_192887, _192889, _192891])]]]]], (606 ^ _170730) ^ [_191630, _191632, _191634] : [plus_terminates(_191634, _191632, _191630), 609 ^ _170730 : [(632 ^ _170730) ^ [] : [true___, -(true___)], (638 ^ _170730) ^ [] : [_191634 = '0', true___, -(true___)], (610 ^ _170730) ^ [_191867, _191869] : [true___, -(true___)], (616 ^ _170730) ^ [_192041, _192043] : [_191634 = s(_192043), 619 ^ _170730 : [(620 ^ _170730) ^ [] : [true___, -(true___)], (626 ^ _170730) ^ [] : [_191630 = s(_192041), -(plus_terminates(_192043, _191632, _192041))]]]]], (686 ^ _170730) ^ [_194225, _194227] : ['@=<_succeeds'(_194227, _194225), 693 ^ _170730 : [(694 ^ _170730) ^ [] : [-(_194227 = s(691 ^ [_194225, _194227]))], (696 ^ _170730) ^ [] : [-(_194225 = s(692 ^ [_194225, _194227]))], (698 ^ _170730) ^ [] : [-('@=<_succeeds'(691 ^ [_194225, _194227], 692 ^ [_194225, _194227]))]], -(_194227 = '0')], (702 ^ _170730) ^ [_194813, _194815] : [-('@=<_succeeds'(_194815, _194813)), 703 ^ _170730 : [(714 ^ _170730) ^ [] : [_194815 = '0'], (704 ^ _170730) ^ [_194960, _194962] : [_194815 = s(_194962), _194813 = s(_194960), '@=<_succeeds'(_194962, _194960)]]], (734 ^ _170730) ^ [_195956, _195958] : [-('@=<_fails'(_195958, _195956)), 739 ^ _170730 : [(740 ^ _170730) ^ [] : [-(_195958 = s(737 ^ [_195956, _195958]))], (742 ^ _170730) ^ [] : [-(_195956 = s(738 ^ [_195956, _195958]))], (744 ^ _170730) ^ [] : ['@=<_fails'(737 ^ [_195956, _195958], 738 ^ [_195956, _195958])]], -(_195958 = '0')], (718 ^ _170730) ^ [_195419, _195421] : ['@=<_fails'(_195421, _195419), 721 ^ _170730 : [(732 ^ _170730) ^ [] : [_195421 = '0'], (722 ^ _170730) ^ [_195617, _195619] : [_195421 = s(_195619), _195419 = s(_195617), -('@=<_fails'(_195619, _195617))]]], (782 ^ _170730) ^ [_197602, _197604] : [-('@=<_terminates'(_197604, _197602)), 805 ^ _170730 : [(806 ^ _170730) ^ [] : [-(true___)], (808 ^ _170730) ^ [] : [true___]], 789 ^ _170730 : [(790 ^ _170730) ^ [] : [-(true___)], (792 ^ _170730) ^ [] : [true___]], 793 ^ _170730 : [(794 ^ _170730) ^ [] : [-(_197604 = s(785 ^ [_197602, _197604]))], (796 ^ _170730) ^ [] : [797 ^ _170730 : [(798 ^ _170730) ^ [] : [-(true___)], (800 ^ _170730) ^ [] : [true___]], 801 ^ _170730 : [(802 ^ _170730) ^ [] : [-(_197602 = s(786 ^ [_197602, _197604]))], (804 ^ _170730) ^ [] : ['@=<_terminates'(785 ^ [_197602, _197604], 786 ^ [_197602, _197604])]]]]], (750 ^ _170730) ^ [_196637, _196639] : ['@=<_terminates'(_196639, _196637), 753 ^ _170730 : [(776 ^ _170730) ^ [] : [true___, -(true___)], (754 ^ _170730) ^ [_196856, _196858] : [true___, -(true___)], (760 ^ _170730) ^ [_197022, _197024] : [_196639 = s(_197024), 763 ^ _170730 : [(764 ^ _170730) ^ [] : [true___, -(true___)], (770 ^ _170730) ^ [] : [_196637 = s(_197022), -('@=<_terminates'(_197024, _197022))]]]]], (812 ^ _170730) ^ [_198651, _198653] : ['@<_succeeds'(_198653, _198651), 819 ^ _170730 : [(820 ^ _170730) ^ [] : [-(_198653 = s(817 ^ [_198651, _198653]))], (822 ^ _170730) ^ [] : [-(_198651 = s(818 ^ [_198651, _198653]))], (824 ^ _170730) ^ [] : [-('@<_succeeds'(817 ^ [_198651, _198653], 818 ^ [_198651, _198653]))]], 826 ^ _170730 : [(827 ^ _170730) ^ [] : [-(_198653 = '0')], (829 ^ _170730) ^ [] : [-(_198651 = s(825 ^ [_198651, _198653]))]]], (831 ^ _170730) ^ [_199383, _199385] : [-('@<_succeeds'(_199385, _199383)), 832 ^ _170730 : [(843 ^ _170730) ^ [_199839] : [_199385 = '0', _199383 = s(_199839)], (833 ^ _170730) ^ [_199543, _199545] : [_199385 = s(_199545), _199383 = s(_199543), '@<_succeeds'(_199545, _199543)]]], (871 ^ _170730) ^ [_200846, _200848] : [-('@<_fails'(_200848, _200846)), 876 ^ _170730 : [(877 ^ _170730) ^ [] : [-(_200848 = s(874 ^ [_200846, _200848]))], (879 ^ _170730) ^ [] : [-(_200846 = s(875 ^ [_200846, _200848]))], (881 ^ _170730) ^ [] : ['@<_fails'(874 ^ [_200846, _200848], 875 ^ [_200846, _200848])]], 883 ^ _170730 : [(884 ^ _170730) ^ [] : [-(_200848 = '0')], (886 ^ _170730) ^ [] : [-(_200846 = s(882 ^ [_200846, _200848]))]]], (851 ^ _170730) ^ [_200146, _200148] : ['@<_fails'(_200148, _200146), 854 ^ _170730 : [(865 ^ _170730) ^ [_200660] : [_200148 = '0', _200146 = s(_200660)], (855 ^ _170730) ^ [_200359, _200361] : [_200148 = s(_200361), _200146 = s(_200359), -('@<_fails'(_200361, _200359))]]], (932 ^ _170730) ^ [_202985, _202987] : [-('@<_terminates'(_202987, _202985)), 958 ^ _170730 : [(959 ^ _170730) ^ [] : [-(true___)], (961 ^ _170730) ^ [] : [true___]], 962 ^ _170730 : [(963 ^ _170730) ^ [] : [-(_202987 = '0')], (965 ^ _170730) ^ [] : [-(true___)], (967 ^ _170730) ^ [] : [true___]], 939 ^ _170730 : [(940 ^ _170730) ^ [] : [-(true___)], (942 ^ _170730) ^ [] : [true___]], 943 ^ _170730 : [(944 ^ _170730) ^ [] : [-(_202987 = s(935 ^ [_202985, _202987]))], (946 ^ _170730) ^ [] : [947 ^ _170730 : [(948 ^ _170730) ^ [] : [-(true___)], (950 ^ _170730) ^ [] : [true___]], 951 ^ _170730 : [(952 ^ _170730) ^ [] : [-(_202985 = s(936 ^ [_202985, _202987]))], (954 ^ _170730) ^ [] : ['@<_terminates'(935 ^ [_202985, _202987], 936 ^ [_202985, _202987])]]]]], (890 ^ _170730) ^ [_201677, _201679] : ['@<_terminates'(_201679, _201677), 893 ^ _170730 : [(916 ^ _170730) ^ [_202562] : [true___, -(true___)], (922 ^ _170730) ^ [_202722] : [_201679 = '0', true___, -(true___)], (894 ^ _170730) ^ [_201912, _201914] : [true___, -(true___)], (900 ^ _170730) ^ [_202078, _202080] : [_201679 = s(_202080), 903 ^ _170730 : [(904 ^ _170730) ^ [] : [true___, -(true___)], (910 ^ _170730) ^ [] : [_201677 = s(_202078), -('@<_terminates'(_202080, _202078))]]]]], (971 ^ _170730) ^ [_204305] : [nat_succeeds(_204305), 977 ^ _170730 : [(978 ^ _170730) ^ [] : [-(_204305 = s(976 ^ [_204305]))], (980 ^ _170730) ^ [] : [-(nat_succeeds(976 ^ [_204305]))]], -(_204305 = '0')], (984 ^ _170730) ^ [_204683] : [-(nat_succeeds(_204683)), 985 ^ _170730 : [(992 ^ _170730) ^ [] : [_204683 = '0'], (986 ^ _170730) ^ [_204799] : [_204683 = s(_204799), nat_succeeds(_204799)]]], (996 ^ _170730) ^ [_205122] : [nat_fails(_205122), 999 ^ _170730 : [(1006 ^ _170730) ^ [] : [_205122 = '0'], (1000 ^ _170730) ^ [_205284] : [_205122 = s(_205284), -(nat_fails(_205284))]]], (1008 ^ _170730) ^ [_205502] : [-(nat_fails(_205502)), 1012 ^ _170730 : [(1013 ^ _170730) ^ [] : [-(_205502 = s(1011 ^ [_205502]))], (1015 ^ _170730) ^ [] : [nat_fails(1011 ^ [_205502])]], -(_205502 = '0')], (1043 ^ _170730) ^ [_206577] : [-(nat_terminates(_206577)), 1057 ^ _170730 : [(1058 ^ _170730) ^ [] : [-(true___)], (1060 ^ _170730) ^ [] : [true___]], 1049 ^ _170730 : [(1050 ^ _170730) ^ [] : [-(true___)], (1052 ^ _170730) ^ [] : [true___]], 1053 ^ _170730 : [(1054 ^ _170730) ^ [] : [-(_206577 = s(1046 ^ [_206577]))], (1056 ^ _170730) ^ [] : [nat_terminates(1046 ^ [_206577])]]], (1021 ^ _170730) ^ [_205951] : [nat_terminates(_205951), 1024 ^ _170730 : [(1037 ^ _170730) ^ [] : [true___, -(true___)], (1025 ^ _170730) ^ [_206131] : [true___, -(true___)], (1031 ^ _170730) ^ [_206283] : [_205951 = s(_206283), -(nat_terminates(_206283))]]], (1064 ^ _170730) ^ [_207226, _207228, _207230] : [nat_succeeds(_207230), 1067 ^ _170730 : [(1068 ^ _170730) ^ [] : [@+(_207230, _207228) = _207226, -(plus_succeeds(_207230, _207228, _207226))], (1074 ^ _170730) ^ [] : [plus_succeeds(_207230, _207228, _207226), -(@+(_207230, _207228) = _207226)]]], (1080 ^ _170730) ^ [_207726, _207728, _207730] : [nat_succeeds(_207730), nat_succeeds(_207728), 1087 ^ _170730 : [(1088 ^ _170730) ^ [] : [@*(_207730, _207728) = _207726, -(times_succeeds(_207730, _207728, _207726))], (1094 ^ _170730) ^ [] : [times_succeeds(_207730, _207728, _207726), -(@*(_207730, _207728) = _207726)]]], (1100 ^ _170730) ^ [_208291] : [nat_succeeds(_208291), -(nat_terminates(_208291))], (1106 ^ _170730) ^ [_208477] : [nat_succeeds(_208477), -(gr(_208477))], (1112 ^ _170730) ^ [_208691, _208693, _208695] : [nat_succeeds(_208695), -(plus_terminates(_208695, _208693, _208691))], (1118 ^ _170730) ^ [_208921, _208923, _208925] : [nat_succeeds(_208921), -(plus_terminates(_208925, _208923, _208921))], (1124 ^ _170730) ^ [_209151, _209153, _209155] : [plus_succeeds(_209155, _209153, _209151), -(nat_succeeds(_209155))], (1130 ^ _170730) ^ [_209381, _209383, _209385] : [-(nat_succeeds(_209381)), plus_succeeds(_209385, _209383, _209381), nat_succeeds(_209383)], (1140 ^ _170730) ^ [_209702, _209704, _209706] : [-(nat_succeeds(_209704)), plus_succeeds(_209706, _209704, _209702), nat_succeeds(_209702)], (1150 ^ _170730) ^ [_210023, _210025, _210027] : [plus_succeeds(_210027, _210025, _210023), -(plus_terminates(_210027, _210025, _210023))], (1156 ^ _170730) ^ [_210257, _210259, _210261] : [plus_succeeds(_210261, _210259, _210257), -(gr(_210261))], (1162 ^ _170730) ^ [_210487, _210489, _210491] : [-(gr(_210487)), plus_succeeds(_210491, _210489, _210487), gr(_210489)], (1172 ^ _170730) ^ [_210808, _210810, _210812] : [-(gr(_210810)), plus_succeeds(_210812, _210810, _210808), gr(_210808)], (1182 ^ _170730) ^ [_211115, _211117] : [nat_succeeds(_211117), -(plus_succeeds(_211117, _211115, 1185 ^ [_211115, _211117]))], (1189 ^ _170730) ^ [_211411, _211413, _211415, _211417] : [-(_211413 = _211411), plus_succeeds(_211417, _211415, _211413), plus_succeeds(_211417, _211415, _211411)], (1199 ^ _170730) ^ [_211705] : [-(@+('0', _211705) = _211705)], (1201 ^ _170730) ^ [_211815, _211817] : [nat_succeeds(_211817), -(@+(s(_211817), _211815) = s(@+(_211817, _211815)))], (1207 ^ _170730) ^ [_212043, _212045] : [-(nat_succeeds(@+(_212045, _212043))), nat_succeeds(_212045), nat_succeeds(_212043)], (1217 ^ _170730) ^ [_212356, _212358, _212360] : [-(@+(@+(_212360, _212358), _212356) = @+(_212360, @+(_212358, _212356))), nat_succeeds(_212360), nat_succeeds(_212358), nat_succeeds(_212356)], (1231 ^ _170730) ^ [_212762] : [nat_succeeds(_212762), -(@+(_212762, '0') = _212762)], (1237 ^ _170730) ^ [_212970, _212972] : [-(@+(_212972, s(_212970)) = @+(s(_212972), _212970)), nat_succeeds(_212972), nat_succeeds(_212970)], (1247 ^ _170730) ^ [_213285, _213287] : [-(@+(_213287, _213285) = @+(_213285, _213287)), nat_succeeds(_213287), nat_succeeds(_213285)], (1257 ^ _170730) ^ [_213606, _213608, _213610] : [-(_213608 = _213606), nat_succeeds(_213610), @+(_213610, _213608) = @+(_213610, _213606)], (1267 ^ _170730) ^ [_213939, _213941, _213943] : [times_succeeds(_213943, _213941, _213939), -(nat_succeeds(_213943))], (1273 ^ _170730) ^ [_214169, _214171, _214173] : [-(nat_succeeds(_214169)), times_succeeds(_214173, _214171, _214169), nat_succeeds(_214171)], (1283 ^ _170730) ^ [_214490, _214492, _214494] : [times_succeeds(_214494, _214492, _214490), -(gr(_214494))], (1289 ^ _170730) ^ [_214720, _214722, _214724] : [-(gr(_214720)), times_succeeds(_214724, _214722, _214720), gr(_214722)], (1299 ^ _170730) ^ [_215041, _215043, _215045] : [-(times_terminates(_215045, _215043, _215041)), nat_succeeds(_215045), nat_succeeds(_215043)], (1309 ^ _170730) ^ [_215348, _215350] : [-(times_succeeds(_215350, _215348, 1316 ^ [_215348, _215350])), nat_succeeds(_215350), nat_succeeds(_215348)], (1320 ^ _170730) ^ [_215731, _215733, _215735, _215737] : [-(_215733 = _215731), times_succeeds(_215737, _215735, _215733), times_succeeds(_215737, _215735, _215731)], (1330 ^ _170730) ^ [_216040] : [nat_succeeds(_216040), -(@*('0', _216040) = '0')], (1336 ^ _170730) ^ [] : [1338 ^ _170730 : [(1355 ^ _170730) ^ [] : [-(nat_succeeds(1353 ^ []))], (1357 ^ _170730) ^ [] : [@*(s(1337 ^ []), 1353 ^ []) = @+(1353 ^ [], @*(1337 ^ [], 1353 ^ []))], (1339 ^ _170730) ^ [] : [-(1337 ^ [] = '0'), 1341 ^ _170730 : [(1342 ^ _170730) ^ [] : [-(1337 ^ [] = s(1340 ^ []))], (1344 ^ _170730) ^ [] : [-(nat_succeeds(1340 ^ []))], (1346 ^ _170730) ^ [_216580] : [nat_succeeds(_216580), -(@*(s(1340 ^ []), _216580) = @+(_216580, @*(1340 ^ [], _216580)))]]]], 1358 ^ _170730 : [(1359 ^ _170730) ^ [_216950] : [nat_succeeds(_216950), 1362 ^ _170730 : [(1363 ^ _170730) ^ [_217091] : [nat_succeeds(_217091), -(@*(s(_216950), _217091) = @+(_217091, @*(_216950, _217091)))]]]]]], input).
% 10.83/10.70 ncf('1',plain,[@*(s(1368 ^ []), 1369 ^ []) = @+(1369 ^ [], @*(1368 ^ [], 1369 ^ []))],start(1375 ^ 0)).
% 10.83/10.70 ncf('1.1',plain,[-(@*(s(1368 ^ []), 1369 ^ []) = @+(1369 ^ [], @*(1368 ^ [], 1369 ^ []))), 1094 : times_succeeds(s(1368 ^ []), 1369 ^ [], @+(1369 ^ [], @*(1368 ^ [], 1369 ^ []))), 1094 : nat_succeeds(s(1368 ^ [])), 1094 : nat_succeeds(1369 ^ [])],extension(1080 ^ 1,bind([[_207726, _207728, _207730], [@+(1369 ^ [], @*(1368 ^ [], 1369 ^ [])), 1369 ^ [], s(1368 ^ [])]]))).
% 10.83/10.70 ncf('1.1.1',plain,[-(times_succeeds(s(1368 ^ []), 1369 ^ [], @+(1369 ^ [], @*(1368 ^ [], 1369 ^ [])))), 400 : s(1368 ^ []) = s(1368 ^ []), 400 : times_succeeds(1368 ^ [], 1369 ^ [], @*(1368 ^ [], 1369 ^ [])), 400 : plus_succeeds(1369 ^ [], @*(1368 ^ [], 1369 ^ []), @+(1369 ^ [], @*(1368 ^ [], 1369 ^ [])))],extension(398 ^ 4,bind([[_184048, _184050, _184052, _184204, _184206], [@+(1369 ^ [], @*(1368 ^ [], 1369 ^ [])), 1369 ^ [], s(1368 ^ []), @*(1368 ^ [], 1369 ^ []), 1368 ^ []]]))).
% 10.83/10.70 ncf('1.1.1.1',plain,[-(s(1368 ^ []) = s(1368 ^ [])), 1368 ^ [] = 1368 ^ []],extension(252 ^ 7,bind([[_179048, _179050], [1368 ^ [], 1368 ^ []]]))).
% 10.83/10.70 ncf('1.1.1.1.1',plain,[-(1368 ^ [] = 1368 ^ [])],extension(2 ^ 8,bind([[_170874], [1368 ^ []]]))).
% 10.83/10.70 ncf('1.1.1.2',plain,[-(times_succeeds(1368 ^ [], 1369 ^ [], @*(1368 ^ [], 1369 ^ []))), 1088 : @*(1368 ^ [], 1369 ^ []) = @*(1368 ^ [], 1369 ^ []), 1088 : nat_succeeds(1368 ^ []), 1088 : nat_succeeds(1369 ^ [])],extension(1080 ^ 7,bind([[_207726, _207728, _207730], [@*(1368 ^ [], 1369 ^ []), 1369 ^ [], 1368 ^ []]]))).
% 10.83/10.70 ncf('1.1.1.2.1',plain,[-(@*(1368 ^ [], 1369 ^ []) = @*(1368 ^ [], 1369 ^ []))],extension(2 ^ 10,bind([[_170874], [@*(1368 ^ [], 1369 ^ [])]]))).
% 10.83/10.70 ncf('1.1.1.2.2',plain,[-(nat_succeeds(1368 ^ []))],extension(1371 ^ 8)).
% 10.83/10.70 ncf('1.1.1.2.3',plain,[-(nat_succeeds(1369 ^ []))],extension(1373 ^ 8)).
% 10.83/10.70 ncf('1.1.1.3',plain,[-(plus_succeeds(1369 ^ [], @*(1368 ^ [], 1369 ^ []), @+(1369 ^ [], @*(1368 ^ [], 1369 ^ [])))), 1068 : @+(1369 ^ [], @*(1368 ^ [], 1369 ^ [])) = @+(1369 ^ [], @*(1368 ^ [], 1369 ^ [])), 1068 : nat_succeeds(1369 ^ [])],extension(1064 ^ 7,bind([[_207226, _207228, _207230], [@+(1369 ^ [], @*(1368 ^ [], 1369 ^ [])), @*(1368 ^ [], 1369 ^ []), 1369 ^ []]]))).
% 10.83/10.70 ncf('1.1.1.3.1',plain,[-(@+(1369 ^ [], @*(1368 ^ [], 1369 ^ [])) = @+(1369 ^ [], @*(1368 ^ [], 1369 ^ [])))],extension(2 ^ 10,bind([[_170874], [@+(1369 ^ [], @*(1368 ^ [], 1369 ^ []))]]))).
% 10.83/10.70 ncf('1.1.1.3.2',plain,[-(nat_succeeds(1369 ^ []))],extension(1373 ^ 8)).
% 10.83/10.70 ncf('1.1.2',plain,[-(nat_succeeds(s(1368 ^ []))), 986 : s(1368 ^ []) = s(1368 ^ []), 986 : nat_succeeds(1368 ^ [])],extension(984 ^ 2,bind([[_204683, _204799], [s(1368 ^ []), 1368 ^ []]]))).
% 10.83/10.70 ncf('1.1.2.1',plain,[-(s(1368 ^ []) = s(1368 ^ [])), 1368 ^ [] = 1368 ^ []],extension(252 ^ 5,bind([[_179048, _179050], [1368 ^ [], 1368 ^ []]]))).
% 10.83/10.70 ncf('1.1.2.1.1',plain,[-(1368 ^ [] = 1368 ^ [])],extension(2 ^ 6,bind([[_170874], [1368 ^ []]]))).
% 10.83/10.70 ncf('1.1.2.2',plain,[-(nat_succeeds(1368 ^ []))],extension(1371 ^ 5)).
% 10.83/10.70 ncf('1.1.3',plain,[-(nat_succeeds(1369 ^ []))],extension(1373 ^ 2)).
% 10.83/10.70 %-----------------------------------------------------
% 10.83/10.70 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------