signature { automatic } theory
{
A (D (P1))
}