Implement conditional redundancy handler

[mezpusz]

First checkpoint in a series of improving what was known (briefly) as InstanceRedundancyHandler (cf. irc flag).

• Renamed to ConditionalRedundancyHandler and added more general functionality.
• Accordingly added options and statistics to reflect the current features.
• Refactored binary resolution and superposition code a bit, which contained some unused stuff.
• Removed the incompleteness flag in Options.cpp as I believe I have a proof of completeness.

Some motivation statistics by running a single strategy (discount/otter) for 10s over TPTP:

	baseline	crc	croc	crac	crlc
discount	9985(0)	10013(124)	10001(147)	10041(163)	9979(124)
otter	9721(0)	9764(110)	9770(142)	9772(130)	9745(101)
	baseline	cr[oa]c	cr[ol]c	cr[al]c	cr[oal]c
discount	9985(0)	10018(172)	9964(135)	10009(163)	9988(169)
otter	9721(0)	9785(163)	9766(143)	9771(131)	9780(161)

(values are "number of solved problem (number of uniques w.r.t. baseline)") (cr[oal]c means -crc on -croc on -crac on -crlc on)

More info/documentation/evaluation comes later as this is work in progress.

[mezpusz]

the AVATAR integration seems much less painful than expected.

We could still try to extend it to unfrozen inferences later. But this version seemed like a good starting point. :)