Tool CaT
stdout:
MAYBE
Problem:
tower(0(x1)) -> s(0(p(s(p(s(x1))))))
tower(s(x1)) -> p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))))
twoto(0(x1)) -> s(0(x1))
twoto(s(x1)) ->
p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))))
twice(0(x1)) -> 0(x1)
twice(s(x1)) -> p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))))
p(p(s(x1))) -> p(x1)
p(s(x1)) -> x1
p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
Proof:
Complexity Transformation Processor:
strict:
tower(0(x1)) -> s(0(p(s(p(s(x1))))))
tower(s(x1)) -> p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))))
twoto(0(x1)) -> s(0(x1))
twoto(s(x1)) ->
p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))))
twice(0(x1)) -> 0(x1)
twice(s(x1)) -> p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))))
p(p(s(x1))) -> p(x1)
p(s(x1)) -> x1
p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
weak:
Arctic Interpretation Processor:
dimension: 1
interpretation:
[twice](x0) = x0,
[twoto](x0) = x0,
[p](x0) = x0,
[s](x0) = x0,
[tower](x0) = 4x0,
[0](x0) = x0
orientation:
tower(0(x1)) = 4x1 >= x1 = s(0(p(s(p(s(x1))))))
tower(s(x1)) = 4x1 >= 4x1 = p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))))
twoto(0(x1)) = x1 >= x1 = s(0(x1))
twoto(s(x1)) = x1 >= x1 = p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))))
twice(0(x1)) = x1 >= x1 = 0(x1)
twice(s(x1)) = x1 >= x1 = p(p(p(s(s(s(s(s(twice(p(p(p(s(s(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(x1)))))))))
problem:
strict:
tower(s(x1)) -> p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))))
twoto(0(x1)) -> s(0(x1))
twoto(s(x1)) ->
p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))))
twice(0(x1)) -> 0(x1)
twice(s(x1)) -> p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))))
p(p(s(x1))) -> p(x1)
p(s(x1)) -> x1
p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
weak:
tower(0(x1)) -> s(0(p(s(p(s(x1))))))
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[twice](x0) = x0 + 81,
[twoto](x0) = x0 + 13,
[p](x0) = x0 + 2,
[s](x0) = x0 + 2,
[tower](x0) = x0 + 57,
[0](x0) = x0 + 123
orientation:
tower(s(x1)) = x1 + 59 >= x1 + 94 = p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))))
twoto(0(x1)) = x1 + 136 >= x1 + 125 = s(0(x1))
twoto(s(x1)) = x1 + 15 >= x1 + 154 = p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))))
twice(0(x1)) = x1 + 204 >= x1 + 123 = 0(x1)
twice(s(x1)) = x1 + 83 >= x1 + 109 = p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))))
p(p(s(x1))) = x1 + 6 >= x1 + 2 = p(x1)
p(s(x1)) = x1 + 4 >= x1 = x1
p(0(x1)) = x1 + 125 >= x1 + 139 = 0(s(s(s(s(s(s(s(s(x1)))))))))
tower(0(x1)) = x1 + 180 >= x1 + 133 = s(0(p(s(p(s(x1))))))
problem:
strict:
tower(s(x1)) -> p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))))
twoto(s(x1)) ->
p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))))
twice(s(x1)) -> p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))))
p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
weak:
twoto(0(x1)) -> s(0(x1))
twice(0(x1)) -> 0(x1)
p(p(s(x1))) -> p(x1)
p(s(x1)) -> x1
tower(0(x1)) -> s(0(p(s(p(s(x1))))))
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[twice](x0) = x0 + 17,
[twoto](x0) = x0,
[p](x0) = x0 + 1,
[s](x0) = x0,
[tower](x0) = x0 + 8,
[0](x0) = x0 + 6
orientation:
tower(s(x1)) = x1 + 8 >= x1 + 14 = p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))))
twoto(s(x1)) = x1 >= x1 + 32 = p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))))
twice(s(x1)) = x1 + 17 >= x1 + 23 = p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))))
p(0(x1)) = x1 + 7 >= x1 + 6 = 0(s(s(s(s(s(s(s(s(x1)))))))))
twoto(0(x1)) = x1 + 6 >= x1 + 6 = s(0(x1))
twice(0(x1)) = x1 + 23 >= x1 + 6 = 0(x1)
p(p(s(x1))) = x1 + 2 >= x1 + 1 = p(x1)
p(s(x1)) = x1 + 1 >= x1 = x1
tower(0(x1)) = x1 + 14 >= x1 + 8 = s(0(p(s(p(s(x1))))))
problem:
strict:
tower(s(x1)) -> p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))))
twoto(s(x1)) ->
p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))))
twice(s(x1)) -> p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))))
weak:
p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))
twoto(0(x1)) -> s(0(x1))
twice(0(x1)) -> 0(x1)
p(p(s(x1))) -> p(x1)
p(s(x1)) -> x1
tower(0(x1)) -> s(0(p(s(p(s(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:
{ tower(0(x1)) -> s(0(p(s(p(s(x1))))))
, tower(s(x1)) ->
p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))))
, twoto(0(x1)) -> s(0(x1))
, twoto(s(x1)) ->
p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))))
, twice(0(x1)) -> 0(x1)
, twice(s(x1)) ->
p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(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:
{ tower(0(x1)) -> s(0(p(s(p(s(x1))))))
, tower(s(x1)) ->
p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))))
, twoto(0(x1)) -> s(0(x1))
, twoto(s(x1)) ->
p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))))
, twice(0(x1)) -> 0(x1)
, twice(s(x1)) ->
p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))}
Proof Output:
Computation stopped due to timeout after 60.0 seconds