Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrCit../1d100..
PUXym../55a8b..
vout
PrCit../17445.. 2.65 bars
TMR65../2cf22.. ownership of c978c.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMLp5../55262.. ownership of 59db2.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
PUZCC../4eccb.. doc published by Pr4zB..
Param 4402e.. : ι(ιιο) → ο
Param cf2df.. : ι(ιιο) → ο
Param SubqSubq : ιιο
Param setminussetminus : ιιι
Param SingSing : ιι
Param atleastpatleastp : ιιο
Param u10 : ι
Param a0244.. : ι(ιιο) → ο
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.. : (ιιο) → ιιιιιιιιιιο
Known 87262.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)(∀ x4 . x4x3∀ x5 . x5x3x1 x4 x5x1 x5 x4)atleastp u10 x34402e.. x3 x1cf2df.. x3 x1∀ x4 : ο . (a0244.. x0 x1x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x362379.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x32e38c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x30897f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3306f8.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x39ed6a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3fee51.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3bae07.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3cd4ee.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x322563.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3bdc7f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3dfb78.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3f8ada.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3d3342.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x30f762.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x355451.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3f380c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x342e23.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x38bcec.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x31c6c9.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3754da.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3a4ce7.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x360a51.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3ea33e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x39fce6.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x30aaf4.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3ce3b4.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x327e6e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3a89de.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3f5fe1.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3fd185.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3b7bfe.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x386078.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3d29be.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x35cc7a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x349015.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x39dea4.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3f0075.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x30a362.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x36b1e6.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3e9c43.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3a3d78.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x311982.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3fe4dd.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3b5215.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3f982a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3f1135.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x35c669.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x38faa8.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3458ae.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x322989.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x383885.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3b7bbc.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x39f4c9.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3be274.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x314707.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x34f588.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3218e4.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x30e6a7.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x30809e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x36f746.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x36e201.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3311f0.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3f9cba.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x33cb02.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x36d791.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3fa7d9.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3fc088.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3e974a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x333f3e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x387bb9.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3d0a24.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x33ad6c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x377953.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3fcbed.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3ff800.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3f98b7.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x36f07c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x360dbb.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3f1c88.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x397406.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x30d539.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x34b1cb.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x372942.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x347362.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3d8b5d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x355171.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x31465e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3ce338.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x36dee7.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3ea964.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3d1a27.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x360a50.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3c059e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3e9db0.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x377203.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3133c1.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3bc7ef.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x39e253.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x368ab4.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x381575.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x386385.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x37c588.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3b019a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x33d346.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x369895.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x31a764.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x351ac7.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3f78c3.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x339cca.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x334ea6.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x36caea.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3e5411.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3948b4.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x358295.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x34a04b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x368a6f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x35d868.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x38629d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3ea11f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x32005f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3de50b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x33369f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3f9d60.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3ff926.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x371397.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x32560b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x348a66.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3289d9.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x337c80.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x35a5ea.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3dd8d8.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3c6a41.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3c2a1e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x315aa1.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3ccc6b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x30446d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x37683c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x396c77.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x307f55.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x393e63.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3c222a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3c61bd.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x302f40.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3b1def.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3e68b8.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x35bc1a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x38befb.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x38fb7c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x39bc89.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x33d118.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x333b5a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3a2f4a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x379b37.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3d833d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x323d0b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3c1005.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x361f8f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3ab383.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3856bc.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3788a1.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x33906f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3c9658.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3b72b8.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3cf898.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3f5373.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x348106.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3d4ea7.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3c1146.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3ca8ce.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x33f609.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x33656c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x39eb9c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x333102.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x348a69.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3d9cea.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3a56d9.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x35f015.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3903bc.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x34a22a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x374e48.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x320d20.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x343c4e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3f8fdb.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x366dda.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x33429e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x328e6a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3d9823.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x31b9db.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3b6bd6.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x326830.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x303c1b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x30d1ce.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x311d3d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x353762.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x31ccbe.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x373f56.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3e5a83.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x37861e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x394275.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x32ad4c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3e5b49.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x36b6c2.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3a0b66.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x36d19b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x308d9f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x399903.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x38a782.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x347dfa.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x322755.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x33f29d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3518d7.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x399ac9.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x399fe6.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x32427f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3d09b6.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x32997a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x35904d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x33c675.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x379a0f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3a79f5.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3c3712.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3f0b8a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3ff600.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x387daf.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3b4530.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x366bd0.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3558af.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x352ac0.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x34c6fc.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x34a27c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3bde2c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x389b0b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3cc2aa.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x334b68.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3ed7e5.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)x4
Known 673c9.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x362379.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 9cdab.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x32e38c.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known df4d3.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x00897f.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known 29284.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0306f8.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known 4ad92.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x09ed6a.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known a818b.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3fee51.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known dfc93.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3bae07.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 4f247.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3cd4ee.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 3ed61.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x022563.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known b387e.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0bdc7f.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known 7d551.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0dfb78.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known 2142a.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0f8ada.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known 038c0.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0d3342.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known a8e6f.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x00f762.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known 5241a.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x355451.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 23ded.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3f380c.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 06c3b.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x042e23.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known d37c2.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x08bcec.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known b83b1.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x31c6c9.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known d1330.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0754da.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known a358e.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0a4ce7.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known 4f598.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x060a51.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known 70225.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0ea33e.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known 07b06.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x09fce6.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known 30e73.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x00aaf4.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known 094a1.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3ce3b4.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 0f7bc.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x327e6e.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 17591.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3a89de.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 60913.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3f5fe1.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 95907.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3fd185.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 9cc6f.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3b7bfe.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 58c96.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x386078.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known f68e0.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3d29be.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known e007f.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x35cc7a.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 133a3.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x349015.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 72b3e.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x39dea4.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 483ac.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3f0075.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known d6e51.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x00a362.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known d05fa.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x06b1e6.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known 9e3bd.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3e9c43.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known b559d.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0a3d78.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known 7f345.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x311982.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 28bd6.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3fe4dd.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 85cbc.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3b5215.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known d33f7.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3f982a.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known cdcd3.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0f1135.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known 3683a.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x35c669.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 22c0f.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x08faa8.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known 65de2.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3458ae.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 60404.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x322989.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known a9633.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x383885.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 4afe4.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3b7bbc.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known c4b0b.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x39f4c9.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 0e6fe.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3be274.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known b1f09.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x014707.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known ea099.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x34f588.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 5d059.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3218e4.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known d8185.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x30e6a7.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 54ba8.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x30809e.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 72e1d.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x36f746.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known b2b97.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x36e201.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known d0d55.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0311f0.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known 03559.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3f9cba.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 6e010.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x33cb02.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known fe38f.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x36d791.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 44533.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3fa7d9.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 3c4b7.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3fc088.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 516ef.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0e974a.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known 16b3d.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x333f3e.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known b459a.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x387bb9.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known ef6e8.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3d0a24.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 3c181.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x03ad6c.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known 9af4b.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x377953.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 26e20.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0fcbed.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . x14
Known c24c1.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3ff800.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 5426d.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3f98b7.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known 4d317.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x36f07c.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Known c23b5.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x360dbb.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13a0244.. x0 x1
Theorem c978c.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)(∀ x4 . x4x3∀ x5 . x5x3x1 x4 x5x1 x5 x4)atleastp u10 x34402e.. x3 x1cf2df.. x3 x1∀ x4 : ο . (a0244.. x0 x1x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3f1c88.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x397406.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x30d539.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x34b1cb.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x372942.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x347362.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3d8b5d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x355171.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x31465e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3ce338.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x36dee7.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3ea964.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3d1a27.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x360a50.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3c059e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3e9db0.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x377203.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3133c1.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3bc7ef.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x39e253.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x368ab4.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x381575.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x386385.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x37c588.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3b019a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x33d346.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x369895.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x31a764.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x351ac7.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3f78c3.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x339cca.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x334ea6.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x36caea.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3e5411.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3948b4.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x358295.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x34a04b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x368a6f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x35d868.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x38629d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3ea11f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x32005f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3de50b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x33369f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3f9d60.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3ff926.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x371397.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x32560b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x348a66.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3289d9.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x337c80.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x35a5ea.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3dd8d8.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3c6a41.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3c2a1e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x315aa1.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3ccc6b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x30446d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x37683c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x396c77.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x307f55.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x393e63.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3c222a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3c61bd.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x302f40.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3b1def.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3e68b8.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x35bc1a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x38befb.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x38fb7c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x39bc89.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x33d118.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x333b5a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3a2f4a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x379b37.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3d833d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x323d0b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3c1005.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x361f8f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3ab383.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3856bc.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3788a1.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x33906f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3c9658.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3b72b8.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3cf898.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3f5373.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x348106.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3d4ea7.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3c1146.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3ca8ce.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x33f609.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x33656c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x39eb9c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x333102.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x348a69.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3d9cea.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3a56d9.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x35f015.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3903bc.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x34a22a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x374e48.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x320d20.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x343c4e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3f8fdb.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x366dda.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x33429e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x328e6a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3d9823.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x31b9db.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3b6bd6.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x326830.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x303c1b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x30d1ce.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x311d3d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x353762.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x31ccbe.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x373f56.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3e5a83.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x37861e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x394275.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x32ad4c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3e5b49.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x36b6c2.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3a0b66.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x36d19b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x308d9f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x399903.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x38a782.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x347dfa.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x322755.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x33f29d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3518d7.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x399ac9.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x399fe6.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x32427f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3d09b6.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x32997a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x35904d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x33c675.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x379a0f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3a79f5.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3c3712.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3f0b8a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3ff600.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x387daf.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3b4530.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x366bd0.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3558af.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x352ac0.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x34c6fc.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x34a27c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3bde2c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x389b0b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3cc2aa.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x334b68.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x3ed7e5.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x4)x4 (proof)