Tool CaT
Execution Time | Unknown |
---|
Answer | MAYBE |
---|
Input | SK90 4.10 |
---|
stdout:
MAYBE
Problem:
*(x,*(y,z)) -> *(otimes(x,y),z)
*(1(),y) -> y
*(+(x,y),z) -> oplus(*(x,z),*(y,z))
*(x,oplus(y,z)) -> oplus(*(x,y),*(x,z))
Proof:
OpenTool IRC1
Execution Time | Unknown |
---|
Answer | MAYBE |
---|
Input | SK90 4.10 |
---|
stdout:
MAYBE
Tool IRC2
Execution Time | Unknown |
---|
Answer | MAYBE |
---|
Input | SK90 4.10 |
---|
stdout:
MAYBE
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: MAYBE
Input Problem: innermost runtime-complexity with respect to
Rules:
{ *(x, *(y, z)) -> *(otimes(x, y), z)
, *(1(), y) -> y
, *(+(x, y), z) -> oplus(*(x, z), *(y, z))
, *(x, oplus(y, z)) -> oplus(*(x, y), *(x, z))}
Proof Output:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'wdg' failed due to the following reason:
Transformation Details:
-----------------------
We have computed the following set of weak (innermost) dependency pairs:
{ 1: *^#(x, *(y, z)) -> c_0(*^#(otimes(x, y), z))
, 2: *^#(1(), y) -> c_1()
, 3: *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))
, 4: *^#(x, oplus(y, z)) -> c_3(*^#(x, y), *^#(x, z))}
Following Dependency Graph (modulo SCCs) was computed. (Answers to
subproofs are indicated to the right.)
->{1,4,3} [ MAYBE ]
|
`->{2} [ NA ]
Sub-problems:
-------------
* Path {1,4,3}: MAYBE
-------------------
The usable rules of this path are empty.
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(*) = {}, Uargs(otimes) = {}, Uargs(+) = {},
Uargs(oplus) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1},
Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
*(x1, x2) = [3 3 3] x1 + [3 3 3] x2 + [0]
[3 3 3] [3 3 3] [0]
[3 3 3] [3 3 3] [0]
otimes(x1, x2) = [1 3 3] x1 + [1 3 3] x2 + [0]
[0 1 3] [0 1 3] [0]
[0 0 1] [0 0 1] [0]
1() = [0]
[0]
[0]
+(x1, x2) = [1 3 3] x1 + [1 3 3] x2 + [0]
[0 1 3] [0 1 3] [0]
[0 0 1] [0 0 1] [0]
oplus(x1, x2) = [1 3 3] x1 + [1 3 3] x2 + [0]
[0 1 3] [0 1 3] [0]
[0 0 1] [0 0 1] [0]
*^#(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
[3 3 3] [3 3 3] [0]
[3 3 3] [3 3 3] [0]
c_0(x1) = [1 0 0] x1 + [0]
[0 1 0] [0]
[0 0 1] [0]
c_1() = [0]
[0]
[0]
c_2(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
c_3(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 3'
--------------------------------------
Answer: MAYBE
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules:
{ *^#(x, *(y, z)) -> c_0(*^#(otimes(x, y), z))
, *^#(x, oplus(y, z)) -> c_3(*^#(x, y), *^#(x, z))
, *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
Weak Rules: {}
Proof Output:
The input cannot be shown compatible
* Path {1,4,3}->{2}: NA
---------------------
The usable rules of this path are empty.
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(*) = {}, Uargs(otimes) = {}, Uargs(+) = {},
Uargs(oplus) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1},
Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
*(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 0] [0 0 0] [0]
otimes(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 0] [0 0 0] [0]
1() = [0]
[0]
[0]
+(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 0] [0 0 0] [0]
oplus(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 0] [0 0 0] [0]
*^#(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 0] [0 0 0] [0]
c_0(x1) = [1 0 0] x1 + [0]
[0 1 0] [0]
[0 0 1] [0]
c_1() = [0]
[0]
[0]
c_2(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
c_3(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
We have not generated a proof for the resulting sub-problem.
2) 'wdg' failed due to the following reason:
Transformation Details:
-----------------------
We have computed the following set of weak (innermost) dependency pairs:
{ 1: *^#(x, *(y, z)) -> c_0(*^#(otimes(x, y), z))
, 2: *^#(1(), y) -> c_1()
, 3: *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))
, 4: *^#(x, oplus(y, z)) -> c_3(*^#(x, y), *^#(x, z))}
Following Dependency Graph (modulo SCCs) was computed. (Answers to
subproofs are indicated to the right.)
->{1,4,3} [ MAYBE ]
|
`->{2} [ NA ]
Sub-problems:
-------------
* Path {1,4,3}: MAYBE
-------------------
The usable rules of this path are empty.
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(*) = {}, Uargs(otimes) = {}, Uargs(+) = {},
Uargs(oplus) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1},
Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
*(x1, x2) = [3 3] x1 + [3 3] x2 + [0]
[3 3] [3 3] [0]
otimes(x1, x2) = [1 3] x1 + [1 3] x2 + [0]
[0 1] [0 1] [0]
1() = [0]
[0]
+(x1, x2) = [1 3] x1 + [1 3] x2 + [0]
[0 1] [0 1] [0]
oplus(x1, x2) = [1 3] x1 + [1 3] x2 + [0]
[0 1] [0 1] [0]
*^#(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[3 3] [3 3] [0]
c_0(x1) = [1 0] x1 + [0]
[0 1] [0]
c_1() = [0]
[0]
c_2(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [0]
c_3(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [0]
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 2'
--------------------------------------
Answer: MAYBE
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules:
{ *^#(x, *(y, z)) -> c_0(*^#(otimes(x, y), z))
, *^#(x, oplus(y, z)) -> c_3(*^#(x, y), *^#(x, z))
, *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
Weak Rules: {}
Proof Output:
The input cannot be shown compatible
* Path {1,4,3}->{2}: NA
---------------------
The usable rules of this path are empty.
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(*) = {}, Uargs(otimes) = {}, Uargs(+) = {},
Uargs(oplus) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1},
Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
*(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
otimes(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
1() = [0]
[0]
+(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
oplus(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
*^#(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
c_0(x1) = [1 0] x1 + [0]
[0 1] [0]
c_1() = [0]
[0]
c_2(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [0]
c_3(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [0]
We have not generated a proof for the resulting sub-problem.
3) 'wdg' failed due to the following reason:
Transformation Details:
-----------------------
We have computed the following set of weak (innermost) dependency pairs:
{ 1: *^#(x, *(y, z)) -> c_0(*^#(otimes(x, y), z))
, 2: *^#(1(), y) -> c_1()
, 3: *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))
, 4: *^#(x, oplus(y, z)) -> c_3(*^#(x, y), *^#(x, z))}
Following Dependency Graph (modulo SCCs) was computed. (Answers to
subproofs are indicated to the right.)
->{1,4,3} [ MAYBE ]
|
`->{2} [ NA ]
Sub-problems:
-------------
* Path {1,4,3}: MAYBE
-------------------
The usable rules of this path are empty.
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(*) = {}, Uargs(otimes) = {}, Uargs(+) = {},
Uargs(oplus) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1},
Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
*(x1, x2) = [3] x1 + [3] x2 + [0]
otimes(x1, x2) = [1] x1 + [1] x2 + [0]
1() = [0]
+(x1, x2) = [1] x1 + [1] x2 + [0]
oplus(x1, x2) = [1] x1 + [1] x2 + [0]
*^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_0(x1) = [1] x1 + [0]
c_1() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [0]
c_3(x1, x2) = [1] x1 + [1] x2 + [0]
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 1'
--------------------------------------
Answer: MAYBE
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules:
{ *^#(x, *(y, z)) -> c_0(*^#(otimes(x, y), z))
, *^#(x, oplus(y, z)) -> c_3(*^#(x, y), *^#(x, z))
, *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
Weak Rules: {}
Proof Output:
The input cannot be shown compatible
* Path {1,4,3}->{2}: NA
---------------------
The usable rules of this path are empty.
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(*) = {}, Uargs(otimes) = {}, Uargs(+) = {},
Uargs(oplus) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1},
Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
*(x1, x2) = [0] x1 + [0] x2 + [0]
otimes(x1, x2) = [0] x1 + [0] x2 + [0]
1() = [0]
+(x1, x2) = [0] x1 + [0] x2 + [0]
oplus(x1, x2) = [0] x1 + [0] x2 + [0]
*^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_0(x1) = [1] x1 + [0]
c_1() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [0]
c_3(x1, x2) = [1] x1 + [1] x2 + [0]
We have not generated a proof for the resulting sub-problem.
4) 'matrix-interpretation of dimension 1' failed due to the following reason:
The input cannot be shown compatible
5) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
match-boundness of the problem could not be verified.
6) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason:
match-boundness of the problem could not be verified.
Tool RC1
Execution Time | Unknown |
---|
Answer | MAYBE |
---|
Input | SK90 4.10 |
---|
stdout:
MAYBE
Tool RC2
Execution Time | Unknown |
---|
Answer | MAYBE |
---|
Input | SK90 4.10 |
---|
stdout:
MAYBE
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: MAYBE
Input Problem: runtime-complexity with respect to
Rules:
{ *(x, *(y, z)) -> *(otimes(x, y), z)
, *(1(), y) -> y
, *(+(x, y), z) -> oplus(*(x, z), *(y, z))
, *(x, oplus(y, z)) -> oplus(*(x, y), *(x, z))}
Proof Output:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'wdg' failed due to the following reason:
Transformation Details:
-----------------------
We have computed the following set of weak (innermost) dependency pairs:
{ 1: *^#(x, *(y, z)) -> c_0(*^#(otimes(x, y), z))
, 2: *^#(1(), y) -> c_1(y)
, 3: *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))
, 4: *^#(x, oplus(y, z)) -> c_3(*^#(x, y), *^#(x, z))}
Following Dependency Graph (modulo SCCs) was computed. (Answers to
subproofs are indicated to the right.)
->{1,4,3} [ NA ]
|
`->{2} [ MAYBE ]
Sub-problems:
-------------
* Path {1,4,3}: NA
----------------
The usable rules of this path are empty.
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(*) = {}, Uargs(otimes) = {}, Uargs(+) = {},
Uargs(oplus) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1},
Uargs(c_1) = {}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
*(x1, x2) = [3 3 3] x1 + [3 3 3] x2 + [0]
[3 3 3] [3 3 3] [0]
[3 3 3] [3 3 3] [0]
otimes(x1, x2) = [1 3 3] x1 + [1 3 3] x2 + [0]
[0 1 3] [0 1 3] [0]
[0 0 1] [0 0 1] [0]
1() = [0]
[0]
[0]
+(x1, x2) = [1 3 3] x1 + [1 3 3] x2 + [0]
[0 1 3] [0 1 3] [0]
[0 0 1] [0 0 1] [0]
oplus(x1, x2) = [1 3 3] x1 + [1 3 3] x2 + [0]
[0 1 3] [0 1 3] [0]
[0 0 1] [0 0 1] [0]
*^#(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
[3 3 3] [3 3 3] [0]
[3 3 3] [3 3 3] [0]
c_0(x1) = [1 0 0] x1 + [0]
[0 1 0] [0]
[0 0 1] [0]
c_1(x1) = [0 0 0] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
c_2(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
c_3(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
We have not generated a proof for the resulting sub-problem.
* Path {1,4,3}->{2}: MAYBE
------------------------
The usable rules of this path are empty.
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(*) = {}, Uargs(otimes) = {}, Uargs(+) = {},
Uargs(oplus) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1},
Uargs(c_1) = {}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
*(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 0] [0 0 0] [0]
otimes(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 0] [0 0 0] [0]
1() = [0]
[0]
[0]
+(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 0] [0 0 0] [0]
oplus(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 0] [0 0 0] [0]
*^#(x1, x2) = [0 0 0] x1 + [3 3 3] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 0] [0 0 0] [0]
c_0(x1) = [1 0 0] x1 + [0]
[0 1 0] [0]
[0 0 1] [0]
c_1(x1) = [1 1 1] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
c_2(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
c_3(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 3'
--------------------------------------
Answer: MAYBE
Input Problem: DP runtime-complexity with respect to
Strict Rules: {*^#(1(), y) -> c_1(y)}
Weak Rules:
{ *^#(x, *(y, z)) -> c_0(*^#(otimes(x, y), z))
, *^#(x, oplus(y, z)) -> c_3(*^#(x, y), *^#(x, z))
, *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
Proof Output:
The input cannot be shown compatible
2) 'wdg' failed due to the following reason:
Transformation Details:
-----------------------
We have computed the following set of weak (innermost) dependency pairs:
{ 1: *^#(x, *(y, z)) -> c_0(*^#(otimes(x, y), z))
, 2: *^#(1(), y) -> c_1(y)
, 3: *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))
, 4: *^#(x, oplus(y, z)) -> c_3(*^#(x, y), *^#(x, z))}
Following Dependency Graph (modulo SCCs) was computed. (Answers to
subproofs are indicated to the right.)
->{1,4,3} [ MAYBE ]
|
`->{2} [ NA ]
Sub-problems:
-------------
* Path {1,4,3}: MAYBE
-------------------
The usable rules of this path are empty.
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(*) = {}, Uargs(otimes) = {}, Uargs(+) = {},
Uargs(oplus) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1},
Uargs(c_1) = {}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
*(x1, x2) = [3 3] x1 + [3 3] x2 + [0]
[3 3] [3 3] [0]
otimes(x1, x2) = [1 3] x1 + [1 3] x2 + [0]
[0 1] [0 1] [0]
1() = [0]
[0]
+(x1, x2) = [1 3] x1 + [1 3] x2 + [0]
[0 1] [0 1] [0]
oplus(x1, x2) = [1 3] x1 + [1 3] x2 + [0]
[0 1] [0 1] [0]
*^#(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[3 3] [3 3] [0]
c_0(x1) = [1 0] x1 + [0]
[0 1] [0]
c_1(x1) = [0 0] x1 + [0]
[0 0] [0]
c_2(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [0]
c_3(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [0]
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 2'
--------------------------------------
Answer: MAYBE
Input Problem: DP runtime-complexity with respect to
Strict Rules:
{ *^#(x, *(y, z)) -> c_0(*^#(otimes(x, y), z))
, *^#(x, oplus(y, z)) -> c_3(*^#(x, y), *^#(x, z))
, *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
Weak Rules: {}
Proof Output:
The input cannot be shown compatible
* Path {1,4,3}->{2}: NA
---------------------
The usable rules of this path are empty.
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(*) = {}, Uargs(otimes) = {}, Uargs(+) = {},
Uargs(oplus) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1},
Uargs(c_1) = {}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
*(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
otimes(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
1() = [0]
[0]
+(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
oplus(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
*^#(x1, x2) = [0 0] x1 + [3 3] x2 + [0]
[0 0] [0 0] [0]
c_0(x1) = [1 0] x1 + [0]
[0 1] [0]
c_1(x1) = [1 1] x1 + [0]
[0 0] [0]
c_2(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [0]
c_3(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [0]
We have not generated a proof for the resulting sub-problem.
3) 'wdg' failed due to the following reason:
Transformation Details:
-----------------------
We have computed the following set of weak (innermost) dependency pairs:
{ 1: *^#(x, *(y, z)) -> c_0(*^#(otimes(x, y), z))
, 2: *^#(1(), y) -> c_1(y)
, 3: *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))
, 4: *^#(x, oplus(y, z)) -> c_3(*^#(x, y), *^#(x, z))}
Following Dependency Graph (modulo SCCs) was computed. (Answers to
subproofs are indicated to the right.)
->{1,4,3} [ MAYBE ]
|
`->{2} [ NA ]
Sub-problems:
-------------
* Path {1,4,3}: MAYBE
-------------------
The usable rules of this path are empty.
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(*) = {}, Uargs(otimes) = {}, Uargs(+) = {},
Uargs(oplus) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1},
Uargs(c_1) = {}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
*(x1, x2) = [3] x1 + [3] x2 + [0]
otimes(x1, x2) = [1] x1 + [1] x2 + [0]
1() = [0]
+(x1, x2) = [1] x1 + [1] x2 + [0]
oplus(x1, x2) = [1] x1 + [1] x2 + [0]
*^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_0(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [0]
c_3(x1, x2) = [1] x1 + [1] x2 + [0]
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 1'
--------------------------------------
Answer: MAYBE
Input Problem: DP runtime-complexity with respect to
Strict Rules:
{ *^#(x, *(y, z)) -> c_0(*^#(otimes(x, y), z))
, *^#(x, oplus(y, z)) -> c_3(*^#(x, y), *^#(x, z))
, *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
Weak Rules: {}
Proof Output:
The input cannot be shown compatible
* Path {1,4,3}->{2}: NA
---------------------
The usable rules of this path are empty.
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(*) = {}, Uargs(otimes) = {}, Uargs(+) = {},
Uargs(oplus) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1},
Uargs(c_1) = {}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
*(x1, x2) = [0] x1 + [0] x2 + [0]
otimes(x1, x2) = [0] x1 + [0] x2 + [0]
1() = [0]
+(x1, x2) = [0] x1 + [0] x2 + [0]
oplus(x1, x2) = [0] x1 + [0] x2 + [0]
*^#(x1, x2) = [0] x1 + [3] x2 + [0]
c_0(x1) = [1] x1 + [0]
c_1(x1) = [1] x1 + [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [0]
c_3(x1, x2) = [1] x1 + [1] x2 + [0]
We have not generated a proof for the resulting sub-problem.
4) 'matrix-interpretation of dimension 1' failed due to the following reason:
The input cannot be shown compatible
5) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
match-boundness of the problem could not be verified.
6) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason:
match-boundness of the problem could not be verified.
Tool pair1rc
Execution Time | Unknown |
---|
Answer | TIMEOUT |
---|
Input | SK90 4.10 |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ *(x, *(y, z)) -> *(otimes(x, y), z)
, *(1(), y) -> y
, *(+(x, y), z) -> oplus(*(x, z), *(y, z))
, *(x, oplus(y, z)) -> oplus(*(x, y), *(x, 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.10 |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ *(x, *(y, z)) -> *(otimes(x, y), z)
, *(1(), y) -> y
, *(+(x, y), z) -> oplus(*(x, z), *(y, z))
, *(x, oplus(y, z)) -> oplus(*(x, y), *(x, 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.10 |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ *(x, *(y, z)) -> *(otimes(x, y), z)
, *(1(), y) -> y
, *(+(x, y), z) -> oplus(*(x, z), *(y, z))
, *(x, oplus(y, z)) -> oplus(*(x, y), *(x, 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.10 |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ *(x, *(y, z)) -> *(otimes(x, y), z)
, *(1(), y) -> y
, *(+(x, y), z) -> oplus(*(x, z), *(y, z))
, *(x, oplus(y, z)) -> oplus(*(x, y), *(x, 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 | YES(?,O(n^1)) |
---|
Input | SK90 4.10 |
---|
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ *(x, *(y, z)) -> *(otimes(x, y), z)
, *(1(), y) -> y
, *(+(x, y), z) -> oplus(*(x, z), *(y, z))
, *(x, oplus(y, z)) -> oplus(*(x, y), *(x, z))}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
Application of 'rc (timeout of 60.0 seconds)':
----------------------------------------------
'dp' proved the goal fastest:
We have computed the following dependency pairs
Strict Dependency Pairs:
{ *^#(x, *(y, z)) -> c_1(*^#(otimes(x, y), z))
, *^#(1(), y) -> c_2(y)
, *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z))
, *^#(x, oplus(y, z)) -> c_4(*^#(x, y), *^#(x, z))}
We consider the following Problem:
Strict DPs:
{ *^#(x, *(y, z)) -> c_1(*^#(otimes(x, y), z))
, *^#(1(), y) -> c_2(y)
, *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z))
, *^#(x, oplus(y, z)) -> c_4(*^#(x, y), *^#(x, z))}
Strict Trs:
{ *(x, *(y, z)) -> *(otimes(x, y), z)
, *(1(), y) -> y
, *(+(x, y), z) -> oplus(*(x, z), *(y, z))
, *(x, oplus(y, z)) -> oplus(*(x, y), *(x, z))}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
Application of 'usablerules':
-----------------------------
No rule is usable.
We consider the following Problem:
Strict DPs:
{ *^#(x, *(y, z)) -> c_1(*^#(otimes(x, y), z))
, *^#(1(), y) -> c_2(y)
, *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z))
, *^#(x, oplus(y, z)) -> c_4(*^#(x, y), *^#(x, z))}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
Application of 'Fastest':
-------------------------
'pathanalysis' proved the goal fastest:
We use following congruence DG for path analysis
->{1,4,3} [ YES(?,O(n^1)) ]
|
`->{2} [ YES(O(1),O(1)) ]
Here rules are as follows:
{ 1: *^#(x, *(y, z)) -> c_1(*^#(otimes(x, y), z))
, 2: *^#(1(), y) -> c_2(y)
, 3: *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z))
, 4: *^#(x, oplus(y, z)) -> c_4(*^#(x, y), *^#(x, z))}
* Path {1,4,3}: YES(?,O(n^1))
---------------------------
We consider the following Problem:
Strict DPs:
{ *^#(x, *(y, z)) -> c_1(*^#(otimes(x, y), z))
, *^#(x, oplus(y, z)) -> c_4(*^#(x, y), *^#(x, z))
, *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z))}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
No dependency-pair could be removed
We apply the transformation 'weightgap of dimension Nat 2, maximal degree 1, cbits 4 <> ...' on the resulting sub-problems:
Sub-problem 1:
--------------
We consider the problem
Strict DPs:
{ *^#(x, *(y, z)) -> c_1(*^#(otimes(x, y), z))
, *^#(x, oplus(y, z)) -> c_4(*^#(x, y), *^#(x, z))
, *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z))}
StartTerms: basic terms
Strategy: none
We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Strict DPs:
{ *^#(x, *(y, z)) -> c_1(*^#(otimes(x, y), z))
, *^#(x, oplus(y, z)) -> c_4(*^#(x, y), *^#(x, z))
, *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z))}
StartTerms: basic terms
Strategy: none
We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
Strict DPs:
{ *^#(x, *(y, z)) -> c_1(*^#(otimes(x, y), z))
, *^#(x, oplus(y, z)) -> c_4(*^#(x, y), *^#(x, z))
, *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z))}
StartTerms: basic terms
Strategy: none
The weightgap principle does not apply
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{ *^#(x, *(y, z)) -> c_1(*^#(otimes(x, y), z))
, *^#(x, oplus(y, z)) -> c_4(*^#(x, y), *^#(x, z))
, *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z))}
StartTerms: basic terms
Strategy: none
1) 'Fastest' proved the goal fastest:
'Bounds with perSymbol-enrichment and initial automaton 'match' (timeout of 5.0 seconds)' proved the goal fastest:
The problem is match-bounded by 0.
The enriched problem is compatible with the following automaton:
{}
* Path {1,4,3}->{2}: YES(O(1),O(1))
---------------------------------
We consider the following Problem:
Strict DPs: {*^#(1(), y) -> c_2(y)}
Weak DPs:
{ *^#(x, *(y, z)) -> c_1(*^#(otimes(x, y), z))
, *^#(x, oplus(y, z)) -> c_4(*^#(x, y), *^#(x, z))
, *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z))}
StartTerms: basic terms
Strategy: none
Certificate: YES(O(1),O(1))
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
We consider the the dependency-graph
1: *^#(1(), y) -> c_2(y)
2: *^#(x, *(y, z)) -> c_1(*^#(otimes(x, y), z))
--> *^#(x, oplus(y, z)) -> c_4(*^#(x, y), *^#(x, z)): 3
--> *^#(x, *(y, z)) -> c_1(*^#(otimes(x, y), z)): 2
3: *^#(x, oplus(y, z)) -> c_4(*^#(x, y), *^#(x, z))
--> *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z)): 4
--> *^#(x, oplus(y, z)) -> c_4(*^#(x, y), *^#(x, z)): 3
--> *^#(x, *(y, z)) -> c_1(*^#(otimes(x, y), z)): 2
--> *^#(1(), y) -> c_2(y): 1
4: *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z))
--> *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z)): 4
--> *^#(x, oplus(y, z)) -> c_4(*^#(x, y), *^#(x, z)): 3
--> *^#(x, *(y, z)) -> c_1(*^#(otimes(x, y), z)): 2
--> *^#(1(), y) -> c_2(y): 1
together with the congruence-graph
->{2,4,3} Weak SCC
|
`->{1} Noncyclic, trivial, SCC
Here rules are as follows:
{ 1: *^#(1(), y) -> c_2(y)
, 2: *^#(x, *(y, z)) -> c_1(*^#(otimes(x, y), z))
, 3: *^#(x, oplus(y, z)) -> c_4(*^#(x, y), *^#(x, z))
, 4: *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: *^#(x, *(y, z)) -> c_1(*^#(otimes(x, y), z))
, 4: *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z))
, 3: *^#(x, oplus(y, z)) -> c_4(*^#(x, y), *^#(x, z))
, 1: *^#(1(), y) -> c_2(y)}
We consider the following Problem:
StartTerms: basic terms
Strategy: none
Certificate: YES(O(1),O(1))
Application of 'simpDPRHS >>> ...':
-----------------------------------
No rule was simplified
We apply the transformation 'usablerules' on the resulting sub-problems:
Sub-problem 1:
--------------
We consider the problem
StartTerms: basic terms
Strategy: none
The input problem is not a DP-problem.
We abort the transformation and continue with the subprocessor on the problem
StartTerms: basic terms
Strategy: none
1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
All strict components are empty, nothing to further orient
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
StartTerms: basic terms
Strategy: none
We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
All strict components are empty, nothing to further orient
We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
StartTerms: basic terms
Strategy: none
All strict components are empty, nothing to further orient
We abort the transformation and continue with the subprocessor on the problem
StartTerms: basic terms
Strategy: none
1) No dependency-pair could be removed
We apply the transformation 'weightgap of dimension Nat 2, maximal degree 1, cbits 4 <> ...' on the resulting sub-problems:
Sub-problem 1:
--------------
We consider the problem
StartTerms: basic terms
Strategy: none
We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
All strict components are empty, nothing to further orient
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
StartTerms: basic terms
Strategy: none
We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
All strict components are empty, nothing to further orient
We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
StartTerms: basic terms
Strategy: none
All strict components are empty, nothing to further orient
We abort the transformation and continue with the subprocessor on the problem
StartTerms: basic terms
Strategy: none
1) 'Sequentially' proved the goal fastest:
'empty' succeeded:
Empty rules are trivially bounded
Hurray, we answered YES(?,O(n^1))Tool tup3irc
Execution Time | 62.290443ms |
---|
Answer | TIMEOUT |
---|
Input | SK90 4.10 |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ *(x, *(y, z)) -> *(otimes(x, y), z)
, *(1(), y) -> y
, *(+(x, y), z) -> oplus(*(x, z), *(y, z))
, *(x, oplus(y, z)) -> oplus(*(x, y), *(x, 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..