% had bad model building at some point with chain blocking

signature { automatic } theory

{
A<><>!N1;
[](P1 v N1) & []!P1
}