YES
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()}
 RUF:
  Strict:
   {                                                      busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(),
                                                        busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(),
                                                        busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i),
                                busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(),
    busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)),
                                       busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i),
                                            busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i),
                                                  busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i),
                                                   busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i),
                                                busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i),
                                                 busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i),
                                                  busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i),
                                                           busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(),
                                                      busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i),
                                                    busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i),
                                                           busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(),
                                                      busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i),
                                                    busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i),
                                                        busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i),
                                busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(),
    busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)),
                                       busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i),
                                            busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i),
                                                  busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i),
                                                   busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i),
                                                     busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i),
                                                  busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i),
                                                        busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i),
                                            busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i),
                                busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(),
    busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)),
                                       busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i),
                                                       busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i),
                                                busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i),
                                                 busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i),
                                                  busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i),
                                                            idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()),
                                          idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i),
                                                                                 or(false(), b) -> b,
                                                                                  or(true(), b) -> true()}
  Weak:
   {}
  DP:
   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),
                                             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)}
   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),
                                                            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()}
   EDG:
    {
     (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))
     (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#(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)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), 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, 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(), 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(), 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(), 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(), 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(), 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#(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#(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(), 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(), 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(), 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(), 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(), 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#(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(), 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#(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(), 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#(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(), 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(), 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(), 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(), 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(), 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(), 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(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, 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#(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, 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#(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)) -> 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, 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)) -> 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, 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#(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)) -> 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, 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)) -> 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, 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#(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)) -> 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, 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)) -> 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, 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#(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)) -> 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, 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)) -> 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, 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#(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)) -> 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, 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)) -> 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, 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#(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)) -> 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, 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)) -> 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, 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#(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)) -> 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, 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)) -> 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, 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#(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)) -> 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, 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)) -> 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, 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#(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)) -> 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, 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)) -> 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, 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#(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)) -> 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, 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)) -> 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, 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#(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)) -> 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, 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)) -> 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, 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#(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)) -> 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, 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)) -> or#(b3, i3))
     (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#(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)) -> 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, 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), 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(), 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(), 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, 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)) -> 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#(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, 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)) -> 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)) -> 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)) -> 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#(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, 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)) -> 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)) -> 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)) -> 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#(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, 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)) -> 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)) -> 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)) -> 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#(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, 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)) -> 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)) -> 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)) -> 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#(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, 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)) -> 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)) -> 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)) -> 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#(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, 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)) -> 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)) -> 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)) -> 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#(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, 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)) -> 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)) -> 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)) -> 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#(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, 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)) -> 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)) -> 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)) -> 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#(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, 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)) -> 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)) -> 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)) -> 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#(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, 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)) -> 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)) -> 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)) -> 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#(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, 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)) -> 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)) -> 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)) -> 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#(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, 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)) -> 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#(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)) -> 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#(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)) -> 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#(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)) -> 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#(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)) -> 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)) -> 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)) -> 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#(b3, i3))
    }
    SCCS:
     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:
      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),
                                                               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()}
      SPSC:
       Simple Projection:
        pi(idle#) = 6, pi(busy#) = 6
       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())}
       EDG:
        {(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, 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(), 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(), 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(), 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(), 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(), 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#(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#(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(), 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(), 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(), 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(), 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(), 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#(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(), 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#(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(), 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#(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(), 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(), 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(), 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(), 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(), 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(), 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(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i))
         (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(), 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(), 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(), 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(), 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(), 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(), 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(), 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(), 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#(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(), 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(), 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(), 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(), 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(), 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(), 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#(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#(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(), 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(), 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#(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#(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#(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(), 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(), 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(), 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()))}
        SCCS:
         Scc:
          {                 busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, 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(), 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(), 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())}
         SCC:
          Strict:
           {                 busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, 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(), 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(), 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())}
          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),
                                                                   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()}
          POLY:
           Argument Filtering:
            pi(or) = [], pi(true) = [], pi(newbuttons) = [], pi(idle#) = 3, pi(idle) = [], pi(S) = [], pi(empty) = [], pi(B) = [], pi(correct) = [], pi(down) = [], pi(up) = [], pi(open) = [], pi(FS) = [], pi(BF) = [], pi(incorrect) = [], pi(false) = [], pi(stop) = [], pi(closed) = [], pi(F) = [], pi(busy#) = 3, pi(busy) = []
           Usable Rules:
            {}
           Interpretation:
            [true] = 1,
            [false] = 0
           Strict:
            {                 busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, 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(), 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(), 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())}
           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),
                                                                     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()}
           EDG:
            {(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, 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, 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, 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#(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(), 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(), 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#(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(), 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(), 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(), 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(), 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(), 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(), 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#(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#(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(), 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#(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#(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#(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(), 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(), 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(), 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()))
             (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(), 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))}
            SCCS:
             Scc:
              {                 busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, 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(), 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(), 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())}
             SCC:
              Strict:
               {                 busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, 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(), 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(), 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())}
              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),
                                                                       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()}
              POLY:
               Argument Filtering:
                pi(or) = [], pi(true) = [], pi(newbuttons) = [], pi(idle#) = [2,4], pi(idle) = [], pi(S) = [], pi(empty) = [], pi(B) = [], pi(correct) = [], pi(down) = [], pi(up) = [], pi(open) = [], pi(FS) = [], pi(BF) = [], pi(incorrect) = [], pi(false) = [], pi(stop) = [], pi(closed) = [], pi(F) = [], pi(busy#) = 4, pi(busy) = []
               Usable Rules:
                {}
               Interpretation:
                [idle#](x0, x1) = x0 + x1,
                [true] = 1,
                [down] = 0,
                [up] = 0,
                [false] = 0,
                [stop] = 0
               Strict:
                {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(), 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(), 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())}
               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),
                                                                         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()}
               EDG:
                {(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, 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#(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, 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(), 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(), 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#(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(), 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(), 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(), 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, 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(), 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#(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(), 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(), 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#(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#(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(), 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#(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#(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#(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(), 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(), 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(), 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()))}
                SCCS:
                 Scc:
                  {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(), 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(), 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())}
                 SCC:
                  Strict:
                   {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(), 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(), 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())}
                  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),
                                                                           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()}
                  POLY:
                   Argument Filtering:
                    pi(or) = [], pi(true) = [], pi(newbuttons) = [], pi(idle#) = 5, pi(idle) = [], pi(S) = [], pi(empty) = [], pi(B) = [], pi(correct) = [], pi(down) = [], pi(up) = [], pi(open) = [], pi(FS) = [], pi(BF) = [], pi(incorrect) = [], pi(false) = [], pi(stop) = [], pi(closed) = [], pi(F) = [], pi(busy#) = 5, pi(busy) = []
                   Usable Rules:
                    {}
                   Interpretation:
                    [true] = 1,
                    [false] = 0
                   Strict:
                    {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(), 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(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i),
                     busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i),
                                     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())}
                   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),
                                                                             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()}
                   EDG:
                    {(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(), 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(), 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(), 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(), 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(), 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(), 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, 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(), 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(), 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(), 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(), 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(), 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(), 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#(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(), 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(), 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#(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#(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#(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(), 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(), 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()))
                     (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(), 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(), 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))}
                    SCCS:
                     Scc:
                      {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(), 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(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i),
                       busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i),
                                       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())}
                     SCC:
                      Strict:
                       {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(), 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(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i),
                        busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i),
                                        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())}
                      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),
                                                                               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()}
                      POLY:
                       Argument Filtering:
                        pi(or) = [], pi(true) = [], pi(newbuttons) = [], pi(idle#) = 1, pi(idle) = [], pi(S) = [], pi(empty) = [], pi(B) = [], pi(correct) = [], pi(down) = [], pi(up) = [], pi(open) = [], pi(FS) = [], pi(BF) = [], pi(incorrect) = [], pi(false) = [], pi(stop) = [], pi(closed) = [], pi(F) = [], pi(busy#) = 1, pi(busy) = []
                       Usable Rules:
                        {}
                       Interpretation:
                        [open] = 1,
                        [closed] = 0
                       Strict:
                        {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#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i),
                                      busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i),
                                        busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i),
                                      busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i),
                         busy#(B(), closed(), stop(), false(), 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#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i),
                         busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i),
                                         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),
                                              idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())}
                       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),
                                                                                 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()}
                       EDG:
                        {(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(), 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(), 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#(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, 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(), 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(), 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#(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(), 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(), 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(), 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#(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(), 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#(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#(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#(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(), 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(), 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()))
                         (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#(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(), 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#(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))}
                        SCCS:
                         Scc:
                          {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#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i),
                                        busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i),
                                          busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i),
                                        busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i),
                           busy#(B(), closed(), stop(), false(), 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#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i),
                           busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i),
                                           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),
                                                idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())}
                         SCC:
                          Strict:
                           {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#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i),
                                         busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i),
                                           busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i),
                                         busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i),
                            busy#(B(), closed(), stop(), false(), 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#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i),
                            busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i),
                                            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),
                                                 idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())}
                          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),
                                                                                   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:
                           {}
                           BOUND:
                            Bound: match(-raise)-bounded by 6
                            Automaton:
                             {
                                                            a_0() -> 2*
                                                         true_2() -> 64*
                                                         true_1() -> 41*
                                                         true_0() -> 8*
                              idle#_5(79, 77, 78, 66, 66, 64, 72) -> 25 | 11
                              idle#_5(76, 77, 78, 64, 66, 66, 72) -> 33 | 1
                              idle#_4(75, 69, 74, 54, 54, 41, 60) -> 25 | 11
                               idle#_4(75, 69, 74, 54, 54, 8, 60) -> 25 | 11
                               idle#_4(75, 69, 74, 54, 54, 2, 60) -> 1*
                               idle#_4(75, 69, 74, 43, 54, 8, 60) -> 25 | 11
                              idle#_4(75, 69, 70, 66, 66, 64, 60) -> 25 | 11
                              idle#_4(73, 69, 74, 41, 54, 54, 60) -> 33 | 1
                               idle#_4(73, 69, 74, 8, 54, 54, 60) -> 33 | 1
                               idle#_4(73, 69, 74, 8, 54, 43, 60) -> 33 | 1
                               idle#_4(73, 69, 74, 2, 54, 54, 60) -> 1*
                              idle#_4(73, 69, 71, 64, 66, 66, 60) -> 33 | 1
                              idle#_4(68, 69, 71, 64, 54, 66, 60) -> 33 | 1
                              idle#_4(68, 69, 70, 66, 54, 64, 60) -> 25 | 11
                              idle#_3(67, 57, 63, 64, 54, 66, 52) -> 33 | 1
                              idle#_3(67, 57, 62, 66, 66, 64, 72) -> 25 | 11
                              idle#_3(65, 57, 63, 64, 66, 66, 72) -> 33 | 1
                              idle#_3(65, 57, 62, 66, 54, 64, 52) -> 25 | 11
                              idle#_3(61, 57, 63, 41, 43, 54, 52) -> 33 | 1
                               idle#_3(61, 57, 63, 8, 43, 54, 52) -> 33 | 1
                               idle#_3(61, 57, 63, 2, 43, 54, 52) -> 1*
                              idle#_3(61, 57, 62, 54, 43, 41, 52) -> 25 | 11
                               idle#_3(61, 57, 62, 54, 43, 8, 52) -> 25 | 11
                               idle#_3(61, 57, 62, 54, 43, 2, 52) -> 1*
                              idle#_3(59, 57, 62, 54, 54, 41, 52) -> 25 | 11
                               idle#_3(59, 57, 62, 54, 54, 8, 52) -> 25 | 11
                               idle#_3(59, 57, 62, 54, 54, 2, 52) -> 1*
                               idle#_3(59, 57, 62, 43, 54, 8, 52) -> 25 | 11
                              idle#_3(59, 57, 58, 54, 54, 64, 52) -> 25 | 11
                               idle#_3(59, 57, 58, 43, 43, 8, 52) -> 25 | 11
                               idle#_3(59, 57, 58, 43, 43, 2, 52) -> 1*
                               idle#_3(59, 57, 58, 12, 43, 8, 52) -> 25*
                               idle#_3(59, 57, 58, 12, 43, 8, 45) -> 25 | 11
                              idle#_3(56, 57, 63, 41, 54, 54, 52) -> 33 | 1
                               idle#_3(56, 57, 63, 8, 54, 54, 52) -> 33 | 1
                               idle#_3(56, 57, 63, 8, 54, 43, 52) -> 33 | 1
                               idle#_3(56, 57, 63, 2, 54, 54, 52) -> 1*
                              idle#_3(56, 57, 58, 64, 54, 54, 52) -> 33 | 1
                               idle#_3(56, 57, 58, 8, 43, 43, 52) -> 33 | 1
                               idle#_3(56, 57, 58, 8, 43, 12, 52) -> 33 | 1
                               idle#_3(56, 57, 58, 8, 43, 12, 45) -> 33 | 1
                                idle#_3(56, 57, 58, 8, 43, 2, 52) -> 1*
                                idle#_3(56, 57, 58, 8, 43, 2, 45) -> 15 | 1
                               idle#_3(56, 57, 58, 2, 43, 43, 52) -> 1*
                              idle#_2(55, 47, 49, 41, 43, 54, 45) -> 33 | 1
                               idle#_2(55, 47, 49, 8, 43, 54, 52) -> 33 | 1
                               idle#_2(55, 47, 49, 2, 43, 54, 52) -> 1*
                              idle#_2(55, 47, 48, 54, 54, 41, 60) -> 25 | 11
                               idle#_2(55, 47, 48, 54, 54, 8, 60) -> 25 | 11
                               idle#_2(55, 47, 48, 54, 54, 2, 60) -> 1*
                               idle#_2(55, 47, 48, 43, 54, 8, 52) -> 25 | 11
                              idle#_2(53, 47, 49, 41, 54, 54, 60) -> 33 | 1
                               idle#_2(53, 47, 49, 8, 54, 54, 60) -> 33 | 1
                               idle#_2(53, 47, 49, 8, 54, 43, 52) -> 33 | 1
                               idle#_2(53, 47, 49, 2, 54, 54, 60) -> 1*
                              idle#_2(53, 47, 48, 54, 43, 41, 45) -> 25 | 11
                               idle#_2(53, 47, 48, 54, 43, 8, 52) -> 25 | 11
                               idle#_2(53, 47, 48, 54, 43, 2, 52) -> 1*
                              idle#_2(50, 47, 51, 43, 43, 41, 45) -> 25 | 11
                              idle#_2(50, 47, 51, 41, 43, 43, 45) -> 33 | 1
                               idle#_2(50, 47, 51, 12, 12, 8, 45) -> 25 | 11
                               idle#_2(50, 47, 51, 12, 12, 8, 34) -> 25 | 11
                               idle#_2(50, 47, 51, 12, 12, 2, 45) -> 1*
                               idle#_2(50, 47, 51, 12, 12, 2, 34) -> 1*
                               idle#_2(50, 47, 51, 8, 12, 12, 45) -> 33 | 1
                               idle#_2(50, 47, 51, 8, 12, 12, 34) -> 33 | 1
                                idle#_2(50, 47, 51, 8, 12, 2, 45) -> 15 | 1
                                idle#_2(50, 47, 51, 8, 12, 2, 34) -> 15 | 1
                               idle#_2(50, 47, 51, 2, 12, 12, 45) -> 1*
                               idle#_2(50, 47, 51, 2, 12, 12, 34) -> 1*
                                idle#_2(50, 47, 51, 2, 12, 2, 45) -> 1*
                                idle#_2(50, 47, 51, 2, 12, 2, 34) -> 1*
                              idle#_2(50, 47, 49, 64, 54, 54, 52) -> 33 | 1
                               idle#_2(50, 47, 49, 8, 43, 43, 45) -> 33 | 1
                               idle#_2(50, 47, 49, 8, 43, 12, 45) -> 33 | 1
                               idle#_2(50, 47, 49, 8, 43, 12, 34) -> 33 | 1
                                idle#_2(50, 47, 49, 8, 43, 2, 45) -> 1*
                                idle#_2(50, 47, 49, 8, 43, 2, 34) -> 15 | 1
                               idle#_2(50, 47, 49, 2, 43, 43, 45) -> 1*
                              idle#_2(50, 47, 48, 54, 54, 64, 52) -> 25 | 11
                               idle#_2(50, 47, 48, 43, 43, 8, 45) -> 25 | 11
                               idle#_2(50, 47, 48, 43, 43, 2, 45) -> 1*
                               idle#_2(50, 47, 48, 12, 43, 8, 45) -> 25*
                               idle#_2(50, 47, 48, 12, 43, 8, 34) -> 25 | 11
                               idle#_2(46, 47, 49, 8, 43, 43, 45) -> 33 | 1
                               idle#_2(46, 47, 49, 8, 12, 43, 45) -> 33 | 1
                               idle#_2(46, 47, 49, 8, 12, 43, 34) -> 33 | 1
                               idle#_2(46, 47, 49, 2, 12, 43, 45) -> 1*
                                idle#_2(46, 47, 49, 2, 8, 43, 45) -> 1*
                                idle#_2(46, 47, 49, 2, 8, 43, 34) -> 32 | 1
                               idle#_2(46, 47, 48, 43, 43, 8, 45) -> 25 | 11
                               idle#_2(46, 47, 48, 43, 12, 8, 45) -> 25 | 11 | 1
                               idle#_2(46, 47, 48, 43, 12, 8, 34) -> 25*
                               idle#_2(46, 47, 48, 43, 12, 2, 45) -> 1*
                                idle#_2(46, 47, 48, 43, 8, 2, 45) -> 1*
                                idle#_2(46, 47, 48, 43, 8, 2, 34) -> 26 | 1
                               idle#_1(44, 36, 38, 8, 43, 43, 52) -> 33 | 1
                               idle#_1(44, 36, 38, 8, 43, 43, 45) -> 33 | 1
                               idle#_1(44, 36, 38, 8, 12, 43, 45) -> 33 | 1
                               idle#_1(44, 36, 38, 8, 12, 43, 34) -> 33 | 1
                                idle#_1(44, 36, 38, 8, 12, 43, 3) -> 33 | 1
                               idle#_1(44, 36, 38, 2, 12, 43, 45) -> 1*
                               idle#_1(44, 36, 38, 2, 12, 43, 34) -> 1*
                                idle#_1(44, 36, 38, 2, 8, 43, 34) -> 1*
                                 idle#_1(44, 36, 38, 2, 8, 43, 3) -> 32 | 1
                               idle#_1(44, 36, 37, 43, 43, 8, 52) -> 25 | 11 | 1
                               idle#_1(44, 36, 37, 43, 43, 8, 45) -> 25*
                               idle#_1(44, 36, 37, 43, 43, 2, 52) -> 1*
                               idle#_1(44, 36, 37, 12, 43, 8, 45) -> 25*
                               idle#_1(44, 36, 37, 12, 43, 8, 34) -> 25*
                                idle#_1(44, 36, 37, 12, 43, 8, 3) -> 25 | 11
                               idle#_1(42, 36, 38, 8, 43, 43, 52) -> 33 | 1
                               idle#_1(42, 36, 38, 8, 43, 43, 45) -> 33 | 1
                               idle#_1(42, 36, 38, 8, 43, 12, 45) -> 33 | 1
                               idle#_1(42, 36, 38, 8, 43, 12, 34) -> 33 | 1
                                idle#_1(42, 36, 38, 8, 43, 12, 3) -> 33 | 1
                                idle#_1(42, 36, 38, 8, 43, 2, 34) -> 1*
                                 idle#_1(42, 36, 38, 8, 43, 2, 3) -> 15 | 1
                               idle#_1(42, 36, 38, 2, 43, 43, 52) -> 1*
                               idle#_1(42, 36, 37, 43, 43, 8, 52) -> 25*
                               idle#_1(42, 36, 37, 43, 43, 8, 45) -> 25 | 11
                               idle#_1(42, 36, 37, 43, 12, 8, 45) -> 25 | 11
                               idle#_1(42, 36, 37, 43, 12, 8, 34) -> 25 | 11 | 1
                                idle#_1(42, 36, 37, 43, 12, 8, 3) -> 25*
                               idle#_1(42, 36, 37, 43, 12, 2, 45) -> 1*
                               idle#_1(42, 36, 37, 43, 12, 2, 34) -> 1*
                                idle#_1(42, 36, 37, 43, 8, 2, 34) -> 1*
                                 idle#_1(42, 36, 37, 43, 8, 2, 3) -> 26 | 1
                               idle#_1(39, 36, 40, 12, 12, 8, 34) -> 25 | 11
                                idle#_1(39, 36, 40, 12, 12, 8, 3) -> 25 | 11
                               idle#_1(39, 36, 40, 12, 12, 2, 34) -> 1*
                                idle#_1(39, 36, 40, 12, 12, 2, 3) -> 1*
                               idle#_1(39, 36, 40, 8, 12, 12, 34) -> 33 | 1
                                idle#_1(39, 36, 40, 8, 12, 12, 3) -> 33 | 1
                                idle#_1(39, 36, 40, 8, 12, 2, 34) -> 15 | 1
                                 idle#_1(39, 36, 40, 8, 12, 2, 3) -> 15 | 1
                               idle#_1(39, 36, 40, 2, 12, 12, 34) -> 1*
                                idle#_1(39, 36, 40, 2, 12, 12, 3) -> 1*
                                idle#_1(39, 36, 40, 2, 12, 2, 34) -> 1*
                                 idle#_1(39, 36, 40, 2, 12, 2, 3) -> 1*
                                 idle#_1(39, 36, 40, 2, 2, 2, 34) -> 1*
                                  idle#_1(39, 36, 40, 2, 2, 2, 3) -> 27*
                              idle#_1(39, 36, 38, 41, 43, 43, 52) -> 33 | 1
                              idle#_1(39, 36, 38, 41, 43, 43, 45) -> 33 | 1
                              idle#_1(39, 36, 38, 41, 43, 43, 34) -> 33 | 1
                               idle#_1(39, 36, 38, 8, 12, 12, 34) -> 33 | 1
                                idle#_1(39, 36, 38, 8, 12, 12, 3) -> 33 | 1
                                idle#_1(39, 36, 38, 8, 12, 2, 34) -> 15 | 1
                                 idle#_1(39, 36, 38, 8, 12, 2, 3) -> 15 | 1
                               idle#_1(39, 36, 38, 2, 12, 12, 34) -> 1*
                                idle#_1(39, 36, 38, 2, 12, 12, 3) -> 1*
                                idle#_1(39, 36, 38, 2, 12, 2, 34) -> 1*
                                 idle#_1(39, 36, 38, 2, 12, 2, 3) -> 1*
                              idle#_1(39, 36, 37, 43, 43, 41, 52) -> 25 | 11
                              idle#_1(39, 36, 37, 43, 43, 41, 45) -> 25 | 11
                              idle#_1(39, 36, 37, 43, 43, 41, 34) -> 25 | 11
                               idle#_1(39, 36, 37, 12, 12, 8, 34) -> 25 | 11
                                idle#_1(39, 36, 37, 12, 12, 8, 3) -> 25 | 11
                               idle#_1(39, 36, 37, 12, 12, 2, 34) -> 1*
                                idle#_1(39, 36, 37, 12, 12, 2, 3) -> 1*
                                idle#_1(39, 36, 37, 2, 12, 2, 34) -> 1*
                                 idle#_1(39, 36, 37, 2, 12, 2, 3) -> 1*
                               idle#_1(35, 36, 40, 43, 41, 2, 52) -> 1*
                               idle#_1(35, 36, 40, 43, 41, 2, 45) -> 26 | 1
                               idle#_1(35, 36, 40, 12, 41, 2, 45) -> 26 | 1
                               idle#_1(35, 36, 40, 12, 41, 2, 34) -> 26 | 1
                                idle#_1(35, 36, 40, 12, 41, 2, 3) -> 26 | 1
                               idle#_1(35, 36, 40, 2, 41, 43, 52) -> 1*
                               idle#_1(35, 36, 40, 2, 41, 43, 45) -> 32 | 1
                               idle#_1(35, 36, 40, 2, 41, 12, 45) -> 32 | 1
                               idle#_1(35, 36, 40, 2, 41, 12, 34) -> 32 | 1
                                idle#_1(35, 36, 40, 2, 41, 12, 3) -> 32 | 1
                               idle#_1(35, 36, 38, 8, 12, 12, 34) -> 33 | 1
                                idle#_1(35, 36, 38, 8, 12, 12, 3) -> 33 | 1
                                idle#_1(35, 36, 38, 2, 8, 12, 34) -> 32 | 1
                                 idle#_1(35, 36, 38, 2, 8, 12, 3) -> 32 | 1
                                idle#_1(35, 36, 38, 2, 2, 12, 34) -> 1*
                                 idle#_1(35, 36, 38, 2, 2, 12, 3) -> 1*
                               idle#_1(35, 36, 37, 12, 12, 8, 34) -> 25*
                                idle#_1(35, 36, 37, 12, 12, 8, 3) -> 25*
                                idle#_1(35, 36, 37, 12, 8, 2, 34) -> 26 | 1
                                 idle#_1(35, 36, 37, 12, 8, 2, 3) -> 26 | 1
                                idle#_1(35, 36, 37, 12, 2, 2, 34) -> 1*
                                 idle#_1(35, 36, 37, 12, 2, 2, 3) -> 1*
                                 idle#_0(29, 6, 14, 8, 12, 12, 3) -> 1*
                                 idle#_0(29, 6, 14, 8, 12, 12, 2) -> 33*
                                  idle#_0(29, 6, 14, 2, 8, 12, 3) -> 1*
                                  idle#_0(29, 6, 14, 2, 8, 12, 2) -> 32*
                                 idle#_0(29, 6, 10, 12, 12, 8, 3) -> 25 | 11
                                 idle#_0(29, 6, 10, 12, 12, 2, 3) -> 1*
                                  idle#_0(29, 6, 10, 2, 12, 2, 3) -> 19 | 1
                                   idle#_0(29, 6, 10, 2, 2, 2, 3) -> 1*
                                   idle#_0(29, 6, 10, 2, 2, 2, 2) -> 31*
                                  idle#_0(29, 6, 7, 12, 12, 8, 3) -> 25 | 11
                                  idle#_0(29, 6, 7, 12, 12, 2, 3) -> 1*
                                   idle#_0(29, 6, 7, 2, 12, 2, 3) -> 19 | 1
                                    idle#_0(29, 6, 7, 2, 2, 8, 3) -> 1*
                                    idle#_0(29, 6, 7, 2, 2, 8, 2) -> 30*
                                    idle#_0(29, 6, 7, 2, 2, 2, 3) -> 31*
                                    idle#_0(29, 6, 7, 2, 2, 2, 2) -> 28*
                                 idle#_0(23, 6, 14, 8, 12, 12, 3) -> 33 | 1
                                  idle#_0(23, 6, 14, 8, 12, 2, 3) -> 15 | 1
                                 idle#_0(23, 6, 14, 2, 12, 12, 3) -> 1*
                                  idle#_0(23, 6, 14, 2, 12, 2, 3) -> 18 | 1
                                   idle#_0(23, 6, 14, 2, 2, 2, 3) -> 1*
                                   idle#_0(23, 6, 14, 2, 2, 2, 2) -> 27*
                                 idle#_0(23, 6, 10, 12, 12, 8, 3) -> 1*
                                 idle#_0(23, 6, 10, 12, 12, 8, 2) -> 25*
                                  idle#_0(23, 6, 10, 12, 8, 2, 3) -> 1*
                                  idle#_0(23, 6, 10, 12, 8, 2, 2) -> 26*
                                  idle#_0(23, 6, 7, 8, 12, 12, 3) -> 33 | 1
                                   idle#_0(23, 6, 7, 8, 12, 2, 3) -> 15 | 1
                                    idle#_0(23, 6, 7, 8, 2, 2, 3) -> 1*
                                    idle#_0(23, 6, 7, 8, 2, 2, 2) -> 24*
                                  idle#_0(23, 6, 7, 2, 12, 12, 3) -> 1*
                                   idle#_0(23, 6, 7, 2, 12, 2, 3) -> 18 | 1
                                    idle#_0(23, 6, 7, 2, 2, 2, 3) -> 27*
                                    idle#_0(23, 6, 7, 2, 2, 2, 2) -> 22*
                                 idle#_0(20, 6, 14, 8, 12, 12, 3) -> 33 | 1
                                  idle#_0(20, 6, 14, 2, 8, 12, 3) -> 32 | 1
                                  idle#_0(20, 6, 14, 2, 2, 12, 3) -> 1*
                                  idle#_0(20, 6, 14, 2, 2, 12, 2) -> 21*
                                 idle#_0(20, 6, 10, 12, 12, 8, 3) -> 25 | 11
                                 idle#_0(20, 6, 10, 12, 12, 2, 3) -> 1*
                                  idle#_0(20, 6, 10, 2, 12, 2, 3) -> 1*
                                  idle#_0(20, 6, 10, 2, 12, 2, 2) -> 19*
                                 idle#_0(17, 6, 14, 8, 12, 12, 3) -> 33 | 1
                                  idle#_0(17, 6, 14, 8, 12, 2, 3) -> 15 | 1
                                 idle#_0(17, 6, 14, 2, 12, 12, 3) -> 1*
                                  idle#_0(17, 6, 14, 2, 12, 2, 3) -> 1*
                                  idle#_0(17, 6, 14, 2, 12, 2, 2) -> 18*
                                 idle#_0(17, 6, 10, 12, 12, 8, 3) -> 25*
                                  idle#_0(17, 6, 10, 12, 8, 2, 3) -> 26 | 1
                                  idle#_0(17, 6, 10, 12, 2, 2, 3) -> 1*
                                  idle#_0(17, 6, 10, 12, 2, 2, 2) -> 16*
                                  idle#_0(5, 6, 14, 8, 12, 12, 3) -> 33 | 1
                                   idle#_0(5, 6, 14, 8, 12, 2, 3) -> 1*
                                   idle#_0(5, 6, 14, 8, 12, 2, 2) -> 15*
                                   idle#_0(5, 6, 14, 2, 8, 12, 3) -> 32 | 1
                                   idle#_0(5, 6, 14, 2, 2, 12, 3) -> 21 | 1
                                    idle#_0(5, 6, 14, 2, 2, 2, 3) -> 1*
                                    idle#_0(5, 6, 14, 2, 2, 2, 2) -> 13*
                                  idle#_0(5, 6, 10, 12, 12, 8, 3) -> 25*
                                  idle#_0(5, 6, 10, 12, 12, 8, 2) -> 11*
                                   idle#_0(5, 6, 10, 12, 8, 2, 3) -> 26 | 1
                                   idle#_0(5, 6, 10, 12, 2, 2, 3) -> 16 | 1
                                    idle#_0(5, 6, 10, 2, 2, 2, 3) -> 1*
                                    idle#_0(5, 6, 10, 2, 2, 2, 2) -> 9*
                                    idle#_0(5, 6, 7, 12, 8, 2, 3) -> 26 | 1
                                    idle#_0(5, 6, 7, 2, 8, 12, 3) -> 32 | 1
                                     idle#_0(5, 6, 7, 2, 8, 2, 3) -> 1*
                                     idle#_0(5, 6, 7, 2, 8, 2, 2) -> 4*
                                                            S_5() -> 79*
                                                            S_4() -> 75*
                                                            S_3() -> 59*
                                                            S_2() -> 50*
                                                            S_1() -> 39*
                                                            S_0() -> 29*
                                                        empty_6() -> 80*
                                                        empty_5() -> 72*
                                                        empty_4() -> 60*
                                                        empty_3() -> 52*
                                                        empty_2() -> 45*
                                                        empty_1() -> 34*
                                                        empty_0() -> 3*
                                                            B_5() -> 76*
                                                            B_4() -> 73*
                                                            B_3() -> 56*
                                                            B_2() -> 50*
                                                            B_1() -> 39*
                                                            B_0() -> 23*
                                                         down_4() -> 71*
                                                         down_3() -> 63*
                                                         down_2() -> 49*
                                                         down_1() -> 38*
                                                         down_0() -> 14*
                                                           up_4() -> 70*
                                                           up_3() -> 62*
                                                           up_2() -> 48*
                                                           up_1() -> 37*
                                                           up_0() -> 10*
                                                           FS_3() -> 67*
                                                           FS_2() -> 55*
                                                           FS_1() -> 44*
                                                           FS_0() -> 20*
                                                           BF_3() -> 65*
                                                           BF_2() -> 53*
                                                           BF_1() -> 42*
                                                           BF_0() -> 17*
                                                        false_3() -> 66*
                                                        false_2() -> 54*
                                                        false_1() -> 43*
                                                        false_0() -> 12*
                                                         stop_5() -> 78*
                                                         stop_4() -> 74*
                                                         stop_3() -> 58*
                                                         stop_2() -> 51*
                                                         stop_1() -> 40*
                                                         stop_0() -> 7*
                                                       closed_5() -> 77*
                                                       closed_4() -> 69*
                                                       closed_3() -> 57*
                                                       closed_2() -> 47*
                                                       closed_1() -> 36*
                                                       closed_0() -> 6*
                                                            F_4() -> 68*
                                                            F_3() -> 61*
                                                            F_2() -> 46*
                                                            F_1() -> 35*
                                                            F_0() -> 5*
                              busy#_6(79, 77, 78, 66, 66, 64, 80) -> 25 | 11
                              busy#_6(76, 77, 78, 64, 66, 66, 80) -> 33 | 1
                              busy#_5(75, 69, 74, 54, 54, 41, 72) -> 25 | 11
                               busy#_5(75, 69, 74, 54, 54, 8, 72) -> 25 | 11
                               busy#_5(75, 69, 74, 54, 54, 2, 72) -> 1*
                               busy#_5(75, 69, 74, 43, 54, 8, 72) -> 25 | 11
                              busy#_5(75, 69, 70, 66, 66, 64, 72) -> 25 | 11
                              busy#_5(73, 69, 74, 41, 54, 54, 72) -> 33 | 1
                               busy#_5(73, 69, 74, 8, 54, 54, 72) -> 33 | 1
                               busy#_5(73, 69, 74, 8, 54, 43, 72) -> 33 | 1
                               busy#_5(73, 69, 74, 2, 54, 54, 72) -> 1*
                              busy#_5(73, 69, 71, 64, 66, 66, 72) -> 33 | 1
                              busy#_5(68, 69, 71, 64, 54, 66, 72) -> 33 | 1
                              busy#_5(68, 69, 70, 66, 54, 64, 72) -> 25 | 11
                              busy#_4(67, 57, 63, 64, 54, 66, 60) -> 33 | 1
                              busy#_4(67, 57, 62, 66, 66, 64, 60) -> 25 | 11
                              busy#_4(65, 57, 63, 64, 66, 66, 60) -> 33 | 1
                              busy#_4(65, 57, 62, 66, 54, 64, 60) -> 25 | 11
                              busy#_4(61, 57, 63, 41, 43, 54, 60) -> 33 | 1
                               busy#_4(61, 57, 63, 8, 43, 54, 60) -> 33 | 1
                               busy#_4(61, 57, 63, 2, 43, 54, 60) -> 1*
                              busy#_4(61, 57, 62, 54, 43, 41, 60) -> 25 | 11
                               busy#_4(61, 57, 62, 54, 43, 8, 60) -> 25 | 11
                               busy#_4(61, 57, 62, 54, 43, 2, 60) -> 1*
                              busy#_4(59, 57, 62, 54, 54, 41, 60) -> 25 | 11
                               busy#_4(59, 57, 62, 54, 54, 8, 60) -> 25 | 11
                               busy#_4(59, 57, 62, 54, 54, 2, 60) -> 1*
                               busy#_4(59, 57, 62, 43, 54, 8, 60) -> 25 | 11
                              busy#_4(59, 57, 58, 54, 54, 64, 60) -> 25 | 11
                               busy#_4(59, 57, 58, 43, 43, 8, 60) -> 25 | 11
                               busy#_4(59, 57, 58, 43, 43, 2, 60) -> 1*
                               busy#_4(59, 57, 58, 12, 43, 8, 60) -> 25*
                              busy#_4(56, 57, 63, 41, 54, 54, 60) -> 33 | 1
                               busy#_4(56, 57, 63, 8, 54, 54, 60) -> 33 | 1
                               busy#_4(56, 57, 63, 8, 54, 43, 60) -> 33 | 1
                               busy#_4(56, 57, 63, 2, 54, 54, 60) -> 1*
                              busy#_4(56, 57, 58, 64, 54, 54, 60) -> 33 | 1
                               busy#_4(56, 57, 58, 8, 43, 43, 60) -> 33 | 1
                               busy#_4(56, 57, 58, 8, 43, 12, 60) -> 33 | 1
                                busy#_4(56, 57, 58, 8, 43, 2, 60) -> 1*
                               busy#_4(56, 57, 58, 2, 43, 43, 60) -> 1*
                               busy#_3(59, 57, 58, 12, 43, 8, 52) -> 25 | 11
                               busy#_3(56, 57, 58, 8, 43, 12, 52) -> 33 | 1
                                busy#_3(56, 57, 58, 8, 43, 2, 52) -> 15 | 1
                              busy#_3(55, 47, 49, 41, 43, 54, 52) -> 33 | 1
                               busy#_3(55, 47, 49, 8, 43, 54, 52) -> 33 | 1
                               busy#_3(55, 47, 49, 2, 43, 54, 52) -> 1*
                              busy#_3(55, 47, 48, 54, 54, 41, 52) -> 25 | 11
                               busy#_3(55, 47, 48, 54, 54, 8, 52) -> 25 | 11
                               busy#_3(55, 47, 48, 54, 54, 2, 52) -> 1*
                               busy#_3(55, 47, 48, 43, 54, 8, 52) -> 25 | 11
                              busy#_3(53, 47, 49, 41, 54, 54, 52) -> 33 | 1
                               busy#_3(53, 47, 49, 8, 54, 54, 52) -> 33 | 1
                               busy#_3(53, 47, 49, 8, 54, 43, 52) -> 33 | 1
                               busy#_3(53, 47, 49, 2, 54, 54, 52) -> 1*
                              busy#_3(53, 47, 48, 54, 43, 41, 52) -> 25 | 11
                               busy#_3(53, 47, 48, 54, 43, 8, 52) -> 25 | 11
                               busy#_3(53, 47, 48, 54, 43, 2, 52) -> 1*
                              busy#_3(50, 47, 51, 43, 43, 41, 52) -> 25 | 11
                              busy#_3(50, 47, 51, 41, 43, 43, 52) -> 33 | 1
                               busy#_3(50, 47, 51, 12, 12, 8, 52) -> 25 | 11
                               busy#_3(50, 47, 51, 12, 12, 2, 52) -> 1*
                               busy#_3(50, 47, 51, 8, 12, 12, 52) -> 33 | 1
                                busy#_3(50, 47, 51, 8, 12, 2, 52) -> 15 | 1
                               busy#_3(50, 47, 51, 2, 12, 12, 52) -> 1*
                                busy#_3(50, 47, 51, 2, 12, 2, 52) -> 1*
                              busy#_3(50, 47, 49, 64, 54, 54, 52) -> 33 | 1
                               busy#_3(50, 47, 49, 8, 43, 43, 52) -> 33 | 1
                               busy#_3(50, 47, 49, 8, 43, 12, 52) -> 33 | 1
                                busy#_3(50, 47, 49, 8, 43, 2, 52) -> 1*
                               busy#_3(50, 47, 49, 2, 43, 43, 52) -> 1*
                              busy#_3(50, 47, 48, 54, 54, 64, 52) -> 25 | 11
                               busy#_3(50, 47, 48, 43, 43, 8, 52) -> 25 | 11
                               busy#_3(50, 47, 48, 43, 43, 2, 52) -> 1*
                               busy#_3(50, 47, 48, 12, 43, 8, 52) -> 25*
                               busy#_3(46, 47, 49, 8, 43, 43, 52) -> 33 | 1
                               busy#_3(46, 47, 49, 8, 12, 43, 52) -> 33 | 1
                               busy#_3(46, 47, 49, 2, 12, 43, 52) -> 1*
                                busy#_3(46, 47, 49, 2, 8, 43, 52) -> 1*
                               busy#_3(46, 47, 48, 43, 43, 8, 52) -> 25 | 11
                               busy#_3(46, 47, 48, 43, 12, 8, 52) -> 25 | 11 | 1
                               busy#_3(46, 47, 48, 43, 12, 2, 52) -> 1*
                                busy#_3(46, 47, 48, 43, 8, 2, 52) -> 1*
                               busy#_2(50, 47, 51, 12, 12, 8, 45) -> 25 | 11
                               busy#_2(50, 47, 51, 12, 12, 2, 45) -> 1*
                               busy#_2(50, 47, 51, 8, 12, 12, 45) -> 33 | 1
                                busy#_2(50, 47, 51, 8, 12, 2, 45) -> 15 | 1
                               busy#_2(50, 47, 51, 2, 12, 12, 45) -> 1*
                                busy#_2(50, 47, 51, 2, 12, 2, 45) -> 1*
                               busy#_2(50, 47, 49, 8, 43, 12, 45) -> 33 | 1
                                busy#_2(50, 47, 49, 8, 43, 2, 45) -> 15 | 1
                               busy#_2(50, 47, 48, 12, 43, 8, 45) -> 25 | 11
                               busy#_2(46, 47, 49, 8, 12, 43, 45) -> 33 | 1
                                busy#_2(46, 47, 49, 2, 8, 43, 45) -> 32 | 1
                               busy#_2(46, 47, 48, 43, 12, 8, 45) -> 25*
                                busy#_2(46, 47, 48, 43, 8, 2, 45) -> 26 | 1
                               busy#_2(44, 36, 38, 8, 43, 43, 45) -> 33 | 1
                               busy#_2(44, 36, 38, 8, 12, 43, 45) -> 33 | 1
                               busy#_2(44, 36, 38, 2, 12, 43, 45) -> 1*
                                busy#_2(44, 36, 38, 2, 8, 43, 45) -> 1*
                               busy#_2(44, 36, 37, 43, 43, 8, 45) -> 25 | 11
                               busy#_2(44, 36, 37, 43, 43, 2, 45) -> 1*
                               busy#_2(44, 36, 37, 12, 43, 8, 45) -> 25*
                               busy#_2(42, 36, 38, 8, 43, 43, 45) -> 33 | 1
                               busy#_2(42, 36, 38, 8, 43, 12, 45) -> 33 | 1
                                busy#_2(42, 36, 38, 8, 43, 2, 45) -> 1*
                               busy#_2(42, 36, 38, 2, 43, 43, 45) -> 1*
                               busy#_2(42, 36, 37, 43, 43, 8, 45) -> 25 | 11
                               busy#_2(42, 36, 37, 43, 12, 8, 45) -> 25 | 11 | 1
                               busy#_2(42, 36, 37, 43, 12, 2, 45) -> 1*
                                busy#_2(42, 36, 37, 43, 8, 2, 45) -> 1*
                               busy#_2(39, 36, 40, 12, 12, 8, 45) -> 25 | 11
                               busy#_2(39, 36, 40, 12, 12, 2, 45) -> 1*
                               busy#_2(39, 36, 40, 8, 12, 12, 45) -> 33 | 1
                                busy#_2(39, 36, 40, 8, 12, 2, 45) -> 15 | 1
                               busy#_2(39, 36, 40, 2, 12, 12, 45) -> 1*
                                busy#_2(39, 36, 40, 2, 12, 2, 45) -> 1*
                                 busy#_2(39, 36, 40, 2, 2, 2, 45) -> 1*
                              busy#_2(39, 36, 38, 41, 43, 43, 45) -> 33 | 1
                               busy#_2(39, 36, 38, 8, 12, 12, 45) -> 33 | 1
                                busy#_2(39, 36, 38, 8, 12, 2, 45) -> 15 | 1
                               busy#_2(39, 36, 38, 2, 12, 12, 45) -> 1*
                                busy#_2(39, 36, 38, 2, 12, 2, 45) -> 1*
                              busy#_2(39, 36, 37, 43, 43, 41, 45) -> 25 | 11
                               busy#_2(39, 36, 37, 12, 12, 8, 45) -> 25 | 11
                               busy#_2(39, 36, 37, 12, 12, 2, 45) -> 1*
                                busy#_2(39, 36, 37, 2, 12, 2, 45) -> 1*
                               busy#_2(35, 36, 40, 43, 41, 2, 45) -> 26 | 1
                               busy#_2(35, 36, 40, 12, 41, 2, 45) -> 26 | 1
                               busy#_2(35, 36, 40, 2, 41, 43, 45) -> 32 | 1
                               busy#_2(35, 36, 40, 2, 41, 12, 45) -> 32 | 1
                               busy#_2(35, 36, 38, 8, 12, 12, 45) -> 33 | 1
                                busy#_2(35, 36, 38, 2, 8, 12, 45) -> 32 | 1
                                busy#_2(35, 36, 38, 2, 2, 12, 45) -> 1*
                               busy#_2(35, 36, 37, 12, 12, 8, 45) -> 25*
                                busy#_2(35, 36, 37, 12, 8, 2, 45) -> 26 | 1
                                busy#_2(35, 36, 37, 12, 2, 2, 45) -> 1*
                               busy#_1(44, 36, 38, 8, 12, 43, 34) -> 33 | 1
                                busy#_1(44, 36, 38, 2, 8, 43, 34) -> 32 | 1
                               busy#_1(44, 36, 37, 12, 43, 8, 34) -> 25 | 11
                               busy#_1(42, 36, 38, 8, 43, 12, 34) -> 33 | 1
                                busy#_1(42, 36, 38, 8, 43, 2, 34) -> 15 | 1
                               busy#_1(42, 36, 37, 43, 12, 8, 34) -> 25*
                                busy#_1(42, 36, 37, 43, 8, 2, 34) -> 26 | 1
                               busy#_1(39, 36, 40, 12, 12, 8, 34) -> 25 | 11
                               busy#_1(39, 36, 40, 12, 12, 2, 34) -> 1*
                               busy#_1(39, 36, 40, 8, 12, 12, 34) -> 33 | 1
                                busy#_1(39, 36, 40, 8, 12, 2, 34) -> 15 | 1
                               busy#_1(39, 36, 40, 2, 12, 12, 34) -> 1*
                                busy#_1(39, 36, 40, 2, 12, 2, 34) -> 1*
                                 busy#_1(39, 36, 40, 2, 2, 2, 34) -> 27*
                               busy#_1(39, 36, 38, 8, 12, 12, 34) -> 33 | 1
                                busy#_1(39, 36, 38, 8, 12, 2, 34) -> 15 | 1
                               busy#_1(39, 36, 38, 2, 12, 12, 34) -> 1*
                                busy#_1(39, 36, 38, 2, 12, 2, 34) -> 1*
                               busy#_1(39, 36, 37, 12, 12, 8, 34) -> 25 | 11
                               busy#_1(39, 36, 37, 12, 12, 2, 34) -> 1*
                                busy#_1(39, 36, 37, 2, 12, 2, 34) -> 1*
                               busy#_1(35, 36, 40, 12, 41, 2, 34) -> 26 | 1
                               busy#_1(35, 36, 40, 2, 41, 12, 34) -> 32 | 1
                               busy#_1(35, 36, 38, 8, 12, 12, 34) -> 33 | 1
                                busy#_1(35, 36, 38, 2, 8, 12, 34) -> 32 | 1
                                busy#_1(35, 36, 38, 2, 2, 12, 34) -> 1*
                               busy#_1(35, 36, 37, 12, 12, 8, 34) -> 25*
                                busy#_1(35, 36, 37, 12, 8, 2, 34) -> 26 | 1
                                busy#_1(35, 36, 37, 12, 2, 2, 34) -> 1*
                                busy#_1(29, 6, 14, 8, 12, 12, 34) -> 1*
                                 busy#_1(29, 6, 14, 2, 8, 12, 34) -> 1*
                                busy#_1(29, 6, 10, 12, 12, 8, 34) -> 25 | 11
                                busy#_1(29, 6, 10, 12, 12, 2, 34) -> 1*
                                 busy#_1(29, 6, 10, 2, 12, 2, 34) -> 1*
                                  busy#_1(29, 6, 10, 2, 2, 2, 34) -> 1*
                                 busy#_1(29, 6, 7, 12, 12, 8, 34) -> 25 | 11
                                 busy#_1(29, 6, 7, 12, 12, 2, 34) -> 1*
                                  busy#_1(29, 6, 7, 2, 12, 2, 34) -> 1*
                                   busy#_1(29, 6, 7, 2, 2, 8, 34) -> 1*
                                   busy#_1(29, 6, 7, 2, 2, 2, 34) -> 31*
                                busy#_1(23, 6, 14, 8, 12, 12, 34) -> 33 | 1
                                 busy#_1(23, 6, 14, 8, 12, 2, 34) -> 15 | 1
                                busy#_1(23, 6, 14, 2, 12, 12, 34) -> 1*
                                 busy#_1(23, 6, 14, 2, 12, 2, 34) -> 1*
                                  busy#_1(23, 6, 14, 2, 2, 2, 34) -> 1*
                                busy#_1(23, 6, 10, 12, 12, 8, 34) -> 1*
                                 busy#_1(23, 6, 10, 12, 8, 2, 34) -> 1*
                                 busy#_1(23, 6, 7, 8, 12, 12, 34) -> 33 | 1
                                  busy#_1(23, 6, 7, 8, 12, 2, 34) -> 15 | 1
                                   busy#_1(23, 6, 7, 8, 2, 2, 34) -> 1*
                                 busy#_1(23, 6, 7, 2, 12, 12, 34) -> 1*
                                  busy#_1(23, 6, 7, 2, 12, 2, 34) -> 1*
                                   busy#_1(23, 6, 7, 2, 2, 2, 34) -> 27*
                                busy#_1(20, 6, 14, 8, 12, 12, 34) -> 33 | 1
                                 busy#_1(20, 6, 14, 2, 8, 12, 34) -> 32 | 1
                                 busy#_1(20, 6, 14, 2, 2, 12, 34) -> 1*
                                busy#_1(20, 6, 10, 12, 12, 8, 34) -> 25 | 11
                                busy#_1(20, 6, 10, 12, 12, 2, 34) -> 1*
                                 busy#_1(20, 6, 10, 2, 12, 2, 34) -> 1*
                                busy#_1(17, 6, 14, 8, 12, 12, 34) -> 33 | 1
                                 busy#_1(17, 6, 14, 8, 12, 2, 34) -> 15 | 1
                                busy#_1(17, 6, 14, 2, 12, 12, 34) -> 1*
                                 busy#_1(17, 6, 14, 2, 12, 2, 34) -> 1*
                                busy#_1(17, 6, 10, 12, 12, 8, 34) -> 25*
                                 busy#_1(17, 6, 10, 12, 8, 2, 34) -> 26 | 1
                                 busy#_1(17, 6, 10, 12, 2, 2, 34) -> 1*
                                 busy#_1(5, 6, 14, 8, 12, 12, 34) -> 33 | 1
                                  busy#_1(5, 6, 14, 8, 12, 2, 34) -> 1*
                                  busy#_1(5, 6, 14, 2, 8, 12, 34) -> 32 | 1
                                  busy#_1(5, 6, 14, 2, 2, 12, 34) -> 1*
                                   busy#_1(5, 6, 14, 2, 2, 2, 34) -> 1*
                                 busy#_1(5, 6, 10, 12, 12, 8, 34) -> 25*
                                  busy#_1(5, 6, 10, 12, 8, 2, 34) -> 26 | 1
                                  busy#_1(5, 6, 10, 12, 2, 2, 34) -> 1*
                                   busy#_1(5, 6, 10, 2, 2, 2, 34) -> 1*
                                   busy#_1(5, 6, 7, 12, 8, 2, 34) -> 26 | 1
                                   busy#_1(5, 6, 7, 2, 8, 12, 34) -> 32 | 1
                                    busy#_1(5, 6, 7, 2, 8, 2, 34) -> 1*
                                 busy#_0(29, 6, 14, 8, 12, 12, 3) -> 33 | 1
                                  busy#_0(29, 6, 14, 2, 8, 12, 3) -> 32 | 1
                                 busy#_0(29, 6, 10, 12, 12, 8, 3) -> 25 | 11
                                 busy#_0(29, 6, 10, 12, 12, 2, 3) -> 1*
                                  busy#_0(29, 6, 10, 2, 12, 2, 3) -> 19 | 1
                                   busy#_0(29, 6, 10, 2, 2, 2, 3) -> 31*
                                  busy#_0(29, 6, 7, 12, 12, 8, 3) -> 25 | 11
                                  busy#_0(29, 6, 7, 12, 12, 2, 3) -> 1*
                                   busy#_0(29, 6, 7, 2, 12, 2, 3) -> 19 | 1
                                    busy#_0(29, 6, 7, 2, 2, 8, 3) -> 30 | 1
                                    busy#_0(29, 6, 7, 2, 2, 2, 3) -> 31 | 28
                                 busy#_0(23, 6, 14, 8, 12, 12, 3) -> 33 | 1
                                  busy#_0(23, 6, 14, 8, 12, 2, 3) -> 15 | 1
                                 busy#_0(23, 6, 14, 2, 12, 12, 3) -> 1*
                                  busy#_0(23, 6, 14, 2, 12, 2, 3) -> 18 | 1
                                   busy#_0(23, 6, 14, 2, 2, 2, 3) -> 27*
                                 busy#_0(23, 6, 10, 12, 12, 8, 3) -> 25*
                                  busy#_0(23, 6, 10, 12, 8, 2, 3) -> 26 | 1
                                  busy#_0(23, 6, 7, 8, 12, 12, 3) -> 33 | 1
                                   busy#_0(23, 6, 7, 8, 12, 2, 3) -> 15 | 1
                                    busy#_0(23, 6, 7, 8, 2, 2, 3) -> 24 | 1
                                  busy#_0(23, 6, 7, 2, 12, 12, 3) -> 1*
                                   busy#_0(23, 6, 7, 2, 12, 2, 3) -> 18 | 1
                                    busy#_0(23, 6, 7, 2, 2, 2, 3) -> 27 | 22
                                 busy#_0(20, 6, 14, 8, 12, 12, 3) -> 33 | 1
                                  busy#_0(20, 6, 14, 2, 8, 12, 3) -> 32 | 1
                                  busy#_0(20, 6, 14, 2, 2, 12, 3) -> 21 | 1
                                 busy#_0(20, 6, 10, 12, 12, 8, 3) -> 25 | 11
                                 busy#_0(20, 6, 10, 12, 12, 2, 3) -> 1*
                                  busy#_0(20, 6, 10, 2, 12, 2, 3) -> 19 | 1
                                 busy#_0(17, 6, 14, 8, 12, 12, 3) -> 33 | 1
                                  busy#_0(17, 6, 14, 8, 12, 2, 3) -> 15 | 1
                                 busy#_0(17, 6, 14, 2, 12, 12, 3) -> 1*
                                  busy#_0(17, 6, 14, 2, 12, 2, 3) -> 18 | 1
                                 busy#_0(17, 6, 10, 12, 12, 8, 3) -> 25*
                                  busy#_0(17, 6, 10, 12, 8, 2, 3) -> 26 | 1
                                  busy#_0(17, 6, 10, 12, 2, 2, 3) -> 16 | 1
                                  busy#_0(5, 6, 14, 8, 12, 12, 3) -> 33 | 1
                                   busy#_0(5, 6, 14, 8, 12, 2, 3) -> 15 | 1
                                   busy#_0(5, 6, 14, 2, 8, 12, 3) -> 32 | 1
                                   busy#_0(5, 6, 14, 2, 2, 12, 3) -> 21 | 1
                                    busy#_0(5, 6, 14, 2, 2, 2, 3) -> 13 | 1
                                  busy#_0(5, 6, 10, 12, 12, 8, 3) -> 25 | 11
                                   busy#_0(5, 6, 10, 12, 8, 2, 3) -> 26 | 1
                                   busy#_0(5, 6, 10, 12, 2, 2, 3) -> 16 | 1
                                    busy#_0(5, 6, 10, 2, 2, 2, 3) -> 9 | 1
                                    busy#_0(5, 6, 7, 12, 8, 2, 3) -> 26 | 1
                                    busy#_0(5, 6, 7, 2, 8, 12, 3) -> 32 | 1
                                     busy#_0(5, 6, 7, 2, 8, 2, 3) -> 4 | 1
                                     busy#_0(2, 2, 2, 2, 2, 2, 3) -> 1*
                                                               31 -> 1*
                                                               27 -> 1*
                                                               25 -> 1*
                                                                1 -> 31 | 28 | 27 | 22 | 21 | 19 | 18 | 16 | 13 | 9
                             }
                            Strict:
                             {}
                            Qed