Shortest known proofs of the propositional calculus theorems from ----------------------------------------------------------------- _Principia Mathematica_ ----------------------- ---------------------------------------------------------------------------- ~~ PUBLIC DOMAIN ~~ This work is waived of all rights, including copyright, according to the CC0 Public Domain Dedication. http://creativecommons.org/publicdomain/zero/1.0/ ---------------------------------------------------------------------------- Created with pmGenerator (https://xamidi.github.io/pmGenerator) from pmproofs.txt (https://us.metamath.org/mmsolitaire/pmproofs.txt) by Samiro Discher on 11-Nov-2025. In contrast to using Metamath's set.mm propositional axioms (ax-1,ax-2,ax-3), the here used axioms are: luk-1 ((P -> Q) -> ((Q -> R) -> (P -> R))) luk-2 ((~ P -> P) -> P) luk-3 (P -> (~ P -> Q)) Wrap: pmGenerator -c -n -s CCpqCCqrCpr,CCNppp,CpCNpq -a SD data/empty.txt data/L-pmproofs-nowrap.txt data/L-pmproofs.txt -s -l -w -d ------------------------------------------------------------------------------- For pmGenerator: THERE MUST BE NO SEMICOLONS IN THE ENTIRE BODY OF TEXT ABOVE. For pmGenerator: THIS COMMENT HEADER ENDS WITH THE LINE OF DASHES BELOW. ------------------------------------------------------------------------------- ((P v P) -> P); ! *1.2 Taut ((~ P -> P) -> P); ! Result of proof 2; ! 1 step (Q -> (P v Q)); ! *1.3 Add (P -> (Q -> P)); ! Result of proof DD13DD11DD11DD1D1DD13DD1D1D322DD12D13; ! 37 steps ((P v Q) -> (Q v P)); ! *1.4 ((~ P -> Q) -> (~ Q -> P)); ! Result of proof DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11DD1D1DD13DD1D1D3222; ! 79 steps ((P v (Q v R)) -> (Q v (P v R))); ! *1.5 Assoc ((P -> (Q -> R)) -> (Q -> (P -> R))); ! Result of proof DD11D1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1D12; ! 55 steps ((Q -> R) -> ((P v Q) -> (P v R))); ! *1.6 Sum ((P -> Q) -> ((R -> P) -> (R -> Q))); ! Result of proof DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D12; ! 53 steps ((P -> ~ P) -> ~ P); ! *2.01 ((P -> ~ P) -> ~ P); ! Result of proof DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222; ! 57 steps (Q -> (P -> Q)); ! *2.02 Simp (P -> (Q -> P)); ! Result of proof DD13DD11DD11DD1D1DD13DD1D1D322DD12D13; ! 37 steps ((P -> ~ Q) -> (Q -> ~ P)); ! *2.03 ((P -> ~ Q) -> (Q -> ~ P)); ! Result of proof DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD11DD11DD1D1DD13DD1D1D322DD12D13; ! 89 steps ((P -> (Q -> R)) -> (Q -> (P -> R))); ! *2.04 Comm ((P -> (Q -> R)) -> (Q -> (P -> R))); ! Result of proof DD11D1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1D12; ! 55 steps ((Q -> R) -> ((P -> Q) -> (P -> R))); ! *2.05 Syll ((P -> Q) -> ((R -> P) -> (R -> Q))); ! Result of proof DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D12; ! 53 steps ((P -> Q) -> ((Q -> R) -> (P -> R))); ! *2.06 Syll ((P -> Q) -> ((Q -> R) -> (P -> R))); ! Result of proof 1; ! 1 step (P -> (P v P)); ! *2.07 (P -> (Q -> P)); ! Result of proof DD13DD11DD11DD1D1DD13DD1D1D322DD12D13; ! 37 steps (P -> P); ! *2.08 Id (P -> P); ! Result of proof DD132; ! 5 steps (~ P v P); ! *2.1 (~ ~ P -> P); ! Result of proof DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222; ! 51 steps (P v ~ P); ! *2.11 (P -> P); ! Result of proof DD132; ! 5 steps (P -> ~ ~ P); ! *2.12 (P -> ~ ~ P); ! Result of proof DD13DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222; ! 61 steps (P v ~ ~ ~ P); ! *2.13 (P -> ~ ~ P); ! Result of proof DD13DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222; ! 61 steps (~ ~ P -> P); ! *2.14 (~ ~ P -> P); ! Result of proof DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222; ! 51 steps ((~ P -> Q) -> (~ Q -> P)); ! *2.15 Transp ((~ P -> Q) -> (~ Q -> P)); ! Result of proof DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11DD1D1DD13DD1D1D3222; ! 79 steps ((P -> Q) -> (~ Q -> ~ P)); ! *2.16 ((P -> Q) -> (~ Q -> ~ P)); ! Result of proof DD1DD11DD1D1DD13DD1D1D3322DD1D1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1322; ! 125 steps ((~ Q -> ~ P) -> (P -> Q)); ! *2.17 Transp ((~ P -> ~ Q) -> (Q -> P)); ! Result of proof DD11DD11DD1D1DD13DD1D1D322DD12D13; ! 33 steps ((~ P -> P) -> P); ! *2.18 ((~ P -> P) -> P); ! Result of proof 2; ! 1 step (P -> (P v Q)); ! *2.2 (P -> (~ P -> Q)); ! Result of proof 3; ! 1 step (~ P -> (P -> Q)); ! *2.21 (~ P -> (P -> Q)); ! Result of proof DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122; ! 47 steps (P -> (~ P -> Q)); ! *2.24 (P -> (~ P -> Q)); ! Result of proof 3; ! 1 step (P v ((P v Q) -> Q)); ! *2.25 (P -> ((P -> Q) -> Q)); ! Result of proof DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1D12; ! 49 steps (~ P v ((P -> Q) -> Q)); ! *2.26 (~ ~ P -> ((P -> Q) -> Q)); ! Result of proof DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12DD11DD11DD1D1DD13DD1D1D3222D1D12; ! 81 steps (P -> ((P -> Q) -> Q)); ! *2.27 (P -> ((P -> Q) -> Q)); ! Result of proof DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1D12; ! 49 steps ((P v (Q v R)) -> (P v (R v Q))); ! *2.3 ((P -> (~ Q -> R)) -> (P -> (~ R -> Q))); ! Result of proof DD11DD1D1DD1DD1DD13D1D3DD11DD1D1DD13DD1D1D32222D1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222; ! 103 steps ((P v (Q v R)) -> ((P v Q) v R)); ! *2.31 ((P -> (~ Q -> R)) -> (~ (P -> Q) -> R)); ! Result of proof DD11DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12DD11DD11DD1D1DD13DD1D1D3222D1DD1DD11DD11DD1D1DD13DD1D1D3222D1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD1DD11DD1D1DD13DD1D1D33222; ! 185 steps (((P v Q) v R) -> (P v (Q v R))); ! *2.32 ((~ (P -> Q) -> R) -> (P -> (~ Q -> R))); ! Result of proof DD1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D12D1D2DD1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D3222DD11DD1D1DD13DD1D1D3322; ! 175 steps ((Q -> R) -> ((P v Q) -> (R v P))); ! *2.36 ((P -> Q) -> ((~ R -> P) -> (~ Q -> R))); ! Result of proof DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11D1DD11DD11DD1D1DD13DD1D1D3222; ! 89 steps ((Q -> R) -> ((Q v P) -> (P v R))); ! *2.37 ((P -> Q) -> ((~ P -> R) -> (~ R -> Q))); ! Result of proof DD1D12DD1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D12D1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122; ! 117 steps ((Q -> R) -> ((Q v P) -> (R v P))); ! *2.38 ((P -> Q) -> ((~ P -> R) -> (~ Q -> R))); ! Result of proof DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11D1D12; ! 121 steps ((P v (P v Q)) -> (P v Q)); ! *2.4 ((P -> (P -> Q)) -> (P -> Q)); ! Result of proof DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222; ! 57 steps ((Q v (P v Q)) -> (P v Q)); ! *2.41 ((~ P -> (Q -> P)) -> (Q -> P)); ! Result of proof DD1DD11D1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1D12DD11DD1D1DD13DD1D1D3222; ! 81 steps ((~ P v (P -> Q)) -> (P -> Q)); ! *2.42 ((~ ~ P -> (P -> Q)) -> (P -> Q)); ! Result of proof DD1D1DD13DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222; ! 123 steps ((P -> (P -> Q)) -> (P -> Q)); ! *2.43 ((P -> (P -> Q)) -> (P -> Q)); ! Result of proof DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222; ! 57 steps (~ (P v Q) -> ~ P); ! *2.45 (~ (P -> Q) -> P); ! Result of proof DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D1332; ! 73 steps (~ (P v Q) -> ~ Q); ! *2.46 (~ (P -> Q) -> ~ Q); ! Result of proof D2DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D123; ! 117 steps (~ (P v Q) -> (~ P v Q)); ! *2.47 (~ (P -> Q) -> (~ P -> R)); ! Result of proof D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D133; ! 69 steps (~ (P v Q) -> (P v ~ Q)); ! *2.48 (~ (P -> Q) -> (R -> ~ Q)); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD1DD11DD11DD1D1DD13DD1D1D322DD12D133; ! 127 steps (~ (P v Q) -> (~ P v ~ Q)); ! *2.49 (~ (P -> Q) -> (~ P -> R)); ! Result of proof D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D133; ! 69 steps (~ (P -> Q) -> (~ P -> Q)); ! *2.5 (~ (P -> Q) -> (~ P -> R)); ! Result of proof D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D133; ! 69 steps (~ (P -> Q) -> (P -> ~ Q)); ! *2.51 (~ (P -> Q) -> (R -> ~ Q)); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD1DD11DD11DD1D1DD13DD1D1D322DD12D133; ! 127 steps (~ (P -> Q) -> (~ P -> ~ Q)); ! *2.52 (~ (P -> Q) -> (~ P -> R)); ! Result of proof D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D133; ! 69 steps (~ (P -> Q) -> (Q -> P)); ! *2.521 (~ (P -> Q) -> (Q -> R)); ! Result of proof DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13; ! 89 steps ((P v Q) -> (~ P -> Q)); ! *2.53 (P -> P); ! Result of proof DD132; ! 5 steps ((~ P -> Q) -> (P v Q)); ! *2.54 (P -> P); ! Result of proof DD132; ! 5 steps (~ P -> ((P v Q) -> Q)); ! *2.55 (P -> ((P -> Q) -> Q)); ! Result of proof DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1D12; ! 49 steps (~ Q -> ((P v Q) -> P)); ! *2.56 (~ P -> ((~ Q -> P) -> Q)); ! Result of proof DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12DD1DD11D11DD11DD1D1DD13DD1D1D3222DD11DD1D1DD13DD1D1D3222; ! 105 steps ((~ P -> Q) -> ((P -> Q) -> Q)); ! *2.6 ((~ P -> Q) -> ((P -> Q) -> Q)); ! Result of proof DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11DD11DD1D1DD13DD1D1D3222D1D12; ! 91 steps ((P -> Q) -> ((~ P -> Q) -> Q)); ! *2.61 ((P -> Q) -> ((~ P -> Q) -> Q)); ! Result of proof DD1D12DD1DD1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D12DD11DD1D1DD13DD1D1D3222D1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122; ! 143 steps ((P v Q) -> ((P -> Q) -> Q)); ! *2.62 ((~ P -> Q) -> ((P -> Q) -> Q)); ! Result of proof DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11DD11DD1D1DD13DD1D1D3222D1D12; ! 91 steps ((P -> Q) -> ((P v Q) -> Q)); ! *2.621 ((P -> Q) -> ((~ P -> Q) -> Q)); ! Result of proof DD1D12DD1DD1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D12DD11DD1D1DD13DD1D1D3222D1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122; ! 143 steps ((P v Q) -> ((~ P v Q) -> Q)); ! *2.63 ((P -> Q) -> ((~ P -> Q) -> Q)); ! Result of proof DD1D12DD1DD1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D12DD11DD1D1DD13DD1D1D3222D1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122; ! 143 steps ((P v Q) -> ((P v ~ Q) -> P)); ! *2.64 ((~ P -> Q) -> ((~ P -> ~ Q) -> P)); ! Result of proof DD1DD11D1DD11DD11DD1D1DD13DD1D1D322DD12D13DD11DD1D1DD13DD1D1D3222; ! 65 steps ((P -> Q) -> ((P -> ~ Q) -> ~ P)); ! *2.65 ((P -> Q) -> ((P -> ~ Q) -> ~ P)); ! Result of proof DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11DD11DD1D1DD13DD1D1D3222D1DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD11DD11DD1D1DD13DD1D1D322DD12D13; ! 177 steps (((P v Q) -> Q) -> (P -> Q)); ! *2.67 (((~ P -> Q) -> R) -> (P -> R)); ! Result of proof D13; ! 3 steps (((P -> Q) -> Q) -> (P v Q)); ! *2.68 (((P -> Q) -> R) -> (~ P -> R)); ! Result of proof D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122; ! 49 steps (((P -> Q) -> Q) -> ((Q -> P) -> P)); ! *2.69 (((P -> Q) -> R) -> ((R -> P) -> P)); ! Result of proof DD1D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11DD11DD1D1DD13DD1D1D3222; ! 79 steps ((P -> Q) -> (((P v Q) v R) -> (Q v R))); ! *2.73 ((P -> Q) -> ((~ (~ P -> Q) -> R) -> (~ Q -> R))); ! Result of proof DD1D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD12DD1DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11D1D12DD11DD1D1DD13DD1D1D3DD123221; ! 193 steps ((Q -> P) -> (((P v Q) v R) -> (P v R))); ! *2.74 ((P -> Q) -> ((~ (~ Q -> P) -> R) -> (~ Q -> R))); ! Result of proof DD1D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD12DD11DD11DD1D1DD13DD1D1D3DD123221; ! 129 steps ((P v Q) -> ((P v (Q -> R)) -> (P v R))); ! *2.75 ((P -> Q) -> ((P -> (Q -> R)) -> (P -> R))); ! Result of proof DD11DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11D11DD11DD1D1DD13DD1D1D3222; ! 93 steps ((P v (Q -> R)) -> ((P v Q) -> (P v R))); ! *2.76 ((P -> (Q -> R)) -> ((P -> Q) -> (P -> R))); ! Result of proof DD1DD11D11DD11DD1D1DD1DD13DD1D1D322D1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222; ! 91 steps ((P -> (Q -> R)) -> ((P -> Q) -> (P -> R))); ! *2.77 ((P -> (Q -> R)) -> ((P -> Q) -> (P -> R))); ! Result of proof DD1DD11D11DD11DD1D1DD1DD13DD1D1D322D1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222; ! 91 steps ((Q v R) -> ((~ R v S) -> (Q v S))); ! *2.8 ((P -> Q) -> ((~ ~ Q -> R) -> (P -> R))); ! Result of proof DD11D1D1DD13DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222; ! 69 steps ((Q -> (R -> S)) -> ((P v Q) -> ((P v R) -> (P v S)))); ! *2.81 ((P -> (Q -> R)) -> ((S -> P) -> ((S -> Q) -> (S -> R)))); ! Result of proof DD1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D12DD1DD11D1DD1DD13DD1D1D322D1DD1DD11D11DD11D1DD1DD13DD1D1D322D1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222; ! 171 steps (((P v Q) v R) -> (((P v ~ R) v S) -> ((P v Q) v S))); ! *2.82 ((~ (P -> Q) -> R) -> ((~ (P -> ~ R) -> S) -> (~ (P -> Q) -> S))); ! Result of proof DD1DD11DD1D1DD11D13DD1D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD11DD1D1DD13DD1D1D3DD1232DD1221; ! 129 steps ((P -> (Q -> R)) -> ((P -> (R -> S)) -> (P -> (Q -> S)))); ! *2.83 ((P -> (Q -> R)) -> ((P -> (R -> S)) -> (P -> (Q -> S)))); ! Result of proof DD11DD1D1DD11D11DD11DD1D1DD1DD13DD1D1D322D1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222; ! 97 steps (((P v Q) -> (P v R)) -> (P v (Q -> R))); ! *2.85 (((P -> Q) -> (R -> S)) -> (R -> (Q -> S))); ! Result of proof DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD11D1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1D12; ! 97 steps (((P -> Q) -> (P -> R)) -> (P -> (Q -> R))); ! *2.86 (((P -> Q) -> (R -> S)) -> (R -> (Q -> S))); ! Result of proof DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD11D1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1D12; ! 97 steps ((P ^ Q) -> ~ (~ P v ~ Q)); ! *3.1 (~ (P -> Q) -> ~ (~ ~ P -> Q)); ! Result of proof DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD1DD13DD11DD1D13DD11D1DD13D12DD12D1DD13DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122222; ! 153 steps (~ (~ P v ~ Q) -> (P ^ Q)); ! *3.11 (~ (~ ~ P -> Q) -> ~ (P -> Q)); ! Result of proof D2DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD12D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12223; ! 135 steps ((~ P v ~ Q) v (P ^ Q)); ! *3.12 (~ (~ ~ P -> Q) -> ~ (P -> Q)); ! Result of proof D2DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD12D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12223; ! 135 steps (~ (P ^ Q) -> (~ P v ~ Q)); ! *3.13 (~ ~ (P -> Q) -> (~ ~ P -> Q)); ! Result of proof DD1DD13DD11DD1D13DD11D1DD13D12DD12D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222; ! 87 steps ((~ P v ~ Q) -> ~ (P ^ Q)); ! *3.14 ((~ ~ P -> Q) -> ~ ~ (P -> Q)); ! Result of proof DD1D1DD13DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222DD13DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222; ! 127 steps (P -> (Q -> (P ^ Q))); ! *3.2 (P -> (Q -> ~ (P -> ~ Q))); ! Result of proof DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12; ! 101 steps (Q -> (P -> (P ^ Q))); ! *3.21 (P -> (Q -> ~ (Q -> ~ P))); ! Result of proof DD13D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD121; ! 99 steps ((P ^ Q) -> (Q ^ P)); ! *3.22 (~ (P -> ~ Q) -> ~ (Q -> ~ P)); ! Result of proof D2DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD12D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11DD11DD1D1DD13DD1D1D322DD12D133; ! 171 steps ~ (P ^ ~ P); ! *3.24 ~ ~ (P -> ~ ~ P); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222D3DD13DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222; ! 119 steps ((P ^ Q) -> P); ! *3.26 Simp (~ (P -> Q) -> P); ! Result of proof DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D1332; ! 73 steps ((P ^ Q) -> Q); ! *3.27 Simp (~ (P -> ~ Q) -> Q); ! Result of proof DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132; ! 93 steps (((P ^ Q) -> R) -> (P -> (Q -> R))); ! *3.3 Exp ((~ (P -> ~ Q) -> R) -> (P -> (Q -> R))); ! Result of proof DD1DD13DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD1DD1DD1DD13DD11DD1D13DD11D1D12D1DD13DD11DD1D13DD11DD1D1DD13DD13D1222DD11DD1D13DD11D1DD12D12; ! 139 steps ((P -> (Q -> R)) -> ((P ^ Q) -> R)); ! *3.31 Imp ((P -> (Q -> R)) -> (~ (P -> ~ Q) -> R)); ! Result of proof DD1DD1DD11D11DD1D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11DD1D1DD13DD1D1D33222; ! 209 steps (((P -> Q) ^ (Q -> R)) -> (P -> R)); ! *3.33 Syll (~ ((P -> Q) -> ~ (Q -> R)) -> (P -> R)); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD11D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1323; ! 137 steps (((Q -> R) ^ (P -> Q)) -> (P -> R)); ! *3.34 Syll (~ ((P -> Q) -> ~ (R -> P)) -> (R -> Q)); ! Result of proof D2DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1332DD11D1DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D1332; ! 161 steps ((P ^ (P -> Q)) -> Q); ! *3.35 Ass (~ (P -> ~ (P -> Q)) -> Q); ! Result of proof D2DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D133DD12D1DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D1332; ! 157 steps (((P ^ Q) -> R) -> ((P ^ ~ R) -> ~ Q)); ! *3.37 Transp ((~ (P -> ~ Q) -> R) -> (~ (P -> ~ ~ R) -> ~ Q)); ! Result of proof DD1DD1DD11D1DD1DD13DD1D1D322D1DD13D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222D2DD1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D3222DD1DD1DD13D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD1211DD11DD1D1DD13DD1D1D3322; ! 311 steps ((P ^ Q) -> (P -> Q)); ! *3.4 (~ (P -> ~ Q) -> (R -> Q)); ! Result of proof DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12; ! 111 steps ((P -> R) -> ((P ^ Q) -> R)); ! *3.41 ((P -> Q) -> (~ (P -> R) -> Q)); ! Result of proof D1DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D1332; ! 75 steps ((Q -> R) -> ((P ^ Q) -> R)); ! *3.42 ((P -> Q) -> (~ (R -> ~ P) -> Q)); ! Result of proof D1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132; ! 95 steps (((P -> Q) ^ (P -> R)) -> (P -> (Q ^ R))); ! *3.43 Comp (~ ((P -> Q) -> ~ (P -> R)) -> (P -> ~ (Q -> ~ R))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD11DD1D1DD13D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD121DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11D11DD11DD1D1DD13DD1D1D3222D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1323; ! 333 steps (((Q -> P) ^ (R -> P)) -> ((Q v R) -> P)); ! *3.44 (~ ((P -> Q) -> ~ (R -> Q)) -> ((~ P -> R) -> Q)); ! Result of proof DD1D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD11D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD1DD123DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D12DD1D1DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11D1D123DD11DD1D1DD13DD1D1D3222; ! 345 steps ((P -> Q) -> ((P ^ R) -> (Q ^ R))); ! *3.45 Fact ((P -> Q) -> (~ (P -> R) -> ~ (Q -> R))); ! Result of proof DD1DD11D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD1DD11DD1D1DD13DD1D1D33222; ! 109 steps (((P -> R) ^ (Q -> S)) -> ((P ^ Q) -> (R ^ S))); ! *3.47 (~ ((P -> Q) -> ~ (R -> S)) -> (~ (P -> ~ R) -> ~ (Q -> ~ S))); ! Result of proof D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12232DD1D1D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD133DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D1DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132D1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132; ! 511 steps (((P -> R) ^ (Q -> S)) -> ((P v Q) -> (R v S))); ! *3.48 (~ ((P -> Q) -> ~ (R -> S)) -> ((~ P -> R) -> (~ Q -> S))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD11D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD1DD123DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D12DD1D1DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11D1D123; ! 319 steps ((P -> Q) <-> (~ Q -> ~ P)); ! *4.1 ~ (((P -> Q) -> (~ Q -> ~ P)) -> ~ ((~ R -> ~ S) -> (S -> R))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13DD1D1D322D1DD1D1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD11DD1D1DD13DD1D1D33222D3DD11DD11DD1D1DD13DD1D1D322DD12D13; ! 219 steps ((P <-> Q) <-> (~ P <-> ~ Q)); ! *4.11 ~ ((~ ((P -> Q) -> ~ (R -> S)) -> ~ ((~ S -> ~ R) -> ~ (~ Q -> ~ P))) -> ~ (~ ((~ T -> ~ U) -> ~ (~ V -> ~ W)) -> ~ ((W -> V) -> ~ (U -> T)))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1332DD1DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11D1DD13DD1D1D322DD1DD11D1DD1DD13DD11DD1D13DD11D1DD13D122DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11D1DD13DD1D1D322322D3D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1332DD1DD1DD11D13DD11D1DD13DD1D1D322DD1DD11D1DD1DD13DD11DD1D13DD11D1DD13D122DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD11D13DD11D1DD13DD1D1D3223; ! 833 steps ((P <-> ~ Q) <-> (Q <-> ~ P)); ! *4.12 ~ ((~ ((P -> ~ Q) -> ~ (~ R -> S)) -> ~ ((Q -> ~ P) -> ~ (~ S -> R))) -> ~ (~ ((T -> ~ U) -> ~ (~ V -> W)) -> ~ ((U -> ~ T) -> ~ (~ W -> V)))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12232DD1DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11D13DD11D1DD13DD1D1D322DD1DD11D1DD1DD13DD11DD1D13DD11D1DD13D122DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD12DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11DD1D1DD13DD1D1D322222D3D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12232DD1DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11D13DD11D1DD13DD1D1D322DD1DD11D1DD1DD13DD11DD1D13DD11D1DD13D122DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD12DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11DD1D1DD13DD1D1D3222; ! 897 steps (P <-> ~ ~ P); ! *4.13 ~ ((P -> ~ ~ P) -> ~ (~ ~ Q -> Q)); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13DD1D1D322D1DD13D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222D3DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222; ! 173 steps (((P ^ Q) -> R) <-> ((P ^ ~ R) -> ~ Q)); ! *4.14 ~ (((~ (P -> ~ Q) -> R) -> (~ (P -> ~ ~ R) -> ~ Q)) -> ~ ((~ (S -> ~ ~ T) -> U) -> (~ (S -> U) -> T))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3DD1DD1DD11D1DD1DD13DD1D1D322D1DD13D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222D2DD1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D3222DD1DD1DD13D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD1211DD11DD1D1DD13DD1D1D332222D3DD1DD1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1D12D1DD1DD13D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD1211DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11DD1D1DD13DD1D1D3222; ! 609 steps (((P ^ Q) -> ~ R) <-> ((Q ^ R) -> ~ P)); ! *4.15 ~ (((~ (P -> ~ Q) -> R) -> (~ (Q -> R) -> ~ P)) -> ~ ((~ (S -> T) -> ~ U) -> (~ (U -> ~ S) -> T))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3D2DD1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D3222DD1DD1DD1DD1DD13DD11DD1D13DD11D1D12D1DD13DD11DD1D13DD11DD1D1DD13DD13D1222DD11DD1D13DD11D1D12DD11DD1D1DD13DD1D1D332222D3DD1DD1DD11DD11DD1D1DD13DD1D1D3222D1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D133DD1DD11D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12DD11DD11DD1D1DD13DD1D1D3222D1D1DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13322; ! 509 steps (P <-> P); ! *4.2 ~ ((P -> P) -> ~ (Q -> Q)); ! Result of proof D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD12D1DD13DD1D1D3DD13222D3DD132; ! 69 steps ((P <-> Q) <-> (Q <-> P)); ! *4.21 ~ ((~ (P -> ~ Q) -> ~ (Q -> ~ P)) -> ~ (~ (R -> ~ S) -> ~ (S -> ~ R))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3D2DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD12D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11DD11DD1D1DD13DD1D1D322DD12D13322D3D2DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD12D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11DD11DD1D1DD13DD1D1D322DD12D133; ! 401 steps (((P <-> Q) ^ (Q <-> R)) -> (P <-> R)); ! *4.22 (~ (~ ((P -> Q) -> ~ (R -> S)) -> ~ ~ ((Q -> T) -> ~ (U -> R))) -> ~ ((P -> T) -> ~ (U -> S))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12232DD1DD11D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12232DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D1DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD1DD1DD13DD11DD1D13DD11D1D12D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D133212D1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1323; ! 677 steps (P <-> (P ^ P)); ! *4.24 ~ ((P -> ~ (P -> ~ P)) -> ~ (~ (Q -> ~ R) -> R)); ! Result of proof D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122DD1D1DD1DD13D1D3DD1DD13D12DD1D1DD1DD13DD11DD1D13DD11D1DD13D12DD12D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222222D3DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132; ! 255 steps (P <-> (P v P)); ! *4.25 ~ ((P -> (Q -> P)) -> ~ ((~ R -> R) -> R)); ! Result of proof D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122DD1D1DD1DD13D1D3DD13DD11DD11DD1D1DD13DD1D1D322DD12D1322D32; ! 97 steps ((P ^ Q) <-> (Q ^ P)); ! *4.3 ~ ((~ (P -> ~ Q) -> ~ (Q -> ~ P)) -> ~ (~ (R -> ~ S) -> ~ (S -> ~ R))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3D2DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD12D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11DD11DD1D1DD13DD1D1D322DD12D13322D3D2DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD12D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11DD11DD1D1DD13DD1D1D322DD12D133; ! 401 steps ((P v Q) <-> (Q v P)); ! *4.31 ~ (((~ P -> Q) -> (~ Q -> P)) -> ~ ((~ R -> S) -> (~ S -> R))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD1DD13D1D3DD11DD1D1DD13DD1D1D32222D1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222D3DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11DD1D1DD13DD1D1D3222; ! 219 steps (((P ^ Q) ^ R) <-> (P ^ (Q ^ R))); ! *4.32 ~ ((~ (~ (P -> ~ Q) -> R) -> ~ (P -> ~ ~ (Q -> R))) -> ~ (~ (S -> ~ ~ (T -> U)) -> ~ (~ (S -> ~ T) -> U))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD13DD11DD1D13DD11D1DD13D12DD12DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222DD1DD1DD11D11DD1D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD1D1DD13DD11DD1D13DD11D1DD13DD13D1222D3DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12DD11DD11DD1D1DD13DD1D1D3222D1DD1DD1DD1DD13DD11DD1D13DD11D1D12D1DD13DD11DD1D13DD11DD1D1DD13DD13D1222DD11DD1D13DD11D1DD12D12DD1DD11D1DD1DD13DD1D1D322D1DD13D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122222; ! 669 steps (((P v Q) v R) <-> (P v (Q v R))); ! *4.33 ~ (((~ (P -> Q) -> R) -> (P -> (~ Q -> R))) -> ~ ((S -> (~ T -> U)) -> (~ (S -> T) -> U))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3DD1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D12D1D2DD1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D3222DD11DD1D1DD13DD1D1D332222D3DD11DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12DD11DD11DD1D1DD13DD1D1D3222D1DD1DD11DD11DD1D1DD13DD1D1D3222D1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD1DD11DD1D1DD13DD1D1D33222; ! 419 steps ((P <-> Q) -> ((P ^ R) <-> (Q ^ R))); ! *4.36 (~ ((P -> Q) -> ~ (R -> S)) -> ~ ((~ (P -> T) -> ~ (Q -> T)) -> ~ (~ (R -> U) -> ~ (S -> U)))); ! Result of proof DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD11D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD1DD11DD1D1DD13DD1D1D33222DD1DD11D13DD1D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD1DD11D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD1DD11DD1D1DD13DD1D1D3322222; ! 405 steps ((P <-> Q) -> ((P v R) <-> (Q v R))); ! *4.37 (~ ((P -> Q) -> ~ (R -> S)) -> ~ (((~ P -> T) -> (~ Q -> T)) -> ~ ((~ R -> U) -> (~ S -> U)))); ! Result of proof DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11D1D12DD1DD11D13DD1D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD12D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11D1D1222; ! 429 steps (((P <-> R) ^ (Q <-> S)) -> ((P ^ Q) <-> (R ^ S))); ! *4.38 (~ (~ ((P -> Q) -> ~ (R -> S)) -> ~ ~ ((T -> U) -> ~ (V -> W))) -> ~ ((~ (P -> ~ T) -> ~ (Q -> ~ U)) -> ~ (~ (R -> ~ V) -> ~ (S -> ~ W)))); ! Result of proof D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD1D2DD1DD13DD11DD1D13DD11D1DD13D12D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12232DD1D1D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD133DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D1DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1DD1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD1DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D1332D1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1D2DD1DD13DD11DD1D13DD11D1DD13D12D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1332DD1D1D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD133DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D1DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1DD1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD1DD11DD1D13DD11D1D12DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1332D1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132; ! 1423 steps (((P <-> R) ^ (Q <-> S)) -> ((P v Q) <-> (R v S))); ! *4.39 (~ (~ ((P -> Q) -> ~ (R -> S)) -> ~ ~ ((T -> U) -> ~ (V -> W))) -> ~ (((~ P -> T) -> (~ Q -> U)) -> ~ ((~ R -> V) -> (~ S -> W)))); ! Result of proof D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD1D2DD1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1332DD1DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D133DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D12DD11D1DD1D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11D1DD13DD1D1D322DD1331DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1D2DD1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1332DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD1DD123DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D12DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D133DD12D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11D1D12; ! 1033 steps ((P ^ (Q v R)) <-> ((P ^ Q) v (P ^ R))); ! *4.4 ~ ((~ (P -> ~ (Q -> R)) -> (~ ~ (P -> Q) -> ~ (P -> ~ R))) -> ~ ((~ ~ (S -> T) -> ~ (S -> ~ U)) -> ~ (S -> ~ (T -> U)))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12DD1DD11D11DD11DD1D1DD13DD1D1D3222DD11DD1D1DD13DD1D1D3222D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD12DD1DD11D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD1DD11DD11DD1D1DD13DD1D1D3222D1DD1DD11D13DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11D11DD11DD1D1DD13DD1D1D3222D1DD1DD13DD11DD1D13DD11D1DD13D12222D3DD13DD1D1D2DD1DD13DD11DD1D13DD11DD1D1DD13DD13D122DD1DD1DD1DD1DD11D1DD1DD13D1D3DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D133222D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD12DD11DD1D13DD11D1DD13D12D1DD1DD11D13DD1D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D122D1DD1DD13DD11DD1D13DD11D1DD13D1222; ! 885 steps ((P v (Q ^ R)) <-> ((P v Q) ^ (P v R))); ! *4.41 ~ (((P -> ~ (Q -> ~ R)) -> ~ ((P -> Q) -> ~ (P -> R))) -> ~ (~ ((S -> T) -> ~ (S -> U)) -> (S -> ~ (T -> ~ U)))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD1DD11D1DD1DD13D1D3DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D13322DD1DD11D1DD1DD13DD11DD1D13DD11D1DD13D122DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1DD11DD1D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13222D3D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD11DD1D1DD13D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD121DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11D11DD11DD1D1DD13DD1D1D3222D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1323; ! 741 steps (P <-> ((P ^ Q) v (P ^ ~ Q))); ! *4.42 ~ ((P -> (~ ~ (P -> Q) -> ~ (P -> ~ Q))) -> ~ ((~ ~ (R -> S) -> ~ (R -> T)) -> R)); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3D2DD1DD13DD11DD1D13DD11D1DD13D12D1DD1DD1DD1DD13DD11DD1D13DD11D1D12D1DD13DD11DD1D13DD11DD1D1DD13DD13D1222DD11D1DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D1222D3DD1DD11DD11DD1D1DD13DD1D1D3222DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1223DD1DD1DD11D13DD1D1D13DD1D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222; ! 431 steps (P <-> ((P v Q) ^ (P v ~ Q))); ! *4.43 ~ ((P -> ~ ((~ P -> Q) -> ~ (~ P -> R))) -> ~ (~ ((~ S -> T) -> ~ (~ S -> ~ T)) -> S)); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD13DD1DD11D13DD1DD11D1DD1DD13DD11DD1D13DD11D1DD13D122DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1322D3D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD11DD11DD1D1DD13DD1D1D3222D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD12DD11DD11DD1D1DD13DD1D1D322DD12D133; ! 411 steps (P <-> (P v (P ^ Q))); ! *4.44 ~ ((P -> (~ P -> Q)) -> ~ ((~ R -> ~ (R -> S)) -> R)); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD13DD1D1D3322D3DD1DD1DD11D13DD1D1D13DD1D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222; ! 135 steps (P <-> (P ^ (P v Q))); ! *4.45 ~ ((P -> ~ (P -> ~ (~ P -> Q))) -> ~ (~ (R -> S) -> R)); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3D2DD1D2DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1332DD1DD11D13DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1322D3DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D1332; ! 285 steps ((P ^ Q) <-> ~ (~ P v ~ Q)); ! *4.5 ~ ((~ (P -> Q) -> ~ (~ ~ P -> Q)) -> ~ (~ (~ ~ R -> S) -> ~ (R -> S))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD13DD11DD1D13DD11D1DD13D12DD12D1DD13DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122222D3D2DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD12D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12223; ! 349 steps (~ (P ^ Q) <-> (~ P v ~ Q)); ! *4.51 ~ ((~ ~ (P -> Q) -> (~ ~ P -> Q)) -> ~ ((~ ~ R -> S) -> ~ ~ (R -> S))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD1DD13DD1D1D322D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11D1DD1DD13DD11DD1D13DD11D1DD13D1222D3DD1D1DD13DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222DD13DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222; ! 279 steps ((P ^ ~ Q) <-> ~ (~ P v Q)); ! *4.52 ~ ((~ (P -> ~ ~ Q) -> ~ (~ ~ P -> Q)) -> ~ (~ (~ ~ R -> S) -> ~ (R -> ~ ~ S))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD13DD11DD1D13DD11D1DD13D12DD12DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D122D3DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D12DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12DD11DD11DD1D1DD13DD1D1D32222; ! 513 steps (~ (P ^ ~ Q) <-> (~ P v Q)); ! *4.53 ~ ((~ ~ (P -> ~ ~ Q) -> (~ ~ P -> Q)) -> ~ ((~ ~ R -> S) -> ~ ~ (R -> ~ ~ S))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D12DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12DD11DD11DD1D1DD13DD1D1D322222D3DD1DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12DD13DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222; ! 429 steps ((~ P ^ Q) <-> ~ (P v ~ Q)); ! *4.54 ~ ((P -> P) -> ~ (Q -> Q)); ! Result of proof D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD12D1DD13DD1D1D3DD13222D3DD132; ! 69 steps (~ (~ P ^ Q) <-> (P v ~ Q)); ! *4.55 ~ ((~ ~ P -> P) -> ~ (Q -> ~ ~ Q)); ! Result of proof D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD12D1DD1DD13DD1D1D322D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222D3DD13DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222; ! 173 steps ((~ P ^ ~ Q) <-> ~ (P v Q)); ! *4.56 ~ ((~ (P -> ~ ~ Q) -> ~ (P -> Q)) -> ~ (~ (R -> S) -> ~ (R -> ~ ~ S))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD13DD11DD1D13DD11D1DD13D12DD12DD1DD11D1DD1DD13DD1D1D322D1DD13D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122222D3DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD1DD13DD11DD1D13DD11D1DD13D12DD12DD11DD1D1DD1DD13DD1D1D322D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222; ! 401 steps (~ (~ P ^ ~ Q) <-> (P v Q)); ! *4.57 ~ ((~ ~ (P -> ~ ~ Q) -> (P -> Q)) -> ~ ((R -> S) -> ~ ~ (R -> ~ ~ S))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3DD1DD13DD11DD1D13DD11D1DD13D12DD12DD11DD1D1DD1DD13DD1D1D322D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122222D3DD1DD1DD11D1DD1DD13DD1D1D322D1DD13D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222DD13DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222; ! 317 steps ((P -> Q) <-> (~ P v Q)); ! *4.6 ~ (((P -> Q) -> (~ ~ P -> Q)) -> ~ ((~ ~ R -> S) -> (R -> S))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD1DD13DD1D1D322D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12212D3D1DD13DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222; ! 179 steps (~ (P -> Q) <-> (P ^ ~ Q)); ! *4.61 ~ ((~ (P -> Q) -> ~ (P -> ~ ~ Q)) -> ~ (~ (R -> ~ ~ S) -> ~ (R -> S))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13DD1D1D322D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12DD12D1DD1DD13DD11DD1D13DD11D1DD13D12DD12DD11DD1D1DD1DD13DD1D1D322D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222D3DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD1DD13DD11DD1D13DD11D1DD13D12DD12DD1DD11D1DD1DD13DD1D1D322D1DD13D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122222; ! 401 steps ((P -> ~ Q) <-> (~ P v ~ Q)); ! *4.62 ~ (((P -> Q) -> (~ ~ P -> Q)) -> ~ ((~ ~ R -> S) -> (R -> S))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD1DD13DD1D1D322D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12212D3D1DD13DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222; ! 179 steps (~ (P -> ~ Q) <-> (P ^ Q)); ! *4.63 ~ ((P -> P) -> ~ (Q -> Q)); ! Result of proof D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD12D1DD13DD1D1D3DD13222D3DD132; ! 69 steps ((~ P -> Q) <-> (P v Q)); ! *4.64 ~ ((P -> P) -> ~ (Q -> Q)); ! Result of proof D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD12D1DD13DD1D1D3DD13222D3DD132; ! 69 steps (~ (~ P -> Q) <-> (~ P ^ ~ Q)); ! *4.65 ~ ((~ (P -> Q) -> ~ (P -> ~ ~ Q)) -> ~ (~ (R -> ~ ~ S) -> ~ (R -> S))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13DD1D1D322D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12DD12D1DD1DD13DD11DD1D13DD11D1DD13D12DD12DD11DD1D1DD1DD13DD1D1D322D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222D3DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD1DD13DD11DD1D13DD11D1DD13D12DD12DD1DD11D1DD1DD13DD1D1D322D1DD13D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122222; ! 401 steps ((~ P -> ~ Q) <-> (P v ~ Q)); ! *4.66 ~ ((P -> P) -> ~ (Q -> Q)); ! Result of proof D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD12D1DD13DD1D1D3DD13222D3DD132; ! 69 steps (~ (~ P -> ~ Q) <-> (~ P ^ Q)); ! *4.67 ~ ((P -> P) -> ~ (Q -> Q)); ! Result of proof D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD12D1DD13DD1D1D3DD13222D3DD132; ! 69 steps ((P -> Q) <-> (P -> (P ^ Q))); ! *4.7 ~ (((P -> Q) -> (P -> ~ (P -> ~ Q))) -> ~ ((R -> ~ (S -> ~ T)) -> (R -> T))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13DD1D1D322D1DD11D1D2DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1332DD1DD11D13DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222D3DD11DD1D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132; ! 333 steps ((P -> Q) <-> (P <-> (P ^ Q))); ! *4.71 ~ (((P -> Q) -> ~ ((P -> ~ (P -> ~ Q)) -> ~ (~ (R -> S) -> R))) -> ~ (~ ((T -> ~ (U -> ~ V)) -> W) -> (T -> V))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD1DD13D1D3DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D1332D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD121D1DD1DD11D1D2DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1332DD1DD11D13DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222D3D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD11D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D133; ! 557 steps ((P -> Q) <-> (Q <-> (P v Q))); ! *4.72 ~ (((P -> Q) -> ~ ((R -> (S -> R)) -> ~ ((~ P -> Q) -> Q))) -> ~ (~ (T -> ~ ((~ U -> V) -> W)) -> (U -> W))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD1DD13DD1D1D322D1DD13D1DD1DD1DD13DD11DD1D13DD11D1DD13D122DD1D1DD1DD13D1D3DD13DD11DD11DD1D1DD13DD1D1D322DD12D1322D1DD1D12DD1DD1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D12DD11DD1D1DD13DD1D1D3222D1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222D3DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD12D13; ! 387 steps (Q -> (P <-> (P ^ Q))); ! *4.73 (P -> ~ ((Q -> ~ (Q -> ~ P)) -> ~ (~ (R -> S) -> R))); ! Result of proof DD1DD13D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD121D2D2DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1332DD11D1DD13D1D3DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D1332; ! 273 steps (~ P -> (Q <-> (P v Q))); ! *4.74 (P -> ~ ((Q -> (R -> Q)) -> ~ ((P -> S) -> S))); ! Result of proof DD1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1D12DD1DD13D1DD1DD1DD13DD11DD1D13DD11D1DD13D122DD1D1DD1DD13D1D3DD13DD11DD11DD1D1DD13DD1D1D322DD12D13222; ! 151 steps (((P -> Q) ^ (P -> R)) <-> (P -> (Q ^ R))); ! *4.76 ~ ((~ ((P -> Q) -> ~ (P -> R)) -> (P -> ~ (Q -> ~ R))) -> ~ ((S -> ~ (T -> ~ U)) -> ~ ((S -> T) -> ~ (S -> U)))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD11DD1D1DD13D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD121DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11D11DD11DD1D1DD13DD1D1D3222D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132322D3D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD1DD11D1DD1DD13D1D3DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D13322DD1DD11D1DD1DD13DD11DD1D13DD11D1DD13D122DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1DD11DD1D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132; ! 741 steps (((Q -> P) ^ (R -> P)) <-> ((Q v R) -> P)); ! *4.77 ~ ((~ ((P -> Q) -> ~ (R -> Q)) -> ((~ P -> R) -> Q)) -> ~ (((~ S -> T) -> U) -> ~ ((S -> U) -> ~ (T -> U)))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3DD1D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD11D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD1DD123DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D12DD1D1DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11D1D123DD11DD1D1DD13DD1D1D322222D3D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD1D13DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13; ! 609 steps (((P -> Q) v (P -> R)) <-> (P -> (Q v R))); ! *4.78 ~ (((~ (P -> Q) -> (P -> R)) -> (P -> (~ Q -> R))) -> ~ ((S -> (~ T -> U)) -> (~ (V -> T) -> (S -> U)))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3DD1DD11D1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1D12DD1DD11D1DD1D2DD1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D3222DD11DD1D1DD13DD1D1D33221DD11DD1D1DD13DD11DD1D13DD11D1DD13D12222D3DD11D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12DD11DD11DD1D1DD13DD1D1D3222D1D1DD1D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12DD11DD1D1DD13DD1D1D32222; ! 445 steps (((Q -> P) v (R -> P)) <-> ((Q ^ R) -> P)); ! *4.79 ~ (((~ (P -> Q) -> (R -> Q)) -> (~ (P -> ~ R) -> Q)) -> ~ ((~ (S -> ~ T) -> U) -> (~ (S -> V) -> (T -> U)))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3DD1DD1DD11D11DD1D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD1DD1DD11DD11DD1D1DD13DD1D1D3222DD1D1DD13DD11DD1D13DD11D1DD13D12DD11DD1D1DD1DD13D1D3DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D1332DD1212222D3DD1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1D12D1DD1DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D133DD1DD11DD1D13DD11D1D12DD1D1DD13DD11DD1D13DD11DD1D1DD13DD13D1222DD11DD1D13DD11D1D12; ! 561 steps ((P -> ~ P) <-> ~ P); ! *4.8 ~ (((P -> ~ P) -> ~ P) -> ~ (Q -> (R -> Q))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13DD1D1D322D1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222D3DD13DD11DD11DD1D1DD13DD1D1D322DD12D13; ! 155 steps ((~ P -> P) <-> P); ! *4.81 ~ (((~ P -> P) -> P) -> ~ (Q -> (R -> Q))); ! Result of proof D2DD1DD1DD13DD11DD1D13DD11D1DD13D12DD12DD1D1DD13DD1D1D3222D3DD13DD11DD11DD1D1DD13DD1D1D322DD12D13; ! 97 steps (((P -> Q) ^ (P -> ~ Q)) <-> ~ P); ! *4.82 ~ ((~ ((P -> Q) -> ~ (P -> ~ Q)) -> ~ P) -> ~ (~ R -> ~ ((R -> S) -> ~ (R -> T)))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD13D2DD1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D3222DD1D2DD1DD13DD11DD1D13DD11D1DD13D12D1DD1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1D12DD11D1DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12DD1312D3D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12DD11DD11DD1D1DD13DD1D1D3222D1D1D13DD1D1DD1DD13DD11DD1D13DD11D1DD13D122DD1DD11DD11DD1D1DD13DD1D1D3222D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1223; ! 553 steps (((P -> Q) ^ (~ P -> Q)) <-> Q); ! *4.83 ~ ((~ ((P -> Q) -> ~ (~ P -> Q)) -> Q) -> ~ (R -> ~ ((S -> R) -> ~ (T -> R)))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13DD1D1D322D1D2DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1332DD1DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11D1D12D1DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D13322D3D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD1DD13DD1DD11D13DD11D1DD13DD1D1D322DD1DD11D1DD1DD13DD11DD1D13DD11D1DD13D122DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13; ! 501 steps ((P <-> Q) -> ((P -> R) <-> (Q -> R))); ! *4.84 (~ ((P -> Q) -> ~ (R -> S)) -> ~ (((S -> T) -> (R -> T)) -> ~ ((Q -> U) -> (P -> U)))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD11DD1DD13D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD121D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13213; ! 243 steps ((P <-> Q) -> ((R -> P) <-> (R -> Q))); ! *4.85 (~ ((P -> Q) -> ~ (R -> S)) -> ~ (((T -> P) -> (T -> Q)) -> ~ ((U -> R) -> (U -> S)))); ! Result of proof D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12232DD1DD13DD11DD11DD1D1DD11D12DD11D1DD13DD1D1D3DD1D1322DD1DD11D1DD1DD13DD11DD1D13DD11D1DD13D122DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD1DD123DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D12; ! 357 steps ((P <-> Q) -> ((P <-> R) <-> (Q <-> R))); ! *4.86 (~ ((P -> Q) -> ~ (R -> S)) -> ~ ((~ ((S -> T) -> ~ (U -> P)) -> ~ ((R -> T) -> ~ (U -> Q))) -> ~ (~ ((Q -> V) -> ~ (W -> R)) -> ~ ((P -> V) -> ~ (W -> S))))); ! Result of proof D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1332DD1DD11D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12232DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D1DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D133DD1DD11DD1D13DD11D1D12DD1D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D133212DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12232DD1DD11D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12232DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D1DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD1DD1DD13DD11DD1D13DD11D1D12D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D133212; ! 1187 steps (((((P ^ Q) -> R) <-> (P -> (Q -> R))) ^ ((P -> (Q -> R)) <-> (Q -> (P -> R)))) ^ ((Q -> (P -> R)) <-> ((Q ^ P) -> R))); ! *4.87 ~ (~ (~ (((~ (P -> ~ Q) -> R) -> (P -> (Q -> R))) -> ~ ((S -> (T -> U)) -> (~ (S -> ~ T) -> U))) -> ~ ~ (((V -> (W -> X)) -> (W -> (V -> X))) -> ~ ((Y -> (Z -> A)) -> (Z -> (Y -> A))))) -> ~ ~ (((B -> (C -> D)) -> (~ (B -> ~ C) -> D)) -> ~ ((~ (E -> ~ F) -> G) -> (E -> (F -> G))))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD13DD1D1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3DD1DD13DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD1DD1DD1DD13DD11DD1D13DD11D1D12D1DD13DD11DD1D13DD11DD1D1DD13DD13D1222DD11DD1D13DD11D1DD12D1222D3DD1DD1DD11D11DD1D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11DD1D1DD13DD1D1D3322222DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122DD1D1DD1DD13D1D3DD11D1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1D1222D3DD11D1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1D1222DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122DD1D1DD1DD13D1D3DD1DD1DD11D11DD1D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11DD1D1DD13DD1D1D3322222D3DD1DD13DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD1DD1DD1DD13DD11DD1D13DD11D1D12D1DD13DD11DD1D13DD11DD1D1DD13DD13D1222DD11DD1D13DD11D1DD12D12; ! 1085 steps ((P ^ Q) -> (P <-> Q)); ! *5.1 (~ (P -> ~ Q) -> ~ ((R -> Q) -> ~ (S -> P))); ! Result of proof DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD12D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12DD11DD1D1DD13DD1D1D3222DD1DD11DD11DD1D1DD13DD1D1D3222D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1332; ! 237 steps ((P -> Q) v (~ P -> Q)); ! *5.11 (~ (P -> Q) -> (~ P -> R)); ! Result of proof D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D133; ! 69 steps ((P -> Q) v (P -> ~ Q)); ! *5.12 (~ (P -> Q) -> (R -> ~ Q)); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD1DD11DD11DD1D1DD13DD1D1D322DD12D133; ! 127 steps ((P -> Q) v (Q -> P)); ! *5.13 (~ (P -> Q) -> (Q -> R)); ! Result of proof DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13; ! 89 steps ((P -> Q) v (Q -> R)); ! *5.14 (~ (P -> Q) -> (Q -> R)); ! Result of proof DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13; ! 89 steps ((P <-> Q) v (P <-> ~ Q)); ! *5.15 (~ ~ ((P -> Q) -> ~ (R -> S)) -> ~ ((S -> ~ Q) -> ~ (~ R -> P))); ! Result of proof DD1DD1DD13DD11DD1D13DD11D1DD13D122DD13DD1D1D2DD1DD13DD11DD1D13DD11DD1D1DD13DD13D122DD1DD1DD1DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D133DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1DD1DD1D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11DD11DD1D1DD13DD1D1D3222D1DD133D1DD1DD13DD11DD1D13DD11D1DD13D1222; ! 433 steps ~ ((P <-> Q) ^ (P <-> ~ Q)); ! *5.16 ~ ~ (~ ((P -> Q) -> ~ (Q -> P)) -> ~ ~ ((P -> ~ Q) -> ~ (~ Q -> P))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222D3DD1D2DD1DD13DD11DD1D13DD11D1DD13D12D1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD12D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD11DD11DD1D1DD13DD1D1D3222DD1DD11D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD1DD11DD11DD1D1DD13DD1D1D3222D1DD1DD11D13DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11D11DD11DD1D1DD13DD1D1D3222D1D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11D1DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD11DD11DD1D1DD13DD1D1D322DD12D13DD11D1DD13DD1D1D3223DD13DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222; ! 767 steps (((P v Q) ^ ~ (P ^ Q)) <-> (P <-> ~ Q)); ! *5.17 ~ ((~ ((~ P -> Q) -> ~ ~ ~ R) -> ~ (R -> ~ (~ Q -> P))) -> ~ (~ (S -> ~ (~ T -> U)) -> ~ ((~ U -> T) -> ~ ~ ~ S))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD12D1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12DD11DD11DD1D1DD13DD1D1D3222D1DD13D122DD11DD11DD1D1DD13DD1D1D322DD12D13D1DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11DD1D1DD13DD1D1D32222D3DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13DD11DD1D13DD11D1DD13D12DD12DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11DD1D1DD13DD1D1D3222DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222; ! 659 steps ((P <-> Q) <-> ~ (P <-> ~ Q)); ! *5.18 ~ ((~ ((P -> Q) -> ~ (Q -> P)) -> ~ ~ ((P -> ~ Q) -> ~ (~ Q -> P))) -> ~ (~ ~ ((R -> ~ S) -> ~ (~ T -> U)) -> ~ ((U -> S) -> ~ (T -> R)))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD1DD13DD1D1D322D1DD13D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222D1D2DD1DD13DD11DD1D13DD11D1DD13D12D1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD12D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD11DD11DD1D1DD13DD1D1D3222DD1DD11D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD1DD11DD11DD1D1DD13DD1D1D3222D1DD1DD11D13DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11D11DD11DD1D1DD13DD1D1D3222D1D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11D1DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD11DD11DD1D1DD13DD1D1D322DD12D13DD11D1DD13DD1D1D32232D3D2DD1DD13DD11DD1D13DD11DD1D1DD13DD13D122DD1DD1DD1DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D133DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1DD1DD1D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11DD11DD1D1DD13DD1D1D3222D1DD133D1DD1DD13DD11DD1D13DD11D1DD13D122; ! 1161 steps ~ (P <-> ~ P); ! *5.19 ~ ~ ((P -> ~ P) -> ~ (~ P -> P)); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222D3DD13DD1D1DD1DD13DD11DD1D13DD11D1DD13D12DD12DD12DD1DD13D12DD1D1DD1DD13DD11DD1D13DD11D1DD13D12DD12D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122222; ! 209 steps ((~ P ^ ~ Q) -> (P <-> Q)); ! *5.21 (~ (~ P -> ~ ~ Q) -> ~ ((P -> R) -> ~ (Q -> S))); ! Result of proof DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD12D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11DD1D1DD1DD13DD1D1D322D1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D13DD1DD11DD1D13DD11D1DD13D12DD11DD1D1DD13D12DD12322; ! 285 steps (~ (P <-> Q) <-> ((P ^ ~ Q) v (Q ^ ~ P))); ! *5.22 ~ ((~ ~ ((P -> Q) -> ~ (R -> S)) -> (~ ~ (P -> ~ ~ Q) -> ~ (R -> ~ ~ S))) -> ~ ((~ ~ (T -> ~ ~ U) -> ~ (V -> ~ ~ W)) -> ~ ~ ((T -> U) -> ~ (V -> W)))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3DD1DD1DD13DD11DD1D13DD11D1DD13D12DD12D1DD1DD13DD11DD1D13DD11D1DD13D12DD12DD11DD1D1DD1DD13DD1D1D322D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD11DD1D1DD1DD13DD1D1D322D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12DD12D1DD1DD13DD11DD1D13DD11D1DD13D12DD12DD11DD1D1DD1DD13DD1D1D322D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222222D3DD1DD1D1DD1DD1DD11D1DD1DD13DD1D1D322D1DD13D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222DD13DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222DD11DD1D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD13DD11DD1D13DD11D1DD13D12DD12DD1DD11D1DD1DD13DD1D1D322D1DD13D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122222DD13DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222; ! 813 steps ((P <-> Q) <-> ((P ^ Q) v (~ P ^ ~ Q))); ! *5.23 ~ ((~ ((P -> Q) -> ~ (Q -> P)) -> (~ ~ (P -> ~ Q) -> ~ (~ P -> ~ ~ Q))) -> ~ ((~ ~ (R -> ~ S) -> ~ (~ T -> ~ ~ U)) -> ~ ((T -> S) -> ~ (U -> R)))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3DD1D2DD1DD13DD11DD1D13DD11D1DD13D12D1DD1DD1D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11D1DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD11DD11DD1D1DD13DD1D1D322DD12D13DD11D1DD13DD1D1D3223DD11DD1D1DD13D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD121DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11D11DD11DD1D1DD13DD1D1D3222D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD12D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD11DD11DD1D1DD13DD1D1D3222D1DD1DD13DD11DD1D13DD11D1DD13D12222D3DD1D1DD13DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD1DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD133DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1DD1DD1D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11DD11DD1D1DD13DD1D1D322DD12D13D1DD13DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD11DD11DD1D1DD13DD1D1D322DD12D13; ! 1215 steps (~ ((P ^ Q) v (~ P ^ ~ Q)) <-> ((P ^ ~ Q) v (Q ^ ~ P))); ! *5.24 ~ ((~ (~ ~ (P -> ~ Q) -> ~ (~ P -> ~ ~ Q)) -> (~ ~ (P -> ~ ~ Q) -> ~ (Q -> ~ ~ P))) -> ~ ((~ ~ (R -> ~ S) -> ~ (T -> ~ ~ U)) -> ~ (~ ~ (U -> S) -> ~ (~ R -> ~ ~ T)))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3DD1D2DD1DD13DD11DD1D13DD11D1DD13D12D1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1D12DD11DD1D1DD13D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD121DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11D11DD11DD1D1DD13DD1D1D3222D1DD1DD13DD11DD1D13DD11DD1D1DD13DD13D122DD1DD1DD11D13DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11D11DD11DD1D1DD13DD1D1D3222DD1DD11D1DD1DD13DD1D1D322D1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222D1DD1DD13DD11DD1D13DD11D1DD13D12DD12DD11DD1D1DD1DD13DD1D1D322D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122222D3DD1D1DD13DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD1DD1DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD11DD11DD1D1DD13DD1D1D322DD12D13D1DD13DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD11DD11DD1D1DD13DD1D1D322DD12D13D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD12DD11DD1D13DD11D1DD13D12D1DD1D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11DD1D1DD1DD13DD1D1D322D1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D13DD1DD11DD1D13DD11D1DD13D12DD11DD1D1DD13D12DD1232; ! 1367 steps ((P v Q) <-> ((P -> Q) -> Q)); ! *5.25 ~ (((~ P -> Q) -> ((P -> Q) -> Q)) -> ~ (((R -> S) -> T) -> (~ R -> T))); ! Result of proof D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122DD1D1DD1DD13D1D3DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11DD11DD1D1DD13DD1D1D3222D1D1222D3D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122; ! 199 steps (((P ^ Q) -> R) <-> ((P ^ Q) -> (P ^ R))); ! *5.3 ~ (((~ (P -> Q) -> R) -> (~ (P -> Q) -> ~ (P -> ~ R))) -> ~ ((S -> ~ (T -> ~ U)) -> (S -> U))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3DD11DD1D1DD11D13DD1D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD11DD1D1DD13DD1D1D3DD1232DD12222D3DD11DD1D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132; ! 301 steps ((R ^ (P -> Q)) -> (P -> (Q ^ R))); ! *5.31 (~ (P -> ~ (Q -> R)) -> (Q -> ~ (R -> ~ P))); ! Result of proof D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13321D1DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D133D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD121; ! 255 steps ((P -> (Q <-> R)) <-> ((P ^ Q) <-> (P ^ R))); ! *5.32 ~ (((P -> ~ ((Q -> R) -> ~ (S -> T))) -> ~ ((~ (P -> ~ Q) -> ~ (P -> ~ R)) -> ~ (~ (P -> ~ S) -> ~ (P -> ~ T)))) -> ~ (~ ((~ (U -> ~ V) -> ~ (W -> ~ X)) -> ~ (~ (U -> ~ Y) -> ~ (Z -> ~ A))) -> (U -> ~ ((V -> X) -> ~ (Y -> A))))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD1DD1DD1DD1DD1DD11D13DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11D1DD13DD1D1D3222DD1DD11D11DD11DD1D1DD1DD13DD1D1D322D1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11DD1D1DD13DD1D1D3322D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1322DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1DD1DD1DD1DD11DD1D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132D1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD11DD1D1DD13DD1D1D33222DD1DD11D11DD11DD1D1DD1DD13DD1D1D322D1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11DD1D1DD13DD1D1D3322D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132222D3D2DD1DD13DD11DD1D13DD11D1DD13D12D1DD1DD1DD1DD1D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD11D13DD11D1DD13DD1D1D3223DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD11D1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1D12DD1DD11D1DD1DD13D1D3DD11DD11DD1D1DD13DD1D1D322DD12D1322DD11DD1D1DD13D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD121DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11D11DD11DD1D1DD13DD1D1D3222D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD12DD11DD11DD1D1DD13DD1D1D322DD12D13DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD11D1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1D12DD1DD11D1DD1DD13D1D3DD11DD11DD1D1DD13DD1D1D322DD12D1322; ! 1801 steps ((P ^ (Q -> R)) <-> (P ^ ((P ^ Q) -> R))); ! *5.33 ~ ((~ (P -> ~ (Q -> R)) -> ~ (P -> ~ (~ (S -> ~ Q) -> R))) -> ~ (~ (T -> ~ (~ (T -> ~ U) -> V)) -> ~ (T -> ~ (U -> V)))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD1DD13DD11DD1D13DD11D1DD13D122DD1DD11D13DD1D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132D1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13222D3DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD1DD13DD11DD1D13DD11D1DD13D12DD12DD1DD11D1DD1DD1DD1DD1DD1DD13DD11DD1D13DD11D1D12D1DD13DD11DD1D13DD11DD1D1DD13DD13D1222DD11DD1D13DD11D1D12DD1DD11DD1D1DD13DD1D1D3322D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1322DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12222; ! 691 steps (((P -> Q) ^ (P -> R)) -> (P -> (Q <-> R))); ! *5.35 (~ ((P -> Q) -> ~ (P -> R)) -> (P -> ~ ((S -> R) -> ~ (T -> Q)))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD1DD11DD1D1DD1DD13D1D3DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD1DD13D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD121D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1322DD1DD11D11DD11DD1D1DD1DD13DD1D1D322D1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1323; ! 433 steps ((P ^ (P <-> Q)) <-> (Q ^ (P <-> Q))); ! *5.36 ~ ((~ (P -> ~ ~ ((P -> Q) -> R)) -> ~ (Q -> ~ ~ ((P -> Q) -> R))) -> ~ (~ (S -> ~ ~ (T -> ~ (S -> U))) -> ~ (U -> ~ ~ (T -> ~ (S -> U))))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3D2DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D11DD1DD13D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11D13DD11D1DD13DD1D1D322322D3D2DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD1D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD12DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13213; ! 541 steps ((P -> (P -> Q)) <-> (P -> Q)); ! *5.4 ~ (((P -> (P -> Q)) -> (P -> Q)) -> ~ (R -> (S -> R))); ! Result of proof D2DD1DD1DD13DD11DD1D13DD11D1DD13D12DD12DD1D1DD1DD13DD1D1D322D1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222D3DD13DD11DD11DD1D1DD13DD1D1D322DD12D13; ! 155 steps (((P -> Q) -> (P -> R)) <-> (P -> (Q -> R))); ! *5.41 ~ ((((P -> Q) -> (R -> S)) -> (R -> (Q -> S))) -> ~ ((T -> (U -> V)) -> ((T -> U) -> (T -> V)))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD11D1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1D1222D3DD1DD11D11DD11DD1D1DD1DD13DD1D1D322D1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222; ! 247 steps ((P -> (Q -> R)) <-> (P -> (Q -> (P ^ R)))); ! *5.42 ~ (((P -> (Q -> R)) -> (P -> (Q -> ~ (P -> ~ R)))) -> ~ ((S -> (T -> ~ (U -> ~ V))) -> (S -> (T -> V)))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13DD1D1D322D1DD11D1DD1DD13DD11DD1D13DD11D1DD13D12D1DD11D1DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D122D3DD11DD1D1DD1DD13D1D3DD11DD1D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13222; ! 349 steps ((P -> Q) -> ((P -> R) <-> (P -> (Q ^ R)))); ! *5.44 ((P -> Q) -> ~ (((P -> R) -> (P -> ~ (Q -> ~ R))) -> ~ ((S -> ~ (T -> ~ U)) -> (S -> U)))); ! Result of proof DD1DD11DD1D1DD13D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD121DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11D11DD11DD1D1DD13DD1D1D3222D2D2DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1332DD11D1DD13D1D3DD11DD1D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132; ! 415 steps (P -> ((P -> Q) <-> Q)); ! *5.5 (P -> ~ (((P -> Q) -> Q) -> ~ (R -> (S -> R)))); ! Result of proof DD1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1D12DD1DD1DD1DD13DD11DD1D13DD11D1D12D1DD13DD11DD1D13DD11DD1D1DD13DD13D1222DD1DD1DD11D1DD13D1D3DD13DD11DD11DD1D1DD13DD1D1D322DD12D1322; ! 181 steps (P -> (Q <-> (P <-> Q))); ! *5.501 (P -> ~ ((Q -> ~ ((R -> Q) -> ~ (S -> P))) -> ~ (~ ((P -> T) -> U) -> T))); ! Result of proof D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD1DD13D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD121D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1DD1DD13DD11DD1D13DD11D1D12DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11DD1D1DD13DD1D1D33222; ! 453 steps ((((P v Q) v R) -> S) <-> (((P -> S) ^ (Q -> S)) ^ (R -> S))); ! *5.53 ~ ((((~ (~ P -> Q) -> R) -> S) -> ~ (~ ((P -> S) -> ~ (Q -> S)) -> ~ (R -> S))) -> ~ (~ (~ ((T -> U) -> ~ (V -> U)) -> ~ (W -> U)) -> ((~ (~ T -> V) -> W) -> U))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD1DD1D13D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD1D13DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1322D3DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12D1DD1DD1D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD11D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD1DD123DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D12DD1D1DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11D1D123DD1D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD11DD1D1DD13DD1D1D3DD1232DD122DD11DD11D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD1DD123DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D12DD1233DD11DD1D1DD13DD1D1D3222; ! 1117 steps (((P ^ Q) <-> P) v ((P ^ Q) <-> Q)); ! *5.54 (~ ~ ((P -> Q) -> ~ (R -> ~ (R -> ~ S))) -> ~ ((~ (T -> ~ U) -> U) -> ~ (S -> P))); ! Result of proof DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD12D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11DD11DD1D1DD13DD1D1D322DD12D13D1DD13D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD121DD1DD13D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1322; ! 383 steps (((P v Q) <-> P) v ((P v Q) <-> Q)); ! *5.55 (~ ~ (((~ P -> Q) -> P) -> ~ (R -> (~ R -> S))) -> ~ ((T -> Q) -> ~ (U -> (V -> U)))); ! Result of proof DD1DD1DD13DD11DD1D13DD11D1DD13D12DD12DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12DD1DD11D11DD11DD1D1DD13DD1D1D3222DD11DD1D1DD13DD1D1D3222DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D1D33DD1DD1DD1DD13DD11DD1D13DD11D1D12D1DD13DD11DD1D13DD11DD1D1DD13DD13D1222DD1DD1DD11D1DD13D1D3DD13DD11DD11DD1D1DD13DD1D1D322DD12D1322; ! 317 steps (((P ^ ~ Q) -> R) <-> (P -> (Q v R))); ! *5.6 ~ (((~ (P -> ~ Q) -> R) -> (P -> (Q -> R))) -> ~ ((S -> (T -> U)) -> (~ (S -> ~ T) -> U))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3DD1DD13DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD1DD1DD1DD13DD11DD1D13DD11D1D12D1DD13DD11DD1D13DD11DD1D1DD13DD13D1222DD11DD1D13DD11D1DD12D1222D3DD1DD1DD11D11DD1D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11DD1D1DD13DD1D1D33222; ! 407 steps (((P v Q) ^ ~ Q) <-> (P ^ ~ Q)); ! *5.61 ~ ((~ ((~ P -> Q) -> ~ ~ Q) -> ~ (P -> ~ ~ Q)) -> ~ (~ (R -> S) -> ~ ((~ R -> T) -> S))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD13DD11DD1D13DD11D1DD13D12DD12D2DD1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D3222DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12DD1DD11D11DD11DD1D1DD13DD1D1D3222DD11D1D122D3D2DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD12D133; ! 421 steps (((P ^ Q) v ~ Q) <-> (P v ~ Q)); ! *5.62 ~ (((~ ~ (P -> Q) -> R) -> (~ P -> R)) -> ~ ((~ S -> T) -> (~ ~ (S -> T) -> T))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD1DD1DD13DD1D1D322D1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122312D3DD11DD1DD1D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11DD11DD1D1DD13DD1D1D3222D1DD1DD1DD13DD11DD1D13DD11D1DD13D122D12; ! 303 steps ((P v Q) <-> (P v (~ P ^ Q))); ! *5.63 ~ (((P -> Q) -> (P -> ~ (P -> ~ Q))) -> ~ ((R -> ~ (S -> ~ T)) -> (R -> T))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13DD1D1D322D1DD11D1D2DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1332DD1DD11D13DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222D3DD11DD1D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132; ! 333 steps (((P v R) <-> (Q v R)) <-> (R v (P <-> Q))); ! *5.7 ~ ((~ (((~ P -> Q) -> (~ R -> S)) -> ~ ((~ T -> U) -> (~ V -> S))) -> (~ S -> ~ ((P -> R) -> ~ (T -> V)))) -> ~ ((~ W -> ~ ((X -> Y) -> ~ (Z -> A))) -> ~ (((~ X -> W) -> (~ Y -> W)) -> ~ ((~ Z -> W) -> (~ A -> W))))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3D2DD1DD13DD11DD1D13DD11D1DD13D12D1DD1DD1DD1DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D133DD12D13DD11D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12DD1DD11D11DD11DD1D1DD13DD1D1D3222DD11DD1D1DD13DD1D1D3222DD11DD1D1DD13D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD121DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11D11DD11DD1D1DD13DD1D1D3222D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD12D13DD11D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12DD1DD11D11DD11DD1D1DD13DD1D1D3222DD11DD1D1DD13DD1D1D322222D3D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD1DD1DD11DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1223DD11DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D12DD1D1DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11DD1D1DD13DD1D1D3222DD11DD1D1DD1DD1DD13D1D3DD11DD1D1DD13DD1D1D32222D1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1DD1DD11DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D133DD11DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D12DD1D1DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11DD1D1DD13DD1D1D3222DD11DD1D1DD1DD1DD13D1D3DD11DD1D1DD13DD1D1D32222D1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222; ! 1487 steps ((Q -> ~ R) -> (((P v Q) ^ R) <-> (P ^ R))); ! *5.71 ((P -> ~ Q) -> ~ ((~ ((~ R -> P) -> ~ Q) -> ~ (R -> ~ Q)) -> ~ (~ (S -> T) -> ~ ((~ S -> U) -> T)))); ! Result of proof DD1DD1DD1D12DD1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D12D1DD13DD11DD1D13DD11D1D12DD1DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11D1D12DD1D1DD13D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD121DD1D1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13322D2D2DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1332DD11D1DD13D1D3D2DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD12D133; ! 551 steps ((P -> (Q <-> R)) <-> ((P -> Q) <-> (P -> R))); ! *5.74 ~ (((P -> ~ ((Q -> R) -> ~ (S -> T))) -> ~ (((P -> Q) -> (P -> R)) -> ~ ((P -> S) -> (P -> T)))) -> ~ (~ (((U -> V) -> (W -> X)) -> ~ ((Y -> Z) -> (W -> A))) -> (W -> ~ ((V -> X) -> ~ (Z -> A))))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD1DD11DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1223DD11DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D12DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1DD11DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D133DD11DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D1222D3D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12232DD1DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD11D1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1D12DD11DD1D1DD13D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD121DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11D11DD11DD1D1DD13DD1D1D3222D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD11D1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1D12; ! 1049 steps (((R -> ~ Q) ^ (P <-> (Q v R))) -> ((P ^ ~ Q) <-> R)); ! *5.75 (~ ((P -> Q) -> ~ ~ ((R -> (S -> T)) -> ~ ((U -> P) -> V))) -> ~ ((~ (R -> ~ S) -> T) -> ~ (P -> ~ (V -> ~ Q)))); ! Result of proof D2DD1DD1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1332DD1DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D1332DD1DD1DD11D11DD1D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11DD1D1DD13DD1D1D33222DD1DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1D2DD1DD13DD11DD1D13DD11D1DD13D12D1DD1DD1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD1DD11DD1D13DD11D1D12DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1332DD1D1D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D3223DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D1DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D1332; ! 1007 steps (((((P -> Q) -> (~ R -> ~ S)) -> R) -> T) -> ((T -> P) -> (S -> P))); ! Meredith's axiom (((((P -> Q) -> (~ R -> ~ S)) -> R) -> T) -> ((T -> P) -> (S -> P))); ! Result of proof DD11DD11DD1D1DD1DD13D1D3D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12DD11DD11DD1D1DD13DD1D1D3222DD11D1DD1DD13DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11DD11DD1D1DD13DD1D1D32221DD1DD11D13DD11D1DD13DD1D1D32222; ! 271 steps (((P -> Q) -> P) -> P); ! Peirce's axiom (((P -> Q) -> P) -> P); ! Result of proof DD1D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222; ! 53 steps (((P <-> Q) <-> R) <-> (P <-> (Q <-> R))); ! biass ~ ((~ ((~ ((P -> Q) -> ~ (R -> S)) -> T) -> ~ (U -> ~ ((S -> V) -> ~ (R -> P)))) -> ~ ((S -> ~ ((Q -> T) -> ~ (U -> V))) -> ~ (~ ((R -> U) -> ~ (T -> R)) -> P))) -> ~ (~ ((W -> ~ ((X -> Y) -> ~ (Z -> A))) -> ~ (~ ((X -> Z) -> ~ (Y -> B)) -> C)) -> ~ ((~ ((C -> X) -> ~ (X -> W)) -> Y) -> ~ (Z -> ~ ((W -> A) -> ~ (B -> C)))))); ! Result of proof D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D122D1DD1DD13D1D3D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD1D2DD1DD13DD11DD1D13DD11D1DD13D12D1DD1DD1DD1DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D133DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D12D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD1DD13D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD121D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD11DD1D1DD13D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD121DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11D11DD11DD1D1DD13DD1D1D3222D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1321D1DD1DD13DD11DD1D13DD11D1D12DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11DD1D1DD13DD1D1D33222DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1DD1D2DD1DD13DD11DD1D13DD11D1DD13D12D1DD1DD1DD1DD13DD11DD1D13DD11D1D12D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12232DD11D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD1DD11DD11DD1D1DD13DD1D1D3222D1DD1DD11D1DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D12D1DD1DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D133DD121D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD11DD1D1DD1DD13D1D3D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD1DD11DD11DD1D1DD13DD1D1D3222DD1DD11DD1D1DD1DD1DD13D1D3DD11DD11DD1D1DD13DD1D1D322DD12D132D1D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1222D1DD13DD11DD1D13DD11D1DD13D12DD1DD11D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12DD11DD11DD1D1DD13DD1D1D3222D1D1D132DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11DD11DD1D1DD13DD1D1D3222D1D12D1DD1DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D133DD121DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13322222D3D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD1DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D1332DD1DD11D1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D12232DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D1DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D133DD1DD11DD1D13DD11D1D12DD1D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD1DD13DD11DD11DD1D1DD13DD1D1D322DD12D133212DD11DD1D1DD1DD13D1D3D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD1DD1DD1DD1D2DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1D1DD13DD11D1332D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD1DD1DD1DD13DD11DD1D13DD11D1D12D1DD13DD11DD1D13DD11DD1D1DD13DD13D1222DD11DD1D13DD11D1D12DD1D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD11DD11DD1D1DD13DD1D1D3222D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D132DD11DD1D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D1223222DD1DD13DD11DD1D13DD11D1DD12D12DD1D1DD13DD11DD1D13DD11D1DD13D12DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1D2DD1DD13DD11DD1D13DD11D1DD13D12D1DD1DD1DD1D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD11D1DD1DD13DD1D1D322D1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D133DD11D1DD13DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1D12DD11DD1D1DD13D2DD1DD1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122D1DD13DD1DD11D13DD11D1DD13DD1D1D322DD121DD1DD11D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD11D1DD13D122DD1DD11D11DD11DD1D1DD13DD1D1D3222D1DD1DD1DD13DD11DD1D13DD11D1DD13D12DD1D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13DD1DD123DD1DD11D13DD1DD11DD11DD1D1DD13DD1D1D3222D1DD11D12D1DD1DD1DD13DD1DD11D13DD11D1DD13DD1D1D322DD1DD11D1DD1DD13DD11DD1D13DD11D1DD13D122DD1DD11DD11DD1D1DD13DD1D1D3222D1DD13D12D1DD13DD11DD11DD1D1DD13DD1D1D322DD12D13; ! 4129 steps