Tool CaT
stdout:
YES(?,O(n^1))
Problem:
2(7(x1)) -> 1(8(x1))
2(8(1(x1))) -> 8(x1)
2(8(x1)) -> 4(x1)
5(9(x1)) -> 0(x1)
4(x1) -> 5(2(3(x1)))
5(3(x1)) -> 6(0(x1))
2(8(x1)) -> 7(x1)
4(7(x1)) -> 1(3(x1))
5(2(6(x1))) -> 6(2(4(x1)))
9(7(x1)) -> 7(5(x1))
7(2(x1)) -> 4(x1)
7(0(x1)) -> 9(3(x1))
6(9(x1)) -> 9(x1)
9(5(9(x1))) -> 5(7(x1))
4(x1) -> 9(6(6(x1)))
9(x1) -> 6(7(x1))
6(2(x1)) -> 7(7(x1))
2(4(x1)) -> 0(7(x1))
6(6(x1)) -> 3(x1)
0(3(x1)) -> 5(3(x1))
Proof:
Bounds Processor:
bound: 3
enrichment: match
automaton:
final states: {10,9,8,7,6,5,4}
transitions:
51(111) -> 112*
51(41) -> 42*
51(113) -> 114*
51(105) -> 106*
31(49) -> 50*
31(39) -> 40*
31(43) -> 44*
61(97) -> 98*
61(87) -> 88*
61(77) -> 78*
61(52) -> 53*
61(89) -> 90*
61(103) -> 104*
61(78) -> 79*
61(95) -> 96*
71(75) -> 76*
71(67) -> 68*
71(69) -> 70*
91(79) -> 80*
01(59) -> 60*
01(61) -> 62*
01(51) -> 52*
21(40) -> 41*
41(29) -> 30*
41(31) -> 32*
41(23) -> 24*
81(15) -> 16*
81(21) -> 22*
81(13) -> 14*
32(177) -> 178*
32(121) -> 122*
32(183) -> 184*
32(205) -> 206*
32(185) -> 186*
32(135) -> 136*
32(125) -> 126*
62(172) -> 173*
62(167) -> 168*
62(152) -> 153*
62(164) -> 165*
62(151) -> 152*
62(141) -> 142*
62(163) -> 164*
20(2) -> 4*
20(1) -> 4*
20(3) -> 4*
72(171) -> 172*
70(2) -> 8*
70(1) -> 8*
70(3) -> 8*
92(153) -> 154*
92(165) -> 166*
10(2) -> 1*
10(1) -> 1*
10(3) -> 1*
02(149) -> 150*
02(143) -> 144*
02(140) -> 141*
80(2) -> 2*
80(1) -> 2*
80(3) -> 2*
52(127) -> 128*
52(123) -> 124*
40(2) -> 6*
40(1) -> 6*
40(3) -> 6*
22(122) -> 123*
22(126) -> 127*
50(2) -> 5*
50(1) -> 5*
50(3) -> 5*
33(217) -> 218*
33(209) -> 210*
33(203) -> 204*
33(215) -> 216*
90(2) -> 7*
90(1) -> 7*
90(3) -> 7*
63(196) -> 197*
63(193) -> 194*
00(2) -> 10*
00(1) -> 10*
00(3) -> 10*
73(192) -> 193*
73(195) -> 196*
30(2) -> 3*
30(1) -> 3*
30(3) -> 3*
60(2) -> 9*
60(1) -> 9*
60(3) -> 9*
1 -> 87,69,59,43,29,15
2 -> 89,67,51,49,23,13
3 -> 77,75,61,39,31,21
14 -> 4*
16 -> 4*
22 -> 4*
23 -> 163,125
24 -> 4*
29 -> 167,135
30 -> 4*
31 -> 151,121
32 -> 4*
39 -> 143*
40 -> 113*
42 -> 6*
43 -> 149*
44 -> 111,40
49 -> 140*
50 -> 105,40
53 -> 5*
60 -> 52*
62 -> 52*
68 -> 103,4
70 -> 97,4
76 -> 95,4
77 -> 183*
79 -> 171*
80 -> 6*
87 -> 177*
88 -> 78*
89 -> 185*
90 -> 78*
96 -> 7*
98 -> 7*
104 -> 7*
106 -> 144,141,62,52,10
112 -> 144,141,62,52,10
114 -> 144,141,62,52,10
124 -> 30,32
128 -> 24*
136 -> 122*
141 -> 217,205
142 -> 112,106,114
144 -> 141*
150 -> 141*
151 -> 215*
153 -> 192*
154 -> 30,32
163 -> 203*
165 -> 195*
166 -> 24*
167 -> 209*
168 -> 152*
173 -> 80,6
178 -> 79*
184 -> 79*
186 -> 79*
194 -> 154,32,30
197 -> 166*
204 -> 165*
206 -> 53,5
210 -> 153*
216 -> 153*
218 -> 142*
problem:
QedTool IRC1
stdout:
YES(?,O(n^1))
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:
{ 2(7(x1)) -> 1(8(x1))
, 2(8(1(x1))) -> 8(x1)
, 2(8(x1)) -> 4(x1)
, 5(9(x1)) -> 0(x1)
, 4(x1) -> 5(2(3(x1)))
, 5(3(x1)) -> 6(0(x1))
, 2(8(x1)) -> 7(x1)
, 4(7(x1)) -> 1(3(x1))
, 5(2(6(x1))) -> 6(2(4(x1)))
, 9(7(x1)) -> 7(5(x1))
, 7(2(x1)) -> 4(x1)
, 7(0(x1)) -> 9(3(x1))
, 6(9(x1)) -> 9(x1)
, 9(5(9(x1))) -> 5(7(x1))
, 4(x1) -> 9(6(6(x1)))
, 9(x1) -> 6(7(x1))
, 6(2(x1)) -> 7(7(x1))
, 2(4(x1)) -> 0(7(x1))
, 6(6(x1)) -> 3(x1)
, 0(3(x1)) -> 5(3(x1))}
Proof Output:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with minimal-enrichment and initial automaton 'match''
--------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ 2(7(x1)) -> 1(8(x1))
, 2(8(1(x1))) -> 8(x1)
, 2(8(x1)) -> 4(x1)
, 5(9(x1)) -> 0(x1)
, 4(x1) -> 5(2(3(x1)))
, 5(3(x1)) -> 6(0(x1))
, 2(8(x1)) -> 7(x1)
, 4(7(x1)) -> 1(3(x1))
, 5(2(6(x1))) -> 6(2(4(x1)))
, 9(7(x1)) -> 7(5(x1))
, 7(2(x1)) -> 4(x1)
, 7(0(x1)) -> 9(3(x1))
, 6(9(x1)) -> 9(x1)
, 9(5(9(x1))) -> 5(7(x1))
, 4(x1) -> 9(6(6(x1)))
, 9(x1) -> 6(7(x1))
, 6(2(x1)) -> 7(7(x1))
, 2(4(x1)) -> 0(7(x1))
, 6(6(x1)) -> 3(x1)
, 0(3(x1)) -> 5(3(x1))}
Proof Output:
The problem is match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ 2_0(2) -> 1
, 2_1(4) -> 3
, 2_2(6) -> 5
, 7_0(2) -> 1
, 7_1(1) -> 1
, 7_1(2) -> 1
, 7_2(2) -> 12
, 7_2(4) -> 12
, 7_2(8) -> 12
, 7_3(2) -> 13
, 7_3(4) -> 13
, 7_3(8) -> 13
, 7_3(10) -> 13
, 1_0(2) -> 2
, 8_0(2) -> 2
, 8_1(2) -> 1
, 4_0(2) -> 1
, 4_1(2) -> 1
, 5_0(2) -> 1
, 5_1(3) -> 1
, 5_1(4) -> 1
, 5_1(4) -> 7
, 5_1(4) -> 12
, 5_2(5) -> 1
, 9_0(2) -> 1
, 9_1(2) -> 1
, 9_1(4) -> 1
, 9_1(8) -> 1
, 9_2(2) -> 1
, 9_2(4) -> 1
, 9_2(8) -> 1
, 9_2(10) -> 1
, 0_0(2) -> 1
, 0_1(2) -> 7
, 0_2(2) -> 12
, 3_0(2) -> 2
, 3_1(2) -> 1
, 3_1(2) -> 4
, 3_2(1) -> 1
, 3_2(2) -> 6
, 3_2(2) -> 8
, 3_2(7) -> 1
, 3_2(12) -> 1
, 3_2(13) -> 1
, 3_3(2) -> 10
, 3_3(12) -> 1
, 3_3(12) -> 7
, 3_3(12) -> 12
, 6_0(2) -> 1
, 6_1(1) -> 1
, 6_1(2) -> 9
, 6_1(7) -> 1
, 6_1(9) -> 8
, 6_2(2) -> 11
, 6_2(11) -> 10
, 6_2(12) -> 1
, 6_2(12) -> 7
, 6_2(12) -> 12
, 6_3(13) -> 1}Tool RC1
stdout:
YES(?,O(n^1))
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:
{ 2(7(x1)) -> 1(8(x1))
, 2(8(1(x1))) -> 8(x1)
, 2(8(x1)) -> 4(x1)
, 5(9(x1)) -> 0(x1)
, 4(x1) -> 5(2(3(x1)))
, 5(3(x1)) -> 6(0(x1))
, 2(8(x1)) -> 7(x1)
, 4(7(x1)) -> 1(3(x1))
, 5(2(6(x1))) -> 6(2(4(x1)))
, 9(7(x1)) -> 7(5(x1))
, 7(2(x1)) -> 4(x1)
, 7(0(x1)) -> 9(3(x1))
, 6(9(x1)) -> 9(x1)
, 9(5(9(x1))) -> 5(7(x1))
, 4(x1) -> 9(6(6(x1)))
, 9(x1) -> 6(7(x1))
, 6(2(x1)) -> 7(7(x1))
, 2(4(x1)) -> 0(7(x1))
, 6(6(x1)) -> 3(x1)
, 0(3(x1)) -> 5(3(x1))}
Proof Output:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with minimal-enrichment and initial automaton 'match''
--------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ 2(7(x1)) -> 1(8(x1))
, 2(8(1(x1))) -> 8(x1)
, 2(8(x1)) -> 4(x1)
, 5(9(x1)) -> 0(x1)
, 4(x1) -> 5(2(3(x1)))
, 5(3(x1)) -> 6(0(x1))
, 2(8(x1)) -> 7(x1)
, 4(7(x1)) -> 1(3(x1))
, 5(2(6(x1))) -> 6(2(4(x1)))
, 9(7(x1)) -> 7(5(x1))
, 7(2(x1)) -> 4(x1)
, 7(0(x1)) -> 9(3(x1))
, 6(9(x1)) -> 9(x1)
, 9(5(9(x1))) -> 5(7(x1))
, 4(x1) -> 9(6(6(x1)))
, 9(x1) -> 6(7(x1))
, 6(2(x1)) -> 7(7(x1))
, 2(4(x1)) -> 0(7(x1))
, 6(6(x1)) -> 3(x1)
, 0(3(x1)) -> 5(3(x1))}
Proof Output:
The problem is match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ 2_0(2) -> 1
, 2_1(4) -> 3
, 2_2(6) -> 5
, 7_0(2) -> 1
, 7_1(1) -> 1
, 7_1(2) -> 1
, 7_2(2) -> 12
, 7_2(4) -> 12
, 7_2(8) -> 12
, 7_3(2) -> 13
, 7_3(4) -> 13
, 7_3(8) -> 13
, 7_3(10) -> 13
, 1_0(2) -> 2
, 8_0(2) -> 2
, 8_1(2) -> 1
, 4_0(2) -> 1
, 4_1(2) -> 1
, 5_0(2) -> 1
, 5_1(3) -> 1
, 5_1(4) -> 1
, 5_1(4) -> 7
, 5_1(4) -> 12
, 5_2(5) -> 1
, 9_0(2) -> 1
, 9_1(2) -> 1
, 9_1(4) -> 1
, 9_1(8) -> 1
, 9_2(2) -> 1
, 9_2(4) -> 1
, 9_2(8) -> 1
, 9_2(10) -> 1
, 0_0(2) -> 1
, 0_1(2) -> 7
, 0_2(2) -> 12
, 3_0(2) -> 2
, 3_1(2) -> 1
, 3_1(2) -> 4
, 3_2(1) -> 1
, 3_2(2) -> 6
, 3_2(2) -> 8
, 3_2(7) -> 1
, 3_2(12) -> 1
, 3_2(13) -> 1
, 3_3(2) -> 10
, 3_3(12) -> 1
, 3_3(12) -> 7
, 3_3(12) -> 12
, 6_0(2) -> 1
, 6_1(1) -> 1
, 6_1(2) -> 9
, 6_1(7) -> 1
, 6_1(9) -> 8
, 6_2(2) -> 11
, 6_2(11) -> 10
, 6_2(12) -> 1
, 6_2(12) -> 7
, 6_2(12) -> 12
, 6_3(13) -> 1}