Given a set of xor clauses, all generated clauses of size <=4canbefoundbya"path"thatdoesnotcontainanyclauseofsize> 4. If this conjecture is true, we can benefit from a strong abstraction with a ``little'' generation cost.
For instance, in this case, the limitation does not allow to infer the clause `{2, 12, 22}`, but this clause can be obtained by xor-ing all the input clauses.