Let $ varphi $ to be a logical formula of first order with $ n $ literals ($ X_1, …, X_n $).
$ varphi $ 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 $ literals and we can solve them one by one. Some research has learned that there are unsatisfactory formulas that require a considerable multiplication of results for the empty clause. I have read $ 4 ^ n $ somewhere but I do not understand why this should be the upper limit.
I hope someone can help me understand that!