COF_T10a
Premises:
(forall (?X ?Y ?Z) (= (+ ?X (+ ?Y ?Z)) (+ (+ ?X ?Y) ?Z))) (forall (?X ?Y) (= (+ ?X ?Y) (+ ?Y ?X))) (forall ?X (= (+ ?X 0) ?X)) (forall ?X (= (+ ?X (neg ?X)) 0)) (forall (?X ?Y ?Z) (=> (= (+ ?Z ?X) (+ ?Z ?Y)) (= ?X ?Y)))
Conclusion:
(forall ?X (= (neg (neg ?X)) ?X))