Tool CaT
stdout:
MAYBE
Problem:
f(0(),1()) -> f(2(),2())
2() -> 0()
2() -> 1()
f(2(),1()) -> 2()
f(0(),2()) -> 2()
Proof:
Uncurry Processor:
01(1()) -> 21(2())
21(x1) -> 01(x1)
2() -> 0()
21(x2) -> f(1(),x2)
2() -> 1()
21(1()) -> 2()
01(2()) -> 2()
f(0(),x0) -> 01(x0)
f(2(),x0) -> 21(x0)
Complexity Transformation Processor:
strict:
01(1()) -> 21(2())
21(x1) -> 01(x1)
2() -> 0()
21(x2) -> f(1(),x2)
2() -> 1()
21(1()) -> 2()
01(2()) -> 2()
f(0(),x0) -> 01(x0)
f(2(),x0) -> 21(x0)
weak:
Bounds Processor:
bound: 0
enrichment: match
automaton:
final states: {6,5,4,3}
transitions:
0{1,0}(5) -> 3*
0{1,0}(2) -> 6,4,3
0{1,0}(4) -> 4,6
0{1,0}(1) -> 6,4,3
10() -> 6,3,4,5,1
2{1,0}(5) -> 3*
2{1,0}(2) -> 4*
2{1,0}(4) -> 6,4
2{1,0}(1) -> 4*
20() -> 6,3,4,5
00() -> 6,3,4,5,2
f0(1,2) -> 4,6
f0(1,4) -> 4,6
f0(2,1) -> 6*
f0(1,1) -> 4,6
f0(1,5) -> 3*
f0(2,2) -> 6*
problem:
strict:
01(1()) -> 21(2())
21(x1) -> 01(x1)
2() -> 0()
21(x2) -> f(1(),x2)
2() -> 1()
21(1()) -> 2()
01(2()) -> 2()
f(0(),x0) -> 01(x0)
weak:
f(2(),x0) -> 21(x0)
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {6,5,4,3}
transitions:
f1(12,1) -> 4*
f1(12,5) -> 3*
f1(12,2) -> 4*
f1(12,4) -> 6,4
11() -> 12*
0{1,0}(5) -> 3*
0{1,0}(2) -> 6,4,3
0{1,0}(4) -> 4,6
0{1,0}(1) -> 6,4,3
10() -> 6,3,4,5,1
2{1,0}(5) -> 3*
2{1,0}(2) -> 4*
2{1,0}(4) -> 6,4
2{1,0}(1) -> 4*
20() -> 6,3,4,5
00() -> 6,3,4,5,2
f0(1,2) -> 6*
f0(2,1) -> 6*
f0(1,1) -> 6*
f0(2,2) -> 6*
problem:
strict:
01(1()) -> 21(2())
21(x1) -> 01(x1)
2() -> 0()
2() -> 1()
21(1()) -> 2()
01(2()) -> 2()
f(0(),x0) -> 01(x0)
weak:
21(x2) -> f(1(),x2)
f(2(),x0) -> 21(x0)
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {6,5,4,3}
transitions:
01() -> 11*
f1(23,1) -> 4*
f1(23,5) -> 3*
f1(23,2) -> 4*
f1(23,4) -> 4,6
11() -> 23*
0{1,0}(5) -> 3*
0{1,0}(2) -> 6,4,3
0{1,0}(4) -> 4,6
0{1,0}(1) -> 6,4,3
10() -> 6,3,4,5,1
2{1,0}(5) -> 3*
2{1,0}(2) -> 4*
2{1,0}(4) -> 6,4
2{1,0}(1) -> 4*
20() -> 6,3,4,5
00() -> 2*
f0(1,2) -> 6*
f0(2,1) -> 6*
f0(1,1) -> 6*
f0(2,2) -> 6*
11 -> 6,3,4,5
problem:
strict:
01(1()) -> 21(2())
21(x1) -> 01(x1)
2() -> 1()
21(1()) -> 2()
01(2()) -> 2()
f(0(),x0) -> 01(x0)
weak:
2() -> 0()
21(x2) -> f(1(),x2)
f(2(),x0) -> 21(x0)
Matrix Interpretation Processor:
dimension: 4
max_matrix:
[1 0 1 1]
[0 0 1 0]
[0 0 0 0]
[0 0 0 0]
interpretation:
[1 0 1 1] [0]
[0 0 1 0] [0]
[21](x0) = [0 0 0 0]x0 + [2]
[0 0 0 0] [0],
[1 0 1 0] [0]
[0 0 1 0] [0]
[01](x0) = [0 0 0 0]x0 + [2]
[0 0 0 0] [0],
[0]
[0]
[2] = [2]
[0],
[1 0 0 0] [1 0 1 1] [0]
[0 0 0 0] [0 0 1 0] [0]
[f](x0, x1) = [0 0 0 0]x0 + [0 0 0 0]x1 + [2]
[0 0 0 0] [0 0 0 0] [0],
[0]
[0]
[1] = [2]
[0],
[0]
[0]
[0] = [0]
[0]
orientation:
[2] [2]
[2] [2]
01(1()) = [2] >= [2] = 21(2())
[0] [0]
[1 0 1 1] [0] [1 0 1 0] [0]
[0 0 1 0] [0] [0 0 1 0] [0]
21(x1) = [0 0 0 0]x1 + [2] >= [0 0 0 0]x1 + [2] = 01(x1)
[0 0 0 0] [0] [0 0 0 0] [0]
[0] [0]
[0] [0]
2() = [2] >= [2] = 1()
[0] [0]
[2] [0]
[2] [0]
21(1()) = [2] >= [2] = 2()
[0] [0]
[2] [0]
[2] [0]
01(2()) = [2] >= [2] = 2()
[0] [0]
[1 0 1 1] [0] [1 0 1 0] [0]
[0 0 1 0] [0] [0 0 1 0] [0]
f(0(),x0) = [0 0 0 0]x0 + [2] >= [0 0 0 0]x0 + [2] = 01(x0)
[0 0 0 0] [0] [0 0 0 0] [0]
[0] [0]
[0] [0]
2() = [2] >= [0] = 0()
[0] [0]
[1 0 1 1] [0] [1 0 1 1] [0]
[0 0 1 0] [0] [0 0 1 0] [0]
21(x2) = [0 0 0 0]x2 + [2] >= [0 0 0 0]x2 + [2] = f(1(),x2)
[0 0 0 0] [0] [0 0 0 0] [0]
[1 0 1 1] [0] [1 0 1 1] [0]
[0 0 1 0] [0] [0 0 1 0] [0]
f(2(),x0) = [0 0 0 0]x0 + [2] >= [0 0 0 0]x0 + [2] = 21(x0)
[0 0 0 0] [0] [0 0 0 0] [0]
problem:
strict:
01(1()) -> 21(2())
21(x1) -> 01(x1)
2() -> 1()
f(0(),x0) -> 01(x0)
weak:
21(1()) -> 2()
01(2()) -> 2()
2() -> 0()
21(x2) -> f(1(),x2)
f(2(),x0) -> 21(x0)
Matrix Interpretation Processor:
dimension: 4
max_matrix:
[1 0 0 1]
[0 0 2 0]
[0 0 0 0]
[0 0 0 0]
interpretation:
[1 0 0 0] [2]
[0 0 2 0] [1]
[21](x0) = [0 0 0 0]x0 + [2]
[0 0 0 0] [3],
[1 0 0 0] [2]
[0 0 0 0] [1]
[01](x0) = [0 0 0 0]x0 + [2]
[0 0 0 0] [3],
[0]
[0]
[2] = [0]
[3],
[1 0 0 1] [1 0 0 0] [0]
[0 0 0 0] [0 0 2 0] [1]
[f](x0, x1) = [0 0 0 0]x0 + [0 0 0 0]x1 + [2]
[0 0 0 0] [0 0 0 0] [3],
[0]
[0]
[1] = [0]
[2],
[0]
[0]
[0] = [0]
[3]
orientation:
[2] [2]
[1] [1]
01(1()) = [2] >= [2] = 21(2())
[3] [3]
[1 0 0 0] [2] [1 0 0 0] [2]
[0 0 2 0] [1] [0 0 0 0] [1]
21(x1) = [0 0 0 0]x1 + [2] >= [0 0 0 0]x1 + [2] = 01(x1)
[0 0 0 0] [3] [0 0 0 0] [3]
[0] [0]
[0] [0]
2() = [0] >= [0] = 1()
[3] [2]
[1 0 0 0] [3] [1 0 0 0] [2]
[0 0 2 0] [1] [0 0 0 0] [1]
f(0(),x0) = [0 0 0 0]x0 + [2] >= [0 0 0 0]x0 + [2] = 01(x0)
[0 0 0 0] [3] [0 0 0 0] [3]
[2] [0]
[1] [0]
21(1()) = [2] >= [0] = 2()
[3] [3]
[2] [0]
[1] [0]
01(2()) = [2] >= [0] = 2()
[3] [3]
[0] [0]
[0] [0]
2() = [0] >= [0] = 0()
[3] [3]
[1 0 0 0] [2] [1 0 0 0] [2]
[0 0 2 0] [1] [0 0 2 0] [1]
21(x2) = [0 0 0 0]x2 + [2] >= [0 0 0 0]x2 + [2] = f(1(),x2)
[0 0 0 0] [3] [0 0 0 0] [3]
[1 0 0 0] [3] [1 0 0 0] [2]
[0 0 2 0] [1] [0 0 2 0] [1]
f(2(),x0) = [0 0 0 0]x0 + [2] >= [0 0 0 0]x0 + [2] = 21(x0)
[0 0 0 0] [3] [0 0 0 0] [3]
problem:
strict:
01(1()) -> 21(2())
21(x1) -> 01(x1)
2() -> 1()
weak:
f(0(),x0) -> 01(x0)
21(1()) -> 2()
01(2()) -> 2()
2() -> 0()
21(x2) -> f(1(),x2)
f(2(),x0) -> 21(x0)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[21](x0) = x0 + 76,
[01](x0) = x0,
[2] = 78,
[f](x0, x1) = x0 + x1,
[1] = 2,
[0] = 0
orientation:
01(1()) = 2 >= 154 = 21(2())
21(x1) = x1 + 76 >= x1 = 01(x1)
2() = 78 >= 2 = 1()
f(0(),x0) = x0 >= x0 = 01(x0)
21(1()) = 78 >= 78 = 2()
01(2()) = 78 >= 78 = 2()
2() = 78 >= 0 = 0()
21(x2) = x2 + 76 >= x2 + 2 = f(1(),x2)
f(2(),x0) = x0 + 78 >= x0 + 76 = 21(x0)
problem:
strict:
01(1()) -> 21(2())
weak:
21(x1) -> 01(x1)
2() -> 1()
f(0(),x0) -> 01(x0)
21(1()) -> 2()
01(2()) -> 2()
2() -> 0()
21(x2) -> f(1(),x2)
f(2(),x0) -> 21(x0)
Open
Tool IRC1
stdout:
MAYBE
Warning when parsing problem:
Unsupported strategy 'OUTERMOST'Tool IRC2
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: innermost runtime-complexity with respect to
Rules:
{ f(0(), 1()) -> f(2(), 2())
, 2() -> 0()
, 2() -> 1()
, f(2(), 1()) -> 2()
, f(0(), 2()) -> 2()}
Proof Output:
Computation stopped due to timeout after 60.0 secondsTool RC1
stdout:
MAYBE
Warning when parsing problem:
Unsupported strategy 'OUTERMOST'Tool RC2
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: runtime-complexity with respect to
Rules:
{ f(0(), 1()) -> f(2(), 2())
, 2() -> 0()
, 2() -> 1()
, f(2(), 1()) -> 2()
, f(0(), 2()) -> 2()}
Proof Output:
Computation stopped due to timeout after 60.0 seconds