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 &lt; 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} -&gt; D # there are |D|^c such functions
            f(x) := (x &gt; 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$-$SAT$, and represents the rule $a,\sim a \vdash b$.
$\{(\emptyset,\{1,-1\}),(\{\{1\}\},\{1,2\}),(\{\{1,2\},\{-1,3\}\},\{2,3\})\}$ is complete for $2$-$SAT$, and represents the system consisting of the rules (1) $\vdash a\lor\sim a$, (2) $a\lor a \vdash a\lor b$, and (3) $a\lor b, \sim a\lor c \vdash b\lor c$.
Question 1. Is it known that no sound KPS can be complete for $3$-$SAT$?
If such a KPS was found, it would imply $P=NP$ and the polynomial-boundedness of natural propositional proof systems.
I am particularly interested in the completeness of the system $S_3 = \{(\emptyset,\{1,-1,2\}),(\{\{1,2,3\},\{1,2,4\},\{-3,-4,5\}\},\{1,2,5\})\}$ for $3$-$SAT$, where the main rule corresponds to the fact that if $a \land b \Rightarrow c$, $a \land b \Rightarrow d$, and $c\land d\Rightarrow e$, then $a\land b\Rightarrow e$.
Question 2. Can $S_3$ be shown to be complete for $3$-$SAT$, or at least some restricted class thereof such as $Horn$-$SAT\cap 3$-$CNF$ or the pigeonhole principle?
An $(S,F,d)$-proof is the same as an $(S,F)$-proof $\langle C_1,..,C_n\rangle$, except that we have a function $h : \{1,..,n\} \rightarrow \{0,..,d\}$, and the last part of the old definition, namely "$C_j = g(B)$", is strengthened by additionally requiring that $h(j) &lt; h(i)$.
So far, I have been able to show that if $\langle C_1,..,C_n,C_{n+1}\rangle$ is an $(S_3,F\cup \{\{a,b,c\}\})$-proof of $C_{n+1} = \{d,e,f\}$ with $C_1,..,C_n \in F$, then for $x=a,b,c$ there exists an $(S_3,F\cup\{ \{\sim d\}, \{\sim e\}, \{\sim f\}\},5)$-proof $\langle D_1,..,D_{23}\rangle$ of $\{\sim x\}$.
However, the algorithm given above takes $O(n^8)$ steps on the RAM model of computation in the case of $S_3$. Krom's original algorithm for 2-SAT had a running time of $O(n^3)$, but this upper bound has since been improved to $O(n)$, even if we want to find a satisfying assignment when one exists.
Question 3. How quickly can we solve the $S_3$-provability problem? If this system happens to be complete for $3$-$SAT$, how quickly can we find satisfying assignments to consistent formulae?
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.