signature { automatic } theory
{
!P1 v ![R1](!N1 v !D(!P2 v N1:(N1 v P3)));
!N1 v !D(P1 v !A(!N1 v !N1:(!N1 v !P1)));
P3 v A(!P3 v [R1](!N1 v D(!P2 v P3)));
P1 v [R1](P3 v A(N1 v N1:(!P3 v !N1)));
!N1 v !A(N1 v !D(P2 v ![R1](P1 v N1)));
!P1 v !A(P3 v !D(N1 v N1:(!N1 v !P2)));
N1 v !A(P1 v !N1:(!N1 v [R1](P1 v P3)));
!P1 v !D(!P1 v !A(N1 v !N1:(P1 v !P3)));
!N1 v !A(!N1 v !D(N1 v N1:(P2 v N1)));
N1 v ![R1](P1 v [R1](!P2 v D(!P1 v P3)));
N1 v A(!P2 v D(!P1 v ![R1](!P3 v !N1)));
!P2 v N1:(N1 v [R1](!P2 v !A(P3 v N1)));
N1 v [R1](N1 v !N1:(P3 v !N1:(!P2 v N1)))
}