MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { merge#1(nil(), @l2) -> @l2
  , merge#1(::(@x, @xs), @l2) -> merge#2(@l2, @x, @xs)
  , msplit#3(tuple#2(@l1, @l2), @x1, @x2) ->
    tuple#2(::(@x1, @l1), ::(@x2, @l2))
  , mergesort#1(nil()) -> nil()
  , mergesort#1(::(@x1, @xs)) -> mergesort#2(@xs, @x1)
  , mergesort#2(nil(), @x1) -> ::(@x1, nil())
  , mergesort#2(::(@x2, @xs'), @x1) ->
    mergesort#3(msplit(::(@x1, ::(@x2, @xs'))))
  , mergesort#3(tuple#2(@l1, @l2)) ->
    merge(mergesort(@l1), mergesort(@l2))
  , merge#3(#true(), @x, @xs, @y, @ys) ->
    ::(@x, merge(@xs, ::(@y, @ys)))
  , merge#3(#false(), @x, @xs, @y, @ys) ->
    ::(@y, merge(::(@x, @xs), @ys))
  , merge(@l1, @l2) -> merge#1(@l1, @l2)
  , msplit#2(nil(), @x1) -> tuple#2(::(@x1, nil()), nil())
  , msplit#2(::(@x2, @xs'), @x1) -> msplit#3(msplit(@xs'), @x1, @x2)
  , merge#2(nil(), @x, @xs) -> ::(@x, @xs)
  , merge#2(::(@y, @ys), @x, @xs) ->
    merge#3(#less(@x, @y), @x, @xs, @y, @ys)
  , msplit(@l) -> msplit#1(@l)
  , msplit#1(nil()) -> tuple#2(nil(), nil())
  , msplit#1(::(@x1, @xs)) -> msplit#2(@xs, @x1)
  , mergesort(@l) -> mergesort#1(@l)
  , #less(@x, @y) -> #cklt(#compare(@x, @y)) }
Weak Trs:
  { #cklt(#EQ()) -> #false()
  , #cklt(#LT()) -> #true()
  , #cklt(#GT()) -> #false()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) }
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) '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
         
      
      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 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..