of AND and OR clauses.  The key point here is that an OR on the
predicate side has to be treated gingerly: we may be able to prove
that the OR is implied even when no one of its components is implied.
For example (x OR y) implies (x OR y OR z) even though no one of x,
y, or z can be individually proven.  This code handles both the
example shown recently by Sergey Koshcheyev and the one shown last
October by Dawid Kuroczko.