Added test for or-pos aux axiom.

Note that the proof is not correct for the last case.  The
tautology clause is not flat but used directly with @clause.