A lower bound of ?(n/logn) space is shown for two natural proof systems for equational logic. The method introduces an edging game, a generalization of the pebble game [P].
