A benchmark method for the propositional modal logics K, KT, S4

Alain Heuerding^{∗}, Stefan Schwendimann^{∗} Institut für Informatik und angewandte Mathematik, Universität Bern, Switzerland

October 17, 1996

Abstract

A lot of methods have been proposed (and sometimes implemented) for proof search in the propositional modal logics K, KT, and S4.

It is difficult to compare the usefulness of these methods in practice, since mostly only the execution times for a few simple formulas have been published. We try to improve this unsatisfactory situation by presenting a set of benchmark formulas. Note that we do not just list formulas, but give a method that allows to compare different provers today and in the future.

As a starting point we give the results we obtained when we applied this benchmark method to the Logics Workbench (LWB). Moreover we hope that the discussion of postulates concerning benchmark tests for automated theorem provers help to obtain improved benchmark methods for other logics, too.

1 Introduction

A lot of methods have been proposed (and sometimes implemented) for proof search in the propositional modal logics K, KT, and S4. An incomplete list: tableaux and sequent calculi, embeddings in other logics, connection method, inverse method, logical frameworks. It is difficult to compare the usefulness of these methods in practice. In most publications no or only a few execution times are listed. There are some exceptions like [1] (31 formulas for K, KT, S4) and [2] (38 formulas for S4). However, these formulas are already today too simple to serve as benchmarks. For example it takes about 0.002 seconds to solve the hardest problem of [1] for K, KT, S4 with the Logics Workbench (LWB). The formulas of [2] are harder, but also there it takes only about 0.035 seconds to solve the hardest formula with the LWB. This situation is very unsatisfactory. Therefore we decided to collect a set of benchmark problems for the propositional modal logics K, KT, and S4. In classical predicate logic, the often-cited collection of Pelletier [9] has been replaced by the TPTP library [11]. Although this library is considerably large, it is still common to choose a dozen of these formulas out of this library and publish the execution times for these formulas. Therefore we do not just give a list of formulas, but present a method that makes it possible to compare different provers. (The producers of TPTP plan a so-called benchmark suite for the next version that should allow the computation of a performance index for automated theorem provers for classical predicate logic; cp. [11].)

∗Work supported by the Swiss National Science Foundation, 21-43197.95.

The selection of the hard benchmark formulas was guided by the following postulates (see the following section for a thorough discussion).

1. Provable as well as unprovable formulas.

2. Formulas of various structures.

3. Some of the benchmark formulas are hard enough for forth-coming provers.

4. For each formula the result is already known today.

5. Simple ‘tricks’ do not help to solve the problems.

6. Applying the benchmark test to a prover takes not too much time.

7. The results can be summarized.

These postulates lead us to the exclusive use of scalable formulas. We test for which parameters n a certain prover can decide whether the scalable formula A(n) is provable or not in less than 100 seconds. The drawback of scalable formulas is their regular structure. If ‘by chance’ a prover ‘recognizes’ this structure, it can perform extremly well for a certain class of formulas, but still work very bad for slightly different formulas. We try to overcome this problem by hiding their structure with superfluous subformulas, and by presenting a sufficient number of different classes. Collecting and constructing scalable formulas – always keeping the seven postulates in mind – is a very time-consuming task. Therefore the number of classes we propose is not as large as we would like it to be. The number of formulas is no longer a problem in the approach chosen in [3]. There formulas in some sort of nested conjunctive normal form were constructed using a random generator. It seems possible to choose length, number of clauses, and modal depth such that the resulting formulas are on the edge between ‘satisfiable’ and ‘not satisfiable’. On the other hand this method has two drawbacks: the formulas all have a similar structure (cp. postulate 2), and – more serious – the correct result is not known beforehand (cp. postulate 4). In our opinion a method relying on such formulas cannot replace our method, but could serve as a complementary method. At the end of this report we apply the benchmark method on the decision procedures integrated in the LWB. Of course it is possible to implement much faster decision procedures for K, KT, and S4, but hopefully these results serve as a starting point. This paper contains all the information that is required in order to use the benchmark method. For convenience we offer the possibility to fetch some formulas and the programs that produce these formulas via WWW.

2 Postulates

In this section we discuss the seven postulates mentioned in the introduction in more detail. Note that they are widely applicable, not just for the logics for which we present benchmark formulas in this report.

Provable as well as unprovable formulas.

Often only provable formulas are considered as benchmark fomulas. We think that not provable formulas are as interesting as provable ones. Moreover, algorithms like the Greedy procedure in classical propositional logic ([8], [10]) can recognize many unprovable formulas in a very short time, but they cannot show that a formula is provable. A benchmark method must also be applicable for such semi-decision procedures.

Formulas of various structures

It is clear that four or five formulas are not enough to obtain representative results about the performance of a prover. However, also a large number of formulas does not guarantee the quality of the benchmark set. For example it is tempting to use the embedding of IPC in S4 in order to obtain a list of benchmark formulas for S4 from a list of benchmark formulas for IPC, but all the resulting formulas look similar. An even more dubious method it the use of just one class of formulas, e.g. the pigeonhole formulas. Things look of course different if one has a certain application in mind and develops a tuned prover for this application, but here we want to measure the overall performance.

Some of the benchmark formulas are hard enough for forth-coming provers.

It is not enough if the benchmark test is hard enough for today’s provers. The test should still be applicable for much faster computers and improved search methods in the future. Thus the test must contain formulas that are far too hard for existing provers.

For each formula the result is already known today.

The correct result, i.e. ‘provable’ or ‘unprovable’, must be known already today. Therefore it must be possible to check the provability resp. non-provability of the formulas with logical methods, and not just with theorem provers. Random formulas do not fulfill this postulate.

Simple ‘tricks’ do not help.

The addition of a simple trick to the prover should not influence the results. Assume for example that a benchmark set for K contains formulas without □ and without ◇. Such formulas are provable in K iff they are provable in classical propositional logic. If a prover checks at the beginning whether modal operators occur in the formula, then he can apply a fast decision procedure for classical propositional logic in order to solve the problem. Therefore our benchmark test contains no such formulas. For example the pigeonhole formula is disguised with some ‘superfluous’ □ and ◇. If a prover recognizes this disguise, or if he sees during the proof search that a subproblem is purely classical, then we think that this is no longer a simple trick. Of course it is impossible to foresee all such tricks, but at least one should try.

Execution of the benchmark test takes not too much time.

Nobody wants to spend a lot of time to measure the performance of his prover. In particular, the required time should not depend on the prover or on the computer. Therefore some limits must be used, e.g. ‘if the prover cannot solve the problem in n seconds, then stop’.

Results can be summarized.

A list of hundreds of numbers is not a satisfactory result, since it makes a comparison of several provers almost impossible. Therefore it must be possible to summarize the results. On the other hand the result should still show some properties of the prover. We think that in most cases it is sensible to give a list of numbers and not just one number in order to describe the performance of the prover. (Remember the semi-decision procedures already mentioned above.)

3 Benchmark method for K, KT, and S4

3.1 Formulas

For each logic L, the formulas are divided into 9 classes of provable and 9 classes of unprovable formulas. The formulas in each class are parametrized by a number in ℕ. We call the jth formula in the ith class of provable resp. unprovable formulas F_{p,i,j} resp. F_{n,i,j}. Thus L ⊢ F_{p,i,j} and L ⊬ F_{n,i,j} for all i ∈ {1, …, 9}, j ∈ ℕ. Let t(C) be the time in seconds the prover takes to decide whether or not the formula C is provable, i.e. t : Fml → ℕ ∪ ∞. We compute for each i ∈ {1, …, 9} the numbers n_{p,i} := max{j | t(F_{p,i,j}) < 100 seconds} and n_{n,i} := max{j | t(F_{n,i,j}) < 100 seconds}. Thus F_{p,i,n_{p,i}+1} is the first formula in the ith class of provable formulas such that the prover cannot decide its provability in less than 100 seconds (F_{n,i,n_{n,i}+1} analogous).

3.2 Timing

It is not possible to describe a timing procedure that is sensible for all provers (think e.g. of non-deterministic and parallel provers). Therefore it is important that everybody who applies the benchmark method describes exactly how the timing took place. See section 9 for an example. If possible, then observe the following conditions in order to make the comparison of different provers easier.

• The timing starts after the start-up of the prover

• No conversions, e.g. in negation normal form, before the timing starts.

• The timing includes the construction of the data structure that contains the formula. This is especially important if you put additional information into the data structure before starting the ‘real’ proof search.

• Make your prover accessible in some way, in order to give people the possibility to check your results.

3.3 Presentation of the results

We propose the following form to present your results. With this information it should be possible to check the obtained results. See section 9 for an example of a filled in form.

1. Name of the prover. Short description of the methods used by the prover (or a reference).

2. Availability of the prover.

3. Short list of features your prover offers besides checking the provability of formulas (or a reference). Examples: Is the prover tuned for a certain application ? Has the correctness of the prover been verified ? Can one use one prover for many logics ? Is a proof resp. a counter-model generated ?

4. Hardware that was used for the benchmark test.

5. An example of the way you timed your prover.

6. Results, i.e. the numbers n_{p,i} and n_{n,i} for all i ∈ {1, …, 9}.

7. Discussion of the results (optional).

3.4 What about the postulates ?

Our method largely satisfies the seven postulates:

1. There are provable as well as not provable formulas.

2. The formulas have various properties (number of variables, modal depth, …) and origins.

3. Each class contains arbitrarily hard formulas.

4. It is clear which formulas are provable.

5. We tried …

6. Applying our benchmark method is rather tiresome if one does not automate it, but the required time seems reasonable to us.

7. For each logic the result consists of a list of 18 numbers.

The main problems are the postulate 5, and the — at least for semi-decision procedures — relatively small number of classes.

4 Notation

Logics: CPC stands for classical propositional logic. K, KT, S4 are the modal propositional logics we consider. In order to avoid misunderstanding we list the corresponding properties of the accessibility relation in Kripke semantics: K: neither reflexive nor transitive, KT: reflexive, but not transitive, S4: reflexive and transitive. Variables and formulas: Var = {p_{0}, p_{1}, p_{2}, …} is the set of the variables. We inductively define the set of the formulas Fml: ⊤, ⊥ ∈ Fml; P ∈ Var ⇒ P ∈ Fml; A ∈ Fml ⇒ □A, ◇A, ¬A ∈ Fml; A, B ∈ Fml ⇒ A ∧ B, A ∨ B, A → B, A ↔ B ∈ Fml. Conventions: We use meta-variables (sometimes with subscripts) as follows: A, C for formulas, k, n for elements of {1, 2, …}. ∨ and ∧ are left-associative. ¬, □, ◇ have the highest priority, followed by ∧, ∨, →, and ↔. We omit the outermost brackets. Example: p_{0} ∨ p_{1} ∨ p_{2} → (¬p_{2} ∧ p_{1}) ↔ p_{0} stands for the formula ((((p_{0} ∨ p_{1}) ∨ p_{2}) → ((¬p_{2}) ∧ p_{1})) ↔ p_{0}). Iterations: □^{0}A stands for the formula A, □^{n}A stands for the formula □□^{n−1}A. ◇^{0}A stands for the formula A, ◇^{n}A stands for the formula ◇◇^{n−1}A. ⋀_{i=n_{1},...,n_{2}}(A_{i}) stands for the formula A_{n_{1}} ∧ A_{n_{1}+1} ∧ … ∧ A_{n_{2}} (if n_{1} ≤ n_{2}) resp. for the formula true (if n_{1} > n_{2}). ⋁_{i=n_{1},...,n_{2}}(A_{i}) stands for the formula A_{n_{1}} ∨ A_{n_{1}+1} ∨ … ∨ A_{n_{2}} (if n_{1} ≤ n_{2}) resp. for the formula false (if n_{1} > n_{2}). Equality: A ≡ C means that the two formulas A and C are (syntactically) equal. Substitution: If P_{1}, …, P_{n} are variables, then A{C_{1}/P_{1}, …, C_{n}/P_{n}} is the formula A with simultaneously substituted P_{1} by C_{1}, …, P_{n} by C_{n}. Example: (p_{0} ∨ □(p_{1} → p_{0})){p_{2}/p_{0}, ◇p_{1} ↔ p_{0}/p_{1}} ≡ p_{2} ∨ □((◇p_{1} ↔ p_{0}) → p_{2}). Lists: [x_{1}, x_{2}, …, x_{n}] is the list with the elements x_{1}, x_{2}, …, x_{n}. Note that [1, 2], [2, 1], [1, 1, 2] are three different lists. ⋁_{y∈[x_{1},...,x_{n}]}(A_{x}) stands for A_{x_{1}} ∨ … ∨ A_{x_{n}}.

Standard formulas: D :≡ □p_{0} → ◇p_{0} D_{2} :≡ ◇true B :≡ p_{0} → □◇p_{0} T :≡ □p_{0} → p_{0} A4 :≡ □p_{0} → □□p_{0} A5 :≡ ¬□p_{0} → □¬□p_{0} H :≡ □(p_{0} ∨ p_{1}) ∧ □(□p_{0} ∨ p_{1}) ∧ □(p_{0} ∨ □p_{1}) → □p_{0} ∨ □p_{1} L :≡ □(p_{0} ∧ □p_{0} → p_{1}) ∨ □(p_{1} ∧ □p_{1} → p_{0}) L^{+} :≡ □(□p_{0} → p_{1}) ∨ □(□p_{1} → p_{0}) Grz :≡ □(□(p_{0} → □p_{0}) → p_{0}) → p_{0} Grz_{1} :≡ □(□(p_{0} → □p_{0}) → p_{0}) → □p_{0} Dum :≡ □(□(p_{0} → □p_{0}) → p_{0}) → (◇□p_{0} → p_{0}) Dum_{1} :≡ □(□(p_{0} → □p_{0}) → p_{0}) → (◇□p_{0} → □p_{0}) Dum_{4} :≡ □(□(p_{0} → □p_{0}) → p_{0}) → (◇□p_{0} → p_{0} ∨ □p_{0})

Negation normal form: We inductively define the function nnf for formulas without ↔. • nnf(true) :≡ true, nnf(false) :≡ false, nnf(¬true) :≡ false, nnf(¬false) :≡ true

• nnf(P) :≡ P, nnf(¬P) :≡ ¬P

• nnf(□A) :≡ □nnf(A), nnf(◇A) :≡ ◇nnf(A)

• nnf(A ∧ B) :≡ nnf(A) ∧ nnf(B), nnf(A ∨ B) :≡ nnf(A) ∨ nnf(B)

• nnf(A → B) :≡ nnf(¬A ∨ B)

• nnf(¬□A) :≡ nnf(◇¬A), nnf(¬◇A) :≡ nnf(□¬A)

• nnf(¬(A ∧ B)) :≡ nnf(¬A ∨ ¬B), nnf(¬(A ∨ B)) :≡ nnf(¬A ∧ ¬B)

• nnf(¬(A → B)) :≡ nnf(A ∧ ¬B)

• nnf(¬¬A) :≡ nnf(A) Length and modal depth: We inductively define the functions length and modaldepth.

• length(true) := 1, length(false) := 1, length(P) := 1

• ∘ ∈ {□, ◇, ¬} ⇒ length(∘A) := length(A) + 1

• ∘ ∈ {∧, ∨, →, ↔} ⇒ length(A ∘ B) := length(A) + length(B) + 1

• modaldepth(true) := 0, modaldepth(false) := 0, modaldepth(P) := 0

• ∘ ∈ {□, ◇} ⇒ modaldepth(∘A) := modaldepth(A) + 1

• modaldepth(¬A) := modaldepth(A)

• ∘ ∈ {∧, ∨, →, ↔} ⇒ modaldepth(A ∘ B) := max(modaldepth(A), modaldepth(B))

Integer division: The functions div and mod are defined as usual. Example: 14 div 3 = 4, 14 mod 3 = 2.

5 Presentation of formulas

For each class of formulas we list in the following section:

1. Idea: Why is the formula provable resp. unprovable ?

2. Hiding: How is the formula ‘hidden’ in order to make the problem harder to solve ?

3. Characteristics: Modal depth, number of variables, …

4. An inductive definition of the formulas. Appendix I contains the first two formulas of each class, and the length, depth, modal depth, variables of the first six formulas of each class. If you generate the formulas by yourself, then please compute these values and compare them with the ones in appendix I. In this way you can make (relatively) sure that you consider the correct formulas. (See section 4 for the definitions of length and modal depth of a formula.)

Appendix II contains the listings of the procedures (written in the LWB programming language) we used to generate the formulas for the benchmark test in section 9. The formulas you can fetch were obtained with the help of these programs. In order to avoid inconsistencies between the formulas in the sections 6, 7, 8 and the programs in appendix II, we implemented a Perl program that automatically converts the LaTeX definitions into LWB programs. We then compared the results of these generated LWB programs with the results of the LWB programs in appendix II.

6 Formulas for K

6.1 k branch p

Idea: The branching formula as defined in [4], plus a negation symbol in front and the additional subformula ¬□^{n}p_{n div 3+1} in order to make the formula provable. We assume n < 100. Charateristics: 2n + 3 variables, modal depth O(n).

k branch p(n) :≡ ¬(p_{100} ∧ ¬p_{101} ∧ ⋀_{i=0,...,n}(□^{i}(bdepth(n) ∧ det(n) ∧ branching(n)))) ∨ ¬□^{n}p_{n div 3+1} bdepth(n) :≡ ⋀_{i=1,...,n+1}(p_{100+i} → p_{99+i}) det(n) :≡ ⋀_{i=0,...,n}(p_{100+i} → (p_{i} → □(p_{100+i} → p_{i})) ∧ (¬p_{i} → □(p_{100+i} → ¬p_{i}))) branching(n) :≡

⋀_{i=0,...,n−1}(p_{100+i} ∧ ¬p_{101+i} → ◇(p_{101+i} ∧ ¬p_{102+i} ∧ p_{i+1}) ∧ ◇(p_{101+i} ∧ ¬p_{102+i} ∧ ¬p_{i+1}))

6.2 k branch n

Idea: The branching formula as defined in [4]. Characteristics: Every Kripke model that satisfies the pure branching formula must have an exponential number of worlds (cp. [4]). 2n + 3 variables, modal depth n + 1. We assume n < 100.

k branch n(n) :≡ ¬(p_{100} ∧ ¬p_{101} ∧ ⋀_{i=0,...,n}(□^{i}(bdepth(n) ∧ det(n) ∧ branching(n))))

bdepth, det, branching as in 6.1.

6.3 k d4 p

Idea: K ⊢ D ∧ A4 ∧ B{¬p_{0}/p_{0}} → T. Hiding: The left hand side occurs with 1 to n □, the right hand side occurs just with n □ in front. □^{n}T is repeated n times. Additionally some superfluous instances, and the whole formula in negation normal form. Characteristics: One variable, modal depth n + 3, in negation normal form.

k d4 p(n) :≡ nnf(⋁_{i=1,...,n}(□^{n}T ∨ ¬□^{i}D_{2} ∨ ¬□^{i}A4 ∨ ¬□^{i}A4{◇p_{0}/p_{0}} ∨ ¬□^{i}B ∨ ¬□^{i}B{¬p_{0}/p_{0}}))

6.4 k d4 n

Idea: A5 is not provable in K plus any instances of D, A4, and T. Hiding: As in 6.3. Characteristics: One variable, modal depth n + 3, in negation normal form.

k d4 n(n) :≡ nnf(⋁_{i=1,...,n}(□^{n}(□p_{0} ∨ □◇¬p_{0}) ∨ ¬□^{i}D_{2} ∨ ¬□^{i}A4 ∨ ¬□^{i}A4{◇p_{0}/p_{0}} ∨ ¬□^{i}D ∨ ¬□^{i}A4{◇p_{0} → p_{0}/p_{0}} ∨ ¬□^{i}A4{□p_{0} → p_{0}/p_{0}}))

6.5 k dum p

Idea: K ⊢ A4{□(p_{0} → □p_{0}) → p_{0}/p_{0}} ∧ □A4 ∧ Dum ∧ Dum{p_{0} → □p_{0}/p_{0}} → Dum_{1}. Hiding: Some of the formulas on the left hand side of the implication occur with 1 to n − 1 □ in front, the right hand side occurs just once with n div 2 + 1 □ in front. Characteristics: One variable, modal depth n + 2 (for n > 4).

k dum p(n) :≡ ⋀_{i=1,...,n div 2}(□^{i}(□A4 ∧ Dum)) ∧ ¬□^{n div 2+1}Dum_{1}

→ ◇^{n div 2+1}¬(A4{□(p_{0} → □p_{0}) → p_{0}/p_{0}} ∧ □A4 ∧ Dum ∧ Dum{p_{0} → □p_{0}/p_{0}})

∨ ⋁_{i=n div 2+2,...,n−1}(◇^{i}¬(□A4 ∧ Dum))

6.6 k dum n

Idea: Dum is not provable in K plus any instances of Dum_{4} and A4. Hiding: As in 6.5. Characteristics: One variable, modal depth n + 5.

k dum n(n) :≡ ⋀_{i=1,...,n div 2}(□^{i}(□A4 ∧ Dum_{4})) ∧ ¬□^{n+1}Dum

→ ◇^{n+1}¬(A4{□(p_{0} → □p_{0}) → p_{0}/p_{0}} ∧ □A4 ∧ Dum_{4} ∧ Dum_{4}{p_{0} → □p_{0}/p_{0}})

∨ ⋁_{i=n div 2+2,...,n−1}(◇^{i}¬(□A4 ∧ Dum_{4}))

6.7 k grz p

Idea: K ⊢ □Grz ∧ Grz{C () ∧ A4{C ()/p_{0}}/p_{0}} → Grz_{1}, where C () is defined as below. Hiding: Many superfluous instances with three variables, and iterated □ inside the instances. Characteristics: 3 (if n < 5) resp. 4 variables, modal depth 7 (if n < 14) resp. n + 14 div 4.

k grz p(n) :≡ □Grz{p_{2}/p_{0}} ∧ ⋀_{i=1,...,n−1}(l(i)) ∧ Grz{C () ∧ A4{C ()/p_{0}}/p_{0}} → Grz_{1}{p_{1}/p_{0}} ∨ Grz_{1}{p_{2}/p_{0}} ∨ Grz_{1}{p_{3}/p_{0}}

