A SAT instance is given below in the DIMACS format. (a) What is the CNF formula captured by this instance? (b) By inspection, answer whether the instance is satisfiable, and why. (c) If it is not...

A SAT instance is given below in the DIMACS format. (a) What is the CNF formula captured by this instance? (b) By inspection, answer whether the instance is satisfiable, and why. (c) If it is not satisfiable, then what is the minimal number of rows that must be deleted before the instance becomes satisfiable? If these rows are not unique, list the first two possible such omissions (of sets of rows), starting from the top of the given listing. (d) Check your answer using CryptoMiniSat.