Can someone provide with the smallest (as small as possible) 3SAT example (w.r.t. number of variables and the number of equations) that is:Unsatisfiable. Not provable unsatisfiable by simply reduction (successive simplification and rewriting) of the equations by the process similar to as described below:Example:Assuming a 3SAT Problem that includes 4 equations:~a + b + c  = 1~a + ~b + c = 1b + d + ~e  = 1b + d + e   = 1(1. and 2.) combined can be replaced with ~a+c=1.(3. and 4.) combined can be replaced with b+d=1.and so on.. Thus, we require a problem instance where such a successive reduction/simplification of the equations (containing either 2 or 3 variables) in the given problem do not automatically lead to the conclusion of unsatisfiability.
Non-reducible Unsatisfiable 3SAT instance example
complexity theory
Resolution is a complete proof system for contradictions: if a given set of clauses is contradictory, then this fact is provable using resolution.Since Resolution exactly corresponds to your simple reduction, it follows that your question cannot be answered.