signature { automatic } theory

{
 P1 & !P1
}