On the Structure of Dual-line Standard Contradictions and their General Forms in First-order Logic

Contradiction separation (CS) and its first-order version S-CS are multiclause inference schemes for clausal refutation. They isolate a standard contradiction core within a clause set and derive a propagated clause from the remaining literals. This paper develops structural characterizations of non-unit standard contradictions that make such cores explicit and easier to identify. In propositional logic, we introduce a canonical dual-line family and prove that every instance is a standard contradiction. We study admissible literal extensions, define ladder structures as maximal dual-line extensions, and present a regular triple-line family with constructive generation schemes. We also analyze how dual-line cores compose via clause connections and give sufficient conditions under which the composed clause set remains a standard contradiction. In first-order logic, we exhibit clause families that are not standard contradictions syntactically but become standard contradictions after suitable instantiation and controlled clause reuse.