J008
(forall ?X (forall ?Y (or (not (= ?X ?Y)) (= (succ ?X) (succ ?Y)))))
Proof Trace