l(i) :≡ \{ \begin{matrix}Grz\{l2 (i div 4)/p_{0}\} & i mod 4 = 0 \\ Grz\{□l2 (i div 4) ∨ p_{1}/p_{0}\} & i mod 4 = 1 \\ Grz\{□l2 (i div 4) ∨ p_{1} ∨ p_{2}/p_{0}\} & i mod 4 = 2 \\ Grz\{□l2 (i div 4) ∨ p_{1} ∨ p_{2} ∨ p_{3}/p_{0}\} & otherwise \end{matrix}

l2 (i) :≡ \{ \begin{matrix}false & i = 0 \\ □l2 (i − 1) ∨ p_{1} ∨ p_{2} ∨ p_{3} ∨ p_{4} & otherwise \end{matrix}

C () :≡ □(p_{2} → □p_{2}) → p_{2}

6.8 k grz n

Idea: Grz is not provable in K plus instances of Grz_{1}. Hiding: As in 6.7. Characteristics: 3 (if n < 5) resp. 4 variables, modal depth 7 (if n < 14) resp. n + 14 div 4.

k grz n(n) :≡ □Grz_{1}{p_{2}/p_{0}} ∧ ⋀_{i=1,...,n−1}(l(i)) ∧ Grz_{1}{C () ∧ A4{C ()/p_{0}}/p_{0}} → Grz{p_{1}/p_{0}} ∨ Grz{p_{2}/p_{0}} ∨ Grz{p_{3}/p_{0}}

l(i) :≡ \{ \begin{matrix}Grz_{1}\{l2 (i div 4)/p_{0}\} & i mod 4 = 0 \\ Grz_{1}\{□l2 (i div 4) ∨ p_{1}/p_{0}\} & i mod 4 = 1 \\ Grz_{1}\{□l2 (i div 4) ∨ p_{1} ∨ p_{2}/p_{0}\} & i mod 4 = 2 \\ Grz_{1}\{□l2 (i div 4) ∨ p_{1} ∨ p_{2} ∨ p_{3}/p_{0}\} & otherwise \end{matrix}

l2 , C as in 6.7.

6.9 k lin p

Idea: K ⊢ H2 → L, where H2 is the instance of H defined below. Hiding: Superfluous instances of H2 with other variables. Characteristics: n + 1 variables, modal depth 3.

k lin p(n) :≡ ⋁_{i=1,...,n div 3}(¬H2 (p_{i}, p_{i+1}))

∨ L{p_{n}/p_{0}, p_{n}/p_{1}}

∨ ⋁_{i=n div 3+1,...,n}(¬H2 (p_{i}, p_{i+1}))

H2 (A, B) :≡ H{A ∧ □A ∧ A → B/p_{0}, ¬A → ¬(□B ∧ B)/p_{1}}

6.10 k lin n

Idea: L^{+} is not provable in K plus any instances of L. Characteristics: n + 1 variables, modal depth 2 (if n = 1) resp. 3.

k lin n(n) :≡ ⋁_{i=1,...,2n−2}(¬L{◇p_{i}/p_{0}, p_{i+1}/p_{1}} ∨ ¬L{p_{i} → □p_{i+1}/p_{0}, p_{i+1}/p_{1}}) ∨ L^{+}{p_{n}/p_{0}, p_{n}/p_{1}}

∨ ⋁_{i=2n,...,4n−4}(¬L{◇p_{i}/p_{0}, p_{i+1}/p_{1}} ∨ ¬L{p_{i} → □p_{i+1}/p_{0}, p_{i+1}/p_{1}})

6.11 k path p

Idea: Without hiding, the formula would just be □p_{path el(1,n)} ∨ ◇(¬p_{path el(1,n)} ∧ □p_{path el(2,n)}) ∨ … ∨ ◇(¬p_{path el(n−1,n)} ∧ □p_{path el}(n, n)) ∨ ◇^{n}p_{path el(n,n)}. Hiding: The formula above is the path from the entry to the exit of a labyrinth described by k path p. It makes no difference whether one starts at the entry or at the exit. Characteristics: In backward proof search, the path from the entry to the exit has to be found with backtracking, i.e. the function path el must be reconstructed. 6 variables, modal depth n.

k path p(n) :≡ (□p_{1} ∨ □p_{path el(1,n)} ∨ □p_{3} ∨ □p_{5})

∨ ⋁_{i=1,...,n;j=1,...,6}(left to right(i, j, n) ∨ right to left(i, j, n))

∨ (◇^{n}¬p_{2} ∨ ◇^{n}¬p_{4} ∨ ◇^{n}¬p_{path el(n,n)} ∨ ◇^{n}¬p_{6})

path el(l, n) :≡ \{ \begin{matrix}2 & l = 1 \\ modg (path el(l − 1, n) + 3, 6) & l > n div 2 \\ modg (path el(l − 1, n) + 5, 6) & otherwise \end{matrix}

left to right(l, k, n) :≡

false  l = n
false  l ≠ n, k mod 2 = 0, k ≠ path el(l, n)
lists2fml(l, k, [path el(l + 1, n)])  l ≠ n, k mod 2 = 0, k = path el(l, n)
lists2fml(l, k, [1, 3, path el(l + 1, n), 5])  l ≠ n, k mod 2 ≠ 0, k = path el(l, n)
lists2fml(l, k, delete(path el(l + 1, n), 1, 3, 5)) otherwise

right to left(l, k, n) :≡ \{ \begin{matrix}false & l = 1 \\ false & l ≠ 1, k mod 2 = 1 \\ lists2fml back(l − 1, k, delete(path el(l − 1, n), 2, 4, 6)) & otherwise \end{matrix}

lists2fml(l, k, s) :≡ ⋁_{x∈s}(◇^{l}(¬p_{k} ∧ □p_{x})) lists2fml back(l, k, s) :≡ ⋁_{x∈s}(◇^{l}(¬p_{x} ∧ □p_{k}))

delete(x, y1, y2, y3) :≡ \{ \begin{matrix}[y2 , y3 ] & x = y1 \\ [y1 , y3 ] & x = y2 \\ [y1 , y2 ] & x = y3 \\ [y1 , y2 , y3 ] & otherwise \end{matrix}

modg(n_{1}, n_{2}) :≡ \{ \begin{matrix}n_{2} & n_{1} mod n_{2} = 0 \\ n_{1} mod n_{2} & otherwise \end{matrix}

6.12 k path n

Idea: As in 6.11, but one piece of the path is missing (cp. the different definitions of left to right in 6.11 and 6.12). Hiding: As in 6.11. Characteristics: In backward proof search, the labyrinth is searched (using backtracking) for a path from the entry to the exit. 6 variables, modal depth n + 1.

k path n(n) :≡ (□p_{1} ∨ □p_{path el(1,n+1)} ∨ □p_{3} ∨ □p_{5}) ∨ ⋁_{i=1,...,n+1;j=1,...,6}(left to right(i, j, n + 1) ∨ right to left(i, j, n + 1)) ∨ (◇^{n+1}¬p_{2} ∨ ◇^{n+1}¬p_{4} ∨ ◇^{n+1}¬p_{path el(n+1,n+1)} ∨ ◇^{n+1}¬p_{6})

path el, right to left, lists2fml, lists2fml back, delete, modg as in 6.11. left to right(l, k, n) :≡

false  l = n
false  l ≠ n, k mod 2 = 0, k ≠ path el(l, n)
false  l ≠ n, k mod 2 = 0, k = path el(l, n), l = n div 2
lists2fml(l, k, [path el(l + 1, n)])  l ≠ n, k mod 2 = 0, k = path el(l, n), l ≠ n div 2
lists2fml(l, k, [1, 3, 5])  l ≠ n, k mod 2 ≠ 0, k = path el(l, n), l = n div 2
lists2fml(l, k, [1, 3, path el(l + 1, n), 5])  l ≠ n, k mod 2 ≠ 0, k = path el(l, n), l ≠ n div 2
lists2fml(l, k, delete(path el(l + 1, n), 1, 3, 5)) otherwise

6.13 k ph p

Idea: The pigeonhole formulas. We assume n < 100. Hiding: Some □ and ◇. Characteristics: Essentially a CPC problem. n^{2} + n variables, modal depth 1 (if n = 1) resp. 2.

k ph p(n) :≡ ◇left(n) → ◇right(n) left(n) :≡ ⋀_{i=1,...,n+1}(⋁_{j=1,...,n}(l(i, j))) right(n) :≡ ⋁_{j=1,...,n;i_{1}=1,...,n+1;i_{2}=i_{1}+1,...,n+1}(l(i_{1}, j) ∧ l(i_{2}, j))

l(i, j) :≡ \{ \begin{matrix}□p_{100i+j} & i < j \\ p_{100i+j} & otherwise \end{matrix}

6.14 k ph n

Idea: The pigeonhole formulas, with one missing conjunct on the right hand side. We assume n < 100. Hiding: Some □ and ◇. Characteristics: Essentially a CPC problem. n^{2} + n variables, modal depth 1 (if n = 1) resp. 2.

k ph n(n) :≡ ◇left(n) → ◇right(n) left, l as in 6.13. right(n) :≡ ⋁_{j=1,...,n;i_{1}=1,...,n+1;i_{2}=i_{1}+1,...,n+1}(l2 (n, i_{1}, j) ∧ l2 (n, i_{2}, j))

l2 (n, i, j) :≡ \{ \begin{matrix}¬l(i, j) & i = j, i = (2n) div 3 + 1 \\ l(i, j) & otherwise \end{matrix}

6.15 k poly p

Idea: The formula (p_{1} ↔ p_{2})∨(p_{2} ↔ p_{3})∨…∨(p_{n−1} ↔ p_{n})∨(p_{n} ↔ p_{1}) says: If we have a polygon with n vertices, and all the vertices are either black or white, then two adjacent vertices have the same colour. If n is odd, then this formula is provable in CPC.

Hiding: Many □, ◇, and superfluous subformulas. Characteristics: Essentially a CPC problem. About 4.5n variables, modal depth about 3n.

k poly p(n) :≡ \{ \begin{matrix}poly(3n + 1) & n mod 2 = 0 \\ poly(3n) & n mod 2 = 1 \end{matrix}

poly(n) :≡ □^{n+1} ⋀_{i=1,...,n+1}(p_{i}) ∨ f(n, n) ∨ □^{n+1} ⋀_{i=1,...,n+1}(¬p_{2i})

f (i, n) :≡ \{ \begin{matrix}false & i = 0 \\ ◇(f (i − 1, n) ∨ ◇^{i}(p_{n} ↔ p_{1})) ∨ □p_{i+2} & i = n \\ ◇(f (i − 1, n) ∨ ◇^{i}(p_{i} ↔ p_{i+1})) ∨ □p_{i+2} & otherwise \end{matrix}

6.16 k poly n

Idea: As in 6.15, but for an even number of vertices. Hiding: Many □, ◇, and superfluous subformulas. The superfluous subformulas do not influence the non-provability. Characteristics: Essentially a CPC problem. About 4.5n variables, modal depth about 3n.

k poly n(n) :≡ \{ \begin{matrix}poly(3n) & n mod 2 = 0 \\ poly(3n + 1) & n mod 2 = 1 \end{matrix}

poly, f as in 6.15.

6.17 k t4p p

Idea: K ⊢ T{◇p_{0}/p_{0}} ∧ □T{¬□◇p_{0}/p_{0}} ∧ A4{◇p_{0}/p_{0}} ∧ □(◇□◇p_{0} → (p_{0} → □p_{0})) → ◇□p_{0} ∨ ◇□¬p_{0} Hiding: Superfluous subformulas (◇¬p_{3}, ◇p_{4}), superfluous instances of A4 and A5, nested □. Characteristics: 4 variables, modal depth n + 5. Partially in negation normal form.

k t4p p(n) :≡ E(n) ∨ nnf(¬C (n)) ∨ ◇p_{4}

C (i) :≡ \{ \begin{matrix}((□◇p_{0} → ◇p_{1}) ∧ □(□¬□◇p_{1} → ¬□◇p_{0}) ∧ (□◇p_{0} → □□◇p_{1}) \\ ∧□(◇□◇p_{0} ∧ p_{0} → □p_{1}) ∧ □◇p_{1})\{p_{0} ∧ ◇¬p_{3}/p_{1}\} & i = 0 \\ □A4\{p_{1}/p_{0}\} ∧ □C (i − 1) ∧ □A4\{◇p_{1}/p_{0}\} & otherwise \end{matrix}

E(i) :≡ \{ \begin{matrix}◇□p_{0} & i = 0 \\ ◇¬A4\{¬p_{1}/p_{0}\} ∨ □E(i − 1) ∨ □A5\{p_{1}/p_{0}\} & otherwise \end{matrix}

6.18 k t4p n

Idea: ◇□p_{0} is not provable in K plus any instances of T, A4, and □(◇□◇p_{0} → (p_{0} → □p_{0})). Hiding: As in 6.17. Characteristics: 4 variables, modal depth 2n + 4. Partially in negation normal form.

k t4p n(n) :≡ E(2n − 1) ∨ nnf(¬C (2n − 1)) ∨ ◇p_{4}

C (i) :≡ \{ \begin{matrix}((□◇p_{0} → ◇p_{1}) ∧ □(□¬□◇p_{1} → ¬□◇p_{0}) ∧ (□◇p_{0} → □□◇p_{1}) \\ ∧□(◇□◇p_{0} ∧ p_{0} → □p_{1}))\{p_{0} ∧ ◇¬p_{3}/p_{1}\} & i = 0 \\ □A4\{p_{1}/p_{0}\} ∧ □C (i − 1) ∧ □A4\{◇p_{1}/p_{0}\} & otherwise \end{matrix}

E as in 6.17.

7 Formulas for KT

7.1 kt 45 p

Idea: KT ⊢ A5{□p_{0}/p_{0}} ∧ □A5{¬p_{0}/p_{0}} → A4. Hiding: The left hand side occurs with 1 to n □, the right hand side occurs just with n □ in front. Additionally some superfluous instances, and the whole formula in negation normal form. Characteristics: One variable, modal depth n + 3, in negation normal form.

kt 45 p(n) :≡ nnf(⋁_{i=1,...,n}(□^{n}A4 ∨ ¬□^{i}D_{2} ∨ ¬□^{i}A5{◇¬p_{0}/p_{0}} ∨ ¬□^{i}□A5 ∨ ¬□^{i}B))

7.2 kt 45 n

Idea: A5 is not provable in KT plus any instances of A4. Hiding: As in 7.1. Characteristics: One variable, modal depth n + 3, in negation normal form.

kt 45 n(n) :≡ nnf(⋁_{i=1,...,n}(□^{n}(□p_{0} ∨ □◇¬p_{0}) ∨ ¬□^{i}A4 ∨ ¬□^{i}A4{◇p_{0}/p_{0}} ∨ ¬□^{i}T ∨ ¬□^{i}A4{◇p_{0} → p_{0}/p_{0}} ∨ ¬□^{i}A4{□p_{0} → p_{0}/p_{0}}))

7.3 kt branch p

Idea: The branching formula as described in [4], plus a negation symbol in front and the additional subformula ¬□^{n}p_{(n div 3)+1} in order to make the formula provable. Charateristics: 2n + 3 variables, modal depth n + 1.

kt branch p(n) :≡ ¬(p_{100} ∧ ¬p_{101} ∧ □^{n}(bdepth(n) ∧ det(n) ∧ branching(n))) ∨ ¬□^{n}p_{(n div 3)+1} bdepth, det, branching as in 6.1.

7.4 kt branch n

Idea: The branching formula as defined in [4]. Characteristics: Every Kripke model that satisfies the pure branching formula must have an exponential number of worlds (cp. [4]). 2n + 3 variables, modal depth n + 1.

kt branch n(n) :≡ ¬(p_{100} ∧ ¬p_{101} ∧ □^{n}(bdepth(n) ∧ det(n) ∧ branching(n)))

bdepth, det, branching as in 6.1.

7.5 kt dum p

Idea: KT ⊢ A4{□(p_{0} → □p_{0}) → p_{0}} ∧ □A4 ∧ Dum ∧ Dum{p_{0} → □p_{0}/p_{0}} → Dum_{1}. Hiding: Some of he formulas on the left hand side of the implication occur with 1 to n − 1 □ in front, the right hand side occurs just once with (n div 2) + 1 □ in front. Characteristics: One variable, modal depth n + 1 (if n > 6).

kt dum p(n) :≡ ⋀_{i=1,...,n div 2}(□^{i}A4) ∧ ¬□^{(n div 2)+1}Dum_{1}

→ ◇^{(n div 2)+1}¬(A4{□(p_{0} → □p_{0}) → p_{0}/p_{0}} ∧ □A4 ∧ Dum ∧ Dum{p_{0} → □p_{0}/p_{0}})

∨ ⋁_{i=n div 2+2,...,n−1}(◇^{i}¬A4)

7.6 kt dum n

Idea: Grz is not provable in KT plus any instances of Dum. Hiding: As in 7.5. Characteristics: One variable, modal depth n + 2 (if n > 4).

kt dum n(n) :≡ ⋀_{i=1,...,n div 2}(□^{i}(□A4 ∧ Dum)) ∧ ¬□^{n div 2+1}Grz

→ ◇^{n div 2+1}¬(A4{□(p_{0} → □p_{0}) → p_{0}/p_{0}} ∧ □A4 ∧ Dum ∧ Dum{p_{0} → □p_{0}/p_{0}})

∨ ⋁_{i=n div 2+2,...,n−1}(◇^{i}¬(□A4 ∧ Dum))

7.7 kt grz p

Idea: KT ⊢ □Grz ∧ Grz{C () ∧ (A4{C ()/p_{0}})/p_{0}} → Grz_{1}, where C is defined as below. Hiding: Many superfluous instances with iterated □ inside the instances. The subformulas ◇□¬p_{0} and ◇p_{0} are the parts of an instance of T. Characteristics: 3 (if n < 5) resp. 4 variables, modal depth 7 (if n < 14) resp. n + 14 div 4.

kt grz p(n) :≡ □Grz{p_{2}/p_{0}} ∧ ⋀_{i=1,...,n−1}(l(i)) ∧ Grz{C () ∧ (A4{C ()/p_{0}})/p_{0}}

→ Grz_{1}{p_{1}/p_{0}} ∨ Grz_{1}{p_{2}/p_{0}} ∧ ◇□¬p_{0} ∨ Grz_{1}{p_{3}/p_{0}} ∨ Grz_{1}{p_{2}/p_{0}} ∧ ◇p_{0}

l, l2 , C as in 6.7.

7.8 kt grz n

Idea: A5 is not provable in KT plus instances of Grz_{1}. Hiding: As in 6.7. Characteristics: 3 (if n < 5) resp. 4 variables, modal depth 7 (if n < 14) resp. n + 14 div 4.

kt grz n(n) :≡ □Grz_{1}{p_{2}/p_{0}} ∧ ⋀_{i=1,...,n−1}(l(i)) ∧ Grz_{1}{C () ∧ A4{C ()/p_{0}}/p_{0}} → A5{p_{1}/p_{0}} ∨ A5{p_{2}/p_{0}} ∨ A5{p_{3}/p_{0}}

l(i) :≡ \{ \begin{matrix}Grz_{1}\{l2 (i div 4)/p_{0}\} & i mod 4 = 0 \\ Grz_{1}\{□l2 (i div 4) ∨ p_{1}/p_{0}\} & i mod 4 = 1 \\ Grz_{1}\{□l2 (i div 4) ∨ p_{1} ∨ p_{2}/p_{0}\} & i mod 4 = 2 \\ Grz_{1}\{□l2 (i div 4) ∨ p_{1} ∨ p_{2} ∨ p_{3}/p_{0}\} & otherwise \end{matrix}

l2 , C as in 6.7.

7.9 kt md p

Idea: In backward proof search, we have to find the way to g(n, n, ¬p_{1}) through a lot of □ and ◇. Charateristics: One (if n = 1) resp. two variables, modal depth 0 (if n = 1) resp. n^{2} − n + 1.

kt md p(n) :≡ p_{1} ∨ ⋁_{i=1,...,n−1}(g(i, n, ¬p_{1} ∧ ◇f(1, n, p_{2})) ∨ g(i, n, ¬p_{1} ∧ ◇f (1, n, p_{1})) ∨ g(i, n, ¬p_{2} ∧ ◇f (1, n, p_{1}))) ∨ g(n, n, ¬p_{1})

g(i, n, A) :≡ \{ \begin{matrix}A & i = 1 \\ f (i, n, g(i − 1, n, A)) & otherwise \end{matrix}

f (i, n, A) :≡ ◇^{i−1}□◇^{n−i}A

7.10 kt md n

Idea: Similar to 7.9, but simpler. The subformula g(n, n, ¬p_{1}) is missing in order to make the formulas unprovable. Charateristics: One variable, modal depth 0 (if n = 1) resp. n^{2} − n + 1.

kt md n(n) :≡ p_{1} ∨ ⋁_{i=1,...,n−1}(g(i, n, ¬p_{1} ∧ ◇f (1, n, p_{1})))

f , g as in 7.9.

7.11 kt path p

Idea, hiding: As in 6.11, but we use new variables on each level of the labyrinth. (The formulas k path p collapse in KT since KT ⊢ ◇^{n}A → A.) Characteristics: 6n variables, modal depth n.

kt path p(n) :≡ (□p_{11} ∨ □p_{10+path el(1,n)} ∨ □p_{13} ∨ □p_{15})

∨ ⋁_{i=1,...,n;j=1,...,6}(left to right(i, j, n) ∨ right to left(i, j, n))

∨ (◇^{n}¬p_{10n+2} ∨ ◇^{n}¬p_{10n+4} ∨ ◇^{n}¬p_{10n+path el(n,n)} ∨ ◇^{n}¬p_{10n+6})

path el, left to right, right to left, delete, modg as in 6.11. lists2fml(l, k, s) :≡ ⋁_{x∈s}(◇^{l}(¬p_{10l+k} ∧ □p_{10(l+1)+x})) lists2fml back(l, k, s) :≡ ⋁_{x∈s}(◇^{l}(¬p_{10l+x} ∧ □p_{10(l+1)+k}))

7.12 kt path n

Idea, hiding: As in 6.12, but we use new variables on each level of the labyrinth. (The formulas k path p collapse in KT since KT ⊢ ◇^{n}A → A.) Characteristics: 6n variables, modal depth n + 1.

kt path n(n) :≡ (□p_{11} ∨ □p_{10+path el(1,n+1)} ∨ □p_{13} ∨ □p_{15}) ∨ ⋁_{i=1,...,n+1;j=1,...,6}(left to right(i, j, n + 1) ∨ right to left(i, j, n + 1)) ∨ (◇^{n+1}¬p_{10(n+1)+2} ∨ ◇^{n+1}¬p_{10(n+1)+4} ∨ ◇^{n+1}¬p_{10(n+1)+path el(n+1,n+1)} ∨ ◇^{n+1}¬p_{10(n+1)+6})

path el, left to right, right to left, delete, modg as in 6.12. lists2fml, lists2fml back as in 7.11.

7.13 kt ph p

Idea, hiding: As in 6.13. Characteristics: Essentially a CPC problem. n^{2} + n variables, modal depth 1 (if n = 1) resp. 2.

kt ph p(n) :≡ left(n) → ◇right(n) left, right, l as in 6.13.

7.14 kt ph n

Idea, hiding: As in 6.14. Characteristics: Essentially a CPC problem. n^{2} + n variables, modal depth 1 (if n = 1) resp. 2.

kt ph n(n) :≡ left(n) → ◇right(n) left, right, l, l2 as in 6.14.

7.15 kt poly p

Idea, hiding: As in 6.15. Characteristics: Essentially a CPC problem. About 7.5n variables, modal depth about 5n.

kt poly p(n) :≡ \{ \begin{matrix}poly(5n + 1) & n mod 2 = 0 \\ poly(5n) & n mod 2 = 1 \end{matrix} poly as in 6.15.

f (i, n) :≡ \{ \begin{matrix}false & i = 0 \\ ◇(f (i − 1, n) ∨ ◇^{i+2}(p_{n} ↔ p_{1})) ∨ □p_{i+2} & i = n \\ ◇(f (i − 1, n) ∨ ◇^{i+2}(p_{i} ↔ p_{i+1})) ∨ □p_{i+2} & otherwise \end{matrix}

7.16 kt poly n

Idea, hiding: As in 6.16. Characteristics: Essentially a CPC problem. About 7.5n variables, modal depth about 5n.

kt poly n(n) :≡ \{ \begin{matrix}poly(3n) & n mod 2 = 0 \\ poly(3n + 1) & n mod 2 = 1 \end{matrix}

poly, f as in 7.15.

7.17 kt t4p p

Idea, hiding: As in 6.17. Characteristics: 4 variables, modal depth n + 4. Partially in negation normal form.

kt t4p p(n) :≡ E(n) ∨ nnf(¬C (n)) ∨ ◇p_{4}

C (i) :≡ \{ \begin{matrix}((□◇p_{0} → □□◇p_{1}) ∧ □(◇□◇p_{0} ∧ p_{0} → □p_{1}) ∧ □◇p_{1})\{p_{0} ∧ ◇¬p_{3}/p_{1}\} & i = 0 \\ □A4\{p_{1}/p_{0}\} ∧ □C (i − 1) & otherwise \end{matrix}

E as in 6.17.

7.18 kt t4p n

Idea, hiding: As in 6.18. Characteristics: 4 variables, modal depth 2n + 3. Partially in negation normal form.

kt t4p n(n) :≡ E(2n − 1) ∨ nnf(¬C (2n − 1)) ∨ ◇p_{4}

C (i) :≡ \{ \begin{matrix}((□◇p_{0} → ◇p_{1}) ∧ (□◇p_{0} → □□◇p_{1}) \\ ∧□(◇□◇p_{0} ∧ p_{0} → □p_{1}))\{p_{0} ∧ ◇¬p_{3}/p_{1}\} & i = 0 \\ □A4\{p_{1}/p_{0}\} ∧ □C (i − 1) & otherwise \end{matrix}

E as in 6.17.

8 Formulas for S4

8.1 s4 45 p

Idea: S4 ⊢ A5{□p_{0}/p_{0}} ∧ □A5{¬p_{0}/p_{0}} → A5. Hiding: The left hand side occurs with 1 to n □, the right hand side occurs just with n □ in front. Additionally some superfluous instances, and the whole formula in negation normal form. Characteristics: One variable, modal depth n + 3, in negation normal form.

s4 45 p(n) :≡ nnf(⋁_{i=1,...,n}(h(n, A5) ∨ ¬h(i, D_{2}) ∨ ¬h(i, A5{◇¬p_{0}/p_{0}}) ∨ ¬h(i, □A5) ∨ ¬h(i, B)))

h(i, A) :≡ \{ \begin{matrix}A & i = 0 \\ □p_{0} ∨ □h(i − 1, A) ∨ □p_{1} & otherwise \end{matrix}

8.2 s4 45 n

Idea: A5 is not provable in S4. Hiding: As in 8.1. Characteristics: One variable, modal depth n + 3, in negation normal form.

s4 45 n(n) :≡ nnf(⋁_{i=1,...,n}(h(n, (□p_{0} ∨ □◇¬p_{0})) ∨ ¬h(i, A4) ∨ ¬h(i, A4{◇p_{0}/p_{0}}) ∨ ¬h(i, T)

∨ ¬h(i, A4{□p_{0} → p_{0}/p_{0}}) ∨ ¬h(i, T{□p_{0} → p_{0}/p_{0}})))

h as in 8.1.

8.3 s4 branch p

Idea: The branching formula as described in [4], plus a negation symbol in front and the additional subformula □p_{(n div 3)+1} in order to make the formula provable. Charateristics: 2n + 3 variables, modal depth 2.

s4 branch p(n) :≡ ¬(p_{100} ∧ ¬p_{101} ∧ □(bdepth(n) ∧ det(n) ∧ branching(n))) ∨ ¬□p_{(n div 3)+1} bdepth, det, branching as in 6.1.

8.4 s4 branch n

Idea: The branching formula as defined in [4]. Characteristics: Every Kripke model that satisfies the pure branching formula must have an exponential number of worlds (cp. [4]). 2n + 3 variables, modal depth 2.

s4 branch n(n) :≡ ¬(p_{100} ∧ ¬p_{101} ∧ □(bdepth(n) ∧ det(n) ∧ branching(n)))

bdepth, det, branching as in 6.1.

8.5 s4 grz p

Idea: S4 ⊢ □Grz ∧ Grz{C () ∧ (A4{C ()/p_{0}})/p_{0} → Grz_{1}, where C is defined as below. Hiding: Many superfluous instances with iterated □ inside the instances. The subformulas ¬□◇p_{0} and ¬◇¬(□◇p_{0} ∨ p_{1}) are the parts of a weakened instance of A4. Characteristics: 4 (if n < 5) resp. 5 variables, modal depth 7 (if n < 14) resp. n + 14 div 4.

s4 grz p(n) :≡ □Grz{p_{2}/p_{0}} ∧ ⋀_{i=1,...,n−1}(l(i)) ∧ Grz{C () ∧ (A4{C ()/p_{0}})/p_{0}} → Grz_{1}{p_{1}/p_{0}} ∨ Grz_{1}{p_{2}/p_{0}} ∧ ¬□◇p_{0} ∨ Grz_{1}{p_{3}/p_{0}} ∨ Grz_{1}{p_{2}/p_{0}} ∧ ¬◇¬(□◇p_{0} ∨ p_{1})

l, l2 , C as in 6.7.

8.6 s4 grz n

Idea: A5 is not provable in S4 plus instances of Grz_{1}. Hiding: As in 6.7. Characteristics: 3 (if n < 5) resp. 4 variables, modal depth 7 (if n < 14) resp. n + 14 div 4.

s4 grz n(n) :≡ □Grz_{1}{p_{2}/p_{0}} ∧ ⋀_{i=1,...,n−1}(l(i)) ∧ Grz_{1}{C () ∧ A4{C ()/p_{0}}/p_{0}} → A5{p_{1}/p_{0}} ∨ A5{p_{2}/p_{0}} ∨ A5{p_{3}/p_{0}}

l(i) :≡ \{ \begin{matrix}Grz_{1}\{l2 (i div 4)/p_{0}\} & i mod 4 = 0 \\ Grz_{1}\{□l2 (i div 4) ∨ p_{1}/p_{0}\} & i mod 4 = 1 \\ Grz_{1}\{□l2 (i div 4) ∨ p_{1} ∨ p_{2}/p_{0}\} & i mod 4 = 2 \\ Grz_{1}\{□l2 (i div 4) ∨ p_{1} ∨ p_{2} ∨ p_{3}/p_{0}\} & otherwise \end{matrix}

l2 , C as in 6.7.

8.7 s4 ipc p

Idea: We embed a formula that is provable in intuitionistic propositional logic in S4. Characteristics: n variables, modal depth 3.

s4 ipc p(n) :≡ ⋀_{i=1,...,n}(f(i, n)) → false

f (i, n) :≡ □(□(□p_{i} → ⋀_{j=1,...,n}(□p_{j})) → false)

8.8 s4 ipc n

Idea: We embed a formula that is not provable in intuitionistic propositional logic in S4. Characteristics: n variables, modal depth 3.

s4 ipc n(n) :≡ ⋀_{i=1,...,n}(f2 (i, n)) → false

f2 (i, n) :≡ \{ \begin{matrix}true & i = (n + 1) div 2 \\ f (i, n) & otherwise \end{matrix} f as in 8.7.

8.9 s4 md p

Idea: In backward proof search, we have to find the way to g(n, n, ¬p_{1}) through a lot of □ and ◇. Charateristics: One (if n = 1) resp. two variables, modal depth 0 (if n = 1) resp. n^{2} − n + 1.

s4 md p(n) :≡ p_{1} ∨ ⋁_{i=1,...,n−1}(g(i, n, ¬p_{1} ∧ ◇f (1, n, p_{2})) ∨ g(i, n, ¬p_{1} ∧ ◇f (1, n, p_{1})) ∨ g(i, n, ¬p_{2} ∧ ◇f (1, n, p_{1}))) ∨ g(n, n, ¬p_{1})

g as in 7.9. f (i, n, A) :≡ h(i − 1, □h(n − i, A))

h(i, A) :≡ \{ \begin{matrix}A & i = 0 \\ ◇h(i − 1, A) ∨ p_{2} & otherwise \end{matrix}

8.10 s4 md n

Idea: Similar to 8.9, but simpler. The subformula g(n, n, ¬p_{1}) is missing in order to make the formulas unprovable. Charateristics: One (if n = 1) resp. two variables, modal depth 0 (if n = 1) resp. n^{2} − n + 1.

s4 md n(n) :≡ p_{1} ∨ ⋁_{i=1,...,n−1}(g(i, n, ¬p_{1} ∧ ◇f(1, n, p_{1}))) f , g, h as in 8.9.

8.11 s4 path p

Idea, hiding: As in 7.11. Characteristics: 6n variables, modal depth n + 1.

s4 path p(n) :≡ (□□p_{11} ∨ □□p_{10+path el(1,n)} ∨ □□p_{13} ∨ □□p_{15}) ∨ ⋁_{i=1,...,n;j=1,...,6}(left to right(i, j, n) ∨ right to left(i, j, n))

∨ ◇(◇¬p_{10n+2} ∨ ◇¬p_{10n+4} ∨ ◇¬p_{10n+path el(n,n)} ∨ ◇¬p_{10n+6})

path el, left to right, right to left, delete, modg, lists2fml, lists2fml back as in 7.11.

8.12 s4 path n

Idea, hiding: As in 7.12. Characteristics: 6n variables, modal depth n + 2.

s4 path n(n) :≡ (□□p_{11} ∨ □□p_{10+path el(1,n+1)} ∨ □□p_{13} ∨ □□p_{15}) ∨ ⋁_{i=1,...,n+1;j=1,...,6}(left to right(i, j, n + 1) ∨ right to left(i, j, n + 1)) ∨ ◇(◇¬p_{10(n+1)+2} ∨ ◇¬p_{10(n+1)+4} ∨ ◇¬p_{10(n+1)+path el((n+1),(n+1))} ∨ ◇¬p_{10(n+1)+6})

path el, left to right, right to left, delete, modg, lists2fml, lists2fml back as in 7.12.

8.13 s4 ph p

Idea: The pigeonhole formulas. We assume n < 100. Hiding: Some □ and ◇. Characteristics: Essentially a CPC problem. O(n^{2}) variables, modal depth 2.

s4 ph p(n) :≡ left(n) → ◇right(n)

right(n) :≡ ⋁_{j=1,...,n;i_{1}=1,...,n+1;i_{2}=i_{1}+1,...,n+1}(◇(l(i_{1}, j) ∧ l(i_{2}, j)))

left, l as in 6.13.

8.14 s4 ph n

Idea: The pigeonhole formulas, with one missing conjunct on the right hand side. We assume n < 100. Hiding: Some □ and ◇. Characteristics: Essentially a CPC problem. O(n^{2}) variables, modal depth 2.

s4 ph n(n) :≡ left(n) → ◇right(n)

right(n) :≡ ⋁_{j=1,...,n;i_{1}=1,...,n+1;i_{2}=i_{1}+1,...,n+1}(◇(l2 (n, i_{1}, j) ∧ l2 (n, i_{2}, j)))

left, l as in 6.13.

l2 (n, i, j) :≡ \{ \begin{matrix}¬l(i, j) & i = j, i = (2n) div 3 + 1 \\ l(i, j) & otherwise \end{matrix}

8.15 s4 s5 p

Idea: A formula that is provable in S5 embedded in S4. Hiding: Some superfluous subformulas. Characteristics: 3n variables, modal depth 3n.

s4 s5 p(n) :≡ □◇(□ ⋁_{i=1,...,3n−2}(p_{i} ↔ p_{i+1}) ∨ □p_{3n} ∨ f (1, 3n − 1)) ∨ □(◇p_{1} → ¬p_{3n})

f (i, n) :≡ \{ \begin{matrix}false & i = n \\ ◇(p_{i} ∧ ¬p_{i+1} ∨ ¬p_{i} ∧ p_{i+1}) ∨ □f (i + 1, n) & otherwise \end{matrix}

8.16 s4 s5 n

Idea: A formula that is not provable in S5 embedded in S4. Hiding: Some superfluous subformulas. Characteristics: 6n variables, modal depth 6 − 4n.

s4 s5 n(n) :≡ □◇(□p_{6n} ∨ f (1, 6n − 5)) ∨ □(◇p_{1} → ¬p_{6n})

f as in 8.15.

8.17 s4 t4p p

Idea, hiding: As in 6.17. Characteristics: 4 variables, modal depth n + 4. Partially in negation normal form.

s4 t4p p(n) :≡ E(n) ∨ nnf(¬C (2n − 1)) ∨ ◇p_{4}

C (i) :≡ \{ \begin{matrix}(□(◇□◇p_{0} ∧ p_{0} → □p_{1}) ∧ □◇p_{1})\{p_{0} ∧ ◇¬p_{3}/p_{1}\} & i = 0 \\ Dum\{p_{1}/p_{0}\} ∧ □C (i − 1) & otherwise \end{matrix}

E as in 6.17.

8.18 s4 t4p n

Idea, hiding: As in 6.18. Characteristics: 4 variables, modal depth 2n + 3. Partially in negation normal form.

s4 t4p n(n) :≡ E(2n − 1) ∨ nnf(¬C (4n − 1)) ∨ ◇p_{4}

C (i) :≡ \{ \begin{matrix}((□◇p_{0} → ◇p_{1}) ∧ □(◇□◇p_{0} ∧ p_{0} → □p_{1}))\{p_{0} ∧ ◇¬p_{3}/p_{1}\} & i = 0 \\ Dum\{p_{1}/p_{0}\} ∧ □C (i − 1) & otherwise \end{matrix}

E as in 6.17.

9 Benchmark results for the LWB

Prover: We used the Logics Workbench (LWB), version 1.0. See [5] or the LWB home page

http://lwbwww.unibe.ch:8080/LWBinfo.html for more information.

For all the logics the LWB uses backward proof search in two-sided sequent calculi. Use-check (similar to [6]) helps to cut off superfluous branches. In the case of S4, a loop-check is used (see [7]). Programming language: C++ . Compiler: Sun C++ 4.0.1 . Operating system: Solaris 2.4 .

Availability: The binaries of the LWB 1.0 are available via the LWB home page (choose about

the LWB, install the LWB).

You can also use the LWB 1.0 via WWW. Choose run a session via WWW on the LWB home page and type in your request.

Additional facilities of the prover:

• graphical user interface

• built-in programming language

• progress indicator: a slider shows how the proof search is going on

• various functions to convert formulas

Hardware: Sun SPARCstation 5, main memory: 80MB, 1 CPU (70 MHz microSPARC II)

Timing: The timing includes the parsing of the formulas and the construction of the corresponding data structure. The files loaded by the LWB have the following form:

load(k);
timestart; provable(box p0 -> box box p0); timestop;
quit;

Results:

class  n_{p,i} class  n_{n,i}
k branch p  6 k branch n  7
k d4 p  8 k d4 n  6
k dum p  13 k dum n  19
k grz p  7 k grz n  13
k lin p  11 k lin n  8
k path p  12 k path n  10
k ph p  4 k ph n  8
k poly p  8 k poly n  11
k t4p p  8 k t4p n  7

class  n_{p,i} class  n_{n,i}
kt 45 p  5 kt 45 n  4
kt branch p  5 kt branch n  6
kt dum p  5 kt dum n  10
kt grz p  6 kt grz n  > 20
kt md p  5 kt md n  5
kt path p  10 kt path n  9
kt ph p  4 kt ph n  8
kt poly p  14 kt poly n  2
kt t4p p  5 kt t4p n  7

class  n_{p,i} class  n_{n,i}
s4 45 p  3 s4 45 n  5
s4 branch p 11 s4 branch n  7
s4 grz p  9 s4 grz n  > 20
s4 ipc p  8 s4 ipc n  7
s4 md p  8 s4 md n  6
s4 path p  8 s4 path n  6
s4 ph p  4 s4 ph n  8
s4 s5 p  4 s4 s5 n  9
s4 t4p p  9 s4 t4p n  12

In order to make absolutely clear how we obtained the numbers in the tables above from the run times, we give the run times for some of the formulas in the classes k branch p and k branch n. k branch p(6) resp. k branch n(7) are the last formulas that could be decided in less than 100 seconds; therefore we enter the numbers 6 resp. 7 in the first line of the table for K.

formula

run time (in seconds)

k branch p(1)  0.02
k branch p(2)  0.06
k branch p(3)  0.28
k branch p(4)  1.80
k branch p(5)  11.89
k branch p(6)  74.64
k branch p(7)  503.94

formula

run time (in seconds)

k branch n(1)  0.02
k branch n(2)  0.05
k branch n(3)  0.15
k branch n(4)  0.51
k branch n(5)  2.17
k branch n(6)  9.69
k branch n(7)  43.42
k branch n(8)  203.81

10 Availability of the formulas

You can get the first 15 formulas of each class as well as the LWB programs that generated these

formulas. Load the LWB home page http://lwbwww.unibe.ch:8080/LWBinfo.html in a WWW

browser and then choose the item benchmarks. For each class of the three logics K, KT, S4 there is a compressed ASCII file (inside a tar file) that contains the first 15 formulas. The files contain a header line, a line with the word begin , then one formula on each line (with the corresponding number in front), and finally a line with the word end . The formulas are written in infix notation. The connectives are ~ for ¬, & for ∧, v for ∨, -> for →, <-> for ↔. No brackets are omitted in the formulas in order to make the conversion into other formats easier. It can happen that for some classes you need more than 15 formulas. Then you have several possibilities:

• Get the LWB procedures we used to generate the formulas, install the LWB, and generate the required formulas.

• Write a procedure that generates the formulas in this class according to the definitions in the sections 6, 7, 8. Please make sure that you generate the same formulas as we do by comparing the first 15 formulas, or at least by comparing the values of appendix I.

• Get the LWB procedures and use the LWB via WWW (choose the item run a session on the LWB home page). You have to replace the read statements in the files by the corresponding files for this purpose. Use set("bracketmode", "full"); to obtain all the brackets.

11 Conclusion

We stated postulates for benchmark methods for proof search procedures. and presented a benchmark method for the propositional modal logics K, KT, S4 that satisfies these postulates. Until now often just a few arbitrary — and often very easy — formulas were used to judge the efficiency of such theorem provers. With our method it is now possible to compare these provers in a standardized and fair way. Since we use but scalable formulas, the method will still be applicable when there are much faster machines and more efficient proof search procedures. Of course the postulates are not limited to benchmark tests for modal logic theorem provers, but seem also reasonable for other non-classical logics.

References

[1] L. Catach. Tableaux: A general theorem prover for modal logics. Journal of Automated Reasoning, 7:489–510, 1991.

[2] S. Demri. Uniform and non uniform strategies for tableaux calculi for modal logics. Journal of Applied Non-Classical Logics, 5(1):77–96, 1995.

[3] F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propositional decision procedures – the case study of modal K. In CADE 96, LNCS, 1996.

[4] J. Halpern and Y. Moses. A guide to completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence, 54:319–379, 1992.

[5] A. Heuerding, G. Jäger, S. Schwendimann, and M. Seyfried. Propositional logics on the computer. In P. Baumgartner, R. Hähnle, and J. Posegga, editors, Tableaux 95, LNCS 918, pages 310–323, 1995.

[6] A. Heuerding and S. Schwendimann. On the modal logic K plus theories. In H. Kleine Büning, editor, CSL 95, LNCS 1092, pages 308–319, 1996.

[7] A. Heuerding, M. Seyfried, and H. Zimmermann. Efficient loop-check for backward proof search in some non-classical propositional logics. In P. Miglioli, U. Moscato, D. Mundici, and M. Ornaghi, editors, Tableaux 96, LNCS 1071, pages 210–225, 1996.

[8] E. Koutsoupias and C. Papadimitriou. On the greedy algorithm for satisfiability. Information Processing Letters, 43:53–55, 1992.

[9] F. Pelletier. Seventy-five problems for testing automatic theorem provers. Journal of Automated Reasoning, 2:191–216, 1986.

[10] B. Selman, H. Levesque, and D. Mitchell. A new method for solving hard satisfiability problems. In Proceedings 10th AAAI, pages 47–59, 1992.

[11] G. Sutcliffe, C. Suttner, and T. Yemenis. The TPTP problem library. In A. Bundy, editor, CADE 12, LNCS 814, pages 252–266, 1994.

12 Appendix I: Formulas generated with the LWB

12.1 K

12.1.1 k branch p
> for i := 1 to 6 do
      print(i, ":  ", length(k_branch_p(i)), ", ", modaldepth(k_branch_p(i)), ", ", vars(k_branch_p(i)));
    1:  142, 2, [p0, p1, p100, p101, p102]
    2:  343, 3, [p0, p1, p2, p100, p101, p102, p103]
    3:  633, 4, [p0, p1, p2, p3, p100, p101, p102, p103, p104]
    4:  1012, 5, [p0, p1, p2, p3, p4, p100, p101, p102, p103, p104, p105]
    5:  1480, 6, [p0, p1, p2, p3, p4, p5, p100, p101, p102, p103, p104, p105, p106]
    6:  2037, 7, [p0, p1, p2, p3, p4, p5, p6, p100, p101, p102, p103, p104, p105, p106, p107]
> k_branch_p(1);
    ~(p100 & ~p101 & ((p101 -> p100) & (p102 -> p101) & ((p100 -> (p0 -> box (p100 -> p0)) & (~p0 -> box (p100 -> ~p0))) & (p101 ->
(p1 -> box (p101 -> p1)) & (~p1 -> box (p101 -> ~p1)))) & (p100 & ~p101 -> dia (p101 & ~p102 & p1) & dia (p101 & ~p102 & ~p1)) & box
((p101 -> p100) & (p102 -> p101) & ((p100 -> (p0 -> box (p100 -> p0)) & (~p0 -> box (p100 -> ~p0))) & (p101 -> (p1 -> box (p101 ->
p1)) & (~p1 -> box (p101 -> ~p1)))) & (p100 & ~p101 -> dia (p101 & ~p102 & p1) & dia (p101 & ~p102 & ~p1))))) v ~box p1
> k_branch_p(2);
    ~(p100 & ~p101 & ((p101 -> p100) & (p102 -> p101) & (p103 -> p102) & ((p100 -> (p0 -> box (p100 -> p0)) & (~p0 -> box (p100 ->
~p0))) & (p101 -> (p1 -> box (p101 -> p1)) & (~p1 -> box (p101 -> ~p1))) & (p102 -> (p2 -> box (p102 -> p2)) & (~p2 -> box (p102 ->
~p2)))) & ((p100 & ~p101 -> dia (p101 & ~p102 & p1) & dia (p101 & ~p102 & ~p1)) & (p101 & ~p102 -> dia (p102 & ~p103 & p2) & dia (p102
& ~p103 & ~p2))) & box ((p101 -> p100) & (p102 -> p101) & (p103 -> p102) & ((p100 -> (p0 -> box (p100 -> p0)) & (~p0 -> box (p100 ->
~p0))) & (p101 -> (p1 -> box (p101 -> p1)) & (~p1 -> box (p101 -> ~p1))) & (p102 -> (p2 -> box (p102 -> p2)) & (~p2 -> box (p102 ->
~p2)))) & ((p100 & ~p101 -> dia (p101 & ~p102 & p1) & dia (p101 & ~p102 & ~p1)) & (p101 & ~p102 -> dia (p102 & ~p103 & p2) & dia (p102
& ~p103 & ~p2)))) & box box ((p101 -> p100) & (p102 -> p101) & (p103 -> p102) & ((p100 -> (p0 -> box (p100 -> p0)) & (~p0 -> box (p100
-> ~p0))) & (p101 -> (p1 -> box (p101 -> p1)) & (~p1 -> box (p101 -> ~p1))) & (p102 -> (p2 -> box (p102 -> p2)) & (~p2 -> box (p102
-> ~p2)))) & ((p100 & ~p101 -> dia (p101 & ~p102 & p1) & dia (p101 & ~p102 & ~p1)) & (p101 & ~p102 -> dia (p102 & ~p103 & p2) & dia
(p102 & ~p103 & ~p2)))))) v ~box box p1

12.1.2 k branch n
> for i := 1 to 6 do
      print(i, ":  ", length(k_branch_n(i)), ", ", modaldepth(k_branch_n(i)), ", ", vars(k_branch_n(i)));
    1:  138, 2, [p0, p1, p100, p101, p102]
    2:  338, 3, [p0, p1, p2, p100, p101, p102, p103]
    3:  627, 4, [p0, p1, p2, p3, p100, p101, p102, p103, p104]
    4:  1005, 5, [p0, p1, p2, p3, p4, p100, p101, p102, p103, p104, p105]
    5:  1472, 6, [p0, p1, p2, p3, p4, p5, p100, p101, p102, p103, p104, p105, p106]
    6:  2028, 7, [p0, p1, p2, p3, p4, p5, p6, p100, p101, p102, p103, p104, p105, p106, p107]
> k_branch_n(1);
    ~(p100 & ~p101 & ((p101 -> p100) & (p102 -> p101) & ((p100 -> (p0 -> box (p100 -> p0)) & (~p0 -> box (p100 -> ~p0))) & (p101 ->
(p1 -> box (p101 -> p1)) & (~p1 -> box (p101 -> ~p1)))) & (p100 & ~p101 -> dia (p101 & ~p102 & p1) & dia (p101 & ~p102 & ~p1)) & box
((p101 -> p100) & (p102 -> p101) & ((p100 -> (p0 -> box (p100 -> p0)) & (~p0 -> box (p100 -> ~p0))) & (p101 -> (p1 -> box (p101 ->
p1)) & (~p1 -> box (p101 -> ~p1)))) & (p100 & ~p101 -> dia (p101 & ~p102 & p1) & dia (p101 & ~p102 & ~p1)))))
> k_branch_n(2);
    ~(p100 & ~p101 & ((p101 -> p100) & (p102 -> p101) & (p103 -> p102) & ((p100 -> (p0 -> box (p100 -> p0)) & (~p0 -> box (p100 ->
~p0))) & (p101 -> (p1 -> box (p101 -> p1)) & (~p1 -> box (p101 -> ~p1))) & (p102 -> (p2 -> box (p102 -> p2)) & (~p2 -> box (p102 ->
~p2)))) & ((p100 & ~p101 -> dia (p101 & ~p102 & p1) & dia (p101 & ~p102 & ~p1)) & (p101 & ~p102 -> dia (p102 & ~p103 & p2) & dia (p102
& ~p103 & ~p2))) & box ((p101 -> p100) & (p102 -> p101) & (p103 -> p102) & ((p100 -> (p0 -> box (p100 -> p0)) & (~p0 -> box (p100 ->
~p0))) & (p101 -> (p1 -> box (p101 -> p1)) & (~p1 -> box (p101 -> ~p1))) & (p102 -> (p2 -> box (p102 -> p2)) & (~p2 -> box (p102 ->
~p2)))) & ((p100 & ~p101 -> dia (p101 & ~p102 & p1) & dia (p101 & ~p102 & ~p1)) & (p101 & ~p102 -> dia (p102 & ~p103 & p2) & dia (p102
& ~p103 & ~p2)))) & box box ((p101 -> p100) & (p102 -> p101) & (p103 -> p102) & ((p100 -> (p0 -> box (p100 -> p0)) & (~p0 -> box (p100
-> ~p0))) & (p101 -> (p1 -> box (p101 -> p1)) & (~p1 -> box (p101 -> ~p1))) & (p102 -> (p2 -> box (p102 -> p2)) & (~p2 -> box (p102
-> ~p2)))) & ((p100 & ~p101 -> dia (p101 & ~p102 & p1) & dia (p101 & ~p102 & ~p1)) & (p101 & ~p102 -> dia (p102 & ~p103 & p2) & dia
(p102 & ~p103 & ~p2))))))

12.1.3 k d4 p

> for i := 1 to 6 do
      print(i, ":  ", length(k_d4_p(i)), ", ", modaldepth(k_d4_p(i)), ", ", vars(k_d4_p(i)));
    1:  46, 4, [p0]
    2:  100, 5, [p0]
    3:  161, 6, [p0]
    4:  229, 7, [p0]
    5:  304, 8, [p0]
    6:  386, 9, [p0]
> k_d4_p(1);
    box (dia ~p0 v p0) v dia box false v dia (box p0 & dia dia ~p0) v dia (box dia p0 & dia dia box ~p0) v dia (p0 & dia box ~p0) v
dia (~p0 & dia box p0)
> k_d4_p(2);
    box box (dia ~p0 v p0) v dia box false v dia (box p0 & dia dia ~p0) v dia (box dia p0 & dia dia box ~p0) v dia (p0 & dia box ~p0)
v dia (~p0 & dia box p0) v (box box (dia ~p0 v p0) v dia dia box false v dia dia (box p0 & dia dia ~p0) v dia dia (box dia p0 & dia
dia box ~p0) v dia dia (p0 & dia box ~p0) v dia dia (~p0 & dia box p0))

12.1.4 k d4 n

> for i := 1 to 6 do
  print(i, ":  ", length(k_d4_n(i)), ", ", modaldepth(k_d4_n(i)), ", ", vars(k_d4_n(i)));
1:  72, 4, [p0]
2:  153, 5, [p0]
3:  242, 6, [p0]
4:  339, 7, [p0]
5:  444, 8, [p0]
6:  557, 9, [p0]
> k_d4_n(1);
box (box p0 v box dia ~p0) v dia box false v dia (box p0 & dia dia ~p0) v dia (box dia p0 & dia dia box ~p0) v dia (box p0 & box
~p0) v dia (box (box ~p0 v p0) & dia dia (dia p0 & ~p0)) v dia (box (dia ~p0 v p0) & dia dia (box p0 & ~p0))
> k_d4_n(2);
box box (box p0 v box dia ~p0) v dia box false v dia (box p0 & dia dia ~p0) v dia (box dia p0 & dia dia box ~p0) v dia (box p0
& box ~p0) v dia (box (box ~p0 v p0) & dia dia (dia p0 & ~p0)) v dia (box (dia ~p0 v p0) & dia dia (box p0 & ~p0)) v (box box (box
p0 v box dia ~p0) v dia dia box false v dia dia (box p0 & dia dia ~p0) v dia dia (box dia p0 & dia dia box ~p0) v dia dia (box p0 &
box ~p0) v dia dia (box (box ~p0 v p0) & dia dia (dia p0 & ~p0)) v dia dia (box (dia ~p0 v p0) & dia dia (box p0 & ~p0)))

12.1.5 k dum p

> for i := 1 to 6 do
  print(i, ":  ", length(k_dum_p(i)), ", ", modaldepth(k_dum_p(i)), ", ", vars(k_dum_p(i)));
1:  95, 5, [p0]
2:  119, 5, [p0]
3:  119, 5, [p0]
4:  146, 6, [p0]
5:  172, 7, [p0]
6:  201, 7, [p0]
> k_dum_p(1);
true & ~box (box (box (p0 -> box p0) -> p0) -> dia box p0 -> box p0) -> dia ~((box (box (p0 -> box p0) -> p0) -> box box (box (p0
-> box p0) -> p0)) & box (box p0 -> box box p0) & (box (box (p0 -> box p0) -> p0) -> dia box p0 -> p0) & (box (box ((p0 -> box p0)
-> box (p0 -> box p0)) -> p0 -> box p0) -> dia box (p0 -> box p0) -> p0 -> box p0)) v false
> k_dum_p(2);
box (box (box p0 -> box box p0) & (box (box (p0 -> box p0) -> p0) -> dia box p0 -> p0)) & ~box box (box (box (p0 -> box p0) ->
p0) -> dia box p0 -> box p0) -> dia dia ~((box (box (p0 -> box p0) -> p0) -> box box (box (p0 -> box p0) -> p0)) & box (box p0 -> box
box p0) & (box (box (p0 -> box p0) -> p0) -> dia box p0 -> p0) & (box (box ((p0 -> box p0) -> box (p0 -> box p0)) -> p0 -> box p0)
-> dia box (p0 -> box p0) -> p0 -> box p0)) v false

12.1.6 k dum n

> for i := 1 to 6 do
  print(i, ":  ", length(k_dum_n(i)), ", ", modaldepth(k_dum_n(i)), ", ", vars(k_dum_n(i)));
1:  105, 6, [p0]
2:  132, 7, [p0]
3:  134, 8, [p0]
4:  164, 9, [p0]
5:  195, 10, [p0]
6:  227, 11, [p0]
> k_dum_n(1);
true & ~box box (box (box (p0 -> box p0) -> p0) -> dia box p0 -> p0) -> dia dia ~((box (box (p0 -> box p0) -> p0) -> box box (box
(p0 -> box p0) -> p0)) & box (box p0 -> box box p0) & (box (box (p0 -> box p0) -> p0) -> dia box p0 -> p0 v box p0) & (box (box ((p0
-> box p0) -> box (p0 -> box p0)) -> p0 -> box p0) -> dia box (p0 -> box p0) -> (p0 -> box p0) v box (p0 -> box p0))) v false
> k_dum_n(2);
box (box (box p0 -> box box p0) & (box (box (p0 -> box p0) -> p0) -> dia box p0 -> p0 v box p0)) & ~box box box (box (box (p0 ->
box p0) -> p0) -> dia box p0 -> p0) -> dia dia dia ~((box (box (p0 -> box p0) -> p0) -> box box (box (p0 -> box p0) -> p0)) & box (box
p0 -> box box p0) & (box (box (p0 -> box p0) -> p0) -> dia box p0 -> p0 v box p0) & (box (box ((p0 -> box p0) -> box (p0 -> box p0))
-> p0 -> box p0) -> dia box (p0 -> box p0) -> (p0 -> box p0) v box (p0 -> box p0))) v false

12.1.7 k grz p

> for i := 1 to 6 do
  print(i, ":  ", length(k_grz_p(i)), ", ", modaldepth(k_grz_p(i)), ", ", vars(k_grz_p(i)));
1:  160, 7, [p1, p2, p3]
2:  181, 7, [p1, p2, p3]
3:  212, 7, [p1, p2, p3]
4:  251, 7, [p1, p2, p3]
5:  298, 7, [p1, p2, p3, p4]
6:  357, 7, [p1, p2, p3, p4]
> k_grz_p(1);

    box (box (box (p2 -> box p2) -> p2) -> p2) & true & (box (box ((box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) ->
box box (box (p2 -> box p2) -> p2)) -> box ((box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box
p2) -> p2)))) -> (box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2))) -> (box (p2 ->
box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2))) -> (box (box (p1 -> box p1) -> p1) -> box
p1) v (box (box (p2 -> box p2) -> p2) -> box p2) v (box (box (p3 -> box p3) -> p3) -> box p3)
> k_grz_p(2);
    box (box (box (p2 -> box p2) -> p2) -> p2) & (box (box (box false v p1 -> box (box false v p1)) -> box false v p1) -> box false
v p1) & (box (box ((box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2)) -> box ((box
(p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2)))) -> (box (p2 -> box p2) -> p2) & (box
(box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2))) -> (box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2)
-> box box (box (p2 -> box p2) -> p2))) -> (box (box (p1 -> box p1) -> p1) -> box p1) v (box (box (p2 -> box p2) -> p2) -> box p2)
v (box (box (p3 -> box p3) -> p3) -> box p3)

12.1.8 k grz n

> for i := 1 to 6 do
      print(i, ":  ", length(k_grz_n(i)), ", ", modaldepth(k_grz_n(i)), ", ", vars(k_grz_n(i)));
    1:  159, 7, [p1, p2, p3]
    2:  181, 7, [p1, p2, p3]
    3:  213, 7, [p1, p2, p3]
    4:  253, 7, [p1, p2, p3]
    5:  301, 7, [p1, p2, p3, p4]
    6:  361, 7, [p1, p2, p3, p4]
> k_grz_n(1);
    box (box (box (p2 -> box p2) -> p2) -> box p2) & true & (box (box ((box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2)
-> box box (box (p2 -> box p2) -> p2)) -> box ((box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 ->
box p2) -> p2)))) -> (box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2))) -> box ((box
(p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2)))) -> (box (box (p1 -> box p1) -> p1)
-> p1) v (box (box (p2 -> box p2) -> p2) -> p2) v (box (box (p3 -> box p3) -> p3) -> p3)
> k_grz_n(2);
    box (box (box (p2 -> box p2) -> p2) -> box p2) & (box (box (box false v p1 -> box (box false v p1)) -> box false v p1) -> box (box
false v p1)) & (box (box ((box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2)) -> box
((box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2)))) -> (box (p2 -> box p2) -> p2)
& (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2))) -> box ((box (p2 -> box p2) -> p2) & (box (box (p2 -> box
p2) -> p2) -> box box (box (p2 -> box p2) -> p2)))) -> (box (box (p1 -> box p1) -> p1) -> p1) v (box (box (p2 -> box p2) -> p2) ->
p2) v (box (box (p3 -> box p3) -> p3) -> p3)

12.1.9 k lin p

> for i := 1 to 6 do
      print(i, ":  ", length(k_lin_p(i)), ", ", modaldepth(k_lin_p(i)), ", ", vars(k_lin_p(i)));
    1:  97, 3, [p1, p2]
    2:  177, 3, [p1, p2, p3]
    3:  255, 3, [p1, p2, p3, p4]
    4:  335, 3, [p1, p2, p3, p4, p5]
    5:  415, 3, [p1, p2, p3, p4, p5, p6]
    6:  495, 3, [p1, p2, p3, p4, p5, p6, p7]
> k_lin_p(1);
    false v (box (p1 & box p1 -> p1) v box (p1 & box p1 -> p1)) v ~(box ((p1 & box p1 & p1 -> p2) v (~p1 -> ~(box p2 & p2))) & box
(box (p1 & box p1 & p1 -> p2) v (~p1 -> ~(box p2 & p2))) & box ((p1 & box p1 & p1 -> p2) v box (~p1 -> ~(box p2 & p2))) -> box (p1
& box p1 & p1 -> p2) v box (~p1 -> ~(box p2 & p2)))
> k_lin_p(2);
    false v (box (p2 & box p2 -> p2) v box (p2 & box p2 -> p2)) v (~(box ((p1 & box p1 & p1 -> p2) v (~p1 -> ~(box p2 & p2))) & box
(box (p1 & box p1 & p1 -> p2) v (~p1 -> ~(box p2 & p2))) & box ((p1 & box p1 & p1 -> p2) v box (~p1 -> ~(box p2 & p2))) -> box (p1
& box p1 & p1 -> p2) v box (~p1 -> ~(box p2 & p2))) v ~(box ((p2 & box p2 & p2 -> p3) v (~p2 -> ~(box p3 & p3))) & box (box (p2 & box
p2 & p2 -> p3) v (~p2 -> ~(box p3 & p3))) & box ((p2 & box p2 & p2 -> p3) v box (~p2 -> ~(box p3 & p3))) -> box (p2 & box p2 & p2 ->
p3) v box (~p2 -> ~(box p3 & p3))))

12.1.10 k lin n

> for i := 1 to 6 do
      print(i, ":  ", length(k_lin_n(i)), ", ", modaldepth(k_lin_n(i)), ", ", vars(k_lin_n(i)));
    1:  15, 2, [p1]
    2:  149, 3, [p1, p2, p3, p4, p5]
    3:  333, 3, [p1, p2, p3, p4, p5, p6, p7, p8, p9]
    4:  517, 3, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13]
    5:  701, 3, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17]
    6:  885, 3, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21]
> k_lin_n(1);
    false v (box (box p1 -> p1) v box (box p1 -> p1)) v false
> k_lin_n(2);
    ~(box (dia p1 & box dia p1 -> p2) v box (p2 & box p2 -> dia p1)) v ~(box ((p1 -> box p2) & box (p1 -> box p2) -> p2) v box (p2
& box p2 -> p1 -> box p2)) v (~(box (dia p2 & box dia p2 -> p3) v box (p3 & box p3 -> dia p2)) v ~(box ((p2 -> box p3) & box (p2 ->
box p3) -> p3) v box (p3 & box p3 -> p2 -> box p3))) v (box (box p2 -> p2) v box (box p2 -> p2)) v (~(box (dia p4 & box dia p4 -> p5)
v box (p5 & box p5 -> dia p4)) v ~(box ((p4 -> box p5) & box (p4 -> box p5) -> p5) v box (p5 & box p5 -> p4 -> box p5)))

12.1.11 k path p

> for i := 1 to 6 do
      print(i, ":  ", length(k_path_p(i)), ", ", modaldepth(k_path_p(i)), ", ", vars(k_path_p(i)));
    1:  51, 1, [p1, p2, p3, p4, p5, p6]
    2:  156, 2, [p1, p2, p3, p4, p5, p6]
    3:  324, 3, [p1, p2, p3, p4, p5, p6]
    4:  455, 4, [p1, p2, p3, p4, p5, p6]
    5:  661, 5, [p1, p2, p3, p4, p5, p6]
    6:  818, 6, [p1, p2, p3, p4, p5, p6]
> k_path_p(1);
    box p1 v box p2 v box p3 v box p5 v (false v false v (false v false) v (false v false) v (false v false) v (false v false) v (false
v false)) v (dia ~p2 v dia ~p4 v dia ~p2 v dia ~p6)
> k_path_p(2);
    box p1 v box p2 v box p3 v box p5 v (dia (~p1 & box p1) v dia (~p1 & box p3) v false v (dia (~p2 & box p5) v false) v (dia (~p3
& box p1) v dia (~p3 & box p3) v false) v (false v false) v (dia (~p5 & box p1) v dia (~p5 & box p3) v false) v (false v false) v (false
v false) v (false v (dia (~p4 & box p2) v dia (~p6 & box p2))) v (false v false) v (false v (dia (~p4 & box p4) v dia (~p6 & box p4)))
v (false v false) v (false v (dia (~p4 & box p6) v dia (~p6 & box p6)))) v (dia dia ~p2 v dia dia ~p4 v dia dia ~p5 v dia dia ~p6)

12.1.12 k path n

> for i := 1 to 6 do
      print(i, ":  ", length(k_path_n(i)), ", ", modaldepth(k_path_n(i)), ", ", vars(k_path_n(i)));
    1:  151, 2, [p1, p2, p3, p4, p5, p6]
    2:  319, 3, [p1, p2, p3, p4, p5, p6]
    3:  447, 4, [p1, p2, p3, p4, p5, p6]
    4:  653, 5, [p1, p2, p3, p4, p5, p6]
    5:  811, 6, [p1, p2, p3, p4, p5, p6]
    6:  1055, 7, [p1, p2, p3, p4, p5, p6]
> k_path_n(1);
    box p1 v box p2 v box p3 v box p5 v (dia (~p1 & box p1) v dia (~p1 & box p3) v false v (false v false) v (dia (~p3 & box p1) v
dia (~p3 & box p3) v false) v (false v false) v (dia (~p5 & box p1) v dia (~p5 & box p3) v false) v (false v false) v (false v false)
v (false v (dia (~p4 & box p2) v dia (~p6 & box p2))) v (false v false) v (false v (dia (~p4 & box p4) v dia (~p6 & box p4))) v (false
v false) v (false v (dia (~p4 & box p6) v dia (~p6 & box p6)))) v (dia dia ~p2 v dia dia ~p4 v dia dia ~p5 v dia dia ~p6)
> k_path_n(2);
    box p1 v box p2 v box p3 v box p5 v (dia (~p1 & box p1) v dia (~p1 & box p3) v false v (false v false) v (dia (~p3 & box p1) v
dia (~p3 & box p3) v false) v (false v false) v (dia (~p5 & box p1) v dia (~p5 & box p3) v false) v (false v false) v (dia dia (~p1
& box p1) v dia dia (~p1 & box p3) v dia dia (~p1 & box p5) v false) v (false v (dia (~p4 & box p2) v dia (~p6 & box p2))) v (dia dia
(~p3 & box p1) v dia dia (~p3 & box p3) v dia dia (~p3 & box p5) v false) v (false v (dia (~p4 & box p4) v dia (~p6 & box p4))) v (dia
dia (~p5 & box p1) v dia dia (~p5 & box p3) v dia dia (~p5 & box p2) v dia dia (~p5 & box p5) v false) v (false v (dia (~p4 & box p6)
v dia (~p6 & box p6))) v (false v false) v (false v (dia dia (~p2 & box p2) v dia dia (~p4 & box p2) v dia dia (~p6 & box p2))) v (false
v false) v (false v (dia dia (~p2 & box p4) v dia dia (~p4 & box p4) v dia dia (~p6 & box p4))) v (false v false) v (false v (dia dia
(~p2 & box p6) v dia dia (~p4 & box p6) v dia dia (~p6 & box p6)))) v (dia dia dia ~p2 v dia dia dia ~p4 v dia dia dia ~p2 v dia dia
dia ~p6)

12.1.13 k ph p

> for i := 1 to 6 do
      print(i, ":  ", length(k_ph_p(i)), ", ", modaldepth(k_ph_p(i)), ", ", vars(k_ph_p(i)));
    1:  9, 1, [p101, p201]
    2:  40, 2, [p101, p102, p201, p202, p301, p302]
    3:  109, 2, [p101, p102, p103, p201, p202, p203, p301, p302, p303, p401, p402, p403]
    4:  231, 2, [p101, p102, p103, p104, p201, p202, p203, p204, p301, p302, p303, p304, p401, p402, p403, p404, p501, p502, p503,
p504]
    5:  421, 2, [p101, p102, p103, p104, p105, p201, p202, p203, p204, p205, p301, p302, p303, p304, p305, p401, p402, p403, p404,
p405, p501, p502, p503, p504, p505, p601, p602, p603, p604, p605]
    6:  694, 2, [p101, p102, p103, p104, p105, p106, p201, p202, p203, p204, p205, p206, p301, p302, p303, p304, p305, p306, p401,
p402, p403, p404, p405, p406, p501, p502, p503, p504, p505, p506, p601, p602, p603, p604, p605, p606, p701, p702, p703, p704, p705,
p706]
> k_ph_p(1);
    dia (p101 & p201) -> dia (p101 & p201)
> k_ph_p(2);
    dia ((p101 v box p102) & (p201 v p202) & (p301 v p302)) -> dia (p101 & p201 v p101 & p301 v p201 & p301 v box p102 & p202 v box
p102 & p302 v p202 & p302)

12.1.14 k ph n

> for i := 1 to 6 do
      print(i, ":  ", length(k_ph_n(i)), ", ", modaldepth(k_ph_n(i)), ", ", vars(k_ph_n(i)));
    1:  10, 1, [p101, p201]
    2:  42, 2, [p101, p102, p201, p202, p301, p302]
    3:  112, 2, [p101, p102, p103, p201, p202, p203, p301, p302, p303, p401, p402, p403]

    4:  235, 2, [p101, p102, p103, p104, p201, p202, p203, p204, p301, p302, p303, p304, p401, p402, p403, p404, p501, p502, p503,
p504]
    5:  426, 2, [p101, p102, p103, p104, p105, p201, p202, p203, p204, p205, p301, p302, p303, p304, p305, p401, p402, p403, p404,
p405, p501, p502, p503, p504, p505, p601, p602, p603, p604, p605]
    6:  700, 2, [p101, p102, p103, p104, p105, p106, p201, p202, p203, p204, p205, p206, p301, p302, p303, p304, p305, p306, p401,
p402, p403, p404, p405, p406, p501, p502, p503, p504, p505, p506, p601, p602, p603, p604, p605, p606, p701, p702, p703, p704, p705,
p706]
> k_ph_n(1);
    dia (p101 & p201) -> dia (~p101 & p201)
> k_ph_n(2);
    dia ((p101 v box p102) & (p201 v p202) & (p301 v p302)) -> dia (p101 & p201 v p101 & p301 v p201 & p301 v box p102 & ~p202 v box
p102 & p302 v ~p202 & p302)

12.1.15 k poly p

> for i := 1 to 6 do
      print(i, ":  ", length(k_poly_p(i)), ", ", modaldepth(k_poly_p(i)), ", ", vars(k_poly_p(i)));
    1:  59, 4, [p1, p2, p3, p4, p5, p6, p8]
    2:  141, 8, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p12, p14, p16]
    3:  188, 10, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p14, p16, p18, p20]
    4:  294, 14, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p18, p20, p22, p24, p26, p28]
    5:  353, 16, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p20, p22, p24, p26, p28, p30, p32]
    6:  483, 20, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p24, p26, p28,
p30, p32, p34, p36, p38, p40]
> k_poly_p(1);
    box box box box (p1 & p2 & p3 & p4) v (dia (dia (dia (false v dia (p1 <-> p2)) v box p3 v dia dia (p2 <-> p3)) v box p4 v dia dia
dia (p3 <-> p1)) v box p5) v box box box box (~p2 & ~p4 & ~p6 & ~p8)
> k_poly_p(2);
    box box box box box box box box (p1 & p2 & p3 & p4 & p5 & p6 & p7 & p8) v (dia (dia (dia (dia (dia (dia (dia (false v dia (p1 <->
p2)) v box p3 v dia dia (p2 <-> p3)) v box p4 v dia dia dia (p3 <-> p4)) v box p5 v dia dia dia dia (p4 <-> p5)) v box p6 v dia dia
dia dia dia (p5 <-> p6)) v box p7 v dia dia dia dia dia dia (p6 <-> p7)) v box p8 v dia dia dia dia dia dia dia (p7 <-> p1)) v box
p9) v box box box box box box box box (~p2 & ~p4 & ~p6 & ~p8 & ~p10 & ~p12 & ~p14 & ~p16)

12.1.16 k poly n

> for i := 1 to 6 do
      print(i, ":  ", length(k_poly_n(i)), ", ", modaldepth(k_poly_n(i)), ", ", vars(k_poly_n(i)));
    1:  78, 5, [p1, p2, p3, p4, p5, p6, p8, p10]
    2:  119, 7, [p1, p2, p3, p4, p5, p6, p7, p8, p10, p12, p14]
    3:  213, 11, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p14, p16, p18, p20, p22]
    4:  266, 13, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p16, p18, p20, p22, p24, p26]
    5:  384, 17, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p20, p22, p24, p26, p28, p30, p32,
p34]
    6:  449, 19, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p22, p24, p26, p28, p30,
p32, p34, p36, p38]
> k_poly_n(1);
    box box box box box (p1 & p2 & p3 & p4 & p5) v (dia (dia (dia (dia (false v dia (p1 <-> p2)) v box p3 v dia dia (p2 <-> p3)) v
box p4 v dia dia dia (p3 <-> p4)) v box p5 v dia dia dia dia (p4 <-> p1)) v box p6) v box box box box box (~p2 & ~p4 & ~p6 & ~p8 &
~p10)
> k_poly_n(2);
    box box box box box box box (p1 & p2 & p3 & p4 & p5 & p6 & p7) v (dia (dia (dia (dia (dia (dia (false v dia (p1 <-> p2)) v box
p3 v dia dia (p2 <-> p3)) v box p4 v dia dia dia (p3 <-> p4)) v box p5 v dia dia dia dia (p4 <-> p5)) v box p6 v dia dia dia dia dia
(p5 <-> p6)) v box p7 v dia dia dia dia dia dia (p6 <-> p1)) v box p8) v box box box box box box box (~p2 & ~p4 & ~p6 & ~p8 & ~p10
& ~p12 & ~p14)

12.1.17 k t4p p

> for i := 1 to 6 do
      print(i, ":  ", length(k_t4p_p(i)), ", ", modaldepth(k_t4p_p(i)), ", ", vars(k_t4p_p(i)));
    1:  110, 6, [p0, p1, p3, p4]
    2:  153, 7, [p0, p1, p3, p4]
    3:  196, 8, [p0, p1, p3, p4]
    4:  239, 9, [p0, p1, p3, p4]
    5:  282, 10, [p0, p1, p3, p4]
    6:  325, 11, [p0, p1, p3, p4]
> k_t4p_p(1);
    dia ~(box ~p1 -> box box ~p1) v box dia box p0 v box (~box p1 -> box ~box p1) v (dia (box p1 & dia dia ~p1) v dia (box dia p0 &
box (~p0 v box p3) v dia (box dia box (~p0 v box p3) & box dia p0) v box dia p0 & dia dia box (~p0 v box p3) v dia (dia box dia p0
& p0 & dia (~p0 v box p3)) v dia box (~p0 v box p3)) v dia (box dia p1 & dia dia box ~p1)) v dia p4
> k_t4p_p(2);
    dia ~(box ~p1 -> box box ~p1) v box (dia ~(box ~p1 -> box box ~p1) v box dia box p0 v box (~box p1 -> box ~box p1)) v box (~box
p1 -> box ~box p1) v (dia (box p1 & dia dia ~p1) v dia (dia (box p1 & dia dia ~p1) v dia (box dia p0 & box (~p0 v box p3) v dia (box
dia box (~p0 v box p3) & box dia p0) v box dia p0 & dia dia box (~p0 v box p3) v dia (dia box dia p0 & p0 & dia (~p0 v box p3)) v dia
box (~p0 v box p3)) v dia (box dia p1 & dia dia box ~p1)) v dia (box dia p1 & dia dia box ~p1)) v dia p4

12.1.18 k t4p n

> for i := 1 to 6 do
  print(i, ":  ", length(k_t4p_n(i)), ", ", modaldepth(k_t4p_n(i)), ", ", vars(k_t4p_n(i)));
1:  102, 6, [p0, p1, p3, p4]
2:  188, 8, [p0, p1, p3, p4]
3:  274, 10, [p0, p1, p3, p4]
4:  360, 12, [p0, p1, p3, p4]
5:  446, 14, [p0, p1, p3, p4]
6:  532, 16, [p0, p1, p3, p4]
> k_t4p_n(1);
dia ~(box ~p1 -> box box ~p1) v box dia box p0 v box (~box p1 -> box ~box p1) v (dia (box p1 & dia dia ~p1) v dia (box dia p0 &
box (~p0 v box p3) v dia (box dia box (~p0 v box p3) & box dia p0) v box dia p0 & dia dia box (~p0 v box p3) v dia (dia box dia p0
& p0 & dia (~p0 v box p3))) v dia (box dia p1 & dia dia box ~p1)) v dia p4
> k_t4p_n(2);
dia ~(box ~p1 -> box box ~p1) v box (dia ~(box ~p1 -> box box ~p1) v box (dia ~(box ~p1 -> box box ~p1) v box dia box p0 v box
(~box p1 -> box ~box p1)) v box (~box p1 -> box ~box p1)) v box (~box p1 -> box ~box p1) v (dia (box p1 & dia dia ~p1) v dia (dia (box
p1 & dia dia ~p1) v dia (dia (box p1 & dia dia ~p1) v dia (box dia p0 & box (~p0 v box p3) v dia (box dia box (~p0 v box p3) & box
dia p0) v box dia p0 & dia dia box (~p0 v box p3) v dia (dia box dia p0 & p0 & dia (~p0 v box p3))) v dia (box dia p1 & dia dia box
~p1)) v dia (box dia p1 & dia dia box ~p1)) v dia (box dia p1 & dia dia box ~p1)) v dia p4

12.2 KT

12.2.1 kt 45 p

> for i := 1 to 6 do
  print(i, ":  ", length(kt_45_p(i)), ", ", modaldepth(kt_45_p(i)), ", ", vars(kt_45_p(i)));
1:  41, 4, [p0]
2:  89, 5, [p0]
3:  143, 6, [p0]
4:  203, 7, [p0]
5:  269, 8, [p0]
6:  341, 9, [p0]
> kt_45_p(1);
box (dia ~p0 v box box p0) v dia box false v dia (dia box p0 & dia box dia ~p0) v dia dia (dia ~p0 & dia box p0) v dia (p0 & dia
box ~p0)
> kt_45_p(2);
box box (dia ~p0 v box box p0) v dia box false v dia (dia box p0 & dia box dia ~p0) v dia dia (dia ~p0 & dia box p0) v dia (p0
& dia box ~p0) v (box box (dia ~p0 v box box p0) v dia dia box false v dia dia (dia box p0 & dia box dia ~p0) v dia dia dia (dia ~p0
& dia box p0) v dia dia (p0 & dia box ~p0))

12.2.2 kt 45 n

> for i := 1 to 6 do
  print(i, ":  ", length(kt_45_n(i)), ", ", modaldepth(kt_45_n(i)), ", ", vars(kt_45_n(i)));
1:  67, 4, [p0]
2:  142, 5, [p0]
3:  224, 6, [p0]
4:  313, 7, [p0]
5:  409, 8, [p0]
6:  512, 9, [p0]
> kt_45_n(1);
box (box p0 v box dia ~p0) v dia (box p0 & dia dia ~p0) v dia (box dia p0 & dia dia box ~p0) v dia (box p0 & ~p0) v dia (box (box
~p0 v p0) & dia dia (dia p0 & ~p0)) v dia (box (dia ~p0 v p0) & dia dia (box p0 & ~p0))
> kt_45_n(2);
box box (box p0 v box dia ~p0) v dia (box p0 & dia dia ~p0) v dia (box dia p0 & dia dia box ~p0) v dia (box p0 & ~p0) v dia (box
(box ~p0 v p0) & dia dia (dia p0 & ~p0)) v dia (box (dia ~p0 v p0) & dia dia (box p0 & ~p0)) v (box box (box p0 v box dia ~p0) v dia
dia (box p0 & dia dia ~p0) v dia dia (box dia p0 & dia dia box ~p0) v dia dia (box p0 & ~p0) v dia dia (box (box ~p0 v p0) & dia dia
(dia p0 & ~p0)) v dia dia (box (dia ~p0 v p0) & dia dia (box p0 & ~p0)))

12.2.3 kt branch p
> for i := 1 to 6 do
  print(i, ":  ", length(kt_branch_p(i)), ", ", modaldepth(kt_branch_p(i)), ", ", vars(kt_branch_p(i)));
1:  76, 2, [p0, p1, p100, p101, p102]
2:  122, 3, [p0, p1, p2, p100, p101, p102, p103]
3:  168, 4, [p0, p1, p2, p3, p100, p101, p102, p103, p104]
4:  214, 5, [p0, p1, p2, p3, p4, p100, p101, p102, p103, p104, p105]
5:  260, 6, [p0, p1, p2, p3, p4, p5, p100, p101, p102, p103, p104, p105, p106]
6:  306, 7, [p0, p1, p2, p3, p4, p5, p6, p100, p101, p102, p103, p104, p105, p106, p107]
> kt_branch_p(1);

    ~(p100 & ~p101 & box ((p101 -> p100) & (p102 -> p101) & ((p100 -> (p0 -> box (p100 -> p0)) & (~p0 -> box (p100 -> ~p0))) & (p101
-> (p1 -> box (p101 -> p1)) & (~p1 -> box (p101 -> ~p1)))) & (p100 & ~p101 -> dia (p101 & ~p102 & p1) & dia (p101 & ~p102 & ~p1))))
v ~box p1
> kt_branch_p(2);
    ~(p100 & ~p101 & box box ((p101 -> p100) & (p102 -> p101) & (p103 -> p102) & ((p100 -> (p0 -> box (p100 -> p0)) & (~p0 -> box (p100
-> ~p0))) & (p101 -> (p1 -> box (p101 -> p1)) & (~p1 -> box (p101 -> ~p1))) & (p102 -> (p2 -> box (p102 -> p2)) & (~p2 -> box (p102
-> ~p2)))) & ((p100 & ~p101 -> dia (p101 & ~p102 & p1) & dia (p101 & ~p102 & ~p1)) & (p101 & ~p102 -> dia (p102 & ~p103 & p2) & dia
(p102 & ~p103 & ~p2))))) v ~box box p1

12.2.4 kt branch n
> for i := 1 to 6 do
      print(i, ":  ", length(kt_branch_n(i)), ", ", modaldepth(kt_branch_n(i)), ", ", vars(kt_branch_n(i)));
    1:  72, 2, [p0, p1, p100, p101, p102]
    2:  117, 3, [p0, p1, p2, p100, p101, p102, p103]
    3:  162, 4, [p0, p1, p2, p3, p100, p101, p102, p103, p104]
    4:  207, 5, [p0, p1, p2, p3, p4, p100, p101, p102, p103, p104, p105]
    5:  252, 6, [p0, p1, p2, p3, p4, p5, p100, p101, p102, p103, p104, p105, p106]
    6:  297, 7, [p0, p1, p2, p3, p4, p5, p6, p100, p101, p102, p103, p104, p105, p106, p107]
> kt_branch_n(1);
    ~(p100 & ~p101 & box ((p101 -> p100) & (p102 -> p101) & ((p100 -> (p0 -> box (p100 -> p0)) & (~p0 -> box (p100 -> ~p0))) & (p101
-> (p1 -> box (p101 -> p1)) & (~p1 -> box (p101 -> ~p1)))) & (p100 & ~p101 -> dia (p101 & ~p102 & p1) & dia (p101 & ~p102 & ~p1))))
> kt_branch_n(2);
    ~(p100 & ~p101 & box box ((p101 -> p100) & (p102 -> p101) & (p103 -> p102) & ((p100 -> (p0 -> box (p100 -> p0)) & (~p0 -> box (p100
-> ~p0))) & (p101 -> (p1 -> box (p101 -> p1)) & (~p1 -> box (p101 -> ~p1))) & (p102 -> (p2 -> box (p102 -> p2)) & (~p2 -> box (p102
-> ~p2)))) & ((p100 & ~p101 -> dia (p101 & ~p102 & p1) & dia (p101 & ~p102 & ~p1)) & (p101 & ~p102 -> dia (p102 & ~p103 & p2) & dia
(p102 & ~p103 & ~p2)))))

12.2.5 kt dum p
> for i := 1 to 6 do
      print(i, ":  ", length(kt_dum_p(i)), ", ", modaldepth(kt_dum_p(i)), ", ", vars(kt_dum_p(i)));
    1:  95, 5, [p0]
    2:  103, 5, [p0]
    3:  103, 5, [p0]
    4:  114, 6, [p0]
    5:  124, 7, [p0]
    6:  137, 7, [p0]
> kt_dum_p(1);
    true & ~box (box (box (p0 -> box p0) -> p0) -> dia box p0 -> box p0) -> dia ~((box (box (p0 -> box p0) -> p0) -> box box (box (p0
-> box p0) -> p0)) & box (box p0 -> box box p0) & (box (box (p0 -> box p0) -> p0) -> dia box p0 -> p0) & (box (box ((p0 -> box p0)
-> box (p0 -> box p0)) -> p0 -> box p0) -> dia box (p0 -> box p0) -> p0 -> box p0)) v false
> kt_dum_p(2);
    box (box p0 -> box box p0) & ~box box (box (box (p0 -> box p0) -> p0) -> dia box p0 -> box p0) -> dia dia ~((box (box (p0 -> box
p0) -> p0) -> box box (box (p0 -> box p0) -> p0)) & box (box p0 -> box box p0) & (box (box (p0 -> box p0) -> p0) -> dia box p0 -> p0)
& (box (box ((p0 -> box p0) -> box (p0 -> box p0)) -> p0 -> box p0) -> dia box (p0 -> box p0) -> p0 -> box p0)) v false

12.2.6 kt dum n
> for i := 1 to 6 do
      print(i, ":  ", length(kt_dum_n(i)), ", ", modaldepth(kt_dum_n(i)), ", ", vars(kt_dum_n(i)));
    1:  90, 5, [p0]
    2:  114, 6, [p0]
    3:  114, 6, [p0]
    4:  141, 7, [p0]
    5:  167, 7, [p0]
    6:  196, 8, [p0]
> kt_dum_n(1);
    true & ~box (box (box (p0 -> box p0) -> p0) -> p0) -> dia ~((box (box (p0 -> box p0) -> p0) -> box box (box (p0 -> box p0) -> p0))
& box (box p0 -> box box p0) & (box (box (p0 -> box p0) -> p0) -> dia box p0 -> p0) & (box (box ((p0 -> box p0) -> box (p0 -> box p0))
-> p0 -> box p0) -> dia box (p0 -> box p0) -> p0 -> box p0)) v false
> kt_dum_n(2);
    box (box (box p0 -> box box p0) & (box (box (p0 -> box p0) -> p0) -> dia box p0 -> p0)) & ~box box (box (box (p0 -> box p0) ->
p0) -> p0) -> dia dia ~((box (box (p0 -> box p0) -> p0) -> box box (box (p0 -> box p0) -> p0)) & box (box p0 -> box box p0) & (box
(box (p0 -> box p0) -> p0) -> dia box p0 -> p0) & (box (box ((p0 -> box p0) -> box (p0 -> box p0)) -> p0 -> box p0) -> dia box (p0
-> box p0) -> p0 -> box p0)) v false

12.2.7 kt grz p
> for i := 1 to 6 do
  print(i, ":  ", length(kt_grz_p(i)), ", ", modaldepth(kt_grz_p(i)), ", ", vars(kt_grz_p(i)));
1:  180, 7, [p0, p1, p2, p3]
2:  201, 7, [p0, p1, p2, p3]
3:  232, 7, [p0, p1, p2, p3]
4:  271, 7, [p0, p1, p2, p3]
5:  318, 7, [p0, p1, p2, p3, p4]
6:  377, 7, [p0, p1, p2, p3, p4]
> kt_grz_p(1);
box (box (box (p2 -> box p2) -> p2) -> p2) & true & (box (box ((box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) ->
box box (box (p2 -> box p2) -> p2)) -> box ((box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box
p2) -> p2)))) -> (box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2))) -> (box (p2 ->
box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2))) -> (box (box (p1 -> box p1) -> p1) -> box
p1) v (box (box (p2 -> box p2) -> p2) -> box p2) & dia box ~p0 v (box (box (p3 -> box p3) -> p3) -> box p3) v (box (box (p2 -> box
p2) -> p2) -> box p2) & dia p0
> kt_grz_p(2);
box (box (box (p2 -> box p2) -> p2) -> p2) & (box (box (box false v p1 -> box (box false v p1)) -> box false v p1) -> box false
v p1) & (box (box ((box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2)) -> box ((box
(p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2)))) -> (box (p2 -> box p2) -> p2) & (box
(box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2))) -> (box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2)
-> box box (box (p2 -> box p2) -> p2))) -> (box (box (p1 -> box p1) -> p1) -> box p1) v (box (box (p2 -> box p2) -> p2) -> box p2)
& dia box ~p0 v (box (box (p3 -> box p3) -> p3) -> box p3) v (box (box (p2 -> box p2) -> p2) -> box p2) & dia p0

