Search for blocks/addresses/...

Proofgold Asset

asset id
1b5a7be684b211178b30b471b14313eb513f7ff4d643c45c88a63687013d81c1
asset hash
60525289b74c7a83209fbac5f0427dcc87d9fc0327e4ef34299248f93722d975
bday / block
38407
tx
a8e91..
preasset
doc published by Pr4zB..
Param 4402e.. : ι(ιιο) → ο
Param cf2df.. : ι(ιιο) → ο
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Param setminussetminus : ιιι
Param SingSing : ιι
Param c7001.. : (ιιο) → ιιιιιιιιιο
Param 68d0b.. : (ιιο) → ιιιιιιιιιιο
Param f4564.. : (ιιο) → ιιιιιιιιιιο
Param 4ff4c.. : (ιιο) → ιιιιιιιιιιο
Param b0a38.. : (ιιο) → ιιιιιιιιιιο
Param a60f8.. : (ιιο) → ιιιιιιιιιιο
Param 78c9a.. : (ιιο) → ιιιιιιιιιιο
Param 69a33.. : (ιιο) → ιιιιιιιιιιο
Param b5965.. : (ιιο) → ιιιιιιιιιιο
Param d7308.. : (ιιο) → ιιιιιιιιιιο
Param 4c67f.. : (ιιο) → ιιιιιιιιιιο
Param 94fe6.. : (ιιο) → ιιιιιιιιιιο
Param 456a0.. : (ιιο) → ιιιιιιιιιιο
Param 03a93.. : (ιιο) → ιιιιιιιιιιο
Param 5dfb3.. : (ιιο) → ιιιιιιιιιιο
Param 6410a.. : (ιιο) → ιιιιιιιιιιο
Param 08130.. : (ιιο) → ιιιιιιιιιιο
Param e26ca.. : (ιιο) → ιιιιιιιιιιο
Param 4e84e.. : (ιιο) → ιιιιιιιιιιο
Param 33d88.. : (ιιο) → ιιιιιιιιιιο
Param a4b3d.. : (ιιο) → ιιιιιιιιιιο
Param 507e8.. : (ιιο) → ιιιιιιιιιιο
Param e0533.. : (ιιο) → ιιιιιιιιιιο
Param f0c46.. : (ιιο) → ιιιιιιιιιιο
Param 4e371.. : (ιιο) → ιιιιιιιιιιο
Param abccc.. : (ιιο) → ιιιιιιιιιιο
Param f4324.. : (ιιο) → ιιιιιιιιιιο
Param fe361.. : (ιιο) → ιιιιιιιιιιο
Param ae9a0.. : (ιιο) → ιιιιιιιιιιο
Param c6b73.. : (ιιο) → ιιιιιιιιιιο
Param 1a172.. : (ιιο) → ιιιιιιιιιιο
Param fb24f.. : (ιιο) → ιιιιιιιιιιο
Param 3c996.. : (ιιο) → ιιιιιιιιιιο
Param 4679c.. : (ιιο) → ιιιιιιιιιιο
Param 26d71.. : (ιιο) → ιιιιιιιιιιο
Param 2fe16.. : (ιιο) → ιιιιιιιιιιο
Param c331d.. : (ιιο) → ιιιιιιιιιιο
Param 24ede.. : (ιιο) → ιιιιιιιιιιο
Param 6f860.. : (ιιο) → ιιιιιιιιιιο
Param d2465.. : (ιιο) → ιιιιιιιιιιο
Param 3b3a3.. : (ιιο) → ιιιιιιιιιιο
Param a7aba.. : (ιιο) → ιιιιιιιιιιο
Param 90ffc.. : (ιιο) → ιιιιιιιιιιο
Param 3759a.. : (ιιο) → ιιιιιιιιιιο
Param 58ba6.. : (ιιο) → ιιιιιιιιιιο
Param e1ba3.. : (ιιο) → ιιιιιιιιιιο
Param 5ffcf.. : (ιιο) → ιιιιιιιιιιο
Param 6cb43.. : (ιιο) → ιιιιιιιιιιο
Param d0208.. : (ιιο) → ιιιιιιιιιιο
Param 9e613.. : (ιιο) → ιιιιιιιιιιο
Param 0fd6e.. : (ιιο) → ιιιιιιιιιιο
Param bdc72.. : (ιιο) → ιιιιιιιιιιο
Param 91378.. : (ιιο) → ιιιιιιιιιιο
Param 14af1.. : (ιιο) → ιιιιιιιιιιο
Param b8539.. : (ιιο) → ιιιιιιιιιιο
Param 8198e.. : (ιιο) → ιιιιιιιιιιο
Param 2365e.. : (ιιο) → ιιιιιιιιιιο
Param 3a344.. : (ιιο) → ιιιιιιιιιιο
Param 29a66.. : (ιιο) → ιιιιιιιιιιο
Param 6935c.. : (ιιο) → ιιιιιιιιιιο
Param 2ed56.. : (ιιο) → ιιιιιιιιιιο
Param d5680.. : (ιιο) → ιιιιιιιιιιο
Param e8fec.. : (ιιο) → ιιιιιιιιιιο
Param d8325.. : (ιιο) → ιιιιιιιιιιο
Param e0b94.. : (ιιο) → ιιιιιιιιιιο
Param f63e8.. : (ιιο) → ιιιιιιιιιιο
Param 251ab.. : (ιιο) → ιιιιιιιιιιο
Param 732e2.. : (ιιο) → ιιιιιιιιιιο
Param 576d3.. : (ιιο) → ιιιιιιιιιιο
Param 1a8a9.. : (ιιο) → ιιιιιιιιιιο
Param 9ab74.. : (ιιο) → ιιιιιιιιιιο
Param 0f519.. : (ιιο) → ιιιιιιιιιιο
Param 1dd74.. : (ιιο) → ιιιιιιιιιιο
Param 5932b.. : (ιιο) → ιιιιιιιιιιο
Param 53b49.. : (ιιο) → ιιιιιιιιιιο
Param 50a7f.. : (ιιο) → ιιιιιιιιιιο
Param efbf0.. : (ιιο) → ιιιιιιιιιιο
Param c13a7.. : (ιιο) → ιιιιιιιιιιο
Param 9002a.. : (ιιο) → ιιιιιιιιιιο
Param 62379.. : (ιιο) → ιιιιιιιιιιο
Param 2e38c.. : (ιιο) → ιιιιιιιιιιο
Param 0897f.. : (ιιο) → ιιιιιιιιιιο
Param 306f8.. : (ιιο) → ιιιιιιιιιιο
Param 9ed6a.. : (ιιο) → ιιιιιιιιιιο
Param fee51.. : (ιιο) → ιιιιιιιιιιο
Param bae07.. : (ιιο) → ιιιιιιιιιιο
Param cd4ee.. : (ιιο) → ιιιιιιιιιιο
Param 22563.. : (ιιο) → ιιιιιιιιιιο
Param bdc7f.. : (ιιο) → ιιιιιιιιιιο
Param dfb78.. : (ιιο) → ιιιιιιιιιιο
Param f8ada.. : (ιιο) → ιιιιιιιιιιο
Param d3342.. : (ιιο) → ιιιιιιιιιιο
Param 0f762.. : (ιιο) → ιιιιιιιιιιο
Param 55451.. : (ιιο) → ιιιιιιιιιιο
Param f380c.. : (ιιο) → ιιιιιιιιιιο
Param 42e23.. : (ιιο) → ιιιιιιιιιιο
Param 8bcec.. : (ιιο) → ιιιιιιιιιιο
Param 1c6c9.. : (ιιο) → ιιιιιιιιιιο
Param 754da.. : (ιιο) → ιιιιιιιιιιο
Param a4ce7.. : (ιιο) → ιιιιιιιιιιο
Param 60a51.. : (ιιο) → ιιιιιιιιιιο
Param ea33e.. : (ιιο) → ιιιιιιιιιιο
Param 9fce6.. : (ιιο) → ιιιιιιιιιιο
Param 0aaf4.. : (ιιο) → ιιιιιιιιιιο
Param ce3b4.. : (ιιο) → ιιιιιιιιιιο
Param 27e6e.. : (ιιο) → ιιιιιιιιιιο
Param a89de.. : (ιιο) → ιιιιιιιιιιο
Param f5fe1.. : (ιιο) → ιιιιιιιιιιο
Param fd185.. : (ιιο) → ιιιιιιιιιιο
Param b7bfe.. : (ιιο) → ιιιιιιιιιιο
Param 86078.. : (ιιο) → ιιιιιιιιιιο
Param d29be.. : (ιιο) → ιιιιιιιιιιο
Param 5cc7a.. : (ιιο) → ιιιιιιιιιιο
Param 49015.. : (ιιο) → ιιιιιιιιιιο
Param 9dea4.. : (ιιο) → ιιιιιιιιιιο
Param f0075.. : (ιιο) → ιιιιιιιιιιο
Param 0a362.. : (ιιο) → ιιιιιιιιιιο
Param 6b1e6.. : (ιιο) → ιιιιιιιιιιο
Param e9c43.. : (ιιο) → ιιιιιιιιιιο
Param a3d78.. : (ιιο) → ιιιιιιιιιιο
Param 11982.. : (ιιο) → ιιιιιιιιιιο
Param fe4dd.. : (ιιο) → ιιιιιιιιιιο
Param b5215.. : (ιιο) → ιιιιιιιιιιο
Param f982a.. : (ιιο) → ιιιιιιιιιιο
Param f1135.. : (ιιο) → ιιιιιιιιιιο
Param 5c669.. : (ιιο) → ιιιιιιιιιιο
Param 8faa8.. : (ιιο) → ιιιιιιιιιιο
Param 458ae.. : (ιιο) → ιιιιιιιιιιο
Param 22989.. : (ιιο) → ιιιιιιιιιιο
Param 83885.. : (ιιο) → ιιιιιιιιιιο
Param b7bbc.. : (ιιο) → ιιιιιιιιιιο
Param 9f4c9.. : (ιιο) → ιιιιιιιιιιο
Param be274.. : (ιιο) → ιιιιιιιιιιο
Param 14707.. : (ιιο) → ιιιιιιιιιιο
Param 4f588.. : (ιιο) → ιιιιιιιιιιο
Param 218e4.. : (ιιο) → ιιιιιιιιιιο
Param 0e6a7.. : (ιιο) → ιιιιιιιιιιο
Param 0809e.. : (ιιο) → ιιιιιιιιιιο
Param 6f746.. : (ιιο) → ιιιιιιιιιιο
Param 6e201.. : (ιιο) → ιιιιιιιιιιο
Param 311f0.. : (ιιο) → ιιιιιιιιιιο
Param f9cba.. : (ιιο) → ιιιιιιιιιιο
Param 3cb02.. : (ιιο) → ιιιιιιιιιιο
Param 6d791.. : (ιιο) → ιιιιιιιιιιο
Param fa7d9.. : (ιιο) → ιιιιιιιιιιο
Param fc088.. : (ιιο) → ιιιιιιιιιιο
Param e974a.. : (ιιο) → ιιιιιιιιιιο
Param 33f3e.. : (ιιο) → ιιιιιιιιιιο
Param 87bb9.. : (ιιο) → ιιιιιιιιιιο
Param d0a24.. : (ιιο) → ιιιιιιιιιιο
Param 3ad6c.. : (ιιο) → ιιιιιιιιιιο
Param 77953.. : (ιιο) → ιιιιιιιιιιο
Param fcbed.. : (ιιο) → ιιιιιιιιιιο
Param ff800.. : (ιιο) → ιιιιιιιιιιο
Param f98b7.. : (ιιο) → ιιιιιιιιιιο
Param 6f07c.. : (ιιο) → ιιιιιιιιιιο
Param 60dbb.. : (ιιο) → ιιιιιιιιιιο
Param f1c88.. : (ιιο) → ιιιιιιιιιιο
Param 97406.. : (ιιο) → ιιιιιιιιιιο
Param 0d539.. : (ιιο) → ιιιιιιιιιιο
Param 4b1cb.. : (ιιο) → ιιιιιιιιιιο
Param 72942.. : (ιιο) → ιιιιιιιιιιο
Param 47362.. : (ιιο) → ιιιιιιιιιιο
Param d8b5d.. : (ιιο) → ιιιιιιιιιιο
Param 55171.. : (ιιο) → ιιιιιιιιιιο
Param 1465e.. : (ιιο) → ιιιιιιιιιιο
Param ce338.. : (ιιο) → ιιιιιιιιιιο
Param 6dee7.. : (ιιο) → ιιιιιιιιιιο
Param ea964.. : (ιιο) → ιιιιιιιιιιο
Param d1a27.. : (ιιο) → ιιιιιιιιιιο
Param 60a50.. : (ιιο) → ιιιιιιιιιιο
Param c059e.. : (ιιο) → ιιιιιιιιιιο
Param e9db0.. : (ιιο) → ιιιιιιιιιιο
Param 77203.. : (ιιο) → ιιιιιιιιιιο
Param 133c1.. : (ιιο) → ιιιιιιιιιιο
Param bc7ef.. : (ιιο) → ιιιιιιιιιιο
Param 9e253.. : (ιιο) → ιιιιιιιιιιο
Param 68ab4.. : (ιιο) → ιιιιιιιιιιο
Param 81575.. : (ιιο) → ιιιιιιιιιιο
Param 86385.. : (ιιο) → ιιιιιιιιιιο
Param 7c588.. : (ιιο) → ιιιιιιιιιιο
Param b019a.. : (ιιο) → ιιιιιιιιιιο
Param 3d346.. : (ιιο) → ιιιιιιιιιιο
Param 69895.. : (ιιο) → ιιιιιιιιιιο
Param 1a764.. : (ιιο) → ιιιιιιιιιιο
Param 51ac7.. : (ιιο) → ιιιιιιιιιιο
Param f78c3.. : (ιιο) → ιιιιιιιιιιο
Param 39cca.. : (ιιο) → ιιιιιιιιιιο
Param 34ea6.. : (ιιο) → ιιιιιιιιιιο
Param 6caea.. : (ιιο) → ιιιιιιιιιιο
Param e5411.. : (ιιο) → ιιιιιιιιιιο
Param 948b4.. : (ιιο) → ιιιιιιιιιιο
Param 58295.. : (ιιο) → ιιιιιιιιιιο
Param 4a04b.. : (ιιο) → ιιιιιιιιιιο
Param 68a6f.. : (ιιο) → ιιιιιιιιιιο
Param 5d868.. : (ιιο) → ιιιιιιιιιιο
Param 8629d.. : (ιιο) → ιιιιιιιιιιο
Param ea11f.. : (ιιο) → ιιιιιιιιιιο
Param 2005f.. : (ιιο) → ιιιιιιιιιιο
Param de50b.. : (ιιο) → ιιιιιιιιιιο
Param 3369f.. : (ιιο) → ιιιιιιιιιιο
Param f9d60.. : (ιιο) → ιιιιιιιιιιο
Param ff926.. : (ιιο) → ιιιιιιιιιιο
Param 71397.. : (ιιο) → ιιιιιιιιιιο
Param 2560b.. : (ιιο) → ιιιιιιιιιιο
Param 48a66.. : (ιιο) → ιιιιιιιιιιο
Param 289d9.. : (ιιο) → ιιιιιιιιιιο
Param 37c80.. : (ιιο) → ιιιιιιιιιιο
Param 5a5ea.. : (ιιο) → ιιιιιιιιιιο
Param dd8d8.. : (ιιο) → ιιιιιιιιιιο
Param c6a41.. : (ιιο) → ιιιιιιιιιιο
Param c2a1e.. : (ιιο) → ιιιιιιιιιιο
Param 15aa1.. : (ιιο) → ιιιιιιιιιιο
Param ccc6b.. : (ιιο) → ιιιιιιιιιιο
Param 0446d.. : (ιιο) → ιιιιιιιιιιο
Param 7683c.. : (ιιο) → ιιιιιιιιιιο
Param 96c77.. : (ιιο) → ιιιιιιιιιιο
Param 07f55.. : (ιιο) → ιιιιιιιιιιο
Param 93e63.. : (ιιο) → ιιιιιιιιιιο
Param c222a.. : (ιιο) → ιιιιιιιιιιο
Param c61bd.. : (ιιο) → ιιιιιιιιιιο
Param 02f40.. : (ιιο) → ιιιιιιιιιιο
Param b1def.. : (ιιο) → ιιιιιιιιιιο
Param e68b8.. : (ιιο) → ιιιιιιιιιιο
Param 5bc1a.. : (ιιο) → ιιιιιιιιιιο
Param 8befb.. : (ιιο) → ιιιιιιιιιιο
Param 8fb7c.. : (ιιο) → ιιιιιιιιιιο
Param 9bc89.. : (ιιο) → ιιιιιιιιιιο
Param 3d118.. : (ιιο) → ιιιιιιιιιιο
Param 33b5a.. : (ιιο) → ιιιιιιιιιιο
Param a2f4a.. : (ιιο) → ιιιιιιιιιιο
Param 79b37.. : (ιιο) → ιιιιιιιιιιο
Param d833d.. : (ιιο) → ιιιιιιιιιιο
Param 23d0b.. : (ιιο) → ιιιιιιιιιιο
Param c1005.. : (ιιο) → ιιιιιιιιιιο
Param 61f8f.. : (ιιο) → ιιιιιιιιιιο
Param ab383.. : (ιιο) → ιιιιιιιιιιο
Param 856bc.. : (ιιο) → ιιιιιιιιιιο
Param 788a1.. : (ιιο) → ιιιιιιιιιιο
Param 3906f.. : (ιιο) → ιιιιιιιιιιο
Param c9658.. : (ιιο) → ιιιιιιιιιιο
Param b72b8.. : (ιιο) → ιιιιιιιιιιο
Param cf898.. : (ιιο) → ιιιιιιιιιιο
Param f5373.. : (ιιο) → ιιιιιιιιιιο
Param 48106.. : (ιιο) → ιιιιιιιιιιο
Param d4ea7.. : (ιιο) → ιιιιιιιιιιο
Param c1146.. : (ιιο) → ιιιιιιιιιιο
Param ca8ce.. : (ιιο) → ιιιιιιιιιιο
Param 3f609.. : (ιιο) → ιιιιιιιιιιο
Param 3656c.. : (ιιο) → ιιιιιιιιιιο
Param 9eb9c.. : (ιιο) → ιιιιιιιιιιο
Param 33102.. : (ιιο) → ιιιιιιιιιιο
Param 48a69.. : (ιιο) → ιιιιιιιιιιο
Param d9cea.. : (ιιο) → ιιιιιιιιιιο
Param a56d9.. : (ιιο) → ιιιιιιιιιιο
Param 5f015.. : (ιιο) → ιιιιιιιιιιο
Param 903bc.. : (ιιο) → ιιιιιιιιιιο
Param 4a22a.. : (ιιο) → ιιιιιιιιιιο
Param 74e48.. : (ιιο) → ιιιιιιιιιιο
Param 20d20.. : (ιιο) → ιιιιιιιιιιο
Param 43c4e.. : (ιιο) → ιιιιιιιιιιο
Param f8fdb.. : (ιιο) → ιιιιιιιιιιο
Param 66dda.. : (ιιο) → ιιιιιιιιιιο
Param 3429e.. : (ιιο) → ιιιιιιιιιιο
Param 28e6a.. : (ιιο) → ιιιιιιιιιιο
Param d9823.. : (ιιο) → ιιιιιιιιιιο
Param 1b9db.. : (ιιο) → ιιιιιιιιιιο
Param b6bd6.. : (ιιο) → ιιιιιιιιιιο
Param 26830.. : (ιιο) → ιιιιιιιιιιο
Param 03c1b.. : (ιιο) → ιιιιιιιιιιο
Param 0d1ce.. : (ιιο) → ιιιιιιιιιιο
Param 11d3d.. : (ιιο) → ιιιιιιιιιιο
Param 53762.. : (ιιο) → ιιιιιιιιιιο
Param 1ccbe.. : (ιιο) → ιιιιιιιιιιο
Param 73f56.. : (ιιο) → ιιιιιιιιιιο
Param e5a83.. : (ιιο) → ιιιιιιιιιιο
Param 7861e.. : (ιιο) → ιιιιιιιιιιο
Param 94275.. : (ιιο) → ιιιιιιιιιιο
Param 2ad4c.. : (ιιο) → ιιιιιιιιιιο
Param e5b49.. : (ιιο) → ιιιιιιιιιιο
Param 6b6c2.. : (ιιο) → ιιιιιιιιιιο
Param a0b66.. : (ιιο) → ιιιιιιιιιιο
Param 6d19b.. : (ιιο) → ιιιιιιιιιιο
Param 08d9f.. : (ιιο) → ιιιιιιιιιιο
Param 99903.. : (ιιο) → ιιιιιιιιιιο
Param 8a782.. : (ιιο) → ιιιιιιιιιιο
Param 47dfa.. : (ιιο) → ιιιιιιιιιιο
Param 22755.. : (ιιο) → ιιιιιιιιιιο
Param 3f29d.. : (ιιο) → ιιιιιιιιιιο
Param 518d7.. : (ιιο) → ιιιιιιιιιιο
Param 99ac9.. : (ιιο) → ιιιιιιιιιιο
Param 99fe6.. : (ιιο) → ιιιιιιιιιιο
Param 2427f.. : (ιιο) → ιιιιιιιιιιο
Param d09b6.. : (ιιο) → ιιιιιιιιιιο
Param 2997a.. : (ιιο) → ιιιιιιιιιιο
Param 5904d.. : (ιιο) → ιιιιιιιιιιο
Param 3c675.. : (ιιο) → ιιιιιιιιιιο
Param 79a0f.. : (ιιο) → ιιιιιιιιιιο
Param a79f5.. : (ιιο) → ιιιιιιιιιιο
Param c3712.. : (ιιο) → ιιιιιιιιιιο
Param f0b8a.. : (ιιο) → ιιιιιιιιιιο
Param ff600.. : (ιιο) → ιιιιιιιιιιο
Param 87daf.. : (ιιο) → ιιιιιιιιιιο
Param b4530.. : (ιιο) → ιιιιιιιιιιο
Param 66bd0.. : (ιιο) → ιιιιιιιιιιο
Param 558af.. : (ιιο) → ιιιιιιιιιιο
Param 52ac0.. : (ιιο) → ιιιιιιιιιιο
Param 4c6fc.. : (ιιο) → ιιιιιιιιιιο
Param 4a27c.. : (ιιο) → ιιιιιιιιιιο
Param bde2c.. : (ιιο) → ιιιιιιιιιιο
Param 89b0b.. : (ιιο) → ιιιιιιιιιιο
Param cc2aa.. : (ιιο) → ιιιιιιιιιιο
Param 34b68.. : (ιιο) → ιιιιιιιιιιο
Param ed7e5.. : (ιιο) → ιιιιιιιιιιο
Definition 5bab1.. := λ x0 . λ x1 : ι → ι → ο . ∀ x2 : ο . (∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x068d0b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0f4564.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x04ff4c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0b0a38.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0a60f8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x078c9a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x069a33.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0b5965.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0d7308.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x04c67f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x094fe6.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0456a0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x003a93.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x05dfb3.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x06410a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x008130.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0e26ca.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x04e84e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x033d88.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0a4b3d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0507e8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0e0533.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0f0c46.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x04e371.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0abccc.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0f4324.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0fe361.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0ae9a0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0c6b73.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x01a172.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0fb24f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x03c996.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x04679c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x026d71.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x02fe16.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0c331d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x024ede.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x06f860.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0d2465.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x03b3a3.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0a7aba.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x090ffc.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x03759a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x058ba6.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0e1ba3.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x05ffcf.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x06cb43.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0d0208.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x09e613.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x00fd6e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0bdc72.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x091378.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x014af1.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0b8539.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x08198e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x02365e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x03a344.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x029a66.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x06935c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x02ed56.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0d5680.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0e8fec.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0d8325.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0e0b94.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0f63e8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0251ab.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0732e2.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0576d3.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x01a8a9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x09ab74.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x00f519.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x01dd74.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x05932b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x053b49.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x050a7f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0efbf0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0c13a7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x09002a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x062379.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x02e38c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x00897f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0306f8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x09ed6a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0fee51.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0bae07.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0cd4ee.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x022563.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0bdc7f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0dfb78.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0f8ada.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0d3342.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x00f762.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x055451.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0f380c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x042e23.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x08bcec.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x01c6c9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0754da.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0a4ce7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x060a51.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0ea33e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x09fce6.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x00aaf4.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0ce3b4.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x027e6e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0a89de.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0f5fe1.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0fd185.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0b7bfe.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x086078.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0d29be.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x05cc7a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x049015.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x09dea4.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0f0075.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x00a362.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x06b1e6.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0e9c43.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0a3d78.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x011982.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0fe4dd.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0b5215.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0f982a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0f1135.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x05c669.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x08faa8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0458ae.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x022989.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x083885.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0b7bbc.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x09f4c9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0be274.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x014707.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x04f588.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0218e4.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x00e6a7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x00809e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x06f746.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x06e201.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0311f0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0f9cba.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x03cb02.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x06d791.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0fa7d9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0fc088.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0e974a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x033f3e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x087bb9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0d0a24.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x03ad6c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x077953.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0fcbed.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0ff800.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0f98b7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x06f07c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x060dbb.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0f1c88.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x097406.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x00d539.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x04b1cb.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x072942.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x047362.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0d8b5d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x055171.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x01465e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0ce338.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x06dee7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0ea964.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0d1a27.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x060a50.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0c059e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0e9db0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x077203.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0133c1.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0bc7ef.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x09e253.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x068ab4.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x081575.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x086385.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x07c588.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0b019a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x03d346.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x069895.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x01a764.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x051ac7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0f78c3.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x039cca.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x034ea6.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x06caea.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0e5411.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0948b4.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x058295.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x04a04b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x068a6f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x05d868.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x08629d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0ea11f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x02005f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0de50b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x03369f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0f9d60.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0ff926.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x071397.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x02560b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x048a66.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0289d9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x037c80.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x05a5ea.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0dd8d8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0c6a41.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0c2a1e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x015aa1.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0ccc6b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x00446d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x07683c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x096c77.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x007f55.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x093e63.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0c222a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0c61bd.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x002f40.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0b1def.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0e68b8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x05bc1a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x08befb.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x08fb7c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x09bc89.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x03d118.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x033b5a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0a2f4a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x079b37.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0d833d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x023d0b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0c1005.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x061f8f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0ab383.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0856bc.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0788a1.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x03906f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0c9658.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0b72b8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0cf898.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0f5373.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x048106.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0d4ea7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0c1146.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0ca8ce.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x03f609.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x03656c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x09eb9c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x033102.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x048a69.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0d9cea.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0a56d9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x05f015.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0903bc.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x04a22a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x074e48.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x020d20.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x043c4e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0f8fdb.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x066dda.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x03429e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x028e6a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0d9823.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x01b9db.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0b6bd6.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x026830.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x003c1b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x00d1ce.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x011d3d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x053762.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x01ccbe.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x073f56.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0e5a83.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x07861e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x094275.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x02ad4c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0e5b49.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x06b6c2.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0a0b66.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x06d19b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x008d9f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x099903.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x08a782.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x047dfa.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x022755.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x03f29d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0518d7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x099ac9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x099fe6.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x02427f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0d09b6.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x02997a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x05904d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x03c675.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x079a0f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0a79f5.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0c3712.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0f0b8a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0ff600.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x087daf.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0b4530.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x066bd0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0558af.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x052ac0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x04c6fc.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x04a27c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0bde2c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x089b0b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0cc2aa.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x034b68.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0ed7e5.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12x2)x2
Known 49b01.. : ∀ 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 . x12x0c7001.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12∀ x13 : ο . (∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0∀ x21 . x21x0∀ x22 . x22x05ffcf.. x2 x14 x15 x16 x17 x18 x19 x20 x3 x21 x22x13)(∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0∀ x21 . x21x0∀ x22 . x22x02ed56.. x2 x14 x3 x15 x16 x17 x18 x19 x20 x21 x22x13)(∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0∀ x21 . x21x0∀ x22 . x22x0d5680.. x2 x14 x15 x16 x17 x18 x19 x20 x3 x21 x22x13)(∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0∀ x21 . x21x0∀ x22 . x22x0a89de.. x2 x14 x15 x16 x17 x18 x19 x20 x21 x3 x22x13)(∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0∀ x21 . x21x0∀ x22 . x22x0f5fe1.. x2 x14 x15 x16 x17 x18 x19 x20 x21 x22 x3x13)(∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0∀ x21 . x21x0∀ x22 . x22x0d29be.. x2 x14 x15 x16 x17 x18 x19 x20 x21 x3 x22x13)(∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0∀ x21 . x21x0∀ x22 . x22x049015.. x2 x14 x15 x16 x17 x18 x19 x20 x21 x22 x3x13)(∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0∀ x21 . x21x0∀ x22 . x22x0289d9.. x2 x14 x15 x16 x17 x18 x3 x19 x20 x21 x22x13)(∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0∀ x21 . x21x0∀ x22 . x22x0b1def.. x2 x14 x15 x16 x17 x18 x19 x20 x21 x3 x22x13)(∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0∀ x21 . x21x0∀ x22 . x22x023d0b.. x2 x14 x15 x16 x17 x18 x19 x20 x3 x21 x22x13)(∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0∀ x21 . x21x0∀ x22 . x22x0b72b8.. x2 x14 x15 x16 x17 x18 x3 x19 x20 x21 x22x13)(∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0∀ x21 . x21x0∀ x22 . x22x0a56d9.. x2 x14 x15 x16 x17 x18 x3 x19 x20 x21 x22x13)(∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0∀ x21 . x21x0∀ x22 . x22x066dda.. x2 x14 x15 x16 x17 x18 x3 x19 x20 x21 x22x13)x13
Known Subq_traSubq_tra : ∀ x0 x1 x2 . x0x1x1x2x0x2
Known setminus_Subqsetminus_Subq : ∀ x0 x1 . setminus x0 x1x0
Theorem 3701a.. : ∀ 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 . x12x3c7001.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1 (proof)