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

Question

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$-$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) < 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?