% Interpolation formula

signature { automatic } theory
{
!((<>p1 & <>!p1) --> (([](p2 --> N1) --> <>!p2)))
}