Donkey
(Click "Prove" to run)
Premises:
;All owners of animals beat them. (forall (?X ?Y) (=> (and (owns ?X ?Y) (animal ?Y)) (beats ?X ?Y))) ; All donkeys are animals. (forall ?X (=> (donkey ?X) (animal ?X)))
Conclusion:
; Prove that this formula is entailed by the premise. ; If a donkey is owned, it is beaten. (forall (?X ?Y) (=> (and (donkey ?Y) (owns ?X ?Y)) (exists ?Z (and (animal ?Z) (donkey ?Z) (= ?Y ?Z) (beats ?X ?Z)))))
Proof Trace