MAYBE
Time: 0.664651
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()}
 DP:
  DP:
   {                                                      busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, 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#(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(), 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(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i),
    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(), 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),
                                            idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1),
                                            idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2),
                                            idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)}
  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()}
  UR:
   {or(false(), b) -> b,
     or(true(), b) -> true()}
   EDG:
    {
     (busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), 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))
     (busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), 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))
     (busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), 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))
     (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), 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))
     (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), 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))
     (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), 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))
     (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), 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))
     (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), 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))
     (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), 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))
     (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), 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))
     (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), 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))
     (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), 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))
     (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), 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))
     (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), 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))
     (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), 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))
     (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), 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), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), 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)))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), i), busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), i), busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), i), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), 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)))
     (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), i), busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i))
     (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), busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i))
     (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), busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)))
     (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), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i))
     (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), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i))
     (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), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i))
     (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), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i))
     (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), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i))
     (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), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i))
     (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), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i))
     (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), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i))
     (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), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i))
     (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), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i))
     (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), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i))
     (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), busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i))
     (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), busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)))
     (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), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i))
     (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), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i))
     (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), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i))
     (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), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i))
     (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), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i))
     (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), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i))
     (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), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i))
     (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), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i))
     (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), busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)))
     (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), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i))
     (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), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i))
     (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), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i))
     (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), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i))
     (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), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), 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()))
     (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), 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))
     (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), 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))
     (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (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()))
     (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), 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))
     (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), 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))
     (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), 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))
     (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), 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))
     (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), 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))
     (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), 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))
     (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), 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))
     (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), 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))
     (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), 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))
     (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), 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))
     (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), 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))
     (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), 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()), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i))
     (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i))
     (busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
     (busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), 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))
     (busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
     (busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
     (busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
    }
    EDG:
     {
      (busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), 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))
      (busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), 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))
      (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), 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))
      (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
      (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), 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))
      (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
      (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), 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))
      (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
      (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), 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))
      (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
      (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), 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))
      (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
      (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), 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))
      (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
      (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), 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))
      (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
      (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), 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))
      (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
      (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), 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))
      (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
      (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), 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))
      (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
      (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), 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))
      (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
      (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), 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))
      (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
      (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), 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))
      (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
      (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), 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)))
      (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), busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i))
      (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), busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)))
      (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), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i))
      (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), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i))
      (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), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i))
      (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), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i))
      (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), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i))
      (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), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i))
      (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), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i))
      (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), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i))
      (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), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i))
      (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), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i))
      (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), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i))
      (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), busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i))
      (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), busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)))
      (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), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i))
      (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), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i))
      (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), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i))
      (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), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i))
      (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), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i))
      (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), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i))
      (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), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i))
      (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), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i))
      (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), busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)))
      (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), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i))
      (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), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i))
      (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), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i))
      (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), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i))
      (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), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), 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()))
      (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), 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))
      (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
      (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), 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))
      (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (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()))
      (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), 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))
      (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
      (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), 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))
      (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
      (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), 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))
      (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
      (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), 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))
      (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
      (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), 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))
      (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
      (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), 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))
      (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
      (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), 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))
      (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
      (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), 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))
      (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
      (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), 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))
      (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
      (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), 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))
      (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
      (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), 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))
      (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i))
      (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i))
      (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i))
      (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i))
      (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i))
      (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i))
      (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i))
      (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i))
      (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i))
      (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i))
      (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i))
      (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i))
      (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i))
      (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i))
      (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i))
      (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i))
      (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i))
      (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i))
      (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i))
      (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i))
      (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i))
      (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), 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()), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i))
      (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i))
      (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i))
      (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i))
      (busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), 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))
      (busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
      (busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
      (busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
     }
     EDG:
      {
       (busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), 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))
       (busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), 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))
       (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), 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))
       (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
       (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), 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))
       (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
       (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), 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))
       (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
       (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), 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))
       (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
       (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), 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))
       (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
       (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), 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))
       (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
       (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), 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))
       (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
       (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), 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))
       (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
       (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), 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))
       (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
       (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), 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))
       (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
       (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), 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))
       (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
       (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), 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))
       (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
       (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), 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))
       (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
       (start# i -> busy#(F(), closed(), stop(), false(), false(), false(), 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)))
       (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), busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i))
       (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), busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)))
       (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), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i))
       (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), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i))
       (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), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i))
       (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), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i))
       (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), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i))
       (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), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i))
       (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), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i))
       (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), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i))
       (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), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i))
       (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), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i))
       (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), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i))
       (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), busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i))
       (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), busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)))
       (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), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i))
       (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), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i))
       (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), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i))
       (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), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i))
       (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), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i))
       (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), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i))
       (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), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i))
       (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), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i))
       (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), busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)))
       (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), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i))
       (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), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i))
       (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), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i))
       (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), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i))
       (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), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), 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()))
       (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), 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))
       (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
       (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), 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))
       (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (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()))
       (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), 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))
       (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
       (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), 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))
       (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
       (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), 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))
       (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
       (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), 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))
       (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
       (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), 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))
       (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
       (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), 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))
       (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
       (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), 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))
       (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
       (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), 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))
       (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
       (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), 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))
       (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
       (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), 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))
       (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))
       (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), 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))
       (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
       (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i))
       (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i))
       (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i))
       (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i))
       (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i))
       (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i))
       (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i))
       (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i))
       (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i))
       (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i))
       (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i))
       (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i))
       (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i))
       (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i))
       (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i))
       (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i))
       (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i))
       (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i))
       (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i))
       (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i))
       (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i))
       (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), 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()), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i))
       (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i))
       (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i))
       (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i))
       (busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), 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))
       (busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1))
       (busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2))
       (busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3))
      }
      STATUS:
       arrows: 0.838367
       SCCS (1):
        Scc:
         {                                                      busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, 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#(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(), 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(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i),
          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(), 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)}
        
        
        SCC (31):
         Strict:
          {                                                      busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, 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#(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(), 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(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i),
           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(), 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)}
         Weak:
         {                                                      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()}
         Open