If you can find a short example in which tlapm hangs after it has begun proving obligations, we would appreciate seeing it.
In fact nothing is wrong with tlapm. I just sometimes believe it is able to prove a step but realize, because
of the time it takes, that I would rather split the goal into simpler ones.
--
FL