diff --git a/pmproofs.txt b/pmproofs.txt index c6545a0..2db9637 100644 --- a/pmproofs.txt +++ b/pmproofs.txt @@ -13,6 +13,9 @@ Created and maintained by Norman Megill http://us.metamath.org/email.html Revision history: +15-Jun-2024: Samiro Discher (SD) found shorter proofs for 40 theorems with + the proof compression feature '--transform -z' of his software tool + pmGenerator (version 1.2.1). 17-Apr-2023: Shorter proofs of *3.44, *4.77, *4.85, *4.86, and biass were found by Samiro Discher (SD). In addition, eliminated (sub-)proofs by lexicographically smaller @@ -326,10 +329,10 @@ D2D1DD2D13D2D1D3DD2DD2D13DD2D1311; ! 33 steps DD2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D1DD2D1DD22D11DD2D112D2D1DD2D13D 2D1D3DD2DD2D13DD2D1311; ! 91 steps -(((P v Q) v R) -> (P v (Q v R))); ! *2.32 +(((P v Q) v R) -> (P v (Q v R))); ! *2.32 (SD 91->83) ((~ (P -> Q) -> R) -> (P -> (~ Q -> R))); ! Result of proof -DD2D1D2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D1DD2D1DD22D11DD2D112DD2D13D -2D1D3DD2DD2D13DD2D1311; ! 91 steps +DD2DD2D12DD2D11DD2D121D1DD2D13DD2D1D2D1D3DD2DD2D13DD2D1311DD2D1D2DD2D +D2D13DD2D13111; ! 83 steps ((Q -> R) -> ((P v Q) -> (R v P))); ! *2.36 ((P -> Q) -> ((~ R -> P) -> (~ Q -> R))); ! Result of proof @@ -558,10 +561,10 @@ D3DD2D1D3DD2DD2D13DD2D1311DD2D131; ! 33 steps (~ (P -> ~ Q) -> Q); ! Result of proof D3DD2D1D3DD2DD2D13DD2D13111; ! 27 steps -(((P ^ Q) -> R) -> (P -> (Q -> R))); ! *3.3 Exp (GB 63->59) +(((P ^ Q) -> R) -> (P -> (Q -> R))) +; ! *3.3 Exp (GB 63->59) (SD 59->55) ((~ (P -> ~ Q) -> R) -> (P -> (Q -> R))); ! Result of proof -DD2D1D2DD2D1DD2D1D2DD2D1211DD2D13DD2D1D2DD2DD2D13DD2D131111 -; ! 59 steps +DD2DD2D12DD2D11DD2D121D1DD2D13DD2D1D2DD2DD2D13DD2D13111; ! 55 steps ((P -> (Q -> R)) -> ((P ^ Q) -> R)); ! *3.31 Imp (SD 103->83) ((P -> (Q -> R)) -> (~ (P -> ~ Q) -> R)); ! Result of proof @@ -569,15 +572,15 @@ DD2DD2D12DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D1311DD2D131D1D3DD2D1D3DD2D D2D13DD2D13111; ! 83 steps (((P -> Q) ^ (Q -> R)) -> (P -> R)) -; ! *3.33 Syll (GB 113->105) (SF 105->95) +; ! *3.33 Syll (GB 113->105) (SF 105->95) (SD 95->73) (~ ((P -> Q) -> ~ (Q -> R)) -> (P -> R)); ! Result of proof -D3DD2D1D3DD2DD2D13DD2D1311DD2D1D2DD2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD -2D1D2DD2D12DD2D13DD2D13111; ! 95 steps +DD2DD2D12DD2D13DD2D1DD22D11DD2D11DD2D131D3DD2D1D3DD2DD2D13DD2D1311DD2 +D131; ! 73 steps -(((Q -> R) ^ (P -> Q)) -> (P -> R)); ! *3.34 Syll +(((Q -> R) ^ (P -> Q)) -> (P -> R)); ! *3.34 Syll (SD 105->73) (~ ((P -> Q) -> ~ (R -> P)) -> (R -> Q)); ! Result of proof -D3DD2D1D3DD2DD2D13DD2D1311DD2D1D2DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2 -D1311D2D1D3DD2DD2D13DD2D1311DD2D1211; ! 105 steps +DD2DD2D12DD2D13DD2D1DD22D1DD2D131DD2D11DD2D131D3DD2D1D3DD2DD2D13DD2D1 +3111; ! 73 steps ((P ^ (P -> Q)) -> Q); ! *3.35 Ass (GB 93->63) (~ (P -> ~ (P -> Q)) -> Q); ! Result of proof @@ -604,18 +607,18 @@ DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D1311DD2D131; ! 45 steps DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D13111; ! 39 steps (((P -> Q) ^ (P -> R)) -> (P -> (Q ^ R))) -; ! *3.43 Comp (SF 143->139) (RR 139->137) (SD 137->117) +; ! *3.43 Comp (SF 143->139) (RR 139->137) (SD 137->109) (~ ((P -> Q) -> ~ (P -> R)) -> (P -> ~ (Q -> ~ R))) ; ! Result of proof -DD2DD2D12DD2D1D2D13DD2D1D2D1D2DD2DD2D13DD2D1311DD2D1D2D11D3DD2D1D3DD2 -DD2D13DD2D1311DD2D131D3DD2D1D3DD2DD2D13DD2D13111; ! 117 steps +DD2DD2D1DD2D12D2D1DD2D13DD2D1D2DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13DD +2D1311DD2D131D3DD2D1D3DD2DD2D13DD2D13111; ! 109 steps (((Q -> P) ^ (R -> P)) -> ((Q v R) -> P)) -; ! *3.44 (RR 271->203) (SD 203->181) +; ! *3.44 (RR 271->203) (SD 203->161) (~ ((P -> Q) -> ~ (R -> Q)) -> ((~ P -> R) -> Q)); ! Result of proof -DD2DD2D12DD2D1D2D13DD2D1D2D1D2DD2D131DD2DD2D12DD2D11DD2D1DD2D121D3DD2 -D1D3DD2DD2D13DD2D1311DD2D131DD2D1D2D13DD2D1D2D1D2D1D3DD2DD2D13DD2D131 -1DD2D12DD2D13DD2D1DD22D11DD2D11DD2D131D1D11; ! 181 steps +DD2D1D2D1DD2DD2D13D2DD2D1311DD2DD2D12DD2D11DD2D12DD2D13DD2D1DD22D1DD2 +D131DD2D11DD2D131DD2D1D2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D12DD2D13DD +2D1DD22D11DD2D11DD2D131; ! 161 steps ((P -> Q) -> ((P ^ R) -> (Q ^ R))) ; ! *3.45 Fact (GB 79->71) (SF 71->61) @@ -623,22 +626,22 @@ D1D3DD2DD2D13DD2D1311DD2D131DD2D1D2D13DD2D1D2D1D2D1D3DD2DD2D13DD2D131 DD2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D1D2DD2D12DD2D13DD2D1311 ; ! 61 steps -(((P -> R) ^ (Q -> S)) -> ((P ^ Q) -> (R ^ S))); ! *3.47 +(((P -> R) ^ (Q -> S)) -> ((P ^ Q) -> (R ^ S))) +; ! *3.47 (SD 203->199) (~ ((P -> Q) -> ~ (R -> S)) -> (~ (P -> ~ R) -> ~ (Q -> ~ S))) ; ! Result of proof -DD2DD2D1DD2D12D2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1DD2DD2D121D1D3D -D2D1D3DD2DD2D13DD2D1311DD2D131D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2D1D -D2DD2D121D1D3DD2D1D3DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13DD2D13111 -; ! 203 steps +DD2DD2D1DD2D12D2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2DD2D12DD2D13DD2D1 +DD22D1DD2D131DD2D11DD2D131D1D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2DD2D1 +2DD2D13DD2D1DD22D11DD2D11DD2D131D1D3DD2D1D3DD2DD2D13DD2D13111 +; ! 199 steps (((P -> R) ^ (Q -> S)) -> ((P v Q) -> (R v S))) -; ! *3.48 (GB 245->241) +; ! *3.48 (GB 245->241) (SD 241->171) (~ ((P -> Q) -> ~ (R -> S)) -> ((~ P -> R) -> (~ Q -> S))) ; ! Result of proof -DD2D1D2DD2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D1DD2D1DD22D11DD2D112DD2D -1D2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311DD2D1 -DD2DD2D121D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D13 -11DD2D1D2D1DD2D1D2DD2D1211DD2D1211; ! 241 steps +DD2D1D2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2DD2D12DD2D11DD2D12DD2D13DD2D +1DD22D1DD2D131DD2D11DD2D131DD2D1D2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D +12DD2D13DD2D1DD22D11DD2D11DD2D131; ! 171 steps ((P -> Q) <-> (~ Q -> ~ P)); ! *4.1 ~ (((P -> Q) -> (~ Q -> ~ P)) -> ~ ((~ R -> ~ S) -> (S -> R))) @@ -674,23 +677,22 @@ DD3DD2DD2DD2D13DD2D1311D1D3DD2DD2D13DD2D1311DD2DD2D13DD2D1311 ; ! 61 steps (((P ^ Q) -> R) <-> ((P ^ ~ R) -> ~ Q)) -; ! *4.14 (GB 325->321) (SD 321->283) +; ! *4.14 (GB 325->321) (SD 321->263) ~ (((~ (P -> ~ Q) -> R) -> (~ (P -> ~ ~ R) -> ~ Q)) -> ~ ((~ (S -> ~ ~ T) -> U) -> (~ (S -> U) -> T))); ! Result of proof DD3DD2DD2DD2D13DD2D1311D1DD2D1DD2D13D2DD2D1DD2D1D2D1DD2D1D3DD2DD2D13D D2D1311D2D1D3DD2DD2D13DD2D1311DD2D1DD2D1D2DD2D1211D2DD2D13DD2D1D2DD2D -D2D13DD2D13111DD2D13DD2D1311DD2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D1DD -2D1DD22D11DD2D112DD2D1D2DD2D1DD2D1D2DD2D1211DD2D13DD2D1D2DD2DD2D13DD2 -D131111; ! 283 steps +D2D13DD2D13111DD2D13DD2D1311DD2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2DD2D +12DD2D11DD2D121D1DD2D1D2DD2D13DD2D1D2DD2DD2D13DD2D131111; ! 263 steps -(((P ^ Q) -> ~ R) <-> ((Q ^ R) -> ~ P)); ! *4.15 (GB 281->277) -~ (((~ (P -> ~ Q) -> R) -> (~ (Q -> R) -> ~ P)) -> ~ ((~ (S -> ~ T) - -> ~ U) -> (~ (U -> ~ S) -> ~ T))); ! Result of proof +(((P ^ Q) -> ~ R) <-> ((Q ^ R) -> ~ P)) +; ! *4.15 (GB 281->277) (SD 277->233) +~ (((~ (P -> ~ Q) -> R) -> (~ (Q -> R) -> ~ P)) -> ~ ((~ (S -> T) -> + ~ U) -> (~ (U -> ~ S) -> T))); ! Result of proof DD3DD2DD2DD2D13DD2D1311D1DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D -1D3DD2DD2D13DD2D1311DD2D1D2DD2D1DD2D1D2DD2D1211DD2D13DD2D1D2DD2DD2D13 -DD2D131111DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2 -D1311DD2D1DD2D1DD22D11DD2D112DD2D1D2D1DD2D13DD2D1DD22D2DD2D13DD2D1311 -3; ! 277 steps +1D3DD2DD2D13DD2D1311DD2DD2D12DD2D11DD2D121D1DD2D13DD2D1D2DD2DD2D13DD2 +D13111DD2D1DD2DD2D12DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D1311DD2D131D1D3 +DD2D1D3DD2DD2D13DD2D131113; ! 233 steps (P <-> P); ! *4.2 ~ ((P -> P) -> ~ (Q -> Q)); ! Result of proof @@ -735,22 +737,22 @@ DD3DD2DD2DD2D13DD2D1311D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D13D2D1D3DD2 DD2D13DD2D1311; ! 83 steps (((P ^ Q) ^ R) <-> (P ^ (Q ^ R))) -; ! *4.32 (GB 359->355) (SD 355->317) +; ! *4.32 (GB 359->355) (SD 355->313) ~ ((~ (~ (P -> ~ Q) -> R) -> ~ (P -> ~ ~ (Q -> R))) -> ~ (~ (S -> ~ ~ (T -> U)) -> ~ (~ (S -> ~ T) -> U))); ! Result of proof DD3DD2DD2DD2D13DD2D1311D1D3DD2D1D3DD2DD2D13DD2D1311DD2D1DD2D1DD2DD2D1 2DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D1311DD2D131D1D3DD2D1D3DD2DD2D13DD2 D13111D2D1DD2DD2D13DD2D1311DD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D131 -1DD2D1DD2D1D2D1D3DD2DD2D13DD2D1311DD2D1D2DD2D1DD2D1D2DD2D1211DD2D13DD -2D1D2DD2DD2D13DD2D131111DD2DD2D13DD2D1311; ! 317 steps +1DD2D1DD2D1D2D1D3DD2DD2D13DD2D1311DD2DD2D12DD2D11DD2D121D1DD2D13DD2D1 +D2DD2DD2D13DD2D13111DD2DD2D13DD2D1311; ! 313 steps -(((P v Q) v R) <-> (P v (Q v R))); ! *4.33 +(((P v Q) v R) <-> (P v (Q v R))); ! *4.33 (SD 207->199) ~ (((~ (P -> Q) -> R) -> (P -> (~ Q -> R))) -> ~ ((S -> (~ T -> U)) -> (~ (S -> T) -> U))); ! Result of proof -DD3DD2DD2DD2D13DD2D1311D1DD2D1D2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D1D -D2D1DD22D11DD2D112DD2D13D2D1D3DD2DD2D13DD2D1311DD2D1DD2D13D2D1D3DD2DD -2D13DD2D1311DD2D1DD2D1DD22D11DD2D112D2D1DD2D13D2D1D3DD2DD2D13DD2D1311 -; ! 207 steps +DD3DD2DD2DD2D13DD2D1311D1DD2DD2D12DD2D11DD2D121D1DD2D13DD2D1D2D1D3DD2 +DD2D13DD2D1311DD2D1D2DD2DD2D13DD2D13111DD2D1DD2D13D2D1D3DD2DD2D13DD2D +1311DD2D1DD2D1DD22D11DD2D112D2D1DD2D13D2D1D3DD2DD2D13DD2D1311 +; ! 199 steps ((P <-> Q) -> ((P ^ R) <-> (Q ^ R))) ; ! *4.36 (GB 311->291) (SF 291->271) @@ -771,53 +773,53 @@ D13DD2D1311DD2D1DD2D1D2DD2D1211DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2 D1D3DD2DD2D13DD2D1311DD2D1DD2D1D2DD2D1211DD2D1DD2D13DD2D1DD22D2DD2D13 DD2D1311D2D1D3DD2DD2D13DD2D1311; ! 307 steps -(((P <-> R) ^ (Q <-> S)) -> ((P ^ Q) <-> (R ^ S))); ! *4.38 +(((P <-> R) ^ (Q <-> S)) -> ((P ^ Q) <-> (R ^ S))) +; ! *4.38 (SD 585->529) (~ (~ ((P -> Q) -> ~ (R -> S)) -> ~ ~ ((T -> U) -> ~ (V -> W))) -> ~ ((~ (P -> ~ T) -> ~ (Q -> ~ U)) -> ~ (~ (R -> ~ V) -> ~ (S -> ~ W)))); ! Result of proof DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2DD2D1DD2D12D2D1DD2D13DD2D1D -2DD2DD2D13DD2D13111DD2D1DD2D1DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D1311DD -2D131D3DD2D1D3DD2DD2D13DD2D1311DD2D131D3DD2D1D3DD2DD2D13DD2D1311DD2D1 -31DD2D1DD2D1DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13 -DD2D1311DD2D131D3DD2D1D3DD2DD2D13DD2D13111DD2DD2D1DD2D12D2D1DD2D13DD2 -D1D2DD2DD2D13DD2D13111DD2D1DD2D1DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D131 -1DD2D131D3DD2D1D3DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13DD2D1311DD2D131D -D2D1DD2D1DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13DD2 -D13111D3DD2D1D3DD2DD2D13DD2D13111; ! 585 steps +2DD2DD2D13DD2D13111DD2D1DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D1311DD2D131 +D3DD2D1DD2D1D3DD2DD2D13DD2D1311DD2D1D2DD2D1311DD2D131DD2DD2D1DD2D121D +3DD2D1D3D3DD2D1D3DD2DD2D13DD2D13DD2D13DD2D13111DD2D131D1D3DD2D1D3DD2D +D2D13DD2D13111DD2DD2D1DD2D12D2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2DD2 +D1DD2D121D3DD2D1DD2D1D3DD2DD2D13DD2D1311DD2D1D2DD2D13111D1D3DD2D1D3DD +2DD2D13DD2D1311DD2D131DD2D1DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D13111D3D +D2D1D3D3DD2D1D3DD2DD2D13DD2D13DD2D13DD2D131111; ! 529 steps (((P <-> R) ^ (Q <-> S)) -> ((P v Q) <-> (R v S))) -; ! *4.39 (GB 913->901) (RR 901->609) (SD 609->479) +; ! *4.39 (GB 913->901) (RR 901->609) (SD 609->465) (~ (~ ((P -> Q) -> ~ (R -> S)) -> ~ ~ ((T -> U) -> ~ (V -> W))) -> ~ (((~ P -> T) -> (~ Q -> U)) -> ~ ((~ R -> V) -> (~ S -> W)))) ; ! Result of proof DD2DD2D13DD2D1D2DD2DD2D13DD2D1311DD2D11DD2DD2D12DD2D11DD2D1DD2D121D3D D2D1D3D3DD2D1D3DD2DD2D13DD2D13DD2D13DD2D13111DD2D131DD2D1D2DD2D121DD2 -D11DD2D13DD2DD2D12DD2D11DD2D1D2D1D3DD2DD2D13DD2D1311D3DD2D1DD2D1D3DD2 -DD2D13DD2D1311DD2D1D2DD2D1311DD2D131D1DD2DD2D13DD2D1311DD2DD2D12DD2D1 -1DD2D12DD2D13DD2DD2D12DD2D11DD2D13DD2D13DD2D1DD22D11DD2D11DD2D131D11D -D2D1D2DD2D121DD2D11DD2D13DD2DD2D12DD2D11DD2D1D2D1D3DD2DD2D13DD2D1311D -3DD2D1DD2D1D3DD2DD2D13DD2D1311DD2D1D2DD2D13111D1DD2DD2D13DD2D1311 -; ! 479 steps - -((P ^ (Q v R)) <-> ((P ^ Q) v (P ^ R))); ! *4.4 (SF 359->355) +D11DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311D3 +DD2D1DD2D1D3DD2DD2D13DD2D1311DD2D1D2DD2D1311DD2D131DD2DD2D12DD2D11DD2 +D1DD2D121D3DD2D1D3D3DD2D1D3DD2DD2D13DD2D13DD2D13DD2D131111DD2D1D2DD2D +121DD2D11DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D +1311D3DD2D1DD2D1D3DD2DD2D13DD2D1311DD2D1D2DD2D13111; ! 465 steps + +((P ^ (Q v R)) <-> ((P ^ Q) v (P ^ R))) +; ! *4.4 (SF 359->355) (SD 355->345) ~ ((~ (P -> ~ (Q -> R)) -> (~ ~ (P -> Q) -> ~ (P -> ~ R))) -> ~ ((~ ~ (S -> T) -> ~ (S -> ~ U)) -> ~ (S -> ~ (T -> U)))) ; ! Result of proof DD3DD2DD2DD2D13DD2D1311D1DD2D1D2DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D 1311D2D1D3DD2DD2D13DD2D1311DD2D1DD2D12D2D1DD2D13DD2D1D2D1D3DD2DD2D13D D2D1311DD2D1D2DD2DD2D13DD2D13111DD2DD2D13DD2D13111D3DD2D1DD2DD2D1DD2D -13DD2D1D2DD2DD2D13DD2D13111DD2D1D3DD2DD2D13DD2D1311D2D1D3DD2D1D3DD2DD -2D13DD2D1311DD2D131D2D1D3DD2D1D3DD2DD2D13DD2D1311DD2D13DD2D131DD2DD2D -13DD2D1311; ! 355 steps +1D2DD2D13DD2D1D2DD2D13DD2DD2D13DD2D131111D2D1D3DD2D1D3DD2DD2D13DD2D13 +11DD2D131D2D1D3DD2D1D3DD2DD2D13DD2D1311DD2D13DD2D131DD2DD2D13DD2D1311 +; ! 345 steps ((P v (Q ^ R)) <-> ((P v Q) ^ (P v R))) -; ! *4.41 (SF 275->271) (SD 271->249) +; ! *4.41 (SF 275->271) (SD 271->241) ~ (((P -> ~ (Q -> ~ R)) -> ~ ((P -> Q) -> ~ (P -> R))) -> ~ (~ ((S -> T) -> ~ (S -> U)) -> (S -> ~ (T -> ~ U)))); ! Result of proof DD3DD2DD2DD2D13DD2D1311D1DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111D2D1D 3DD2D1D3DD2DD2D13DD2D1311DD2D131D2D1D3DD2D1D3DD2DD2D13DD2D13111DD2DD2 -D12DD2D1D2D13DD2D1D2D1D2DD2DD2D13DD2D1311DD2D1D2D11D3DD2D1D3DD2DD2D13 -DD2D1311DD2D131D3DD2D1D3DD2DD2D13DD2D13111; ! 249 steps +D1DD2D12D2D1DD2D13DD2D1D2DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13DD2D1311 +DD2D131D3DD2D1D3DD2DD2D13DD2D13111; ! 241 steps (P <-> ((P ^ Q) v (P ^ ~ Q))); ! *4.42 (GB 175->165) ~ ((P -> (~ ~ (P -> Q) -> ~ (P -> ~ Q))) -> ~ ((~ ~ (R -> S) -> ~ (R @@ -858,20 +860,20 @@ D2D131DD2D13DD2D131; ! 157 steps DD3DD2DD2DD2D13DD2D1311D1DD2D1DD22D2DD2D13DD2D131DD2D13DD2D131DD2D1D3 DD2DD2D13DD2D1311DD2D1DD22D1D3DD2DD2D13DD2D13111; ! 117 steps -((P ^ ~ Q) <-> ~ (~ P v Q)); ! *4.52 (GB 231->219) +((P ^ ~ Q) <-> ~ (~ P v Q)); ! *4.52 (GB 231->219) (SD 219->209) ~ ((~ (P -> ~ ~ Q) -> ~ (~ ~ P -> Q)) -> ~ (~ (~ ~ R -> S) -> ~ (R -> ~ ~ S))); ! Result of proof DD3DD2DD2DD2D13DD2D1311D1D3DD2D1D3DD2DD2D13DD2D1311DD2D1DD2D13DD2D13D 2D1D3DD2DD2D13DD2D13DD2D13DD2D1311DD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13 -DD2D1311DD2D1DD2D1D2D1DD2DD2D13DD2D1311DD2D1DD22D2DD2D13DD2D1311DD2DD -2D13DD2D1311; ! 219 steps +DD2D1311DD2D1D2D1DD2DD2D13DD2D1311DD2D1DD22D2DD2D13DD2D131DD2D13DD2D1 +31; ! 209 steps -(~ (P ^ ~ Q) <-> (~ P v Q)); ! *4.53 (GB 181->169) +(~ (P ^ ~ Q) <-> (~ P v Q)); ! *4.53 (GB 181->169) (SD 169->159) ~ ((~ ~ (P -> ~ ~ Q) -> (~ ~ P -> Q)) -> ~ ((~ ~ R -> S) -> ~ ~ (R -> ~ ~ S))); ! Result of proof -DD3DD2DD2DD2D13DD2D1311D1DD2D1DD2D1D2D1DD2DD2D13DD2D1311DD2D1DD22D2DD -2D13DD2D1311DD2DD2D13DD2D1311DD2D1D3DD2DD2D13DD2D1311DD2D13DD2D13D2D1 -D3DD2DD2D13DD2D13DD2D13DD2D1311; ! 169 steps +DD3DD2DD2DD2D13DD2D1311D1DD2D1D2D1DD2DD2D13DD2D1311DD2D1DD22D2DD2D13D +D2D131DD2D13DD2D131DD2D1D3DD2DD2D13DD2D1311DD2D13DD2D13D2D1D3DD2DD2D1 +3DD2D13DD2D13DD2D1311; ! 159 steps ((~ P ^ Q) <-> ~ (P v ~ Q)); ! *4.54 ~ ((P -> P) -> ~ (Q -> Q)); ! Result of proof @@ -951,13 +953,12 @@ D2D1D3DD2DD2D13DD2D1311DD2D131D2DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1D 2D1D3DD2D1D3DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13DD2D1311DD2D131 ; ! 201 steps -((P -> Q) <-> (Q <-> (P v Q))); ! *4.72 +((P -> Q) <-> (Q <-> (P v Q))); ! *4.72 (SD 195->193) ~ (((P -> Q) -> ~ ((R -> (S -> R)) -> ~ ((~ P -> Q) -> Q))) -> ~ (~ (T -> ~ ((~ U -> V) -> W)) -> (U -> W))); ! Result of proof DD3DD2DD2DD2D13DD2D1311D1DD2D1D3DD2DD2DD2D13DD2D1311D11DD2D1D2D1DD2DD 2D13D2DD2D1311DD2D1DD2DD2D121D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D121DD -2D1DD2D1DD22D1DD2D1D2DD2D13111D3DD2D1D3DD2DD2D13DD2D13111 -; ! 195 steps +2DD2D12DD2D13DD2D1DD22D11DD2D11DD2D131D1DD2D1D2DD2D1311; ! 193 steps (Q -> (P <-> (P ^ Q))); ! *4.73 (P -> ~ ((Q -> ~ (Q -> ~ P)) -> ~ (~ (R -> S) -> R))) @@ -970,22 +971,22 @@ D2D131111D1D3DD2D1D3DD2DD2D13DD2D1311DD2D131; ! 113 steps DD2D1D3DD2DD2DD2D13DD2D1311D11DD2D1D2DD2111; ! 43 steps (((P -> Q) ^ (P -> R)) <-> (P -> (Q ^ R))) -; ! *4.76 (SF 275->271) (SD 271->249) +; ! *4.76 (SF 275->271) (SD 271->241) ~ ((~ ((P -> Q) -> ~ (P -> R)) -> (P -> ~ (Q -> ~ R))) -> ~ ((S -> ~ (T -> ~ U)) -> ~ ((S -> T) -> ~ (S -> U)))); ! Result of proof -DD3DD2DD2DD2D13DD2D1311D1DD2DD2D12DD2D1D2D13DD2D1D2D1D2DD2DD2D13DD2D1 -311DD2D1D2D11D3DD2D1D3DD2DD2D13DD2D1311DD2D131D3DD2D1D3DD2DD2D13DD2D1 -3111DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111D2D1D3DD2D1D3DD2DD2D13DD2D -1311DD2D131D2D1D3DD2D1D3DD2DD2D13DD2D13111; ! 249 steps +DD3DD2DD2DD2D13DD2D1311D1DD2DD2D1DD2D12D2D1DD2D13DD2D1D2DD2DD2D13DD2D +13111D3DD2D1D3DD2DD2D13DD2D1311DD2D131D3DD2D1D3DD2DD2D13DD2D13111DD2D +D2D1DD2D13DD2D1D2DD2DD2D13DD2D13111D2D1D3DD2D1D3DD2DD2D13DD2D1311DD2D +131D2D1D3DD2D1D3DD2DD2D13DD2D13111; ! 241 steps -(((Q -> P) ^ (R -> P)) <-> ((Q v R) -> P)); ! *4.77 (SD 375->285) +(((Q -> P) ^ (R -> P)) <-> ((Q v R) -> P)); ! *4.77 (SD 375->265) ~ ((~ ((P -> Q) -> ~ (R -> Q)) -> ((~ P -> R) -> Q)) -> ~ (((~ S -> T) -> U) -> ~ ((S -> U) -> ~ (T -> U)))); ! Result of proof -DD3DD2DD2DD2D13DD2D1311D1DD2DD2D12DD2D1D2D13DD2D1D2D1D2DD2D131DD2DD2D -12DD2D11DD2D1DD2D121D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2D1D2D13DD2D1D -2D1D2D1D3DD2DD2D13DD2D1311DD2D12DD2D13DD2D1DD22D11DD2D11DD2D131D1D11D -D2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1DD22D1DD2D1D2DD2D13111DD2D -1DD22D111; ! 285 steps +DD3DD2DD2DD2D13DD2D1311D1DD2D1D2D1DD2DD2D13D2DD2D1311DD2DD2D12DD2D11D +D2D12DD2D13DD2D1DD22D1DD2D131DD2D11DD2D131DD2D1D2D1DD2D13D2D1D3DD2DD2 +D13DD2D1311DD2D12DD2D13DD2D1DD22D11DD2D11DD2D131DD2DD2D1DD2D13DD2D1D2 +DD2DD2D13DD2D13111DD2D1DD22D1DD2D1D2DD2D13111DD2D1DD22D111 +; ! 265 steps (((P -> Q) v (P -> R)) <-> (P -> (Q v R))); ! *4.78 (GB 327->319) ~ (((~ (P -> Q) -> (P -> R)) -> (P -> (~ Q -> R))) -> ~ ((S -> (~ T @@ -1016,20 +1017,20 @@ D13111; ! 75 steps DD3DD2DD2DD2D13DD2D1311D1DD2DD2D13D2DD2D13111; ! 45 steps (((P -> Q) ^ (P -> ~ Q)) <-> ~ P) -; ! *4.82 (GB 249->179) (RR 179->175) +; ! *4.82 (GB 249->179) (RR 179->175) (SD 175->157) ~ ((~ ((P -> Q) -> ~ (P -> ~ Q)) -> ~ P) -> ~ (~ R -> ~ ((R -> S) -> ~ (R -> T)))); ! Result of proof -DD3DD2DD2DD2D13DD2D1311D1D3DD2D1D3DD2DD2D13DD2D1311DD2D1D2DD2D1DD2D1D -D22D2DD2D13DD2D1311D2DD2D13DD2D1D2DD2DD2D13DD2D131111DD2DD2D1DD2D13DD -2D1D2DD2DD2D13DD2D13111DD2D131DD2D131; ! 175 steps +DD3DD2DD2DD2D13DD2D1311D1D3DD2D1D3DD2DD2D13DD2D1311DD2D1D2D2DD2D13DD2 +D1D2DD2DD2D13DD2D13111DD2D13DD2D131DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D +13111DD2D131DD2D131; ! 157 steps -(((P -> Q) ^ (~ P -> Q)) <-> Q); ! *4.83 (SF 249->245) +(((P -> Q) ^ (~ P -> Q)) <-> Q); ! *4.83 (SF 249->245) (SD 245->231) ~ ((~ ((P -> Q) -> ~ (~ P -> Q)) -> Q) -> ~ (R -> ~ ((S -> R) -> ~ (T -> R)))); ! Result of proof -DD3DD2DD2DD2D13DD2D1311D1D3DD2D1D3DD2DD2D13DD2D1311DD2D1D2DD2D1DD2D1D -D2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311DD2D1D2D1DD2DD2D -13D2DD2D1311DD2D1DD2DD2D121D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D1211DD2 -DD2D13DD2D1D2DD2DD2D13DD2D1311DD2D1111; ! 245 steps +DD3DD2DD2DD2D13DD2D1311D1DDD2DD2D12DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D +1311DD2D131D1D3DD2D1D3DD2DD2D13DD2D13111DD2D1D2D1DD2DD2D13D2DD2D1311D +D2D1DD2DD2D121D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D121DD2DD2D13DD2D1D2D +D2DD2D13DD2D1311DD2D1111; ! 231 steps ((P <-> Q) -> ((P -> R) <-> (Q -> R))); ! *4.84 (GB 139->135) (~ ((P -> Q) -> ~ (R -> S)) -> ~ (((S -> T) -> (R -> T)) -> ~ ((Q -> @@ -1038,42 +1039,42 @@ DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1D2DD2D121DD2D13DD2D1DD22D 11DD2D11DD2D131DD2D1D2DD2D121DD2D13DD2D1DD22D1DD2D131DD2D11DD2D131 ; ! 135 steps -((P <-> Q) -> ((R -> P) <-> (R -> Q))); ! *4.85 (SD 123->121) +((P <-> Q) -> ((R -> P) <-> (R -> Q))); ! *4.85 (SD 123->119) (~ ((P -> Q) -> ~ (R -> S)) -> ~ (((T -> P) -> (T -> Q)) -> ~ ((U -> R) -> (U -> S)))); ! Result of proof -DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1DD2D121D3DD2D1D3DD2DD2D13 -DD2D1311DD2D131DD2D12DD2D13DD2D1DD22D11DD2D11DD2D131; ! 121 steps +DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D12DD2D13DD2D1DD22D1DD2D131 +DD2D11DD2D131DD2D12DD2D13DD2D1DD22D11DD2D11DD2D131; ! 119 steps ((P <-> Q) -> ((P <-> R) <-> (Q <-> R))) -; ! *4.86 (GB 621->617) (SD 617->555) +; ! *4.86 (GB 621->617) (SD 617->551) (~ ((P -> Q) -> ~ (R -> S)) -> ~ ((~ ((S -> T) -> ~ (U -> P)) -> ~ ((R -> T) -> ~ (U -> Q))) -> ~ (~ ((Q -> V) -> ~ (W -> R)) -> ~ ((P -> V) -> ~ (W -> S))))); ! Result of proof DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2DD2D12DD2D1D2D1DD2D1D2DD2D1 -3DD2D1D2DD2DD2D13DD2D131111DD2DD2D12DD2D11DD2D1DD2D121D3DD2D1D3DD2DD2 -D13DD2D1311DD2D131D1D3DD2D1D3DD2DD2D13DD2D13111DD2D1D2DD2D1DD2D121D3D -D2D1D3DD2DD2D13DD2D1311DD2D131DD2D13DD2D1DD22D11DD2D11DD2D131DD2DD2D1 -DD2D1D2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311D -D2D1DD2DD2D121D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD -2D1311DD2D1D2DD2D12DD2D11DD2D121DD2D11DD2D1D2DD2D1211DD2D1D2DD2D121DD -2D13DD2D1DD22D1DD2D131DD2D11DD2D131DD2D12DD2D13DD2D1DD22D11DD2D11DD2D -131; ! 555 steps +3DD2D1D2DD2DD2D13DD2D131111DD2DD2D12DD2D11DD2D12DD2D13DD2D1DD22D1DD2D +131DD2D11DD2D131D1D3DD2D1D3DD2DD2D13DD2D13111DD2D1D2DD2D12DD2D13DD2D1 +DD22D1DD2D131DD2D11DD2D131DD2D13DD2D1DD22D11DD2D11DD2D131DD2DD2D1DD2D +1D2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311DD2D1 +DD2DD2D121D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D13 +11DD2D1D2DD2D12DD2D11DD2D121DD2D11DD2D1D2DD2D1211DD2D1D2DD2D121DD2D13 +DD2D1DD22D1DD2D131DD2D11DD2D131DD2D12DD2D13DD2D1DD22D11DD2D11DD2D131 +; ! 551 steps (((((P ^ Q) -> R) <-> (P -> (Q -> R))) ^ ((P -> (Q -> R)) <-> (Q -> (P -> R)))) ^ ((Q -> (P -> R)) <-> ((Q ^ P) -> R))) -; ! *4.87 (GB 531->523) (SD 523->447) +; ! *4.87 (GB 531->523) (SD 523->439) ~ (~ (~ (((~ (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 DD3DD2DD2DD2D13DD2D1311D1DD3DD2DD2DD2D13DD2D1311D1DD3DD2DD2DD2D13DD2D -1311D1DD2D1D2DD2D1DD2D1D2DD2D1211DD2D13DD2D1D2DD2DD2D13DD2D131111DD2D -D2D12DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D1311DD2D131D1D3DD2D1D3DD2DD2D1 -3DD2D13111DD3DD2DD2DD2D13DD2D1311D1DD2D1DD22D11DD2D112DD2D1DD22D11DD2 -D112DD3DD2DD2DD2D13DD2D1311D1DD2DD2D12DD2DD2D121D1D3DD2D1D3DD2DD2D13D -D2D1311DD2D131D1D3DD2D1D3DD2DD2D13DD2D13111DD2D1D2DD2D1DD2D1D2DD2D121 -1DD2D13DD2D1D2DD2DD2D13DD2D131111; ! 447 steps +1311D1DD2DD2D12DD2D11DD2D121D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2DD2D1 +2DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D1311DD2D131D1D3DD2D1D3DD2DD2D13DD2 +D13111DD3DD2DD2DD2D13DD2D1311D1DD2D1DD22D11DD2D112DD2D1DD22D11DD2D112 +DD3DD2DD2DD2D13DD2D1311D1DD2DD2D12DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D1 +311DD2D131D1D3DD2D1D3DD2DD2D13DD2D13111DD2DD2D12DD2D11DD2D121D1DD2D13 +DD2D1D2DD2DD2D13DD2D13111; ! 439 steps ((P ^ Q) -> (P <-> Q)); ! *5.1 (GB 111->107) (~ (P -> ~ Q) -> ~ ((R -> Q) -> ~ (S -> P))); ! Result of proof @@ -1096,24 +1097,21 @@ DD2D1DD22D11DD2D11DD2D131; ! 25 steps (~ (P -> Q) -> (Q -> R)); ! Result of proof DD2D1DD22D11DD2D11DD2D131; ! 25 steps -((P <-> Q) v (P <-> ~ Q)); ! *5.15 +((P <-> Q) v (P <-> ~ Q)); ! *5.15 (SD 267->185) (~ ~ ((P -> Q) -> ~ (R -> S)) -> ~ ((S -> ~ Q) -> ~ (~ R -> P))) ; ! Result of proof -DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1D2DD2D1DD2D1DD2D13DD2D1DD -22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311DD2D1D2DD2D13DD2D1D2DD2DD2D1 -3DD2D1311DD2D111DD2D1111DD2D1D2DD2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D -1DD2D1D2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1311DD2D1311 -; ! 267 steps +DDD2D13D2D1D3DD2DD2D13DD2D1311DD2D1DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D +13111DD2D1DD22D11DD2D11DD2D13DD2D1DD22D111DD2D1DD2D1DD22D1DD2D1D2DD2D +13111DD2D13DD2D1DD22D1DD2D1311DD2DD2D13DD2D1311; ! 185 steps -~ ((P <-> Q) ^ (P <-> ~ Q)); ! *5.16 (GB 377->333) +~ ((P <-> Q) ^ (P <-> ~ Q)); ! *5.16 (GB 377->333) (SD 333->331) ~ ~ (~ ((P -> Q) -> ~ (Q -> P)) -> ~ ~ ((P -> ~ Q) -> ~ (~ Q -> P))) ; ! Result of proof DD3DD2DD2D13DD2D1311DD2D1D3DD2DD2D13DD2D1311DD2DD2D1DD2D12D2D1DD2D13D -D2D1D2D1D3DD2DD2D13DD2D1311DD2D1D2DD2DD2D13DD2D13111DD2D1DD2D1D2D1DD2 -D1DD2DD2D13D2DD2D1311DD2D1DD22D2DD2D13DD2D1311DD2D1D2DD2D1211D3DD2D1D -3DD2DD2D13DD2D13111DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2DD2D13D -D2D1D2DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13DD2D1311DD2D131 -; ! 333 steps +D2D1D2D1D3DD2DD2D13DD2D1311DD2D1D2DD2DD2D13DD2D13111DD2D1D2D1DD2D1DD2 +DD2D13D2DD2D1311DD2D1DD22D2DD2D13DD2D1311DD2D1D2DD2D121DD2D13DD2D1DD2 +2D11DD2D11DD2D131DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2DD2D13DD2 +D1D2DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13DD2D1311DD2D131; ! 331 steps (((P v Q) ^ ~ (P ^ Q)) <-> (P <-> ~ Q)); ! *5.17 ~ ((~ ((~ P -> Q) -> ~ ~ ~ R) -> ~ (R -> ~ (~ Q -> P))) -> ~ (~ (S @@ -1124,18 +1122,18 @@ DD3DD2DD2DD2D13DD2D1311D1D3DD2D1D3DD2DD2D13DD2D1311DD2D1DD2D1D2D1D3DD D1DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311DD2DD2D121D1DD2D13D2D1D3DD 2DD2D13DD2D1311D2D1DD2DD2D13DD2D1311DD2DD2D13DD2D1311; ! 329 steps -((P <-> Q) <-> ~ (P <-> ~ Q)); ! *5.18 (GB 577->503) +((P <-> Q) <-> ~ (P <-> ~ Q)); ! *5.18 (GB 577->503) (SD 503->491) ~ ((~ ((P -> Q) -> ~ (Q -> P)) -> ~ ~ ((P -> ~ Q) -> ~ (~ Q -> P))) -> ~ (~ ~ ((R -> ~ S) -> ~ (~ T -> U)) -> ~ ((U -> S) -> ~ (T -> R)))); ! Result of proof DD3DD2DD2DD2D13DD2D1311D1DD2D1D3DD2DD2D13DD2D1311DD2DD2D1DD2D12D2D1DD -2D13DD2D1D2D1D3DD2DD2D13DD2D1311DD2D1D2DD2DD2D13DD2D13111DD2D1DD2D1D2 -D1DD2D1DD2DD2D13D2DD2D1311DD2D1DD22D2DD2D13DD2D1311DD2D1D2DD2D1211D3D -D2D1D3DD2DD2D13DD2D13111DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2DD -2D13DD2D1D2DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2D1DD -2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1DD22D11DD2D11DD2D13DD2D1DD2 -2D111DD2D1DD2D13DD2D1DD22D1DD2D1311D2D1D3DD2D1D3DD2DD2D13DD2D1311DD2D -131DD2DD2D13DD2D1311; ! 503 steps +2D13DD2D1D2D1D3DD2DD2D13DD2D1311DD2D1D2DD2DD2D13DD2D13111DD2D1D2D1DD2 +D1DD2DD2D13D2DD2D1311DD2D1DD22D2DD2D13DD2D1311DD2D1D2DD2D121DD2D13DD2 +D1DD22D11DD2D11DD2D131DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2DD2D +13DD2D1D2DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2D1DD2D +D2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1DD22D11DD2D11DD2D13DD2D1DD22D +111DD2D1DD2D1DD22D1DD2D1D2DD2D13111DD2D13DD2D1DD22D1DD2D1311DD2DD2D13 +DD2D1311; ! 491 steps ~ (P <-> ~ P); ! *5.19 (GB 141->131) (RR 131->123) ~ ~ ((P -> ~ P) -> ~ (~ P -> P)); ! Result of proof @@ -1158,18 +1156,19 @@ D1311DD2D1DD2D1D2D1D3DD2D1D3DD2DD2D13DD2D1311DD2D1D2D1D3DD2DD2D13DD2D 1311DD2DD2D13DD2D1311DD2D1DD22D1D2D1D3DD2DD2D13DD2D13111DD2D1DD22D1D3 DD2DD2D13DD2D13111; ! 363 steps -((P <-> Q) <-> ((P ^ Q) v (~ P ^ ~ Q))); ! *5.23 (GB 557->513) +((P <-> Q) <-> ((P ^ Q) v (~ P ^ ~ Q))) +; ! *5.23 (GB 557->513) (SD 513->501) ~ ((~ ((P -> Q) -> ~ (Q -> P)) -> (~ ~ (P -> ~ Q) -> ~ (~ P -> ~ ~ Q))) -> ~ ((~ ~ (R -> ~ S) -> ~ (~ T -> ~ ~ U)) -> ~ ((T -> S) -> ~ (U -> R)))); ! Result of proof DD3DD2DD2DD2D13DD2D1311D1DD2D1DD2D1DD22D2DD2D13DD2D1311DD2DD2D1DD2D12 D2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13D D2D1311D2DD2D13DD2D1D2DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13DD2D1311DD2 -D131DD2D1DD2D1D2D1DD2D1DD2DD2D13D2DD2D1311DD2D1DD22D2DD2D13DD2D1311DD -2D1D2DD2D1211D3DD2D1D3DD2DD2D13DD2D13111DD2D1DD2DD2D1DD2D13DD2D1D2DD2 -DD2D13DD2D13111DD2D1DD2D13DD2D1DD22D111D2D1D3DD2D1D3DD2DD2D13DD2D1311 -DD2D131DD2D1DD2D13DD2D1DD22D1DD2D1311D2D1D3DD2D1D3DD2DD2D13DD2D13111D -D2D1DD22D1D3DD2DD2D13DD2D13111; ! 513 steps +D131DD2D1D2D1DD2D1DD2DD2D13D2DD2D1311DD2D1DD22D2DD2D13DD2D1311DD2D1D2 +DD2D121DD2D13DD2D1DD22D11DD2D11DD2D131DD2D1DD2DD2D1DD2D13DD2D1D2DD2DD +2D13DD2D13111DD2D1DD2D1DD22D1DD2D1D2DD2D13111DD2D13DD2D1DD22D111DD2D1 +DD2D13DD2D1DD22D1DD2D1311D2D1D3DD2D1D3DD2DD2D13DD2D13111DD2D1DD22D1D3 +DD2DD2D13DD2D13111; ! 501 steps (~ ((P ^ Q) v (~ P ^ ~ Q)) <-> ((P ^ ~ Q) v (Q ^ ~ P))) ; ! *5.24 (GB 669->585) @@ -1221,23 +1220,25 @@ D2D12DD2D1DD22D111DD2D13D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2D1D2D13DD 2D1DD2D1DD22D11DD2D11DD2D12DD2D1DD22D111DD2D13D3DD2D1D3DD2DD2D13DD2D1 3111; ! 625 steps -((P ^ (Q -> R)) <-> (P ^ ((P ^ Q) -> R))); ! *5.33 (SF 393->389) +((P ^ (Q -> R)) <-> (P ^ ((P ^ Q) -> R))) +; ! *5.33 (SF 393->389) (SD 389->343) ~ ((~ (P -> ~ (Q -> R)) -> ~ (P -> ~ (~ (S -> ~ Q) -> R))) -> ~ (~ (T -> ~ (~ (T -> ~ U) -> V)) -> ~ (T -> ~ (U -> V)))) ; ! Result of proof DD3DD2DD2DD2D13DD2D1311D1DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111D3DD2 -D1D3DD2DD2D13DD2D1311DD2D131DD2D1DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D13 -111D3DD2D1D3DD2DD2D13DD2D13111DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111 -D3DD2D1D3DD2DD2D13DD2D1311DD2D131D3DD2D1D3DD2DD2D13DD2D1311DD2D1D2DD2 -D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311DD2D1DD2 -D1D2DD2D1211DD2D13DD2D1D2DD2DD2D13DD2D131111; ! 389 steps - -(((P -> Q) ^ (P -> R)) -> (P -> (Q <-> R))); ! *5.35 (SF 163->159) +D1D3DD2DD2D13DD2D1311DD2D131DD2DD2D12DD2D13DD2D1DD22D11DD2D11DD2D131D +1D3DD2D1D3DD2DD2D13DD2D13111DDD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1 +D3DD2DD2D13DD2D1311D2DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3D +D2DD2D13DD2D1311DD2D1DD2D1D2DD2D1211DD2D13DD2D1D2DD2DD2D13DD2D13111 +; ! 343 steps + +(((P -> Q) ^ (P -> R)) -> (P -> (Q <-> R))) +; ! *5.35 (SF 163->159) (SD 159->145) (~ ((P -> Q) -> ~ (P -> R)) -> (P -> ~ ((S -> R) -> ~ (T -> Q)))) ; ! Result of proof -D3DD2D1D3DD2DD2D13DD2D1311DD2D1D2DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2 -D1311D2D1D3DD2DD2D13DD2D1311DD2D12D2D1DD2D1D2DD2D13DD2D1D2DD2DD2D13DD -2D1311DD2D111DD2D1111; ! 159 steps +DDD2DD2D12DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D1311DD2D131D1D3DD2D1D3DD2 +DD2D13DD2D13111DD2D12D2D1DD2D1D2DD2D13DD2D1D2DD2DD2D13DD2D1311DD2D111 +DD2D111; ! 145 steps ((P ^ (P <-> Q)) <-> (Q ^ (P <-> Q))) ; ! *5.36 (GB 417->393) (SF 393->381) @@ -1286,7 +1287,7 @@ D2D1311DD2D111DD2D111DD2D1D2D3DD2D1D3DD2DD2D13DD2D1311DD2D1311 ; ! 131 steps ((((P v Q) v R) -> S) <-> (((P -> S) ^ (Q -> S)) ^ (R -> S))) -; ! *5.53 +; ! *5.53 (SD 673->633) ~ ((((~ (~ P -> Q) -> R) -> S) -> ~ (~ ((P -> S) -> ~ (Q -> S)) -> ~ (R -> S))) -> ~ (~ (~ ((T -> U) -> ~ (V -> U)) -> ~ (W -> U)) -> ((~ (~ T -> V) -> W) -> U))); ! Result of proof @@ -1294,20 +1295,21 @@ DD3DD2DD2DD2D13DD2D1311D1DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2DD 2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2DD2D121D1DD2D1D2DD2D131DD2D11DD2 D1D2DD2D1311DD2D1DD22D1DD2D1D2DD2D131DD2D1111DD2D1DD22D111DD2D13DD2DD 2D1DD2D12D2D1DD2D13DD2D1D2D1D3DD2DD2D13DD2D1311DD2D1D2DD2DD2D13DD2D13 -111DD2D1DD2DD2D1DD2D12D2D1DD2D13DD2D1D2D1D3DD2DD2D13DD2D1311DD2D1D2DD -2DD2D13DD2D13111DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2 -D13DD2D1311D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2D1DD2D1DD2D13DD2D1DD22 -D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D13111D3D -D2D1D3DD2DD2D13DD2D1311DD2D131DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D13 -11D2D1D3DD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D13111; ! 673 steps - -(((P ^ Q) <-> P) v ((P ^ Q) <-> Q)); ! *5.54 (GB 253->239) +111DD2D1DD2D1DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1 +311DD2D1D2D1DD2DD2D13D2DD2D1311DD2DD2D12DD2D11DD2D12DD2D13DD2D1DD22D1 +DD2D131DD2D11DD2D131DD2D1D2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D12DD2D1 +3DD2D1DD22D11DD2D11DD2D131D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2D1DD2D1 +DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311D3DD2D1D3DD2DD2 +D13DD2D13111; ! 633 steps + +(((P ^ Q) <-> P) v ((P ^ Q) <-> Q)) +; ! *5.54 (GB 253->239) (SD 239->233) (~ ~ ((P -> Q) -> ~ (R -> ~ (R -> ~ S))) -> ~ ((~ (T -> ~ U) -> U) -> ~ (S -> P))); ! Result of proof DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111D1D3DD2D1D3DD2DD2D13DD2D13111D 3DD2D1D3DD2DD2D13DD2D1311DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1 -DD22D11DD2D11DD2D131DD2D1DD2D1D2DD2D13DD2D1D2DD2DD2D13DD2D13111D2D1D3 -DD2D1D3DD2DD2D13DD2D1311DD2D1311; ! 239 steps +DD22D11DD2D11DD2D131DD2D1D2DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D13DD2D1 +DD22D1DD2D131DD2D11DD2D131; ! 233 steps (((P v Q) <-> P) v ((P v Q) <-> Q)); ! *5.55 (~ ~ (((~ P -> Q) -> P) -> ~ (R -> (~ R -> S))) -> ~ ((T -> Q) -> ~ @@ -1317,27 +1319,27 @@ D2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1D2DD2D13D2D1DD2D1D3DD2DD2D13D D2D131111D1DD2D1D2DD2D1311D11; ! 167 steps (((P ^ ~ Q) -> R) <-> (P -> (Q v R))) -; ! *5.6 (GB 207->203) (SD 203->167) +; ! *5.6 (GB 207->203) (SD 203->163) ~ (((~ (P -> ~ Q) -> R) -> (P -> (Q -> R))) -> ~ ((S -> (T -> U)) -> (~ (S -> ~ T) -> U))); ! Result of proof -DD3DD2DD2DD2D13DD2D1311D1DD2D1D2DD2D1DD2D1D2DD2D1211DD2D13DD2D1D2DD2D -D2D13DD2D131111DD2DD2D12DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D1311DD2D131 -D1D3DD2D1D3DD2DD2D13DD2D13111; ! 167 steps +DD3DD2DD2DD2D13DD2D1311D1DD2DD2D12DD2D11DD2D121D1DD2D13DD2D1D2DD2DD2D +13DD2D13111DD2DD2D12DD2DD2D121D1D3DD2D1D3DD2DD2D13DD2D1311DD2D131D1D3 +DD2D1D3DD2DD2D13DD2D13111; ! 163 steps -(((P v Q) ^ ~ Q) <-> (P ^ ~ Q)); ! *5.61 (GB 269->259) +(((P v Q) ^ ~ Q) <-> (P ^ ~ Q)); ! *5.61 (GB 269->259) (SD 259->249) ~ ((~ ((~ P -> Q) -> ~ ~ Q) -> ~ (P -> ~ ~ Q)) -> ~ (~ (R -> S) -> ~ ((~ R -> T) -> S))); ! Result of proof -DD3DD2DD2DD2D13DD2D1311D1D3DD2D1D3DD2DD2D13DD2D1311DD2D1DD2D1DD2D1DD2 -2D1D2D1D3DD2DD2D13DD2D13111DD2D1D2D1DD2DD2D13D2DD2D1311DD2D1DD2DD2D12 -1D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D121DD2DD2D13DD2D1311D3DD2D1D3DD2D -D2D13DD2D1311DD2DD2D12DD2D13DD2D131D1DD2D1D2DD2D1311; ! 259 steps +DD3DD2DD2DD2D13DD2D1311D1D3DD2D1D3DD2DD2D13DD2D1311DD2D1DD2D1D2D1DD2D +1DD2DD2D13D2DD2D1311DD2D1DD22D2DD2D13DD2D1311DD2D1DD2DD2D121D1DD2D13D +2D1D3DD2DD2D13DD2D1311DD2D121DD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D1 +311DD2DD2D12DD2D13DD2D131D1DD2D1D2DD2D1311; ! 249 steps -(((P ^ Q) v ~ Q) <-> (P v ~ Q)); ! *5.62 (RR 187->167) +(((P ^ Q) v ~ Q) <-> (P v ~ Q)); ! *5.62 (RR 187->167) (SD 167->157) ~ (((~ ~ (P -> Q) -> R) -> (~ P -> R)) -> ~ ((~ S -> T) -> (~ ~ (S -> T) -> T))); ! Result of proof DD3DD2DD2DD2D13DD2D1311D1DD2DD2D121D1DD2D1D3DD2DD2D13DD2D1311DD2D131D -D2D1DD2D1DD2D1D2DD2D1DD2D1D2D1DD2DD2D13D2DD2D1311DD2D121DD2DD2D13DD2D -131113D2D1D3DD2DD2D13DD2D1311; ! 167 steps +D2D1DD2D1DD2D1D2D1DD2DD2D13D2DD2D1311DD2D1D2DD2D12DD2D13DD2D13113D2D1 +D3DD2DD2D13DD2D1311; ! 157 steps ((P v Q) <-> (P v (~ P ^ Q))); ! *5.63 ~ (((P -> Q) -> (P -> ~ (P -> ~ Q))) -> ~ ((R -> ~ (S -> ~ T)) -> (R @@ -1370,7 +1372,7 @@ DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2DD2D1DD2D12D2D1DD2D13DD2D1D 311DD2DD2D12DD2D13DD2D131D1DD2D1D2DD2D1311; ! 249 steps ((P -> (Q <-> R)) <-> ((P -> Q) <-> (P -> R))) -; ! *5.74 (GB 345->337) +; ! *5.74 (GB 345->337) (SD 337->335) ~ (((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))))) @@ -1379,19 +1381,18 @@ DD3DD2DD2DD2D13DD2D1311D1DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1 2D2D1D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2D12D2D1D3DD2D1D3DD2DD2D13DD2 D13111DD2DD2D1DD2D12D2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1DD2D1DD22 D11DD2D11DD2D12DD2D1DD22D111D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2D1DD2 -D1DD22D11DD2D11DD2D12DD2D1DD22D111D3DD2D1D3DD2DD2D13DD2D13111 -; ! 337 steps +D1DD22D11DD2D112DD2DD2D12DD2D13DD2D1DD22D11DD2D11DD2D131D11 +; ! 335 steps (((R -> ~ Q) ^ (P <-> (Q v R))) -> ((P ^ ~ Q) <-> R)) -; ! *5.75 (SD 387->351) +; ! *5.75 (SD 387->331) (~ ((P -> Q) -> ~ ~ ((R -> (S -> T)) -> ~ ((U -> P) -> V))) -> ~ ((~ (R -> ~ S) -> T) -> ~ (P -> ~ (V -> ~ Q)))); ! Result of proof -DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1DD2D1DD2DD2D12DD2DD2D121D -1D3DD2D1D3DD2DD2D13DD2D1311DD2D131D1D3DD2D1D3DD2DD2D13DD2D13111D3DD2D -1D3DD2DD2D13DD2D1311DD2D131D3DD2D1D3DD2DD2D13DD2D13111DD2DD2D1DD2D12D -2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1DD2D1DD2D1DD22D111D3DD2D1D3DD2 -DD2D13DD2D13111D3DD2D1D3DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13DD2D1311D -D2D131; ! 351 steps +DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2D1DD2DD2D12DD2DD2D121D1D3DD +2D1D3DD2DD2D13DD2D1311DD2D131D1D3DD2D1D3DD2DD2D13DD2D13111D3DD2D1D3D3 +DD2D1D3DD2DD2D13DD2D13DD2D13DD2D13111DD2D131DD2DD2D1DD2D12D2D1DD2D13D +D2D1D2DD2DD2D13DD2D13111DD2D1DD2D1DD22D111D3DD2D1D3D3DD2D1D3DD2DD2D13 +DD2D13DD2D13DD2D131111D3DD2D1D3DD2DD2D13DD2D1311DD2D131; ! 331 steps (((((P -> Q) -> (~ R -> ~ S)) -> R) -> T) -> ((T -> P) -> (S -> P))) ; ! Meredith's axiom (SF) (GSZ 205->199) (RR 199->145) (SD 145->141) @@ -1406,7 +1407,7 @@ DD2D1DD2D1D2DD2D1211DD2D1DD2D1DD22D11DD2D112DD2D1D2D2D13DD2D11DD2D131 DD2D1DD2DD2D13D2DD2D1311DD2D1DD22D1DD2D1311; ! 43 steps (((P <-> Q) <-> R) <-> (P <-> (Q <-> R))) -; ! biass (RR) (SD 2127->1877) +; ! biass (RR) (SD 2127->1851) ~ ((~ ((~ ((P -> Q) -> ~ (R -> S)) -> T) -> ~ (U -> ~ ((S -> V) -> ~ (R -> P)))) -> ~ ((S -> ~ ((Q -> T) -> ~ (U -> V))) -> ~ (~ ((R -> U) -> ~ (T -> R)) -> P))) -> ~ (~ ((W -> ~ ((X -> Y) -> ~ (Z -> @@ -1414,30 +1415,30 @@ DD2D1DD2DD2D13D2DD2D1311DD2D1DD22D1DD2D1311; ! 43 steps ~ (X -> W)) -> Y) -> ~ (Z -> ~ ((W -> A) -> ~ (B -> C)))))) ; ! Result of proof DD3DD2DD2DD2D13DD2D1311D1DD2DD2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2DD -2D12DD2D1D2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2DD2D12DD2D11DD2D1DD2D1 -21D3DD2D1D3DD2DD2D13DD2D1311DD2D131D1DD2D1D2DD2D13DD2D1D2DD2DD2D13DD2 -D1311DD2D111DD2D111DD2DD2D12DD2D11DD2D12DD2D1D2D1D3DD2D1D3DD2DD2D13DD -2D1311DD2D131D3DD2D1D3DD2DD2D13DD2D13111D11DD2D1D2D1DD2DD2D1DD2D1DD2D -1DD2D1D2D1DD2DD2D13D2DD2D1311DD2D1D2DD2D12113D2D1D3DD2DD2D13DD2D1311D -D2D1DD2D1D2DD2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D1DD2D1D2DD2D1DD2D13D -D2D1D2DD2DD2D13DD2D13111DD2D1311DD2D131DD2D1DD2D13DD2D1DD22D2DD2D13DD -2D1311D2D1D3DD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D13111DD2DD2D12DD2D -1D2D1D3DD2D1D3DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13DD2D1311DD2D131D1DD -211DD2DD2D12DD2D1D2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2DD2D12DD2D11DD -2D12DD2D13DD2D1DD22D11DD2D11DD2D131D1D3DD2D1D3DD2DD2D13DD2D1311DD2D13 -1DD2D1D2DD2D12DD2D13DD2D1DD22D11DD2D11DD2D131DD2D13DD2D1DD22D1DD2D131 -DD2D11DD2D131DD2DD2D1DD2D1D2DD2D13DD2D1D2DD2DD2D13DD2D131111DD2DD2D12 -DD2D1D2D1DD2D1D2DD2D13DD2D1D2DD2DD2D13DD2D131111DD2DD2D12DD2D11DD2D12 -DD2D13DD2D1DD22D11DD2D11DD2D131D1DD2D1D2DD2D1DD2D1D2DD2D13DD2D1D2DD2D -D2D13DD2D1311111DD2D111DD2DD2D12DD2D11DD2D12DD2D1D2D1D3DD2D1D3DD2DD2D -13DD2D13111D3DD2D1D3DD2DD2D13DD2D1311DD2D131D11DD2D1D2D1DD2DD2D1DD2D1 -DD2D1DD2D1D2D1DD2DD2D13D2DD2D1311DD2D1D2DD2D12113D2D1D3DD2DD2D13DD2D1 -311DD2D1DD2D1D2DD2D1D2D3DD2D1D3DD2DD2D13DD2D1311DD2DD2D1DD2D1D2DD2D13 -DD2D1D2DD2DD2D13DD2D131111DD2D1DD22D11DD2D11DD2D131DD2DD2D12DD2D11DD2 -D131D1DD2D1D2DD2D13111DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD -2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2DD2D12DD2D1D2D1D3DD2D -1D3DD2DD2D13DD2D1311DD2D131D3DD2D1D3DD2DD2D13DD2D13111D1DD211DD2DD2D1 -2DD2D1D2D1DD2D1D2DD2D13DD2D1D2DD2DD2D13DD2D131111DD2DD2D12DD2D11DD2D1 -DD2D121D3DD2D1D3DD2DD2D13DD2D1311DD2D131D1D3DD2D1D3DD2DD2D13DD2D13111 -DD2D1D2DD2D1DD2D121D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2D13DD2D1DD22D1 -1DD2D11DD2D131; ! 1877 steps +2D12DD2D1D2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2DD2D12DD2D11DD2D12DD2D +13DD2D1DD22D1DD2D131DD2D11DD2D131D1DD2D1D2DD2D13DD2D1D2DD2DD2D13DD2D1 +311DD2D111DD2D111DD2DD2D12DD2D11DD2D12DD2D1D2D1D3DD2D1D3DD2DD2D13DD2D +1311DD2D131D3DD2D1D3DD2DD2D13DD2D13111D11DD2D1D2D1DD2DD2D1DD2D1DD2D1D +D2D1D2D1DD2DD2D13D2DD2D1311DD2D1D2DD2D12113D2D1D3DD2DD2D13DD2D1311DD2 +D1DD2D1D2DD2D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D1DD2D1D2DD2D1DD2D13DD2 +D1D2DD2DD2D13DD2D13111DD2D1311DD2D131DD2D1DD2D13DD2D1DD22D2DD2D13DD2D +1311D2D1D3DD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D13111DD2D1DD22D21DD2 +D1D2D1D3DD2D1D3DD2DD2D13DD2D13111D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2 +DD2D12DD2D1D2D1DD2D13DD2D1D2DD2DD2D13DD2D13111DD2DD2D12DD2D11DD2D12DD +2D13DD2D1DD22D11DD2D11DD2D131D1D3DD2D1D3DD2DD2D13DD2D1311DD2D131DD2D1 +D2DD2D12DD2D13DD2D1DD22D11DD2D11DD2D131DD2D13DD2D1DD22D1DD2D131DD2D11 +DD2D131DD2DD2D1DD2D1D2DD2D13DD2D1D2DD2DD2D13DD2D131111DD2DD2D12DD2D1D +2D1DD2D1D2DD2D13DD2D1D2DD2DD2D13DD2D131111DD2DD2D12DD2D11DD2D12DD2D13 +DD2D1DD22D11DD2D11DD2D131D1DD2D1DD2D1DD22D111DD2D13DD2D1D2DD2DD2D13DD +2D1311DD2D111DD2DD2D12DD2D11DD2D12DD2D1D2D1D3DD2D1D3DD2DD2D13DD2D1311 +1D3DD2D1D3DD2DD2D13DD2D1311DD2D131D11DD2D1D2D1DD2DD2D1DD2D1DD2D1DD2D1 +D2D1DD2DD2D13D2DD2D1311DD2D1D2DD2D12113D2D1D3DD2DD2D13DD2D1311DD2D1DD +2D1D2DD2D1D2D3DD2D1D3DD2DD2D13DD2D1311DD2DD2D1DD2D13DD2D1D2DD2DD2D13D +D2D13111DD2DD2D12DD2D11DD2D131D1DD2D1D2DD2D1311DD2D1DD22D11DD2D11DD2D +1311DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311D3DD2D +1D3DD2DD2D13DD2D1311DD2D131DD2D1DD22D21DD2D1D2D1D3DD2D1D3DD2DD2D13DD2 +D1311DD2D131D3DD2D1D3DD2DD2D13DD2D13111DD2DD2D12DD2D1D2D1DD2D1D2DD2D1 +3DD2D1D2DD2DD2D13DD2D131111DD2DD2D12DD2D11DD2D12DD2D13DD2D1DD22D1DD2D +131DD2D11DD2D131D1D3DD2D1D3DD2DD2D13DD2D13111DD2D1D2DD2D12DD2D13DD2D1 +DD22D1DD2D131DD2D11DD2D131DD2D13DD2D1DD22D11DD2D11DD2D131 +; ! 1851 steps