PAOE05Ind
Premises:
(forall (?X ?Y ?Z) (= (* ?X (+ ?Y ?Z)) (+ (* ?X ?Y) (* ?X ?Z)))) (forall ?X (<=> (even ?X) (exists ?Y (= ?X (+ ?Y ?Y))))) (forall ?X (<=> (odd ?X) (not (even ?X)))) (forall (?X ?Y) (= (* ?X ?Y) (* ?Y ?X)))
Conclusion:
(forall (?X ?Y) (=> (even ?X) (even (* ?X ?Y))))