Tool CaT
stdout:
YES(?,O(n^1))
Problem:
f(a(),a()) -> f(a(),b())
f(a(),b()) -> f(s(a()),c())
f(s(X),c()) -> f(X,c())
f(c(),c()) -> f(a(),a())
Proof:
Bounds Processor:
bound: 4
enrichment: match
automaton:
final states: {5}
transitions:
c3() -> 18*
s3(19) -> 20*
a3() -> 19*
f4(19,24) -> 5*
c4() -> 24*
f0(3,1) -> 5*
f0(3,3) -> 5*
f0(4,2) -> 5*
f0(4,4) -> 5*
f0(1,2) -> 5*
f0(1,4) -> 5*
f0(2,1) -> 5*
f0(2,3) -> 5*
f0(3,2) -> 5*
f0(3,4) -> 5*
f0(4,1) -> 5*
f0(4,3) -> 5*
f0(1,1) -> 5*
f0(1,3) -> 5*
f0(2,2) -> 5*
f0(2,4) -> 5*
a0() -> 1*
b0() -> 2*
s0(2) -> 3*
s0(4) -> 3*
s0(1) -> 3*
s0(3) -> 3*
c0() -> 4*
f1(4,10) -> 5*
f1(11,10) -> 5*
f1(1,10) -> 5*
f1(7,7) -> 5*
f1(3,10) -> 5*
f1(7,6) -> 5*
f1(2,10) -> 5*
a1() -> 7*
c1() -> 10*
s1(7) -> 11*
b1() -> 6*
f2(17,16) -> 5*
f2(7,16) -> 5*
f2(15,14) -> 5*
c2() -> 16*
s2(15) -> 17*
a2() -> 15*
b2() -> 14*
f3(20,18) -> 5*
f3(15,18) -> 5*
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(), a()) -> f(a(), b())
, f(a(), b()) -> f(s(a()), c())
, f(s(X), c()) -> f(X, c())
, f(c(), c()) -> f(a(), a())}
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(), a()) -> f(a(), b())
, f(a(), b()) -> f(s(a()), c())
, f(s(X), c()) -> f(X, c())
, f(c(), c()) -> f(a(), a())}
Proof Output:
The problem is match-bounded by 4.
The enriched problem is compatible with the following automaton:
{ f_0(2, 2) -> 1
, f_1(2, 4) -> 1
, f_1(3, 3) -> 1
, f_1(3, 4) -> 1
, f_2(3, 6) -> 1
, f_2(5, 6) -> 1
, f_2(7, 9) -> 1
, f_3(7, 8) -> 1
, f_4(10, 11) -> 1
, a_0() -> 2
, a_1() -> 3
, a_2() -> 7
, a_3() -> 10
, b_0() -> 2
, b_1() -> 4
, b_2() -> 9
, s_0(2) -> 2
, s_1(3) -> 3
, s_2(7) -> 5
, s_3(10) -> 7
, c_0() -> 2
, c_1() -> 4
, c_2() -> 6
, c_3() -> 8
, c_4() -> 11}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(), a()) -> f(a(), b())
, f(a(), b()) -> f(s(a()), c())
, f(s(X), c()) -> f(X, c())
, f(c(), c()) -> f(a(), a())}
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(), a()) -> f(a(), b())
, f(a(), b()) -> f(s(a()), c())
, f(s(X), c()) -> f(X, c())
, f(c(), c()) -> f(a(), a())}
Proof Output:
The problem is match-bounded by 4.
The enriched problem is compatible with the following automaton:
{ f_0(2, 2) -> 1
, f_1(2, 4) -> 1
, f_1(3, 3) -> 1
, f_1(3, 4) -> 1
, f_2(3, 6) -> 1
, f_2(5, 6) -> 1
, f_2(7, 9) -> 1
, f_3(7, 8) -> 1
, f_4(10, 11) -> 1
, a_0() -> 2
, a_1() -> 3
, a_2() -> 7
, a_3() -> 10
, b_0() -> 2
, b_1() -> 4
, b_2() -> 9
, s_0(2) -> 2
, s_1(3) -> 3
, s_2(7) -> 5
, s_3(10) -> 7
, c_0() -> 2
, c_1() -> 4
, c_2() -> 6
, c_3() -> 8
, c_4() -> 11}