Function sos_refutes 

pub fn sos_refutes(num_vars: usize, clauses: &[Vec<Lit>]) -> bool

Does a degree-2 Positivstellensatz (diagonal SoS) refutation of the CNF exist over ℚ? Sound: a true result is a certified UNSAT. Declines (false) when no degree-2 refutation exists or the instance exceeds [MAX_VARS] / the elimination caps.