12.2.8 kt grz n
> for i := 1 to 6 do
  print(i, ":  ", length(kt_grz_n(i)), ", ", modaldepth(kt_grz_n(i)), ", ", vars(kt_grz_n(i)));
1:  153, 7, [p1, p2, p3]
2:  175, 7, [p1, p2, p3]
3:  207, 7, [p1, p2, p3]
4:  247, 7, [p1, p2, p3]
5:  295, 7, [p1, p2, p3, p4]
6:  355, 7, [p1, p2, p3, p4]
> kt_grz_n(1);
box (box (box (p2 -> box p2) -> p2) -> box p2) & true & (box (box ((box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2)
-> box box (box (p2 -> box p2) -> p2)) -> box ((box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 ->
box p2) -> p2)))) -> (box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2))) -> box ((box
(p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2)))) -> (~box p1 -> box ~box p1) v (~box
p2 -> box ~box p2) v (~box p3 -> box ~box p3)
> kt_grz_n(2);
box (box (box (p2 -> box p2) -> p2) -> box p2) & (box (box (box false v p1 -> box (box false v p1)) -> box false v p1) -> box (box
false v p1)) & (box (box ((box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2)) -> box
((box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2)))) -> (box (p2 -> box p2) -> p2)
& (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2))) -> box ((box (p2 -> box p2) -> p2) & (box (box (p2 -> box
p2) -> p2) -> box box (box (p2 -> box p2) -> p2)))) -> (~box p1 -> box ~box p1) v (~box p2 -> box ~box p2) v (~box p3 -> box ~box p3)

