Claude Marché wrote: > Done. With 20 seconds time limit, no tool find any proof. Sorry, I overlooked torpa's syntax error. And matchbox does in fact find a proof? http://www.lri.fr/~marche/termination-competition/2007/matchbox/results/SRS.Waldmann.jw1.srs.stdout Best regards, Johannes.