Coursework from CTU. The program generates the formalism of the railway station in the 1st order logic (TPTP format) for the provers and model checkers