| vout |
|---|
PrS5Z../e0f74.. 24.98 barsTMcrh../3794e.. ownership of e92bb.. as prop with payaddr PrDsC.. rights free controlledby PrDsC.. upto 0TMPUV../361c6.. ownership of 40683.. as prop with payaddr PrDsC.. rights free controlledby PrDsC.. upto 0PUeHT../11e98.. doc published by PrDsC..Definition FalseFalse := ∀ x0 : ο . x0Definition notnot := λ x0 : ο . x0 ⟶ FalseTheorem e92bb..t10_sin_cos8 : ∀ 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 : ι → ι . ∀ x55 : ι → ι → ι . ∀ x56 : ι → ι . ∀ x57 : ι → ι → ι . (x57 (x54 (x48 x52 x50)) (x55 (x56 x52) (x54 x50)) = x48 (x51 x52) (x49 x50) ⟶ x57 (x54 (x53 x52 x50)) (x55 (x56 x52) (x54 x50)) = x53 (x51 x52) (x49 x50) ⟶ False) ⟶ (∀ x58 x59 . (x57 (x53 (x49 x59) (x49 x58)) (x53 x1 (x55 (x49 x59) (x49 x58))) = x49 (x53 x59 x58) ⟶ False) ⟶ x0 x58 ⟶ x0 x59 ⟶ False) ⟶ (∀ x58 x59 . (x57 (x48 (x49 x59) (x49 x58)) (x48 x1 (x55 (x49 x59) (x49 x58))) = x49 (x48 x59 x58) ⟶ False) ⟶ x0 x58 ⟶ x0 x59 ⟶ False) ⟶ (∀ x58 x59 . (x53 (x55 (x56 x59) (x54 x58)) (x55 (x54 x59) (x56 x58)) = x56 (x53 x59 x58) ⟶ False) ⟶ x0 x58 ⟶ x0 x59 ⟶ False) ⟶ (∀ x58 x59 . (x48 (x55 (x56 x59) (x54 x58)) (x55 (x54 x59) (x56 x58)) = x56 (x48 x59 x58) ⟶ False) ⟶ x0 x58 ⟶ x0 x59 ⟶ False) ⟶ (∀ x58 x59 . (x53 (x55 (x54 x59) (x54 x58)) (x55 (x56 x59) (x56 x58)) = x54 (x53 x59 x58) ⟶ False) ⟶ x0 x58 ⟶ x0 x59 ⟶ False) ⟶ (∀ x58 x59 . (x48 (x55 (x54 x59) (x54 x58)) (x55 (x56 x59) (x56 x58)) = x54 (x48 x59 x58) ⟶ False) ⟶ x0 x58 ⟶ x0 x59 ⟶ False) ⟶ (∀ x58 x59 x60 . (x2 x60 ⟶ False) ⟶ (x2 x58 ⟶ False) ⟶ (x3 x59 x58 ⟶ False) ⟶ x5 x59 x58 x60 ⟶ x3 x60 (x4 x58) ⟶ False) ⟶ (∀ x58 x59 x60 . (x2 x60 ⟶ False) ⟶ (x2 x58 ⟶ False) ⟶ (x3 x59 x60 ⟶ False) ⟶ x5 x59 x58 x60 ⟶ x3 x60 (x4 x58) ⟶ False) ⟶ (∀ x58 x59 x60 . (x53 (x57 x58 x59) (x57 x60 x59) = x57 (x53 x58 x60) x59 ⟶ False) ⟶ x6 x60 ⟶ x6 x59 ⟶ x6 x58 ⟶ False) ⟶ (∀ x58 x59 x60 . (x48 (x57 x58 x59) (x57 x60 x59) = x57 (x48 x58 x60) x59 ⟶ False) ⟶ x6 x60 ⟶ x6 x59 ⟶ x6 x58 ⟶ False) ⟶ (∀ x58 x59 x60 . (x48 (x55 x58 x60) (x55 x59 x60) = x55 (x48 x58 x59) x60 ⟶ False) ⟶ x6 x60 ⟶ x6 x59 ⟶ x6 x58 ⟶ False) ⟶ (∀ x58 x59 . (x2 x59 ⟶ False) ⟶ (x2 x58 ⟶ False) ⟶ (x5 (x47 x58 x59) x58 x59 ⟶ False) ⟶ x3 x59 (x4 x58) ⟶ False) ⟶ (∀ x58 x59 x60 . (x2 x60 ⟶ False) ⟶ (x2 x58 ⟶ False) ⟶ (x5 x59 x60 x58 ⟶ False) ⟶ x3 x59 x58 ⟶ x3 x58 (x4 x60) ⟶ False) ⟶ (∀ x58 x59 x60 . (x60 = x46 ⟶ False) ⟶ (x57 (x55 x59 x60) (x55 x58 x60) = x57 x59 x58 ⟶ False) ⟶ x6 x58 ⟶ x6 x59 ⟶ x6 x60 ⟶ False) ⟶ (∀ x58 x59 x60 . (x55 (x55 x58 x59) x60 = x55 x58 (x55 x59 x60) ⟶ False) ⟶ x6 x60 ⟶ x6 x59 ⟶ x6 x58 ⟶ False) ⟶ (∀ x58 x59 x60 . (x48 (x48 x58 x59) x60 = x48 x58 (x48 x59 x60) ⟶ False) ⟶ x6 x60 ⟶ x6 x59 ⟶ x6 x58 ⟶ False) ⟶ (∀ x58 x59 x60 . (x57 (x55 x58 x59) x60 = x55 x58 (x57 x59 x60) ⟶ False) ⟶ x6 x60 ⟶ x6 x59 ⟶ x6 x58 ⟶ False) ⟶ (∀ x58 x59 . (x45 x59 ⟶ False) ⟶ (x45 x58 ⟶ False) ⟶ x0 x59 ⟶ x0 x58 ⟶ x45 (x48 x58 x59) ⟶ False) ⟶ (∀ x58 x59 . (x45 x59 ⟶ False) ⟶ (x45 x58 ⟶ False) ⟶ x0 x59 ⟶ x0 x58 ⟶ x7 (x57 x58 x59) ⟶ False) ⟶ (∀ x58 x59 . (x45 x59 ⟶ False) ⟶ (x45 x58 ⟶ False) ⟶ x0 x59 ⟶ x0 x58 ⟶ x7 (x55 x58 x59) ⟶ False) ⟶ (∀ x58 x59 . (x7 x59 ⟶ False) ⟶ (x45 x58 ⟶ False) ⟶ x0 x58 ⟶ x0 x59 ⟶ x45 (x53 x58 x59) ⟶ False) ⟶ (∀ x58 x59 . (x7 x59 ⟶ False) ⟶ (x45 x58 ⟶ False) ⟶ x0 x58 ⟶ x0 x59 ⟶ x45 (x57 x59 x58) ⟶ False) ⟶ (∀ x58 x59 . (x7 x59 ⟶ False) ⟶ (x45 x58 ⟶ False) ⟶ x0 x58 ⟶ x0 x59 ⟶ x45 (x57 x58 x59) ⟶ False) ⟶ (∀ x58 x59 . (x7 x59 ⟶ False) ⟶ (x45 x58 ⟶ False) ⟶ x0 x58 ⟶ x0 x59 ⟶ x7 (x53 x59 x58) ⟶ False) ⟶ (∀ x58 x59 . (x7 x59 ⟶ False) ⟶ (x45 x58 ⟶ False) ⟶ x0 x59 ⟶ x0 x58 ⟶ x45 (x55 x58 x59) ⟶ False) ⟶ (∀ x58 x59 . (x7 x59 ⟶ False) ⟶ (x45 x58 ⟶ False) ⟶ x0 x59 ⟶ x0 x58 ⟶ x45 (x55 x59 x58) ⟶ False) ⟶ (∀ x58 x59 . (x7 x59 ⟶ False) ⟶ (x7 x58 ⟶ False) ⟶ x0 x59 ⟶ x0 x58 ⟶ x7 (x57 x58 x59) ⟶ False) ⟶ (∀ x58 x59 . (x7 x59 ⟶ False) ⟶ (x7 x58 ⟶ False) ⟶ x0 x59 ⟶ x0 x58 ⟶ x7 (x55 x58 x59) ⟶ False) ⟶ (∀ x58 x59 . (x7 x59 ⟶ False) ⟶ (x7 x58 ⟶ False) ⟶ x0 x59 ⟶ x0 x58 ⟶ x7 (x48 x58 x59) ⟶ False) ⟶ (∀ x58 x59 . (x48 (x44 x59) (x44 x58) = x44 (x48 x59 x58) ⟶ False) ⟶ x6 x58 ⟶ x6 x59 ⟶ False) ⟶ (∀ x58 x59 x60 . (x3 x59 x60 ⟶ False) ⟶ x8 x59 x58 ⟶ x3 x58 (x4 x60) ⟶ False) ⟶ (∀ x58 x59 . (x2 x59 ⟶ False) ⟶ x43 x59 ⟶ x43 x58 ⟶ x2 (x48 x58 x59) ⟶ False) ⟶ (∀ x58 x59 . (x2 x59 ⟶ False) ⟶ x43 x59 ⟶ x43 x58 ⟶ x2 (x48 x59 x58) ⟶ False) ⟶ (∀ x58 x59 . (x3 (x41 x59 x58) x42 ⟶ False) ⟶ x0 x58 ⟶ x3 x59 x42 ⟶ False) ⟶ (∀ x58 x59 x60 . x2 x60 ⟶ x8 x59 x58 ⟶ x3 x58 (x4 x60) ⟶ False) ⟶ (∀ x58 x59 . (x45 x59 ⟶ False) ⟶ (x45 (x53 x58 x59) ⟶ False) ⟶ x0 x59 ⟶ x0 x58 ⟶ x45 x58 ⟶ False) ⟶ (∀ x58 x59 . (x45 x59 ⟶ False) ⟶ (x7 (x53 x59 x58) ⟶ False) ⟶ x0 x59 ⟶ x0 x58 ⟶ x45 x58 ⟶ False) ⟶ (∀ x58 x59 . (x45 x59 ⟶ False) ⟶ (x7 (x48 x58 x59) ⟶ False) ⟶ x0 x59 ⟶ x0 x58 ⟶ x7 x58 ⟶ False) ⟶ (∀ x58 x59 . (x45 x59 ⟶ False) ⟶ (x7 (x48 x59 x58) ⟶ False) ⟶ x0 x59 ⟶ x0 x58 ⟶ x7 x58 ⟶ False) ⟶ (∀ x58 x59 . (x7 x59 ⟶ False) ⟶ (x45 (x53 x59 x58) ⟶ False) ⟶ x0 x59 ⟶ x0 x58 ⟶ x7 x58 ⟶ False) ⟶ (∀ x58 x59 . (x7 x59 ⟶ False) ⟶ (x45 (x48 x58 x59) ⟶ False) ⟶ x0 x59 ⟶ x0 x58 ⟶ x45 x58 ⟶ False) ⟶ (∀ x58 x59 . (x7 x59 ⟶ False) ⟶ (x45 (x48 x59 x58) ⟶ False) ⟶ x0 x59 ⟶ x0 x58 ⟶ x45 x58 ⟶ False) ⟶ (∀ x58 x59 . (x7 x59 ⟶ False) ⟶ (x7 (x53 x58 x59) ⟶ False) ⟶ x0 x59 ⟶ x0 x58 ⟶ x7 x58 ⟶ False) ⟶ (∀ x58 x59 . (x41 x59 x58 = x57 x59 x58 ⟶ False) ⟶ x0 x58 ⟶ x3 x59 x42 ⟶ False) ⟶ (∀ x58 x59 . (x53 (x44 x59) (x44 x58) = x53 x58 x59 ⟶ False) ⟶ x6 x58 ⟶ x6 x59 ⟶ False) ⟶ (∀ x58 x59 . (x2 x59 ⟶ False) ⟶ (x7 x59 ⟶ False) ⟶ (x45 x58 ⟶ False) ⟶ x0 x58 ⟶ x0 x59 ⟶ x40 x59 x58 ⟶ False) ⟶ (∀ x58 x59 . (x2 x59 ⟶ False) ⟶ (x7 x58 ⟶ False) ⟶ (x45 x59 ⟶ False) ⟶ x0 x59 ⟶ x0 x58 ⟶ x40 x58 x59 ⟶ False) ⟶ (∀ x58 x59 . (x45 x59 ⟶ False) ⟶ x0 x59 ⟶ x0 x58 ⟶ x45 x58 ⟶ x40 x58 x59 ⟶ False) ⟶ (∀ x58 x59 . (x45 x59 ⟶ False) ⟶ x0 x59 ⟶ x0 x58 ⟶ x45 x58 ⟶ x40 x58 x59 ⟶ False) ⟶ (∀ x58 x59 . (x7 x59 ⟶ False) ⟶ x0 x58 ⟶ x0 x59 ⟶ x7 x58 ⟶ x40 x59 x58 ⟶ False) ⟶ (∀ x58 x59 . (x7 x59 ⟶ False) ⟶ x0 x58 ⟶ x0 x59 ⟶ x7 x58 ⟶ x40 x59 x58 ⟶ False) ⟶ (∀ x58 x59 . (x48 x59 (x44 x58) = x53 x59 x58 ⟶ False) ⟶ x6 x58 ⟶ x6 x59 ⟶ False) ⟶ (∀ x58 x59 . (x9 x59 x58 ⟶ False) ⟶ x3 x59 (x4 x58) ⟶ False) ⟶ (∀ x58 x59 . x8 x58 x59 ⟶ x8 x59 x58 ⟶ False) ⟶ (∀ x58 x59 . (x43 (x55 x59 x58) ⟶ False) ⟶ x43 x58 ⟶ x43 x59 ⟶ False) ⟶ (∀ x58 x59 . (x43 (x48 x59 x58) ⟶ False) ⟶ x43 x58 ⟶ x43 x59 ⟶ False) ⟶ (∀ x58 x59 . (x0 (x53 x59 x58) ⟶ False) ⟶ x0 x58 ⟶ x0 x59 ⟶ False) ⟶ (∀ x58 x59 . (x0 (x57 x59 x58) ⟶ False) ⟶ x0 x58 ⟶ x0 x59 ⟶ False) ⟶ (∀ x58 x59 . (x0 (x55 x59 x58) ⟶ False) ⟶ x0 x58 ⟶ x0 x59 ⟶ False) ⟶ (∀ x58 x59 . (x0 (x48 x59 x58) ⟶ False) ⟶ x0 x58 ⟶ x0 x59 ⟶ False) ⟶ (∀ x58 x59 . (x10 x59 ⟶ False) ⟶ x10 x58 ⟶ x3 x59 (x4 x58) ⟶ False) ⟶ (∀ x58 x59 . (x39 x59 ⟶ False) ⟶ x39 x58 ⟶ x3 x59 (x4 x58) ⟶ False) ⟶ (∀ x58 x59 . (x11 x59 ⟶ False) ⟶ x11 x58 ⟶ x3 x59 (x4 x58) ⟶ False) ⟶ (∀ x58 x59 . (x38 x59 ⟶ False) ⟶ x38 x58 ⟶ x3 x59 (x4 x58) ⟶ False) ⟶ (∀ x58 x59 . (x12 x59 ⟶ False) ⟶ x12 x58 ⟶ x3 x59 (x4 x58) ⟶ False) ⟶ (∀ x58 x59 . (x37 x59 ⟶ False) ⟶ x37 x58 ⟶ x3 x59 (x4 x58) ⟶ False) ⟶ (∀ x58 x59 . (x40 x58 x59 ⟶ False) ⟶ (x40 x59 x58 ⟶ False) ⟶ x13 x58 ⟶ x13 x59 ⟶ False) ⟶ (∀ x58 x59 . (x3 x59 (x4 x58) ⟶ False) ⟶ x9 x59 x58 ⟶ False) ⟶ (∀ x58 x59 . (x55 x59 x58 = x55 x58 x59 ⟶ False) ⟶ x6 x58 ⟶ x6 x59 ⟶ False) ⟶ (∀ x58 x59 . (x48 x59 x58 = x48 x58 x59 ⟶ False) ⟶ x6 x58 ⟶ x6 x59 ⟶ False) ⟶ (∀ x58 x59 . (x2 x59 ⟶ False) ⟶ (x8 x58 x59 ⟶ False) ⟶ x3 x58 x59 ⟶ False) ⟶ (∀ x58 x59 . (x7 x59 ⟶ False) ⟶ (x45 x58 ⟶ False) ⟶ (x40 x58 x59 ⟶ False) ⟶ x0 x59 ⟶ x0 x58 ⟶ False) ⟶ (∀ x58 x59 . (x7 x59 ⟶ False) ⟶ (x45 x58 ⟶ False) ⟶ (x40 x58 x59 ⟶ False) ⟶ x0 x59 ⟶ x0 x58 ⟶ False) ⟶ (∀ x58 . (x57 (x56 x58) (x54 x58) = x49 x58 ⟶ False) ⟶ x0 x58 ⟶ False) ⟶ (∀ x58 . (x41 (x54 x58) (x56 x58) = x51 x58 ⟶ False) ⟶ x0 x58 ⟶ False) ⟶ (∀ x58 x59 . (x3 x59 x58 ⟶ False) ⟶ x8 x59 x58 ⟶ False) ⟶ (∀ x58 x59 . (x43 x59 ⟶ False) ⟶ x37 x58 ⟶ x3 x59 x58 ⟶ False) ⟶ (∀ x58 x59 . (x36 x59 ⟶ False) ⟶ x10 x58 ⟶ x3 x59 x58 ⟶ False) ⟶ (∀ x58 x59 . (x14 x59 ⟶ False) ⟶ x39 x58 ⟶ x3 x59 x58 ⟶ False) ⟶ (∀ x58 x59 . (x13 x59 ⟶ False) ⟶ x38 x58 ⟶ x3 x59 x58 ⟶ False) ⟶ (∀ x58 x59 . (x6 x59 ⟶ False) ⟶ x12 x58 ⟶ x3 x59 x58 ⟶ False) ⟶ (∀ x58 x59 . (x0 x59 ⟶ False) ⟶ x11 x58 ⟶ x3 x59 x58 ⟶ False) ⟶ (∀ x58 . (x11 x58 ⟶ False) ⟶ x3 x58 (x4 x42) ⟶ False) ⟶ (∀ x58 . (x37 x58 ⟶ False) ⟶ x3 x58 (x4 x35) ⟶ False) ⟶ (∀ x58 x59 . x2 x59 ⟶ x8 x58 x59 ⟶ False) ⟶ (∀ x58 x59 . (x40 x59 x59 ⟶ False) ⟶ x13 x58 ⟶ x13 x59 ⟶ False) ⟶ (∀ x58 . (x45 x58 ⟶ False) ⟶ x0 x58 ⟶ x7 (x44 x58) ⟶ False) ⟶ (∀ x58 . (x7 x58 ⟶ False) ⟶ x0 x58 ⟶ x45 (x44 x58) ⟶ False) ⟶ (∀ x58 . (x55 x58 (x44 x1) = x44 x58 ⟶ False) ⟶ x6 x58 ⟶ False) ⟶ (∀ x58 . x7 x58 ⟶ x3 x58 x35 ⟶ False) ⟶ (∀ x58 . (x3 (x51 x58) x42 ⟶ False) ⟶ x0 x58 ⟶ False) ⟶ (∀ x58 . (x40 x1 (x54 x58) ⟶ False) ⟶ x0 x58 ⟶ False) ⟶ (∀ x58 . (x37 x58 ⟶ False) ⟶ x3 x58 x35 ⟶ False) ⟶ (∀ x58 . (x0 x58 ⟶ False) ⟶ x3 x58 x42 ⟶ False) ⟶ (∀ x58 . (x45 x58 ⟶ False) ⟶ (x6 (x44 x58) ⟶ False) ⟶ x0 x58 ⟶ False) ⟶ (∀ x58 . (x7 x58 ⟶ False) ⟶ (x6 (x44 x58) ⟶ False) ⟶ x0 x58 ⟶ False) ⟶ (∀ x58 . x13 x58 ⟶ x7 x58 ⟶ x45 x58 ⟶ False) ⟶ (∀ x58 . x13 x58 ⟶ x7 x58 ⟶ x45 x58 ⟶ False) ⟶ (∀ x58 . x13 x58 ⟶ x2 x58 ⟶ x45 x58 ⟶ False) ⟶ (∀ x58 . x13 x58 ⟶ x2 x58 ⟶ x45 x58 ⟶ False) ⟶ (∀ x58 . x13 x58 ⟶ x2 x58 ⟶ x7 x58 ⟶ False) ⟶ (∀ x58 . x13 x58 ⟶ x2 x58 ⟶ x7 x58 ⟶ False) ⟶ (∀ x58 . (x2 x58 ⟶ False) ⟶ (x7 x58 ⟶ False) ⟶ (x45 x58 ⟶ False) ⟶ x13 x58 ⟶ False) ⟶ (∀ x58 . (x2 x58 ⟶ False) ⟶ (x7 x58 ⟶ False) ⟶ (x45 x58 ⟶ False) ⟶ x13 x58 ⟶ False) ⟶ (∀ x58 . (x2 x58 ⟶ False) ⟶ (x7 x58 ⟶ False) ⟶ (x45 x58 ⟶ False) ⟶ x13 x58 ⟶ False) ⟶ (∀ x58 . (x55 x1 x58 = x58 ⟶ False) ⟶ x6 x58 ⟶ False) ⟶ (∀ x58 . (x53 x58 x46 = x58 ⟶ False) ⟶ x6 x58 ⟶ False) ⟶ (∀ x58 . (x57 x58 x1 = x58 ⟶ False) ⟶ x6 x58 ⟶ False) ⟶ (∀ x58 . (x48 x58 x46 = x58 ⟶ False) ⟶ x6 x58 ⟶ False) ⟶ (∀ x58 . (x57 x46 x58 = x46 ⟶ False) ⟶ x6 x58 ⟶ False) ⟶ (∀ x58 . (x55 x58 x46 = x46 ⟶ False) ⟶ x6 x58 ⟶ False) ⟶ (∀ x58 . (x44 (x44 x58) = x58 ⟶ False) ⟶ x6 x58 ⟶ False) ⟶ (∀ x58 . (x6 (x44 x58) ⟶ False) ⟶ x6 x58 ⟶ False) ⟶ (∀ x58 . (x6 (x44 x58) ⟶ False) ⟶ x0 x58 ⟶ False) ⟶ (∀ x58 . (x0 (x44 x58) ⟶ False) ⟶ x0 x58 ⟶ False) ⟶ (∀ x58 x59 . (x59 = x58 ⟶ False) ⟶ x2 x58 ⟶ x2 x59 ⟶ False) ⟶ (∀ x58 . (x58 = x46 ⟶ False) ⟶ x56 x58 = x46 ⟶ x0 x58 ⟶ False) ⟶ (∀ x58 . (x58 = x46 ⟶ False) ⟶ x49 x58 = x46 ⟶ x0 x58 ⟶ False) ⟶ (∀ x58 . x43 x58 ⟶ x7 x58 ⟶ False) ⟶ (∀ x58 . (x34 x58 ⟶ False) ⟶ x2 x58 ⟶ False) ⟶ (∀ x58 . (x15 x58 ⟶ False) ⟶ x43 x58 ⟶ False) ⟶ (∀ x58 . (x10 x58 ⟶ False) ⟶ x37 x58 ⟶ False) ⟶ (∀ x58 . (x39 x58 ⟶ False) ⟶ x10 x58 ⟶ False) ⟶ (∀ x58 . (x11 x58 ⟶ False) ⟶ x39 x58 ⟶ False) ⟶ (∀ x58 . (x13 x58 ⟶ False) ⟶ x43 x58 ⟶ False) ⟶ (∀ x58 . (x13 x58 ⟶ False) ⟶ x0 x58 ⟶ False) ⟶ (∀ x58 . (x38 x58 ⟶ False) ⟶ x11 x58 ⟶ False) ⟶ (∀ x58 . (x6 x58 ⟶ False) ⟶ x0 x58 ⟶ False) ⟶ (∀ x58 . (x12 x58 ⟶ False) ⟶ x11 x58 ⟶ False) ⟶ (∀ x58 . (x37 x58 ⟶ False) ⟶ x2 x58 ⟶ False) ⟶ (∀ x58 . (x0 x58 ⟶ False) ⟶ x43 x58 ⟶ False) ⟶ (∀ x58 . (x56 x46 = x46 ⟶ False) ⟶ x0 x58 ⟶ False) ⟶ (∀ x58 . (x54 x46 = x1 ⟶ False) ⟶ x0 x58 ⟶ False) ⟶ (∀ x58 . (x49 x46 = x46 ⟶ False) ⟶ x0 x58 ⟶ False) ⟶ (∀ x58 . (x58 = x16 ⟶ False) ⟶ x2 x58 ⟶ False) ⟶ (x40 x33 (x44 x1) ⟶ False) ⟶ (x40 x1 (x44 x1) ⟶ False) ⟶ (x40 x1 x33 ⟶ False) ⟶ (x2 x17 ⟶ False) ⟶ (x2 x32 ⟶ False) ⟶ (x2 x18 ⟶ False) ⟶ (x2 x31 ⟶ False) ⟶ (x2 x19 ⟶ False) ⟶ (x2 x1 ⟶ False) ⟶ (x52 = x46 ⟶ False) ⟶ ((x5 x33 x42 x35 ⟶ False) ⟶ False) ⟶ ((x5 x1 x42 x35 ⟶ False) ⟶ False) ⟶ ((x5 x46 x42 x35 ⟶ False) ⟶ False) ⟶ ((x40 (x44 x1) (x44 x1) ⟶ False) ⟶ False) ⟶ ((x53 (x44 x1) (x44 x1) = x33 ⟶ False) ⟶ False) ⟶ (∀ x58 . (x3 (x20 x58) x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . (x3 (x56 x58) x42 ⟶ False) ⟶ False) ⟶ (∀ x58 . (x3 (x54 x58) x42 ⟶ False) ⟶ False) ⟶ (∀ x58 . (x3 (x49 x58) x42 ⟶ False) ⟶ False) ⟶ ((x53 (x44 x1) x33 = x44 x1 ⟶ False) ⟶ False) ⟶ ((x48 (x44 x1) x33 = x44 x1 ⟶ False) ⟶ False) ⟶ ((x57 x1 (x44 x1) = x44 x1 ⟶ False) ⟶ False) ⟶ ((x48 x33 (x44 x1) = x44 x1 ⟶ False) ⟶ False) ⟶ ((x40 (x44 x1) x33 ⟶ False) ⟶ False) ⟶ ((x40 (x44 x1) x1 ⟶ False) ⟶ False) ⟶ ((x3 x18 (x4 x42) ⟶ False) ⟶ False) ⟶ ((x3 x35 (x4 x42) ⟶ False) ⟶ False) ⟶ ((x48 (x44 x1) x1 = x33 ⟶ False) ⟶ False) ⟶ ((x53 x33 (x44 x1) = x1 ⟶ False) ⟶ False) ⟶ ((x48 x1 (x44 x1) = x33 ⟶ False) ⟶ False) ⟶ (∀ x58 . (x9 x58 x58 ⟶ False) ⟶ False) ⟶ ((x53 x33 x1 = x44 x1 ⟶ False) ⟶ False) ⟶ ((x40 x33 x33 ⟶ False) ⟶ False) ⟶ ((x40 x33 x1 ⟶ False) ⟶ False) ⟶ ((x40 x1 x1 ⟶ False) ⟶ False) ⟶ ((x3 x33 x42 ⟶ False) ⟶ False) ⟶ ((x3 x33 x35 ⟶ False) ⟶ False) ⟶ ((x3 x1 x42 ⟶ False) ⟶ False) ⟶ ((x3 x1 x35 ⟶ False) ⟶ False) ⟶ ((x3 x16 x21 ⟶ False) ⟶ False) ⟶ ((x53 x1 x33 = x1 ⟶ False) ⟶ False) ⟶ ((x53 x1 x1 = x33 ⟶ False) ⟶ False) ⟶ ((x57 x1 x1 = x1 ⟶ False) ⟶ False) ⟶ ((x55 x33 x33 = x33 ⟶ False) ⟶ False) ⟶ ((x55 x33 x1 = x33 ⟶ False) ⟶ False) ⟶ ((x55 x1 x33 = x33 ⟶ False) ⟶ False) ⟶ ((x55 x1 x1 = x1 ⟶ False) ⟶ False) ⟶ ((x48 x33 x33 = x33 ⟶ False) ⟶ False) ⟶ ((x48 x33 x1 = x1 ⟶ False) ⟶ False) ⟶ ((x48 x1 x33 = x1 ⟶ False) ⟶ False) ⟶ ((x44 (x44 x1) = x1 ⟶ False) ⟶ False) ⟶ ((x45 x22 ⟶ False) ⟶ False) ⟶ ((x45 x30 ⟶ False) ⟶ False) ⟶ ((x45 x1 ⟶ False) ⟶ False) ⟶ ((x7 x29 ⟶ False) ⟶ False) ⟶ ((x7 x23 ⟶ False) ⟶ False) ⟶ ((x34 x17 ⟶ False) ⟶ False) ⟶ ((x34 x21 ⟶ False) ⟶ False) ⟶ ((x34 x42 ⟶ False) ⟶ False) ⟶ ((x15 x18 ⟶ False) ⟶ False) ⟶ ((x2 x28 ⟶ False) ⟶ False) ⟶ ((x2 x24 ⟶ False) ⟶ False) ⟶ ((x2 x27 ⟶ False) ⟶ False) ⟶ ((x2 x33 ⟶ False) ⟶ False) ⟶ ((x2 x16 ⟶ False) ⟶ False) ⟶ ((x11 x42 ⟶ False) ⟶ False) ⟶ ((x13 x28 ⟶ False) ⟶ False) ⟶ ((x13 x24 ⟶ False) ⟶ False) ⟶ ((x13 x29 ⟶ False) ⟶ False) ⟶ ((x13 x23 ⟶ False) ⟶ False) ⟶ ((x13 x22 ⟶ False) ⟶ False) ⟶ ((x13 x30 ⟶ False) ⟶ False) ⟶ (( |
|