HTab-1.5.4: examples/sat/test17.frm

signature { automatic } theory
{
[R1](<R3>[R1]p3 --> n1 --> n2:n1 --> n3:n3:n4);
n1 --> ([R1] p3 v <R3><R1>[R2] (p2 v [R1]p4));
(n1:n3) v (n3:n1) <--> [R1](<R3>(n1 --> n3 ))
}