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: DP Processor: DPs: start#(i) -> busy#(F(),closed(),stop(),false(),false(),false(),i) busy#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) 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)) -> 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: 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 EDG Processor: DPs: start#(i) -> busy#(F(),closed(),stop(),false(),false(),false(),i) busy#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) 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)) -> 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: 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 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#(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#(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) -> busy#(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> 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#(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#(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#(B(),d,stop(),true(),b2,b3,i) -> idle#(B(),open(),stop(),false(),b2,b3,i) idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) -> busy#(F(),d,stop(),b1,true(),b3,i) -> idle#(F(),open(),stop(),b1,false(),b3,i) idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) -> busy#(S(),d,stop(),b1,b2,true(),i) -> idle#(S(),open(),stop(),b1,b2,false(),i) idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) -> busy#(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(),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(),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#(F(),closed(),up(),b1,true(),b3,i) -> idle#(F(),closed(),stop(),b1,true(),b3,i) idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) -> busy#(F(),closed(),down(),b1,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#(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#(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#(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(),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#(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#(BF(),closed(),up(),b1,b2,b3,i) -> idle#(F(),closed(),up(),b1,b2,b3,i) idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) -> busy#(BF(),closed(),down(),b1,b2,b3,i) -> idle#(B(),closed(),down(),b1,b2,b3,i) idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) -> busy#(FS(),closed(),up(),b1,b2,b3,i) -> idle#(S(),closed(),up(),b1,b2,b3,i) idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) -> busy#(FS(),closed(),down(),b1,b2,b3,i) -> idle#(F(),closed(),down(),b1,b2,b3,i) idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) -> busy#(B(),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(),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#(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(),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#(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(),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#(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(),d,stop(),true(),b2,b3,i) -> idle#(B(),open(),stop(),false(),b2,b3,i) idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) -> busy#(F(),d,stop(),b1,true(),b3,i) -> idle#(F(),open(),stop(),b1,false(),b3,i) idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) -> busy#(S(),d,stop(),b1,b2,true(),i) -> idle#(S(),open(),stop(),b1,b2,false(),i) idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) -> busy#(B(),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(),open(),stop(),b1,b2,false(),i) -> idle#(S(),closed(),stop(),b1,b2,false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(S(),open(),stop(),b1,b2,false(),i) -> idle#(S(),closed(),stop(),b1,b2,false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(S(),open(),stop(),b1,b2,false(),i) -> idle#(S(),closed(),stop(),b1,b2,false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(S(),open(),stop(),b1,b2,false(),i) -> idle#(S(),closed(),stop(),b1,b2,false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(S(),closed(),down(),b1,b2,true(),i) -> idle#(S(),closed(),stop(),b1,b2,true(),i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(S(),closed(),down(),b1,b2,true(),i) -> idle#(S(),closed(),stop(),b1,b2,true(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(S(),closed(),down(),b1,b2,true(),i) -> idle#(S(),closed(),stop(),b1,b2,true(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(S(),closed(),down(),b1,b2,true(),i) -> idle#(S(),closed(),stop(),b1,b2,true(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(S(),closed(),down(),b1,b2,true(),i) -> idle#(S(),closed(),stop(),b1,b2,true(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(S(),closed(),down(),b1,b2,false(),i) -> idle#(FS(),closed(),down(),b1,b2,false(),i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(S(),closed(),down(),b1,b2,false(),i) -> idle#(FS(),closed(),down(),b1,b2,false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(S(),closed(),down(),b1,b2,false(),i) -> idle#(FS(),closed(),down(),b1,b2,false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(S(),closed(),down(),b1,b2,false(),i) -> idle#(FS(),closed(),down(),b1,b2,false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(S(),closed(),down(),b1,b2,false(),i) -> idle#(FS(),closed(),down(),b1,b2,false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(S(),closed(),up(),b1,b2,b3,i) -> idle#(S(),closed(),stop(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(S(),closed(),up(),b1,b2,b3,i) -> idle#(S(),closed(),stop(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(S(),closed(),up(),b1,b2,b3,i) -> idle#(S(),closed(),stop(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(S(),closed(),up(),b1,b2,b3,i) -> idle#(S(),closed(),stop(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(S(),closed(),up(),b1,b2,b3,i) -> idle#(S(),closed(),stop(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(S(),closed(),stop(),true(),false(),false(),i) -> idle#(S(),closed(),down(),true(),false(),false(),i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(S(),closed(),stop(),true(),false(),false(),i) -> idle#(S(),closed(),down(),true(),false(),false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(S(),closed(),stop(),true(),false(),false(),i) -> idle#(S(),closed(),down(),true(),false(),false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(S(),closed(),stop(),true(),false(),false(),i) -> idle#(S(),closed(),down(),true(),false(),false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(S(),closed(),stop(),true(),false(),false(),i) -> idle#(S(),closed(),down(),true(),false(),false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(S(),closed(),stop(),b1,true(),false(),i) -> idle#(S(),closed(),down(),b1,true(),false(),i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(S(),closed(),stop(),b1,true(),false(),i) -> idle#(S(),closed(),down(),b1,true(),false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(S(),closed(),stop(),b1,true(),false(),i) -> idle#(S(),closed(),down(),b1,true(),false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(S(),closed(),stop(),b1,true(),false(),i) -> idle#(S(),closed(),down(),b1,true(),false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(S(),closed(),stop(),b1,true(),false(),i) -> idle#(S(),closed(),down(),b1,true(),false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(S(),d,stop(),b1,b2,true(),i) -> idle#(S(),open(),stop(),b1,b2,false(),i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(S(),d,stop(),b1,b2,true(),i) -> idle#(S(),open(),stop(),b1,b2,false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(S(),d,stop(),b1,b2,true(),i) -> idle#(S(),open(),stop(),b1,b2,false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(S(),d,stop(),b1,b2,true(),i) -> idle#(S(),open(),stop(),b1,b2,false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(S(),d,stop(),b1,b2,true(),i) -> idle#(S(),open(),stop(),b1,b2,false(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(B(),open(),stop(),false(),b2,b3,i) -> idle#(B(),closed(),stop(),false(),b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(B(),open(),stop(),false(),b2,b3,i) -> idle#(B(),closed(),stop(),false(),b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(B(),open(),stop(),false(),b2,b3,i) -> idle#(B(),closed(),stop(),false(),b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(B(),open(),stop(),false(),b2,b3,i) -> idle#(B(),closed(),stop(),false(),b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(B(),open(),stop(),false(),b2,b3,i) -> idle#(B(),closed(),stop(),false(),b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(B(),closed(),down(),b1,b2,b3,i) -> idle#(B(),closed(),stop(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(B(),closed(),down(),b1,b2,b3,i) -> idle#(B(),closed(),stop(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(B(),closed(),down(),b1,b2,b3,i) -> idle#(B(),closed(),stop(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(B(),closed(),down(),b1,b2,b3,i) -> idle#(B(),closed(),stop(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(B(),closed(),down(),b1,b2,b3,i) -> idle#(B(),closed(),stop(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(B(),closed(),up(),true(),b2,b3,i) -> idle#(B(),closed(),stop(),true(),b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(B(),closed(),up(),true(),b2,b3,i) -> idle#(B(),closed(),stop(),true(),b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(B(),closed(),up(),true(),b2,b3,i) -> idle#(B(),closed(),stop(),true(),b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(B(),closed(),up(),true(),b2,b3,i) -> idle#(B(),closed(),stop(),true(),b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(B(),closed(),up(),true(),b2,b3,i) -> idle#(B(),closed(),stop(),true(),b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(B(),closed(),up(),false(),b2,b3,i) -> idle#(BF(),closed(),up(),false(),b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(B(),closed(),up(),false(),b2,b3,i) -> idle#(BF(),closed(),up(),false(),b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(B(),closed(),up(),false(),b2,b3,i) -> idle#(BF(),closed(),up(),false(),b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(B(),closed(),up(),false(),b2,b3,i) -> idle#(BF(),closed(),up(),false(),b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(B(),closed(),up(),false(),b2,b3,i) -> idle#(BF(),closed(),up(),false(),b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(B(),closed(),stop(),false(),true(),b3,i) -> idle#(B(),closed(),up(),false(),true(),b3,i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(B(),closed(),stop(),false(),true(),b3,i) -> idle#(B(),closed(),up(),false(),true(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(B(),closed(),stop(),false(),true(),b3,i) -> idle#(B(),closed(),up(),false(),true(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(B(),closed(),stop(),false(),true(),b3,i) -> idle#(B(),closed(),up(),false(),true(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(B(),closed(),stop(),false(),true(),b3,i) -> idle#(B(),closed(),up(),false(),true(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(B(),closed(),stop(),false(),false(),true(),i) -> idle#(B(),closed(),up(),false(),false(),true(),i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(B(),closed(),stop(),false(),false(),true(),i) -> idle#(B(),closed(),up(),false(),false(),true(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(B(),closed(),stop(),false(),false(),true(),i) -> idle#(B(),closed(),up(),false(),false(),true(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(B(),closed(),stop(),false(),false(),true(),i) -> idle#(B(),closed(),up(),false(),false(),true(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(B(),closed(),stop(),false(),false(),true(),i) -> idle#(B(),closed(),up(),false(),false(),true(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(B(),d,stop(),true(),b2,b3,i) -> idle#(B(),open(),stop(),false(),b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(B(),d,stop(),true(),b2,b3,i) -> idle#(B(),open(),stop(),false(),b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(B(),d,stop(),true(),b2,b3,i) -> idle#(B(),open(),stop(),false(),b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(B(),d,stop(),true(),b2,b3,i) -> idle#(B(),open(),stop(),false(),b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(B(),d,stop(),true(),b2,b3,i) -> idle#(B(),open(),stop(),false(),b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(FS(),closed(),down(),b1,b2,b3,i) -> idle#(F(),closed(),down(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(FS(),closed(),down(),b1,b2,b3,i) -> idle#(F(),closed(),down(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(FS(),closed(),down(),b1,b2,b3,i) -> idle#(F(),closed(),down(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(FS(),closed(),down(),b1,b2,b3,i) -> idle#(F(),closed(),down(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(FS(),closed(),down(),b1,b2,b3,i) -> idle#(F(),closed(),down(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(FS(),closed(),up(),b1,b2,b3,i) -> idle#(S(),closed(),up(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(FS(),closed(),up(),b1,b2,b3,i) -> idle#(S(),closed(),up(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(FS(),closed(),up(),b1,b2,b3,i) -> idle#(S(),closed(),up(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(FS(),closed(),up(),b1,b2,b3,i) -> idle#(S(),closed(),up(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(FS(),closed(),up(),b1,b2,b3,i) -> idle#(S(),closed(),up(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(BF(),closed(),down(),b1,b2,b3,i) -> idle#(B(),closed(),down(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(BF(),closed(),down(),b1,b2,b3,i) -> idle#(B(),closed(),down(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(BF(),closed(),down(),b1,b2,b3,i) -> idle#(B(),closed(),down(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(BF(),closed(),down(),b1,b2,b3,i) -> idle#(B(),closed(),down(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(BF(),closed(),down(),b1,b2,b3,i) -> idle#(B(),closed(),down(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(BF(),closed(),up(),b1,b2,b3,i) -> idle#(F(),closed(),up(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(BF(),closed(),up(),b1,b2,b3,i) -> idle#(F(),closed(),up(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(BF(),closed(),up(),b1,b2,b3,i) -> idle#(F(),closed(),up(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(BF(),closed(),up(),b1,b2,b3,i) -> idle#(F(),closed(),up(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(BF(),closed(),up(),b1,b2,b3,i) -> idle#(F(),closed(),up(),b1,b2,b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(F(),open(),stop(),b1,false(),b3,i) -> idle#(F(),closed(),stop(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(F(),open(),stop(),b1,false(),b3,i) -> idle#(F(),closed(),stop(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(F(),open(),stop(),b1,false(),b3,i) -> idle#(F(),closed(),stop(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(F(),open(),stop(),b1,false(),b3,i) -> idle#(F(),closed(),stop(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(F(),open(),stop(),b1,false(),b3,i) -> idle#(F(),closed(),stop(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(F(),closed(),down(),b1,true(),b3,i) -> idle#(F(),closed(),stop(),b1,true(),b3,i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(F(),closed(),down(),b1,true(),b3,i) -> idle#(F(),closed(),stop(),b1,true(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(F(),closed(),down(),b1,true(),b3,i) -> idle#(F(),closed(),stop(),b1,true(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(F(),closed(),down(),b1,true(),b3,i) -> idle#(F(),closed(),stop(),b1,true(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(F(),closed(),down(),b1,true(),b3,i) -> idle#(F(),closed(),stop(),b1,true(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(F(),closed(),down(),b1,false(),b3,i) -> idle#(BF(),closed(),down(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(F(),closed(),down(),b1,false(),b3,i) -> idle#(BF(),closed(),down(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(F(),closed(),down(),b1,false(),b3,i) -> idle#(BF(),closed(),down(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(F(),closed(),down(),b1,false(),b3,i) -> idle#(BF(),closed(),down(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(F(),closed(),down(),b1,false(),b3,i) -> idle#(BF(),closed(),down(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(F(),closed(),up(),b1,true(),b3,i) -> idle#(F(),closed(),stop(),b1,true(),b3,i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(F(),closed(),up(),b1,true(),b3,i) -> idle#(F(),closed(),stop(),b1,true(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(F(),closed(),up(),b1,true(),b3,i) -> idle#(F(),closed(),stop(),b1,true(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(F(),closed(),up(),b1,true(),b3,i) -> idle#(F(),closed(),stop(),b1,true(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(F(),closed(),up(),b1,true(),b3,i) -> idle#(F(),closed(),stop(),b1,true(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(F(),closed(),up(),b1,false(),b3,i) -> idle#(FS(),closed(),up(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(F(),closed(),up(),b1,false(),b3,i) -> idle#(FS(),closed(),up(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(F(),closed(),up(),b1,false(),b3,i) -> idle#(FS(),closed(),up(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(F(),closed(),up(),b1,false(),b3,i) -> idle#(FS(),closed(),up(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(F(),closed(),up(),b1,false(),b3,i) -> idle#(FS(),closed(),up(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(F(),closed(),stop(),true(),false(),b3,i) -> idle#(F(),closed(),down(),true(),false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(F(),closed(),stop(),true(),false(),b3,i) -> idle#(F(),closed(),down(),true(),false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(F(),closed(),stop(),true(),false(),b3,i) -> idle#(F(),closed(),down(),true(),false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(F(),closed(),stop(),true(),false(),b3,i) -> idle#(F(),closed(),down(),true(),false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(F(),closed(),stop(),true(),false(),b3,i) -> idle#(F(),closed(),down(),true(),false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(F(),closed(),stop(),false(),false(),true(),i) -> idle#(F(),closed(),up(),false(),false(),true(),i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(F(),closed(),stop(),false(),false(),true(),i) -> idle#(F(),closed(),up(),false(),false(),true(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(F(),closed(),stop(),false(),false(),true(),i) -> idle#(F(),closed(),up(),false(),false(),true(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(F(),closed(),stop(),false(),false(),true(),i) -> idle#(F(),closed(),up(),false(),false(),true(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(F(),closed(),stop(),false(),false(),true(),i) -> idle#(F(),closed(),up(),false(),false(),true(),i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) busy#(F(),d,stop(),b1,true(),b3,i) -> idle#(F(),open(),stop(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,empty()) -> busy#(fl,d,m,b1,b2,b3,empty()) busy#(F(),d,stop(),b1,true(),b3,i) -> idle#(F(),open(),stop(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b3,i3) busy#(F(),d,stop(),b1,true(),b3,i) -> idle#(F(),open(),stop(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b2,i2) busy#(F(),d,stop(),b1,true(),b3,i) -> idle#(F(),open(),stop(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> or#(b1,i1) busy#(F(),d,stop(),b1,true(),b3,i) -> idle#(F(),open(),stop(),b1,false(),b3,i) -> idle#(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy#(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) start#(i) -> busy#(F(),closed(),stop(),false(),false(),false(),i) -> busy#(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) SCC Processor: #sccs: 1 #rules: 31 #arcs: 198/1225 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#(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) 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(),d,stop(),b1,b2,true(),i) -> idle#(S(),open(),stop(),b1,b2,false(),i) busy#(F(),d,stop(),b1,true(),b3,i) -> idle#(F(),open(),stop(),b1,false(),b3,i) busy#(B(),d,stop(),true(),b2,b3,i) -> idle#(B(),open(),stop(),false(),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) 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#(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,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)) TRS: 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 Subterm Criterion Processor: simple projection: pi(busy#) = 6 pi(idle#) = 6 problem: DPs: 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) 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(),d,stop(),b1,b2,true(),i) -> idle#(S(),open(),stop(),b1,b2,false(),i) busy#(F(),d,stop(),b1,true(),b3,i) -> idle#(F(),open(),stop(),b1,false(),b3,i) busy#(B(),d,stop(),true(),b2,b3,i) -> idle#(B(),open(),stop(),false(),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) 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#(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle#(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,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)) TRS: 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 Matrix Interpretation Processor: dimension: 1 interpretation: [idle#](x0, x1, x2, x3, x4, x5, x6) = x2, [busy#](x0, x1, x2, x3, x4, x5, x6) = x6, [or](x0, x1) = x1, [true] = 0, [idle](x0, x1, x2, x3, x4, x5, x6) = 0, [newbuttons](x0, x1, x2, x3) = x0 + 1, [S] = 0, [correct] = 0, [empty] = 0, [B] = 0, [down] = 0, [up] = 0, [open] = 0, [FS] = 0, [incorrect] = 0, [BF] = 0, [busy](x0, x1, x2, x3, x4, x5, x6) = 0, [false] = 0, [stop] = 0, [closed] = 0, [F] = 0, [start](x0) = x0 + 1 orientation: busy#(S(),closed(),stop(),true(),false(),false(),i) = i >= 0 = idle#(S(),closed(),down(),true(),false(),false(),i) idle#(fl,d,m,b1,b2,b3,empty()) = m >= 0 = busy#(fl,d,m,b1,b2,b3,empty()) busy#(S(),closed(),stop(),b1,true(),false(),i) = i >= 0 = idle#(S(),closed(),down(),b1,true(),false(),i) busy#(F(),closed(),stop(),false(),false(),true(),i) = i >= 0 = idle#(F(),closed(),up(),false(),false(),true(),i) busy#(F(),closed(),stop(),true(),false(),b3,i) = i >= 0 = idle#(F(),closed(),down(),true(),false(),b3,i) busy#(B(),closed(),stop(),false(),false(),true(),i) = i >= 0 = idle#(B(),closed(),up(),false(),false(),true(),i) busy#(B(),closed(),stop(),false(),true(),b3,i) = i >= 0 = idle#(B(),closed(),up(),false(),true(),b3,i) busy#(FS(),closed(),down(),b1,b2,b3,i) = i >= 0 = idle#(F(),closed(),down(),b1,b2,b3,i) busy#(FS(),closed(),up(),b1,b2,b3,i) = i >= 0 = idle#(S(),closed(),up(),b1,b2,b3,i) busy#(BF(),closed(),down(),b1,b2,b3,i) = i >= 0 = idle#(B(),closed(),down(),b1,b2,b3,i) busy#(BF(),closed(),up(),b1,b2,b3,i) = i >= 0 = idle#(F(),closed(),up(),b1,b2,b3,i) busy#(S(),closed(),down(),b1,b2,false(),i) = i >= 0 = idle#(FS(),closed(),down(),b1,b2,false(),i) busy#(F(),closed(),down(),b1,false(),b3,i) = i >= 0 = idle#(BF(),closed(),down(),b1,false(),b3,i) busy#(F(),closed(),up(),b1,false(),b3,i) = i >= 0 = idle#(FS(),closed(),up(),b1,false(),b3,i) busy#(B(),closed(),up(),false(),b2,b3,i) = i >= 0 = idle#(BF(),closed(),up(),false(),b2,b3,i) busy#(S(),closed(),down(),b1,b2,true(),i) = i >= 0 = idle#(S(),closed(),stop(),b1,b2,true(),i) busy#(F(),closed(),down(),b1,true(),b3,i) = i >= 0 = idle#(F(),closed(),stop(),b1,true(),b3,i) busy#(F(),closed(),up(),b1,true(),b3,i) = i >= 0 = idle#(F(),closed(),stop(),b1,true(),b3,i) busy#(B(),closed(),up(),true(),b2,b3,i) = i >= 0 = idle#(B(),closed(),stop(),true(),b2,b3,i) busy#(S(),closed(),up(),b1,b2,b3,i) = i >= 0 = idle#(S(),closed(),stop(),b1,b2,b3,i) busy#(B(),closed(),down(),b1,b2,b3,i) = i >= 0 = idle#(B(),closed(),stop(),b1,b2,b3,i) busy#(S(),d,stop(),b1,b2,true(),i) = i >= 0 = idle#(S(),open(),stop(),b1,b2,false(),i) busy#(F(),d,stop(),b1,true(),b3,i) = i >= 0 = idle#(F(),open(),stop(),b1,false(),b3,i) busy#(B(),d,stop(),true(),b2,b3,i) = i >= 0 = idle#(B(),open(),stop(),false(),b2,b3,i) busy#(S(),open(),stop(),b1,b2,false(),i) = i >= 0 = idle#(S(),closed(),stop(),b1,b2,false(),i) busy#(F(),open(),stop(),b1,false(),b3,i) = i >= 0 = idle#(F(),closed(),stop(),b1,false(),b3,i) busy#(B(),open(),stop(),false(),b2,b3,i) = i >= 0 = idle#(B(),closed(),stop(),false(),b2,b3,i) busy#(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = i1 + 1 >= 0 = idle#(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) busy#(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = i1 + 1 >= 0 = idle#(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) busy#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = i1 + 1 >= 0 = idle#(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) start(i) = i + 1 >= 0 = busy(F(),closed(),stop(),false(),false(),false(),i) busy(BF(),d,stop(),b1,b2,b3,i) = 0 >= 0 = incorrect() busy(FS(),d,stop(),b1,b2,b3,i) = 0 >= 0 = incorrect() busy(fl,open(),up(),b1,b2,b3,i) = 0 >= 0 = incorrect() busy(fl,open(),down(),b1,b2,b3,i) = 0 >= 0 = incorrect() busy(B(),closed(),stop(),false(),false(),false(),empty()) = 0 >= 0 = correct() busy(F(),closed(),stop(),false(),false(),false(),empty()) = 0 >= 0 = correct() busy(S(),closed(),stop(),false(),false(),false(),empty()) = 0 >= 0 = correct() busy(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = 0 >= 0 = idle(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) busy(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = 0 >= 0 = idle(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) busy(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = 0 >= 0 = idle(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) busy(B(),open(),stop(),false(),b2,b3,i) = 0 >= 0 = idle(B(),closed(),stop(),false(),b2,b3,i) busy(F(),open(),stop(),b1,false(),b3,i) = 0 >= 0 = idle(F(),closed(),stop(),b1,false(),b3,i) busy(S(),open(),stop(),b1,b2,false(),i) = 0 >= 0 = idle(S(),closed(),stop(),b1,b2,false(),i) busy(B(),d,stop(),true(),b2,b3,i) = 0 >= 0 = idle(B(),open(),stop(),false(),b2,b3,i) busy(F(),d,stop(),b1,true(),b3,i) = 0 >= 0 = idle(F(),open(),stop(),b1,false(),b3,i) busy(S(),d,stop(),b1,b2,true(),i) = 0 >= 0 = idle(S(),open(),stop(),b1,b2,false(),i) busy(B(),closed(),down(),b1,b2,b3,i) = 0 >= 0 = idle(B(),closed(),stop(),b1,b2,b3,i) busy(S(),closed(),up(),b1,b2,b3,i) = 0 >= 0 = idle(S(),closed(),stop(),b1,b2,b3,i) busy(B(),closed(),up(),true(),b2,b3,i) = 0 >= 0 = idle(B(),closed(),stop(),true(),b2,b3,i) busy(F(),closed(),up(),b1,true(),b3,i) = 0 >= 0 = idle(F(),closed(),stop(),b1,true(),b3,i) busy(F(),closed(),down(),b1,true(),b3,i) = 0 >= 0 = idle(F(),closed(),stop(),b1,true(),b3,i) busy(S(),closed(),down(),b1,b2,true(),i) = 0 >= 0 = idle(S(),closed(),stop(),b1,b2,true(),i) busy(B(),closed(),up(),false(),b2,b3,i) = 0 >= 0 = idle(BF(),closed(),up(),false(),b2,b3,i) busy(F(),closed(),up(),b1,false(),b3,i) = 0 >= 0 = idle(FS(),closed(),up(),b1,false(),b3,i) busy(F(),closed(),down(),b1,false(),b3,i) = 0 >= 0 = idle(BF(),closed(),down(),b1,false(),b3,i) busy(S(),closed(),down(),b1,b2,false(),i) = 0 >= 0 = idle(FS(),closed(),down(),b1,b2,false(),i) busy(BF(),closed(),up(),b1,b2,b3,i) = 0 >= 0 = idle(F(),closed(),up(),b1,b2,b3,i) busy(BF(),closed(),down(),b1,b2,b3,i) = 0 >= 0 = idle(B(),closed(),down(),b1,b2,b3,i) busy(FS(),closed(),up(),b1,b2,b3,i) = 0 >= 0 = idle(S(),closed(),up(),b1,b2,b3,i) busy(FS(),closed(),down(),b1,b2,b3,i) = 0 >= 0 = idle(F(),closed(),down(),b1,b2,b3,i) busy(B(),closed(),stop(),false(),true(),b3,i) = 0 >= 0 = idle(B(),closed(),up(),false(),true(),b3,i) busy(B(),closed(),stop(),false(),false(),true(),i) = 0 >= 0 = idle(B(),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(F(),closed(),stop(),false(),false(),true(),i) = 0 >= 0 = idle(F(),closed(),up(),false(),false(),true(),i) busy(S(),closed(),stop(),b1,true(),false(),i) = 0 >= 0 = idle(S(),closed(),down(),b1,true(),false(),i) busy(S(),closed(),stop(),true(),false(),false(),i) = 0 >= 0 = idle(S(),closed(),down(),true(),false(),false(),i) idle(fl,d,m,b1,b2,b3,empty()) = 0 >= 0 = busy(fl,d,m,b1,b2,b3,empty()) idle(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) = 0 >= 0 = busy(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) or(true(),b) = b >= 0 = true() or(false(),b) = b >= b = b problem: DPs: 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) 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(),d,stop(),b1,b2,true(),i) -> idle#(S(),open(),stop(),b1,b2,false(),i) busy#(F(),d,stop(),b1,true(),b3,i) -> idle#(F(),open(),stop(),b1,false(),b3,i) busy#(B(),d,stop(),true(),b2,b3,i) -> idle#(B(),open(),stop(),false(),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: 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 Matrix Interpretation Processor: dimension: 1 interpretation: [idle#](x0, x1, x2, x3, x4, x5, x6) = x1 + x2 + x5, [busy#](x0, x1, x2, x3, x4, x5, x6) = x5 + x6, [or](x0, x1) = x1 + 1, [true] = 1, [idle](x0, x1, x2, x3, x4, x5, x6) = x4 + x6, [newbuttons](x0, x1, x2, x3) = x1 + x3 + 1, [S] = 0, [correct] = 0, [empty] = 0, [B] = 0, [down] = 0, [up] = 0, [open] = 0, [FS] = 0, [incorrect] = 0, [BF] = 0, [busy](x0, x1, x2, x3, x4, x5, x6) = x4 + x6, [false] = 0, [stop] = 0, [closed] = 0, [F] = 0, [start](x0) = x0 orientation: busy#(S(),closed(),stop(),true(),false(),false(),i) = i >= 0 = idle#(S(),closed(),down(),true(),false(),false(),i) idle#(fl,d,m,b1,b2,b3,empty()) = b3 + d + m >= b3 = busy#(fl,d,m,b1,b2,b3,empty()) busy#(S(),closed(),stop(),b1,true(),false(),i) = i >= 0 = idle#(S(),closed(),down(),b1,true(),false(),i) busy#(F(),closed(),stop(),false(),false(),true(),i) = i + 1 >= 1 = idle#(F(),closed(),up(),false(),false(),true(),i) busy#(F(),closed(),stop(),true(),false(),b3,i) = b3 + i >= b3 = idle#(F(),closed(),down(),true(),false(),b3,i) busy#(B(),closed(),stop(),false(),false(),true(),i) = i + 1 >= 1 = idle#(B(),closed(),up(),false(),false(),true(),i) busy#(B(),closed(),stop(),false(),true(),b3,i) = b3 + i >= b3 = idle#(B(),closed(),up(),false(),true(),b3,i) busy#(FS(),closed(),down(),b1,b2,b3,i) = b3 + i >= b3 = idle#(F(),closed(),down(),b1,b2,b3,i) busy#(FS(),closed(),up(),b1,b2,b3,i) = b3 + i >= b3 = idle#(S(),closed(),up(),b1,b2,b3,i) busy#(BF(),closed(),down(),b1,b2,b3,i) = b3 + i >= b3 = idle#(B(),closed(),down(),b1,b2,b3,i) busy#(BF(),closed(),up(),b1,b2,b3,i) = b3 + i >= b3 = idle#(F(),closed(),up(),b1,b2,b3,i) busy#(S(),closed(),down(),b1,b2,false(),i) = i >= 0 = idle#(FS(),closed(),down(),b1,b2,false(),i) busy#(F(),closed(),down(),b1,false(),b3,i) = b3 + i >= b3 = idle#(BF(),closed(),down(),b1,false(),b3,i) busy#(F(),closed(),up(),b1,false(),b3,i) = b3 + i >= b3 = idle#(FS(),closed(),up(),b1,false(),b3,i) busy#(B(),closed(),up(),false(),b2,b3,i) = b3 + i >= b3 = idle#(BF(),closed(),up(),false(),b2,b3,i) busy#(S(),closed(),down(),b1,b2,true(),i) = i + 1 >= 1 = idle#(S(),closed(),stop(),b1,b2,true(),i) busy#(F(),closed(),down(),b1,true(),b3,i) = b3 + i >= b3 = idle#(F(),closed(),stop(),b1,true(),b3,i) busy#(F(),closed(),up(),b1,true(),b3,i) = b3 + i >= b3 = idle#(F(),closed(),stop(),b1,true(),b3,i) busy#(B(),closed(),up(),true(),b2,b3,i) = b3 + i >= b3 = idle#(B(),closed(),stop(),true(),b2,b3,i) busy#(S(),closed(),up(),b1,b2,b3,i) = b3 + i >= b3 = idle#(S(),closed(),stop(),b1,b2,b3,i) busy#(B(),closed(),down(),b1,b2,b3,i) = b3 + i >= b3 = idle#(B(),closed(),stop(),b1,b2,b3,i) busy#(S(),d,stop(),b1,b2,true(),i) = i + 1 >= 0 = idle#(S(),open(),stop(),b1,b2,false(),i) busy#(F(),d,stop(),b1,true(),b3,i) = b3 + i >= b3 = idle#(F(),open(),stop(),b1,false(),b3,i) busy#(B(),d,stop(),true(),b2,b3,i) = b3 + i >= b3 = idle#(B(),open(),stop(),false(),b2,b3,i) busy#(S(),open(),stop(),b1,b2,false(),i) = i >= 0 = idle#(S(),closed(),stop(),b1,b2,false(),i) busy#(F(),open(),stop(),b1,false(),b3,i) = b3 + i >= b3 = idle#(F(),closed(),stop(),b1,false(),b3,i) busy#(B(),open(),stop(),false(),b2,b3,i) = b3 + i >= b3 = idle#(B(),closed(),stop(),false(),b2,b3,i) start(i) = i >= i = busy(F(),closed(),stop(),false(),false(),false(),i) busy(BF(),d,stop(),b1,b2,b3,i) = b2 + i >= 0 = incorrect() busy(FS(),d,stop(),b1,b2,b3,i) = b2 + i >= 0 = incorrect() busy(fl,open(),up(),b1,b2,b3,i) = b2 + i >= 0 = incorrect() busy(fl,open(),down(),b1,b2,b3,i) = b2 + i >= 0 = incorrect() busy(B(),closed(),stop(),false(),false(),false(),empty()) = 0 >= 0 = correct() busy(F(),closed(),stop(),false(),false(),false(),empty()) = 0 >= 0 = correct() busy(S(),closed(),stop(),false(),false(),false(),empty()) = 0 >= 0 = correct() busy(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = i + i2 + 1 >= i + i2 + 1 = idle(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) busy(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = i + i2 + 1 >= i + i2 + 1 = idle(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) busy(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = i + i2 + 1 >= i + i2 + 1 = idle(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) busy(B(),open(),stop(),false(),b2,b3,i) = b2 + i >= b2 + i = idle(B(),closed(),stop(),false(),b2,b3,i) busy(F(),open(),stop(),b1,false(),b3,i) = i >= i = idle(F(),closed(),stop(),b1,false(),b3,i) busy(S(),open(),stop(),b1,b2,false(),i) = b2 + i >= b2 + i = idle(S(),closed(),stop(),b1,b2,false(),i) busy(B(),d,stop(),true(),b2,b3,i) = b2 + i >= b2 + i = idle(B(),open(),stop(),false(),b2,b3,i) busy(F(),d,stop(),b1,true(),b3,i) = i + 1 >= i = idle(F(),open(),stop(),b1,false(),b3,i) busy(S(),d,stop(),b1,b2,true(),i) = b2 + i >= b2 + i = idle(S(),open(),stop(),b1,b2,false(),i) busy(B(),closed(),down(),b1,b2,b3,i) = b2 + i >= b2 + i = idle(B(),closed(),stop(),b1,b2,b3,i) busy(S(),closed(),up(),b1,b2,b3,i) = b2 + i >= b2 + i = idle(S(),closed(),stop(),b1,b2,b3,i) busy(B(),closed(),up(),true(),b2,b3,i) = b2 + i >= b2 + i = idle(B(),closed(),stop(),true(),b2,b3,i) busy(F(),closed(),up(),b1,true(),b3,i) = i + 1 >= i + 1 = idle(F(),closed(),stop(),b1,true(),b3,i) busy(F(),closed(),down(),b1,true(),b3,i) = i + 1 >= i + 1 = idle(F(),closed(),stop(),b1,true(),b3,i) busy(S(),closed(),down(),b1,b2,true(),i) = b2 + i >= b2 + i = idle(S(),closed(),stop(),b1,b2,true(),i) busy(B(),closed(),up(),false(),b2,b3,i) = b2 + i >= b2 + i = idle(BF(),closed(),up(),false(),b2,b3,i) busy(F(),closed(),up(),b1,false(),b3,i) = i >= i = idle(FS(),closed(),up(),b1,false(),b3,i) busy(F(),closed(),down(),b1,false(),b3,i) = i >= i = idle(BF(),closed(),down(),b1,false(),b3,i) busy(S(),closed(),down(),b1,b2,false(),i) = b2 + i >= b2 + i = idle(FS(),closed(),down(),b1,b2,false(),i) busy(BF(),closed(),up(),b1,b2,b3,i) = b2 + i >= b2 + i = idle(F(),closed(),up(),b1,b2,b3,i) busy(BF(),closed(),down(),b1,b2,b3,i) = b2 + i >= b2 + i = idle(B(),closed(),down(),b1,b2,b3,i) busy(FS(),closed(),up(),b1,b2,b3,i) = b2 + i >= b2 + i = idle(S(),closed(),up(),b1,b2,b3,i) busy(FS(),closed(),down(),b1,b2,b3,i) = b2 + i >= b2 + i = idle(F(),closed(),down(),b1,b2,b3,i) busy(B(),closed(),stop(),false(),true(),b3,i) = i + 1 >= i + 1 = idle(B(),closed(),up(),false(),true(),b3,i) busy(B(),closed(),stop(),false(),false(),true(),i) = i >= i = idle(B(),closed(),up(),false(),false(),true(),i) busy(F(),closed(),stop(),true(),false(),b3,i) = i >= i = idle(F(),closed(),down(),true(),false(),b3,i) busy(F(),closed(),stop(),false(),false(),true(),i) = i >= i = idle(F(),closed(),up(),false(),false(),true(),i) busy(S(),closed(),stop(),b1,true(),false(),i) = i + 1 >= i + 1 = idle(S(),closed(),down(),b1,true(),false(),i) busy(S(),closed(),stop(),true(),false(),false(),i) = i >= i = idle(S(),closed(),down(),true(),false(),false(),i) idle(fl,d,m,b1,b2,b3,empty()) = b2 >= b2 = busy(fl,d,m,b1,b2,b3,empty()) idle(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) = b2 + i + i2 + 1 >= i + i2 + 1 = busy(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) or(true(),b) = b + 1 >= 1 = true() or(false(),b) = b + 1 >= b = b problem: DPs: 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) 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#(F(),d,stop(),b1,true(),b3,i) -> idle#(F(),open(),stop(),b1,false(),b3,i) busy#(B(),d,stop(),true(),b2,b3,i) -> idle#(B(),open(),stop(),false(),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: 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 Matrix Interpretation Processor: dimension: 1 interpretation: [idle#](x0, x1, x2, x3, x4, x5, x6) = x0 + x1 + x2 + x3, [busy#](x0, x1, x2, x3, x4, x5, x6) = x2 + x3 + x6, [or](x0, x1) = x0 + x1 + 1, [true] = 1, [idle](x0, x1, x2, x3, x4, x5, x6) = x1, [newbuttons](x0, x1, x2, x3) = 0, [S] = 0, [correct] = 0, [empty] = 0, [B] = 0, [down] = 1, [up] = 1, [open] = 0, [FS] = 0, [incorrect] = 0, [BF] = 0, [busy](x0, x1, x2, x3, x4, x5, x6) = 0, [false] = 0, [stop] = 1, [closed] = 0, [F] = 0, [start](x0) = x0 + 1 orientation: busy#(S(),closed(),stop(),true(),false(),false(),i) = i + 2 >= 2 = idle#(S(),closed(),down(),true(),false(),false(),i) idle#(fl,d,m,b1,b2,b3,empty()) = b1 + d + fl + m >= b1 + m = busy#(fl,d,m,b1,b2,b3,empty()) busy#(S(),closed(),stop(),b1,true(),false(),i) = b1 + i + 1 >= b1 + 1 = idle#(S(),closed(),down(),b1,true(),false(),i) busy#(F(),closed(),stop(),false(),false(),true(),i) = i + 1 >= 1 = idle#(F(),closed(),up(),false(),false(),true(),i) busy#(F(),closed(),stop(),true(),false(),b3,i) = i + 2 >= 2 = idle#(F(),closed(),down(),true(),false(),b3,i) busy#(B(),closed(),stop(),false(),false(),true(),i) = i + 1 >= 1 = idle#(B(),closed(),up(),false(),false(),true(),i) busy#(B(),closed(),stop(),false(),true(),b3,i) = i + 1 >= 1 = idle#(B(),closed(),up(),false(),true(),b3,i) busy#(FS(),closed(),down(),b1,b2,b3,i) = b1 + i + 1 >= b1 + 1 = idle#(F(),closed(),down(),b1,b2,b3,i) busy#(FS(),closed(),up(),b1,b2,b3,i) = b1 + i + 1 >= b1 + 1 = idle#(S(),closed(),up(),b1,b2,b3,i) busy#(BF(),closed(),down(),b1,b2,b3,i) = b1 + i + 1 >= b1 + 1 = idle#(B(),closed(),down(),b1,b2,b3,i) busy#(BF(),closed(),up(),b1,b2,b3,i) = b1 + i + 1 >= b1 + 1 = idle#(F(),closed(),up(),b1,b2,b3,i) busy#(S(),closed(),down(),b1,b2,false(),i) = b1 + i + 1 >= b1 + 1 = idle#(FS(),closed(),down(),b1,b2,false(),i) busy#(F(),closed(),down(),b1,false(),b3,i) = b1 + i + 1 >= b1 + 1 = idle#(BF(),closed(),down(),b1,false(),b3,i) busy#(F(),closed(),up(),b1,false(),b3,i) = b1 + i + 1 >= b1 + 1 = idle#(FS(),closed(),up(),b1,false(),b3,i) busy#(B(),closed(),up(),false(),b2,b3,i) = i + 1 >= 1 = idle#(BF(),closed(),up(),false(),b2,b3,i) busy#(S(),closed(),down(),b1,b2,true(),i) = b1 + i + 1 >= b1 + 1 = idle#(S(),closed(),stop(),b1,b2,true(),i) busy#(F(),closed(),down(),b1,true(),b3,i) = b1 + i + 1 >= b1 + 1 = idle#(F(),closed(),stop(),b1,true(),b3,i) busy#(F(),closed(),up(),b1,true(),b3,i) = b1 + i + 1 >= b1 + 1 = idle#(F(),closed(),stop(),b1,true(),b3,i) busy#(B(),closed(),up(),true(),b2,b3,i) = i + 2 >= 2 = idle#(B(),closed(),stop(),true(),b2,b3,i) busy#(S(),closed(),up(),b1,b2,b3,i) = b1 + i + 1 >= b1 + 1 = idle#(S(),closed(),stop(),b1,b2,b3,i) busy#(B(),closed(),down(),b1,b2,b3,i) = b1 + i + 1 >= b1 + 1 = idle#(B(),closed(),stop(),b1,b2,b3,i) busy#(F(),d,stop(),b1,true(),b3,i) = b1 + i + 1 >= b1 + 1 = idle#(F(),open(),stop(),b1,false(),b3,i) busy#(B(),d,stop(),true(),b2,b3,i) = i + 2 >= 1 = idle#(B(),open(),stop(),false(),b2,b3,i) busy#(S(),open(),stop(),b1,b2,false(),i) = b1 + i + 1 >= b1 + 1 = idle#(S(),closed(),stop(),b1,b2,false(),i) busy#(F(),open(),stop(),b1,false(),b3,i) = b1 + i + 1 >= b1 + 1 = idle#(F(),closed(),stop(),b1,false(),b3,i) busy#(B(),open(),stop(),false(),b2,b3,i) = i + 1 >= 1 = idle#(B(),closed(),stop(),false(),b2,b3,i) start(i) = i + 1 >= 0 = busy(F(),closed(),stop(),false(),false(),false(),i) busy(BF(),d,stop(),b1,b2,b3,i) = 0 >= 0 = incorrect() busy(FS(),d,stop(),b1,b2,b3,i) = 0 >= 0 = incorrect() busy(fl,open(),up(),b1,b2,b3,i) = 0 >= 0 = incorrect() busy(fl,open(),down(),b1,b2,b3,i) = 0 >= 0 = incorrect() busy(B(),closed(),stop(),false(),false(),false(),empty()) = 0 >= 0 = correct() busy(F(),closed(),stop(),false(),false(),false(),empty()) = 0 >= 0 = correct() busy(S(),closed(),stop(),false(),false(),false(),empty()) = 0 >= 0 = correct() busy(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = 0 >= 0 = idle(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) busy(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = 0 >= 0 = idle(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) busy(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = 0 >= 0 = idle(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) busy(B(),open(),stop(),false(),b2,b3,i) = 0 >= 0 = idle(B(),closed(),stop(),false(),b2,b3,i) busy(F(),open(),stop(),b1,false(),b3,i) = 0 >= 0 = idle(F(),closed(),stop(),b1,false(),b3,i) busy(S(),open(),stop(),b1,b2,false(),i) = 0 >= 0 = idle(S(),closed(),stop(),b1,b2,false(),i) busy(B(),d,stop(),true(),b2,b3,i) = 0 >= 0 = idle(B(),open(),stop(),false(),b2,b3,i) busy(F(),d,stop(),b1,true(),b3,i) = 0 >= 0 = idle(F(),open(),stop(),b1,false(),b3,i) busy(S(),d,stop(),b1,b2,true(),i) = 0 >= 0 = idle(S(),open(),stop(),b1,b2,false(),i) busy(B(),closed(),down(),b1,b2,b3,i) = 0 >= 0 = idle(B(),closed(),stop(),b1,b2,b3,i) busy(S(),closed(),up(),b1,b2,b3,i) = 0 >= 0 = idle(S(),closed(),stop(),b1,b2,b3,i) busy(B(),closed(),up(),true(),b2,b3,i) = 0 >= 0 = idle(B(),closed(),stop(),true(),b2,b3,i) busy(F(),closed(),up(),b1,true(),b3,i) = 0 >= 0 = idle(F(),closed(),stop(),b1,true(),b3,i) busy(F(),closed(),down(),b1,true(),b3,i) = 0 >= 0 = idle(F(),closed(),stop(),b1,true(),b3,i) busy(S(),closed(),down(),b1,b2,true(),i) = 0 >= 0 = idle(S(),closed(),stop(),b1,b2,true(),i) busy(B(),closed(),up(),false(),b2,b3,i) = 0 >= 0 = idle(BF(),closed(),up(),false(),b2,b3,i) busy(F(),closed(),up(),b1,false(),b3,i) = 0 >= 0 = idle(FS(),closed(),up(),b1,false(),b3,i) busy(F(),closed(),down(),b1,false(),b3,i) = 0 >= 0 = idle(BF(),closed(),down(),b1,false(),b3,i) busy(S(),closed(),down(),b1,b2,false(),i) = 0 >= 0 = idle(FS(),closed(),down(),b1,b2,false(),i) busy(BF(),closed(),up(),b1,b2,b3,i) = 0 >= 0 = idle(F(),closed(),up(),b1,b2,b3,i) busy(BF(),closed(),down(),b1,b2,b3,i) = 0 >= 0 = idle(B(),closed(),down(),b1,b2,b3,i) busy(FS(),closed(),up(),b1,b2,b3,i) = 0 >= 0 = idle(S(),closed(),up(),b1,b2,b3,i) busy(FS(),closed(),down(),b1,b2,b3,i) = 0 >= 0 = idle(F(),closed(),down(),b1,b2,b3,i) busy(B(),closed(),stop(),false(),true(),b3,i) = 0 >= 0 = idle(B(),closed(),up(),false(),true(),b3,i) busy(B(),closed(),stop(),false(),false(),true(),i) = 0 >= 0 = idle(B(),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(F(),closed(),stop(),false(),false(),true(),i) = 0 >= 0 = idle(F(),closed(),up(),false(),false(),true(),i) busy(S(),closed(),stop(),b1,true(),false(),i) = 0 >= 0 = idle(S(),closed(),down(),b1,true(),false(),i) busy(S(),closed(),stop(),true(),false(),false(),i) = 0 >= 0 = idle(S(),closed(),down(),true(),false(),false(),i) idle(fl,d,m,b1,b2,b3,empty()) = d >= 0 = busy(fl,d,m,b1,b2,b3,empty()) idle(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) = d >= 0 = busy(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) or(true(),b) = b + 2 >= 1 = true() or(false(),b) = b + 1 >= b = b problem: DPs: 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) 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#(F(),d,stop(),b1,true(),b3,i) -> idle#(F(),open(),stop(),b1,false(),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: 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 Matrix Interpretation Processor: dimension: 1 interpretation: [idle#](x0, x1, x2, x3, x4, x5, x6) = x0 + x1 + x2 + x4, [busy#](x0, x1, x2, x3, x4, x5, x6) = x0 + x1 + x4, [or](x0, x1) = x0 + x1, [true] = 1, [idle](x0, x1, x2, x3, x4, x5, x6) = x4 + x5 + x6 + 1, [newbuttons](x0, x1, x2, x3) = x1 + x2 + x3, [S] = 1, [correct] = 0, [empty] = 0, [B] = 1, [down] = 0, [up] = 0, [open] = 1, [FS] = 1, [incorrect] = 0, [BF] = 1, [busy](x0, x1, x2, x3, x4, x5, x6) = x4 + x5 + x6 + 1, [false] = 0, [stop] = 0, [closed] = 0, [F] = 1, [start](x0) = x0 + 1 orientation: busy#(S(),closed(),stop(),true(),false(),false(),i) = 1 >= 1 = idle#(S(),closed(),down(),true(),false(),false(),i) idle#(fl,d,m,b1,b2,b3,empty()) = b2 + d + fl + m >= b2 + d + fl = busy#(fl,d,m,b1,b2,b3,empty()) busy#(S(),closed(),stop(),b1,true(),false(),i) = 2 >= 2 = idle#(S(),closed(),down(),b1,true(),false(),i) busy#(F(),closed(),stop(),false(),false(),true(),i) = 1 >= 1 = idle#(F(),closed(),up(),false(),false(),true(),i) busy#(F(),closed(),stop(),true(),false(),b3,i) = 1 >= 1 = idle#(F(),closed(),down(),true(),false(),b3,i) busy#(B(),closed(),stop(),false(),false(),true(),i) = 1 >= 1 = idle#(B(),closed(),up(),false(),false(),true(),i) busy#(B(),closed(),stop(),false(),true(),b3,i) = 2 >= 2 = idle#(B(),closed(),up(),false(),true(),b3,i) busy#(FS(),closed(),down(),b1,b2,b3,i) = b2 + 1 >= b2 + 1 = idle#(F(),closed(),down(),b1,b2,b3,i) busy#(FS(),closed(),up(),b1,b2,b3,i) = b2 + 1 >= b2 + 1 = idle#(S(),closed(),up(),b1,b2,b3,i) busy#(BF(),closed(),down(),b1,b2,b3,i) = b2 + 1 >= b2 + 1 = idle#(B(),closed(),down(),b1,b2,b3,i) busy#(BF(),closed(),up(),b1,b2,b3,i) = b2 + 1 >= b2 + 1 = idle#(F(),closed(),up(),b1,b2,b3,i) busy#(S(),closed(),down(),b1,b2,false(),i) = b2 + 1 >= b2 + 1 = idle#(FS(),closed(),down(),b1,b2,false(),i) busy#(F(),closed(),down(),b1,false(),b3,i) = 1 >= 1 = idle#(BF(),closed(),down(),b1,false(),b3,i) busy#(F(),closed(),up(),b1,false(),b3,i) = 1 >= 1 = idle#(FS(),closed(),up(),b1,false(),b3,i) busy#(B(),closed(),up(),false(),b2,b3,i) = b2 + 1 >= b2 + 1 = idle#(BF(),closed(),up(),false(),b2,b3,i) busy#(S(),closed(),down(),b1,b2,true(),i) = b2 + 1 >= b2 + 1 = idle#(S(),closed(),stop(),b1,b2,true(),i) busy#(F(),closed(),down(),b1,true(),b3,i) = 2 >= 2 = idle#(F(),closed(),stop(),b1,true(),b3,i) busy#(F(),closed(),up(),b1,true(),b3,i) = 2 >= 2 = idle#(F(),closed(),stop(),b1,true(),b3,i) busy#(B(),closed(),up(),true(),b2,b3,i) = b2 + 1 >= b2 + 1 = idle#(B(),closed(),stop(),true(),b2,b3,i) busy#(S(),closed(),up(),b1,b2,b3,i) = b2 + 1 >= b2 + 1 = idle#(S(),closed(),stop(),b1,b2,b3,i) busy#(B(),closed(),down(),b1,b2,b3,i) = b2 + 1 >= b2 + 1 = idle#(B(),closed(),stop(),b1,b2,b3,i) busy#(F(),d,stop(),b1,true(),b3,i) = d + 2 >= 2 = idle#(F(),open(),stop(),b1,false(),b3,i) busy#(S(),open(),stop(),b1,b2,false(),i) = b2 + 2 >= b2 + 1 = idle#(S(),closed(),stop(),b1,b2,false(),i) busy#(F(),open(),stop(),b1,false(),b3,i) = 2 >= 1 = idle#(F(),closed(),stop(),b1,false(),b3,i) busy#(B(),open(),stop(),false(),b2,b3,i) = b2 + 2 >= b2 + 1 = idle#(B(),closed(),stop(),false(),b2,b3,i) start(i) = i + 1 >= i + 1 = busy(F(),closed(),stop(),false(),false(),false(),i) busy(BF(),d,stop(),b1,b2,b3,i) = b2 + b3 + i + 1 >= 0 = incorrect() busy(FS(),d,stop(),b1,b2,b3,i) = b2 + b3 + i + 1 >= 0 = incorrect() busy(fl,open(),up(),b1,b2,b3,i) = b2 + b3 + i + 1 >= 0 = incorrect() busy(fl,open(),down(),b1,b2,b3,i) = b2 + b3 + i + 1 >= 0 = incorrect() busy(B(),closed(),stop(),false(),false(),false(),empty()) = 1 >= 0 = correct() busy(F(),closed(),stop(),false(),false(),false(),empty()) = 1 >= 0 = correct() busy(S(),closed(),stop(),false(),false(),false(),empty()) = 1 >= 0 = correct() busy(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = i + i2 + i3 + 1 >= i + i2 + i3 + 1 = idle(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) busy(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = i + i2 + i3 + 1 >= i + i2 + i3 + 1 = idle(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) busy(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = i + i2 + i3 + 1 >= i + i2 + i3 + 1 = idle(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) busy(B(),open(),stop(),false(),b2,b3,i) = b2 + b3 + i + 1 >= b2 + b3 + i + 1 = idle(B(),closed(),stop(),false(),b2,b3,i) busy(F(),open(),stop(),b1,false(),b3,i) = b3 + i + 1 >= b3 + i + 1 = idle(F(),closed(),stop(),b1,false(),b3,i) busy(S(),open(),stop(),b1,b2,false(),i) = b2 + i + 1 >= b2 + i + 1 = idle(S(),closed(),stop(),b1,b2,false(),i) busy(B(),d,stop(),true(),b2,b3,i) = b2 + b3 + i + 1 >= b2 + b3 + i + 1 = idle(B(),open(),stop(),false(),b2,b3,i) busy(F(),d,stop(),b1,true(),b3,i) = b3 + i + 2 >= b3 + i + 1 = idle(F(),open(),stop(),b1,false(),b3,i) busy(S(),d,stop(),b1,b2,true(),i) = b2 + i + 2 >= b2 + i + 1 = idle(S(),open(),stop(),b1,b2,false(),i) busy(B(),closed(),down(),b1,b2,b3,i) = b2 + b3 + i + 1 >= b2 + b3 + i + 1 = idle(B(),closed(),stop(),b1,b2,b3,i) busy(S(),closed(),up(),b1,b2,b3,i) = b2 + b3 + i + 1 >= b2 + b3 + i + 1 = idle(S(),closed(),stop(),b1,b2,b3,i) busy(B(),closed(),up(),true(),b2,b3,i) = b2 + b3 + i + 1 >= b2 + b3 + i + 1 = idle(B(),closed(),stop(),true(),b2,b3,i) busy(F(),closed(),up(),b1,true(),b3,i) = b3 + i + 2 >= b3 + i + 2 = idle(F(),closed(),stop(),b1,true(),b3,i) busy(F(),closed(),down(),b1,true(),b3,i) = b3 + i + 2 >= b3 + i + 2 = idle(F(),closed(),stop(),b1,true(),b3,i) busy(S(),closed(),down(),b1,b2,true(),i) = b2 + i + 2 >= b2 + i + 2 = idle(S(),closed(),stop(),b1,b2,true(),i) busy(B(),closed(),up(),false(),b2,b3,i) = b2 + b3 + i + 1 >= b2 + b3 + i + 1 = idle(BF(),closed(),up(),false(),b2,b3,i) busy(F(),closed(),up(),b1,false(),b3,i) = b3 + i + 1 >= b3 + i + 1 = idle(FS(),closed(),up(),b1,false(),b3,i) busy(F(),closed(),down(),b1,false(),b3,i) = b3 + i + 1 >= b3 + i + 1 = idle(BF(),closed(),down(),b1,false(),b3,i) busy(S(),closed(),down(),b1,b2,false(),i) = b2 + i + 1 >= b2 + i + 1 = idle(FS(),closed(),down(),b1,b2,false(),i) busy(BF(),closed(),up(),b1,b2,b3,i) = b2 + b3 + i + 1 >= b2 + b3 + i + 1 = idle(F(),closed(),up(),b1,b2,b3,i) busy(BF(),closed(),down(),b1,b2,b3,i) = b2 + b3 + i + 1 >= b2 + b3 + i + 1 = idle(B(),closed(),down(),b1,b2,b3,i) busy(FS(),closed(),up(),b1,b2,b3,i) = b2 + b3 + i + 1 >= b2 + b3 + i + 1 = idle(S(),closed(),up(),b1,b2,b3,i) busy(FS(),closed(),down(),b1,b2,b3,i) = b2 + b3 + i + 1 >= b2 + b3 + i + 1 = idle(F(),closed(),down(),b1,b2,b3,i) busy(B(),closed(),stop(),false(),true(),b3,i) = b3 + i + 2 >= b3 + i + 2 = idle(B(),closed(),up(),false(),true(),b3,i) busy(B(),closed(),stop(),false(),false(),true(),i) = i + 2 >= i + 2 = idle(B(),closed(),up(),false(),false(),true(),i) busy(F(),closed(),stop(),true(),false(),b3,i) = b3 + i + 1 >= b3 + i + 1 = idle(F(),closed(),down(),true(),false(),b3,i) busy(F(),closed(),stop(),false(),false(),true(),i) = i + 2 >= i + 2 = idle(F(),closed(),up(),false(),false(),true(),i) busy(S(),closed(),stop(),b1,true(),false(),i) = i + 2 >= i + 2 = idle(S(),closed(),down(),b1,true(),false(),i) busy(S(),closed(),stop(),true(),false(),false(),i) = i + 1 >= i + 1 = idle(S(),closed(),down(),true(),false(),false(),i) idle(fl,d,m,b1,b2,b3,empty()) = b2 + b3 + 1 >= b2 + b3 + 1 = busy(fl,d,m,b1,b2,b3,empty()) idle(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) = b2 + b3 + i + i2 + i3 + 1 >= b2 + b3 + i + i2 + i3 + 1 = busy(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) or(true(),b) = b + 1 >= 1 = true() or(false(),b) = b >= b = b problem: DPs: 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) 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#(F(),d,stop(),b1,true(),b3,i) -> idle#(F(),open(),stop(),b1,false(),b3,i) TRS: 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 Matrix Interpretation Processor: dimension: 1 interpretation: [idle#](x0, x1, x2, x3, x4, x5, x6) = x0 + x4 + 1, [busy#](x0, x1, x2, x3, x4, x5, x6) = x0 + x4 + 1, [or](x0, x1) = x0 + x1, [true] = 1, [idle](x0, x1, x2, x3, x4, x5, x6) = 0, [newbuttons](x0, x1, x2, x3) = 0, [S] = 1, [correct] = 0, [empty] = 0, [B] = 1, [down] = 0, [up] = 0, [open] = 0, [FS] = 1, [incorrect] = 0, [BF] = 1, [busy](x0, x1, x2, x3, x4, x5, x6) = 0, [false] = 0, [stop] = 0, [closed] = 0, [F] = 1, [start](x0) = 0 orientation: busy#(S(),closed(),stop(),true(),false(),false(),i) = 2 >= 2 = idle#(S(),closed(),down(),true(),false(),false(),i) idle#(fl,d,m,b1,b2,b3,empty()) = b2 + fl + 1 >= b2 + fl + 1 = busy#(fl,d,m,b1,b2,b3,empty()) busy#(S(),closed(),stop(),b1,true(),false(),i) = 3 >= 3 = idle#(S(),closed(),down(),b1,true(),false(),i) busy#(F(),closed(),stop(),false(),false(),true(),i) = 2 >= 2 = idle#(F(),closed(),up(),false(),false(),true(),i) busy#(F(),closed(),stop(),true(),false(),b3,i) = 2 >= 2 = idle#(F(),closed(),down(),true(),false(),b3,i) busy#(B(),closed(),stop(),false(),false(),true(),i) = 2 >= 2 = idle#(B(),closed(),up(),false(),false(),true(),i) busy#(B(),closed(),stop(),false(),true(),b3,i) = 3 >= 3 = idle#(B(),closed(),up(),false(),true(),b3,i) busy#(FS(),closed(),down(),b1,b2,b3,i) = b2 + 2 >= b2 + 2 = idle#(F(),closed(),down(),b1,b2,b3,i) busy#(FS(),closed(),up(),b1,b2,b3,i) = b2 + 2 >= b2 + 2 = idle#(S(),closed(),up(),b1,b2,b3,i) busy#(BF(),closed(),down(),b1,b2,b3,i) = b2 + 2 >= b2 + 2 = idle#(B(),closed(),down(),b1,b2,b3,i) busy#(BF(),closed(),up(),b1,b2,b3,i) = b2 + 2 >= b2 + 2 = idle#(F(),closed(),up(),b1,b2,b3,i) busy#(S(),closed(),down(),b1,b2,false(),i) = b2 + 2 >= b2 + 2 = idle#(FS(),closed(),down(),b1,b2,false(),i) busy#(F(),closed(),down(),b1,false(),b3,i) = 2 >= 2 = idle#(BF(),closed(),down(),b1,false(),b3,i) busy#(F(),closed(),up(),b1,false(),b3,i) = 2 >= 2 = idle#(FS(),closed(),up(),b1,false(),b3,i) busy#(B(),closed(),up(),false(),b2,b3,i) = b2 + 2 >= b2 + 2 = idle#(BF(),closed(),up(),false(),b2,b3,i) busy#(S(),closed(),down(),b1,b2,true(),i) = b2 + 2 >= b2 + 2 = idle#(S(),closed(),stop(),b1,b2,true(),i) busy#(F(),closed(),down(),b1,true(),b3,i) = 3 >= 3 = idle#(F(),closed(),stop(),b1,true(),b3,i) busy#(F(),closed(),up(),b1,true(),b3,i) = 3 >= 3 = idle#(F(),closed(),stop(),b1,true(),b3,i) busy#(B(),closed(),up(),true(),b2,b3,i) = b2 + 2 >= b2 + 2 = idle#(B(),closed(),stop(),true(),b2,b3,i) busy#(S(),closed(),up(),b1,b2,b3,i) = b2 + 2 >= b2 + 2 = idle#(S(),closed(),stop(),b1,b2,b3,i) busy#(B(),closed(),down(),b1,b2,b3,i) = b2 + 2 >= b2 + 2 = idle#(B(),closed(),stop(),b1,b2,b3,i) busy#(F(),d,stop(),b1,true(),b3,i) = 3 >= 2 = idle#(F(),open(),stop(),b1,false(),b3,i) start(i) = 0 >= 0 = busy(F(),closed(),stop(),false(),false(),false(),i) busy(BF(),d,stop(),b1,b2,b3,i) = 0 >= 0 = incorrect() busy(FS(),d,stop(),b1,b2,b3,i) = 0 >= 0 = incorrect() busy(fl,open(),up(),b1,b2,b3,i) = 0 >= 0 = incorrect() busy(fl,open(),down(),b1,b2,b3,i) = 0 >= 0 = incorrect() busy(B(),closed(),stop(),false(),false(),false(),empty()) = 0 >= 0 = correct() busy(F(),closed(),stop(),false(),false(),false(),empty()) = 0 >= 0 = correct() busy(S(),closed(),stop(),false(),false(),false(),empty()) = 0 >= 0 = correct() busy(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = 0 >= 0 = idle(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) busy(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = 0 >= 0 = idle(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) busy(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = 0 >= 0 = idle(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) busy(B(),open(),stop(),false(),b2,b3,i) = 0 >= 0 = idle(B(),closed(),stop(),false(),b2,b3,i) busy(F(),open(),stop(),b1,false(),b3,i) = 0 >= 0 = idle(F(),closed(),stop(),b1,false(),b3,i) busy(S(),open(),stop(),b1,b2,false(),i) = 0 >= 0 = idle(S(),closed(),stop(),b1,b2,false(),i) busy(B(),d,stop(),true(),b2,b3,i) = 0 >= 0 = idle(B(),open(),stop(),false(),b2,b3,i) busy(F(),d,stop(),b1,true(),b3,i) = 0 >= 0 = idle(F(),open(),stop(),b1,false(),b3,i) busy(S(),d,stop(),b1,b2,true(),i) = 0 >= 0 = idle(S(),open(),stop(),b1,b2,false(),i) busy(B(),closed(),down(),b1,b2,b3,i) = 0 >= 0 = idle(B(),closed(),stop(),b1,b2,b3,i) busy(S(),closed(),up(),b1,b2,b3,i) = 0 >= 0 = idle(S(),closed(),stop(),b1,b2,b3,i) busy(B(),closed(),up(),true(),b2,b3,i) = 0 >= 0 = idle(B(),closed(),stop(),true(),b2,b3,i) busy(F(),closed(),up(),b1,true(),b3,i) = 0 >= 0 = idle(F(),closed(),stop(),b1,true(),b3,i) busy(F(),closed(),down(),b1,true(),b3,i) = 0 >= 0 = idle(F(),closed(),stop(),b1,true(),b3,i) busy(S(),closed(),down(),b1,b2,true(),i) = 0 >= 0 = idle(S(),closed(),stop(),b1,b2,true(),i) busy(B(),closed(),up(),false(),b2,b3,i) = 0 >= 0 = idle(BF(),closed(),up(),false(),b2,b3,i) busy(F(),closed(),up(),b1,false(),b3,i) = 0 >= 0 = idle(FS(),closed(),up(),b1,false(),b3,i) busy(F(),closed(),down(),b1,false(),b3,i) = 0 >= 0 = idle(BF(),closed(),down(),b1,false(),b3,i) busy(S(),closed(),down(),b1,b2,false(),i) = 0 >= 0 = idle(FS(),closed(),down(),b1,b2,false(),i) busy(BF(),closed(),up(),b1,b2,b3,i) = 0 >= 0 = idle(F(),closed(),up(),b1,b2,b3,i) busy(BF(),closed(),down(),b1,b2,b3,i) = 0 >= 0 = idle(B(),closed(),down(),b1,b2,b3,i) busy(FS(),closed(),up(),b1,b2,b3,i) = 0 >= 0 = idle(S(),closed(),up(),b1,b2,b3,i) busy(FS(),closed(),down(),b1,b2,b3,i) = 0 >= 0 = idle(F(),closed(),down(),b1,b2,b3,i) busy(B(),closed(),stop(),false(),true(),b3,i) = 0 >= 0 = idle(B(),closed(),up(),false(),true(),b3,i) busy(B(),closed(),stop(),false(),false(),true(),i) = 0 >= 0 = idle(B(),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(F(),closed(),stop(),false(),false(),true(),i) = 0 >= 0 = idle(F(),closed(),up(),false(),false(),true(),i) busy(S(),closed(),stop(),b1,true(),false(),i) = 0 >= 0 = idle(S(),closed(),down(),b1,true(),false(),i) busy(S(),closed(),stop(),true(),false(),false(),i) = 0 >= 0 = idle(S(),closed(),down(),true(),false(),false(),i) idle(fl,d,m,b1,b2,b3,empty()) = 0 >= 0 = busy(fl,d,m,b1,b2,b3,empty()) idle(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) = 0 >= 0 = busy(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i) or(true(),b) = b + 1 >= 1 = true() or(false(),b) = b >= b = b problem: DPs: 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) 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: 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 Open