the TerminationRegression test checks if counterexamples are found

counting from 31 down to 0 instead of from 0 up to 31

1) The termination checker (of which only 1 instance exists per run)
2) The modules which depend on a size function (of which several
   instances per run might exist, one per size function impl)

but do it in sizeDecreasing, because DRY, and because it provides more
flexibility for other potential implementations of sizeDecreasing

(but not timeout)