In presence of conjectures, TPTP requires us to prove
their conjunction, but no conjectures means |- false.
This is awkward, and most provers treat conjectures
disjunctively, as in a sequent. We follow TPTP here.

(OCaml polymorphic equality fails on big nums)

sudoku example now uses arrays only