HTab-1.5.4: examples/sat/test30.frm

signature { automatic } theory
{
A(!N0 v !N1)
}