Tool CaT
stdout:
MAYBE
Problem:
p(0(x1)) -> 0(s(s(p(x1))))
p(s(x1)) -> x1
p(p(s(x1))) -> p(x1)
f(s(x1)) -> g(s(x1))
g(x1) -> i(s(half(x1)))
i(x1) -> f(p(x1))
half(0(x1)) -> 0(s(s(half(x1))))
half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
0(x1) -> x1
rd(0(x1)) -> 0(0(0(0(0(0(rd(x1)))))))
Proof:
Complexity Transformation Processor:
strict:
p(0(x1)) -> 0(s(s(p(x1))))
p(s(x1)) -> x1
p(p(s(x1))) -> p(x1)
f(s(x1)) -> g(s(x1))
g(x1) -> i(s(half(x1)))
i(x1) -> f(p(x1))
half(0(x1)) -> 0(s(s(half(x1))))
half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
0(x1) -> x1
rd(0(x1)) -> 0(0(0(0(0(0(rd(x1)))))))
weak:
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[rd](x0) = x0 + 8,
[i](x0) = x0 + 16,
[half](x0) = x0 + 16,
[g](x0) = x0 + 8,
[f](x0) = x0,
[s](x0) = x0,
[p](x0) = x0 + 15,
[0](x0) = x0
orientation:
p(0(x1)) = x1 + 15 >= x1 + 15 = 0(s(s(p(x1))))
p(s(x1)) = x1 + 15 >= x1 = x1
p(p(s(x1))) = x1 + 30 >= x1 + 15 = p(x1)
f(s(x1)) = x1 >= x1 + 8 = g(s(x1))
g(x1) = x1 + 8 >= x1 + 32 = i(s(half(x1)))
i(x1) = x1 + 16 >= x1 + 15 = f(p(x1))
half(0(x1)) = x1 + 16 >= x1 + 16 = 0(s(s(half(x1))))
half(s(s(x1))) = x1 + 16 >= x1 + 46 = s(half(p(p(s(s(x1))))))
0(x1) = x1 >= x1 = x1
rd(0(x1)) = x1 + 8 >= x1 + 8 = 0(0(0(0(0(0(rd(x1)))))))
problem:
strict:
p(0(x1)) -> 0(s(s(p(x1))))
f(s(x1)) -> g(s(x1))
g(x1) -> i(s(half(x1)))
half(0(x1)) -> 0(s(s(half(x1))))
half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
0(x1) -> x1
rd(0(x1)) -> 0(0(0(0(0(0(rd(x1)))))))
weak:
p(s(x1)) -> x1
p(p(s(x1))) -> p(x1)
i(x1) -> f(p(x1))
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[rd](x0) = x0 + 7,
[i](x0) = x0 + 1,
[half](x0) = x0 + 28,
[g](x0) = x0,
[f](x0) = x0 + 1,
[s](x0) = x0,
[p](x0) = x0,
[0](x0) = x0
orientation:
p(0(x1)) = x1 >= x1 = 0(s(s(p(x1))))
f(s(x1)) = x1 + 1 >= x1 = g(s(x1))
g(x1) = x1 >= x1 + 29 = i(s(half(x1)))
half(0(x1)) = x1 + 28 >= x1 + 28 = 0(s(s(half(x1))))
half(s(s(x1))) = x1 + 28 >= x1 + 28 = s(half(p(p(s(s(x1))))))
0(x1) = x1 >= x1 = x1
rd(0(x1)) = x1 + 7 >= x1 + 7 = 0(0(0(0(0(0(rd(x1)))))))
p(s(x1)) = x1 >= x1 = x1
p(p(s(x1))) = x1 >= x1 = p(x1)
i(x1) = x1 + 1 >= x1 + 1 = f(p(x1))
problem:
strict:
p(0(x1)) -> 0(s(s(p(x1))))
g(x1) -> i(s(half(x1)))
half(0(x1)) -> 0(s(s(half(x1))))
half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
0(x1) -> x1
rd(0(x1)) -> 0(0(0(0(0(0(rd(x1)))))))
weak:
f(s(x1)) -> g(s(x1))
p(s(x1)) -> x1
p(p(s(x1))) -> p(x1)
i(x1) -> f(p(x1))
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[rd](x0) = x0 + 7,
[i](x0) = x0 + 10,
[half](x0) = x0 + 32,
[g](x0) = x0,
[f](x0) = x0,
[s](x0) = x0,
[p](x0) = x0,
[0](x0) = x0 + 40
orientation:
p(0(x1)) = x1 + 40 >= x1 + 40 = 0(s(s(p(x1))))
g(x1) = x1 >= x1 + 42 = i(s(half(x1)))
half(0(x1)) = x1 + 72 >= x1 + 72 = 0(s(s(half(x1))))
half(s(s(x1))) = x1 + 32 >= x1 + 32 = s(half(p(p(s(s(x1))))))
0(x1) = x1 + 40 >= x1 = x1
rd(0(x1)) = x1 + 47 >= x1 + 247 = 0(0(0(0(0(0(rd(x1)))))))
f(s(x1)) = x1 >= x1 = g(s(x1))
p(s(x1)) = x1 >= x1 = x1
p(p(s(x1))) = x1 >= x1 = p(x1)
i(x1) = x1 + 10 >= x1 = f(p(x1))
problem:
strict:
p(0(x1)) -> 0(s(s(p(x1))))
g(x1) -> i(s(half(x1)))
half(0(x1)) -> 0(s(s(half(x1))))
half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
rd(0(x1)) -> 0(0(0(0(0(0(rd(x1)))))))
weak:
0(x1) -> x1
f(s(x1)) -> g(s(x1))
p(s(x1)) -> x1
p(p(s(x1))) -> p(x1)
i(x1) -> f(p(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:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, f(s(x1)) -> g(s(x1))
, g(x1) -> i(s(half(x1)))
, i(x1) -> f(p(x1))
, half(0(x1)) -> 0(s(s(half(x1))))
, half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
, 0(x1) -> x1
, rd(0(x1)) -> 0(0(0(0(0(0(rd(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:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, f(s(x1)) -> g(s(x1))
, g(x1) -> i(s(half(x1)))
, i(x1) -> f(p(x1))
, half(0(x1)) -> 0(s(s(half(x1))))
, half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
, 0(x1) -> x1
, rd(0(x1)) -> 0(0(0(0(0(0(rd(x1)))))))}
Proof Output:
Computation stopped due to timeout after 60.0 seconds