COF_T10
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 (or (=< 0 ?X) (=< 0 (neg ?X)))) (forall ?X (=> (not (= ?X 0)) (or (not (=< 0 ?X)) (not (=< 0 (neg ?X)))))) (forall (?X ?Y) (=> (and (=< 0 ?X) (=< 0 ?Y)) (=< 0 (+ ?X ?Y)))) (forall (?X ?Y) (<=> (=< ?X ?Y) (=< 0 (+ ?Y (neg ?X)))))
Conclusion:
(forall ?X (= (neg (neg ?X)) ?X))