MAYBE

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

Strict Trs:
  { #abs(#0()) -> #0()
  , #abs(#neg(@x)) -> #pos(@x)
  , #abs(#pos(@x)) -> #pos(@x)
  , #abs(#s(@x)) -> #pos(#s(@x))
  , #equal(@x, @y) -> #eq(@x, @y)
  , #greater(@x, @y) -> #ckgt(#compare(@x, @y))
  , +(@x, @y) -> #add(@x, @y)
  , firstline(@l) -> firstline#1(@l)
  , firstline#1(::(@x, @xs)) -> ::(#abs(#0()), firstline(@xs))
  , firstline#1(nil()) -> nil()
  , lcs(@l1, @l2) -> lcs#1(lcstable(@l1, @l2))
  , lcstable(@l1, @l2) -> lcstable#1(@l1, @l2)
  , lcs#1(@m) -> lcs#2(@m)
  , lcs#2(::(@l1, @_@2)) -> lcs#3(@l1)
  , lcs#2(nil()) -> #abs(#0())
  , lcs#3(::(@len, @_@1)) -> @len
  , lcs#3(nil()) -> #abs(#0())
  , lcstable#1(::(@x, @xs), @l2) ->
    lcstable#2(lcstable(@xs, @l2), @l2, @x)
  , lcstable#1(nil(), @l2) -> ::(firstline(@l2), nil())
  , lcstable#2(@m, @l2, @x) -> lcstable#3(@m, @l2, @x)
  , lcstable#3(::(@l, @ls), @l2, @x) ->
    ::(newline(@x, @l, @l2), ::(@l, @ls))
  , lcstable#3(nil(), @l2, @x) -> nil()
  , newline(@y, @lastline, @l) -> newline#1(@l, @lastline, @y)
  , max(@a, @b) -> max#1(#greater(@a, @b), @a, @b)
  , max#1(#false(), @a, @b) -> @b
  , max#1(#true(), @a, @b) -> @a
  , newline#1(::(@x, @xs), @lastline, @y) ->
    newline#2(@lastline, @x, @xs, @y)
  , newline#1(nil(), @lastline, @y) -> nil()
  , newline#2(::(@belowVal, @lastline'), @x, @xs, @y) ->
    newline#3(newline(@y, @lastline', @xs),
              @belowVal,
              @lastline',
              @x,
              @y)
  , newline#2(nil(), @x, @xs, @y) -> nil()
  , newline#3(@nl, @belowVal, @lastline', @x, @y) ->
    newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y)
  , right(@l) -> right#1(@l)
  , newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) ->
    newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y)
  , newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) ->
    newline#6(newline#7(#equal(@x, @y),
                        @belowVal,
                        @diagVal,
                        @rightVal),
              @nl)
  , newline#7(#false(), @belowVal, @diagVal, @rightVal) ->
    max(@belowVal, @rightVal)
  , newline#7(#true(), @belowVal, @diagVal, @rightVal) ->
    +(@diagVal, #pos(#s(#0())))
  , newline#6(@elem, @nl) -> ::(@elem, @nl)
  , right#1(::(@x, @xs)) -> @x
  , right#1(nil()) -> #abs(#0()) }
Weak Trs:
  { #eq(#0(), #0()) -> #true()
  , #eq(#0(), #neg(@y)) -> #false()
  , #eq(#0(), #pos(@y)) -> #false()
  , #eq(#0(), #s(@y)) -> #false()
  , #eq(#neg(@x), #0()) -> #false()
  , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
  , #eq(#neg(@x), #pos(@y)) -> #false()
  , #eq(#pos(@x), #0()) -> #false()
  , #eq(#pos(@x), #neg(@y)) -> #false()
  , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
  , #eq(#s(@x), #0()) -> #false()
  , #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
  , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
    #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
  , #eq(::(@x_1, @x_2), nil()) -> #false()
  , #eq(nil(), ::(@y_1, @y_2)) -> #false()
  , #eq(nil(), nil()) -> #true()
  , #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #ckgt(#EQ()) -> #false()
  , #ckgt(#GT()) -> #true()
  , #ckgt(#LT()) -> #false()
  , #add(#0(), @y) -> @y
  , #add(#neg(#s(#0())), @y) -> #pred(@y)
  , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
  , #add(#pos(#s(#0())), @y) -> #succ(@y)
  , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
  , #pred(#0()) -> #neg(#s(#0()))
  , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
  , #pred(#pos(#s(#0()))) -> #0()
  , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
  , #succ(#0()) -> #pos(#s(#0()))
  , #succ(#neg(#s(#0()))) -> #0()
  , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
  , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
  , #and(#false(), #false()) -> #false()
  , #and(#false(), #true()) -> #false()
  , #and(#true(), #false()) -> #false()
  , #and(#true(), #true()) -> #true() }
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) 'Fastest' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'trivial' 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) 'Sequentially' failed due to the following reason:
         
         None of the processors succeeded.
         
         Details of failed attempt(s):
         -----------------------------
         1) 'Polynomial Path Order (PS)' failed due to the following reason:
            
            The input cannot be shown compatible
         
         2) 'Polynomial Path Order' failed due to the following reason:
            
            The input cannot be shown compatible
         
      
   
   2) 'Fastest (timeout of 5 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..