12.2.9 kt md p

> for i := 1 to 6 do
  print(i, ":  ", length(kt_md_p(i)), ", ", modaldepth(kt_md_p(i)), ", ", vars(kt_md_p(i)));
1:  6, 0, [p1]
2:  30, 3, [p1, p2]
3:  73, 7, [p1, p2]
4:  142, 13, [p1, p2]
5:  246, 21, [p1, p2]
6:  394, 31, [p1, p2]
> kt_md_p(1);
p1 v false v ~p1
> kt_md_p(2);
p1 v (~p1 & dia box dia p2 v ~p1 & dia box dia p1 v ~p2 & dia box dia p1) v dia box ~p1

12.2.10 kt md n

> for i := 1 to 6 do
  print(i, ":  ", length(kt_md_n(i)), ", ", modaldepth(kt_md_n(i)), ", ", vars(kt_md_n(i)));
1:  3, 0, [p1]
2:  9, 3, [p1]
3:  22, 7, [p1]
4:  43, 13, [p1]
5:  75, 21, [p1]
6:  121, 31, [p1]
> kt_md_n(1);
p1 v false
> kt_md_n(2);
p1 v ~p1 & dia box dia p1

12.2.11 kt path p
> for i := 1 to 6 do
      print(i, ":  ", length(kt_path_p(i)), ", ", modaldepth(kt_path_p(i)), ", ", vars(kt_path_p(i)));
    1:  51, 1, [p11, p12, p13, p14, p15, p16]
    2:  156, 2, [p11, p12, p13, p14, p15, p16, p21, p22, p23, p24, p25, p26]
    3:  324, 3, [p11, p12, p13, p14, p15, p16, p21, p22, p23, p24, p25, p26, p31, p32, p33, p34, p35, p36]
    4:  455, 4, [p11, p12, p13, p14, p15, p16, p21, p22, p23, p24, p25, p26, p31, p32, p33, p34, p35, p36, p41, p42, p43, p44, p45,
p46]
    5:  661, 5, [p11, p12, p13, p14, p15, p16, p21, p22, p23, p24, p25, p26, p31, p32, p33, p34, p35, p36, p41, p42, p43, p44, p45,
p46, p51, p52, p53, p54, p55, p56]
    6:  818, 6, [p11, p12, p13, p14, p15, p16, p21, p22, p23, p24, p25, p26, p31, p32, p33, p34, p35, p36, p41, p42, p43, p44, p45,
p46, p51, p52, p53, p54, p55, p56, p61, p62, p63, p64, p65, p66]
> kt_path_p(1);
    box p11 v box p12 v box p13 v box p15 v (false v false v (false v false) v (false v false) v (false v false) v (false v false)
v (false v false)) v (dia ~p12 v dia ~p14 v dia ~p12 v dia ~p16)
> kt_path_p(2);
    box p11 v box p12 v box p13 v box p15 v (dia (~p11 & box p21) v dia (~p11 & box p23) v false v (dia (~p12 & box p25) v false) v
(dia (~p13 & box p21) v dia (~p13 & box p23) v false) v (false v false) v (dia (~p15 & box p21) v dia (~p15 & box p23) v false) v (false
v false) v (false v false) v (false v (dia (~p14 & box p22) v dia (~p16 & box p22))) v (false v false) v (false v (dia (~p14 & box
p24) v dia (~p16 & box p24))) v (false v false) v (false v (dia (~p14 & box p26) v dia (~p16 & box p26)))) v (dia dia ~p22 v dia dia
~p24 v dia dia ~p25 v dia dia ~p26)

