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