%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWX048+1 : TPTP v9.1.0. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n006.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:14 AM UTC 2025
% Result : Theorem 218.51s 211.42s
% Output : Proof 218.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX048+1 : TPTP v9.1.0. Released v9.1.0.
% 0.12/0.12 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n006.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Mon Mar 31 14:58:25 EDT 2025
% 0.13/0.34 % CPUTime :
% 218.51/211.42
% 218.51/211.42 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 218.51/211.42 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 218.51/211.42 %-----------------------------------------------------
% 218.51/211.42 ncf(matrix, plain, [(5094 ^ _492262) ^ [] : [occ(5086 ^ [], cons(5087 ^ [], 5088 ^ [])) = occ(5086 ^ [], 5088 ^ [])], (5092 ^ _492262) ^ [] : [5086 ^ [] = 5087 ^ []], (5090 ^ _492262) ^ [] : [-(list_succeeds(5088 ^ []))], !, (5025 ^ _315349) ^ [_487001, _487003, _487005] : [occ_succeeds(_487005, _487003, _487001), 5028 ^ _315349 : [(5031 ^ _315349) ^ [] : [-(nat_succeeds(_487001))], (5029 ^ _315349) ^ [] : [-(list_succeeds(_487003))]]], (2706 ^ _315349) ^ [_410430, _410432, _410434] : [-(plus_succeeds(_410434, _410432, _410430)), 2707 ^ _315349 : [(2708 ^ _315349) ^ [_410587, _410589] : [_410434 = s(_410589), _410430 = s(_410587), plus_succeeds(_410589, _410432, _410587)], (2718 ^ _315349) ^ [] : [_410434 = '0', _410430 = _410432]]], (3570 ^ _315349) ^ [_439712, _439714] : ['@<_succeeds'(_439714, _439712), -(nat_succeeds(_439714))], (1372 ^ _315349) ^ [_361544, _361546, _361548] : [-(occ_terminates(_361548, _361546, _361544)), 1379 ^ _315349 : [(1382 ^ _315349) ^ [] : [true___], (1380 ^ _315349) ^ [] : [-(true___)]], 1383 ^ _315349 : [(1386 ^ _315349) ^ [] : [1387 ^ _315349 : [(1390 ^ _315349) ^ [] : [true___], (1388 ^ _315349) ^ [] : [-(true___)]], gr(_361548), gr(1375 ^ [_361544, _361546, _361548]), 1399 ^ _315349 : [(1402 ^ _315349) ^ [] : [occ_terminates(_361548, 1376 ^ [_361544, _361546, _361548], _361544)], (1400 ^ _315349) ^ [] : [_361548 = 1375 ^ [_361544, _361546, _361548]]]], (1384 ^ _315349) ^ [] : [-(_361546 = cons(1375 ^ [_361544, _361546, _361548], 1376 ^ [_361544, _361546, _361548]))]], 1427 ^ _315349 : [(1430 ^ _315349) ^ [] : [true___], (1428 ^ _315349) ^ [] : [-(true___)]], 1431 ^ _315349 : [(1436 ^ _315349) ^ [] : [true___], (1434 ^ _315349) ^ [] : [-(true___)], (1432 ^ _315349) ^ [] : [-(_361546 = nil)]], 1409 ^ _315349 : [(1412 ^ _315349) ^ [] : [true___], (1410 ^ _315349) ^ [] : [-(true___)]], 1413 ^ _315349 : [(1416 ^ _315349) ^ [] : [1417 ^ _315349 : [(1420 ^ _315349) ^ [] : [true___], (1418 ^ _315349) ^ [] : [-(true___)]], 1421 ^ _315349 : [(1424 ^ _315349) ^ [] : [occ_terminates(_361548, 1405 ^ [_361544, _361546, _361548], 1406 ^ [_361544, _361546, _361548])], (1422 ^ _315349) ^ [] : [-(_361544 = s(1406 ^ [_361544, _361546, _361548]))]]], (1414 ^ _315349) ^ [] : [-(_361546 = cons(_361548, 1405 ^ [_361544, _361546, _361548]))]]], (3979 ^ _315349) ^ [_452643, _452645, _452647, _452649] : [-('@<_succeeds'(@+(_452649, _452647), @+(_452645, _452643))), '@=<_succeeds'(_452649, _452645), '@<_succeeds'(_452647, _452643), nat_succeeds(_452645)], (4264 ^ _315349) ^ [_461867, _461869] : [-(gr(_461869 ** _461867)), list_succeeds(_461869), gr(_461869), gr(_461867)], (3787 ^ _315349) ^ [_446574, _446576, _446578] : [-('@<_succeeds'(_446578, _446574)), '@<_succeeds'(_446578, _446576), '@=<_succeeds'(_446576, _446574)], (2746 ^ _315349) ^ [_411821, _411823, _411825] : [-(plus_fails(_411825, _411823, _411821)), 2751 ^ _315349 : [(2756 ^ _315349) ^ [] : [plus_fails(2749 ^ [_411821, _411823, _411825], _411823, 2750 ^ [_411821, _411823, _411825])], (2754 ^ _315349) ^ [] : [-(_411821 = s(2750 ^ [_411821, _411823, _411825]))], (2752 ^ _315349) ^ [] : [-(_411825 = s(2749 ^ [_411821, _411823, _411825]))]], 2757 ^ _315349 : [(2760 ^ _315349) ^ [] : [-(_411821 = _411823)], (2758 ^ _315349) ^ [] : [-(_411825 = '0')]]], (3532 ^ _315349) ^ [_438454] : [nat_succeeds(_438454), -(@*(s('0'), _438454) = _438454)], (2764 ^ _315349) ^ [_412635, _412637, _412639] : [plus_terminates(_412639, _412637, _412635), 2767 ^ _315349 : [(2774 ^ _315349) ^ [_413046, _413048] : [_412639 = s(_413048), 2777 ^ _315349 : [(2784 ^ _315349) ^ [] : [_412635 = s(_413046), -(plus_terminates(_413048, _412637, _413046))], (2778 ^ _315349) ^ [] : [true___, -(true___)]]], (2790 ^ _315349) ^ [] : [true___, -(true___)], (2768 ^ _315349) ^ [_412872, _412874] : [true___, -(true___)], (2796 ^ _315349) ^ [] : [_412639 = '0', true___, -(true___)]]], (4149 ^ _315349) ^ [_458025, _458027, _458029] : [-(list_succeeds(_458025)), append_succeeds(_458029, _458027, _458025), list_succeeds(_458027)], (3129 ^ _315349) ^ [_425310] : [nat_succeeds(_425310), 3135 ^ _315349 : [(3138 ^ _315349) ^ [] : [-(nat_succeeds(3134 ^ [_425310]))], (3136 ^ _315349) ^ [] : [-(_425310 = s(3134 ^ [_425310]))]], -(_425310 = '0')], (382 ^ _315349) ^ [_327828, _327830, _327832, _327834, _327836, _327838] : [-(append_terminates(_327836, _327832, _327828)), append_terminates(_327838, _327834, _327830), _327838 = _327836, _327834 = _327832, _327830 = _327828], (768 ^ _315349) ^ [_340658, _340660, _340662, _340664] : [-(@*(_340664, _340660) = @*(_340662, _340658)), _340664 = _340662, _340660 = _340658], (3323 ^ _315349) ^ [_431727, _431729] : [nat_succeeds(_431729), -(@+(s(_431729), _431727) = s(@+(_431729, _431727)))], (854 ^ _315349) ^ [_343830] : [gr(s(_343830)), -(gr(_343830))], (3599 ^ _315349) ^ [_440748, _440750, _440752] : [-('@<_succeeds'(_440752, _440748)), '@<_succeeds'(_440752, _440750), '@<_succeeds'(_440750, _440748)], (3839 ^ _315349) ^ [_448222, _448224] : [nat_succeeds(_448224), -('@<_succeeds'(_448224, @+(_448224, s(_448222))))], (1491 ^ _315349) ^ [_365881, _365883] : [1495 ^ _315349 : [(1502 ^ _315349) ^ [] : [1493 ^ [_365881, _365883] = 1494 ^ [_365881, _365883]], (1496 ^ _315349) ^ [] : [member2_fails(1492 ^ [_365881, _365883], _365883, _365881)], (1500 ^ _315349) ^ [] : [occ_fails(1492 ^ [_365881, _365883], _365881, 1494 ^ [_365881, _365883])], (1498 ^ _315349) ^ [] : [occ_fails(1492 ^ [_365881, _365883], _365883, 1493 ^ [_365881, _365883])]], -(not_same_occ_fails(_365883, _365881))], (1983 ^ _315349) ^ [_384656, _384658] : [length_terminates(_384658, _384656), 1986 ^ _315349 : [(1993 ^ _315349) ^ [_385078, _385080, _385082] : [_384658 = cons(_385082, _385080), 1996 ^ _315349 : [(2003 ^ _315349) ^ [] : [_384656 = s(_385078), -(length_terminates(_385080, _385078))], (1997 ^ _315349) ^ [] : [true___, -(true___)]]], (2009 ^ _315349) ^ [] : [true___, -(true___)], (1987 ^ _315349) ^ [_384906, _384908, _384910] : [true___, -(true___)], (2015 ^ _315349) ^ [] : [_384658 = nil, true___, -(true___)]]], (4219 ^ _315349) ^ [_460317, _460319] : [list_succeeds(_460319), -(append_succeeds(_460319, _460317, 4222 ^ [_460317, _460319]))], (4515 ^ _315349) ^ [_470310, _470312, _470314] : [-(member_succeeds(_470314, _470312 ** _470310)), member_succeeds(_470314, _470310), list_succeeds(_470312)], (3883 ^ _315349) ^ [_449601, _449603, _449605] : [-('@=<_succeeds'(@+(_449605, _449601), @+(_449603, _449601))), '@=<_succeeds'(_449605, _449603), nat_succeeds(_449603), nat_succeeds(_449601)], (3941 ^ _315349) ^ [_451388, _451390, _451392] : [-('@=<_succeeds'(_451390, _451388)), nat_succeeds(_451392), '@=<_succeeds'(@+(_451392, _451390), @+(_451392, _451388))], (4435 ^ _315349) ^ [_467455, _467457, _467459] : [-('@=<_succeeds'(lh(_467457), lh(_467455))), append_succeeds(_467459, _467457, _467455), list_succeeds(_467455)], (5050 ^ _315349) ^ [_487882] : [-(occ(_487882, nil) = '0')], (4101 ^ _315349) ^ [_456424] : [list_succeeds(_456424), -(list_terminates(_456424))], (4814 ^ _315349) ^ [_480526, _480528, _480530] : [nat_succeeds(_480530), 4817 ^ _315349 : [(4824 ^ _315349) ^ [] : [plus_succeeds(_480530, _480528, _480526), -(@+(_480530, _480528) = _480526)], (4818 ^ _315349) ^ [] : [@+(_480530, _480528) = _480526, -(plus_succeeds(_480530, _480528, _480526))]]], (4306 ^ _315349) ^ [_463162, _463164] : [length_succeeds(_463164, _463162), 4309 ^ _315349 : [(4312 ^ _315349) ^ [] : [-(nat_succeeds(_463162))], (4310 ^ _315349) ^ [] : [-(list_succeeds(_463164))]]], (4399 ^ _315349) ^ [_466238, _466240] : [-('@=<_succeeds'(lh(_466238), lh(_466240 ** _466238))), list_succeeds(_466240), list_succeeds(_466238)], (4892 ^ _315349) ^ [_482912, _482914] : [4894 ^ _315349 : [(4897 ^ _315349) ^ [] : [member_succeeds(4893 ^ [_482912, _482914], _482912)], (4895 ^ _315349) ^ [] : [-(member_succeeds(4893 ^ [_482912, _482914], _482914))]], -(sub(_482914, _482912))], (4685 ^ _315349) ^ [_475904, _475906, _475908] : [list_succeeds(_475904), -(delete_terminates(_475908, _475906, _475904))], (3583 ^ _315349) ^ [_440207, _440209, _440211] : [-('@<_succeeds'(_440211, _440207)), '@<_succeeds'(_440211, _440209), '@<_succeeds'(_440209, s(_440207))], (1304 ^ _315349) ^ [_359365, _359367, _359369] : [occ_terminates(_359369, _359367, _359365), 1307 ^ _315349 : [(1334 ^ _315349) ^ [_360518, _360520] : [true___, -(true___)], (1362 ^ _315349) ^ [] : [_359367 = nil, true___, -(true___)], (1340 ^ _315349) ^ [_360692, _360694] : [_359367 = cons(_359369, _360694), 1343 ^ _315349 : [(1350 ^ _315349) ^ [] : [_359365 = s(_360692), -(occ_terminates(_359369, _360694, _360692))], (1344 ^ _315349) ^ [] : [true___, -(true___)]]], (1308 ^ _315349) ^ [_359653, _359655] : [true___, -(true___)], (1314 ^ _315349) ^ [_359827, _359829] : [_359367 = cons(_359829, _359827), 1317 ^ _315349 : [(1328 ^ _315349) ^ [] : [-(_359369 = _359829), -(occ_terminates(_359369, _359827, _359365))], (1318 ^ _315349) ^ [] : [true___, -(true___)], (1326 ^ _315349) ^ [] : [-(gr(_359829))], (1324 ^ _315349) ^ [] : [-(gr(_359369))]]], (1356 ^ _315349) ^ [] : [true___, -(true___)]]], (824 ^ _315349) ^ [_342697, _342699] : [s(_342699) = s(_342697), -(_342699 = _342697)], (214 ^ _315349) ^ [_322452, _322454, _322456, _322458, _322460, _322462] : [-(plus_fails(_322460, _322456, _322452)), plus_fails(_322462, _322458, _322454), _322462 = _322460, _322458 = _322456, _322454 = _322452], (438 ^ _315349) ^ [_329592, _329594, _329596, _329598] : [-('@<_succeeds'(_329596, _329592)), '@<_succeeds'(_329598, _329594), _329598 = _329596, _329594 = _329592], (3329 ^ _315349) ^ [_431955, _431957] : [-(nat_succeeds(@+(_431957, _431955))), nat_succeeds(_431957), nat_succeeds(_431955)], (4357 ^ _315349) ^ [_464876] : [-(_464876 = nil), list_succeeds(_464876), lh(_464876) = '0'], (4830 ^ _315349) ^ [_481026, _481028, _481030] : [nat_succeeds(_481030), nat_succeeds(_481028), 4837 ^ _315349 : [(4844 ^ _315349) ^ [] : [times_succeeds(_481030, _481028, _481026), -(@*(_481030, _481028) = _481026)], (4838 ^ _315349) ^ [] : [@*(_481030, _481028) = _481026, -(times_succeeds(_481030, _481028, _481026))]]], (3166 ^ _315349) ^ [_426507] : [-(nat_fails(_426507)), 3170 ^ _315349 : [(3173 ^ _315349) ^ [] : [nat_fails(3169 ^ [_426507])], (3171 ^ _315349) ^ [] : [-(_426507 = s(3169 ^ [_426507]))]], -(_426507 = '0')], (1006 ^ _315349) ^ [_348891, _348893] : [member_succeeds(_348893, _348891), member_fails(_348893, _348891)], (2556 ^ _315349) ^ [_405053, _405055, _405057] : [-(times_succeeds(_405057, _405055, _405053)), 2557 ^ _315349 : [(2558 ^ _315349) ^ [_405209, _405211] : [_405057 = s(_405211), times_succeeds(_405211, _405055, _405209), plus_succeeds(_405055, _405209, _405053)], (2568 ^ _315349) ^ [] : [_405057 = '0', _405053 = '0']]], (4143 ^ _315349) ^ [_457795, _457797, _457799] : [append_succeeds(_457799, _457797, _457795), -(list_succeeds(_457799))], (2510 ^ _315349) ^ [_403404] : [-(nat_list_terminates(_403404)), 2531 ^ _315349 : [(2534 ^ _315349) ^ [] : [true___], (2532 ^ _315349) ^ [] : [-(true___)]], 2517 ^ _315349 : [(2520 ^ _315349) ^ [] : [true___], (2518 ^ _315349) ^ [] : [-(true___)]], 2521 ^ _315349 : [(2524 ^ _315349) ^ [] : [nat_terminates(2513 ^ [_403404]), 2527 ^ _315349 : [(2530 ^ _315349) ^ [] : [nat_list_terminates(2514 ^ [_403404])], (2528 ^ _315349) ^ [] : [nat_fails(2513 ^ [_403404])]]], (2522 ^ _315349) ^ [] : [-(_403404 = cons(2513 ^ [_403404], 2514 ^ [_403404]))]]], (4314 ^ _315349) ^ [_463443, _463445] : [list_succeeds(_463445), -(length_terminates(_463445, _463443))], (4531 ^ _315349) ^ [_470909, _470911, _470913, _470915] : [append_succeeds(_470913, _470911, _470909), member_succeeds(_470915, _470909), -(member_succeeds(_470915, _470913)), -(member_succeeds(_470915, _470911))], (2434 ^ _315349) ^ [_400887] : [-(nat_list_succeeds(_400887)), 2435 ^ _315349 : [(2436 ^ _315349) ^ [_401028, _401030] : [_400887 = cons(_401030, _401028), nat_succeeds(_401030), nat_list_succeeds(_401028)], (2446 ^ _315349) ^ [] : [_400887 = nil]]], (1054 ^ _315349) ^ [_350324, _350326, _350328] : [times_succeeds(_350328, _350326, _350324), times_fails(_350328, _350326, _350324)], (788 ^ _315349) ^ [_341348, _341350] : [_341350 = _341348, -(lh(_341350) = lh(_341348))], (4333 ^ _315349) ^ [_464112, _464114, _464116] : [-(_464114 = _464112), length_succeeds(_464116, _464114), length_succeeds(_464116, _464112)], (1160 ^ _315349) ^ [_353802, _353804, _353806] : [-(member2_fails(_353806, _353804, _353802)), member_fails(_353806, _353802), member_fails(_353806, _353804)], (4351 ^ _315349) ^ [_464686] : [list_succeeds(_464686), -(nat_succeeds(lh(_464686)))], (3709 ^ _315349) ^ [_444292, _444294] : ['@<_succeeds'(_444294, _444292), -('@=<_succeeds'(_444294, _444292))], (3702 ^ _315349) ^ [_444010, _444012] : ['@<_succeeds'(_444012, _444010), -(@+(_444012, s(3705 ^ [_444010, _444012])) = _444010)], (20 ^ _315349) ^ [_316153, _316155, _316157, _316159, _316161, _316163] : [-(member2_fails(_316161, _316157, _316153)), member2_fails(_316163, _316159, _316155), _316163 = _316161, _316159 = _316157, _316155 = _316153], (3240 ^ _315349) ^ [_428833, _428835, _428837] : [nat_succeeds(_428833), -(plus_terminates(_428837, _428835, _428833))], (4193 ^ _315349) ^ [_459523, _459525, _459527] : [-(gr(_459523)), append_succeeds(_459527, _459525, _459523), gr(_459527), gr(_459525)], (2860 ^ _315349) ^ [_415818, _415820] : [-('@=<_succeeds'(_415820, _415818)), 2861 ^ _315349 : [(2862 ^ _315349) ^ [_415965, _415967] : [_415820 = s(_415967), _415818 = s(_415965), '@=<_succeeds'(_415967, _415965)], (2872 ^ _315349) ^ [] : [_415820 = '0']]], (1118 ^ _315349) ^ [_352440] : [nat_succeeds(_352440), nat_fails(_352440)], (3512 ^ _315349) ^ [_437844, _437846] : [-(@+(@*(_437846, _437844), _437846) = @*(_437846, s(_437844))), nat_succeeds(_437846), nat_succeeds(_437844)], (1276 ^ _315349) ^ [_358089, _358091, _358093] : [-(occ_fails(_358093, _358091, _358089)), 1281 ^ _315349 : [(1286 ^ _315349) ^ [] : [occ_fails(_358093, 1280 ^ [_358089, _358091, _358093], _358089)], (1284 ^ _315349) ^ [] : [_358093 = 1279 ^ [_358089, _358091, _358093]], (1282 ^ _315349) ^ [] : [-(_358091 = cons(1279 ^ [_358089, _358091, _358093], 1280 ^ [_358089, _358091, _358093]))]], 1291 ^ _315349 : [(1296 ^ _315349) ^ [] : [occ_fails(_358093, 1289 ^ [_358089, _358091, _358093], 1290 ^ [_358089, _358091, _358093])], (1294 ^ _315349) ^ [] : [-(_358089 = s(1290 ^ [_358089, _358091, _358093]))], (1292 ^ _315349) ^ [] : [-(_358091 = cons(_358093, 1289 ^ [_358089, _358091, _358093]))]], 1297 ^ _315349 : [(1300 ^ _315349) ^ [] : [-(_358089 = '0')], (1298 ^ _315349) ^ [] : [-(_358091 = nil)]]], (4783 ^ _315349) ^ [_479472, _479474, _479476, _479478] : [-(member_succeeds(_479476, _479474)), delete_succeeds(_479478, _479474, _479472), member_succeeds(_479476, _479472)], (2025 ^ _315349) ^ [_385906, _385908] : [-(length_terminates(_385908, _385906)), 2051 ^ _315349 : [(2054 ^ _315349) ^ [] : [true___], (2052 ^ _315349) ^ [] : [-(true___)]], 2055 ^ _315349 : [(2060 ^ _315349) ^ [] : [true___], (2058 ^ _315349) ^ [] : [-(true___)], (2056 ^ _315349) ^ [] : [-(_385908 = nil)]], 2033 ^ _315349 : [(2036 ^ _315349) ^ [] : [true___], (2034 ^ _315349) ^ [] : [-(true___)]], 2037 ^ _315349 : [(2040 ^ _315349) ^ [] : [2041 ^ _315349 : [(2044 ^ _315349) ^ [] : [true___], (2042 ^ _315349) ^ [] : [-(true___)]], 2045 ^ _315349 : [(2048 ^ _315349) ^ [] : [length_terminates(2029 ^ [_385906, _385908], 2030 ^ [_385906, _385908])], (2046 ^ _315349) ^ [] : [-(_385906 = s(2030 ^ [_385906, _385908]))]]], (2038 ^ _315349) ^ [] : [-(_385908 = cons(2028 ^ [_385906, _385908], 2029 ^ [_385906, _385908]))]]], (98 ^ _315349) ^ [_318675, _318677, _318679, _318681] : [-(not_same_occ_succeeds(_318679, _318675)), not_same_occ_succeeds(_318681, _318677), _318681 = _318679, _318677 = _318675], (4485 ^ _315349) ^ [_469299, _469301, _469303, _469305] : [-(member_succeeds(_469305, _469299)), append_succeeds(_469303, _469301, _469299), member_succeeds(_469305, _469303)], (2142 ^ _315349) ^ [_390582, _390584, _390586] : [append_terminates(_390586, _390584, _390582), 2145 ^ _315349 : [(2152 ^ _315349) ^ [_391020, _391022, _391024] : [_390586 = cons(_391024, _391022), 2155 ^ _315349 : [(2162 ^ _315349) ^ [] : [_390582 = cons(_391024, _391020), -(append_terminates(_391022, _390584, _391020))], (2156 ^ _315349) ^ [] : [true___, -(true___)]]], (2168 ^ _315349) ^ [] : [true___, -(true___)], (2146 ^ _315349) ^ [_390840, _390842, _390844] : [true___, -(true___)], (2174 ^ _315349) ^ [] : [_390586 = nil, true___, -(true___)]]], (1682 ^ _315349) ^ [_372949, _372951] : [-(permutation_fails(_372951, _372949)), 1688 ^ _315349 : [(1693 ^ _315349) ^ [] : [permutation_fails(1687 ^ [_372949, _372951], 1686 ^ [_372949, _372951])], (1691 ^ _315349) ^ [] : [delete_fails(1685 ^ [_372949, _372951], _372951, 1687 ^ [_372949, _372951])], (1689 ^ _315349) ^ [] : [-(_372949 = cons(1685 ^ [_372949, _372951], 1686 ^ [_372949, _372951]))]], 1694 ^ _315349 : [(1697 ^ _315349) ^ [] : [-(_372949 = nil)], (1695 ^ _315349) ^ [] : [-(_372951 = nil)]]], (622 ^ _315349) ^ [_335624, _335626, _335628, _335630, _335632, _335634] : [-(member2_terminates(_335632, _335628, _335624)), member2_terminates(_335634, _335630, _335626), _335634 = _335632, _335630 = _335628, _335626 = _335624], (3777 ^ _315349) ^ [_446251, _446253, _446255] : [-('@<_succeeds'(_446255, _446251)), '@=<_succeeds'(_446255, _446253), '@<_succeeds'(_446253, _446251)], (3359 ^ _315349) ^ [_432882, _432884] : [-(@+(_432884, s(_432882)) = @+(s(_432884), _432882)), nat_succeeds(_432884), nat_succeeds(_432882)], (3284 ^ _315349) ^ [_430399, _430401, _430403] : [-(gr(_430399)), plus_succeeds(_430403, _430401, _430399), gr(_430401)], (4091 ^ _315349) ^ [_455994, _455996] : [-(list_succeeds(cons(_455996, cons(_455994, nil))))], (270 ^ _315349) ^ [_324260, _324262, _324264, _324266, _324268, _324270] : [-(times_terminates(_324268, _324264, _324260)), times_terminates(_324270, _324266, _324262), _324270 = _324268, _324266 = _324264, _324262 = _324260], (3641 ^ _315349) ^ [_442019, _442021] : [nat_succeeds(_442021), nat_succeeds(_442019), -('@<_succeeds'(_442021, _442019)), -(_442021 = _442019), -('@<_succeeds'(_442019, _442021))], (4721 ^ _315349) ^ [_477111, _477113, _477115] : [list_succeeds(_477113), -(delete_succeeds(_477115, _477113 ** cons(_477115, _477111), _477113 ** _477111))], (658 ^ _315349) ^ [_336842, _336844, _336846, _336848, _336850, _336852] : [-(member2_succeeds(_336850, _336846, _336842)), member2_succeeds(_336852, _336848, _336844), _336852 = _336850, _336848 = _336846, _336844 = _336842], (3411 ^ _315349) ^ [_434632, _434634, _434636] : [-(gr(_434632)), times_succeeds(_434636, _434634, _434632), gr(_434634)], (4495 ^ _315349) ^ [_469648, _469650, _469652, _469654] : [-(member_succeeds(_469654, _469648)), append_succeeds(_469652, _469650, _469648), member_succeeds(_469654, _469650)], (996 ^ _315349) ^ [_348575, _348577, _348579] : [append_terminates(_348579, _348577, _348575), -(append_succeeds(_348579, _348577, _348575)), -(append_fails(_348579, _348577, _348575))], (4343 ^ _315349) ^ [] : [-(lh(nil) = '0')], (242 ^ _315349) ^ [_323300, _323302] : [-(nat_terminates(_323300)), _323302 = _323300, nat_terminates(_323302)], (4367 ^ _315349) ^ [_465167, _465169] : [-(_465167 = cons(4374 ^ [_465167, _465169], 4375 ^ [_465167, _465169])), list_succeeds(_465167), lh(_465167) = s(_465169)], (4901 ^ _315349) ^ [_483283, _483285, _483287] : [list_succeeds(_483285), 4904 ^ _315349 : [(4911 ^ _315349) ^ [] : [occ_succeeds(_483287, _483285, _483283), -(occ(_483287, _483285) = _483283)], (4905 ^ _315349) ^ [] : [occ(_483287, _483285) = _483283, -(occ_succeeds(_483287, _483285, _483283))]]], (232 ^ _315349) ^ [_323005, _323007] : [-(nat_fails(_323005)), _323007 = _323005, nat_fails(_323007)], (1246 ^ _315349) ^ [_357049, _357051, _357053] : [occ_fails(_357053, _357051, _357049), 1249 ^ _315349 : [(1260 ^ _315349) ^ [_357643, _357645] : [_357051 = cons(_357053, _357645), _357049 = s(_357643), -(occ_fails(_357053, _357645, _357643))], (1270 ^ _315349) ^ [] : [_357051 = nil, _357049 = '0'], (1250 ^ _315349) ^ [_357297, _357299] : [_357051 = cons(_357299, _357297), -(_357053 = _357299), -(occ_fails(_357053, _357297, _357049))]]], (926 ^ _315349) ^ [_346238, _346240] : [same_occ_succeeds(_346240, _346238), same_occ_fails(_346240, _346238)], (4278 ^ _315349) ^ [_462253, _462255] : [4285 ^ _315349 : [(4288 ^ _315349) ^ [] : [-(gr(_462253))], (4286 ^ _315349) ^ [] : [-(gr(_462255))]], list_succeeds(_462255), gr(_462255 ** _462253)], (848 ^ _315349) ^ [_343674] : [gr(_343674), -(gr(s(_343674)))], (4326 ^ _315349) ^ [_463845] : [list_succeeds(_463845), -(length_succeeds(_463845, 4329 ^ [_463845]))], (3272 ^ _315349) ^ [_429935, _429937, _429939] : [plus_succeeds(_429939, _429937, _429935), -(plus_terminates(_429939, _429937, _429935))], (3544 ^ _315349) ^ [_438870, _438872, _438874] : [-(@*(_438870, @+(_438874, _438872)) = @+(@*(_438870, _438874), @*(_438870, _438872))), nat_succeeds(_438874), nat_succeeds(_438872), nat_succeeds(_438870)], (552 ^ _315349) ^ [_333376, _333378, _333380, _333382] : [-(length_succeeds(_333380, _333376)), length_succeeds(_333382, _333378), _333382 = _333380, _333378 = _333376], (498 ^ _315349) ^ [_331577, _331579, _331581, _331583, _331585, _331587] : [-(plus_succeeds(_331585, _331581, _331577)), plus_succeeds(_331587, _331583, _331579), _331587 = _331585, _331583 = _331581, _331579 = _331577], (4053 ^ _315349) ^ [_454905, _454907, _454909] : [-('@=<_succeeds'(_454907, _454905)), nat_succeeds(_454909), nat_succeeds(_454907), nat_succeeds(_454905), '@=<_succeeds'(@*(s(_454909), _454907), @*(s(_454909), _454905))], (3458 ^ _315349) ^ [_436160, _436162] : [-(@*(s(_436162), _436160) = @+(_436160, @*(_436162, _436160))), nat_succeeds(_436162), nat_succeeds(_436160)], (1924 ^ _315349) ^ [_382405, _382407] : [-(length_succeeds(_382407, _382405)), 1925 ^ _315349 : [(1926 ^ _315349) ^ [_382578, _382580, _382582] : [_382407 = cons(_382582, _382580), _382405 = s(_382578), length_succeeds(_382580, _382578)], (1936 ^ _315349) ^ [] : [_382407 = nil, _382405 = '0']]], (3609 ^ _315349) ^ [_441043] : [nat_succeeds(_441043), -('@<_fails'(_441043, _441043))], (3478 ^ _315349) ^ [_436790, _436792, _436794] : [-(@*(@+(_436794, _436792), _436790) = @+(@*(_436794, _436790), @*(_436792, _436790))), nat_succeeds(_436794), nat_succeeds(_436792), nat_succeeds(_436790)], (186 ^ _315349) ^ [_321492, _321494] : [-(nat_list_fails(_321492)), _321494 = _321492, nat_list_fails(_321494)], (3009 ^ _315349) ^ [_421151, _421153] : ['@<_fails'(_421153, _421151), 3012 ^ _315349 : [(3013 ^ _315349) ^ [_421364, _421366] : [_421153 = s(_421366), _421151 = s(_421364), -('@<_fails'(_421366, _421364))], (3023 ^ _315349) ^ [_421665] : [_421153 = '0', _421151 = s(_421665)]]], (1642 ^ _315349) ^ [_371571, _371573] : [-(permutation_succeeds(_371573, _371571)), 1643 ^ _315349 : [(1644 ^ _315349) ^ [_371743, _371745, _371747] : [_371571 = cons(_371747, _371745), delete_succeeds(_371747, _371573, _371743), permutation_succeeds(_371743, _371745)], (1654 ^ _315349) ^ [] : [_371573 = nil, _371571 = nil]]], (2450 ^ _315349) ^ [_401450] : [nat_list_fails(_401450), 2453 ^ _315349 : [(2454 ^ _315349) ^ [_401637, _401639] : [_401450 = cons(_401639, _401637), -(nat_fails(_401639)), -(nat_list_fails(_401637))], (2464 ^ _315349) ^ [] : [_401450 = nil]]], (3659 ^ _315349) ^ [_442482] : [-('@<_succeeds'('0', _442482)), nat_succeeds(_442482), -(_442482 = '0')], (4645 ^ _315349) ^ [_474504] : [nat_list_succeeds(_474504), -(gr(_474504))], (480 ^ _315349) ^ [_330968, _330970, _330972, _330974, _330976, _330978] : [-(delete_succeeds(_330976, _330972, _330968)), delete_succeeds(_330978, _330974, _330970), _330978 = _330976, _330974 = _330972, _330970 = _330968], (2908 ^ _315349) ^ [_417642, _417644] : ['@=<_terminates'(_417644, _417642), 2911 ^ _315349 : [(2918 ^ _315349) ^ [_418027, _418029] : [_417644 = s(_418029), 2921 ^ _315349 : [(2928 ^ _315349) ^ [] : [_417642 = s(_418027), -('@=<_terminates'(_418029, _418027))], (2922 ^ _315349) ^ [] : [true___, -(true___)]]], (2912 ^ _315349) ^ [_417861, _417863] : [true___, -(true___)], (2934 ^ _315349) ^ [] : [true___, -(true___)]]], (932 ^ _315349) ^ [_346447, _346449] : [same_occ_terminates(_346449, _346447), -(same_occ_succeeds(_346449, _346447)), -(same_occ_fails(_346449, _346447))], (1028 ^ _315349) ^ [_349571] : [list_terminates(_349571), -(list_succeeds(_349571)), -(list_fails(_349571))], (1776 ^ _315349) ^ [_376375, _376377, _376379] : [delete_succeeds(_376379, _376377, _376375), 1784 ^ _315349 : [(1789 ^ _315349) ^ [] : [-(delete_succeeds(_376379, 1782 ^ [_376375, _376377, _376379], 1783 ^ [_376375, _376377, _376379]))], (1787 ^ _315349) ^ [] : [-(_376375 = cons(1781 ^ [_376375, _376377, _376379], 1783 ^ [_376375, _376377, _376379]))], (1785 ^ _315349) ^ [] : [-(_376377 = cons(1781 ^ [_376375, _376377, _376379], 1782 ^ [_376375, _376377, _376379]))]], -(_376377 = cons(_376379, _376375))], (4665 ^ _315349) ^ [_475210, _475212, _475214, _475216] : [-('@<_succeeds'(@+(lh(_475216), lh(_475212)), _475210)), list_succeeds(_475216), list_succeeds(_475212), '@<_succeeds'(@+(lh(_475216), lh(cons(_475214, _475212))), s(_475210))], (4701 ^ _315349) ^ [_476455, _476457, _476459] : [-(list_succeeds(_476457)), delete_succeeds(_476459, _476457, _476455), list_succeeds(_476455)], (3993 ^ _315349) ^ [_453097, _453099, _453101, _453103] : [-('@<_succeeds'(@+(_453103, _453101), @+(_453099, _453097))), '@<_succeeds'(_453103, _453099), '@<_succeeds'(_453101, _453097), nat_succeeds(_453099)], (3688 ^ _315349) ^ [_443458, _443460] : ['@=<_succeeds'(_443460, _443458), -(@+(_443460, 3691 ^ [_443458, _443460]) = _443458)], (3576 ^ _315349) ^ [_439920, _439922] : ['@<_succeeds'(_439922, _439920), -(_439920 = s(3579 ^ [_439920, _439922]))], (1793 ^ _315349) ^ [_377154, _377156, _377158] : [-(delete_succeeds(_377158, _377156, _377154)), 1794 ^ _315349 : [(1795 ^ _315349) ^ [_377329, _377331, _377333] : [_377156 = cons(_377333, _377331), _377154 = cons(_377333, _377329), delete_succeeds(_377158, _377331, _377329)], (1805 ^ _315349) ^ [] : [_377156 = cons(_377158, _377154)]]], (838 ^ _315349) ^ [_343319, _343321, _343323, _343325] : [cons(_343325, _343323) = cons(_343321, _343319), -(_343325 = _343321)], (2348 ^ _315349) ^ [_398029] : [list_fails(_398029), 2351 ^ _315349 : [(2352 ^ _315349) ^ [_398211, _398213] : [_398029 = cons(_398213, _398211), -(list_fails(_398211))], (2358 ^ _315349) ^ [] : [_398029 = nil]]], (4459 ^ _315349) ^ [_468241] : [-(sub(nil, _468241))], (4763 ^ _315349) ^ [_478791, _478793, _478795, _478797] : [delete_succeeds(_478797, _478793, _478791), member_succeeds(_478795, _478793), -(member_succeeds(_478795, _478791)), -(_478795 = _478797)], (1124 ^ _315349) ^ [_352625] : [nat_terminates(_352625), -(nat_succeeds(_352625)), -(nat_fails(_352625))], (1623 ^ _315349) ^ [_370790, _370792] : [permutation_succeeds(_370792, _370790), 1631 ^ _315349 : [(1636 ^ _315349) ^ [] : [-(permutation_succeeds(1630 ^ [_370790, _370792], 1629 ^ [_370790, _370792]))], (1634 ^ _315349) ^ [] : [-(delete_succeeds(1628 ^ [_370790, _370792], _370792, 1630 ^ [_370790, _370792]))], (1632 ^ _315349) ^ [] : [-(_370790 = cons(1628 ^ [_370790, _370792], 1629 ^ [_370790, _370792]))]], 1637 ^ _315349 : [(1640 ^ _315349) ^ [] : [-(_370790 = nil)], (1638 ^ _315349) ^ [] : [-(_370792 = nil)]]], (2806 ^ _315349) ^ [_413892, _413894, _413896] : [-(plus_terminates(_413896, _413894, _413892)), 2831 ^ _315349 : [(2834 ^ _315349) ^ [] : [true___], (2832 ^ _315349) ^ [] : [-(true___)]], 2835 ^ _315349 : [(2840 ^ _315349) ^ [] : [true___], (2838 ^ _315349) ^ [] : [-(true___)], (2836 ^ _315349) ^ [] : [-(_413896 = '0')]], 2813 ^ _315349 : [(2816 ^ _315349) ^ [] : [true___], (2814 ^ _315349) ^ [] : [-(true___)]], 2817 ^ _315349 : [(2820 ^ _315349) ^ [] : [2821 ^ _315349 : [(2824 ^ _315349) ^ [] : [true___], (2822 ^ _315349) ^ [] : [-(true___)]], 2825 ^ _315349 : [(2828 ^ _315349) ^ [] : [plus_terminates(2809 ^ [_413892, _413894, _413896], _413894, 2810 ^ [_413892, _413894, _413896])], (2826 ^ _315349) ^ [] : [-(_413892 = s(2810 ^ [_413892, _413894, _413896]))]]], (2818 ^ _315349) ^ [] : [-(_413896 = s(2809 ^ [_413892, _413894, _413896]))]]], (3395 ^ _315349) ^ [_434081, _434083, _434085] : [-(nat_succeeds(_434081)), times_succeeds(_434085, _434083, _434081), nat_succeeds(_434083)], (3222 ^ _315349) ^ [_428203] : [nat_succeeds(_428203), -(nat_terminates(_428203))], (832 ^ _315349) ^ [_343057, _343059, _343061, _343063] : [cons(_343063, _343061) = cons(_343059, _343057), -(_343061 = _343057)], (344 ^ _315349) ^ [_326589, _326591] : [-(list_terminates(_326589)), _326591 = _326589, list_terminates(_326591)], (2876 ^ _315349) ^ [_416424, _416426] : ['@=<_fails'(_416426, _416424), 2879 ^ _315349 : [(2880 ^ _315349) ^ [_416622, _416624] : [_416426 = s(_416624), _416424 = s(_416622), -('@=<_fails'(_416624, _416622))], (2890 ^ _315349) ^ [] : [_416426 = '0']]], (3452 ^ _315349) ^ [_435952] : [nat_succeeds(_435952), -(@*('0', _435952) = '0')], (4691 ^ _315349) ^ [_476134, _476136, _476138] : [-(list_succeeds(_476134)), delete_succeeds(_476138, _476136, _476134), list_succeeds(_476136)], (4187 ^ _315349) ^ [_459293, _459295, _459297] : [list_succeeds(_459293), -(append_terminates(_459297, _459295, _459293))], (690 ^ _315349) ^ [_337839, _337841] : [-(gr(_337839)), _337841 = _337839, gr(_337841)], (4477 ^ _315349) ^ [_468919, _468921] : [member_succeeds(_468921, _468919), -(append_succeeds(4480 ^ [_468919, _468921], cons(_468921, 4481 ^ [_468919, _468921]), _468919))], (3294 ^ _315349) ^ [_430720, _430722, _430724] : [-(gr(_430722)), plus_succeeds(_430724, _430722, _430720), gr(_430720)], (814 ^ _315349) ^ [] : ['0' = nil], (2299 ^ _315349) ^ [_396296, _396298] : [-(member_terminates(_396298, _396296)), 2315 ^ _315349 : [(2318 ^ _315349) ^ [] : [true___], (2316 ^ _315349) ^ [] : [-(true___)]], 2306 ^ _315349 : [(2309 ^ _315349) ^ [] : [true___], (2307 ^ _315349) ^ [] : [-(true___)]], 2310 ^ _315349 : [(2313 ^ _315349) ^ [] : [member_terminates(_396298, 2303 ^ [_396296, _396298])], (2311 ^ _315349) ^ [] : [-(_396296 = cons(2302 ^ [_396296, _396298], 2303 ^ [_396296, _396298]))]]], (4591 ^ _315349) ^ [_472862, _472864, _472866, _472868] : [-(_472868 = _472862), append_succeeds(_472868, _472866, _472864), append_succeeds(_472862, _472866, _472864), list_succeeds(_472864)], (4071 ^ _315349) ^ [_455428, _455430, _455432] : [-(_455432 = _455430), nat_succeeds(_455432), nat_succeeds(_455430), nat_succeeds(_455428), @+(_455432, _455428) = @+(_455430, _455428)], (3142 ^ _315349) ^ [_425688] : [-(nat_succeeds(_425688)), 3143 ^ _315349 : [(3144 ^ _315349) ^ [_425804] : [_425688 = s(_425804), nat_succeeds(_425804)], (3150 ^ _315349) ^ [] : [_425688 = '0']]], (4969 ^ _315349) ^ [_485421, _485423, _485425] : [-(gr(_485425)), member2_succeeds(_485425, _485423, _485421), gr(_485423), gr(_485421)], (1092 ^ _315349) ^ [_351645, _351647] : ['@=<_terminates'(_351647, _351645), -('@=<_succeeds'(_351647, _351645)), -('@=<_fails'(_351647, _351645))], (1038 ^ _315349) ^ [_349841] : [nat_list_succeeds(_349841), nat_list_fails(_349841)], (1587 ^ _315349) ^ [_369665, _369667] : [same_occ_fails(_369667, _369665), -(not_same_occ_succeeds(_369667, _369665))], (3695 ^ _315349) ^ [_443734, _443736] : ['@<_succeeds'(_443736, _443734), -(plus_succeeds(_443736, s(3698 ^ [_443734, _443736]), _443734))], (414 ^ _315349) ^ [_328853, _328855, _328857, _328859] : [-('@=<_succeeds'(_328857, _328853)), '@=<_succeeds'(_328859, _328855), _328859 = _328857, _328855 = _328853], (1076 ^ _315349) ^ [_351120, _351122, _351124] : [plus_terminates(_351124, _351122, _351120), -(plus_succeeds(_351124, _351122, _351120)), -(plus_fails(_351124, _351122, _351120))], (1216 ^ _315349) ^ [_355929, _355931, _355933] : [-(occ_succeeds(_355933, _355931, _355929)), 1217 ^ _315349 : [(1228 ^ _315349) ^ [_356466, _356468] : [_355931 = cons(_355933, _356468), _355929 = s(_356466), occ_succeeds(_355933, _356468, _356466)], (1238 ^ _315349) ^ [] : [_355931 = nil, _355929 = '0'], (1218 ^ _315349) ^ [_356121, _356123] : [_355931 = cons(_356123, _356121), -(_355933 = _356123), occ_succeeds(_355933, _356121, _355929)]]], (5033 ^ _315349) ^ [_487292, _487294] : [list_succeeds(_487292), -(occ_succeeds(_487294, _487292, 5036 ^ [_487292, _487294]))], (3845 ^ _315349) ^ [_448454, _448456, _448458] : [-('@<_succeeds'(@+(_448458, _448454), @+(_448456, _448454))), '@<_succeeds'(_448458, _448456), nat_succeeds(_448456), nat_succeeds(_448454)], (4623 ^ _315349) ^ [_473823, _473825, _473827, _473829] : [-(_473827 = _473823), append_succeeds(_473829, _473827, _473825), append_succeeds(_473829, _473823, _473825)], (676 ^ _315349) ^ [_337423, _337425, _337427, _337429] : [-(not_same_occ_terminates(_337427, _337423)), not_same_occ_terminates(_337429, _337425), _337429 = _337427, _337425 = _337423], (4300 ^ _315349) ^ [_462954] : [list_succeeds(_462954), -(_462954 ** nil = _462954)], (1170 ^ _315349) ^ [_354158, _354160, _354162] : [member2_terminates(_354162, _354160, _354158), 1173 ^ _315349 : [(1176 ^ _315349) ^ [] : [-(member_terminates(_354162, _354160))], (1174 ^ _315349) ^ [] : [-(member_terminates(_354162, _354158))]]], (566 ^ _315349) ^ [_333820, _333822, _333824, _333826] : [-(sub(_333824, _333820)), sub(_333826, _333822), _333826 = _333824, _333822 = _333820], (3389 ^ _315349) ^ [_433851, _433853, _433855] : [times_succeeds(_433855, _433853, _433851), -(nat_succeeds(_433855))], (2223 ^ _315349) ^ [_393379, _393381] : [member_succeeds(_393381, _393379), 2230 ^ _315349 : [(2233 ^ _315349) ^ [] : [-(member_succeeds(_393381, 2229 ^ [_393379, _393381]))], (2231 ^ _315349) ^ [] : [-(_393379 = cons(2228 ^ [_393379, _393381], 2229 ^ [_393379, _393381]))]], -(_393379 = cons(_393381, 2234 ^ [_393379, _393381]))], (4525 ^ _315349) ^ [_470651, _470653, _470655, _470657] : [append_succeeds(_470655, cons(_470657, _470653), _470651), -(member_succeeds(_470657, _470651))], (4882 ^ _315349) ^ [_482598, _482600] : [sub(_482600, _482598), 4885 ^ _315349 : [(4886 ^ _315349) ^ [_482735] : [member_succeeds(_482735, _482600), -(member_succeeds(_482735, _482598))]]], (894 ^ _315349) ^ [_345180, _345182, _345184] : [occ_succeeds(_345184, _345182, _345180), occ_fails(_345184, _345182, _345180)], (3903 ^ _315349) ^ [_450225, _450227] : [-('@=<_succeeds'(_450225, @+(_450227, _450225))), nat_succeeds(_450227), nat_succeeds(_450225)], (3339 ^ _315349) ^ [_432268, _432270, _432272] : [-(@+(@+(_432272, _432270), _432268) = @+(_432272, @+(_432270, _432268))), nat_succeeds(_432272), nat_succeeds(_432270), nat_succeeds(_432268)], (724 ^ _315349) ^ [_338929, _338931, _338933, _338935, _338937, _338939] : [-(occ_succeeds(_338937, _338933, _338929)), occ_succeeds(_338939, _338935, _338931), _338939 = _338937, _338935 = _338933, _338931 = _338929], (1581 ^ _315349) ^ [_369424, _369426] : [not_same_occ_fails(_369426, _369424), -(same_occ_succeeds(_369426, _369424))], (2688 ^ _315349) ^ [_409725, _409727, _409729] : [plus_succeeds(_409729, _409727, _409725), 2695 ^ _315349 : [(2700 ^ _315349) ^ [] : [-(plus_succeeds(2693 ^ [_409725, _409727, _409729], _409727, 2694 ^ [_409725, _409727, _409729]))], (2698 ^ _315349) ^ [] : [-(_409725 = s(2694 ^ [_409725, _409727, _409729]))], (2696 ^ _315349) ^ [] : [-(_409729 = s(2693 ^ [_409725, _409727, _409729]))]], 2701 ^ _315349 : [(2704 ^ _315349) ^ [] : [-(_409725 = _409727)], (2702 ^ _315349) ^ [] : [-(_409729 = '0')]]], (4425 ^ _315349) ^ [_467124, _467126, _467128] : [-('@=<_succeeds'(lh(_467128), lh(_467124))), append_succeeds(_467128, _467126, _467124), list_succeeds(_467124)], (4320 ^ _315349) ^ [_463651, _463653] : [length_succeeds(_463653, _463651), -(gr(_463651))], (4169 ^ _315349) ^ [_458667, _458669, _458671] : [4176 ^ _315349 : [(4179 ^ _315349) ^ [] : [-(list_succeeds(_458669))], (4177 ^ _315349) ^ [] : [-(list_succeeds(_458671))]], append_succeeds(_458671, _458669, _458667), list_succeeds(_458667)], (158 ^ _315349) ^ [_320644, _320646, _320648, _320650, _320652, _320654] : [-(append_fails(_320652, _320648, _320644)), append_fails(_320654, _320650, _320646), _320654 = _320652, _320650 = _320648, _320646 = _320644], (470 ^ _315349) ^ [_330617, _330619] : [-(nat_list_succeeds(_330617)), _330619 = _330617, nat_list_succeeds(_330619)], (608 ^ _315349) ^ [_335152, _335154, _335156, _335158] : [-(permutation_terminates(_335156, _335152)), permutation_terminates(_335158, _335154), _335158 = _335156, _335154 = _335152], (3228 ^ _315349) ^ [_428389] : [nat_succeeds(_428389), -(gr(_428389))], (4447 ^ _315349) ^ [_467840] : [-(sub(_467840, _467840))], (4989 ^ _315349) ^ [_486049, _486051] : [-(not_same_occ_terminates(_486051, _486049)), list_succeeds(_486051), list_succeeds(_486049), gr(_486051), gr(_486049)], (1070 ^ _315349) ^ [_350887, _350889, _350891] : [plus_succeeds(_350891, _350889, _350887), plus_fails(_350891, _350889, _350887)], (900 ^ _315349) ^ [_345413, _345415, _345417] : [occ_terminates(_345417, _345415, _345413), -(occ_succeeds(_345417, _345415, _345413)), -(occ_fails(_345417, _345415, _345413))], (4925 ^ _315349) ^ [_484064, _484066, _484068] : [-(permutation_terminates(_484066, _484064)), nat_succeeds(_484068), list_succeeds(_484066), lh(_484066) = _484068], (2940 ^ _315349) ^ [_418607, _418609] : [-('@=<_terminates'(_418609, _418607)), 2963 ^ _315349 : [(2966 ^ _315349) ^ [] : [true___], (2964 ^ _315349) ^ [] : [-(true___)]], 2947 ^ _315349 : [(2950 ^ _315349) ^ [] : [true___], (2948 ^ _315349) ^ [] : [-(true___)]], 2951 ^ _315349 : [(2954 ^ _315349) ^ [] : [2955 ^ _315349 : [(2958 ^ _315349) ^ [] : [true___], (2956 ^ _315349) ^ [] : [-(true___)]], 2959 ^ _315349 : [(2962 ^ _315349) ^ [] : ['@=<_terminates'(2943 ^ [_418607, _418609], 2944 ^ [_418607, _418609])], (2960 ^ _315349) ^ [] : [-(_418607 = s(2944 ^ [_418607, _418609]))]]], (2952 ^ _315349) ^ [] : [-(_418609 = s(2943 ^ [_418607, _418609]))]]], (3721 ^ _315349) ^ [_444690, _444692] : [nat_succeeds(_444692), nat_succeeds(_444690), -('@=<_succeeds'(_444692, _444690)), -('@=<_succeeds'(_444690, _444692))], (3405 ^ _315349) ^ [_434402, _434404, _434406] : [times_succeeds(_434406, _434404, _434402), -(gr(_434406))], (3923 ^ _315349) ^ [_450873, _450875, _450877] : [-('@<_succeeds'(_450877, _450875)), nat_succeeds(_450877), nat_succeeds(_450875), nat_succeeds(_450873), '@<_succeeds'(@+(_450877, _450873), @+(_450875, _450873))], (4983 ^ _315349) ^ [_485833, _485835, _485837] : [occ_succeeds(_485837, _485835, _485833), -(gr(_485833))], (4238 ^ _315349) ^ [_461031, _461033, _461035] : [list_succeeds(_461033), -(cons(_461035, _461033) ** _461031 = cons(_461035, _461033 ** _461031))], (4639 ^ _315349) ^ [_474318] : [nat_list_succeeds(_474318), -(nat_list_terminates(_474318))], (2466 ^ _315349) ^ [_401955] : [-(nat_list_fails(_401955)), 2471 ^ _315349 : [(2476 ^ _315349) ^ [] : [nat_list_fails(2470 ^ [_401955])], (2474 ^ _315349) ^ [] : [nat_fails(2469 ^ [_401955])], (2472 ^ _315349) ^ [] : [-(_401955 = cons(2469 ^ [_401955], 2470 ^ [_401955]))]], -(_401955 = nil)], (112 ^ _315349) ^ [_319119, _319121, _319123, _319125] : [-(permutation_fails(_319123, _319119)), permutation_fails(_319125, _319121), _319125 = _319123, _319121 = _319119], (4133 ^ _315349) ^ [_457453, _457455, _457457, _457459] : [-(member_succeeds(_457459, _457453)), member_succeeds(_457459, cons(_457457, _457453)), -(_457459 = _457457)], (3492 ^ _315349) ^ [_437230, _437232, _437234] : [-(@*(@*(_437234, _437232), _437230) = @*(_437234, @*(_437232, _437230))), nat_succeeds(_437234), nat_succeeds(_437232), nat_succeeds(_437230)], (1178 ^ _315349) ^ [_354405, _354407, _354409] : [-(member2_terminates(_354409, _354407, _354405)), member_terminates(_354409, _354405), member_terminates(_354409, _354407)], (4345 ^ _315349) ^ [_464474, _464476] : [list_succeeds(_464474), -(lh(cons(_464476, _464474)) = s(lh(_464474)))], (3681 ^ _315349) ^ [_443188, _443190] : ['@=<_succeeds'(_443190, _443188), -(plus_succeeds(_443190, 3684 ^ [_443188, _443190], _443188))], (3735 ^ _315349) ^ [_445077, _445079] : [nat_succeeds(_445079), nat_succeeds(_445077), -('@<_succeeds'(_445079, _445077)), -('@=<_succeeds'(_445077, _445079))], (2538 ^ _315349) ^ [_404352, _404354, _404356] : [times_succeeds(_404356, _404354, _404352), 2545 ^ _315349 : [(2550 ^ _315349) ^ [] : [-(plus_succeeds(_404354, 2544 ^ [_404352, _404354, _404356], _404352))], (2548 ^ _315349) ^ [] : [-(times_succeeds(2543 ^ [_404352, _404354, _404356], _404354, 2544 ^ [_404352, _404354, _404356]))], (2546 ^ _315349) ^ [] : [-(_404356 = s(2543 ^ [_404352, _404354, _404356]))]], 2551 ^ _315349 : [(2554 ^ _315349) ^ [] : [-(_404352 = '0')], (2552 ^ _315349) ^ [] : [-(_404356 = '0')]]], (1506 ^ _315349) ^ [_366681, _366683] : [not_same_occ_terminates(_366683, _366681), 1509 ^ _315349 : [(1512 ^ _315349) ^ [_366972, _366974, _366976] : [-(member2_fails(_366976, _366683, _366681)), 1515 ^ _315349 : [(1518 ^ _315349) ^ [] : [-(occ_fails(_366976, _366683, _366974)), 1521 ^ _315349 : [(1524 ^ _315349) ^ [] : [-(occ_fails(_366976, _366681, _366972)), 1527 ^ _315349 : [(1528 ^ _315349) ^ [] : [true___, -(true___)], (1536 ^ _315349) ^ [] : [-(gr(_366972))], (1534 ^ _315349) ^ [] : [-(gr(_366974))]]], (1522 ^ _315349) ^ [] : [-(occ_terminates(_366976, _366681, _366972))]]], (1516 ^ _315349) ^ [] : [-(occ_terminates(_366976, _366683, _366974))]]], (1510 ^ _315349) ^ [_366904, _366906, _366908] : [-(member2_terminates(_366908, _366683, _366681))]]], (822 ^ _315349) ^ [_342585, _342587] : [nil = cons(_342587, _342585)], (1739 ^ _315349) ^ [_374984, _374986] : [-(permutation_terminates(_374986, _374984)), 1763 ^ _315349 : [(1766 ^ _315349) ^ [] : [true___], (1764 ^ _315349) ^ [] : [-(true___)]], 1767 ^ _315349 : [(1772 ^ _315349) ^ [] : [true___], (1770 ^ _315349) ^ [] : [-(true___)], (1768 ^ _315349) ^ [] : [-(_374986 = nil)]], 1747 ^ _315349 : [(1750 ^ _315349) ^ [] : [true___], (1748 ^ _315349) ^ [] : [-(true___)]], 1751 ^ _315349 : [(1754 ^ _315349) ^ [] : [delete_terminates(1742 ^ [_374984, _374986], _374986, 1744 ^ [_374984, _374986]), 1757 ^ _315349 : [(1760 ^ _315349) ^ [] : [permutation_terminates(1744 ^ [_374984, _374986], 1743 ^ [_374984, _374986])], (1758 ^ _315349) ^ [] : [delete_fails(1742 ^ [_374984, _374986], _374986, 1744 ^ [_374984, _374986])]]], (1752 ^ _315349) ^ [] : [-(_374984 = cons(1742 ^ [_374984, _374986], 1743 ^ [_374984, _374986]))]]], (1144 ^ _315349) ^ [_353216, _353218, _353220] : [1145 ^ _315349 : [(1148 ^ _315349) ^ [] : [member_succeeds(_353220, _353218)], (1146 ^ _315349) ^ [] : [member_succeeds(_353220, _353216)]], -(member2_succeeds(_353220, _353218, _353216))], (2596 ^ _315349) ^ [_406435, _406437, _406439] : [-(times_fails(_406439, _406437, _406435)), 2601 ^ _315349 : [(2606 ^ _315349) ^ [] : [plus_fails(_406437, 2600 ^ [_406435, _406437, _406439], _406435)], (2604 ^ _315349) ^ [] : [times_fails(2599 ^ [_406435, _406437, _406439], _406437, 2600 ^ [_406435, _406437, _406439])], (2602 ^ _315349) ^ [] : [-(_406439 = s(2599 ^ [_406435, _406437, _406439]))]], 2607 ^ _315349 : [(2610 ^ _315349) ^ [] : [-(_406435 = '0')], (2608 ^ _315349) ^ [] : [-(_406439 = '0')]]], (4123 ^ _315349) ^ [_457130, _457132] : [-(gr(_457132)), member_succeeds(_457132, _457130), gr(_457130)], (5052 ^ _315349) ^ [] : [5054 ^ _315349 : [(5055 ^ _315349) ^ [] : [-(5053 ^ [] = nil), 5058 ^ _315349 : [(5063 ^ _315349) ^ [_488446, _488448] : [-(_488448 = _488446), -(occ(_488448, cons(_488446, 5057 ^ [])) = occ(_488448, 5057 ^ []))], (5061 ^ _315349) ^ [] : [-(list_succeeds(5057 ^ []))], (5059 ^ _315349) ^ [] : [-(5053 ^ [] = cons(5056 ^ [], 5057 ^ []))]]], (5075 ^ _315349) ^ [] : [occ(5070 ^ [], cons(5071 ^ [], 5053 ^ [])) = occ(5070 ^ [], 5053 ^ [])], (5073 ^ _315349) ^ [] : [5070 ^ [] = 5071 ^ []]], 5076 ^ _315349 : [(5077 ^ _315349) ^ [_488885] : [list_succeeds(_488885), 5080 ^ _315349 : [(5081 ^ _315349) ^ [_489046, _489048] : [-(_489048 = _489046), -(occ(_489048, cons(_489046, _488885)) = occ(_489048, _488885))]]]]], (1538 ^ _315349) ^ [_367785, _367787] : [-(not_same_occ_terminates(_367787, _367785)), member2_terminates(1539 ^ [_367785, _367787], _367787, _367785), 1546 ^ _315349 : [(1549 ^ _315349) ^ [] : [occ_terminates(1539 ^ [_367785, _367787], _367787, 1540 ^ [_367785, _367787]), 1552 ^ _315349 : [(1555 ^ _315349) ^ [] : [occ_terminates(1539 ^ [_367785, _367787], _367785, 1541 ^ [_367785, _367787]), 1558 ^ _315349 : [(1561 ^ _315349) ^ [] : [1562 ^ _315349 : [(1565 ^ _315349) ^ [] : [true___], (1563 ^ _315349) ^ [] : [-(true___)]], gr(1540 ^ [_367785, _367787]), gr(1541 ^ [_367785, _367787])], (1559 ^ _315349) ^ [] : [occ_fails(1539 ^ [_367785, _367787], _367785, 1541 ^ [_367785, _367787])]]], (1553 ^ _315349) ^ [] : [occ_fails(1539 ^ [_367785, _367787], _367787, 1540 ^ [_367785, _367787])]]], (1547 ^ _315349) ^ [] : [member2_fails(1539 ^ [_367785, _367787], _367787, _367785)]]], (4445 ^ _315349) ^ [_467757, _467759] : [-(sub(_467757, cons(_467759, _467757)))], (4800 ^ _315349) ^ [_480091, _480093, _480095, _480097] : [-(member_succeeds(_480095, _480091)), delete_succeeds(_480097, _480093, _480091), member_succeeds(_480095, _480093), -(_480097 = _480095)], (1108 ^ _315349) ^ [_352154, _352156] : ['@<_terminates'(_352156, _352154), -('@<_succeeds'(_352156, _352154)), -('@<_fails'(_352156, _352154))], (742 ^ _315349) ^ [_339462, _339464] : [-(list_succeeds(_339462)), _339464 = _339462, list_succeeds(_339464)], (3304 ^ _315349) ^ [_431027, _431029] : [nat_succeeds(_431029), -(plus_succeeds(_431029, _431027, 3307 ^ [_431027, _431029]))], (3669 ^ _315349) ^ [_442772, _442774] : [nat_succeeds(_442774), -('@=<_terminates'(_442774, _442772))], (5007 ^ _315349) ^ [_486518, _486520] : [-(same_occ_terminates(_486520, _486518)), list_succeeds(_486520), list_succeeds(_486518), gr(_486520), gr(_486518)], (778 ^ _315349) ^ [_341017, _341019, _341021, _341023] : [-(_341023 ** _341019 = _341021 ** _341017), _341023 = _341021, _341019 = _341017], (4 ^ _315349) ^ [_315580, _315582] : [_315582 = _315580, -(_315580 = _315582)], (4939 ^ _315349) ^ [_484466, _484468] : [list_succeeds(_484468), -(permutation_terminates(_484468, _484466))], (1599 ^ _315349) ^ [_370068, _370070] : [same_occ_terminates(_370070, _370068), 1602 ^ _315349 : [(1607 ^ _315349) ^ [] : [-(gr(_370068))], (1605 ^ _315349) ^ [] : [-(gr(_370070))], (1603 ^ _315349) ^ [] : [-(not_same_occ_terminates(_370070, _370068))]]], (252 ^ _315349) ^ [_323651, _323653, _323655, _323657, _323659, _323661] : [-(plus_terminates(_323659, _323655, _323651)), plus_terminates(_323661, _323657, _323653), _323661 = _323659, _323657 = _323655, _323653 = _323651], (1575 ^ _315349) ^ [_369262, _369264] : [same_occ_succeeds(_369264, _369262), -(not_same_occ_fails(_369264, _369262))], (4461 ^ _315349) ^ [_468362, _468364, _468366] : [-(sub(cons(_468366, _468364), _468362)), sub(_468364, _468362), member_succeeds(_468366, _468362)], (70 ^ _315349) ^ [_317787, _317789, _317791, _317793] : [-(not_same_occ_fails(_317791, _317787)), not_same_occ_fails(_317793, _317789), _317793 = _317791, _317789 = _317787], (958 ^ _315349) ^ [_347270, _347272, _347274] : [delete_succeeds(_347274, _347272, _347270), delete_fails(_347274, _347272, _347270)], (3797 ^ _315349) ^ [_446897, _446899, _446901] : [-('@=<_succeeds'(_446901, _446897)), '@=<_succeeds'(_446901, _446899), '@=<_succeeds'(_446899, _446897)], (580 ^ _315349) ^ [_334264, _334266, _334268, _334270] : [-(member_succeeds(_334268, _334264)), member_succeeds(_334270, _334266), _334270 = _334268, _334266 = _334264], (1701 ^ _315349) ^ [_373820, _373822] : [permutation_terminates(_373822, _373820), 1704 ^ _315349 : [(1729 ^ _315349) ^ [] : [_373822 = nil, true___, -(true___)], (1705 ^ _315349) ^ [_374071, _374073, _374075] : [true___, -(true___)], (1723 ^ _315349) ^ [] : [true___, -(true___)], (1711 ^ _315349) ^ [_374243, _374245, _374247] : [_373820 = cons(_374247, _374245), 1714 ^ _315349 : [(1717 ^ _315349) ^ [] : [-(delete_fails(_374247, _373822, _374243)), -(permutation_terminates(_374243, _374245))], (1715 ^ _315349) ^ [] : [-(delete_terminates(_374247, _373822, _374243))]]]]], (4581 ^ _315349) ^ [_472535, _472537] : [-(_472537 = nil), append_succeeds(_472537, _472535, _472535), list_succeeds(_472535)], (700 ^ _315349) ^ [_338162, _338164, _338166, _338168] : [-(same_occ_terminates(_338166, _338162)), same_occ_terminates(_338168, _338164), _338168 = _338166, _338164 = _338162], (1944 ^ _315349) ^ [_383132, _383134] : [length_fails(_383134, _383132), 1947 ^ _315349 : [(1948 ^ _315349) ^ [_383358, _383360, _383362] : [_383134 = cons(_383362, _383360), _383132 = s(_383358), -(length_fails(_383360, _383358))], (1958 ^ _315349) ^ [] : [_383134 = nil, _383132 = '0']]], (4415 ^ _315349) ^ [_466783, _466785, _466787] : [-(@+(lh(_466787), lh(_466785)) = lh(_466783)), append_succeeds(_466787, _466785, _466783), list_succeeds(_466783)], (974 ^ _315349) ^ [_347819, _347821] : [length_succeeds(_347821, _347819), length_fails(_347821, _347819)], (3431 ^ _315349) ^ [_435260, _435262] : [-(times_succeeds(_435262, _435260, 3438 ^ [_435260, _435262])), nat_succeeds(_435262), nat_succeeds(_435260)], (4945 ^ _315349) ^ [_484688, _484690, _484692] : [-(member2_terminates(_484692, _484690, _484688)), list_succeeds(_484690), list_succeeds(_484688)], (3201 ^ _315349) ^ [_427582] : [-(nat_terminates(_427582)), 3215 ^ _315349 : [(3218 ^ _315349) ^ [] : [true___], (3216 ^ _315349) ^ [] : [-(true___)]], 3207 ^ _315349 : [(3210 ^ _315349) ^ [] : [true___], (3208 ^ _315349) ^ [] : [-(true___)]], 3211 ^ _315349 : [(3214 ^ _315349) ^ [] : [nat_terminates(3204 ^ [_427582])], (3212 ^ _315349) ^ [] : [-(_427582 = s(3204 ^ [_427582]))]]], (144 ^ _315349) ^ [_320172, _320174, _320176, _320178] : [-(length_fails(_320176, _320172)), length_fails(_320178, _320174), _320178 = _320176, _320174 = _320172], (4254 ^ _315349) ^ [_461568, _461570] : [-(list_succeeds(_461568)), list_succeeds(_461570), list_succeeds(_461570 ** _461568)], (4089 ^ _315349) ^ [_455900] : [-(list_succeeds(cons(_455900, nil)))], (758 ^ _315349) ^ [_340299, _340301, _340303, _340305] : [-(@+(_340305, _340301) = @+(_340303, _340299)), _340305 = _340303, _340301 = _340299], (3807 ^ _315349) ^ [_447206, _447208] : [-(_447208 = _447206), '@=<_succeeds'(_447208, _447206), '@=<_succeeds'(_447206, _447208)], (1609 ^ _315349) ^ [_370375, _370377] : [-(same_occ_terminates(_370377, _370375)), not_same_occ_terminates(_370377, _370375), gr(_370377), gr(_370375)], (2277 ^ _315349) ^ [_395549, _395551] : [member_terminates(_395551, _395549), 2280 ^ _315349 : [(2287 ^ _315349) ^ [_395927, _395929] : [_395549 = cons(_395929, _395927), -(member_terminates(_395551, _395927))], (2281 ^ _315349) ^ [_395761, _395763] : [true___, -(true___)], (2293 ^ _315349) ^ [_396129] : [true___, -(true___)]]], (3621 ^ _315349) ^ [_441420] : [nat_succeeds(_441420), -('@<_succeeds'(_441420, s(_441420)))], (3179 ^ _315349) ^ [_426956] : [nat_terminates(_426956), 3182 ^ _315349 : [(3189 ^ _315349) ^ [_427288] : [_426956 = s(_427288), -(nat_terminates(_427288))], (3183 ^ _315349) ^ [_427136] : [true___, -(true___)], (3195 ^ _315349) ^ [] : [true___, -(true___)]]], (2652 ^ _315349) ^ [_408409, _408411, _408413] : [-(times_terminates(_408413, _408411, _408409)), 2675 ^ _315349 : [(2678 ^ _315349) ^ [] : [true___], (2676 ^ _315349) ^ [] : [-(true___)]], 2679 ^ _315349 : [(2684 ^ _315349) ^ [] : [true___], (2682 ^ _315349) ^ [] : [-(true___)], (2680 ^ _315349) ^ [] : [-(_408413 = '0')]], 2659 ^ _315349 : [(2662 ^ _315349) ^ [] : [true___], (2660 ^ _315349) ^ [] : [-(true___)]], 2663 ^ _315349 : [(2666 ^ _315349) ^ [] : [times_terminates(2655 ^ [_408409, _408411, _408413], _408411, 2656 ^ [_408409, _408411, _408413]), 2669 ^ _315349 : [(2672 ^ _315349) ^ [] : [plus_terminates(_408411, 2656 ^ [_408409, _408411, _408413], _408409)], (2670 ^ _315349) ^ [] : [times_fails(2655 ^ [_408409, _408411, _408413], _408411, 2656 ^ [_408409, _408411, _408413])]]], (2664 ^ _315349) ^ [] : [-(_408413 = s(2655 ^ [_408409, _408411, _408413]))]]], (3442 ^ _315349) ^ [_435643, _435645, _435647, _435649] : [-(_435645 = _435643), times_succeeds(_435649, _435647, _435645), times_succeeds(_435649, _435647, _435643)], (4035 ^ _315349) ^ [_454385, _454387, _454389] : [-('@<_succeeds'(@*(_454389, _454387), @*(_454389, _454385))), nat_succeeds(_454389), -(_454389 = '0'), '@<_succeeds'(_454387, _454385), nat_succeeds(_454385)], (3859 ^ _315349) ^ [_448864, _448866] : [-('@<_succeeds'(_448866, @+(_448864, _448866))), '@<_succeeds'('0', _448864), nat_succeeds(_448866), nat_succeeds(_448864)], (640 ^ _315349) ^ [_336233, _336235, _336237, _336239, _336241, _336243] : [-(occ_terminates(_336241, _336237, _336233)), occ_terminates(_336243, _336239, _336235), _336243 = _336241, _336239 = _336237, _336235 = _336233], (3749 ^ _315349) ^ [_445464, _445466] : [-('@=<_succeeds'(_445464, _445466)), nat_succeeds(_445466), nat_succeeds(_445464), '@=<_fails'(_445466, _445464)], (804 ^ _315349) ^ [_341933, _341935, _341937, _341939] : [-(occ(_341939, _341935) = occ(_341937, _341933)), _341939 = _341937, _341935 = _341933], (4679 ^ _315349) ^ [_475674, _475676, _475678] : [list_succeeds(_475676), -(delete_terminates(_475678, _475676, _475674))], (4107 ^ _315349) ^ [_456624, _456626] : [list_succeeds(_456624), -(member_terminates(_456626, _456624))], (3965 ^ _315349) ^ [_452189, _452191, _452193, _452195] : [-('@<_succeeds'(@+(_452195, _452193), @+(_452191, _452189))), '@<_succeeds'(_452195, _452191), '@=<_succeeds'(_452193, _452189), nat_succeeds(_452191)], (2396 ^ _315349) ^ [_399620] : [-(list_terminates(_399620)), 2411 ^ _315349 : [(2414 ^ _315349) ^ [] : [true___], (2412 ^ _315349) ^ [] : [-(true___)]], 2403 ^ _315349 : [(2406 ^ _315349) ^ [] : [true___], (2404 ^ _315349) ^ [] : [-(true___)]], 2407 ^ _315349 : [(2410 ^ _315349) ^ [] : [list_terminates(2400 ^ [_399620])], (2408 ^ _315349) ^ [] : [-(_399620 = cons(2399 ^ [_399620], 2400 ^ [_399620]))]]], (4505 ^ _315349) ^ [_469983, _469985, _469987] : [-(member_succeeds(_469987, _469985 ** _469983)), member_succeeds(_469987, _469985), list_succeeds(_469985)], (3593 ^ _315349) ^ [_440520, _440522] : ['@<_succeeds'(_440522, _440520), -('@<_succeeds'(_440522, s(_440520)))], (1134 ^ _315349) ^ [_352952, _352954, _352956] : [member2_succeeds(_352956, _352954, _352952), -(member_succeeds(_352956, _352952)), -(member_succeeds(_352956, _352954))], (3817 ^ _315349) ^ [_447491] : [nat_succeeds(_447491), -('@=<_succeeds'(_447491, s(_447491)))], (4545 ^ _315349) ^ [_471344, _471346, _471348] : [list_succeeds(_471346), member_succeeds(_471348, _471346 ** _471344), -(member_succeeds(_471348, _471346)), -(member_succeeds(_471348, _471344))], (4095 ^ _315349) ^ [_456226, _456228] : [list_succeeds(cons(_456228, _456226)), -(list_succeeds(_456226))], (794 ^ _315349) ^ [_341594, _341596, _341598, _341600] : [-(cons(_341600, _341596) = cons(_341598, _341594)), _341600 = _341598, _341596 = _341594], (3246 ^ _315349) ^ [_429063, _429065, _429067] : [plus_succeeds(_429067, _429065, _429063), -(nat_succeeds(_429067))], (4559 ^ _315349) ^ [_471753, _471755] : [list_succeeds(_471755), -(sub(_471755, _471755 ** _471753))], (5040 ^ _315349) ^ [_487588, _487590, _487592, _487594] : [-(_487590 = _487588), occ_succeeds(_487594, _487592, _487590), occ_succeeds(_487594, _487592, _487588)], (2250 ^ _315349) ^ [_394456, _394458] : [member_fails(_394458, _394456), 2253 ^ _315349 : [(2254 ^ _315349) ^ [_394653, _394655] : [_394456 = cons(_394655, _394653), -(member_fails(_394458, _394653))], (2260 ^ _315349) ^ [_394837] : [_394456 = cons(_394458, _394837)]]], (818 ^ _315349) ^ [_342410, _342412] : ['0' = cons(_342412, _342410)], (1455 ^ _315349) ^ [_364620, _364622] : [-(not_same_occ_succeeds(_364622, _364620)), 1456 ^ _315349 : [(1457 ^ _315349) ^ [_364767, _364769, _364771] : [member2_succeeds(_364771, _364622, _364620), occ_succeeds(_364771, _364622, _364769), occ_succeeds(_364771, _364620, _364767), -(_364769 = _364767)]]], (4113 ^ _315349) ^ [_456832, _456834] : [list_succeeds(_456832), -(member_succeeds(_456834, _456832)), -(member_fails(_456834, _456832))], (3252 ^ _315349) ^ [_429293, _429295, _429297] : [-(nat_succeeds(_429293)), plus_succeeds(_429297, _429295, _429293), nat_succeeds(_429295)], (2970 ^ _315349) ^ [_419656, _419658] : ['@<_succeeds'(_419658, _419656), 2977 ^ _315349 : [(2982 ^ _315349) ^ [] : [-('@<_succeeds'(2975 ^ [_419656, _419658], 2976 ^ [_419656, _419658]))], (2980 ^ _315349) ^ [] : [-(_419656 = s(2976 ^ [_419656, _419658]))], (2978 ^ _315349) ^ [] : [-(_419658 = s(2975 ^ [_419656, _419658]))]], 2984 ^ _315349 : [(2987 ^ _315349) ^ [] : [-(_419656 = s(2983 ^ [_419656, _419658]))], (2985 ^ _315349) ^ [] : [-(_419658 = '0')]]], (4605 ^ _315349) ^ [_473294, _473296, _473298] : [-(_473298 = _473296), list_succeeds(_473298), list_succeeds(_473296), list_succeeds(_473294), _473298 ** _473294 = _473296 ** _473294], (2123 ^ _315349) ^ [_389619, _389621, _389623] : [-(append_fails(_389623, _389621, _389619)), 2129 ^ _315349 : [(2134 ^ _315349) ^ [] : [append_fails(2127 ^ [_389619, _389621, _389623], _389621, 2128 ^ [_389619, _389621, _389623])], (2132 ^ _315349) ^ [] : [-(_389619 = cons(2126 ^ [_389619, _389621, _389623], 2128 ^ [_389619, _389621, _389623]))], (2130 ^ _315349) ^ [] : [-(_389623 = cons(2126 ^ [_389619, _389621, _389623], 2127 ^ [_389619, _389621, _389623]))]], 2135 ^ _315349 : [(2138 ^ _315349) ^ [] : [-(_389619 = _389621)], (2136 ^ _315349) ^ [] : [-(_389623 = nil)]]], (3873 ^ _315349) ^ [_449268, _449270, _449272] : [-('@=<_succeeds'(@+(_449272, _449270), @+(_449272, _449268))), nat_succeeds(_449272), '@=<_succeeds'(_449270, _449268)], (2576 ^ _315349) ^ [_405786, _405788, _405790] : [times_fails(_405790, _405788, _405786), 2579 ^ _315349 : [(2580 ^ _315349) ^ [_405996, _405998] : [_405790 = s(_405998), -(times_fails(_405998, _405788, _405996)), -(plus_fails(_405788, _405996, _405786))], (2590 ^ _315349) ^ [] : [_405790 = '0', _405786 = '0']]], (368 ^ _315349) ^ [_327356, _327358, _327360, _327362] : [-(member_fails(_327360, _327356)), member_fails(_327362, _327358), _327362 = _327360, _327358 = _327356], (4159 ^ _315349) ^ [_458346, _458348, _458350] : [-(list_succeeds(_458348)), append_succeeds(_458350, _458348, _458346), list_succeeds(_458346)], (1102 ^ _315349) ^ [_351945, _351947] : ['@<_succeeds'(_351947, _351945), '@<_fails'(_351947, _351945)], (2184 ^ _315349) ^ [_391886, _391888, _391890] : [-(append_terminates(_391890, _391888, _391886)), 2210 ^ _315349 : [(2213 ^ _315349) ^ [] : [true___], (2211 ^ _315349) ^ [] : [-(true___)]], 2214 ^ _315349 : [(2219 ^ _315349) ^ [] : [true___], (2217 ^ _315349) ^ [] : [-(true___)], (2215 ^ _315349) ^ [] : [-(_391890 = nil)]], 2192 ^ _315349 : [(2195 ^ _315349) ^ [] : [true___], (2193 ^ _315349) ^ [] : [-(true___)]], 2196 ^ _315349 : [(2199 ^ _315349) ^ [] : [2200 ^ _315349 : [(2203 ^ _315349) ^ [] : [true___], (2201 ^ _315349) ^ [] : [-(true___)]], 2204 ^ _315349 : [(2207 ^ _315349) ^ [] : [append_terminates(2188 ^ [_391886, _391888, _391890], _391888, 2189 ^ [_391886, _391888, _391890])], (2205 ^ _315349) ^ [] : [-(_391886 = cons(2187 ^ [_391886, _391888, _391890], 2189 ^ [_391886, _391888, _391890]))]]], (2197 ^ _315349) ^ [] : [-(_391890 = cons(2187 ^ [_391886, _391888, _391890], 2188 ^ [_391886, _391888, _391890]))]]], (126 ^ _315349) ^ [_319591, _319593, _319595, _319597, _319599, _319601] : [-(delete_fails(_319599, _319595, _319591)), delete_fails(_319601, _319597, _319593), _319601 = _319599, _319597 = _319595, _319593 = _319591], (176 ^ _315349) ^ [_321197, _321199] : [-(list_fails(_321197)), _321199 = _321197, list_fails(_321199)], (1152 ^ _315349) ^ [_353555, _353557, _353559] : [member2_fails(_353559, _353557, _353555), 1155 ^ _315349 : [(1158 ^ _315349) ^ [] : [-(member_fails(_353559, _353557))], (1156 ^ _315349) ^ [] : [-(member_fails(_353559, _353555))]]], (400 ^ _315349) ^ [_328409, _328411, _328413, _328415] : [-(length_terminates(_328413, _328409)), length_terminates(_328415, _328411), _328415 = _328413, _328411 = _328409], (2844 ^ _315349) ^ [_415230, _415232] : ['@=<_succeeds'(_415232, _415230), 2851 ^ _315349 : [(2856 ^ _315349) ^ [] : [-('@=<_succeeds'(2849 ^ [_415230, _415232], 2850 ^ [_415230, _415232]))], (2854 ^ _315349) ^ [] : [-(_415230 = s(2850 ^ [_415230, _415232]))], (2852 ^ _315349) ^ [] : [-(_415232 = s(2849 ^ [_415230, _415232]))]], -(_415232 = '0')], (3369 ^ _315349) ^ [_433197, _433199] : [-(@+(_433199, _433197) = @+(_433197, _433199)), nat_succeeds(_433199), nat_succeeds(_433197)], (84 ^ _315349) ^ [_318231, _318233, _318235, _318237] : [-(same_occ_fails(_318235, _318231)), same_occ_fails(_318237, _318233), _318237 = _318235, _318233 = _318231], (330 ^ _315349) ^ [_326173, _326175, _326177, _326179] : [-('@=<_fails'(_326177, _326173)), '@=<_fails'(_326179, _326175), _326179 = _326177, _326175 = _326173], (2238 ^ _315349) ^ [_393929, _393931] : [-(member_succeeds(_393931, _393929)), 2239 ^ _315349 : [(2240 ^ _315349) ^ [_394077, _394079] : [_393929 = cons(_394079, _394077), member_succeeds(_393931, _394077)], (2246 ^ _315349) ^ [_394258] : [_393929 = cons(_393931, _394258)]]], (3090 ^ _315349) ^ [_423990, _423992] : [-('@<_terminates'(_423992, _423990)), 3116 ^ _315349 : [(3119 ^ _315349) ^ [] : [true___], (3117 ^ _315349) ^ [] : [-(true___)]], 3120 ^ _315349 : [(3125 ^ _315349) ^ [] : [true___], (3123 ^ _315349) ^ [] : [-(true___)], (3121 ^ _315349) ^ [] : [-(_423992 = '0')]], 3097 ^ _315349 : [(3100 ^ _315349) ^ [] : [true___], (3098 ^ _315349) ^ [] : [-(true___)]], 3101 ^ _315349 : [(3104 ^ _315349) ^ [] : [3105 ^ _315349 : [(3108 ^ _315349) ^ [] : [true___], (3106 ^ _315349) ^ [] : [-(true___)]], 3109 ^ _315349 : [(3112 ^ _315349) ^ [] : ['@<_terminates'(3093 ^ [_423990, _423992], 3094 ^ [_423990, _423992])], (3110 ^ _315349) ^ [] : [-(_423990 = s(3094 ^ [_423990, _423992]))]]], (3102 ^ _315349) ^ [] : [-(_423992 = s(3093 ^ [_423990, _423992]))]]], (1060 ^ _315349) ^ [_350557, _350559, _350561] : [times_terminates(_350561, _350559, _350557), -(times_succeeds(_350561, _350559, _350557)), -(times_fails(_350561, _350559, _350557))], (354 ^ _315349) ^ [_326912, _326914, _326916, _326918] : [-(member_terminates(_326916, _326912)), member_terminates(_326918, _326914), _326918 = _326916, _326914 = _326912], (1188 ^ _315349) ^ [_354761, _354763, _354765] : [occ_succeeds(_354765, _354763, _354761), 1195 ^ _315349 : [(1200 ^ _315349) ^ [] : [-(occ_succeeds(_354765, 1194 ^ [_354761, _354763, _354765], _354761))], (1198 ^ _315349) ^ [] : [_354765 = 1193 ^ [_354761, _354763, _354765]], (1196 ^ _315349) ^ [] : [-(_354763 = cons(1193 ^ [_354761, _354763, _354765], 1194 ^ [_354761, _354763, _354765]))]], 1205 ^ _315349 : [(1210 ^ _315349) ^ [] : [-(occ_succeeds(_354765, 1203 ^ [_354761, _354763, _354765], 1204 ^ [_354761, _354763, _354765]))], (1208 ^ _315349) ^ [] : [-(_354761 = s(1204 ^ [_354761, _354763, _354765]))], (1206 ^ _315349) ^ [] : [-(_354763 = cons(_354765, 1203 ^ [_354761, _354763, _354765]))]], 1211 ^ _315349 : [(1214 ^ _315349) ^ [] : [-(_354761 = '0')], (1212 ^ _315349) ^ [] : [-(_354763 = nil)]]], (752 ^ _315349) ^ [_340053, _340055] : [_340055 = _340053, -(s(_340055) = s(_340053))], (3564 ^ _315349) ^ [_439504, _439506] : [nat_succeeds(_439504), -('@<_terminates'(_439506, _439504))], (4711 ^ _315349) ^ [_476776, _476778, _476780] : [-(lh(_476778) = s(lh(_476776))), delete_succeeds(_476780, _476778, _476776), list_succeeds(_476778)], (1809 ^ _315349) ^ [_377838, _377840, _377842] : [delete_fails(_377842, _377840, _377838), 1812 ^ _315349 : [(1813 ^ _315349) ^ [_378067, _378069, _378071] : [_377840 = cons(_378071, _378069), _377838 = cons(_378071, _378067), -(delete_fails(_377842, _378069, _378067))], (1823 ^ _315349) ^ [] : [_377840 = cons(_377842, _377838)]]], (3048 ^ _315349) ^ [_422682, _422684] : ['@<_terminates'(_422684, _422682), 3051 ^ _315349 : [(3058 ^ _315349) ^ [_423083, _423085] : [_422684 = s(_423085), 3061 ^ _315349 : [(3068 ^ _315349) ^ [] : [_422682 = s(_423083), -('@<_terminates'(_423085, _423083))], (3062 ^ _315349) ^ [] : [true___, -(true___)]]], (3074 ^ _315349) ^ [_423567] : [true___, -(true___)], (3052 ^ _315349) ^ [_422917, _422919] : [true___, -(true___)], (3080 ^ _315349) ^ [_423727] : [_422684 = '0', true___, -(true___)]]], (1825 ^ _315349) ^ [_378439, _378441, _378443] : [-(delete_fails(_378443, _378441, _378439)), 1831 ^ _315349 : [(1836 ^ _315349) ^ [] : [delete_fails(_378443, 1829 ^ [_378439, _378441, _378443], 1830 ^ [_378439, _378441, _378443])], (1834 ^ _315349) ^ [] : [-(_378439 = cons(1828 ^ [_378439, _378441, _378443], 1830 ^ [_378439, _378441, _378443]))], (1832 ^ _315349) ^ [] : [-(_378441 = cons(1828 ^ [_378439, _378441, _378443], 1829 ^ [_378439, _378441, _378443]))]], -(_378441 = cons(_378443, _378439))], (2892 ^ _315349) ^ [_416961, _416963] : [-('@=<_fails'(_416963, _416961)), 2897 ^ _315349 : [(2902 ^ _315349) ^ [] : ['@=<_fails'(2895 ^ [_416961, _416963], 2896 ^ [_416961, _416963])], (2900 ^ _315349) ^ [] : [-(_416961 = s(2896 ^ [_416961, _416963]))], (2898 ^ _315349) ^ [] : [-(_416963 = s(2895 ^ [_416961, _416963]))]], -(_416963 = '0')], (4409 ^ _315349) ^ [_466547, _466549] : [list_succeeds(_466547), -('@=<_succeeds'(lh(_466547), lh(cons(_466549, _466547))))], (816 ^ _315349) ^ [_342317] : ['0' = s(_342317)], (4236 ^ _315349) ^ [_460907] : [-(nil ** _460907 = _460907)], (3311 ^ _315349) ^ [_431323, _431325, _431327, _431329] : [-(_431325 = _431323), plus_succeeds(_431329, _431327, _431325), plus_succeeds(_431329, _431327, _431323)], (3558 ^ _315349) ^ [_439296, _439298] : [nat_succeeds(_439298), -('@<_terminates'(_439298, _439296))], (844 ^ _315349) ^ [] : [-(gr('0'))], (878 ^ _315349) ^ [_344617, _344619, _344621] : [member2_succeeds(_344621, _344619, _344617), member2_fails(_344621, _344619, _344617)], (4379 ^ _315349) ^ [_465610, _465612] : [-(lh(_465612 ** _465610) = @+(lh(_465612), lh(_465610))), list_succeeds(_465612), list_succeeds(_465610)], (1044 ^ _315349) ^ [_350026] : [nat_list_terminates(_350026), -(nat_list_succeeds(_350026)), -(nat_list_fails(_350026))], (4093 ^ _315349) ^ [_456107, _456109, _456111] : [-(list_succeeds(cons(_456111, cons(_456109, cons(_456107, nil)))))], (3262 ^ _315349) ^ [_429614, _429616, _429618] : [-(nat_succeeds(_429616)), plus_succeeds(_429618, _429616, _429614), nat_succeeds(_429614)], (2989 ^ _315349) ^ [_420388, _420390] : [-('@<_succeeds'(_420390, _420388)), 2990 ^ _315349 : [(2991 ^ _315349) ^ [_420548, _420550] : [_420390 = s(_420550), _420388 = s(_420548), '@<_succeeds'(_420550, _420548)], (3001 ^ _315349) ^ [_420844] : [_420390 = '0', _420388 = s(_420844)]]], (1086 ^ _315349) ^ [_351436, _351438] : ['@=<_succeeds'(_351438, _351436), '@=<_fails'(_351438, _351436)], (1593 ^ _315349) ^ [_369827, _369829] : [not_same_occ_succeeds(_369829, _369827), -(same_occ_fails(_369829, _369827))], (2726 ^ _315349) ^ [_411166, _411168, _411170] : [plus_fails(_411170, _411168, _411166), 2729 ^ _315349 : [(2730 ^ _315349) ^ [_411379, _411381] : [_411170 = s(_411381), _411166 = s(_411379), -(plus_fails(_411381, _411168, _411379))], (2740 ^ _315349) ^ [] : [_411170 = '0', _411166 = _411168]]], (4751 ^ _315349) ^ [_478381, _478383, _478385] : [4758 ^ _315349 : [(4761 ^ _315349) ^ [] : [-(gr(_478381))], (4759 ^ _315349) ^ [] : [-(gr(_478385))]], delete_succeeds(_478385, _478383, _478381), gr(_478383)], (4917 ^ _315349) ^ [_483769, _483771] : [permutation_succeeds(_483771, _483769), 4920 ^ _315349 : [(4923 ^ _315349) ^ [] : [-(list_succeeds(_483769))], (4921 ^ _315349) ^ [] : [-(list_succeeds(_483771))]]], (820 ^ _315349) ^ [_342492] : [nil = s(_342492)], (4850 ^ _315349) ^ [_481619, _481621, _481623] : [list_succeeds(_481623), 4853 ^ _315349 : [(4860 ^ _315349) ^ [] : [append_succeeds(_481623, _481621, _481619), -(_481623 ** _481621 = _481619)], (4854 ^ _315349) ^ [] : [_481623 ** _481621 = _481619, -(append_succeeds(_481623, _481621, _481619))]]], (3421 ^ _315349) ^ [_434953, _434955, _434957] : [-(times_terminates(_434957, _434955, _434953)), nat_succeeds(_434957), nat_succeeds(_434955)], (452 ^ _315349) ^ [_330064, _330066, _330068, _330070, _330072, _330074] : [-(delete_terminates(_330072, _330068, _330064)), delete_terminates(_330074, _330070, _330066), _330074 = _330072, _330070 = _330068, _330066 = _330064], (4633 ^ _315349) ^ [_474132] : [nat_list_succeeds(_474132), -(list_succeeds(_474132))], (2103 ^ _315349) ^ [_388929, _388931, _388933] : [append_fails(_388933, _388931, _388929), 2106 ^ _315349 : [(2107 ^ _315349) ^ [_389163, _389165, _389167] : [_388933 = cons(_389167, _389165), _388929 = cons(_389167, _389163), -(append_fails(_389165, _388931, _389163))], (2117 ^ _315349) ^ [] : [_388933 = nil, _388929 = _388931]]], (3897 ^ _315349) ^ [_450011, _450013] : [nat_succeeds(_450013), -('@=<_succeeds'(_450013, @+(_450013, _450011)))], (3379 ^ _315349) ^ [_433518, _433520, _433522] : [-(_433520 = _433518), nat_succeeds(_433522), @+(_433522, _433520) = @+(_433522, _433518)], (1964 ^ _315349) ^ [_383792, _383794] : [-(length_fails(_383794, _383792)), 1970 ^ _315349 : [(1975 ^ _315349) ^ [] : [length_fails(1968 ^ [_383792, _383794], 1969 ^ [_383792, _383794])], (1973 ^ _315349) ^ [] : [-(_383792 = s(1969 ^ [_383792, _383794]))], (1971 ^ _315349) ^ [] : [-(_383794 = cons(1967 ^ [_383792, _383794], 1968 ^ [_383792, _383794]))]], 1976 ^ _315349 : [(1979 ^ _315349) ^ [] : [-(_383792 = '0')], (1977 ^ _315349) ^ [] : [-(_383794 = nil)]]], (428 ^ _315349) ^ [_329269, _329271] : [-(nat_list_terminates(_329269)), _329271 = _329269, nat_list_terminates(_329271)], (3627 ^ _315349) ^ [_441626, _441628] : [nat_succeeds(_441626), '@<_succeeds'(_441628, s(_441626)), -('@<_succeeds'(_441628, _441626)), -(_441628 = _441626)], (4449 ^ _315349) ^ [_467961, _467963, _467965] : [-(sub(_467965, _467961)), sub(_467965, _467963), sub(_467963, _467961)], (2482 ^ _315349) ^ [_402567] : [nat_list_terminates(_402567), 2485 ^ _315349 : [(2492 ^ _315349) ^ [_402935, _402937] : [_402567 = cons(_402937, _402935), 2495 ^ _315349 : [(2498 ^ _315349) ^ [] : [-(nat_fails(_402937)), -(nat_list_terminates(_402935))], (2496 ^ _315349) ^ [] : [-(nat_terminates(_402937))]]], (2486 ^ _315349) ^ [_402777, _402779] : [true___, -(true___)], (2504 ^ _315349) ^ [] : [true___, -(true___)]]], (4207 ^ _315349) ^ [_459935, _459937, _459939] : [4214 ^ _315349 : [(4217 ^ _315349) ^ [] : [-(gr(_459937))], (4215 ^ _315349) ^ [] : [-(gr(_459939))]], append_succeeds(_459939, _459937, _459935), gr(_459935)], (3715 ^ _315349) ^ [_444488] : [nat_succeeds(_444488), -('@=<_succeeds'(_444488, _444488))], (910 ^ _315349) ^ [_345729, _345731] : [not_same_occ_succeeds(_345731, _345729), not_same_occ_fails(_345731, _345729)], (2336 ^ _315349) ^ [_397562] : [-(list_succeeds(_397562)), 2337 ^ _315349 : [(2338 ^ _315349) ^ [_397698, _397700] : [_397562 = cons(_397700, _397698), list_succeeds(_397698)], (2344 ^ _315349) ^ [] : [_397562 = nil]]], (714 ^ _315349) ^ [_338578, _338580] : [-(nat_succeeds(_338578)), _338580 = _338578, nat_succeeds(_338580)], (3278 ^ _315349) ^ [_430169, _430171, _430173] : [plus_succeeds(_430173, _430171, _430169), -(gr(_430173))], (1905 ^ _315349) ^ [_381640, _381642] : [length_succeeds(_381642, _381640), 1913 ^ _315349 : [(1918 ^ _315349) ^ [] : [-(length_succeeds(1911 ^ [_381640, _381642], 1912 ^ [_381640, _381642]))], (1916 ^ _315349) ^ [] : [-(_381640 = s(1912 ^ [_381640, _381642]))], (1914 ^ _315349) ^ [] : [-(_381642 = cons(1910 ^ [_381640, _381642], 1911 ^ [_381640, _381642]))]], 1919 ^ _315349 : [(1922 ^ _315349) ^ [] : [-(_381640 = '0')], (1920 ^ _315349) ^ [] : [-(_381642 = nil)]]], (3913 ^ _315349) ^ [_450540, _450542, _450544] : [-('@<_succeeds'(_450542, _450540)), nat_succeeds(_450544), '@<_succeeds'(@+(_450544, _450542), @+(_450544, _450540))], (38 ^ _315349) ^ [_316762, _316764, _316766, _316768, _316770, _316772] : [-(occ_fails(_316770, _316766, _316762)), occ_fails(_316772, _316768, _316764), _316772 = _316770, _316768 = _316766, _316764 = _316762], (1662 ^ _315349) ^ [_372295, _372297] : [permutation_fails(_372297, _372295), 1665 ^ _315349 : [(1666 ^ _315349) ^ [_372518, _372520, _372522] : [_372295 = cons(_372522, _372520), -(delete_fails(_372522, _372297, _372518)), -(permutation_fails(_372518, _372520))], (1676 ^ _315349) ^ [] : [_372297 = nil, _372295 = nil]]], (846 ^ _315349) ^ [] : [-(gr(nil))], (4793 ^ _315349) ^ [_479793, _479795] : [member_succeeds(_479795, _479793), -(delete_succeeds(_479795, _479793, 4796 ^ [_479793, _479795]))], (916 ^ _315349) ^ [_345938, _345940] : [not_same_occ_terminates(_345940, _345938), -(not_same_occ_succeeds(_345940, _345938)), -(not_same_occ_fails(_345940, _345938))], (2360 ^ _315349) ^ [_398437] : [-(list_fails(_398437)), 2365 ^ _315349 : [(2368 ^ _315349) ^ [] : [list_fails(2364 ^ [_398437])], (2366 ^ _315349) ^ [] : [-(_398437 = cons(2363 ^ [_398437], 2364 ^ [_398437]))]], -(_398437 = nil)], (4571 ^ _315349) ^ [_472209, _472211, _472213, _472215] : [_472211 = cons(_472215, _472209), append_succeeds(_472213, _472211, _472209), list_succeeds(_472209)], (3823 ^ _315349) ^ [_447683] : [nat_succeeds(_447683), -('@=<_fails'(s(_447683), _447683))], (4244 ^ _315349) ^ [_461269, _461271] : [-(list_succeeds(_461271 ** _461269)), list_succeeds(_461271), list_succeeds(_461269)], (4389 ^ _315349) ^ [_465929, _465931] : [-('@=<_succeeds'(lh(_465931), lh(_465931 ** _465929))), list_succeeds(_465931), list_succeeds(_465929)], (2614 ^ _315349) ^ [_407238, _407240, _407242] : [times_terminates(_407242, _407240, _407238), 2617 ^ _315349 : [(2642 ^ _315349) ^ [] : [_407242 = '0', true___, -(true___)], (2618 ^ _315349) ^ [_407476, _407478] : [true___, -(true___)], (2636 ^ _315349) ^ [] : [true___, -(true___)], (2624 ^ _315349) ^ [_407650, _407652] : [_407242 = s(_407652), 2627 ^ _315349 : [(2630 ^ _315349) ^ [] : [-(times_fails(_407652, _407240, _407650)), -(plus_terminates(_407240, _407650, _407238))], (2628 ^ _315349) ^ [] : [-(times_terminates(_407652, _407240, _407650))]]]]], (4290 ^ _315349) ^ [_462639, _462641, _462643] : [-((_462643 ** _462641) ** _462639 = _462643 ** (_462641 ** _462639)), list_succeeds(_462643), list_succeeds(_462641)], (1022 ^ _315349) ^ [_349386] : [list_succeeds(_349386), list_fails(_349386)], (3829 ^ _315349) ^ [_447903, _447905, _447907] : [-('@<_succeeds'(@+(_447907, _447905), @+(_447907, _447903))), nat_succeeds(_447907), '@<_succeeds'(_447905, _447903)], (4651 ^ _315349) ^ [_474732, _474734, _474736, _474738] : [-('@<_succeeds'(@+(lh(_474736), lh(_474734)), _474732)), list_succeeds(_474736), list_succeeds(_474734), '@<_succeeds'(@+(lh(cons(_474738, _474736)), lh(_474734)), s(_474732))], (4226 ^ _315349) ^ [_460613, _460615, _460617, _460619] : [-(_460615 = _460613), append_succeeds(_460619, _460617, _460615), append_succeeds(_460619, _460617, _460613)], (594 ^ _315349) ^ [_334708, _334710, _334712, _334714] : [-(permutation_succeeds(_334712, _334708)), permutation_succeeds(_334714, _334710), _334714 = _334712, _334710 = _334708], (3506 ^ _315349) ^ [_437636] : [nat_succeeds(_437636), -(@*(_437636, '0') = '0')], (4739 ^ _315349) ^ [_477985, _477987, _477989] : [4746 ^ _315349 : [(4749 ^ _315349) ^ [] : [-(nat_list_succeeds(_477985))], (4747 ^ _315349) ^ [] : [-(nat_succeeds(_477989))]], delete_succeeds(_477989, _477987, _477985), nat_list_succeeds(_477987)], (3763 ^ _315349) ^ [_445848, _445850] : ['@=<_succeeds'(_445850, _445848), nat_succeeds(_445848), -('@<_succeeds'(_445850, _445848)), -(_445850 = _445848)], (990 ^ _315349) ^ [_348342, _348344, _348346] : [append_succeeds(_348346, _348344, _348342), append_fails(_348346, _348344, _348342)], (870 ^ _315349) ^ [_344316, _344318] : [gr(cons(_344318, _344316)), 873 ^ _315349 : [(876 ^ _315349) ^ [] : [-(gr(_344316))], (874 ^ _315349) ^ [] : [-(gr(_344318))]]], (1012 ^ _315349) ^ [_349100, _349102] : [member_terminates(_349102, _349100), -(member_succeeds(_349102, _349100)), -(member_fails(_349102, _349100))], (1842 ^ _315349) ^ [_379329, _379331, _379333] : [delete_terminates(_379333, _379331, _379329), 1845 ^ _315349 : [(1852 ^ _315349) ^ [_379756, _379758, _379760] : [_379331 = cons(_379760, _379758), 1855 ^ _315349 : [(1862 ^ _315349) ^ [] : [_379329 = cons(_379760, _379756), -(delete_terminates(_379333, _379758, _379756))], (1856 ^ _315349) ^ [] : [true___, -(true___)]]], (1846 ^ _315349) ^ [_379576, _379578, _379580] : [true___, -(true___)], (1868 ^ _315349) ^ [] : [true___, -(true___)]]], (2374 ^ _315349) ^ [_398960] : [list_terminates(_398960), 2377 ^ _315349 : [(2384 ^ _315349) ^ [_399318, _399320] : [_398960 = cons(_399320, _399318), -(list_terminates(_399318))], (2378 ^ _315349) ^ [_399160, _399162] : [true___, -(true___)], (2390 ^ _315349) ^ [] : [true___, -(true___)]]], (4866 ^ _315349) ^ [_482105, _482107] : [list_succeeds(_482107), 4869 ^ _315349 : [(4876 ^ _315349) ^ [] : [length_succeeds(_482107, _482105), -(lh(_482107) = _482105)], (4870 ^ _315349) ^ [] : [lh(_482107) = _482105, -(length_succeeds(_482107, _482105))]]], (1440 ^ _315349) ^ [_363889, _363891] : [not_same_occ_succeeds(_363891, _363889), 1446 ^ _315349 : [(1453 ^ _315349) ^ [] : [1444 ^ [_363889, _363891] = 1445 ^ [_363889, _363891]], (1447 ^ _315349) ^ [] : [-(member2_succeeds(1443 ^ [_363889, _363891], _363891, _363889))], (1451 ^ _315349) ^ [] : [-(occ_succeeds(1443 ^ [_363889, _363891], _363889, 1445 ^ [_363889, _363891]))], (1449 ^ _315349) ^ [] : [-(occ_succeeds(1443 ^ [_363889, _363891], _363891, 1444 ^ [_363889, _363891]))]]], (10 ^ _315349) ^ [_315784, _315786, _315788] : [-(_315788 = _315784), _315788 = _315786, _315786 = _315784], (3522 ^ _315349) ^ [_438161, _438163] : [-(@*(_438163, _438161) = @*(_438161, _438163)), nat_succeeds(_438163), nat_succeeds(_438161)], (2 ^ _315349) ^ [_315473] : [-(_315473 = _315473)], (884 ^ _315349) ^ [_344850, _344852, _344854] : [member2_terminates(_344854, _344852, _344850), -(member2_succeeds(_344854, _344852, _344850)), -(member2_fails(_344854, _344852, _344850))], (3321 ^ _315349) ^ [_431617] : [-(@+('0', _431617) = _431617)], (4021 ^ _315349) ^ [_453961, _453963, _453965] : [-('@=<_succeeds'(@*(_453965, _453961), @*(_453963, _453961))), '@=<_succeeds'(_453965, _453963), nat_succeeds(_453963), nat_succeeds(_453961)], (2262 ^ _315349) ^ [_394910, _394912] : [-(member_fails(_394912, _394910)), 2267 ^ _315349 : [(2270 ^ _315349) ^ [] : [member_fails(_394912, 2266 ^ [_394910, _394912])], (2268 ^ _315349) ^ [] : [-(_394910 = cons(2265 ^ [_394910, _394912], 2266 ^ [_394910, _394912]))]], -(_394910 = cons(_394912, 2271 ^ [_394910, _394912]))], (316 ^ _315349) ^ [_325729, _325731, _325733, _325735] : [-('@=<_terminates'(_325733, _325729)), '@=<_terminates'(_325735, _325731), _325735 = _325733, _325731 = _325729], (964 ^ _315349) ^ [_347503, _347505, _347507] : [delete_terminates(_347507, _347505, _347503), -(delete_succeeds(_347507, _347505, _347503)), -(delete_fails(_347507, _347505, _347503))], (3951 ^ _315349) ^ [_451735, _451737, _451739, _451741] : [-('@=<_succeeds'(@+(_451741, _451739), @+(_451737, _451735))), '@=<_succeeds'(_451741, _451737), '@=<_succeeds'(_451739, _451735), nat_succeeds(_451737)], (4955 ^ _315349) ^ [_485009, _485011, _485013] : [-(occ_terminates(_485013, _485011, _485009)), list_succeeds(_485011), gr(_485011), gr(_485013)], (1473 ^ _315349) ^ [_365291, _365293] : [not_same_occ_fails(_365293, _365291), 1476 ^ _315349 : [(1477 ^ _315349) ^ [_365481, _365483, _365485] : [-(member2_fails(_365485, _365293, _365291)), -(occ_fails(_365485, _365293, _365483)), -(occ_fails(_365485, _365291, _365481)), -(_365483 = _365481)]]], (860 ^ _315349) ^ [_344065, _344067] : [-(gr(cons(_344067, _344065))), gr(_344067), gr(_344065)], (3029 ^ _315349) ^ [_421851, _421853] : [-('@<_fails'(_421853, _421851)), 3034 ^ _315349 : [(3039 ^ _315349) ^ [] : ['@<_fails'(3032 ^ [_421851, _421853], 3033 ^ [_421851, _421853])], (3037 ^ _315349) ^ [] : [-(_421851 = s(3033 ^ [_421851, _421853]))], (3035 ^ _315349) ^ [] : [-(_421853 = s(3032 ^ [_421851, _421853]))]], 3041 ^ _315349 : [(3044 ^ _315349) ^ [] : [-(_421851 = s(3040 ^ [_421851, _421853]))], (3042 ^ _315349) ^ [] : [-(_421853 = '0')]]], (4777 ^ _315349) ^ [_479226, _479228, _479230] : [delete_succeeds(_479230, _479228, _479226), -(member_succeeds(_479230, _479228))], (942 ^ _315349) ^ [_346747, _346749] : [permutation_succeeds(_346749, _346747), permutation_fails(_346749, _346747)], (1874 ^ _315349) ^ [_380382, _380384, _380386] : [-(delete_terminates(_380386, _380384, _380382)), 1898 ^ _315349 : [(1901 ^ _315349) ^ [] : [true___], (1899 ^ _315349) ^ [] : [-(true___)]], 1882 ^ _315349 : [(1885 ^ _315349) ^ [] : [true___], (1883 ^ _315349) ^ [] : [-(true___)]], 1886 ^ _315349 : [(1889 ^ _315349) ^ [] : [1890 ^ _315349 : [(1893 ^ _315349) ^ [] : [true___], (1891 ^ _315349) ^ [] : [-(true___)]], 1894 ^ _315349 : [(1897 ^ _315349) ^ [] : [delete_terminates(_380386, 1878 ^ [_380382, _380384, _380386], 1879 ^ [_380382, _380384, _380386])], (1895 ^ _315349) ^ [] : [-(_380382 = cons(1877 ^ [_380382, _380384, _380386], 1879 ^ [_380382, _380384, _380386]))]]], (1887 ^ _315349) ^ [] : [-(_380384 = cons(1877 ^ [_380382, _380384, _380386], 1878 ^ [_380382, _380384, _380386]))]]], (4727 ^ _315349) ^ [_477359, _477361, _477363] : [delete_succeeds(_477363, _477361, _477359), 4732 ^ _315349 : [(4737 ^ _315349) ^ [] : [-(_477359 = (4730 ^ [_477359, _477361, _477363]) ** (4731 ^ [_477359, _477361, _477363]))], (4735 ^ _315349) ^ [] : [-(_477361 = (4730 ^ [_477359, _477361, _477363]) ** cons(_477363, 4731 ^ [_477359, _477361, _477363]))], (4733 ^ _315349) ^ [] : [-(list_succeeds(4730 ^ [_477359, _477361, _477363]))]]], (3234 ^ _315349) ^ [_428603, _428605, _428607] : [nat_succeeds(_428607), -(plus_terminates(_428607, _428605, _428603))], (56 ^ _315349) ^ [_317343, _317345, _317347, _317349] : [-(same_occ_succeeds(_317347, _317343)), same_occ_succeeds(_317349, _317345), _317349 = _317347, _317345 = _317343], (516 ^ _315349) ^ [_332186, _332188, _332190, _332192, _332194, _332196] : [-(times_succeeds(_332194, _332190, _332186)), times_succeeds(_332196, _332192, _332188), _332196 = _332194, _332192 = _332190, _332188 = _332186], (288 ^ _315349) ^ [_324841, _324843, _324845, _324847] : [-('@<_terminates'(_324845, _324841)), '@<_terminates'(_324847, _324843), _324847 = _324845, _324843 = _324841], (3675 ^ _315349) ^ [_442980, _442982] : ['@=<_succeeds'(_442982, _442980), -(nat_succeeds(_442982))], (4565 ^ _315349) ^ [_471967, _471969] : [list_succeeds(_471969), -(sub(_471967, _471969 ** _471967))], (3353 ^ _315349) ^ [_432674] : [nat_succeeds(_432674), -(@+(_432674, '0') = _432674)], (2322 ^ _315349) ^ [_397112] : [list_succeeds(_397112), 2329 ^ _315349 : [(2332 ^ _315349) ^ [] : [-(list_succeeds(2328 ^ [_397112]))], (2330 ^ _315349) ^ [] : [-(_397112 = cons(2327 ^ [_397112], 2328 ^ [_397112]))]], -(_397112 = nil)], (2064 ^ _315349) ^ [_387308, _387310, _387312] : [append_succeeds(_387312, _387310, _387308), 2072 ^ _315349 : [(2077 ^ _315349) ^ [] : [-(append_succeeds(2070 ^ [_387308, _387310, _387312], _387310, 2071 ^ [_387308, _387310, _387312]))], (2075 ^ _315349) ^ [] : [-(_387308 = cons(2069 ^ [_387308, _387310, _387312], 2071 ^ [_387308, _387310, _387312]))], (2073 ^ _315349) ^ [] : [-(_387312 = cons(2069 ^ [_387308, _387310, _387312], 2070 ^ [_387308, _387310, _387312]))]], 2078 ^ _315349 : [(2081 ^ _315349) ^ [] : [-(_387308 = _387310)], (2079 ^ _315349) ^ [] : [-(_387312 = nil)]]], (302 ^ _315349) ^ [_325285, _325287, _325289, _325291] : [-('@<_fails'(_325289, _325285)), '@<_fails'(_325291, _325287), _325291 = _325289, _325287 = _325285], (4471 ^ _315349) ^ [_468691, _468693, _468695] : [sub(_468693, _468691), -(sub(cons(_468695, _468693), cons(_468695, _468691)))], (948 ^ _315349) ^ [_346956, _346958] : [permutation_terminates(_346958, _346956), -(permutation_succeeds(_346958, _346956)), -(permutation_fails(_346958, _346956))], (3615 ^ _315349) ^ [_441231] : [nat_succeeds(_441231), '@<_succeeds'(_441231, _441231)], (830 ^ _315349) ^ [_342913, _342915, _342917] : [s(_342917) = cons(_342915, _342913)], (3468 ^ _315349) ^ [_436477, _436479] : [-(nat_succeeds(@*(_436479, _436477))), nat_succeeds(_436479), nat_succeeds(_436477)], (3154 ^ _315349) ^ [_426127] : [nat_fails(_426127), 3157 ^ _315349 : [(3158 ^ _315349) ^ [_426289] : [_426127 = s(_426289), -(nat_fails(_426289))], (3164 ^ _315349) ^ [] : [_426127 = '0']]], (534 ^ _315349) ^ [_332795, _332797, _332799, _332801, _332803, _332805] : [-(append_succeeds(_332803, _332799, _332795)), append_succeeds(_332805, _332801, _332797), _332805 = _332803, _332801 = _332799, _332797 = _332795], (2418 ^ _315349) ^ [_400347] : [nat_list_succeeds(_400347), 2425 ^ _315349 : [(2430 ^ _315349) ^ [] : [-(nat_list_succeeds(2424 ^ [_400347]))], (2428 ^ _315349) ^ [] : [-(nat_succeeds(2423 ^ [_400347]))], (2426 ^ _315349) ^ [] : [-(_400347 = cons(2423 ^ [_400347], 2424 ^ [_400347]))]], -(_400347 = nil)], (196 ^ _315349) ^ [_321843, _321845, _321847, _321849, _321851, _321853] : [-(times_fails(_321851, _321847, _321843)), times_fails(_321853, _321849, _321845), _321853 = _321851, _321849 = _321847, _321845 = _321843], (2083 ^ _315349) ^ [_388158, _388160, _388162] : [-(append_succeeds(_388162, _388160, _388158)), 2084 ^ _315349 : [(2085 ^ _315349) ^ [_388336, _388338, _388340] : [_388162 = cons(_388340, _388338), _388158 = cons(_388340, _388336), append_succeeds(_388338, _388160, _388336)], (2095 ^ _315349) ^ [] : [_388162 = nil, _388158 = _388160]]], (4181 ^ _315349) ^ [_459063, _459065, _459067] : [list_succeeds(_459067), -(append_terminates(_459067, _459065, _459063))], (4007 ^ _315349) ^ [_453537, _453539, _453541] : [-('@=<_succeeds'(@*(_453541, _453539), @*(_453541, _453537))), nat_succeeds(_453541), '@=<_succeeds'(_453539, _453537), nat_succeeds(_453537)], (3538 ^ _315349) ^ [_438648] : [nat_succeeds(_438648), -(@*(_438648, s('0')) = _438648)], (980 ^ _315349) ^ [_348028, _348030] : [length_terminates(_348030, _348028), -(length_succeeds(_348030, _348028)), -(length_fails(_348030, _348028))]], input).
% 218.51/211.42 ncf('1',plain,[occ(5086 ^ [], cons(5087 ^ [], 5088 ^ [])) = occ(5086 ^ [], 5088 ^ [])],start(5094 ^ 0)).
% 218.51/211.42 ncf('1.1',plain,[-(occ(5086 ^ [], cons(5087 ^ [], 5088 ^ [])) = occ(5086 ^ [], 5088 ^ [])), 4911 : occ_succeeds(5086 ^ [], cons(5087 ^ [], 5088 ^ []), occ(5086 ^ [], 5088 ^ [])), 4911 : list_succeeds(cons(5087 ^ [], 5088 ^ []))],extension(4901 ^ 1,bind([[_483283, _483285, _483287], [occ(5086 ^ [], 5088 ^ []), cons(5087 ^ [], 5088 ^ []), 5086 ^ []]]))).
% 218.51/211.42 ncf('1.1.1',plain,[-(occ_succeeds(5086 ^ [], cons(5087 ^ [], 5088 ^ []), occ(5086 ^ [], 5088 ^ []))), 1218 : cons(5087 ^ [], 5088 ^ []) = cons(5087 ^ [], 5088 ^ []), 1218 : -(5086 ^ [] = 5087 ^ []), 1218 : occ_succeeds(5086 ^ [], 5088 ^ [], occ(5086 ^ [], 5088 ^ []))],extension(1216 ^ 4,bind([[_355929, _355931, _355933, _356121, _356123], [occ(5086 ^ [], 5088 ^ []), cons(5087 ^ [], 5088 ^ []), 5086 ^ [], 5088 ^ [], 5087 ^ []]]))).
% 218.51/211.42 ncf('1.1.1.1',plain,[-(cons(5087 ^ [], 5088 ^ []) = cons(5087 ^ [], 5088 ^ [])), s(cons(5087 ^ [], 5088 ^ [])) = s(cons(5087 ^ [], 5088 ^ []))],extension(824 ^ 7,bind([[_342697, _342699], [cons(5087 ^ [], 5088 ^ []), cons(5087 ^ [], 5088 ^ [])]]))).
% 218.51/211.42 ncf('1.1.1.1.1',plain,[-(s(cons(5087 ^ [], 5088 ^ [])) = s(cons(5087 ^ [], 5088 ^ [])))],extension(2 ^ 8,bind([[_315473], [s(cons(5087 ^ [], 5088 ^ []))]]))).
% 218.51/211.42 ncf('1.1.1.2',plain,[5086 ^ [] = 5087 ^ []],extension(5092 ^ 7)).
% 218.51/211.42 ncf('1.1.1.3',plain,[-(occ_succeeds(5086 ^ [], 5088 ^ [], occ(5086 ^ [], 5088 ^ []))), 4905 : occ(5086 ^ [], 5088 ^ []) = occ(5086 ^ [], 5088 ^ []), 4905 : list_succeeds(5088 ^ [])],extension(4901 ^ 7,bind([[_483283, _483285, _483287], [occ(5086 ^ [], 5088 ^ []), 5088 ^ [], 5086 ^ []]]))).
% 218.51/211.42 ncf('1.1.1.3.1',plain,[-(occ(5086 ^ [], 5088 ^ []) = occ(5086 ^ [], 5088 ^ []))],extension(2 ^ 10,bind([[_315473], [occ(5086 ^ [], 5088 ^ [])]]))).
% 218.51/211.42 ncf('1.1.1.3.2',plain,[-(list_succeeds(5088 ^ []))],extension(5090 ^ 8)).
% 218.51/211.42 ncf('1.1.2',plain,[-(list_succeeds(cons(5087 ^ [], 5088 ^ []))), occ_succeeds(5086 ^ [], cons(5087 ^ [], 5088 ^ []), 5036 ^ [5088 ^ [], 5086 ^ []])],extension(5025 ^ 2,bind([[_487001, _487003, _487005], [5036 ^ [5088 ^ [], 5086 ^ []], cons(5087 ^ [], 5088 ^ []), 5086 ^ []]]))).
% 218.51/211.42 ncf('1.1.2.1',plain,[-(occ_succeeds(5086 ^ [], cons(5087 ^ [], 5088 ^ []), 5036 ^ [5088 ^ [], 5086 ^ []])), 1218 : cons(5087 ^ [], 5088 ^ []) = cons(5087 ^ [], 5088 ^ []), 1218 : -(5086 ^ [] = 5087 ^ []), 1218 : occ_succeeds(5086 ^ [], 5088 ^ [], 5036 ^ [5088 ^ [], 5086 ^ []])],extension(1216 ^ 3,bind([[_355929, _355931, _355933, _356121, _356123], [5036 ^ [5088 ^ [], 5086 ^ []], cons(5087 ^ [], 5088 ^ []), 5086 ^ [], 5088 ^ [], 5087 ^ []]]))).
% 218.51/211.42 ncf('1.1.2.1.1',plain,[-(cons(5087 ^ [], 5088 ^ []) = cons(5087 ^ [], 5088 ^ []))],extension(2 ^ 6,bind([[_315473], [cons(5087 ^ [], 5088 ^ [])]]))).
% 218.51/211.42 ncf('1.1.2.1.2',plain,[5086 ^ [] = 5087 ^ []],extension(5092 ^ 6)).
% 218.51/211.42 ncf('1.1.2.1.3',plain,[-(occ_succeeds(5086 ^ [], 5088 ^ [], 5036 ^ [5088 ^ [], 5086 ^ []])), list_succeeds(5088 ^ [])],extension(5033 ^ 6,bind([[_487292, _487294], [5088 ^ [], 5086 ^ []]]))).
% 218.51/211.42 ncf('1.1.2.1.3.1',plain,[-(list_succeeds(5088 ^ []))],extension(5090 ^ 7)).
% 218.51/211.42 %-----------------------------------------------------
% 218.51/211.42 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------