HTab-1.6.1: examples/unsat/test22.frm
begin n1:<>(!((<>(n1 & p1) & <>(n1 & p2))-> <>(p1 & p2))); <>(p1 v <>(p1 v <>(p1 v <>(p1 v <>(p1 v <>(p1 v <>(n2:n1))))))); []!p1; [][]!p1; [][][]!p1; [][][][]!p1; [][][][][]!p1; n2:<>true end
begin n1:<>(!((<>(n1 & p1) & <>(n1 & p2))-> <>(p1 & p2))); <>(p1 v <>(p1 v <>(p1 v <>(p1 v <>(p1 v <>(p1 v <>(n2:n1))))))); []!p1; [][]!p1; [][][]!p1; [][][][]!p1; [][][][][]!p1; n2:<>true end