MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ rec[mapL_0][2](NilL()) -> NilL()
, rec[mapL_0][2](ConsL(x2, x1)) ->
ConsL(rec[dc_0][1](x2), rec[mapL_0][2](x1))
, rec[dc_0][1](Nil()) -> Nil()
, rec[dc_0][1](Cons(x77, Nil())) -> Cons(x77, Nil())
, rec[dc_0][1](Cons(x3, Cons(x2, x1))) ->
const_f[2](Cons(x3, Cons(x2, x1)),
rec[mapL_0][2](ConsL(Cons(x3,
rec[take_0][2](rec[halve_0][1](rec[length_0][1](x1)),
Cons(x2, x1))),
ConsL(rec[drop_0][2](rec[halve_0][1](rec[length_0][1](x1)),
Cons(x2, x1)),
NilL()))))
, rec[length_0][1](Nil()) -> 0()
, rec[length_0][1](Cons(x13, x17)) -> S(rec[length_0][1](x17))
, rec[halve_0][1](0()) -> 0()
, rec[halve_0][1](S(0())) -> S(0())
, rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17))
, rec[take_0][2](0(), x26) -> Nil()
, rec[take_0][2](S(x14), Cons(x10, x6)) ->
Cons(x10, rec[take_0][2](x14, x6))
, rec[take_0][2](S(0()), Nil()) ->
Cons(Head_error_empty_list(), Nil())
, rec[drop_0][2](0(), x26) -> x26
, rec[drop_0][2](S(x14), Cons(x10, x6)) -> rec[drop_0][2](x14, x6)
, rec[drop_0][2](S(0()), Nil()) -> Tail_error_empty_list()
, const_f[2](Cons(x4, Cons(x5, x6)), ConsL(x3, ConsL(x2, x1))) ->
rec[merge_0][2](x3, x2)
, rec[merge_0][2](Nil(), x58) -> x58
, rec[merge_0][2](Cons(x66, x74), Nil()) -> Cons(x66, x74)
, rec[merge_0][2](Cons(x18, x14), Cons(x10, x6)) ->
merge_cond_2(rec[leq_0][2](x18, x10),
Cons(x18, x14),
Cons(x10, x6),
x18,
x14,
x10,
x6)
, merge_cond_2(True(),
Cons(x15, x17),
Cons(x11, x13),
x9,
x7,
x5,
x3)
-> Cons(x9, rec[merge_0][2](x7, Cons(x11, x13)))
, merge_cond_2(False(),
Cons(x15, x17),
Cons(x11, x13),
x9,
x7,
x5,
x3)
-> Cons(x5, rec[merge_0][2](Cons(x15, x17), x3))
, rec[leq_0][2](0(), x106) -> True()
, rec[leq_0][2](S(x114), 0()) -> False()
, rec[leq_0][2](S(x10), S(x6)) -> rec[leq_0][2](x10, x6)
, main(x43) -> rec[dc_0][1](x43) }
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:
Computation stopped due to timeout after 60.0 seconds.
2) 'Best' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)'
failed due to the following reason:
Computation stopped due to timeout after 30.0 seconds.
2) 'Best' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the
following reason:
The input cannot be shown compatible
2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due
to the following reason:
The input cannot be shown compatible
3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed
due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Bounds with minimal-enrichment and initial automaton 'match''
failed due to the following reason:
match-boundness of the problem could not be verified.
2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
failed due to the following reason:
match-boundness of the problem could not be verified.
Arrrr..