lifting rules send cwm into a tailspin

I'm trying to do some lifting and policy reasoning,
but it's not working. I reduced it to this testcase:

--8<--
@keywords is, of, a.

@forAll S, P, O.

@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix s: <http://www.w3.org/2000/01/rdf-schema#>.

# truth predicate, limited to simple triples. hmm.
{ ?F a Truth; log:includes { S P O }. P a s:Property }
 => { S P O }.
log:implies a s:Property.

{ { S a Man } => { S a Mortal } } a Truth.
socrates a Man.
--8<--

If I put that in test/truthpred.n3 and run it thusly

$ python cwm.py test/truthpred.n3 --chatty=10 --think

I get an endless stream of...
                  warning - reopen formula:{1216111124 type Man}
                  warning - reopen formula:{1216111124 type Man}
                  warning - reopen formula:{1216111124 type Man}
                  warning - reopen formula:{1216111124 type Man}
                  warning - reopen formula:{1216111124 type Man}
                  warning - reopen formula:{1216111124 type Man}

I'm not sure how this sort of lifting is supposed to work
when S and O bind to formulas with variables, but I don't think
it should send cwm into an infinite loop.

-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/
D3C2 887B 0F92 6005 C541  0875 0F91 96DE 6E52 C29E