signature { automatic } theory
{
A (p1 ^ []!p1)
}