%------------------------------------------------------------------------------
% File : Geo-III---2018C
% Problem : LCL681+1.015 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : geo -tptp_input -nonempty -inputfile %s
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 12:06:51 PM UTC 2026
% Result : CounterSatisfiable 45.81s 46.06s
% Output : Model 45.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL681+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : geo -tptp_input -nonempty -inputfile %s
% 0.09/0.35 % Computer : n002.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Fri Sep 4 12:55:20 UTC 2026
% 0.09/0.35 % CPUTime :
% 45.81/46.06 GeoParameters:
% 45.81/46.06
% 45.81/46.06 tptp_input = 1
% 45.81/46.06 tptp_output = 0
% 45.81/46.06 nonempty = 1
% 45.81/46.06 inputfile = /export/starexec/sandbox2/benchmark/theBenchmark.p
% 45.81/46.06 includepath = /export/starexec/sandbox2/solver/bin/../../benchmark/
% 45.81/46.06
% 45.81/46.06
% 45.81/46.06 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 45.81/46.06 % SZS output start Model for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 45.81/46.06
% 45.81/46.06 Interpretation 12:
% 45.81/46.06 Guesses:
% 45.81/46.06 0 : guesser 2, 1, ( | 1, 0 ), 0, 45s old, 0 lemmas
% 45.81/46.06 1 : guesser 22, 20, ( | 0, 2, 1 ), 1, 44s old, 0 lemmas
% 45.81/46.06 2 : guesser 43, 41, ( | 0, 2, 1 ), 1, 44s old, 0 lemmas
% 45.81/46.06 3 : guesser 48, 46, ( | 0, 2, 1 ), 2, 38s old, 0 lemmas
% 45.81/46.06 4 : guesser 52, 50, ( | 1, 2, 0 ), 2, 38s old, 0 lemmas
% 45.81/46.06 5 : guesser 59, 57, ( | 0, 2, 1 ), 2, 38s old, 0 lemmas
% 45.81/46.06 6 : guesser 63, 61, ( | 0, 2, 1 ), 2, 38s old, 0 lemmas
% 45.81/46.06 7 : guesser 67, 65, ( | 1, 2, 0 ), 2, 38s old, 0 lemmas
% 45.81/46.06 8 : guesser 74, 72, ( | 1, 2, 0 ), 2, 37s old, 0 lemmas
% 45.81/46.06 9 : guesser 81, 79, ( | 1, 2, 0 ), 2, 37s old, 0 lemmas
% 45.81/46.06 10 : guesser 88, 86, ( | 0, 2, 1 ), 2, 37s old, 0 lemmas
% 45.81/46.06 11 : guesser 92, 90, ( | 0, 2, 1 ), 2, 37s old, 0 lemmas
% 45.81/46.06 12 : guesser 96, 94, ( | 1, 2, 0 ), 2, 37s old, 0 lemmas
% 45.81/46.06 13 : guesser 103, 101, ( | 0, 2, 1 ), 2, 37s old, 0 lemmas
% 45.81/46.06 14 : guesser 107, 105, ( | 0, 2, 1 ), 2, 36s old, 0 lemmas
% 45.81/46.06 15 : guesser 111, 109, ( | 1, 2, 0 ), 2, 36s old, 0 lemmas
% 45.81/46.06 16 : guesser 141, 139, ( | 1, 2, 0 ), 2, 36s old, 0 lemmas
% 45.81/46.06 17 : guesser 142, 140, ( | 1, 2, 0 ), 2, 36s old, 0 lemmas
% 45.81/46.06 18 : guesser 143, 141, ( | 0, 2, 1 ), 2, 36s old, 0 lemmas
% 45.81/46.06 19 : guesser 144, 142, ( | 1, 2, 0 ), 2, 36s old, 0 lemmas
% 45.81/46.06 20 : guesser 145, 143, ( | 0, 2, 1 ), 2, 36s old, 0 lemmas
% 45.81/46.06 21 : guesser 146, 144, ( | 1, 2, 0 ), 2, 36s old, 0 lemmas
% 45.81/46.06 22 : guesser 147, 145, ( | 0, 2, 1 ), 2, 36s old, 0 lemmas
% 45.81/46.06 23 : guesser 148, 146, ( | 0, 2, 1 ), 2, 36s old, 0 lemmas
% 45.81/46.06 24 : guesser 149, 147, ( | 0, 2, 1 ), 2, 36s old, 0 lemmas
% 45.81/46.06 25 : guesser 150, 148, ( | 1, 2, 0 ), 2, 36s old, 0 lemmas
% 45.81/46.06 26 : guesser 151, 149, ( | 1, 2, 0 ), 2, 36s old, 0 lemmas
% 45.81/46.06 27 : guesser 152, 150, ( | 0, 2, 1 ), 2, 36s old, 0 lemmas
% 45.81/46.06 28 : guesser 153, 151, ( | 0, 2, 1 ), 2, 36s old, 0 lemmas
% 45.81/46.06 29 : guesser 154, 152, ( | 0, 2, 1 ), 2, 36s old, 0 lemmas
% 45.81/46.06 30 : guesser 161, 159, ( | 1, 2, 0 ), 2, 35s old, 0 lemmas
% 45.81/46.06 31 : guesser 170, 168, ( | 1, 2, 0 ), 3, 33s old, 0 lemmas
% 45.81/46.06 32 : guesser 177, 175, ( | 1, 2, 0 ), 3, 32s old, 0 lemmas
% 45.81/46.06 33 : guesser 178, 176, ( | 0, 2, 1 ), 3, 32s old, 0 lemmas
% 45.81/46.06 34 : guesser 185, 183, ( | 0, 2, 1 ), 3, 32s old, 0 lemmas
% 45.81/46.06 35 : guesser 192, 190, ( | 1, 2, 0 ), 3, 32s old, 0 lemmas
% 45.81/46.06 36 : guesser 199, 197, ( | 1, 2, 0 ), 3, 32s old, 0 lemmas
% 45.81/46.06 37 : guesser 200, 198, ( | 1, 2, 0 ), 3, 32s old, 0 lemmas
% 45.81/46.06 38 : guesser 207, 205, ( | 0, 2, 1 ), 3, 32s old, 0 lemmas
% 45.81/46.06 39 : guesser 208, 206, ( | 0, 2, 1 ), 3, 32s old, 0 lemmas
% 45.81/46.06 40 : guesser 215, 213, ( | 0, 2, 1 ), 3, 31s old, 0 lemmas
% 45.81/46.06 41 : guesser 216, 214, ( | 1, 2, 0 ), 3, 31s old, 0 lemmas
% 45.81/46.06 42 : guesser 223, 221, ( | 1, 2, 0 ), 3, 31s old, 0 lemmas
% 45.81/46.06 43 : guesser 230, 228, ( | 1, 2, 0 ), 3, 31s old, 0 lemmas
% 45.81/46.06 44 : guesser 237, 235, ( | 1, 2, 0 ), 3, 31s old, 0 lemmas
% 45.81/46.06 45 : guesser 238, 236, ( | 0, 2, 1 ), 3, 31s old, 0 lemmas
% 45.81/46.06 46 : guesser 245, 243, ( | 0, 2, 1 ), 3, 31s old, 0 lemmas
% 45.81/46.06 47 : guesser 252, 250, ( | 0, 2, 1 ), 3, 30s old, 0 lemmas
% 45.81/46.06 48 : guesser 253, 251, ( | 0, 2, 1 ), 3, 30s old, 0 lemmas
% 45.81/46.06 49 : guesser 254, 252, ( | 0, 2, 1 ), 3, 30s old, 0 lemmas
% 45.81/46.06 50 : guesser 255, 253, ( | 1, 2, 0 ), 3, 30s old, 0 lemmas
% 45.81/46.06 51 : guesser 256, 254, ( | 1, 2, 0 ), 3, 30s old, 0 lemmas
% 45.81/46.06 52 : guesser 257, 255, ( | 1, 2, 0 ), 3, 30s old, 0 lemmas
% 45.81/46.06 53 : guesser 258, 256, ( | 1, 2, 0 ), 3, 30s old, 0 lemmas
% 45.81/46.06 54 : guesser 259, 257, ( | 1, 2, 0 ), 3, 30s old, 0 lemmas
% 45.81/46.06 55 : guesser 260, 258, ( | 1, 2, 0 ), 3, 30s old, 0 lemmas
% 45.81/46.06 56 : guesser 267, 265, ( | 0, 2, 1 ), 3, 30s old, 0 lemmas
% 45.81/46.06 57 : guesser 268, 266, ( | 1, 2, 0 ), 3, 30s old, 0 lemmas
% 45.81/46.06 58 : guesser 275, 273, ( | 0, 2, 1 ), 3, 30s old, 0 lemmas
% 45.81/46.06 59 : guesser 276, 274, ( | 1, 2, 0 ), 3, 30s old, 0 lemmas
% 45.81/46.06 60 : guesser 283, 281, ( | 0, 2, 1 ), 3, 30s old, 0 lemmas
% 45.81/46.06 61 : guesser 284, 282, ( | 0, 2, 1 ), 3, 30s old, 0 lemmas
% 45.81/46.06 62 : guesser 291, 289, ( | 1, 2, 0 ), 3, 29s old, 0 lemmas
% 45.81/46.06 63 : guesser 292, 290, ( | 0, 2, 1 ), 3, 29s old, 0 lemmas
% 45.81/46.06 64 : guesser 299, 297, ( | 0, 2, 1 ), 3, 29s old, 0 lemmas
% 45.81/46.06 65 : guesser 300, 298, ( | 1, 2, 0 ), 3, 29s old, 0 lemmas
% 45.81/46.06 66 : guesser 307, 305, ( | 1, 2, 0 ), 3, 29s old, 0 lemmas
% 45.81/46.06 67 : guesser 308, 306, ( | 1, 2, 0 ), 3, 29s old, 0 lemmas
% 45.81/46.06 68 : guesser 315, 313, ( | 1, 2, 0 ), 3, 29s old, 0 lemmas
% 45.81/46.06 69 : guesser 316, 314, ( | 0, 2, 1 ), 3, 29s old, 0 lemmas
% 45.81/46.06 70 : guesser 323, 321, ( | 1, 2, 0 ), 3, 28s old, 0 lemmas
% 45.81/46.06 71 : guesser 324, 322, ( | 1, 2, 0 ), 3, 28s old, 0 lemmas
% 45.81/46.06 72 : guesser 331, 329, ( | 1, 2, 0 ), 3, 28s old, 0 lemmas
% 45.81/46.06 73 : guesser 332, 330, ( | 1, 2, 0 ), 3, 28s old, 0 lemmas
% 45.81/46.06 74 : guesser 339, 337, ( | 0, 2, 1 ), 3, 28s old, 0 lemmas
% 45.81/46.06 75 : guesser 340, 338, ( | 1, 2, 0 ), 3, 28s old, 0 lemmas
% 45.81/46.06 76 : guesser 347, 345, ( | 1, 2, 0 ), 3, 28s old, 0 lemmas
% 45.81/46.06 77 : guesser 348, 346, ( | 1, 2, 0 ), 3, 28s old, 0 lemmas
% 45.81/46.06 78 : guesser 355, 353, ( | 0, 2, 1 ), 3, 27s old, 0 lemmas
% 45.81/46.06 79 : guesser 356, 354, ( | 0, 1 ), 3, 27s old, 0 lemmas
% 45.81/46.06 80 : guesser 357, 355, ( | 1, 2, 0 ), 3, 27s old, 0 lemmas
% 45.81/46.06 81 : guesser 366, 364, ( | 0, 1 ), 5, 22s old, 0 lemmas
% 45.81/46.06 82 : guesser 367, 365, ( | 0, 2, 1 ), 5, 22s old, 0 lemmas
% 45.81/46.06 83 : guesser 368, 366, ( | 0, 2, 1 ), 5, 22s old, 0 lemmas
% 45.81/46.06 84 : guesser 375, 373, ( | 1, 2, 0 ), 5, 22s old, 0 lemmas
% 45.81/46.06 85 : guesser 376, 374, ( | 1, 2, 0 ), 5, 22s old, 0 lemmas
% 45.81/46.06 86 : guesser 383, 381, ( | 0, 2, 1 ), 5, 21s old, 0 lemmas
% 45.81/46.06 87 : guesser 384, 382, ( | 1, 2, 0 ), 5, 21s old, 0 lemmas
% 45.81/46.06 88 : guesser 391, 389, ( | 0, 2, 1 ), 5, 21s old, 0 lemmas
% 45.81/46.06 89 : guesser 392, 390, ( | 0, 2, 1 ), 5, 21s old, 0 lemmas
% 45.81/46.06 90 : guesser 399, 397, ( | 1, 2, 0 ), 5, 21s old, 0 lemmas
% 45.81/46.06 91 : guesser 400, 398, ( | 1, 2, 0 ), 5, 21s old, 0 lemmas
% 45.81/46.06 92 : guesser 407, 405, ( | 1, 2, 0 ), 5, 21s old, 0 lemmas
% 45.81/46.06 93 : guesser 408, 406, ( | 0, 2, 1 ), 5, 21s old, 0 lemmas
% 45.81/46.06 94 : guesser 415, 413, ( | 1, 2, 0 ), 5, 21s old, 0 lemmas
% 45.81/46.06 95 : guesser 416, 414, ( | 1, 2, 0 ), 5, 21s old, 0 lemmas
% 45.81/46.06 96 : guesser 423, 421, ( | 1, 2, 0 ), 5, 20s old, 0 lemmas
% 45.81/46.06 97 : guesser 424, 422, ( | 1, 2, 0 ), 5, 20s old, 0 lemmas
% 45.81/46.06 98 : guesser 431, 429, ( | 1, 2, 0 ), 5, 20s old, 0 lemmas
% 45.81/46.06 99 : guesser 432, 430, ( | 1, 2, 0 ), 5, 20s old, 0 lemmas
% 45.81/46.06 100 : guesser 439, 437, ( | 0, 2, 1 ), 5, 20s old, 0 lemmas
% 45.81/46.06 101 : guesser 440, 438, ( | 1, 2, 0 ), 5, 20s old, 0 lemmas
% 45.81/46.06 102 : guesser 447, 445, ( | 1, 2, 0 ), 5, 20s old, 0 lemmas
% 45.81/46.06 103 : guesser 454, 452, ( | 0, 2, 1 ), 5, 19s old, 0 lemmas
% 45.81/46.06 104 : guesser 455, 453, ( | 0, 2, 1 ), 5, 19s old, 0 lemmas
% 45.81/46.06 105 : guesser 456, 454, ( | 1, 2, 0 ), 5, 19s old, 0 lemmas
% 45.81/46.06 106 : guesser 465, 463, ( | 1, 2, 0 ), 5, 19s old, 0 lemmas
% 45.81/46.06 107 : guesser 466, 464, ( | 1, 2, 0 ), 5, 19s old, 0 lemmas
% 45.81/46.06 108 : guesser 473, 471, ( | 0, 2, 1 ), 5, 19s old, 0 lemmas
% 45.81/46.06 109 : guesser 474, 472, ( | 1, 2, 0 ), 5, 19s old, 0 lemmas
% 45.81/46.06 110 : guesser 481, 479, ( | 1, 2, 0 ), 5, 19s old, 0 lemmas
% 45.81/46.06 111 : guesser 482, 480, ( | 0, 2, 1 ), 5, 19s old, 0 lemmas
% 45.81/46.06 112 : guesser 489, 487, ( | 1, 2, 0 ), 5, 19s old, 0 lemmas
% 45.81/46.06 113 : guesser 490, 488, ( | 0, 2, 1 ), 5, 19s old, 0 lemmas
% 45.81/46.06 114 : guesser 497, 495, ( | 0, 2, 1 ), 5, 18s old, 0 lemmas
% 45.81/46.06 115 : guesser 498, 496, ( | 0, 2, 1 ), 5, 18s old, 0 lemmas
% 45.81/46.06 116 : guesser 505, 503, ( | 0, 2, 1 ), 5, 18s old, 0 lemmas
% 45.81/46.06 117 : guesser 506, 504, ( | 1, 2, 0 ), 5, 18s old, 0 lemmas
% 45.81/46.06 118 : guesser 513, 511, ( | 0, 2, 1 ), 5, 18s old, 0 lemmas
% 45.81/46.06 119 : guesser 514, 512, ( | 1, 2, 0 ), 5, 18s old, 0 lemmas
% 45.81/46.06 120 : guesser 521, 519, ( | 1, 2, 0 ), 5, 18s old, 0 lemmas
% 45.81/46.06 121 : guesser 522, 520, ( | 1, 2, 0 ), 5, 18s old, 0 lemmas
% 45.81/46.06 122 : guesser 529, 527, ( | 1, 2, 0 ), 5, 17s old, 0 lemmas
% 45.81/46.06 123 : guesser 530, 528, ( | 1, 2, 0 ), 5, 17s old, 0 lemmas
% 45.81/46.06 124 : guesser 537, 535, ( | 0, 2, 1 ), 5, 17s old, 0 lemmas
% 45.81/46.06 125 : guesser 538, 536, ( | 1, 2, 0 ), 5, 17s old, 0 lemmas
% 45.81/46.06 126 : guesser 547, 545, ( | 1, 2, 0 ), 6, 15s old, 0 lemmas
% 45.81/46.06 127 : guesser 548, 546, ( | 0, 2, 1 ), 6, 15s old, 0 lemmas
% 45.81/46.06 128 : guesser 555, 553, ( | 0, 2, 1 ), 6, 15s old, 0 lemmas
% 45.81/46.06 129 : guesser 556, 554, ( | 1, 2, 0 ), 6, 15s old, 0 lemmas
% 45.81/46.06 130 : guesser 563, 561, ( | 0, 2, 1 ), 6, 15s old, 0 lemmas
% 45.81/46.06 131 : guesser 564, 562, ( | 1, 2, 0 ), 6, 15s old, 0 lemmas
% 45.81/46.06 132 : guesser 571, 569, ( | 1, 2, 0 ), 6, 15s old, 0 lemmas
% 45.81/46.06 133 : guesser 572, 570, ( | 0, 2, 1 ), 6, 15s old, 0 lemmas
% 45.81/46.06 134 : guesser 579, 577, ( | 0, 2, 1 ), 6, 14s old, 0 lemmas
% 45.81/46.06 135 : guesser 580, 578, ( | 0, 2, 1 ), 6, 14s old, 0 lemmas
% 45.81/46.06 136 : guesser 587, 585, ( | 1, 2, 0 ), 6, 14s old, 0 lemmas
% 45.81/46.06 137 : guesser 588, 586, ( | 1, 2, 0 ), 6, 14s old, 0 lemmas
% 45.81/46.06 138 : guesser 595, 593, ( | 0, 2, 1 ), 6, 14s old, 0 lemmas
% 45.81/46.06 139 : guesser 596, 594, ( | 0, 2, 1 ), 6, 14s old, 0 lemmas
% 45.81/46.06 140 : guesser 603, 601, ( | 1, 2, 0 ), 6, 14s old, 0 lemmas
% 45.81/46.06 141 : guesser 604, 602, ( | 1, 2, 0 ), 6, 14s old, 0 lemmas
% 45.81/46.06 142 : guesser 611, 609, ( | 0, 2, 1 ), 6, 13s old, 0 lemmas
% 45.81/46.06 143 : guesser 612, 610, ( | 0, 2, 1 ), 6, 13s old, 0 lemmas
% 45.81/46.06 144 : guesser 621, 619, ( | 1, 2, 0 ), 7, 12s old, 0 lemmas
% 45.81/46.06 145 : guesser 622, 620, ( | 0, 2, 1 ), 7, 12s old, 0 lemmas
% 45.81/46.06 146 : guesser 629, 627, ( | 1, 2, 0 ), 7, 12s old, 0 lemmas
% 45.81/46.06 147 : guesser 630, 628, ( | 0, 2, 1 ), 7, 12s old, 0 lemmas
% 45.81/46.06 148 : guesser 637, 635, ( | 1, 2, 0 ), 7, 11s old, 0 lemmas
% 45.81/46.06 149 : guesser 638, 636, ( | 1, 2, 0 ), 7, 11s old, 0 lemmas
% 45.81/46.06 150 : guesser 645, 643, ( | 0, 2, 1 ), 7, 11s old, 0 lemmas
% 45.81/46.06 151 : guesser 646, 644, ( | 0, 2, 1 ), 7, 11s old, 0 lemmas
% 45.81/46.06 152 : guesser 653, 651, ( | 0, 2, 1 ), 7, 11s old, 0 lemmas
% 45.81/46.06 153 : guesser 654, 652, ( | 0, 2, 1 ), 7, 11s old, 0 lemmas
% 45.81/46.06 154 : guesser 661, 659, ( | 0, 2, 1 ), 7, 11s old, 0 lemmas
% 45.81/46.06 155 : guesser 662, 660, ( | 0, 2, 1 ), 7, 11s old, 0 lemmas
% 45.81/46.06 156 : guesser 669, 667, ( | 1, 2, 0 ), 7, 10s old, 0 lemmas
% 45.81/46.06 157 : guesser 670, 668, ( | 0, 2, 1 ), 7, 10s old, 0 lemmas
% 45.81/46.06 158 : guesser 677, 675, ( | 0, 2, 1 ), 7, 10s old, 0 lemmas
% 45.81/46.06 159 : guesser 678, 676, ( | 1, 2, 0 ), 7, 10s old, 0 lemmas
% 45.81/46.06 160 : guesser 687, 685, ( | 0, 2, 1 ), 8, 9s old, 0 lemmas
% 45.81/46.06 161 : guesser 688, 686, ( | 1, 2, 0 ), 8, 9s old, 0 lemmas
% 45.81/46.06 162 : guesser 695, 693, ( | 1, 2, 0 ), 8, 9s old, 0 lemmas
% 45.81/46.06 163 : guesser 696, 694, ( | 1, 2, 0 ), 8, 9s old, 0 lemmas
% 45.81/46.06 164 : guesser 703, 701, ( | 0, 2, 1 ), 8, 8s old, 0 lemmas
% 45.81/46.06 165 : guesser 704, 702, ( | 0, 2, 1 ), 8, 8s old, 0 lemmas
% 45.81/46.06 166 : guesser 711, 709, ( | 1, 2, 0 ), 8, 8s old, 0 lemmas
% 45.81/46.06 167 : guesser 712, 710, ( | 0, 2, 1 ), 8, 8s old, 0 lemmas
% 45.81/46.06 168 : guesser 719, 717, ( | 1, 2, 0 ), 8, 8s old, 0 lemmas
% 45.81/46.06 169 : guesser 720, 718, ( | 1, 2, 0 ), 8, 8s old, 0 lemmas
% 45.81/46.06 170 : guesser 727, 725, ( | 0, 2, 1 ), 8, 8s old, 0 lemmas
% 45.81/46.06 171 : guesser 728, 726, ( | 0, 2, 1 ), 8, 8s old, 0 lemmas
% 45.81/46.06 172 : guesser 735, 733, ( | 1, 2, 0 ), 8, 7s old, 0 lemmas
% 45.81/46.06 173 : guesser 736, 734, ( | 1, 2, 0 ), 8, 7s old, 0 lemmas
% 45.81/46.06 174 : guesser 745, 743, ( | 0, 2, 1 ), 9, 6s old, 0 lemmas
% 45.81/46.06 175 : guesser 746, 744, ( | 1, 2, 0 ), 9, 6s old, 0 lemmas
% 45.81/46.06 176 : guesser 753, 751, ( | 0, 2, 1 ), 9, 6s old, 0 lemmas
% 45.81/46.06 177 : guesser 754, 752, ( | 0, 2, 1 ), 9, 6s old, 0 lemmas
% 45.81/46.06 178 : guesser 761, 759, ( | 0, 2, 1 ), 9, 6s old, 0 lemmas
% 45.81/46.06 179 : guesser 762, 760, ( | 1, 2, 0 ), 9, 6s old, 0 lemmas
% 45.81/46.06 180 : guesser 769, 767, ( | 0, 2, 1 ), 9, 5s old, 0 lemmas
% 45.81/46.06 181 : guesser 770, 768, ( | 1, 2, 0 ), 9, 5s old, 0 lemmas
% 45.81/46.06 182 : guesser 777, 775, ( | 0, 2, 1 ), 9, 5s old, 0 lemmas
% 45.81/46.06 183 : guesser 778, 776, ( | 1, 2, 0 ), 9, 5s old, 0 lemmas
% 45.81/46.06 184 : guesser 785, 783, ( | 0, 2, 1 ), 9, 5s old, 0 lemmas
% 45.81/46.06 185 : guesser 786, 784, ( | 0, 2, 1 ), 9, 5s old, 0 lemmas
% 45.81/46.06 186 : guesser 795, 793, ( | 0, 2, 1 ), 10, 4s old, 0 lemmas
% 45.81/46.06 187 : guesser 796, 794, ( | 1, 2, 0 ), 10, 4s old, 0 lemmas
% 45.81/46.06 188 : guesser 803, 801, ( | 0, 2, 1 ), 10, 4s old, 0 lemmas
% 45.81/46.06 189 : guesser 804, 802, ( | 0, 2, 1 ), 10, 4s old, 0 lemmas
% 45.81/46.06 190 : guesser 811, 809, ( | 1, 2, 0 ), 10, 4s old, 0 lemmas
% 45.81/46.06 191 : guesser 812, 810, ( | 1, 2, 0 ), 10, 4s old, 0 lemmas
% 45.81/46.06 192 : guesser 819, 817, ( | 1, 2, 0 ), 10, 3s old, 0 lemmas
% 45.81/46.06 193 : guesser 820, 818, ( | 1, 2, 0 ), 10, 3s old, 0 lemmas
% 45.81/46.06 194 : guesser 827, 825, ( | 0, 2, 1 ), 10, 3s old, 0 lemmas
% 45.81/46.06 195 : guesser 828, 826, ( | 0, 2, 1 ), 10, 3s old, 0 lemmas
% 45.81/46.06 196 : guesser 837, 835, ( | 1, 2, 0 ), 11, 2s old, 0 lemmas
% 45.81/46.06 197 : guesser 838, 836, ( | 1, 2, 0 ), 11, 2s old, 0 lemmas
% 45.81/46.06 198 : guesser 845, 843, ( | 1, 2, 0 ), 11, 2s old, 0 lemmas
% 45.81/46.06 199 : guesser 846, 844, ( | 1, 2, 0 ), 11, 2s old, 0 lemmas
% 45.81/46.06 200 : guesser 853, 851, ( | 1, 2, 0 ), 11, 2s old, 0 lemmas
% 45.81/46.06 201 : guesser 854, 852, ( | 1, 2, 0 ), 11, 2s old, 0 lemmas
% 45.81/46.06 202 : guesser 861, 859, ( | 1, 2, 0 ), 11, 1s old, 0 lemmas
% 45.81/46.06 203 : guesser 862, 860, ( | 0, 2, 1 ), 11, 1s old, 0 lemmas
% 45.81/46.06 204 : guesser 871, 869, ( | 1, 2, 0 ), 12, 1s old, 0 lemmas
% 45.81/46.06 205 : guesser 872, 870, ( | 1, 2, 0 ), 12, 1s old, 0 lemmas
% 45.81/46.06 206 : guesser 879, 877, ( | 1, 2, 0 ), 12, 0s old, 0 lemmas
% 45.81/46.06 207 : guesser 880, 878, ( | 0, 2, 1 ), 12, 0s old, 0 lemmas
% 45.81/46.06 208 : guesser 887, 885, ( | 1, 2, 0 ), 12, 0s old, 0 lemmas
% 45.81/46.06 209 : guesser 888, 886, ( | 1, 2, 0 ), 12, 0s old, 0 lemmas
% 45.81/46.06 210 : guesser 895, 893, ( | 1, 2, 0 ), 12, 0s old, 0 lemmas
% 45.81/46.06 211 : guesser 896, 894, ( | 0, 1 ), 12, 0s old, 0 lemmas
% 45.81/46.06 212 : guesser 897, 895, ( | 0, 1 ), 12, 0s old, 0 lemmas
% 45.81/46.06 213 : guesser 898, 896, ( | 1, 2, 0 ), 12, 0s old, 0 lemmas
% 45.81/46.06 214 : guesser 905, 903, ( | 0, 2, 1 ), 12, 0s old, 0 lemmas
% 45.81/46.06
% 45.81/46.06 Elements:
% 45.81/46.06 { E0, E1 }
% 45.81/46.06
% 45.81/46.06 Atoms:
% 45.81/46.06 0 : #-{T} E0 { }
% 45.81/46.06 1 : r1-{T}(E0,E0) { }
% 45.81/46.06 2 : #-{T} E1 { 0 }
% 45.81/46.06 3 : pppp436-{T}(E1) { 0 }
% 45.81/46.06 4 : r1-{T}(E1,E1) { 0 }
% 45.81/46.06 5 : pppp435-{T}(E1) { 0 }
% 45.81/46.06 6 : pppp374-{T}(E1) { 0 }
% 45.81/46.06 7 : pppp250-{T}(E1) { 0 }
% 45.81/46.06 8 : pppp58-{T}(E1) { 0 }
% 45.81/46.06 9 : pppp349-{T}(E1) { 0 }
% 45.81/46.06 10 : pppp208-{T}(E1) { 0 }
% 45.81/46.06 11 : pppp320-{T}(E1) { 0 }
% 45.81/46.06 12 : pppp162-{T}(E1) { 0 }
% 45.81/46.06 13 : pppp287-{T}(E1) { 0 }
% 45.81/46.06 14 : pppp112-{T}(E1) { 0 }
% 45.81/46.06 15 : pppp249-{T}(E1) { 0 }
% 45.81/46.06 16 : pppp207-{T}(E1) { 0 }
% 45.81/46.06 17 : pppp161-{T}(E1) { 0 }
% 45.81/46.06 18 : pppp111-{T}(E1) { 0 }
% 45.81/46.06 19 : pppp57-{T}(E1) { 0 }
% 45.81/46.06 20 : pppp56-{T}(E1) { 0 }
% 45.81/46.06 21 : pppp437-{T}(E1) { 0 }
% 45.81/46.06 22 : pppp434-{T}(E0,E1) { 0, 1 }
% 45.81/46.06 23 : r1-{T}(E1,E0) { 0, 1 }
% 45.81/46.06 24 : pppp433-{T}(E0) { 0, 1 }
% 45.81/46.06 25 : pppp374-{T}(E0) { 0, 1 }
% 45.81/46.06 26 : pppp250-{T}(E0) { 0, 1 }
% 45.81/46.06 27 : pppp58-{T}(E0) { 0, 1 }
% 45.81/46.06 28 : pppp437-{T}(E0) { 0, 1 }
% 45.81/46.06 29 : pppp349-{T}(E0) { 0, 1 }
% 45.81/46.06 30 : pppp208-{T}(E0) { 0, 1 }
% 45.81/46.06 31 : pppp320-{T}(E0) { 0, 1 }
% 45.81/46.06 32 : pppp162-{T}(E0) { 0, 1 }
% 45.81/46.06 33 : pppp287-{T}(E0) { 0, 1 }
% 45.81/46.06 34 : pppp112-{T}(E0) { 0, 1 }
% 45.81/46.06 35 : pppp432-{T}(E0) { 0, 1 }
% 45.81/46.06 36 : pppp249-{T}(E0) { 0, 1 }
% 45.81/46.06 37 : pppp431-{T}(E0) { 0, 1 }
% 45.81/46.06 38 : pppp207-{T}(E0) { 0, 1 }
% 45.81/46.06 39 : pppp161-{T}(E0) { 0, 1 }
% 45.81/46.06 40 : pppp111-{T}(E0) { 0, 1 }
% 45.81/46.06 41 : pppp57-{T}(E0) { 0, 1 }
% 45.81/46.06 42 : pppp56-{T}(E0) { 0, 1 }
% 45.81/46.06 43 : pppp430-{T}(E0,E1) { 0, 2 }
% 45.81/46.06 44 : pppp429-{T}(E0) { 0, 2 }
% 45.81/46.06 45 : pppp428-{T}(E0) { 0, 2 }
% 45.81/46.06 46 : pppp427-{T}(E0) { 0, 2 }
% 45.81/46.06 47 : pppp438-{T}(E0) { 0, 1, 2 }
% 45.81/46.06 48 : pppp422-{T}(E1,E0) { 0, 3 }
% 45.81/46.06 49 : pppp421-{T}(E0) { 0, 3 }
% 45.81/46.06 50 : pppp420-{T}(E0) { 0, 3 }
% 45.81/46.06 51 : pppp419-{T}(E0) { 0, 3 }
% 45.81/46.06 52 : pppp410-{T}(E1,E1) { 0, 4 }
% 45.81/46.06 53 : pppp409-{T}(E1) { 0, 4 }
% 45.81/46.06 54 : pppp408-{T}(E1) { 0, 4 }
% 45.81/46.06 55 : pppp409-{T}(E0) { 0, 1, 4 }
% 45.81/46.06 56 : pppp407-{T}(E1) { 0, 4 }
% 45.81/46.06 57 : pppp408-{T}(E0) { 0, 1, 4 }
% 45.81/46.06 58 : pppp407-{T}(E0) { 0, 1, 4 }
% 45.81/46.06 59 : pppp394-{T}(E1,E0) { 0, 5 }
% 45.81/46.06 60 : pppp393-{T}(E0) { 0, 5 }
% 45.81/46.06 61 : pppp392-{T}(E0) { 0, 5 }
% 45.81/46.06 62 : pppp391-{T}(E0) { 0, 5 }
% 45.81/46.06 63 : pppp373-{T}(E0,E1) { 0, 6 }
% 45.81/46.06 64 : pppp372-{T}(E0) { 0, 6 }
% 45.81/46.06 65 : pppp371-{T}(E0) { 0, 6 }
% 45.81/46.06 66 : pppp370-{T}(E0) { 0, 6 }
% 45.81/46.06 67 : pppp348-{T}(E1,E1) { 0, 7 }
% 45.81/46.06 68 : pppp347-{T}(E1) { 0, 7 }
% 45.81/46.06 69 : pppp346-{T}(E1) { 0, 7 }
% 45.81/46.06 70 : pppp347-{T}(E0) { 0, 1, 7 }
% 45.81/46.06 71 : pppp345-{T}(E1) { 0, 7 }
% 45.81/46.06 72 : pppp346-{T}(E0) { 0, 1, 7 }
% 45.81/46.06 73 : pppp345-{T}(E0) { 0, 1, 7 }
% 45.81/46.06 74 : pppp319-{T}(E1,E1) { 0, 8 }
% 45.81/46.06 75 : pppp318-{T}(E1) { 0, 8 }
% 45.81/46.06 76 : pppp317-{T}(E1) { 0, 8 }
% 45.81/46.06 77 : pppp318-{T}(E0) { 0, 1, 8 }
% 45.81/46.06 78 : pppp316-{T}(E1) { 0, 8 }
% 45.81/46.06 79 : pppp317-{T}(E0) { 0, 1, 8 }
% 45.81/46.06 80 : pppp316-{T}(E0) { 0, 1, 8 }
% 45.81/46.06 81 : pppp286-{T}(E1,E1) { 0, 9 }
% 45.81/46.06 82 : pppp285-{T}(E1) { 0, 9 }
% 45.81/46.06 83 : pppp284-{T}(E1) { 0, 9 }
% 45.81/46.06 84 : pppp285-{T}(E0) { 0, 1, 9 }
% 45.81/46.06 85 : pppp283-{T}(E1) { 0, 9 }
% 45.81/46.06 86 : pppp284-{T}(E0) { 0, 1, 9 }
% 45.81/46.06 87 : pppp283-{T}(E0) { 0, 1, 9 }
% 45.81/46.06 88 : pppp248-{T}(E0,E1) { 0, 10 }
% 45.81/46.06 89 : pppp247-{T}(E0) { 0, 10 }
% 45.81/46.06 90 : pppp246-{T}(E0) { 0, 10 }
% 45.81/46.06 91 : pppp245-{T}(E0) { 0, 10 }
% 45.81/46.06 92 : pppp206-{T}(E1,E0) { 0, 11 }
% 45.81/46.06 93 : pppp205-{T}(E0) { 0, 11 }
% 45.81/46.06 94 : pppp204-{T}(E0) { 0, 11 }
% 45.81/46.06 95 : pppp203-{T}(E0) { 0, 11 }
% 45.81/46.06 96 : pppp160-{T}(E1,E1) { 0, 12 }
% 45.81/46.06 97 : pppp159-{T}(E1) { 0, 12 }
% 45.81/46.06 98 : pppp158-{T}(E1) { 0, 12 }
% 45.81/46.06 99 : pppp159-{T}(E0) { 0, 1, 12 }
% 45.81/46.06 100 : pppp157-{T}(E1) { 0, 12 }
% 45.81/46.06 101 : pppp158-{T}(E0) { 0, 1, 12 }
% 45.81/46.06 102 : pppp157-{T}(E0) { 0, 1, 12 }
% 45.81/46.06 103 : pppp110-{T}(E1,E0) { 0, 13 }
% 45.81/46.06 104 : pppp109-{T}(E0) { 0, 13 }
% 45.81/46.06 105 : pppp108-{T}(E0) { 0, 13 }
% 45.81/46.06 106 : pppp107-{T}(E0) { 0, 13 }
% 45.81/46.06 107 : pppp55-{T}(E0,E1) { 0, 14 }
% 45.81/46.06 108 : pppp54-{T}(E0) { 0, 14 }
% 45.81/46.06 109 : pppp53-{T}(E0) { 0, 14 }
% 45.81/46.06 110 : pppp52-{T}(E0) { 0, 14 }
% 45.81/46.06 111 : pppp434-{T}(E1,E0) { 0, 1, 15 }
% 45.81/46.06 112 : r1-{T}(E0,E1) { 0, 1, 15 }
% 45.81/46.06 113 : pppp433-{T}(E1) { 0, 1, 15 }
% 45.81/46.06 114 : pppp432-{T}(E1) { 0, 1, 15 }
% 45.81/46.06 115 : pppp431-{T}(E1) { 0, 1, 15 }
% 45.81/46.06 116 : pppp429-{T}(E1) { 0, 1, 2, 15 }
% 45.81/46.06 117 : pppp428-{T}(E1) { 0, 1, 2, 15 }
% 45.81/46.06 118 : pppp427-{T}(E1) { 0, 1, 2, 15 }
% 45.81/46.06 119 : pppp438-{T}(E1) { 0, 1, 2, 15 }
% 45.81/46.06 120 : pppp421-{T}(E1) { 0, 1, 3, 15 }
% 45.81/46.06 121 : pppp420-{T}(E1) { 0, 1, 3, 15 }
% 45.81/46.06 122 : pppp419-{T}(E1) { 0, 1, 3, 15 }
% 45.81/46.06 123 : pppp393-{T}(E1) { 0, 1, 5, 15 }
% 45.81/46.06 124 : pppp392-{T}(E1) { 0, 1, 5, 15 }
% 45.81/46.06 125 : pppp391-{T}(E1) { 0, 1, 5, 15 }
% 45.81/46.06 126 : pppp372-{T}(E1) { 0, 1, 6, 15 }
% 45.81/46.06 127 : pppp371-{T}(E1) { 0, 1, 6, 15 }
% 45.81/46.06 128 : pppp370-{T}(E1) { 0, 1, 6, 15 }
% 45.81/46.06 129 : pppp247-{T}(E1) { 0, 1, 10, 15 }
% 45.81/46.06 130 : pppp246-{T}(E1) { 0, 1, 10, 15 }
% 45.81/46.06 131 : pppp245-{T}(E1) { 0, 1, 10, 15 }
% 45.81/46.06 132 : pppp205-{T}(E1) { 0, 1, 11, 15 }
% 45.81/46.06 133 : pppp204-{T}(E1) { 0, 1, 11, 15 }
% 45.81/46.06 134 : pppp203-{T}(E1) { 0, 1, 11, 15 }
% 45.81/46.06 135 : pppp109-{T}(E1) { 0, 1, 13, 15 }
% 45.81/46.06 136 : pppp108-{T}(E1) { 0, 1, 13, 15 }
% 45.81/46.06 137 : pppp107-{T}(E1) { 0, 1, 13, 15 }
% 45.81/46.06 138 : pppp54-{T}(E1) { 0, 1, 14, 15 }
% 45.81/46.06 139 : pppp53-{T}(E1) { 0, 1, 14, 15 }
% 45.81/46.06 140 : pppp52-{T}(E1) { 0, 1, 14, 15 }
% 45.81/46.06 141 : pppp430-{T}(E1,E0) { 0, 1, 16 }
% 45.81/46.06 142 : pppp422-{T}(E0,E1) { 0, 1, 17 }
% 45.81/46.06 143 : pppp410-{T}(E0,E0) { 0, 1, 18 }
% 45.81/46.06 144 : pppp394-{T}(E0,E1) { 0, 1, 19 }
% 45.81/46.06 145 : pppp373-{T}(E0,E0) { 0, 1, 20 }
% 45.81/46.06 146 : pppp348-{T}(E0,E1) { 0, 1, 21 }
% 45.81/46.06 147 : pppp319-{T}(E0,E0) { 0, 1, 22 }
% 45.81/46.06 148 : pppp286-{T}(E0,E0) { 0, 1, 23 }
% 45.81/46.06 149 : pppp248-{T}(E0,E0) { 0, 1, 24 }
% 45.81/46.06 150 : pppp206-{T}(E0,E1) { 0, 1, 25 }
% 45.81/46.06 151 : pppp160-{T}(E1,E0) { 0, 1, 26 }
% 45.81/46.06 152 : pppp110-{T}(E0,E0) { 0, 1, 27 }
% 45.81/46.06 153 : pppp55-{T}(E0,E0) { 0, 1, 28 }
% 45.81/46.06 154 : pppp426-{T}(E0,E0) { 0, 1, 2, 29 }
% 45.81/46.06 155 : pppp425-{T}(E0) { 0, 1, 2, 29 }
% 45.81/46.06 156 : pppp424-{T}(E0) { 0, 1, 2, 29 }
% 45.81/46.06 157 : pppp425-{T}(E1) { 0, 1, 2, 15, 29 }
% 45.81/46.06 158 : pppp423-{T}(E0) { 0, 1, 2, 29 }
% 45.81/46.06 159 : pppp424-{T}(E1) { 0, 1, 2, 15, 29 }
% 45.81/46.06 160 : pppp423-{T}(E1) { 0, 1, 2, 15, 29 }
% 45.81/46.06 161 : pppp418-{T}(E0,E1) { 0, 3, 30 }
% 45.81/46.06 162 : pppp417-{T}(E1) { 0, 3, 30 }
% 45.81/46.06 163 : pppp416-{T}(E1) { 0, 3, 30 }
% 45.81/46.06 164 : pppp417-{T}(E0) { 0, 1, 3, 30 }
% 45.81/46.06 165 : pppp415-{T}(E1) { 0, 3, 30 }
% 45.81/46.06 166 : pppp416-{T}(E0) { 0, 1, 3, 30 }
% 45.81/46.06 167 : pppp415-{T}(E0) { 0, 1, 3, 30 }
% 45.81/46.06 168 : pppp439-{T}(E1) { 0, 3, 30 }
% 45.81/46.06 169 : pppp439-{T}(E0) { 0, 1, 3, 30 }
% 45.81/46.06 170 : pppp406-{T}(E1,E1) { 0, 4, 31 }
% 45.81/46.06 171 : pppp405-{T}(E1) { 0, 4, 31 }
% 45.81/46.06 172 : pppp404-{T}(E1) { 0, 4, 31 }
% 45.81/46.06 173 : pppp405-{T}(E0) { 0, 1, 4, 31 }
% 45.81/46.06 174 : pppp403-{T}(E1) { 0, 4, 31 }
% 45.81/46.06 175 : pppp404-{T}(E0) { 0, 1, 4, 31 }
% 45.81/46.06 176 : pppp403-{T}(E0) { 0, 1, 4, 31 }
% 45.81/46.06 177 : pppp406-{T}(E1,E0) { 0, 1, 4, 32 }
% 45.81/46.06 178 : pppp390-{T}(E0,E0) { 0, 5, 33 }
% 45.81/46.06 179 : pppp389-{T}(E0) { 0, 5, 33 }
% 45.81/46.06 180 : pppp388-{T}(E0) { 0, 5, 33 }
% 45.81/46.06 181 : pppp389-{T}(E1) { 0, 1, 5, 15, 33 }
% 45.81/46.06 182 : pppp387-{T}(E0) { 0, 5, 33 }
% 45.81/46.06 183 : pppp388-{T}(E1) { 0, 1, 5, 15, 33 }
% 45.81/46.06 184 : pppp387-{T}(E1) { 0, 1, 5, 15, 33 }
% 45.81/46.06 185 : pppp369-{T}(E0,E0) { 0, 6, 34 }
% 45.81/46.06 186 : pppp368-{T}(E0) { 0, 6, 34 }
% 45.81/46.06 187 : pppp367-{T}(E0) { 0, 6, 34 }
% 45.81/46.06 188 : pppp368-{T}(E1) { 0, 1, 6, 15, 34 }
% 45.81/46.06 189 : pppp366-{T}(E0) { 0, 6, 34 }
% 45.81/46.06 190 : pppp367-{T}(E1) { 0, 1, 6, 15, 34 }
% 45.81/46.06 191 : pppp366-{T}(E1) { 0, 1, 6, 15, 34 }
% 45.81/46.06 192 : pppp344-{T}(E1,E1) { 0, 7, 35 }
% 45.81/46.06 193 : pppp343-{T}(E1) { 0, 7, 35 }
% 45.81/46.06 194 : pppp342-{T}(E1) { 0, 7, 35 }
% 45.81/46.06 195 : pppp343-{T}(E0) { 0, 1, 7, 35 }
% 45.81/46.06 196 : pppp341-{T}(E1) { 0, 7, 35 }
% 45.81/46.06 197 : pppp342-{T}(E0) { 0, 1, 7, 35 }
% 45.81/46.06 198 : pppp341-{T}(E0) { 0, 1, 7, 35 }
% 45.81/46.06 199 : pppp344-{T}(E0,E1) { 0, 1, 7, 36 }
% 45.81/46.06 200 : pppp315-{T}(E1,E1) { 0, 8, 37 }
% 45.81/46.06 201 : pppp314-{T}(E1) { 0, 8, 37 }
% 45.81/46.06 202 : pppp313-{T}(E1) { 0, 8, 37 }
% 45.81/46.06 203 : pppp314-{T}(E0) { 0, 1, 8, 37 }
% 45.81/46.06 204 : pppp312-{T}(E1) { 0, 8, 37 }
% 45.81/46.06 205 : pppp313-{T}(E0) { 0, 1, 8, 37 }
% 45.81/46.06 206 : pppp312-{T}(E0) { 0, 1, 8, 37 }
% 45.81/46.06 207 : pppp315-{T}(E0,E0) { 0, 1, 8, 38 }
% 45.81/46.06 208 : pppp282-{T}(E1,E0) { 0, 9, 39 }
% 45.81/46.06 209 : pppp281-{T}(E0) { 0, 9, 39 }
% 45.81/46.06 210 : pppp280-{T}(E0) { 0, 9, 39 }
% 45.81/46.06 211 : pppp281-{T}(E1) { 0, 1, 9, 15, 39 }
% 45.81/46.06 212 : pppp279-{T}(E0) { 0, 9, 39 }
% 45.81/46.06 213 : pppp280-{T}(E1) { 0, 1, 9, 15, 39 }
% 45.81/46.06 214 : pppp279-{T}(E1) { 0, 1, 9, 15, 39 }
% 45.81/46.06 215 : pppp282-{T}(E0,E0) { 0, 1, 9, 40 }
% 45.81/46.06 216 : pppp244-{T}(E1,E0) { 0, 10, 41 }
% 45.81/46.06 217 : pppp243-{T}(E1) { 0, 10, 41 }
% 45.81/46.06 218 : pppp242-{T}(E1) { 0, 10, 41 }
% 45.81/46.06 219 : pppp243-{T}(E0) { 0, 1, 10, 41 }
% 45.81/46.06 220 : pppp241-{T}(E1) { 0, 10, 41 }
% 45.81/46.06 221 : pppp242-{T}(E0) { 0, 1, 10, 41 }
% 45.81/46.06 222 : pppp241-{T}(E0) { 0, 1, 10, 41 }
% 45.81/46.06 223 : pppp202-{T}(E0,E1) { 0, 11, 42 }
% 45.81/46.06 224 : pppp201-{T}(E1) { 0, 11, 42 }
% 45.81/46.06 225 : pppp200-{T}(E1) { 0, 11, 42 }
% 45.81/46.06 226 : pppp201-{T}(E0) { 0, 1, 11, 42 }
% 45.81/46.06 227 : pppp199-{T}(E1) { 0, 11, 42 }
% 45.81/46.06 228 : pppp200-{T}(E0) { 0, 1, 11, 42 }
% 45.81/46.06 229 : pppp199-{T}(E0) { 0, 1, 11, 42 }
% 45.81/46.06 230 : pppp156-{T}(E1,E1) { 0, 12, 43 }
% 45.81/46.06 231 : pppp155-{T}(E1) { 0, 12, 43 }
% 45.81/46.06 232 : pppp154-{T}(E1) { 0, 12, 43 }
% 45.81/46.06 233 : pppp155-{T}(E0) { 0, 1, 12, 43 }
% 45.81/46.06 234 : pppp153-{T}(E1) { 0, 12, 43 }
% 45.81/46.06 235 : pppp154-{T}(E0) { 0, 1, 12, 43 }
% 45.81/46.06 236 : pppp153-{T}(E0) { 0, 1, 12, 43 }
% 45.81/46.06 237 : pppp156-{T}(E1,E0) { 0, 1, 12, 44 }
% 45.81/46.06 238 : pppp106-{T}(E0,E0) { 0, 13, 45 }
% 45.81/46.06 239 : pppp105-{T}(E0) { 0, 13, 45 }
% 45.81/46.06 240 : pppp104-{T}(E0) { 0, 13, 45 }
% 45.81/46.06 241 : pppp105-{T}(E1) { 0, 1, 13, 15, 45 }
% 45.81/46.06 242 : pppp103-{T}(E0) { 0, 13, 45 }
% 45.81/46.06 243 : pppp104-{T}(E1) { 0, 1, 13, 15, 45 }
% 45.81/46.06 244 : pppp103-{T}(E1) { 0, 1, 13, 15, 45 }
% 45.81/46.06 245 : pppp51-{T}(E0,E0) { 0, 14, 46 }
% 45.81/46.06 246 : pppp50-{T}(E0) { 0, 14, 46 }
% 45.81/46.06 247 : pppp49-{T}(E0) { 0, 14, 46 }
% 45.81/46.06 248 : pppp50-{T}(E1) { 0, 1, 14, 15, 46 }
% 45.81/46.06 249 : pppp48-{T}(E0) { 0, 14, 46 }
% 45.81/46.06 250 : pppp49-{T}(E1) { 0, 1, 14, 15, 46 }
% 45.81/46.06 251 : pppp48-{T}(E1) { 0, 1, 14, 15, 46 }
% 45.81/46.06 252 : pppp426-{T}(E1,E0) { 0, 1, 2, 15, 47 }
% 45.81/46.06 253 : pppp418-{T}(E1,E0) { 0, 1, 3, 15, 48 }
% 45.81/46.06 254 : pppp390-{T}(E1,E0) { 0, 1, 5, 15, 49 }
% 45.81/46.06 255 : pppp369-{T}(E1,E1) { 0, 1, 6, 15, 50 }
% 45.81/46.06 256 : pppp244-{T}(E1,E1) { 0, 1, 10, 15, 51 }
% 45.81/46.06 257 : pppp202-{T}(E1,E1) { 0, 1, 11, 15, 52 }
% 45.81/46.06 258 : pppp106-{T}(E1,E1) { 0, 1, 13, 15, 53 }
% 45.81/46.06 259 : pppp51-{T}(E1,E1) { 0, 1, 14, 15, 54 }
% 45.81/46.06 260 : pppp414-{T}(E1,E1) { 0, 3, 30, 55 }
% 45.81/46.06 261 : pppp413-{T}(E1) { 0, 3, 30, 55 }
% 45.81/46.06 262 : pppp412-{T}(E1) { 0, 3, 30, 55 }
% 45.81/46.06 263 : pppp413-{T}(E0) { 0, 1, 3, 30, 55 }
% 45.81/46.06 264 : pppp411-{T}(E1) { 0, 3, 30, 55 }
% 45.81/46.06 265 : pppp412-{T}(E0) { 0, 1, 3, 30, 55 }
% 45.81/46.06 266 : pppp411-{T}(E0) { 0, 1, 3, 30, 55 }
% 45.81/46.06 267 : pppp414-{T}(E0,E0) { 0, 1, 3, 30, 56 }
% 45.81/46.06 268 : pppp402-{T}(E1,E1) { 0, 4, 31, 57 }
% 45.81/46.06 269 : pppp401-{T}(E1) { 0, 4, 31, 57 }
% 45.81/46.06 270 : pppp400-{T}(E1) { 0, 4, 31, 57 }
% 45.81/46.06 271 : pppp401-{T}(E0) { 0, 1, 4, 31, 57 }
% 45.81/46.06 272 : pppp399-{T}(E1) { 0, 4, 31, 57 }
% 45.81/46.06 273 : pppp400-{T}(E0) { 0, 1, 4, 31, 57 }
% 45.81/46.06 274 : pppp399-{T}(E0) { 0, 1, 4, 31, 57 }
% 45.81/46.06 275 : pppp402-{T}(E0,E0) { 0, 1, 4, 31, 58 }
% 45.81/46.06 276 : pppp386-{T}(E0,E1) { 0, 5, 33, 59 }
% 45.81/46.06 277 : pppp385-{T}(E1) { 0, 5, 33, 59 }
% 45.81/46.06 278 : pppp384-{T}(E1) { 0, 5, 33, 59 }
% 45.81/46.06 279 : pppp385-{T}(E0) { 0, 1, 5, 33, 59 }
% 45.81/46.06 280 : pppp383-{T}(E1) { 0, 5, 33, 59 }
% 45.81/46.06 281 : pppp384-{T}(E0) { 0, 1, 5, 33, 59 }
% 45.81/46.06 282 : pppp383-{T}(E0) { 0, 1, 5, 33, 59 }
% 45.81/46.06 283 : pppp386-{T}(E1,E0) { 0, 1, 5, 15, 33, 60 }
% 45.81/46.06 284 : pppp365-{T}(E0,E0) { 0, 6, 34, 61 }
% 45.81/46.06 285 : pppp364-{T}(E0) { 0, 6, 34, 61 }
% 45.81/46.06 286 : pppp363-{T}(E0) { 0, 6, 34, 61 }
% 45.81/46.06 287 : pppp364-{T}(E1) { 0, 1, 6, 15, 34, 61 }
% 45.81/46.06 288 : pppp362-{T}(E0) { 0, 6, 34, 61 }
% 45.81/46.06 289 : pppp363-{T}(E1) { 0, 1, 6, 15, 34, 61 }
% 45.81/46.06 290 : pppp362-{T}(E1) { 0, 1, 6, 15, 34, 61 }
% 45.81/46.06 291 : pppp365-{T}(E1,E1) { 0, 1, 6, 15, 34, 62 }
% 45.81/46.06 292 : pppp340-{T}(E1,E0) { 0, 7, 35, 63 }
% 45.81/46.06 293 : pppp339-{T}(E0) { 0, 7, 35, 63 }
% 45.81/46.06 294 : pppp338-{T}(E0) { 0, 7, 35, 63 }
% 45.81/46.06 295 : pppp339-{T}(E1) { 0, 1, 7, 15, 35, 63 }
% 45.81/46.06 296 : pppp337-{T}(E0) { 0, 7, 35, 63 }
% 45.81/46.06 297 : pppp338-{T}(E1) { 0, 1, 7, 15, 35, 63 }
% 45.81/46.06 298 : pppp337-{T}(E1) { 0, 1, 7, 15, 35, 63 }
% 45.81/46.06 299 : pppp340-{T}(E0,E0) { 0, 1, 7, 35, 64 }
% 45.81/46.06 300 : pppp311-{T}(E1,E1) { 0, 8, 37, 65 }
% 45.81/46.06 301 : pppp310-{T}(E1) { 0, 8, 37, 65 }
% 45.81/46.06 302 : pppp309-{T}(E1) { 0, 8, 37, 65 }
% 45.81/46.06 303 : pppp310-{T}(E0) { 0, 1, 8, 37, 65 }
% 45.81/46.06 304 : pppp308-{T}(E1) { 0, 8, 37, 65 }
% 45.81/46.06 305 : pppp309-{T}(E0) { 0, 1, 8, 37, 65 }
% 45.81/46.06 306 : pppp308-{T}(E0) { 0, 1, 8, 37, 65 }
% 45.81/46.06 307 : pppp311-{T}(E1,E0) { 0, 1, 8, 37, 66 }
% 45.81/46.06 308 : pppp278-{T}(E0,E1) { 0, 9, 39, 67 }
% 45.81/46.06 309 : pppp277-{T}(E1) { 0, 9, 39, 67 }
% 45.81/46.06 310 : pppp276-{T}(E1) { 0, 9, 39, 67 }
% 45.81/46.06 311 : pppp277-{T}(E0) { 0, 1, 9, 39, 67 }
% 45.81/46.06 312 : pppp275-{T}(E1) { 0, 9, 39, 67 }
% 45.81/46.06 313 : pppp276-{T}(E0) { 0, 1, 9, 39, 67 }
% 45.81/46.06 314 : pppp275-{T}(E0) { 0, 1, 9, 39, 67 }
% 45.81/46.06 315 : pppp278-{T}(E1,E1) { 0, 1, 9, 15, 39, 68 }
% 45.81/46.06 316 : pppp240-{T}(E0,E1) { 0, 10, 41, 69 }
% 45.81/46.06 317 : pppp239-{T}(E0) { 0, 10, 41, 69 }
% 45.81/46.06 318 : pppp238-{T}(E0) { 0, 10, 41, 69 }
% 45.81/46.06 319 : pppp239-{T}(E1) { 0, 1, 10, 15, 41, 69 }
% 45.81/46.06 320 : pppp237-{T}(E0) { 0, 10, 41, 69 }
% 45.81/46.06 321 : pppp238-{T}(E1) { 0, 1, 10, 15, 41, 69 }
% 45.81/46.06 322 : pppp237-{T}(E1) { 0, 1, 10, 15, 41, 69 }
% 45.81/46.06 323 : pppp240-{T}(E1,E0) { 0, 1, 10, 41, 70 }
% 45.81/46.06 324 : pppp198-{T}(E1,E1) { 0, 11, 42, 71 }
% 45.81/46.06 325 : pppp197-{T}(E1) { 0, 11, 42, 71 }
% 45.81/46.06 326 : pppp196-{T}(E1) { 0, 11, 42, 71 }
% 45.81/46.06 327 : pppp197-{T}(E0) { 0, 1, 11, 42, 71 }
% 45.81/46.06 328 : pppp195-{T}(E1) { 0, 11, 42, 71 }
% 45.81/46.06 329 : pppp196-{T}(E0) { 0, 1, 11, 42, 71 }
% 45.81/46.06 330 : pppp195-{T}(E0) { 0, 1, 11, 42, 71 }
% 45.81/46.06 331 : pppp198-{T}(E0,E1) { 0, 1, 11, 42, 72 }
% 45.81/46.06 332 : pppp152-{T}(E1,E1) { 0, 12, 43, 73 }
% 45.81/46.06 333 : pppp151-{T}(E1) { 0, 12, 43, 73 }
% 45.81/46.06 334 : pppp150-{T}(E1) { 0, 12, 43, 73 }
% 45.81/46.06 335 : pppp151-{T}(E0) { 0, 1, 12, 43, 73 }
% 45.81/46.06 336 : pppp149-{T}(E1) { 0, 12, 43, 73 }
% 45.81/46.06 337 : pppp150-{T}(E0) { 0, 1, 12, 43, 73 }
% 45.81/46.06 338 : pppp149-{T}(E0) { 0, 1, 12, 43, 73 }
% 45.81/46.06 339 : pppp152-{T}(E0,E0) { 0, 1, 12, 43, 74 }
% 45.81/46.06 340 : pppp102-{T}(E0,E1) { 0, 13, 45, 75 }
% 45.81/46.06 341 : pppp101-{T}(E1) { 0, 13, 45, 75 }
% 45.81/46.06 342 : pppp100-{T}(E1) { 0, 13, 45, 75 }
% 45.81/46.06 343 : pppp101-{T}(E0) { 0, 1, 13, 45, 75 }
% 45.81/46.06 344 : pppp99-{T}(E1) { 0, 13, 45, 75 }
% 45.81/46.06 345 : pppp100-{T}(E0) { 0, 1, 13, 45, 75 }
% 45.81/46.06 346 : pppp99-{T}(E0) { 0, 1, 13, 45, 75 }
% 45.81/46.06 347 : pppp102-{T}(E1,E1) { 0, 1, 13, 15, 45, 76 }
% 45.81/46.06 348 : pppp47-{T}(E1,E0) { 0, 14, 46, 77 }
% 45.81/46.06 349 : pppp46-{T}(E1) { 0, 14, 46, 77 }
% 45.81/46.06 350 : pppp45-{T}(E1) { 0, 14, 46, 77 }
% 45.81/46.06 351 : pppp46-{T}(E0) { 0, 1, 14, 46, 77 }
% 45.81/46.06 352 : pppp44-{T}(E1) { 0, 14, 46, 77 }
% 45.81/46.06 353 : pppp45-{T}(E0) { 0, 1, 14, 46, 77 }
% 45.81/46.06 354 : pppp44-{T}(E0) { 0, 1, 14, 46, 77 }
% 45.81/46.06 355 : pppp47-{T}(E0,E1) { 0, 1, 14, 15, 46, 78 }
% 45.81/46.06 356 : pppp440-{T}(E1) { 0, 4, 31, 57, 79 }
% 45.81/46.06 357 : pppp382-{T}(E1,E1) { 0, 5, 33, 59, 80 }
% 45.81/46.06 358 : pppp381-{T}(E1) { 0, 5, 33, 59, 80 }
% 45.81/46.06 359 : pppp380-{T}(E1) { 0, 5, 33, 59, 80 }
% 45.81/46.06 360 : pppp381-{T}(E0) { 0, 1, 5, 33, 59, 80 }
% 45.81/46.06 361 : pppp379-{T}(E1) { 0, 5, 33, 59, 80 }
% 45.81/46.06 362 : pppp380-{T}(E0) { 0, 1, 5, 33, 59, 80 }
% 45.81/46.06 363 : pppp379-{T}(E0) { 0, 1, 5, 33, 59, 80 }
% 45.81/46.06 364 : pppp441-{T}(E0) { 0, 1, 5, 33, 59, 80 }
% 45.81/46.06 365 : pppp441-{T}(E1) { 0, 1, 5, 15, 33, 59, 80 }
% 45.81/46.06 366 : pppp440-{T}(E0) { 0, 1, 4, 31, 57, 81 }
% 45.81/46.06 367 : pppp382-{T}(E0,E0) { 0, 1, 5, 33, 59, 82 }
% 45.81/46.06 368 : pppp361-{T}(E0,E0) { 0, 6, 34, 61, 83 }
% 45.81/46.06 369 : pppp360-{T}(E0) { 0, 6, 34, 61, 83 }
% 45.81/46.06 370 : pppp359-{T}(E0) { 0, 6, 34, 61, 83 }
% 45.81/46.06 371 : pppp360-{T}(E1) { 0, 1, 6, 15, 34, 61, 83 }
% 45.81/46.06 372 : pppp358-{T}(E0) { 0, 6, 34, 61, 83 }
% 45.81/46.06 373 : pppp359-{T}(E1) { 0, 1, 6, 15, 34, 61, 83 }
% 45.81/46.06 374 : pppp358-{T}(E1) { 0, 1, 6, 15, 34, 61, 83 }
% 45.81/46.06 375 : pppp361-{T}(E1,E1) { 0, 1, 6, 15, 34, 61, 84 }
% 45.81/46.06 376 : pppp336-{T}(E0,E1) { 0, 7, 35, 63, 85 }
% 45.81/46.06 377 : pppp335-{T}(E1) { 0, 7, 35, 63, 85 }
% 45.81/46.06 378 : pppp334-{T}(E1) { 0, 7, 35, 63, 85 }
% 45.81/46.06 379 : pppp335-{T}(E0) { 0, 1, 7, 35, 63, 85 }
% 45.81/46.06 380 : pppp333-{T}(E1) { 0, 7, 35, 63, 85 }
% 45.81/46.06 381 : pppp334-{T}(E0) { 0, 1, 7, 35, 63, 85 }
% 45.81/46.06 382 : pppp333-{T}(E0) { 0, 1, 7, 35, 63, 85 }
% 45.81/46.06 383 : pppp336-{T}(E1,E0) { 0, 1, 7, 15, 35, 63, 86 }
% 45.81/46.06 384 : pppp307-{T}(E1,E1) { 0, 8, 37, 65, 87 }
% 45.81/46.06 385 : pppp306-{T}(E1) { 0, 8, 37, 65, 87 }
% 45.81/46.06 386 : pppp305-{T}(E1) { 0, 8, 37, 65, 87 }
% 45.81/46.06 387 : pppp306-{T}(E0) { 0, 1, 8, 37, 65, 87 }
% 45.81/46.06 388 : pppp304-{T}(E1) { 0, 8, 37, 65, 87 }
% 45.81/46.06 389 : pppp305-{T}(E0) { 0, 1, 8, 37, 65, 87 }
% 45.81/46.06 390 : pppp304-{T}(E0) { 0, 1, 8, 37, 65, 87 }
% 45.81/46.06 391 : pppp307-{T}(E0,E0) { 0, 1, 8, 37, 65, 88 }
% 45.81/46.06 392 : pppp274-{T}(E1,E0) { 0, 9, 39, 67, 89 }
% 45.81/46.06 393 : pppp273-{T}(E0) { 0, 9, 39, 67, 89 }
% 45.81/46.06 394 : pppp272-{T}(E0) { 0, 9, 39, 67, 89 }
% 45.81/46.06 395 : pppp273-{T}(E1) { 0, 1, 9, 15, 39, 67, 89 }
% 45.81/46.06 396 : pppp271-{T}(E0) { 0, 9, 39, 67, 89 }
% 45.81/46.06 397 : pppp272-{T}(E1) { 0, 1, 9, 15, 39, 67, 89 }
% 45.81/46.06 398 : pppp271-{T}(E1) { 0, 1, 9, 15, 39, 67, 89 }
% 45.81/46.06 399 : pppp274-{T}(E0,E1) { 0, 1, 9, 39, 67, 90 }
% 45.81/46.06 400 : pppp236-{T}(E1,E0) { 0, 10, 41, 69, 91 }
% 45.81/46.06 401 : pppp235-{T}(E1) { 0, 10, 41, 69, 91 }
% 45.81/46.06 402 : pppp234-{T}(E1) { 0, 10, 41, 69, 91 }
% 45.81/46.06 403 : pppp235-{T}(E0) { 0, 1, 10, 41, 69, 91 }
% 45.81/46.06 404 : pppp233-{T}(E1) { 0, 10, 41, 69, 91 }
% 45.81/46.06 405 : pppp234-{T}(E0) { 0, 1, 10, 41, 69, 91 }
% 45.81/46.06 406 : pppp233-{T}(E0) { 0, 1, 10, 41, 69, 91 }
% 45.81/46.06 407 : pppp236-{T}(E1,E1) { 0, 1, 10, 15, 41, 69, 92 }
% 45.81/46.06 408 : pppp194-{T}(E1,E0) { 0, 11, 42, 71, 93 }
% 45.81/46.06 409 : pppp193-{T}(E0) { 0, 11, 42, 71, 93 }
% 45.81/46.06 410 : pppp192-{T}(E0) { 0, 11, 42, 71, 93 }
% 45.81/46.06 411 : pppp193-{T}(E1) { 0, 1, 11, 15, 42, 71, 93 }
% 45.81/46.06 412 : pppp191-{T}(E0) { 0, 11, 42, 71, 93 }
% 45.81/46.06 413 : pppp192-{T}(E1) { 0, 1, 11, 15, 42, 71, 93 }
% 45.81/46.06 414 : pppp191-{T}(E1) { 0, 1, 11, 15, 42, 71, 93 }
% 45.81/46.06 415 : pppp194-{T}(E0,E1) { 0, 1, 11, 42, 71, 94 }
% 45.81/46.06 416 : pppp148-{T}(E1,E1) { 0, 12, 43, 73, 95 }
% 45.81/46.06 417 : pppp147-{T}(E1) { 0, 12, 43, 73, 95 }
% 45.81/46.06 418 : pppp146-{T}(E1) { 0, 12, 43, 73, 95 }
% 45.81/46.06 419 : pppp147-{T}(E0) { 0, 1, 12, 43, 73, 95 }
% 45.81/46.06 420 : pppp145-{T}(E1) { 0, 12, 43, 73, 95 }
% 45.81/46.06 421 : pppp146-{T}(E0) { 0, 1, 12, 43, 73, 95 }
% 45.81/46.06 422 : pppp145-{T}(E0) { 0, 1, 12, 43, 73, 95 }
% 45.81/46.06 423 : pppp148-{T}(E1,E0) { 0, 1, 12, 43, 73, 96 }
% 45.81/46.06 424 : pppp98-{T}(E1,E1) { 0, 13, 45, 75, 97 }
% 45.81/46.06 425 : pppp97-{T}(E1) { 0, 13, 45, 75, 97 }
% 45.81/46.06 426 : pppp96-{T}(E1) { 0, 13, 45, 75, 97 }
% 45.81/46.06 427 : pppp97-{T}(E0) { 0, 1, 13, 45, 75, 97 }
% 45.81/46.06 428 : pppp95-{T}(E1) { 0, 13, 45, 75, 97 }
% 45.81/46.06 429 : pppp96-{T}(E0) { 0, 1, 13, 45, 75, 97 }
% 45.81/46.06 430 : pppp95-{T}(E0) { 0, 1, 13, 45, 75, 97 }
% 45.81/46.06 431 : pppp98-{T}(E0,E1) { 0, 1, 13, 45, 75, 98 }
% 45.81/46.06 432 : pppp43-{T}(E1,E1) { 0, 14, 46, 77, 99 }
% 45.81/46.06 433 : pppp42-{T}(E1) { 0, 14, 46, 77, 99 }
% 45.81/46.06 434 : pppp41-{T}(E1) { 0, 14, 46, 77, 99 }
% 45.81/46.06 435 : pppp42-{T}(E0) { 0, 1, 14, 46, 77, 99 }
% 45.81/46.06 436 : pppp40-{T}(E1) { 0, 14, 46, 77, 99 }
% 45.81/46.06 437 : pppp41-{T}(E0) { 0, 1, 14, 46, 77, 99 }
% 45.81/46.06 438 : pppp40-{T}(E0) { 0, 1, 14, 46, 77, 99 }
% 45.81/46.06 439 : pppp43-{T}(E0,E0) { 0, 1, 14, 46, 77, 100 }
% 45.81/46.06 440 : pppp398-{T}(E1,E1) { 0, 4, 31, 57, 79, 101 }
% 45.81/46.06 441 : pppp397-{T}(E1) { 0, 4, 31, 57, 79, 101 }
% 45.81/46.06 442 : pppp396-{T}(E1) { 0, 4, 31, 57, 79, 101 }
% 45.81/46.06 443 : pppp397-{T}(E0) { 0, 1, 4, 31, 57, 79, 101 }
% 45.81/46.06 444 : pppp395-{T}(E1) { 0, 4, 31, 57, 79, 101 }
% 45.81/46.06 445 : pppp396-{T}(E0) { 0, 1, 4, 31, 57, 79, 101 }
% 45.81/46.06 446 : pppp395-{T}(E0) { 0, 1, 4, 31, 57, 79, 101 }
% 45.81/46.06 447 : pppp378-{T}(E1,E0) { 0, 1, 5, 33, 59, 80, 102 }
% 45.81/46.06 448 : pppp377-{T}(E0) { 0, 1, 5, 33, 59, 80, 102 }
% 45.81/46.06 449 : pppp377-{T}(E1) { 0, 1, 5, 33, 59, 80, 102 }
% 45.81/46.06 450 : pppp376-{T}(E0) { 0, 1, 5, 33, 59, 80, 102 }
% 45.81/46.06 451 : pppp376-{T}(E1) { 0, 1, 5, 33, 59, 80, 102 }
% 45.81/46.06 452 : pppp375-{T}(E0) { 0, 1, 5, 33, 59, 80, 102 }
% 45.81/46.06 453 : pppp375-{T}(E1) { 0, 1, 5, 33, 59, 80, 102 }
% 45.81/46.06 454 : pppp378-{T}(E0,E1) { 0, 1, 5, 15, 33, 59, 80, 103 }
% 45.81/46.06 455 : pppp398-{T}(E0,E0) { 0, 1, 4, 31, 57, 81, 104 }
% 45.81/46.06 456 : pppp357-{T}(E1,E0) { 0, 6, 34, 61, 83, 105 }
% 45.81/46.06 457 : pppp356-{T}(E1) { 0, 6, 34, 61, 83, 105 }
% 45.81/46.06 458 : pppp355-{T}(E1) { 0, 6, 34, 61, 83, 105 }
% 45.81/46.06 459 : pppp356-{T}(E0) { 0, 1, 6, 34, 61, 83, 105 }
% 45.81/46.06 460 : pppp354-{T}(E1) { 0, 6, 34, 61, 83, 105 }
% 45.81/46.06 461 : pppp355-{T}(E0) { 0, 1, 6, 34, 61, 83, 105 }
% 45.81/46.06 462 : pppp354-{T}(E0) { 0, 1, 6, 34, 61, 83, 105 }
% 45.81/46.06 463 : pppp442-{T}(E0) { 0, 1, 6, 34, 61, 83, 105 }
% 45.81/46.06 464 : pppp442-{T}(E1) { 0, 1, 6, 15, 34, 61, 83, 105 }
% 45.81/46.06 465 : pppp357-{T}(E1,E1) { 0, 1, 6, 15, 34, 61, 83, 106 }
% 45.81/46.06 466 : pppp332-{T}(E1,E1) { 0, 7, 35, 63, 85, 107 }
% 45.81/46.06 467 : pppp331-{T}(E1) { 0, 7, 35, 63, 85, 107 }
% 45.81/46.06 468 : pppp330-{T}(E1) { 0, 7, 35, 63, 85, 107 }
% 45.81/46.06 469 : pppp331-{T}(E0) { 0, 1, 7, 35, 63, 85, 107 }
% 45.81/46.06 470 : pppp329-{T}(E1) { 0, 7, 35, 63, 85, 107 }
% 45.81/46.06 471 : pppp330-{T}(E0) { 0, 1, 7, 35, 63, 85, 107 }
% 45.81/46.06 472 : pppp329-{T}(E0) { 0, 1, 7, 35, 63, 85, 107 }
% 45.81/46.06 473 : pppp332-{T}(E0,E0) { 0, 1, 7, 35, 63, 85, 108 }
% 45.81/46.06 474 : pppp303-{T}(E1,E1) { 0, 8, 37, 65, 87, 109 }
% 45.81/46.06 475 : pppp302-{T}(E1) { 0, 8, 37, 65, 87, 109 }
% 45.81/46.06 476 : pppp301-{T}(E1) { 0, 8, 37, 65, 87, 109 }
% 45.81/46.06 477 : pppp302-{T}(E0) { 0, 1, 8, 37, 65, 87, 109 }
% 45.81/46.06 478 : pppp300-{T}(E1) { 0, 8, 37, 65, 87, 109 }
% 45.81/46.06 479 : pppp301-{T}(E0) { 0, 1, 8, 37, 65, 87, 109 }
% 45.81/46.06 480 : pppp300-{T}(E0) { 0, 1, 8, 37, 65, 87, 109 }
% 45.81/46.06 481 : pppp303-{T}(E1,E0) { 0, 1, 8, 37, 65, 87, 110 }
% 45.81/46.06 482 : pppp270-{T}(E0,E0) { 0, 9, 39, 67, 89, 111 }
% 45.81/46.06 483 : pppp269-{T}(E0) { 0, 9, 39, 67, 89, 111 }
% 45.81/46.06 484 : pppp268-{T}(E0) { 0, 9, 39, 67, 89, 111 }
% 45.81/46.06 485 : pppp269-{T}(E1) { 0, 1, 9, 15, 39, 67, 89, 111 }
% 45.81/46.06 486 : pppp267-{T}(E0) { 0, 9, 39, 67, 89, 111 }
% 45.81/46.06 487 : pppp268-{T}(E1) { 0, 1, 9, 15, 39, 67, 89, 111 }
% 45.81/46.06 488 : pppp267-{T}(E1) { 0, 1, 9, 15, 39, 67, 89, 111 }
% 45.81/46.06 489 : pppp270-{T}(E1,E1) { 0, 1, 9, 15, 39, 67, 89, 112 }
% 45.81/46.06 490 : pppp232-{T}(E0,E1) { 0, 10, 41, 69, 91, 113 }
% 45.81/46.06 491 : pppp231-{T}(E0) { 0, 10, 41, 69, 91, 113 }
% 45.81/46.06 492 : pppp230-{T}(E0) { 0, 10, 41, 69, 91, 113 }
% 45.81/46.06 493 : pppp231-{T}(E1) { 0, 1, 10, 15, 41, 69, 91, 113 }
% 45.81/46.06 494 : pppp229-{T}(E0) { 0, 10, 41, 69, 91, 113 }
% 45.81/46.06 495 : pppp230-{T}(E1) { 0, 1, 10, 15, 41, 69, 91, 113 }
% 45.81/46.06 496 : pppp229-{T}(E1) { 0, 1, 10, 15, 41, 69, 91, 113 }
% 45.81/46.06 497 : pppp232-{T}(E0,E0) { 0, 1, 10, 41, 69, 91, 114 }
% 45.81/46.06 498 : pppp190-{T}(E0,E0) { 0, 11, 42, 71, 93, 115 }
% 45.81/46.06 499 : pppp189-{T}(E0) { 0, 11, 42, 71, 93, 115 }
% 45.81/46.06 500 : pppp188-{T}(E0) { 0, 11, 42, 71, 93, 115 }
% 45.81/46.06 501 : pppp189-{T}(E1) { 0, 1, 11, 15, 42, 71, 93, 115 }
% 45.81/46.06 502 : pppp187-{T}(E0) { 0, 11, 42, 71, 93, 115 }
% 45.81/46.06 503 : pppp188-{T}(E1) { 0, 1, 11, 15, 42, 71, 93, 115 }
% 45.81/46.06 504 : pppp187-{T}(E1) { 0, 1, 11, 15, 42, 71, 93, 115 }
% 45.81/46.06 505 : pppp190-{T}(E1,E0) { 0, 1, 11, 15, 42, 71, 93, 116 }
% 45.81/46.06 506 : pppp144-{T}(E1,E1) { 0, 12, 43, 73, 95, 117 }
% 45.81/46.06 507 : pppp143-{T}(E1) { 0, 12, 43, 73, 95, 117 }
% 45.81/46.06 508 : pppp142-{T}(E1) { 0, 12, 43, 73, 95, 117 }
% 45.81/46.06 509 : pppp143-{T}(E0) { 0, 1, 12, 43, 73, 95, 117 }
% 45.81/46.06 510 : pppp141-{T}(E1) { 0, 12, 43, 73, 95, 117 }
% 45.81/46.06 511 : pppp142-{T}(E0) { 0, 1, 12, 43, 73, 95, 117 }
% 45.81/46.06 512 : pppp141-{T}(E0) { 0, 1, 12, 43, 73, 95, 117 }
% 45.81/46.06 513 : pppp144-{T}(E0,E0) { 0, 1, 12, 43, 73, 95, 118 }
% 45.81/46.06 514 : pppp94-{T}(E1,E1) { 0, 13, 45, 75, 97, 119 }
% 45.81/46.06 515 : pppp93-{T}(E1) { 0, 13, 45, 75, 97, 119 }
% 45.81/46.06 516 : pppp92-{T}(E1) { 0, 13, 45, 75, 97, 119 }
% 45.81/46.06 517 : pppp93-{T}(E0) { 0, 1, 13, 45, 75, 97, 119 }
% 45.81/46.06 518 : pppp91-{T}(E1) { 0, 13, 45, 75, 97, 119 }
% 45.81/46.06 519 : pppp92-{T}(E0) { 0, 1, 13, 45, 75, 97, 119 }
% 45.81/46.06 520 : pppp91-{T}(E0) { 0, 1, 13, 45, 75, 97, 119 }
% 45.81/46.06 521 : pppp94-{T}(E0,E1) { 0, 1, 13, 45, 75, 97, 120 }
% 45.81/46.06 522 : pppp39-{T}(E1,E1) { 0, 14, 46, 77, 99, 121 }
% 45.81/46.06 523 : pppp38-{T}(E1) { 0, 14, 46, 77, 99, 121 }
% 45.81/46.06 524 : pppp37-{T}(E1) { 0, 14, 46, 77, 99, 121 }
% 45.81/46.06 525 : pppp38-{T}(E0) { 0, 1, 14, 46, 77, 99, 121 }
% 45.81/46.06 526 : pppp36-{T}(E1) { 0, 14, 46, 77, 99, 121 }
% 45.81/46.06 527 : pppp37-{T}(E0) { 0, 1, 14, 46, 77, 99, 121 }
% 45.81/46.06 528 : pppp36-{T}(E0) { 0, 1, 14, 46, 77, 99, 121 }
% 45.81/46.06 529 : pppp39-{T}(E1,E0) { 0, 1, 14, 46, 77, 99, 122 }
% 45.81/46.06 530 : pppp353-{T}(E0,E1) { 0, 1, 6, 34, 61, 83, 105, 123 }
% 45.81/46.06 531 : pppp352-{T}(E0) { 0, 1, 6, 34, 61, 83, 105, 123 }
% 45.81/46.06 532 : pppp352-{T}(E1) { 0, 1, 6, 34, 61, 83, 105, 123 }
% 45.81/46.06 533 : pppp351-{T}(E0) { 0, 1, 6, 34, 61, 83, 105, 123 }
% 45.81/46.06 534 : pppp351-{T}(E1) { 0, 1, 6, 34, 61, 83, 105, 123 }
% 45.81/46.06 535 : pppp350-{T}(E0) { 0, 1, 6, 34, 61, 83, 105, 123 }
% 45.81/46.06 536 : pppp350-{T}(E1) { 0, 1, 6, 34, 61, 83, 105, 123 }
% 45.81/46.06 537 : pppp353-{T}(E1,E0) { 0, 1, 6, 15, 34, 61, 83, 105, 124 }
% 45.81/46.06 538 : pppp328-{T}(E1,E1) { 0, 7, 35, 63, 85, 107, 125 }
% 45.81/46.06 539 : pppp327-{T}(E1) { 0, 7, 35, 63, 85, 107, 125 }
% 45.81/46.06 540 : pppp326-{T}(E1) { 0, 7, 35, 63, 85, 107, 125 }
% 45.81/46.06 541 : pppp327-{T}(E0) { 0, 1, 7, 35, 63, 85, 107, 125 }
% 45.81/46.06 542 : pppp325-{T}(E1) { 0, 7, 35, 63, 85, 107, 125 }
% 45.81/46.06 543 : pppp326-{T}(E0) { 0, 1, 7, 35, 63, 85, 107, 125 }
% 45.81/46.06 544 : pppp325-{T}(E0) { 0, 1, 7, 35, 63, 85, 107, 125 }
% 45.81/46.06 545 : pppp443-{T}(E1) { 0, 7, 35, 63, 85, 107, 125 }
% 45.81/46.06 546 : pppp443-{T}(E0) { 0, 1, 7, 35, 63, 85, 107, 125 }
% 45.81/46.06 547 : pppp328-{T}(E0,E1) { 0, 1, 7, 35, 63, 85, 107, 126 }
% 45.81/46.06 548 : pppp299-{T}(E0,E1) { 0, 8, 37, 65, 87, 109, 127 }
% 45.81/46.06 549 : pppp298-{T}(E0) { 0, 8, 37, 65, 87, 109, 127 }
% 45.81/46.06 550 : pppp297-{T}(E0) { 0, 8, 37, 65, 87, 109, 127 }
% 45.81/46.06 551 : pppp298-{T}(E1) { 0, 1, 8, 15, 37, 65, 87, 109, 127 }
% 45.81/46.06 552 : pppp296-{T}(E0) { 0, 8, 37, 65, 87, 109, 127 }
% 45.81/46.06 553 : pppp297-{T}(E1) { 0, 1, 8, 15, 37, 65, 87, 109, 127 }
% 45.81/46.06 554 : pppp296-{T}(E1) { 0, 1, 8, 15, 37, 65, 87, 109, 127 }
% 45.81/46.06 555 : pppp299-{T}(E0,E0) { 0, 1, 8, 37, 65, 87, 109, 128 }
% 45.81/46.06 556 : pppp266-{T}(E0,E1) { 0, 9, 39, 67, 89, 111, 129 }
% 45.81/46.06 557 : pppp265-{T}(E1) { 0, 9, 39, 67, 89, 111, 129 }
% 45.81/46.06 558 : pppp264-{T}(E1) { 0, 9, 39, 67, 89, 111, 129 }
% 45.81/46.06 559 : pppp265-{T}(E0) { 0, 1, 9, 39, 67, 89, 111, 129 }
% 45.81/46.06 560 : pppp263-{T}(E1) { 0, 9, 39, 67, 89, 111, 129 }
% 45.81/46.06 561 : pppp264-{T}(E0) { 0, 1, 9, 39, 67, 89, 111, 129 }
% 45.81/46.06 562 : pppp263-{T}(E0) { 0, 1, 9, 39, 67, 89, 111, 129 }
% 45.81/46.06 563 : pppp266-{T}(E1,E0) { 0, 1, 9, 15, 39, 67, 89, 111, 130 }
% 45.81/46.06 564 : pppp228-{T}(E1,E0) { 0, 10, 41, 69, 91, 113, 131 }
% 45.81/46.06 565 : pppp227-{T}(E1) { 0, 10, 41, 69, 91, 113, 131 }
% 45.81/46.06 566 : pppp226-{T}(E1) { 0, 10, 41, 69, 91, 113, 131 }
% 45.81/46.06 567 : pppp227-{T}(E0) { 0, 1, 10, 41, 69, 91, 113, 131 }
% 45.81/46.06 568 : pppp225-{T}(E1) { 0, 10, 41, 69, 91, 113, 131 }
% 45.81/46.06 569 : pppp226-{T}(E0) { 0, 1, 10, 41, 69, 91, 113, 131 }
% 45.81/46.06 570 : pppp225-{T}(E0) { 0, 1, 10, 41, 69, 91, 113, 131 }
% 45.81/46.06 571 : pppp228-{T}(E1,E1) { 0, 1, 10, 15, 41, 69, 91, 113, 132 }
% 45.81/46.06 572 : pppp186-{T}(E0,E0) { 0, 11, 42, 71, 93, 115, 133 }
% 45.81/46.06 573 : pppp185-{T}(E0) { 0, 11, 42, 71, 93, 115, 133 }
% 45.81/46.06 574 : pppp184-{T}(E0) { 0, 11, 42, 71, 93, 115, 133 }
% 45.81/46.06 575 : pppp185-{T}(E1) { 0, 1, 11, 15, 42, 71, 93, 115, 133 }
% 45.81/46.06 576 : pppp183-{T}(E0) { 0, 11, 42, 71, 93, 115, 133 }
% 45.81/46.06 577 : pppp184-{T}(E1) { 0, 1, 11, 15, 42, 71, 93, 115, 133 }
% 45.81/46.06 578 : pppp183-{T}(E1) { 0, 1, 11, 15, 42, 71, 93, 115, 133 }
% 45.81/46.06 579 : pppp186-{T}(E1,E0) { 0, 1, 11, 15, 42, 71, 93, 115, 134 }
% 45.81/46.06 580 : pppp140-{T}(E0,E1) { 0, 12, 43, 73, 95, 117, 135 }
% 45.81/46.06 581 : pppp139-{T}(E0) { 0, 12, 43, 73, 95, 117, 135 }
% 45.81/46.06 582 : pppp138-{T}(E0) { 0, 12, 43, 73, 95, 117, 135 }
% 45.81/46.06 583 : pppp139-{T}(E1) { 0, 1, 12, 15, 43, 73, 95, 117, 135 }
% 45.81/46.06 584 : pppp137-{T}(E0) { 0, 12, 43, 73, 95, 117, 135 }
% 45.81/46.06 585 : pppp138-{T}(E1) { 0, 1, 12, 15, 43, 73, 95, 117, 135 }
% 45.81/46.06 586 : pppp137-{T}(E1) { 0, 1, 12, 15, 43, 73, 95, 117, 135 }
% 45.81/46.06 587 : pppp140-{T}(E1,E0) { 0, 1, 12, 43, 73, 95, 117, 136 }
% 45.81/46.06 588 : pppp90-{T}(E1,E1) { 0, 13, 45, 75, 97, 119, 137 }
% 45.81/46.06 589 : pppp89-{T}(E1) { 0, 13, 45, 75, 97, 119, 137 }
% 45.81/46.06 590 : pppp88-{T}(E1) { 0, 13, 45, 75, 97, 119, 137 }
% 45.81/46.06 591 : pppp89-{T}(E0) { 0, 1, 13, 45, 75, 97, 119, 137 }
% 45.81/46.06 592 : pppp87-{T}(E1) { 0, 13, 45, 75, 97, 119, 137 }
% 45.81/46.06 593 : pppp88-{T}(E0) { 0, 1, 13, 45, 75, 97, 119, 137 }
% 45.81/46.06 594 : pppp87-{T}(E0) { 0, 1, 13, 45, 75, 97, 119, 137 }
% 45.81/46.06 595 : pppp90-{T}(E0,E0) { 0, 1, 13, 45, 75, 97, 119, 138 }
% 45.81/46.06 596 : pppp35-{T}(E0,E1) { 0, 14, 46, 77, 99, 121, 139 }
% 45.81/46.06 597 : pppp34-{T}(E0) { 0, 14, 46, 77, 99, 121, 139 }
% 45.81/46.06 598 : pppp33-{T}(E0) { 0, 14, 46, 77, 99, 121, 139 }
% 45.81/46.06 599 : pppp34-{T}(E1) { 0, 1, 14, 15, 46, 77, 99, 121, 139 }
% 45.81/46.06 600 : pppp32-{T}(E0) { 0, 14, 46, 77, 99, 121, 139 }
% 45.81/46.06 601 : pppp33-{T}(E1) { 0, 1, 14, 15, 46, 77, 99, 121, 139 }
% 45.81/46.06 602 : pppp32-{T}(E1) { 0, 1, 14, 15, 46, 77, 99, 121, 139 }
% 45.81/46.06 603 : pppp35-{T}(E1,E0) { 0, 1, 14, 46, 77, 99, 121, 140 }
% 45.81/46.06 604 : pppp324-{T}(E1,E1) { 0, 7, 35, 63, 85, 107, 125, 141 }
% 45.81/46.06 605 : pppp323-{T}(E1) { 0, 7, 35, 63, 85, 107, 125, 141 }
% 45.81/46.06 606 : pppp322-{T}(E1) { 0, 7, 35, 63, 85, 107, 125, 141 }
% 45.81/46.06 607 : pppp323-{T}(E0) { 0, 1, 7, 35, 63, 85, 107, 125, 141 }
% 45.81/46.06 608 : pppp321-{T}(E1) { 0, 7, 35, 63, 85, 107, 125, 141 }
% 45.81/46.06 609 : pppp322-{T}(E0) { 0, 1, 7, 35, 63, 85, 107, 125, 141 }
% 45.81/46.06 610 : pppp321-{T}(E0) { 0, 1, 7, 35, 63, 85, 107, 125, 141 }
% 45.81/46.06 611 : pppp324-{T}(E0,E0) { 0, 1, 7, 35, 63, 85, 107, 125, 142 }
% 45.81/46.06 612 : pppp295-{T}(E0,E0) { 0, 8, 37, 65, 87, 109, 127, 143 }
% 45.81/46.06 613 : pppp294-{T}(E0) { 0, 8, 37, 65, 87, 109, 127, 143 }
% 45.81/46.06 614 : pppp293-{T}(E0) { 0, 8, 37, 65, 87, 109, 127, 143 }
% 45.81/46.06 615 : pppp294-{T}(E1) { 0, 1, 8, 15, 37, 65, 87, 109, 127, 143 }
% 45.81/46.06 616 : pppp292-{T}(E0) { 0, 8, 37, 65, 87, 109, 127, 143 }
% 45.81/46.06 617 : pppp293-{T}(E1) { 0, 1, 8, 15, 37, 65, 87, 109, 127, 143 }
% 45.81/46.06 618 : pppp292-{T}(E1) { 0, 1, 8, 15, 37, 65, 87, 109, 127, 143 }
% 45.81/46.06 619 : pppp444-{T}(E0) { 0, 1, 8, 37, 65, 87, 109, 127, 143 }
% 45.81/46.06 620 : pppp444-{T}(E1) { 0, 1, 8, 15, 37, 65, 87, 109, 127, 143 }
% 45.81/46.06 621 : pppp295-{T}(E1,E1) { 0, 1, 8, 15, 37, 65, 87, 109, 127, 144 }
% 45.81/46.06 622 : pppp262-{T}(E1,E0) { 0, 9, 39, 67, 89, 111, 129, 145 }
% 45.81/46.06 623 : pppp261-{T}(E0) { 0, 9, 39, 67, 89, 111, 129, 145 }
% 45.81/46.06 624 : pppp260-{T}(E0) { 0, 9, 39, 67, 89, 111, 129, 145 }
% 45.81/46.06 625 : pppp261-{T}(E1) { 0, 1, 9, 15, 39, 67, 89, 111, 129, 145 }
% 45.81/46.06 626 : pppp259-{T}(E0) { 0, 9, 39, 67, 89, 111, 129, 145 }
% 45.81/46.06 627 : pppp260-{T}(E1) { 0, 1, 9, 15, 39, 67, 89, 111, 129, 145 }
% 45.81/46.06 628 : pppp259-{T}(E1) { 0, 1, 9, 15, 39, 67, 89, 111, 129, 145 }
% 45.81/46.06 629 : pppp262-{T}(E0,E1) { 0, 1, 9, 39, 67, 89, 111, 129, 146 }
% 45.81/46.06 630 : pppp224-{T}(E0,E1) { 0, 10, 41, 69, 91, 113, 131, 147 }
% 45.81/46.06 631 : pppp223-{T}(E0) { 0, 10, 41, 69, 91, 113, 131, 147 }
% 45.81/46.06 632 : pppp222-{T}(E0) { 0, 10, 41, 69, 91, 113, 131, 147 }
% 45.81/46.06 633 : pppp223-{T}(E1) { 0, 1, 10, 15, 41, 69, 91, 113, 131, 147 }
% 45.81/46.06 634 : pppp221-{T}(E0) { 0, 10, 41, 69, 91, 113, 131, 147 }
% 45.81/46.06 635 : pppp222-{T}(E1) { 0, 1, 10, 15, 41, 69, 91, 113, 131, 147 }
% 45.81/46.06 636 : pppp221-{T}(E1) { 0, 1, 10, 15, 41, 69, 91, 113, 131, 147 }
% 45.81/46.06 637 : pppp224-{T}(E1,E0) { 0, 1, 10, 41, 69, 91, 113, 131, 148 }
% 45.81/46.06 638 : pppp182-{T}(E0,E1) { 0, 11, 42, 71, 93, 115, 133, 149 }
% 45.81/46.06 639 : pppp181-{T}(E1) { 0, 11, 42, 71, 93, 115, 133, 149 }
% 45.81/46.06 640 : pppp180-{T}(E1) { 0, 11, 42, 71, 93, 115, 133, 149 }
% 45.81/46.06 641 : pppp181-{T}(E0) { 0, 1, 11, 42, 71, 93, 115, 133, 149 }
% 45.81/46.06 642 : pppp179-{T}(E1) { 0, 11, 42, 71, 93, 115, 133, 149 }
% 45.81/46.06 643 : pppp180-{T}(E0) { 0, 1, 11, 42, 71, 93, 115, 133, 149 }
% 45.81/46.06 644 : pppp179-{T}(E0) { 0, 1, 11, 42, 71, 93, 115, 133, 149 }
% 45.81/46.06 645 : pppp182-{T}(E1,E0) { 0, 1, 11, 15, 42, 71, 93, 115, 133, 150 }
% 45.81/46.06 646 : pppp136-{T}(E0,E0) { 0, 12, 43, 73, 95, 117, 135, 151 }
% 45.81/46.06 647 : pppp135-{T}(E0) { 0, 12, 43, 73, 95, 117, 135, 151 }
% 45.81/46.06 648 : pppp134-{T}(E0) { 0, 12, 43, 73, 95, 117, 135, 151 }
% 45.81/46.06 649 : pppp135-{T}(E1) { 0, 1, 12, 15, 43, 73, 95, 117, 135, 151 }
% 45.81/46.06 650 : pppp133-{T}(E0) { 0, 12, 43, 73, 95, 117, 135, 151 }
% 45.81/46.06 651 : pppp134-{T}(E1) { 0, 1, 12, 15, 43, 73, 95, 117, 135, 151 }
% 45.81/46.06 652 : pppp133-{T}(E1) { 0, 1, 12, 15, 43, 73, 95, 117, 135, 151 }
% 45.81/46.06 653 : pppp136-{T}(E0,E1) { 0, 1, 12, 15, 43, 73, 95, 117, 135, 152 }
% 45.81/46.06 654 : pppp86-{T}(E1,E0) { 0, 13, 45, 75, 97, 119, 137, 153 }
% 45.81/46.06 655 : pppp85-{T}(E0) { 0, 13, 45, 75, 97, 119, 137, 153 }
% 45.81/46.06 656 : pppp84-{T}(E0) { 0, 13, 45, 75, 97, 119, 137, 153 }
% 45.81/46.06 657 : pppp85-{T}(E1) { 0, 1, 13, 15, 45, 75, 97, 119, 137, 153 }
% 45.81/46.06 658 : pppp83-{T}(E0) { 0, 13, 45, 75, 97, 119, 137, 153 }
% 45.81/46.06 659 : pppp84-{T}(E1) { 0, 1, 13, 15, 45, 75, 97, 119, 137, 153 }
% 45.81/46.06 660 : pppp83-{T}(E1) { 0, 1, 13, 15, 45, 75, 97, 119, 137, 153 }
% 45.81/46.06 661 : pppp86-{T}(E0,E0) { 0, 1, 13, 45, 75, 97, 119, 137, 154 }
% 45.81/46.06 662 : pppp31-{T}(E0,E0) { 0, 14, 46, 77, 99, 121, 139, 155 }
% 45.81/46.06 663 : pppp30-{T}(E0) { 0, 14, 46, 77, 99, 121, 139, 155 }
% 45.81/46.06 664 : pppp29-{T}(E0) { 0, 14, 46, 77, 99, 121, 139, 155 }
% 45.81/46.06 665 : pppp30-{T}(E1) { 0, 1, 14, 15, 46, 77, 99, 121, 139, 155 }
% 45.81/46.06 666 : pppp28-{T}(E0) { 0, 14, 46, 77, 99, 121, 139, 155 }
% 45.81/46.06 667 : pppp29-{T}(E1) { 0, 1, 14, 15, 46, 77, 99, 121, 139, 155 }
% 45.81/46.06 668 : pppp28-{T}(E1) { 0, 1, 14, 15, 46, 77, 99, 121, 139, 155 }
% 45.81/46.06 669 : pppp31-{T}(E1,E1) { 0, 1, 14, 15, 46, 77, 99, 121, 139, 156 }
% 45.81/46.06 670 : pppp291-{T}(E0,E0) { 0, 1, 8, 37, 65, 87, 109, 127, 143, 157 }
% 45.81/46.06 671 : pppp290-{T}(E0) { 0, 1, 8, 37, 65, 87, 109, 127, 143, 157 }
% 45.81/46.06 672 : pppp289-{T}(E0) { 0, 1, 8, 37, 65, 87, 109, 127, 143, 157 }
% 45.81/46.06 673 : pppp290-{T}(E1) { 0, 1, 8, 15, 37, 65, 87, 109, 127, 143, 157 }
% 45.81/46.06 674 : pppp288-{T}(E0) { 0, 1, 8, 37, 65, 87, 109, 127, 143, 157 }
% 45.81/46.06 675 : pppp289-{T}(E1) { 0, 1, 8, 15, 37, 65, 87, 109, 127, 143, 157 }
% 45.81/46.06 676 : pppp288-{T}(E1) { 0, 1, 8, 15, 37, 65, 87, 109, 127, 143, 157 }
% 45.81/46.06 677 : pppp291-{T}(E1,E0) { 0, 1, 8, 15, 37, 65, 87, 109, 127, 143, 158 }
% 45.81/46.06 678 : pppp258-{T}(E0,E1) { 0, 9, 39, 67, 89, 111, 129, 145, 159 }
% 45.81/46.06 679 : pppp257-{T}(E1) { 0, 9, 39, 67, 89, 111, 129, 145, 159 }
% 45.81/46.06 680 : pppp256-{T}(E1) { 0, 9, 39, 67, 89, 111, 129, 145, 159 }
% 45.81/46.06 681 : pppp257-{T}(E0) { 0, 1, 9, 39, 67, 89, 111, 129, 145, 159 }
% 45.81/46.06 682 : pppp255-{T}(E1) { 0, 9, 39, 67, 89, 111, 129, 145, 159 }
% 45.81/46.06 683 : pppp256-{T}(E0) { 0, 1, 9, 39, 67, 89, 111, 129, 145, 159 }
% 45.81/46.06 684 : pppp255-{T}(E0) { 0, 1, 9, 39, 67, 89, 111, 129, 145, 159 }
% 45.81/46.06 685 : pppp445-{T}(E1) { 0, 9, 39, 67, 89, 111, 129, 145, 159 }
% 45.81/46.06 686 : pppp445-{T}(E0) { 0, 1, 9, 39, 67, 89, 111, 129, 145, 159 }
% 45.81/46.06 687 : pppp258-{T}(E1,E0) { 0, 1, 9, 15, 39, 67, 89, 111, 129, 145, 160 }
% 45.81/46.06 688 : pppp220-{T}(E1,E0) { 0, 10, 41, 69, 91, 113, 131, 147, 161 }
% 45.81/46.06 689 : pppp219-{T}(E1) { 0, 10, 41, 69, 91, 113, 131, 147, 161 }
% 45.81/46.06 690 : pppp218-{T}(E1) { 0, 10, 41, 69, 91, 113, 131, 147, 161 }
% 45.81/46.06 691 : pppp219-{T}(E0) { 0, 1, 10, 41, 69, 91, 113, 131, 147, 161 }
% 45.81/46.06 692 : pppp217-{T}(E1) { 0, 10, 41, 69, 91, 113, 131, 147, 161 }
% 45.81/46.06 693 : pppp218-{T}(E0) { 0, 1, 10, 41, 69, 91, 113, 131, 147, 161 }
% 45.81/46.06 694 : pppp217-{T}(E0) { 0, 1, 10, 41, 69, 91, 113, 131, 147, 161 }
% 45.81/46.06 695 : pppp220-{T}(E1,E1) { 0, 1, 10, 15, 41, 69, 91, 113, 131, 147, 162 }
% 45.81/46.06 696 : pppp178-{T}(E1,E1) { 0, 11, 42, 71, 93, 115, 133, 149, 163 }
% 45.81/46.06 697 : pppp177-{T}(E1) { 0, 11, 42, 71, 93, 115, 133, 149, 163 }
% 45.81/46.06 698 : pppp176-{T}(E1) { 0, 11, 42, 71, 93, 115, 133, 149, 163 }
% 45.81/46.06 699 : pppp177-{T}(E0) { 0, 1, 11, 42, 71, 93, 115, 133, 149, 163 }
% 45.81/46.06 700 : pppp175-{T}(E1) { 0, 11, 42, 71, 93, 115, 133, 149, 163 }
% 45.81/46.06 701 : pppp176-{T}(E0) { 0, 1, 11, 42, 71, 93, 115, 133, 149, 163 }
% 45.81/46.06 702 : pppp175-{T}(E0) { 0, 1, 11, 42, 71, 93, 115, 133, 149, 163 }
% 45.81/46.06 703 : pppp178-{T}(E0,E0) { 0, 1, 11, 42, 71, 93, 115, 133, 149, 164 }
% 45.81/46.06 704 : pppp132-{T}(E0,E0) { 0, 12, 43, 73, 95, 117, 135, 151, 165 }
% 45.81/46.06 705 : pppp131-{T}(E0) { 0, 12, 43, 73, 95, 117, 135, 151, 165 }
% 45.81/46.06 706 : pppp130-{T}(E0) { 0, 12, 43, 73, 95, 117, 135, 151, 165 }
% 45.81/46.06 707 : pppp131-{T}(E1) { 0, 1, 12, 15, 43, 73, 95, 117, 135, 151, 165 }
% 45.81/46.06 708 : pppp129-{T}(E0) { 0, 12, 43, 73, 95, 117, 135, 151, 165 }
% 45.81/46.06 709 : pppp130-{T}(E1) { 0, 1, 12, 15, 43, 73, 95, 117, 135, 151, 165 }
% 45.81/46.06 710 : pppp129-{T}(E1) { 0, 1, 12, 15, 43, 73, 95, 117, 135, 151, 165 }
% 45.81/46.06 711 : pppp132-{T}(E1,E1) { 0, 1, 12, 15, 43, 73, 95, 117, 135, 151, 166 }
% 45.81/46.06 712 : pppp82-{T}(E0,E0) { 0, 13, 45, 75, 97, 119, 137, 153, 167 }
% 45.81/46.06 713 : pppp81-{T}(E0) { 0, 13, 45, 75, 97, 119, 137, 153, 167 }
% 45.81/46.06 714 : pppp80-{T}(E0) { 0, 13, 45, 75, 97, 119, 137, 153, 167 }
% 45.81/46.06 715 : pppp81-{T}(E1) { 0, 1, 13, 15, 45, 75, 97, 119, 137, 153, 167 }
% 45.81/46.06 716 : pppp79-{T}(E0) { 0, 13, 45, 75, 97, 119, 137, 153, 167 }
% 45.81/46.06 717 : pppp80-{T}(E1) { 0, 1, 13, 15, 45, 75, 97, 119, 137, 153, 167 }
% 45.81/46.06 718 : pppp79-{T}(E1) { 0, 1, 13, 15, 45, 75, 97, 119, 137, 153, 167 }
% 45.81/46.06 719 : pppp82-{T}(E1,E1) { 0, 1, 13, 15, 45, 75, 97, 119, 137, 153, 168 }
% 45.81/46.06 720 : pppp27-{T}(E1,E0) { 0, 14, 46, 77, 99, 121, 139, 155, 169 }
% 45.81/46.06 721 : pppp26-{T}(E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169 }
% 45.81/46.06 722 : pppp25-{T}(E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169 }
% 45.81/46.06 723 : pppp26-{T}(E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169 }
% 45.81/46.06 724 : pppp24-{T}(E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169 }
% 45.81/46.06 725 : pppp25-{T}(E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169 }
% 45.81/46.06 726 : pppp24-{T}(E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169 }
% 45.81/46.06 727 : pppp27-{T}(E0,E1) { 0, 1, 14, 15, 46, 77, 99, 121, 139, 155, 170 }
% 45.81/46.06 728 : pppp254-{T}(E0,E1) { 0, 9, 39, 67, 89, 111, 129, 145, 159, 171 }
% 45.81/46.06 729 : pppp253-{T}(E0) { 0, 9, 39, 67, 89, 111, 129, 145, 159, 171 }
% 45.81/46.06 730 : pppp252-{T}(E0) { 0, 9, 39, 67, 89, 111, 129, 145, 159, 171 }
% 45.81/46.06 731 : pppp253-{T}(E1) { 0, 1, 9, 15, 39, 67, 89, 111, 129, 145, 159, 171 }
% 45.81/46.06 732 : pppp251-{T}(E0) { 0, 9, 39, 67, 89, 111, 129, 145, 159, 171 }
% 45.81/46.06 733 : pppp252-{T}(E1) { 0, 1, 9, 15, 39, 67, 89, 111, 129, 145, 159, 171 }
% 45.81/46.06 734 : pppp251-{T}(E1) { 0, 1, 9, 15, 39, 67, 89, 111, 129, 145, 159, 171 }
% 45.81/46.06 735 : pppp254-{T}(E1,E0) { 0, 1, 9, 39, 67, 89, 111, 129, 145, 159, 172 }
% 45.81/46.06 736 : pppp216-{T}(E1,E1) { 0, 10, 41, 69, 91, 113, 131, 147, 161, 173 }
% 45.81/46.06 737 : pppp215-{T}(E1) { 0, 10, 41, 69, 91, 113, 131, 147, 161, 173 }
% 45.81/46.06 738 : pppp214-{T}(E1) { 0, 10, 41, 69, 91, 113, 131, 147, 161, 173 }
% 45.81/46.06 739 : pppp215-{T}(E0) { 0, 1, 10, 41, 69, 91, 113, 131, 147, 161, 173 }
% 45.81/46.06 740 : pppp213-{T}(E1) { 0, 10, 41, 69, 91, 113, 131, 147, 161, 173 }
% 45.81/46.06 741 : pppp214-{T}(E0) { 0, 1, 10, 41, 69, 91, 113, 131, 147, 161, 173 }
% 45.81/46.06 742 : pppp213-{T}(E0) { 0, 1, 10, 41, 69, 91, 113, 131, 147, 161, 173 }
% 45.81/46.06 743 : pppp446-{T}(E1) { 0, 10, 41, 69, 91, 113, 131, 147, 161, 173 }
% 45.81/46.06 744 : pppp446-{T}(E0) { 0, 1, 10, 41, 69, 91, 113, 131, 147, 161, 173 }
% 45.81/46.06 745 : pppp216-{T}(E0,E0) { 0, 1, 10, 41, 69, 91, 113, 131, 147, 161, 174 }
% 45.81/46.06 746 : pppp174-{T}(E1,E1) { 0, 11, 42, 71, 93, 115, 133, 149, 163, 175 }
% 45.81/46.06 747 : pppp173-{T}(E1) { 0, 11, 42, 71, 93, 115, 133, 149, 163, 175 }
% 45.81/46.06 748 : pppp172-{T}(E1) { 0, 11, 42, 71, 93, 115, 133, 149, 163, 175 }
% 45.81/46.06 749 : pppp173-{T}(E0) { 0, 1, 11, 42, 71, 93, 115, 133, 149, 163, 175 }
% 45.81/46.06 750 : pppp171-{T}(E1) { 0, 11, 42, 71, 93, 115, 133, 149, 163, 175 }
% 45.81/46.06 751 : pppp172-{T}(E0) { 0, 1, 11, 42, 71, 93, 115, 133, 149, 163, 175 }
% 45.81/46.06 752 : pppp171-{T}(E0) { 0, 1, 11, 42, 71, 93, 115, 133, 149, 163, 175 }
% 45.81/46.06 753 : pppp174-{T}(E0,E0) { 0, 1, 11, 42, 71, 93, 115, 133, 149, 163, 176 }
% 45.81/46.06 754 : pppp128-{T}(E0,E0) { 0, 12, 43, 73, 95, 117, 135, 151, 165, 177 }
% 45.81/46.06 755 : pppp127-{T}(E0) { 0, 12, 43, 73, 95, 117, 135, 151, 165, 177 }
% 45.81/46.06 756 : pppp126-{T}(E0) { 0, 12, 43, 73, 95, 117, 135, 151, 165, 177 }
% 45.81/46.06 757 : pppp127-{T}(E1) { 0, 1, 12, 15, 43, 73, 95, 117, 135, 151, 165, 177 }
% 45.81/46.06 758 : pppp125-{T}(E0) { 0, 12, 43, 73, 95, 117, 135, 151, 165, 177 }
% 45.81/46.06 759 : pppp126-{T}(E1) { 0, 1, 12, 15, 43, 73, 95, 117, 135, 151, 165, 177 }
% 45.81/46.06 760 : pppp125-{T}(E1) { 0, 1, 12, 15, 43, 73, 95, 117, 135, 151, 165, 177 }
% 45.81/46.06 761 : pppp128-{T}(E0,E1) { 0, 1, 12, 15, 43, 73, 95, 117, 135, 151, 165, 178 }
% 45.81/46.06 762 : pppp78-{T}(E0,E1) { 0, 13, 45, 75, 97, 119, 137, 153, 167, 179 }
% 45.81/46.06 763 : pppp77-{T}(E1) { 0, 13, 45, 75, 97, 119, 137, 153, 167, 179 }
% 45.81/46.06 764 : pppp76-{T}(E1) { 0, 13, 45, 75, 97, 119, 137, 153, 167, 179 }
% 45.81/46.06 765 : pppp77-{T}(E0) { 0, 1, 13, 45, 75, 97, 119, 137, 153, 167, 179 }
% 45.81/46.06 766 : pppp75-{T}(E1) { 0, 13, 45, 75, 97, 119, 137, 153, 167, 179 }
% 45.81/46.06 767 : pppp76-{T}(E0) { 0, 1, 13, 45, 75, 97, 119, 137, 153, 167, 179 }
% 45.81/46.06 768 : pppp75-{T}(E0) { 0, 1, 13, 45, 75, 97, 119, 137, 153, 167, 179 }
% 45.81/46.06 769 : pppp78-{T}(E1,E0) { 0, 1, 13, 15, 45, 75, 97, 119, 137, 153, 167, 180 }
% 45.81/46.06 770 : pppp23-{T}(E1,E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169, 181 }
% 45.81/46.06 771 : pppp22-{T}(E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169, 181 }
% 45.81/46.06 772 : pppp21-{T}(E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169, 181 }
% 45.81/46.06 773 : pppp22-{T}(E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169, 181 }
% 45.81/46.06 774 : pppp20-{T}(E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169, 181 }
% 45.81/46.06 775 : pppp21-{T}(E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169, 181 }
% 45.81/46.06 776 : pppp20-{T}(E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169, 181 }
% 45.81/46.06 777 : pppp23-{T}(E0,E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169, 182 }
% 45.81/46.06 778 : pppp212-{T}(E1,E1) { 0, 10, 41, 69, 91, 113, 131, 147, 161, 173, 183 }
% 45.81/46.06 779 : pppp211-{T}(E1) { 0, 10, 41, 69, 91, 113, 131, 147, 161, 173, 183 }
% 45.81/46.06 780 : pppp210-{T}(E1) { 0, 10, 41, 69, 91, 113, 131, 147, 161, 173, 183 }
% 45.81/46.06 781 : pppp211-{T}(E0) { 0, 1, 10, 41, 69, 91, 113, 131, 147, 161, 173, 183 }
% 45.81/46.06 782 : pppp209-{T}(E1) { 0, 10, 41, 69, 91, 113, 131, 147, 161, 173, 183 }
% 45.81/46.06 783 : pppp210-{T}(E0) { 0, 1, 10, 41, 69, 91, 113, 131, 147, 161, 173, 183 }
% 45.81/46.06 784 : pppp209-{T}(E0) { 0, 1, 10, 41, 69, 91, 113, 131, 147, 161, 173, 183 }
% 45.81/46.06 785 : pppp212-{T}(E0,E0) { 0, 1, 10, 41, 69, 91, 113, 131, 147, 161, 173, 184 }
% 45.81/46.06 786 : pppp170-{T}(E1,E0) { 0, 11, 42, 71, 93, 115, 133, 149, 163, 175, 185 }
% 45.81/46.06 787 : pppp169-{T}(E0) { 0, 11, 42, 71, 93, 115, 133, 149, 163, 175, 185 }
% 45.81/46.06 788 : pppp168-{T}(E0) { 0, 11, 42, 71, 93, 115, 133, 149, 163, 175, 185 }
% 45.81/46.06 789 : pppp169-{T}(E1) { 0, 1, 11, 15, 42, 71, 93, 115, 133, 149, 163, 175, 185 }
% 45.81/46.06 790 : pppp167-{T}(E0) { 0, 11, 42, 71, 93, 115, 133, 149, 163, 175, 185 }
% 45.81/46.06 791 : pppp168-{T}(E1) { 0, 1, 11, 15, 42, 71, 93, 115, 133, 149, 163, 175, 185 }
% 45.81/46.06 792 : pppp167-{T}(E1) { 0, 1, 11, 15, 42, 71, 93, 115, 133, 149, 163, 175, 185 }
% 45.81/46.06 793 : pppp447-{T}(E0) { 0, 1, 11, 42, 71, 93, 115, 133, 149, 163, 175, 185 }
% 45.81/46.06 794 : pppp447-{T}(E1) { 0, 1, 11, 15, 42, 71, 93, 115, 133, 149, 163, 175, 185 }
% 45.81/46.06 795 : pppp170-{T}(E0,E0) { 0, 1, 11, 42, 71, 93, 115, 133, 149, 163, 175, 186 }
% 45.81/46.06 796 : pppp124-{T}(E1,E0) { 0, 12, 43, 73, 95, 117, 135, 151, 165, 177, 187 }
% 45.81/46.06 797 : pppp123-{T}(E1) { 0, 12, 43, 73, 95, 117, 135, 151, 165, 177, 187 }
% 45.81/46.06 798 : pppp122-{T}(E1) { 0, 12, 43, 73, 95, 117, 135, 151, 165, 177, 187 }
% 45.81/46.06 799 : pppp123-{T}(E0) { 0, 1, 12, 43, 73, 95, 117, 135, 151, 165, 177, 187 }
% 45.81/46.06 800 : pppp121-{T}(E1) { 0, 12, 43, 73, 95, 117, 135, 151, 165, 177, 187 }
% 45.81/46.06 801 : pppp122-{T}(E0) { 0, 1, 12, 43, 73, 95, 117, 135, 151, 165, 177, 187 }
% 45.81/46.06 802 : pppp121-{T}(E0) { 0, 1, 12, 43, 73, 95, 117, 135, 151, 165, 177, 187 }
% 45.81/46.06 803 : pppp124-{T}(E0,E1) { 0, 1, 12, 15, 43, 73, 95, 117, 135, 151, 165, 177, 188 }
% 45.81/46.06 804 : pppp74-{T}(E1,E0) { 0, 13, 45, 75, 97, 119, 137, 153, 167, 179, 189 }
% 45.81/46.06 805 : pppp73-{T}(E0) { 0, 13, 45, 75, 97, 119, 137, 153, 167, 179, 189 }
% 45.81/46.06 806 : pppp72-{T}(E0) { 0, 13, 45, 75, 97, 119, 137, 153, 167, 179, 189 }
% 45.81/46.06 807 : pppp73-{T}(E1) { 0, 1, 13, 15, 45, 75, 97, 119, 137, 153, 167, 179, 189 }
% 45.81/46.06 808 : pppp71-{T}(E0) { 0, 13, 45, 75, 97, 119, 137, 153, 167, 179, 189 }
% 45.81/46.06 809 : pppp72-{T}(E1) { 0, 1, 13, 15, 45, 75, 97, 119, 137, 153, 167, 179, 189 }
% 45.81/46.06 810 : pppp71-{T}(E1) { 0, 1, 13, 15, 45, 75, 97, 119, 137, 153, 167, 179, 189 }
% 45.81/46.06 811 : pppp74-{T}(E0,E1) { 0, 1, 13, 45, 75, 97, 119, 137, 153, 167, 179, 190 }
% 45.81/46.06 812 : pppp19-{T}(E1,E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191 }
% 45.81/46.06 813 : pppp18-{T}(E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191 }
% 45.81/46.06 814 : pppp17-{T}(E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191 }
% 45.81/46.06 815 : pppp18-{T}(E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191 }
% 45.81/46.06 816 : pppp16-{T}(E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191 }
% 45.81/46.06 817 : pppp17-{T}(E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191 }
% 45.81/46.06 818 : pppp16-{T}(E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191 }
% 45.81/46.06 819 : pppp19-{T}(E1,E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169, 181, 192 }
% 45.81/46.06 820 : pppp166-{T}(E1,E0) { 0, 1, 11, 42, 71, 93, 115, 133, 149, 163, 175, 185, 193 }
% 45.81/46.06 821 : pppp165-{T}(E0) { 0, 1, 11, 42, 71, 93, 115, 133, 149, 163, 175, 185, 193 }
% 45.81/46.06 822 : pppp165-{T}(E1) { 0, 1, 11, 42, 71, 93, 115, 133, 149, 163, 175, 185, 193 }
% 45.81/46.06 823 : pppp164-{T}(E0) { 0, 1, 11, 42, 71, 93, 115, 133, 149, 163, 175, 185, 193 }
% 45.81/46.06 824 : pppp164-{T}(E1) { 0, 1, 11, 42, 71, 93, 115, 133, 149, 163, 175, 185, 193 }
% 45.81/46.06 825 : pppp163-{T}(E0) { 0, 1, 11, 42, 71, 93, 115, 133, 149, 163, 175, 185, 193 }
% 45.81/46.06 826 : pppp163-{T}(E1) { 0, 1, 11, 42, 71, 93, 115, 133, 149, 163, 175, 185, 193 }
% 45.81/46.06 827 : pppp166-{T}(E0,E1) { 0, 1, 11, 15, 42, 71, 93, 115, 133, 149, 163, 175, 185, 194 }
% 45.81/46.06 828 : pppp120-{T}(E0,E1) { 0, 12, 43, 73, 95, 117, 135, 151, 165, 177, 187, 195 }
% 45.81/46.06 829 : pppp119-{T}(E0) { 0, 12, 43, 73, 95, 117, 135, 151, 165, 177, 187, 195 }
% 45.81/46.06 830 : pppp118-{T}(E0) { 0, 12, 43, 73, 95, 117, 135, 151, 165, 177, 187, 195 }
% 45.81/46.06 831 : pppp119-{T}(E1) { 0, 1, 12, 15, 43, 73, 95, 117, 135, 151, 165, 177, 187, 195 }
% 45.81/46.06 832 : pppp117-{T}(E0) { 0, 12, 43, 73, 95, 117, 135, 151, 165, 177, 187, 195 }
% 45.81/46.06 833 : pppp118-{T}(E1) { 0, 1, 12, 15, 43, 73, 95, 117, 135, 151, 165, 177, 187, 195 }
% 45.81/46.06 834 : pppp117-{T}(E1) { 0, 1, 12, 15, 43, 73, 95, 117, 135, 151, 165, 177, 187, 195 }
% 45.81/46.06 835 : pppp448-{T}(E0) { 0, 1, 12, 43, 73, 95, 117, 135, 151, 165, 177, 187, 195 }
% 45.81/46.06 836 : pppp448-{T}(E1) { 0, 1, 12, 15, 43, 73, 95, 117, 135, 151, 165, 177, 187, 195 }
% 45.81/46.06 837 : pppp120-{T}(E1,E0) { 0, 1, 12, 43, 73, 95, 117, 135, 151, 165, 177, 187, 196 }
% 45.81/46.06 838 : pppp70-{T}(E0,E1) { 0, 13, 45, 75, 97, 119, 137, 153, 167, 179, 189, 197 }
% 45.81/46.06 839 : pppp69-{T}(E1) { 0, 13, 45, 75, 97, 119, 137, 153, 167, 179, 189, 197 }
% 45.81/46.06 840 : pppp68-{T}(E1) { 0, 13, 45, 75, 97, 119, 137, 153, 167, 179, 189, 197 }
% 45.81/46.06 841 : pppp69-{T}(E0) { 0, 1, 13, 45, 75, 97, 119, 137, 153, 167, 179, 189, 197 }
% 45.81/46.06 842 : pppp67-{T}(E1) { 0, 13, 45, 75, 97, 119, 137, 153, 167, 179, 189, 197 }
% 45.81/46.06 843 : pppp68-{T}(E0) { 0, 1, 13, 45, 75, 97, 119, 137, 153, 167, 179, 189, 197 }
% 45.81/46.06 844 : pppp67-{T}(E0) { 0, 1, 13, 45, 75, 97, 119, 137, 153, 167, 179, 189, 197 }
% 45.81/46.06 845 : pppp70-{T}(E1,E1) { 0, 1, 13, 15, 45, 75, 97, 119, 137, 153, 167, 179, 189, 198 }
% 45.81/46.06 846 : pppp15-{T}(E1,E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199 }
% 45.81/46.06 847 : pppp14-{T}(E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199 }
% 45.81/46.06 848 : pppp13-{T}(E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199 }
% 45.81/46.06 849 : pppp14-{T}(E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199 }
% 45.81/46.06 850 : pppp12-{T}(E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199 }
% 45.81/46.06 851 : pppp13-{T}(E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199 }
% 45.81/46.06 852 : pppp12-{T}(E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199 }
% 45.81/46.06 853 : pppp15-{T}(E1,E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 200 }
% 45.81/46.06 854 : pppp116-{T}(E0,E1) { 0, 1, 12, 43, 73, 95, 117, 135, 151, 165, 177, 187, 195, 201 }
% 45.81/46.06 855 : pppp115-{T}(E0) { 0, 1, 12, 43, 73, 95, 117, 135, 151, 165, 177, 187, 195, 201 }
% 45.81/46.06 856 : pppp115-{T}(E1) { 0, 1, 12, 43, 73, 95, 117, 135, 151, 165, 177, 187, 195, 201 }
% 45.81/46.06 857 : pppp114-{T}(E0) { 0, 1, 12, 43, 73, 95, 117, 135, 151, 165, 177, 187, 195, 201 }
% 45.81/46.06 858 : pppp114-{T}(E1) { 0, 1, 12, 43, 73, 95, 117, 135, 151, 165, 177, 187, 195, 201 }
% 45.81/46.06 859 : pppp113-{T}(E0) { 0, 1, 12, 43, 73, 95, 117, 135, 151, 165, 177, 187, 195, 201 }
% 45.81/46.06 860 : pppp113-{T}(E1) { 0, 1, 12, 43, 73, 95, 117, 135, 151, 165, 177, 187, 195, 201 }
% 45.81/46.06 861 : pppp116-{T}(E1,E1) { 0, 1, 12, 15, 43, 73, 95, 117, 135, 151, 165, 177, 187, 195, 202 }
% 45.81/46.06 862 : pppp66-{T}(E1,E0) { 0, 13, 45, 75, 97, 119, 137, 153, 167, 179, 189, 197, 203 }
% 45.81/46.06 863 : pppp65-{T}(E0) { 0, 13, 45, 75, 97, 119, 137, 153, 167, 179, 189, 197, 203 }
% 45.81/46.06 864 : pppp64-{T}(E0) { 0, 13, 45, 75, 97, 119, 137, 153, 167, 179, 189, 197, 203 }
% 45.81/46.06 865 : pppp65-{T}(E1) { 0, 1, 13, 15, 45, 75, 97, 119, 137, 153, 167, 179, 189, 197, 203 }
% 45.81/46.06 866 : pppp63-{T}(E0) { 0, 13, 45, 75, 97, 119, 137, 153, 167, 179, 189, 197, 203 }
% 45.81/46.06 867 : pppp64-{T}(E1) { 0, 1, 13, 15, 45, 75, 97, 119, 137, 153, 167, 179, 189, 197, 203 }
% 45.81/46.06 868 : pppp63-{T}(E1) { 0, 1, 13, 15, 45, 75, 97, 119, 137, 153, 167, 179, 189, 197, 203 }
% 45.81/46.06 869 : pppp449-{T}(E1) { 0, 1, 13, 15, 45, 75, 97, 119, 137, 153, 167, 179, 189, 197, 203 }
% 45.81/46.06 870 : pppp449-{T}(E0) { 0, 1, 13, 45, 75, 97, 119, 137, 153, 167, 179, 189, 197, 203 }
% 45.81/46.06 871 : pppp66-{T}(E0,E1) { 0, 1, 13, 45, 75, 97, 119, 137, 153, 167, 179, 189, 197, 204 }
% 45.81/46.06 872 : pppp11-{T}(E1,E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 205 }
% 45.81/46.06 873 : pppp10-{T}(E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 205 }
% 45.81/46.06 874 : pppp9-{T}(E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 205 }
% 45.81/46.06 875 : pppp10-{T}(E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 205 }
% 45.81/46.06 876 : pppp8-{T}(E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 205 }
% 45.81/46.06 877 : pppp9-{T}(E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 205 }
% 45.81/46.06 878 : pppp8-{T}(E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 205 }
% 45.81/46.06 879 : pppp11-{T}(E1,E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 206 }
% 45.81/46.06 880 : pppp62-{T}(E0,E0) { 0, 1, 13, 45, 75, 97, 119, 137, 153, 167, 179, 189, 197, 203, 207 }
% 45.81/46.06 881 : pppp61-{T}(E0) { 0, 1, 13, 45, 75, 97, 119, 137, 153, 167, 179, 189, 197, 203, 207 }
% 45.81/46.06 882 : pppp60-{T}(E0) { 0, 1, 13, 45, 75, 97, 119, 137, 153, 167, 179, 189, 197, 203, 207 }
% 45.81/46.06 883 : pppp61-{T}(E1) { 0, 1, 13, 15, 45, 75, 97, 119, 137, 153, 167, 179, 189, 197, 203, 207 }
% 45.81/46.06 884 : pppp59-{T}(E0) { 0, 1, 13, 45, 75, 97, 119, 137, 153, 167, 179, 189, 197, 203, 207 }
% 45.81/46.06 885 : pppp60-{T}(E1) { 0, 1, 13, 15, 45, 75, 97, 119, 137, 153, 167, 179, 189, 197, 203, 207 }
% 45.81/46.06 886 : pppp59-{T}(E1) { 0, 1, 13, 15, 45, 75, 97, 119, 137, 153, 167, 179, 189, 197, 203, 207 }
% 45.81/46.06 887 : pppp62-{T}(E1,E1) { 0, 1, 13, 15, 45, 75, 97, 119, 137, 153, 167, 179, 189, 197, 203, 208 }
% 45.81/46.06 888 : pppp7-{T}(E1,E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 205, 209 }
% 45.81/46.06 889 : pppp6-{T}(E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 205, 209 }
% 45.81/46.06 890 : pppp5-{T}(E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 205, 209 }
% 45.81/46.06 891 : pppp6-{T}(E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 205, 209 }
% 45.81/46.06 892 : pppp4-{T}(E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 205, 209 }
% 45.81/46.06 893 : pppp5-{T}(E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 205, 209 }
% 45.81/46.08 894 : pppp4-{T}(E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 205, 209 }
% 45.81/46.08 895 : pppp7-{T}(E1,E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 205, 210 }
% 45.81/46.08 896 : pppp450-{T}(E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 205, 209, 211 }
% 45.81/46.08 897 : pppp450-{T}(E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 205, 209, 212 }
% 45.81/46.08 898 : pppp3-{T}(E1,E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 205, 209, 211, 213 }
% 45.81/46.08 899 : pppp2-{T}(E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 205, 209, 211, 213 }
% 45.81/46.08 900 : pppp1-{T}(E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 205, 209, 211, 213 }
% 45.81/46.08 901 : pppp2-{T}(E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 205, 209, 211, 213 }
% 45.81/46.08 902 : pppp0-{T}(E1) { 0, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 205, 209, 211, 213 }
% 45.81/46.08 903 : pppp1-{T}(E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 205, 209, 211, 213 }
% 45.81/46.08 904 : pppp0-{T}(E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 205, 209, 211, 213 }
% 45.81/46.08 905 : pppp3-{T}(E0,E0) { 0, 1, 14, 46, 77, 99, 121, 139, 155, 169, 181, 191, 199, 205, 209, 212, 214 }
% 45.81/46.08
% 45.81/46.08
% 45.81/46.08 % SZS output end Model for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 45.81/46.08
% 45.81/46.08 randbase = 1
%------------------------------------------------------------------------------