[Termination tools] small hard string termination problem

[Johannes Waldmann]

Dear termination provers,

for a few weeks we (jambox, matchbox, torpa) have been trying
to decide termination of the string rewriting system

   ( RULES 1 0 1 -> 0 0 0 , 0 0 0 -> 1 1 1 )

None of the available tools seem to find a proof
(and neither do two of the not-yet-available tools...)
and we really don't know the termination status ourselves.

I think this is a very nice problem so it shouldn't get hidden
among the (secret) submissions to the next competition
and that's why I'm posting it here.

Perhaps there is a machine proof outside the one-minute
competition format, or one that requires hand-tuned parameter settings.
I'd encourage other tool authors to give it a try.

Best regards,
-- 
-- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 --
---- http://www.imn.htwk-leipzig.de/~waldmann/ -------