sat(+CNf) call a sat solver on the conjunctive normal formula CNF
(undocumented)
1. prolog::sat_1::sat/1(int ARG1)():