12.2.12 kt path n
> for i := 1 to 6 do
      print(i, ":  ", length(kt_path_n(i)), ", ", modaldepth(kt_path_n(i)), ", ", vars(kt_path_n(i)));
    1:  151, 2, [p11, p12, p13, p14, p15, p16, p21, p22, p23, p24, p25, p26]
    2:  319, 3, [p11, p12, p13, p14, p15, p16, p21, p22, p23, p24, p25, p26, p31, p32, p33, p34, p35, p36]
    3:  447, 4, [p11, p12, p13, p14, p15, p16, p21, p22, p23, p24, p25, p26, p31, p32, p33, p34, p35, p36, p41, p42, p43, p44, p45,
p46]
    4:  653, 5, [p11, p12, p13, p14, p15, p16, p21, p22, p23, p24, p25, p26, p31, p32, p33, p34, p35, p36, p41, p42, p43, p44, p45,
p46, p51, p52, p53, p54, p55, p56]
    5:  811, 6, [p11, p12, p13, p14, p15, p16, p21, p22, p23, p24, p25, p26, p31, p32, p33, p34, p35, p36, p41, p42, p43, p44, p45,
p46, p51, p52, p53, p54, p55, p56, p61, p62, p63, p64, p65, p66]
    6:  1055, 7, [p11, p12, p13, p14, p15, p16, p21, p22, p23, p24, p25, p26, p31, p32, p33, p34, p35, p36, p41, p42, p43, p44, p45,
p46, p51, p52, p53, p54, p55, p56, p61, p62, p63, p64, p65, p66, p71, p72, p73, p74, p75, p76]
> kt_path_n(1);
    box p11 v box p12 v box p13 v box p15 v (dia (~p11 & box p21) v dia (~p11 & box p23) v false v (false v false) v (dia (~p13 & box
p21) v dia (~p13 & box p23) v false) v (false v false) v (dia (~p15 & box p21) v dia (~p15 & box p23) v false) v (false v false) v
(false v false) v (false v (dia (~p14 & box p22) v dia (~p16 & box p22))) v (false v false) v (false v (dia (~p14 & box p24) v dia
(~p16 & box p24))) v (false v false) v (false v (dia (~p14 & box p26) v dia (~p16 & box p26)))) v (dia dia ~p22 v dia dia ~p24 v dia
dia ~p25 v dia dia ~p26)
> kt_path_n(2);
    box p11 v box p12 v box p13 v box p15 v (dia (~p11 & box p21) v dia (~p11 & box p23) v false v (false v false) v (dia (~p13 & box
p21) v dia (~p13 & box p23) v false) v (false v false) v (dia (~p15 & box p21) v dia (~p15 & box p23) v false) v (false v false) v
(dia dia (~p21 & box p31) v dia dia (~p21 & box p33) v dia dia (~p21 & box p35) v false) v (false v (dia (~p14 & box p22) v dia (~p16
& box p22))) v (dia dia (~p23 & box p31) v dia dia (~p23 & box p33) v dia dia (~p23 & box p35) v false) v (false v (dia (~p14 & box
p24) v dia (~p16 & box p24))) v (dia dia (~p25 & box p31) v dia dia (~p25 & box p33) v dia dia (~p25 & box p32) v dia dia (~p25 & box
p35) v false) v (false v (dia (~p14 & box p26) v dia (~p16 & box p26))) v (false v false) v (false v (dia dia (~p22 & box p32) v dia
dia (~p24 & box p32) v dia dia (~p26 & box p32))) v (false v false) v (false v (dia dia (~p22 & box p34) v dia dia (~p24 & box p34)
v dia dia (~p26 & box p34))) v (false v false) v (false v (dia dia (~p22 & box p36) v dia dia (~p24 & box p36) v dia dia (~p26 & box
p36)))) v (dia dia dia ~p32 v dia dia dia ~p34 v dia dia dia ~p32 v dia dia dia ~p36)

12.2.13 kt ph p

> for i := 1 to 6 do
      print(i, ":  ", length(kt_ph_p(i)), ", ", modaldepth(kt_ph_p(i)), ", ", vars(kt_ph_p(i)));
    1:  8, 1, [p101, p201]
    2:  39, 2, [p101, p102, p201, p202, p301, p302]
    3:  108, 2, [p101, p102, p103, p201, p202, p203, p301, p302, p303, p401, p402, p403]
    4:  230, 2, [p101, p102, p103, p104, p201, p202, p203, p204, p301, p302, p303, p304, p401, p402, p403, p404, p501, p502, p503,
p504]
    5:  420, 2, [p101, p102, p103, p104, p105, p201, p202, p203, p204, p205, p301, p302, p303, p304, p305, p401, p402, p403, p404,
p405, p501, p502, p503, p504, p505, p601, p602, p603, p604, p605]
    6:  693, 2, [p101, p102, p103, p104, p105, p106, p201, p202, p203, p204, p205, p206, p301, p302, p303, p304, p305, p306, p401,
p402, p403, p404, p405, p406, p501, p502, p503, p504, p505, p506, p601, p602, p603, p604, p605, p606, p701, p702, p703, p704, p705,
p706]
> kt_ph_p(1);
    p101 & p201 -> dia (p101 & p201)
> kt_ph_p(2);
    (p101 v box p102) & (p201 v p202) & (p301 v p302) -> dia (p101 & p201 v p101 & p301 v p201 & p301 v box p102 & p202 v box p102
& p302 v p202 & p302)

12.2.14 kt ph n

> for i := 1 to 6 do
      print(i, ":  ", length(kt_ph_n(i)), ", ", modaldepth(kt_ph_n(i)), ", ", vars(kt_ph_n(i)));
    1:  9, 1, [p101, p201]
    2:  41, 2, [p101, p102, p201, p202, p301, p302]
    3:  111, 2, [p101, p102, p103, p201, p202, p203, p301, p302, p303, p401, p402, p403]
    4:  234, 2, [p101, p102, p103, p104, p201, p202, p203, p204, p301, p302, p303, p304, p401, p402, p403, p404, p501, p502, p503,
p504]
    5:  425, 2, [p101, p102, p103, p104, p105, p201, p202, p203, p204, p205, p301, p302, p303, p304, p305, p401, p402, p403, p404,
p405, p501, p502, p503, p504, p505, p601, p602, p603, p604, p605]
    6:  699, 2, [p101, p102, p103, p104, p105, p106, p201, p202, p203, p204, p205, p206, p301, p302, p303, p304, p305, p306, p401,
p402, p403, p404, p405, p406, p501, p502, p503, p504, p505, p506, p601, p602, p603, p604, p605, p606, p701, p702, p703, p704, p705,
p706]
> kt_ph_n(1);
    p101 & p201 -> dia (~p101 & p201)
> kt_ph_n(2);
    (p101 v box p102) & (p201 v p202) & (p301 v p302) -> dia (p101 & p201 v p101 & p301 v p201 & p301 v box p102 & ~p202 v box p102
& p302 v ~p202 & p302)

12.2.15 kt poly p
> for i := 1 to 6 do
      print(i, ":  ", length(kt_poly_p(i)), ", ", modaldepth(kt_poly_p(i)), ", ", vars(kt_poly_p(i)));
    1:  108, 8, [p1, p2, p3, p4, p5, p6, p7, p8, p10, p12]
    2:  261, 14, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p16, p18, p20, p22, p24]
    3:  383, 18, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p20, p22, p24, p26, p28, p30, p32]
    4:  596, 24, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24, p26,
p28, p30, p32, p34, p36, p38, p40, p42, p44]
    5:  758, 28, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24, p25,
p26, p27, p28, p30, p32, p34, p36, p38, p40, p42, p44, p46, p48, p50, p52]
    6:  1031, 34, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24, p25,
p26, p27, p28, p29, p30, p31, p32, p33, p34, p36, p38, p40, p42, p44, p46, p48, p50, p52, p54, p56, p58, p60, p62, p64]
> kt_poly_p(1);
    box box box box box box (p1 & p2 & p3 & p4 & p5 & p6) v (dia (dia (dia (dia (dia (false v dia dia dia (p1 <-> p2)) v box p3 v dia
dia dia dia (p2 <-> p3)) v box p4 v dia dia dia dia dia (p3 <-> p4)) v box p5 v dia dia dia dia dia dia (p4 <-> p5)) v box p6 v dia
dia dia dia dia dia dia (p5 <-> p1)) v box p7) v box box box box box box (~p2 & ~p4 & ~p6 & ~p8 & ~p10 & ~p12)
> kt_poly_p(2);
    box box box box box box box box box box box box (p1 & p2 & p3 & p4 & p5 & p6 & p7 & p8 & p9 & p10 & p11 & p12) v (dia (dia (dia
(dia (dia (dia (dia (dia (dia (dia (dia (false v dia dia dia (p1 <-> p2)) v box p3 v dia dia dia dia (p2 <-> p3)) v box p4 v dia dia
dia dia dia (p3 <-> p4)) v box p5 v dia dia dia dia dia dia (p4 <-> p5)) v box p6 v dia dia dia dia dia dia dia (p5 <-> p6)) v box
p7 v dia dia dia dia dia dia dia dia (p6 <-> p7)) v box p8 v dia dia dia dia dia dia dia dia dia (p7 <-> p8)) v box p9 v dia dia dia
dia dia dia dia dia dia dia (p8 <-> p9)) v box p10 v dia dia dia dia dia dia dia dia dia dia dia (p9 <-> p10)) v box p11 v dia dia
dia dia dia dia dia dia dia dia dia dia (p10 <-> p11)) v box p12 v dia dia dia dia dia dia dia dia dia dia dia dia dia (p11 <-> p1))
v box p13) v box box box box box box box box box box box box (~p2 & ~p4 & ~p6 & ~p8 & ~p10 & ~p12 & ~p14 & ~p16 & ~p18 & ~p20 & ~p22
& ~p24)

12.2.16 kt poly n
> for i := 1 to 6 do
      print(i, ":  ", length(kt_poly_n(i)), ", ", modaldepth(kt_poly_n(i)), ", ", vars(kt_poly_n(i)));
    1:  86, 7, [p1, p2, p3, p4, p5, p6, p8, p10]
    2:  131, 9, [p1, p2, p3, p4, p5, p6, p7, p8, p10, p12, p14]
    3:  233, 13, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p14, p16, p18, p20, p22]
    4:  290, 15, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p16, p18, p20, p22, p24, p26]
    5:  416, 19, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p20, p22, p24, p26, p28, p30, p32,
p34]
    6:  485, 21, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p22, p24, p26, p28, p30,
