An Exponential Example
In "Cut Normal Forms and Proof Complexity"
Matthias Baaz and Alexander Leitsch proved that the formula scheme
where
denotes
the transitivity of
, i.e.
, is
valid. Note that all cut-free proofs of
are of
length 
.
Note that, due to their sizes, some of the following files are compressed (gziped). We recommend you leave them compressed since uncompressing would yield files of tremendous sizes (more then 1 GB in some cases). Besides the system CERES and all our tools are also capable of working with gziped files directly.
-
instance of this scheme where n = 1:
$ hlk --ceres -o n1.xml n1.hlk p$ ceres --cutelim -ac n1.xml p n1-ce.xmlSupplemental files: n1-otter.in (Otter input file) | n1-otter.out (Otter output file)
-
instance of this scheme where n = 2:
$ hlk --ceres -o n2.xml n2.hlk p$ ceres --cutelim -ac n2.xml p n2-ce.xmlSupplemental files: n2-otter.in (Otter input file) | n2-otter.out (Otter output file)
-
instance of this scheme where n = 3:
$ hlk --ceres -o n3.xml n3.hlk p$ ceres --cutelim -ac n3.xml p n3-ce.xmlSupplemental files: n3-otter.in (Otter input file) | n3-otter.out (Otter output file)
-
instance of this scheme where n = 4:
$ hlk --ceres -o n4.xml n4.hlk p$ ceres --cutelim -ac n4.xml p n4-ce.xmlSupplemental files: n4-otter.in (Otter input file) | n4-otter.out (Otter output file)
-
instance of this scheme where n = 5:
$ hlk --ceres -o n5.xml n5.hlk p$ ceres --cutelim -ac n5.xml p n5-ce.xmlSupplemental files: n5-otter.in (Otter input file) | n5-otter.out (Otter output file)
-
instance of this scheme where n = 6:
$ hlk --ceres -o n6.xml n6.hlk p$ ceres --cutelim -ac n6.xml p n6-ce.xmlSupplemental files: n6-otter.in (Otter input file) | n6-otter.out (Otter output file)
-
instance of this scheme where n = 7:
$ hlk --ceres -o n7.xml n7.hlk p$ ceres --cutelim -ac n7.xml p n7-ce.xmlSupplemental files: n7-otter.in (Otter input file) | n7-otter.out (Otter output file)