Tool CaT
stdout:
YES(?,O(n^1))
Problem:
0(1(1(x1))) -> 0(1(2(3(4(1(x1))))))
0(1(1(x1))) -> 1(3(1(3(4(0(x1))))))
0(1(1(x1))) -> 5(1(3(0(3(1(x1))))))
0(1(4(x1))) -> 0(1(3(4(x1))))
0(1(4(x1))) -> 1(3(4(2(0(x1)))))
0(1(4(x1))) -> 1(5(3(4(0(x1)))))
0(1(4(x1))) -> 3(1(3(4(0(x1)))))
0(1(4(x1))) -> 1(1(5(3(4(0(x1))))))
0(1(4(x1))) -> 1(2(3(4(3(0(x1))))))
0(1(4(x1))) -> 1(3(3(4(4(0(x1))))))
0(1(4(x1))) -> 1(3(4(5(0(5(x1))))))
0(1(4(x1))) -> 3(4(5(5(0(1(x1))))))
1(2(4(x1))) -> 1(2(3(4(1(x1)))))
1(2(4(x1))) -> 5(3(4(1(2(x1)))))
1(2(4(x1))) -> 1(5(2(3(4(3(x1))))))
1(2(4(x1))) -> 2(3(3(4(5(1(x1))))))
5(2(1(x1))) -> 1(2(2(3(5(4(x1))))))
5(2(1(x1))) -> 1(3(2(5(3(4(x1))))))
5(2(4(x1))) -> 0(5(2(3(4(x1)))))
5(2(4(x1))) -> 5(5(3(4(2(x1)))))
5(2(4(x1))) -> 0(3(4(4(5(2(x1))))))
5(2(4(x1))) -> 2(2(5(3(4(4(x1))))))
5(2(4(x1))) -> 2(3(3(4(5(5(x1))))))
5(2(4(x1))) -> 2(3(4(3(5(3(x1))))))
5(2(4(x1))) -> 2(5(3(4(0(5(x1))))))
5(2(4(x1))) -> 3(1(2(5(3(4(x1))))))
5(2(4(x1))) -> 5(2(3(4(0(3(x1))))))
0(0(2(4(x1)))) -> 0(4(3(0(2(x1)))))
0(1(1(5(x1)))) -> 0(1(3(5(1(2(x1))))))
0(1(2(4(x1)))) -> 0(1(2(3(3(4(x1))))))
0(1(4(5(x1)))) -> 3(4(0(5(1(x1)))))
0(1(4(5(x1)))) -> 3(4(5(3(0(1(x1))))))
0(4(2(1(x1)))) -> 0(4(1(2(3(4(x1))))))
0(5(1(4(x1)))) -> 0(0(3(5(4(1(x1))))))
1(0(1(4(x1)))) -> 3(4(0(1(2(1(x1))))))
1(1(2(4(x1)))) -> 1(3(4(1(2(x1)))))
1(2(2(4(x1)))) -> 2(2(2(3(4(1(x1))))))
1(2(4(2(x1)))) -> 1(2(3(4(2(3(x1))))))
1(5(2(1(x1)))) -> 1(0(3(5(1(2(x1))))))
1(5(2(4(x1)))) -> 3(2(3(5(1(4(x1))))))
1(5(2(4(x1)))) -> 5(2(3(3(1(4(x1))))))
5(0(1(4(x1)))) -> 3(4(0(5(3(1(x1))))))
5(2(5(1(x1)))) -> 3(5(1(5(2(x1)))))
0(1(1(5(4(x1))))) -> 0(0(5(4(1(1(x1))))))
1(0(0(2(4(x1))))) -> 0(2(0(4(4(1(x1))))))
1(0(4(2(1(x1))))) -> 1(2(3(4(1(0(x1))))))
1(2(5(0(1(x1))))) -> 2(3(5(1(0(1(x1))))))
1(5(3(0(4(x1))))) -> 5(1(3(4(0(4(x1))))))
5(0(5(2(4(x1))))) -> 4(0(0(5(5(2(x1))))))
5(3(2(4(2(x1))))) -> 2(1(5(3(4(2(x1))))))
Proof:
Bounds Processor:
bound: 2
enrichment: match
automaton:
final states: {6,5,4}
transitions:
21(187) -> 188*
21(122) -> 123*
21(87) -> 88*
21(27) -> 28*
21(189) -> 190*
21(71) -> 72*
21(56) -> 57*
21(41) -> 42*
21(16) -> 17*
21(123) -> 124*
21(43) -> 44*
21(195) -> 196*
21(170) -> 171*
11(25) -> 26*
11(197) -> 198*
11(17) -> 18*
11(19) -> 20*
11(171) -> 172*
11(28) -> 29*
11(13) -> 14*
51(167) -> 168*
51(137) -> 138*
51(102) -> 103*
51(67) -> 68*
51(57) -> 58*
51(169) -> 170*
51(149) -> 150*
51(114) -> 115*
51(151) -> 152*
51(121) -> 122*
51(101) -> 102*
51(31) -> 32*
51(143) -> 144*
51(138) -> 139*
51(88) -> 89*
31(70) -> 71*
31(65) -> 66*
31(55) -> 56*
31(30) -> 31*
31(15) -> 16*
31(172) -> 173*
31(152) -> 153*
31(117) -> 118*
31(69) -> 70*
31(59) -> 60*
31(186) -> 187*
31(166) -> 167*
31(141) -> 142*
31(86) -> 87*
31(53) -> 54*
31(140) -> 141*
31(120) -> 121*
31(100) -> 101*
41(85) -> 86*
41(97) -> 98*
41(139) -> 140*
41(119) -> 120*
41(99) -> 100*
41(54) -> 55*
41(29) -> 30*
41(14) -> 15*
41(116) -> 117*
41(91) -> 92*
41(153) -> 154*
41(68) -> 69*
41(185) -> 186*
41(165) -> 166*
41(115) -> 116*
01(184) -> 185*
01(164) -> 165*
01(89) -> 90*
12(213) -> 214*
00(2) -> 4*
00(1) -> 4*
00(3) -> 4*
32(218) -> 219*
32(215) -> 216*
32(210) -> 211*
10(2) -> 5*
10(1) -> 5*
10(3) -> 5*
22(217) -> 218*
22(212) -> 213*
22(211) -> 212*
20(2) -> 1*
20(1) -> 1*
20(3) -> 1*
52(209) -> 210*
52(216) -> 217*
30(2) -> 2*
30(1) -> 2*
30(3) -> 2*
42(208) -> 209*
40(2) -> 3*
40(1) -> 3*
40(3) -> 3*
50(2) -> 6*
50(1) -> 6*
50(3) -> 6*
1 -> 143,91,59,41,19
2 -> 137,85,53,27,13
3 -> 149,97,65,43,25
14 -> 67*
17 -> 189*
18 -> 20,29,67,5
20 -> 14*
26 -> 14*
28 -> 114,99
32 -> 20,29,67,5
42 -> 28*
44 -> 28*
54 -> 195,184,151
58 -> 17*
60 -> 54*
66 -> 54*
72 -> 20,29,67,5
86 -> 119*
87 -> 169*
90 -> 115,144,138,6
92 -> 86*
98 -> 86*
102 -> 197*
103 -> 115,144,138,6
118 -> 89*
124 -> 152,115,144,138,6
138 -> 164*
142 -> 123*
144 -> 138*
150 -> 138*
154 -> 141*
168 -> 123*
173 -> 115,144,138,6
188 -> 102*
190 -> 71*
196 -> 14*
197 -> 208*
198 -> 123*
209 -> 215*
214 -> 139*
219 -> 213*
problem:
QedTool IRC1
stdout:
MAYBE
Tool IRC2
stdout:
YES(?,O(n^1))
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ 0(1(1(x1))) -> 0(1(2(3(4(1(x1))))))
, 0(1(1(x1))) -> 1(3(1(3(4(0(x1))))))
, 0(1(1(x1))) -> 5(1(3(0(3(1(x1))))))
, 0(1(4(x1))) -> 0(1(3(4(x1))))
, 0(1(4(x1))) -> 1(3(4(2(0(x1)))))
, 0(1(4(x1))) -> 1(5(3(4(0(x1)))))
, 0(1(4(x1))) -> 3(1(3(4(0(x1)))))
, 0(1(4(x1))) -> 1(1(5(3(4(0(x1))))))
, 0(1(4(x1))) -> 1(2(3(4(3(0(x1))))))
, 0(1(4(x1))) -> 1(3(3(4(4(0(x1))))))
, 0(1(4(x1))) -> 1(3(4(5(0(5(x1))))))
, 0(1(4(x1))) -> 3(4(5(5(0(1(x1))))))
, 1(2(4(x1))) -> 1(2(3(4(1(x1)))))
, 1(2(4(x1))) -> 5(3(4(1(2(x1)))))
, 1(2(4(x1))) -> 1(5(2(3(4(3(x1))))))
, 1(2(4(x1))) -> 2(3(3(4(5(1(x1))))))
, 5(2(1(x1))) -> 1(2(2(3(5(4(x1))))))
, 5(2(1(x1))) -> 1(3(2(5(3(4(x1))))))
, 5(2(4(x1))) -> 0(5(2(3(4(x1)))))
, 5(2(4(x1))) -> 5(5(3(4(2(x1)))))
, 5(2(4(x1))) -> 0(3(4(4(5(2(x1))))))
, 5(2(4(x1))) -> 2(2(5(3(4(4(x1))))))
, 5(2(4(x1))) -> 2(3(3(4(5(5(x1))))))
, 5(2(4(x1))) -> 2(3(4(3(5(3(x1))))))
, 5(2(4(x1))) -> 2(5(3(4(0(5(x1))))))
, 5(2(4(x1))) -> 3(1(2(5(3(4(x1))))))
, 5(2(4(x1))) -> 5(2(3(4(0(3(x1))))))
, 0(0(2(4(x1)))) -> 0(4(3(0(2(x1)))))
, 0(1(1(5(x1)))) -> 0(1(3(5(1(2(x1))))))
, 0(1(2(4(x1)))) -> 0(1(2(3(3(4(x1))))))
, 0(1(4(5(x1)))) -> 3(4(0(5(1(x1)))))
, 0(1(4(5(x1)))) -> 3(4(5(3(0(1(x1))))))
, 0(4(2(1(x1)))) -> 0(4(1(2(3(4(x1))))))
, 0(5(1(4(x1)))) -> 0(0(3(5(4(1(x1))))))
, 1(0(1(4(x1)))) -> 3(4(0(1(2(1(x1))))))
, 1(1(2(4(x1)))) -> 1(3(4(1(2(x1)))))
, 1(2(2(4(x1)))) -> 2(2(2(3(4(1(x1))))))
, 1(2(4(2(x1)))) -> 1(2(3(4(2(3(x1))))))
, 1(5(2(1(x1)))) -> 1(0(3(5(1(2(x1))))))
, 1(5(2(4(x1)))) -> 3(2(3(5(1(4(x1))))))
, 1(5(2(4(x1)))) -> 5(2(3(3(1(4(x1))))))
, 5(0(1(4(x1)))) -> 3(4(0(5(3(1(x1))))))
, 5(2(5(1(x1)))) -> 3(5(1(5(2(x1)))))
, 0(1(1(5(4(x1))))) -> 0(0(5(4(1(1(x1))))))
, 1(0(0(2(4(x1))))) -> 0(2(0(4(4(1(x1))))))
, 1(0(4(2(1(x1))))) -> 1(2(3(4(1(0(x1))))))
, 1(2(5(0(1(x1))))) -> 2(3(5(1(0(1(x1))))))
, 1(5(3(0(4(x1))))) -> 5(1(3(4(0(4(x1))))))
, 5(0(5(2(4(x1))))) -> 4(0(0(5(5(2(x1))))))
, 5(3(2(4(2(x1))))) -> 2(1(5(3(4(2(x1))))))}
Proof Output:
'Bounds with perSymbol-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with perSymbol-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with perSymbol-enrichment and initial automaton 'match''
----------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ 0(1(1(x1))) -> 0(1(2(3(4(1(x1))))))
, 0(1(1(x1))) -> 1(3(1(3(4(0(x1))))))
, 0(1(1(x1))) -> 5(1(3(0(3(1(x1))))))
, 0(1(4(x1))) -> 0(1(3(4(x1))))
, 0(1(4(x1))) -> 1(3(4(2(0(x1)))))
, 0(1(4(x1))) -> 1(5(3(4(0(x1)))))
, 0(1(4(x1))) -> 3(1(3(4(0(x1)))))
, 0(1(4(x1))) -> 1(1(5(3(4(0(x1))))))
, 0(1(4(x1))) -> 1(2(3(4(3(0(x1))))))
, 0(1(4(x1))) -> 1(3(3(4(4(0(x1))))))
, 0(1(4(x1))) -> 1(3(4(5(0(5(x1))))))
, 0(1(4(x1))) -> 3(4(5(5(0(1(x1))))))
, 1(2(4(x1))) -> 1(2(3(4(1(x1)))))
, 1(2(4(x1))) -> 5(3(4(1(2(x1)))))
, 1(2(4(x1))) -> 1(5(2(3(4(3(x1))))))
, 1(2(4(x1))) -> 2(3(3(4(5(1(x1))))))
, 5(2(1(x1))) -> 1(2(2(3(5(4(x1))))))
, 5(2(1(x1))) -> 1(3(2(5(3(4(x1))))))
, 5(2(4(x1))) -> 0(5(2(3(4(x1)))))
, 5(2(4(x1))) -> 5(5(3(4(2(x1)))))
, 5(2(4(x1))) -> 0(3(4(4(5(2(x1))))))
, 5(2(4(x1))) -> 2(2(5(3(4(4(x1))))))
, 5(2(4(x1))) -> 2(3(3(4(5(5(x1))))))
, 5(2(4(x1))) -> 2(3(4(3(5(3(x1))))))
, 5(2(4(x1))) -> 2(5(3(4(0(5(x1))))))
, 5(2(4(x1))) -> 3(1(2(5(3(4(x1))))))
, 5(2(4(x1))) -> 5(2(3(4(0(3(x1))))))
, 0(0(2(4(x1)))) -> 0(4(3(0(2(x1)))))
, 0(1(1(5(x1)))) -> 0(1(3(5(1(2(x1))))))
, 0(1(2(4(x1)))) -> 0(1(2(3(3(4(x1))))))
, 0(1(4(5(x1)))) -> 3(4(0(5(1(x1)))))
, 0(1(4(5(x1)))) -> 3(4(5(3(0(1(x1))))))
, 0(4(2(1(x1)))) -> 0(4(1(2(3(4(x1))))))
, 0(5(1(4(x1)))) -> 0(0(3(5(4(1(x1))))))
, 1(0(1(4(x1)))) -> 3(4(0(1(2(1(x1))))))
, 1(1(2(4(x1)))) -> 1(3(4(1(2(x1)))))
, 1(2(2(4(x1)))) -> 2(2(2(3(4(1(x1))))))
, 1(2(4(2(x1)))) -> 1(2(3(4(2(3(x1))))))
, 1(5(2(1(x1)))) -> 1(0(3(5(1(2(x1))))))
, 1(5(2(4(x1)))) -> 3(2(3(5(1(4(x1))))))
, 1(5(2(4(x1)))) -> 5(2(3(3(1(4(x1))))))
, 5(0(1(4(x1)))) -> 3(4(0(5(3(1(x1))))))
, 5(2(5(1(x1)))) -> 3(5(1(5(2(x1)))))
, 0(1(1(5(4(x1))))) -> 0(0(5(4(1(1(x1))))))
, 1(0(0(2(4(x1))))) -> 0(2(0(4(4(1(x1))))))
, 1(0(4(2(1(x1))))) -> 1(2(3(4(1(0(x1))))))
, 1(2(5(0(1(x1))))) -> 2(3(5(1(0(1(x1))))))
, 1(5(3(0(4(x1))))) -> 5(1(3(4(0(4(x1))))))
, 5(0(5(2(4(x1))))) -> 4(0(0(5(5(2(x1))))))
, 5(3(2(4(2(x1))))) -> 2(1(5(3(4(2(x1))))))}
Proof Output:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ 0_0(3) -> 1
, 0_0(4) -> 1
, 0_0(5) -> 1
, 0_1(18) -> 51
, 0_1(23) -> 6
, 0_1(23) -> 32
, 0_1(23) -> 40
, 0_1(40) -> 45
, 1_0(3) -> 2
, 1_0(4) -> 2
, 1_0(5) -> 2
, 1_1(3) -> 10
, 1_1(4) -> 10
, 1_1(5) -> 10
, 1_1(7) -> 2
, 1_1(7) -> 10
, 1_1(7) -> 13
, 1_1(14) -> 13
, 1_1(27) -> 33
, 1_1(47) -> 46
, 1_2(52) -> 39
, 2_0(3) -> 3
, 2_0(4) -> 3
, 2_0(5) -> 3
, 2_1(3) -> 14
, 2_1(4) -> 14
, 2_1(5) -> 14
, 2_1(7) -> 19
, 2_1(8) -> 7
, 2_1(16) -> 15
, 2_1(18) -> 10
, 2_1(19) -> 2
, 2_1(19) -> 10
, 2_1(19) -> 13
, 2_1(25) -> 24
, 2_1(33) -> 6
, 2_1(33) -> 32
, 2_1(33) -> 40
, 2_1(33) -> 42
, 2_1(34) -> 33
, 2_1(48) -> 47
, 2_1(49) -> 27
, 2_2(53) -> 52
, 2_2(54) -> 53
, 2_2(58) -> 57
, 3_0(3) -> 4
, 3_0(4) -> 4
, 3_0(5) -> 4
, 3_1(3) -> 18
, 3_1(4) -> 18
, 3_1(5) -> 18
, 3_1(9) -> 8
, 3_1(12) -> 11
, 3_1(17) -> 16
, 3_1(20) -> 19
, 3_1(21) -> 20
, 3_1(26) -> 25
, 3_1(29) -> 28
, 3_1(30) -> 23
, 3_1(36) -> 35
, 3_1(37) -> 33
, 3_1(38) -> 37
, 3_1(42) -> 41
, 3_1(44) -> 43
, 3_1(46) -> 6
, 3_1(46) -> 32
, 3_1(46) -> 40
, 3_1(50) -> 49
, 3_2(55) -> 54
, 3_2(56) -> 59
, 3_2(57) -> 52
, 4_0(3) -> 5
, 4_0(4) -> 5
, 4_0(5) -> 5
, 4_1(3) -> 26
, 4_1(4) -> 26
, 4_1(5) -> 26
, 4_1(10) -> 9
, 4_1(13) -> 12
, 4_1(14) -> 29
, 4_1(18) -> 17
, 4_1(22) -> 21
, 4_1(26) -> 36
, 4_1(31) -> 30
, 4_1(32) -> 31
, 4_1(39) -> 38
, 4_1(41) -> 37
, 4_1(45) -> 44
, 4_1(51) -> 50
, 4_2(27) -> 56
, 5_0(3) -> 6
, 5_0(4) -> 6
, 5_0(5) -> 6
, 5_1(3) -> 40
, 5_1(4) -> 40
, 5_1(5) -> 40
, 5_1(10) -> 22
, 5_1(11) -> 2
, 5_1(11) -> 10
, 5_1(11) -> 13
, 5_1(14) -> 32
, 5_1(15) -> 7
, 5_1(18) -> 42
, 5_1(24) -> 23
, 5_1(25) -> 48
, 5_1(27) -> 6
, 5_1(27) -> 32
, 5_1(27) -> 40
, 5_1(28) -> 27
, 5_1(35) -> 34
, 5_1(40) -> 39
, 5_1(43) -> 33
, 5_2(56) -> 55
, 5_2(59) -> 58}Tool RC1
stdout:
MAYBE
Tool RC2
stdout:
YES(?,O(n^1))
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ 0(1(1(x1))) -> 0(1(2(3(4(1(x1))))))
, 0(1(1(x1))) -> 1(3(1(3(4(0(x1))))))
, 0(1(1(x1))) -> 5(1(3(0(3(1(x1))))))
, 0(1(4(x1))) -> 0(1(3(4(x1))))
, 0(1(4(x1))) -> 1(3(4(2(0(x1)))))
, 0(1(4(x1))) -> 1(5(3(4(0(x1)))))
, 0(1(4(x1))) -> 3(1(3(4(0(x1)))))
, 0(1(4(x1))) -> 1(1(5(3(4(0(x1))))))
, 0(1(4(x1))) -> 1(2(3(4(3(0(x1))))))
, 0(1(4(x1))) -> 1(3(3(4(4(0(x1))))))
, 0(1(4(x1))) -> 1(3(4(5(0(5(x1))))))
, 0(1(4(x1))) -> 3(4(5(5(0(1(x1))))))
, 1(2(4(x1))) -> 1(2(3(4(1(x1)))))
, 1(2(4(x1))) -> 5(3(4(1(2(x1)))))
, 1(2(4(x1))) -> 1(5(2(3(4(3(x1))))))
, 1(2(4(x1))) -> 2(3(3(4(5(1(x1))))))
, 5(2(1(x1))) -> 1(2(2(3(5(4(x1))))))
, 5(2(1(x1))) -> 1(3(2(5(3(4(x1))))))
, 5(2(4(x1))) -> 0(5(2(3(4(x1)))))
, 5(2(4(x1))) -> 5(5(3(4(2(x1)))))
, 5(2(4(x1))) -> 0(3(4(4(5(2(x1))))))
, 5(2(4(x1))) -> 2(2(5(3(4(4(x1))))))
, 5(2(4(x1))) -> 2(3(3(4(5(5(x1))))))
, 5(2(4(x1))) -> 2(3(4(3(5(3(x1))))))
, 5(2(4(x1))) -> 2(5(3(4(0(5(x1))))))
, 5(2(4(x1))) -> 3(1(2(5(3(4(x1))))))
, 5(2(4(x1))) -> 5(2(3(4(0(3(x1))))))
, 0(0(2(4(x1)))) -> 0(4(3(0(2(x1)))))
, 0(1(1(5(x1)))) -> 0(1(3(5(1(2(x1))))))
, 0(1(2(4(x1)))) -> 0(1(2(3(3(4(x1))))))
, 0(1(4(5(x1)))) -> 3(4(0(5(1(x1)))))
, 0(1(4(5(x1)))) -> 3(4(5(3(0(1(x1))))))
, 0(4(2(1(x1)))) -> 0(4(1(2(3(4(x1))))))
, 0(5(1(4(x1)))) -> 0(0(3(5(4(1(x1))))))
, 1(0(1(4(x1)))) -> 3(4(0(1(2(1(x1))))))
, 1(1(2(4(x1)))) -> 1(3(4(1(2(x1)))))
, 1(2(2(4(x1)))) -> 2(2(2(3(4(1(x1))))))
, 1(2(4(2(x1)))) -> 1(2(3(4(2(3(x1))))))
, 1(5(2(1(x1)))) -> 1(0(3(5(1(2(x1))))))
, 1(5(2(4(x1)))) -> 3(2(3(5(1(4(x1))))))
, 1(5(2(4(x1)))) -> 5(2(3(3(1(4(x1))))))
, 5(0(1(4(x1)))) -> 3(4(0(5(3(1(x1))))))
, 5(2(5(1(x1)))) -> 3(5(1(5(2(x1)))))
, 0(1(1(5(4(x1))))) -> 0(0(5(4(1(1(x1))))))
, 1(0(0(2(4(x1))))) -> 0(2(0(4(4(1(x1))))))
, 1(0(4(2(1(x1))))) -> 1(2(3(4(1(0(x1))))))
, 1(2(5(0(1(x1))))) -> 2(3(5(1(0(1(x1))))))
, 1(5(3(0(4(x1))))) -> 5(1(3(4(0(4(x1))))))
, 5(0(5(2(4(x1))))) -> 4(0(0(5(5(2(x1))))))
, 5(3(2(4(2(x1))))) -> 2(1(5(3(4(2(x1))))))}
Proof Output:
'Bounds with perSymbol-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with perSymbol-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with perSymbol-enrichment and initial automaton 'match''
----------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ 0(1(1(x1))) -> 0(1(2(3(4(1(x1))))))
, 0(1(1(x1))) -> 1(3(1(3(4(0(x1))))))
, 0(1(1(x1))) -> 5(1(3(0(3(1(x1))))))
, 0(1(4(x1))) -> 0(1(3(4(x1))))
, 0(1(4(x1))) -> 1(3(4(2(0(x1)))))
, 0(1(4(x1))) -> 1(5(3(4(0(x1)))))
, 0(1(4(x1))) -> 3(1(3(4(0(x1)))))
, 0(1(4(x1))) -> 1(1(5(3(4(0(x1))))))
, 0(1(4(x1))) -> 1(2(3(4(3(0(x1))))))
, 0(1(4(x1))) -> 1(3(3(4(4(0(x1))))))
, 0(1(4(x1))) -> 1(3(4(5(0(5(x1))))))
, 0(1(4(x1))) -> 3(4(5(5(0(1(x1))))))
, 1(2(4(x1))) -> 1(2(3(4(1(x1)))))
, 1(2(4(x1))) -> 5(3(4(1(2(x1)))))
, 1(2(4(x1))) -> 1(5(2(3(4(3(x1))))))
, 1(2(4(x1))) -> 2(3(3(4(5(1(x1))))))
, 5(2(1(x1))) -> 1(2(2(3(5(4(x1))))))
, 5(2(1(x1))) -> 1(3(2(5(3(4(x1))))))
, 5(2(4(x1))) -> 0(5(2(3(4(x1)))))
, 5(2(4(x1))) -> 5(5(3(4(2(x1)))))
, 5(2(4(x1))) -> 0(3(4(4(5(2(x1))))))
, 5(2(4(x1))) -> 2(2(5(3(4(4(x1))))))
, 5(2(4(x1))) -> 2(3(3(4(5(5(x1))))))
, 5(2(4(x1))) -> 2(3(4(3(5(3(x1))))))
, 5(2(4(x1))) -> 2(5(3(4(0(5(x1))))))
, 5(2(4(x1))) -> 3(1(2(5(3(4(x1))))))
, 5(2(4(x1))) -> 5(2(3(4(0(3(x1))))))
, 0(0(2(4(x1)))) -> 0(4(3(0(2(x1)))))
, 0(1(1(5(x1)))) -> 0(1(3(5(1(2(x1))))))
, 0(1(2(4(x1)))) -> 0(1(2(3(3(4(x1))))))
, 0(1(4(5(x1)))) -> 3(4(0(5(1(x1)))))
, 0(1(4(5(x1)))) -> 3(4(5(3(0(1(x1))))))
, 0(4(2(1(x1)))) -> 0(4(1(2(3(4(x1))))))
, 0(5(1(4(x1)))) -> 0(0(3(5(4(1(x1))))))
, 1(0(1(4(x1)))) -> 3(4(0(1(2(1(x1))))))
, 1(1(2(4(x1)))) -> 1(3(4(1(2(x1)))))
, 1(2(2(4(x1)))) -> 2(2(2(3(4(1(x1))))))
, 1(2(4(2(x1)))) -> 1(2(3(4(2(3(x1))))))
, 1(5(2(1(x1)))) -> 1(0(3(5(1(2(x1))))))
, 1(5(2(4(x1)))) -> 3(2(3(5(1(4(x1))))))
, 1(5(2(4(x1)))) -> 5(2(3(3(1(4(x1))))))
, 5(0(1(4(x1)))) -> 3(4(0(5(3(1(x1))))))
, 5(2(5(1(x1)))) -> 3(5(1(5(2(x1)))))
, 0(1(1(5(4(x1))))) -> 0(0(5(4(1(1(x1))))))
, 1(0(0(2(4(x1))))) -> 0(2(0(4(4(1(x1))))))
, 1(0(4(2(1(x1))))) -> 1(2(3(4(1(0(x1))))))
, 1(2(5(0(1(x1))))) -> 2(3(5(1(0(1(x1))))))
, 1(5(3(0(4(x1))))) -> 5(1(3(4(0(4(x1))))))
, 5(0(5(2(4(x1))))) -> 4(0(0(5(5(2(x1))))))
, 5(3(2(4(2(x1))))) -> 2(1(5(3(4(2(x1))))))}
Proof Output:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ 0_0(3) -> 1
, 0_0(4) -> 1
, 0_0(5) -> 1
, 0_1(18) -> 51
, 0_1(23) -> 6
, 0_1(23) -> 32
, 0_1(23) -> 40
, 0_1(40) -> 45
, 1_0(3) -> 2
, 1_0(4) -> 2
, 1_0(5) -> 2
, 1_1(3) -> 10
, 1_1(4) -> 10
, 1_1(5) -> 10
, 1_1(7) -> 2
, 1_1(7) -> 10
, 1_1(7) -> 13
, 1_1(14) -> 13
, 1_1(27) -> 33
, 1_1(47) -> 46
, 1_2(52) -> 39
, 2_0(3) -> 3
, 2_0(4) -> 3
, 2_0(5) -> 3
, 2_1(3) -> 14
, 2_1(4) -> 14
, 2_1(5) -> 14
, 2_1(7) -> 19
, 2_1(8) -> 7
, 2_1(16) -> 15
, 2_1(18) -> 10
, 2_1(19) -> 2
, 2_1(19) -> 10
, 2_1(19) -> 13
, 2_1(25) -> 24
, 2_1(33) -> 6
, 2_1(33) -> 32
, 2_1(33) -> 40
, 2_1(33) -> 42
, 2_1(34) -> 33
, 2_1(48) -> 47
, 2_1(49) -> 27
, 2_2(53) -> 52
, 2_2(54) -> 53
, 2_2(58) -> 57
, 3_0(3) -> 4
, 3_0(4) -> 4
, 3_0(5) -> 4
, 3_1(3) -> 18
, 3_1(4) -> 18
, 3_1(5) -> 18
, 3_1(9) -> 8
, 3_1(12) -> 11
, 3_1(17) -> 16
, 3_1(20) -> 19
, 3_1(21) -> 20
, 3_1(26) -> 25
, 3_1(29) -> 28
, 3_1(30) -> 23
, 3_1(36) -> 35
, 3_1(37) -> 33
, 3_1(38) -> 37
, 3_1(42) -> 41
, 3_1(44) -> 43
, 3_1(46) -> 6
, 3_1(46) -> 32
, 3_1(46) -> 40
, 3_1(50) -> 49
, 3_2(55) -> 54
, 3_2(56) -> 59
, 3_2(57) -> 52
, 4_0(3) -> 5
, 4_0(4) -> 5
, 4_0(5) -> 5
, 4_1(3) -> 26
, 4_1(4) -> 26
, 4_1(5) -> 26
, 4_1(10) -> 9
, 4_1(13) -> 12
, 4_1(14) -> 29
, 4_1(18) -> 17
, 4_1(22) -> 21
, 4_1(26) -> 36
, 4_1(31) -> 30
, 4_1(32) -> 31
, 4_1(39) -> 38
, 4_1(41) -> 37
, 4_1(45) -> 44
, 4_1(51) -> 50
, 4_2(27) -> 56
, 5_0(3) -> 6
, 5_0(4) -> 6
, 5_0(5) -> 6
, 5_1(3) -> 40
, 5_1(4) -> 40
, 5_1(5) -> 40
, 5_1(10) -> 22
, 5_1(11) -> 2
, 5_1(11) -> 10
, 5_1(11) -> 13
, 5_1(14) -> 32
, 5_1(15) -> 7
, 5_1(18) -> 42
, 5_1(24) -> 23
, 5_1(25) -> 48
, 5_1(27) -> 6
, 5_1(27) -> 32
, 5_1(27) -> 40
, 5_1(28) -> 27
, 5_1(35) -> 34
, 5_1(40) -> 39
, 5_1(43) -> 33
, 5_2(56) -> 55
, 5_2(59) -> 58}