MAYBE Problem: 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 Proof: Matrix Interpretation Processor: dim=3 interpretation: [1 0 0] [1 0 1] [0] [or](x0, x1) = [0 0 0]x0 + [0 1 0]x1 + [1] [0 0 0] [1 1 1] [1], [1] [true] = [0] [0], [1 0 0] [1 0 0] [1 1 0] [1 0 0] [1 0 0] [1 0 1] [idle](x0, x1, x2, x3, x4, x5, x6) = x0 + [0 0 0]x1 + [0 1 0]x2 + [0 0 1]x3 + [0 0 0]x4 + [1 0 0]x5 + [0 1 0]x6 [0 1 0] [0 0 0] [0 0 0] [0 0 0] [0 0 0] [1 0 0] , [1 1 1] [1 0 0] [1 0 0] [1 1 0] [0] [newbuttons](x0, x1, x2, x3) = [1 1 1]x0 + [0 0 0]x1 + [1 0 1]x2 + [1 1 1]x3 + [1] [0 0 0] [0 0 1] [0 1 1] [0 0 1] [1], [0] [S] = [0] [1], [0] [correct] = [0] [1], [0] [empty] = [0] [0], [0] [B] = [0] [1], [0] [down] = [0] [0], [0] [up] = [0] [0], [0] [open] = [0] [0], [0] [FS] = [0] [1], [0] [incorrect] = [0] [0], [0] [BF] = [0] [1], [1 0 0] [1 0 0] [1 0 0] [1 1 0] [1 0 0] [1 0 0] [1 0 1] [busy](x0, x1, x2, x3, x4, x5, x6) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2 + [0 0 1]x3 + [0 0 0]x4 + [1 0 0]x5 + [0 1 0]x6 [0 0 1] [0 0 0] [0 0 0] [0 0 0] [0 0 0] [0 0 0] [1 0 0] , [0] [false] = [0] [0], [0] [stop] = [0] [0], [0] [closed] = [0] [0], [0] [F] = [0] [1], [1 1 1] [1] [start](x0) = [0 1 0]x0 + [1] [1 1 0] [1] orientation: [1 1 1] [1] [1 0 1] [0] start(i) = [0 1 0]i + [1] >= [0 1 0]i + [0] = busy(F(),closed(),stop(),false(),false(),false(),i) [1 1 0] [1] [1 0 0] [1] [1 1 0] [1 0 0] [1 0 0] [1 0 0] [1 0 1] [0] [0] busy(BF(),d,stop(),b1,b2,b3,i) = [0 0 1]b1 + [0 0 0]b2 + [1 0 0]b3 + [0 0 0]d + [0 1 0]i + [0] >= [0] = incorrect() [0 0 0] [0 0 0] [0 0 0] [0 0 0] [1 0 0] [1] [0] [1 1 0] [1 0 0] [1 0 0] [1 0 0] [1 0 1] [0] [0] busy(FS(),d,stop(),b1,b2,b3,i) = [0 0 1]b1 + [0 0 0]b2 + [1 0 0]b3 + [0 0 0]d + [0 1 0]i + [0] >= [0] = incorrect() [0 0 0] [0 0 0] [0 0 0] [0 0 0] [1 0 0] [1] [0] [1 1 0] [1 0 0] [1 0 0] [1 0 0] [1 0 1] [0] busy(fl,open(),up(),b1,b2,b3,i) = [0 0 1]b1 + [0 0 0]b2 + [1 0 0]b3 + [0 0 0]fl + [0 1 0]i >= [0] = incorrect() [0 0 0] [0 0 0] [0 0 0] [0 0 1] [1 0 0] [0] [1 1 0] [1 0 0] [1 0 0] [1 0 0] [1 0 1] [0] busy(fl,open(),down(),b1,b2,b3,i) = [0 0 1]b1 + [0 0 0]b2 + [1 0 0]b3 + [0 0 0]fl + [0 1 0]i >= [0] = incorrect() [0 0 0] [0 0 0] [0 0 0] [0 0 1] [1 0 0] [0] [0] [0] busy(B(),closed(),stop(),false(),false(),false(),empty()) = [0] >= [0] = correct() [1] [1] [0] [0] busy(F(),closed(),stop(),false(),false(),false(),empty()) = [0] >= [0] = correct() [1] [1] [0] [0] busy(S(),closed(),stop(),false(),false(),false(),empty()) = [0] >= [0] = correct() [1] [1] [1 1 1] [1 1 1] [1 0 1] [1 1 1] [1] [1 1 1] [1 1 1] [1 0 1] [1 1 1] [1] busy(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = [1 1 1]i + [1 1 1]i1 + [0 0 0]i2 + [1 0 1]i3 + [1] >= [1 1 1]i + [1 1 1]i1 + [0 0 0]i2 + [1 0 1]i3 + [1] = idle(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) [1 1 0] [1 1 1] [1 0 0] [1 0 0] [1] [1 1 0] [1 1 1] [1 0 0] [1 0 0] [1] [1 1 1] [1 1 1] [1 0 1] [1 1 1] [1] [1 1 1] [1 1 1] [1 0 1] [1 1 1] [1] busy(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = [1 1 1]i + [1 1 1]i1 + [0 0 0]i2 + [1 0 1]i3 + [1] >= [1 1 1]i + [1 1 1]i1 + [0 0 0]i2 + [1 0 1]i3 + [1] = idle(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) [1 1 0] [1 1 1] [1 0 0] [1 0 0] [1] [1 1 0] [1 1 1] [1 0 0] [1 0 0] [1] [1 1 1] [1 1 1] [1 0 1] [1 1 1] [1] [1 1 1] [1 1 1] [1 0 1] [1 1 1] [1] busy(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = [1 1 1]i + [1 1 1]i1 + [0 0 0]i2 + [1 0 1]i3 + [1] >= [1 1 1]i + [1 1 1]i1 + [0 0 0]i2 + [1 0 1]i3 + [1] = idle(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) [1 1 0] [1 1 1] [1 0 0] [1 0 0] [1] [1 1 0] [1 1 1] [1 0 0] [1 0 0] [1] [1 0 0] [1 0 0] [1 0 1] [0] [1 0 0] [1 0 0] [1 0 1] [0] busy(B(),open(),stop(),false(),b2,b3,i) = [0 0 0]b2 + [1 0 0]b3 + [0 1 0]i + [0] >= [0 0 0]b2 + [1 0 0]b3 + [0 1 0]i + [0] = idle(B(),closed(),stop(),false(),b2,b3,i) [0 0 0] [0 0 0] [1 0 0] [1] [0 0 0] [0 0 0] [1 0 0] [1] [1 1 0] [1 0 0] [1 0 1] [0] [1 1 0] [1 0 0] [1 0 1] [0] busy(F(),open(),stop(),b1,false(),b3,i) = [0 0 1]b1 + [1 0 0]b3 + [0 1 0]i + [0] >= [0 0 1]b1 + [1 0 0]b3 + [0 1 0]i + [0] = idle(F(),closed(),stop(),b1,false(),b3,i) [0 0 0] [0 0 0] [1 0 0] [1] [0 0 0] [0 0 0] [1 0 0] [1] [1 1 0] [1 0 0] [1 0 1] [0] [1 1 0] [1 0 0] [1 0 1] [0] busy(S(),open(),stop(),b1,b2,false(),i) = [0 0 1]b1 + [0 0 0]b2 + [0 1 0]i + [0] >= [0 0 1]b1 + [0 0 0]b2 + [0 1 0]i + [0] = idle(S(),closed(),stop(),b1,b2,false(),i) [0 0 0] [0 0 0] [1 0 0] [1] [0 0 0] [0 0 0] [1 0 0] [1] [1 0 0] [1 0 0] [1 0 0] [1 0 1] [1] [1 0 0] [1 0 0] [1 0 1] [0] busy(B(),d,stop(),true(),b2,b3,i) = [0 0 0]b2 + [1 0 0]b3 + [0 0 0]d + [0 1 0]i + [0] >= [0 0 0]b2 + [1 0 0]b3 + [0 1 0]i + [0] = idle(B(),open(),stop(),false(),b2,b3,i) [0 0 0] [0 0 0] [0 0 0] [1 0 0] [1] [0 0 0] [0 0 0] [1 0 0] [1] [1 1 0] [1 0 0] [1 0 0] [1 0 1] [1] [1 1 0] [1 0 0] [1 0 1] [0] busy(F(),d,stop(),b1,true(),b3,i) = [0 0 1]b1 + [1 0 0]b3 + [0 0 0]d + [0 1 0]i + [0] >= [0 0 1]b1 + [1 0 0]b3 + [0 1 0]i + [0] = idle(F(),open(),stop(),b1,false(),b3,i) [0 0 0] [0 0 0] [0 0 0] [1 0 0] [1] [0 0 0] [0 0 0] [1 0 0] [1] [1 1 0] [1 0 0] [1 0 0] [1 0 1] [1] [1 1 0] [1 0 0] [1 0 1] [0] busy(S(),d,stop(),b1,b2,true(),i) = [0 0 1]b1 + [0 0 0]b2 + [0 0 0]d + [0 1 0]i + [1] >= [0 0 1]b1 + [0 0 0]b2 + [0 1 0]i + [0] = idle(S(),open(),stop(),b1,b2,false(),i) [0 0 0] [0 0 0] [0 0 0] [1 0 0] [1] [0 0 0] [0 0 0] [1 0 0] [1] [1 1 0] [1 0 0] [1 0 0] [1 0 1] [0] [1 1 0] [1 0 0] [1 0 0] [1 0 1] [0] busy(B(),closed(),down(),b1,b2,b3,i) = [0 0 1]b1 + [0 0 0]b2 + [1 0 0]b3 + [0 1 0]i + [0] >= [0 0 1]b1 + [0 0 0]b2 + [1 0 0]b3 + [0 1 0]i + [0] = idle(B(),closed(),stop(),b1,b2,b3,i) [0 0 0] [0 0 0] [0 0 0] [1 0 0] [1] [0 0 0] [0 0 0] [0 0 0] [1 0 0] [1] [1 1 0] [1 0 0] [1 0 0] [1 0 1] [0] [1 1 0] [1 0 0] [1 0 0] [1 0 1] [0] busy(S(),closed(),up(),b1,b2,b3,i) = [0 0 1]b1 + [0 0 0]b2 + [1 0 0]b3 + [0 1 0]i + [0] >= [0 0 1]b1 + [0 0 0]b2 + [1 0 0]b3 + [0 1 0]i + [0] = idle(S(),closed(),stop(),b1,b2,b3,i) [0 0 0] [0 0 0] [0 0 0] [1 0 0] [1] [0 0 0] [0 0 0] [0 0 0] [1 0 0] [1] [1 0 0] [1 0 0] [1 0 1] [1] [1 0 0] [1 0 0] [1 0 1] [1] busy(B(),closed(),up(),true(),b2,b3,i) = [0 0 0]b2 + [1 0 0]b3 + [0 1 0]i + [0] >= [0 0 0]b2 + [1 0 0]b3 + [0 1 0]i + [0] = idle(B(),closed(),stop(),true(),b2,b3,i) [0 0 0] [0 0 0] [1 0 0] [1] [0 0 0] [0 0 0] [1 0 0] [1] [1 1 0] [1 0 0] [1 0 1] [1] [1 1 0] [1 0 0] [1 0 1] [1] busy(F(),closed(),up(),b1,true(),b3,i) = [0 0 1]b1 + [1 0 0]b3 + [0 1 0]i + [0] >= [0 0 1]b1 + [1 0 0]b3 + [0 1 0]i + [0] = idle(F(),closed(),stop(),b1,true(),b3,i) [0 0 0] [0 0 0] [1 0 0] [1] [0 0 0] [0 0 0] [1 0 0] [1] [1 1 0] [1 0 0] [1 0 1] [1] [1 1 0] [1 0 0] [1 0 1] [1] busy(F(),closed(),down(),b1,true(),b3,i) = [0 0 1]b1 + [1 0 0]b3 + [0 1 0]i + [0] >= [0 0 1]b1 + [1 0 0]b3 + [0 1 0]i + [0] = idle(F(),closed(),stop(),b1,true(),b3,i) [0 0 0] [0 0 0] [1 0 0] [1] [0 0 0] [0 0 0] [1 0 0] [1] [1 1 0] [1 0 0] [1 0 1] [1] [1 1 0] [1 0 0] [1 0 1] [1] busy(S(),closed(),down(),b1,b2,true(),i) = [0 0 1]b1 + [0 0 0]b2 + [0 1 0]i + [1] >= [0 0 1]b1 + [0 0 0]b2 + [0 1 0]i + [1] = idle(S(),closed(),stop(),b1,b2,true(),i) [0 0 0] [0 0 0] [1 0 0] [1] [0 0 0] [0 0 0] [1 0 0] [1] [1 0 0] [1 0 0] [1 0 1] [0] [1 0 0] [1 0 0] [1 0 1] [0] busy(B(),closed(),up(),false(),b2,b3,i) = [0 0 0]b2 + [1 0 0]b3 + [0 1 0]i + [0] >= [0 0 0]b2 + [1 0 0]b3 + [0 1 0]i + [0] = idle(BF(),closed(),up(),false(),b2,b3,i) [0 0 0] [0 0 0] [1 0 0] [1] [0 0 0] [0 0 0] [1 0 0] [1] [1 1 0] [1 0 0] [1 0 1] [0] [1 1 0] [1 0 0] [1 0 1] [0] busy(F(),closed(),up(),b1,false(),b3,i) = [0 0 1]b1 + [1 0 0]b3 + [0 1 0]i + [0] >= [0 0 1]b1 + [1 0 0]b3 + [0 1 0]i + [0] = idle(FS(),closed(),up(),b1,false(),b3,i) [0 0 0] [0 0 0] [1 0 0] [1] [0 0 0] [0 0 0] [1 0 0] [1] [1 1 0] [1 0 0] [1 0 1] [0] [1 1 0] [1 0 0] [1 0 1] [0] busy(F(),closed(),down(),b1,false(),b3,i) = [0 0 1]b1 + [1 0 0]b3 + [0 1 0]i + [0] >= [0 0 1]b1 + [1 0 0]b3 + [0 1 0]i + [0] = idle(BF(),closed(),down(),b1,false(),b3,i) [0 0 0] [0 0 0] [1 0 0] [1] [0 0 0] [0 0 0] [1 0 0] [1] [1 1 0] [1 0 0] [1 0 1] [0] [1 1 0] [1 0 0] [1 0 1] [0] busy(S(),closed(),down(),b1,b2,false(),i) = [0 0 1]b1 + [0 0 0]b2 + [0 1 0]i + [0] >= [0 0 1]b1 + [0 0 0]b2 + [0 1 0]i + [0] = idle(FS(),closed(),down(),b1,b2,false(),i) [0 0 0] [0 0 0] [1 0 0] [1] [0 0 0] [0 0 0] [1 0 0] [1] [1 1 0] [1 0 0] [1 0 0] [1 0 1] [0] [1 1 0] [1 0 0] [1 0 0] [1 0 1] [0] busy(BF(),closed(),up(),b1,b2,b3,i) = [0 0 1]b1 + [0 0 0]b2 + [1 0 0]b3 + [0 1 0]i + [0] >= [0 0 1]b1 + [0 0 0]b2 + [1 0 0]b3 + [0 1 0]i + [0] = idle(F(),closed(),up(),b1,b2,b3,i) [0 0 0] [0 0 0] [0 0 0] [1 0 0] [1] [0 0 0] [0 0 0] [0 0 0] [1 0 0] [1] [1 1 0] [1 0 0] [1 0 0] [1 0 1] [0] [1 1 0] [1 0 0] [1 0 0] [1 0 1] [0] busy(BF(),closed(),down(),b1,b2,b3,i) = [0 0 1]b1 + [0 0 0]b2 + [1 0 0]b3 + [0 1 0]i + [0] >= [0 0 1]b1 + [0 0 0]b2 + [1 0 0]b3 + [0 1 0]i + [0] = idle(B(),closed(),down(),b1,b2,b3,i) [0 0 0] [0 0 0] [0 0 0] [1 0 0] [1] [0 0 0] [0 0 0] [0 0 0] [1 0 0] [1] [1 1 0] [1 0 0] [1 0 0] [1 0 1] [0] [1 1 0] [1 0 0] [1 0 0] [1 0 1] [0] busy(FS(),closed(),up(),b1,b2,b3,i) = [0 0 1]b1 + [0 0 0]b2 + [1 0 0]b3 + [0 1 0]i + [0] >= [0 0 1]b1 + [0 0 0]b2 + [1 0 0]b3 + [0 1 0]i + [0] = idle(S(),closed(),up(),b1,b2,b3,i) [0 0 0] [0 0 0] [0 0 0] [1 0 0] [1] [0 0 0] [0 0 0] [0 0 0] [1 0 0] [1] [1 1 0] [1 0 0] [1 0 0] [1 0 1] [0] [1 1 0] [1 0 0] [1 0 0] [1 0 1] [0] busy(FS(),closed(),down(),b1,b2,b3,i) = [0 0 1]b1 + [0 0 0]b2 + [1 0 0]b3 + [0 1 0]i + [0] >= [0 0 1]b1 + [0 0 0]b2 + [1 0 0]b3 + [0 1 0]i + [0] = idle(F(),closed(),down(),b1,b2,b3,i) [0 0 0] [0 0 0] [0 0 0] [1 0 0] [1] [0 0 0] [0 0 0] [0 0 0] [1 0 0] [1] [1 0 0] [1 0 1] [1] [1 0 0] [1 0 1] [1] busy(B(),closed(),stop(),false(),true(),b3,i) = [1 0 0]b3 + [0 1 0]i + [0] >= [1 0 0]b3 + [0 1 0]i + [0] = idle(B(),closed(),up(),false(),true(),b3,i) [0 0 0] [1 0 0] [1] [0 0 0] [1 0 0] [1] [1 0 1] [1] [1 0 1] [1] busy(B(),closed(),stop(),false(),false(),true(),i) = [0 1 0]i + [1] >= [0 1 0]i + [1] = idle(B(),closed(),up(),false(),false(),true(),i) [1 0 0] [1] [1 0 0] [1] [1 0 0] [1 0 1] [1] [1 0 0] [1 0 1] [1] busy(F(),closed(),stop(),true(),false(),b3,i) = [1 0 0]b3 + [0 1 0]i + [0] >= [1 0 0]b3 + [0 1 0]i + [0] = idle(F(),closed(),down(),true(),false(),b3,i) [0 0 0] [1 0 0] [1] [0 0 0] [1 0 0] [1] [1 0 1] [1] [1 0 1] [1] busy(F(),closed(),stop(),false(),false(),true(),i) = [0 1 0]i + [1] >= [0 1 0]i + [1] = idle(F(),closed(),up(),false(),false(),true(),i) [1 0 0] [1] [1 0 0] [1] [1 1 0] [1 0 1] [1] [1 1 0] [1 0 1] [1] busy(S(),closed(),stop(),b1,true(),false(),i) = [0 0 1]b1 + [0 1 0]i + [0] >= [0 0 1]b1 + [0 1 0]i + [0] = idle(S(),closed(),down(),b1,true(),false(),i) [0 0 0] [1 0 0] [1] [0 0 0] [1 0 0] [1] [1 0 1] [1] [1 0 1] [1] busy(S(),closed(),stop(),true(),false(),false(),i) = [0 1 0]i + [0] >= [0 1 0]i + [0] = idle(S(),closed(),down(),true(),false(),false(),i) [1 0 0] [1] [1 0 0] [1] [1 1 0] [1 0 0] [1 0 0] [1 0 0] [1 0 0] [1 1 0] [1 0 0] [1 0 0] [1 0 0] [1 0 0] [1 0 0] idle(fl,d,m,b1,b2,b3,empty()) = [0 0 1]b1 + [0 0 0]b2 + [1 0 0]b3 + [0 0 0]d + fl + [0 1 0]m >= [0 0 1]b1 + [0 0 0]b2 + [1 0 0]b3 + [0 0 0]d + [0 0 0]fl + [0 0 0]m = busy(fl,d,m,b1,b2,b3,empty()) [0 0 0] [0 0 0] [0 0 0] [0 1 0] [0 0 0] [0 0 0] [0 0 0] [0 0 0] [0 0 0] [0 0 1] [0 0 0] [1 1 0] [1 0 0] [1 0 0] [1 0 0] [1 1 1] [1 1 1] [1 0 1] [1 1 1] [1 0 0] [1] [1 0 0] [1 0 0] [1 0 0] [1 0 0] [1 0 0] [1 0 1] [1 1 1] [1 0 1] [1 0 1] [1 0 0] [1] idle(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) = [0 0 1]b1 + [0 0 0]b2 + [1 0 0]b3 + [0 0 0]d + fl + [1 1 1]i + [1 1 1]i1 + [0 0 0]i2 + [1 0 1]i3 + [0 1 0]m + [1] >= [0 0 0]b1 + [0 0 0]b2 + [1 0 0]b3 + [0 0 0]d + [0 0 0]fl + [0 1 0]i + [1 1 1]i1 + [0 0 0]i2 + [1 0 1]i3 + [0 0 0]m + [1] = busy(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) [0 0 0] [0 0 0] [0 0 0] [0 1 0] [1 1 0] [1 1 1] [1 0 0] [1 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0 0 0] [0 0 0] [0 0 1] [1 0 0] [0 0 0] [0 0 0] [0 0 0] [0 0 0] [0] [1 0 1] [1] [1] or(true(),b) = [0 1 0]b + [1] >= [0] = true() [1 1 1] [1] [0] [1 0 1] [0] or(false(),b) = [0 1 0]b + [1] >= b = b [1 1 1] [1] problem: 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(),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 DP Processor: DPs: 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(),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)) -> or#(b3,i3) 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#(b1,i1) idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) TRS: 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(),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 TDG Processor: DPs: 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(),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)) -> or#(b3,i3) 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#(b1,i1) idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) TRS: 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(),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 graph: idle#(fl,d,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(),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#(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#(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#(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(),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#(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(),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#(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#(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(),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#(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#(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#(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(),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#(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#(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#(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#(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#(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#(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(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) -> busy#(F(),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#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) -> busy#(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#(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#(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#(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#(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#(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#(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#(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#(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#(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#(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#(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(),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#(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#(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(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) -> busy#(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) -> busy#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) busy#(S(),open(),stop(),b1,b2,false(),i) -> idle#(S(),closed(),stop(),b1,b2,false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(S(),open(),stop(),b1,b2,false(),i) -> idle#(S(),closed(),stop(),b1,b2,false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(S(),open(),stop(),b1,b2,false(),i) -> idle#(S(),closed(),stop(),b1,b2,false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(S(),open(),stop(),b1,b2,false(),i) -> idle#(S(),closed(),stop(),b1,b2,false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(S(),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,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(),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,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(S(),closed(),down(),b1,b2,false(),i) -> idle#(FS(),closed(),down(),b1,b2,false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(S(),closed(),down(),b1,b2,false(),i) -> idle#(FS(),closed(),down(),b1,b2,false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(S(),closed(),down(),b1,b2,false(),i) -> idle#(FS(),closed(),down(),b1,b2,false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(S(),closed(),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,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(),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,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(S(),closed(),stop(),true(),false(),false(),i) -> idle#(S(),closed(),down(),true(),false(),false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(S(),closed(),stop(),true(),false(),false(),i) -> idle#(S(),closed(),down(),true(),false(),false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(S(),closed(),stop(),true(),false(),false(),i) -> idle#(S(),closed(),down(),true(),false(),false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(S(),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(),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#(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(S(),closed(),stop(),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#(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,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(),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,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(B(),closed(),down(),b1,b2,b3,i) -> idle#(B(),closed(),stop(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(B(),closed(),down(),b1,b2,b3,i) -> idle#(B(),closed(),stop(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(B(),closed(),down(),b1,b2,b3,i) -> idle#(B(),closed(),stop(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(B(),closed(),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,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(),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,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(B(),closed(),up(),false(),b2,b3,i) -> idle#(BF(),closed(),up(),false(),b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(B(),closed(),up(),false(),b2,b3,i) -> idle#(BF(),closed(),up(),false(),b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(B(),closed(),up(),false(),b2,b3,i) -> idle#(BF(),closed(),up(),false(),b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(B(),closed(),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,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(),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,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(B(),closed(),stop(),false(),false(),true(),i) -> idle#(B(),closed(),up(),false(),false(),true(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(B(),closed(),stop(),false(),false(),true(),i) -> idle#(B(),closed(),up(),false(),false(),true(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(B(),closed(),stop(),false(),false(),true(),i) -> idle#(B(),closed(),up(),false(),false(),true(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(B(),closed(),stop(),false(),false(),true(),i) -> idle#(B(),closed(),up(),false(),false(),true(),i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(FS(),closed(),down(),b1,b2,b3,i) -> idle#(F(),closed(),down(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(FS(),closed(),down(),b1,b2,b3,i) -> idle#(F(),closed(),down(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(FS(),closed(),down(),b1,b2,b3,i) -> idle#(F(),closed(),down(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(FS(),closed(),down(),b1,b2,b3,i) -> idle#(F(),closed(),down(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(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,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#(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,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(BF(),closed(),down(),b1,b2,b3,i) -> idle#(B(),closed(),down(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(BF(),closed(),down(),b1,b2,b3,i) -> idle#(B(),closed(),down(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(BF(),closed(),down(),b1,b2,b3,i) -> idle#(B(),closed(),down(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(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,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#(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,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(F(),open(),stop(),b1,false(),b3,i) -> idle#(F(),closed(),stop(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(F(),open(),stop(),b1,false(),b3,i) -> idle#(F(),closed(),stop(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(F(),open(),stop(),b1,false(),b3,i) -> idle#(F(),closed(),stop(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(F(),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,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(),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,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(F(),closed(),down(),b1,false(),b3,i) -> idle#(BF(),closed(),down(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(F(),closed(),down(),b1,false(),b3,i) -> idle#(BF(),closed(),down(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(F(),closed(),down(),b1,false(),b3,i) -> idle#(BF(),closed(),down(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(F(),closed(),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,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(),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,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(F(),closed(),up(),b1,false(),b3,i) -> idle#(FS(),closed(),up(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(F(),closed(),up(),b1,false(),b3,i) -> idle#(FS(),closed(),up(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(F(),closed(),up(),b1,false(),b3,i) -> idle#(FS(),closed(),up(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(F(),closed(),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,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(),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,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(F(),closed(),stop(),false(),false(),true(),i) -> idle#(F(),closed(),up(),false(),false(),true(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(F(),closed(),stop(),false(),false(),true(),i) -> idle#(F(),closed(),up(),false(),false(),true(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(F(),closed(),stop(),false(),false(),true(),i) -> idle#(F(),closed(),up(),false(),false(),true(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(F(),closed(),stop(),false(),false(),true(),i) -> idle#(F(),closed(),up(),false(),false(),true(),i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(F(),closed(),stop(),false(),false(),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) busy#(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) SCC Processor: #sccs: 1 #rules: 28 #arcs: 182/961 DPs: idle#(fl,d,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,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) 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(),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) TRS: 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(),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 Subterm Criterion Processor: simple projection: pi(busy#) = 6 pi(idle#) = 6 problem: DPs: busy#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(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(),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) TRS: 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(),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 EDG Processor: DPs: busy#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(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(),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) TRS: 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(),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 graph: 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#(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#(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#(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(),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#(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#(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#(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#(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#(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#(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#(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(),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#(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#(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) 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#(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#(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()) SCC Processor: #sccs: 1 #rules: 24 #arcs: 46/729 DPs: 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) busy#(S(),closed(),stop(),b1,true(),false(),i) -> idle#(S(),closed(),down(),b1,true(),false(),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#(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#(FS(),closed(),down(),b1,b2,b3,i) -> idle#(F(),closed(),down(),b1,b2,b3,i) busy#(FS(),closed(),up(),b1,b2,b3,i) -> idle#(S(),closed(),up(),b1,b2,b3,i) busy#(BF(),closed(),down(),b1,b2,b3,i) -> idle#(B(),closed(),down(),b1,b2,b3,i) busy#(BF(),closed(),up(),b1,b2,b3,i) -> idle#(F(),closed(),up(),b1,b2,b3,i) busy#(S(),closed(),down(),b1,b2,false(),i) -> idle#(FS(),closed(),down(),b1,b2,false(),i) busy#(F(),closed(),down(),b1,false(),b3,i) -> idle#(BF(),closed(),down(),b1,false(),b3,i) busy#(F(),closed(),up(),b1,false(),b3,i) -> idle#(FS(),closed(),up(),b1,false(),b3,i) busy#(B(),closed(),up(),false(),b2,b3,i) -> idle#(BF(),closed(),up(),false(),b2,b3,i) busy#(S(),closed(),down(),b1,b2,true(),i) -> idle#(S(),closed(),stop(),b1,b2,true(),i) busy#(F(),closed(),down(),b1,true(),b3,i) -> idle#(F(),closed(),stop(),b1,true(),b3,i) busy#(F(),closed(),up(),b1,true(),b3,i) -> idle#(F(),closed(),stop(),b1,true(),b3,i) busy#(B(),closed(),up(),true(),b2,b3,i) -> idle#(B(),closed(),stop(),true(),b2,b3,i) busy#(S(),closed(),up(),b1,b2,b3,i) -> idle#(S(),closed(),stop(),b1,b2,b3,i) busy#(B(),closed(),down(),b1,b2,b3,i) -> idle#(B(),closed(),stop(),b1,b2,b3,i) busy#(S(),open(),stop(),b1,b2,false(),i) -> idle#(S(),closed(),stop(),b1,b2,false(),i) busy#(F(),open(),stop(),b1,false(),b3,i) -> idle#(F(),closed(),stop(),b1,false(),b3,i) busy#(B(),open(),stop(),false(),b2,b3,i) -> idle#(B(),closed(),stop(),false(),b2,b3,i) TRS: 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(),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 Matrix Interpretation Processor: dim=1 interpretation: [idle#](x0, x1, x2, x3, x4, x5, x6) = 5x1 + 4x4, [busy#](x0, x1, x2, x3, x4, x5, x6) = 5x1 + 4x4, [or](x0, x1) = x0 + 2x1 + 1, [true] = 5, [idle](x0, x1, x2, x3, x4, x5, x6) = x4 + x6 + 3, [newbuttons](x0, x1, x2, x3) = 4x0 + 3x1 + 4x2 + 6x3 + 1, [S] = 0, [correct] = 3, [empty] = 0, [B] = 0, [down] = 0, [up] = 0, [open] = 6, [FS] = 0, [incorrect] = 0, [BF] = 0, [busy](x0, x1, x2, x3, x4, x5, x6) = x4 + x6 + 3, [false] = 0, [stop] = 0, [closed] = 0, [F] = 0 orientation: idle#(fl,d,m,b1,b2,b3,empty()) = 4b2 + 5d >= 4b2 + 5d = busy#(fl,d,m,b1,b2,b3,empty()) busy#(S(),closed(),stop(),true(),false(),false(),i) = 0 >= 0 = idle#(S(),closed(),down(),true(),false(),false(),i) busy#(S(),closed(),stop(),b1,true(),false(),i) = 20 >= 20 = idle#(S(),closed(),down(),b1,true(),false(),i) busy#(F(),closed(),stop(),false(),false(),true(),i) = 0 >= 0 = idle#(F(),closed(),up(),false(),false(),true(),i) busy#(F(),closed(),stop(),true(),false(),b3,i) = 0 >= 0 = idle#(F(),closed(),down(),true(),false(),b3,i) busy#(B(),closed(),stop(),false(),false(),true(),i) = 0 >= 0 = idle#(B(),closed(),up(),false(),false(),true(),i) busy#(B(),closed(),stop(),false(),true(),b3,i) = 20 >= 20 = idle#(B(),closed(),up(),false(),true(),b3,i) busy#(FS(),closed(),down(),b1,b2,b3,i) = 4b2 >= 4b2 = idle#(F(),closed(),down(),b1,b2,b3,i) busy#(FS(),closed(),up(),b1,b2,b3,i) = 4b2 >= 4b2 = idle#(S(),closed(),up(),b1,b2,b3,i) busy#(BF(),closed(),down(),b1,b2,b3,i) = 4b2 >= 4b2 = idle#(B(),closed(),down(),b1,b2,b3,i) busy#(BF(),closed(),up(),b1,b2,b3,i) = 4b2 >= 4b2 = idle#(F(),closed(),up(),b1,b2,b3,i) busy#(S(),closed(),down(),b1,b2,false(),i) = 4b2 >= 4b2 = idle#(FS(),closed(),down(),b1,b2,false(),i) busy#(F(),closed(),down(),b1,false(),b3,i) = 0 >= 0 = idle#(BF(),closed(),down(),b1,false(),b3,i) busy#(F(),closed(),up(),b1,false(),b3,i) = 0 >= 0 = idle#(FS(),closed(),up(),b1,false(),b3,i) busy#(B(),closed(),up(),false(),b2,b3,i) = 4b2 >= 4b2 = idle#(BF(),closed(),up(),false(),b2,b3,i) busy#(S(),closed(),down(),b1,b2,true(),i) = 4b2 >= 4b2 = idle#(S(),closed(),stop(),b1,b2,true(),i) busy#(F(),closed(),down(),b1,true(),b3,i) = 20 >= 20 = idle#(F(),closed(),stop(),b1,true(),b3,i) busy#(F(),closed(),up(),b1,true(),b3,i) = 20 >= 20 = idle#(F(),closed(),stop(),b1,true(),b3,i) busy#(B(),closed(),up(),true(),b2,b3,i) = 4b2 >= 4b2 = idle#(B(),closed(),stop(),true(),b2,b3,i) busy#(S(),closed(),up(),b1,b2,b3,i) = 4b2 >= 4b2 = idle#(S(),closed(),stop(),b1,b2,b3,i) busy#(B(),closed(),down(),b1,b2,b3,i) = 4b2 >= 4b2 = idle#(B(),closed(),stop(),b1,b2,b3,i) busy#(S(),open(),stop(),b1,b2,false(),i) = 4b2 + 30 >= 4b2 = idle#(S(),closed(),stop(),b1,b2,false(),i) busy#(F(),open(),stop(),b1,false(),b3,i) = 30 >= 0 = idle#(F(),closed(),stop(),b1,false(),b3,i) busy#(B(),open(),stop(),false(),b2,b3,i) = 4b2 + 30 >= 4b2 = idle#(B(),closed(),stop(),false(),b2,b3,i) busy(BF(),d,stop(),b1,b2,b3,i) = b2 + i + 3 >= 0 = incorrect() busy(FS(),d,stop(),b1,b2,b3,i) = b2 + i + 3 >= 0 = incorrect() busy(fl,open(),up(),b1,b2,b3,i) = b2 + i + 3 >= 0 = incorrect() busy(fl,open(),down(),b1,b2,b3,i) = b2 + i + 3 >= 0 = incorrect() busy(B(),closed(),stop(),false(),false(),false(),empty()) = 3 >= 3 = correct() busy(F(),closed(),stop(),false(),false(),false(),empty()) = 3 >= 3 = correct() busy(S(),closed(),stop(),false(),false(),false(),empty()) = 3 >= 3 = correct() busy(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = 6i + 4i1 + 3i2 + 4i3 + 4 >= 6i + 4i1 + 3i2 + 4i3 + 4 = idle(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) busy(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = 6i + 4i1 + 3i2 + 4i3 + 4 >= 6i + 4i1 + 3i2 + 4i3 + 4 = idle(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) busy(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = 6i + 4i1 + 3i2 + 4i3 + 4 >= 6i + 4i1 + 3i2 + 4i3 + 4 = idle(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) busy(B(),open(),stop(),false(),b2,b3,i) = b2 + i + 3 >= b2 + i + 3 = idle(B(),closed(),stop(),false(),b2,b3,i) busy(F(),open(),stop(),b1,false(),b3,i) = i + 3 >= i + 3 = idle(F(),closed(),stop(),b1,false(),b3,i) busy(S(),open(),stop(),b1,b2,false(),i) = b2 + i + 3 >= b2 + i + 3 = idle(S(),closed(),stop(),b1,b2,false(),i) busy(B(),closed(),down(),b1,b2,b3,i) = b2 + i + 3 >= b2 + i + 3 = idle(B(),closed(),stop(),b1,b2,b3,i) busy(S(),closed(),up(),b1,b2,b3,i) = b2 + i + 3 >= b2 + i + 3 = idle(S(),closed(),stop(),b1,b2,b3,i) busy(B(),closed(),up(),true(),b2,b3,i) = b2 + i + 3 >= b2 + i + 3 = idle(B(),closed(),stop(),true(),b2,b3,i) busy(F(),closed(),up(),b1,true(),b3,i) = i + 8 >= i + 8 = idle(F(),closed(),stop(),b1,true(),b3,i) busy(F(),closed(),down(),b1,true(),b3,i) = i + 8 >= i + 8 = idle(F(),closed(),stop(),b1,true(),b3,i) busy(S(),closed(),down(),b1,b2,true(),i) = b2 + i + 3 >= b2 + i + 3 = idle(S(),closed(),stop(),b1,b2,true(),i) busy(B(),closed(),up(),false(),b2,b3,i) = b2 + i + 3 >= b2 + i + 3 = idle(BF(),closed(),up(),false(),b2,b3,i) busy(F(),closed(),up(),b1,false(),b3,i) = i + 3 >= i + 3 = idle(FS(),closed(),up(),b1,false(),b3,i) busy(F(),closed(),down(),b1,false(),b3,i) = i + 3 >= i + 3 = idle(BF(),closed(),down(),b1,false(),b3,i) busy(S(),closed(),down(),b1,b2,false(),i) = b2 + i + 3 >= b2 + i + 3 = idle(FS(),closed(),down(),b1,b2,false(),i) busy(BF(),closed(),up(),b1,b2,b3,i) = b2 + i + 3 >= b2 + i + 3 = idle(F(),closed(),up(),b1,b2,b3,i) busy(BF(),closed(),down(),b1,b2,b3,i) = b2 + i + 3 >= b2 + i + 3 = idle(B(),closed(),down(),b1,b2,b3,i) busy(FS(),closed(),up(),b1,b2,b3,i) = b2 + i + 3 >= b2 + i + 3 = idle(S(),closed(),up(),b1,b2,b3,i) busy(FS(),closed(),down(),b1,b2,b3,i) = b2 + i + 3 >= b2 + i + 3 = idle(F(),closed(),down(),b1,b2,b3,i) busy(B(),closed(),stop(),false(),true(),b3,i) = i + 8 >= i + 8 = idle(B(),closed(),up(),false(),true(),b3,i) busy(B(),closed(),stop(),false(),false(),true(),i) = i + 3 >= i + 3 = idle(B(),closed(),up(),false(),false(),true(),i) busy(F(),closed(),stop(),true(),false(),b3,i) = i + 3 >= i + 3 = idle(F(),closed(),down(),true(),false(),b3,i) busy(F(),closed(),stop(),false(),false(),true(),i) = i + 3 >= i + 3 = idle(F(),closed(),up(),false(),false(),true(),i) busy(S(),closed(),stop(),b1,true(),false(),i) = i + 8 >= i + 8 = idle(S(),closed(),down(),b1,true(),false(),i) busy(S(),closed(),stop(),true(),false(),false(),i) = i + 3 >= i + 3 = idle(S(),closed(),down(),true(),false(),false(),i) idle(fl,d,m,b1,b2,b3,empty()) = b2 + 3 >= b2 + 3 = busy(fl,d,m,b1,b2,b3,empty()) idle(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) = b2 + 6i + 4i1 + 3i2 + 4i3 + 4 >= b2 + i + 2i2 + 4 = busy(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) or(true(),b) = 2b + 6 >= 5 = true() or(false(),b) = 2b + 1 >= b = b problem: DPs: 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) busy#(S(),closed(),stop(),b1,true(),false(),i) -> idle#(S(),closed(),down(),b1,true(),false(),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#(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#(FS(),closed(),down(),b1,b2,b3,i) -> idle#(F(),closed(),down(),b1,b2,b3,i) busy#(FS(),closed(),up(),b1,b2,b3,i) -> idle#(S(),closed(),up(),b1,b2,b3,i) busy#(BF(),closed(),down(),b1,b2,b3,i) -> idle#(B(),closed(),down(),b1,b2,b3,i) busy#(BF(),closed(),up(),b1,b2,b3,i) -> idle#(F(),closed(),up(),b1,b2,b3,i) busy#(S(),closed(),down(),b1,b2,false(),i) -> idle#(FS(),closed(),down(),b1,b2,false(),i) busy#(F(),closed(),down(),b1,false(),b3,i) -> idle#(BF(),closed(),down(),b1,false(),b3,i) busy#(F(),closed(),up(),b1,false(),b3,i) -> idle#(FS(),closed(),up(),b1,false(),b3,i) busy#(B(),closed(),up(),false(),b2,b3,i) -> idle#(BF(),closed(),up(),false(),b2,b3,i) busy#(S(),closed(),down(),b1,b2,true(),i) -> idle#(S(),closed(),stop(),b1,b2,true(),i) busy#(F(),closed(),down(),b1,true(),b3,i) -> idle#(F(),closed(),stop(),b1,true(),b3,i) busy#(F(),closed(),up(),b1,true(),b3,i) -> idle#(F(),closed(),stop(),b1,true(),b3,i) busy#(B(),closed(),up(),true(),b2,b3,i) -> idle#(B(),closed(),stop(),true(),b2,b3,i) busy#(S(),closed(),up(),b1,b2,b3,i) -> idle#(S(),closed(),stop(),b1,b2,b3,i) busy#(B(),closed(),down(),b1,b2,b3,i) -> idle#(B(),closed(),stop(),b1,b2,b3,i) TRS: 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(),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 Open