Your problem is to use first-order logic to represent the following example of reasoning, and use the Prover9 theorem prover to prove (or possibly disprove) that the reasoning is valid.
Use the following template file to create your Prover9 encoding of the problem: invalid_syllogism.p9
Marks: There are two marks for each sentence, making a total of 6 marks.
| A1 | Some rhombuses are equilateral. |
| A2 | Some equilaterals are triangular. |
| Goal | Some rhombuses are triangular. |