| vout |
|---|
PrPhD../f6ed0.. 102.58 barsTMdfa../d14d8.. ownership of c1dc4.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0TMc3S../019c6.. ownership of 71dfa.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0PUVcx../a6960.. doc published by PrPhD..Definition FalseFalse := ∀ x0 : ο . x0Definition notnot := λ x0 : ο . x0 ⟶ FalseTheorem c1dc4.. : ∀ 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 : ι → ο . ∀ x58 . ∀ x59 : ι → ο . ∀ x60 . ∀ x61 : ι → ο . ∀ x62 . ∀ x63 : ι → ο . ∀ x64 : ι → ι . ∀ x65 : ι → ο . ∀ x66 x67 : ι → ι → ι . ∀ x68 : ι → ι → ι → ο . ∀ x69 . ∀ x70 : ι → ι → ι . ∀ x71 : ι → ι . ∀ x72 : ι → ι → ι . ∀ x73 : ι → ι → ι → ι . ∀ x74 : ι → ι . ∀ x75 . ∀ x76 : ι → ο . (∀ x77 x78 . x76 x78 ⟶ (x78 = x77 ⟶ False) ⟶ x76 x77 ⟶ False) ⟶ (∀ x77 x78 . x0 x77 x78 ⟶ x76 x78 ⟶ False) ⟶ (∀ x77 . x76 x77 ⟶ (x77 = x75 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 . (x1 x80 ⟶ False) ⟶ (x15 x80 ⟶ False) ⟶ x2 x80 ⟶ x14 x80 ⟶ x3 x80 ⟶ x13 x80 ⟶ x4 x80 ⟶ x12 x80 ⟶ (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x2 x79 ⟶ x14 x79 ⟶ x3 x79 ⟶ x13 x79 ⟶ x4 x79 ⟶ x12 x79 ⟶ x5 x78 x80 x79 ⟶ x10 x77 (x11 x80) ⟶ (x9 (x7 x80) (x7 x79) x78 (x8 x80 x77) = x8 x79 (x9 (x11 x80) (x11 x79) (x6 x80 x79 x78) x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x0 x77 x78 ⟶ x10 x78 (x74 x79) ⟶ x76 x79 ⟶ False) ⟶ (∀ x77 x78 x79 . x0 x78 x79 ⟶ x10 x79 (x74 x77) ⟶ (x10 x78 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 . (x1 x80 ⟶ False) ⟶ (x15 x80 ⟶ False) ⟶ x2 x80 ⟶ x14 x80 ⟶ x3 x80 ⟶ x13 x80 ⟶ x4 x80 ⟶ x12 x80 ⟶ (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x2 x79 ⟶ x14 x79 ⟶ x3 x79 ⟶ x13 x79 ⟶ x4 x79 ⟶ x12 x79 ⟶ x5 x78 x80 x79 ⟶ x10 x77 (x11 (x71 x80)) ⟶ (x9 (x11 (x71 x80)) (x11 x79) (x6 (x71 x80) x79 (x73 x80 x79 x78)) x77 = x9 (x11 x80) (x11 x79) (x6 x80 x79 x78) (x72 x80 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x16 x78 x77 ⟶ (x10 x78 (x74 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x10 x78 (x74 x77) ⟶ (x16 x78 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x10 x77 x78 ⟶ (x76 x78 ⟶ False) ⟶ (x0 x77 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x10 x77 (x11 (x71 x78)) ⟶ (x70 x78 (x8 (x71 x78) x77) = x8 x78 (x72 x78 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x0 x78 x77 ⟶ (x10 x78 x77 ⟶ False) ⟶ False) ⟶ (x76 x69 ⟶ False) ⟶ (∀ x77 . (x16 x77 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 . (x76 x80 ⟶ False) ⟶ x65 x77 ⟶ x68 x77 x80 x79 ⟶ x10 x77 (x74 (x67 x80 x79)) ⟶ x10 x78 x80 ⟶ (x9 x80 x79 x77 x78 = x66 x77 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 . (x76 x80 ⟶ False) ⟶ (x76 x77 ⟶ False) ⟶ (x76 x79 ⟶ False) ⟶ x65 x78 ⟶ x10 x78 (x74 (x67 (x67 x80 x77) x79)) ⟶ (x17 x80 x77 x79 x78 = x18 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ x63 x77 ⟶ x76 (x64 x77) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ x63 x77 ⟶ (x10 (x64 x77) (x74 (x11 x77)) ⟶ False) ⟶ False) ⟶ ((x4 x62 ⟶ False) ⟶ False) ⟶ ((x13 x62 ⟶ False) ⟶ False) ⟶ ((x3 x62 ⟶ False) ⟶ False) ⟶ ((x14 x62 ⟶ False) ⟶ False) ⟶ ((x2 x62 ⟶ False) ⟶ False) ⟶ ((x19 x62 ⟶ False) ⟶ False) ⟶ ((x61 x62 ⟶ False) ⟶ False) ⟶ (x15 x62 ⟶ False) ⟶ (x1 x62 ⟶ False) ⟶ ((x12 x62 ⟶ False) ⟶ False) ⟶ (x76 x60 ⟶ False) ⟶ (x15 x20 ⟶ False) ⟶ (x1 x20 ⟶ False) ⟶ ((x12 x20 ⟶ False) ⟶ False) ⟶ (x59 x58 ⟶ False) ⟶ ((x21 x58 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x57 x77 ⟶ False) ⟶ x63 x77 ⟶ x56 (x55 x77) ⟶ False) ⟶ (∀ x77 . (x57 x77 ⟶ False) ⟶ x63 x77 ⟶ (x10 (x55 x77) (x74 (x11 x77)) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ x63 x77 ⟶ (x56 (x54 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ x63 x77 ⟶ x76 (x54 x77) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ x63 x77 ⟶ (x10 (x54 x77) (x74 (x11 x77)) ⟶ False) ⟶ False) ⟶ ((x76 x22 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x53 (x52 x77 x78) x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x23 (x52 x78 x77) x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x51 (x52 x77 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x76 (x52 x77 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x10 (x52 x77 x78) (x74 (x67 x78 x77)) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x68 (x24 x77 x78) x78 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x65 (x24 x77 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x53 (x24 x77 x78) x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x23 (x24 x78 x77) x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x51 (x24 x77 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x10 (x24 x77 x78) (x74 (x67 x78 x77)) ⟶ False) ⟶ False) ⟶ ((x19 x25 ⟶ False) ⟶ False) ⟶ ((x12 x25 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 x81 x82 x83 x84 x85 x86 . x65 x86 ⟶ x68 x86 x77 x78 ⟶ x10 x86 (x74 (x67 x77 x78)) ⟶ x65 x79 ⟶ x68 x79 x77 x78 ⟶ x10 x79 (x74 (x67 x77 x78)) ⟶ x65 x85 ⟶ x10 x85 (x74 (x67 (x67 x77 x77) x77)) ⟶ x26 x78 x77 x86 x79 x85 = x26 x83 x80 x82 x81 x84 ⟶ (x85 = x84 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 x81 x82 x83 x84 x85 x86 . x65 x86 ⟶ x68 x86 x77 x78 ⟶ x10 x86 (x74 (x67 x77 x78)) ⟶ x65 x79 ⟶ x68 x79 x77 x78 ⟶ x10 x79 (x74 (x67 x77 x78)) ⟶ x65 x85 ⟶ x10 x85 (x74 (x67 (x67 x77 x77) x77)) ⟶ x26 x78 x77 x86 x79 x85 = x26 x83 x80 x82 x84 x81 ⟶ (x79 = x84 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 x81 x82 x83 x84 x85 x86 . x65 x86 ⟶ x68 x86 x77 x78 ⟶ x10 x86 (x74 (x67 x77 x78)) ⟶ x65 x79 ⟶ x68 x79 x77 x78 ⟶ x10 x79 (x74 (x67 x77 x78)) ⟶ x65 x85 ⟶ x10 x85 (x74 (x67 (x67 x77 x77) x77)) ⟶ x26 x78 x77 x86 x79 x85 = x26 x83 x80 x84 x82 x81 ⟶ (x86 = x84 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 x81 x82 x83 x84 x85 x86 . x65 x86 ⟶ x68 x86 x77 x78 ⟶ x10 x86 (x74 (x67 x77 x78)) ⟶ x65 x79 ⟶ x68 x79 x77 x78 ⟶ x10 x79 (x74 (x67 x77 x78)) ⟶ x65 x85 ⟶ x10 x85 (x74 (x67 (x67 x77 x77) x77)) ⟶ x26 x78 x77 x86 x79 x85 = x26 x83 x84 x82 x81 x80 ⟶ (x77 = x84 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 x81 x82 x83 x84 x85 x86 . x65 x86 ⟶ x68 x86 x77 x78 ⟶ x10 x86 (x74 (x67 x77 x78)) ⟶ x65 x79 ⟶ x68 x79 x77 x78 ⟶ x10 x79 (x74 (x67 x77 x78)) ⟶ x65 x85 ⟶ x10 x85 (x74 (x67 (x67 x77 x77) x77)) ⟶ x26 x78 x77 x86 x79 x85 = x26 x84 x80 x83 x82 x81 ⟶ (x78 = x84 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x50 x77 ⟶ False) ⟶ x63 x77 ⟶ x49 (x11 x77) ⟶ False) ⟶ (∀ x77 . x50 x77 ⟶ x63 x77 ⟶ (x49 (x11 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x57 x77 ⟶ x63 x77 ⟶ (x56 (x11 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x57 x77 ⟶ False) ⟶ x63 x77 ⟶ x56 (x11 x77) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ x63 x77 ⟶ x76 (x11 x77) ⟶ False) ⟶ (∀ x77 . (x59 x77 ⟶ False) ⟶ x21 x77 ⟶ x56 (x7 x77) ⟶ False) ⟶ (∀ x77 . x59 x77 ⟶ x21 x77 ⟶ (x56 (x7 x77) ⟶ False) ⟶ False) ⟶ ((x76 x75 ⟶ False) ⟶ False) ⟶ (∀ x77 . x1 x77 ⟶ x63 x77 ⟶ (x76 (x11 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ (x4 (x71 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ (x13 (x71 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ (x3 (x71 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ (x14 (x71 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ (x2 (x71 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ (x19 (x71 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ x15 (x71 x77) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ x1 (x71 x77) ⟶ False) ⟶ (∀ x77 . (x15 x77 ⟶ False) ⟶ x21 x77 ⟶ x76 (x7 x77) ⟶ False) ⟶ (∀ x77 . x15 x77 ⟶ x21 x77 ⟶ (x76 (x7 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ (x5 (x27 x77 x78) x78 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x10 (x48 x77) x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x12 x79 ⟶ x10 x77 (x11 x79) ⟶ x10 x78 (x11 x79) ⟶ (x28 (x29 x78 x77 x79) x79 x77 x78 ⟶ False) ⟶ False) ⟶ ((x21 x47 ⟶ False) ⟶ False) ⟶ ((x63 x30 ⟶ False) ⟶ False) ⟶ ((x46 x45 ⟶ False) ⟶ False) ⟶ ((x12 x31 ⟶ False) ⟶ False) ⟶ (∀ x77 . x46 x77 ⟶ (x10 (x44 x77) (x74 (x67 (x7 x77) (x11 x77))) ⟶ False) ⟶ False) ⟶ (∀ x77 . x46 x77 ⟶ (x68 (x44 x77) (x7 x77) (x11 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x46 x77 ⟶ (x65 (x44 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x46 x77 ⟶ (x10 (x32 x77) (x74 (x67 (x7 x77) (x11 x77))) ⟶ False) ⟶ False) ⟶ (∀ x77 . x46 x77 ⟶ (x68 (x32 x77) (x7 x77) (x11 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x46 x77 ⟶ (x65 (x32 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x10 (x43 x77) (x74 (x67 (x67 (x7 x77) (x7 x77)) (x7 x77))) ⟶ False) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x65 (x43 x77) ⟶ False) ⟶ False) ⟶ ((x76 x42 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x2 x79 ⟶ x14 x79 ⟶ x3 x79 ⟶ x13 x79 ⟶ x4 x79 ⟶ x12 x79 ⟶ (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x5 x77 x79 x78 ⟶ (x10 x77 (x74 (x67 (x7 x79) (x7 x78))) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x2 x79 ⟶ x14 x79 ⟶ x3 x79 ⟶ x13 x79 ⟶ x4 x79 ⟶ x12 x79 ⟶ (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x5 x77 x79 x78 ⟶ (x68 x77 (x7 x79) (x7 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x2 x79 ⟶ x14 x79 ⟶ x3 x79 ⟶ x13 x79 ⟶ x4 x79 ⟶ x12 x79 ⟶ (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x5 x77 x79 x78 ⟶ (x65 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 . (x1 x80 ⟶ False) ⟶ (x15 x80 ⟶ False) ⟶ x12 x80 ⟶ x10 x77 (x11 x80) ⟶ x10 x79 (x11 x80) ⟶ x28 x78 x80 x77 x79 ⟶ (x10 x78 (x7 x80) ⟶ False) ⟶ False) ⟶ (∀ x77 . x21 x77 ⟶ (x63 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x46 x77 ⟶ (x21 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x46 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x2 x79 ⟶ x14 x79 ⟶ x3 x79 ⟶ x13 x79 ⟶ x4 x79 ⟶ x12 x79 ⟶ (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x65 x77 ⟶ x68 x77 (x7 x79) (x7 x78) ⟶ x10 x77 (x74 (x67 (x7 x79) (x7 x78))) ⟶ (x10 (x6 x79 x78 x77) (x74 (x67 (x11 x79) (x11 x78))) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x2 x79 ⟶ x14 x79 ⟶ x3 x79 ⟶ x13 x79 ⟶ x4 x79 ⟶ x12 x79 ⟶ (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x65 x77 ⟶ x68 x77 (x7 x79) (x7 x78) ⟶ x10 x77 (x74 (x67 (x7 x79) (x7 x78))) ⟶ (x68 (x6 x79 x78 x77) (x11 x79) (x11 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x2 x79 ⟶ x14 x79 ⟶ x3 x79 ⟶ x13 x79 ⟶ x4 x79 ⟶ x12 x79 ⟶ (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x65 x77 ⟶ x68 x77 (x7 x79) (x7 x78) ⟶ x10 x77 (x74 (x67 (x7 x79) (x7 x78))) ⟶ (x65 (x6 x79 x78 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x10 x77 (x7 (x71 x78)) ⟶ (x10 (x70 x78 x77) (x7 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x10 x77 (x7 x78) ⟶ (x10 (x41 x78 x77) (x7 (x71 x78)) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x10 x77 (x11 (x71 x78)) ⟶ (x10 (x72 x78 x77) (x11 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x10 x77 (x11 x78) ⟶ (x28 (x8 x78 x77) x78 x77 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x10 x77 (x11 x78) ⟶ (x10 (x33 x78 x77) (x11 (x71 x78)) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 . (x76 x80 ⟶ False) ⟶ x65 x77 ⟶ x68 x77 x80 x79 ⟶ x10 x77 (x74 (x67 x80 x79)) ⟶ x10 x78 x80 ⟶ (x10 (x9 x80 x79 x77 x78) x79 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ (x12 (x71 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ (x19 (x71 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ x15 (x71 x77) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ x1 (x71 x77) ⟶ False) ⟶ (∀ x77 . x51 x77 ⟶ x65 x77 ⟶ (x65 (x18 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x51 x77 ⟶ x65 x77 ⟶ (x51 (x18 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 . (x76 x80 ⟶ False) ⟶ (x76 x77 ⟶ False) ⟶ (x76 x79 ⟶ False) ⟶ x65 x78 ⟶ x10 x78 (x74 (x67 (x67 x80 x77) x79)) ⟶ (x10 (x17 x80 x77 x79 x78) (x74 (x67 (x67 x77 x80) x79)) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 . (x76 x80 ⟶ False) ⟶ (x76 x77 ⟶ False) ⟶ (x76 x79 ⟶ False) ⟶ x65 x78 ⟶ x10 x78 (x74 (x67 (x67 x80 x77) x79)) ⟶ (x65 (x17 x80 x77 x79 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x2 x79 ⟶ x14 x79 ⟶ x3 x79 ⟶ x13 x79 ⟶ x4 x79 ⟶ x12 x79 ⟶ (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x65 x77 ⟶ x68 x77 (x7 x79) (x7 x78) ⟶ x10 x77 (x74 (x67 (x7 x79) (x7 x78))) ⟶ (x10 (x73 x79 x78 x77) (x74 (x67 (x7 (x71 x79)) (x7 x78))) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x2 x79 ⟶ x14 x79 ⟶ x3 x79 ⟶ x13 x79 ⟶ x4 x79 ⟶ x12 x79 ⟶ (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x65 x77 ⟶ x68 x77 (x7 x79) (x7 x78) ⟶ x10 x77 (x74 (x67 (x7 x79) (x7 x78))) ⟶ (x68 (x73 x79 x78 x77) (x7 (x71 x79)) (x7 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x2 x79 ⟶ x14 x79 ⟶ x3 x79 ⟶ x13 x79 ⟶ x4 x79 ⟶ x12 x79 ⟶ (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x65 x77 ⟶ x68 x77 (x7 x79) (x7 x78) ⟶ x10 x77 (x74 (x67 (x7 x79) (x7 x78))) ⟶ (x65 (x73 x79 x78 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 x81 . x65 x81 ⟶ x68 x81 x77 x78 ⟶ x10 x81 (x74 (x67 x77 x78)) ⟶ x65 x79 ⟶ x68 x79 x77 x78 ⟶ x10 x79 (x74 (x67 x77 x78)) ⟶ x65 x80 ⟶ x10 x80 (x74 (x67 (x67 x77 x77) x77)) ⟶ (x12 (x26 x78 x77 x81 x79 x80) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 x81 . x65 x81 ⟶ x68 x81 x77 x78 ⟶ x10 x81 (x74 (x67 x77 x78)) ⟶ x65 x79 ⟶ x68 x79 x77 x78 ⟶ x10 x79 (x74 (x67 x77 x78)) ⟶ x65 x80 ⟶ x10 x80 (x74 (x67 (x67 x77 x77) x77)) ⟶ (x19 (x26 x78 x77 x81 x79 x80) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x10 x77 (x7 (x71 x78)) ⟶ (x70 x78 x77 = x41 (x71 x78) x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x10 x77 (x7 x78) ⟶ (x41 x78 x77 = x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x10 x77 (x11 (x71 x78)) ⟶ (x72 x78 x77 = x33 (x71 x78) x77 ⟶ False) ⟶ False) ⟶ ((x75 = x42 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x10 x77 (x11 x78) ⟶ (x33 x78 x77 = x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ (x71 x77 = x26 (x11 x77) (x7 x77) (x44 x77) (x32 x77) (x17 (x7 x77) (x7 x77) (x7 x77) (x43 x77)) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 . (x1 x80 ⟶ False) ⟶ (x15 x80 ⟶ False) ⟶ x2 x80 ⟶ x14 x80 ⟶ x3 x80 ⟶ x13 x80 ⟶ x4 x80 ⟶ x12 x80 ⟶ (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x2 x79 ⟶ x14 x79 ⟶ x3 x79 ⟶ x13 x79 ⟶ x4 x79 ⟶ x12 x79 ⟶ x65 x78 ⟶ x68 x78 (x7 x80) (x7 x79) ⟶ x10 x78 (x74 (x67 (x7 x80) (x7 x79))) ⟶ x65 x77 ⟶ x68 x77 (x7 (x71 x80)) (x7 x79) ⟶ x10 x77 (x74 (x67 (x7 (x71 x80)) (x7 x79))) ⟶ x9 (x7 (x71 x80)) (x7 x79) x77 (x40 x77 x78 x79 x80) = x9 (x7 x80) (x7 x79) x78 (x70 x80 (x40 x77 x78 x79 x80)) ⟶ (x77 = x73 x80 x79 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 . (x1 x80 ⟶ False) ⟶ (x15 x80 ⟶ False) ⟶ x2 x80 ⟶ x14 x80 ⟶ x3 x80 ⟶ x13 x80 ⟶ x4 x80 ⟶ x12 x80 ⟶ (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x2 x79 ⟶ x14 x79 ⟶ x3 x79 ⟶ x13 x79 ⟶ x4 x79 ⟶ x12 x79 ⟶ x65 x78 ⟶ x68 x78 (x7 x80) (x7 x79) ⟶ x10 x78 (x74 (x67 (x7 x80) (x7 x79))) ⟶ x65 x77 ⟶ x68 x77 (x7 (x71 x80)) (x7 x79) ⟶ x10 x77 (x74 (x67 (x7 (x71 x80)) (x7 x79))) ⟶ (x10 (x40 x77 x78 x79 x80) (x7 (x71 x80)) ⟶ False) ⟶ (x77 = x73 x80 x79 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 x81 . (x1 x81 ⟶ False) ⟶ (x15 x81 ⟶ False) ⟶ x2 x81 ⟶ x14 x81 ⟶ x3 x81 ⟶ x13 x81 ⟶ x4 x81 ⟶ x12 x81 ⟶ (x1 x80 ⟶ False) ⟶ (x15 x80 ⟶ False) ⟶ x2 x80 ⟶ x14 x80 ⟶ x3 x80 ⟶ x13 x80 ⟶ x4 x80 ⟶ x12 x80 ⟶ x65 x79 ⟶ x68 x79 (x7 x81) (x7 x80) ⟶ x10 x79 (x74 (x67 (x7 x81) (x7 x80))) ⟶ x65 x77 ⟶ x68 x77 (x7 (x71 x81)) (x7 x80) ⟶ x10 x77 (x74 (x67 (x7 (x71 x81)) (x7 x80))) ⟶ x77 = x73 x81 x80 x79 ⟶ x10 x78 (x7 (x71 x81)) ⟶ (x9 (x7 (x71 x81)) (x7 x80) x77 x78 = x9 (x7 x81) (x7 x80) x79 (x70 x81 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 . x63 x77 ⟶ x34 x77 x75 ⟶ (x1 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x63 x77 ⟶ x1 x77 ⟶ (x34 x77 x75 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x76 x79 ⟶ False) ⟶ (x76 x77 ⟶ False) ⟶ x10 x78 (x74 (x67 x79 x77)) ⟶ x65 x78 ⟶ x68 x78 x79 x77 ⟶ (x68 x78 x79 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x76 x79 ⟶ False) ⟶ (x76 x77 ⟶ False) ⟶ x10 x78 (x74 (x67 x79 x77)) ⟶ x65 x78 ⟶ x68 x78 x79 x77 ⟶ x76 x78 ⟶ False) ⟶ (∀ x77 x78 x79 . (x76 x79 ⟶ False) ⟶ (x76 x77 ⟶ False) ⟶ x10 x78 (x74 (x67 x79 x77)) ⟶ x65 x78 ⟶ x68 x78 x79 x77 ⟶ (x65 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 . x63 x77 ⟶ (x50 x77 ⟶ False) ⟶ x57 x77 ⟶ False) ⟶ (∀ x77 . x63 x77 ⟶ x57 x77 ⟶ (x50 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x63 x77 ⟶ (x50 x77 ⟶ False) ⟶ x50 x77 ⟶ False) ⟶ (∀ x77 . x63 x77 ⟶ (x50 x77 ⟶ False) ⟶ x1 x77 ⟶ False) ⟶ (∀ x77 . x63 x77 ⟶ x1 x77 ⟶ (x50 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x63 x77 ⟶ x1 x77 ⟶ (x1 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x76 x79 ⟶ x10 x77 (x74 (x67 x78 x79)) ⟶ (x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x10 x78 (x74 (x67 x77 x77)) ⟶ x68 x78 x77 x77 ⟶ (x35 x78 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x76 x79 ⟶ x10 x77 (x74 (x67 x79 x78)) ⟶ (x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x76 x79 ⟶ False) ⟶ x10 x77 (x74 (x67 x78 x79)) ⟶ x68 x77 x78 x79 ⟶ (x35 x77 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 . x63 x77 ⟶ (x57 x77 ⟶ False) ⟶ x1 x77 ⟶ False) ⟶ (∀ x77 x78 x79 . x10 x79 (x74 (x67 x77 x78)) ⟶ (x53 x79 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x10 x79 (x74 (x67 x78 x77)) ⟶ (x23 x79 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x76 x79 ⟶ x10 x77 (x74 (x67 x79 x78)) ⟶ x68 x77 x79 x78 ⟶ (x35 x77 x79 ⟶ False) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x59 x77 ⟶ (x4 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x59 x77 ⟶ (x3 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x59 x77 ⟶ x15 x77 ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x59 x77 ⟶ x1 x77 ⟶ False) ⟶ (∀ x77 . x63 x77 ⟶ x1 x77 ⟶ (x57 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x10 x79 (x74 (x67 x77 x78)) ⟶ (x51 x79 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x10 x78 (x74 (x67 x79 x77)) ⟶ x35 x78 x79 ⟶ (x68 x78 x79 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x1 x77 ⟶ False) ⟶ x57 x77 ⟶ (x15 x77 ⟶ False) ⟶ (x13 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x1 x77 ⟶ False) ⟶ x57 x77 ⟶ (x15 x77 ⟶ False) ⟶ (x14 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x1 x77 ⟶ False) ⟶ x57 x77 ⟶ (x15 x77 ⟶ False) ⟶ x15 x77 ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x1 x77 ⟶ False) ⟶ x57 x77 ⟶ (x15 x77 ⟶ False) ⟶ x1 x77 ⟶ False) ⟶ (∀ x77 . x63 x77 ⟶ (x57 x77 ⟶ False) ⟶ x1 x77 ⟶ False) ⟶ (∀ x77 . x21 x77 ⟶ x15 x77 ⟶ (x59 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x21 x77 ⟶ (x15 x77 ⟶ False) ⟶ x61 x77 ⟶ x1 x77 ⟶ False) ⟶ (∀ x77 . x21 x77 ⟶ x1 x77 ⟶ x61 x77 ⟶ (x15 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x21 x77 ⟶ x15 x77 ⟶ (x61 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x21 x77 ⟶ (x1 x77 ⟶ False) ⟶ (x61 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x63 x77 ⟶ x34 x77 x69 ⟶ (x57 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x63 x77 ⟶ x34 x77 x69 ⟶ x1 x77 ⟶ False) ⟶ (∀ x77 . x63 x77 ⟶ (x1 x77 ⟶ False) ⟶ x57 x77 ⟶ (x34 x77 x69 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x0 x77 x78 ⟶ x0 x78 x77 ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ x19 x77 ⟶ (x77 = x26 ( |
|