Tool CaT
stdout:
YES(?,O(n^1))
Problem:
r(r(x1)) -> s(r(x1))
r(s(x1)) -> s(r(x1))
r(n(x1)) -> s(r(x1))
r(b(x1)) -> u(s(b(x1)))
r(u(x1)) -> u(r(x1))
s(u(x1)) -> u(s(x1))
n(u(x1)) -> u(n(x1))
t(r(u(x1))) -> t(c(r(x1)))
t(s(u(x1))) -> t(c(r(x1)))
t(n(u(x1))) -> t(c(r(x1)))
c(u(x1)) -> u(c(x1))
c(s(x1)) -> s(c(x1))
c(r(x1)) -> r(c(x1))
c(n(x1)) -> n(c(x1))
c(n(x1)) -> n(x1)
Proof:
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {7,6,5,4,3}
transitions:
u1(52) -> 53*
u1(42) -> 43*
u1(32) -> 33*
u1(14) -> 15*
c1(54) -> 55*
c1(51) -> 52*
n1(44) -> 45*
n1(41) -> 42*
s1(34) -> 35*
s1(31) -> 32*
s1(13) -> 14*
r1(22) -> 23*
r1(24) -> 25*
b1(12) -> 13*
b1(16) -> 17*
r0(2) -> 3*
r0(1) -> 3*
s0(2) -> 4*
s0(1) -> 4*
n0(2) -> 5*
n0(1) -> 5*
b0(2) -> 1*
b0(1) -> 1*
u0(2) -> 2*
u0(1) -> 2*
t0(2) -> 6*
t0(1) -> 6*
c0(2) -> 7*
c0(1) -> 7*
1 -> 54,44,34,24,16
2 -> 51,41,31,22,12
15 -> 23,25,14,3
17 -> 13*
23 -> 14*
25 -> 14*
33 -> 32,4
35 -> 32*
43 -> 42,5
45 -> 42*
53 -> 52,7
55 -> 52*
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:
{ r(r(x1)) -> s(r(x1))
, r(s(x1)) -> s(r(x1))
, r(n(x1)) -> s(r(x1))
, r(b(x1)) -> u(s(b(x1)))
, r(u(x1)) -> u(r(x1))
, s(u(x1)) -> u(s(x1))
, n(u(x1)) -> u(n(x1))
, t(r(u(x1))) -> t(c(r(x1)))
, t(s(u(x1))) -> t(c(r(x1)))
, t(n(u(x1))) -> t(c(r(x1)))
, c(u(x1)) -> u(c(x1))
, c(s(x1)) -> s(c(x1))
, c(r(x1)) -> r(c(x1))
, c(n(x1)) -> n(c(x1))
, c(n(x1)) -> n(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:
{ r(r(x1)) -> s(r(x1))
, r(s(x1)) -> s(r(x1))
, r(n(x1)) -> s(r(x1))
, r(b(x1)) -> u(s(b(x1)))
, r(u(x1)) -> u(r(x1))
, s(u(x1)) -> u(s(x1))
, n(u(x1)) -> u(n(x1))
, t(r(u(x1))) -> t(c(r(x1)))
, t(s(u(x1))) -> t(c(r(x1)))
, t(n(u(x1))) -> t(c(r(x1)))
, c(u(x1)) -> u(c(x1))
, c(s(x1)) -> s(c(x1))
, c(r(x1)) -> r(c(x1))
, c(n(x1)) -> n(c(x1))
, c(n(x1)) -> n(x1)}
Proof Output:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ r_0(2) -> 1
, r_1(2) -> 3
, s_0(2) -> 1
, s_1(2) -> 3
, s_1(4) -> 3
, n_0(2) -> 1
, n_1(2) -> 3
, b_0(2) -> 2
, b_1(2) -> 4
, u_0(2) -> 2
, u_1(3) -> 1
, u_1(3) -> 3
, t_0(2) -> 1
, c_0(2) -> 1
, c_1(2) -> 3}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:
{ r(r(x1)) -> s(r(x1))
, r(s(x1)) -> s(r(x1))
, r(n(x1)) -> s(r(x1))
, r(b(x1)) -> u(s(b(x1)))
, r(u(x1)) -> u(r(x1))
, s(u(x1)) -> u(s(x1))
, n(u(x1)) -> u(n(x1))
, t(r(u(x1))) -> t(c(r(x1)))
, t(s(u(x1))) -> t(c(r(x1)))
, t(n(u(x1))) -> t(c(r(x1)))
, c(u(x1)) -> u(c(x1))
, c(s(x1)) -> s(c(x1))
, c(r(x1)) -> r(c(x1))
, c(n(x1)) -> n(c(x1))
, c(n(x1)) -> n(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:
{ r(r(x1)) -> s(r(x1))
, r(s(x1)) -> s(r(x1))
, r(n(x1)) -> s(r(x1))
, r(b(x1)) -> u(s(b(x1)))
, r(u(x1)) -> u(r(x1))
, s(u(x1)) -> u(s(x1))
, n(u(x1)) -> u(n(x1))
, t(r(u(x1))) -> t(c(r(x1)))
, t(s(u(x1))) -> t(c(r(x1)))
, t(n(u(x1))) -> t(c(r(x1)))
, c(u(x1)) -> u(c(x1))
, c(s(x1)) -> s(c(x1))
, c(r(x1)) -> r(c(x1))
, c(n(x1)) -> n(c(x1))
, c(n(x1)) -> n(x1)}
Proof Output:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ r_0(2) -> 1
, r_1(2) -> 3
, s_0(2) -> 1
, s_1(2) -> 3
, s_1(4) -> 3
, n_0(2) -> 1
, n_1(2) -> 3
, b_0(2) -> 2
, b_1(2) -> 4
, u_0(2) -> 2
, u_1(3) -> 1
, u_1(3) -> 3
, t_0(2) -> 1
, c_0(2) -> 1
, c_1(2) -> 3}