Tool CaT
stdout:
YES(?,O(n^1))
Problem:
b(b(x1)) -> a(a(a(x1)))
b(a(b(x1))) -> a(x1)
b(a(a(x1))) -> b(a(b(x1)))
Proof:
Complexity Transformation Processor:
strict:
b(b(x1)) -> a(a(a(x1)))
b(a(b(x1))) -> a(x1)
b(a(a(x1))) -> b(a(b(x1)))
weak:
Arctic Interpretation Processor:
dimension: 2
interpretation:
[0 2]
[a](x0) = [0 0]x0,
[2 2]
[b](x0) = [0 0]x0
orientation:
[4 4] [2 4]
b(b(x1)) = [2 2]x1 >= [2 2]x1 = a(a(a(x1)))
[4 4] [0 2]
b(a(b(x1))) = [2 2]x1 >= [0 0]x1 = a(x1)
[4 4] [4 4]
b(a(a(x1))) = [2 2]x1 >= [2 2]x1 = b(a(b(x1)))
problem:
strict:
b(b(x1)) -> a(a(a(x1)))
b(a(a(x1))) -> b(a(b(x1)))
weak:
b(a(b(x1))) -> a(x1)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[a](x0) = x0 + 37,
[b](x0) = x0 + 28
orientation:
b(b(x1)) = x1 + 56 >= x1 + 111 = a(a(a(x1)))
b(a(a(x1))) = x1 + 102 >= x1 + 93 = b(a(b(x1)))
b(a(b(x1))) = x1 + 93 >= x1 + 37 = a(x1)
problem:
strict:
b(b(x1)) -> a(a(a(x1)))
weak:
b(a(a(x1))) -> b(a(b(x1)))
b(a(b(x1))) -> a(x1)
Arctic Interpretation Processor:
dimension: 3
interpretation:
[0 -& 0 ]
[a](x0) = [-& -& 0 ]x0
[-& 0 -&] ,
[0 0 1 ]
[b](x0) = [-& -& 0 ]x0
[0 0 1 ]
orientation:
[1 1 2] [0 0 0 ]
b(b(x1)) = [0 0 1]x1 >= [-& -& 0 ]x1 = a(a(a(x1)))
[1 1 2] [-& 0 -&]
[0 0 1 ] [0 0 1 ]
b(a(a(x1))) = [-& -& 0 ]x1 >= [-& -& 0 ]x1 = b(a(b(x1)))
[0 0 1 ] [0 0 1 ]
[0 0 1 ] [0 -& 0 ]
b(a(b(x1))) = [-& -& 0 ]x1 >= [-& -& 0 ]x1 = a(x1)
[0 0 1 ] [-& 0 -&]
problem:
strict:
weak:
b(b(x1)) -> a(a(a(x1)))
b(a(a(x1))) -> b(a(b(x1)))
b(a(b(x1))) -> a(x1)
Qed
Tool IRC1
stdout:
MAYBE
Tool IRC2
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: innermost runtime-complexity with respect to
Rules:
{ b(b(x1)) -> a(a(a(x1)))
, b(a(b(x1))) -> a(x1)
, b(a(a(x1))) -> b(a(b(x1)))}
Proof Output:
Computation stopped due to timeout after 60.0 secondsTool RC1
stdout:
MAYBE
Tool RC2
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: runtime-complexity with respect to
Rules:
{ b(b(x1)) -> a(a(a(x1)))
, b(a(b(x1))) -> a(x1)
, b(a(a(x1))) -> b(a(b(x1)))}
Proof Output:
Computation stopped due to timeout after 60.0 seconds