Система доказательств Res(+), предложенная Ицыксоном и Соколовым, -- расширение резолюционной системы доказательств. Она оперирует с дизъюнкциями линейных равенств над $F_2$. В докладе мы рассмотрим технику доказательства нижних оценок на размер доказательств некоторых противоречивых семейств формул для древовидной Res(+), основанную на играх Прувера и Дилеера. Данная техника является обобщением доказательства нижней оценки для принципа Дирихле. Затем мы применим данную технику для доказательства нижних оценок на Ordering principle и Dense Linear Ordering principle.

Ordering principle утверждает, что не существует конечного линейного порядка без минимума. Мы дадим нижнюю оценку $2^{n−O(1)}$ на размер любого древовидного Res(+) доказательства этого утверждения, записанного в КНФ. Dense Linear Ordering principle утверждает, что не существует конечных плотных линейных порядков. Мы дадим $2^{n/3−O(1)}$ нижнюю оценку на размер любого древовидного Res(+) доказательства этого утверждения, записанного в КНФ.

Ordering principle и Dense Linear Ordering principle имеют доказательство полиномиального размера в резолюциях. Таким образом, мы приведем естественные примеры, разделяющие древовидную версию системы Res(+) и резолюцию.