Search for blocks/addresses/...

Proofgold Signed Transaction

vin
Pr7eJ../3a92b..
PUeYp../3f449..
vout
Pr7eJ../4a349.. 5.99 bars
TMFJr../0ada5.. ownership of 16283.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMZ4y../f3470.. ownership of 6db68.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
PUesd../9e272.. doc published by Pr4zB..
Param 4402e.. : ι(ιιο) → ο
Param cf2df.. : ι(ιιο) → ο
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Param setminussetminus : ιιι
Param SingSing : ιι
Param b0193.. : (ιιο) → ιιιιιιιο
Param 372ed.. : (ιιο) → ιιιιιιιιο
Param 3b695.. : (ιιο) → ιιιιιιιιο
Param f7c3d.. : (ιιο) → ιιιιιιιιο
Param 389f9.. : (ιιο) → ιιιιιιιιο
Param b1cc0.. : (ιιο) → ιιιιιιιιο
Param f3cdc.. : (ιιο) → ιιιιιιιιο
Param e37d4.. : (ιιο) → ιιιιιιιιο
Param 230e1.. : (ιιο) → ιιιιιιιιο
Param 05e53.. : (ιιο) → ιιιιιιιιο
Param c0878.. : (ιιο) → ιιιιιιιιο
Param c2463.. : (ιιο) → ιιιιιιιιο
Param 9ea95.. : (ιιο) → ιιιιιιιιο
Param b4c8a.. : (ιιο) → ιιιιιιιιο
Param 7c528.. : (ιιο) → ιιιιιιιιο
Param 0b76b.. : (ιιο) → ιιιιιιιιο
Param 5cb4b.. : (ιιο) → ιιιιιιιιο
Param 6c725.. : (ιιο) → ιιιιιιιιο
Param 84d5a.. : (ιιο) → ιιιιιιιιο
Param 615f5.. : (ιιο) → ιιιιιιιιο
Param fd1bb.. : (ιιο) → ιιιιιιιιο
Param 0c647.. : (ιιο) → ιιιιιιιιο
Param 99ce8.. : (ιιο) → ιιιιιιιιο
Param 0b765.. : (ιιο) → ιιιιιιιιο
Param 1b190.. : (ιιο) → ιιιιιιιιο
Param 1b79b.. : (ιιο) → ιιιιιιιιο
Param 27059.. : (ιιο) → ιιιιιιιιο
Param 1c6d8.. : (ιιο) → ιιιιιιιιο
Param 3a674.. : (ιιο) → ιιιιιιιιο
Param cc0ce.. : (ιιο) → ιιιιιιιιο
Param 60df6.. : (ιιο) → ιιιιιιιιο
Param d03a7.. : (ιιο) → ιιιιιιιιο
Param 7676b.. : (ιιο) → ιιιιιιιιο
Param 2bd9d.. : (ιιο) → ιιιιιιιιο
Param db72f.. : (ιιο) → ιιιιιιιιο
Param c1515.. : (ιιο) → ιιιιιιιιο
Param ccd93.. : (ιιο) → ιιιιιιιιο
Param d5e1e.. : (ιιο) → ιιιιιιιιο
Param 9a85f.. : (ιιο) → ιιιιιιιιο
Param 10481.. : (ιιο) → ιιιιιιιιο
Param afd75.. : (ιιο) → ιιιιιιιιο
Param 29a16.. : (ιιο) → ιιιιιιιιο
Param ac04a.. : (ιιο) → ιιιιιιιιο
Param 7f9b0.. : (ιιο) → ιιιιιιιιο
Param 6d3ff.. : (ιιο) → ιιιιιιιιο
Param e1b03.. : (ιιο) → ιιιιιιιιο
Param 5c2af.. : (ιιο) → ιιιιιιιιο
Param 5f483.. : (ιιο) → ιιιιιιιιο
Param 1610e.. : (ιιο) → ιιιιιιιιο
Param d2827.. : (ιιο) → ιιιιιιιιο
Param da3f2.. : (ιιο) → ιιιιιιιιο
Param 5b060.. : (ιιο) → ιιιιιιιιο
Param 2cfca.. : (ιιο) → ιιιιιιιιο
Param c148f.. : (ιιο) → ιιιιιιιιο
Param d7cce.. : (ιιο) → ιιιιιιιιο
Param 8b97c.. : (ιιο) → ιιιιιιιιο
Param 985a5.. : (ιιο) → ιιιιιιιιο
Param 0314a.. : (ιιο) → ιιιιιιιιο
Param aa9ff.. : (ιιο) → ιιιιιιιιο
Param dd0e6.. : (ιιο) → ιιιιιιιιο
Param 08a39.. : (ιιο) → ιιιιιιιιο
Param cb63a.. : (ιιο) → ιιιιιιιιο
Param 79f22.. : (ιιο) → ιιιιιιιιο
Param d8761.. : (ιιο) → ιιιιιιιιο
Param aa035.. : (ιιο) → ιιιιιιιιο
Param 771b4.. : (ιιο) → ιιιιιιιιο
Param 11c17.. : (ιιο) → ιιιιιιιιο
Param d98cb.. : (ιιο) → ιιιιιιιιο
Param 77ff4.. : (ιιο) → ιιιιιιιιο
Param 83424.. : (ιιο) → ιιιιιιιιο
Param 49663.. : (ιιο) → ιιιιιιιιο
Param 0282b.. : (ιιο) → ιιιιιιιιο
Param 00e1f.. : (ιιο) → ιιιιιιιιο
Param af16d.. : (ιιο) → ιιιιιιιιο
Param a5c5d.. : (ιιο) → ιιιιιιιιο
Param a6215.. : (ιιο) → ιιιιιιιιο
Param c8b10.. : (ιιο) → ιιιιιιιιο
Param 5072f.. : (ιιο) → ιιιιιιιιο
Param 40e45.. : (ιιο) → ιιιιιιιιο
Param fa72d.. : (ιιο) → ιιιιιιιιο
Param 3b6e0.. : (ιιο) → ιιιιιιιιο
Param 662fb.. : (ιιο) → ιιιιιιιιο
Param fd83c.. : (ιιο) → ιιιιιιιιο
Param 3da93.. : (ιιο) → ιιιιιιιιο
Param 24019.. : (ιιο) → ιιιιιιιιο
Param 04ae3.. : (ιιο) → ιιιιιιιιο
Param 45d70.. : (ιιο) → ιιιιιιιιο
Param e4c05.. : (ιιο) → ιιιιιιιιο
Param 3b69b.. : (ιιο) → ιιιιιιιιο
Param 6a4fb.. : (ιιο) → ιιιιιιιιο
Param dbaa8.. : (ιιο) → ιιιιιιιιο
Param 599ac.. : (ιιο) → ιιιιιιιιο
Param e7651.. : (ιιο) → ιιιιιιιιο
Param 33dd8.. : (ιιο) → ιιιιιιιιο
Param 3cc90.. : (ιιο) → ιιιιιιιιο
Param a2a3d.. : (ιιο) → ιιιιιιιιο
Param f693b.. : (ιιο) → ιιιιιιιιο
Param fcfd2.. : (ιιο) → ιιιιιιιιο
Param bc1b4.. : (ιιο) → ιιιιιιιιο
Param e36fd.. : (ιιο) → ιιιιιιιιο
Param 14b71.. : (ιιο) → ιιιιιιιιο
Param fdf53.. : (ιιο) → ιιιιιιιιο
Param 0aba1.. : (ιιο) → ιιιιιιιιο
Param 5ef43.. : (ιιο) → ιιιιιιιιο
Param 85162.. : (ιιο) → ιιιιιιιιο
Param bddcc.. : (ιιο) → ιιιιιιιιο
Param 7c692.. : (ιιο) → ιιιιιιιιο
Param df54f.. : (ιιο) → ιιιιιιιιο
Param 303f2.. : (ιιο) → ιιιιιιιιο
Param 983a2.. : (ιιο) → ιιιιιιιιο
Param 6647d.. : (ιιο) → ιιιιιιιιο
Param 4a35f.. : (ιιο) → ιιιιιιιιο
Param 4f557.. : (ιιο) → ιιιιιιιιο
Param cbd9e.. : (ιιο) → ιιιιιιιιο
Param e643b.. : (ιιο) → ιιιιιιιιο
Param 242d1.. : (ιιο) → ιιιιιιιιο
Param e3246.. : (ιιο) → ιιιιιιιιο
Param 3c797.. : (ιιο) → ιιιιιιιιο
Param 55a2d.. : (ιιο) → ιιιιιιιιο
Param cb670.. : (ιιο) → ιιιιιιιιο
Param dfcf9.. : (ιιο) → ιιιιιιιιο
Param 70101.. : (ιιο) → ιιιιιιιιο
Param 26176.. : (ιιο) → ιιιιιιιιο
Param b9708.. : (ιιο) → ιιιιιιιιο
Param 164fa.. : (ιιο) → ιιιιιιιιο
Param 83a9f.. : (ιιο) → ιιιιιιιιο
Param 830c6.. : (ιιο) → ιιιιιιιιο
Param 70e9a.. : (ιιο) → ιιιιιιιιο
Param 916cb.. : (ιιο) → ιιιιιιιιο
Param ec99f.. : (ιιο) → ιιιιιιιιο
Param 6ea2b.. : (ιιο) → ιιιιιιιιο
Param 9420c.. : (ιιο) → ιιιιιιιιο
Param 089ad.. : (ιιο) → ιιιιιιιιο
Param 35e15.. : (ιιο) → ιιιιιιιιο
Param 279d8.. : (ιιο) → ιιιιιιιιο
Param 2158f.. : (ιιο) → ιιιιιιιιο
Param aa8e6.. : (ιιο) → ιιιιιιιιο
Param 0881d.. : (ιιο) → ιιιιιιιιο
Param 24054.. : (ιιο) → ιιιιιιιιο
Param f0d5b.. : (ιιο) → ιιιιιιιιο
Param 11426.. : (ιιο) → ιιιιιιιιο
Param 725c8.. : (ιιο) → ιιιιιιιιο
Param 81fa4.. : (ιιο) → ιιιιιιιιο
Param 89dbd.. : (ιιο) → ιιιιιιιιο
Param 50d07.. : (ιιο) → ιιιιιιιιο
Param 25f2f.. : (ιιο) → ιιιιιιιιο
Param 02262.. : (ιιο) → ιιιιιιιιο
Param c5458.. : (ιιο) → ιιιιιιιιο
Param 3f579.. : (ιιο) → ιιιιιιιιο
Param 14240.. : (ιιο) → ιιιιιιιιο
Param 67161.. : (ιιο) → ιιιιιιιιο
Param 110e1.. : (ιιο) → ιιιιιιιιο
Param 24aad.. : (ιιο) → ιιιιιιιιο
Param 3dc22.. : (ιιο) → ιιιιιιιιο
Param 7b2a6.. : (ιιο) → ιιιιιιιιο
Param db744.. : (ιιο) → ιιιιιιιιο
Param 80211.. : (ιιο) → ιιιιιιιιο
Param 0d9e0.. : (ιιο) → ιιιιιιιιο
Param 810e7.. : (ιιο) → ιιιιιιιιο
Param 5d19f.. : (ιιο) → ιιιιιιιιο
Param b33d3.. : (ιιο) → ιιιιιιιιο
Param 8f06c.. : (ιιο) → ιιιιιιιιο
Param 478f3.. : (ιιο) → ιιιιιιιιο
Param bd6bc.. : (ιιο) → ιιιιιιιιο
Param cb643.. : (ιιο) → ιιιιιιιιο
Param 6caef.. : (ιιο) → ιιιιιιιιο
Param 97536.. : (ιιο) → ιιιιιιιιο
Param 7a491.. : (ιιο) → ιιιιιιιιο
Param 86c47.. : (ιιο) → ιιιιιιιιο
Param 04e02.. : (ιιο) → ιιιιιιιιο
Param 737dc.. : (ιιο) → ιιιιιιιιο
Param d7a9f.. : (ιιο) → ιιιιιιιιο
Param 5c6e5.. : (ιιο) → ιιιιιιιιο
Param 8df3f.. : (ιιο) → ιιιιιιιιο
Param d97a2.. : (ιιο) → ιιιιιιιιο
Param bc747.. : (ιιο) → ιιιιιιιιο
Param c6cd1.. : (ιιο) → ιιιιιιιιο
Param 1d96c.. : (ιιο) → ιιιιιιιιο
Param c2c18.. : (ιιο) → ιιιιιιιιο
Param 70e38.. : (ιιο) → ιιιιιιιιο
Definition 2426f.. := λ x0 . λ x1 : ι → ι → ο . ∀ x2 : ο . (∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0372ed.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x03b695.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0f7c3d.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0389f9.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0b1cc0.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0f3cdc.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0e37d4.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0230e1.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x005e53.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0c0878.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0c2463.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x09ea95.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0b4c8a.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x07c528.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x00b76b.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x05cb4b.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x06c725.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x084d5a.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0615f5.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0fd1bb.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x00c647.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x099ce8.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x00b765.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x01b190.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x01b79b.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x027059.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x01c6d8.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x03a674.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0cc0ce.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x060df6.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0d03a7.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x07676b.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x02bd9d.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0db72f.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0c1515.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0ccd93.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0d5e1e.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x09a85f.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x010481.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0afd75.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x029a16.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0ac04a.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x07f9b0.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x06d3ff.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0e1b03.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x05c2af.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x05f483.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x01610e.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0d2827.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0da3f2.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x05b060.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x02cfca.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0c148f.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0d7cce.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x08b97c.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0985a5.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x00314a.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0aa9ff.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0dd0e6.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x008a39.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0cb63a.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x079f22.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0d8761.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0aa035.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0771b4.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x011c17.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0d98cb.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x077ff4.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x083424.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x049663.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x00282b.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x000e1f.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0af16d.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0a5c5d.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0a6215.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0c8b10.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x05072f.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x040e45.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0fa72d.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x03b6e0.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0662fb.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0fd83c.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x03da93.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x024019.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x004ae3.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x045d70.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0e4c05.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x03b69b.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x06a4fb.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0dbaa8.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0599ac.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0e7651.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x033dd8.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x03cc90.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0a2a3d.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0f693b.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0fcfd2.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0bc1b4.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0e36fd.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x014b71.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0fdf53.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x00aba1.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x05ef43.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x085162.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0bddcc.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x07c692.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0df54f.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0303f2.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0983a2.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x06647d.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x04a35f.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x04f557.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0cbd9e.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0e643b.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0242d1.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0e3246.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x03c797.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x055a2d.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0cb670.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0dfcf9.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x070101.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x026176.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0b9708.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0164fa.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x083a9f.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0830c6.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x070e9a.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0916cb.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0ec99f.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x06ea2b.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x09420c.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0089ad.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x035e15.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0279d8.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x02158f.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0aa8e6.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x00881d.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x024054.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0f0d5b.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x011426.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0725c8.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x081fa4.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x089dbd.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x050d07.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x025f2f.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x002262.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0c5458.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x03f579.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x014240.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x067161.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0110e1.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x024aad.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x03dc22.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x07b2a6.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0db744.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x080211.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x00d9e0.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0810e7.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x05d19f.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0b33d3.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x08f06c.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0478f3.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0bd6bc.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0cb643.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x06caef.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x097536.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x07a491.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x086c47.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x004e02.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0737dc.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0d7a9f.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x05c6e5.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x08df3f.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0d97a2.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0bc747.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0c6cd1.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x01d96c.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0c2c18.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x070e38.. x1 x3 x4 x5 x6 x7 x8 x9 x10x2)x2
Known 9eb08.. : ∀ 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 . x10x0b0193.. x2 x4 x5 x6 x7 x8 x9 x10∀ x11 : ο . (∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x055a2d.. x2 x12 x13 x14 x15 x16 x17 x18 x3x11)(∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0164fa.. x2 x3 x12 x13 x14 x15 x16 x17 x18x11)(∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x070e9a.. x2 x12 x13 x14 x3 x15 x16 x17 x18x11)(∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x06ea2b.. x2 x12 x13 x3 x14 x15 x16 x17 x18x11)(∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0089ad.. x2 x12 x13 x14 x15 x3 x16 x17 x18x11)(∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0c2c18.. x2 x12 x13 x14 x15 x3 x16 x17 x18x11)(∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x070e38.. x2 x12 x13 x3 x14 x15 x16 x17 x18x11)x11
Known Subq_traSubq_tra : ∀ x0 x1 x2 . x0x1x1x2x0x2
Known setminus_Subqsetminus_Subq : ∀ x0 x1 . setminus x0 x1x0
Theorem 16283.. : ∀ 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 . x10x3b0193.. x1 x4 x5 x6 x7 x8 x9 x102426f.. x0 x1 (proof)