MAYBE
201.11/60.83	MAYBE
201.11/60.83	
201.11/60.83	Problem:
201.11/60.83	 start(i) -> busy(F(),closed(),stop(),false(),false(),false(),i)
201.11/60.83	 busy(BF(),d,stop(),b1,b2,b3,i) -> incorrect()
201.11/60.83	 busy(FS(),d,stop(),b1,b2,b3,i) -> incorrect()
201.11/60.83	 busy(fl,open(),up(),b1,b2,b3,i) -> incorrect()
201.11/60.83	 busy(fl,open(),down(),b1,b2,b3,i) -> incorrect()
201.11/60.83	 busy(B(),closed(),stop(),false(),false(),false(),empty()) -> correct()
201.11/60.83	 busy(F(),closed(),stop(),false(),false(),false(),empty()) -> correct()
201.11/60.83	 busy(S(),closed(),stop(),false(),false(),false(),empty()) -> correct()
201.11/60.83	 busy(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) ->
201.11/60.83	 idle(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i))
201.11/60.83	 busy(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) ->
201.11/60.83	 idle(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i))
201.11/60.83	 busy(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) ->
201.11/60.83	 idle(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i))
201.11/60.83	 busy(B(),open(),stop(),false(),b2,b3,i) -> idle(B(),closed(),stop(),false(),b2,b3,i)
201.11/60.83	 busy(F(),open(),stop(),b1,false(),b3,i) -> idle(F(),closed(),stop(),b1,false(),b3,i)
201.11/60.83	 busy(S(),open(),stop(),b1,b2,false(),i) -> idle(S(),closed(),stop(),b1,b2,false(),i)
201.11/60.83	 busy(B(),d,stop(),true(),b2,b3,i) -> idle(B(),open(),stop(),false(),b2,b3,i)
201.11/60.83	 busy(F(),d,stop(),b1,true(),b3,i) -> idle(F(),open(),stop(),b1,false(),b3,i)
201.11/60.83	 busy(S(),d,stop(),b1,b2,true(),i) -> idle(S(),open(),stop(),b1,b2,false(),i)
201.11/60.83	 busy(B(),closed(),down(),b1,b2,b3,i) -> idle(B(),closed(),stop(),b1,b2,b3,i)
201.11/60.83	 busy(S(),closed(),up(),b1,b2,b3,i) -> idle(S(),closed(),stop(),b1,b2,b3,i)
201.11/60.83	 busy(B(),closed(),up(),true(),b2,b3,i) -> idle(B(),closed(),stop(),true(),b2,b3,i)
201.11/60.83	 busy(F(),closed(),up(),b1,true(),b3,i) -> idle(F(),closed(),stop(),b1,true(),b3,i)
201.11/60.83	 busy(F(),closed(),down(),b1,true(),b3,i) -> idle(F(),closed(),stop(),b1,true(),b3,i)
201.11/60.83	 busy(S(),closed(),down(),b1,b2,true(),i) -> idle(S(),closed(),stop(),b1,b2,true(),i)
201.11/60.83	 busy(B(),closed(),up(),false(),b2,b3,i) -> idle(BF(),closed(),up(),false(),b2,b3,i)
201.11/60.83	 busy(F(),closed(),up(),b1,false(),b3,i) -> idle(FS(),closed(),up(),b1,false(),b3,i)
201.11/60.83	 busy(F(),closed(),down(),b1,false(),b3,i) -> idle(BF(),closed(),down(),b1,false(),b3,i)
201.11/60.83	 busy(S(),closed(),down(),b1,b2,false(),i) -> idle(FS(),closed(),down(),b1,b2,false(),i)
201.11/60.83	 busy(BF(),closed(),up(),b1,b2,b3,i) -> idle(F(),closed(),up(),b1,b2,b3,i)
201.11/60.83	 busy(BF(),closed(),down(),b1,b2,b3,i) -> idle(B(),closed(),down(),b1,b2,b3,i)
201.11/60.83	 busy(FS(),closed(),up(),b1,b2,b3,i) -> idle(S(),closed(),up(),b1,b2,b3,i)
201.11/60.83	 busy(FS(),closed(),down(),b1,b2,b3,i) -> idle(F(),closed(),down(),b1,b2,b3,i)
201.11/60.83	 busy(B(),closed(),stop(),false(),true(),b3,i) -> idle(B(),closed(),up(),false(),true(),b3,i)
201.11/60.83	 busy(B(),closed(),stop(),false(),false(),true(),i) ->
201.11/60.83	 idle(B(),closed(),up(),false(),false(),true(),i)
201.11/60.83	 busy(F(),closed(),stop(),true(),false(),b3,i) -> idle(F(),closed(),down(),true(),false(),b3,i)
201.11/60.83	 busy(F(),closed(),stop(),false(),false(),true(),i) ->
201.11/60.83	 idle(F(),closed(),up(),false(),false(),true(),i)
201.11/60.83	 busy(S(),closed(),stop(),b1,true(),false(),i) -> idle(S(),closed(),down(),b1,true(),false(),i)
201.11/60.83	 busy(S(),closed(),stop(),true(),false(),false(),i) ->
201.11/60.83	 idle(S(),closed(),down(),true(),false(),false(),i)
201.11/60.83	 idle(fl,d,m,b1,b2,b3,empty()) -> busy(fl,d,m,b1,b2,b3,empty())
201.11/60.83	 idle(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) -> busy(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i)
201.11/60.83	 or(true(),b) -> true()
201.11/60.83	 or(false(),b) -> b
201.11/60.83	
201.11/60.83	Proof:
201.11/60.83	 Open
201.11/60.84	EOF