signature { automatic } theory
{
A (p1 ^ <>!p1)
}