MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ f() -> f()
, g(b()) -> c()
, b() -> c() }
Obligation:
innermost runtime complexity
Answer:
MAYBE
Arguments of following rules are not normal-forms:
{ g(b()) -> c() }
All above mentioned rules can be savely removed.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ f() -> f()
, b() -> c() }
Obligation:
innermost runtime complexity
Answer:
MAYBE
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) 'Best' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'WithProblem (timeout of 60 seconds)' failed due to the
following reason:
We add the following innermost weak dependency pairs:
Strict DPs:
{ f^#() -> c_1(f^#())
, b^#() -> c_2() }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs:
{ f^#() -> c_1(f^#())
, b^#() -> c_2() }
Strict Trs:
{ f() -> f()
, b() -> c() }
Obligation:
innermost runtime complexity
Answer:
MAYBE
No rule is usable, rules are removed from the input problem.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs:
{ f^#() -> c_1(f^#())
, b^#() -> c_2() }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The weightgap principle applies (using the following constant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(c_1) = {1}
TcT has computed the following constructor-restricted matrix
interpretation.
[f^#] = [1]
[1]
[c_1](x1) = [1 0] x1 + [2]
[0 1] [2]
[b^#] = [2]
[1]
[c_2] = [1]
[1]
The following symbols are considered usable
{f^#, b^#}
The order satisfies the following ordering constraints:
[f^#()] = [1]
[1]
? [3]
[3]
= [c_1(f^#())]
[b^#()] = [2]
[1]
> [1]
[1]
= [c_2()]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs: { f^#() -> c_1(f^#()) }
Weak DPs: { b^#() -> c_2() }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ b^#() -> c_2() }
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs: { f^#() -> c_1(f^#()) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
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) 'WithProblem' 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) 'Fastest (timeout of 5 seconds)' failed due to the following
reason:
Computation stopped due to timeout after 5.0 seconds.
2) 'WithProblem' 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) 'Polynomial Path Order (PS)' failed due to the following reason:
The input cannot be shown compatible
3) 'Polynomial Path Order (PS)' failed due to the following reason:
The input cannot be shown compatible
2) 'Best' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed
due to the following reason:
Computation stopped due to timeout after 5.0 seconds.
2) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)'
failed due to the following reason:
We use the processor 'Small Polynomial Path Order (PS,1-bounded)'
to orient following rules strictly.
Trs: { b() -> c() }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The input was oriented with the instance of 'Small Polynomial Path
Order (PS,1-bounded)' as induced by the safe mapping
safe(f) = {}, safe(g) = {}, safe(b) = {}, safe(c) = {}
and precedence
empty .
Following symbols are considered recursive:
{f}
The recursion depth is 1.
For your convenience, here are the satisfied ordering constraints:
f() >= f()
b() > c()
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs: { f() -> f() }
Weak Trs: { b() -> c() }
Obligation:
innermost runtime complexity
Answer:
MAYBE
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) 'WithProblem' 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) 'WithProblem' 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) 'WithProblem' 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) 'WithProblem' 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) 'WithProblem' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'WithProblem' 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) 'WithProblem' failed due to the following reason:
Empty strict component of the problem is NOT empty.
3) 'Best' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due
to the following reason:
The input cannot be shown compatible
2) 'bsearch-popstar (timeout of 60 seconds)' failed due to the
following reason:
The input cannot be shown compatible
Arrrr..