Ordering check with applied terms + optimised unidirectional comparison for LPO and KBO

[mezpusz]

This PR refactors functionality of KBO and LPO such that two terms can be compared modulo some substitution without creating the result of the application. Some notes:

• The overhead for regular terms on which no substitution has to be applied should be minimal.
• The new functionality is only used in the main check for demodulation, but it would be possible to use it elsewhere (e.g. in superposition, binary resolution, demodulation helper, subsumption demodulation, etc.)
• KBOForEPR has been removed as the use case in my opinion is not that prevalent and the code does not give a major improvement over KBO.
• SKIKBO has not been adapted, but I did not remove it due to some functionaility being used elsewhere.

Additionally, a unidirectional check has been implemented for KBO and exposed for LPO. This is far from super optimal, but it's a bit more efficient than the bidirectional check when we don't need the latter.

I did some optimisations here and there in other parts too, see comments below.

[quickbeam123]

Will look forward to doing some performance checks with this one!

[MichaelRawson]

Thanks for changes! Fine to merge for me, imagine @quickbeam123 would like to check some perf.

[mezpusz]

@joe-hauns Thanks for the review! I tried to address your comments, but let me know if there is something I misunderstood, or is still not satisfactory.

[quickbeam123]

Is this stable/ready for one final quick round of my checks?