| vout |
|---|
PrNUD../f53f1.. 0.04 barsTMYdq../b6252.. ownership of 4d1b3.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0TMWC4../8aceb.. ownership of 3b16c.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0PUKKP../d1116.. doc published by PrPhD..Definition FalseFalse := ∀ x0 : ο . x0Definition notnot := λ x0 : ο . x0 ⟶ FalseTheorem 4d1b3.. : ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ι → ι → ι → ι → ο . ∀ x4 : ι → ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 : ι → ο . ∀ x7 : ι → ι . ∀ x8 x9 : ι → ο . ∀ x10 x11 : ι → ι . ∀ x12 . ∀ x13 x14 : ι → ι → ι . ∀ x15 : ι → ι → ι → ι → ι . ∀ x16 : ι → ι → ο . ∀ x17 x18 . ∀ x19 : ι → ο . ∀ x20 x21 x22 x23 x24 x25 x26 . ∀ x27 : ι → ι . ∀ x28 x29 : ι → ο . ∀ x30 : ι → ι → ι → ι . ∀ x31 . ∀ x32 : ι → ι → ι → ι → ι . ∀ x33 : ι → ι → ο . ∀ x34 : ι → ο . ∀ x35 : ι → ι . ∀ x36 : ι → ι → ι → ι → ο . ∀ x37 x38 : ι → ο . ∀ x39 . ∀ x40 : ι → ο . (∀ x41 x42 . x40 x42 ⟶ (x42 = x41 ⟶ False) ⟶ x40 x41 ⟶ False) ⟶ (∀ x41 x42 . x0 x41 x42 ⟶ x40 x42 ⟶ False) ⟶ (∀ x41 . x40 x41 ⟶ (x41 = x39 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 . x0 x41 x42 ⟶ x2 x42 (x1 x43) ⟶ x40 x43 ⟶ False) ⟶ (∀ x41 x42 x43 x44 x45 x46 . (x38 x46 ⟶ False) ⟶ x34 x46 ⟶ x37 x46 ⟶ x2 x41 (x35 x46) ⟶ x2 x45 (x35 x46) ⟶ x2 x42 (x35 x46) ⟶ x2 x44 (x35 x46) ⟶ x2 x43 (x35 x46) ⟶ x36 x46 x41 x45 x44 ⟶ x36 x46 x41 x42 x43 ⟶ x44 = x43 ⟶ (x36 x46 x41 x45 x42 ⟶ False) ⟶ (x43 = x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 x45 x46 . (x38 x46 ⟶ False) ⟶ x34 x46 ⟶ x37 x46 ⟶ x2 x41 (x35 x46) ⟶ x2 x45 (x35 x46) ⟶ x2 x42 (x35 x46) ⟶ x2 x44 (x35 x46) ⟶ x2 x43 (x35 x46) ⟶ x36 x46 x41 x45 x44 ⟶ x36 x46 x41 x42 x43 ⟶ x44 = x43 ⟶ (x36 x46 x41 x45 x42 ⟶ False) ⟶ (x44 = x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 . x0 x42 x43 ⟶ x2 x43 (x1 x41) ⟶ (x2 x42 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 x45 . (x38 x45 ⟶ False) ⟶ x34 x45 ⟶ x37 x45 ⟶ x2 x41 (x35 x45) ⟶ x2 x44 (x35 x45) ⟶ x2 x42 (x35 x45) ⟶ x2 x43 (x35 x45) ⟶ x3 x45 x41 x44 x42 x43 ⟶ (x3 x45 x43 x42 x44 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 x45 . (x38 x45 ⟶ False) ⟶ x34 x45 ⟶ x37 x45 ⟶ x2 x41 (x35 x45) ⟶ x2 x44 (x35 x45) ⟶ x2 x42 (x35 x45) ⟶ x2 x43 (x35 x45) ⟶ x3 x45 x41 x44 x42 x43 ⟶ (x3 x45 x43 x42 x41 x44 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 x45 . (x38 x45 ⟶ False) ⟶ x34 x45 ⟶ x37 x45 ⟶ x2 x41 (x35 x45) ⟶ x2 x44 (x35 x45) ⟶ x2 x42 (x35 x45) ⟶ x2 x43 (x35 x45) ⟶ x3 x45 x41 x44 x42 x43 ⟶ (x3 x45 x42 x43 x44 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 x45 . (x38 x45 ⟶ False) ⟶ x34 x45 ⟶ x37 x45 ⟶ x2 x41 (x35 x45) ⟶ x2 x44 (x35 x45) ⟶ x2 x42 (x35 x45) ⟶ x2 x43 (x35 x45) ⟶ x3 x45 x41 x44 x42 x43 ⟶ (x3 x45 x42 x43 x41 x44 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 x45 . (x38 x45 ⟶ False) ⟶ x34 x45 ⟶ x37 x45 ⟶ x2 x41 (x35 x45) ⟶ x2 x44 (x35 x45) ⟶ x2 x42 (x35 x45) ⟶ x2 x43 (x35 x45) ⟶ x3 x45 x41 x44 x42 x43 ⟶ (x3 x45 x44 x41 x43 x42 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 x45 . (x38 x45 ⟶ False) ⟶ x34 x45 ⟶ x37 x45 ⟶ x2 x41 (x35 x45) ⟶ x2 x44 (x35 x45) ⟶ x2 x42 (x35 x45) ⟶ x2 x43 (x35 x45) ⟶ x3 x45 x41 x44 x42 x43 ⟶ (x3 x45 x44 x41 x42 x43 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 x45 . (x38 x45 ⟶ False) ⟶ x34 x45 ⟶ x37 x45 ⟶ x2 x41 (x35 x45) ⟶ x2 x44 (x35 x45) ⟶ x2 x42 (x35 x45) ⟶ x2 x43 (x35 x45) ⟶ x3 x45 x41 x44 x42 x43 ⟶ (x3 x45 x41 x44 x43 x42 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x33 x42 x41 ⟶ (x2 x42 (x1 x41) ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x2 x42 (x1 x41) ⟶ (x33 x42 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x2 x41 x42 ⟶ (x40 x42 ⟶ False) ⟶ (x0 x41 x42 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 . (x38 x44 ⟶ False) ⟶ x34 x44 ⟶ x37 x44 ⟶ x2 x41 (x35 x44) ⟶ x2 x43 (x35 x44) ⟶ x2 x42 (x1 (x35 x44)) ⟶ x5 x42 x44 ⟶ x0 x41 x42 ⟶ x0 x43 x42 ⟶ (x41 = x43 ⟶ False) ⟶ (x42 = x4 x44 x41 x43 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 . (x38 x44 ⟶ False) ⟶ x34 x44 ⟶ x37 x44 ⟶ x2 x41 (x35 x44) ⟶ x2 x43 (x35 x44) ⟶ x2 x42 (x1 (x35 x44)) ⟶ x5 x42 x44 ⟶ x0 x41 x42 ⟶ x0 x43 x42 ⟶ (x41 = x43 ⟶ False) ⟶ x41 = x43 ⟶ False) ⟶ (∀ x41 x42 x43 x44 . (x38 x44 ⟶ False) ⟶ x34 x44 ⟶ x37 x44 ⟶ x2 x41 (x35 x44) ⟶ x2 x43 (x35 x44) ⟶ x2 x42 (x1 (x35 x44)) ⟶ x42 = x4 x44 x41 x43 ⟶ (x41 = x43 ⟶ False) ⟶ x41 = x43 ⟶ False) ⟶ (∀ x41 x42 x43 x44 . (x38 x44 ⟶ False) ⟶ x34 x44 ⟶ x37 x44 ⟶ x2 x41 (x35 x44) ⟶ x2 x43 (x35 x44) ⟶ x2 x42 (x1 (x35 x44)) ⟶ x42 = x4 x44 x41 x43 ⟶ (x41 = x43 ⟶ False) ⟶ (x0 x43 x42 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 . (x38 x44 ⟶ False) ⟶ x34 x44 ⟶ x37 x44 ⟶ x2 x41 (x35 x44) ⟶ x2 x43 (x35 x44) ⟶ x2 x42 (x1 (x35 x44)) ⟶ x42 = x4 x44 x41 x43 ⟶ (x41 = x43 ⟶ False) ⟶ (x0 x41 x42 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 . (x38 x44 ⟶ False) ⟶ x34 x44 ⟶ x37 x44 ⟶ x2 x41 (x35 x44) ⟶ x2 x43 (x35 x44) ⟶ x2 x42 (x1 (x35 x44)) ⟶ x42 = x4 x44 x41 x43 ⟶ (x41 = x43 ⟶ False) ⟶ (x5 x42 x44 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 x45 . (x38 x45 ⟶ False) ⟶ x34 x45 ⟶ x37 x45 ⟶ x2 x41 (x35 x45) ⟶ x2 x44 (x35 x45) ⟶ x2 x42 (x35 x45) ⟶ x2 x43 (x35 x45) ⟶ x0 x41 (x4 x45 x44 x42) ⟶ (x44 = x42 ⟶ False) ⟶ x3 x45 x44 x42 x41 x43 ⟶ (x0 x43 (x4 x45 x44 x42) ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 x45 . (x38 x45 ⟶ False) ⟶ x34 x45 ⟶ x37 x45 ⟶ x2 x41 (x35 x45) ⟶ x2 x44 (x35 x45) ⟶ x2 x42 (x35 x45) ⟶ x2 x43 (x35 x45) ⟶ x0 x41 (x4 x45 x44 x42) ⟶ (x44 = x42 ⟶ False) ⟶ x0 x43 (x4 x45 x44 x42) ⟶ (x3 x45 x44 x42 x41 x43 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 x45 . (x38 x45 ⟶ False) ⟶ x34 x45 ⟶ x37 x45 ⟶ x2 x41 (x35 x45) ⟶ x2 x44 (x35 x45) ⟶ x2 x42 (x35 x45) ⟶ x2 x43 (x1 (x35 x45)) ⟶ x5 x43 x45 ⟶ x0 x41 x43 ⟶ x0 x44 x43 ⟶ x0 x42 x43 ⟶ (x36 x45 x41 x44 x42 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 . (x38 x44 ⟶ False) ⟶ x34 x44 ⟶ x37 x44 ⟶ x2 x41 (x35 x44) ⟶ x2 x43 (x35 x44) ⟶ x2 x42 (x35 x44) ⟶ x36 x44 x41 x43 x42 ⟶ (x0 x42 (x32 x42 x43 x41 x44) ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 . (x38 x44 ⟶ False) ⟶ x34 x44 ⟶ x37 x44 ⟶ x2 x41 (x35 x44) ⟶ x2 x43 (x35 x44) ⟶ x2 x42 (x35 x44) ⟶ x36 x44 x41 x43 x42 ⟶ (x0 x43 (x32 x42 x43 x41 x44) ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 . (x38 x44 ⟶ False) ⟶ x34 x44 ⟶ x37 x44 ⟶ x2 x41 (x35 x44) ⟶ x2 x43 (x35 x44) ⟶ x2 x42 (x35 x44) ⟶ x36 x44 x41 x43 x42 ⟶ (x0 x41 (x32 x42 x43 x41 x44) ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 . (x38 x44 ⟶ False) ⟶ x34 x44 ⟶ x37 x44 ⟶ x2 x41 (x35 x44) ⟶ x2 x43 (x35 x44) ⟶ x2 x42 (x35 x44) ⟶ x36 x44 x41 x43 x42 ⟶ (x5 (x32 x42 x43 x41 x44) x44 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 . (x38 x44 ⟶ False) ⟶ x34 x44 ⟶ x37 x44 ⟶ x2 x41 (x35 x44) ⟶ x2 x43 (x35 x44) ⟶ x2 x42 (x35 x44) ⟶ x36 x44 x41 x43 x42 ⟶ (x2 (x32 x42 x43 x41 x44) (x1 (x35 x44)) ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x0 x42 x41 ⟶ (x2 x42 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 . (x38 x43 ⟶ False) ⟶ x34 x43 ⟶ x37 x43 ⟶ x2 x41 (x35 x43) ⟶ x2 x42 (x35 x43) ⟶ (x0 x42 (x4 x43 x41 x42) ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 . (x38 x43 ⟶ False) ⟶ x34 x43 ⟶ x37 x43 ⟶ x2 x41 (x35 x43) ⟶ x2 x42 (x35 x43) ⟶ (x0 x41 (x4 x43 x41 x42) ⟶ False) ⟶ False) ⟶ (x40 x31 ⟶ False) ⟶ (∀ x41 . (x33 x41 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 . (x38 x43 ⟶ False) ⟶ x34 x43 ⟶ x37 x43 ⟶ x2 x41 (x35 x43) ⟶ x2 x42 (x35 x43) ⟶ (x4 x43 x41 x42 = x30 x43 x41 x42 ⟶ False) ⟶ False) ⟶ (∀ x41 . (x6 x41 ⟶ False) ⟶ x8 x41 ⟶ x40 (x7 x41) ⟶ False) ⟶ (∀ x41 . (x6 x41 ⟶ False) ⟶ x8 x41 ⟶ (x2 (x7 x41) (x1 (x35 x41)) ⟶ False) ⟶ False) ⟶ (∀ x41 . (x38 x41 ⟶ False) ⟶ x8 x41 ⟶ x9 (x10 x41) ⟶ False) ⟶ (∀ x41 . (x38 x41 ⟶ False) ⟶ x8 x41 ⟶ (x2 (x10 x41) (x1 (x35 x41)) ⟶ False) ⟶ False) ⟶ (∀ x41 . (x6 x41 ⟶ False) ⟶ x8 x41 ⟶ (x9 (x11 x41) ⟶ False) ⟶ False) ⟶ (∀ x41 . (x6 x41 ⟶ False) ⟶ x8 x41 ⟶ x40 (x11 x41) ⟶ False) ⟶ (∀ x41 . (x6 x41 ⟶ False) ⟶ x8 x41 ⟶ (x2 (x11 x41) (x1 (x35 x41)) ⟶ False) ⟶ False) ⟶ (∀ x41 . (x29 x41 ⟶ False) ⟶ x8 x41 ⟶ x28 (x35 x41) ⟶ False) ⟶ (∀ x41 . x29 x41 ⟶ x8 x41 ⟶ (x28 (x35 x41) ⟶ False) ⟶ False) ⟶ (∀ x41 . x38 x41 ⟶ x8 x41 ⟶ (x9 (x35 x41) ⟶ False) ⟶ False) ⟶ (∀ x41 . (x38 x41 ⟶ False) ⟶ x8 x41 ⟶ x9 (x35 x41) ⟶ False) ⟶ (∀ x41 . (x6 x41 ⟶ False) ⟶ x8 x41 ⟶ x40 (x35 x41) ⟶ False) ⟶ (∀ x41 . x6 x41 ⟶ x8 x41 ⟶ (x40 (x35 x41) ⟶ False) ⟶ False) ⟶ (∀ x41 . (x2 (x27 x41) x41 ⟶ False) ⟶ False) ⟶ ((x8 x12 ⟶ False) ⟶ False) ⟶ ((x37 x26 ⟶ False) ⟶ False) ⟶ (∀ x41 . x37 x41 ⟶ (x8 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 . (x38 x43 ⟶ False) ⟶ x34 x43 ⟶ x37 x43 ⟶ x2 x41 (x35 x43) ⟶ x2 x42 (x35 x43) ⟶ (x2 (x4 x43 x41 x42) (x1 (x35 x43)) ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 . (x38 x43 ⟶ False) ⟶ x34 x43 ⟶ x37 x43 ⟶ x2 x41 (x35 x43) ⟶ x2 x42 (x35 x43) ⟶ (x2 (x30 x43 x41 x42) (x1 (x35 x43)) ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 . (x38 x44 ⟶ False) ⟶ x34 x44 ⟶ x37 x44 ⟶ x2 x41 (x1 (x35 x44)) ⟶ x2 x43 (x35 x44) ⟶ x2 x42 (x35 x44) ⟶ (x43 = x42 ⟶ False) ⟶ x41 = x4 x44 x43 x42 ⟶ (x5 x41 x44 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . (x38 x42 ⟶ False) ⟶ x34 x42 ⟶ x37 x42 ⟶ x2 x41 (x1 (x35 x42)) ⟶ x5 x41 x42 ⟶ (x41 = x4 x42 (x14 x41 x42) (x13 x41 x42) ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . (x38 x42 ⟶ False) ⟶ x34 x42 ⟶ x37 x42 ⟶ x2 x41 (x1 (x35 x42)) ⟶ x5 x41 x42 ⟶ x14 x41 x42 = x13 x41 x42 ⟶ False) ⟶ (∀ x41 x42 . (x38 x42 ⟶ False) ⟶ x34 x42 ⟶ x37 x42 ⟶ x2 x41 (x1 (x35 x42)) ⟶ x5 x41 x42 ⟶ (x2 (x13 x41 x42) (x35 x42) ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . (x38 x42 ⟶ False) ⟶ x34 x42 ⟶ x37 x42 ⟶ x2 x41 (x1 (x35 x42)) ⟶ x5 x41 x42 ⟶ (x2 (x14 x41 x42) (x35 x42) ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 . (x38 x44 ⟶ False) ⟶ x34 x44 ⟶ x37 x44 ⟶ x2 x41 (x35 x44) ⟶ x2 x43 (x35 x44) ⟶ x2 x42 (x1 (x35 x44)) ⟶ (x36 x44 x41 x43 (x15 x42 x43 x41 x44) ⟶ False) ⟶ (x0 (x15 x42 x43 x41 x44) x42 ⟶ False) ⟶ (x42 = x30 x44 x41 x43 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 . (x38 x44 ⟶ False) ⟶ x34 x44 ⟶ x37 x44 ⟶ x2 x41 (x35 x44) ⟶ x2 x43 (x35 x44) ⟶ x2 x42 (x1 (x35 x44)) ⟶ x0 (x15 x42 x43 x41 x44) x42 ⟶ x36 x44 x41 x43 (x15 x42 x43 x41 x44) ⟶ (x42 = x30 x44 x41 x43 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 . (x38 x44 ⟶ False) ⟶ x34 x44 ⟶ x37 x44 ⟶ x2 x41 (x35 x44) ⟶ x2 x43 (x35 x44) ⟶ x2 x42 (x1 (x35 x44)) ⟶ (x2 (x15 x42 x43 x41 x44) (x35 x44) ⟶ False) ⟶ (x42 = x30 x44 x41 x43 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 x45 . (x38 x45 ⟶ False) ⟶ x34 x45 ⟶ x37 x45 ⟶ x2 x41 (x35 x45) ⟶ x2 x44 (x35 x45) ⟶ x2 x42 (x1 (x35 x45)) ⟶ x42 = x30 x45 x41 x44 ⟶ x2 x43 (x35 x45) ⟶ x36 x45 x41 x44 x43 ⟶ (x0 x43 x42 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 x44 x45 . (x38 x45 ⟶ False) ⟶ x34 x45 ⟶ x37 x45 ⟶ x2 x41 (x35 x45) ⟶ x2 x44 (x35 x45) ⟶ x2 x42 (x1 (x35 x45)) ⟶ x42 = x30 x45 x41 x44 ⟶ x2 x43 (x35 x45) ⟶ x0 x43 x42 ⟶ (x36 x45 x41 x44 x43 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 x43 . (x38 x43 ⟶ False) ⟶ x34 x43 ⟶ x37 x43 ⟶ x2 x41 (x35 x43) ⟶ x2 x42 (x35 x43) ⟶ (x4 x43 x41 x42 = x4 x43 x42 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . x8 x41 ⟶ x16 x41 x39 ⟶ (x6 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . x8 x41 ⟶ x6 x41 ⟶ (x16 x41 x39 ⟶ False) ⟶ False) ⟶ (∀ x41 . x8 x41 ⟶ (x29 x41 ⟶ False) ⟶ x38 x41 ⟶ False) ⟶ (∀ x41 . x8 x41 ⟶ x38 x41 ⟶ (x29 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . x8 x41 ⟶ (x29 x41 ⟶ False) ⟶ x29 x41 ⟶ False) ⟶ (∀ x41 . x8 x41 ⟶ (x29 x41 ⟶ False) ⟶ x6 x41 ⟶ False) ⟶ (∀ x41 . x8 x41 ⟶ x6 x41 ⟶ (x29 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . x8 x41 ⟶ x6 x41 ⟶ (x6 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . x8 x41 ⟶ (x38 x41 ⟶ False) ⟶ x6 x41 ⟶ False) ⟶ (∀ x41 . x8 x41 ⟶ x6 x41 ⟶ (x38 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . x8 x41 ⟶ (x38 x41 ⟶ False) ⟶ x6 x41 ⟶ False) ⟶ (∀ x41 . x8 x41 ⟶ x16 x41 x31 ⟶ (x38 x41 ⟶ False) ⟶ False) ⟶ (∀ x41 . x8 x41 ⟶ x16 x41 x31 ⟶ x6 x41 ⟶ False) ⟶ (∀ x41 . x8 x41 ⟶ (x6 x41 ⟶ False) ⟶ x38 x41 ⟶ (x16 x41 x31 ⟶ False) ⟶ False) ⟶ (∀ x41 x42 . x0 x41 x42 ⟶ x0 x42 x41 ⟶ False) ⟶ (x36 x25 x22 x23 x24 ⟶ False) ⟶ ((x3 x25 x23 x24 x18 x17 ⟶ False) ⟶ (x36 x25 x22 x23 x17 ⟶ False) ⟶ False) ⟶ ((x3 x25 x23 x24 x18 x17 ⟶ False) ⟶ (x3 x25 x20 x24 x21 x17 ⟶ False) ⟶ False) ⟶ ((x3 x25 x23 x24 x18 x17 ⟶ False) ⟶ (x3 x25 x23 x20 x18 x21 ⟶ False) ⟶ False) ⟶ ((x3 x25 x23 x24 x18 x17 ⟶ False) ⟶ (x36 x25 x22 x20 x21 ⟶ False) ⟶ False) ⟶ ((x3 x25 x23 x24 x18 x17 ⟶ False) ⟶ x36 x25 x22 x23 x20 ⟶ False) ⟶ ((x3 x25 x23 x24 x18 x17 ⟶ False) ⟶ (x2 x21 (x35 x25) ⟶ False) ⟶ False) ⟶ ((x3 x25 x23 x24 x18 x17 ⟶ False) ⟶ (x2 x20 (x35 x25) ⟶ False) ⟶ False) ⟶ ((x3 x25 x23 x24 x18 x17 ⟶ False) ⟶ (x36 x25 x22 x23 x24 ⟶ False) ⟶ False) ⟶ ((x36 x25 x22 x24 x17 ⟶ False) ⟶ (x36 x25 x22 x23 x17 ⟶ False) ⟶ False) ⟶ ((x36 x25 x22 x24 x17 ⟶ False) ⟶ (x3 x25 x20 x24 x21 x17 ⟶ False) ⟶ False) ⟶ ((x36 x25 x22 x24 x17 ⟶ False) ⟶ (x3 x25 x23 x20 x18 x21 ⟶ False) ⟶ False) ⟶ ((x36 x25 x22 x24 x17 ⟶ False) ⟶ (x36 x25 x22 x20 x21 ⟶ False) ⟶ False) ⟶ ((x36 x25 x22 x24 x17 ⟶ False) ⟶ x36 x25 x22 x23 x20 ⟶ False) ⟶ ((x36 x25 x22 x24 x17 ⟶ False) ⟶ (x2 x21 (x35 x25) ⟶ False) ⟶ False) ⟶ ((x36 x25 x22 x24 x17 ⟶ False) ⟶ (x2 x20 (x35 x25) ⟶ False) ⟶ False) ⟶ ((x36 x25 x22 x24 x17 ⟶ False) ⟶ (x36 x25 x22 x23 x24 ⟶ False) ⟶ False) ⟶ (x36 x25 x22 x23 x24 ⟶ (x36 x25 x22 x23 x17 ⟶ False) ⟶ False) ⟶ (x36 x25 x22 x23 x24 ⟶ (x3 x25 x20 x24 x21 x17 ⟶ False) ⟶ False) ⟶ (x36 x25 x22 x23 x24 ⟶ (x3 x25 x23 x20 x18 x21 ⟶ False) ⟶ False) ⟶ (x36 x25 x22 x23 x24 ⟶ (x36 x25 x22 x20 x21 ⟶ False) ⟶ False) ⟶ (x36 x25 x22 x23 x24 ⟶ x36 x25 x22 x23 x20 ⟶ False) ⟶ (x36 x25 x22 x23 x24 ⟶ (x2 x21 (x35 x25) ⟶ False) ⟶ False) ⟶ (x36 x25 x22 x23 x24 ⟶ (x2 x20 (x35 x25) ⟶ False) ⟶ False) ⟶ (x36 x25 x22 x23 x24 ⟶ (x36 x25 x22 x23 x24 ⟶ False) ⟶ False) ⟶ (x22 = x18 ⟶ False) ⟶ (x22 = x23 ⟶ False) ⟶ ((x36 x25 x22 x23 x17 ⟶ False) ⟶ False) ⟶ ((x36 x25 x22 x23 x18 ⟶ False) ⟶ False) ⟶ ((x2 x24 (x35 x25) ⟶ False) ⟶ False) ⟶ ((x2 x17 (x35 x25) ⟶ False) ⟶ False) ⟶ ((x2 x18 (x35 x25) ⟶ False) ⟶ False) ⟶ ((x2 x23 (x35 x25) ⟶ False) ⟶ False) ⟶ ((x2 x22 (x35 x25) ⟶ False) ⟶ False) ⟶ ((x37 x25 ⟶ False) ⟶ False) ⟶ ((x19 x25 ⟶ False) ⟶ False) ⟶ ((x34 x25 ⟶ False) ⟶ False) ⟶ (x38 x25 ⟶ False) ⟶ False (proof) |
|