No feasible monotone interpolation for simple combinatorial reasoning (Q1575265)

The feasible monotone interpolation method has been one of the main tools to prove the exponential lower bounds for relatively weak propositional systems. \textit{N. H. Arai} [Theor. Comput. Sci. 170, No. 1-2, 129-144 (1996; Zbl 0874.03065)] introduced a simple combinatorial reasoning system, GCNF+permutation, as a candidate for an automatizable, though powerful, propositional calculus. We show that the monotone interpolation method is not applicable to prove the superpolynomial lower bounds for Simple Combinatorial Reasoning. At the same time, we show that cutting planes, Hilbert's nullstellensatz and the polynomial calculus do not \(p\)-simulate simple combinatorial reasoning.