Tool CaT
stdout:
MAYBE
Problem:
f(s(x)) -> s(f(f(x)))
f(x) -> c(x,x)
Proof:
OpenTool IRC1
stdout:
MAYBE
Tool IRC2
stdout:
MAYBE
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: MAYBE
Input Problem: innermost runtime-complexity with respect to
Rules:
{ f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
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: f^#(s(x)) -> c_0(f^#(f(x)))
, 2: f^#(x) -> c_1()}
Following Dependency Graph (modulo SCCs) was computed. (Answers to
subproofs are indicated to the right.)
->{1} [ inherited ]
|
`->{2} [ MAYBE ]
Sub-problems:
-------------
* Path {1}: inherited
-------------------
This path is subsumed by the proof of path {1}->{2}.
* Path {1}->{2}: MAYBE
--------------------
The usable rules for this path are:
{ f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
The weight gap principle does not apply:
The input cannot be shown compatible
Complexity induced by the adequate RMI: MAYBE
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 3'
--------------------------------------
Answer: MAYBE
Input Problem: innermost runtime-complexity with respect to
Rules:
{ f^#(s(x)) -> c_0(f^#(f(x)))
, f^#(x) -> c_1()
, f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
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: f^#(s(x)) -> c_0(f^#(f(x)))
, 2: f^#(x) -> c_1()}
Following Dependency Graph (modulo SCCs) was computed. (Answers to
subproofs are indicated to the right.)
->{1} [ inherited ]
|
`->{2} [ MAYBE ]
Sub-problems:
-------------
* Path {1}: inherited
-------------------
This path is subsumed by the proof of path {1}->{2}.
* Path {1}->{2}: MAYBE
--------------------
The usable rules for this path are:
{ f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
The weight gap principle does not apply:
The input cannot be shown compatible
Complexity induced by the adequate RMI: MAYBE
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 2'
--------------------------------------
Answer: MAYBE
Input Problem: innermost runtime-complexity with respect to
Rules:
{ f^#(s(x)) -> c_0(f^#(f(x)))
, f^#(x) -> c_1()
, f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
Proof Output:
The input cannot be shown compatible
3) 'wdg' failed due to the following reason:
Transformation Details:
-----------------------
We have computed the following set of weak (innermost) dependency pairs:
{ 1: f^#(s(x)) -> c_0(f^#(f(x)))
, 2: f^#(x) -> c_1()}
Following Dependency Graph (modulo SCCs) was computed. (Answers to
subproofs are indicated to the right.)
->{1} [ inherited ]
|
`->{2} [ MAYBE ]
Sub-problems:
-------------
* Path {1}: inherited
-------------------
This path is subsumed by the proof of path {1}->{2}.
* Path {1}->{2}: MAYBE
--------------------
The usable rules for this path are:
{ f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
The weight gap principle does not apply:
The input cannot be shown compatible
Complexity induced by the adequate RMI: MAYBE
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 1'
--------------------------------------
Answer: MAYBE
Input Problem: innermost runtime-complexity with respect to
Rules:
{ f^#(s(x)) -> c_0(f^#(f(x)))
, f^#(x) -> c_1()
, f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
Proof Output:
The input cannot be shown compatible
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
stdout:
MAYBE
Tool RC2
stdout:
MAYBE
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: MAYBE
Input Problem: runtime-complexity with respect to
Rules:
{ f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
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: f^#(s(x)) -> c_0(f^#(f(x)))
, 2: f^#(x) -> c_1(x, x)}
Following Dependency Graph (modulo SCCs) was computed. (Answers to
subproofs are indicated to the right.)
->{1} [ inherited ]
|
`->{2} [ MAYBE ]
Sub-problems:
-------------
* Path {1}: inherited
-------------------
This path is subsumed by the proof of path {1}->{2}.
* Path {1}->{2}: MAYBE
--------------------
The usable rules for this path are:
{ f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
The weight gap principle does not apply:
The input cannot be shown compatible
Complexity induced by the adequate RMI: MAYBE
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 3'
--------------------------------------
Answer: MAYBE
Input Problem: runtime-complexity with respect to
Rules:
{ f^#(s(x)) -> c_0(f^#(f(x)))
, f^#(x) -> c_1(x, x)
, f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
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: f^#(s(x)) -> c_0(f^#(f(x)))
, 2: f^#(x) -> c_1(x, x)}
Following Dependency Graph (modulo SCCs) was computed. (Answers to
subproofs are indicated to the right.)
->{1} [ inherited ]
|
`->{2} [ MAYBE ]
Sub-problems:
-------------
* Path {1}: inherited
-------------------
This path is subsumed by the proof of path {1}->{2}.
* Path {1}->{2}: MAYBE
--------------------
The usable rules for this path are:
{ f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
The weight gap principle does not apply:
The input cannot be shown compatible
Complexity induced by the adequate RMI: MAYBE
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 2'
--------------------------------------
Answer: MAYBE
Input Problem: runtime-complexity with respect to
Rules:
{ f^#(s(x)) -> c_0(f^#(f(x)))
, f^#(x) -> c_1(x, x)
, f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
Proof Output:
The input cannot be shown compatible
3) 'wdg' failed due to the following reason:
Transformation Details:
-----------------------
We have computed the following set of weak (innermost) dependency pairs:
{ 1: f^#(s(x)) -> c_0(f^#(f(x)))
, 2: f^#(x) -> c_1(x, x)}
Following Dependency Graph (modulo SCCs) was computed. (Answers to
subproofs are indicated to the right.)
->{1} [ inherited ]
|
`->{2} [ MAYBE ]
Sub-problems:
-------------
* Path {1}: inherited
-------------------
This path is subsumed by the proof of path {1}->{2}.
* Path {1}->{2}: MAYBE
--------------------
The usable rules for this path are:
{ f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
The weight gap principle does not apply:
The input cannot be shown compatible
Complexity induced by the adequate RMI: MAYBE
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 1'
--------------------------------------
Answer: MAYBE
Input Problem: runtime-complexity with respect to
Rules:
{ f^#(s(x)) -> c_0(f^#(f(x)))
, f^#(x) -> c_1(x, x)
, f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
Proof Output:
The input cannot be shown compatible
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
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
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
stdout:
MAYBE
We consider the following Problem:
Strict Trs:
{ f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'pair2 (timeout of 60.0 seconds)':
-------------------------------------------------
The processor is not applicable, reason is:
Input problem is not restricted to innermost rewriting
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{ f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
StartTerms: basic terms
Strategy: none
1) None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'dp' failed due to the following reason:
We have computed the following dependency pairs
Strict Dependency Pairs:
{ f^#(s(x)) -> c_1(f^#(f(x)))
, f^#(x) -> c_2(x, x)}
We consider the following Problem:
Strict DPs:
{ f^#(s(x)) -> c_1(f^#(f(x)))
, f^#(x) -> c_2(x, x)}
Strict Trs:
{ f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'Fastest':
-------------------------
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'pathanalysis' failed due to the following reason:
We use following congruence DG for path analysis
->{1} [ MAYBE ]
|
`->{2} [ ? ]
Here rules are as follows:
{ 1: f^#(s(x)) -> c_1(f^#(f(x)))
, 2: f^#(x) -> c_2(x, x)}
* Path {1}: MAYBE
---------------
We consider the following Problem:
Strict DPs: {f^#(s(x)) -> c_1(f^#(f(x)))}
Strict Trs:
{ f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the strict component of the
input problem is not empty
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: {f^#(s(x)) -> c_1(f^#(f(x)))}
Strict Trs:
{ f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
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: {f^#(s(x)) -> c_1(f^#(f(x)))}
Strict Trs:
{ f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
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: {f^#(s(x)) -> c_1(f^#(f(x)))}
Strict Trs:
{ f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
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: {f^#(s(x)) -> c_1(f^#(f(x)))}
Strict Trs:
{ f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
StartTerms: basic terms
Strategy: none
1) None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Sequentially' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'compose (statically using 'split first congruence from CWD', multiplication)' failed due to the following reason:
Compose is inapplicable since some strict rule is size increasing
No subproblems were generated.
* Path {1}->{2}: ?
----------------
CANNOT find proof of path {1}->{2}. Propably computation has been aborted since some other path cannot be solved.
2) 'Sequentially' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Sequentially' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
match-boundness of the problem could not be verified.
2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason:
match-boundness of the problem could not be verified.
Arrrr..Tool pair3irc
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
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
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
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 tup3irc
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ f(s(x)) -> s(f(f(x)))
, f(x) -> c(x, x)}
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..