fix URR to be (really) complete also under AVATAR

[quickbeam123]

Currently, the following will happily saturate and report SAT (on an unsat problem)

./vampire_rel_master_6966 Problems/SYN/SYN941+1.p --decode ott+10_1:1_si=on:rtra=on:urr=on:br=off:amm=off_0 --random_seed 148952160

(on your machine, the random seed might need to be altered, but the problem is small and the probability of trouble quite high).

The issue is that we work with binary_resolution = off and urr as the saving grace of completeness for a Horn problem (which SYN941+1 is). URR implements a heuristic which makes it happy on generating the first empty clauses from a given parent. However, in this case, we need all the urr resolvents to close all the AVATAR branches.

This PR adds an option to skip the mentioned heuristic (urr=full) and also updates Options::complete to properly reflect when we are complete and when not. Newly, the above reports

% Termination reason: Refutation not found, incomplete strategy

[hzzv]

Looks good to me!

[MichaelRawson]

Nice. If you think the check for _full might be in the hot path, we could make URResolution template<bool full> URResolution to save some tiny amount of branching...but probably it doesn't matter.

[MichaelRawson]

Conflicts are because URResolution doesn't need to USE_ALLOCATOR. Should be a quick rebase, lmk if you want me to fix it.