Let's try to solve "co3SAT" with an NTM in polynomial time. It seems we need, more or less, to guess a proof that the formula is unsatisfiable i.e. derive a contradiction.
We've got a formula in conjunctive normal form, a big AND of OR clauses, each clause with 3 literals. Let's suppose we adopt the following strategy: at each stage, we expand two of of the clauses using the distributive law (AND distributes over OR), and simplify the result whenever possible. In the end, if the formula is unsatisfiable, we should get "false" from this procedure.
Is a lower bound known for this procedure (i.e. is it known whether this necessarily uses exponential time, given that we can use the non-determinism to select the optimal order in which the clauses are expanded)?
I read a little a bit about lower bounds for resolution techniques using the pigeonhole principle, but at first glance this seems like a different problem.