We have extracted non-linear smt2 formulae from the Flyspeck Project.
Among formulae, we have UNSATs, \( \delta \)-SATs (\(\delta = 10^{-3} \)), and Timeouts (= 5mins). We were able to verify instances of the UNSAT results. All the experiments below are run on a machine of with a 48-core 2.2GHz AMD Opteron Processor and 512GB of RAM.