# Logic: upper limit for a minimum resolution of an unsatisfactory formula.

Leave $$varphi$$ be a logical formula of the first order with $$n$$ literals$$X_1, …, X_n$$).

$$varphi$$ It is unsatisfiable.

Now I want to know the upper limit of a minimum resolution of $$varphi$$ resulting in the empty clause ($$square$$).

My first idea was that it should be possible in linear time ($$n$$) because the longest clause can have up to $$2n$$ The literals and we can solve them one by one. Some research taught me that there are unsatisfiable formulas that require exponentially many results for the empty clause. I read $$4 ^ n$$ somewhere, but I do not understand why this should be the upper limit.

I hope someone can help me solve this!