HTab-1.6.1: examples/sat/test18.frm

begin
([R1] p1 )<--> ([R3]p1 <--> <R2>[R1]!p3);
n1: [R2]<R1>p1 <--> p2 --> p3;
false --> (false <--> n1:n3)
end