(prover (name z3) (version "Z3 version 4.8.12 - 64 bit") (cmd <unknown>) (binary z3) (ulimit (time memory )) (sat "(^sat)|(s SATISFIABLE)") (unsat "unsat|(s UNSATISFIABLE)") (produces_proof false))