Tool CaT
Execution Time | Unknown |
---|
Answer | MAYBE |
---|
Input | SK90 4.43 |
---|
stdout:
MAYBE
Problem:
+(x,0()) -> x
+(x,s(y)) -> s(+(x,y))
+(0(),y) -> y
+(s(x),y) -> s(+(x,y))
+(x,+(y,z)) -> +(+(x,y),z)
f(g(f(x))) -> f(h(s(0()),x))
f(g(h(x,y))) -> f(h(s(x),y))
f(h(x,h(y,z))) -> f(h(+(x,y),z))
Proof:
Complexity Transformation Processor:
strict:
+(x,0()) -> x
+(x,s(y)) -> s(+(x,y))
+(0(),y) -> y
+(s(x),y) -> s(+(x,y))
+(x,+(y,z)) -> +(+(x,y),z)
f(g(f(x))) -> f(h(s(0()),x))
f(g(h(x,y))) -> f(h(s(x),y))
f(h(x,h(y,z))) -> f(h(+(x,y),z))
weak:
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[h](x0, x1) = x0 + x1 + 12,
[g](x0) = x0 + 3,
[f](x0) = x0 + 7,
[s](x0) = x0,
[+](x0, x1) = x0 + x1 + 1,
[0] = 1
orientation:
+(x,0()) = x + 2 >= x = x
+(x,s(y)) = x + y + 1 >= x + y + 1 = s(+(x,y))
+(0(),y) = y + 2 >= y = y
+(s(x),y) = x + y + 1 >= x + y + 1 = s(+(x,y))
+(x,+(y,z)) = x + y + z + 2 >= x + y + z + 2 = +(+(x,y),z)
f(g(f(x))) = x + 17 >= x + 20 = f(h(s(0()),x))
f(g(h(x,y))) = x + y + 22 >= x + y + 19 = f(h(s(x),y))
f(h(x,h(y,z))) = x + y + z + 31 >= x + y + z + 20 = f(h(+(x,y),z))
problem:
strict:
+(x,s(y)) -> s(+(x,y))
+(s(x),y) -> s(+(x,y))
+(x,+(y,z)) -> +(+(x,y),z)
f(g(f(x))) -> f(h(s(0()),x))
weak:
+(x,0()) -> x
+(0(),y) -> y
f(g(h(x,y))) -> f(h(s(x),y))
f(h(x,h(y,z))) -> f(h(+(x,y),z))
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[h](x0, x1) = x0 + x1 + 73,
[g](x0) = x0 + 72,
[f](x0) = x0 + 72,
[s](x0) = x0 + 39,
[+](x0, x1) = x0 + x1 + 3,
[0] = 10
orientation:
+(x,s(y)) = x + y + 42 >= x + y + 42 = s(+(x,y))
+(s(x),y) = x + y + 42 >= x + y + 42 = s(+(x,y))
+(x,+(y,z)) = x + y + z + 6 >= x + y + z + 6 = +(+(x,y),z)
f(g(f(x))) = x + 216 >= x + 194 = f(h(s(0()),x))
+(x,0()) = x + 13 >= x = x
+(0(),y) = y + 13 >= y = y
f(g(h(x,y))) = x + y + 217 >= x + y + 184 = f(h(s(x),y))
f(h(x,h(y,z))) = x + y + z + 218 >= x + y + z + 148 = f(h(+(x,y),z))
problem:
strict:
+(x,s(y)) -> s(+(x,y))
+(s(x),y) -> s(+(x,y))
+(x,+(y,z)) -> +(+(x,y),z)
weak:
f(g(f(x))) -> f(h(s(0()),x))
+(x,0()) -> x
+(0(),y) -> y
f(g(h(x,y))) -> f(h(s(x),y))
f(h(x,h(y,z))) -> f(h(+(x,y),z))
Matrix Interpretation Processor:
dimension: 2
max_matrix:
[1 2]
[0 1]
interpretation:
[1 1] [1 1] [0]
[h](x0, x1) = [0 1]x0 + [0 1]x1 + [1],
[1 2] [1]
[g](x0) = [0 1]x0 + [0],
[0]
[f](x0) = x0 + [1],
[1]
[s](x0) = x0 + [0],
[1 1] [0]
[+](x0, x1) = x0 + [0 1]x1 + [1],
[2]
[0] = [0]
orientation:
[1 1] [1] [1 1] [1]
+(x,s(y)) = x + [0 1]y + [1] >= x + [0 1]y + [1] = s(+(x,y))
[1 1] [1] [1 1] [1]
+(s(x),y) = x + [0 1]y + [1] >= x + [0 1]y + [1] = s(+(x,y))
[1 1] [1 2] [1] [1 1] [1 1] [0]
+(x,+(y,z)) = x + [0 1]y + [0 1]z + [2] >= x + [0 1]y + [0 1]z + [2] = +(+(x,y),z)
[1 2] [3] [1 1] [3]
f(g(f(x))) = [0 1]x + [2] >= [0 1]x + [2] = f(h(s(0()),x))
[2]
+(x,0()) = x + [1] >= x = x
[1 1] [2]
+(0(),y) = [0 1]y + [1] >= y = y
[1 3] [1 3] [3] [1 1] [1 1] [1]
f(g(h(x,y))) = [0 1]x + [0 1]y + [2] >= [0 1]x + [0 1]y + [2] = f(h(s(x),y))
[1 1] [1 2] [1 2] [1] [1 1] [1 2] [1 1] [1]
f(h(x,h(y,z))) = [0 1]x + [0 1]y + [0 1]z + [3] >= [0 1]x + [0 1]y + [0 1]z + [3] = f(h(+(x,y),z))
problem:
strict:
+(x,s(y)) -> s(+(x,y))
+(s(x),y) -> s(+(x,y))
weak:
+(x,+(y,z)) -> +(+(x,y),z)
f(g(f(x))) -> f(h(s(0()),x))
+(x,0()) -> x
+(0(),y) -> y
f(g(h(x,y))) -> f(h(s(x),y))
f(h(x,h(y,z))) -> f(h(+(x,y),z))
Matrix Interpretation Processor:
dimension: 2
max_matrix:
[1 2]
[0 1]
interpretation:
[1 1]
[h](x0, x1) = x0 + [0 1]x1,
[1 2] [1]
[g](x0) = [0 1]x0 + [2],
[1]
[f](x0) = x0 + [0],
[0]
[s](x0) = x0 + [2],
[1 1]
[+](x0, x1) = x0 + [0 1]x1,
[0]
[0] = [0]
orientation:
[1 1] [2] [1 1] [0]
+(x,s(y)) = x + [0 1]y + [2] >= x + [0 1]y + [2] = s(+(x,y))
[1 1] [0] [1 1] [0]
+(s(x),y) = x + [0 1]y + [2] >= x + [0 1]y + [2] = s(+(x,y))
[1 1] [1 2] [1 1] [1 1]
+(x,+(y,z)) = x + [0 1]y + [0 1]z >= x + [0 1]y + [0 1]z = +(+(x,y),z)
[1 2] [3] [1 1] [1]
f(g(f(x))) = [0 1]x + [2] >= [0 1]x + [2] = f(h(s(0()),x))
+(x,0()) = x >= x = x
[1 1]
+(0(),y) = [0 1]y >= y = y
[1 2] [1 3] [2] [1 1] [1]
f(g(h(x,y))) = [0 1]x + [0 1]y + [2] >= x + [0 1]y + [2] = f(h(s(x),y))
[1 1] [1 2] [1] [1 1] [1 1] [1]
f(h(x,h(y,z))) = x + [0 1]y + [0 1]z + [0] >= x + [0 1]y + [0 1]z + [0] = f(h(+(x,y),z))
problem:
strict:
+(s(x),y) -> s(+(x,y))
weak:
+(x,s(y)) -> s(+(x,y))
+(x,+(y,z)) -> +(+(x,y),z)
f(g(f(x))) -> f(h(s(0()),x))
+(x,0()) -> x
+(0(),y) -> y
f(g(h(x,y))) -> f(h(s(x),y))
f(h(x,h(y,z))) -> f(h(+(x,y),z))
Open
Tool IRC1
Execution Time | Unknown |
---|
Answer | MAYBE |
---|
Input | SK90 4.43 |
---|
stdout:
MAYBE
Tool IRC2
Execution Time | Unknown |
---|
Answer | TIMEOUT |
---|
Input | SK90 4.43 |
---|
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: innermost runtime-complexity with respect to
Rules:
{ +(x, 0()) -> x
, +(x, s(y)) -> s(+(x, y))
, +(0(), y) -> y
, +(s(x), y) -> s(+(x, y))
, +(x, +(y, z)) -> +(+(x, y), z)
, f(g(f(x))) -> f(h(s(0()), x))
, f(g(h(x, y))) -> f(h(s(x), y))
, f(h(x, h(y, z))) -> f(h(+(x, y), z))}
Proof Output:
Computation stopped due to timeout after 60.0 secondsTool RC1
Execution Time | Unknown |
---|
Answer | MAYBE |
---|
Input | SK90 4.43 |
---|
stdout:
MAYBE
Tool RC2
Execution Time | Unknown |
---|
Answer | TIMEOUT |
---|
Input | SK90 4.43 |
---|
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: runtime-complexity with respect to
Rules:
{ +(x, 0()) -> x
, +(x, s(y)) -> s(+(x, y))
, +(0(), y) -> y
, +(s(x), y) -> s(+(x, y))
, +(x, +(y, z)) -> +(+(x, y), z)
, f(g(f(x))) -> f(h(s(0()), x))
, f(g(h(x, y))) -> f(h(s(x), y))
, f(h(x, h(y, z))) -> f(h(+(x, y), z))}
Proof Output:
Computation stopped due to timeout after 60.0 secondsTool pair1rc
Execution Time | Unknown |
---|
Answer | TIMEOUT |
---|
Input | SK90 4.43 |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ +(x, 0()) -> x
, +(x, s(y)) -> s(+(x, y))
, +(0(), y) -> y
, +(s(x), y) -> s(+(x, y))
, +(x, +(y, z)) -> +(+(x, y), z)
, f(g(f(x))) -> f(h(s(0()), x))
, f(g(h(x, y))) -> f(h(s(x), y))
, f(h(x, h(y, z))) -> f(h(+(x, y), z))}
StartTerms: basic terms
Strategy: none
Certificate: TIMEOUT
Application of 'pair1 (timeout of 60.0 seconds)':
-------------------------------------------------
Computation stopped due to timeout after 60.0 seconds
Arrrr..Tool pair2rc
Execution Time | Unknown |
---|
Answer | TIMEOUT |
---|
Input | SK90 4.43 |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ +(x, 0()) -> x
, +(x, s(y)) -> s(+(x, y))
, +(0(), y) -> y
, +(s(x), y) -> s(+(x, y))
, +(x, +(y, z)) -> +(+(x, y), z)
, f(g(f(x))) -> f(h(s(0()), x))
, f(g(h(x, y))) -> f(h(s(x), y))
, f(h(x, h(y, z))) -> f(h(+(x, y), z))}
StartTerms: basic terms
Strategy: none
Certificate: TIMEOUT
Application of 'pair2 (timeout of 60.0 seconds)':
-------------------------------------------------
Computation stopped due to timeout after 60.0 seconds
Arrrr..Tool pair3irc
Execution Time | Unknown |
---|
Answer | TIMEOUT |
---|
Input | SK90 4.43 |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ +(x, 0()) -> x
, +(x, s(y)) -> s(+(x, y))
, +(0(), y) -> y
, +(s(x), y) -> s(+(x, y))
, +(x, +(y, z)) -> +(+(x, y), z)
, f(g(f(x))) -> f(h(s(0()), x))
, f(g(h(x, y))) -> f(h(s(x), y))
, f(h(x, h(y, z))) -> f(h(+(x, y), z))}
StartTerms: basic terms
Strategy: innermost
Certificate: TIMEOUT
Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
Computation stopped due to timeout after 60.0 seconds
Arrrr..Tool pair3rc
Execution Time | Unknown |
---|
Answer | TIMEOUT |
---|
Input | SK90 4.43 |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ +(x, 0()) -> x
, +(x, s(y)) -> s(+(x, y))
, +(0(), y) -> y
, +(s(x), y) -> s(+(x, y))
, +(x, +(y, z)) -> +(+(x, y), z)
, f(g(f(x))) -> f(h(s(0()), x))
, f(g(h(x, y))) -> f(h(s(x), y))
, f(h(x, h(y, z))) -> f(h(+(x, y), z))}
StartTerms: basic terms
Strategy: none
Certificate: TIMEOUT
Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
Computation stopped due to timeout after 60.0 seconds
Arrrr..Tool rc
Execution Time | Unknown |
---|
Answer | TIMEOUT |
---|
Input | SK90 4.43 |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ +(x, 0()) -> x
, +(x, s(y)) -> s(+(x, y))
, +(0(), y) -> y
, +(s(x), y) -> s(+(x, y))
, +(x, +(y, z)) -> +(+(x, y), z)
, f(g(f(x))) -> f(h(s(0()), x))
, f(g(h(x, y))) -> f(h(s(x), y))
, f(h(x, h(y, z))) -> f(h(+(x, y), z))}
StartTerms: basic terms
Strategy: none
Certificate: TIMEOUT
Application of 'rc (timeout of 60.0 seconds)':
----------------------------------------------
Computation stopped due to timeout after 60.0 seconds
Arrrr..Tool tup3irc
Execution Time | 63.132195ms |
---|
Answer | TIMEOUT |
---|
Input | SK90 4.43 |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ +(x, 0()) -> x
, +(x, s(y)) -> s(+(x, y))
, +(0(), y) -> y
, +(s(x), y) -> s(+(x, y))
, +(x, +(y, z)) -> +(+(x, y), z)
, f(g(f(x))) -> f(h(s(0()), x))
, f(g(h(x, y))) -> f(h(s(x), y))
, f(h(x, h(y, z))) -> f(h(+(x, y), z))}
StartTerms: basic terms
Strategy: innermost
Certificate: TIMEOUT
Application of 'tup3 (timeout of 60.0 seconds)':
------------------------------------------------
Computation stopped due to timeout after 60.0 seconds
Arrrr..