vout |
---|
Pr5q4../2d392.. 24.99 barsTMWmv../7b9e4.. ownership of b257d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMZ51../5c663.. ownership of 1239c.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0PUR5T../b81a6.. doc published by Pr4zB..Param 4402e.. : ι → (ι → ι → ο) → οParam cf2df.. : ι → (ι → ι → ο) → οDefinition SubqSubq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1Param setminussetminus : ι → ι → ιParam SingSing : ι → ιParam 2bb2a.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 68d0b.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam f4564.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 4ff4c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam b0a38.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam a60f8.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 78c9a.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 69a33.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam b5965.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam d7308.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 4c67f.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 94fe6.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 456a0.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 03a93.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 5dfb3.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 6410a.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 08130.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam e26ca.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 4e84e.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 33d88.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam a4b3d.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 507e8.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam e0533.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam f0c46.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 4e371.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam abccc.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam f4324.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam fe361.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam ae9a0.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam c6b73.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 1a172.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam fb24f.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 3c996.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 4679c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 26d71.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 2fe16.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam c331d.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 24ede.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 6f860.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam d2465.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 3b3a3.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam a7aba.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 90ffc.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 3759a.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 58ba6.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam e1ba3.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 5ffcf.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 6cb43.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam d0208.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 9e613.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 0fd6e.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam bdc72.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 91378.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 14af1.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam b8539.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 8198e.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 2365e.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 3a344.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 29a66.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 6935c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 2ed56.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam d5680.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam e8fec.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam d8325.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam e0b94.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam f63e8.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 251ab.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 732e2.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 576d3.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 1a8a9.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 9ab74.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 0f519.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 1dd74.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 5932b.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 53b49.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 50a7f.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam efbf0.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam c13a7.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 9002a.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 62379.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 2e38c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 0897f.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 306f8.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 9ed6a.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam fee51.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam bae07.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam cd4ee.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 22563.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam bdc7f.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam dfb78.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam f8ada.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam d3342.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 0f762.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 55451.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam f380c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 42e23.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 8bcec.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 1c6c9.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 754da.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam a4ce7.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 60a51.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam ea33e.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 9fce6.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 0aaf4.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam ce3b4.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 27e6e.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam a89de.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam f5fe1.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam fd185.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam b7bfe.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 86078.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam d29be.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 5cc7a.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 49015.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 9dea4.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam f0075.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 0a362.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 6b1e6.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam e9c43.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam a3d78.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 11982.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam fe4dd.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam b5215.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam f982a.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam f1135.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 5c669.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 8faa8.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 458ae.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 22989.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 83885.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam b7bbc.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 9f4c9.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam be274.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 14707.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 4f588.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 218e4.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 0e6a7.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 0809e.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 6f746.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 6e201.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 311f0.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam f9cba.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 3cb02.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 6d791.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam fa7d9.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam fc088.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam e974a.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 33f3e.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 87bb9.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam d0a24.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 3ad6c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 77953.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam fcbed.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam ff800.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam f98b7.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 6f07c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 60dbb.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam f1c88.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 97406.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 0d539.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 4b1cb.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 72942.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 47362.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam d8b5d.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 55171.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 1465e.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam ce338.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 6dee7.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam ea964.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam d1a27.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 60a50.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam c059e.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam e9db0.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 77203.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 133c1.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam bc7ef.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 9e253.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 68ab4.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 81575.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 86385.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 7c588.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam b019a.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 3d346.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 69895.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 1a764.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 51ac7.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam f78c3.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 39cca.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 34ea6.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 6caea.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam e5411.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 948b4.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 58295.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 4a04b.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 68a6f.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 5d868.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 8629d.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam ea11f.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 2005f.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam de50b.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 3369f.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam f9d60.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam ff926.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 71397.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 2560b.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 48a66.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 289d9.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 37c80.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 5a5ea.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam dd8d8.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam c6a41.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam c2a1e.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 15aa1.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam ccc6b.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 0446d.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 7683c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 96c77.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 07f55.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 93e63.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam c222a.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam c61bd.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 02f40.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam b1def.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam e68b8.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 5bc1a.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 8befb.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 8fb7c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 9bc89.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 3d118.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 33b5a.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam a2f4a.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 79b37.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam d833d.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 23d0b.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam c1005.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 61f8f.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam ab383.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 856bc.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 788a1.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 3906f.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam c9658.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam b72b8.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam cf898.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam f5373.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 48106.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam d4ea7.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam c1146.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam ca8ce.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 3f609.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 3656c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 9eb9c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 33102.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 48a69.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam d9cea.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam a56d9.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 5f015.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 903bc.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 4a22a.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 74e48.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 20d20.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 43c4e.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam f8fdb.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 66dda.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 3429e.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 28e6a.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam d9823.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 1b9db.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam b6bd6.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 26830.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 03c1b.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 0d1ce.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 11d3d.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 53762.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 1ccbe.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 73f56.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam e5a83.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 7861e.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 94275.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 2ad4c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam e5b49.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 6b6c2.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam a0b66.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 6d19b.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 08d9f.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 99903.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 8a782.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 47dfa.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 22755.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 3f29d.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 518d7.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 99ac9.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 99fe6.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 2427f.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam d09b6.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 2997a.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 5904d.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 3c675.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 79a0f.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam a79f5.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam c3712.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam f0b8a.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam ff600.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 87daf.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam b4530.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 66bd0.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 558af.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 52ac0.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 4c6fc.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 4a27c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam bde2c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 89b0b.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam cc2aa.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam 34b68.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam ed7e5.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οDefinition 5bab1.. := λ x0 . λ x1 : ι → ι → ο . ∀ x2 : ο . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 68d0b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ f4564.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 4ff4c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ b0a38.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ a60f8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 78c9a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 69a33.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ b5965.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ d7308.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 4c67f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 94fe6.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 456a0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 03a93.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 5dfb3.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 6410a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 08130.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ e26ca.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 4e84e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 33d88.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ a4b3d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 507e8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ e0533.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ f0c46.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 4e371.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ abccc.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ f4324.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ fe361.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ ae9a0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ c6b73.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 1a172.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ fb24f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 3c996.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 4679c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 26d71.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 2fe16.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ c331d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 24ede.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 6f860.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ d2465.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 3b3a3.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ a7aba.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 90ffc.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 3759a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 58ba6.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ e1ba3.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 5ffcf.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 6cb43.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ d0208.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 9e613.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 0fd6e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ bdc72.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 91378.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 14af1.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ b8539.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 8198e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 2365e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 3a344.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 29a66.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 6935c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 2ed56.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ d5680.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ e8fec.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ d8325.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ e0b94.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ f63e8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 251ab.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 732e2.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 576d3.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 1a8a9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 9ab74.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 0f519.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 1dd74.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 5932b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 53b49.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 50a7f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ efbf0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ c13a7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 9002a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 62379.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 2e38c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 0897f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 306f8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 9ed6a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ fee51.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ bae07.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ cd4ee.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 22563.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ bdc7f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ dfb78.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ f8ada.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ d3342.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 0f762.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 55451.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ f380c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 42e23.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 8bcec.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 1c6c9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 754da.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ a4ce7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 60a51.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ ea33e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 9fce6.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 0aaf4.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ ce3b4.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 27e6e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ a89de.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ f5fe1.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ fd185.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ b7bfe.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 86078.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ d29be.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 5cc7a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 49015.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 9dea4.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ f0075.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 0a362.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 6b1e6.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ e9c43.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ a3d78.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 11982.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ fe4dd.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ b5215.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ f982a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ f1135.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 5c669.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 8faa8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 458ae.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 22989.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 83885.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ b7bbc.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 9f4c9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ be274.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 14707.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 4f588.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 218e4.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 0e6a7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 0809e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 6f746.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 6e201.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 311f0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ f9cba.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 3cb02.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 6d791.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ fa7d9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ fc088.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ e974a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 33f3e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 87bb9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ d0a24.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 3ad6c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 77953.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ fcbed.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ ff800.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ f98b7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 6f07c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 60dbb.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ f1c88.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 97406.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 0d539.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 4b1cb.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 72942.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 47362.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ d8b5d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 55171.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 1465e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ ce338.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 6dee7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ ea964.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ d1a27.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 60a50.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ c059e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ e9db0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 77203.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 133c1.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ bc7ef.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 9e253.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 68ab4.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 81575.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 86385.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 7c588.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ b019a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 3d346.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 69895.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 1a764.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 51ac7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ f78c3.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 39cca.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 34ea6.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 6caea.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ e5411.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 948b4.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 58295.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 4a04b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 68a6f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 5d868.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 8629d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ ea11f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 2005f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ de50b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 3369f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ f9d60.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ ff926.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 71397.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 2560b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 48a66.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 289d9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 37c80.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 5a5ea.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ |
|