Search for blocks/addresses/...

Proofgold Asset

asset id
454ede6c41a0ef17008c1344a47c34cd8ed40597428ff22a5c2826e2b0d217a9
asset hash
755b134e27611d44150af9c5ab6608640331a9055e102e4ba2e42190de1c3425
bday / block
35123
tx
a0441..
preasset
doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem f8cd3.. : ∀ 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 x43 . ∀ x44 : ι → ι . ∀ x45 : ι → ι → ο . ∀ x46 : ι → ι . ∀ x47 . ∀ x48 : ι → ο . (∀ x49 x50 . x48 x50 ⟶ (x50 = x49 ⟶ False) ⟶ x48 x49 ⟶ False) ⟶ (∀ x49 x50 . x0 x49 x50 ⟶ x48 x50 ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ (x49 = x47 ⟶ False) ⟶ False) ⟶ (∀ x49 . x1 x49 ⟶ (x2 x49 x3 = x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 x51 . x0 x49 x50 ⟶ x45 x50 (x46 x51) ⟶ x48 x51 ⟶ False) ⟶ (∀ x49 . x1 x49 ⟶ (x2 x4 x49 = x4 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 x51 . x0 x50 x51 ⟶ x45 x51 (x46 x49) ⟶ (x45 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x1 x49 ⟶ (x5 x49 x4 = x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x1 x49 ⟶ (x2 x49 x4 = x4 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x6 x50 x49 ⟶ (x45 x50 (x46 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x45 x50 (x46 x49) ⟶ (x6 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x1 x49 ⟶ (x7 x3 x49 = x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x45 x49 x50 ⟶ (x48 x50 ⟶ False) ⟶ (x0 x49 x50 ⟶ False) ⟶ False) ⟶ (∀ x49 . x1 x49 ⟶ (x7 x49 x4 = x4 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x0 x50 x49 ⟶ (x45 x50 x49 ⟶ False) ⟶ False) ⟶ ((x45 x47 x8 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x1 x50 ⟶ x1 x49 ⟶ x7 x49 x50 = x44 x50 ⟶ (x50 = x4 ⟶ False) ⟶ (x49 = x44 x3 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x1 x50 ⟶ x1 x49 ⟶ (x5 (x44 x50) (x44 x49) = x5 x49 x50 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 x51 . x1 x51 ⟶ x1 x49 ⟶ x1 x50 ⟶ (x7 (x7 x51 x49) x50 = x7 x51 (x7 x49 x50) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 x51 . x1 x51 ⟶ x1 x49 ⟶ x1 x50 ⟶ (x7 x51 (x2 x49 x50) = x2 (x7 x51 x49) x50 ⟶ False) ⟶ False) ⟶ ((x45 x42 x43 ⟶ False) ⟶ False) ⟶ ((x45 x42 x9 ⟶ False) ⟶ False) ⟶ ((x41 x42 x43 x9 ⟶ False) ⟶ False) ⟶ ((x10 x42 ⟶ False) ⟶ False) ⟶ (x48 x42 ⟶ False) ⟶ (∀ x49 . x1 x49 ⟶ (x7 x49 (x44 x3) = x44 x49 ⟶ False) ⟶ False) ⟶ ((x45 x3 x43 ⟶ False) ⟶ False) ⟶ ((x45 x3 x9 ⟶ False) ⟶ False) ⟶ ((x41 x3 x43 x9 ⟶ False) ⟶ False) ⟶ ((x10 x3 ⟶ False) ⟶ False) ⟶ (x48 x3 ⟶ False) ⟶ ((x45 x11 x43 ⟶ False) ⟶ False) ⟶ ((x45 x11 x9 ⟶ False) ⟶ False) ⟶ ((x41 x11 x43 x9 ⟶ False) ⟶ False) ⟶ ((x48 x11 ⟶ False) ⟶ False) ⟶ ((x44 (x2 (x44 x3) x42) = x2 x3 x42 ⟶ False) ⟶ False) ⟶ ((x44 (x2 x3 x42) = x2 (x44 x3) x42 ⟶ False) ⟶ False) ⟶ ((x44 (x44 x42) = x42 ⟶ False) ⟶ False) ⟶ ((x44 (x44 x3) = x3 ⟶ False) ⟶ False) ⟶ ((x44 x42 = x44 x42 ⟶ False) ⟶ False) ⟶ ((x44 x3 = x44 x3 ⟶ False) ⟶ False) ⟶ ((x44 x11 = x11 ⟶ False) ⟶ False) ⟶ ((x7 (x2 (x44 x3) x42) (x44 x42) = x3 ⟶ False) ⟶ False) ⟶ ((x7 (x2 (x44 x3) x42) x42 = x44 x3 ⟶ False) ⟶ False) ⟶ ((x7 (x2 (x44 x3) x42) x3 = x2 (x44 x3) x42 ⟶ False) ⟶ False) ⟶ ((x7 (x2 x3 x42) (x44 x42) = x44 x3 ⟶ False) ⟶ False) ⟶ ((x7 (x2 x3 x42) x42 = x3 ⟶ False) ⟶ False) ⟶ ((x7 (x2 x3 x42) x3 = x2 x3 x42 ⟶ False) ⟶ False) ⟶ ((x7 (x2 x3 x42) x11 = x11 ⟶ False) ⟶ False) ⟶ ((x7 (x44 x42) (x2 (x44 x3) x42) = x3 ⟶ False) ⟶ False) ⟶ ((x7 (x44 x42) (x2 x3 x42) = x44 x3 ⟶ False) ⟶ False) ⟶ ((x7 (x44 x42) x3 = x44 x42 ⟶ False) ⟶ False) ⟶ ((x7 (x44 x42) x11 = x11 ⟶ False) ⟶ False) ⟶ ((x7 x42 (x2 (x44 x3) x42) = x44 x3 ⟶ False) ⟶ False) ⟶ ((x7 x42 (x2 x3 x42) = x3 ⟶ False) ⟶ False) ⟶ ((x7 x42 x3 = x42 ⟶ False) ⟶ False) ⟶ ((x7 x42 x11 = x11 ⟶ False) ⟶ False) ⟶ ((x7 x3 (x2 (x44 x3) x42) = x2 (x44 x3) x42 ⟶ False) ⟶ False) ⟶ ((x7 x3 (x2 x3 x42) = x2 x3 x42 ⟶ False) ⟶ False) ⟶ ((x7 x3 (x44 x42) = x44 x42 ⟶ False) ⟶ False) ⟶ ((x7 x3 x42 = x42 ⟶ False) ⟶ False) ⟶ ((x7 x3 x3 = x3 ⟶ False) ⟶ False) ⟶ ((x7 x3 x11 = x11 ⟶ False) ⟶ False) ⟶ ((x7 x11 (x2 x3 x42) = x11 ⟶ False) ⟶ False) ⟶ ((x7 x11 (x44 x42) = x11 ⟶ False) ⟶ False) ⟶ ((x7 x11 x42 = x11 ⟶ False) ⟶ False) ⟶ ((x7 x11 x3 = x11 ⟶ False) ⟶ False) ⟶ ((x7 x11 x11 = x11 ⟶ False) ⟶ False) ⟶ ((x2 (x44 x42) x42 = x44 x3 ⟶ False) ⟶ False) ⟶ ((x2 (x44 x3) x42 = x2 (x44 x3) x42 ⟶ False) ⟶ False) ⟶ ((x2 (x44 x3) x3 = x44 x3 ⟶ False) ⟶ False) ⟶ ((x2 x42 x42 = x3 ⟶ False) ⟶ False) ⟶ ((x2 x42 x3 = x42 ⟶ False) ⟶ False) ⟶ ((x2 x3 (x2 (x44 x3) x42) = x44 x42 ⟶ False) ⟶ False) ⟶ ((x2 x3 (x2 x3 x42) = x42 ⟶ False) ⟶ False) ⟶ ((x2 x3 (x44 x42) = x2 (x44 x3) x42 ⟶ False) ⟶ False) ⟶ ((x2 x3 (x44 x3) = x44 x3 ⟶ False) ⟶ False) ⟶ ((x2 x3 x42 = x2 x3 x42 ⟶ False) ⟶ False) ⟶ ((x2 x3 x3 = x3 ⟶ False) ⟶ False) ⟶ ((x5 (x2 (x44 x3) x42) (x2 (x44 x3) x42) = x11 ⟶ False) ⟶ False) ⟶ ((x5 (x2 (x44 x3) x42) (x2 x3 x42) = x44 x3 ⟶ False) ⟶ False) ⟶ ((x5 (x2 (x44 x3) x42) (x44 x3) = x2 x3 x42 ⟶ False) ⟶ False) ⟶ ((x5 (x2 (x44 x3) x42) x11 = x2 (x44 x3) x42 ⟶ False) ⟶ False) ⟶ ((x5 (x2 x3 x42) (x2 (x44 x3) x42) = x3 ⟶ False) ⟶ False) ⟶ ((x5 (x2 x3 x42) (x2 x3 x42) = x11 ⟶ False) ⟶ False) ⟶ ((x5 (x2 x3 x42) x3 = x2 (x44 x3) x42 ⟶ False) ⟶ False) ⟶ ((x5 (x2 x3 x42) x11 = x2 x3 x42 ⟶ False) ⟶ False) ⟶ ((x5 (x44 x42) (x44 x42) = x11 ⟶ False) ⟶ False) ⟶ ((x5 (x44 x42) (x44 x3) = x44 x3 ⟶ False) ⟶ False) ⟶ ((x5 (x44 x42) x11 = x44 x42 ⟶ False) ⟶ False) ⟶ ((x5 (x44 x3) (x2 (x44 x3) x42) = x2 (x44 x3) x42 ⟶ False) ⟶ False) ⟶ ((x5 (x44 x3) (x44 x42) = x3 ⟶ False) ⟶ False) ⟶ ((x5 (x44 x3) (x44 x3) = x11 ⟶ False) ⟶ False) ⟶ ((x5 (x44 x3) x3 = x44 x42 ⟶ False) ⟶ False) ⟶ ((x5 (x44 x3) x11 = x44 x3 ⟶ False) ⟶ False) ⟶ ((x5 x42 x42 = x11 ⟶ False) ⟶ False) ⟶ ((x5 x42 x3 = x3 ⟶ False) ⟶ False) ⟶ ((x5 x42 x11 = x42 ⟶ False) ⟶ False) ⟶ ((x5 x3 (x2 x3 x42) = x2 x3 x42 ⟶ False) ⟶ False) ⟶ ((x5 x3 (x44 x3) = x42 ⟶ False) ⟶ False) ⟶ ((x5 x3 x42 = x44 x3 ⟶ False) ⟶ False) ⟶ ((x5 x3 x3 = x11 ⟶ False) ⟶ False) ⟶ ((x5 x3 x11 = x3 ⟶ False) ⟶ False) ⟶ ((x5 x11 (x2 (x44 x3) x42) = x2 x3 x42 ⟶ False) ⟶ False) ⟶ ((x5 x11 (x2 x3 x42) = x2 (x44 x3) x42 ⟶ False) ⟶ False) ⟶ ((x5 x11 (x44 x42) = x42 ⟶ False) ⟶ False) ⟶ ((x5 x11 (x44 x3) = x3 ⟶ False) ⟶ False) ⟶ ((x5 x11 x42 = x44 x42 ⟶ False) ⟶ False) ⟶ ((x5 x11 x3 = x44 x3 ⟶ False) ⟶ False) ⟶ ((x5 x11 x11 = x11 ⟶ False) ⟶ False) ⟶ (∀ x49 . (x6 x49 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 x51 . (x48 x51 ⟶ False) ⟶ (x48 x49 ⟶ False) ⟶ x45 x49 (x46 x51) ⟶ x45 x50 x49 ⟶ (x41 x50 x51 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 x51 . (x48 x51 ⟶ False) ⟶ (x48 x49 ⟶ False) ⟶ x45 x49 (x46 x51) ⟶ x41 x50 x51 x49 ⟶ (x45 x50 x49 ⟶ False) ⟶ False) ⟶ ((x4 = x47 ⟶ False) ⟶ False) ⟶ ((x9 = x8 ⟶ False) ⟶ False) ⟶ ((x12 x13 ⟶ False) ⟶ False) ⟶ (x48 x13 ⟶ False) ⟶ ((x14 x15 ⟶ False) ⟶ False) ⟶ ((x48 x15 ⟶ False) ⟶ False) ⟶ ((x16 x17 ⟶ False) ⟶ False) ⟶ ((x14 x17 ⟶ False) ⟶ False) ⟶ ((x1 x17 ⟶ False) ⟶ False) ⟶ ((x48 x17 ⟶ False) ⟶ False) ⟶ ((x12 x18 ⟶ False) ⟶ False) ⟶ ((x40 x39 ⟶ False) ⟶ False) ⟶ ((x14 x39 ⟶ False) ⟶ False) ⟶ ((x16 x38 ⟶ False) ⟶ False) ⟶ ((x40 x38 ⟶ False) ⟶ False) ⟶ ((x14 x38 ⟶ False) ⟶ False) ⟶ ((x1 x38 ⟶ False) ⟶ False) ⟶ ((x10 x37 ⟶ False) ⟶ False) ⟶ ((x14 x37 ⟶ False) ⟶ False) ⟶ ((x16 x36 ⟶ False) ⟶ False) ⟶ ((x10 x36 ⟶ False) ⟶ False) ⟶ ((x14 x36 ⟶ False) ⟶ False) ⟶ ((x1 x36 ⟶ False) ⟶ False) ⟶ ((x1 x35 ⟶ False) ⟶ False) ⟶ (x48 x35 ⟶ False) ⟶ (x48 x34 ⟶ False) ⟶ ((x19 x20 ⟶ False) ⟶ False) ⟶ ((x33 x20 ⟶ False) ⟶ False) ⟶ ((x21 x20 ⟶ False) ⟶ False) ⟶ (x48 x20 ⟶ False) ⟶ ((x14 x22 ⟶ False) ⟶ False) ⟶ ((x16 x32 ⟶ False) ⟶ False) ⟶ ((x1 x23 ⟶ False) ⟶ False) ⟶ ((x48 x31 ⟶ False) ⟶ False) ⟶ ((x19 x24 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x1 x50 ⟶ x1 x49 ⟶ (x50 = x4 ⟶ False) ⟶ (x7 (x2 x49 x50) x50 = x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x1 x49 ⟶ (x44 (x44 x49) = x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . (x48 x50 ⟶ False) ⟶ x1 x50 ⟶ (x48 x49 ⟶ False) ⟶ x1 x49 ⟶ x48 (x2 x50 x49) ⟶ False) ⟶ (∀ x49 x50 . x16 x50 ⟶ x16 x49 ⟶ (x16 (x2 x50 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . (x48 x50 ⟶ False) ⟶ x1 x50 ⟶ (x48 x49 ⟶ False) ⟶ x1 x49 ⟶ x48 (x7 x50 x49) ⟶ False) ⟶ (∀ x49 x50 . x16 x50 ⟶ x16 x49 ⟶ (x16 (x5 x50 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x16 x50 ⟶ x16 x49 ⟶ (x16 (x7 x50 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 . (x48 x49 ⟶ False) ⟶ x1 x49 ⟶ (x1 (x44 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 . (x48 x49 ⟶ False) ⟶ x1 x49 ⟶ x48 (x44 x49) ⟶ False) ⟶ ((x19 x8 ⟶ False) ⟶ False) ⟶ (x48 x8 ⟶ False) ⟶ (∀ x49 x50 . x1 x50 ⟶ x1 x49 ⟶ (x1 (x2 x50 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x1 x50 ⟶ x1 x49 ⟶ (x1 (x5 x50 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 . x16 x49 ⟶ (x16 (x44 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 . x16 x49 ⟶ (x1 (x44 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x1 x50 ⟶ x1 x49 ⟶ (x1 (x7 x50 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . (x10 x50 ⟶ False) ⟶ x16 x50 ⟶ (x10 x49 ⟶ False) ⟶ x16 x49 ⟶ x40 (x2 x50 x49) ⟶ False) ⟶ (∀ x49 x50 . (x40 x50 ⟶ False) ⟶ x16 x50 ⟶ (x40 x49 ⟶ False) ⟶ x16 x49 ⟶ x40 (x2 x50 x49) ⟶ False) ⟶ (∀ x49 x50 . (x40 x50 ⟶ False) ⟶ x16 x50 ⟶ (x10 x49 ⟶ False) ⟶ x16 x49 ⟶ x10 (x2 x49 x50) ⟶ False) ⟶ (∀ x49 x50 . (x40 x50 ⟶ False) ⟶ x16 x50 ⟶ (x10 x49 ⟶ False) ⟶ x16 x49 ⟶ x10 (x2 x50 x49) ⟶ False) ⟶ (∀ x49 x50 . (x40 x50 ⟶ False) ⟶ x16 x50 ⟶ (x40 x49 ⟶ False) ⟶ x16 x49 ⟶ x40 (x7 x50 x49) ⟶ False) ⟶ (∀ x49 x50 . (x10 x50 ⟶ False) ⟶ x16 x50 ⟶ (x10 x49 ⟶ False) ⟶ x16 x49 ⟶ x40 (x7 x50 x49) ⟶ False) ⟶ (∀ x49 x50 . (x10 x50 ⟶ False) ⟶ x16 x50 ⟶ (x40 x49 ⟶ False) ⟶ x16 x49 ⟶ x10 (x7 x49 x50) ⟶ False) ⟶ (∀ x49 x50 . (x10 x50 ⟶ False) ⟶ x16 x50 ⟶ (x40 x49 ⟶ False) ⟶ x16 x49 ⟶ x10 (x7 x50 x49) ⟶ False) ⟶ (∀ x49 x50 . x40 x50 ⟶ x16 x50 ⟶ (x40 x49 ⟶ False) ⟶ x16 x49 ⟶ (x10 (x5 x49 x50) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x40 x50 ⟶ x16 x50 ⟶ (x40 x49 ⟶ False) ⟶ x16 x49 ⟶ (x40 (x5 x50 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x10 x50 ⟶ x16 x50 ⟶ (x10 x49 ⟶ False) ⟶ x16 x49 ⟶ (x40 (x5 x49 x50) ⟶ False) ⟶ False) ⟶ ((x48 x47 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x10 x50 ⟶ x16 x50 ⟶ (x10 x49 ⟶ False) ⟶ x16 x49 ⟶ (x10 (x5 x50 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . (x40 x50 ⟶ False) ⟶ x16 x50 ⟶ (x10 x49 ⟶ False) ⟶ x16 x49 ⟶ x10 (x5 x49 x50) ⟶ False) ⟶ (∀ x49 x50 . (x40 x50 ⟶ False) ⟶ x16 x50 ⟶ (x10 x49 ⟶ False) ⟶ x16 x49 ⟶ x40 (x5 x50 x49) ⟶ False) ⟶ (∀ x49 . (x40 x49 ⟶ False) ⟶ x16 x49 ⟶ x10 (x44 x49) ⟶ False) ⟶ (∀ x49 . (x40 x49 ⟶ False) ⟶ x16 x49 ⟶ (x1 (x44 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 . (x10 x49 ⟶ False) ⟶ x16 x49 ⟶ x40 (x44 x49) ⟶ False) ⟶ (∀ x49 . (x10 x49 ⟶ False) ⟶ x16 x49 ⟶ (x1 (x44 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . (x48 x50 ⟶ False) ⟶ (x48 x49 ⟶ False) ⟶ x45 x49 (x46 x50) ⟶ (x41 (x25 x49 x50) x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . (x45 (x30 x49) x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 x51 . (x48 x51 ⟶ False) ⟶ (x48 x49 ⟶ False) ⟶ x45 x49 (x46 x51) ⟶ x41 x50 x51 x49 ⟶ (x45 x50 x51 ⟶ False) ⟶ False) ⟶ ((x41 x4 x43 x9 ⟶ False) ⟶ False) ⟶ ((x45 x9 (x46 x43) ⟶ False) ⟶ False) ⟶ (∀ x49 . x1 x49 ⟶ (x1 (x44 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x1 x50 ⟶ x1 x49 ⟶ (x7 x50 x49 = x7 x49 x50 ⟶ False) ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ (x29 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x14 x49 ⟶ (x10 x49 ⟶ False) ⟶ (x40 x49 ⟶ False) ⟶ (x14 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x14 x49 ⟶ (x10 x49 ⟶ False) ⟶ (x40 x49 ⟶ False) ⟶ (x48 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x45 x49 x8 ⟶ (x12 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ x14 x49 ⟶ x40 x49 ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ x14 x49 ⟶ x10 x49 ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ x14 x49 ⟶ (x14 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ (x12 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . (x48 x49 ⟶ False) ⟶ x14 x49 ⟶ (x10 x49 ⟶ False) ⟶ (x40 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . (x48 x49 ⟶ False) ⟶ x14 x49 ⟶ (x10 x49 ⟶ False) ⟶ (x14 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x12 x49 ⟶ (x19 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x14 x49 ⟶ x40 x49 ⟶ x10 x49 ⟶ False) ⟶ (∀ x49 . x14 x49 ⟶ x40 x49 ⟶ (x14 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x14 x49 ⟶ x40 x49 ⟶ x48 x49 ⟶ False) ⟶ (∀ x49 x50 . x19 x50 ⟶ x45 x49 x50 ⟶ (x19 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . (x48 x49 ⟶ False) ⟶ x14 x49 ⟶ (x40 x49 ⟶ False) ⟶ (x10 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . (x48 x49 ⟶ False) ⟶ x14 x49 ⟶ (x40 x49 ⟶ False) ⟶ (x14 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x16 x49 ⟶ (x14 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ (x28 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x14 x49 ⟶ x10 x49 ⟶ x40 x49 ⟶ False) ⟶ (∀ x49 . x14 x49 ⟶ x10 x49 ⟶ (x14 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x14 x49 ⟶ x10 x49 ⟶ x48 x49 ⟶ False) ⟶ (∀ x49 . x16 x49 ⟶ (x1 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ (x19 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x12 x49 ⟶ (x14 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x12 x49 ⟶ (x16 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x12 x49 ⟶ (x1 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x21 x49 ⟶ x33 x49 ⟶ (x19 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x45 x49 x43 ⟶ (x16 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x45 x49 x43 ⟶ (x1 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x19 x49 ⟶ (x33 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x19 x49 ⟶ (x21 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x29 x50 ⟶ x45 x49 (x46 x50) ⟶ (x29 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x0 x49 x50 ⟶ x0 x50 x49 ⟶ False) ⟶ (x27 = x44 x3 ⟶ False) ⟶ (x26 = x4 ⟶ False) ⟶ ((x2 x26 x27 = x44 x26 ⟶ False) ⟶ False) ⟶ ((x1 x27 ⟶ False) ⟶ False) ⟶ ((x1 x26 ⟶ False) ⟶ False) ⟶ False (proof)