Change the weight function

[hferee]

I believe that the weight function on formulas, from which the termination ordering is defined, could be replaced with the so-called "Dyckhoff's degree".

It replaces sums with max, making it linear in the depth of the formula, and not in its size.

This has no effect on efficiency, but would help better understand the computational complexity of our construction.