Tool CaT
| Execution Time | Unknown |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | AG01 3.33 |
|---|
stdout:
YES(?,O(n^1))
Problem:
p(f(f(x))) -> q(f(g(x)))
p(g(g(x))) -> q(g(f(x)))
q(f(f(x))) -> p(f(g(x)))
q(g(g(x))) -> p(g(f(x)))
Proof:
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {4,3}
transitions:
p1(27) -> 28*
g1(15) -> 16*
g1(5) -> 6*
g1(18) -> 19*
f1(25) -> 26*
f1(17) -> 18*
f1(6) -> 7*
q1(7) -> 8*
p0(2) -> 3*
p0(1) -> 3*
f0(2) -> 1*
f0(1) -> 1*
q0(2) -> 4*
q0(1) -> 4*
g0(2) -> 2*
g0(1) -> 2*
1 -> 25,15
2 -> 17,5
7 -> 27*
8 -> 3*
16 -> 6*
19 -> 7*
26 -> 18*
28 -> 4*
problem:
QedTool IRC1
| Execution Time | Unknown |
|---|
| Answer | YES(?,O(1)) |
|---|
| Input | AG01 3.33 |
|---|
stdout:
YES(?,O(1))
Tool IRC2
| Execution Time | Unknown |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | AG01 3.33 |
|---|
stdout:
YES(?,O(n^1))
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
Proof Output:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with minimal-enrichment and initial automaton 'match''
--------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
Proof Output:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ p_0(2) -> 1
, p_1(3) -> 1
, f_0(2) -> 2
, f_1(2) -> 5
, f_1(4) -> 3
, q_0(2) -> 1
, q_1(3) -> 1
, g_0(2) -> 2
, g_1(2) -> 4
, g_1(5) -> 3}Tool RC1
| Execution Time | Unknown |
|---|
| Answer | YES(?,O(1)) |
|---|
| Input | AG01 3.33 |
|---|
stdout:
YES(?,O(1))
Tool RC2
| Execution Time | Unknown |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | AG01 3.33 |
|---|
stdout:
YES(?,O(n^1))
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
Proof Output:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with minimal-enrichment and initial automaton 'match''
--------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
Proof Output:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ p_0(2) -> 1
, p_1(3) -> 1
, f_0(2) -> 2
, f_1(2) -> 5
, f_1(4) -> 3
, q_0(2) -> 1
, q_1(3) -> 1
, g_0(2) -> 2
, g_1(2) -> 4
, g_1(5) -> 3}Tool pair1rc
| Execution Time | Unknown |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | AG01 3.33 |
|---|
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
Application of 'pair1 (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:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
StartTerms: basic terms
Strategy: none
1) 'Fastest' proved the goal fastest:
'Fastest' proved the goal fastest:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the goal fastest:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ p_0(2) -> 1
, p_1(3) -> 1
, f_0(2) -> 2
, f_1(2) -> 5
, f_1(4) -> 3
, q_0(2) -> 1
, q_1(3) -> 1
, g_0(2) -> 2
, g_1(2) -> 4
, g_1(5) -> 3}
Hurray, we answered YES(?,O(n^1))Tool pair2rc
| Execution Time | Unknown |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | AG01 3.33 |
|---|
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
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:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
StartTerms: basic terms
Strategy: none
1) 'Fastest' proved the goal fastest:
'Fastest' proved the goal fastest:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the goal fastest:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ p_0(2) -> 1
, p_1(3) -> 1
, f_0(2) -> 2
, f_1(2) -> 5
, f_1(4) -> 3
, q_0(2) -> 1
, q_1(3) -> 1
, g_0(2) -> 2
, g_1(2) -> 4
, g_1(5) -> 3}
Hurray, we answered YES(?,O(n^1))Tool pair3irc
| Execution Time | Unknown |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | AG01 3.33 |
|---|
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
The input problem contains no overlaps that give rise to inapplicable rules.
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
StartTerms: basic terms
Strategy: innermost
1) 'Fastest' proved the goal fastest:
'Fastest' proved the goal fastest:
'Bounds with perSymbol-enrichment and initial automaton 'match'' proved the goal fastest:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ p_0(2) -> 1
, p_0(4) -> 1
, p_1(5) -> 3
, f_0(2) -> 2
, f_0(4) -> 2
, f_1(2) -> 7
, f_1(4) -> 7
, f_1(6) -> 5
, q_0(2) -> 3
, q_0(4) -> 3
, q_1(5) -> 1
, g_0(2) -> 4
, g_0(4) -> 4
, g_1(2) -> 6
, g_1(4) -> 6
, g_1(7) -> 5}
Hurray, we answered YES(?,O(n^1))Tool pair3rc
| Execution Time | Unknown |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | AG01 3.33 |
|---|
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
Application of 'pair3 (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:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
StartTerms: basic terms
Strategy: none
1) 'Fastest' proved the goal fastest:
'Fastest' proved the goal fastest:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the goal fastest:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ p_0(2) -> 1
, p_1(3) -> 1
, f_0(2) -> 2
, f_1(2) -> 5
, f_1(4) -> 3
, q_0(2) -> 1
, q_1(3) -> 1
, g_0(2) -> 2
, g_1(2) -> 4
, g_1(5) -> 3}
Hurray, we answered YES(?,O(n^1))Tool rc
| Execution Time | Unknown |
|---|
| Answer | YES(O(1),O(1)) |
|---|
| Input | AG01 3.33 |
|---|
stdout:
YES(O(1),O(1))
We consider the following Problem:
Strict Trs:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
StartTerms: basic terms
Strategy: none
Certificate: YES(O(1),O(1))
Application of 'rc (timeout of 60.0 seconds)':
----------------------------------------------
'dp' proved the goal fastest:
We have computed the following dependency pairs
Strict Dependency Pairs:
{ p^#(f(f(x))) -> c_1(q^#(f(g(x))))
, p^#(g(g(x))) -> c_2(q^#(g(f(x))))
, q^#(f(f(x))) -> c_3(p^#(f(g(x))))
, q^#(g(g(x))) -> c_4(p^#(g(f(x))))}
We consider the following Problem:
Strict DPs:
{ p^#(f(f(x))) -> c_1(q^#(f(g(x))))
, p^#(g(g(x))) -> c_2(q^#(g(f(x))))
, q^#(f(f(x))) -> c_3(p^#(f(g(x))))
, q^#(g(g(x))) -> c_4(p^#(g(f(x))))}
Strict Trs:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
StartTerms: basic terms
Strategy: none
Certificate: YES(O(1),O(1))
Application of 'usablerules':
-----------------------------
No rule is usable.
We consider the following Problem:
Strict DPs:
{ p^#(f(f(x))) -> c_1(q^#(f(g(x))))
, p^#(g(g(x))) -> c_2(q^#(g(f(x))))
, q^#(f(f(x))) -> c_3(p^#(f(g(x))))
, q^#(g(g(x))) -> c_4(p^#(g(f(x))))}
StartTerms: basic terms
Strategy: none
Certificate: YES(O(1),O(1))
Application of 'Fastest':
-------------------------
'removetails >>> ... >>> ... >>> ...' proved the goal fastest:
We consider the the dependency-graph
1: p^#(f(f(x))) -> c_1(q^#(f(g(x))))
2: p^#(g(g(x))) -> c_2(q^#(g(f(x))))
3: q^#(f(f(x))) -> c_3(p^#(f(g(x))))
4: q^#(g(g(x))) -> c_4(p^#(g(f(x))))
together with the congruence-graph
->{1} Noncyclic, trivial, SCC
->{2} Noncyclic, trivial, SCC
->{3} Noncyclic, trivial, SCC
->{4} Noncyclic, trivial, SCC
Here rules are as follows:
{ 1: p^#(f(f(x))) -> c_1(q^#(f(g(x))))
, 2: p^#(g(g(x))) -> c_2(q^#(g(f(x))))
, 3: q^#(f(f(x))) -> c_3(p^#(f(g(x))))
, 4: q^#(g(g(x))) -> c_4(p^#(g(f(x))))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 4: q^#(g(g(x))) -> c_4(p^#(g(f(x))))
, 3: q^#(f(f(x))) -> c_3(p^#(f(g(x))))
, 2: p^#(g(g(x))) -> c_2(q^#(g(f(x))))
, 1: p^#(f(f(x))) -> c_1(q^#(f(g(x))))}
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(1),O(1))Tool tup3irc
| Execution Time | 6.481099e-2ms |
|---|
| Answer | YES(O(1),O(1)) |
|---|
| Input | AG01 3.33 |
|---|
stdout:
YES(O(1),O(1))
We consider the following Problem:
Strict Trs:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Application of 'tup3 (timeout of 60.0 seconds)':
------------------------------------------------
The input problem contains no overlaps that give rise to inapplicable rules.
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
StartTerms: basic terms
Strategy: innermost
1) 'dp' proved the goal fastest:
We have computed the following dependency pairs
Strict Dependency Pairs:
{ p^#(f(f(x))) -> c_1(q^#(f(g(x))))
, p^#(g(g(x))) -> c_2(q^#(g(f(x))))
, q^#(f(f(x))) -> c_3(p^#(f(g(x))))
, q^#(g(g(x))) -> c_4(p^#(g(f(x))))}
We consider the following Problem:
Strict DPs:
{ p^#(f(f(x))) -> c_1(q^#(f(g(x))))
, p^#(g(g(x))) -> c_2(q^#(g(f(x))))
, q^#(f(f(x))) -> c_3(p^#(f(g(x))))
, q^#(g(g(x))) -> c_4(p^#(g(f(x))))}
Weak Trs:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Application of 'Fastest':
-------------------------
'compose (statically using 'split all congruence from CWD except leafs', multiplication)' proved the goal fastest:
Compose is inapplicable since some strict rule is size increasing
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{ p^#(f(f(x))) -> c_1(q^#(f(g(x))))
, p^#(g(g(x))) -> c_2(q^#(g(f(x))))
, q^#(f(f(x))) -> c_3(p^#(f(g(x))))
, q^#(g(g(x))) -> c_4(p^#(g(f(x))))}
Weak Trs:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
StartTerms: basic terms
Strategy: innermost
1) We consider the the dependency-graph
1: p^#(f(f(x))) -> c_1(q^#(f(g(x))))
2: p^#(g(g(x))) -> c_2(q^#(g(f(x))))
3: q^#(f(f(x))) -> c_3(p^#(f(g(x))))
4: q^#(g(g(x))) -> c_4(p^#(g(f(x))))
together with the congruence-graph
->{1} Noncyclic, trivial, SCC
->{2} Noncyclic, trivial, SCC
->{3} Noncyclic, trivial, SCC
->{4} Noncyclic, trivial, SCC
Here rules are as follows:
{ 1: p^#(f(f(x))) -> c_1(q^#(f(g(x))))
, 2: p^#(g(g(x))) -> c_2(q^#(g(f(x))))
, 3: q^#(f(f(x))) -> c_3(p^#(f(g(x))))
, 4: q^#(g(g(x))) -> c_4(p^#(g(f(x))))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 4: q^#(g(g(x))) -> c_4(p^#(g(f(x))))
, 3: q^#(f(f(x))) -> c_3(p^#(f(g(x))))
, 2: p^#(g(g(x))) -> c_2(q^#(g(f(x))))
, 1: p^#(f(f(x))) -> c_1(q^#(f(g(x))))}
We consider the following Problem:
Weak Trs:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
StartTerms: basic terms
Strategy: innermost
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
Weak Trs:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
StartTerms: basic terms
Strategy: innermost
The input problem is not a DP-problem.
We abort the transformation and continue with the subprocessor on the problem
Weak Trs:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
StartTerms: basic terms
Strategy: innermost
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
Weak Trs:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
StartTerms: basic terms
Strategy: innermost
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
Weak Trs:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
StartTerms: basic terms
Strategy: innermost
All strict components are empty, nothing to further orient
We abort the transformation and continue with the subprocessor on the problem
Weak Trs:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
StartTerms: basic terms
Strategy: innermost
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
Weak Trs:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
StartTerms: basic terms
Strategy: innermost
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
Weak Trs:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
StartTerms: basic terms
Strategy: innermost
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
Weak Trs:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
StartTerms: basic terms
Strategy: innermost
All strict components are empty, nothing to further orient
We abort the transformation and continue with the subprocessor on the problem
Weak Trs:
{ p(f(f(x))) -> q(f(g(x)))
, p(g(g(x))) -> q(g(f(x)))
, q(f(f(x))) -> p(f(g(x)))
, q(g(g(x))) -> p(g(f(x)))}
StartTerms: basic terms
Strategy: innermost
1) 'empty' succeeded:
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(1))