Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrCit../23a6d..
PUcpV../90a0b..
vout
PrCit../d1aa3.. 2.68 bars
TMKv8../8e32f.. ownership of feec2.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMZwu../6bc92.. ownership of 88254.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
PUSMn../5330e.. doc published by Pr4zB..
Param atleastpatleastp : ιιο
Param ordsuccordsucc : ιι
Param u9 : ι
Definition u10 := ordsucc u9
Param 4402e.. : ι(ιιο) → ο
Param cf2df.. : ι(ιιο) → ο
Param 5bab1.. : ι(ιιο) → ο
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Param setminussetminus : ιιι
Param SingSing : ιι
Known e2ea8.. : ∀ x0 x1 . atleastp (ordsucc x0) x1∀ x2 : ο . (∀ x3 . and (x3x1) (atleastp x0 (setminus x1 (Sing x3)))x2)x2
Param SubqSubq : ιιο
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.. : (ιιο) → ιιιιιιιιιο
Known f256b.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)(∀ x4 . x4x3∀ x5 . x5x3x1 x4 x5x1 x5 x4)atleastp u9 x34402e.. x3 x1cf2df.. x3 x1∀ x4 : ο . (5bab1.. x0 x1x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x306ba7.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3b0e38.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x361b2a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3093ca.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x392dea.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x396162.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x306d7e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3f3db6.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x31a9c5.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x321189.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3d2a2c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3a13f2.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x35c8a3.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x302d0f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3241b0.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x391113.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3d3618.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3f630d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3fb26f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3dcb32.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x389fec.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x355a3e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x39a66e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3a3d60.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3d0e7c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x32dac5.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3bacd8.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3858d1.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3c7001.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3a4abc.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3f51b8.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x38be9f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3858ba.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x317819.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x38c70b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3a1497.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3d2e51.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x30076f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x359a16.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x394f0c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3fa661.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3b9a4e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3eb506.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x370a3c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x39aef0.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x339c17.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3a62c3.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x322587.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x39f93b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x362e18.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x344916.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x38acce.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3f5da9.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x32bf4d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x31e021.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3ef324.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x31ecf8.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3aa64f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x391ca0.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3c705c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3bc2c6.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x33c50c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3a3794.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x37db3a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3b0749.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3b19dd.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3176ba.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x397793.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x34b4dd.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x38d9b1.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3ee649.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x343a9d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x39eede.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3b7a83.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3cec27.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x31a9fd.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x381d98.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x337e04.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x361fc8.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3bfd4f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3496a0.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3915dd.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3e2ec9.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x384d91.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x322b3a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3a3e51.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3ed012.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x37e5de.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x36e051.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3b4c31.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3e13e5.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x31cf57.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3a47b6.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x31668d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3b47d4.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3dd43e.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3a7e88.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x322bb5.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x353f52.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x36bc75.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x374a95.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3492fc.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x37f17b.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3cc7e8.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x310d66.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3ceccf.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3cf078.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3f4940.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x33a6bc.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x327706.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x30e6b2.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3d5d69.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3255f4.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3e2fd7.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x370755.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3a0d70.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x32e1d5.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3f9a67.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3fef36.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3b8d2a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3e5024.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3a9907.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x38bd80.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x376a6c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3ee178.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3824ef.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x372d65.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x33d3e7.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3446f4.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x314be0.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3f7902.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3076b3.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3654b9.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3d92ce.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x372e0a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x349901.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x36348c.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3e5063.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x393f0f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x32bb2a.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x378a44.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3cdde4.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x38f55d.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x34818f.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)(∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x323b03.. x1 x5 x6 x7 x8 x9 x10 x11 x12 x13x4)x4
Known 7daf4.. : ∀ 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 . x12x006ba7.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12∀ x13 : ο . x13
Known e0719.. : ∀ 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 . x12x3b0e38.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 1a30f.. : ∀ 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 . x12x361b2a.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known f59a2.. : ∀ 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 . x12x3093ca.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 858e2.. : ∀ 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 . x12x392dea.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 2ab05.. : ∀ 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 . x12x396162.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known e9a54.. : ∀ 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 . x12x306d7e.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known f1358.. : ∀ 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 . x12x3f3db6.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known d08d7.. : ∀ 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 . x12x31a9c5.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 7c096.. : ∀ 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 . x12x321189.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known e8ce3.. : ∀ 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 . x12x3d2a2c.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 6beb8.. : ∀ 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 . x12x3a13f2.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 59256.. : ∀ 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 . x12x35c8a3.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 3613d.. : ∀ 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 . x12x302d0f.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 0bc50.. : ∀ 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 . x12x3241b0.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known cd391.. : ∀ 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 . x12x391113.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 50ee3.. : ∀ 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 . x12x3d3618.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 94de4.. : ∀ 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 . x12x3f630d.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 54cef.. : ∀ 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 . x12x3fb26f.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 3a774.. : ∀ 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 . x12x3dcb32.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 71ec1.. : ∀ 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 . x12x389fec.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 53960.. : ∀ 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 . x12x355a3e.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known b25e2.. : ∀ 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 . x12x39a66e.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known c7ce2.. : ∀ 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 . x12x3a3d60.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 54a2e.. : ∀ 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 . x12x3d0e7c.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known e2134.. : ∀ 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 . x12x32dac5.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 6b571.. : ∀ 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 . x12x3bacd8.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 10aef.. : ∀ 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 . x12x3858d1.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 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
Known 96398.. : ∀ 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 . x12x3a4abc.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 018c9.. : ∀ 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 . x12x3f51b8.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known ba3e4.. : ∀ 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 . x12x38be9f.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 1a73e.. : ∀ 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 . x12x3858ba.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known c0798.. : ∀ 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 . x12x317819.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known c89cc.. : ∀ 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 . x12x38c70b.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 3bafe.. : ∀ 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 . x12x3a1497.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 075bf.. : ∀ 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 . x12x3d2e51.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 58605.. : ∀ 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 . x12x00076f.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12∀ x13 : ο . x13
Known 8ef8b.. : ∀ 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 . x12x359a16.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 49ae6.. : ∀ 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 . x12x394f0c.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 385f8.. : ∀ 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 . x12x3fa661.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known af32d.. : ∀ 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 . x12x3b9a4e.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known d3d64.. : ∀ 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 . x12x3eb506.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 5c6d8.. : ∀ 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 . x12x370a3c.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known e2fb1.. : ∀ 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 . x12x39aef0.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 4eecf.. : ∀ 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 . x12x339c17.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 1b89c.. : ∀ 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 . x12x3a62c3.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known ef05e.. : ∀ 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 . x12x322587.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known afd8e.. : ∀ 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 . x12x39f93b.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 7a927.. : ∀ 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 . x12x362e18.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known eee35.. : ∀ 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 . x12x344916.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known b0add.. : ∀ 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 . x12x38acce.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 34f71.. : ∀ 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 . x12x3f5da9.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 275da.. : ∀ 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 . x12x32bf4d.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known d030a.. : ∀ 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 . x12x31e021.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 4cb2c.. : ∀ 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 . x12x3ef324.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 2609f.. : ∀ 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 . x12x31ecf8.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 4ee2c.. : ∀ 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 . x12x3aa64f.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 4e454.. : ∀ 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 . x12x391ca0.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 12ea2.. : ∀ 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 . x12x3c705c.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 09417.. : ∀ 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 . x12x3bc2c6.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 232fb.. : ∀ 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 . x12x33c50c.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 49425.. : ∀ 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 . x12x3a3794.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 9c794.. : ∀ 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 . x12x37db3a.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 947d7.. : ∀ 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 . x12x3b0749.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 33589.. : ∀ 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 . x12x3b19dd.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known cd9af.. : ∀ 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 . x12x3176ba.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 86d7f.. : ∀ 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 . x12x397793.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 25eec.. : ∀ 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 . x12x34b4dd.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known e7c32.. : ∀ 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 . x12x38d9b1.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 9ae9f.. : ∀ 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 . x12x3ee649.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 02ebd.. : ∀ 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 . x12x043a9d.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12∀ x13 : ο . x13
Known efeff.. : ∀ 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 . x12x39eede.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known c85e7.. : ∀ 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 . x12x3b7a83.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 0f029.. : ∀ 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 . x12x3cec27.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 501e3.. : ∀ 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 . x12x31a9fd.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known cc277.. : ∀ 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 . x12x381d98.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 9efdc.. : ∀ 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 . x12x337e04.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 29dfb.. : ∀ 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 . x12x361fc8.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 8fa6b.. : ∀ 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 . x12x3bfd4f.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 75ae5.. : ∀ 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 . x12x3496a0.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 601fe.. : ∀ 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 . x12x3915dd.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known dda92.. : ∀ 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 . x12x3e2ec9.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 43aa1.. : ∀ 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 . x12x384d91.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 48184.. : ∀ 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 . x12x322b3a.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 586ac.. : ∀ 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 . x12x3a3e51.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 79a4a.. : ∀ 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 . x12x3ed012.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known bfd15.. : ∀ 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 . x12x37e5de.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 2d870.. : ∀ 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 . x12x36e051.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 22120.. : ∀ 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 . x12x3b4c31.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 08dcf.. : ∀ 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 . x12x3e13e5.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 01e8a.. : ∀ 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 . x12x31cf57.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known e60d0.. : ∀ 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 . x12x3a47b6.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 771e8.. : ∀ 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 . x12x31668d.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 86e3f.. : ∀ 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 . x12x3b47d4.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 1811c.. : ∀ 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 . x12x3dd43e.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known be44a.. : ∀ 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 . x12x3a7e88.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 2e3f7.. : ∀ 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 . x12x322bb5.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 58d86.. : ∀ 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 . x12x353f52.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 0c026.. : ∀ 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 . x12x06bc75.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12∀ x13 : ο . x13
Known 472a0.. : ∀ 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 . x12x374a95.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 0f7d7.. : ∀ 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 . x12x3492fc.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known dabf4.. : ∀ 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 . x12x37f17b.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 37e36.. : ∀ 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 . x12x0cc7e8.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12∀ x13 : ο . x13
Known 9aae9.. : ∀ 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 . x12x310d66.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known bf274.. : ∀ 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 . x12x3ceccf.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 366b5.. : ∀ 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 . x12x3cf078.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known e1218.. : ∀ 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 . x12x3f4940.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known e4093.. : ∀ 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 . x12x33a6bc.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 10f87.. : ∀ 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 . x12x327706.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 26d62.. : ∀ 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 . x12x30e6b2.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 13c6c.. : ∀ 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 . x12x3d5d69.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known cc30c.. : ∀ 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 . x12x0255f4.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12∀ x13 : ο . x13
Known 5b367.. : ∀ 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 . x12x3e2fd7.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 79b20.. : ∀ 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 . x12x370755.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 6bfe2.. : ∀ 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 . x12x3a0d70.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 17f14.. : ∀ 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 . x12x32e1d5.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known cfa25.. : ∀ 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 . x12x0f9a67.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12∀ x13 : ο . x13
Known dd305.. : ∀ 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 . x12x3fef36.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known a72a1.. : ∀ 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 . x12x3b8d2a.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 684fa.. : ∀ 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 . x12x3e5024.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 73bf7.. : ∀ 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 . x12x3a9907.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 5b6aa.. : ∀ 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 . x12x38bd80.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 71413.. : ∀ 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 . x12x376a6c.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 79ed5.. : ∀ 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 . x12x3ee178.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known f116f.. : ∀ 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 . x12x3824ef.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 8ac5c.. : ∀ 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 . x12x372d65.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 30b69.. : ∀ 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 . x12x33d3e7.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 7cfa2.. : ∀ 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 . x12x3446f4.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 8896c.. : ∀ 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 . x12x314be0.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 2b542.. : ∀ 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 . x12x3f7902.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known c0ca2.. : ∀ 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 . x12x3076b3.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 8513d.. : ∀ 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 . x12x3654b9.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 5e6fc.. : ∀ 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 . x12x3d92ce.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 5d08d.. : ∀ 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 . x12x372e0a.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 4de8c.. : ∀ 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 . x12x349901.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 71e5b.. : ∀ 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 . x12x36348c.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 909ba.. : ∀ 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 . x12x3e5063.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 7cd66.. : ∀ 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 . x12x393f0f.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known b257d.. : ∀ 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 . x12x32bb2a.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known e60b6.. : ∀ 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 . x12x378a44.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 4982b.. : ∀ 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 . x12x3cdde4.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 6f2ec.. : ∀ 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 . x12x38f55d.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 151a9.. : ∀ 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 . x12x34818f.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 68054.. : ∀ 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 . x12x323b03.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known setminus_Subqsetminus_Subq : ∀ x0 x1 . setminus x0 x1x0
Known Subq_refSubq_ref : ∀ x0 . x0x0
Known e7c7c.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . x0x1cf2df.. x1 x2cf2df.. x0 x2
Known a55d1.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . x0x14402e.. x1 x24402e.. x0 x2
Known setminusE1setminusE1 : ∀ x0 x1 x2 . x2setminus x0 x1x2x0
Theorem feec2.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)atleastp u10 x04402e.. x0 x1cf2df.. x0 x15bab1.. x0 x1 (proof)