Tool CaT
stdout:
YES(?,O(n^1))
Problem:
a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
p(p(s(x1))) -> p(x1)
p(s(x1)) -> x1
Proof:
Bounds Processor:
bound: 2
enrichment: match
automaton:
final states: {5,4,3,2}
transitions:
p1(60) -> 61*
p1(35) -> 36*
p1(30) -> 31*
p1(20) -> 21*
p1(62) -> 63*
p1(34) -> 35*
p1(19) -> 20*
p1(28) -> 29*
p1(23) -> 24*
s1(25) -> 26*
s1(37) -> 38*
s1(32) -> 33*
s1(22) -> 23*
s1(17) -> 18*
s1(59) -> 60*
s1(29) -> 30*
s1(24) -> 25*
s1(61) -> 62*
s1(36) -> 37*
s1(26) -> 27*
s1(38) -> 39*
s1(33) -> 34*
s1(18) -> 19*
a1(58) -> 59*
c1(31) -> 32*
b1(21) -> 22*
p2(66) -> 67*
p2(68) -> 69*
a0(1) -> 2*
s0(1) -> 1*
p0(1) -> 5*
b0(1) -> 3*
c0(1) -> 4*
1 -> 5,17
17 -> 67,21,29
18 -> 20,66,28
22 -> 24*
27 -> 59,61,4,2
29 -> 31*
31 -> 58*
32 -> 69*
33 -> 35,68
39 -> 22,24,3
59 -> 61*
61 -> 63*
63 -> 32,4
67 -> 21*
69 -> 36*
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:
{ a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> 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:
{ a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1}
Proof Output:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ a_0(2) -> 1
, a_1(15) -> 1
, a_1(15) -> 5
, a_1(15) -> 14
, a_1(15) -> 19
, a_1(15) -> 21
, s_0(2) -> 1
, s_0(2) -> 2
, s_0(2) -> 8
, s_0(2) -> 15
, s_0(2) -> 17
, s_1(2) -> 9
, s_1(2) -> 11
, s_1(3) -> 1
, s_1(3) -> 5
, s_1(3) -> 7
, s_1(3) -> 14
, s_1(3) -> 19
, s_1(3) -> 21
, s_1(4) -> 3
, s_1(5) -> 4
, s_1(7) -> 6
, s_1(11) -> 10
, s_1(13) -> 12
, s_1(14) -> 6
, s_1(14) -> 13
, s_1(17) -> 16
, s_1(19) -> 18
, s_1(21) -> 20
, p_0(2) -> 1
, p_1(6) -> 5
, p_1(9) -> 8
, p_1(10) -> 9
, p_1(11) -> 15
, p_1(11) -> 17
, p_1(12) -> 6
, p_1(16) -> 15
, p_1(18) -> 1
, p_1(18) -> 5
, p_1(18) -> 14
, p_1(20) -> 1
, p_1(20) -> 5
, p_1(20) -> 14
, p_1(20) -> 19
, p_2(11) -> 8
, p_2(13) -> 5
, b_0(2) -> 1
, b_1(8) -> 5
, b_1(8) -> 7
, c_0(2) -> 1
, c_1(15) -> 5
, c_1(15) -> 14}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:
{ a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> 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:
{ a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1))))))))))
, b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
, c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1)))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1}
Proof Output:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ a_0(2) -> 1
, a_1(15) -> 1
, a_1(15) -> 5
, a_1(15) -> 14
, a_1(15) -> 19
, a_1(15) -> 21
, s_0(2) -> 1
, s_0(2) -> 2
, s_0(2) -> 8
, s_0(2) -> 15
, s_0(2) -> 17
, s_1(2) -> 9
, s_1(2) -> 11
, s_1(3) -> 1
, s_1(3) -> 5
, s_1(3) -> 7
, s_1(3) -> 14
, s_1(3) -> 19
, s_1(3) -> 21
, s_1(4) -> 3
, s_1(5) -> 4
, s_1(7) -> 6
, s_1(11) -> 10
, s_1(13) -> 12
, s_1(14) -> 6
, s_1(14) -> 13
, s_1(17) -> 16
, s_1(19) -> 18
, s_1(21) -> 20
, p_0(2) -> 1
, p_1(6) -> 5
, p_1(9) -> 8
, p_1(10) -> 9
, p_1(11) -> 15
, p_1(11) -> 17
, p_1(12) -> 6
, p_1(16) -> 15
, p_1(18) -> 1
, p_1(18) -> 5
, p_1(18) -> 14
, p_1(20) -> 1
, p_1(20) -> 5
, p_1(20) -> 14
, p_1(20) -> 19
, p_2(11) -> 8
, p_2(13) -> 5
, b_0(2) -> 1
, b_1(8) -> 5
, b_1(8) -> 7
, c_0(2) -> 1
, c_1(15) -> 5
, c_1(15) -> 14}