MAYBE

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

Strict Trs:
  { start(i) ->
    busy(F(), closed(), stop(), false(), false(), false(), i)
  , busy(fl, open(), up(), b1, b2, b3, i) -> incorrect()
  , busy(fl, open(), down(), b1, b2, b3, i) -> incorrect()
  , busy(F(), d, stop(), b1, true(), b3, i) ->
    idle(F(), open(), stop(), b1, false(), b3, i)
  , busy(F(), closed(), stop(), false(), false(), false(), empty())
    -> correct()
  , busy(F(),
         closed(),
         stop(),
         false(),
         false(),
         false(),
         newbuttons(i1, i2, i3, i))
    ->
    idle(F(),
         closed(),
         stop(),
         false(),
         false(),
         false(),
         newbuttons(i1, i2, i3, i))
  , busy(F(), closed(), stop(), false(), false(), true(), i) ->
    idle(F(), closed(), up(), false(), false(), true(), i)
  , busy(F(), closed(), stop(), true(), false(), b3, i) ->
    idle(F(), closed(), down(), true(), false(), b3, i)
  , busy(F(), closed(), up(), b1, false(), b3, i) ->
    idle(FS(), closed(), up(), b1, false(), b3, i)
  , busy(F(), closed(), up(), b1, true(), b3, i) ->
    idle(F(), closed(), stop(), b1, true(), b3, i)
  , busy(F(), closed(), down(), b1, false(), b3, i) ->
    idle(BF(), closed(), down(), b1, false(), b3, i)
  , busy(F(), closed(), down(), b1, true(), b3, i) ->
    idle(F(), closed(), stop(), b1, true(), b3, i)
  , busy(F(), open(), stop(), b1, false(), b3, i) ->
    idle(F(), closed(), stop(), b1, false(), b3, i)
  , busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect()
  , busy(BF(), closed(), up(), b1, b2, b3, i) ->
    idle(F(), closed(), up(), b1, b2, b3, i)
  , busy(BF(), closed(), down(), b1, b2, b3, i) ->
    idle(B(), closed(), down(), b1, b2, b3, i)
  , busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect()
  , busy(FS(), closed(), up(), b1, b2, b3, i) ->
    idle(S(), closed(), up(), b1, b2, b3, i)
  , busy(FS(), closed(), down(), b1, b2, b3, i) ->
    idle(F(), closed(), down(), b1, b2, b3, i)
  , busy(B(), d, stop(), true(), b2, b3, i) ->
    idle(B(), open(), stop(), false(), b2, b3, i)
  , busy(B(), closed(), stop(), false(), false(), false(), empty())
    -> correct()
  , busy(B(),
         closed(),
         stop(),
         false(),
         false(),
         false(),
         newbuttons(i1, i2, i3, i))
    ->
    idle(B(),
         closed(),
         stop(),
         false(),
         false(),
         false(),
         newbuttons(i1, i2, i3, i))
  , busy(B(), closed(), stop(), false(), false(), true(), i) ->
    idle(B(), closed(), up(), false(), false(), true(), i)
  , busy(B(), closed(), stop(), false(), true(), b3, i) ->
    idle(B(), closed(), up(), false(), true(), b3, i)
  , busy(B(), closed(), up(), false(), b2, b3, i) ->
    idle(BF(), closed(), up(), false(), b2, b3, i)
  , busy(B(), closed(), up(), true(), b2, b3, i) ->
    idle(B(), closed(), stop(), true(), b2, b3, i)
  , busy(B(), closed(), down(), b1, b2, b3, i) ->
    idle(B(), closed(), stop(), b1, b2, b3, i)
  , busy(B(), open(), stop(), false(), b2, b3, i) ->
    idle(B(), closed(), stop(), false(), b2, b3, i)
  , busy(S(), d, stop(), b1, b2, true(), i) ->
    idle(S(), open(), stop(), b1, b2, false(), i)
  , busy(S(), closed(), stop(), b1, true(), false(), i) ->
    idle(S(), closed(), down(), b1, true(), false(), i)
  , busy(S(), closed(), stop(), false(), false(), false(), empty())
    -> correct()
  , busy(S(),
         closed(),
         stop(),
         false(),
         false(),
         false(),
         newbuttons(i1, i2, i3, i))
    ->
    idle(S(),
         closed(),
         stop(),
         false(),
         false(),
         false(),
         newbuttons(i1, i2, i3, i))
  , busy(S(), closed(), stop(), true(), false(), false(), i) ->
    idle(S(), closed(), down(), true(), false(), false(), i)
  , busy(S(), closed(), up(), b1, b2, b3, i) ->
    idle(S(), closed(), stop(), b1, b2, b3, i)
  , busy(S(), closed(), down(), b1, b2, false(), i) ->
    idle(FS(), closed(), down(), b1, b2, false(), i)
  , busy(S(), closed(), down(), b1, b2, true(), i) ->
    idle(S(), closed(), stop(), b1, b2, true(), i)
  , busy(S(), open(), stop(), b1, b2, false(), i) ->
    idle(S(), closed(), stop(), b1, b2, false(), i)
  , idle(fl, d, m, b1, b2, b3, empty()) ->
    busy(fl, d, m, b1, b2, b3, empty())
  , idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
    busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
  , or(false(), b) -> b
  , or(true(), b) -> true() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..