HTab-1.5.4: examples/unsat/test36.frm

signature { automatic } theory
{
!((down (N1 dia (N1 ^ p1) )) --> p1)
}