HTab-1.5.4: examples/sat/down01.frm

signature { automatic } theory
{
N2 & <>( down N3 . ( N1:(N2 & !N3)))
}