[Termtools] SRS-standard

[Harald Roman Zankl]

Hi,

Zitat von Johannes Waldmann <waldmann at imn.htwk-leipzig.de>:

>...
> Did TTT2 use the "SAT for loop-detection" idea this time?
>...

Yes. All loops found within the DP-setting are due to this idea.
We just searched for looping reductions of lenth at most 20 where
all terms within the loop are at most of length 20. Probably other
configurations produce better results ...

Harald.