Note: The Metamath Solitaire applet can be found at http://metamath.org This file contains proofs of all 193 theorems of propositional calculus in Whitehead and Russell's _Principia Mathematica_, directly from axioms ax-1, ax-2, ax-3, and ax-mp in the Metamath Solitaire applet. These are the shortest direct proofs I could find. If you find a shorter one, let me know at nm (at) alum (dot) mit (dot) edu. In these proofs, the resulting theorem is in a form which has all abbreviations expanded, so instead of "(~ P v P)" for theorem *2.1 you will see "(~ ~ P -> P)" or in Metamath Solitaire's ASCII notation, "(-. -. P -> P)". To get "(~ P v P)" we would apply the definition of logical OR, which is shown in the applet using: Select Logic Family -> Propositional Calculus + Definitions -> Axioms -> df-or. If we wanted we could extend the proof to apply the definition directly in the proof, but that is somewhat tedious and was not our purpose here. In addition, sometimes "more general" theorems are proved. For example, the proof of theorem *1.6 actually proves "((P -> Q) -> ((R -> P) -> (R -> Q)))" in the applet. We obtain theorem *1.6 by substituting "-. R" for "R", then applying the definition of logical OR. The notation for proofs is as follows. For theorem *1.6, for example, the proof shown is "DD2D121". To enter this into the applet, you enter the steps in _reverse_ order i.e. "121D2DD". The character mapping is as follows: "1" is ax-1, "2" is ax-2, "3" is ax-3, and "D" is ax-mp. Thus this proof would be entered into the applet as: ax-1 ax-2 ax-1 ax-mp ax-2 ax-mp ax-mp As a historical note, the notation in "DD2D121" is called "condensed detachment" and expresses the proof in Polish notation. It was invented by logician C. A. Meredith in the 1950's. For more information on this notation you can reference the article "A Finitely Axiomatized Formalization of Predicate Calculus with Equality" linked to from the Metamath Home Page. The Appendix in that article shows how to write a very simple program for verifying these proofs. For longer proofs such a program is much more convenient than repeated clicks on the applet. (If this interests you, I have a C program, drule.c, that implements the algorithm. However it is a personal ad-hoc working tool not intended for general release. If you want a copy to extract the algorithm contact me.) --- Proofs of propositional calculus theorems from _Principia Mathematica_ --- ((P v P) -> P); ! *1.2 Taut DD2DD2D13D2DD2D1311; ! 19 steps (Q -> (P v Q)); ! *1.3 Add 1; ! 1 step ((P v Q) -> (Q v P)); ! *1.4 DD2D13D2D1D3DD2DD2D13DD2D1311; ! 29 steps ((P v (Q v R)) -> (Q v (P v R))); ! *1.5 Assoc DD2D1DD22D11DD2D112; ! 19 steps ((Q -> R) -> ((P v Q) -> (P v R))); ! *1.6 Sum DD2D121; ! 7 steps ((P -> ~ P) -> ~ P); ! *2.01 DD2D1DD2DD2D13D2DD2D1311DD2D1DD22D2DD2D13DD2D1311; ! 49 steps (Q -> (P -> Q)); ! *2.02 Simp 1; ! 1 step ((P -> ~ Q) -> (Q -> ~ P)); ! *2.03 DD2D13DD2D1DD22D2DD2D13DD2D1311; ! 31 steps ((P -> (Q -> R)) -> (Q -> (P -> R))); ! *2.04 Comm DD2D1DD22D11DD2D112; ! 19 steps ((Q -> R) -> ((P -> Q) -> (P -> R))); ! *2.05 Syll DD2D121; ! 7 steps ((P -> Q) -> ((Q -> R) -> (P -> R))); ! *2.06 Syll DD2D1D2DD2D1211; ! 15 steps (P -> (P v P)); ! *2.07 1; ! 1 step (P -> P); ! *2.08 Id DD211; ! 5 steps (~ P v P); ! *2.1 DD2DD2D13DD2D1311; ! 17 steps (P v ~ P); ! *2.11 DD211; ! 5 steps (P -> ~ ~ P); ! *2.12 D3DD2DD2D13DD2D1311; ! 19 steps (P v ~ ~ ~ P); ! *2.13 D3DD2DD2D13DD2D1311; ! 19 steps (~ ~ P -> P); ! *2.14 DD2DD2D13DD2D1311; ! 17 steps ((~ P -> Q) -> (~ Q -> P)); ! *2.15 Transp DD2D13D2D1D3DD2DD2D13DD2D1311; ! 29 steps ((P -> Q) -> (~ Q -> ~ P)); ! *2.16 DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D131 1; ! 59 steps ((~ Q -> ~ P) -> (P -> Q)); ! *2.17 Transp 3; ! 1 step ((~ P -> P) -> P); ! *2.18 DD2DD2D13D2DD2D1311; ! 19 steps (P -> (P v Q)); ! *2.2 DD2D1D2DD2D1311; ! 15 steps (~ P -> (P -> Q)); ! *2.21 DD2D131; ! 7 steps (P -> (~ P -> Q)); ! *2.24 DD2D1D2DD2D1311; ! 15 steps (P v ((P v Q) -> Q)); ! *2.25 DD2D1D2DD2111; ! 13 steps (~ P v ((P -> Q) -> Q)); ! *2.26 DD2D1DD2D1D2DD2111DD2DD2D13DD2D1311; ! 35 steps (P -> ((P -> Q) -> Q)); ! *2.27 DD2D1D2DD2111; ! 13 steps ((P v (Q v R)) -> (P v (R v Q))); ! *2.3 D2D1DD2D13D2D1D3DD2DD2D13DD2D1311; ! 33 steps ((P v (Q v R)) -> ((P v Q) v R)); ! *2.31 DD2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D1DD2D1DD22D11DD2D112D2D1DD2D13D 2D1D3DD2DD2D13DD2D1311; ! 91 steps (((P v Q) v R) -> (P v (Q v R))); ! *2.32 DD2D1D2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D1DD2D1DD22D11DD2D112DD2D13D 2D1D3DD2DD2D13DD2D1311; ! 91 steps ((Q -> R) -> ((~ P -> Q) -> (~ R -> P))); ! *2.36 DD2D1D2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D121; ! 45 steps ((Q -> R) -> ((~ Q -> P) -> (~ P -> R))); ! *2.37 DD2D1DD2DD2D121D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D121; ! 53 steps ((Q -> R) -> ((~ Q -> P) -> (~ R -> P))); ! *2.38 DD2D1DD2D1D2DD2D1211DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D 13DD2D1311; ! 79 steps ((P v (P v Q)) -> (P v Q)); ! *2.4 DD22D21; ! 7 steps ((Q v (P v Q)) -> (P v Q)); ! *2.41 DD2D1D2D1DD2DD2D13D2DD2D1311DD2D1DD22D11DD2D112; ! 47 steps ((~ P v (P -> Q)) -> (P -> Q)); ! *2.42 DD2D1DD22D21DD2DD2D121D1D3DD2DD2D13DD2D1311; ! 43 steps ((P -> (P -> Q)) -> (P -> Q)); ! *2.43 DD22D21; ! 7 steps (~ (P v Q) -> ~ P); ! *2.45 D3DD2D1D3DD2DD2D13DD2D1311DD2D131; ! 33 steps (~ (P v Q) -> ~ Q); ! *2.46 D3DD2D1D3DD2DD2D13DD2D1311DD2D13DD2D131; ! 39 steps (~ (P v Q) -> (~ P v Q)); ! *2.47 DD2D1D2DD2D1D2DD2D131DD2D11DD2D1311; ! 35 steps (~ (P v Q) -> (P v ~ Q)); ! *2.48 DD2D11D3DD2D1D3DD2DD2D13DD2D1311DD2D13DD2D131; ! 45 steps (~ (P v Q) -> (~ P v ~ Q)); ! *2.49 DD2D1D2DD2D1D2DD2D131DD2D11DD2D1311; ! 35 steps (~ (P -> Q) -> (~ P -> Q)); ! *2.5 DD2D1D2DD2D1D2DD2D131DD2D11DD2D1311; ! 35 steps (~ (P -> Q) -> (P -> ~ Q)); ! *2.51 DD2D11D3DD2D1D3DD2DD2D13DD2D1311DD2D13DD2D131; ! 45 steps (~ (P -> Q) -> (~ P -> ~ Q)); ! *2.52 DD2D1D2DD2D1D2DD2D131DD2D11DD2D1311; ! 35 steps (~ (P -> Q) -> (Q -> P)); ! *2.521 DD2D1D2DD2D1D2DD2D131DD2D1111; ! 29 steps ((P v Q) -> (~ P -> Q)); ! *2.53 DD211; ! 5 steps ((~ P -> Q) -> (P v Q)); ! *2.54 DD211; ! 5 steps (~ P -> ((P v Q) -> Q)); ! *2.55 DD2D1D2DD2111; ! 13 steps (~ Q -> ((P v Q) -> P)); ! *2.56 DD2D1D2DD2D13D2D1D3DD2DD2D13DD2D13111; ! 37 steps ((~ P -> Q) -> ((P -> Q) -> Q)); ! *2.6 DD2D1D2DD2D1D2D1DD2DD2D13D2DD2D1311DD2D1DD2DD2D121D1DD2D13D2D1D3DD2DD 2D13DD2D1311DD2D1211; ! 89 steps ((P -> Q) -> ((~ P -> Q) -> Q)); ! *2.61 DD2D1D2D1DD2DD2D13D2DD2D1311DD2D1DD2DD2D121D1DD2D13D2D1D3DD2DD2D13DD2 D1311DD2D121; ! 81 steps ((P v Q) -> ((P -> Q) -> Q)); ! *2.62 DD2D1D2DD2D1D2D1DD2DD2D13D2DD2D1311DD2D1DD2DD2D121D1DD2D13D2D1D3DD2DD 2D13DD2D1311DD2D1211; ! 89 steps ((P -> Q) -> ((P v Q) -> Q)); ! *2.621 DD2D1D2D1DD2DD2D13D2DD2D1311DD2D1DD2DD2D121D1DD2D13D2D1D3DD2DD2D13DD2 D1311DD2D121; ! 81 steps ((P v Q) -> ((~ P v Q) -> Q)); ! *2.63 DD2D1D2D1DD2DD2D13D2DD2D1311DD2D1DD2DD2D121D1DD2D13D2D1D3DD2DD2D13DD2 D1311DD2D121; ! 81 steps ((P v Q) -> ((P v ~ Q) -> P)); ! *2.64 DD2D1DD2DD2D121D13DD2D1D2D1DD2DD2D13D2DD2D1311DD2D1D2DD2D121 1; ! 61 steps ((P -> Q) -> ((P -> ~ Q) -> ~ P)); ! *2.65 DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2DD2D13DD2D1D2DD2DD2D13DD2D1311 1; ! 69 steps (((P v Q) -> Q) -> (P -> Q)); ! *2.67 DD2DD2D121D1DD2D1D2DD2D1311; ! 27 steps (((P -> Q) -> Q) -> (P v Q)); ! *2.68 DD2DD2D121D1DD2D131; ! 19 steps (((P -> Q) -> Q) -> ((Q -> P) -> P)); ! *2.69 DD2D1DD2D1D2D1DD2DD2D13D2DD2D1311DD2D1D2DD2D1211DD2DD2D121D1DD2D13 1; ! 67 steps ((P -> Q) -> (((P v Q) v R) -> (Q v R))); ! *2.73 DD2D1DD2D1D2DD2D1211DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD 2DD2D13DD2D1311DD2D1D2D1DD2DD2D13D2DD2D1311DD2D1DD2DD2D121D1DD2D13D2D 1D3DD2DD2D13DD2D1311DD2D121; ! 165 steps ((Q -> P) -> (((P v Q) v R) -> (P v R))); ! *2.74 DD2D1DD2D1D2DD2D1211DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD 2DD2D13DD2D1311DD2D1D2D1DD2DD2D13D2DD2D1311DD2D121; ! 119 steps ((P v Q) -> ((P v (Q -> R)) -> (P v R))); ! *2.75 DD2D1D221; ! 9 steps ((P v (Q -> R)) -> ((P v Q) -> (P v R))); ! *2.76 2; ! 1 step ((P -> (Q -> R)) -> ((P -> Q) -> (P -> R))); ! *2.77 2; ! 1 step ((Q v R) -> ((~ R v S) -> (Q v S))); ! *2.8 DD2D1DD2DD2D121D1DD2DD2D121D1D3DD2DD2D13DD2D1311DD2D1D2DD2D121 1; ! 63 steps ((Q -> (R -> S)) -> ((P v Q) -> ((P v R) -> (P v S)))); ! *2.81 DD2D1D2D12DD2D121; ! 17 steps (((P v Q) v R) -> (((P v ~ R) v S) -> ((P v Q) v S))); ! *2.82 DD2D1DD2D1D2DD2D1211D2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111D3DD2D1D3DD 2DD2D13DD2D1311DD2D131; ! 91 steps ((P -> (Q -> R)) -> ((P -> (R -> S)) -> (P -> (Q -> S)))); ! *2.83 DD2D12D2D1DD2D1D2DD2D1211; ! 25 steps (((P v Q) -> (P v R)) -> (P v (Q -> R))); ! *2.85 DD2D1D2D1DD2DD2D121D11DD2D1DD22D11DD2D112; ! 41 steps (((P -> Q) -> (P -> R)) -> (P -> (Q -> R))); ! *2.86 DD2D1D2D1DD2DD2D121D11DD2D1DD22D11DD2D112; ! 41 steps ((P ^ Q) -> ~ (~ P v ~ Q)); ! *3.1 D3DD2D1D3DD2DD2D13DD2D1311DD2D1DD2DD2D121D1D3DD2DD2D13DD2D1311DD2DD2D 13DD2D1311; ! 79 steps (~ (~ P v ~ Q) -> (P ^ Q)); ! *3.11 D3DD2D1D3DD2DD2D13DD2D1311DD2D1DD2D1DD22D2DD2D13DD2D1311DD2DD2D13DD2D 1311; ! 73 steps ((~ P v ~ Q) v (P ^ Q)); ! *3.12 D3DD2D1D3DD2DD2D13DD2D1311DD2D1DD2D1DD22D2DD2D13DD2D1311DD2DD2D13DD2D 1311; ! 73 steps (~ (P ^ Q) -> (~ P v ~ Q)); ! *3.13 DD2D1DD2D1DD22D2DD2D13DD2D1311DD2DD2D13DD2D1311; ! 47 steps ((~ P v ~ Q) -> ~ (P ^ Q)); ! *3.14 DD2D1D3DD2DD2D13DD2D1311DD2DD2D121D1D3DD2DD2D13DD2D1311; ! 55 steps (P -> (Q -> (P ^ Q))); ! *3.2 DD2D13DD2D1D2DD2DD2D13DD2D13111; ! 31 steps (Q -> (P -> (P ^ Q))); ! *3.21 DD2D1D2DD2D13DD2D1D2DD2DD2D13DD2D131111; ! 39 steps ((P ^ Q) -> (Q ^ P)); ! *3.22 D3DD2D1D3DD2DD2D13DD2D1311DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311DD2DD2D 13DD2D1311; ! 79 steps ~ (P ^ ~ P); ! *3.24 DD3DD2DD2D13DD2D1311D3DD2DD2D13DD2D1311; ! 39 steps ((P ^ Q) -> P); ! *3.26 Simp D3DD2D1D3DD2DD2D13DD2D1311DD2D131; ! 33 steps ((P ^ Q) -> Q); ! *3.27 Simp D3DD2D1D3DD2DD2D13DD2D13111; ! 27 steps (((P ^ Q) -> R) -> (P -> (Q -> R))); ! *3.3 Exp DD2D1D2D13DD2D1DD2D1DD22D11DD2D112DD2D13D2D1D3DD2DD2D13DD2D131 1; ! 63 steps ((P -> (Q -> R)) -> ((P ^ Q) -> R)); ! *3.31 Imp DD2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D1DD2D1DD22D11DD2D112D2D1DD2D1DD 2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311; ! 121 steps (((P -> Q) ^ (Q -> R)) -> (P -> R)); ! *3.33 Syll D3DD2D1D3DD2DD2D13DD2D1311DD2D1D2DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2 D1311D2D1D3DD2DD2D13DD2D1311DD2D1D2DD2D12111; ! 113 steps (((Q -> R) ^ (P -> Q)) -> (P -> R)); ! *3.34 Syll D3DD2D1D3DD2DD2D13DD2D1311DD2D1D2DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2 D1311D2D1D3DD2DD2D13DD2D1311DD2D1211; ! 105 steps ((P ^ (P -> Q)) -> Q); ! *3.35 Ass D3DD2D1D3DD2DD2D13DD2D1311DD2D1D2DD2D13DD2D1D2D1D3DD2DD2D13DD2D1311DD 2D1D2DD2DD2D13DD2D131111; ! 93 steps (((P ^ Q) -> R) -> ((P ^ ~ R) -> ~ Q)); ! *3.37 Transp DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311DD2D1 DD2D1DD2D1DD2D1DD22D11DD2D112D2D1DD2D1D2D1D3DD2DD2D13DD2D13113DD2D1DD 22D11DD2D112DD2D13D2D1D3DD2DD2D13DD2D1311; ! 179 steps ((P ^ Q) -> (P -> Q)); ! *3.4 DD2D11D3DD2D1D3DD2DD2D13DD2D13111; ! 33 steps ((P -> R) -> ((P ^ Q) -> R)); ! *3.41 DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D1311DD2D131; ! 45 steps ((Q -> R) -> ((P ^ Q) -> R)); ! *3.42 DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D13111; ! 39 steps (((P -> Q) ^ (P -> R)) -> (P -> (Q ^ R))); ! *3.43 Comp D3DD2D1D3DD2DD2D13DD2D1311DDD22D11D1D2DD2D1DD2D13D2D1D3DD2DD2D13DD2D1 311DD2D1DD2D1DD22D2DD2D13DD2D1311DD2D12D2D1DD2D13DD2D1D2DD2DD2D13DD2D 13111; ! 143 steps (((Q -> P) ^ (R -> P)) -> ((Q v R) -> P)); ! *3.44 DD2D13DD2DD2D1DD2D12D2D1DD2D13DD2D1D2D1D3DD2DD2D13DD2D1311DD2D1D2DD2D D2D13DD2D13111DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D1 3DD2D1311D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2D1DD2D1DD2D13DD2D1DD22D2 DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D1311 1; ! 271 steps ((P -> Q) -> ((P ^ R) -> (Q ^ R))); ! *3.45 Fact DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311DD2D1 D2DD2D1211; ! 79 steps (((P -> R) ^ (Q -> S)) -> ((P ^ Q) -> (R ^ S))); ! *3.47 DD2DD2D1DD2D12D2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1DD2DD2D121D1D3D D2D1D3DD2DD2D13DD2D1311DD2D131D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2D1D D2DD2D121D1D3DD2D1D3DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13DD2D1311 1; ! 203 steps (((P -> R) ^ (Q -> S)) -> ((P v Q) -> (R v S))); ! *3.48 DD2D1D2DD2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D1DD2D1DD22D11DD2D112DD2D 1D2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311DD2D1 DD2DD2D121D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D13 11DD2D1D2D1D2DD2D121DD2D1D2D11DD2D1211; ! 245 steps ((P -> Q) <-> (~ Q -> ~ P)); ! *4.1 DD3DD2DD2DD2D13DD2D1311D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD 2DD2D13DD2D13113; ! 85 steps ((P <-> Q) <-> (~ P <-> ~ Q)); ! *4.11 DD3DD2DD2DD2D13DD2D1311D1DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1 DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311D3DD2D1D3D D2DD2D13DD2D13111DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD 2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2DD2D1DD2D13DD2D1D2DD2 DD2D13DD2D13111DD2D13D3DD2D1D3DD2DD2D13DD2D13111DD2D13D3DD2D1D3DD2DD2 D13DD2D1311DD2D131; ! 363 steps ((P <-> ~ Q) <-> (Q <-> ~ P)); ! *4.12 DD3DD2DD2DD2D13DD2D1311D1DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1 DD2D13DD2D1DD22D2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2D1 DD2D13D2D1D3DD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D13111DD2DD2D1DD2D1 3DD2D1D2DD2DD2D13DD2D13111DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D3DD2D1 D3DD2DD2D13DD2D1311DD2D131DD2D1DD2D13D2D1D3DD2DD2D13DD2D1311D3DD2D1D3 DD2DD2D13DD2D13111; ! 363 steps (P <-> ~ ~ P); ! *4.13 DD3DD2DD2DD2D13DD2D1311D1D3DD2DD2D13DD2D1311DD2DD2D13DD2D131 1; ! 61 steps (((P ^ Q) -> R) <-> ((P ^ ~ R) -> ~ Q)); ! *4.14 DD3DD2DD2DD2D13DD2D1311D1DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D 1D3DD2DD2D13DD2D1311DD2D1DD2D1DD2D1DD2D1DD22D11DD2D112D2D1DD2D1D2D1D3 DD2DD2D13DD2D13113DD2D1DD22D11DD2D112DD2D13D2D1D3DD2DD2D13DD2D1311DD2 D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D1DD2D1DD22D11DD2D112DD2D1D2D13DD2D 1DD2D1DD22D11DD2D112DD2D13D2D1D3DD2DD2D13DD2D1311; ! 325 steps (((P ^ Q) -> ~ R) <-> ((Q ^ R) -> ~ P)); ! *4.15 DD3DD2DD2DD2D13DD2D1311D1DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D 1D3DD2DD2D13DD2D1311DD2D1D2D13DD2D1DD2D1DD22D11DD2D112DD2D13D2D1D3DD2 DD2D13DD2D1311DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D1 3DD2D1311DD2D1DD2D1DD22D11DD2D112DD2D1D2D1DD2D13DD2D1DD22D2DD2D13DD2D 13113; ! 281 steps (P <-> P); ! *4.2 DD3DD2DD2DD2D13DD2D1311D1DD211DD211; ! 35 steps ((P <-> Q) <-> (Q <-> P)); ! *4.21 DD3DD2DD2DD2D13DD2D1311D1D3DD2D1D3DD2DD2D13DD2D1311DD2D1DD2D13DD2D1DD 22D2DD2D13DD2D1311DD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D1311DD2D1DD2 D13DD2D1DD22D2DD2D13DD2D1311DD2DD2D13DD2D1311; ! 183 steps (((P <-> Q) ^ (Q <-> R)) -> (P <-> R)); ! *4.22 DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2DD2D1DD2D121DD2D1D3DD2D1D3D D2DD2D13DD2D1311DD2D131D3DD2D1D3DD2DD2D13DD2D13111DD2D1D3DD2D1D3DD2DD 2D13DD2D1311DD2D131D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2DD2D1DD2D121DD 2D1D3DD2D1D3DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2D1D 3DD2D1D3DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13DD2D13111; ! 329 steps (P <-> (P ^ P)); ! *4.24 DD3DD2DD2DD2D13DD2D1311D1DDD22D21DD2D13DD2D1D2DD2DD2D13DD2D13111D3DD2 D1D3DD2DD2D13DD2D13111; ! 91 steps (P <-> (P v P)); ! *4.25 DD3DD2DD2DD2D13DD2D1311D11DD2DD2D13D2DD2D1311; ! 45 steps ((P ^ Q) <-> (Q ^ P)); ! *4.3 DD3DD2DD2DD2D13DD2D1311D1D3DD2D1D3DD2DD2D13DD2D1311DD2D1DD2D13DD2D1DD 22D2DD2D13DD2D1311DD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D1311DD2D1DD2 D13DD2D1DD22D2DD2D13DD2D1311DD2DD2D13DD2D1311; ! 183 steps ((P v Q) <-> (Q v P)); ! *4.31 DD3DD2DD2DD2D13DD2D1311D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D13D2D1D3DD2 DD2D13DD2D1311; ! 83 steps (((P ^ Q) ^ R) <-> (P ^ (Q ^ R))); ! *4.32 DD3DD2DD2DD2D13DD2D1311D1D3DD2D1D3DD2DD2D13DD2D1311DD2D1DD2D1DD2D1DD2 D13D2D1D3DD2DD2D13DD2D1311DD2D1DD2D1DD22D11DD2D112D2D1DD2D1DD2D13DD2D 1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311D2D1DD2DD2D13DD2D1311DD2D D2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D1311DD2D1DD2D1D2D1D3DD2DD2D13DD2D1 311DD2D1D2D13DD2D1DD2D1DD22D11DD2D112DD2D13D2D1D3DD2DD2D13DD2D1311DD2 DD2D13DD2D1311; ! 359 steps (((P v Q) v R) <-> (P v (Q v R))); ! *4.33 DD3DD2DD2DD2D13DD2D1311D1DD2D1D2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D1D D2D1DD22D11DD2D112DD2D13D2D1D3DD2DD2D13DD2D1311DD2D1DD2D13D2D1D3DD2DD 2D13DD2D1311DD2D1DD2D1DD22D11DD2D112D2D1DD2D13D2D1D3DD2DD2D13DD2D131 1; ! 207 steps ((P <-> Q) -> ((P ^ R) <-> (Q ^ R))); ! *4.36 D3DDD22D2DD2D13DD2D131D1DD2D1D3DD2DD2D13DD2D1311DDDD2DD2D12DD2D1D2D12 DD2D11DD2D11DD2D121D1DD2D1D2DD2D1211D3DDD22D2DD2D13DD2D131D1DD2D1D3DD 2DD2D13DD2D1311DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D 13DD2D1311DD2D1D2DD2D1211DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D 1D3DD2DD2D13DD2D1311DD2D1D2DD2D1211; ! 311 steps ((P <-> Q) -> ((P v R) <-> (Q v R))); ! *4.37 D3DDD22D2DD2D13DD2D131D1DD2D1D3DD2DD2D13DD2D1311DDDD2DD2D12DD2D1D2D12 DD2D11DD2D11DD2D121D1DD2D1D2DD2D1211D3DDD22D2DD2D13DD2D131D1DD2D1D3DD 2DD2D13DD2D1311DD2D1DD2D1D2DD2D1211DD2D1DD2D13DD2D1DD22D2DD2D13DD2D13 11D2D1D3DD2DD2D13DD2D1311DD2D1DD2D1D2DD2D1211DD2D1DD2D13DD2D1DD22D2DD 2D13DD2D1311D2D1D3DD2DD2D13DD2D1311; ! 311 steps (((P <-> R) ^ (Q <-> S)) -> ((P ^ Q) <-> (R ^ S))); ! *4.38 DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2DD2D1DD2D12D2D1DD2D13DD2D1D 2DD2DD2D13DD2D13111DD2D1DD2D1DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D1311DD 2D131D3DD2D1D3DD2DD2D13DD2D1311DD2D131D3DD2D1D3DD2DD2D13DD2D1311DD2D1 31DD2D1DD2D1DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13 DD2D1311DD2D131D3DD2D1D3DD2DD2D13DD2D13111DD2DD2D1DD2D12D2D1DD2D13DD2 D1D2DD2DD2D13DD2D13111DD2D1DD2D1DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D131 1DD2D131D3DD2D1D3DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13DD2D1311DD2D131D D2D1DD2D1DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13DD2 D13111D3DD2D1D3DD2DD2D13DD2D13111; ! 585 steps (((P <-> R) ^ (Q <-> S)) -> ((P v Q) <-> (R v S))); ! *4.39 DD2D1D3DD2D1D3DD2DD2D13DD2D1311DD2D1DDDD2DD2D12DD2D1D2D12DD2D11DD2D11 DD2D121D1DD2D1D2DD2D1211D3DD2D1D3DD2DD2D13DD2D1311DD2D1DD2D1D2DD2D1DD 2D13D2D1D3DD2DD2D13DD2D1311DD2D1DD2D1DD22D11DD2D112DD2D1D2D1DD2D1DD2D 13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311DD2D1DD2DD2D121D1DD 2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311DD2D1D2D1D2D D2D121DD2D1D2D11DD2D1211DD2DD2D13DD2D1311DD2D1D2DD2D1DD2D13D2D1D3DD2D D2D13DD2D1311DD2D1DD2D1DD22D11DD2D112DD2D1D2D1DD2D1DD2D13DD2D1DD22D2D D2D13DD2D1311D2D1D3DD2DD2D13DD2D1311DD2D1DD2DD2D121D1DD2D1DD2D13DD2D1 DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311DD2D1D2D1D2DD2D121DD2D1D2D 11DD2D1211DD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D1311DD2D1DD2D1DD2D1D D2D1D2D1D3DD2DD2D13DD2D13113D2D1D3DD2DD2D13DD2D1311DD2D1DD2D1DD2D1DD2 D1DD22D11DD2D112DD2D1DD2D1D2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D 1D3DD2DD2D13DD2D1311D2D1DD2D1DD22D11DD2D112D2D13DD2D1DD22D11DD2D1123D D2DD2D13DD2D1311; ! 913 steps ((P ^ (Q v R)) <-> ((P ^ Q) v (P ^ R))); ! *4.4 DD3DD2DD2DD2D13DD2D1311D1DDD22D11D1D2DD2D1DD2D1DD2D13DD2D1DD22D2DD2D1 3DD2D1311D2D1D3DD2DD2D13DD2D1311DD2D1DD2D12D2D1DD2D13DD2D1D2D1D3DD2DD 2D13DD2D1311DD2D1D2DD2DD2D13DD2D13111DD2DD2D13DD2D1311D3DD2D1DD2DD2D1 DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1D3DD2DD2D13DD2D1311D2D1D3DD2D1D3D D2DD2D13DD2D1311DD2D131D2D1D3DD2D1D3DD2DD2D13DD2D1311DD2D13DD2D131DD2 DD2D13DD2D1311; ! 359 steps ((P v (Q ^ R)) <-> ((P v Q) ^ (P v R))); ! *4.41 DD3DD2DD2DD2D13DD2D1311D1DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111D2D1D 3DD2D1D3DD2DD2D13DD2D1311DD2D131D2D1D3DD2D1D3DD2DD2D13DD2D13111D3DD2D 1D3DD2DD2D13DD2D1311DDD22D11D1D2DD2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2 D1DD2D1DD22D2DD2D13DD2D1311DD2D12D2D1DD2D13DD2D1D2DD2DD2D13DD2D1311 1; ! 275 steps (P <-> ((P ^ Q) v (P ^ ~ Q))); ! *4.42 DD3DD2DD2DD2D13DD2D1311D1DD2D1DD2D1DD22D2DD2D13DD2D1311DD2D1D2D2DD2D1 3DD2D1D2DD2DD2D13DD2D131111D3DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111D D2D1D3DD2DD2D13DD2D1311DD2D131DD2D131; ! 175 steps (P <-> ((P v Q) ^ (P v ~ Q))); ! *4.43 DD3DD2DD2DD2D13DD2D1311D1DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1 D2DD2D1311DD2D1D2DD2D1311D3DD2D1D3DD2DD2D13DD2D1311DD2D1D2D2DD2D13DD2 D1D2DD2DD2D13DD2D131111; ! 161 steps (P <-> (P v (P ^ Q))); ! *4.44 DD3DD2DD2DD2D13DD2D1311D1DD2D1D2DD2D1311DD2DD2D13D2DD2D1D2DD2D131DD2D 11DD2D1313; ! 79 steps (P <-> (P ^ (P v Q))); ! *4.45 DD3DD2DD2DD2D13DD2D1311D1D3DD2D1DD2D1DD2D1DD2DD2D13D2DD2D1311DD2DD2D1 21D1DD2D131DD2D13DD2D1DD22D2DD2D13DD2D1311DD2DD2D13DD2D1311D3DD2D1D3D D2DD2D13DD2D1311DD2D131; ! 161 steps ((P ^ Q) <-> ~ (~ P v ~ Q)); ! *4.5 DD3DD2DD2DD2D13DD2D1311D1D3DD2D1D3DD2DD2D13DD2D1311DD2D1DD2DD2D121D1D 3DD2DD2D13DD2D1311DD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D1311DD2D1DD2 D1DD22D2DD2D13DD2D1311DD2DD2D13DD2D1311; ! 177 steps (~ (P ^ Q) <-> (~ P v ~ Q)); ! *4.51 DD3DD2DD2DD2D13DD2D1311D1DD2D1DD2D1DD22D2DD2D13DD2D1311DD2DD2D13DD2D1 311DD2D1D3DD2DD2D13DD2D1311DD2DD2D121D1D3DD2DD2D13DD2D131 1; ! 127 steps ((P ^ ~ Q) <-> ~ (~ P v Q)); ! *4.52 DD3DD2DD2DD2D13DD2D1311D1D3DD2D1D3DD2DD2D13DD2D1311DD2D1DD2D1D2D1D3DD 2DD2D13DD2D1311DD2DD2D121D1D3DD2DD2D13DD2D1311DD2DD2D13DD2D1311D3DD2D 1D3DD2DD2D13DD2D1311DD2D1DD2D1D2D1DD2DD2D13DD2D1311DD2D1DD22D2DD2D13D D2D1311DD2DD2D13DD2D1311; ! 231 steps (~ (P ^ ~ Q) <-> (~ P v Q)); ! *4.53 DD3DD2DD2DD2D13DD2D1311D1DD2D1DD2D1D2D1DD2DD2D13DD2D1311DD2D1DD22D2DD 2D13DD2D1311DD2DD2D13DD2D1311DD2D1DD2D1D3DD2DD2D13DD2D1311D2D1D3DD2DD 2D13DD2D1311DD2DD2D121D1D3DD2DD2D13DD2D1311; ! 181 steps ((~ P ^ Q) <-> ~ (P v ~ Q)); ! *4.54 DD3DD2DD2DD2D13DD2D1311D1DD211DD211; ! 35 steps (~ (~ P ^ Q) <-> (P v ~ Q)); ! *4.55 DD3DD2DD2DD2D13DD2D1311D1DD2DD2D13DD2D1311D3DD2DD2D13DD2D131 1; ! 61 steps ((~ P ^ ~ Q) <-> ~ (P v Q)); ! *4.56 DD3DD2DD2DD2D13DD2D1311D1D3DD2D1D3DD2DD2D13DD2D1311DD2D1D2D1D3DD2DD2D 13DD2D1311DD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D1311DD2D1D2D1DD2DD2D 13DD2D1311DD2DD2D13DD2D1311; ! 165 steps (~ (~ P ^ ~ Q) <-> (P v Q)); ! *4.57 DD3DD2DD2DD2D13DD2D1311D1DD2D1D2D1DD2DD2D13DD2D1311DD2DD2D13DD2D1311D D2D1D3DD2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311; ! 115 steps ((P -> Q) <-> (~ P v Q)); ! *4.6 DD3DD2DD2DD2D13DD2D1311D1DD2D1DD22D2DD2D13DD2D1311DD2DD2D121D1D3DD2DD 2D13DD2D1311; ! 81 steps (~ (P -> Q) <-> (P ^ ~ Q)); ! *4.61 DD3DD2DD2DD2D13DD2D1311D1D3DD2D1D3DD2DD2D13DD2D1311DD2D1D2D1DD2DD2D13 DD2D1311DD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D1311DD2D1D2D1D3DD2DD2D 13DD2D1311DD2DD2D13DD2D1311; ! 165 steps ((P -> ~ Q) <-> (~ P v ~ Q)); ! *4.62 DD3DD2DD2DD2D13DD2D1311D1DD2D1DD22D2DD2D13DD2D1311DD2DD2D121D1D3DD2DD 2D13DD2D1311; ! 81 steps (~ (P -> ~ Q) <-> (P ^ Q)); ! *4.63 DD3DD2DD2DD2D13DD2D1311D1DD211DD211; ! 35 steps ((~ P -> Q) <-> (P v Q)); ! *4.64 DD3DD2DD2DD2D13DD2D1311D1DD211DD211; ! 35 steps (~ (~ P -> Q) <-> (~ P ^ ~ Q)); ! *4.65 DD3DD2DD2DD2D13DD2D1311D1D3DD2D1D3DD2DD2D13DD2D1311DD2D1D2D1DD2DD2D13 DD2D1311DD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D1311DD2D1D2D1D3DD2DD2D 13DD2D1311DD2DD2D13DD2D1311; ! 165 steps ((~ P -> ~ Q) <-> (P v ~ Q)); ! *4.66 DD3DD2DD2DD2D13DD2D1311D1DD211DD211; ! 35 steps (~ (~ P -> ~ Q) <-> (~ P ^ Q)); ! *4.67 DD3DD2DD2DD2D13DD2D1311D1DD211DD211; ! 35 steps ((P -> Q) <-> (P -> (P ^ Q))); ! *4.7 DD3DD2DD2DD2D13DD2D1311D1D2DD2D13DD2D1D2DD2DD2D13DD2D13111D2D1D3DD2D1 D3DD2DD2D13DD2D13111; ! 89 steps ((P -> Q) <-> (P <-> (P ^ Q))); ! *4.71 DD3DD2DD2DD2D13DD2D1311D1DD2D1DD2DD2D13DD2D1D2DD2DD2D13DD2D13111D1D3D D2D1D3DD2DD2D13DD2D1311DD2D131D2DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1D 2D1D3DD2D1D3DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13DD2D1311DD2D13 1; ! 201 steps ((P -> Q) <-> (Q <-> (P v Q))); ! *4.72 DD3DD2DD2DD2D13DD2D1311D1DD2D1D3DD2DD2DD2D13DD2D1311D11DD2D1D2D1DD2DD 2D13D2DD2D1311DD2D1DD2DD2D121D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D121DD 2D1DD2DD2D121D1DD2D1D2DD2D1311D3DD2D1D3DD2DD2D13DD2D1311 1; ! 195 steps (Q -> (P <-> (P ^ Q))); ! *4.73 DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1D2DD2D13DD2D1D2DD2DD2D13D D2D131111D1D3DD2D1D3DD2DD2D13DD2D1311DD2D131; ! 113 steps (~ P -> (Q <-> (P v Q))); ! *4.74 DD2D1D3DD2DD2DD2D13DD2D1311D11DD2D1D2DD2111; ! 43 steps (((P -> Q) ^ (P -> R)) <-> (P -> (Q ^ R))); ! *4.76 DD3DD2DD2DD2D13DD2D1311D1D3DD2D1D3DD2DD2D13DD2D1311DDD22D11D1D2DD2D1D D2D13D2D1D3DD2DD2D13DD2D1311DD2D1DD2D1DD22D2DD2D13DD2D1311DD2D12D2D1D D2D13DD2D1D2DD2DD2D13DD2D13111DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111 D2D1D3DD2D1D3DD2DD2D13DD2D1311DD2D131D2D1D3DD2D1D3DD2DD2D13DD2D1311 1; ! 275 steps (((Q -> P) ^ (R -> P)) <-> ((Q v R) -> P)); ! *4.77 DD3DD2DD2DD2D13DD2D1311D1DD2D13DD2DD2D1DD2D12D2D1DD2D13DD2D1D2D1D3DD2 DD2D13DD2D1311DD2D1D2DD2DD2D13DD2D13111DD2D1DD2D1DD2D13DD2D1DD22D2DD2 D13DD2D1311D2D1D3DD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD 2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311D3DD2D1 D3DD2DD2D13DD2D13111DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2DD2D121 D1DD2D1D2DD2D1311DD2DD2D121D11; ! 375 steps (((P -> Q) v (P -> R)) <-> (P -> (Q v R))); ! *4.78 DD3DD2DD2DD2D13DD2D1311D1DD2D1DD2D1D2D1DD2DD2D121D11DD2D1DD22D11DD2D1 12DD2D1DD2D1DD22D11DD2D112DD2D1DD2D1DD2D1D2D13DD2D1DD2D1DD22D11DD2D11 2DD2D1D2D1DD2D1D2DD2D13DD2D1D2DD2DD2D13DD2D13111DD22D21DD2D1DD22D11DD 2D112D2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D1DD22D11DD2D112DD2D1DD2DD2D 121D1DD2D11D3DD2D1D3DD2DD2D13DD2D1311DD2D13DD2D1312; ! 327 steps (((Q -> P) v (R -> P)) <-> ((Q ^ R) -> P)); ! *4.79 DD3DD2DD2DD2D13DD2D1311D1DD2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D1DD2D1 D2D1DD2DD2D121D11DD2D1DD22D11DD2D112DD2D1D2D1DD2D1DD2D13DD2D1DD22D2DD 2D13DD2D1311D2D1D3DD2DD2D13DD2D1311DD2D1DD2D1DD22D11DD2D112DD2D1DD2D1 DD2D1D2D13D2D1DD2D1D2DD2D13DD2D1D2D1D3DD2DD2D13DD2D1311DD2D1D2DD2DD2D 13DD2D13111DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD 2D1311DD2D1D2D1DD2DD2D13D2DD2D1311DD2D1DD22D11DD2D112D2D1DD2D13DD2D1D 2DD2D131D2D11DD2D1DD22D11DD2D112DD2D1DD2D1DD2D1DD2DD2D121D1DD2D11D3DD 2D1D3DD2DD2D13DD2D1311DD2D131D2D132DD2D13D2D1D3DD2DD2D13DD2D131 1; ! 547 steps ((P -> ~ P) <-> ~ P); ! *4.8 DD3DD2DD2DD2D13DD2D1311D1DD2D1DD2DD2D13D2DD2D1311DD2D1DD22D2DD2D13DD2 D13111; ! 75 steps ((~ P -> P) <-> P); ! *4.81 DD3DD2DD2DD2D13DD2D1311D1DD2DD2D13D2DD2D13111; ! 45 steps (((P -> Q) ^ (P -> ~ Q)) <-> ~ P); ! *4.82 DD3DD2DD2DD2D13DD2D1311D1D3DD2D1D3DD2DD2D13DD2D1311DDD22D11D1D2DD2D1D D2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311DD2D1DD2D13 DD2D1DD22D2DD2D13DD2D1311D2DD2D13DD2D1D2DD2DD2D13DD2D13111DD2DD2D1DD2 D13DD2D1D2DD2DD2D13DD2D13111DD2D131DD2D131; ! 249 steps (((P -> Q) ^ (~ P -> Q)) <-> Q); ! *4.83 DD3DD2DD2DD2D13DD2D1311D1D3DD2D1D3DD2DD2D13DD2D1311DDD22D11D1D2DD2D1D D2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311DD2D1D2D1DD 2DD2D13D2DD2D1311DD2D1DD2DD2D121D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D12 1DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D1311111; ! 249 steps ((P <-> Q) -> ((P -> R) <-> (Q -> R))); ! *4.84 DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1DD2D1D2DD2D1211D3DD2D1D3D D2DD2D13DD2D13111DD2D1DD2D1D2DD2D1211D3DD2D1D3DD2DD2D13DD2D1311DD2D13 1; ! 139 steps ((P <-> Q) -> ((R -> P) <-> (R -> Q))); ! *4.85 DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1DD2D121D3DD2D1D3DD2DD2D13 DD2D1311DD2D131DD2D1DD2D121D3DD2D1D3DD2DD2D13DD2D13111; ! 123 steps ((P <-> Q) -> ((P <-> R) <-> (Q <-> R))); ! *4.86 DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2DD2D1DD2D1D2D1DD2D1DD2D13DD 2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311DD2D1DD2DD2D121D1DD2D1D D2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311DD2D1D2DD2D12DD2 D11DD2D121DD2D11DD2D1D2DD2D1211DD2D1DD2D1D2DD2D1211D3DD2D1D3DD2DD2D13 DD2D13111DD2D1DD2D121D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2DD2D1DD2D1D2 D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311DD2D1DD2 DD2D121D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311D D2D1D2DD2D12DD2D11DD2D121DD2D11DD2D1D2DD2D1211DD2D1DD2D1D2DD2D1211D3D D2D1D3DD2DD2D13DD2D1311DD2D131DD2D1DD2D121D3DD2D1D3DD2DD2D13DD2D1311 1; ! 621 steps (((((P ^ Q) -> R) <-> (P -> (Q -> R))) ^ ((P -> (Q -> R)) <-> (Q -> (P -> R)))) ^ ((Q -> (P -> R)) <-> ((Q ^ P) -> R))); ! *4.87 DD3DD2DD2DD2D13DD2D1311D1DD3DD2DD2DD2D13DD2D1311D1DD3DD2DD2DD2D13DD2D 1311D1DD2D1D2D13DD2D1DD2D1DD22D11DD2D112DD2D13D2D1D3DD2DD2D13DD2D1311 DD2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D1DD2D1DD22D11DD2D112D2D1DD2D1DD 2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311DD3DD2DD2DD2D13DD 2D1311D1DD2D1DD22D11DD2D112DD2D1DD22D11DD2D112DD3DD2DD2DD2D13DD2D1311 D1DD2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D1DD2D1DD22D11DD2D112D2D1DD2D1 DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311DD2D1D2D13DD2D1 DD2D1DD22D11DD2D112DD2D13D2D1D3DD2DD2D13DD2D1311; ! 531 steps ((P ^ Q) -> (P <-> Q)); ! *5.1 DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D11D3DD2D1D3DD2DD2D13DD2D13 111DD2D11D3DD2D1D3DD2DD2D13DD2D1311DD2D131; ! 111 steps ((P -> Q) v (~ P -> Q)); ! *5.11 DD2D1D2DD2D1D2DD2D131DD2D11DD2D1311; ! 35 steps ((P -> Q) v (P -> ~ Q)); ! *5.12 DD2D11D3DD2D1D3DD2DD2D13DD2D1311DD2D13DD2D131; ! 45 steps ((P -> Q) v (Q -> P)); ! *5.13 DD2D1D2DD2D1D2DD2D131DD2D1111; ! 29 steps ((P -> Q) v (Q -> R)); ! *5.14 DD2D1D2DD2D1D2DD2D131DD2D1111; ! 29 steps ((P <-> Q) v (P <-> ~ Q)); ! *5.15 DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1D2DD2D1DD2D1DD2D13DD2D1DD 22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311DD2D1DD2D1D2DD2D1DD2D13DD2D1 D2DD2DD2D13DD2D131111111DD2D1D2DD2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D 1DD2D1D2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1311DD2D131 1; ! 267 steps ~ ((P <-> Q) ^ (P <-> ~ Q)); ! *5.16 DD3DD2DD2D13DD2D1311DD2D1D3DD2DD2D13DD2D1311DD2DD2D1DD2D12D2D1DD2D13D D2D1D2D1D3DD2DD2D13DD2D1311DD2D1D2DD2DD2D13DD2D13111DD2D1DD2D1DD2DD2D 121D1DD2D13DD2D1DD22D2DD2D13DD2D1311DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1 311D2DD2D13DD2D1D2DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13DD2D13111DD2D1D D2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2DD2D13DD2D1D2DD2DD2D13DD2D13111D 3DD2D1D3DD2DD2D13DD2D1311DD2D131; ! 377 steps (((P v Q) ^ ~ (P ^ Q)) <-> (P <-> ~ Q)); ! *5.17 DD3DD2DD2DD2D13DD2D1311D1D3DD2D1D3DD2DD2D13DD2D1311DD2D1DD2D1D2D1D3DD 2DD2D13DD2D1311DD2D1DD2DD2D121D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D13DD 2D1DD22D2DD2D13DD2D1311DD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D1311DD2 D1DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311DD2DD2D121D1DD2D13D2D1D3DD 2DD2D13DD2D1311D2D1DD2DD2D13DD2D1311DD2DD2D13DD2D1311; ! 329 steps ((P <-> Q) <-> ~ (P <-> ~ Q)); ! *5.18 DD3DD2DD2DD2D13DD2D1311D1DD2D1D3DD2DD2D13DD2D1311DD2DD2D1DD2D12D2D1DD 2D13DD2D1D2D1D3DD2DD2D13DD2D1311DD2D1D2DD2DD2D13DD2D13111DD2D1DD2D1DD 2DD2D121D1DD2D13DD2D1DD22D2DD2D13DD2D1311DD2D1DD2D13DD2D1DD22D2DD2D13 DD2D1311D2DD2D13DD2D1D2DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13DD2D13111D D2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2DD2D13DD2D1D2DD2DD2D13DD2D1 3111D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2D1DD2DD2D1DD2D13DD2D1D2DD2DD2 D13DD2D13111DD2D1DD2D13DD2DD2D121D11D2D1D3DD2D1D3DD2DD2D13DD2D1311DD2 D13DD2D131DD2D1DD2D13DD2DD2D121D1DD2D131D2D1D3DD2D1D3DD2DD2D13DD2D131 1DD2D131DD2DD2D13DD2D1311; ! 577 steps ~ (P <-> ~ P); ! *5.19 DD3DD2DD2D13DD2D1311DD2D1D3DD2D1D3DD2DD2D13DD2D1311DD2D1DD2DD2D13D2DD 2D1311DD2DD2D13DD2D1311DD2D1DD2DD2D13D2DD2D1311DD2D1DD22D2DD2D13DD2D1 311; ! 141 steps ((~ P ^ ~ Q) -> (P <-> Q)); ! *5.21 DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D13DD2D11D3DD2D1D3DD2DD2D13 DD2D1311DD2D131DD2D13DD2D11D3DD2D1D3DD2DD2D13DD2D13111; ! 123 steps (~ (P <-> Q) <-> ((P ^ ~ Q) v (Q ^ ~ P))); ! *5.22 DD3DD2DD2DD2D13DD2D1311D1DD2D1DD2D1DD2D1DD22D2DD2D13DD2D1311DD2D1DD2D D2D121D1D2D1DD2DD2D13DD2D1311D2D1D3DD2D1D3DD2DD2D13DD2D1311DD2D1D2D1D D2DD2D13DD2D1311DD2DD2D13DD2D1311DD2DD2D13DD2D1311DD2D1D3DD2DD2D13DD2 D1311DD2D1DD2D1D2D1D3DD2D1D3DD2DD2D13DD2D1311DD2D1D2D1D3DD2DD2D13DD2D 1311DD2DD2D13DD2D1311DD2DD2D121D1D2D1D3DD2DD2D13DD2D1311DD2DD2D121D1D 3DD2DD2D13DD2D1311; ! 363 steps ((P <-> Q) <-> ((P ^ Q) v (~ P ^ ~ Q))); ! *5.23 DD3DD2DD2DD2D13DD2D1311D1DD2D1DD2D1DD22D2DD2D13DD2D1311DD2DD2D1DD2D12 D2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13D D2D1311D2DD2D13DD2D1D2DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13DD2D1311DD2 D131DD2D1DD2D1DD2DD2D121D1DD2D13DD2D1DD22D2DD2D13DD2D1311DD2D1DD2D13D D2D1DD22D2DD2D13DD2D1311D2DD2D13DD2D1D2DD2DD2D13DD2D13111D3DD2D1D3DD2 DD2D13DD2D13111DD2D1DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1DD2D1 3DD2DD2D121D11D2D1D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2D1DD2D13DD2DD2D 121D1DD2D131D2D1D3DD2D1D3DD2DD2D13DD2D13111DD2DD2D121D1D3DD2DD2D13DD2 D1311; ! 557 steps (~ ((P ^ Q) v (~ P ^ ~ Q)) <-> ((P ^ ~ Q) v (Q ^ ~ P))); ! *5.24 DD3DD2DD2DD2D13DD2D1311D1DD2D1DD2D1DD22D2DD2D13DD2D1311DD2D1DD2DD2D12 1D1D2D1DD2DD2D13DD2D1311DD2DD2D1DD2D12D2D1DD2D13DD2D1D2DD2DD2D13DD2D1 3111DD2D1DD2D1DD2D1D2DD2D1D2D1DD2DD2D13D2DD2D1311DD2D1DD2DD2D121D1DD2 D13D2D1D3DD2DD2D13DD2D1311DD2D1211D2D1DD2DD2D13DD2D1311D3DD2D1D3DD2DD 2D13DD2D13111DD2D1DD2D1DD2D1D2DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D D2D13DD2D1D2DD2DD2D13DD2D131111DD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2 D1311DD2D131DD2D1DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1DD2D1DD2 D1D3DD2DD2D13DD2D13113D2D1D3DD2D1D3DD2DD2D13DD2D13111DD2DD2D121D11DD2 D1DD2D1D2D1D3DD2DD2D13DD2D1311D2D1D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD 2DD2D121D1DD2D131DD2DD2D121D1D3DD2DD2D13DD2D1311; ! 669 steps ((P v Q) <-> ((P -> Q) -> Q)); ! *5.25 DD3DD2DD2DD2D13DD2D1311D1DD2D1D2DD2D1D2D1DD2DD2D13D2DD2D1311DD2D1DD2D D2D121D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D1211DD2DD2D121D1DD2D13 1; ! 133 steps (((P ^ Q) -> R) <-> ((P ^ Q) -> (P ^ R))); ! *5.3 DD3DD2DD2DD2D13DD2D1311D1D2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111D3DD2D 1D3DD2DD2D13DD2D1311DD2D131D2D1D3DD2D1D3DD2DD2D13DD2D1311 1; ! 127 steps ((R ^ (P -> Q)) -> (P -> (Q ^ R))); ! *5.31 DD2D1D2DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D13 11DD2D1DD2DD2D121D1DD2D13DD2D1DD22D2DD2D13DD2D1311DD2D12DD2D11DD2D13D D2D1D2D1D3DD2DD2D13DD2D1311DD2D1D2DD2DD2D13DD2D131111; ! 191 steps ((P -> (Q <-> R)) <-> ((P ^ Q) <-> (P ^ R))); ! *5.32 DD3DD2DD2DD2D13DD2D1311D1DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1 DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311DD2D12D2D1 DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311D3DD2 D1D3DD2DD2D13DD2D1311DD2D131DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311 D2D1D3DD2DD2D13DD2D1311DD2D12D2D1DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2 D1311D2D1D3DD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D13111DD2DD2D1DD2D12 D2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1D2D13DD2D1DD2D1D2D1DD2DD2D121 D11DD2D1DD22D11DD2D112DD2D13D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2D1D2D 13DD2D1DD2D1D2D1DD2DD2D121D11DD2D1DD22D11DD2D112DD2D13D3DD2D1D3DD2DD2 D13DD2D13111; ! 633 steps ((P ^ (Q -> R)) <-> (P ^ ((P ^ Q) -> R))); ! *5.33 DD3DD2DD2DD2D13DD2D1311D1DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111D3DD2 D1D3DD2DD2D13DD2D1311DD2D131DD2D1DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D13 111D3DD2D1D3DD2DD2D13DD2D13111DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111 D3DD2D1D3DD2DD2D13DD2D1311DD2D131D3DD2D1D3DD2DD2D13DD2D1311DDD22D11D1 D2DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311DD2 D1DD2D1D2DD2D1211DD2D13DD2D1D2DD2DD2D13DD2D13111; ! 393 steps (((P -> Q) ^ (P -> R)) -> (P -> (Q <-> R))); ! *5.35 D3DD2D1D3DD2DD2D13DD2D1311DDD22D11D1D2DD2D1DD2D1DD2D13DD2D1DD22D2DD2D 13DD2D1311D2D1D3DD2DD2D13DD2D1311DD2D12D2D1DD2D1DD2D1D2DD2D1DD2D13DD2 D1D2DD2DD2D13DD2D13111111; ! 163 steps ((P ^ (P <-> Q)) <-> (Q ^ (P <-> Q))); ! *5.36 DD3DD2DD2DD2D13DD2D1311D1DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111D3DD2 D1D3DD2DD2D13DD2D1311DD2D1D2D1DD2D1D3DD2DD2D13DD2D1311DD2D131DD2D1D2D D2D13DD2D1D2D1D3DD2DD2D13DD2D1311DD2D1D2DD2DD2D13DD2D131111D3DD2D1D3D D2DD2D13DD2D13111DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111D3DD2D1D3DD2D D2D13DD2D1311DD2D1D2D1DD2D1D3DD2DD2D13DD2D13111DD2D1D2DD2D13DD2D1D2D1 D3DD2DD2D13DD2D1311DD2D1D2DD2DD2D13DD2D131111D3DD2D1D3DD2DD2D13DD2D13 111; ! 417 steps ((P -> (P -> Q)) <-> (P -> Q)); ! *5.4 DD3DD2DD2DD2D13DD2D1311D1DD22D211; ! 33 steps (((P -> Q) -> (P -> R)) <-> (P -> (Q -> R))); ! *5.41 DD3DD2DD2DD2D13DD2D1311D1DD2D1D2D1DD2DD2D121D11DD2D1DD22D11DD2D112 2; ! 67 steps ((P -> (Q -> R)) <-> (P -> (Q -> (P ^ R)))); ! *5.42 DD3DD2DD2DD2D13DD2D1311D1D2DD2D1DD2D12D2D1DD2D13DD2D1D2DD2DD2D13DD2D1 31111D2D1D2D1D3DD2D1D3DD2DD2D13DD2D13111; ! 109 steps ((P -> Q) -> ((P -> R) <-> (P -> (Q ^ R)))); ! *5.44 DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D12D2D1DD2D13DD2D1D2DD2DD2D 13DD2D13111D1D2D1D3DD2D1D3DD2DD2D13DD2D13111; ! 113 steps (P -> ((P -> Q) <-> Q)); ! *5.5 DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1D2DD2111D11; ! 55 steps (P -> (Q <-> (P <-> Q))); ! *5.501 DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1DD2D1D2DD2D1DD2D13DD2D1D2 DD2DD2D13DD2D13111111DD2D1D2D3DD2D1D3DD2DD2D13DD2D1311DD2D131 1; ! 131 steps ((((P v Q) v R) -> S) <-> (((P -> S) ^ (Q -> S)) ^ (R -> S))); ! *5.53 DD3DD2DD2DD2D13DD2D1311D1DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2DD 2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2DD2D121D1DD2D1D2DD2D131DD2D11DD2 D1D2DD2D1311DD2DD2D121D1DD2D1D2DD2D131DD2D111DD2DD2D121D11DD2D13DD2DD 2D1DD2D12D2D1DD2D13DD2D1D2D1D3DD2DD2D13DD2D1311DD2D1D2DD2DD2D13DD2D13 111DD2D1DD2DD2D1DD2D12D2D1DD2D13DD2D1D2D1D3DD2DD2D13DD2D1311DD2D1D2DD 2DD2D13DD2D13111DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2 D13DD2D1311D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2D1DD2D1DD2D13DD2D1DD22 D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D13111D3D D2D1D3DD2DD2D13DD2D1311DD2D131DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D13 11D2D1D3DD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D13111; ! 673 steps (((P ^ Q) <-> P) v ((P ^ Q) <-> Q)); ! *5.54 DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111D1D3DD2D1D3DD2DD2D13DD2D13111D 3DD2D1D3DD2DD2D13DD2D1311DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1 D2DD2D1D2DD2D131DD2D1111DD2D1D2DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1 311D2D1D3DD2DD2D13DD2D1311DD2D1D2D2D1DD2D13111; ! 253 steps (((P v Q) <-> P) v ((P v Q) <-> Q)); ! *5.55 DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13DD2D1311DD2D D2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1D2DD2D13D2D1DD2D1D3DD2DD2D13D D2D131111D1DD2D1D2DD2D1311D11; ! 167 steps (((P ^ ~ Q) -> R) <-> (P -> (Q v R))); ! *5.6 DD3DD2DD2DD2D13DD2D1311D1DD2D1D2D13DD2D1DD2D1DD22D11DD2D112DD2D13D2D1 D3DD2DD2D13DD2D1311DD2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D1DD2D1DD22D1 1DD2D112D2D1DD2D1DD2D1D2D1D3DD2DD2D13DD2D13113D2D1D3DD2DD2D13DD2D131 1; ! 207 steps (((P v Q) ^ ~ Q) <-> (P ^ ~ Q)); ! *5.61 DD3DD2DD2DD2D13DD2D1311D1D3DD2D1D3DD2DD2D13DD2D1311DD2D1DD2D1DD2DD2D1 21D1D2D1D3DD2DD2D13DD2D1311DD2D1D2D1DD2DD2D13D2DD2D1311DD2D1DD2DD2D12 1D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D121DD2DD2D13DD2D1311D3DD2D1D3DD2D D2D13DD2D1311DD2D1DD2DD2D121D1DD2D1D2DD2D1311DD2DD2D13DD2D131 1; ! 269 steps (((P ^ Q) v ~ Q) <-> (P v ~ Q)); ! *5.62 DD3DD2DD2DD2D13DD2D1311D1DD2DD2D121D1DD2D1D3DD2DD2D13DD2D1311DD2D131D D2D1DD2D1DD22D2DD2D13DD2D1311DD2D1D2DD2D1D2D1DD2DD2D13D2DD2D1311DD2D1 DD2DD2D121D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D1211; ! 187 steps ((P v Q) <-> (P v (~ P ^ Q))); ! *5.63 DD3DD2DD2DD2D13DD2D1311D1D2DD2D13DD2D1D2DD2DD2D13DD2D13111D2D1D3DD2D1 D3DD2DD2D13DD2D13111; ! 89 steps (((P v R) <-> (Q v R)) <-> (R v (P <-> Q))); ! *5.7 DD3DD2DD2DD2D13DD2D1311D1DD2DD2D1DD2D12D2D1DD2D13DD2D1D2DD2DD2D13DD2D 13111DD2D1DD2D1DD2D1DD2D1D2D1DD2DD2D121D11DD2D1DD22D11DD2D112D2D1DD2D 13D2D1D3DD2DD2D13DD2D1311DD2DD2D121D1DD2D13D2D1D3DD2DD2D13DD2D1311D3D D2D1D3DD2DD2D13DD2D1311DD2D131DD2D1DD2D1DD2D1DD2D1D2D1DD2DD2D121D11DD 2D1DD22D11DD2D112D2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2DD2D121D1DD2D13D 2D1D3DD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D13111DD2DD2D1DD2D13DD2D1D 2DD2DD2D13DD2D13111DD2D1DD2D1DD2D1DD2DD2D121D1DD2D13D2D1D3DD2DD2D13DD 2D1311D2D1DD2D13D2D1D3DD2DD2D13DD2D13112D2D1D3DD2D1D3DD2DD2D13DD2D131 1DD2D131DD2D1DD2D1DD2D1DD2DD2D121D1DD2D13D2D1D3DD2DD2D13DD2D1311D2D1D D2D13D2D1D3DD2DD2D13DD2D13112D2D1D3DD2D1D3DD2DD2D13DD2D1311 1; ! 681 steps ((Q -> ~ R) -> (((P v Q) ^ R) <-> (P ^ R))); ! *5.71 DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2DD2D1DD2D12D2D1DD2D13DD2D1D 2DD2DD2D13DD2D13111DD2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D1DD2D1DD22D1 1DD2D112DD2D121D1D3DD2D1D3DD2DD2D13DD2D13111D1D3DD2D1D3DD2DD2D13DD2D1 311DD2D1DD2DD2D121D1DD2D1D2DD2D1311DD2DD2D13DD2D1311; ! 259 steps ((P -> (Q <-> R)) <-> ((P -> Q) <-> (P -> R))); ! *5.74 DD3DD2DD2DD2D13DD2D1311D1DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1 2D2D1D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2D12D2D1D3DD2D1D3DD2DD2D13DD2 D13111DD2DD2D1DD2D12D2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1DD2D1D2D1 DD2DD2D121D11DD2D1DD22D11DD2D112D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2D 1DD2D1D2D1DD2DD2D121D11DD2D1DD22D11DD2D112D3DD2D1D3DD2DD2D13DD2D1311 1; ! 345 steps (((R -> ~ Q) ^ (P <-> (Q v R))) -> ((P ^ ~ Q) <-> R)); ! *5.75 DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1DD2D1DD2D1DD2D13D2D1D3DD2 DD2D13DD2D1311DD2D1DD2D1DD22D11DD2D112D2D1DD2D1DD2D1D2D1D3DD2DD2D13DD 2D13113D2D1D3DD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D1311DD2D131D3DD2D 1D3DD2DD2D13DD2D13111DD2DD2D1DD2D12D2D1DD2D13DD2D1D2DD2DD2D13DD2D1311 1DD2D1DD2D1DD2DD2D121D11D3DD2D1D3DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13 DD2D13111D3DD2D1D3DD2DD2D13DD2D1311DD2D131; ! 387 steps