| ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ (∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ x1 x4 x5 ⟶ x1 x5 x4) ⟶ atleastp u10 x3 ⟶ 4402e.. x3 x1 ⟶ cf2df.. x3 x1 ⟶ ∀ x4 : ο . (a0244.. x0 x1 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ f1c88.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 97406.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 0d539.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 4b1cb.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 72942.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 47362.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ d8b5d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 55171.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 1465e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ ce338.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 6dee7.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ ea964.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ d1a27.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 60a50.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ c059e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ e9db0.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 77203.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 133c1.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ bc7ef.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 9e253.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 68ab4.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 81575.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 86385.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 7c588.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ b019a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 3d346.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 69895.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 1a764.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 51ac7.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ f78c3.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 39cca.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 34ea6.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 6caea.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ e5411.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 948b4.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 58295.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 4a04b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 68a6f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 5d868.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 8629d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ ea11f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 2005f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ de50b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 3369f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ f9d60.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ ff926.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 71397.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 2560b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 48a66.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 289d9.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 37c80.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 5a5ea.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ dd8d8.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ c6a41.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ c2a1e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 15aa1.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ ccc6b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 0446d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 7683c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 96c77.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 07f55.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 93e63.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ c222a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ c61bd.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 02f40.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ b1def.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ e68b8.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 5bc1a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 8befb.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 8fb7c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 9bc89.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 3d118.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 33b5a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ a2f4a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 79b37.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ d833d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 23d0b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ c1005.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 61f8f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ ab383.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 856bc.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 788a1.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 3906f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ c9658.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ b72b8.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ cf898.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ f5373.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 48106.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ d4ea7.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ c1146.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ ca8ce.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 3f609.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 3656c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 9eb9c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 33102.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 48a69.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ d9cea.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ a56d9.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 5f015.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 903bc.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 4a22a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 74e48.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 20d20.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 43c4e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ f8fdb.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 66dda.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 3429e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 28e6a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ d9823.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 1b9db.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ b6bd6.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 26830.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 03c1b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 0d1ce.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 11d3d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 53762.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 1ccbe.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 73f56.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ e5a83.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 7861e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 94275.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 2ad4c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ e5b49.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 6b6c2.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ a0b66.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 6d19b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 08d9f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 99903.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 8a782.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 47dfa.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 22755.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 3f29d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 518d7.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 99ac9.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 99fe6.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 2427f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ d09b6.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 2997a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 5904d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 3c675.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 79a0f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ a79f5.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ c3712.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ f0b8a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ ff600.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 87daf.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ b4530.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 66bd0.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 558af.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 52ac0.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 4c6fc.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 4a27c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ bde2c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 89b0b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ cc2aa.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ 34b68.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ ed7e5.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ x4) ⟶ x4 |
|