Search for blocks/addresses/...

Proofgold Asset

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