signature { automatic } theory
{

P1 |  P2 ;
P1 | !P2;
!P1
}