p32, p34, p36, p38]
> kt_poly_n(1);
    box box box box box (p1 & p2 & p3 & p4 & p5) v (dia (dia (dia (dia (false v dia dia dia (p1 <-> p2)) v box p3 v dia dia dia dia
(p2 <-> p3)) v box p4 v dia dia dia dia dia (p3 <-> p4)) v box p5 v dia dia dia dia dia dia (p4 <-> p1)) v box p6) v box box box box
box (~p2 & ~p4 & ~p6 & ~p8 & ~p10)
> kt_poly_n(2);
    box box box box box box box (p1 & p2 & p3 & p4 & p5 & p6 & p7) v (dia (dia (dia (dia (dia (dia (false v dia dia dia (p1 <-> p2))
v box p3 v dia dia dia dia (p2 <-> p3)) v box p4 v dia dia dia dia dia (p3 <-> p4)) v box p5 v dia dia dia dia dia dia (p4 <-> p5))
v box p6 v dia dia dia dia dia dia dia (p5 <-> p6)) v box p7 v dia dia dia dia dia dia dia dia (p6 <-> p1)) v box p8) v box box box
box box box box (~p2 & ~p4 & ~p6 & ~p8 & ~p10 & ~p12 & ~p14)

12.2.17 kt t4p p

> for i := 1 to 6 do
  print(i, ":  ", length(kt_t4p_p(i)), ", ", modaldepth(kt_t4p_p(i)), ", ", vars(kt_t4p_p(i)));
1:  74, 5, [p0, p1, p3, p4]
2:  106, 6, [p0, p1, p3, p4]
3:  138, 7, [p0, p1, p3, p4]
4:  170, 8, [p0, p1, p3, p4]
5:  202, 9, [p0, p1, p3, p4]
6:  234, 10, [p0, p1, p3, p4]
> kt_t4p_p(1);
dia ~(box ~p1 -> box box ~p1) v box dia box p0 v box (~box p1 -> box ~box p1) v (dia (box p1 & dia dia ~p1) v dia (box dia p0 &
dia dia box (~p0 v box p3) v dia (dia box dia p0 & p0 & dia (~p0 v box p3)) v dia box (~p0 v box p3))) v dia p4
> kt_t4p_p(2);
dia ~(box ~p1 -> box box ~p1) v box (dia ~(box ~p1 -> box box ~p1) v box dia box p0 v box (~box p1 -> box ~box p1)) v box (~box
p1 -> box ~box p1) v (dia (box p1 & dia dia ~p1) v dia (dia (box p1 & dia dia ~p1) v dia (box dia p0 & dia dia box (~p0 v box p3) v
dia (dia box dia p0 & p0 & dia (~p0 v box p3)) v dia box (~p0 v box p3)))) v dia p4

12.2.18 kt t4p n

> for i := 1 to 6 do
  print(i, ":  ", length(kt_t4p_n(i)), ", ", modaldepth(kt_t4p_n(i)), ", ", vars(kt_t4p_n(i)));
1:  77, 5, [p0, p1, p3, p4]
2:  141, 7, [p0, p1, p3, p4]
3:  205, 9, [p0, p1, p3, p4]
4:  269, 11, [p0, p1, p3, p4]
5:  333, 13, [p0, p1, p3, p4]
6:  397, 15, [p0, p1, p3, p4]
> kt_t4p_n(1);
dia ~(box ~p1 -> box box ~p1) v box dia box p0 v box (~box p1 -> box ~box p1) v (dia (box p1 & dia dia ~p1) v dia (box dia p0 &
box (~p0 v box p3) v box dia p0 & dia dia box (~p0 v box p3) v dia (dia box dia p0 & p0 & dia (~p0 v box p3)))) v dia p4
> kt_t4p_n(2);
dia ~(box ~p1 -> box box ~p1) v box (dia ~(box ~p1 -> box box ~p1) v box (dia ~(box ~p1 -> box box ~p1) v box dia box p0 v box
(~box p1 -> box ~box p1)) v box (~box p1 -> box ~box p1)) v box (~box p1 -> box ~box p1) v (dia (box p1 & dia dia ~p1) v dia (dia (box
p1 & dia dia ~p1) v dia (dia (box p1 & dia dia ~p1) v dia (box dia p0 & box (~p0 v box p3) v box dia p0 & dia dia box (~p0 v box p3)
v dia (dia box dia p0 & p0 & dia (~p0 v box p3)))))) v dia p4

12.3 S4

12.3.1 s4 45 p

> for i := 1 to 6 do
  print(i, ":  ", length(s4_45_p(i)), ", ", modaldepth(s4_45_p(i)), ", ", vars(s4_45_p(i)));
1:  79, 4, [p0, p1]
2:  209, 5, [p0, p1]
3:  389, 6, [p0, p1]
4:  619, 7, [p0, p1]
5:  899, 8, [p0, p1]
6:  1229, 9, [p0, p1]
> s4_45_p(1);
box p0 v box (box p0 v box dia ~p0) v box p1 v dia ~p0 & dia box false & dia ~p1 v dia ~p0 & dia (dia box p0 & dia box dia ~p0)
& dia ~p1 v dia ~p0 & dia dia (dia ~p0 & dia box p0) & dia ~p1 v dia ~p0 & dia (p0 & dia box ~p0) & dia ~p1
> s4_45_p(2);
box p0 v box (box p0 v box (box p0 v box dia ~p0) v box p1) v box p1 v dia ~p0 & dia box false & dia ~p1 v dia ~p0 & dia (dia box
p0 & dia box dia ~p0) & dia ~p1 v dia ~p0 & dia dia (dia ~p0 & dia box p0) & dia ~p1 v dia ~p0 & dia (p0 & dia box ~p0) & dia ~p1 v
(box p0 v box (box p0 v box (box p0 v box dia ~p0) v box p1) v box p1 v dia ~p0 & dia (dia ~p0 & dia box false & dia ~p1) & dia ~p1
v dia ~p0 & dia (dia ~p0 & dia (dia box p0 & dia box dia ~p0) & dia ~p1) & dia ~p1 v dia ~p0 & dia (dia ~p0 & dia dia (dia ~p0 & dia
box p0) & dia ~p1) & dia ~p1 v dia ~p0 & dia (dia ~p0 & dia (p0 & dia box ~p0) & dia ~p1) & dia ~p1)

12.3.2 s4 45 n

> for i := 1 to 6 do
  print(i, ":  ", length(s4_45_n(i)), ", ", modaldepth(s4_45_n(i)), ", ", vars(s4_45_n(i)));
1:  111, 4, [p0, p1]
2:  282, 5, [p0, p1]
3:  512, 6, [p0, p1]
4:  801, 7, [p0, p1]
5:  1149, 8, [p0, p1]
6:  1556, 9, [p0, p1]
> s4_45_n(1);

    box p0 v box (box p0 v box dia ~p0) v box p1 v dia ~p0 & dia (box p0 & dia dia ~p0) & dia ~p1 v dia ~p0 & dia (box dia p0 & dia
dia box ~p0) & dia ~p1 v dia ~p0 & dia (box p0 & ~p0) & dia ~p1 v dia ~p0 & dia (box (dia ~p0 v p0) & dia dia (box p0 & ~p0)) & dia
~p1 v dia ~p0 & dia (box (dia ~p0 v p0) & (box p0 & ~p0)) & dia ~p1
> s4_45_n(2);
    box p0 v box (box p0 v box (box p0 v box dia ~p0) v box p1) v box p1 v dia ~p0 & dia (box p0 & dia dia ~p0) & dia ~p1 v dia ~p0
& dia (box dia p0 & dia dia box ~p0) & dia ~p1 v dia ~p0 & dia (box p0 & ~p0) & dia ~p1 v dia ~p0 & dia (box (dia ~p0 v p0) & dia dia
(box p0 & ~p0)) & dia ~p1 v dia ~p0 & dia (box (dia ~p0 v p0) & (box p0 & ~p0)) & dia ~p1 v (box p0 v box (box p0 v box (box p0 v box
dia ~p0) v box p1) v box p1 v dia ~p0 & dia (dia ~p0 & dia (box p0 & dia dia ~p0) & dia ~p1) & dia ~p1 v dia ~p0 & dia (dia ~p0 & dia
(box dia p0 & dia dia box ~p0) & dia ~p1) & dia ~p1 v dia ~p0 & dia (dia ~p0 & dia (box p0 & ~p0) & dia ~p1) & dia ~p1 v dia ~p0 &
dia (dia ~p0 & dia (box (dia ~p0 v p0) & dia dia (box p0 & ~p0)) & dia ~p1) & dia ~p1 v dia ~p0 & dia (dia ~p0 & dia (box (dia ~p0
v p0) & (box p0 & ~p0)) & dia ~p1) & dia ~p1)

12.3.3 s4 branch p
> for i := 1 to 6 do
      print(i, ":  ", length(s4_branch_p(i)), ", ", modaldepth(s4_branch_p(i)), ", ", vars(s4_branch_p(i)));
    1:  76, 2, [p0, p1, p100, p101, p102]
    2:  120, 2, [p0, p1, p2, p100, p101, p102, p103]
    3:  164, 2, [p0, p1, p2, p3, p100, p101, p102, p103, p104]
    4:  208, 2, [p0, p1, p2, p3, p4, p100, p101, p102, p103, p104, p105]
    5:  252, 2, [p0, p1, p2, p3, p4, p5, p100, p101, p102, p103, p104, p105, p106]
    6:  296, 2, [p0, p1, p2, p3, p4, p5, p6, p100, p101, p102, p103, p104, p105, p106, p107]
> s4_branch_p(1);
    ~(p100 & ~p101 & box ((p101 -> p100) & (p102 -> p101) & ((p100 -> (p0 -> box (p100 -> p0)) & (~p0 -> box (p100 -> ~p0))) & (p101
-> (p1 -> box (p101 -> p1)) & (~p1 -> box (p101 -> ~p1)))) & (p100 & ~p101 -> dia (p101 & ~p102 & p1) & dia (p101 & ~p102 & ~p1))))
v ~box p1
> s4_branch_p(2);
    ~(p100 & ~p101 & box ((p101 -> p100) & (p102 -> p101) & (p103 -> p102) & ((p100 -> (p0 -> box (p100 -> p0)) & (~p0 -> box (p100
-> ~p0))) & (p101 -> (p1 -> box (p101 -> p1)) & (~p1 -> box (p101 -> ~p1))) & (p102 -> (p2 -> box (p102 -> p2)) & (~p2 -> box (p102
-> ~p2)))) & ((p100 & ~p101 -> dia (p101 & ~p102 & p1) & dia (p101 & ~p102 & ~p1)) & (p101 & ~p102 -> dia (p102 & ~p103 & p2) & dia
(p102 & ~p103 & ~p2))))) v ~box p1

12.3.4 s4 branch n
> for i := 1 to 6 do
      print(i, ":  ", length(s4_branch_n(i)), ", ", modaldepth(s4_branch_n(i)), ", ", vars(s4_branch_n(i)));
    1:  72, 2, [p0, p1, p100, p101, p102]
    2:  116, 2, [p0, p1, p2, p100, p101, p102, p103]
    3:  160, 2, [p0, p1, p2, p3, p100, p101, p102, p103, p104]
    4:  204, 2, [p0, p1, p2, p3, p4, p100, p101, p102, p103, p104, p105]
    5:  248, 2, [p0, p1, p2, p3, p4, p5, p100, p101, p102, p103, p104, p105, p106]
    6:  292, 2, [p0, p1, p2, p3, p4, p5, p6, p100, p101, p102, p103, p104, p105, p106, p107]
> s4_branch_n(1);
    ~(p100 & ~p101 & box ((p101 -> p100) & (p102 -> p101) & ((p100 -> (p0 -> box (p100 -> p0)) & (~p0 -> box (p100 -> ~p0))) & (p101
-> (p1 -> box (p101 -> p1)) & (~p1 -> box (p101 -> ~p1)))) & (p100 & ~p101 -> dia (p101 & ~p102 & p1) & dia (p101 & ~p102 & ~p1))))
> s4_branch_n(2);
    ~(p100 & ~p101 & box ((p101 -> p100) & (p102 -> p101) & (p103 -> p102) & ((p100 -> (p0 -> box (p100 -> p0)) & (~p0 -> box (p100
-> ~p0))) & (p101 -> (p1 -> box (p101 -> p1)) & (~p1 -> box (p101 -> ~p1))) & (p102 -> (p2 -> box (p102 -> p2)) & (~p2 -> box (p102
-> ~p2)))) & ((p100 & ~p101 -> dia (p101 & ~p102 & p1) & dia (p101 & ~p102 & ~p1)) & (p101 & ~p102 -> dia (p102 & ~p103 & p2) & dia
(p102 & ~p103 & ~p2)))))

12.3.5 s4 grz p
> for i := 1 to 6 do
      print(i, ":  ", length(s4_grz_p(i)), ", ", modaldepth(s4_grz_p(i)), ", ", vars(s4_grz_p(i)));
    1:  186, 7, [p0, p1, p2, p3]
    2:  207, 7, [p0, p1, p2, p3]
    3:  238, 7, [p0, p1, p2, p3]
    4:  277, 7, [p0, p1, p2, p3]
    5:  324, 7, [p0, p1, p2, p3, p4]
    6:  383, 7, [p0, p1, p2, p3, p4]
> s4_grz_p(1);
    box (box (box (p2 -> box p2) -> p2) -> p2) & true & (box (box ((box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) ->
box box (box (p2 -> box p2) -> p2)) -> box ((box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box
p2) -> p2)))) -> (box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2))) -> (box (p2 ->
box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2))) -> (box (box (p1 -> box p1) -> p1) -> box
p1) v (box (box (p2 -> box p2) -> p2) -> box p2) & ~box dia p0 v (box (box (p3 -> box p3) -> p3) -> box p3) v (box (box (p2 -> box
p2) -> p2) -> box p2) & ~dia ~(box dia p0 v p1)
> s4_grz_p(2);
    box (box (box (p2 -> box p2) -> p2) -> p2) & (box (box (box false v p1 -> box (box false v p1)) -> box false v p1) -> box false
v p1) & (box (box ((box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2)) -> box ((box
(p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2)))) -> (box (p2 -> box p2) -> p2) & (box
(box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2))) -> (box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2)
-> box box (box (p2 -> box p2) -> p2))) -> (box (box (p1 -> box p1) -> p1) -> box p1) v (box (box (p2 -> box p2) -> p2) -> box p2)
& ~box dia p0 v (box (box (p3 -> box p3) -> p3) -> box p3) v (box (box (p2 -> box p2) -> p2) -> box p2) & ~dia ~(box dia p0 v p1)

12.3.6 s4 grz n
> for i := 1 to 6 do
  print(i, ":  ", length(s4_grz_n(i)), ", ", modaldepth(s4_grz_n(i)), ", ", vars(s4_grz_n(i)));
1:  153, 7, [p1, p2, p3]
2:  175, 7, [p1, p2, p3]
3:  207, 7, [p1, p2, p3]
4:  247, 7, [p1, p2, p3]
5:  295, 7, [p1, p2, p3, p4]
6:  355, 7, [p1, p2, p3, p4]
> s4_grz_n(1);
box (box (box (p2 -> box p2) -> p2) -> box p2) & true & (box (box ((box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2)
-> box box (box (p2 -> box p2) -> p2)) -> box ((box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 ->
box p2) -> p2)))) -> (box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2))) -> box ((box
(p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2)))) -> (~box p1 -> box ~box p1) v (~box
p2 -> box ~box p2) v (~box p3 -> box ~box p3)
> s4_grz_n(2);
box (box (box (p2 -> box p2) -> p2) -> box p2) & (box (box (box false v p1 -> box (box false v p1)) -> box false v p1) -> box (box
false v p1)) & (box (box ((box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2)) -> box
((box (p2 -> box p2) -> p2) & (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2)))) -> (box (p2 -> box p2) -> p2)
& (box (box (p2 -> box p2) -> p2) -> box box (box (p2 -> box p2) -> p2))) -> box ((box (p2 -> box p2) -> p2) & (box (box (p2 -> box
p2) -> p2) -> box box (box (p2 -> box p2) -> p2)))) -> (~box p1 -> box ~box p1) v (~box p2 -> box ~box p2) v (~box p3 -> box ~box p3)

12.3.7 s4 ipc p
> for i := 1 to 6 do
  print(i, ":  ", length(s4_ipc_p(i)), ", ", modaldepth(s4_ipc_p(i)), ", ", vars(s4_ipc_p(i)));
1:  11, 3, [p1]
2:  27, 3, [p1, p2]
3:  49, 3, [p1, p2, p3]
4:  77, 3, [p1, p2, p3, p4]
5:  111, 3, [p1, p2, p3, p4, p5]
6:  151, 3, [p1, p2, p3, p4, p5, p6]
> s4_ipc_p(1);
box (box (box p1 -> box p1) -> false) -> false
> s4_ipc_p(2);
box (box (box p1 -> box p1 & box p2) -> false) & box (box (box p2 -> box p1 & box p2) -> false) -> false

12.3.8 s4 ipc n
> for i := 1 to 6 do
  print(i, ":  ", length(s4_ipc_n(i)), ", ", modaldepth(s4_ipc_n(i)), ", ", vars(s4_ipc_n(i)));
1:  3, 0, []
2:  16, 3, [p1, p2]
3:  35, 3, [p1, p2, p3]
4:  60, 3, [p1, p2, p3, p4]
5:  91, 3, [p1, p2, p3, p4, p5]
6:  128, 3, [p1, p2, p3, p4, p5, p6]
> s4_ipc_n(1);
true -> false
> s4_ipc_n(2);
true & box (box (box p2 -> box p1 & box p2) -> false) -> false

12.3.9 s4 md p

> for i := 1 to 6 do
  print(i, ":  ", length(s4_md_p(i)), ", ", modaldepth(s4_md_p(i)), ", ", vars(s4_md_p(i)));
1:  6, 0, [p1]
2:  38, 3, [p1, p2]
3:  117, 7, [p1, p2]
4:  268, 13, [p1, p2]
5:  518, 21, [p1, p2]
6:  894, 31, [p1, p2]
> s4_md_p(1);
p1 v false v ~p1
> s4_md_p(2);
p1 v (~p1 & dia box (dia p2 v p2) v ~p1 & dia box (dia p1 v p2) v ~p2 & dia box (dia p1 v p2)) v (dia box ~p1 v p2)

12.3.10 s4 md n

> for i := 1 to 6 do
      print(i, ":  ", length(s4_md_n(i)), ", ", modaldepth(s4_md_n(i)), ", ", vars(s4_md_n(i)));
    1:  3, 0, [p1]
    2:  11, 3, [p1, p2]
    3:  34, 7, [p1, p2]
    4:  79, 13, [p1, p2]
    5:  155, 21, [p1, p2]
    6:  271, 31, [p1, p2]
> s4_md_n(1);
    p1 v false
> s4_md_n(2);
    p1 v ~p1 & dia box (dia p1 v p2)

12.3.11 s4 path p
> for i := 1 to 6 do
      print(i, ":  ", length(s4_path_p(i)), ", ", modaldepth(s4_path_p(i)), ", ", vars(s4_path_p(i)));
    1:  56, 2, [p11, p12, p13, p14, p15, p16]
    2:  157, 2, [p11, p12, p13, p14, p15, p16, p21, p22, p23, p24, p25, p26]
    3:  321, 3, [p11, p12, p13, p14, p15, p16, p21, p22, p23, p24, p25, p26, p31, p32, p33, p34, p35, p36]
    4:  448, 4, [p11, p12, p13, p14, p15, p16, p21, p22, p23, p24, p25, p26, p31, p32, p33, p34, p35, p36, p41, p42, p43, p44, p45,
p46]
    5:  650, 5, [p11, p12, p13, p14, p15, p16, p21, p22, p23, p24, p25, p26, p31, p32, p33, p34, p35, p36, p41, p42, p43, p44, p45,
p46, p51, p52, p53, p54, p55, p56]
    6:  803, 6, [p11, p12, p13, p14, p15, p16, p21, p22, p23, p24, p25, p26, p31, p32, p33, p34, p35, p36, p41, p42, p43, p44, p45,
p46, p51, p52, p53, p54, p55, p56, p61, p62, p63, p64, p65, p66]
> s4_path_p(1);
    box box p11 v box box p12 v box box p13 v box box p15 v (false v false v (false v false) v (false v false) v (false v false) v
(false v false) v (false v false)) v dia (dia ~p12 v dia ~p14 v dia ~p12 v dia ~p16)
> s4_path_p(2);
    box box p11 v box box p12 v box box p13 v box box p15 v (dia (~p11 & box p21) v dia (~p11 & box p23) v false v (dia (~p12 & box
p25) v false) v (dia (~p13 & box p21) v dia (~p13 & box p23) v false) v (false v false) v (dia (~p15 & box p21) v dia (~p15 & box p23)
v false) v (false v false) v (false v false) v (false v (dia (~p14 & box p22) v dia (~p16 & box p22))) v (false v false) v (false v
(dia (~p14 & box p24) v dia (~p16 & box p24))) v (false v false) v (false v (dia (~p14 & box p26) v dia (~p16 & box p26)))) v dia (dia
~p22 v dia ~p24 v dia ~p25 v dia ~p26)

12.3.12 s4 path n
> for i := 1 to 6 do
      print(i, ":  ", length(s4_path_n(i)), ", ", modaldepth(s4_path_n(i)), ", ", vars(s4_path_n(i)));
    1:  152, 2, [p11, p12, p13, p14, p15, p16, p21, p22, p23, p24, p25, p26]
    2:  316, 3, [p11, p12, p13, p14, p15, p16, p21, p22, p23, p24, p25, p26, p31, p32, p33, p34, p35, p36]
    3:  440, 4, [p11, p12, p13, p14, p15, p16, p21, p22, p23, p24, p25, p26, p31, p32, p33, p34, p35, p36, p41, p42, p43, p44, p45,
p46]
    4:  642, 5, [p11, p12, p13, p14, p15, p16, p21, p22, p23, p24, p25, p26, p31, p32, p33, p34, p35, p36, p41, p42, p43, p44, p45,
p46, p51, p52, p53, p54, p55, p56]
    5:  796, 6, [p11, p12, p13, p14, p15, p16, p21, p22, p23, p24, p25, p26, p31, p32, p33, p34, p35, p36, p41, p42, p43, p44, p45,
p46, p51, p52, p53, p54, p55, p56, p61, p62, p63, p64, p65, p66]
    6:  1036, 7, [p11, p12, p13, p14, p15, p16, p21, p22, p23, p24, p25, p26, p31, p32, p33, p34, p35, p36, p41, p42, p43, p44, p45,
p46, p51, p52, p53, p54, p55, p56, p61, p62, p63, p64, p65, p66, p71, p72, p73, p74, p75, p76]
> s4_path_n(1);
    box box p11 v box box p12 v box box p13 v box box p15 v (dia (~p11 & box p21) v dia (~p11 & box p23) v false v (false v false)
v (dia (~p13 & box p21) v dia (~p13 & box p23) v false) v (false v false) v (dia (~p15 & box p21) v dia (~p15 & box p23) v false) v
(false v false) v (false v false) v (false v (dia (~p14 & box p22) v dia (~p16 & box p22))) v (false v false) v (false v (dia (~p14
& box p24) v dia (~p16 & box p24))) v (false v false) v (false v (dia (~p14 & box p26) v dia (~p16 & box p26)))) v dia (dia ~p22 v
dia ~p24 v dia ~p25 v dia ~p26)
> s4_path_n(2);
    box box p11 v box box p12 v box box p13 v box box p15 v (dia (~p11 & box p21) v dia (~p11 & box p23) v false v (false v false)
v (dia (~p13 & box p21) v dia (~p13 & box p23) v false) v (false v false) v (dia (~p15 & box p21) v dia (~p15 & box p23) v false) v
(false v false) v (dia dia (~p21 & box p31) v dia dia (~p21 & box p33) v dia dia (~p21 & box p35) v false) v (false v (dia (~p14 &
box p22) v dia (~p16 & box p22))) v (dia dia (~p23 & box p31) v dia dia (~p23 & box p33) v dia dia (~p23 & box p35) v false) v (false
v (dia (~p14 & box p24) v dia (~p16 & box p24))) v (dia dia (~p25 & box p31) v dia dia (~p25 & box p33) v dia dia (~p25 & box p32)
v dia dia (~p25 & box p35) v false) v (false v (dia (~p14 & box p26) v dia (~p16 & box p26))) v (false v false) v (false v (dia dia
(~p22 & box p32) v dia dia (~p24 & box p32) v dia dia (~p26 & box p32))) v (false v false) v (false v (dia dia (~p22 & box p34) v dia
dia (~p24 & box p34) v dia dia (~p26 & box p34))) v (false v false) v (false v (dia dia (~p22 & box p36) v dia dia (~p24 & box p36)
v dia dia (~p26 & box p36)))) v dia (dia ~p32 v dia ~p34 v dia ~p32 v dia ~p36)

12.3.13 s4 ph p

> for i := 1 to 6 do
  print(i, ":  ", length(s4_ph_p(i)), ", ", modaldepth(s4_ph_p(i)), ", ", vars(s4_ph_p(i)));
1:  9, 2, [p101, p201]
2:  45, 3, [p101, p102, p201, p202, p301, p302]
3:  126, 3, [p101, p102, p103, p201, p202, p203, p301, p302, p303, p401, p402, p403]
4:  270, 3, [p101, p102, p103, p104, p201, p202, p203, p204, p301, p302, p303, p304, p401, p402, p403, p404, p501, p502, p503,
p504]
5:  495, 3, [p101, p102, p103, p104, p105, p201, p202, p203, p204, p205, p301, p302, p303, p304, p305, p401, p402, p403, p404,
p405, p501, p502, p503, p504, p505, p601, p602, p603, p604, p605]
6:  819, 3, [p101, p102, p103, p104, p105, p106, p201, p202, p203, p204, p205, p206, p301, p302, p303, p304, p305, p306, p401,
p402, p403, p404, p405, p406, p501, p502, p503, p504, p505, p506, p601, p602, p603, p604, p605, p606, p701, p702, p703, p704, p705,
p706]
> s4_ph_p(1);
p101 & p201 -> dia dia (p101 & p201)
> s4_ph_p(2);
(p101 v box p102) & (p201 v p202) & (p301 v p302) -> dia (dia (p101 & p201) v dia (p101 & p301) v dia (p201 & p301) v dia (box
p102 & p202) v dia (box p102 & p302) v dia (p202 & p302))

