[Termtools] another bunch of small hard SRS problems

[Johannes Waldmann]

Here is the list of 335 SRS of total size 12, alphabet size 3
that could not be done by last year's provers.
As with the previous list, I think the enumeration is complete
(it took about 4 CPU weeks).

How was the enumeration done?
1. generate all strings of length 12, over 3 letter alphabet
2. for each string, insert "->" and "," everywhere to get a SRS
3. check for rule removal by linear weights (simplex method)
4. check for loop (enumeration of forward closures)
5. check for RFC-matchboundedness
6. call external provers
All of 3-5 uses Matchbox implementations (not calling external
programs) with sharp timeouts. Of course there are some optimizations
(avoid generation of isomorphic copies, the loop check is done
a bit earlier (after each insertion of ",") etc.) Andreas Gebhardt
was helpful with installing and running the external provers.

This was done with 60 seconds limit on a 2 GHz Pentium 4,
so in fact some systems might be solvable on more current hardware
(which I don't have). If you have, and can do a re-run of the provers
(last year's official versions from Claude's web site)
and notice gross differences, then please tell me.

It is not clear whether this problem set should go into TPDB
(I think it should) and whether it should be used in full
for the upcoming comeptition (I don't know).
In any case I think it should be made available.

In fact the competition committee encourages this procedure:
if you propose "public" problems for inclusion in TPDB,
then post them on your web site and announce them here.
(Since the TPDB will be updated only once a year,
after the inclusion of the new public and secret problems.)

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