title: How to model Einstein's ships puzzle in Prover9 (first order logic)
body: <p>I need to model the folowing puzzle in Prover9</p>
  
  <blockquote>
    <p>There are 5 ships in a port:</p>
    
    <ol>
    <li>The Greek ship leaves at six and carries coffee.</li>
    <li>The Ship in the middle has a black chimney.</li>
    <li>The English ship leaves at nine.</li>
    <li>The French ship with blue chimney is to the left of a ship that carries coffee.</li>
    <li>To the right of the ship carrying cocoa is a ship going to Marseille.</li>
    <li>The Brazilian ship is heading for Manila.</li>
    <li>Next to the ship carrying rice is a ship with a green chimney.</li>
    <li>A ship going to Genoa leaves at five.</li>
    <li>The Spanish ship leaves at seven and is to the right of the ship going to Marseille.</li>
    <li>The ship with a red chimney goes to Hamburg.</li>
    <li>Next to the ship leaving at seven is a ship with a white chimney.</li>
    <li>The ship on the border carries corn.</li>
    <li>The ship with a black chimney leaves at eight.</li>
    <li>The ship carrying corn is anchored next to the ship carrying rice.</li>
    <li>The ship to Hamburg leaves at six.</li>
    </ol>
    
    <p>Which ship goes to Port Said? Which ship carries tea?</p>
  </blockquote>
  
  <p>As far as I've seen prover9 accepts first order logic clauses. But I'm really not got at converting natural language to fol. Could someone tell me how to model this in first order logic please, maybe show me how to convert the first statement?</p>