12.3.14 s4 ph n

> for i := 1 to 6 do
  print(i, ":  ", length(s4_ph_n(i)), ", ", modaldepth(s4_ph_n(i)), ", ", vars(s4_ph_n(i)));
1:  10, 2, [p101, p201]
2:  47, 3, [p101, p102, p201, p202, p301, p302]
3:  129, 3, [p101, p102, p103, p201, p202, p203, p301, p302, p303, p401, p402, p403]
4:  274, 3, [p101, p102, p103, p104, p201, p202, p203, p204, p301, p302, p303, p304, p401, p402, p403, p404, p501, p502, p503,
p504]
5:  500, 3, [p101, p102, p103, p104, p105, p201, p202, p203, p204, p205, p301, p302, p303, p304, p305, p401, p402, p403, p404,
p405, p501, p502, p503, p504, p505, p601, p602, p603, p604, p605]
6:  825, 3, [p101, p102, p103, p104, p105, p106, p201, p202, p203, p204, p205, p206, p301, p302, p303, p304, p305, p306, p401,
p402, p403, p404, p405, p406, p501, p502, p503, p504, p505, p506, p601, p602, p603, p604, p605, p606, p701, p702, p703, p704, p705,
p706]
> s4_ph_n(1);
p101 & p201 -> dia dia (~p101 & p201)
> s4_ph_n(2);
(p101 v box p102) & (p201 v p202) & (p301 v p302) -> dia (dia (p101 & p201) v dia (p101 & p301) v dia (p201 & p301) v dia (box
p102 & ~p202) v dia (box p102 & p302) v dia (~p202 & p302))

12.3.15 s4 s5 p

> for i := 1 to 6 do
  print(i, ":  ", length(s4_s5_p(i)), ", ", modaldepth(s4_s5_p(i)), ", ", vars(s4_s5_p(i)));
1:  30, 3, [p1, p2, p3]
2:  78, 6, [p1, p2, p3, p4, p5, p6]
3:  126, 9, [p1, p2, p3, p4, p5, p6, p7, p8, p9]
4:  174, 12, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12]
5:  222, 15, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15]
6:  270, 18, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18]
> s4_s5_p(1);
box dia (box (p1 <-> p2) v box p3 v (dia (p1 & ~p2 v ~p1 & p2) v box false)) v box (dia p1 -> ~p3)
> s4_s5_p(2);
box dia (box ((p1 <-> p2) v (p2 <-> p3) v (p3 <-> p4) v (p4 <-> p5)) v box p6 v (dia (p1 & ~p2 v ~p1 & p2) v box (dia (p2 & ~p3
v ~p2 & p3) v box (dia (p3 & ~p4 v ~p3 & p4) v box (dia (p4 & ~p5 v ~p4 & p5) v box false))))) v box (dia p1 -> ~p6)

12.3.16 s4 s5 n

> for i := 1 to 6 do
  print(i, ":  ", length(s4_s5_n(i)), ", ", modaldepth(s4_s5_n(i)), ", ", vars(s4_s5_n(i)));
1:  13, 3, [p1, p6]
2:  85, 8, [p1, p2, p3, p4, p5, p6, p7, p12]
3:  157, 14, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p18]
4:  229, 20, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p24]
5:  301, 26, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24, p25,
p30]
6:  373, 32, [p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24, p25,
p26, p27, p28, p29, p30, p31, p36]
> s4_s5_n(1);
box dia (box p6 v false) v box (dia p1 -> ~p6)
> s4_s5_n(2);
box dia (box p12 v (dia (p1 & ~p2 v ~p1 & p2) v box (dia (p2 & ~p3 v ~p2 & p3) v box (dia (p3 & ~p4 v ~p3 & p4) v box (dia (p4
& ~p5 v ~p4 & p5) v box (dia (p5 & ~p6 v ~p5 & p6) v box (dia (p6 & ~p7 v ~p6 & p7) v box false))))))) v box (dia p1 -> ~p12)

12.3.17 s4 t4p p

> for i := 1 to 6 do
      print(i, ":  ", length(s4_t4p_p(i)), ", ", modaldepth(s4_t4p_p(i)), ", ", vars(s4_t4p_p(i)));
    1:  69, 5, [p0, p1, p3, p4]
    2:  127, 7, [p0, p1, p3, p4]
    3:  185, 9, [p0, p1, p3, p4]
    4:  243, 11, [p0, p1, p3, p4]
    5:  301, 13, [p0, p1, p3, p4]
    6:  359, 15, [p0, p1, p3, p4]
> s4_t4p_p(1);
    dia ~(box ~p1 -> box box ~p1) v box dia box p0 v box (~box p1 -> box ~box p1) v (box (dia (p1 & dia ~p1) v p1) & (dia box p1 &
~p1) v dia (dia (dia box dia p0 & p0 & dia (~p0 v box p3)) v dia box (~p0 v box p3))) v dia p4
> s4_t4p_p(2);
    dia ~(box ~p1 -> box box ~p1) v box (dia ~(box ~p1 -> box box ~p1) v box dia box p0 v box (~box p1 -> box ~box p1)) v box (~box
p1 -> box ~box p1) v (box (dia (p1 & dia ~p1) v p1) & (dia box p1 & ~p1) v dia (box (dia (p1 & dia ~p1) v p1) & (dia box p1 & ~p1)
v dia (box (dia (p1 & dia ~p1) v p1) & (dia box p1 & ~p1) v dia (dia (dia box dia p0 & p0 & dia (~p0 v box p3)) v dia box (~p0 v box
p3))))) v dia p4

12.3.18 s4 t4p n

> for i := 1 to 6 do
      print(i, ":  ", length(s4_t4p_n(i)), ", ", modaldepth(s4_t4p_n(i)), ", ", vars(s4_t4p_n(i)));
    1:  108, 7, [p0, p1, p3, p4]
    2:  224, 11, [p0, p1, p3, p4]
    3:  340, 15, [p0, p1, p3, p4]
    4:  456, 19, [p0, p1, p3, p4]
    5:  572, 23, [p0, p1, p3, p4]
    6:  688, 27, [p0, p1, p3, p4]
> s4_t4p_n(1);
    dia ~(box ~p1 -> box box ~p1) v box dia box p0 v box (~box p1 -> box ~box p1) v (box (dia (p1 & dia ~p1) v p1) & (dia box p1 &
~p1) v dia (box (dia (p1 & dia ~p1) v p1) & (dia box p1 & ~p1) v dia (box (dia (p1 & dia ~p1) v p1) & (dia box p1 & ~p1) v dia (box
dia p0 & box (~p0 v box p3) v dia (dia box dia p0 & p0 & dia (~p0 v box p3)))))) v dia p4
> s4_t4p_n(2);
    dia ~(box ~p1 -> box box ~p1) v box (dia ~(box ~p1 -> box box ~p1) v box (dia ~(box ~p1 -> box box ~p1) v box dia box p0 v box
(~box p1 -> box ~box p1)) v box (~box p1 -> box ~box p1)) v box (~box p1 -> box ~box p1) v (box (dia (p1 & dia ~p1) v p1) & (dia box
p1 & ~p1) v dia (box (dia (p1 & dia ~p1) v p1) & (dia box p1 & ~p1) v dia (box (dia (p1 & dia ~p1) v p1) & (dia box p1 & ~p1) v dia
(box (dia (p1 & dia ~p1) v p1) & (dia box p1 & ~p1) v dia (box (dia (p1 & dia ~p1) v p1) & (dia box p1 & ~p1) v dia (box (dia (p1 &
dia ~p1) v p1) & (dia box p1 & ~p1) v dia (box (dia (p1 & dia ~p1) v p1) & (dia box p1 & ~p1) v dia (box dia p0 & box (~p0 v box p3)
v dia (dia box dia p0 & p0 & dia (~p0 v box p3)))))))))) v dia p4

13 Appendix II: LWB programs that generate the formulas

13.1 Preliminary remarks

This appendix contains procedures that generate the formulas. The procedures are implemented in the LWB programming language (cp. LWB home page, item programming language). In order to avoid inconsistencies between the formulas in the sections 6, 7, 8 and the programs in this appendix, we implemented a Perl program that automatically converts the LaTeX definitions into LWB programs. We then compared the results of these generated LWB programs with the results of the LWB programs in this appendix. A typical session where such a procedure is used looks as follows:

 LWB  -  The Logics Workbench  1.0
 type 'help;' for help

> read("k_lin_p.lwb");
k  user
k> provable(k_lin_p(3));
true
k> quit

13.2 fml lib.lwb
# fml_lib.lwb
####################################################################################################
load(k);
####################################################################################################
D     :== box p0 -> dia p0;
D2    :== dia true;
B     :== p0 -> box dia p0;
T     :== box p0 -> p0;
A4    :== box p0 -> box box p0;
A5    :== ~ box p0 -> box ~ box p0;
H     :== box(p0 v p1) & box(box p0 v p1) & box(p0 v box p1) -> box p0 v box p1;
L     :== box(p0 & box p0 -> p1) v box(p1 & box p1 -> p0);
Lplus :== box(box p0 -> p1) v box(box p1 -> p0);
Grz   :== box(box(p0 -> box p0) -> p0) -> p0;
Grz1  :== box(box(p0 -> box p0) -> p0) -> box p0;
Dum   :== box(box(p0 -> box p0) -> p0) -> (dia box p0 -> p0);
Dum1  :== box(box(p0 -> box p0) -> p0) -> (dia box p0 -> box p0);
Dum4  :== box(box(p0 -> box p0) -> p0) -> (dia box p0 -> p0 v box p0);
####################################################################################################
# Puts  n  box  in front of the formula  a .
# If  n  is 0 then  a  is returned.
proc : mbox(n, a)
local i;
begin
  for i := 1 to n do a := box a;
  return a;
end;
####################################################################################################
# Puts  n  dia  in front of the formula  a .
# If  n  is 0 then  a  is returned.
proc : mdia(n, a)
local i;
begin
  for i := 1 to n do a := dia a;
  return a;
end;

####################################################################################################
proc : p(i)
begin
  return symbol("p", i);
end;
####################################################################################################
# Converts the list  l  into a conjunction.
proc : list2conj(l)
local c, i, x;
begin
  if nops(l) = 0 then return true;
  c := l[1]; for i := 2 to nops(l) do c := c & l[i];
  return c;
end;
####################################################################################################
# Converts the list  l  into a disjunction.
proc : list2disj(l)
local d, i, x;
begin
  if nops(l) = 0 then return false;
  d := l[1]; for i := 2 to nops(l) do d := d v l[i];
  return d;
end;
####################################################################################################
####################################################################################################

13.3 K

13.3.1 k branch p.lwb
# k_branch_p.lwb
####################################################################################################
read("fml_lib.lwb");
####################################################################################################
proc : k_branch_p(n)
local b, i, l;
begin
  b := bdepth(n) & det(n) & branching(n);
  l := []; for i := 0 to n do append(l, mbox(i, b));
  return ~(p(100) & ~p(101) & list2conj(l)) v ~mbox(n, p(n div 3 + 1));
end; # k_branch_p
####################################################################################################
proc : bdepth(n)
local c, i;
begin
  c := []; for i := 1 to n + 1 do append(c, p(100 + i) -> p(99 + i));
  return list2conj(c);
end; # bdepth
####################################################################################################
proc : det(n)
local c, i;
begin
  c := [];
  for i := 0 to n do
    append(c, p(100 + i)
              -> ((p(i) -> box(p(100 + i) -> p(i))) & (~p(i) -> box(p(100 + i) -> ~p(i)))));
  return list2conj(c);
end; # det

####################################################################################################
proc : branching(n)
local c, i;
begin
  c := [];
  for i := 0 to n - 1 do
    append(c, p(100 + i) & ~p(101 + i)
              -> (dia(p(101 + i) & ~p(102 + i) & p(i + 1)) & dia(p(101 + i) & ~p(102 + i) & ~p(i + 1))));
  return list2conj(c);
end; # branching
####################################################################################################
####################################################################################################
13.3.2 k branch n
# k_branch_n.lwb
####################################################################################################
read("k_branch_p.lwb");
####################################################################################################
proc : k_branch_n(n)
local b, i, l;
begin
  b := bdepth(n) & det(n) & branching(n);
  l := []; for i := 0 to n do append(l, mbox(i, b));
  return ~(p(100) & ~p(101) & list2conj(l));
end; # k_branch_n
####################################################################################################
####################################################################################################

13.3.3 k d4 p

# k_d4_p.lwb
####################################################################################################
read("fml_lib.lwb");
####################################################################################################
proc : k_d4_p(n)
local i, d;
begin
  d := [];
  for i := 1 to n do
    append(d,
           mbox(n, T) v ~mbox(i, D2) v ~mbox(i, A4)
           v ~mbox(i, A4{dia p0/p0}) v ~mbox(i, B) v ~mbox(i, B{~p0/p0}));
  return k::nnf(list2disj(d));
end; # k_d4_p
####################################################################################################
####################################################################################################

13.3.4 k d4 n

# k_d4_n.lwb
####################################################################################################
read("fml_lib.lwb");
####################################################################################################
proc : k_d4_n(n)
local i, d;
begin
  d := [];

  for i := 1 to n do
    d := concat(d,
                [mbox(n, box p0 v box dia ~p0)
                 v ~mbox(i, D2)
                 v ~mbox(i, A4)
                 v ~mbox(i, A4{dia p0/p0}) v ~mbox(i, D)
                 v ~mbox(i, A4{dia p0 -> p0/p0})
                 v ~mbox(i, A4{box p0 -> p0/p0})]);
  return k::nnf(list2disj(d));
end; # k_d4_n
####################################################################################################
####################################################################################################

13.3.5 k dum p

# k_dum_p.lwb
####################################################################################################
read("fml_lib.lwb");
####################################################################################################
proc : k_dum_p(n)
local c, d1, d2;
begin
  c := A4{box(p0 -> box p0) -> p0 / p0} & box A4 & Dum & Dum{p0 -> box p0 / p0};
  d1 := []; for i := 1 to n div 2 do append(d1, mbox(i, box A4 & Dum));
  d2 := []; for i := n div 2 + 2 to n - 1 do append(d2, mdia(i, ~(box A4 & Dum)));
  return list2conj(d1) & ~ mbox(n div 2 + 1, Dum1) -> mdia(n div 2 + 1, ~c) v list2disj(d2);
end; # k_dum_p
####################################################################################################
####################################################################################################

13.3.6 k dum n

# k_dum_n.lwb
####################################################################################################
read("fml_lib.lwb");
####################################################################################################
proc : k_dum_n(n)
local c, d1, d2, i;
begin
  c := A4{box(p0 -> box p0) -> p0 / p0} & box A4 & Dum4 & Dum4{p0 -> box p0 / p0};
  d1 := []; for i := 1 to n div 2 do append(d1, mbox(i, box A4 & Dum4));
  d2 := []; for i := n div 2 + 2 to n - 1 do append(d2, mdia(i, ~(box A4 & Dum4)));
  return list2conj(d1) & ~ mbox(n + 1, Dum) -> mdia(n + 1, ~c) v list2disj(d2);
end; # k_dum_n
####################################################################################################
####################################################################################################

13.3.7 k grz p

# k_grz_p.lwb
####################################################################################################
read("fml_lib.lwb");
####################################################################################################
proc : k_grz_p(n)
local c, i, d;
begin
  C := box(p2 -> box p2) -> p2;
  d := []; for i := 1 to n - 1 do append(d, l(i));
  return box Grz{p2/p0} & list2conj(d) & Grz{C & A4{C/p0}/p0} -> Grz1{p1/p0} v Grz1{p2/p0} v Grz1{p3/p0};
end; # k_grz_p

####################################################################################################
proc : l(i)
begin
  if i mod 4 = 0 then return Grz{l2(i div 4) / p0};
  if i mod 4 = 1 then return Grz{box l2(i div 4) v p1 / p0};
  if i mod 4 = 2 then return Grz{box l2(i div 4) v p1 v p2 / p0};
  return Grz{box l2(i div 4) v p1 v p2 v p3 / p0};
end; # l
####################################################################################################
proc : l2(i)
begin
  if i = 0 then return false; else return box l2(i - 1) v p1 v p2 v p3 v p4;
end; # l2
####################################################################################################
####################################################################################################

13.3.8 k grz n

# k_grz_n.lwb
####################################################################################################
read("k_grz_p.lwb");
####################################################################################################
proc : k_grz_n(n)
local c, i, d;
begin
  C := box(p2 -> box p2) -> p2;
  d := []; for i := 1 to n - 1 do append(d, l(i));
  return box Grz1{p2/p0} & list2conj(d) & Grz1{C & A4{C/p0}/p0} -> Grz{p1/p0} v Grz{p2/p0} v Grz{p3/p0};
end; # k_grz_n
####################################################################################################
proc : l(i)
begin
  if i mod 4 = 0 then return Grz1{l2(i div 4) / p0};
  if i mod 4 = 1 then return Grz1{box l2(i div 4) v p1 / p0};
  if i mod 4 = 2 then return Grz1{box l2(i div 4) v p1 v p2 / p0};
  return Grz1{box l2(i div 4) v p1 v p2 v p3 / p0};
end; # l
####################################################################################################
####################################################################################################

13.3.9 k lin p

# k_lin_p.lwb
####################################################################################################
read("fml_lib.lwb");
####################################################################################################
proc : k_lin_p(n)
local d1, d2, i, H2;
begin
  H2 := H{p0 & box p0 & p0 -> p1/p0, ~p0 -> ~(box p1 & p1)/p1};
  d1 := []; for i := 1 to n div 3 do append(d1, ~ H2{p(i)/p0, p(i + 1)/p1});
  d2 := []; for i := ((n div 3) + 1) to n do append(d2, ~ H2{p(i)/p0, p(i + 1)/p1});
  return list2disj(d1) v L{p(n)/p0, p(n)/p1} v list2disj(d2);
end; # k_lin_p
####################################################################################################
####################################################################################################

13.3.10 k lin n

# k_lin_n.lwb
####################################################################################################
read("fml_lib.lwb");
####################################################################################################
proc : k_lin_n(n)
local d1, d2, i;
begin
  d1 := [];
  for i := 1 to 2 mult n - 2 do
    append(d1, ~ L{dia p(i)/p0, p(i + 1)/p1} v ~ L{p(i) -> box p(i + 1)/p0, p(i + 1)/p1});
  d2 := [];
  for i := 2 mult n to 4 mult n - 4 do
    append(d2, ~ L{dia p(i)/p0, p(i + 1)/p1} v ~ L{p(i) -> box p(i + 1)/p0, p(i + 1)/p1});
  return list2disj(d1) v Lplus{p(n)/p0, p(n)/p1} v list2disj(d2);
end; # k_lin_n
####################################################################################################
####################################################################################################

13.3.11 k path p

# k_path_p.lwb
####################################################################################################
read("fml_lib.lwb");
####################################################################################################
proc : k_path_p(n)
local d1, d2, d3, i, j;
begin
  d1 := []; foreach i in [1,path_el(1,n),3,5] do append(d1, box p(i));
  d2 := [];
  for i := 1 to n do
    for j := 1 to 6 do
      append(d2, (left_to_right(i, j, n) v right_to_left(i, j, n)));
  d3 := []; foreach i in [2,4,path_el(n,n),6] do append(d3, mdia(n, ~p(i)));
  return list2disj(d1) v list2disj(d2) v list2disj(d3);
end; # k_path_p
####################################################################################################
proc : path_el(level, n)
local x;
begin
  if (level = 1) then return 2;
  if (level > n div 2) then x := path_el(level - 1, n) + 3; else x := path_el(level - 1, n) + 5;
  if (x > 6) then x := x - 6;
  return x;
end; # path_el
####################################################################################################
proc : left_to_right(level, k, n)
local x;
begin
  if level = n then return false;
  if (k mod 2 = 0) and (k <> path_el(level,n)) then return false;
  x := path_el(level + 1, n);
  if (k mod 2 = 0) then return lists2fml(level, k, [x]);
  if (k = path_el(level,n)) then return lists2fml(level, k, [1,3,x,5]);
  return lists2fml(level, k, delete(x, 1, 3, 5));
end; # left_to_right
####################################################################################################
proc : right_to_left(level, k, n)
local x;
begin
  if level = 1 then return false;

  if (k mod 2 = 1) then return false;
  x := path_el(level - 1, n);
  return lists2fml_back(level - 1, k, delete(x, 2, 4, 6));
end; # right_to_left
####################################################################################################
proc : delete(x, y1, y2, y3)
begin
  if x = y1 then return [y2,y3];
  if x = y2 then return [y1,y3];
  if x = y3 then return [y1,y2];
  return [y1,y2,y3];
end; # delete
####################################################################################################
proc : lists2fml(level, k, s)
local d, x;
begin
  d := []; foreach x in s do append(d, mdia(level, ~p(k) & box p(x)));
  return list2disj(d);
end; # lists2fml
####################################################################################################
proc : lists2fml_back(level, k, s)
local d, x;
begin
  d := []; foreach x in s do append(d, mdia(level, ~p(x) & box p(k)));
  return list2disj(d);
end; # lists2fml_back
####################################################################################################
####################################################################################################

13.3.12 k path n

# k_path_p.lwb
####################################################################################################
read("fml_lib.lwb");
####################################################################################################
proc : k_path_p(n)
local d1, d2, d3, i, j;
begin
  d1 := []; foreach i in [1,path_el(1,n),3,5] do append(d1, box p(i));
  d2 := [];
  for i := 1 to n do
    for j := 1 to 6 do
      append(d2, (left_to_right(i, j, n) v right_to_left(i, j, n)));
  d3 := []; foreach i in [2,4,path_el(n,n),6] do append(d3, mdia(n, ~p(i)));
  return list2disj(d1) v list2disj(d2) v list2disj(d3);
end; # k_path_p
####################################################################################################
proc : path_el(level, n)
local x;
begin
  if (level = 1) then return 2;
  if (level > n div 2) then x := path_el(level - 1, n) + 3; else x := path_el(level - 1, n) + 5;
  if (x > 6) then x := x - 6;
  return x;
end; # path_el
####################################################################################################
proc : left_to_right(level, k, n)
local x;
begin
  if level = n then return false;
  if (k mod 2 = 0) and (k <> path_el(level,n)) then return false;

  x := path_el(level + 1, n);
  if (k mod 2 = 0) then return lists2fml(level, k, [x]);
  if (k = path_el(level,n)) then return lists2fml(level, k, [1,3,x,5]);
  return lists2fml(level, k, delete(x, 1, 3, 5));
end; # left_to_right
####################################################################################################
proc : right_to_left(level, k, n)
local x;
begin
  if level = 1 then return false;
  if (k mod 2 = 1) then return false;
  x := path_el(level - 1, n);
  return lists2fml_back(level - 1, k, delete(x, 2, 4, 6));
end; # right_to_left
####################################################################################################
proc : delete(x, y1, y2, y3)
begin
  if x = y1 then return [y2,y3];
  if x = y2 then return [y1,y3];
  if x = y3 then return [y1,y2];
  return [y1,y2,y3];
end; # delete
####################################################################################################
proc : lists2fml(level, k, s)
local d, x;
begin
  d := []; foreach x in s do append(d, mdia(level, ~p(k) & box p(x)));
  return list2disj(d);
end; # lists2fml
####################################################################################################
proc : lists2fml_back(level, k, s)
local d, x;
begin
  d := []; foreach x in s do append(d, mdia(level, ~p(x) & box p(k)));
  return list2disj(d);
end; # lists2fml_back
####################################################################################################
####################################################################################################

13.3.13 k ph p

# k_ph_p.lwb
####################################################################################################
read("fml_lib.lwb");
####################################################################################################
proc : k_ph_p(n)
begin
  return dia left(n) -> dia right(n);
end; # k_ph_p
####################################################################################################
proc : left(n)
local c, d, j, i;
begin
  c := [];
  for i := 1 to n + 1 do
  begin
    d := []; for j := 1 to n do append(d, l(i, j));
    append(c, list2disj(d));
  end;
  return list2conj(c);
end; # left

####################################################################################################
proc : right(n)
local d, j, i1, i2;
begin
  d := [];
  for j := 1 to n do
    for i1 := 1 to n + 1 do
      for i2 := i1 + 1 to n + 1 do
        append(d, l(i1, j) & l(i2, j));
  return list2disj(d);
end; # right
####################################################################################################
proc : l(i, j)
begin
  if i < j then return box p(i mult 100 + j); else return p(i mult 100 + j);
end; # l
####################################################################################################
####################################################################################################

13.3.14 k ph n

# k_ph_n.lwb
####################################################################################################
read("k_ph_p.lwb");
####################################################################################################
proc : k_ph_n(n)
begin
  return dia left(n) -> dia right(n);
end; # k_ph_n
####################################################################################################
proc : right(n)
local d, j, i1, i2;
begin
  d := [];
  for j := 1 to n do
    for i1 := 1 to n + 1 do
      for i2 := i1 + 1 to n + 1 do
        append(d, l2(n, i1, j) & l2(n, i2, j));
  return list2disj(d);
end; # right
####################################################################################################
proc : l2(n, i, j)
begin
  if ( i = j ) and ( i = (2 mult n) div 3 + 1) then return ~l(i, j); else return l(i, j);
end; # l2
####################################################################################################
####################################################################################################

13.3.15 k poly p

