Tool CaT
stdout:
YES(?,O(n^4))
Problem:
a(x1) -> b(c(x1))
a(b(x1)) -> b(a(x1))
d(c(x1)) -> d(a(x1))
a(c(x1)) -> c(a(x1))
Proof:
Complexity Transformation Processor:
strict:
a(x1) -> b(c(x1))
a(b(x1)) -> b(a(x1))
d(c(x1)) -> d(a(x1))
a(c(x1)) -> c(a(x1))
weak:
Arctic Interpretation Processor:
dimension: 2
interpretation:
[0 0 ]
[d](x0) = [-& -&]x0,
[0 -&]
[b](x0) = [-& -&]x0,
[0 -&]
[c](x0) = [1 1 ]x0,
[0 -&]
[a](x0) = [0 0 ]x0
orientation:
[0 -&] [0 -&]
a(x1) = [0 0 ]x1 >= [-& -&]x1 = b(c(x1))
[0 -&] [0 -&]
a(b(x1)) = [0 -&]x1 >= [-& -&]x1 = b(a(x1))
[1 1 ] [0 0 ]
d(c(x1)) = [-& -&]x1 >= [-& -&]x1 = d(a(x1))
[0 -&] [0 -&]
a(c(x1)) = [1 1 ]x1 >= [1 1 ]x1 = c(a(x1))
problem:
strict:
a(x1) -> b(c(x1))
a(b(x1)) -> b(a(x1))
a(c(x1)) -> c(a(x1))
weak:
d(c(x1)) -> d(a(x1))
Arctic Interpretation Processor:
dimension: 2
interpretation:
[0 1 ]
[d](x0) = [-& 1 ]x0,
[0 -&]
[b](x0) = [-& -&]x0,
[0 -&]
[c](x0) = [0 2 ]x0,
[1 -&]
[a](x0) = [0 2 ]x0
orientation:
[1 -&] [0 -&]
a(x1) = [0 2 ]x1 >= [-& -&]x1 = b(c(x1))
[1 -&] [1 -&]
a(b(x1)) = [0 -&]x1 >= [-& -&]x1 = b(a(x1))
[1 -&] [1 -&]
a(c(x1)) = [2 4 ]x1 >= [2 4 ]x1 = c(a(x1))
[1 3] [1 3]
d(c(x1)) = [1 3]x1 >= [1 3]x1 = d(a(x1))
problem:
strict:
a(b(x1)) -> b(a(x1))
a(c(x1)) -> c(a(x1))
weak:
a(x1) -> b(c(x1))
d(c(x1)) -> d(a(x1))
Matrix Interpretation Processor:
dimension: 4
max_matrix:
[1 1 1 0]
[0 1 1 1]
[0 0 1 0]
[0 0 0 1]
interpretation:
[1 1 0 0]
[0 0 0 0]
[d](x0) = [0 0 0 0]x0
[0 0 0 0] ,
[1 0 0 0] [0]
[0 0 0 0] [0]
[b](x0) = [0 0 1 0]x0 + [1]
[0 0 0 0] [0],
[1 0 0 0] [0]
[0 1 1 1] [0]
[c](x0) = [0 0 1 0]x0 + [0]
[0 0 0 1] [1],
[1 0 1 0] [0]
[0 1 0 1] [0]
[a](x0) = [0 0 1 0]x0 + [1]
[0 0 0 1] [0]
orientation:
[1 0 1 0] [1] [1 0 1 0] [0]
[0 0 0 0] [0] [0 0 0 0] [0]
a(b(x1)) = [0 0 1 0]x1 + [2] >= [0 0 1 0]x1 + [2] = b(a(x1))
[0 0 0 0] [0] [0 0 0 0] [0]
[1 0 1 0] [0] [1 0 1 0] [0]
[0 1 1 2] [1] [0 1 1 2] [1]
a(c(x1)) = [0 0 1 0]x1 + [1] >= [0 0 1 0]x1 + [1] = c(a(x1))
[0 0 0 1] [1] [0 0 0 1] [1]
[1 0 1 0] [0] [1 0 0 0] [0]
[0 1 0 1] [0] [0 0 0 0] [0]
a(x1) = [0 0 1 0]x1 + [1] >= [0 0 1 0]x1 + [1] = b(c(x1))
[0 0 0 1] [0] [0 0 0 0] [0]
[1 1 1 1] [1 1 1 1]
[0 0 0 0] [0 0 0 0]
d(c(x1)) = [0 0 0 0]x1 >= [0 0 0 0]x1 = d(a(x1))
[0 0 0 0] [0 0 0 0]
problem:
strict:
a(c(x1)) -> c(a(x1))
weak:
a(b(x1)) -> b(a(x1))
a(x1) -> b(c(x1))
d(c(x1)) -> d(a(x1))
Matrix Interpretation Processor:
dimension: 4
max_matrix:
[1 1 1 0]
[0 1 1 1]
[0 0 1 1]
[0 0 0 1]
interpretation:
[1 1 0 0] [0]
[0 0 0 0] [0]
[d](x0) = [0 0 0 1]x0 + [1]
[0 0 0 0] [1],
[1 0 0 0]
[0 0 0 0]
[b](x0) = [0 0 1 0]x0
[0 0 0 0] ,
[1 0 0 0] [0]
[0 1 1 1] [0]
[c](x0) = [0 0 1 0]x0 + [1]
[0 0 0 1] [1],
[1 0 1 0] [0]
[0 1 0 1] [0]
[a](x0) = [0 0 1 0]x0 + [1]
[0 0 0 1] [0]
orientation:
[1 0 1 0] [1] [1 0 1 0] [0]
[0 1 1 2] [1] [0 1 1 2] [1]
a(c(x1)) = [0 0 1 0]x1 + [2] >= [0 0 1 0]x1 + [2] = c(a(x1))
[0 0 0 1] [1] [0 0 0 1] [1]
[1 0 1 0] [0] [1 0 1 0] [0]
[0 0 0 0] [0] [0 0 0 0] [0]
a(b(x1)) = [0 0 1 0]x1 + [1] >= [0 0 1 0]x1 + [1] = b(a(x1))
[0 0 0 0] [0] [0 0 0 0] [0]
[1 0 1 0] [0] [1 0 0 0] [0]
[0 1 0 1] [0] [0 0 0 0] [0]
a(x1) = [0 0 1 0]x1 + [1] >= [0 0 1 0]x1 + [1] = b(c(x1))
[0 0 0 1] [0] [0 0 0 0] [0]
[1 1 1 1] [0] [1 1 1 1] [0]
[0 0 0 0] [0] [0 0 0 0] [0]
d(c(x1)) = [0 0 0 1]x1 + [2] >= [0 0 0 1]x1 + [1] = d(a(x1))
[0 0 0 0] [1] [0 0 0 0] [1]
problem:
strict:
weak:
a(c(x1)) -> c(a(x1))
a(b(x1)) -> b(a(x1))
a(x1) -> b(c(x1))
d(c(x1)) -> d(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:
{ a(x1) -> b(c(x1))
, a(b(x1)) -> b(a(x1))
, d(c(x1)) -> d(a(x1))
, a(c(x1)) -> c(a(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:
{ a(x1) -> b(c(x1))
, a(b(x1)) -> b(a(x1))
, d(c(x1)) -> d(a(x1))
, a(c(x1)) -> c(a(x1))}
Proof Output:
Computation stopped due to timeout after 60.0 seconds