Robbins Algebra Lemmas

LEMMA 1.   Hypothesis  C + D = C.

lemma1.in - Strategy "basic-n-pair", that is, basic
paramodulation, pure best-first search, and the pair
algorithm.  Max-weight=30.

lemma1.proof --  Proof in 1902 seconds on an IBM rs6000.
This proof is different from the one in the paper (which
is from 1992).

LEMMA 2.   Hypothesis  n(C + D) = n(C).

lemma2.in -- This uses strategy "start-n-pair", that is,
no special paramodulation strategy, pure best-first
search, and the pair algorithm.  Max-weight=34.

lemma2.proof -- Proof in 608688 seconds on an IBM rs6000.
The proof is slightly different from the one in the paper:
this one is new, the one in the paper is the original,
from an earlier version of EQP.