Could a modification of Krom's proof system be used to solve 3-SAT in polynomial time?

A literal is a nonzero integer, and we define $\sim x = -x$.

A clause is a nonempty set of literals.

A CNF is a set of clauses.

A K-rule is a pair $(F,C)$ where $F$ is a CNF and $C$ is a clause.

A Krom-style proof system (KPS) is a set of K-rules.

If $S$ is a KPS, then an $S$-proof of $C$ from $F$, or an $(S,F)$-proof of $C$, is a sequence $\langle C_1,..,C_n\rangle$ of clauses such that $C = C_n$ and for all $1\le i\le n$, either $C_i \in F$ or there is a K-rule $R = (G,A) \in S$ and a function $f : \{x,\sim x : x \in B \in G \lor x \in A\} \rightarrow \mathbb{Z}_{\ne 0}$ which respects negation such that letting $g(B) := \{f(a) : a ∈ B\}$, we have $C_i = g(A)$, and for all $B \in G$, there exists some $j < i$ with $C_j = g(B)$.

For fixed $S$, the language $\{(F,C) : F \vdash_S C\}$ is polynomial-time decidable:

read inputs F and C
if C ∈ F
    return true
let D = {x1,~x1,..,xn,~xn} be the set of literals occuring in F or C, and their negations
Contin := true
while Contin
    Contin ← false
    for (G,A) in S
        for h : {abs(x) : x ∈ B ∈ G ∨ x ∈ A} -> D # there are |D|^c such functions
            f(x) := (x > 0 ? h(x) : -h(-x))
            g(B) := {f(a) : a ∈ B}
            for B in G
                if g(B) ∉ G 
                    continue in the for-loop where h is chosen
            if g(A) ∉ F
                push g(A) to F
                Contin ← true
if C ∈ F
    return true
else
    return false

$S$ is sound if for all CNF's $F$ and clauses $C$, the existence of an $(S,F)$-proof of $C$ implies that $F \vDash C$.

$S$ is complete for a class $\Gamma$ of CNF's if for all $F \in \Gamma$ and $C$, if $F \vDash C$ then $C$ is $(S,F)$-provable.

No KPS is complete for full $SAT$, since any clause of the form $\{-1,1,2,3,..,n\}$ is tautological, but for any system $S$, $sup\{|A| : (\emptyset,A) \in S\}$ is only finite, making the clause $(S,\emptyset)$-unprovable for sufficiently large $n$.

$\{(\{\{1\},\{-1\}\},\{2\})\}$ is complete for $1$

Any proof in KPS (with whatever rules) can be rephrased as a sequence of lines, each of which is either a clause or follows from preceding lines according to one of finitely many inference rules. Additionally, the lines come from one of finitely many "patterns" (formulas with placeholders to variables), and so all proofs are polynomially bounded.

Suppose that the maximum depth of a pattern is $d$. Then your proof is also a proof in depth $d$ Frege. It is known that the pigeonhole principle needs $2^{\Omega(n^{1/5^d})}$ lines to refute in depth $d$ Frege. This implies that KPS systems cannot be complete for 3SAT, since all proofs in KPS are polynomially bounded.

StackExchange Computer Science Q#84438, answer score: 3