TU Vienna logic.at Theory and Logic Group (E185-2)

## An Exponential Example

In "Cut Normal Forms and Proof Complexity" Matthias Baaz and Alexander Leitsch investigated a schema of proofs of the sequents where denotes the transitivity of , i.e. . 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.xml```

Supplemental 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.xml```

Supplemental 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.xml```

Supplemental 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.xml```

Supplemental 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.xml```

Supplemental 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.xml```

Supplemental 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.xml```

Supplemental files: n7-otter.in (Otter input file) | n7-otter.out (Otter output file)