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