HTab-1.5.4: examples/unsat/interpol.frm
% Interpolation formula
signature { automatic } theory
{
!((<>p1 & <>!p1) --> (([](p2 --> N1) --> <>!p2)))
}
% Interpolation formula
signature { automatic } theory
{
!((<>p1 & <>!p1) --> (([](p2 --> N1) --> <>!p2)))
}