Tool CaT
stdout:
MAYBE
Problem:
p(0(x1)) -> s(s(0(s(s(p(x1))))))
p(s(0(x1))) -> 0(x1)
p(s(s(x1))) -> s(p(s(x1)))
f(s(x1)) -> g(q(i(x1)))
g(x1) -> f(p(p(x1)))
q(i(x1)) -> q(s(x1))
q(s(x1)) -> s(s(x1))
i(x1) -> s(x1)
Proof:
Complexity Transformation Processor:
strict:
p(0(x1)) -> s(s(0(s(s(p(x1))))))
p(s(0(x1))) -> 0(x1)
p(s(s(x1))) -> s(p(s(x1)))
f(s(x1)) -> g(q(i(x1)))
g(x1) -> f(p(p(x1)))
q(i(x1)) -> q(s(x1))
q(s(x1)) -> s(s(x1))
i(x1) -> s(x1)
weak:
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[g](x0) = x0,
[q](x0) = x0 + 80,
[i](x0) = x0 + 192,
[f](x0) = x0,
[s](x0) = x0,
[p](x0) = x0 + 8,
[0](x0) = x0 + 248
orientation:
p(0(x1)) = x1 + 256 >= x1 + 256 = s(s(0(s(s(p(x1))))))
p(s(0(x1))) = x1 + 256 >= x1 + 248 = 0(x1)
p(s(s(x1))) = x1 + 8 >= x1 + 8 = s(p(s(x1)))
f(s(x1)) = x1 >= x1 + 272 = g(q(i(x1)))
g(x1) = x1 >= x1 + 16 = f(p(p(x1)))
q(i(x1)) = x1 + 272 >= x1 + 80 = q(s(x1))
q(s(x1)) = x1 + 80 >= x1 = s(s(x1))
i(x1) = x1 + 192 >= x1 = s(x1)
problem:
strict:
p(0(x1)) -> s(s(0(s(s(p(x1))))))
p(s(s(x1))) -> s(p(s(x1)))
f(s(x1)) -> g(q(i(x1)))
g(x1) -> f(p(p(x1)))
weak:
p(s(0(x1))) -> 0(x1)
q(i(x1)) -> q(s(x1))
q(s(x1)) -> s(s(x1))
i(x1) -> s(x1)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[g](x0) = x0 + 158,
[q](x0) = x0 + 68,
[i](x0) = x0 + 224,
[f](x0) = x0 + 39,
[s](x0) = x0 + 9,
[p](x0) = x0 + 59,
[0](x0) = x0 + 97
orientation:
p(0(x1)) = x1 + 156 >= x1 + 192 = s(s(0(s(s(p(x1))))))
p(s(s(x1))) = x1 + 77 >= x1 + 77 = s(p(s(x1)))
f(s(x1)) = x1 + 48 >= x1 + 450 = g(q(i(x1)))
g(x1) = x1 + 158 >= x1 + 157 = f(p(p(x1)))
p(s(0(x1))) = x1 + 165 >= x1 + 97 = 0(x1)
q(i(x1)) = x1 + 292 >= x1 + 77 = q(s(x1))
q(s(x1)) = x1 + 77 >= x1 + 18 = s(s(x1))
i(x1) = x1 + 224 >= x1 + 9 = s(x1)
problem:
strict:
p(0(x1)) -> s(s(0(s(s(p(x1))))))
p(s(s(x1))) -> s(p(s(x1)))
f(s(x1)) -> g(q(i(x1)))
weak:
g(x1) -> f(p(p(x1)))
p(s(0(x1))) -> 0(x1)
q(i(x1)) -> q(s(x1))
q(s(x1)) -> s(s(x1))
i(x1) -> s(x1)
Matrix Interpretation Processor:
dimension: 4
max_matrix:
[1 2 2 1]
[0 0 2 2]
[0 0 0 1]
[0 0 0 0]
interpretation:
[1 1 2 0]
[0 0 0 0]
[g](x0) = [0 0 0 1]x0
[0 0 0 0] ,
[1 0 0 0]
[0 0 0 0]
[q](x0) = [0 0 0 0]x0
[0 0 0 0] ,
[1 0 0 0] [0]
[0 0 2 2] [1]
[i](x0) = [0 0 0 1]x0 + [0]
[0 0 0 0] [2],
[1 0 0 0]
[0 0 0 0]
[f](x0) = [0 0 0 0]x0
[0 0 0 0] ,
[1 0 0 0]
[0 0 0 0]
[s](x0) = [0 0 0 1]x0
[0 0 0 0] ,
[1 1 0 0] [0]
[0 0 2 0] [0]
[p](x0) = [0 0 0 1]x0 + [1]
[0 0 0 0] [1],
[1 2 0 1] [1]
[0 0 0 0] [2]
[0](x0) = [0 0 0 0]x0 + [1]
[0 0 0 0] [1]
orientation:
[1 2 0 1] [3] [1 1 0 0] [1]
[0 0 0 0] [2] [0 0 0 0] [0]
p(0(x1)) = [0 0 0 0]x1 + [2] >= [0 0 0 0]x1 + [0] = s(s(0(s(s(p(x1))))))
[0 0 0 0] [1] [0 0 0 0] [0]
[1 0 0 0] [0] [1 0 0 0] [0]
[0 0 0 0] [0] [0 0 0 0] [0]
p(s(s(x1))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = s(p(s(x1)))
[0 0 0 0] [1] [0 0 0 0] [0]
[1 0 0 0] [1 0 0 0]
[0 0 0 0] [0 0 0 0]
f(s(x1)) = [0 0 0 0]x1 >= [0 0 0 0]x1 = g(q(i(x1)))
[0 0 0 0] [0 0 0 0]
[1 1 2 0] [1 1 2 0]
[0 0 0 0] [0 0 0 0]
g(x1) = [0 0 0 1]x1 >= [0 0 0 0]x1 = f(p(p(x1)))
[0 0 0 0] [0 0 0 0]
[1 2 0 1] [1] [1 2 0 1] [1]
[0 0 0 0] [2] [0 0 0 0] [2]
p(s(0(x1))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = 0(x1)
[0 0 0 0] [1] [0 0 0 0] [1]
[1 0 0 0] [1 0 0 0]
[0 0 0 0] [0 0 0 0]
q(i(x1)) = [0 0 0 0]x1 >= [0 0 0 0]x1 = q(s(x1))
[0 0 0 0] [0 0 0 0]
[1 0 0 0] [1 0 0 0]
[0 0 0 0] [0 0 0 0]
q(s(x1)) = [0 0 0 0]x1 >= [0 0 0 0]x1 = s(s(x1))
[0 0 0 0] [0 0 0 0]
[1 0 0 0] [0] [1 0 0 0]
[0 0 2 2] [1] [0 0 0 0]
i(x1) = [0 0 0 1]x1 + [0] >= [0 0 0 1]x1 = s(x1)
[0 0 0 0] [2] [0 0 0 0]
problem:
strict:
p(s(s(x1))) -> s(p(s(x1)))
f(s(x1)) -> g(q(i(x1)))
weak:
p(0(x1)) -> s(s(0(s(s(p(x1))))))
g(x1) -> f(p(p(x1)))
p(s(0(x1))) -> 0(x1)
q(i(x1)) -> q(s(x1))
q(s(x1)) -> s(s(x1))
i(x1) -> 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:
{ p(0(x1)) -> s(s(0(s(s(p(x1))))))
, p(s(0(x1))) -> 0(x1)
, p(s(s(x1))) -> s(p(s(x1)))
, f(s(x1)) -> g(q(i(x1)))
, g(x1) -> f(p(p(x1)))
, q(i(x1)) -> q(s(x1))
, q(s(x1)) -> s(s(x1))
, i(x1) -> 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:
{ p(0(x1)) -> s(s(0(s(s(p(x1))))))
, p(s(0(x1))) -> 0(x1)
, p(s(s(x1))) -> s(p(s(x1)))
, f(s(x1)) -> g(q(i(x1)))
, g(x1) -> f(p(p(x1)))
, q(i(x1)) -> q(s(x1))
, q(s(x1)) -> s(s(x1))
, i(x1) -> s(x1)}
Proof Output:
Computation stopped due to timeout after 60.0 seconds