Automated Reasoning I

Write out a truth table to determine if each Conjecture is a logical consequence of the Axioms.

Axioms Conjectures
p | q | r r => (p | q) (q & r) => p ~p | q | r q | r q & (r => p)
p => q ~q | p p | q ~(p & q) (~q => p) => (q | ~p)
q | p p => q q => (~r | p) r p

Axioms	Conjectures
`p \| q \| r r => (p \| q) (q & r) => p ~p \| q \| r`	`q \| r q & (r => p)`
`p => q ~q \| p p \| q ~(p & q)`	`(~q => p) => (q \| ~p)`
`q \| p p => q q => (~r \| p) r`	`p`

Translate the following problem into 1st order logic:

Suming, Yi, and Yury are students, and are the only three students. If a student works hard then they get a good grade. At least one of the students works hard. Therefore at least one student will get a good grade.

Note that they are the "only" three students - you need to think about how to encode that.