always:
         nonexecutable dunk(P,T) if flush(T).
         nonexecutable dunk(P,T) if dunk(P1,T), P <> P1.
         nonexecutable dunk(P,T) if dunk(P,T1), T <> T1.