PrALTabc
Premises:
(< a b) (< b c) (forall (?X ?Y) (<=> (< ?X ?Y) (exists ?Z (and (not (= 0 ?Z)) (= (+ ?X ?Z) ?Y))))) (forall (?X ?Y) (=> (or (not (= 0 ?X)) (not (= 0 ?Y))) (not (= 0 (+ ?X ?Y))))) (forall (?X ?Y ?Z ?W ?T) (=> (and (= (+ ?X ?Y) ?Z) (= (+ ?Z ?W) ?T)) (= (+ ?X (+ ?Y ?W)) ?T)))
Conclusion:
(< a c)