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}
 Fail