Use a datagen-based solver to find simple counter-examples. Note that
this solver returns Unknown most of the time, so it is best to combine
it with a full-fledged solver.

PortfolioSolver allows us to combine solvers and have them run in
parallel. The first result (!= Unknown) is used. Solvers can be selected
for verification using the --solvers option.