Tool CaT
stdout:
YES(?,O(n^1))
Problem:
f(a()) -> f(c(a()))
f(c(X)) -> X
f(c(a())) -> f(d(b()))
f(a()) -> f(d(a()))
f(d(X)) -> X
f(c(b())) -> f(d(a()))
e(g(X)) -> e(X)
Proof:
Bounds Processor:
bound: 2
enrichment: match
automaton:
final states: {7,6}
transitions:
e1(30) -> 31*
e1(22) -> 23*
e1(36) -> 37*
e1(38) -> 39*
e1(28) -> 29*
f1(9) -> 10*
d1(20) -> 21*
d1(14) -> 15*
a1() -> 8*
b1() -> 14*
c1(8) -> 9*
f2(46) -> 47*
d2(45) -> 46*
f0(5) -> 6*
f0(2) -> 6*
f0(4) -> 6*
f0(1) -> 6*
f0(3) -> 6*
b2() -> 45*
a0() -> 1*
c0(5) -> 2*
c0(2) -> 2*
c0(4) -> 2*
c0(1) -> 2*
c0(3) -> 2*
d0(5) -> 3*
d0(2) -> 3*
d0(4) -> 3*
d0(1) -> 3*
d0(3) -> 3*
b0() -> 4*
e0(5) -> 7*
e0(2) -> 7*
e0(4) -> 7*
e0(1) -> 7*
e0(3) -> 7*
g0(5) -> 5*
g0(2) -> 5*
g0(4) -> 5*
g0(1) -> 5*
g0(3) -> 5*
1 -> 36,6
2 -> 28,6
3 -> 38,6
4 -> 30,6
5 -> 22,6
8 -> 10,6,20
10 -> 6*
14 -> 10,6
15 -> 9*
20 -> 10,6
21 -> 9*
23 -> 7*
29 -> 23,7
31 -> 23,7
37 -> 23,7
39 -> 23,7
45 -> 47,10
47 -> 10,6
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:
{ f(a()) -> f(c(a()))
, f(c(X)) -> X
, f(c(a())) -> f(d(b()))
, f(a()) -> f(d(a()))
, f(d(X)) -> X
, f(c(b())) -> f(d(a()))
, e(g(X)) -> e(X)}
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:
{ f(a()) -> f(c(a()))
, f(c(X)) -> X
, f(c(a())) -> f(d(b()))
, f(a()) -> f(d(a()))
, f(d(X)) -> X
, f(c(b())) -> f(d(a()))
, e(g(X)) -> e(X)}
Proof Output:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ f_0(2) -> 1
, f_1(3) -> 1
, f_2(6) -> 1
, a_0() -> 1
, a_0() -> 2
, a_1() -> 1
, a_1() -> 4
, c_0(2) -> 1
, c_0(2) -> 2
, c_1(4) -> 3
, d_0(2) -> 1
, d_0(2) -> 2
, d_1(4) -> 3
, d_1(5) -> 3
, d_2(7) -> 6
, b_0() -> 1
, b_0() -> 2
, b_1() -> 1
, b_1() -> 5
, b_2() -> 1
, b_2() -> 7
, e_0(2) -> 1
, e_1(2) -> 1
, g_0(2) -> 1
, g_0(2) -> 2}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:
{ f(a()) -> f(c(a()))
, f(c(X)) -> X
, f(c(a())) -> f(d(b()))
, f(a()) -> f(d(a()))
, f(d(X)) -> X
, f(c(b())) -> f(d(a()))
, e(g(X)) -> e(X)}
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:
{ f(a()) -> f(c(a()))
, f(c(X)) -> X
, f(c(a())) -> f(d(b()))
, f(a()) -> f(d(a()))
, f(d(X)) -> X
, f(c(b())) -> f(d(a()))
, e(g(X)) -> e(X)}
Proof Output:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ f_0(2) -> 1
, f_1(3) -> 1
, f_2(6) -> 1
, a_0() -> 1
, a_0() -> 2
, a_1() -> 1
, a_1() -> 4
, c_0(2) -> 1
, c_0(2) -> 2
, c_1(4) -> 3
, d_0(2) -> 1
, d_0(2) -> 2
, d_1(4) -> 3
, d_1(5) -> 3
, d_2(7) -> 6
, b_0() -> 1
, b_0() -> 2
, b_1() -> 1
, b_1() -> 5
, b_2() -> 1
, b_2() -> 7
, e_0(2) -> 1
, e_1(2) -> 1
, g_0(2) -> 1
, g_0(2) -> 2}