Unification of new clauses (produced during saturation) can e.g. focus in new unification literals produced by factoring or paramodulation. Using all eligible literals (negative equalities) can lead to non-solvability of unification constraints. At the moment, the idea is to flag clauses with their origin (i.e. paramodulation) and then use the respectively created unification literal first. This is buggy at the moment, since the flag (acutally not a flag, but a infereceorigin) gets overriden/replaced.
Unification of new clauses (produced during saturation) can e.g. focus in new unification literals produced by factoring or paramodulation. Using all eligible literals (negative equalities) can lead to non-solvability of unification constraints. At the moment, the idea is to flag clauses with their origin (i.e. paramodulation) and then use the respectively created unification literal first. This is buggy at the moment, since the flag (acutally not a flag, but a infereceorigin) gets overriden/replaced.