MAYBE
UNSAT
user error ("/tmp/SMTS19810642601066908520" (line 142, column 15):
unexpected "_"
expecting digit or ")")