YES TRS: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), start(i) -> busy(F(), closed(), stop(), false(), false(), false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} RUF: Strict: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} Weak: {} DP: Strict: { busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)} Weak: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} EDG: { (busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i)) (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i))) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i))) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i))) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i)) (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) } SCCS: Scc: { busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)} SCC: Strict: { busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)} Weak: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} SPSC: Simple Projection: pi(idle#) = 6, pi(busy#) = 6 Strict: { busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} EDG: {(idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i)) (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))} SCCS: Scc: { busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} SCC: Strict: { busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} Weak: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} POLY: Argument Filtering: pi(or) = [], pi(true) = [], pi(newbuttons) = [], pi(idle#) = 3, pi(idle) = [], pi(S) = [], pi(empty) = [], pi(B) = [], pi(correct) = [], pi(down) = [], pi(up) = [], pi(open) = [], pi(FS) = [], pi(BF) = [], pi(incorrect) = [], pi(false) = [], pi(stop) = [], pi(closed) = [], pi(F) = [], pi(busy#) = 3, pi(busy) = [] Usable Rules: {} Interpretation: [true] = 1, [false] = 0 Strict: { busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} Weak: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} EDG: {(busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i))} SCCS: Scc: { busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} SCC: Strict: { busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} Weak: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} POLY: Argument Filtering: pi(or) = [], pi(true) = [], pi(newbuttons) = [], pi(idle#) = [2,4], pi(idle) = [], pi(S) = [], pi(empty) = [], pi(B) = [], pi(correct) = [], pi(down) = [], pi(up) = [], pi(open) = [], pi(FS) = [], pi(BF) = [], pi(incorrect) = [], pi(false) = [], pi(stop) = [], pi(closed) = [], pi(F) = [], pi(busy#) = 4, pi(busy) = [] Usable Rules: {} Interpretation: [idle#](x0, x1) = x0 + x1, [true] = 1, [down] = 0, [up] = 0, [false] = 0, [stop] = 0 Strict: {busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} Weak: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} EDG: {(busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i)) (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))} SCCS: Scc: {busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} SCC: Strict: {busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} Weak: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} POLY: Argument Filtering: pi(or) = [], pi(true) = [], pi(newbuttons) = [], pi(idle#) = 5, pi(idle) = [], pi(S) = [], pi(empty) = [], pi(B) = [], pi(correct) = [], pi(down) = [], pi(up) = [], pi(open) = [], pi(FS) = [], pi(BF) = [], pi(incorrect) = [], pi(false) = [], pi(stop) = [], pi(closed) = [], pi(F) = [], pi(busy#) = 5, pi(busy) = [] Usable Rules: {} Interpretation: [true] = 1, [false] = 0 Strict: {busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} Weak: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} EDG: {(busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i))} SCCS: Scc: {busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} SCC: Strict: {busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} Weak: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} POLY: Argument Filtering: pi(or) = [], pi(true) = [], pi(newbuttons) = [], pi(idle#) = 1, pi(idle) = [], pi(S) = [], pi(empty) = [], pi(B) = [], pi(correct) = [], pi(down) = [], pi(up) = [], pi(open) = [], pi(FS) = [], pi(BF) = [], pi(incorrect) = [], pi(false) = [], pi(stop) = [], pi(closed) = [], pi(F) = [], pi(busy#) = 1, pi(busy) = [] Usable Rules: {} Interpretation: [open] = 1, [closed] = 0 Strict: {busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} Weak: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} EDG: {(busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i))} SCCS: Scc: {busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} SCC: Strict: {busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} Weak: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} UR: {} BOUND: Bound: match(-raise)-bounded by 6 Automaton: { a_0() -> 2* true_2() -> 64* true_1() -> 41* true_0() -> 8* idle#_5(79, 77, 78, 66, 66, 64, 72) -> 25 | 11 idle#_5(76, 77, 78, 64, 66, 66, 72) -> 33 | 1 idle#_4(75, 69, 74, 54, 54, 41, 60) -> 25 | 11 idle#_4(75, 69, 74, 54, 54, 8, 60) -> 25 | 11 idle#_4(75, 69, 74, 54, 54, 2, 60) -> 1* idle#_4(75, 69, 74, 43, 54, 8, 60) -> 25 | 11 idle#_4(75, 69, 70, 66, 66, 64, 60) -> 25 | 11 idle#_4(73, 69, 74, 41, 54, 54, 60) -> 33 | 1 idle#_4(73, 69, 74, 8, 54, 54, 60) -> 33 | 1 idle#_4(73, 69, 74, 8, 54, 43, 60) -> 33 | 1 idle#_4(73, 69, 74, 2, 54, 54, 60) -> 1* idle#_4(73, 69, 71, 64, 66, 66, 60) -> 33 | 1 idle#_4(68, 69, 71, 64, 54, 66, 60) -> 33 | 1 idle#_4(68, 69, 70, 66, 54, 64, 60) -> 25 | 11 idle#_3(67, 57, 63, 64, 54, 66, 52) -> 33 | 1 idle#_3(67, 57, 62, 66, 66, 64, 72) -> 25 | 11 idle#_3(65, 57, 63, 64, 66, 66, 72) -> 33 | 1 idle#_3(65, 57, 62, 66, 54, 64, 52) -> 25 | 11 idle#_3(61, 57, 63, 41, 43, 54, 52) -> 33 | 1 idle#_3(61, 57, 63, 8, 43, 54, 52) -> 33 | 1 idle#_3(61, 57, 63, 2, 43, 54, 52) -> 1* idle#_3(61, 57, 62, 54, 43, 41, 52) -> 25 | 11 idle#_3(61, 57, 62, 54, 43, 8, 52) -> 25 | 11 idle#_3(61, 57, 62, 54, 43, 2, 52) -> 1* idle#_3(59, 57, 62, 54, 54, 41, 52) -> 25 | 11 idle#_3(59, 57, 62, 54, 54, 8, 52) -> 25 | 11 idle#_3(59, 57, 62, 54, 54, 2, 52) -> 1* idle#_3(59, 57, 62, 43, 54, 8, 52) -> 25 | 11 idle#_3(59, 57, 58, 54, 54, 64, 52) -> 25 | 11 idle#_3(59, 57, 58, 43, 43, 8, 52) -> 25 | 11 idle#_3(59, 57, 58, 43, 43, 2, 52) -> 1* idle#_3(59, 57, 58, 12, 43, 8, 52) -> 25* idle#_3(59, 57, 58, 12, 43, 8, 45) -> 25 | 11 idle#_3(56, 57, 63, 41, 54, 54, 52) -> 33 | 1 idle#_3(56, 57, 63, 8, 54, 54, 52) -> 33 | 1 idle#_3(56, 57, 63, 8, 54, 43, 52) -> 33 | 1 idle#_3(56, 57, 63, 2, 54, 54, 52) -> 1* idle#_3(56, 57, 58, 64, 54, 54, 52) -> 33 | 1 idle#_3(56, 57, 58, 8, 43, 43, 52) -> 33 | 1 idle#_3(56, 57, 58, 8, 43, 12, 52) -> 33 | 1 idle#_3(56, 57, 58, 8, 43, 12, 45) -> 33 | 1 idle#_3(56, 57, 58, 8, 43, 2, 52) -> 1* idle#_3(56, 57, 58, 8, 43, 2, 45) -> 15 | 1 idle#_3(56, 57, 58, 2, 43, 43, 52) -> 1* idle#_2(55, 47, 49, 41, 43, 54, 45) -> 33 | 1 idle#_2(55, 47, 49, 8, 43, 54, 52) -> 33 | 1 idle#_2(55, 47, 49, 2, 43, 54, 52) -> 1* idle#_2(55, 47, 48, 54, 54, 41, 60) -> 25 | 11 idle#_2(55, 47, 48, 54, 54, 8, 60) -> 25 | 11 idle#_2(55, 47, 48, 54, 54, 2, 60) -> 1* idle#_2(55, 47, 48, 43, 54, 8, 52) -> 25 | 11 idle#_2(53, 47, 49, 41, 54, 54, 60) -> 33 | 1 idle#_2(53, 47, 49, 8, 54, 54, 60) -> 33 | 1 idle#_2(53, 47, 49, 8, 54, 43, 52) -> 33 | 1 idle#_2(53, 47, 49, 2, 54, 54, 60) -> 1* idle#_2(53, 47, 48, 54, 43, 41, 45) -> 25 | 11 idle#_2(53, 47, 48, 54, 43, 8, 52) -> 25 | 11 idle#_2(53, 47, 48, 54, 43, 2, 52) -> 1* idle#_2(50, 47, 51, 43, 43, 41, 45) -> 25 | 11 idle#_2(50, 47, 51, 41, 43, 43, 45) -> 33 | 1 idle#_2(50, 47, 51, 12, 12, 8, 45) -> 25 | 11 idle#_2(50, 47, 51, 12, 12, 8, 34) -> 25 | 11 idle#_2(50, 47, 51, 12, 12, 2, 45) -> 1* idle#_2(50, 47, 51, 12, 12, 2, 34) -> 1* idle#_2(50, 47, 51, 8, 12, 12, 45) -> 33 | 1 idle#_2(50, 47, 51, 8, 12, 12, 34) -> 33 | 1 idle#_2(50, 47, 51, 8, 12, 2, 45) -> 15 | 1 idle#_2(50, 47, 51, 8, 12, 2, 34) -> 15 | 1 idle#_2(50, 47, 51, 2, 12, 12, 45) -> 1* idle#_2(50, 47, 51, 2, 12, 12, 34) -> 1* idle#_2(50, 47, 51, 2, 12, 2, 45) -> 1* idle#_2(50, 47, 51, 2, 12, 2, 34) -> 1* idle#_2(50, 47, 49, 64, 54, 54, 52) -> 33 | 1 idle#_2(50, 47, 49, 8, 43, 43, 45) -> 33 | 1 idle#_2(50, 47, 49, 8, 43, 12, 45) -> 33 | 1 idle#_2(50, 47, 49, 8, 43, 12, 34) -> 33 | 1 idle#_2(50, 47, 49, 8, 43, 2, 45) -> 1* idle#_2(50, 47, 49, 8, 43, 2, 34) -> 15 | 1 idle#_2(50, 47, 49, 2, 43, 43, 45) -> 1* idle#_2(50, 47, 48, 54, 54, 64, 52) -> 25 | 11 idle#_2(50, 47, 48, 43, 43, 8, 45) -> 25 | 11 idle#_2(50, 47, 48, 43, 43, 2, 45) -> 1* idle#_2(50, 47, 48, 12, 43, 8, 45) -> 25* idle#_2(50, 47, 48, 12, 43, 8, 34) -> 25 | 11 idle#_2(46, 47, 49, 8, 43, 43, 45) -> 33 | 1 idle#_2(46, 47, 49, 8, 12, 43, 45) -> 33 | 1 idle#_2(46, 47, 49, 8, 12, 43, 34) -> 33 | 1 idle#_2(46, 47, 49, 2, 12, 43, 45) -> 1* idle#_2(46, 47, 49, 2, 8, 43, 45) -> 1* idle#_2(46, 47, 49, 2, 8, 43, 34) -> 32 | 1 idle#_2(46, 47, 48, 43, 43, 8, 45) -> 25 | 11 idle#_2(46, 47, 48, 43, 12, 8, 45) -> 25 | 11 | 1 idle#_2(46, 47, 48, 43, 12, 8, 34) -> 25* idle#_2(46, 47, 48, 43, 12, 2, 45) -> 1* idle#_2(46, 47, 48, 43, 8, 2, 45) -> 1* idle#_2(46, 47, 48, 43, 8, 2, 34) -> 26 | 1 idle#_1(44, 36, 38, 8, 43, 43, 52) -> 33 | 1 idle#_1(44, 36, 38, 8, 43, 43, 45) -> 33 | 1 idle#_1(44, 36, 38, 8, 12, 43, 45) -> 33 | 1 idle#_1(44, 36, 38, 8, 12, 43, 34) -> 33 | 1 idle#_1(44, 36, 38, 8, 12, 43, 3) -> 33 | 1 idle#_1(44, 36, 38, 2, 12, 43, 45) -> 1* idle#_1(44, 36, 38, 2, 12, 43, 34) -> 1* idle#_1(44, 36, 38, 2, 8, 43, 34) -> 1* idle#_1(44, 36, 38, 2, 8, 43, 3) -> 32 | 1 idle#_1(44, 36, 37, 43, 43, 8, 52) -> 25 | 11 | 1 idle#_1(44, 36, 37, 43, 43, 8, 45) -> 25* idle#_1(44, 36, 37, 43, 43, 2, 52) -> 1* idle#_1(44, 36, 37, 12, 43, 8, 45) -> 25* idle#_1(44, 36, 37, 12, 43, 8, 34) -> 25* idle#_1(44, 36, 37, 12, 43, 8, 3) -> 25 | 11 idle#_1(42, 36, 38, 8, 43, 43, 52) -> 33 | 1 idle#_1(42, 36, 38, 8, 43, 43, 45) -> 33 | 1 idle#_1(42, 36, 38, 8, 43, 12, 45) -> 33 | 1 idle#_1(42, 36, 38, 8, 43, 12, 34) -> 33 | 1 idle#_1(42, 36, 38, 8, 43, 12, 3) -> 33 | 1 idle#_1(42, 36, 38, 8, 43, 2, 34) -> 1* idle#_1(42, 36, 38, 8, 43, 2, 3) -> 15 | 1 idle#_1(42, 36, 38, 2, 43, 43, 52) -> 1* idle#_1(42, 36, 37, 43, 43, 8, 52) -> 25* idle#_1(42, 36, 37, 43, 43, 8, 45) -> 25 | 11 idle#_1(42, 36, 37, 43, 12, 8, 45) -> 25 | 11 idle#_1(42, 36, 37, 43, 12, 8, 34) -> 25 | 11 | 1 idle#_1(42, 36, 37, 43, 12, 8, 3) -> 25* idle#_1(42, 36, 37, 43, 12, 2, 45) -> 1* idle#_1(42, 36, 37, 43, 12, 2, 34) -> 1* idle#_1(42, 36, 37, 43, 8, 2, 34) -> 1* idle#_1(42, 36, 37, 43, 8, 2, 3) -> 26 | 1 idle#_1(39, 36, 40, 12, 12, 8, 34) -> 25 | 11 idle#_1(39, 36, 40, 12, 12, 8, 3) -> 25 | 11 idle#_1(39, 36, 40, 12, 12, 2, 34) -> 1* idle#_1(39, 36, 40, 12, 12, 2, 3) -> 1* idle#_1(39, 36, 40, 8, 12, 12, 34) -> 33 | 1 idle#_1(39, 36, 40, 8, 12, 12, 3) -> 33 | 1 idle#_1(39, 36, 40, 8, 12, 2, 34) -> 15 | 1 idle#_1(39, 36, 40, 8, 12, 2, 3) -> 15 | 1 idle#_1(39, 36, 40, 2, 12, 12, 34) -> 1* idle#_1(39, 36, 40, 2, 12, 12, 3) -> 1* idle#_1(39, 36, 40, 2, 12, 2, 34) -> 1* idle#_1(39, 36, 40, 2, 12, 2, 3) -> 1* idle#_1(39, 36, 40, 2, 2, 2, 34) -> 1* idle#_1(39, 36, 40, 2, 2, 2, 3) -> 27* idle#_1(39, 36, 38, 41, 43, 43, 52) -> 33 | 1 idle#_1(39, 36, 38, 41, 43, 43, 45) -> 33 | 1 idle#_1(39, 36, 38, 41, 43, 43, 34) -> 33 | 1 idle#_1(39, 36, 38, 8, 12, 12, 34) -> 33 | 1 idle#_1(39, 36, 38, 8, 12, 12, 3) -> 33 | 1 idle#_1(39, 36, 38, 8, 12, 2, 34) -> 15 | 1 idle#_1(39, 36, 38, 8, 12, 2, 3) -> 15 | 1 idle#_1(39, 36, 38, 2, 12, 12, 34) -> 1* idle#_1(39, 36, 38, 2, 12, 12, 3) -> 1* idle#_1(39, 36, 38, 2, 12, 2, 34) -> 1* idle#_1(39, 36, 38, 2, 12, 2, 3) -> 1* idle#_1(39, 36, 37, 43, 43, 41, 52) -> 25 | 11 idle#_1(39, 36, 37, 43, 43, 41, 45) -> 25 | 11 idle#_1(39, 36, 37, 43, 43, 41, 34) -> 25 | 11 idle#_1(39, 36, 37, 12, 12, 8, 34) -> 25 | 11 idle#_1(39, 36, 37, 12, 12, 8, 3) -> 25 | 11 idle#_1(39, 36, 37, 12, 12, 2, 34) -> 1* idle#_1(39, 36, 37, 12, 12, 2, 3) -> 1* idle#_1(39, 36, 37, 2, 12, 2, 34) -> 1* idle#_1(39, 36, 37, 2, 12, 2, 3) -> 1* idle#_1(35, 36, 40, 43, 41, 2, 52) -> 1* idle#_1(35, 36, 40, 43, 41, 2, 45) -> 26 | 1 idle#_1(35, 36, 40, 12, 41, 2, 45) -> 26 | 1 idle#_1(35, 36, 40, 12, 41, 2, 34) -> 26 | 1 idle#_1(35, 36, 40, 12, 41, 2, 3) -> 26 | 1 idle#_1(35, 36, 40, 2, 41, 43, 52) -> 1* idle#_1(35, 36, 40, 2, 41, 43, 45) -> 32 | 1 idle#_1(35, 36, 40, 2, 41, 12, 45) -> 32 | 1 idle#_1(35, 36, 40, 2, 41, 12, 34) -> 32 | 1 idle#_1(35, 36, 40, 2, 41, 12, 3) -> 32 | 1 idle#_1(35, 36, 38, 8, 12, 12, 34) -> 33 | 1 idle#_1(35, 36, 38, 8, 12, 12, 3) -> 33 | 1 idle#_1(35, 36, 38, 2, 8, 12, 34) -> 32 | 1 idle#_1(35, 36, 38, 2, 8, 12, 3) -> 32 | 1 idle#_1(35, 36, 38, 2, 2, 12, 34) -> 1* idle#_1(35, 36, 38, 2, 2, 12, 3) -> 1* idle#_1(35, 36, 37, 12, 12, 8, 34) -> 25* idle#_1(35, 36, 37, 12, 12, 8, 3) -> 25* idle#_1(35, 36, 37, 12, 8, 2, 34) -> 26 | 1 idle#_1(35, 36, 37, 12, 8, 2, 3) -> 26 | 1 idle#_1(35, 36, 37, 12, 2, 2, 34) -> 1* idle#_1(35, 36, 37, 12, 2, 2, 3) -> 1* idle#_0(29, 6, 14, 8, 12, 12, 3) -> 1* idle#_0(29, 6, 14, 8, 12, 12, 2) -> 33* idle#_0(29, 6, 14, 2, 8, 12, 3) -> 1* idle#_0(29, 6, 14, 2, 8, 12, 2) -> 32* idle#_0(29, 6, 10, 12, 12, 8, 3) -> 25 | 11 idle#_0(29, 6, 10, 12, 12, 2, 3) -> 1* idle#_0(29, 6, 10, 2, 12, 2, 3) -> 19 | 1 idle#_0(29, 6, 10, 2, 2, 2, 3) -> 1* idle#_0(29, 6, 10, 2, 2, 2, 2) -> 31* idle#_0(29, 6, 7, 12, 12, 8, 3) -> 25 | 11 idle#_0(29, 6, 7, 12, 12, 2, 3) -> 1* idle#_0(29, 6, 7, 2, 12, 2, 3) -> 19 | 1 idle#_0(29, 6, 7, 2, 2, 8, 3) -> 1* idle#_0(29, 6, 7, 2, 2, 8, 2) -> 30* idle#_0(29, 6, 7, 2, 2, 2, 3) -> 31* idle#_0(29, 6, 7, 2, 2, 2, 2) -> 28* idle#_0(23, 6, 14, 8, 12, 12, 3) -> 33 | 1 idle#_0(23, 6, 14, 8, 12, 2, 3) -> 15 | 1 idle#_0(23, 6, 14, 2, 12, 12, 3) -> 1* idle#_0(23, 6, 14, 2, 12, 2, 3) -> 18 | 1 idle#_0(23, 6, 14, 2, 2, 2, 3) -> 1* idle#_0(23, 6, 14, 2, 2, 2, 2) -> 27* idle#_0(23, 6, 10, 12, 12, 8, 3) -> 1* idle#_0(23, 6, 10, 12, 12, 8, 2) -> 25* idle#_0(23, 6, 10, 12, 8, 2, 3) -> 1* idle#_0(23, 6, 10, 12, 8, 2, 2) -> 26* idle#_0(23, 6, 7, 8, 12, 12, 3) -> 33 | 1 idle#_0(23, 6, 7, 8, 12, 2, 3) -> 15 | 1 idle#_0(23, 6, 7, 8, 2, 2, 3) -> 1* idle#_0(23, 6, 7, 8, 2, 2, 2) -> 24* idle#_0(23, 6, 7, 2, 12, 12, 3) -> 1* idle#_0(23, 6, 7, 2, 12, 2, 3) -> 18 | 1 idle#_0(23, 6, 7, 2, 2, 2, 3) -> 27* idle#_0(23, 6, 7, 2, 2, 2, 2) -> 22* idle#_0(20, 6, 14, 8, 12, 12, 3) -> 33 | 1 idle#_0(20, 6, 14, 2, 8, 12, 3) -> 32 | 1 idle#_0(20, 6, 14, 2, 2, 12, 3) -> 1* idle#_0(20, 6, 14, 2, 2, 12, 2) -> 21* idle#_0(20, 6, 10, 12, 12, 8, 3) -> 25 | 11 idle#_0(20, 6, 10, 12, 12, 2, 3) -> 1* idle#_0(20, 6, 10, 2, 12, 2, 3) -> 1* idle#_0(20, 6, 10, 2, 12, 2, 2) -> 19* idle#_0(17, 6, 14, 8, 12, 12, 3) -> 33 | 1 idle#_0(17, 6, 14, 8, 12, 2, 3) -> 15 | 1 idle#_0(17, 6, 14, 2, 12, 12, 3) -> 1* idle#_0(17, 6, 14, 2, 12, 2, 3) -> 1* idle#_0(17, 6, 14, 2, 12, 2, 2) -> 18* idle#_0(17, 6, 10, 12, 12, 8, 3) -> 25* idle#_0(17, 6, 10, 12, 8, 2, 3) -> 26 | 1 idle#_0(17, 6, 10, 12, 2, 2, 3) -> 1* idle#_0(17, 6, 10, 12, 2, 2, 2) -> 16* idle#_0(5, 6, 14, 8, 12, 12, 3) -> 33 | 1 idle#_0(5, 6, 14, 8, 12, 2, 3) -> 1* idle#_0(5, 6, 14, 8, 12, 2, 2) -> 15* idle#_0(5, 6, 14, 2, 8, 12, 3) -> 32 | 1 idle#_0(5, 6, 14, 2, 2, 12, 3) -> 21 | 1 idle#_0(5, 6, 14, 2, 2, 2, 3) -> 1* idle#_0(5, 6, 14, 2, 2, 2, 2) -> 13* idle#_0(5, 6, 10, 12, 12, 8, 3) -> 25* idle#_0(5, 6, 10, 12, 12, 8, 2) -> 11* idle#_0(5, 6, 10, 12, 8, 2, 3) -> 26 | 1 idle#_0(5, 6, 10, 12, 2, 2, 3) -> 16 | 1 idle#_0(5, 6, 10, 2, 2, 2, 3) -> 1* idle#_0(5, 6, 10, 2, 2, 2, 2) -> 9* idle#_0(5, 6, 7, 12, 8, 2, 3) -> 26 | 1 idle#_0(5, 6, 7, 2, 8, 12, 3) -> 32 | 1 idle#_0(5, 6, 7, 2, 8, 2, 3) -> 1* idle#_0(5, 6, 7, 2, 8, 2, 2) -> 4* S_5() -> 79* S_4() -> 75* S_3() -> 59* S_2() -> 50* S_1() -> 39* S_0() -> 29* empty_6() -> 80* empty_5() -> 72* empty_4() -> 60* empty_3() -> 52* empty_2() -> 45* empty_1() -> 34* empty_0() -> 3* B_5() -> 76* B_4() -> 73* B_3() -> 56* B_2() -> 50* B_1() -> 39* B_0() -> 23* down_4() -> 71* down_3() -> 63* down_2() -> 49* down_1() -> 38* down_0() -> 14* up_4() -> 70* up_3() -> 62* up_2() -> 48* up_1() -> 37* up_0() -> 10* FS_3() -> 67* FS_2() -> 55* FS_1() -> 44* FS_0() -> 20* BF_3() -> 65* BF_2() -> 53* BF_1() -> 42* BF_0() -> 17* false_3() -> 66* false_2() -> 54* false_1() -> 43* false_0() -> 12* stop_5() -> 78* stop_4() -> 74* stop_3() -> 58* stop_2() -> 51* stop_1() -> 40* stop_0() -> 7* closed_5() -> 77* closed_4() -> 69* closed_3() -> 57* closed_2() -> 47* closed_1() -> 36* closed_0() -> 6* F_4() -> 68* F_3() -> 61* F_2() -> 46* F_1() -> 35* F_0() -> 5* busy#_6(79, 77, 78, 66, 66, 64, 80) -> 25 | 11 busy#_6(76, 77, 78, 64, 66, 66, 80) -> 33 | 1 busy#_5(75, 69, 74, 54, 54, 41, 72) -> 25 | 11 busy#_5(75, 69, 74, 54, 54, 8, 72) -> 25 | 11 busy#_5(75, 69, 74, 54, 54, 2, 72) -> 1* busy#_5(75, 69, 74, 43, 54, 8, 72) -> 25 | 11 busy#_5(75, 69, 70, 66, 66, 64, 72) -> 25 | 11 busy#_5(73, 69, 74, 41, 54, 54, 72) -> 33 | 1 busy#_5(73, 69, 74, 8, 54, 54, 72) -> 33 | 1 busy#_5(73, 69, 74, 8, 54, 43, 72) -> 33 | 1 busy#_5(73, 69, 74, 2, 54, 54, 72) -> 1* busy#_5(73, 69, 71, 64, 66, 66, 72) -> 33 | 1 busy#_5(68, 69, 71, 64, 54, 66, 72) -> 33 | 1 busy#_5(68, 69, 70, 66, 54, 64, 72) -> 25 | 11 busy#_4(67, 57, 63, 64, 54, 66, 60) -> 33 | 1 busy#_4(67, 57, 62, 66, 66, 64, 60) -> 25 | 11 busy#_4(65, 57, 63, 64, 66, 66, 60) -> 33 | 1 busy#_4(65, 57, 62, 66, 54, 64, 60) -> 25 | 11 busy#_4(61, 57, 63, 41, 43, 54, 60) -> 33 | 1 busy#_4(61, 57, 63, 8, 43, 54, 60) -> 33 | 1 busy#_4(61, 57, 63, 2, 43, 54, 60) -> 1* busy#_4(61, 57, 62, 54, 43, 41, 60) -> 25 | 11 busy#_4(61, 57, 62, 54, 43, 8, 60) -> 25 | 11 busy#_4(61, 57, 62, 54, 43, 2, 60) -> 1* busy#_4(59, 57, 62, 54, 54, 41, 60) -> 25 | 11 busy#_4(59, 57, 62, 54, 54, 8, 60) -> 25 | 11 busy#_4(59, 57, 62, 54, 54, 2, 60) -> 1* busy#_4(59, 57, 62, 43, 54, 8, 60) -> 25 | 11 busy#_4(59, 57, 58, 54, 54, 64, 60) -> 25 | 11 busy#_4(59, 57, 58, 43, 43, 8, 60) -> 25 | 11 busy#_4(59, 57, 58, 43, 43, 2, 60) -> 1* busy#_4(59, 57, 58, 12, 43, 8, 60) -> 25* busy#_4(56, 57, 63, 41, 54, 54, 60) -> 33 | 1 busy#_4(56, 57, 63, 8, 54, 54, 60) -> 33 | 1 busy#_4(56, 57, 63, 8, 54, 43, 60) -> 33 | 1 busy#_4(56, 57, 63, 2, 54, 54, 60) -> 1* busy#_4(56, 57, 58, 64, 54, 54, 60) -> 33 | 1 busy#_4(56, 57, 58, 8, 43, 43, 60) -> 33 | 1 busy#_4(56, 57, 58, 8, 43, 12, 60) -> 33 | 1 busy#_4(56, 57, 58, 8, 43, 2, 60) -> 1* busy#_4(56, 57, 58, 2, 43, 43, 60) -> 1* busy#_3(59, 57, 58, 12, 43, 8, 52) -> 25 | 11 busy#_3(56, 57, 58, 8, 43, 12, 52) -> 33 | 1 busy#_3(56, 57, 58, 8, 43, 2, 52) -> 15 | 1 busy#_3(55, 47, 49, 41, 43, 54, 52) -> 33 | 1 busy#_3(55, 47, 49, 8, 43, 54, 52) -> 33 | 1 busy#_3(55, 47, 49, 2, 43, 54, 52) -> 1* busy#_3(55, 47, 48, 54, 54, 41, 52) -> 25 | 11 busy#_3(55, 47, 48, 54, 54, 8, 52) -> 25 | 11 busy#_3(55, 47, 48, 54, 54, 2, 52) -> 1* busy#_3(55, 47, 48, 43, 54, 8, 52) -> 25 | 11 busy#_3(53, 47, 49, 41, 54, 54, 52) -> 33 | 1 busy#_3(53, 47, 49, 8, 54, 54, 52) -> 33 | 1 busy#_3(53, 47, 49, 8, 54, 43, 52) -> 33 | 1 busy#_3(53, 47, 49, 2, 54, 54, 52) -> 1* busy#_3(53, 47, 48, 54, 43, 41, 52) -> 25 | 11 busy#_3(53, 47, 48, 54, 43, 8, 52) -> 25 | 11 busy#_3(53, 47, 48, 54, 43, 2, 52) -> 1* busy#_3(50, 47, 51, 43, 43, 41, 52) -> 25 | 11 busy#_3(50, 47, 51, 41, 43, 43, 52) -> 33 | 1 busy#_3(50, 47, 51, 12, 12, 8, 52) -> 25 | 11 busy#_3(50, 47, 51, 12, 12, 2, 52) -> 1* busy#_3(50, 47, 51, 8, 12, 12, 52) -> 33 | 1 busy#_3(50, 47, 51, 8, 12, 2, 52) -> 15 | 1 busy#_3(50, 47, 51, 2, 12, 12, 52) -> 1* busy#_3(50, 47, 51, 2, 12, 2, 52) -> 1* busy#_3(50, 47, 49, 64, 54, 54, 52) -> 33 | 1 busy#_3(50, 47, 49, 8, 43, 43, 52) -> 33 | 1 busy#_3(50, 47, 49, 8, 43, 12, 52) -> 33 | 1 busy#_3(50, 47, 49, 8, 43, 2, 52) -> 1* busy#_3(50, 47, 49, 2, 43, 43, 52) -> 1* busy#_3(50, 47, 48, 54, 54, 64, 52) -> 25 | 11 busy#_3(50, 47, 48, 43, 43, 8, 52) -> 25 | 11 busy#_3(50, 47, 48, 43, 43, 2, 52) -> 1* busy#_3(50, 47, 48, 12, 43, 8, 52) -> 25* busy#_3(46, 47, 49, 8, 43, 43, 52) -> 33 | 1 busy#_3(46, 47, 49, 8, 12, 43, 52) -> 33 | 1 busy#_3(46, 47, 49, 2, 12, 43, 52) -> 1* busy#_3(46, 47, 49, 2, 8, 43, 52) -> 1* busy#_3(46, 47, 48, 43, 43, 8, 52) -> 25 | 11 busy#_3(46, 47, 48, 43, 12, 8, 52) -> 25 | 11 | 1 busy#_3(46, 47, 48, 43, 12, 2, 52) -> 1* busy#_3(46, 47, 48, 43, 8, 2, 52) -> 1* busy#_2(50, 47, 51, 12, 12, 8, 45) -> 25 | 11 busy#_2(50, 47, 51, 12, 12, 2, 45) -> 1* busy#_2(50, 47, 51, 8, 12, 12, 45) -> 33 | 1 busy#_2(50, 47, 51, 8, 12, 2, 45) -> 15 | 1 busy#_2(50, 47, 51, 2, 12, 12, 45) -> 1* busy#_2(50, 47, 51, 2, 12, 2, 45) -> 1* busy#_2(50, 47, 49, 8, 43, 12, 45) -> 33 | 1 busy#_2(50, 47, 49, 8, 43, 2, 45) -> 15 | 1 busy#_2(50, 47, 48, 12, 43, 8, 45) -> 25 | 11 busy#_2(46, 47, 49, 8, 12, 43, 45) -> 33 | 1 busy#_2(46, 47, 49, 2, 8, 43, 45) -> 32 | 1 busy#_2(46, 47, 48, 43, 12, 8, 45) -> 25* busy#_2(46, 47, 48, 43, 8, 2, 45) -> 26 | 1 busy#_2(44, 36, 38, 8, 43, 43, 45) -> 33 | 1 busy#_2(44, 36, 38, 8, 12, 43, 45) -> 33 | 1 busy#_2(44, 36, 38, 2, 12, 43, 45) -> 1* busy#_2(44, 36, 38, 2, 8, 43, 45) -> 1* busy#_2(44, 36, 37, 43, 43, 8, 45) -> 25 | 11 busy#_2(44, 36, 37, 43, 43, 2, 45) -> 1* busy#_2(44, 36, 37, 12, 43, 8, 45) -> 25* busy#_2(42, 36, 38, 8, 43, 43, 45) -> 33 | 1 busy#_2(42, 36, 38, 8, 43, 12, 45) -> 33 | 1 busy#_2(42, 36, 38, 8, 43, 2, 45) -> 1* busy#_2(42, 36, 38, 2, 43, 43, 45) -> 1* busy#_2(42, 36, 37, 43, 43, 8, 45) -> 25 | 11 busy#_2(42, 36, 37, 43, 12, 8, 45) -> 25 | 11 | 1 busy#_2(42, 36, 37, 43, 12, 2, 45) -> 1* busy#_2(42, 36, 37, 43, 8, 2, 45) -> 1* busy#_2(39, 36, 40, 12, 12, 8, 45) -> 25 | 11 busy#_2(39, 36, 40, 12, 12, 2, 45) -> 1* busy#_2(39, 36, 40, 8, 12, 12, 45) -> 33 | 1 busy#_2(39, 36, 40, 8, 12, 2, 45) -> 15 | 1 busy#_2(39, 36, 40, 2, 12, 12, 45) -> 1* busy#_2(39, 36, 40, 2, 12, 2, 45) -> 1* busy#_2(39, 36, 40, 2, 2, 2, 45) -> 1* busy#_2(39, 36, 38, 41, 43, 43, 45) -> 33 | 1 busy#_2(39, 36, 38, 8, 12, 12, 45) -> 33 | 1 busy#_2(39, 36, 38, 8, 12, 2, 45) -> 15 | 1 busy#_2(39, 36, 38, 2, 12, 12, 45) -> 1* busy#_2(39, 36, 38, 2, 12, 2, 45) -> 1* busy#_2(39, 36, 37, 43, 43, 41, 45) -> 25 | 11 busy#_2(39, 36, 37, 12, 12, 8, 45) -> 25 | 11 busy#_2(39, 36, 37, 12, 12, 2, 45) -> 1* busy#_2(39, 36, 37, 2, 12, 2, 45) -> 1* busy#_2(35, 36, 40, 43, 41, 2, 45) -> 26 | 1 busy#_2(35, 36, 40, 12, 41, 2, 45) -> 26 | 1 busy#_2(35, 36, 40, 2, 41, 43, 45) -> 32 | 1 busy#_2(35, 36, 40, 2, 41, 12, 45) -> 32 | 1 busy#_2(35, 36, 38, 8, 12, 12, 45) -> 33 | 1 busy#_2(35, 36, 38, 2, 8, 12, 45) -> 32 | 1 busy#_2(35, 36, 38, 2, 2, 12, 45) -> 1* busy#_2(35, 36, 37, 12, 12, 8, 45) -> 25* busy#_2(35, 36, 37, 12, 8, 2, 45) -> 26 | 1 busy#_2(35, 36, 37, 12, 2, 2, 45) -> 1* busy#_1(44, 36, 38, 8, 12, 43, 34) -> 33 | 1 busy#_1(44, 36, 38, 2, 8, 43, 34) -> 32 | 1 busy#_1(44, 36, 37, 12, 43, 8, 34) -> 25 | 11 busy#_1(42, 36, 38, 8, 43, 12, 34) -> 33 | 1 busy#_1(42, 36, 38, 8, 43, 2, 34) -> 15 | 1 busy#_1(42, 36, 37, 43, 12, 8, 34) -> 25* busy#_1(42, 36, 37, 43, 8, 2, 34) -> 26 | 1 busy#_1(39, 36, 40, 12, 12, 8, 34) -> 25 | 11 busy#_1(39, 36, 40, 12, 12, 2, 34) -> 1* busy#_1(39, 36, 40, 8, 12, 12, 34) -> 33 | 1 busy#_1(39, 36, 40, 8, 12, 2, 34) -> 15 | 1 busy#_1(39, 36, 40, 2, 12, 12, 34) -> 1* busy#_1(39, 36, 40, 2, 12, 2, 34) -> 1* busy#_1(39, 36, 40, 2, 2, 2, 34) -> 27* busy#_1(39, 36, 38, 8, 12, 12, 34) -> 33 | 1 busy#_1(39, 36, 38, 8, 12, 2, 34) -> 15 | 1 busy#_1(39, 36, 38, 2, 12, 12, 34) -> 1* busy#_1(39, 36, 38, 2, 12, 2, 34) -> 1* busy#_1(39, 36, 37, 12, 12, 8, 34) -> 25 | 11 busy#_1(39, 36, 37, 12, 12, 2, 34) -> 1* busy#_1(39, 36, 37, 2, 12, 2, 34) -> 1* busy#_1(35, 36, 40, 12, 41, 2, 34) -> 26 | 1 busy#_1(35, 36, 40, 2, 41, 12, 34) -> 32 | 1 busy#_1(35, 36, 38, 8, 12, 12, 34) -> 33 | 1 busy#_1(35, 36, 38, 2, 8, 12, 34) -> 32 | 1 busy#_1(35, 36, 38, 2, 2, 12, 34) -> 1* busy#_1(35, 36, 37, 12, 12, 8, 34) -> 25* busy#_1(35, 36, 37, 12, 8, 2, 34) -> 26 | 1 busy#_1(35, 36, 37, 12, 2, 2, 34) -> 1* busy#_1(29, 6, 14, 8, 12, 12, 34) -> 1* busy#_1(29, 6, 14, 2, 8, 12, 34) -> 1* busy#_1(29, 6, 10, 12, 12, 8, 34) -> 25 | 11 busy#_1(29, 6, 10, 12, 12, 2, 34) -> 1* busy#_1(29, 6, 10, 2, 12, 2, 34) -> 1* busy#_1(29, 6, 10, 2, 2, 2, 34) -> 1* busy#_1(29, 6, 7, 12, 12, 8, 34) -> 25 | 11 busy#_1(29, 6, 7, 12, 12, 2, 34) -> 1* busy#_1(29, 6, 7, 2, 12, 2, 34) -> 1* busy#_1(29, 6, 7, 2, 2, 8, 34) -> 1* busy#_1(29, 6, 7, 2, 2, 2, 34) -> 31* busy#_1(23, 6, 14, 8, 12, 12, 34) -> 33 | 1 busy#_1(23, 6, 14, 8, 12, 2, 34) -> 15 | 1 busy#_1(23, 6, 14, 2, 12, 12, 34) -> 1* busy#_1(23, 6, 14, 2, 12, 2, 34) -> 1* busy#_1(23, 6, 14, 2, 2, 2, 34) -> 1* busy#_1(23, 6, 10, 12, 12, 8, 34) -> 1* busy#_1(23, 6, 10, 12, 8, 2, 34) -> 1* busy#_1(23, 6, 7, 8, 12, 12, 34) -> 33 | 1 busy#_1(23, 6, 7, 8, 12, 2, 34) -> 15 | 1 busy#_1(23, 6, 7, 8, 2, 2, 34) -> 1* busy#_1(23, 6, 7, 2, 12, 12, 34) -> 1* busy#_1(23, 6, 7, 2, 12, 2, 34) -> 1* busy#_1(23, 6, 7, 2, 2, 2, 34) -> 27* busy#_1(20, 6, 14, 8, 12, 12, 34) -> 33 | 1 busy#_1(20, 6, 14, 2, 8, 12, 34) -> 32 | 1 busy#_1(20, 6, 14, 2, 2, 12, 34) -> 1* busy#_1(20, 6, 10, 12, 12, 8, 34) -> 25 | 11 busy#_1(20, 6, 10, 12, 12, 2, 34) -> 1* busy#_1(20, 6, 10, 2, 12, 2, 34) -> 1* busy#_1(17, 6, 14, 8, 12, 12, 34) -> 33 | 1 busy#_1(17, 6, 14, 8, 12, 2, 34) -> 15 | 1 busy#_1(17, 6, 14, 2, 12, 12, 34) -> 1* busy#_1(17, 6, 14, 2, 12, 2, 34) -> 1* busy#_1(17, 6, 10, 12, 12, 8, 34) -> 25* busy#_1(17, 6, 10, 12, 8, 2, 34) -> 26 | 1 busy#_1(17, 6, 10, 12, 2, 2, 34) -> 1* busy#_1(5, 6, 14, 8, 12, 12, 34) -> 33 | 1 busy#_1(5, 6, 14, 8, 12, 2, 34) -> 1* busy#_1(5, 6, 14, 2, 8, 12, 34) -> 32 | 1 busy#_1(5, 6, 14, 2, 2, 12, 34) -> 1* busy#_1(5, 6, 14, 2, 2, 2, 34) -> 1* busy#_1(5, 6, 10, 12, 12, 8, 34) -> 25* busy#_1(5, 6, 10, 12, 8, 2, 34) -> 26 | 1 busy#_1(5, 6, 10, 12, 2, 2, 34) -> 1* busy#_1(5, 6, 10, 2, 2, 2, 34) -> 1* busy#_1(5, 6, 7, 12, 8, 2, 34) -> 26 | 1 busy#_1(5, 6, 7, 2, 8, 12, 34) -> 32 | 1 busy#_1(5, 6, 7, 2, 8, 2, 34) -> 1* busy#_0(29, 6, 14, 8, 12, 12, 3) -> 33 | 1 busy#_0(29, 6, 14, 2, 8, 12, 3) -> 32 | 1 busy#_0(29, 6, 10, 12, 12, 8, 3) -> 25 | 11 busy#_0(29, 6, 10, 12, 12, 2, 3) -> 1* busy#_0(29, 6, 10, 2, 12, 2, 3) -> 19 | 1 busy#_0(29, 6, 10, 2, 2, 2, 3) -> 31* busy#_0(29, 6, 7, 12, 12, 8, 3) -> 25 | 11 busy#_0(29, 6, 7, 12, 12, 2, 3) -> 1* busy#_0(29, 6, 7, 2, 12, 2, 3) -> 19 | 1 busy#_0(29, 6, 7, 2, 2, 8, 3) -> 30 | 1 busy#_0(29, 6, 7, 2, 2, 2, 3) -> 31 | 28 busy#_0(23, 6, 14, 8, 12, 12, 3) -> 33 | 1 busy#_0(23, 6, 14, 8, 12, 2, 3) -> 15 | 1 busy#_0(23, 6, 14, 2, 12, 12, 3) -> 1* busy#_0(23, 6, 14, 2, 12, 2, 3) -> 18 | 1 busy#_0(23, 6, 14, 2, 2, 2, 3) -> 27* busy#_0(23, 6, 10, 12, 12, 8, 3) -> 25* busy#_0(23, 6, 10, 12, 8, 2, 3) -> 26 | 1 busy#_0(23, 6, 7, 8, 12, 12, 3) -> 33 | 1 busy#_0(23, 6, 7, 8, 12, 2, 3) -> 15 | 1 busy#_0(23, 6, 7, 8, 2, 2, 3) -> 24 | 1 busy#_0(23, 6, 7, 2, 12, 12, 3) -> 1* busy#_0(23, 6, 7, 2, 12, 2, 3) -> 18 | 1 busy#_0(23, 6, 7, 2, 2, 2, 3) -> 27 | 22 busy#_0(20, 6, 14, 8, 12, 12, 3) -> 33 | 1 busy#_0(20, 6, 14, 2, 8, 12, 3) -> 32 | 1 busy#_0(20, 6, 14, 2, 2, 12, 3) -> 21 | 1 busy#_0(20, 6, 10, 12, 12, 8, 3) -> 25 | 11 busy#_0(20, 6, 10, 12, 12, 2, 3) -> 1* busy#_0(20, 6, 10, 2, 12, 2, 3) -> 19 | 1 busy#_0(17, 6, 14, 8, 12, 12, 3) -> 33 | 1 busy#_0(17, 6, 14, 8, 12, 2, 3) -> 15 | 1 busy#_0(17, 6, 14, 2, 12, 12, 3) -> 1* busy#_0(17, 6, 14, 2, 12, 2, 3) -> 18 | 1 busy#_0(17, 6, 10, 12, 12, 8, 3) -> 25* busy#_0(17, 6, 10, 12, 8, 2, 3) -> 26 | 1 busy#_0(17, 6, 10, 12, 2, 2, 3) -> 16 | 1 busy#_0(5, 6, 14, 8, 12, 12, 3) -> 33 | 1 busy#_0(5, 6, 14, 8, 12, 2, 3) -> 15 | 1 busy#_0(5, 6, 14, 2, 8, 12, 3) -> 32 | 1 busy#_0(5, 6, 14, 2, 2, 12, 3) -> 21 | 1 busy#_0(5, 6, 14, 2, 2, 2, 3) -> 13 | 1 busy#_0(5, 6, 10, 12, 12, 8, 3) -> 25 | 11 busy#_0(5, 6, 10, 12, 8, 2, 3) -> 26 | 1 busy#_0(5, 6, 10, 12, 2, 2, 3) -> 16 | 1 busy#_0(5, 6, 10, 2, 2, 2, 3) -> 9 | 1 busy#_0(5, 6, 7, 12, 8, 2, 3) -> 26 | 1 busy#_0(5, 6, 7, 2, 8, 12, 3) -> 32 | 1 busy#_0(5, 6, 7, 2, 8, 2, 3) -> 4 | 1 busy#_0(2, 2, 2, 2, 2, 2, 3) -> 1* 31 -> 1* 27 -> 1* 25 -> 1* 1 -> 31 | 28 | 27 | 22 | 21 | 19 | 18 | 16 | 13 | 9 } Strict: {} Qed