Efficient algorithms for bounded-width RES. In lecture, we saw an Efficient algorithm for searching for space-bounded treelike resolution refutations. This is not the only family of proofs for which proof search is Efficient . A width-"w" resolution proof is one in which every line of the proof is a clause of at most "w" literals. In this exercise, you will show that for a fixed "w", there is an Efficient algorithm for searching for width-w refutations. Crucially, we do not assume that these proofs are treelike. Problem: (a) More precisely, show that there is an algorithm that, on input a CNF "(greek letter varphi)", runs in time n^(O(w)), and decides whether or not there is a width-w refutation of "(greek letter varphi)".