HTab-1.5.4: examples/sat/test12.frm

signature { automatic } theory
{ 
n1:[](n2 <--> n3 v n5);
[](n1: (n2 <--> p1));
[][]<>(p1 <--> []p3) <--> <><>p4;
<><><>(p2 v n2:p3) <--> (<>[]p3 v <>[]p2)   
}