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