MAYBE
MAYBE
TRS:
 {
                                                        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),
                                                                                     
  start(i) -> busy(F(), closed(), stop(), false(), 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(false(), b) -> b,
                                                                                
  or(true(), b) -> true()
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
                                                          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),
                                                                                       
    start(i) -> busy(F(), closed(), stop(), false(), 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(false(), b) -> b,
                                                                                  
    or(true(), b) -> true()
   }
  Fail