Tool Bounds
Execution Time | 60.029915ms |
---|
Answer | TIMEOUT |
---|
Input | SK90 4.08 |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ *(x, x) -> x
, *(x, *(y, z)) -> *(*(x, y), z)}
StartTerms: all
Strategy: none
Certificate: TIMEOUT
Proof:
Computation stopped due to timeout after 60.0 seconds.
Arrrr..Tool CDI
Execution Time | 8.0062866e-2ms |
---|
Answer | MAYBE |
---|
Input | SK90 4.08 |
---|
stdout:
MAYBE
Statistics:
Number of monomials: 84
Last formula building started for bound 3
Last SAT solving started for bound 3Tool EDA
Execution Time | 0.29052806ms |
---|
Answer | YES(?,O(n^2)) |
---|
Input | SK90 4.08 |
---|
stdout:
YES(?,O(n^2))
We consider the following Problem:
Strict Trs:
{ *(x, x) -> x
, *(x, *(y, z)) -> *(*(x, y), z)}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^2))
Proof:
We have the following EDA-non-satisfying matrix interpretation:
Interpretation Functions:
*(x1, x2) = [1 0] x1 + [1 1] x2 + [1]
[0 1] [0 1] [2]
Hurray, we answered YES(?,O(n^2))Tool IDA
Execution Time | 0.27557206ms |
---|
Answer | YES(?,O(n^2)) |
---|
Input | SK90 4.08 |
---|
stdout:
YES(?,O(n^2))
We consider the following Problem:
Strict Trs:
{ *(x, x) -> x
, *(x, *(y, z)) -> *(*(x, y), z)}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^2))
Proof:
We have the following EDA-non-satisfying and IDA(2)-non-satisfying matrix interpretation:
Interpretation Functions:
*(x1, x2) = [1 0] x1 + [1 1] x2 + [1]
[0 1] [0 1] [2]
Hurray, we answered YES(?,O(n^2))Tool TRI
Execution Time | 0.102108955ms |
---|
Answer | YES(?,O(n^2)) |
---|
Input | SK90 4.08 |
---|
stdout:
YES(?,O(n^2))
We consider the following Problem:
Strict Trs:
{ *(x, x) -> x
, *(x, *(y, z)) -> *(*(x, y), z)}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^2))
Proof:
We have the following triangular matrix interpretation:
Interpretation Functions:
*(x1, x2) = [1 0] x1 + [1 1] x2 + [1]
[0 1] [0 1] [2]
Hurray, we answered YES(?,O(n^2))Tool TRI2
Execution Time | 7.041597e-2ms |
---|
Answer | YES(?,O(n^2)) |
---|
Input | SK90 4.08 |
---|
stdout:
YES(?,O(n^2))
We consider the following Problem:
Strict Trs:
{ *(x, x) -> x
, *(x, *(y, z)) -> *(*(x, y), z)}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^2))
Proof:
We have the following triangular matrix interpretation:
Interpretation Functions:
*(x1, x2) = [1 0] x1 + [1 1] x2 + [1]
[0 1] [0 1] [2]
Hurray, we answered YES(?,O(n^2))