Tool CaT
stdout:
MAYBE
Problem:
sq(0(x1)) -> p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(x1)))))))))))))))))
sq(s(x1)) ->
s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))))))))
twice(0(x1)) ->
p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(x1)))))))))))))))))))))))))))
twice(s(x1)) -> p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1)))))))))))))))
p(p(s(x1))) -> p(x1)
p(s(x1)) -> x1
p(0(x1)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x1))))))))))))
0(x1) -> x1
Proof:
Complexity Transformation Processor:
strict:
sq(0(x1)) -> p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(x1)))))))))))))))))
sq(s(x1)) ->
s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))))))))
twice(0(x1)) ->
p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(x1)))))))))))))))))))))))))))
twice(s(x1)) -> p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1)))))))))))))))
p(p(s(x1))) -> p(x1)
p(s(x1)) -> x1
p(0(x1)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x1))))))))))))
0(x1) -> x1
weak:
Arctic Interpretation Processor:
dimension: 1
interpretation:
[twice](x0) = x0,
[p](x0) = x0,
[s](x0) = x0,
[sq](x0) = x0,
[0](x0) = 4x0
orientation:
sq(0(x1)) = 4x1 >= 4x1 = p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(x1)))))))))))))))))
sq(s(x1)) = x1 >= x1 = s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))))))))
twice(0(x1)) = 4x1 >= 4x1 = p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(x1)))))))))))))))))))))))))))
twice(s(x1)) = x1 >= x1 = p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1)))))))))))))))
p(p(s(x1))) = x1 >= x1 = p(x1)
p(s(x1)) = x1 >= x1 = x1
p(0(x1)) = 4x1 >= 4x1 = 0(s(s(s(s(s(s(s(s(s(s(s(x1))))))))))))
0(x1) = 4x1 >= x1 = x1
problem:
strict:
sq(0(x1)) -> p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(x1)))))))))))))))))
sq(s(x1)) ->
s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))))))))
twice(0(x1)) ->
p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(x1)))))))))))))))))))))))))))
twice(s(x1)) -> p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1)))))))))))))))
p(p(s(x1))) -> p(x1)
p(s(x1)) -> x1
p(0(x1)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x1))))))))))))
weak:
0(x1) -> x1
Arctic Interpretation Processor:
dimension: 1
interpretation:
[twice](x0) = x0,
[p](x0) = x0,
[s](x0) = x0,
[sq](x0) = 4x0,
[0](x0) = x0
orientation:
sq(0(x1)) = 4x1 >= x1 = p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(x1)))))))))))))))))
sq(s(x1)) = 4x1 >= 4x1 = s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))))))))
twice(0(x1)) = x1 >= x1 = p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(x1)))))))))))))))))))))))))))
twice(s(x1)) = x1 >= x1 = p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1)))))))))))))))
p(p(s(x1))) = x1 >= x1 = p(x1)
p(s(x1)) = x1 >= x1 = x1
p(0(x1)) = x1 >= x1 = 0(s(s(s(s(s(s(s(s(s(s(s(x1))))))))))))
0(x1) = x1 >= x1 = x1
problem:
strict:
sq(s(x1)) ->
s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))))))))
twice(0(x1)) ->
p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(x1)))))))))))))))))))))))))))
twice(s(x1)) -> p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1)))))))))))))))
p(p(s(x1))) -> p(x1)
p(s(x1)) -> x1
p(0(x1)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x1))))))))))))
weak:
sq(0(x1)) -> p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(x1)))))))))))))))))
0(x1) -> x1
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[twice](x0) = x0 + 28,
[p](x0) = x0 + 8,
[s](x0) = x0,
[sq](x0) = x0 + 244,
[0](x0) = x0 + 246
orientation:
sq(s(x1)) = x1 + 244 >= x1 + 392 = s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))))))))
twice(0(x1)) = x1 + 274 >= x1 + 350 = p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(x1)))))))))))))))))))))))))))
twice(s(x1)) = x1 + 28 >= x1 + 76 = p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1)))))))))))))))
p(p(s(x1))) = x1 + 16 >= x1 + 8 = p(x1)
p(s(x1)) = x1 + 8 >= x1 = x1
p(0(x1)) = x1 + 254 >= x1 + 246 = 0(s(s(s(s(s(s(s(s(s(s(s(x1))))))))))))
sq(0(x1)) = x1 + 490 >= x1 + 310 = p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(x1)))))))))))))))))
0(x1) = x1 + 246 >= x1 = x1
problem:
strict:
sq(s(x1)) ->
s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))))))))
twice(0(x1)) ->
p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(x1)))))))))))))))))))))))))))
twice(s(x1)) -> p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1)))))))))))))))
weak:
p(p(s(x1))) -> p(x1)
p(s(x1)) -> x1
p(0(x1)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x1))))))))))))
sq(0(x1)) -> p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(x1)))))))))))))))))
0(x1) -> x1
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[twice](x0) = x0 + 18,
[p](x0) = x0,
[s](x0) = x0,
[sq](x0) = x0 + 18,
[0](x0) = x0
orientation:
sq(s(x1)) = x1 + 18 >= x1 + 36 = s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))))))))
twice(0(x1)) = x1 + 18 >= x1 = p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(x1)))))))))))))))))))))))))))
twice(s(x1)) = x1 + 18 >= x1 + 18 = p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1)))))))))))))))
p(p(s(x1))) = x1 >= x1 = p(x1)
p(s(x1)) = x1 >= x1 = x1
p(0(x1)) = x1 >= x1 = 0(s(s(s(s(s(s(s(s(s(s(s(x1))))))))))))
sq(0(x1)) = x1 + 18 >= x1 = p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(x1)))))))))))))))))
0(x1) = x1 >= x1 = x1
problem:
strict:
sq(s(x1)) ->
s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))))))))
twice(s(x1)) -> p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1)))))))))))))))
weak:
twice(0(x1)) ->
p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(x1)))))))))))))))))))))))))))
p(p(s(x1))) -> p(x1)
p(s(x1)) -> x1
p(0(x1)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x1))))))))))))
sq(0(x1)) -> p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(x1)))))))))))))))))
0(x1) -> x1
Open
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:
{ sq(0(x1)) ->
p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(x1)))))))))))))))))
, sq(s(x1)) ->
s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))))))))
, twice(0(x1)) ->
p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(x1)))))))))))))))))))))))))))
, twice(s(x1)) ->
p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1)))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x1))))))))))))
, 0(x1) -> 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:
{ sq(0(x1)) ->
p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(x1)))))))))))))))))
, sq(s(x1)) ->
s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1)))))))))))))))))))))))))))))))))
, twice(0(x1)) ->
p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(x1)))))))))))))))))))))))))))
, twice(s(x1)) ->
p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1)))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x1))))))))))))
, 0(x1) -> x1}
Proof Output:
Computation stopped due to timeout after 60.0 seconds