Tool CaT
stdout:
YES(?,O(n^1))
Problem:
0(1(1(2(x1)))) -> 1(0(1(3(2(x1)))))
0(1(1(2(x1)))) -> 4(1(0(1(2(x1)))))
0(1(1(2(x1)))) -> 0(1(4(1(3(2(x1))))))
0(1(1(2(x1)))) -> 0(4(1(4(1(2(x1))))))
0(1(1(2(x1)))) -> 4(1(0(3(1(2(x1))))))
0(1(1(2(x1)))) -> 4(1(3(1(0(2(x1))))))
0(1(1(5(x1)))) -> 4(1(0(1(5(x1)))))
0(1(1(5(x1)))) -> 5(4(1(0(1(x1)))))
0(1(1(5(x1)))) -> 0(4(1(0(1(5(x1))))))
0(1(1(5(x1)))) -> 0(5(4(1(0(1(x1))))))
0(1(1(5(x1)))) -> 1(0(1(3(1(5(x1))))))
0(1(1(5(x1)))) -> 1(4(4(0(1(5(x1))))))
0(1(1(5(x1)))) -> 3(0(1(5(4(1(x1))))))
0(1(1(5(x1)))) -> 3(4(1(0(1(5(x1))))))
0(1(1(5(x1)))) -> 3(4(1(5(0(1(x1))))))
0(1(1(5(x1)))) -> 3(5(4(1(0(1(x1))))))
0(1(1(5(x1)))) -> 4(1(0(1(5(3(x1))))))
0(1(1(5(x1)))) -> 4(1(0(1(5(4(x1))))))
0(1(1(5(x1)))) -> 4(1(3(1(0(5(x1))))))
0(1(1(5(x1)))) -> 4(1(4(1(0(5(x1))))))
0(1(1(5(x1)))) -> 4(4(1(5(0(1(x1))))))
0(1(1(5(x1)))) -> 5(4(1(3(1(0(x1))))))
0(1(2(0(x1)))) -> 0(2(4(1(0(3(x1))))))
0(1(3(5(x1)))) -> 0(3(5(4(1(x1)))))
0(1(4(5(x1)))) -> 0(3(5(4(1(x1)))))
0(1(4(5(x1)))) -> 4(4(0(1(5(3(x1))))))
0(2(4(5(x1)))) -> 4(0(2(3(5(x1)))))
0(2(4(5(x1)))) -> 4(4(0(2(5(x1)))))
0(2(4(5(x1)))) -> 4(0(3(2(3(5(x1))))))
0(0(2(1(5(x1))))) -> 0(0(2(5(4(1(x1))))))
0(0(2(4(5(x1))))) -> 0(0(4(4(2(5(x1))))))
0(1(0(4(5(x1))))) -> 0(4(0(0(1(5(x1))))))
0(1(0(5(0(x1))))) -> 4(1(5(0(0(0(x1))))))
0(1(1(0(5(x1))))) -> 1(0(4(0(1(5(x1))))))
0(1(1(2(0(x1))))) -> 0(4(1(2(1(0(x1))))))
0(1(1(2(0(x1))))) -> 4(1(2(1(0(0(x1))))))
0(1(1(3(5(x1))))) -> 4(1(0(1(3(5(x1))))))
0(1(1(3(5(x1))))) -> 5(4(1(0(3(1(x1))))))
0(1(1(4(2(x1))))) -> 0(4(1(4(1(2(x1))))))
0(1(1(4(2(x1))))) -> 4(1(3(1(2(0(x1))))))
0(1(1(4(2(x1))))) -> 4(2(4(1(0(1(x1))))))
0(1(1(4(5(x1))))) -> 0(5(4(1(3(1(x1))))))
0(1(1(4(5(x1))))) -> 0(5(4(1(4(1(x1))))))
0(1(1(4(5(x1))))) -> 2(4(1(0(1(5(x1))))))
0(1(2(0(2(x1))))) -> 0(4(0(1(2(2(x1))))))
0(1(2(1(5(x1))))) -> 0(1(4(1(2(5(x1))))))
0(1(4(5(0(x1))))) -> 0(5(4(1(0(3(x1))))))
0(1(5(1(5(x1))))) -> 5(4(1(0(1(5(x1))))))
0(2(0(1(5(x1))))) -> 1(0(0(2(3(5(x1))))))
0(2(0(4(5(x1))))) -> 0(0(2(4(1(5(x1))))))
0(2(0(5(0(x1))))) -> 0(2(5(0(3(0(x1))))))
0(2(3(1(5(x1))))) -> 0(0(1(2(3(5(x1))))))
0(2(3(1(5(x1))))) -> 0(2(5(3(4(1(x1))))))
0(2(3(1(5(x1))))) -> 0(3(5(2(4(1(x1))))))
0(2(3(1(5(x1))))) -> 2(0(4(1(3(5(x1))))))
0(2(3(1(5(x1))))) -> 2(0(4(1(5(3(x1))))))
0(2(3(1(5(x1))))) -> 2(3(5(3(0(1(x1))))))
0(2(3(1(5(x1))))) -> 2(5(3(4(1(0(x1))))))
0(2(3(1(5(x1))))) -> 4(1(0(5(2(3(x1))))))
0(2(3(1(5(x1))))) -> 4(1(3(0(2(5(x1))))))
0(2(3(1(5(x1))))) -> 4(1(5(2(0(3(x1))))))
0(2(5(1(2(x1))))) -> 0(2(3(2(1(5(x1))))))
0(2(5(1(5(x1))))) -> 0(3(5(2(1(5(x1))))))
0(2(5(1(5(x1))))) -> 0(4(1(5(2(5(x1))))))
0(2(5(1(5(x1))))) -> 2(4(1(5(0(5(x1))))))
0(2(5(1(5(x1))))) -> 4(1(0(5(2(5(x1))))))
0(2(5(1(5(x1))))) -> 4(1(5(5(2(0(x1))))))
0(3(5(1(5(x1))))) -> 5(0(3(5(4(1(x1))))))
0(4(2(0(2(x1))))) -> 0(0(4(3(2(2(x1))))))
0(4(2(1(5(x1))))) -> 0(2(5(4(4(1(x1))))))
0(4(2(1(5(x1))))) -> 0(4(1(5(3(2(x1))))))
0(4(2(1(5(x1))))) -> 2(4(1(0(0(5(x1))))))
0(4(2(1(5(x1))))) -> 2(4(1(3(0(5(x1))))))
0(4(2(1(5(x1))))) -> 2(4(1(5(4(0(x1))))))
0(4(2(1(5(x1))))) -> 3(0(1(5(2(4(x1))))))
0(4(2(1(5(x1))))) -> 3(0(5(2(4(1(x1))))))
0(4(2(1(5(x1))))) -> 4(1(3(2(5(0(x1))))))
0(4(2(1(5(x1))))) -> 4(4(0(1(5(2(x1))))))
0(4(5(1(5(x1))))) -> 5(4(1(5(0(4(x1))))))
Proof:
Bounds Processor:
bound: 2
enrichment: match
automaton:
final states: {6}
transitions:
51(479) -> 480*
51(75) -> 76*
51(469) -> 470*
51(157) -> 158*
51(97) -> 98*
51(77) -> 78*
51(471) -> 472*
51(461) -> 462*
51(401) -> 402*
51(391) -> 392*
51(386) -> 387*
51(366) -> 367*
51(493) -> 494*
51(463) -> 464*
51(453) -> 454*
51(146) -> 147*
51(91) -> 92*
51(485) -> 486*
51(455) -> 456*
51(607) -> 608*
51(355) -> 356*
51(527) -> 528*
51(517) -> 518*
51(487) -> 488*
51(83) -> 84*
51(477) -> 478*
51(599) -> 600*
51(519) -> 520*
51(85) -> 86*
41(55) -> 56*
41(197) -> 198*
41(389) -> 390*
41(229) -> 230*
41(199) -> 200*
41(189) -> 190*
41(573) -> 574*
41(134) -> 135*
41(49) -> 50*
41(191) -> 192*
41(525) -> 526*
41(96) -> 97*
41(223) -> 224*
41(183) -> 184*
41(133) -> 134*
41(53) -> 54*
41(38) -> 39*
41(145) -> 146*
11(50) -> 51*
11(35) -> 36*
11(232) -> 233*
11(15) -> 16*
11(147) -> 148*
11(339) -> 340*
11(329) -> 330*
11(117) -> 118*
11(107) -> 108*
11(37) -> 38*
11(17) -> 18*
11(109) -> 110*
11(54) -> 55*
11(353) -> 354*
11(131) -> 132*
11(323) -> 324*
11(66) -> 67*
11(345) -> 346*
11(93) -> 94*
11(362) -> 363*
11(347) -> 348*
11(337) -> 338*
11(115) -> 116*
11(307) -> 308*
11(95) -> 96*
01(65) -> 66*
01(429) -> 430*
01(207) -> 208*
01(541) -> 542*
01(511) -> 512*
01(501) -> 502*
01(249) -> 250*
01(426) -> 427*
01(623) -> 624*
01(543) -> 544*
01(533) -> 534*
01(503) -> 504*
01(94) -> 95*
01(251) -> 252*
01(443) -> 444*
01(241) -> 242*
01(231) -> 232*
01(625) -> 626*
01(221) -> 222*
01(615) -> 616*
01(363) -> 364*
01(535) -> 536*
01(495) -> 496*
01(51) -> 52*
01(243) -> 244*
01(36) -> 37*
01(435) -> 436*
01(617) -> 618*
01(16) -> 17*
01(213) -> 214*
01(597) -> 598*
01(148) -> 149*
01(123) -> 124*
01(265) -> 266*
01(437) -> 438*
01(215) -> 216*
01(609) -> 610*
01(205) -> 206*
01(377) -> 378*
01(549) -> 550*
01(125) -> 126*
01(509) -> 510*
21(25) -> 26*
21(409) -> 410*
21(591) -> 592*
21(581) -> 582*
21(299) -> 300*
21(289) -> 290*
21(264) -> 265*
21(27) -> 28*
21(411) -> 412*
21(583) -> 584*
21(331) -> 332*
21(321) -> 322*
21(291) -> 292*
21(19) -> 20*
21(403) -> 404*
21(600) -> 601*
21(575) -> 576*
21(283) -> 284*
21(445) -> 446*
21(400) -> 401*
21(375) -> 376*
21(315) -> 316*
21(33) -> 34*
21(427) -> 428*
21(417) -> 418*
21(13) -> 14*
21(589) -> 590*
21(367) -> 368*
21(297) -> 298*
31(267) -> 268*
31(257) -> 258*
31(419) -> 420*
31(167) -> 168*
31(551) -> 552*
31(67) -> 68*
31(446) -> 447*
31(159) -> 160*
31(149) -> 150*
31(281) -> 282*
31(14) -> 15*
31(181) -> 182*
31(565) -> 566*
31(151) -> 152*
31(313) -> 314*
31(273) -> 274*
31(263) -> 264*
31(233) -> 234*
31(390) -> 391*
31(385) -> 386*
31(173) -> 174*
31(567) -> 568*
31(365) -> 366*
31(557) -> 558*
31(305) -> 306*
31(275) -> 276*
31(63) -> 64*
31(387) -> 388*
31(175) -> 176*
31(165) -> 166*
31(559) -> 560*
02(665) -> 666*
02(639) -> 640*
00(5) -> 6*
00(2) -> 6*
00(4) -> 6*
00(1) -> 6*
00(3) -> 6*
32(638) -> 639*
32(664) -> 665*
10(5) -> 1*
10(2) -> 1*
10(4) -> 1*
10(1) -> 1*
10(3) -> 1*
52(663) -> 664*
52(637) -> 638*
20(5) -> 2*
20(2) -> 2*
20(4) -> 2*
20(1) -> 2*
20(3) -> 2*
42(636) -> 637*
42(662) -> 663*
30(5) -> 3*
30(2) -> 3*
30(4) -> 3*
30(1) -> 3*
30(3) -> 3*
12(661) -> 662*
12(651) -> 652*
12(641) -> 642*
12(653) -> 654*
12(635) -> 636*
12(659) -> 660*
40(5) -> 4*
40(2) -> 4*
40(4) -> 4*
40(1) -> 4*
40(3) -> 4*
50(5) -> 5*
50(2) -> 5*
50(4) -> 5*
50(1) -> 5*
50(3) -> 5*
1 -> 249,197,175,115,85,27
2 -> 241,189,167,107,77,19
3 -> 251,199,181,117,91,33
4 -> 243,191,173,109,83,25
5 -> 231,183,165,93,75,13
14 -> 607,65,35
15 -> 527*
16 -> 49*
18 -> 250,232,95,315,599,6
20 -> 14*
26 -> 14*
28 -> 14*
34 -> 14*
36 -> 445,63,53
37 -> 419,133
39 -> 616,244,37,133,419,66,242,250,232,95,315,599,355,331,229,151,123,6
52 -> 616,244,66,242,37,133,419,250,232,95,315,599,519,6
54 -> 377*
56 -> 51*
64 -> 131,36
67 -> 223*
68 -> 37*
75 -> 653*
76 -> 283,263,205,35
77 -> 635*
78 -> 289,267,207,35
83 -> 651*
84 -> 291,273,213,35
85 -> 659*
86 -> 297,275,215,35
91 -> 641*
92 -> 299,281,221,35
94 -> 313,145
95 -> 385,157
97 -> 321*
98 -> 244,610,250,232,95,315,599,159,125,6
108 -> 94*
110 -> 94*
116 -> 94*
118 -> 94*
124 -> 616,244,66,37,133,419,242,250,232,95,315,599,6
126 -> 250,232,95,315,599,6
132 -> 16*
135 -> 616,244,66,242,250,232,95,315,599,6,17
146 -> 525,375,365,329
147 -> 597,257
150 -> 616,244,250,232,95,315,599,6
152 -> 250,232,95,315,599,6
158 -> 427,252,250,232,95,315,599,37
160 -> 250,232,95,315,599,6
166 -> 426,400,75
168 -> 429,403,75
174 -> 435,409,75
176 -> 437,411,75
182 -> 443,417,75
184 -> 609,575,75
190 -> 615,581,75
192 -> 617,583,75
198 -> 623,589,75
200 -> 625,591,75
206 -> 551,533,477,66
208 -> 557,535,479,66
214 -> 559,541,485,66
216 -> 565,543,487,66
222 -> 567,549,493,66
224 -> 37*
230 -> 250,232,95,315,599,6
232 -> 599,573,315
233 -> 389*
234 -> 95*
242 -> 232*
244 -> 232*
250 -> 232*
252 -> 232*
258 -> 51*
264 -> 307*
265 -> 362,305
266 -> 38*
268 -> 264*
274 -> 264*
276 -> 264*
282 -> 264*
284 -> 455,337,36
290 -> 461,339,36
292 -> 463,345,36
298 -> 469,347,36
300 -> 471,353,36
306 -> 265*
308 -> 36*
314 -> 323,94
316 -> 616,244,37,133,419,250,232,95,315,599,517,66
322 -> 38*
324 -> 96*
330 -> 96*
332 -> 66,242,6
338 -> 49*
340 -> 49*
346 -> 49*
348 -> 49*
354 -> 49*
356 -> 6*
364 -> 51*
368 -> 51*
376 -> 146*
378 -> 331*
388 -> 331*
392 -> 331*
401 -> 661*
402 -> 36*
404 -> 401*
410 -> 401*
412 -> 401*
418 -> 401*
420 -> 37*
428 -> 157*
430 -> 427*
436 -> 427*
438 -> 427*
444 -> 427*
446 -> 453*
447 -> 367*
454 -> 257*
456 -> 495,37
462 -> 501,37
464 -> 503,37
470 -> 509,37
472 -> 511,37
478 -> 37*
480 -> 37*
486 -> 37*
488 -> 37*
494 -> 37*
496 -> 37*
502 -> 37*
504 -> 37*
510 -> 37*
512 -> 37*
518 -> 157*
520 -> 6*
526 -> 366*
528 -> 37*
534 -> 37*
536 -> 37*
542 -> 37*
544 -> 37*
550 -> 37*
552 -> 37*
558 -> 37*
560 -> 37*
566 -> 37*
568 -> 37*
574 -> 157*
576 -> 146*
582 -> 146*
584 -> 146*
590 -> 146*
592 -> 146*
598 -> 149*
601 -> 67*
608 -> 35*
610 -> 157*
616 -> 157*
618 -> 157*
624 -> 157*
626 -> 157*
640 -> 37,133,419
642 -> 636*
652 -> 636*
654 -> 636*
660 -> 636*
666 -> 17*
problem:
QedTool IRC1
stdout:
MAYBE
Tool IRC2
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: innermost runtime-complexity with respect to
Rules:
{ 0(1(1(2(x1)))) -> 1(0(1(3(2(x1)))))
, 0(1(1(2(x1)))) -> 4(1(0(1(2(x1)))))
, 0(1(1(2(x1)))) -> 0(1(4(1(3(2(x1))))))
, 0(1(1(2(x1)))) -> 0(4(1(4(1(2(x1))))))
, 0(1(1(2(x1)))) -> 4(1(0(3(1(2(x1))))))
, 0(1(1(2(x1)))) -> 4(1(3(1(0(2(x1))))))
, 0(1(1(5(x1)))) -> 4(1(0(1(5(x1)))))
, 0(1(1(5(x1)))) -> 5(4(1(0(1(x1)))))
, 0(1(1(5(x1)))) -> 0(4(1(0(1(5(x1))))))
, 0(1(1(5(x1)))) -> 0(5(4(1(0(1(x1))))))
, 0(1(1(5(x1)))) -> 1(0(1(3(1(5(x1))))))
, 0(1(1(5(x1)))) -> 1(4(4(0(1(5(x1))))))
, 0(1(1(5(x1)))) -> 3(0(1(5(4(1(x1))))))
, 0(1(1(5(x1)))) -> 3(4(1(0(1(5(x1))))))
, 0(1(1(5(x1)))) -> 3(4(1(5(0(1(x1))))))
, 0(1(1(5(x1)))) -> 3(5(4(1(0(1(x1))))))
, 0(1(1(5(x1)))) -> 4(1(0(1(5(3(x1))))))
, 0(1(1(5(x1)))) -> 4(1(0(1(5(4(x1))))))
, 0(1(1(5(x1)))) -> 4(1(3(1(0(5(x1))))))
, 0(1(1(5(x1)))) -> 4(1(4(1(0(5(x1))))))
, 0(1(1(5(x1)))) -> 4(4(1(5(0(1(x1))))))
, 0(1(1(5(x1)))) -> 5(4(1(3(1(0(x1))))))
, 0(1(2(0(x1)))) -> 0(2(4(1(0(3(x1))))))
, 0(1(3(5(x1)))) -> 0(3(5(4(1(x1)))))
, 0(1(4(5(x1)))) -> 0(3(5(4(1(x1)))))
, 0(1(4(5(x1)))) -> 4(4(0(1(5(3(x1))))))
, 0(2(4(5(x1)))) -> 4(0(2(3(5(x1)))))
, 0(2(4(5(x1)))) -> 4(4(0(2(5(x1)))))
, 0(2(4(5(x1)))) -> 4(0(3(2(3(5(x1))))))
, 0(0(2(1(5(x1))))) -> 0(0(2(5(4(1(x1))))))
, 0(0(2(4(5(x1))))) -> 0(0(4(4(2(5(x1))))))
, 0(1(0(4(5(x1))))) -> 0(4(0(0(1(5(x1))))))
, 0(1(0(5(0(x1))))) -> 4(1(5(0(0(0(x1))))))
, 0(1(1(0(5(x1))))) -> 1(0(4(0(1(5(x1))))))
, 0(1(1(2(0(x1))))) -> 0(4(1(2(1(0(x1))))))
, 0(1(1(2(0(x1))))) -> 4(1(2(1(0(0(x1))))))
, 0(1(1(3(5(x1))))) -> 4(1(0(1(3(5(x1))))))
, 0(1(1(3(5(x1))))) -> 5(4(1(0(3(1(x1))))))
, 0(1(1(4(2(x1))))) -> 0(4(1(4(1(2(x1))))))
, 0(1(1(4(2(x1))))) -> 4(1(3(1(2(0(x1))))))
, 0(1(1(4(2(x1))))) -> 4(2(4(1(0(1(x1))))))
, 0(1(1(4(5(x1))))) -> 0(5(4(1(3(1(x1))))))
, 0(1(1(4(5(x1))))) -> 0(5(4(1(4(1(x1))))))
, 0(1(1(4(5(x1))))) -> 2(4(1(0(1(5(x1))))))
, 0(1(2(0(2(x1))))) -> 0(4(0(1(2(2(x1))))))
, 0(1(2(1(5(x1))))) -> 0(1(4(1(2(5(x1))))))
, 0(1(4(5(0(x1))))) -> 0(5(4(1(0(3(x1))))))
, 0(1(5(1(5(x1))))) -> 5(4(1(0(1(5(x1))))))
, 0(2(0(1(5(x1))))) -> 1(0(0(2(3(5(x1))))))
, 0(2(0(4(5(x1))))) -> 0(0(2(4(1(5(x1))))))
, 0(2(0(5(0(x1))))) -> 0(2(5(0(3(0(x1))))))
, 0(2(3(1(5(x1))))) -> 0(0(1(2(3(5(x1))))))
, 0(2(3(1(5(x1))))) -> 0(2(5(3(4(1(x1))))))
, 0(2(3(1(5(x1))))) -> 0(3(5(2(4(1(x1))))))
, 0(2(3(1(5(x1))))) -> 2(0(4(1(3(5(x1))))))
, 0(2(3(1(5(x1))))) -> 2(0(4(1(5(3(x1))))))
, 0(2(3(1(5(x1))))) -> 2(3(5(3(0(1(x1))))))
, 0(2(3(1(5(x1))))) -> 2(5(3(4(1(0(x1))))))
, 0(2(3(1(5(x1))))) -> 4(1(0(5(2(3(x1))))))
, 0(2(3(1(5(x1))))) -> 4(1(3(0(2(5(x1))))))
, 0(2(3(1(5(x1))))) -> 4(1(5(2(0(3(x1))))))
, 0(2(5(1(2(x1))))) -> 0(2(3(2(1(5(x1))))))
, 0(2(5(1(5(x1))))) -> 0(3(5(2(1(5(x1))))))
, 0(2(5(1(5(x1))))) -> 0(4(1(5(2(5(x1))))))
, 0(2(5(1(5(x1))))) -> 2(4(1(5(0(5(x1))))))
, 0(2(5(1(5(x1))))) -> 4(1(0(5(2(5(x1))))))
, 0(2(5(1(5(x1))))) -> 4(1(5(5(2(0(x1))))))
, 0(3(5(1(5(x1))))) -> 5(0(3(5(4(1(x1))))))
, 0(4(2(0(2(x1))))) -> 0(0(4(3(2(2(x1))))))
, 0(4(2(1(5(x1))))) -> 0(2(5(4(4(1(x1))))))
, 0(4(2(1(5(x1))))) -> 0(4(1(5(3(2(x1))))))
, 0(4(2(1(5(x1))))) -> 2(4(1(0(0(5(x1))))))
, 0(4(2(1(5(x1))))) -> 2(4(1(3(0(5(x1))))))
, 0(4(2(1(5(x1))))) -> 2(4(1(5(4(0(x1))))))
, 0(4(2(1(5(x1))))) -> 3(0(1(5(2(4(x1))))))
, 0(4(2(1(5(x1))))) -> 3(0(5(2(4(1(x1))))))
, 0(4(2(1(5(x1))))) -> 4(1(3(2(5(0(x1))))))
, 0(4(2(1(5(x1))))) -> 4(4(0(1(5(2(x1))))))
, 0(4(5(1(5(x1))))) -> 5(4(1(5(0(4(x1))))))}
Proof Output:
Computation stopped due to timeout after 60.0 secondsTool RC1
stdout:
MAYBE
Tool RC2
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: runtime-complexity with respect to
Rules:
{ 0(1(1(2(x1)))) -> 1(0(1(3(2(x1)))))
, 0(1(1(2(x1)))) -> 4(1(0(1(2(x1)))))
, 0(1(1(2(x1)))) -> 0(1(4(1(3(2(x1))))))
, 0(1(1(2(x1)))) -> 0(4(1(4(1(2(x1))))))
, 0(1(1(2(x1)))) -> 4(1(0(3(1(2(x1))))))
, 0(1(1(2(x1)))) -> 4(1(3(1(0(2(x1))))))
, 0(1(1(5(x1)))) -> 4(1(0(1(5(x1)))))
, 0(1(1(5(x1)))) -> 5(4(1(0(1(x1)))))
, 0(1(1(5(x1)))) -> 0(4(1(0(1(5(x1))))))
, 0(1(1(5(x1)))) -> 0(5(4(1(0(1(x1))))))
, 0(1(1(5(x1)))) -> 1(0(1(3(1(5(x1))))))
, 0(1(1(5(x1)))) -> 1(4(4(0(1(5(x1))))))
, 0(1(1(5(x1)))) -> 3(0(1(5(4(1(x1))))))
, 0(1(1(5(x1)))) -> 3(4(1(0(1(5(x1))))))
, 0(1(1(5(x1)))) -> 3(4(1(5(0(1(x1))))))
, 0(1(1(5(x1)))) -> 3(5(4(1(0(1(x1))))))
, 0(1(1(5(x1)))) -> 4(1(0(1(5(3(x1))))))
, 0(1(1(5(x1)))) -> 4(1(0(1(5(4(x1))))))
, 0(1(1(5(x1)))) -> 4(1(3(1(0(5(x1))))))
, 0(1(1(5(x1)))) -> 4(1(4(1(0(5(x1))))))
, 0(1(1(5(x1)))) -> 4(4(1(5(0(1(x1))))))
, 0(1(1(5(x1)))) -> 5(4(1(3(1(0(x1))))))
, 0(1(2(0(x1)))) -> 0(2(4(1(0(3(x1))))))
, 0(1(3(5(x1)))) -> 0(3(5(4(1(x1)))))
, 0(1(4(5(x1)))) -> 0(3(5(4(1(x1)))))
, 0(1(4(5(x1)))) -> 4(4(0(1(5(3(x1))))))
, 0(2(4(5(x1)))) -> 4(0(2(3(5(x1)))))
, 0(2(4(5(x1)))) -> 4(4(0(2(5(x1)))))
, 0(2(4(5(x1)))) -> 4(0(3(2(3(5(x1))))))
, 0(0(2(1(5(x1))))) -> 0(0(2(5(4(1(x1))))))
, 0(0(2(4(5(x1))))) -> 0(0(4(4(2(5(x1))))))
, 0(1(0(4(5(x1))))) -> 0(4(0(0(1(5(x1))))))
, 0(1(0(5(0(x1))))) -> 4(1(5(0(0(0(x1))))))
, 0(1(1(0(5(x1))))) -> 1(0(4(0(1(5(x1))))))
, 0(1(1(2(0(x1))))) -> 0(4(1(2(1(0(x1))))))
, 0(1(1(2(0(x1))))) -> 4(1(2(1(0(0(x1))))))
, 0(1(1(3(5(x1))))) -> 4(1(0(1(3(5(x1))))))
, 0(1(1(3(5(x1))))) -> 5(4(1(0(3(1(x1))))))
, 0(1(1(4(2(x1))))) -> 0(4(1(4(1(2(x1))))))
, 0(1(1(4(2(x1))))) -> 4(1(3(1(2(0(x1))))))
, 0(1(1(4(2(x1))))) -> 4(2(4(1(0(1(x1))))))
, 0(1(1(4(5(x1))))) -> 0(5(4(1(3(1(x1))))))
, 0(1(1(4(5(x1))))) -> 0(5(4(1(4(1(x1))))))
, 0(1(1(4(5(x1))))) -> 2(4(1(0(1(5(x1))))))
, 0(1(2(0(2(x1))))) -> 0(4(0(1(2(2(x1))))))
, 0(1(2(1(5(x1))))) -> 0(1(4(1(2(5(x1))))))
, 0(1(4(5(0(x1))))) -> 0(5(4(1(0(3(x1))))))
, 0(1(5(1(5(x1))))) -> 5(4(1(0(1(5(x1))))))
, 0(2(0(1(5(x1))))) -> 1(0(0(2(3(5(x1))))))
, 0(2(0(4(5(x1))))) -> 0(0(2(4(1(5(x1))))))
, 0(2(0(5(0(x1))))) -> 0(2(5(0(3(0(x1))))))
, 0(2(3(1(5(x1))))) -> 0(0(1(2(3(5(x1))))))
, 0(2(3(1(5(x1))))) -> 0(2(5(3(4(1(x1))))))
, 0(2(3(1(5(x1))))) -> 0(3(5(2(4(1(x1))))))
, 0(2(3(1(5(x1))))) -> 2(0(4(1(3(5(x1))))))
, 0(2(3(1(5(x1))))) -> 2(0(4(1(5(3(x1))))))
, 0(2(3(1(5(x1))))) -> 2(3(5(3(0(1(x1))))))
, 0(2(3(1(5(x1))))) -> 2(5(3(4(1(0(x1))))))
, 0(2(3(1(5(x1))))) -> 4(1(0(5(2(3(x1))))))
, 0(2(3(1(5(x1))))) -> 4(1(3(0(2(5(x1))))))
, 0(2(3(1(5(x1))))) -> 4(1(5(2(0(3(x1))))))
, 0(2(5(1(2(x1))))) -> 0(2(3(2(1(5(x1))))))
, 0(2(5(1(5(x1))))) -> 0(3(5(2(1(5(x1))))))
, 0(2(5(1(5(x1))))) -> 0(4(1(5(2(5(x1))))))
, 0(2(5(1(5(x1))))) -> 2(4(1(5(0(5(x1))))))
, 0(2(5(1(5(x1))))) -> 4(1(0(5(2(5(x1))))))
, 0(2(5(1(5(x1))))) -> 4(1(5(5(2(0(x1))))))
, 0(3(5(1(5(x1))))) -> 5(0(3(5(4(1(x1))))))
, 0(4(2(0(2(x1))))) -> 0(0(4(3(2(2(x1))))))
, 0(4(2(1(5(x1))))) -> 0(2(5(4(4(1(x1))))))
, 0(4(2(1(5(x1))))) -> 0(4(1(5(3(2(x1))))))
, 0(4(2(1(5(x1))))) -> 2(4(1(0(0(5(x1))))))
, 0(4(2(1(5(x1))))) -> 2(4(1(3(0(5(x1))))))
, 0(4(2(1(5(x1))))) -> 2(4(1(5(4(0(x1))))))
, 0(4(2(1(5(x1))))) -> 3(0(1(5(2(4(x1))))))
, 0(4(2(1(5(x1))))) -> 3(0(5(2(4(1(x1))))))
, 0(4(2(1(5(x1))))) -> 4(1(3(2(5(0(x1))))))
, 0(4(2(1(5(x1))))) -> 4(4(0(1(5(2(x1))))))
, 0(4(5(1(5(x1))))) -> 5(4(1(5(0(4(x1))))))}
Proof Output:
Computation stopped due to timeout after 60.0 seconds