[Termtools] strange proof

[Johannes Waldmann]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Jörg Endrullis notes that this proof is at least incomplete:
http://www.lri.fr/~marche/termination-competition/2007/webform.cgi?command=viewres&file=srs-standard.db&tool=torpa&prob=SRS.Gebhardt.02.srs

I know that torpa-1.7 can prove termination
http://dfa.imn.htwk-leipzig.de/~waldmann/running/training/07/SRS/output/torpa-1.7/input/tpdb-3.2/Gebhardt/02.srs
and it needs around 60 seconds (it's not deterministic).

Perhaps it was killed during printout? Still strange,
because after "chose polynomial interpretation" (the first)
it should have printed "remaining rules",
instead it continues.

Best regards, Johannes.



-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.2 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFGZG6B3ZnXZuOVyMIRAoHEAKCaytfH6n3ZbIq9buq0Hi2Q3l3YzACdGYLU
AdApQH15xsByvxcx+oP3KHA=
=cCmy
-----END PGP SIGNATURE-----