Tool CaT
stdout:
YES(?,O(n^1))
Problem:
0(1(2(3(4(x1))))) -> 0(2(1(3(4(x1)))))
0(5(1(2(4(3(x1)))))) -> 0(5(2(1(4(3(x1))))))
0(5(2(4(1(3(x1)))))) -> 0(1(5(2(4(3(x1))))))
0(5(3(1(2(4(x1)))))) -> 0(1(5(3(2(4(x1))))))
0(5(4(1(3(2(x1)))))) -> 0(5(4(3(1(2(x1))))))
Proof:
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {6}
transitions:
01(11) -> 12*
51(45) -> 46*
51(64) -> 65*
41(80) -> 81*
41(42) -> 43*
41(7) -> 8*
41(29) -> 30*
41(31) -> 32*
41(21) -> 22*
41(23) -> 24*
31(75) -> 76*
31(55) -> 56*
31(47) -> 48*
31(79) -> 80*
31(61) -> 62*
31(41) -> 42*
31(53) -> 54*
31(8) -> 9*
11(65) -> 66*
11(9) -> 10*
11(78) -> 79*
11(43) -> 44*
21(10) -> 11*
21(97) -> 98*
21(77) -> 78*
21(99) -> 100*
21(89) -> 90*
21(74) -> 75*
21(44) -> 45*
21(91) -> 92*
21(63) -> 64*
00(5) -> 6*
00(2) -> 6*
00(4) -> 6*
00(1) -> 6*
00(3) -> 6*
10(5) -> 1*
10(2) -> 1*
10(4) -> 1*
10(1) -> 1*
10(3) -> 1*
20(5) -> 2*
20(2) -> 2*
20(4) -> 2*
20(1) -> 2*
20(3) -> 2*
30(5) -> 3*
30(2) -> 3*
30(4) -> 3*
30(1) -> 3*
30(3) -> 3*
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 -> 97,55,29
2 -> 89,47,21
3 -> 99,61,31
4 -> 91,53,23
5 -> 77,41,7
8 -> 74*
12 -> 6*
22 -> 8*
24 -> 8*
30 -> 8*
32 -> 8*
43 -> 63*
46 -> 11*
48 -> 42*
54 -> 42*
56 -> 42*
62 -> 42*
66 -> 11*
76 -> 64*
81 -> 45*
90 -> 78*
92 -> 78*
98 -> 78*
100 -> 78*
problem:
QedTool IRC1
stdout:
YES(?,O(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:
{ 0(1(2(3(4(x1))))) -> 0(2(1(3(4(x1)))))
, 0(5(1(2(4(3(x1)))))) -> 0(5(2(1(4(3(x1))))))
, 0(5(2(4(1(3(x1)))))) -> 0(1(5(2(4(3(x1))))))
, 0(5(3(1(2(4(x1)))))) -> 0(1(5(3(2(4(x1))))))
, 0(5(4(1(3(2(x1)))))) -> 0(5(4(3(1(2(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:
{ 0(1(2(3(4(x1))))) -> 0(2(1(3(4(x1)))))
, 0(5(1(2(4(3(x1)))))) -> 0(5(2(1(4(3(x1))))))
, 0(5(2(4(1(3(x1)))))) -> 0(1(5(2(4(3(x1))))))
, 0(5(3(1(2(4(x1)))))) -> 0(1(5(3(2(4(x1))))))
, 0(5(4(1(3(2(x1)))))) -> 0(5(4(3(1(2(x1))))))}
Proof Output:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ 0_0(2) -> 1
, 0_1(3) -> 1
, 1_0(2) -> 2
, 1_1(5) -> 4
, 1_1(9) -> 8
, 1_1(11) -> 3
, 1_1(16) -> 15
, 2_0(2) -> 2
, 2_1(2) -> 16
, 2_1(4) -> 3
, 2_1(6) -> 13
, 2_1(8) -> 7
, 2_1(9) -> 12
, 3_0(2) -> 2
, 3_1(2) -> 10
, 3_1(6) -> 5
, 3_1(13) -> 12
, 3_1(15) -> 14
, 4_0(2) -> 2
, 4_1(2) -> 6
, 4_1(10) -> 9
, 4_1(14) -> 7
, 5_0(2) -> 2
, 5_1(7) -> 3
, 5_1(12) -> 11}Tool RC1
stdout:
YES(?,O(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:
{ 0(1(2(3(4(x1))))) -> 0(2(1(3(4(x1)))))
, 0(5(1(2(4(3(x1)))))) -> 0(5(2(1(4(3(x1))))))
, 0(5(2(4(1(3(x1)))))) -> 0(1(5(2(4(3(x1))))))
, 0(5(3(1(2(4(x1)))))) -> 0(1(5(3(2(4(x1))))))
, 0(5(4(1(3(2(x1)))))) -> 0(5(4(3(1(2(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:
{ 0(1(2(3(4(x1))))) -> 0(2(1(3(4(x1)))))
, 0(5(1(2(4(3(x1)))))) -> 0(5(2(1(4(3(x1))))))
, 0(5(2(4(1(3(x1)))))) -> 0(1(5(2(4(3(x1))))))
, 0(5(3(1(2(4(x1)))))) -> 0(1(5(3(2(4(x1))))))
, 0(5(4(1(3(2(x1)))))) -> 0(5(4(3(1(2(x1))))))}
Proof Output:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ 0_0(2) -> 1
, 0_1(3) -> 1
, 1_0(2) -> 2
, 1_1(5) -> 4
, 1_1(9) -> 8
, 1_1(11) -> 3
, 1_1(16) -> 15
, 2_0(2) -> 2
, 2_1(2) -> 16
, 2_1(4) -> 3
, 2_1(6) -> 13
, 2_1(8) -> 7
, 2_1(9) -> 12
, 3_0(2) -> 2
, 3_1(2) -> 10
, 3_1(6) -> 5
, 3_1(13) -> 12
, 3_1(15) -> 14
, 4_0(2) -> 2
, 4_1(2) -> 6
, 4_1(10) -> 9
, 4_1(14) -> 7
, 5_0(2) -> 2
, 5_1(7) -> 3
, 5_1(12) -> 11}