Tool CaT
stdout:
MAYBE
Problem:
ackin(s(X),s(Y)) -> u21(ackin(s(X),Y),X)
u21(ackout(X),Y) -> u22(ackin(Y,X))
Proof:
OpenTool IRC1
stdout:
MAYBE
Tool IRC2
stdout:
YES(?,O(n^1))
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ ackin(s(X), s(Y)) -> u21(ackin(s(X), Y), X)
, u21(ackout(X), Y) -> u22(ackin(Y, X))}
Proof Output:
'matrix-interpretation of dimension 1' proved the best result:
Details:
--------
'matrix-interpretation of dimension 1' succeeded with the following output:
'matrix-interpretation of dimension 1'
--------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ ackin(s(X), s(Y)) -> u21(ackin(s(X), Y), X)
, u21(ackout(X), Y) -> u22(ackin(Y, X))}
Proof Output:
The following argument positions are usable:
Uargs(ackin) = {}, Uargs(s) = {}, Uargs(u21) = {1},
Uargs(ackout) = {}, Uargs(u22) = {1}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
ackin(x1, x2) = [0] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [2]
u21(x1, x2) = [1] x1 + [0] x2 + [0]
ackout(x1) = [1] x1 + [1]
u22(x1) = [1] x1 + [0]Tool RC1
stdout:
MAYBE
Tool RC2
stdout:
YES(?,O(n^1))
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ ackin(s(X), s(Y)) -> u21(ackin(s(X), Y), X)
, u21(ackout(X), Y) -> u22(ackin(Y, X))}
Proof Output:
'matrix-interpretation of dimension 1' proved the best result:
Details:
--------
'matrix-interpretation of dimension 1' succeeded with the following output:
'matrix-interpretation of dimension 1'
--------------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ ackin(s(X), s(Y)) -> u21(ackin(s(X), Y), X)
, u21(ackout(X), Y) -> u22(ackin(Y, X))}
Proof Output:
The following argument positions are usable:
Uargs(ackin) = {}, Uargs(s) = {}, Uargs(u21) = {1},
Uargs(ackout) = {}, Uargs(u22) = {1}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
ackin(x1, x2) = [0] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [2]
u21(x1, x2) = [1] x1 + [0] x2 + [0]
ackout(x1) = [1] x1 + [1]
u22(x1) = [1] x1 + [0]