(VAR b b1 b2 b3 d fl i i1 i2 i3 m )
(STRATEGY INNERMOST)
(RULES 
        start(i) -> busy(F,closed,stop,false,false,false,i)
        busy(BF,d,stop,b1,b2,b3,i) -> incorrect
        busy(FS,d,stop,b1,b2,b3,i) -> incorrect
        busy(fl,open,up,b1,b2,b3,i) -> incorrect
        busy(fl,open,down,b1,b2,b3,i) -> incorrect
        busy(B,closed,stop,false,false,false,empty) -> correct
        busy(F,closed,stop,false,false,false,empty) -> correct
        busy(S,closed,stop,false,false,false,empty) -> correct
        busy(B,closed,stop,false,false,false,newbuttons(i1,i2,i3,i)) -> idle(B,closed,stop,false,false,false,newbuttons(i1,i2,i3,i))
        busy(F,closed,stop,false,false,false,newbuttons(i1,i2,i3,i)) -> idle(F,closed,stop,false,false,false,newbuttons(i1,i2,i3,i))
        busy(S,closed,stop,false,false,false,newbuttons(i1,i2,i3,i)) -> idle(S,closed,stop,false,false,false,newbuttons(i1,i2,i3,i))
        busy(B,open,stop,false,b2,b3,i) -> idle(B,closed,stop,false,b2,b3,i)
        busy(F,open,stop,b1,false,b3,i) -> idle(F,closed,stop,b1,false,b3,i)
        busy(S,open,stop,b1,b2,false,i) -> idle(S,closed,stop,b1,b2,false,i)
        busy(B,d,stop,true,b2,b3,i) -> idle(B,open,stop,false,b2,b3,i)
        busy(F,d,stop,b1,true,b3,i) -> idle(F,open,stop,b1,false,b3,i)
        busy(S,d,stop,b1,b2,true,i) -> idle(S,open,stop,b1,b2,false,i)
        busy(B,closed,down,b1,b2,b3,i) -> idle(B,closed,stop,b1,b2,b3,i)
        busy(S,closed,up,b1,b2,b3,i) -> idle(S,closed,stop,b1,b2,b3,i)
        busy(B,closed,up,true,b2,b3,i) -> idle(B,closed,stop,true,b2,b3,i)
        busy(F,closed,up,b1,true,b3,i) -> idle(F,closed,stop,b1,true,b3,i)
        busy(F,closed,down,b1,true,b3,i) -> idle(F,closed,stop,b1,true,b3,i)
        busy(S,closed,down,b1,b2,true,i) -> idle(S,closed,stop,b1,b2,true,i)
        busy(B,closed,up,false,b2,b3,i) -> idle(BF,closed,up,false,b2,b3,i)
        busy(F,closed,up,b1,false,b3,i) -> idle(FS,closed,up,b1,false,b3,i)
        busy(F,closed,down,b1,false,b3,i) -> idle(BF,closed,down,b1,false,b3,i)
        busy(S,closed,down,b1,b2,false,i) -> idle(FS,closed,down,b1,b2,false,i)
        busy(BF,closed,up,b1,b2,b3,i) -> idle(F,closed,up,b1,b2,b3,i)
        busy(BF,closed,down,b1,b2,b3,i) -> idle(B,closed,down,b1,b2,b3,i)
        busy(FS,closed,up,b1,b2,b3,i) -> idle(S,closed,up,b1,b2,b3,i)
        busy(FS,closed,down,b1,b2,b3,i) -> idle(F,closed,down,b1,b2,b3,i)
        busy(B,closed,stop,false,true,b3,i) -> idle(B,closed,up,false,true,b3,i)
        busy(B,closed,stop,false,false,true,i) -> idle(B,closed,up,false,false,true,i)
        busy(F,closed,stop,true,false,b3,i) -> idle(F,closed,down,true,false,b3,i)
        busy(F,closed,stop,false,false,true,i) -> idle(F,closed,up,false,false,true,i)
        busy(S,closed,stop,b1,true,false,i) -> idle(S,closed,down,b1,true,false,i)
        busy(S,closed,stop,true,false,false,i) -> idle(S,closed,down,true,false,false,i)
        idle(fl,d,m,b1,b2,b3,empty) -> busy(fl,d,m,b1,b2,b3,empty)
        idle(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i)
        or(true,b) -> true
        or(false,b) -> b
        
)