PAOE07Ind
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))) (forall (?X ?Y) (= (+ ?X ?Y) (+ ?Y ?X))) (odd (* (succ 0) (succ 0))) (even (* 0 0)) (forall ?X (even (* 0 ?X))) (forall (?X ?Y) (=> (even ?X) (even (* ?X ?Y)))) (forall (?X ?Y) (=> (odd (* ?X ?Y)) (even (* (succ ?X) ?Y)))) (forall (?X ?Y) (=> (odd (* ?X ?Y)) (even (* ?X (succ ?Y ))))) (forall (?X ?Y) (=> (even (* ?X ?Y)) (or (even ?X) (even ?Y))))
Conclusion:
(forall (?X ?Y) (=> (odd (* ?X ?Y)) (odd ?X)))