# k_poly_p.lwb
####################################################################################################
read("fml_lib.lwb");
####################################################################################################
proc : k_poly_p(n)
begin
  if (n mod 2 = 1) then return poly(3 mult n); else return poly(3 mult n + 1);
end; # k_poly_p
####################################################################################################

proc : poly(n)
local c1, c2, i;
begin
  c1 := []; for i := 1 to n + 1 do append(c1, p(i));
  c2 := []; for i := 1 to n + 1 do append(c2, ~p(2 mult i));
  return mbox(n + 1, list2conj(c1)) v f(n,n) v mbox(n + 1, list2conj(c2));
end; # poly
####################################################################################################
proc : f(i, n)
local a, j;
begin
  if (i = 0) then return false;
  if (i = n) then return dia(f(n - 1, n) v mdia(n, p(n) <-> p(1))) v box p(n + 2);
  return dia(f(i - 1,n) v mdia(i, p(i) <-> p(i + 1))) v box p(i + 2);
end; # f
####################################################################################################
####################################################################################################

13.3.16 k poly n

# k_poly_n.lwb
####################################################################################################
read("k_poly_p.lwb");
####################################################################################################
proc : k_poly_n(n)
begin
  if (n mod 2 = 0) then return poly(3 mult n); else return poly(3 mult n + 1);
end; # k_poly_n
####################################################################################################
####################################################################################################

13.3.17 k t4p p

# k_t4p_p.lwb
####################################################################################################
read("fml_lib.lwb");
####################################################################################################
proc : k_t4p_p(n)
begin
  return E(n) v nnf(~C(n)) v dia p4;
end; # k_t4p_p
####################################################################################################
proc : C(i)
begin
  if i = 0
  then return ((box dia p0 -> dia p1)
               & box(box ~ box dia p1 -> ~ box dia p0)
               & (box dia p0 -> box box dia p1)
               & box(dia box dia p0 & p0 -> box p1)
               & box dia p1){p0 & dia ~p3/p1};
  return box A4{p1/p0} & box C(i - 1) & box A4{dia p1/p0};
end; # C
####################################################################################################
proc : E(i)
begin
  if i = 0 then return dia box p0;
  return dia ~ A4{~p1/p0} v box E(i - 1) v box A5{p1/p0};
end; # E

####################################################################################################
####################################################################################################

13.3.18 k t4p n

# k_t4p_n.lwb
####################################################################################################
read("k_t4p_p.lwb");
####################################################################################################
proc : k_t4p_n(n)
begin
  return E(2 mult n - 1) v nnf(~C(2 mult n - 1)) v dia p4;
end; # k_t4p_n
####################################################################################################
proc : C(i)
begin
  if i = 0
  then return ((box dia p0 -> dia p1)
               & box(box ~ box dia p1 -> ~ box dia p0)
               & (box dia p0 -> box box dia p1)
               & box(dia box dia p0 & p0 -> box p1)){p0 & dia ~p3/p1};
  return box A4{p1/p0} & box C(i - 1) & box A4{dia p1/p0};
end; # C
####################################################################################################
####################################################################################################

13.4 KT

13.4.1 kt 45 p

# kt_45_p.lwb
####################################################################################################
read("fml_lib.lwb");
####################################################################################################
proc : kt_45_p(n)
local i, d;
begin
  d := [];
  for i := 1 to n do
    append(d, mbox(n, A4) v ~mbox(i, D2)
              v ~mbox(i, A5{dia ~p0/p0}) v ~mbox(i, box A5) v ~mbox(i, B));
  return k::nnf(list2disj(d));
end; # kt_45_p
####################################################################################################
####################################################################################################

13.4.2 kt 45 n

# kt_45_n.lwb
####################################################################################################
read("fml_lib.lwb");
####################################################################################################
proc : kt_45_n(n)
local i, d;
begin
  d := [];
  for i := 1 to n do

    append(d, mbox(n, box p0 v box dia ~p0) v ~mbox(i, A4)
              v ~mbox(i, A4{dia p0/p0}) v ~mbox(i, T)
              v ~mbox(i, A4{dia p0 -> p0/p0})
              v ~mbox(i, A4{box p0 -> p0/p0}));
  return k::nnf(list2disj(d));
end; # kt_45_n
####################################################################################################
####################################################################################################
13.4.3 kt branch p
# kt_branch_p.lwb
####################################################################################################
read("k_branch_p.lwb");
####################################################################################################
proc : kt_branch_p(n)
begin
  return ~(p(100) & ~p(101) & mbox(n, bdepth(n) & det(n) & branching(n))) v ~mbox(n, p(n div 3 + 1));
end; # kt_branch_p
####################################################################################################
####################################################################################################
13.4.4 kt branch n
# kt_branch_n.lwb
####################################################################################################
read("k_branch_p.lwb");
####################################################################################################
proc : kt_branch_n(n)
begin
  return ~(p(100) & ~p(101) & mbox(n, bdepth(n) & det(n) & branching(n)));
end; # kt_branch_n
####################################################################################################
####################################################################################################
13.4.5 kt dum p
# kt_dum_p.lwb
####################################################################################################
read("fml_lib.lwb");
####################################################################################################
proc : kt_dum_p(n)
local c, d1, d2;
begin
  c := A4{box(p0 -> box p0) -> p0 / p0} & box A4 & Dum & Dum{p0 -> box p0 / p0};
  d1 := []; for i := 1 to n div 2 do append(d1, mbox(i, A4));
  d2 := []; for i := n div 2 + 2 to n - 1 do append(d2, mdia(i, ~A4));
  return list2conj(d1) & ~ mbox(n div 2 + 1, Dum1) -> mdia(n div 2 + 1, ~c) v list2disj(d2);
end; # kt_dum_p
####################################################################################################
####################################################################################################
13.4.6 kt dum n
# kt_dum_n.lwb
####################################################################################################
read("fml_lib.lwb");

####################################################################################################
proc : kt_dum_n(n)
local c, d1, d2, i;
begin
  c := A4{box(p0 -> box p0) -> p0 / p0} & box A4 & Dum & Dum{p0 -> box p0 / p0};
  d1 := []; for i := 1 to n div 2 do append(d1, mbox(i, box A4 & Dum));
  d2 := []; for i := n div 2 + 2 to n - 1 do append(d2, mdia(i, ~(box A4 & Dum)));
  return list2conj(d1) & ~ mbox(n div 2 + 1, Grz) -> mdia(n div 2 + 1, ~c) v list2disj(d2);
end; # kt_dum_n
####################################################################################################
####################################################################################################
13.4.7 kt grz p
# kt_grz_p.lwb
####################################################################################################
read("k_grz_p.lwb");
####################################################################################################
proc : kt_grz_p(n)
local a, i, d;
begin
  C := box(p2 -> box p2) -> p2;
  d := []; for i := 1 to n - 1 do append(d, l(i));
  return box Grz{p2/p0} & list2conj(d) & Grz{C & A4{C/p0}/p0}
         -> Grz1{p1/p0} v Grz1{p2/p0} & dia box ~p0 v Grz1{p3/p0} v Grz1{p2/p0} & dia p0;
end; # kt_grz_p
####################################################################################################
####################################################################################################
13.4.8 kt grz n
# kt_grz_n.lwb
####################################################################################################
read("kt_grz_p.lwb");
####################################################################################################
proc : kt_grz_n(n)
local c, i, d;
begin
  C := box(p2 -> box p2) -> p2;
  d := []; for i := 1 to n - 1 do append(d, l(i));
  return box Grz1{p2/p0} & list2conj(d) & Grz1{C & A4{C/p0}/p0} -> A5{p1/p0} v A5{p2/p0} v A5{p3/p0};
end; # kt_grz_n
####################################################################################################
proc : l(i)
begin
  if i mod 4 = 0 then return Grz1{l2(i div 4) / p0};
  if i mod 4 = 1 then return Grz1{box l2(i div 4) v p1 / p0};
  if i mod 4 = 2 then return Grz1{box l2(i div 4) v p1 v p2 / p0};
  return Grz1{box l2(i div 4) v p1 v p2 v p3 / p0};
end; # l
####################################################################################################
####################################################################################################

13.4.9 kt md p

# kt_md_p.lwb
####################################################################################################
read("fml_lib.lwb");
####################################################################################################

proc : kt_md_p(n)
local d, i;
begin
  d := [];
  for i := 1 to n - 1 do
    append(d, g(i, n, ~p1 & dia f(1, n, p2))
              v g(i, n, ~p1 & dia f(1, n, p1))
              v g(i, n, ~p2 & dia f(1, n, p1)));
  return p1 v list2disj(d) v g(n, n, ~p1);
end; # kt_md_p
####################################################################################################
proc : g(i, n, a)
local j;
begin
  if i = 1 then return a;
  return f(i, n, g(i - 1, n, a));
end; # g
####################################################################################################
proc : f(i, n, a)
local j;
begin
  return mdia(i - 1, box mdia(n - i, a));
end; # f
####################################################################################################
####################################################################################################

13.4.10 kt md n

# kt_md_n.lwb
####################################################################################################
read("kt_md_p.lwb");
####################################################################################################
proc : kt_md_n(n)
local d, i;
begin
  d := []; for i := 1 to n - 1 do append(d, g(i, n, ~p1 & dia f(1, n, p1)));
return p1 v list2disj(d);
end; # kt_md_n
####################################################################################################
####################################################################################################
13.4.11 kt path p
# kt_path_p.lwb
####################################################################################################
read("k_path_p.lwb");
####################################################################################################
proc : kt_path_p(n)
local d1, d2, d3, i, j;
begin
  d1 := []; foreach i in [1,path_el(1,n),3,5] do append(d1, box p(10 + i));
  d2 := [];
  for i := 1 to n do
    for j := 1 to 6 do
      append(d2, (left_to_right(i, j, n) v right_to_left(i, j, n)));
  d3 := []; foreach i in [2,4,path_el(n,n),6] do append(d3, mdia(n, ~p(10 mult n + i)));
  return list2disj(d1) v list2disj(d2) v list2disj(d3);
end; # kt_path_p

proc : lists2fml(level, k, s)
local d, x;
begin
  d := [];
  foreach x in s do append(d, mdia(level, ~p(10 mult level + k) & box p(10 mult (level + 1) + x)));
  return list2disj(d);
end; # lists2fml
####################################################################################################
proc : lists2fml_back(level, k, s)
local d, x;
begin
  d := [];
  foreach x in s do append(d, mdia(level, ~p(10 mult level + x) & box p(10 mult (level + 1) + k)));
  return list2disj(d);
end; # lists2fml_back
####################################################################################################
####################################################################################################

13.4.12 kt path n
# kt_path_n.lwb
####################################################################################################
read("k_path_n.lwb");
####################################################################################################
proc : kt_path_n(n)
local d1, d2, d3, i, j;
begin
  d1 := []; foreach i in [1,path_el(1,n+1),3,5] do append(d1, box p(10 + i));
  d2 := [];
  for i := 1 to n + 1 do
    for j := 1 to 6 do
      append(d2, (left_to_right(i, j, n + 1) v right_to_left(i, j, n + 1)));
  d3 := [];
  foreach i in [2,4,path_el(n+1,n+1),6] do append(d3, mdia(n + 1, ~p(10 mult (n + 1) + i)));
  return list2disj(d1) v list2disj(d2) v list2disj(d3);
end; # kt_path_n
####################################################################################################
proc : lists2fml(level, k, s)
local d, x;
begin
  d := [];
  foreach x in s do append(d, mdia(level, ~p(10 mult level + k) & box p(10 mult (level + 1) + x)));
  return list2disj(d);
end; # lists2fml
####################################################################################################
proc : lists2fml_back(level, k, s)
local d, x;
begin
  d := [];
  foreach x in s do append(d, mdia(level, ~p(10 mult level + x) & box p(10 mult (level + 1) + k)));
  return list2disj(d);
end; # lists2fml_back
####################################################################################################
####################################################################################################

13.4.13 kt ph p

# kt_ph_p.lwb

####################################################################################################
read("k_ph_p.lwb");
####################################################################################################
proc : kt_ph_p(n)
begin
  return left(n) -> dia right(n);
end; # kt_ph_p
####################################################################################################
####################################################################################################

13.4.14 kt ph n

# kt_ph_n.lwb
####################################################################################################
read("k_ph_n.lwb");
####################################################################################################
proc : kt_ph_n(n)
begin
  return left(n) -> dia right(n);
end; # kt_ph_n
####################################################################################################
####################################################################################################
13.4.15 kt poly p
# kt_poly_p.lwb
####################################################################################################
read("k_poly_p.lwb");
####################################################################################################
proc : kt_poly_p(n)
begin
  if (n mod 2 = 1) then return poly(5 mult n); else return poly(5 mult n + 1);
end; # kt_poly_p
####################################################################################################
proc : f(i, n)
local a, j;
begin
  if (i = 0) then return false;
  if (i = n) then return dia(f(n - 1, n) v mdia(n + 2, p(n) <-> p(1))) v box p(n + 2);
  return dia(f(i - 1,n) v mdia(i + 2, p(i) <-> p(i + 1))) v box p(i + 2);
end; # f
####################################################################################################
####################################################################################################
13.4.16 kt poly n
# kt_poly_n.lwb
####################################################################################################
read("kt_poly_p.lwb");
####################################################################################################
proc : kt_poly_n(n)
begin
  if (n mod 2 = 0) then return poly(3 mult n); else return poly(3 mult n + 1);
end; # kt_poly_n
####################################################################################################
####################################################################################################

13.4.17 kt t4p p

# kt_t4p_p.lwb
####################################################################################################
read("k_t4p_p.lwb");
####################################################################################################
proc : kt_t4p_p(n)
begin
  return E(n) v nnf(~C(n)) v dia p4;
end; # kt_t4p_p
####################################################################################################
proc : C(i)
begin
  if i = 0
  then return ((box dia p0 -> box box dia p1)
               & box(dia box dia p0 & p0 -> box p1)
               & box dia p1){p0 & dia ~p3/p1};
  return box A4{p1/p0} & box C(i - 1);
end; # C
####################################################################################################
####################################################################################################

13.4.18 kt t4p n

# kt_t4p_n.lwb
####################################################################################################
read("kt_t4p_p.lwb");
####################################################################################################
proc : kt_t4p_n(n)
begin
  return E(2 mult n - 1) v nnf(~C(2 mult n - 1)) v dia p4;
end; # kt_t4p_n
####################################################################################################
proc : C(i)
begin
  if i = 0
  then return ((box dia p0 -> dia p1)
               & (box dia p0 -> box box dia p1)
               & box(dia box dia p0 & p0 -> box p1)){p0 & dia ~p3/p1};
  return box A4{p1/p0} & box C(i - 1);
end; # C
####################################################################################################
####################################################################################################

13.5 S4

13.5.1 s4 45 p

# s4_45_p.lwb
####################################################################################################
read("fml_lib.lwb");
####################################################################################################
proc : s4_45_p(n)
local i, d;
begin
  d := [];
  for i := 1 to n do
    append(d, h(n, A5) v ~h(i, D2) v ~h(i, A5{dia ~p0/p0}) v ~h(i, box A5) v ~h(i, B));
  return k::nnf(list2disj(d));
end; # s4_45_p

####################################################################################################
proc : h(i, a)
begin
  if i = 0 then return a; else return box p0 v box h(i - 1, a) v box p1;
end;
####################################################################################################
####################################################################################################

13.5.2 s4 45 n

# s4_45_n.lwb
####################################################################################################
read("s4_45_p.lwb");
####################################################################################################
proc : s4_45_n(n)
local i, d;
begin
  d := [];
  for i := 1 to n do
    append(d, h(n, box p0 v box dia ~p0) v ~h(i, A4)
              v ~h(i, A4{dia p0/p0}) v ~h(i, T)
              v ~h(i, A4{box p0 -> p0/p0})
              v ~h(i, T{box p0 -> p0/p0}));
  return k::nnf(list2disj(d));
end; # s4_45_n
####################################################################################################
####################################################################################################
13.5.3 s4 branch p
# s4_branch_p.lwb
####################################################################################################
read("k_branch_p.lwb");
####################################################################################################
proc : s4_branch_p(n)
begin
  return ~(p(100) & ~p(101) & box(bdepth(n) & det(n) & branching(n))) v ~box p(n div 3 + 1);
end; # s4_branch_p
####################################################################################################
####################################################################################################
13.5.4 s4 branch n
# s4_branch_n.lwb
####################################################################################################
read("k_branch_p.lwb");
####################################################################################################
proc : s4_branch_n(n)
begin
  return ~(p(100) & ~p(101) & box(bdepth(n) & det(n) & branching(n)));
end; # s4_branch_n
####################################################################################################
####################################################################################################
13.5.5 s4 grz p
# s4_grz_p.lwb

####################################################################################################
read("k_grz_p.lwb");
####################################################################################################
proc : s4_grz_p(n)
local a, C, i, d1;
begin
  C := box(p2 -> box p2) -> p2;
  d1 := []; for i := 1 to n - 1 do append(d1, l(i));
  return box Grz{p2/p0} & list2conj(d1) & Grz{C & A4{C/p0}/p0}
         -> Grz1{p1/p0} v Grz1{p2/p0} & ~ box dia p0 v Grz1{p3/p0} v Grz1{p2/p0} & ~ dia ~(box dia p0 v p1);
end; # s4_grz_p
####################################################################################################
####################################################################################################
13.5.6 s4 grz n
# s4_grz_n.lwb
####################################################################################################
read("s4_grz_p.lwb");
####################################################################################################
proc : s4_grz_n(n)
local C, i, d;
begin
  C := box(p2 -> box p2) -> p2;
  d := []; for i := 1 to n - 1 do append(d, l(i));
  return box Grz1{p2/p0} & list2conj(d) & Grz1{C & A4{C/p0}/p0} -> A5{p1/p0} v A5{p2/p0} v A5{p3/p0};
end; # s4_grz_n
####################################################################################################
proc : l(i)
begin
  if i mod 4 = 0 then return Grz1{l2(i div 4) / p0};
  if i mod 4 = 1 then return Grz1{box l2(i div 4) v p1 / p0};
  if i mod 4 = 2 then return Grz1{box l2(i div 4) v p1 v p2 / p0};
  return Grz1{box l2(i div 4) v p1 v p2 v p3 / p0};
end; # l
####################################################################################################
####################################################################################################
13.5.7 s4 ipc p
# s4_ipc_p.lwb
####################################################################################################
read("fml_lib.lwb");
####################################################################################################
proc : s4_ipc_p(n)
local c, i;
begin
  c := []; for i := 1 to n do append(c, f(i, n));
  return list2conj(c) -> false;
end; # s4_ipc_p
####################################################################################################
proc : f(i, n)
local c, j;
begin
  c := []; for j := 1 to n do append(c, box p(j));
  return box(box(box p(i) -> list2conj(c)) -> false);
end; # f

13.5.8 s4 ipc n
# s4_ipc_n.lwb
####################################################################################################
read("fml_lib.lwb");
####################################################################################################
proc : s4_ipc_n(n)
local c, i;
begin
  c := []; for i := 1 to n do append(c, f2(i, n));
  return list2conj(c) -> false;
end; # s4_ipc_n
####################################################################################################
proc : f2(i, n)
begin
  if i = (n + 1) div 2 then return true; else return f(i, n);
end; # f2
####################################################################################################
proc : f(i, n)
local c, j;
begin
  c := []; for j := 1 to n do append(c, box p(j));
  return box(box(box p(i) -> list2conj(c)) -> false);
end; # f
####################################################################################################
####################################################################################################

13.5.9 s4 md p

# s4_md_p.lwb
####################################################################################################
read("kt_md_p.lwb");
####################################################################################################
proc : s4_md_p(n)
local d, i;
begin
  d := [];
  for i := 1 to n - 1 do
    append(d, g(i, n, ~p1 & dia f(1, n, p2))
              v g(i, n, ~p1 & dia f(1, n, p1))
              v g(i, n, ~p2 & dia f(1, n, p1)));
  return p1 v list2disj(d) v g(n, n, ~p1);
end; # s4_md_p
####################################################################################################
proc : f(i, n, a)
local j;
begin
  return h(i - 1, box h(n - i, a));
end; # f
####################################################################################################
proc : h(i, a)
local j;
begin
  if i = 0 then return a; else return dia h(i - 1, a) v p2;
end; # h

13.5.10 s4 md n

# s4_md_n.lwb
####################################################################################################
read("s4_md_p.lwb");
####################################################################################################
proc : s4_md_n(n)
local d, i;
begin
  d := []; for i := 1 to n - 1 do append(d, g(i, n, ~p1 & dia f(1, n, p1)));
  return p1 v list2disj(d);
end; # s4_md_n
####################################################################################################
####################################################################################################

13.5.11 s4 path p
# s4_path_p.lwb
####################################################################################################
read("kt_path_p.lwb");
####################################################################################################
proc : s4_path_p(n)
local d1, d2, d3, i, j;
begin
  d1 := []; foreach i in [1,path_el(1,n),3,5] do append(d1, box box p(10 + i));
  d2 := [];
  for i := 1 to n do
    for j := 1 to 6 do
      append(d2, (left_to_right(i, j, n) v right_to_left(i, j, n)));
  d3 := []; foreach i in [2,4,path_el(n,n),6] do append(d3, dia ~p(10 mult n + i));
  return list2disj(d1) v list2disj(d2) v dia list2disj(d3);
end; # s4_path_p
####################################################################################################
####################################################################################################

13.5.12 s4 path n
# s4_path_n.lwb
####################################################################################################
read("kt_path_n.lwb");
####################################################################################################
proc : s4_path_n(n)
local d1, d2, d3, i, j;
begin
  d1 := []; foreach i in [1,path_el(1,n+1),3,5] do append(d1, box box p(10 + i));
  d2 := [];
  for i := 1 to n + 1 do
    for j := 1 to 6 do
      append(d2, (left_to_right(i, j, n + 1) v right_to_left(i, j, n + 1)));
  d3 := []; foreach i in [2,4,path_el(n+1,n+1),6] do append(d3, dia ~p(10 mult (n + 1) + i));
  return list2disj(d1) v list2disj(d2) v dia list2disj(d3);
end; # s4_path_n
####################################################################################################
####################################################################################################

13.5.13 s4 ph p

# s4_ph_p.lwb
####################################################################################################
read("k_ph_p.lwb");
####################################################################################################
proc : s4_ph_p(n)
begin
  return left(n) -> dia right(n);
end; # s4_ph_p
####################################################################################################
proc : right(n)
local d, j, i1, i2;
begin
  d := [];
  for j := 1 to n do
    for i1 := 1 to n + 1 do
      for i2 := i1 + 1 to n + 1 do
        append(d, dia(l(i1, j) & l(i2, j)));
  return list2disj(d);
end; # right
####################################################################################################
####################################################################################################

13.5.14 s4 ph n

# s4_ph_n.lwb
####################################################################################################
read("s4_ph_p.lwb");
####################################################################################################
proc : s4_ph_n(n)
begin
return left(n) -> dia right(n);
end; # s4_ph_n
####################################################################################################
proc : right(n)
local d, j, i1, i2;
begin
d := [];
for j := 1 to n do
  for i1 := 1 to n + 1 do
    for i2 := i1 + 1 to n + 1 do
      append(d, dia(l2(n, i1, j) & l2(n, i2, j)));
return list2disj(d);
end; # right
####################################################################################################
proc : l2(n, i, j)
begin
if ( i = j ) and ( i = (2 mult n) div 3 + 1)
then return ~l(i, j);
else return l(i, j);
end; # l2
####################################################################################################
####################################################################################################

13.5.15 s4 s5 p

# s4_s5_p.lwb
####################################################################################################
read("fml_lib.lwb");
####################################################################################################
proc : s4_s5_p(n)
local d, i;
begin
  d := []; for i := 1 to 3 mult n - 2 do append(d, p(i) <-> p(i + 1));
  return box dia(box list2disj(d) v box p(3 mult n) v f(1, 3 mult n - 1)) v box(dia p1 -> ~p(3 mult n));
end; # s4_s5_p
####################################################################################################
proc : f(i, n)
begin
  if i = n then return false; else return dia(p(i) & ~p(i + 1) v ~p(i) & p(i + 1)) v box f(i + 1, n);
end;
####################################################################################################
####################################################################################################

13.5.16 s4 s5 n

# s4_s5_n.lwb
####################################################################################################
read("s4_s5_p.lwb");
####################################################################################################
proc : s4_s5_n(n)
begin
return box dia(box p(6 mult n) v f(1, 6 mult n - 5)) v box(dia p1 -> ~p(6 mult n));
end; # s4_s5_n
####################################################################################################
####################################################################################################

13.5.17 s4 t4p p

# s4_t4p_p.lwb
####################################################################################################
read("k_t4p_p.lwb");
####################################################################################################
proc : s4_t4p_p(n)
begin
  return E(n) v nnf(~C(2 mult n - 1)) v dia p4;
end; # s4_t4p_p
####################################################################################################
proc : C(i)
begin
  if i = 0 then return (box(dia box dia p0 & p0 -> box p1) & box dia p1){p0 & dia ~p3/p1};
  return Dum{p1/p0} & box C(i - 1);
end; # C
####################################################################################################
####################################################################################################

13.5.18 s4 t4p n

# s4_t4p_n.lwb

####################################################################################################
read("s4_t4p_p.lwb");
####################################################################################################
proc : s4_t4p_n(n)
begin
  return E(2 mult n - 1) v nnf(~C(4 mult n - 1)) v dia p4;
end; # s4_t4p_n
####################################################################################################
proc : C(i)
begin
  if i = 0 then return ((box dia p0 -> dia p1) & box(dia box dia p0 & p0 -> box p1)){p0 & dia ~p3/p1};
  return Dum{p1/p0} & box C(i - 1);
end; # C
####################################################################################################
####################################################################################################