Your problem is to use first-order logic to represent the following example of reasoning, and use the Prover9 theorem prover to prove that the reasoning is valid.
Use the following template file to create your Prover9 encoding of the problem: ballooning_pigs.p9
Marks: There are two marks for each sentence, making a total of 22 marks.
| A1 | All, who neither dance on tightropes nor eat penny-buns, are old. |
| A2 | Pigs, that are liable to giddiness, are treated with respect. |
| A3 | A wise balloonist takes an umbrella with him. |
| A4 | No one ought to lunch in public who looks ridiculous and eats penny-buns. |
| A5 | Young creatures, who go up in balloons, are liable to giddiness. |
| A6 | Fat creatures, who look ridiculous, may lunch in public, provided that they do not dance on tightropes. |
| A7 | No wise creatures dance on tightropes, if liable to giddiness. |
| A8 | A pig looks ridiculous, carrying an umbrella. |
| A9 | All, who do not dance on tightropes, and who are treated with respect are fat. |
| A10 | No one is young and old at the same time. |
| Goal | No wise young pigs go up in balloons. |