Search for blocks/addresses/...

Proofgold Asset

asset id
87b73cd69076bfb7a03b0edc5aa2271f65c64baecd356522d44621f8134d9be3
asset hash
aca25b76c2d3ae6547d511eeafba10d27bf4b1079d9cae8a952428a6eed9e8a8
bday / block
37180
tx
fcd54..
preasset
doc published by Pr4zB..
Param 4402e.. : ι(ιιο) → ο
Param cf2df.. : ι(ιιο) → ο
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Param setminussetminus : ιιι
Param SingSing : ιι
Param 0aba1.. : (ιιο) → ιιιιιιιιο
Param 2dbe7.. : (ιιο) → ιιιιιιιιιο
Param 150dd.. : (ιιο) → ιιιιιιιιιο
Param 3fca5.. : (ιιο) → ιιιιιιιιιο
Param 093ad.. : (ιιο) → ιιιιιιιιιο
Param d0980.. : (ιιο) → ιιιιιιιιιο
Param 682ac.. : (ιιο) → ιιιιιιιιιο
Param 05a8c.. : (ιιο) → ιιιιιιιιιο
Param de95d.. : (ιιο) → ιιιιιιιιιο
Param b1702.. : (ιιο) → ιιιιιιιιιο
Param f444d.. : (ιιο) → ιιιιιιιιιο
Param 4086f.. : (ιιο) → ιιιιιιιιιο
Param 07fce.. : (ιιο) → ιιιιιιιιιο
Param 79ee1.. : (ιιο) → ιιιιιιιιιο
Param 7cafd.. : (ιιο) → ιιιιιιιιιο
Param 59632.. : (ιιο) → ιιιιιιιιιο
Param de118.. : (ιιο) → ιιιιιιιιιο
Param a40ae.. : (ιιο) → ιιιιιιιιιο
Param 228c9.. : (ιιο) → ιιιιιιιιιο
Param 3f98b.. : (ιιο) → ιιιιιιιιιο
Param b43ab.. : (ιιο) → ιιιιιιιιιο
Param 286f8.. : (ιιο) → ιιιιιιιιιο
Param a2b8b.. : (ιιο) → ιιιιιιιιιο
Param 62ac7.. : (ιιο) → ιιιιιιιιιο
Param 3c407.. : (ιιο) → ιιιιιιιιιο
Param fa2d0.. : (ιιο) → ιιιιιιιιιο
Param 76e3a.. : (ιιο) → ιιιιιιιιιο
Param 79529.. : (ιιο) → ιιιιιιιιιο
Param ba960.. : (ιιο) → ιιιιιιιιιο
Param 1b69c.. : (ιιο) → ιιιιιιιιιο
Param 86d28.. : (ιιο) → ιιιιιιιιιο
Param 6e81c.. : (ιιο) → ιιιιιιιιιο
Param 2bad0.. : (ιιο) → ιιιιιιιιιο
Param d3446.. : (ιιο) → ιιιιιιιιιο
Param ee5b5.. : (ιιο) → ιιιιιιιιιο
Param e9fc9.. : (ιιο) → ιιιιιιιιιο
Param e8ba7.. : (ιιο) → ιιιιιιιιιο
Param c8a3f.. : (ιιο) → ιιιιιιιιιο
Param 02471.. : (ιιο) → ιιιιιιιιιο
Param 811c0.. : (ιιο) → ιιιιιιιιιο
Param 96c31.. : (ιιο) → ιιιιιιιιιο
Param 68de1.. : (ιιο) → ιιιιιιιιιο
Param 45286.. : (ιιο) → ιιιιιιιιιο
Param a2064.. : (ιιο) → ιιιιιιιιιο
Param ab042.. : (ιιο) → ιιιιιιιιιο
Param 723e0.. : (ιιο) → ιιιιιιιιιο
Param 94ee4.. : (ιιο) → ιιιιιιιιιο
Param 2ffc8.. : (ιιο) → ιιιιιιιιιο
Param d0e1f.. : (ιιο) → ιιιιιιιιιο
Param dc830.. : (ιιο) → ιιιιιιιιιο
Param f96b5.. : (ιιο) → ιιιιιιιιιο
Param 4b18d.. : (ιιο) → ιιιιιιιιιο
Param 356c7.. : (ιιο) → ιιιιιιιιιο
Param d68bd.. : (ιιο) → ιιιιιιιιιο
Param 53286.. : (ιιο) → ιιιιιιιιιο
Param 34ae8.. : (ιιο) → ιιιιιιιιιο
Param df50d.. : (ιιο) → ιιιιιιιιιο
Param 5d8ad.. : (ιιο) → ιιιιιιιιιο
Param 105be.. : (ιιο) → ιιιιιιιιιο
Param 95ba7.. : (ιιο) → ιιιιιιιιιο
Param 2c7a3.. : (ιιο) → ιιιιιιιιιο
Param 54c7d.. : (ιιο) → ιιιιιιιιιο
Param f842a.. : (ιιο) → ιιιιιιιιιο
Param 79af9.. : (ιιο) → ιιιιιιιιιο
Param 74622.. : (ιιο) → ιιιιιιιιιο
Param b39ef.. : (ιιο) → ιιιιιιιιιο
Param 23b40.. : (ιιο) → ιιιιιιιιιο
Param ba015.. : (ιιο) → ιιιιιιιιιο
Param a6296.. : (ιιο) → ιιιιιιιιιο
Param 4e4f8.. : (ιιο) → ιιιιιιιιιο
Param 989b4.. : (ιιο) → ιιιιιιιιιο
Param 4e91d.. : (ιιο) → ιιιιιιιιιο
Param 263f9.. : (ιιο) → ιιιιιιιιιο
Param 0db75.. : (ιιο) → ιιιιιιιιιο
Param bce5f.. : (ιιο) → ιιιιιιιιιο
Param ed1c7.. : (ιιο) → ιιιιιιιιιο
Param 8dd5c.. : (ιιο) → ιιιιιιιιιο
Param 292f7.. : (ιιο) → ιιιιιιιιιο
Param ad740.. : (ιιο) → ιιιιιιιιιο
Param 73f36.. : (ιιο) → ιιιιιιιιιο
Param 010eb.. : (ιιο) → ιιιιιιιιιο
Param b571f.. : (ιιο) → ιιιιιιιιιο
Param c480f.. : (ιιο) → ιιιιιιιιιο
Param 0768d.. : (ιιο) → ιιιιιιιιιο
Param 44fd1.. : (ιιο) → ιιιιιιιιιο
Param 30a11.. : (ιιο) → ιιιιιιιιιο
Param fa0f3.. : (ιιο) → ιιιιιιιιιο
Param 30182.. : (ιιο) → ιιιιιιιιιο
Param 803e1.. : (ιιο) → ιιιιιιιιιο
Param 2eb4b.. : (ιιο) → ιιιιιιιιιο
Param 4d3d7.. : (ιιο) → ιιιιιιιιιο
Param 1e661.. : (ιιο) → ιιιιιιιιιο
Param df026.. : (ιιο) → ιιιιιιιιιο
Param 14fa0.. : (ιιο) → ιιιιιιιιιο
Param ef237.. : (ιιο) → ιιιιιιιιιο
Param 62ca1.. : (ιιο) → ιιιιιιιιιο
Param a94a5.. : (ιιο) → ιιιιιιιιιο
Param 38793.. : (ιιο) → ιιιιιιιιιο
Param 23926.. : (ιιο) → ιιιιιιιιιο
Param 71ae3.. : (ιιο) → ιιιιιιιιιο
Param 889b5.. : (ιιο) → ιιιιιιιιιο
Param 86fe8.. : (ιιο) → ιιιιιιιιιο
Param fb47b.. : (ιιο) → ιιιιιιιιιο
Param 8fbce.. : (ιιο) → ιιιιιιιιιο
Param 2c550.. : (ιιο) → ιιιιιιιιιο
Param 05795.. : (ιιο) → ιιιιιιιιιο
Param aa358.. : (ιιο) → ιιιιιιιιιο
Param f0823.. : (ιιο) → ιιιιιιιιιο
Param 57f60.. : (ιιο) → ιιιιιιιιιο
Param c4d5c.. : (ιιο) → ιιιιιιιιιο
Param 729bd.. : (ιιο) → ιιιιιιιιιο
Param e37fb.. : (ιιο) → ιιιιιιιιιο
Param 5f6ee.. : (ιιο) → ιιιιιιιιιο
Param f14aa.. : (ιιο) → ιιιιιιιιιο
Param 13ddc.. : (ιιο) → ιιιιιιιιιο
Param af5b6.. : (ιιο) → ιιιιιιιιιο
Param f6312.. : (ιιο) → ιιιιιιιιιο
Param 07c0f.. : (ιιο) → ιιιιιιιιιο
Param fc090.. : (ιιο) → ιιιιιιιιιο
Param b7e1a.. : (ιιο) → ιιιιιιιιιο
Param adf05.. : (ιιο) → ιιιιιιιιιο
Param c2e8a.. : (ιιο) → ιιιιιιιιιο
Param 923e2.. : (ιιο) → ιιιιιιιιιο
Param dbf71.. : (ιιο) → ιιιιιιιιιο
Param 47203.. : (ιιο) → ιιιιιιιιιο
Param 8c9ed.. : (ιιο) → ιιιιιιιιιο
Param 13b7c.. : (ιιο) → ιιιιιιιιιο
Param 2122d.. : (ιιο) → ιιιιιιιιιο
Param 4e6fe.. : (ιιο) → ιιιιιιιιιο
Param 4006a.. : (ιιο) → ιιιιιιιιιο
Param 83aec.. : (ιιο) → ιιιιιιιιιο
Param abda1.. : (ιιο) → ιιιιιιιιιο
Param 87273.. : (ιιο) → ιιιιιιιιιο
Param 130d9.. : (ιιο) → ιιιιιιιιιο
Param 58208.. : (ιιο) → ιιιιιιιιιο
Param e1aab.. : (ιιο) → ιιιιιιιιιο
Param 0788d.. : (ιιο) → ιιιιιιιιιο
Param 627df.. : (ιιο) → ιιιιιιιιιο
Param 65996.. : (ιιο) → ιιιιιιιιιο
Param 724e0.. : (ιιο) → ιιιιιιιιιο
Param 24120.. : (ιιο) → ιιιιιιιιιο
Param 58722.. : (ιιο) → ιιιιιιιιιο
Param 90d0e.. : (ιιο) → ιιιιιιιιιο
Param 055d9.. : (ιιο) → ιιιιιιιιιο
Param 6661c.. : (ιιο) → ιιιιιιιιιο
Param 9069f.. : (ιιο) → ιιιιιιιιιο
Param 06ba7.. : (ιιο) → ιιιιιιιιιο
Param b0e38.. : (ιιο) → ιιιιιιιιιο
Param 61b2a.. : (ιιο) → ιιιιιιιιιο
Param 093ca.. : (ιιο) → ιιιιιιιιιο
Param 92dea.. : (ιιο) → ιιιιιιιιιο
Param 96162.. : (ιιο) → ιιιιιιιιιο
Param 06d7e.. : (ιιο) → ιιιιιιιιιο
Param f3db6.. : (ιιο) → ιιιιιιιιιο
Param 1a9c5.. : (ιιο) → ιιιιιιιιιο
Param 21189.. : (ιιο) → ιιιιιιιιιο
Param d2a2c.. : (ιιο) → ιιιιιιιιιο
Param a13f2.. : (ιιο) → ιιιιιιιιιο
Param 5c8a3.. : (ιιο) → ιιιιιιιιιο
Param 02d0f.. : (ιιο) → ιιιιιιιιιο
Param 241b0.. : (ιιο) → ιιιιιιιιιο
Param 91113.. : (ιιο) → ιιιιιιιιιο
Param d3618.. : (ιιο) → ιιιιιιιιιο
Param f630d.. : (ιιο) → ιιιιιιιιιο
Param fb26f.. : (ιιο) → ιιιιιιιιιο
Param dcb32.. : (ιιο) → ιιιιιιιιιο
Param 89fec.. : (ιιο) → ιιιιιιιιιο
Param 55a3e.. : (ιιο) → ιιιιιιιιιο
Param 9a66e.. : (ιιο) → ιιιιιιιιιο
Param a3d60.. : (ιιο) → ιιιιιιιιιο
Param d0e7c.. : (ιιο) → ιιιιιιιιιο
Param 2dac5.. : (ιιο) → ιιιιιιιιιο
Param bacd8.. : (ιιο) → ιιιιιιιιιο
Param 858d1.. : (ιιο) → ιιιιιιιιιο
Param c7001.. : (ιιο) → ιιιιιιιιιο
Param a4abc.. : (ιιο) → ιιιιιιιιιο
Param f51b8.. : (ιιο) → ιιιιιιιιιο
Param 8be9f.. : (ιιο) → ιιιιιιιιιο
Param 858ba.. : (ιιο) → ιιιιιιιιιο
Param 17819.. : (ιιο) → ιιιιιιιιιο
Param 8c70b.. : (ιιο) → ιιιιιιιιιο
Param a1497.. : (ιιο) → ιιιιιιιιιο
Param d2e51.. : (ιιο) → ιιιιιιιιιο
Param 0076f.. : (ιιο) → ιιιιιιιιιο
Param 59a16.. : (ιιο) → ιιιιιιιιιο
Param 94f0c.. : (ιιο) → ιιιιιιιιιο
Param fa661.. : (ιιο) → ιιιιιιιιιο
Param b9a4e.. : (ιιο) → ιιιιιιιιιο
Param eb506.. : (ιιο) → ιιιιιιιιιο
Param 70a3c.. : (ιιο) → ιιιιιιιιιο
Param 9aef0.. : (ιιο) → ιιιιιιιιιο
Param 39c17.. : (ιιο) → ιιιιιιιιιο
Param a62c3.. : (ιιο) → ιιιιιιιιιο
Param 22587.. : (ιιο) → ιιιιιιιιιο
Param 9f93b.. : (ιιο) → ιιιιιιιιιο
Param 62e18.. : (ιιο) → ιιιιιιιιιο
Param 44916.. : (ιιο) → ιιιιιιιιιο
Param 8acce.. : (ιιο) → ιιιιιιιιιο
Param f5da9.. : (ιιο) → ιιιιιιιιιο
Param 2bf4d.. : (ιιο) → ιιιιιιιιιο
Param 1e021.. : (ιιο) → ιιιιιιιιιο
Param ef324.. : (ιιο) → ιιιιιιιιιο
Param 1ecf8.. : (ιιο) → ιιιιιιιιιο
Param aa64f.. : (ιιο) → ιιιιιιιιιο
Param 91ca0.. : (ιιο) → ιιιιιιιιιο
Param c705c.. : (ιιο) → ιιιιιιιιιο
Param bc2c6.. : (ιιο) → ιιιιιιιιιο
Param 3c50c.. : (ιιο) → ιιιιιιιιιο
Param a3794.. : (ιιο) → ιιιιιιιιιο
Param 7db3a.. : (ιιο) → ιιιιιιιιιο
Param b0749.. : (ιιο) → ιιιιιιιιιο
Param b19dd.. : (ιιο) → ιιιιιιιιιο
Param 176ba.. : (ιιο) → ιιιιιιιιιο
Param 97793.. : (ιιο) → ιιιιιιιιιο
Param 4b4dd.. : (ιιο) → ιιιιιιιιιο
Param 8d9b1.. : (ιιο) → ιιιιιιιιιο
Param ee649.. : (ιιο) → ιιιιιιιιιο
Param 43a9d.. : (ιιο) → ιιιιιιιιιο
Param 9eede.. : (ιιο) → ιιιιιιιιιο
Param b7a83.. : (ιιο) → ιιιιιιιιιο
Param cec27.. : (ιιο) → ιιιιιιιιιο
Param 1a9fd.. : (ιιο) → ιιιιιιιιιο
Param 81d98.. : (ιιο) → ιιιιιιιιιο
Param 37e04.. : (ιιο) → ιιιιιιιιιο
Param 61fc8.. : (ιιο) → ιιιιιιιιιο
Param bfd4f.. : (ιιο) → ιιιιιιιιιο
Param 496a0.. : (ιιο) → ιιιιιιιιιο
Param 915dd.. : (ιιο) → ιιιιιιιιιο
Param e2ec9.. : (ιιο) → ιιιιιιιιιο
Param 84d91.. : (ιιο) → ιιιιιιιιιο
Param 22b3a.. : (ιιο) → ιιιιιιιιιο
Param a3e51.. : (ιιο) → ιιιιιιιιιο
Param ed012.. : (ιιο) → ιιιιιιιιιο
Param 7e5de.. : (ιιο) → ιιιιιιιιιο
Param 6e051.. : (ιιο) → ιιιιιιιιιο
Param b4c31.. : (ιιο) → ιιιιιιιιιο
Param e13e5.. : (ιιο) → ιιιιιιιιιο
Param 1cf57.. : (ιιο) → ιιιιιιιιιο
Param a47b6.. : (ιιο) → ιιιιιιιιιο
Param 1668d.. : (ιιο) → ιιιιιιιιιο
Param b47d4.. : (ιιο) → ιιιιιιιιιο
Param dd43e.. : (ιιο) → ιιιιιιιιιο
Param a7e88.. : (ιιο) → ιιιιιιιιιο
Param 22bb5.. : (ιιο) → ιιιιιιιιιο
Param 53f52.. : (ιιο) → ιιιιιιιιιο
Param 6bc75.. : (ιιο) → ιιιιιιιιιο
Param 74a95.. : (ιιο) → ιιιιιιιιιο
Param 492fc.. : (ιιο) → ιιιιιιιιιο
Param 7f17b.. : (ιιο) → ιιιιιιιιιο
Param cc7e8.. : (ιιο) → ιιιιιιιιιο
Param 10d66.. : (ιιο) → ιιιιιιιιιο
Param ceccf.. : (ιιο) → ιιιιιιιιιο
Param cf078.. : (ιιο) → ιιιιιιιιιο
Param f4940.. : (ιιο) → ιιιιιιιιιο
Param 3a6bc.. : (ιιο) → ιιιιιιιιιο
Param 27706.. : (ιιο) → ιιιιιιιιιο
Param 0e6b2.. : (ιιο) → ιιιιιιιιιο
Param d5d69.. : (ιιο) → ιιιιιιιιιο
Param 255f4.. : (ιιο) → ιιιιιιιιιο
Param e2fd7.. : (ιιο) → ιιιιιιιιιο
Param 70755.. : (ιιο) → ιιιιιιιιιο
Param a0d70.. : (ιιο) → ιιιιιιιιιο
Param 2e1d5.. : (ιιο) → ιιιιιιιιιο
Param f9a67.. : (ιιο) → ιιιιιιιιιο
Param fef36.. : (ιιο) → ιιιιιιιιιο
Param b8d2a.. : (ιιο) → ιιιιιιιιιο
Param e5024.. : (ιιο) → ιιιιιιιιιο
Param a9907.. : (ιιο) → ιιιιιιιιιο
Param 8bd80.. : (ιιο) → ιιιιιιιιιο
Param 76a6c.. : (ιιο) → ιιιιιιιιιο
Param ee178.. : (ιιο) → ιιιιιιιιιο
Param 824ef.. : (ιιο) → ιιιιιιιιιο
Param 72d65.. : (ιιο) → ιιιιιιιιιο
Param 3d3e7.. : (ιιο) → ιιιιιιιιιο
Param 446f4.. : (ιιο) → ιιιιιιιιιο
Param 14be0.. : (ιιο) → ιιιιιιιιιο
Param f7902.. : (ιιο) → ιιιιιιιιιο
Param 076b3.. : (ιιο) → ιιιιιιιιιο
Param 654b9.. : (ιιο) → ιιιιιιιιιο
Param d92ce.. : (ιιο) → ιιιιιιιιιο
Param 72e0a.. : (ιιο) → ιιιιιιιιιο
Param 49901.. : (ιιο) → ιιιιιιιιιο
Param 6348c.. : (ιιο) → ιιιιιιιιιο
Param e5063.. : (ιιο) → ιιιιιιιιιο
Param 93f0f.. : (ιιο) → ιιιιιιιιιο
Param 2bb2a.. : (ιιο) → ιιιιιιιιιο
Param 78a44.. : (ιιο) → ιιιιιιιιιο
Param cdde4.. : (ιιο) → ιιιιιιιιιο
Param 8f55d.. : (ιιο) → ιιιιιιιιιο
Param 4818f.. : (ιιο) → ιιιιιιιιιο
Param 23b03.. : (ιιο) → ιιιιιιιιιο
Definition 0946c.. := λ x0 . λ x1 : ι → ι → ο . ∀ x2 : ο . (∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x02dbe7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0150dd.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x03fca5.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0093ad.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0d0980.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0682ac.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x005a8c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0de95d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0b1702.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0f444d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x04086f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x007fce.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x079ee1.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x07cafd.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x059632.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0de118.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a40ae.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0228c9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x03f98b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0b43ab.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0286f8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a2b8b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x062ac7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x03c407.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0fa2d0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x076e3a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x079529.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0ba960.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x01b69c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x086d28.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x06e81c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x02bad0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0d3446.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0ee5b5.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0e9fc9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0e8ba7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0c8a3f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x002471.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0811c0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x096c31.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x068de1.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x045286.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a2064.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0ab042.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0723e0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x094ee4.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x02ffc8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0d0e1f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0dc830.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0f96b5.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x04b18d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0356c7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0d68bd.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x053286.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x034ae8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0df50d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x05d8ad.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0105be.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x095ba7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x02c7a3.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x054c7d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0f842a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x079af9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x074622.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0b39ef.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x023b40.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0ba015.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a6296.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x04e4f8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0989b4.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x04e91d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0263f9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x00db75.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0bce5f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0ed1c7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x08dd5c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0292f7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0ad740.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x073f36.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0010eb.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0b571f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0c480f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x00768d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x044fd1.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x030a11.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0fa0f3.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x030182.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0803e1.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x02eb4b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x04d3d7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x01e661.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0df026.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x014fa0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0ef237.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x062ca1.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a94a5.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x038793.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x023926.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x071ae3.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0889b5.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x086fe8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0fb47b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x08fbce.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x02c550.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x005795.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0aa358.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0f0823.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x057f60.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0c4d5c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0729bd.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0e37fb.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x05f6ee.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0f14aa.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x013ddc.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0af5b6.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0f6312.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x007c0f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0fc090.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0b7e1a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0adf05.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0c2e8a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0923e2.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0dbf71.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x047203.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x08c9ed.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x013b7c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x02122d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x04e6fe.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x04006a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x083aec.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0abda1.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x087273.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0130d9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x058208.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0e1aab.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x00788d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0627df.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x065996.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0724e0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x024120.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x058722.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x090d0e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0055d9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x06661c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x09069f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x006ba7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0b0e38.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x061b2a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0093ca.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x092dea.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x096162.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x006d7e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0f3db6.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x01a9c5.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x021189.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0d2a2c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a13f2.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x05c8a3.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x002d0f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0241b0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x091113.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0d3618.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0f630d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0fb26f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0dcb32.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x089fec.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x055a3e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x09a66e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a3d60.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0d0e7c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x02dac5.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0bacd8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0858d1.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0c7001.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a4abc.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0f51b8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x08be9f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0858ba.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x017819.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x08c70b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a1497.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0d2e51.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x00076f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x059a16.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x094f0c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0fa661.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0b9a4e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0eb506.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x070a3c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x09aef0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x039c17.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a62c3.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x022587.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x09f93b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x062e18.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x044916.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x08acce.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0f5da9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x02bf4d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x01e021.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0ef324.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x01ecf8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0aa64f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x091ca0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0c705c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0bc2c6.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x03c50c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a3794.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x07db3a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0b0749.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0b19dd.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0176ba.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x097793.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x04b4dd.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x08d9b1.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0ee649.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x043a9d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x09eede.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0b7a83.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0cec27.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x01a9fd.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x081d98.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x037e04.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x061fc8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0bfd4f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0496a0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0915dd.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0e2ec9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x084d91.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x022b3a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a3e51.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0ed012.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x07e5de.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x06e051.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0b4c31.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0e13e5.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x01cf57.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a47b6.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x01668d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0b47d4.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0dd43e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a7e88.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x022bb5.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x053f52.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x06bc75.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x074a95.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0492fc.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x07f17b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0cc7e8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x010d66.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0ceccf.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0cf078.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0f4940.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x03a6bc.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x027706.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x00e6b2.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0d5d69.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0255f4.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0e2fd7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x070755.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a0d70.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x02e1d5.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0f9a67.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0fef36.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0b8d2a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0e5024.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a9907.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x08bd80.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x076a6c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0ee178.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0824ef.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x072d65.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x03d3e7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0446f4.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x014be0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0f7902.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0076b3.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0654b9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0d92ce.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x072e0a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x049901.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x06348c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0e5063.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x093f0f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x02bb2a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x078a44.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0cdde4.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x08f55d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x04818f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x023b03.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)x2
Known d6def.. : ∀ 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 . x11x00aba1.. x2 x4 x5 x6 x7 x8 x9 x10 x11∀ x12 : ο . (∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0b43ab.. x2 x13 x14 x15 x16 x17 x3 x18 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x096c31.. x2 x13 x14 x15 x16 x17 x18 x3 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x054c7d.. x2 x3 x13 x14 x15 x16 x17 x18 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0a6296.. x2 x13 x14 x15 x3 x16 x17 x18 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0c480f.. x2 x13 x14 x15 x16 x17 x3 x18 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x00768d.. x2 x13 x14 x15 x16 x17 x3 x18 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x030182.. x2 x13 x14 x15 x3 x16 x17 x18 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0c4d5c.. x2 x13 x14 x15 x16 x17 x18 x3 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x02122d.. x2 x13 x3 x14 x15 x16 x17 x18 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x04e6fe.. x2 x3 x13 x14 x15 x16 x17 x18 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x04006a.. x2 x3 x13 x14 x15 x16 x17 x18 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x083aec.. x2 x13 x3 x14 x15 x16 x17 x18 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x065996.. x2 x13 x14 x15 x16 x3 x17 x18 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0c7001.. x2 x3 x13 x14 x15 x16 x17 x18 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x08be9f.. x2 x13 x14 x15 x16 x3 x17 x18 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0eb506.. x2 x3 x13 x14 x15 x16 x17 x18 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x070a3c.. x2 x13 x3 x14 x15 x16 x17 x18 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x08acce.. x2 x13 x14 x15 x16 x17 x18 x19 x3 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0c705c.. x2 x13 x14 x15 x3 x16 x17 x18 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0cf078.. x2 x13 x14 x15 x3 x16 x17 x18 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x070755.. x2 x13 x14 x3 x15 x16 x17 x18 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0a0d70.. x2 x13 x14 x15 x3 x16 x17 x18 x19 x20x12)x12
Known Subq_traSubq_tra : ∀ x0 x1 x2 . x0x1x1x2x0x2
Known setminus_Subqsetminus_Subq : ∀ x0 x1 . setminus x0 x1x0
Theorem 19619.. : ∀ 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 . x11x30aba1.. x1 x4 x5 x6 x7 x8 x9 x10 x110946c.. x0 x1 (proof)