Tool CaT
stdout:
MAYBE
Problem:
f(0(x1)) -> s(0(x1))
d(0(x1)) -> 0(x1)
d(s(x1)) -> s(s(d(p(s(x1)))))
f(s(x1)) -> d(f(p(s(x1))))
p(s(x1)) -> x1
Proof:
Complexity Transformation Processor:
strict:
f(0(x1)) -> s(0(x1))
d(0(x1)) -> 0(x1)
d(s(x1)) -> s(s(d(p(s(x1)))))
f(s(x1)) -> d(f(p(s(x1))))
p(s(x1)) -> x1
weak:
Arctic Interpretation Processor:
dimension: 1
interpretation:
[p](x0) = x0,
[d](x0) = x0,
[s](x0) = x0,
[f](x0) = 4x0,
[0](x0) = 4x0
orientation:
f(0(x1)) = 8x1 >= 4x1 = s(0(x1))
d(0(x1)) = 4x1 >= 4x1 = 0(x1)
d(s(x1)) = x1 >= x1 = s(s(d(p(s(x1)))))
f(s(x1)) = 4x1 >= 4x1 = d(f(p(s(x1))))
p(s(x1)) = x1 >= x1 = x1
problem:
strict:
d(0(x1)) -> 0(x1)
d(s(x1)) -> s(s(d(p(s(x1)))))
f(s(x1)) -> d(f(p(s(x1))))
p(s(x1)) -> x1
weak:
f(0(x1)) -> s(0(x1))
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {5,4,3}
transitions:
01(45) -> 46*
01(47) -> 48*
s1(60) -> 61*
s1(32) -> 33*
s1(84) -> 85*
s1(59) -> 60*
s1(19) -> 20*
s1(14) -> 15*
s1(83) -> 84*
s1(33) -> 34*
d1(82) -> 83*
d1(17) -> 18*
d1(31) -> 32*
d1(58) -> 59*
p1(15) -> 16*
p1(102) -> 103*
p1(62) -> 63*
p1(57) -> 58*
p1(136) -> 137*
p1(81) -> 82*
p1(130) -> 131*
f1(16) -> 17*
d0(2) -> 3*
d0(1) -> 3*
00(2) -> 1*
00(1) -> 1*
s0(2) -> 2*
s0(1) -> 2*
p0(2) -> 5*
p0(1) -> 5*
f0(2) -> 4*
f0(1) -> 4*
1 -> 47,5,3,19
2 -> 45,5,4,14
14 -> 16*
16 -> 31*
18 -> 17,4
19 -> 16*
20 -> 15*
32 -> 58*
33 -> 82,57,17
34 -> 81,32,3
46 -> 83,59,32
48 -> 83,59,32
59 -> 103*
60 -> 102,63
61 -> 83,62,18
63 -> 58*
83 -> 137*
84 -> 136,131
85 -> 130,59
103 -> 82*
131 -> 58*
137 -> 82*
problem:
strict:
d(0(x1)) -> 0(x1)
d(s(x1)) -> s(s(d(p(s(x1)))))
p(s(x1)) -> x1
weak:
f(s(x1)) -> d(f(p(s(x1))))
f(0(x1)) -> s(0(x1))
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[p](x0) = x0,
[d](x0) = x0,
[s](x0) = x0 + 38,
[f](x0) = x0 + 38,
[0](x0) = x0 + 18
orientation:
d(0(x1)) = x1 + 18 >= x1 + 18 = 0(x1)
d(s(x1)) = x1 + 38 >= x1 + 114 = s(s(d(p(s(x1)))))
p(s(x1)) = x1 + 38 >= x1 = x1
f(s(x1)) = x1 + 76 >= x1 + 76 = d(f(p(s(x1))))
f(0(x1)) = x1 + 56 >= x1 + 56 = s(0(x1))
problem:
strict:
d(0(x1)) -> 0(x1)
d(s(x1)) -> s(s(d(p(s(x1)))))
weak:
p(s(x1)) -> x1
f(s(x1)) -> d(f(p(s(x1))))
f(0(x1)) -> s(0(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:
{ f(0(x1)) -> s(0(x1))
, d(0(x1)) -> 0(x1)
, d(s(x1)) -> s(s(d(p(s(x1)))))
, f(s(x1)) -> d(f(p(s(x1))))
, p(s(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:
{ f(0(x1)) -> s(0(x1))
, d(0(x1)) -> 0(x1)
, d(s(x1)) -> s(s(d(p(s(x1)))))
, f(s(x1)) -> d(f(p(s(x1))))
, p(s(x1)) -> x1}
Proof Output:
Computation stopped due to timeout after 60.0 seconds