Problem HirokawaMiddeldorp 04 t009

MAYBE

We consider the following Problem:

  Strict Trs:
    {  start(i) ->
       busy(F(), closed(), stop(), false(), false(), false(), i)
     , busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect()
     , busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect()
     , busy(fl, open(), up(), b1, b2, b3, i) -> incorrect()
     , busy(fl, open(), down(), b1, b2, b3, i) -> incorrect()
     , busy(B(), closed(), stop(), false(), false(), false(), empty())
       -> correct()
     , busy(F(), closed(), stop(), false(), false(), false(), empty())
       -> correct()
     , busy(S(), 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(F(),
            closed(),
            stop(),
            false(),
            false(),
            false(),
            newbuttons(i1, i2, i3, i))
       ->
       idle(F(),
            closed(),
            stop(),
            false(),
            false(),
            false(),
            newbuttons(i1, i2, i3, i))
     , 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(B(), open(), stop(), false(), b2, b3, i) ->
       idle(B(), closed(), stop(), false(), b2, b3, i)
     , busy(F(), open(), stop(), b1, false(), b3, i) ->
       idle(F(), closed(), stop(), b1, false(), b3, i)
     , busy(S(), open(), stop(), b1, b2, false(), i) ->
       idle(S(), closed(), stop(), b1, b2, false(), i)
     , busy(B(), d, stop(), true(), b2, b3, i) ->
       idle(B(), open(), stop(), false(), b2, b3, i)
     , busy(F(), d, stop(), b1, true(), b3, i) ->
       idle(F(), open(), stop(), b1, false(), b3, i)
     , busy(S(), d, stop(), b1, b2, true(), i) ->
       idle(S(), open(), stop(), b1, b2, false(), i)
     , busy(B(), closed(), down(), b1, b2, b3, i) ->
       idle(B(), closed(), stop(), b1, b2, b3, i)
     , busy(S(), closed(), up(), b1, b2, b3, i) ->
       idle(S(), closed(), stop(), b1, b2, b3, i)
     , busy(B(), closed(), up(), true(), b2, b3, i) ->
       idle(B(), closed(), stop(), true(), b2, b3, i)
     , busy(F(), closed(), up(), b1, true(), b3, i) ->
       idle(F(), closed(), stop(), b1, true(), b3, i)
     , busy(F(), closed(), down(), b1, true(), b3, i) ->
       idle(F(), closed(), stop(), b1, true(), b3, i)
     , busy(S(), closed(), down(), b1, b2, true(), i) ->
       idle(S(), closed(), stop(), b1, b2, true(), i)
     , busy(B(), closed(), up(), false(), b2, b3, i) ->
       idle(BF(), closed(), up(), false(), b2, b3, i)
     , busy(F(), closed(), up(), b1, false(), b3, i) ->
       idle(FS(), closed(), up(), b1, false(), b3, i)
     , busy(F(), closed(), down(), b1, false(), b3, i) ->
       idle(BF(), closed(), down(), b1, false(), b3, i)
     , busy(S(), closed(), down(), b1, b2, false(), i) ->
       idle(FS(), closed(), down(), b1, b2, false(), i)
     , 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(), 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(), closed(), stop(), false(), true(), b3, i) ->
       idle(B(), closed(), up(), false(), true(), b3, i)
     , busy(B(), closed(), stop(), false(), false(), true(), i) ->
       idle(B(), 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(), stop(), false(), false(), true(), i) ->
       idle(F(), closed(), up(), false(), false(), true(), i)
     , busy(S(), closed(), stop(), b1, true(), false(), i) ->
       idle(S(), closed(), down(), b1, true(), false(), i)
     , busy(S(), closed(), stop(), true(), false(), false(), i) ->
       idle(S(), closed(), down(), true(), false(), 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(true(), b) -> true()
     , or(false(), b) -> b}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  start(i) ->
       busy(F(), closed(), stop(), false(), false(), false(), i)
     , busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect()
     , busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect()
     , busy(fl, open(), up(), b1, b2, b3, i) -> incorrect()
     , busy(fl, open(), down(), b1, b2, b3, i) -> incorrect()
     , busy(B(), closed(), stop(), false(), false(), false(), empty())
       -> correct()
     , busy(F(), closed(), stop(), false(), false(), false(), empty())
       -> correct()
     , busy(S(), 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(F(),
            closed(),
            stop(),
            false(),
            false(),
            false(),
            newbuttons(i1, i2, i3, i))
       ->
       idle(F(),
            closed(),
            stop(),
            false(),
            false(),
            false(),
            newbuttons(i1, i2, i3, i))
     , 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(B(), open(), stop(), false(), b2, b3, i) ->
       idle(B(), closed(), stop(), false(), b2, b3, i)
     , busy(F(), open(), stop(), b1, false(), b3, i) ->
       idle(F(), closed(), stop(), b1, false(), b3, i)
     , busy(S(), open(), stop(), b1, b2, false(), i) ->
       idle(S(), closed(), stop(), b1, b2, false(), i)
     , busy(B(), d, stop(), true(), b2, b3, i) ->
       idle(B(), open(), stop(), false(), b2, b3, i)
     , busy(F(), d, stop(), b1, true(), b3, i) ->
       idle(F(), open(), stop(), b1, false(), b3, i)
     , busy(S(), d, stop(), b1, b2, true(), i) ->
       idle(S(), open(), stop(), b1, b2, false(), i)
     , busy(B(), closed(), down(), b1, b2, b3, i) ->
       idle(B(), closed(), stop(), b1, b2, b3, i)
     , busy(S(), closed(), up(), b1, b2, b3, i) ->
       idle(S(), closed(), stop(), b1, b2, b3, i)
     , busy(B(), closed(), up(), true(), b2, b3, i) ->
       idle(B(), closed(), stop(), true(), b2, b3, i)
     , busy(F(), closed(), up(), b1, true(), b3, i) ->
       idle(F(), closed(), stop(), b1, true(), b3, i)
     , busy(F(), closed(), down(), b1, true(), b3, i) ->
       idle(F(), closed(), stop(), b1, true(), b3, i)
     , busy(S(), closed(), down(), b1, b2, true(), i) ->
       idle(S(), closed(), stop(), b1, b2, true(), i)
     , busy(B(), closed(), up(), false(), b2, b3, i) ->
       idle(BF(), closed(), up(), false(), b2, b3, i)
     , busy(F(), closed(), up(), b1, false(), b3, i) ->
       idle(FS(), closed(), up(), b1, false(), b3, i)
     , busy(F(), closed(), down(), b1, false(), b3, i) ->
       idle(BF(), closed(), down(), b1, false(), b3, i)
     , busy(S(), closed(), down(), b1, b2, false(), i) ->
       idle(FS(), closed(), down(), b1, b2, false(), i)
     , 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(), 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(), closed(), stop(), false(), true(), b3, i) ->
       idle(B(), closed(), up(), false(), true(), b3, i)
     , busy(B(), closed(), stop(), false(), false(), true(), i) ->
       idle(B(), 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(), stop(), false(), false(), true(), i) ->
       idle(F(), closed(), up(), false(), false(), true(), i)
     , busy(S(), closed(), stop(), b1, true(), false(), i) ->
       idle(S(), closed(), down(), b1, true(), false(), i)
     , busy(S(), closed(), stop(), true(), false(), false(), i) ->
       idle(S(), closed(), down(), true(), false(), 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(true(), b) -> true()
     , or(false(), b) -> b}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  start(i) ->
       busy(F(), closed(), stop(), false(), false(), false(), i)
     , busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect()
     , busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect()
     , busy(fl, open(), up(), b1, b2, b3, i) -> incorrect()
     , busy(fl, open(), down(), b1, b2, b3, i) -> incorrect()
     , busy(B(), closed(), stop(), false(), false(), false(), empty())
       -> correct()
     , busy(F(), closed(), stop(), false(), false(), false(), empty())
       -> correct()
     , busy(S(), 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(F(),
            closed(),
            stop(),
            false(),
            false(),
            false(),
            newbuttons(i1, i2, i3, i))
       ->
       idle(F(),
            closed(),
            stop(),
            false(),
            false(),
            false(),
            newbuttons(i1, i2, i3, i))
     , 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(B(), open(), stop(), false(), b2, b3, i) ->
       idle(B(), closed(), stop(), false(), b2, b3, i)
     , busy(F(), open(), stop(), b1, false(), b3, i) ->
       idle(F(), closed(), stop(), b1, false(), b3, i)
     , busy(S(), open(), stop(), b1, b2, false(), i) ->
       idle(S(), closed(), stop(), b1, b2, false(), i)
     , busy(B(), d, stop(), true(), b2, b3, i) ->
       idle(B(), open(), stop(), false(), b2, b3, i)
     , busy(F(), d, stop(), b1, true(), b3, i) ->
       idle(F(), open(), stop(), b1, false(), b3, i)
     , busy(S(), d, stop(), b1, b2, true(), i) ->
       idle(S(), open(), stop(), b1, b2, false(), i)
     , busy(B(), closed(), down(), b1, b2, b3, i) ->
       idle(B(), closed(), stop(), b1, b2, b3, i)
     , busy(S(), closed(), up(), b1, b2, b3, i) ->
       idle(S(), closed(), stop(), b1, b2, b3, i)
     , busy(B(), closed(), up(), true(), b2, b3, i) ->
       idle(B(), closed(), stop(), true(), b2, b3, i)
     , busy(F(), closed(), up(), b1, true(), b3, i) ->
       idle(F(), closed(), stop(), b1, true(), b3, i)
     , busy(F(), closed(), down(), b1, true(), b3, i) ->
       idle(F(), closed(), stop(), b1, true(), b3, i)
     , busy(S(), closed(), down(), b1, b2, true(), i) ->
       idle(S(), closed(), stop(), b1, b2, true(), i)
     , busy(B(), closed(), up(), false(), b2, b3, i) ->
       idle(BF(), closed(), up(), false(), b2, b3, i)
     , busy(F(), closed(), up(), b1, false(), b3, i) ->
       idle(FS(), closed(), up(), b1, false(), b3, i)
     , busy(F(), closed(), down(), b1, false(), b3, i) ->
       idle(BF(), closed(), down(), b1, false(), b3, i)
     , busy(S(), closed(), down(), b1, b2, false(), i) ->
       idle(FS(), closed(), down(), b1, b2, false(), i)
     , 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(), 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(), closed(), stop(), false(), true(), b3, i) ->
       idle(B(), closed(), up(), false(), true(), b3, i)
     , busy(B(), closed(), stop(), false(), false(), true(), i) ->
       idle(B(), 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(), stop(), false(), false(), true(), i) ->
       idle(F(), closed(), up(), false(), false(), true(), i)
     , busy(S(), closed(), stop(), b1, true(), false(), i) ->
       idle(S(), closed(), down(), b1, true(), false(), i)
     , busy(S(), closed(), stop(), true(), false(), false(), i) ->
       idle(S(), closed(), down(), true(), false(), 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(true(), b) -> true()
     , or(false(), b) -> b}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  start(i) ->
       busy(F(), closed(), stop(), false(), false(), false(), i)
     , busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect()
     , busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect()
     , busy(fl, open(), up(), b1, b2, b3, i) -> incorrect()
     , busy(fl, open(), down(), b1, b2, b3, i) -> incorrect()
     , busy(B(), closed(), stop(), false(), false(), false(), empty())
       -> correct()
     , busy(F(), closed(), stop(), false(), false(), false(), empty())
       -> correct()
     , busy(S(), 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(F(),
            closed(),
            stop(),
            false(),
            false(),
            false(),
            newbuttons(i1, i2, i3, i))
       ->
       idle(F(),
            closed(),
            stop(),
            false(),
            false(),
            false(),
            newbuttons(i1, i2, i3, i))
     , 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(B(), open(), stop(), false(), b2, b3, i) ->
       idle(B(), closed(), stop(), false(), b2, b3, i)
     , busy(F(), open(), stop(), b1, false(), b3, i) ->
       idle(F(), closed(), stop(), b1, false(), b3, i)
     , busy(S(), open(), stop(), b1, b2, false(), i) ->
       idle(S(), closed(), stop(), b1, b2, false(), i)
     , busy(B(), d, stop(), true(), b2, b3, i) ->
       idle(B(), open(), stop(), false(), b2, b3, i)
     , busy(F(), d, stop(), b1, true(), b3, i) ->
       idle(F(), open(), stop(), b1, false(), b3, i)
     , busy(S(), d, stop(), b1, b2, true(), i) ->
       idle(S(), open(), stop(), b1, b2, false(), i)
     , busy(B(), closed(), down(), b1, b2, b3, i) ->
       idle(B(), closed(), stop(), b1, b2, b3, i)
     , busy(S(), closed(), up(), b1, b2, b3, i) ->
       idle(S(), closed(), stop(), b1, b2, b3, i)
     , busy(B(), closed(), up(), true(), b2, b3, i) ->
       idle(B(), closed(), stop(), true(), b2, b3, i)
     , busy(F(), closed(), up(), b1, true(), b3, i) ->
       idle(F(), closed(), stop(), b1, true(), b3, i)
     , busy(F(), closed(), down(), b1, true(), b3, i) ->
       idle(F(), closed(), stop(), b1, true(), b3, i)
     , busy(S(), closed(), down(), b1, b2, true(), i) ->
       idle(S(), closed(), stop(), b1, b2, true(), i)
     , busy(B(), closed(), up(), false(), b2, b3, i) ->
       idle(BF(), closed(), up(), false(), b2, b3, i)
     , busy(F(), closed(), up(), b1, false(), b3, i) ->
       idle(FS(), closed(), up(), b1, false(), b3, i)
     , busy(F(), closed(), down(), b1, false(), b3, i) ->
       idle(BF(), closed(), down(), b1, false(), b3, i)
     , busy(S(), closed(), down(), b1, b2, false(), i) ->
       idle(FS(), closed(), down(), b1, b2, false(), i)
     , 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(), 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(), closed(), stop(), false(), true(), b3, i) ->
       idle(B(), closed(), up(), false(), true(), b3, i)
     , busy(B(), closed(), stop(), false(), false(), true(), i) ->
       idle(B(), 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(), stop(), false(), false(), true(), i) ->
       idle(F(), closed(), up(), false(), false(), true(), i)
     , busy(S(), closed(), stop(), b1, true(), false(), i) ->
       idle(S(), closed(), down(), b1, true(), false(), i)
     , busy(S(), closed(), stop(), true(), false(), false(), i) ->
       idle(S(), closed(), down(), true(), false(), 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(true(), b) -> true()
     , or(false(), b) -> b}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  start(i) ->
       busy(F(), closed(), stop(), false(), false(), false(), i)
     , busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect()
     , busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect()
     , busy(fl, open(), up(), b1, b2, b3, i) -> incorrect()
     , busy(fl, open(), down(), b1, b2, b3, i) -> incorrect()
     , busy(B(), closed(), stop(), false(), false(), false(), empty())
       -> correct()
     , busy(F(), closed(), stop(), false(), false(), false(), empty())
       -> correct()
     , busy(S(), 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(F(),
            closed(),
            stop(),
            false(),
            false(),
            false(),
            newbuttons(i1, i2, i3, i))
       ->
       idle(F(),
            closed(),
            stop(),
            false(),
            false(),
            false(),
            newbuttons(i1, i2, i3, i))
     , 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(B(), open(), stop(), false(), b2, b3, i) ->
       idle(B(), closed(), stop(), false(), b2, b3, i)
     , busy(F(), open(), stop(), b1, false(), b3, i) ->
       idle(F(), closed(), stop(), b1, false(), b3, i)
     , busy(S(), open(), stop(), b1, b2, false(), i) ->
       idle(S(), closed(), stop(), b1, b2, false(), i)
     , busy(B(), d, stop(), true(), b2, b3, i) ->
       idle(B(), open(), stop(), false(), b2, b3, i)
     , busy(F(), d, stop(), b1, true(), b3, i) ->
       idle(F(), open(), stop(), b1, false(), b3, i)
     , busy(S(), d, stop(), b1, b2, true(), i) ->
       idle(S(), open(), stop(), b1, b2, false(), i)
     , busy(B(), closed(), down(), b1, b2, b3, i) ->
       idle(B(), closed(), stop(), b1, b2, b3, i)
     , busy(S(), closed(), up(), b1, b2, b3, i) ->
       idle(S(), closed(), stop(), b1, b2, b3, i)
     , busy(B(), closed(), up(), true(), b2, b3, i) ->
       idle(B(), closed(), stop(), true(), b2, b3, i)
     , busy(F(), closed(), up(), b1, true(), b3, i) ->
       idle(F(), closed(), stop(), b1, true(), b3, i)
     , busy(F(), closed(), down(), b1, true(), b3, i) ->
       idle(F(), closed(), stop(), b1, true(), b3, i)
     , busy(S(), closed(), down(), b1, b2, true(), i) ->
       idle(S(), closed(), stop(), b1, b2, true(), i)
     , busy(B(), closed(), up(), false(), b2, b3, i) ->
       idle(BF(), closed(), up(), false(), b2, b3, i)
     , busy(F(), closed(), up(), b1, false(), b3, i) ->
       idle(FS(), closed(), up(), b1, false(), b3, i)
     , busy(F(), closed(), down(), b1, false(), b3, i) ->
       idle(BF(), closed(), down(), b1, false(), b3, i)
     , busy(S(), closed(), down(), b1, b2, false(), i) ->
       idle(FS(), closed(), down(), b1, b2, false(), i)
     , 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(), 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(), closed(), stop(), false(), true(), b3, i) ->
       idle(B(), closed(), up(), false(), true(), b3, i)
     , busy(B(), closed(), stop(), false(), false(), true(), i) ->
       idle(B(), 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(), stop(), false(), false(), true(), i) ->
       idle(F(), closed(), up(), false(), false(), true(), i)
     , busy(S(), closed(), stop(), b1, true(), false(), i) ->
       idle(S(), closed(), down(), b1, true(), false(), i)
     , busy(S(), closed(), stop(), true(), false(), false(), i) ->
       idle(S(), closed(), down(), true(), false(), 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(true(), b) -> true()
     , or(false(), b) -> b}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  start(i) ->
       busy(F(), closed(), stop(), false(), false(), false(), i)
     , busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect()
     , busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect()
     , busy(fl, open(), up(), b1, b2, b3, i) -> incorrect()
     , busy(fl, open(), down(), b1, b2, b3, i) -> incorrect()
     , busy(B(), closed(), stop(), false(), false(), false(), empty())
       -> correct()
     , busy(F(), closed(), stop(), false(), false(), false(), empty())
       -> correct()
     , busy(S(), 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(F(),
            closed(),
            stop(),
            false(),
            false(),
            false(),
            newbuttons(i1, i2, i3, i))
       ->
       idle(F(),
            closed(),
            stop(),
            false(),
            false(),
            false(),
            newbuttons(i1, i2, i3, i))
     , 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(B(), open(), stop(), false(), b2, b3, i) ->
       idle(B(), closed(), stop(), false(), b2, b3, i)
     , busy(F(), open(), stop(), b1, false(), b3, i) ->
       idle(F(), closed(), stop(), b1, false(), b3, i)
     , busy(S(), open(), stop(), b1, b2, false(), i) ->
       idle(S(), closed(), stop(), b1, b2, false(), i)
     , busy(B(), d, stop(), true(), b2, b3, i) ->
       idle(B(), open(), stop(), false(), b2, b3, i)
     , busy(F(), d, stop(), b1, true(), b3, i) ->
       idle(F(), open(), stop(), b1, false(), b3, i)
     , busy(S(), d, stop(), b1, b2, true(), i) ->
       idle(S(), open(), stop(), b1, b2, false(), i)
     , busy(B(), closed(), down(), b1, b2, b3, i) ->
       idle(B(), closed(), stop(), b1, b2, b3, i)
     , busy(S(), closed(), up(), b1, b2, b3, i) ->
       idle(S(), closed(), stop(), b1, b2, b3, i)
     , busy(B(), closed(), up(), true(), b2, b3, i) ->
       idle(B(), closed(), stop(), true(), b2, b3, i)
     , busy(F(), closed(), up(), b1, true(), b3, i) ->
       idle(F(), closed(), stop(), b1, true(), b3, i)
     , busy(F(), closed(), down(), b1, true(), b3, i) ->
       idle(F(), closed(), stop(), b1, true(), b3, i)
     , busy(S(), closed(), down(), b1, b2, true(), i) ->
       idle(S(), closed(), stop(), b1, b2, true(), i)
     , busy(B(), closed(), up(), false(), b2, b3, i) ->
       idle(BF(), closed(), up(), false(), b2, b3, i)
     , busy(F(), closed(), up(), b1, false(), b3, i) ->
       idle(FS(), closed(), up(), b1, false(), b3, i)
     , busy(F(), closed(), down(), b1, false(), b3, i) ->
       idle(BF(), closed(), down(), b1, false(), b3, i)
     , busy(S(), closed(), down(), b1, b2, false(), i) ->
       idle(FS(), closed(), down(), b1, b2, false(), i)
     , 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(), 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(), closed(), stop(), false(), true(), b3, i) ->
       idle(B(), closed(), up(), false(), true(), b3, i)
     , busy(B(), closed(), stop(), false(), false(), true(), i) ->
       idle(B(), 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(), stop(), false(), false(), true(), i) ->
       idle(F(), closed(), up(), false(), false(), true(), i)
     , busy(S(), closed(), stop(), b1, true(), false(), i) ->
       idle(S(), closed(), down(), b1, true(), false(), i)
     , busy(S(), closed(), stop(), true(), false(), false(), i) ->
       idle(S(), closed(), down(), true(), false(), 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(true(), b) -> true()
     , or(false(), b) -> b}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..