%------------------------------------------------------------------------------
% File : Geo-III---2018C
% Problem : LCL675+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : geo -tptp_input -nonempty -inputfile %s
% Computer : n028.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:48 PM UTC 2026
% Result : CounterSatisfiable 92.66s 92.94s
% Output : Model 92.66s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL675+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : geo -tptp_input -nonempty -inputfile %s
% 0.11/0.36 % Computer : n028.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Fri Sep 4 21:29:58 UTC 2026
% 0.11/0.36 % CPUTime :
% 92.66/92.94 GeoParameters:
% 92.66/92.94
% 92.66/92.94 tptp_input = 1
% 92.66/92.94 tptp_output = 0
% 92.66/92.94 nonempty = 1
% 92.66/92.94 inputfile = /export/starexec/sandbox2/benchmark/theBenchmark.p
% 92.66/92.94 includepath = /export/starexec/sandbox2/solver/bin/../../benchmark/
% 92.66/92.94
% 92.66/92.94
% 92.66/92.94 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 92.66/92.94 % SZS output start Model for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 92.66/92.94
% 92.66/92.94 Interpretation 1014:
% 92.66/92.94 Guesses:
% 92.66/92.94 0 : guesser 2, 1, ( | 1, 0 ), 0, 1m32s old, 0 lemmas
% 92.66/92.94 1 : guesser 9, 7, ( | 0, 2, 1 ), 2, 1m32s old, 0 lemmas
% 92.66/92.94 2 : guesser 17, 15, ( 0 | 2, 1 ), 5, 1m32s old, 1 lemmas
% 92.66/92.94 3 : guesser 26, 23, ( 1, 0 | 3, 2 ), 8, 1m32s old, 2 lemmas
% 92.66/92.94 4 : guesser 39, 35, ( 3, 2, 1 | 4, 0 ), 22, 1m32s old, 4 lemmas
% 92.66/92.94 5 : guesser 51, 46, ( 3, 0, 2, 4 | 5, 1 ), 57, 1m32s old, 2 lemmas
% 92.66/92.94 6 : guesser 63, 57, ( 1, 0, 5, 4, 3 | 6, 2 ), 60, 1m31s old, 4 lemmas
% 92.66/92.94 7 : guesser 74, 67, ( 0, 4, 1, 5, 2, 6 | 7, 3 ), 64, 1m31s old, 6 lemmas
% 92.66/92.94 8 : guesser 90, 82, ( 6, 5, 4, 3, 2, 1, 0 | 8, 7 ), 165, 1m29s old, 5 lemmas
% 92.66/92.94 9 : guesser 105, 96, ( 6, 5, 4, 3, 2, 1, 0, 8 | 9, 7 ), 239, 1m27s old, 6 lemmas
% 92.66/92.94 10 : guesser 120, 110, ( 2, 9, 6, 3, 0, 7, 4, 1, 8 | 10, 5 ), 245, 1m27s old, 7 lemmas
% 92.66/92.94 11 : guesser 134, 123, ( 0, 8, 5, 2, 10, 7, 4, 1, 9, 6 | 11, 3 ), 252, 1m27s old, 7 lemmas
% 92.66/92.94 12 : guesser 149, 137, ( 7, 6, 5, 4, 3, 2, 1, 0, 11, 10, 9 | 12, 8 ), 259, 1m27s old, 8 lemmas
% 92.66/92.94 13 : guesser 163, 150, ( 2, 12, 9, 6, 3, 0, 10, 7, 4, 1, 11, 8 | 13, 5 ), 266, 1m27s old, 6 lemmas
% 92.66/92.94 14 : guesser 177, 163, ( 1, 12, 9, 6, 3, 0, 11, 8, 5, 2, 13, 10, 7 | 14, 4 ), 272, 1m27s old, 7 lemmas
% 92.66/92.94 15 : guesser 190, 175, ( 11, 13, 0, 2, 4, 6, 8, 10, 12, 14, 1, 3, 5, 7 | 15, 9 ), 279, 1m27s old, 8 lemmas
% 92.66/92.94 16 : guesser 209, 193, ( 4, 11, 2, 9, 0, 7, 14, 5, 12, 3, 10, 1, 8, 15, 6 | 16, 13 ), 394, 1m20s old, 7 lemmas
% 92.66/92.94 17 : guesser 227, 210, ( 5, 16, 10, 4, 15, 9, 3, 14, 8, 2, 13, 7, 1, 12, 6, 0 | 17, 11 ), 645, 1m3s old, 8 lemmas
% 92.66/92.94 18 : guesser 245, 227, ( 16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0 | 18, 17 ), 653, 1m3s old, 7 lemmas
% 92.66/92.94 19 : guesser 262, 243, ( 7, 1, 14, 8, 2, 15, 9, 3, 16, 10, 4, 17, 11, 5, 18, 12, 6, 0 | 19, 13 ), 660, 1m3s old, 7 lemmas
% 92.66/92.94 20 : guesser 280, 260, ( 2, 9, 16, 3, 10, 17, 4, 11, 18, 5, 12, 19, 6, 13, 0, 7, 14, 1, 8 | 20, 15 ), 667, 1m2s old, 8 lemmas
% 92.66/92.94 21 : guesser 297, 276, ( 16, 6, 17, 7, 18, 8, 19, 9, 20, 10, 0, 11, 1, 12, 2, 13, 3, 14, 4, 15 | 21, 5 ), 675, 1m2s old, 8 lemmas
% 92.66/92.94 22 : guesser 314, 292, ( 17, 14, 11, 8, 5, 2, 21, 18, 15, 12, 9, 6, 3, 0, 19, 16, 13, 10, 7, 4, 1 | 22, 20 ), 683, 1m2s old, 9 lemmas
% 92.66/92.94 23 : guesser 330, 307, ( 11, 13, 15, 17, 19, 21, 0, 2, 4, 6, 8, 10, 12, 14, 16, 18, 20, 22, 1, 3, 5, 7 | 23, 9 ), 692, 1m1s old, 7 lemmas
% 92.66/92.94 24 : guesser 348, 324, ( 1, 0, 23, 22, 21, 20, 19, 18, 17, 16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3 | 24, 2 ), 699, 1m1s old, 8 lemmas
% 92.66/92.94 25 : guesser 365, 340, ( 6, 13, 20, 2, 9, 16, 23, 5, 12, 19, 1, 8, 15, 22, 4, 11, 18, 0, 7, 14, 21, 3, 10, 17 | 25, 24 ), 707, 1m0s old, 11 lemmas
% 92.66/92.94 26 : guesser 382, 356, ( 18, 15, 12, 9, 6, 3, 0, 23, 20, 17, 14, 11, 8, 5, 2, 25, 22, 19, 16, 13, 10, 7, 4, 1, 24 | 26, 21 ), 718, 59s old, 9 lemmas
% 92.66/92.94 27 : guesser 398, 371, ( 15, 5, 22, 12, 2, 19, 9, 26, 16, 6, 23, 13, 3, 20, 10, 0, 17, 7, 24, 14, 4, 21, 11, 1, 18, 8 | 27, 25 ), 727, 59s old, 8 lemmas
% 92.66/92.94 28 : guesser 415, 387, ( 7, 18, 1, 12, 23, 6, 17, 0, 11, 22, 5, 16, 27, 10, 21, 4, 15, 26, 9, 20, 3, 14, 25, 8, 19, 2, 13 | 28, 24 ), 735, 58s old, 9 lemmas
% 92.66/92.94 29 : guesser 431, 402, ( 11, 13, 15, 17, 19, 21, 23, 25, 27, 0, 2, 4, 6, 8, 10, 12, 14, 16, 18, 20, 22, 24, 26, 28, 1, 3, 5, 7 | 29, 9 ), 744, 57s old, 8 lemmas
% 92.66/92.94 30 : guesser 447, 417, ( 8, 25, 12, 29, 16, 3, 20, 7, 24, 11, 28, 15, 2, 19, 6, 23, 10, 27, 14, 1, 18, 5, 22, 9, 26, 13, 0, 17, 4 | 30, 21 ), 752, 57s old, 8 lemmas
% 92.66/92.94 31 : guesser 462, 431, ( 7, 1, 26, 20, 14, 8, 2, 27, 21, 15, 9, 3, 28, 22, 16, 10, 4, 29, 23, 17, 11, 5, 30, 24, 18, 12, 6, 0, 25, 19 | 31, 13 ), 760, 56s old, 9 lemmas
% 92.66/92.94 32 : guesser 482, 450, ( 28, 19, 10, 1, 24, 15, 6, 29, 20, 11, 2, 25, 16, 7, 30, 21, 12, 3, 26, 17, 8, 31, 22, 13, 4, 27, 18, 9, 0, 23, 14 | 32, 5 ), 769, 55s old, 7 lemmas
% 92.66/92.94 33 : guesser 501, 468, ( 23, 31, 6, 14, 22, 30, 5, 13, 21, 29, 4, 12, 20, 28, 3, 11, 19, 27, 2, 10, 18, 26, 1, 9, 17, 25, 0, 8, 16, 24, 32, 7 | 33, 15 ), 775, 55s old, 8 lemmas
% 92.66/92.94 34 : guesser 520, 486, ( 21, 32, 9, 20, 31, 8, 19, 30, 7, 18, 29, 6, 17, 28, 5, 16, 27, 4, 15, 26, 3, 14, 25, 2, 13, 24, 1, 12, 23, 0, 11, 22, 33 | 34, 10 ), 782, 54s old, 9 lemmas
% 92.66/92.94 35 : guesser 538, 503, ( 14, 11, 8, 5, 2, 34, 31, 28, 25, 22, 19, 16, 13, 10, 7, 4, 1, 33, 30, 27, 24, 21, 18, 15, 12, 9, 6, 3, 0, 32, 29, 26, 23, 20 | 35, 17 ), 789, 53s old, 10 lemmas
% 92.66/92.94 36 : guesser 557, 521, ( 18, 17, 16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0, 35, 34, 33, 32, 31, 30, 29, 28, 27, 26, 25, 24, 23, 22, 21, 20 | 36, 19 ), 798, 52s old, 9 lemmas
% 92.66/92.94 37 : guesser 575, 538, ( 12, 29, 9, 26, 6, 23, 3, 20, 0, 17, 34, 14, 31, 11, 28, 8, 25, 5, 22, 2, 19, 36, 16, 33, 13, 30, 10, 27, 7, 24, 4, 21, 1, 18, 35, 15 | 37, 32 ), 805, 51s old, 9 lemmas
% 92.66/92.94 38 : guesser 593, 555, ( 28, 3, 16, 29, 4, 17, 30, 5, 18, 31, 6, 19, 32, 7, 20, 33, 8, 21, 34, 9, 22, 35, 10, 23, 36, 11, 24, 37, 12, 25, 0, 13, 26, 1, 14, 27, 2 | 38, 15 ), 813, 50s old, 9 lemmas
% 92.66/92.94 39 : guesser 610, 571, ( 38, 22, 6, 29, 13, 36, 20, 4, 27, 11, 34, 18, 2, 25, 9, 32, 16, 0, 23, 7, 30, 14, 37, 21, 5, 28, 12, 35, 19, 3, 26, 10, 33, 17, 1, 24, 8, 31 | 39, 15 ), 821, 49s old, 10 lemmas
% 92.66/92.94 40 : guesser 629, 589, ( 29, 36, 3, 10, 17, 24, 31, 38, 5, 12, 19, 26, 33, 0, 7, 14, 21, 28, 35, 2, 9, 16, 23, 30, 37, 4, 11, 18, 25, 32, 39, 6, 13, 20, 27, 34, 1, 8, 15 | 40, 22 ), 831, 48s old, 11 lemmas
% 92.66/92.94 41 : guesser 647, 606, ( 17, 20, 23, 26, 29, 32, 35, 38, 0, 3, 6, 9, 12, 15, 18, 21, 24, 27, 30, 33, 36, 39, 1, 4, 7, 10, 13, 16, 19, 22, 25, 28, 31, 34, 37, 40, 2, 5, 8, 11 | 41, 14 ), 841, 46s old, 9 lemmas
% 92.66/92.94 42 : guesser 665, 623, ( 30, 41, 10, 21, 32, 1, 12, 23, 34, 3, 14, 25, 36, 5, 16, 27, 38, 7, 18, 29, 40, 9, 20, 31, 0, 11, 22, 33, 2, 13, 24, 35, 4, 15, 26, 37, 6, 17, 28, 39, 8 | 42, 19 ), 849, 45s old, 12 lemmas
% 92.66/92.94 43 : guesser 682, 639, ( 0, 31, 19, 7, 38, 26, 14, 2, 33, 21, 9, 40, 28, 16, 4, 35, 23, 11, 42, 30, 18, 6, 37, 25, 13, 1, 32, 20, 8, 39, 27, 15, 3, 34, 22, 10, 41, 29, 17, 5, 36, 24 | 43, 12 ), 859, 43s old, 9 lemmas
% 92.66/92.94 44 : guesser 700, 656, ( 36, 11, 30, 5, 24, 43, 18, 37, 12, 31, 6, 25, 0, 19, 38, 13, 32, 7, 26, 1, 20, 39, 14, 33, 8, 27, 2, 21, 40, 15, 34, 9, 28, 3, 22, 41, 16, 35, 10, 29, 4, 23, 42 | 44, 17 ), 868, 42s old, 7 lemmas
% 92.66/92.94 45 : guesser 717, 672, ( 21, 38, 10, 27, 44, 16, 33, 5, 22, 39, 11, 28, 0, 17, 34, 6, 23, 40, 12, 29, 1, 18, 35, 7, 24, 41, 13, 30, 2, 19, 36, 8, 25, 42, 14, 31, 3, 20, 37, 9, 26, 43, 15, 32 | 45, 4 ), 874, 41s old, 10 lemmas
% 92.66/92.94 46 : guesser 734, 688, ( 4, 29, 8, 33, 12, 37, 16, 41, 20, 45, 24, 3, 28, 7, 32, 11, 36, 15, 40, 19, 44, 23, 2, 27, 6, 31, 10, 35, 14, 39, 18, 43, 22, 1, 26, 5, 30, 9, 34, 13, 38, 17, 42, 21, 0 | 46, 25 ), 882, 39s old, 10 lemmas
% 92.66/92.94 47 : guesser 750, 703, ( 0, 43, 39, 35, 31, 27, 23, 19, 15, 11, 7, 3, 46, 42, 38, 34, 30, 26, 22, 18, 14, 10, 6, 2, 45, 41, 37, 33, 29, 25, 21, 17, 13, 9, 5, 1, 44, 40, 36, 32, 28, 24, 20, 16, 12, 8 | 47, 4 ), 891, 37s old, 11 lemmas
% 92.66/92.94 48 : guesser 769, 721, ( 20, 43, 18, 41, 16, 39, 14, 37, 12, 35, 10, 33, 8, 31, 6, 29, 4, 27, 2, 25, 0, 23, 46, 21, 44, 19, 42, 17, 40, 15, 38, 13, 36, 11, 34, 9, 32, 7, 30, 5, 28, 3, 26, 1, 24, 47, 22 | 48, 45 ), 900, 35s old, 8 lemmas
% 92.66/92.94 49 : guesser 787, 738, ( 48, 10, 21, 32, 43, 5, 16, 27, 38, 0, 11, 22, 33, 44, 6, 17, 28, 39, 1, 12, 23, 34, 45, 7, 18, 29, 40, 2, 13, 24, 35, 46, 8, 19, 30, 41, 3, 14, 25, 36, 47, 9, 20, 31, 42, 4, 15, 26 | 49, 37 ), 907, 34s old, 8 lemmas
% 92.66/92.94 50 : guesser 805, 755, ( 5, 12, 19, 26, 33, 40, 47, 4, 11, 18, 25, 32, 39, 46, 3, 10, 17, 24, 31, 38, 45, 2, 9, 16, 23, 30, 37, 44, 1, 8, 15, 22, 29, 36, 43, 0, 7, 14, 21, 28, 35, 42, 49, 6, 13, 20, 27, 34, 41 | 50, 48 ), 915, 32s old, 7 lemmas
% 92.66/92.94 51 : guesser 822, 771, ( 37, 48, 8, 19, 30, 41, 1, 12, 23, 34, 45, 5, 16, 27, 38, 49, 9, 20, 31, 42, 2, 13, 24, 35, 46, 6, 17, 28, 39, 50, 10, 21, 32, 43, 3, 14, 25, 36, 47, 7, 18, 29, 40, 0, 11, 22, 33, 44, 4, 15 | 51, 26 ), 919, 31s old, 8 lemmas
% 92.66/92.94 52 : guesser 840, 788, ( 21, 44, 15, 38, 9, 32, 3, 26, 49, 20, 43, 14, 37, 8, 31, 2, 25, 48, 19, 42, 13, 36, 7, 30, 1, 24, 47, 18, 41, 12, 35, 6, 29, 0, 23, 46, 17, 40, 11, 34, 5, 28, 51, 22, 45, 16, 39, 10, 33, 4, 27 | 52, 50 ), 928, 29s old, 7 lemmas
% 92.66/92.94 53 : guesser 857, 804, ( 26, 16, 6, 49, 39, 29, 19, 9, 52, 42, 32, 22, 12, 2, 45, 35, 25, 15, 5, 48, 38, 28, 18, 8, 51, 41, 31, 21, 11, 1, 44, 34, 24, 14, 4, 47, 37, 27, 17, 7, 50, 40, 30, 20, 10, 0, 43, 33, 23, 13, 3, 46 | 53, 36 ), 934, 27s old, 10 lemmas
% 92.66/92.94 54 : guesser 874, 820, ( 32, 49, 12, 29, 46, 9, 26, 43, 6, 23, 40, 3, 20, 37, 0, 17, 34, 51, 14, 31, 48, 11, 28, 45, 8, 25, 42, 5, 22, 39, 2, 19, 36, 53, 16, 33, 50, 13, 30, 47, 10, 27, 44, 7, 24, 41, 4, 21, 38, 1, 18, 35, 52 | 54, 15 ), 942, 25s old, 7 lemmas
% 92.66/92.94 55 : guesser 890, 835, ( 28, 25, 22, 19, 16, 13, 10, 7, 4, 1, 53, 50, 47, 44, 41, 38, 35, 32, 29, 26, 23, 20, 17, 14, 11, 8, 5, 2, 54, 51, 48, 45, 42, 39, 36, 33, 30, 27, 24, 21, 18, 15, 12, 9, 6, 3, 0, 52, 49, 46, 43, 40, 37, 34 | 55, 31 ), 947, 23s old, 10 lemmas
% 92.66/92.94 56 : guesser 908, 852, ( 24, 7, 46, 29, 12, 51, 34, 17, 0, 39, 22, 5, 44, 27, 10, 49, 32, 15, 54, 37, 20, 3, 42, 25, 8, 47, 30, 13, 52, 35, 18, 1, 40, 23, 6, 45, 28, 11, 50, 33, 16, 55, 38, 21, 4, 43, 26, 9, 48, 31, 14, 53, 36, 19, 2 | 56, 41 ), 957, 20s old, 10 lemmas
% 92.66/92.94 57 : guesser 925, 868, ( 27, 2, 34, 9, 41, 16, 48, 23, 55, 30, 5, 37, 12, 44, 19, 51, 26, 1, 33, 8, 40, 15, 47, 22, 54, 29, 4, 36, 11, 43, 18, 50, 25, 0, 32, 7, 39, 14, 46, 21, 53, 28, 3, 35, 10, 42, 17, 49, 24, 56, 31, 6, 38, 13, 45, 20 | 57, 52 ), 967, 17s old, 9 lemmas
% 92.66/92.94 58 : guesser 942, 884, ( 17, 48, 21, 52, 25, 56, 29, 2, 33, 6, 37, 10, 41, 14, 45, 18, 49, 22, 53, 26, 57, 30, 3, 34, 7, 38, 11, 42, 15, 46, 19, 50, 23, 54, 27, 0, 31, 4, 35, 8, 39, 12, 43, 16, 47, 20, 51, 24, 55, 28, 1, 32, 5, 36, 9, 40, 13 | 58, 44 ), 975, 14s old, 8 lemmas
% 92.66/92.94 59 : guesser 958, 899, ( 9, 45, 22, 58, 35, 12, 48, 25, 2, 38, 15, 51, 28, 5, 41, 18, 54, 31, 8, 44, 21, 57, 34, 11, 47, 24, 1, 37, 14, 50, 27, 4, 40, 17, 53, 30, 7, 43, 20, 56, 33, 10, 46, 23, 0, 36, 13, 49, 26, 3, 39, 16, 52, 29, 6, 42, 19, 55 | 59, 32 ), 982, 12s old, 8 lemmas
% 92.66/92.94 60 : guesser 975, 915, ( 50, 37, 24, 11, 58, 45, 32, 19, 6, 53, 40, 27, 14, 1, 48, 35, 22, 9, 56, 43, 30, 17, 4, 51, 38, 25, 12, 59, 46, 33, 20, 7, 54, 41, 28, 15, 2, 49, 36, 23, 10, 57, 44, 31, 18, 5, 52, 39, 26, 13, 0, 47, 34, 21, 8, 55, 42, 29, 16 | 60, 3 ), 990, 8s old, 7 lemmas
% 92.66/92.94 61 : guesser 991, 930, ( 55, 58, 0, 3, 6, 9, 12, 15, 18, 21, 24, 27, 30, 33, 36, 39, 42, 45, 48, 51, 54, 57, 60, 2, 5, 8, 11, 14, 17, 20, 23, 26, 29, 32, 35, 38, 41, 44, 47, 50, 53, 56, 59, 1, 4, 7, 10, 13, 16, 19, 22, 25, 28, 31, 34, 37, 40, 43, 46, 49 | 61, 52 ), 997, 6s old, 9 lemmas
% 92.66/92.94 62 : guesser 1007, 945, ( 30, 55, 18, 43, 6, 31, 56, 19, 44, 7, 32, 57, 20, 45, 8, 33, 58, 21, 46, 9, 34, 59, 22, 47, 10, 35, 60, 23, 48, 11, 36, 61, 24, 49, 12, 37, 0, 25, 50, 13, 38, 1, 26, 51, 14, 39, 2, 27, 52, 15, 40, 3, 28, 53, 16, 41, 4, 29, 54, 17, 42 | 62, 5 ), 1007, 2s old, 7 lemmas
% 92.66/92.94
% 92.66/92.94 Elements:
% 92.66/92.94 { E0, E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30, E31, E32, E33, E34, E35, E36, E37, E38, E39, E40, E41, E42, E43, E44, E45, E46, E47, E48, E49, E50, E51, E52, E53, E54, E55, E56, E57, E58, E59, E60, E61, E62 }
% 92.66/92.94
% 92.66/92.94 Atoms:
% 92.66/92.94 0 : #-{T} E0 { }
% 92.66/92.94 1 : r1-{T}(E0,E0) { }
% 92.66/92.94 2 : #-{T} E1 { 0 }
% 92.66/92.94 3 : pppp11-{T}(E1) { 0 }
% 92.66/92.94 4 : r1-{T}(E1,E1) { 0 }
% 92.66/92.94 5 : p100-{T}(E1) { 0 }
% 92.66/92.94 6 : pppp10-{T}(E1) { 0 }
% 92.66/92.94 7 : pppp12-{T}(E1) { 0 }
% 92.66/92.94 8 : pppp13-{T}(E1) { 0 }
% 92.66/92.94 9 : pppp9-{T}(E0,E1) { 0, 1 }
% 92.66/92.94 10 : p101-{T}(E0) { 0, 1 }
% 92.66/92.94 11 : p2-{T}(E0) { 0, 1 }
% 92.66/92.94 12 : r1-{T}(E1,E0) { 0, 1 }
% 92.66/92.94 13 : pppp10-{T}(E0) { 0, 1 }
% 92.66/92.94 14 : p100-{T}(E0) { 0, 1 }
% 92.66/92.94 15 : pppp14-{T}(E0) { 0, 1 }
% 92.66/92.94 16 : pppp15-{T}(E0) { 0, 1 }
% 92.66/92.94 17 : #-{T} E2 { 0, 2 }
% 92.66/92.94 18 : pppp8-{T}(E2,E1) { 0, 2 }
% 92.66/92.94 19 : r1-{T}(E2,E2) { 0, 2 }
% 92.66/92.94 20 : p101-{T}(E2) { 0, 2 }
% 92.66/92.94 21 : r1-{T}(E1,E2) { 0, 2 }
% 92.66/92.94 22 : pppp10-{T}(E2) { 0, 2 }
% 92.66/92.94 23 : p100-{T}(E2) { 0, 2 }
% 92.66/92.94 24 : pppp14-{T}(E2) { 0, 2 }
% 92.66/92.94 25 : pppp15-{T}(E2) { 0, 2 }
% 92.66/92.94 26 : #-{T} E3 { 0, 1, 3 }
% 92.66/92.94 27 : pppp7-{T}(E3,E0) { 0, 1, 3 }
% 92.66/92.94 28 : r1-{T}(E3,E3) { 0, 1, 3 }
% 92.66/92.94 29 : p102-{T}(E3) { 0, 1, 3 }
% 92.66/92.94 30 : p3-{T}(E3) { 0, 1, 3 }
% 92.66/92.94 31 : r1-{T}(E0,E3) { 0, 1, 3 }
% 92.66/92.94 32 : r1-{T}(E1,E3) { 0, 1, 3 }
% 92.66/92.94 33 : pppp10-{T}(E3) { 0, 1, 3 }
% 92.66/92.94 34 : p101-{T}(E3) { 0, 1, 3 }
% 92.66/92.94 35 : p100-{T}(E3) { 0, 1, 3 }
% 92.66/92.94 36 : p2-{T}(E3) { 0, 1, 3 }
% 92.66/92.94 37 : pppp16-{T}(E3) { 0, 1, 3 }
% 92.66/92.94 38 : pppp17-{T}(E3) { 0, 1, 3 }
% 92.66/92.94 39 : #-{T} E4 { 0, 1, 4 }
% 92.66/92.94 40 : pppp6-{T}(E4,E0) { 0, 1, 4 }
% 92.66/92.94 41 : r1-{T}(E4,E4) { 0, 1, 4 }
% 92.66/92.94 42 : p102-{T}(E4) { 0, 1, 4 }
% 92.66/92.94 43 : r1-{T}(E0,E4) { 0, 1, 4 }
% 92.66/92.94 44 : r1-{T}(E1,E4) { 0, 1, 4 }
% 92.66/92.94 45 : pppp10-{T}(E4) { 0, 1, 4 }
% 92.66/92.94 46 : p101-{T}(E4) { 0, 1, 4 }
% 92.66/92.94 47 : p100-{T}(E4) { 0, 1, 4 }
% 92.66/92.94 48 : p2-{T}(E4) { 0, 1, 4 }
% 92.66/92.94 49 : pppp16-{T}(E4) { 0, 1, 4 }
% 92.66/92.94 50 : pppp17-{T}(E4) { 0, 1, 4 }
% 92.66/92.94 51 : #-{T} E5 { 0, 2, 5 }
% 92.66/92.94 52 : pppp7-{T}(E5,E2) { 0, 2, 5 }
% 92.66/92.94 53 : r1-{T}(E5,E5) { 0, 2, 5 }
% 92.66/92.94 54 : p102-{T}(E5) { 0, 2, 5 }
% 92.66/92.94 55 : p3-{T}(E5) { 0, 2, 5 }
% 92.66/92.94 56 : r1-{T}(E2,E5) { 0, 2, 5 }
% 92.66/92.94 57 : r1-{T}(E1,E5) { 0, 2, 5 }
% 92.66/92.94 58 : pppp10-{T}(E5) { 0, 2, 5 }
% 92.66/92.94 59 : p101-{T}(E5) { 0, 2, 5 }
% 92.66/92.95 60 : pppp16-{T}(E5) { 0, 2, 5 }
% 92.66/92.95 61 : pppp17-{T}(E5) { 0, 2, 5 }
% 92.66/92.95 62 : p100-{T}(E5) { 0, 2, 5 }
% 92.66/92.95 63 : #-{T} E6 { 0, 2, 6 }
% 92.66/92.95 64 : pppp6-{T}(E6,E2) { 0, 2, 6 }
% 92.66/92.95 65 : r1-{T}(E6,E6) { 0, 2, 6 }
% 92.66/92.95 66 : p102-{T}(E6) { 0, 2, 6 }
% 92.66/92.95 67 : r1-{T}(E2,E6) { 0, 2, 6 }
% 92.66/92.95 68 : r1-{T}(E1,E6) { 0, 2, 6 }
% 92.66/92.95 69 : pppp10-{T}(E6) { 0, 2, 6 }
% 92.66/92.95 70 : p101-{T}(E6) { 0, 2, 6 }
% 92.66/92.95 71 : pppp16-{T}(E6) { 0, 2, 6 }
% 92.66/92.95 72 : pppp17-{T}(E6) { 0, 2, 6 }
% 92.66/92.95 73 : p100-{T}(E6) { 0, 2, 6 }
% 92.66/92.95 74 : #-{T} E7 { 0, 1, 3, 7 }
% 92.66/92.95 75 : pppp5-{T}(E7,E3) { 0, 1, 3, 7 }
% 92.66/92.95 76 : r1-{T}(E7,E7) { 0, 1, 3, 7 }
% 92.66/92.95 77 : p103-{T}(E7) { 0, 1, 3, 7 }
% 92.66/92.95 78 : p4-{T}(E7) { 0, 1, 3, 7 }
% 92.66/92.95 79 : r1-{T}(E3,E7) { 0, 1, 3, 7 }
% 92.66/92.95 80 : r1-{T}(E1,E7) { 0, 1, 3, 7 }
% 92.66/92.95 81 : r1-{T}(E0,E7) { 0, 1, 3, 7 }
% 92.66/92.95 82 : pppp10-{T}(E7) { 0, 1, 3, 7 }
% 92.66/92.95 83 : p102-{T}(E7) { 0, 1, 3, 7 }
% 92.66/92.95 84 : p101-{T}(E7) { 0, 1, 3, 7 }
% 92.66/92.95 85 : p3-{T}(E7) { 0, 1, 3, 7 }
% 92.66/92.95 86 : p100-{T}(E7) { 0, 1, 3, 7 }
% 92.66/92.95 87 : p2-{T}(E7) { 0, 1, 3, 7 }
% 92.66/92.95 88 : pppp18-{T}(E7) { 0, 1, 3, 7 }
% 92.66/92.95 89 : pppp19-{T}(E7) { 0, 1, 3, 7 }
% 92.66/92.95 90 : #-{T} E8 { 0, 1, 3, 8 }
% 92.66/92.95 91 : pppp4-{T}(E8,E3) { 0, 1, 3, 8 }
% 92.66/92.95 92 : r1-{T}(E8,E8) { 0, 1, 3, 8 }
% 92.66/92.95 93 : p103-{T}(E8) { 0, 1, 3, 8 }
% 92.66/92.95 94 : r1-{T}(E3,E8) { 0, 1, 3, 8 }
% 92.66/92.95 95 : r1-{T}(E1,E8) { 0, 1, 3, 8 }
% 92.66/92.95 96 : r1-{T}(E0,E8) { 0, 1, 3, 8 }
% 92.66/92.95 97 : pppp10-{T}(E8) { 0, 1, 3, 8 }
% 92.66/92.95 98 : p102-{T}(E8) { 0, 1, 3, 8 }
% 92.66/92.95 99 : pppp18-{T}(E8) { 0, 1, 3, 8 }
% 92.66/92.95 100 : p101-{T}(E8) { 0, 1, 3, 8 }
% 92.66/92.95 101 : p3-{T}(E8) { 0, 1, 3, 8 }
% 92.66/92.95 102 : p100-{T}(E8) { 0, 1, 3, 8 }
% 92.66/92.95 103 : p2-{T}(E8) { 0, 1, 3, 8 }
% 92.66/92.95 104 : pppp19-{T}(E8) { 0, 1, 3, 8 }
% 92.66/92.95 105 : #-{T} E9 { 0, 1, 4, 9 }
% 92.66/92.95 106 : pppp5-{T}(E9,E4) { 0, 1, 4, 9 }
% 92.66/92.95 107 : r1-{T}(E9,E9) { 0, 1, 4, 9 }
% 92.66/92.95 108 : p103-{T}(E9) { 0, 1, 4, 9 }
% 92.66/92.95 109 : p4-{T}(E9) { 0, 1, 4, 9 }
% 92.66/92.95 110 : r1-{T}(E4,E9) { 0, 1, 4, 9 }
% 92.66/92.95 111 : r1-{T}(E1,E9) { 0, 1, 4, 9 }
% 92.66/92.95 112 : r1-{T}(E0,E9) { 0, 1, 4, 9 }
% 92.66/92.95 113 : pppp10-{T}(E9) { 0, 1, 4, 9 }
% 92.66/92.95 114 : p102-{T}(E9) { 0, 1, 4, 9 }
% 92.66/92.95 115 : pppp18-{T}(E9) { 0, 1, 4, 9 }
% 92.66/92.95 116 : pppp19-{T}(E9) { 0, 1, 4, 9 }
% 92.66/92.95 117 : p101-{T}(E9) { 0, 1, 4, 9 }
% 92.66/92.95 118 : p100-{T}(E9) { 0, 1, 4, 9 }
% 92.66/92.95 119 : p2-{T}(E9) { 0, 1, 4, 9 }
% 92.66/92.95 120 : #-{T} E10 { 0, 1, 4, 10 }
% 92.66/92.95 121 : pppp4-{T}(E10,E4) { 0, 1, 4, 10 }
% 92.66/92.95 122 : r1-{T}(E10,E10) { 0, 1, 4, 10 }
% 92.66/92.95 123 : p103-{T}(E10) { 0, 1, 4, 10 }
% 92.66/92.95 124 : r1-{T}(E4,E10) { 0, 1, 4, 10 }
% 92.66/92.95 125 : r1-{T}(E1,E10) { 0, 1, 4, 10 }
% 92.66/92.95 126 : r1-{T}(E0,E10) { 0, 1, 4, 10 }
% 92.66/92.95 127 : pppp10-{T}(E10) { 0, 1, 4, 10 }
% 92.66/92.95 128 : p102-{T}(E10) { 0, 1, 4, 10 }
% 92.66/92.95 129 : pppp18-{T}(E10) { 0, 1, 4, 10 }
% 92.66/92.95 130 : pppp19-{T}(E10) { 0, 1, 4, 10 }
% 92.66/92.95 131 : p101-{T}(E10) { 0, 1, 4, 10 }
% 92.66/92.95 132 : p100-{T}(E10) { 0, 1, 4, 10 }
% 92.66/92.95 133 : p2-{T}(E10) { 0, 1, 4, 10 }
% 92.66/92.95 134 : #-{T} E11 { 0, 2, 5, 11 }
% 92.66/92.95 135 : pppp5-{T}(E11,E5) { 0, 2, 5, 11 }
% 92.66/92.95 136 : r1-{T}(E11,E11) { 0, 2, 5, 11 }
% 92.66/92.95 137 : p103-{T}(E11) { 0, 2, 5, 11 }
% 92.66/92.95 138 : p4-{T}(E11) { 0, 2, 5, 11 }
% 92.66/92.95 139 : r1-{T}(E5,E11) { 0, 2, 5, 11 }
% 92.66/92.95 140 : r1-{T}(E2,E11) { 0, 2, 5, 11 }
% 92.66/92.95 141 : r1-{T}(E1,E11) { 0, 2, 5, 11 }
% 92.66/92.95 142 : pppp10-{T}(E11) { 0, 2, 5, 11 }
% 92.66/92.95 143 : p102-{T}(E11) { 0, 2, 5, 11 }
% 92.66/92.95 144 : pppp18-{T}(E11) { 0, 2, 5, 11 }
% 92.66/92.95 145 : pppp19-{T}(E11) { 0, 2, 5, 11 }
% 92.66/92.95 146 : p101-{T}(E11) { 0, 2, 5, 11 }
% 92.66/92.95 147 : p3-{T}(E11) { 0, 2, 5, 11 }
% 92.66/92.95 148 : p100-{T}(E11) { 0, 2, 5, 11 }
% 92.66/92.95 149 : #-{T} E12 { 0, 2, 5, 12 }
% 92.66/92.95 150 : pppp4-{T}(E12,E5) { 0, 2, 5, 12 }
% 92.66/92.95 151 : r1-{T}(E12,E12) { 0, 2, 5, 12 }
% 92.66/92.95 152 : p103-{T}(E12) { 0, 2, 5, 12 }
% 92.66/92.95 153 : r1-{T}(E5,E12) { 0, 2, 5, 12 }
% 92.66/92.95 154 : r1-{T}(E1,E12) { 0, 2, 5, 12 }
% 92.66/92.95 155 : r1-{T}(E2,E12) { 0, 2, 5, 12 }
% 92.66/92.95 156 : pppp10-{T}(E12) { 0, 2, 5, 12 }
% 92.66/92.95 157 : p102-{T}(E12) { 0, 2, 5, 12 }
% 92.66/92.95 158 : pppp18-{T}(E12) { 0, 2, 5, 12 }
% 92.66/92.95 159 : pppp19-{T}(E12) { 0, 2, 5, 12 }
% 92.66/92.95 160 : p101-{T}(E12) { 0, 2, 5, 12 }
% 92.66/92.95 161 : p3-{T}(E12) { 0, 2, 5, 12 }
% 92.66/92.95 162 : p100-{T}(E12) { 0, 2, 5, 12 }
% 92.66/92.95 163 : #-{T} E13 { 0, 2, 6, 13 }
% 92.66/92.95 164 : pppp5-{T}(E13,E6) { 0, 2, 6, 13 }
% 92.66/92.95 165 : r1-{T}(E13,E13) { 0, 2, 6, 13 }
% 92.66/92.95 166 : p103-{T}(E13) { 0, 2, 6, 13 }
% 92.66/92.95 167 : p4-{T}(E13) { 0, 2, 6, 13 }
% 92.66/92.95 168 : r1-{T}(E6,E13) { 0, 2, 6, 13 }
% 92.66/92.95 169 : r1-{T}(E1,E13) { 0, 2, 6, 13 }
% 92.66/92.95 170 : r1-{T}(E2,E13) { 0, 2, 6, 13 }
% 92.66/92.95 171 : pppp10-{T}(E13) { 0, 2, 6, 13 }
% 92.66/92.95 172 : p102-{T}(E13) { 0, 2, 6, 13 }
% 92.66/92.95 173 : pppp18-{T}(E13) { 0, 2, 6, 13 }
% 92.66/92.95 174 : pppp19-{T}(E13) { 0, 2, 6, 13 }
% 92.66/92.95 175 : p101-{T}(E13) { 0, 2, 6, 13 }
% 92.66/92.95 176 : p100-{T}(E13) { 0, 2, 6, 13 }
% 92.66/92.95 177 : #-{T} E14 { 0, 2, 6, 14 }
% 92.66/92.95 178 : pppp4-{T}(E14,E6) { 0, 2, 6, 14 }
% 92.66/92.95 179 : r1-{T}(E14,E14) { 0, 2, 6, 14 }
% 92.66/92.95 180 : p103-{T}(E14) { 0, 2, 6, 14 }
% 92.66/92.95 181 : r1-{T}(E6,E14) { 0, 2, 6, 14 }
% 92.66/92.95 182 : r1-{T}(E2,E14) { 0, 2, 6, 14 }
% 92.66/92.95 183 : r1-{T}(E1,E14) { 0, 2, 6, 14 }
% 92.66/92.95 184 : pppp10-{T}(E14) { 0, 2, 6, 14 }
% 92.66/92.95 185 : p102-{T}(E14) { 0, 2, 6, 14 }
% 92.66/92.95 186 : pppp18-{T}(E14) { 0, 2, 6, 14 }
% 92.66/92.95 187 : pppp19-{T}(E14) { 0, 2, 6, 14 }
% 92.66/92.95 188 : p101-{T}(E14) { 0, 2, 6, 14 }
% 92.66/92.95 189 : p100-{T}(E14) { 0, 2, 6, 14 }
% 92.66/92.95 190 : #-{T} E15 { 0, 1, 3, 7, 15 }
% 92.66/92.95 191 : pppp3-{T}(E15,E7) { 0, 1, 3, 7, 15 }
% 92.66/92.95 192 : r1-{T}(E15,E15) { 0, 1, 3, 7, 15 }
% 92.66/92.95 193 : p104-{T}(E15) { 0, 1, 3, 7, 15 }
% 92.66/92.95 194 : p5-{T}(E15) { 0, 1, 3, 7, 15 }
% 92.66/92.95 195 : r1-{T}(E7,E15) { 0, 1, 3, 7, 15 }
% 92.66/92.95 196 : r1-{T}(E0,E15) { 0, 1, 3, 7, 15 }
% 92.66/92.95 197 : r1-{T}(E1,E15) { 0, 1, 3, 7, 15 }
% 92.66/92.95 198 : r1-{T}(E3,E15) { 0, 1, 3, 7, 15 }
% 92.66/92.95 199 : pppp10-{T}(E15) { 0, 1, 3, 7, 15 }
% 92.66/92.95 200 : p103-{T}(E15) { 0, 1, 3, 7, 15 }
% 92.66/92.95 201 : p102-{T}(E15) { 0, 1, 3, 7, 15 }
% 92.66/92.95 202 : p4-{T}(E15) { 0, 1, 3, 7, 15 }
% 92.66/92.95 203 : p101-{T}(E15) { 0, 1, 3, 7, 15 }
% 92.66/92.95 204 : p3-{T}(E15) { 0, 1, 3, 7, 15 }
% 92.66/92.95 205 : p100-{T}(E15) { 0, 1, 3, 7, 15 }
% 92.66/92.95 206 : p2-{T}(E15) { 0, 1, 3, 7, 15 }
% 92.66/92.95 207 : pppp20-{T}(E15) { 0, 1, 3, 7, 15 }
% 92.66/92.95 208 : pppp21-{T}(E15) { 0, 1, 3, 7, 15 }
% 92.66/92.95 209 : #-{T} E16 { 0, 1, 3, 7, 16 }
% 92.66/92.95 210 : pppp2-{T}(E16,E7) { 0, 1, 3, 7, 16 }
% 92.66/92.95 211 : r1-{T}(E16,E16) { 0, 1, 3, 7, 16 }
% 92.66/92.95 212 : p104-{T}(E16) { 0, 1, 3, 7, 16 }
% 92.66/92.95 213 : r1-{T}(E7,E16) { 0, 1, 3, 7, 16 }
% 92.66/92.95 214 : r1-{T}(E0,E16) { 0, 1, 3, 7, 16 }
% 92.66/92.95 215 : r1-{T}(E1,E16) { 0, 1, 3, 7, 16 }
% 92.66/92.95 216 : r1-{T}(E3,E16) { 0, 1, 3, 7, 16 }
% 92.66/92.95 217 : pppp10-{T}(E16) { 0, 1, 3, 7, 16 }
% 92.66/92.95 218 : p103-{T}(E16) { 0, 1, 3, 7, 16 }
% 92.66/92.95 219 : p102-{T}(E16) { 0, 1, 3, 7, 16 }
% 92.66/92.95 220 : p4-{T}(E16) { 0, 1, 3, 7, 16 }
% 92.66/92.95 221 : p101-{T}(E16) { 0, 1, 3, 7, 16 }
% 92.66/92.95 222 : p3-{T}(E16) { 0, 1, 3, 7, 16 }
% 92.66/92.95 223 : p100-{T}(E16) { 0, 1, 3, 7, 16 }
% 92.66/92.95 224 : p2-{T}(E16) { 0, 1, 3, 7, 16 }
% 92.66/92.95 225 : pppp21-{T}(E16) { 0, 1, 3, 7, 16 }
% 92.66/92.95 226 : pppp20-{T}(E16) { 0, 1, 3, 7, 16 }
% 92.66/92.95 227 : #-{T} E17 { 0, 1, 3, 8, 17 }
% 92.66/92.95 228 : pppp3-{T}(E17,E8) { 0, 1, 3, 8, 17 }
% 92.66/92.95 229 : r1-{T}(E17,E17) { 0, 1, 3, 8, 17 }
% 92.66/92.95 230 : p104-{T}(E17) { 0, 1, 3, 8, 17 }
% 92.66/92.95 231 : p5-{T}(E17) { 0, 1, 3, 8, 17 }
% 92.66/92.95 232 : r1-{T}(E8,E17) { 0, 1, 3, 8, 17 }
% 92.66/92.95 233 : r1-{T}(E0,E17) { 0, 1, 3, 8, 17 }
% 92.66/92.95 234 : r1-{T}(E1,E17) { 0, 1, 3, 8, 17 }
% 92.66/92.95 235 : r1-{T}(E3,E17) { 0, 1, 3, 8, 17 }
% 92.66/92.95 236 : pppp10-{T}(E17) { 0, 1, 3, 8, 17 }
% 92.66/92.95 237 : p103-{T}(E17) { 0, 1, 3, 8, 17 }
% 92.66/92.95 238 : pppp20-{T}(E17) { 0, 1, 3, 8, 17 }
% 92.66/92.95 239 : pppp21-{T}(E17) { 0, 1, 3, 8, 17 }
% 92.66/92.95 240 : p102-{T}(E17) { 0, 1, 3, 8, 17 }
% 92.66/92.95 241 : p101-{T}(E17) { 0, 1, 3, 8, 17 }
% 92.66/92.95 242 : p3-{T}(E17) { 0, 1, 3, 8, 17 }
% 92.66/92.95 243 : p100-{T}(E17) { 0, 1, 3, 8, 17 }
% 92.66/92.95 244 : p2-{T}(E17) { 0, 1, 3, 8, 17 }
% 92.66/92.95 245 : #-{T} E18 { 0, 1, 3, 8, 18 }
% 92.66/92.95 246 : pppp2-{T}(E18,E8) { 0, 1, 3, 8, 18 }
% 92.66/92.95 247 : r1-{T}(E18,E18) { 0, 1, 3, 8, 18 }
% 92.66/92.95 248 : p104-{T}(E18) { 0, 1, 3, 8, 18 }
% 92.66/92.95 249 : r1-{T}(E8,E18) { 0, 1, 3, 8, 18 }
% 92.66/92.95 250 : r1-{T}(E0,E18) { 0, 1, 3, 8, 18 }
% 92.66/92.95 251 : r1-{T}(E1,E18) { 0, 1, 3, 8, 18 }
% 92.66/92.95 252 : r1-{T}(E3,E18) { 0, 1, 3, 8, 18 }
% 92.66/92.95 253 : pppp10-{T}(E18) { 0, 1, 3, 8, 18 }
% 92.66/92.95 254 : p103-{T}(E18) { 0, 1, 3, 8, 18 }
% 92.66/92.95 255 : pppp21-{T}(E18) { 0, 1, 3, 8, 18 }
% 92.66/92.95 256 : pppp20-{T}(E18) { 0, 1, 3, 8, 18 }
% 92.66/92.95 257 : p102-{T}(E18) { 0, 1, 3, 8, 18 }
% 92.66/92.95 258 : p101-{T}(E18) { 0, 1, 3, 8, 18 }
% 92.66/92.95 259 : p3-{T}(E18) { 0, 1, 3, 8, 18 }
% 92.66/92.95 260 : p100-{T}(E18) { 0, 1, 3, 8, 18 }
% 92.66/92.95 261 : p2-{T}(E18) { 0, 1, 3, 8, 18 }
% 92.66/92.95 262 : #-{T} E19 { 0, 1, 4, 9, 19 }
% 92.66/92.95 263 : pppp3-{T}(E19,E9) { 0, 1, 4, 9, 19 }
% 92.66/92.95 264 : r1-{T}(E19,E19) { 0, 1, 4, 9, 19 }
% 92.66/92.95 265 : p104-{T}(E19) { 0, 1, 4, 9, 19 }
% 92.66/92.95 266 : p5-{T}(E19) { 0, 1, 4, 9, 19 }
% 92.66/92.95 267 : r1-{T}(E9,E19) { 0, 1, 4, 9, 19 }
% 92.66/92.95 268 : r1-{T}(E0,E19) { 0, 1, 4, 9, 19 }
% 92.66/92.95 269 : r1-{T}(E1,E19) { 0, 1, 4, 9, 19 }
% 92.66/92.95 270 : r1-{T}(E4,E19) { 0, 1, 4, 9, 19 }
% 92.66/92.95 271 : pppp10-{T}(E19) { 0, 1, 4, 9, 19 }
% 92.66/92.95 272 : p103-{T}(E19) { 0, 1, 4, 9, 19 }
% 92.66/92.95 273 : pppp20-{T}(E19) { 0, 1, 4, 9, 19 }
% 92.66/92.95 274 : pppp21-{T}(E19) { 0, 1, 4, 9, 19 }
% 92.66/92.95 275 : p102-{T}(E19) { 0, 1, 4, 9, 19 }
% 92.66/92.95 276 : p4-{T}(E19) { 0, 1, 4, 9, 19 }
% 92.66/92.95 277 : p101-{T}(E19) { 0, 1, 4, 9, 19 }
% 92.66/92.95 278 : p100-{T}(E19) { 0, 1, 4, 9, 19 }
% 92.66/92.95 279 : p2-{T}(E19) { 0, 1, 4, 9, 19 }
% 92.66/92.95 280 : #-{T} E20 { 0, 1, 4, 9, 20 }
% 92.66/92.95 281 : pppp2-{T}(E20,E9) { 0, 1, 4, 9, 20 }
% 92.66/92.95 282 : r1-{T}(E20,E20) { 0, 1, 4, 9, 20 }
% 92.66/92.95 283 : p104-{T}(E20) { 0, 1, 4, 9, 20 }
% 92.66/92.95 284 : r1-{T}(E9,E20) { 0, 1, 4, 9, 20 }
% 92.66/92.95 285 : r1-{T}(E0,E20) { 0, 1, 4, 9, 20 }
% 92.66/92.95 286 : r1-{T}(E1,E20) { 0, 1, 4, 9, 20 }
% 92.66/92.95 287 : r1-{T}(E4,E20) { 0, 1, 4, 9, 20 }
% 92.66/92.95 288 : pppp10-{T}(E20) { 0, 1, 4, 9, 20 }
% 92.66/92.95 289 : p103-{T}(E20) { 0, 1, 4, 9, 20 }
% 92.66/92.95 290 : pppp21-{T}(E20) { 0, 1, 4, 9, 20 }
% 92.66/92.95 291 : pppp20-{T}(E20) { 0, 1, 4, 9, 20 }
% 92.66/92.95 292 : p102-{T}(E20) { 0, 1, 4, 9, 20 }
% 92.66/92.95 293 : p4-{T}(E20) { 0, 1, 4, 9, 20 }
% 92.66/92.95 294 : p101-{T}(E20) { 0, 1, 4, 9, 20 }
% 92.66/92.95 295 : p100-{T}(E20) { 0, 1, 4, 9, 20 }
% 92.66/92.95 296 : p2-{T}(E20) { 0, 1, 4, 9, 20 }
% 92.66/92.95 297 : #-{T} E21 { 0, 1, 4, 10, 21 }
% 92.66/92.95 298 : pppp3-{T}(E21,E10) { 0, 1, 4, 10, 21 }
% 92.66/92.95 299 : r1-{T}(E21,E21) { 0, 1, 4, 10, 21 }
% 92.66/92.95 300 : p104-{T}(E21) { 0, 1, 4, 10, 21 }
% 92.66/92.95 301 : p5-{T}(E21) { 0, 1, 4, 10, 21 }
% 92.66/92.95 302 : r1-{T}(E10,E21) { 0, 1, 4, 10, 21 }
% 92.66/92.95 303 : r1-{T}(E0,E21) { 0, 1, 4, 10, 21 }
% 92.66/92.95 304 : r1-{T}(E1,E21) { 0, 1, 4, 10, 21 }
% 92.66/92.95 305 : r1-{T}(E4,E21) { 0, 1, 4, 10, 21 }
% 92.66/92.95 306 : pppp10-{T}(E21) { 0, 1, 4, 10, 21 }
% 92.66/92.95 307 : p103-{T}(E21) { 0, 1, 4, 10, 21 }
% 92.66/92.95 308 : pppp20-{T}(E21) { 0, 1, 4, 10, 21 }
% 92.66/92.95 309 : pppp21-{T}(E21) { 0, 1, 4, 10, 21 }
% 92.66/92.95 310 : p102-{T}(E21) { 0, 1, 4, 10, 21 }
% 92.66/92.95 311 : p101-{T}(E21) { 0, 1, 4, 10, 21 }
% 92.66/92.95 312 : p100-{T}(E21) { 0, 1, 4, 10, 21 }
% 92.66/92.95 313 : p2-{T}(E21) { 0, 1, 4, 10, 21 }
% 92.66/92.95 314 : #-{T} E22 { 0, 1, 4, 10, 22 }
% 92.66/92.95 315 : pppp2-{T}(E22,E10) { 0, 1, 4, 10, 22 }
% 92.66/92.95 316 : r1-{T}(E22,E22) { 0, 1, 4, 10, 22 }
% 92.66/92.95 317 : p104-{T}(E22) { 0, 1, 4, 10, 22 }
% 92.66/92.95 318 : r1-{T}(E10,E22) { 0, 1, 4, 10, 22 }
% 92.66/92.95 319 : r1-{T}(E0,E22) { 0, 1, 4, 10, 22 }
% 92.66/92.95 320 : r1-{T}(E1,E22) { 0, 1, 4, 10, 22 }
% 92.66/92.95 321 : r1-{T}(E4,E22) { 0, 1, 4, 10, 22 }
% 92.66/92.95 322 : pppp10-{T}(E22) { 0, 1, 4, 10, 22 }
% 92.66/92.95 323 : p103-{T}(E22) { 0, 1, 4, 10, 22 }
% 92.66/92.95 324 : pppp21-{T}(E22) { 0, 1, 4, 10, 22 }
% 92.66/92.95 325 : pppp20-{T}(E22) { 0, 1, 4, 10, 22 }
% 92.66/92.95 326 : p102-{T}(E22) { 0, 1, 4, 10, 22 }
% 92.66/92.95 327 : p101-{T}(E22) { 0, 1, 4, 10, 22 }
% 92.66/92.95 328 : p100-{T}(E22) { 0, 1, 4, 10, 22 }
% 92.66/92.95 329 : p2-{T}(E22) { 0, 1, 4, 10, 22 }
% 92.66/92.95 330 : #-{T} E23 { 0, 2, 5, 11, 23 }
% 92.66/92.95 331 : pppp3-{T}(E23,E11) { 0, 2, 5, 11, 23 }
% 92.66/92.95 332 : r1-{T}(E23,E23) { 0, 2, 5, 11, 23 }
% 92.66/92.95 333 : p104-{T}(E23) { 0, 2, 5, 11, 23 }
% 92.66/92.95 334 : p5-{T}(E23) { 0, 2, 5, 11, 23 }
% 92.66/92.95 335 : r1-{T}(E11,E23) { 0, 2, 5, 11, 23 }
% 92.66/92.95 336 : r1-{T}(E1,E23) { 0, 2, 5, 11, 23 }
% 92.66/92.95 337 : r1-{T}(E2,E23) { 0, 2, 5, 11, 23 }
% 92.66/92.95 338 : pppp10-{T}(E23) { 0, 2, 5, 11, 23 }
% 92.66/92.95 339 : r1-{T}(E5,E23) { 0, 2, 5, 11, 23 }
% 92.66/92.95 340 : p103-{T}(E23) { 0, 2, 5, 11, 23 }
% 92.66/92.95 341 : pppp20-{T}(E23) { 0, 2, 5, 11, 23 }
% 92.66/92.95 342 : p102-{T}(E23) { 0, 2, 5, 11, 23 }
% 92.66/92.95 343 : pppp21-{T}(E23) { 0, 2, 5, 11, 23 }
% 92.66/92.95 344 : p4-{T}(E23) { 0, 2, 5, 11, 23 }
% 92.66/92.95 345 : p101-{T}(E23) { 0, 2, 5, 11, 23 }
% 92.66/92.95 346 : p3-{T}(E23) { 0, 2, 5, 11, 23 }
% 92.66/92.95 347 : p100-{T}(E23) { 0, 2, 5, 11, 23 }
% 92.66/92.95 348 : #-{T} E24 { 0, 2, 5, 11, 24 }
% 92.66/92.95 349 : pppp2-{T}(E24,E11) { 0, 2, 5, 11, 24 }
% 92.66/92.95 350 : r1-{T}(E24,E24) { 0, 2, 5, 11, 24 }
% 92.66/92.95 351 : p104-{T}(E24) { 0, 2, 5, 11, 24 }
% 92.66/92.95 352 : r1-{T}(E11,E24) { 0, 2, 5, 11, 24 }
% 92.66/92.95 353 : r1-{T}(E1,E24) { 0, 2, 5, 11, 24 }
% 92.66/92.95 354 : r1-{T}(E2,E24) { 0, 2, 5, 11, 24 }
% 92.66/92.95 355 : pppp10-{T}(E24) { 0, 2, 5, 11, 24 }
% 92.66/92.95 356 : r1-{T}(E5,E24) { 0, 2, 5, 11, 24 }
% 92.66/92.95 357 : p103-{T}(E24) { 0, 2, 5, 11, 24 }
% 92.66/92.95 358 : pppp21-{T}(E24) { 0, 2, 5, 11, 24 }
% 92.66/92.95 359 : p102-{T}(E24) { 0, 2, 5, 11, 24 }
% 92.66/92.95 360 : pppp20-{T}(E24) { 0, 2, 5, 11, 24 }
% 92.66/92.95 361 : p4-{T}(E24) { 0, 2, 5, 11, 24 }
% 92.66/92.95 362 : p101-{T}(E24) { 0, 2, 5, 11, 24 }
% 92.66/92.95 363 : p3-{T}(E24) { 0, 2, 5, 11, 24 }
% 92.66/92.95 364 : p100-{T}(E24) { 0, 2, 5, 11, 24 }
% 92.66/92.95 365 : #-{T} E25 { 0, 2, 5, 12, 25 }
% 92.66/92.95 366 : pppp3-{T}(E25,E12) { 0, 2, 5, 12, 25 }
% 92.66/92.95 367 : r1-{T}(E25,E25) { 0, 2, 5, 12, 25 }
% 92.66/92.95 368 : p104-{T}(E25) { 0, 2, 5, 12, 25 }
% 92.66/92.95 369 : p5-{T}(E25) { 0, 2, 5, 12, 25 }
% 92.66/92.95 370 : r1-{T}(E12,E25) { 0, 2, 5, 12, 25 }
% 92.66/92.95 371 : r1-{T}(E2,E25) { 0, 2, 5, 12, 25 }
% 92.66/92.95 372 : r1-{T}(E1,E25) { 0, 2, 5, 12, 25 }
% 92.66/92.95 373 : r1-{T}(E5,E25) { 0, 2, 5, 12, 25 }
% 92.66/92.95 374 : pppp10-{T}(E25) { 0, 2, 5, 12, 25 }
% 92.66/92.95 375 : p103-{T}(E25) { 0, 2, 5, 12, 25 }
% 92.66/92.95 376 : pppp20-{T}(E25) { 0, 2, 5, 12, 25 }
% 92.66/92.95 377 : pppp21-{T}(E25) { 0, 2, 5, 12, 25 }
% 92.66/92.95 378 : p102-{T}(E25) { 0, 2, 5, 12, 25 }
% 92.66/92.95 379 : p101-{T}(E25) { 0, 2, 5, 12, 25 }
% 92.66/92.95 380 : p3-{T}(E25) { 0, 2, 5, 12, 25 }
% 92.66/92.95 381 : p100-{T}(E25) { 0, 2, 5, 12, 25 }
% 92.66/92.95 382 : #-{T} E26 { 0, 2, 5, 12, 26 }
% 92.66/92.95 383 : pppp2-{T}(E26,E12) { 0, 2, 5, 12, 26 }
% 92.66/92.95 384 : r1-{T}(E26,E26) { 0, 2, 5, 12, 26 }
% 92.66/92.95 385 : p104-{T}(E26) { 0, 2, 5, 12, 26 }
% 92.66/92.95 386 : r1-{T}(E12,E26) { 0, 2, 5, 12, 26 }
% 92.66/92.95 387 : r1-{T}(E2,E26) { 0, 2, 5, 12, 26 }
% 92.66/92.95 388 : r1-{T}(E1,E26) { 0, 2, 5, 12, 26 }
% 92.66/92.95 389 : r1-{T}(E5,E26) { 0, 2, 5, 12, 26 }
% 92.66/92.95 390 : pppp10-{T}(E26) { 0, 2, 5, 12, 26 }
% 92.66/92.95 391 : p103-{T}(E26) { 0, 2, 5, 12, 26 }
% 92.66/92.95 392 : pppp21-{T}(E26) { 0, 2, 5, 12, 26 }
% 92.66/92.95 393 : pppp20-{T}(E26) { 0, 2, 5, 12, 26 }
% 92.66/92.95 394 : p102-{T}(E26) { 0, 2, 5, 12, 26 }
% 92.66/92.95 395 : p101-{T}(E26) { 0, 2, 5, 12, 26 }
% 92.66/92.95 396 : p3-{T}(E26) { 0, 2, 5, 12, 26 }
% 92.66/92.95 397 : p100-{T}(E26) { 0, 2, 5, 12, 26 }
% 92.66/92.95 398 : #-{T} E27 { 0, 2, 6, 13, 27 }
% 92.66/92.95 399 : pppp3-{T}(E27,E13) { 0, 2, 6, 13, 27 }
% 92.66/92.95 400 : r1-{T}(E27,E27) { 0, 2, 6, 13, 27 }
% 92.66/92.95 401 : p104-{T}(E27) { 0, 2, 6, 13, 27 }
% 92.66/92.95 402 : p5-{T}(E27) { 0, 2, 6, 13, 27 }
% 92.66/92.95 403 : r1-{T}(E13,E27) { 0, 2, 6, 13, 27 }
% 92.66/92.95 404 : r1-{T}(E2,E27) { 0, 2, 6, 13, 27 }
% 92.66/92.95 405 : r1-{T}(E1,E27) { 0, 2, 6, 13, 27 }
% 92.66/92.95 406 : r1-{T}(E6,E27) { 0, 2, 6, 13, 27 }
% 92.66/92.95 407 : pppp10-{T}(E27) { 0, 2, 6, 13, 27 }
% 92.66/92.95 408 : p103-{T}(E27) { 0, 2, 6, 13, 27 }
% 92.66/92.95 409 : pppp20-{T}(E27) { 0, 2, 6, 13, 27 }
% 92.66/92.95 410 : pppp21-{T}(E27) { 0, 2, 6, 13, 27 }
% 92.66/92.95 411 : p102-{T}(E27) { 0, 2, 6, 13, 27 }
% 92.66/92.95 412 : p4-{T}(E27) { 0, 2, 6, 13, 27 }
% 92.66/92.95 413 : p101-{T}(E27) { 0, 2, 6, 13, 27 }
% 92.66/92.95 414 : p100-{T}(E27) { 0, 2, 6, 13, 27 }
% 92.66/92.95 415 : #-{T} E28 { 0, 2, 6, 13, 28 }
% 92.66/92.95 416 : pppp2-{T}(E28,E13) { 0, 2, 6, 13, 28 }
% 92.66/92.95 417 : r1-{T}(E28,E28) { 0, 2, 6, 13, 28 }
% 92.66/92.95 418 : p104-{T}(E28) { 0, 2, 6, 13, 28 }
% 92.66/92.95 419 : r1-{T}(E13,E28) { 0, 2, 6, 13, 28 }
% 92.66/92.95 420 : r1-{T}(E2,E28) { 0, 2, 6, 13, 28 }
% 92.66/92.95 421 : r1-{T}(E1,E28) { 0, 2, 6, 13, 28 }
% 92.66/92.95 422 : r1-{T}(E6,E28) { 0, 2, 6, 13, 28 }
% 92.66/92.95 423 : pppp10-{T}(E28) { 0, 2, 6, 13, 28 }
% 92.66/92.95 424 : p103-{T}(E28) { 0, 2, 6, 13, 28 }
% 92.66/92.95 425 : pppp21-{T}(E28) { 0, 2, 6, 13, 28 }
% 92.66/92.95 426 : pppp20-{T}(E28) { 0, 2, 6, 13, 28 }
% 92.66/92.95 427 : p102-{T}(E28) { 0, 2, 6, 13, 28 }
% 92.66/92.95 428 : p4-{T}(E28) { 0, 2, 6, 13, 28 }
% 92.66/92.95 429 : p101-{T}(E28) { 0, 2, 6, 13, 28 }
% 92.66/92.95 430 : p100-{T}(E28) { 0, 2, 6, 13, 28 }
% 92.66/92.95 431 : #-{T} E29 { 0, 2, 6, 14, 29 }
% 92.66/92.95 432 : pppp3-{T}(E29,E14) { 0, 2, 6, 14, 29 }
% 92.66/92.95 433 : r1-{T}(E29,E29) { 0, 2, 6, 14, 29 }
% 92.66/92.95 434 : p104-{T}(E29) { 0, 2, 6, 14, 29 }
% 92.66/92.95 435 : p5-{T}(E29) { 0, 2, 6, 14, 29 }
% 92.66/92.95 436 : r1-{T}(E14,E29) { 0, 2, 6, 14, 29 }
% 92.66/92.95 437 : r1-{T}(E1,E29) { 0, 2, 6, 14, 29 }
% 92.66/92.95 438 : r1-{T}(E2,E29) { 0, 2, 6, 14, 29 }
% 92.66/92.95 439 : pppp10-{T}(E29) { 0, 2, 6, 14, 29 }
% 92.66/92.95 440 : r1-{T}(E6,E29) { 0, 2, 6, 14, 29 }
% 92.66/92.95 441 : p103-{T}(E29) { 0, 2, 6, 14, 29 }
% 92.66/92.95 442 : pppp20-{T}(E29) { 0, 2, 6, 14, 29 }
% 92.66/92.95 443 : p102-{T}(E29) { 0, 2, 6, 14, 29 }
% 92.66/92.95 444 : pppp21-{T}(E29) { 0, 2, 6, 14, 29 }
% 92.66/92.95 445 : p101-{T}(E29) { 0, 2, 6, 14, 29 }
% 92.66/92.95 446 : p100-{T}(E29) { 0, 2, 6, 14, 29 }
% 92.66/92.95 447 : #-{T} E30 { 0, 2, 6, 14, 30 }
% 92.66/92.95 448 : pppp2-{T}(E30,E14) { 0, 2, 6, 14, 30 }
% 92.66/92.95 449 : r1-{T}(E30,E30) { 0, 2, 6, 14, 30 }
% 92.66/92.95 450 : p104-{T}(E30) { 0, 2, 6, 14, 30 }
% 92.66/92.95 451 : r1-{T}(E14,E30) { 0, 2, 6, 14, 30 }
% 92.66/92.95 452 : r1-{T}(E1,E30) { 0, 2, 6, 14, 30 }
% 92.66/92.95 453 : r1-{T}(E2,E30) { 0, 2, 6, 14, 30 }
% 92.66/92.95 454 : pppp10-{T}(E30) { 0, 2, 6, 14, 30 }
% 92.66/92.95 455 : r1-{T}(E6,E30) { 0, 2, 6, 14, 30 }
% 92.66/92.95 456 : p103-{T}(E30) { 0, 2, 6, 14, 30 }
% 92.66/92.95 457 : pppp21-{T}(E30) { 0, 2, 6, 14, 30 }
% 92.66/92.95 458 : p102-{T}(E30) { 0, 2, 6, 14, 30 }
% 92.66/92.95 459 : pppp20-{T}(E30) { 0, 2, 6, 14, 30 }
% 92.66/92.95 460 : p101-{T}(E30) { 0, 2, 6, 14, 30 }
% 92.66/92.95 461 : p100-{T}(E30) { 0, 2, 6, 14, 30 }
% 92.66/92.95 462 : #-{T} E31 { 0, 1, 3, 7, 15, 31 }
% 92.66/92.95 463 : pppp1-{T}(E31,E15) { 0, 1, 3, 7, 15, 31 }
% 92.66/92.95 464 : r1-{T}(E31,E31) { 0, 1, 3, 7, 15, 31 }
% 92.66/92.95 465 : p105-{T}(E31) { 0, 1, 3, 7, 15, 31 }
% 92.66/92.95 466 : p6-{T}(E31) { 0, 1, 3, 7, 15, 31 }
% 92.66/92.95 467 : r1-{T}(E15,E31) { 0, 1, 3, 7, 15, 31 }
% 92.66/92.95 468 : r1-{T}(E3,E31) { 0, 1, 3, 7, 15, 31 }
% 92.66/92.95 469 : r1-{T}(E1,E31) { 0, 1, 3, 7, 15, 31 }
% 92.66/92.95 470 : r1-{T}(E0,E31) { 0, 1, 3, 7, 15, 31 }
% 92.66/92.95 471 : pppp10-{T}(E31) { 0, 1, 3, 7, 15, 31 }
% 92.66/92.95 472 : r1-{T}(E7,E31) { 0, 1, 3, 7, 15, 31 }
% 92.66/92.95 473 : p104-{T}(E31) { 0, 1, 3, 7, 15, 31 }
% 92.66/92.95 474 : p103-{T}(E31) { 0, 1, 3, 7, 15, 31 }
% 92.66/92.95 475 : p5-{T}(E31) { 0, 1, 3, 7, 15, 31 }
% 92.66/92.95 476 : p102-{T}(E31) { 0, 1, 3, 7, 15, 31 }
% 92.66/92.95 477 : p4-{T}(E31) { 0, 1, 3, 7, 15, 31 }
% 92.66/92.95 478 : p101-{T}(E31) { 0, 1, 3, 7, 15, 31 }
% 92.66/92.95 479 : p3-{T}(E31) { 0, 1, 3, 7, 15, 31 }
% 92.66/92.95 480 : p100-{T}(E31) { 0, 1, 3, 7, 15, 31 }
% 92.66/92.95 481 : p2-{T}(E31) { 0, 1, 3, 7, 15, 31 }
% 92.66/92.95 482 : #-{T} E32 { 0, 1, 3, 7, 15, 32 }
% 92.66/92.95 483 : pppp0-{T}(E32,E15) { 0, 1, 3, 7, 15, 32 }
% 92.66/92.95 484 : r1-{T}(E32,E32) { 0, 1, 3, 7, 15, 32 }
% 92.66/92.95 485 : p105-{T}(E32) { 0, 1, 3, 7, 15, 32 }
% 92.66/92.95 486 : r1-{T}(E15,E32) { 0, 1, 3, 7, 15, 32 }
% 92.66/92.95 487 : r1-{T}(E3,E32) { 0, 1, 3, 7, 15, 32 }
% 92.66/92.95 488 : r1-{T}(E1,E32) { 0, 1, 3, 7, 15, 32 }
% 92.66/92.95 489 : r1-{T}(E0,E32) { 0, 1, 3, 7, 15, 32 }
% 92.66/92.95 490 : pppp10-{T}(E32) { 0, 1, 3, 7, 15, 32 }
% 92.66/92.95 491 : r1-{T}(E7,E32) { 0, 1, 3, 7, 15, 32 }
% 92.66/92.95 492 : p104-{T}(E32) { 0, 1, 3, 7, 15, 32 }
% 92.66/92.95 493 : p103-{T}(E32) { 0, 1, 3, 7, 15, 32 }
% 92.66/92.95 494 : p5-{T}(E32) { 0, 1, 3, 7, 15, 32 }
% 92.66/92.95 495 : p102-{T}(E32) { 0, 1, 3, 7, 15, 32 }
% 92.66/92.95 496 : p4-{T}(E32) { 0, 1, 3, 7, 15, 32 }
% 92.66/92.95 497 : p101-{T}(E32) { 0, 1, 3, 7, 15, 32 }
% 92.66/92.95 498 : p3-{T}(E32) { 0, 1, 3, 7, 15, 32 }
% 92.66/92.95 499 : p100-{T}(E32) { 0, 1, 3, 7, 15, 32 }
% 92.66/92.95 500 : p2-{T}(E32) { 0, 1, 3, 7, 15, 32 }
% 92.66/92.95 501 : #-{T} E33 { 0, 1, 3, 7, 16, 33 }
% 92.66/92.95 502 : pppp1-{T}(E33,E16) { 0, 1, 3, 7, 16, 33 }
% 92.66/92.95 503 : r1-{T}(E33,E33) { 0, 1, 3, 7, 16, 33 }
% 92.66/92.95 504 : p105-{T}(E33) { 0, 1, 3, 7, 16, 33 }
% 92.66/92.95 505 : p6-{T}(E33) { 0, 1, 3, 7, 16, 33 }
% 92.66/92.95 506 : r1-{T}(E16,E33) { 0, 1, 3, 7, 16, 33 }
% 92.66/92.95 507 : r1-{T}(E3,E33) { 0, 1, 3, 7, 16, 33 }
% 92.66/92.95 508 : r1-{T}(E1,E33) { 0, 1, 3, 7, 16, 33 }
% 92.66/92.95 509 : r1-{T}(E0,E33) { 0, 1, 3, 7, 16, 33 }
% 92.66/92.95 510 : pppp10-{T}(E33) { 0, 1, 3, 7, 16, 33 }
% 92.66/92.95 511 : r1-{T}(E7,E33) { 0, 1, 3, 7, 16, 33 }
% 92.66/92.95 512 : p104-{T}(E33) { 0, 1, 3, 7, 16, 33 }
% 92.66/92.95 513 : p103-{T}(E33) { 0, 1, 3, 7, 16, 33 }
% 92.66/92.95 514 : p102-{T}(E33) { 0, 1, 3, 7, 16, 33 }
% 92.66/92.95 515 : p4-{T}(E33) { 0, 1, 3, 7, 16, 33 }
% 92.66/92.95 516 : p101-{T}(E33) { 0, 1, 3, 7, 16, 33 }
% 92.66/92.95 517 : p3-{T}(E33) { 0, 1, 3, 7, 16, 33 }
% 92.66/92.95 518 : p100-{T}(E33) { 0, 1, 3, 7, 16, 33 }
% 92.66/92.95 519 : p2-{T}(E33) { 0, 1, 3, 7, 16, 33 }
% 92.66/92.95 520 : #-{T} E34 { 0, 1, 3, 7, 16, 34 }
% 92.66/92.95 521 : pppp0-{T}(E34,E16) { 0, 1, 3, 7, 16, 34 }
% 92.66/92.95 522 : r1-{T}(E34,E34) { 0, 1, 3, 7, 16, 34 }
% 92.66/92.95 523 : p105-{T}(E34) { 0, 1, 3, 7, 16, 34 }
% 92.66/92.95 524 : r1-{T}(E16,E34) { 0, 1, 3, 7, 16, 34 }
% 92.66/92.95 525 : r1-{T}(E3,E34) { 0, 1, 3, 7, 16, 34 }
% 92.66/92.95 526 : r1-{T}(E1,E34) { 0, 1, 3, 7, 16, 34 }
% 92.66/92.95 527 : r1-{T}(E0,E34) { 0, 1, 3, 7, 16, 34 }
% 92.66/92.95 528 : pppp10-{T}(E34) { 0, 1, 3, 7, 16, 34 }
% 92.66/92.95 529 : r1-{T}(E7,E34) { 0, 1, 3, 7, 16, 34 }
% 92.66/92.95 530 : p104-{T}(E34) { 0, 1, 3, 7, 16, 34 }
% 92.66/92.95 531 : p103-{T}(E34) { 0, 1, 3, 7, 16, 34 }
% 92.66/92.95 532 : p102-{T}(E34) { 0, 1, 3, 7, 16, 34 }
% 92.66/92.95 533 : p4-{T}(E34) { 0, 1, 3, 7, 16, 34 }
% 92.66/92.95 534 : p101-{T}(E34) { 0, 1, 3, 7, 16, 34 }
% 92.66/92.95 535 : p3-{T}(E34) { 0, 1, 3, 7, 16, 34 }
% 92.66/92.95 536 : p100-{T}(E34) { 0, 1, 3, 7, 16, 34 }
% 92.66/92.95 537 : p2-{T}(E34) { 0, 1, 3, 7, 16, 34 }
% 92.66/92.95 538 : #-{T} E35 { 0, 1, 3, 8, 17, 35 }
% 92.66/92.95 539 : pppp1-{T}(E35,E17) { 0, 1, 3, 8, 17, 35 }
% 92.66/92.95 540 : r1-{T}(E35,E35) { 0, 1, 3, 8, 17, 35 }
% 92.66/92.95 541 : p105-{T}(E35) { 0, 1, 3, 8, 17, 35 }
% 92.66/92.95 542 : p6-{T}(E35) { 0, 1, 3, 8, 17, 35 }
% 92.66/92.95 543 : r1-{T}(E17,E35) { 0, 1, 3, 8, 17, 35 }
% 92.66/92.95 544 : r1-{T}(E3,E35) { 0, 1, 3, 8, 17, 35 }
% 92.66/92.95 545 : r1-{T}(E1,E35) { 0, 1, 3, 8, 17, 35 }
% 92.66/92.95 546 : r1-{T}(E0,E35) { 0, 1, 3, 8, 17, 35 }
% 92.66/92.95 547 : pppp10-{T}(E35) { 0, 1, 3, 8, 17, 35 }
% 92.66/92.95 548 : r1-{T}(E8,E35) { 0, 1, 3, 8, 17, 35 }
% 92.66/92.95 549 : p104-{T}(E35) { 0, 1, 3, 8, 17, 35 }
% 92.66/92.95 550 : p103-{T}(E35) { 0, 1, 3, 8, 17, 35 }
% 92.66/92.95 551 : p5-{T}(E35) { 0, 1, 3, 8, 17, 35 }
% 92.66/92.95 552 : p102-{T}(E35) { 0, 1, 3, 8, 17, 35 }
% 92.66/92.95 553 : p101-{T}(E35) { 0, 1, 3, 8, 17, 35 }
% 92.66/92.95 554 : p3-{T}(E35) { 0, 1, 3, 8, 17, 35 }
% 92.66/92.95 555 : p100-{T}(E35) { 0, 1, 3, 8, 17, 35 }
% 92.66/92.95 556 : p2-{T}(E35) { 0, 1, 3, 8, 17, 35 }
% 92.66/92.95 557 : #-{T} E36 { 0, 1, 3, 8, 17, 36 }
% 92.66/92.95 558 : pppp0-{T}(E36,E17) { 0, 1, 3, 8, 17, 36 }
% 92.66/92.95 559 : r1-{T}(E36,E36) { 0, 1, 3, 8, 17, 36 }
% 92.66/92.95 560 : p105-{T}(E36) { 0, 1, 3, 8, 17, 36 }
% 92.66/92.95 561 : r1-{T}(E17,E36) { 0, 1, 3, 8, 17, 36 }
% 92.66/92.95 562 : r1-{T}(E3,E36) { 0, 1, 3, 8, 17, 36 }
% 92.66/92.95 563 : r1-{T}(E1,E36) { 0, 1, 3, 8, 17, 36 }
% 92.66/92.95 564 : r1-{T}(E0,E36) { 0, 1, 3, 8, 17, 36 }
% 92.66/92.95 565 : pppp10-{T}(E36) { 0, 1, 3, 8, 17, 36 }
% 92.66/92.95 566 : r1-{T}(E8,E36) { 0, 1, 3, 8, 17, 36 }
% 92.66/92.95 567 : p104-{T}(E36) { 0, 1, 3, 8, 17, 36 }
% 92.66/92.95 568 : p103-{T}(E36) { 0, 1, 3, 8, 17, 36 }
% 92.66/92.95 569 : p5-{T}(E36) { 0, 1, 3, 8, 17, 36 }
% 92.66/92.95 570 : p102-{T}(E36) { 0, 1, 3, 8, 17, 36 }
% 92.66/92.95 571 : p101-{T}(E36) { 0, 1, 3, 8, 17, 36 }
% 92.66/92.95 572 : p3-{T}(E36) { 0, 1, 3, 8, 17, 36 }
% 92.66/92.95 573 : p100-{T}(E36) { 0, 1, 3, 8, 17, 36 }
% 92.66/92.95 574 : p2-{T}(E36) { 0, 1, 3, 8, 17, 36 }
% 92.66/92.95 575 : #-{T} E37 { 0, 1, 3, 8, 18, 37 }
% 92.66/92.95 576 : pppp1-{T}(E37,E18) { 0, 1, 3, 8, 18, 37 }
% 92.66/92.95 577 : r1-{T}(E37,E37) { 0, 1, 3, 8, 18, 37 }
% 92.66/92.95 578 : p105-{T}(E37) { 0, 1, 3, 8, 18, 37 }
% 92.66/92.95 579 : p6-{T}(E37) { 0, 1, 3, 8, 18, 37 }
% 92.66/92.95 580 : r1-{T}(E18,E37) { 0, 1, 3, 8, 18, 37 }
% 92.66/92.95 581 : r1-{T}(E3,E37) { 0, 1, 3, 8, 18, 37 }
% 92.66/92.95 582 : r1-{T}(E1,E37) { 0, 1, 3, 8, 18, 37 }
% 92.66/92.95 583 : r1-{T}(E0,E37) { 0, 1, 3, 8, 18, 37 }
% 92.66/92.95 584 : pppp10-{T}(E37) { 0, 1, 3, 8, 18, 37 }
% 92.66/92.95 585 : r1-{T}(E8,E37) { 0, 1, 3, 8, 18, 37 }
% 92.66/92.95 586 : p104-{T}(E37) { 0, 1, 3, 8, 18, 37 }
% 92.66/92.95 587 : p103-{T}(E37) { 0, 1, 3, 8, 18, 37 }
% 92.66/92.95 588 : p102-{T}(E37) { 0, 1, 3, 8, 18, 37 }
% 92.66/92.95 589 : p101-{T}(E37) { 0, 1, 3, 8, 18, 37 }
% 92.66/92.95 590 : p3-{T}(E37) { 0, 1, 3, 8, 18, 37 }
% 92.66/92.95 591 : p100-{T}(E37) { 0, 1, 3, 8, 18, 37 }
% 92.66/92.95 592 : p2-{T}(E37) { 0, 1, 3, 8, 18, 37 }
% 92.66/92.95 593 : #-{T} E38 { 0, 1, 3, 8, 18, 38 }
% 92.66/92.95 594 : pppp0-{T}(E38,E18) { 0, 1, 3, 8, 18, 38 }
% 92.66/92.95 595 : r1-{T}(E38,E38) { 0, 1, 3, 8, 18, 38 }
% 92.66/92.95 596 : p105-{T}(E38) { 0, 1, 3, 8, 18, 38 }
% 92.66/92.95 597 : r1-{T}(E18,E38) { 0, 1, 3, 8, 18, 38 }
% 92.66/92.95 598 : r1-{T}(E3,E38) { 0, 1, 3, 8, 18, 38 }
% 92.66/92.95 599 : r1-{T}(E1,E38) { 0, 1, 3, 8, 18, 38 }
% 92.66/92.95 600 : r1-{T}(E0,E38) { 0, 1, 3, 8, 18, 38 }
% 92.66/92.95 601 : pppp10-{T}(E38) { 0, 1, 3, 8, 18, 38 }
% 92.66/92.95 602 : r1-{T}(E8,E38) { 0, 1, 3, 8, 18, 38 }
% 92.66/92.95 603 : p104-{T}(E38) { 0, 1, 3, 8, 18, 38 }
% 92.66/92.95 604 : p103-{T}(E38) { 0, 1, 3, 8, 18, 38 }
% 92.66/92.95 605 : p102-{T}(E38) { 0, 1, 3, 8, 18, 38 }
% 92.66/92.95 606 : p101-{T}(E38) { 0, 1, 3, 8, 18, 38 }
% 92.66/92.95 607 : p3-{T}(E38) { 0, 1, 3, 8, 18, 38 }
% 92.66/92.95 608 : p100-{T}(E38) { 0, 1, 3, 8, 18, 38 }
% 92.66/92.95 609 : p2-{T}(E38) { 0, 1, 3, 8, 18, 38 }
% 92.66/92.95 610 : #-{T} E39 { 0, 1, 4, 9, 19, 39 }
% 92.66/92.95 611 : pppp1-{T}(E39,E19) { 0, 1, 4, 9, 19, 39 }
% 92.66/92.95 612 : r1-{T}(E39,E39) { 0, 1, 4, 9, 19, 39 }
% 92.66/92.95 613 : p105-{T}(E39) { 0, 1, 4, 9, 19, 39 }
% 92.66/92.95 614 : p6-{T}(E39) { 0, 1, 4, 9, 19, 39 }
% 92.66/92.95 615 : r1-{T}(E19,E39) { 0, 1, 4, 9, 19, 39 }
% 92.66/92.95 616 : r1-{T}(E4,E39) { 0, 1, 4, 9, 19, 39 }
% 92.66/92.95 617 : r1-{T}(E1,E39) { 0, 1, 4, 9, 19, 39 }
% 92.66/92.95 618 : r1-{T}(E0,E39) { 0, 1, 4, 9, 19, 39 }
% 92.66/92.95 619 : pppp10-{T}(E39) { 0, 1, 4, 9, 19, 39 }
% 92.66/92.95 620 : r1-{T}(E9,E39) { 0, 1, 4, 9, 19, 39 }
% 92.66/92.95 621 : p104-{T}(E39) { 0, 1, 4, 9, 19, 39 }
% 92.66/92.95 622 : p103-{T}(E39) { 0, 1, 4, 9, 19, 39 }
% 92.66/92.95 623 : p5-{T}(E39) { 0, 1, 4, 9, 19, 39 }
% 92.66/92.95 624 : p102-{T}(E39) { 0, 1, 4, 9, 19, 39 }
% 92.66/92.95 625 : p4-{T}(E39) { 0, 1, 4, 9, 19, 39 }
% 92.66/92.95 626 : p101-{T}(E39) { 0, 1, 4, 9, 19, 39 }
% 92.66/92.95 627 : p100-{T}(E39) { 0, 1, 4, 9, 19, 39 }
% 92.66/92.95 628 : p2-{T}(E39) { 0, 1, 4, 9, 19, 39 }
% 92.66/92.95 629 : #-{T} E40 { 0, 1, 4, 9, 19, 40 }
% 92.66/92.95 630 : pppp0-{T}(E40,E19) { 0, 1, 4, 9, 19, 40 }
% 92.66/92.95 631 : r1-{T}(E40,E40) { 0, 1, 4, 9, 19, 40 }
% 92.66/92.95 632 : p105-{T}(E40) { 0, 1, 4, 9, 19, 40 }
% 92.66/92.95 633 : r1-{T}(E19,E40) { 0, 1, 4, 9, 19, 40 }
% 92.66/92.95 634 : r1-{T}(E4,E40) { 0, 1, 4, 9, 19, 40 }
% 92.66/92.95 635 : r1-{T}(E1,E40) { 0, 1, 4, 9, 19, 40 }
% 92.66/92.95 636 : r1-{T}(E0,E40) { 0, 1, 4, 9, 19, 40 }
% 92.66/92.95 637 : pppp10-{T}(E40) { 0, 1, 4, 9, 19, 40 }
% 92.66/92.95 638 : r1-{T}(E9,E40) { 0, 1, 4, 9, 19, 40 }
% 92.66/92.95 639 : p104-{T}(E40) { 0, 1, 4, 9, 19, 40 }
% 92.66/92.95 640 : p103-{T}(E40) { 0, 1, 4, 9, 19, 40 }
% 92.66/92.95 641 : p5-{T}(E40) { 0, 1, 4, 9, 19, 40 }
% 92.66/92.95 642 : p102-{T}(E40) { 0, 1, 4, 9, 19, 40 }
% 92.66/92.95 643 : p4-{T}(E40) { 0, 1, 4, 9, 19, 40 }
% 92.66/92.95 644 : p101-{T}(E40) { 0, 1, 4, 9, 19, 40 }
% 92.66/92.95 645 : p100-{T}(E40) { 0, 1, 4, 9, 19, 40 }
% 92.66/92.95 646 : p2-{T}(E40) { 0, 1, 4, 9, 19, 40 }
% 92.66/92.95 647 : #-{T} E41 { 0, 1, 4, 9, 20, 41 }
% 92.66/92.95 648 : pppp1-{T}(E41,E20) { 0, 1, 4, 9, 20, 41 }
% 92.66/92.95 649 : r1-{T}(E41,E41) { 0, 1, 4, 9, 20, 41 }
% 92.66/92.95 650 : p105-{T}(E41) { 0, 1, 4, 9, 20, 41 }
% 92.66/92.95 651 : p6-{T}(E41) { 0, 1, 4, 9, 20, 41 }
% 92.66/92.95 652 : r1-{T}(E20,E41) { 0, 1, 4, 9, 20, 41 }
% 92.66/92.95 653 : r1-{T}(E4,E41) { 0, 1, 4, 9, 20, 41 }
% 92.66/92.95 654 : r1-{T}(E1,E41) { 0, 1, 4, 9, 20, 41 }
% 92.66/92.95 655 : r1-{T}(E0,E41) { 0, 1, 4, 9, 20, 41 }
% 92.66/92.95 656 : pppp10-{T}(E41) { 0, 1, 4, 9, 20, 41 }
% 92.66/92.95 657 : r1-{T}(E9,E41) { 0, 1, 4, 9, 20, 41 }
% 92.66/92.95 658 : p104-{T}(E41) { 0, 1, 4, 9, 20, 41 }
% 92.66/92.95 659 : p103-{T}(E41) { 0, 1, 4, 9, 20, 41 }
% 92.66/92.95 660 : p102-{T}(E41) { 0, 1, 4, 9, 20, 41 }
% 92.66/92.95 661 : p4-{T}(E41) { 0, 1, 4, 9, 20, 41 }
% 92.66/92.95 662 : p101-{T}(E41) { 0, 1, 4, 9, 20, 41 }
% 92.66/92.95 663 : p100-{T}(E41) { 0, 1, 4, 9, 20, 41 }
% 92.66/92.95 664 : p2-{T}(E41) { 0, 1, 4, 9, 20, 41 }
% 92.66/92.95 665 : #-{T} E42 { 0, 1, 4, 9, 20, 42 }
% 92.66/92.95 666 : pppp0-{T}(E42,E20) { 0, 1, 4, 9, 20, 42 }
% 92.66/92.95 667 : r1-{T}(E42,E42) { 0, 1, 4, 9, 20, 42 }
% 92.66/92.95 668 : p105-{T}(E42) { 0, 1, 4, 9, 20, 42 }
% 92.66/92.95 669 : r1-{T}(E20,E42) { 0, 1, 4, 9, 20, 42 }
% 92.66/92.95 670 : r1-{T}(E4,E42) { 0, 1, 4, 9, 20, 42 }
% 92.66/92.95 671 : r1-{T}(E1,E42) { 0, 1, 4, 9, 20, 42 }
% 92.66/92.95 672 : r1-{T}(E0,E42) { 0, 1, 4, 9, 20, 42 }
% 92.66/92.95 673 : pppp10-{T}(E42) { 0, 1, 4, 9, 20, 42 }
% 92.66/92.95 674 : r1-{T}(E9,E42) { 0, 1, 4, 9, 20, 42 }
% 92.66/92.95 675 : p104-{T}(E42) { 0, 1, 4, 9, 20, 42 }
% 92.66/92.95 676 : p103-{T}(E42) { 0, 1, 4, 9, 20, 42 }
% 92.66/92.95 677 : p102-{T}(E42) { 0, 1, 4, 9, 20, 42 }
% 92.66/92.95 678 : p4-{T}(E42) { 0, 1, 4, 9, 20, 42 }
% 92.66/92.95 679 : p101-{T}(E42) { 0, 1, 4, 9, 20, 42 }
% 92.66/92.95 680 : p100-{T}(E42) { 0, 1, 4, 9, 20, 42 }
% 92.66/92.95 681 : p2-{T}(E42) { 0, 1, 4, 9, 20, 42 }
% 92.66/92.95 682 : #-{T} E43 { 0, 1, 4, 10, 21, 43 }
% 92.66/92.95 683 : pppp1-{T}(E43,E21) { 0, 1, 4, 10, 21, 43 }
% 92.66/92.95 684 : r1-{T}(E43,E43) { 0, 1, 4, 10, 21, 43 }
% 92.66/92.95 685 : p105-{T}(E43) { 0, 1, 4, 10, 21, 43 }
% 92.66/92.95 686 : p6-{T}(E43) { 0, 1, 4, 10, 21, 43 }
% 92.66/92.95 687 : r1-{T}(E21,E43) { 0, 1, 4, 10, 21, 43 }
% 92.66/92.95 688 : r1-{T}(E4,E43) { 0, 1, 4, 10, 21, 43 }
% 92.66/92.95 689 : r1-{T}(E1,E43) { 0, 1, 4, 10, 21, 43 }
% 92.66/92.95 690 : r1-{T}(E0,E43) { 0, 1, 4, 10, 21, 43 }
% 92.66/92.95 691 : pppp10-{T}(E43) { 0, 1, 4, 10, 21, 43 }
% 92.66/92.95 692 : r1-{T}(E10,E43) { 0, 1, 4, 10, 21, 43 }
% 92.66/92.95 693 : p104-{T}(E43) { 0, 1, 4, 10, 21, 43 }
% 92.66/92.95 694 : p103-{T}(E43) { 0, 1, 4, 10, 21, 43 }
% 92.66/92.95 695 : p5-{T}(E43) { 0, 1, 4, 10, 21, 43 }
% 92.66/92.95 696 : p102-{T}(E43) { 0, 1, 4, 10, 21, 43 }
% 92.66/92.95 697 : p101-{T}(E43) { 0, 1, 4, 10, 21, 43 }
% 92.66/92.95 698 : p100-{T}(E43) { 0, 1, 4, 10, 21, 43 }
% 92.66/92.95 699 : p2-{T}(E43) { 0, 1, 4, 10, 21, 43 }
% 92.66/92.95 700 : #-{T} E44 { 0, 1, 4, 10, 21, 44 }
% 92.66/92.95 701 : pppp0-{T}(E44,E21) { 0, 1, 4, 10, 21, 44 }
% 92.66/92.95 702 : r1-{T}(E44,E44) { 0, 1, 4, 10, 21, 44 }
% 92.66/92.95 703 : p105-{T}(E44) { 0, 1, 4, 10, 21, 44 }
% 92.66/92.95 704 : r1-{T}(E21,E44) { 0, 1, 4, 10, 21, 44 }
% 92.66/92.95 705 : r1-{T}(E4,E44) { 0, 1, 4, 10, 21, 44 }
% 92.66/92.95 706 : r1-{T}(E1,E44) { 0, 1, 4, 10, 21, 44 }
% 92.66/92.95 707 : r1-{T}(E0,E44) { 0, 1, 4, 10, 21, 44 }
% 92.66/92.95 708 : pppp10-{T}(E44) { 0, 1, 4, 10, 21, 44 }
% 92.66/92.95 709 : r1-{T}(E10,E44) { 0, 1, 4, 10, 21, 44 }
% 92.66/92.95 710 : p104-{T}(E44) { 0, 1, 4, 10, 21, 44 }
% 92.66/92.95 711 : p103-{T}(E44) { 0, 1, 4, 10, 21, 44 }
% 92.66/92.95 712 : p5-{T}(E44) { 0, 1, 4, 10, 21, 44 }
% 92.66/92.95 713 : p102-{T}(E44) { 0, 1, 4, 10, 21, 44 }
% 92.66/92.95 714 : p101-{T}(E44) { 0, 1, 4, 10, 21, 44 }
% 92.66/92.95 715 : p100-{T}(E44) { 0, 1, 4, 10, 21, 44 }
% 92.66/92.95 716 : p2-{T}(E44) { 0, 1, 4, 10, 21, 44 }
% 92.66/92.95 717 : #-{T} E45 { 0, 1, 4, 10, 22, 45 }
% 92.66/92.95 718 : pppp1-{T}(E45,E22) { 0, 1, 4, 10, 22, 45 }
% 92.66/92.95 719 : r1-{T}(E45,E45) { 0, 1, 4, 10, 22, 45 }
% 92.66/92.95 720 : p105-{T}(E45) { 0, 1, 4, 10, 22, 45 }
% 92.66/92.95 721 : p6-{T}(E45) { 0, 1, 4, 10, 22, 45 }
% 92.66/92.95 722 : r1-{T}(E22,E45) { 0, 1, 4, 10, 22, 45 }
% 92.66/92.95 723 : r1-{T}(E4,E45) { 0, 1, 4, 10, 22, 45 }
% 92.66/92.95 724 : r1-{T}(E1,E45) { 0, 1, 4, 10, 22, 45 }
% 92.66/92.95 725 : r1-{T}(E0,E45) { 0, 1, 4, 10, 22, 45 }
% 92.66/92.95 726 : pppp10-{T}(E45) { 0, 1, 4, 10, 22, 45 }
% 92.66/92.95 727 : r1-{T}(E10,E45) { 0, 1, 4, 10, 22, 45 }
% 92.66/92.95 728 : p104-{T}(E45) { 0, 1, 4, 10, 22, 45 }
% 92.66/92.95 729 : p103-{T}(E45) { 0, 1, 4, 10, 22, 45 }
% 92.66/92.95 730 : p102-{T}(E45) { 0, 1, 4, 10, 22, 45 }
% 92.66/92.95 731 : p101-{T}(E45) { 0, 1, 4, 10, 22, 45 }
% 92.66/92.95 732 : p100-{T}(E45) { 0, 1, 4, 10, 22, 45 }
% 92.66/92.95 733 : p2-{T}(E45) { 0, 1, 4, 10, 22, 45 }
% 92.66/92.95 734 : #-{T} E46 { 0, 1, 4, 10, 22, 46 }
% 92.66/92.95 735 : pppp0-{T}(E46,E22) { 0, 1, 4, 10, 22, 46 }
% 92.66/92.95 736 : r1-{T}(E46,E46) { 0, 1, 4, 10, 22, 46 }
% 92.66/92.95 737 : p105-{T}(E46) { 0, 1, 4, 10, 22, 46 }
% 92.66/92.95 738 : r1-{T}(E22,E46) { 0, 1, 4, 10, 22, 46 }
% 92.66/92.95 739 : r1-{T}(E4,E46) { 0, 1, 4, 10, 22, 46 }
% 92.66/92.95 740 : r1-{T}(E1,E46) { 0, 1, 4, 10, 22, 46 }
% 92.66/92.95 741 : r1-{T}(E0,E46) { 0, 1, 4, 10, 22, 46 }
% 92.66/92.95 742 : pppp10-{T}(E46) { 0, 1, 4, 10, 22, 46 }
% 92.66/92.95 743 : r1-{T}(E10,E46) { 0, 1, 4, 10, 22, 46 }
% 92.66/92.95 744 : p104-{T}(E46) { 0, 1, 4, 10, 22, 46 }
% 92.66/92.95 745 : p103-{T}(E46) { 0, 1, 4, 10, 22, 46 }
% 92.66/92.95 746 : p102-{T}(E46) { 0, 1, 4, 10, 22, 46 }
% 92.66/92.95 747 : p101-{T}(E46) { 0, 1, 4, 10, 22, 46 }
% 92.66/92.95 748 : p100-{T}(E46) { 0, 1, 4, 10, 22, 46 }
% 92.66/92.95 749 : p2-{T}(E46) { 0, 1, 4, 10, 22, 46 }
% 92.66/92.95 750 : #-{T} E47 { 0, 2, 5, 11, 23, 47 }
% 92.66/92.95 751 : pppp1-{T}(E47,E23) { 0, 2, 5, 11, 23, 47 }
% 92.66/92.95 752 : r1-{T}(E47,E47) { 0, 2, 5, 11, 23, 47 }
% 92.66/92.95 753 : p105-{T}(E47) { 0, 2, 5, 11, 23, 47 }
% 92.66/92.95 754 : p6-{T}(E47) { 0, 2, 5, 11, 23, 47 }
% 92.66/92.95 755 : r1-{T}(E23,E47) { 0, 2, 5, 11, 23, 47 }
% 92.66/92.95 756 : r1-{T}(E5,E47) { 0, 2, 5, 11, 23, 47 }
% 92.66/92.95 757 : r1-{T}(E2,E47) { 0, 2, 5, 11, 23, 47 }
% 92.66/92.95 758 : r1-{T}(E1,E47) { 0, 2, 5, 11, 23, 47 }
% 92.66/92.95 759 : r1-{T}(E11,E47) { 0, 2, 5, 11, 23, 47 }
% 92.66/92.95 760 : pppp10-{T}(E47) { 0, 2, 5, 11, 23, 47 }
% 92.66/92.95 761 : p104-{T}(E47) { 0, 2, 5, 11, 23, 47 }
% 92.66/92.95 762 : p103-{T}(E47) { 0, 2, 5, 11, 23, 47 }
% 92.66/92.95 763 : p5-{T}(E47) { 0, 2, 5, 11, 23, 47 }
% 92.66/92.95 764 : p102-{T}(E47) { 0, 2, 5, 11, 23, 47 }
% 92.66/92.95 765 : p4-{T}(E47) { 0, 2, 5, 11, 23, 47 }
% 92.66/92.95 766 : p101-{T}(E47) { 0, 2, 5, 11, 23, 47 }
% 92.66/92.95 767 : p3-{T}(E47) { 0, 2, 5, 11, 23, 47 }
% 92.66/92.95 768 : p100-{T}(E47) { 0, 2, 5, 11, 23, 47 }
% 92.66/92.95 769 : #-{T} E48 { 0, 2, 5, 11, 23, 48 }
% 92.66/92.95 770 : pppp0-{T}(E48,E23) { 0, 2, 5, 11, 23, 48 }
% 92.66/92.95 771 : r1-{T}(E48,E48) { 0, 2, 5, 11, 23, 48 }
% 92.66/92.95 772 : p105-{T}(E48) { 0, 2, 5, 11, 23, 48 }
% 92.66/92.95 773 : r1-{T}(E23,E48) { 0, 2, 5, 11, 23, 48 }
% 92.66/92.95 774 : r1-{T}(E5,E48) { 0, 2, 5, 11, 23, 48 }
% 92.66/92.95 775 : r1-{T}(E2,E48) { 0, 2, 5, 11, 23, 48 }
% 92.66/92.95 776 : r1-{T}(E1,E48) { 0, 2, 5, 11, 23, 48 }
% 92.66/92.95 777 : r1-{T}(E11,E48) { 0, 2, 5, 11, 23, 48 }
% 92.66/92.95 778 : pppp10-{T}(E48) { 0, 2, 5, 11, 23, 48 }
% 92.66/92.95 779 : p104-{T}(E48) { 0, 2, 5, 11, 23, 48 }
% 92.66/92.95 780 : p103-{T}(E48) { 0, 2, 5, 11, 23, 48 }
% 92.66/92.95 781 : p5-{T}(E48) { 0, 2, 5, 11, 23, 48 }
% 92.66/92.95 782 : p102-{T}(E48) { 0, 2, 5, 11, 23, 48 }
% 92.66/92.95 783 : p4-{T}(E48) { 0, 2, 5, 11, 23, 48 }
% 92.66/92.95 784 : p101-{T}(E48) { 0, 2, 5, 11, 23, 48 }
% 92.66/92.95 785 : p3-{T}(E48) { 0, 2, 5, 11, 23, 48 }
% 92.66/92.95 786 : p100-{T}(E48) { 0, 2, 5, 11, 23, 48 }
% 92.66/92.95 787 : #-{T} E49 { 0, 2, 5, 11, 24, 49 }
% 92.66/92.95 788 : pppp1-{T}(E49,E24) { 0, 2, 5, 11, 24, 49 }
% 92.66/92.95 789 : r1-{T}(E49,E49) { 0, 2, 5, 11, 24, 49 }
% 92.66/92.95 790 : p105-{T}(E49) { 0, 2, 5, 11, 24, 49 }
% 92.66/92.95 791 : p6-{T}(E49) { 0, 2, 5, 11, 24, 49 }
% 92.66/92.95 792 : r1-{T}(E24,E49) { 0, 2, 5, 11, 24, 49 }
% 92.66/92.95 793 : r1-{T}(E5,E49) { 0, 2, 5, 11, 24, 49 }
% 92.66/92.95 794 : r1-{T}(E2,E49) { 0, 2, 5, 11, 24, 49 }
% 92.66/92.95 795 : r1-{T}(E1,E49) { 0, 2, 5, 11, 24, 49 }
% 92.66/92.95 796 : r1-{T}(E11,E49) { 0, 2, 5, 11, 24, 49 }
% 92.66/92.95 797 : pppp10-{T}(E49) { 0, 2, 5, 11, 24, 49 }
% 92.66/92.95 798 : p104-{T}(E49) { 0, 2, 5, 11, 24, 49 }
% 92.66/92.95 799 : p103-{T}(E49) { 0, 2, 5, 11, 24, 49 }
% 92.66/92.95 800 : p102-{T}(E49) { 0, 2, 5, 11, 24, 49 }
% 92.66/92.95 801 : p4-{T}(E49) { 0, 2, 5, 11, 24, 49 }
% 92.66/92.95 802 : p101-{T}(E49) { 0, 2, 5, 11, 24, 49 }
% 92.66/92.95 803 : p3-{T}(E49) { 0, 2, 5, 11, 24, 49 }
% 92.66/92.95 804 : p100-{T}(E49) { 0, 2, 5, 11, 24, 49 }
% 92.66/92.95 805 : #-{T} E50 { 0, 2, 5, 11, 24, 50 }
% 92.66/92.95 806 : pppp0-{T}(E50,E24) { 0, 2, 5, 11, 24, 50 }
% 92.66/92.95 807 : r1-{T}(E50,E50) { 0, 2, 5, 11, 24, 50 }
% 92.66/92.95 808 : p105-{T}(E50) { 0, 2, 5, 11, 24, 50 }
% 92.66/92.95 809 : r1-{T}(E24,E50) { 0, 2, 5, 11, 24, 50 }
% 92.66/92.95 810 : r1-{T}(E5,E50) { 0, 2, 5, 11, 24, 50 }
% 92.66/92.95 811 : r1-{T}(E2,E50) { 0, 2, 5, 11, 24, 50 }
% 92.66/92.95 812 : r1-{T}(E1,E50) { 0, 2, 5, 11, 24, 50 }
% 92.66/92.95 813 : r1-{T}(E11,E50) { 0, 2, 5, 11, 24, 50 }
% 92.66/92.95 814 : pppp10-{T}(E50) { 0, 2, 5, 11, 24, 50 }
% 92.66/92.95 815 : p104-{T}(E50) { 0, 2, 5, 11, 24, 50 }
% 92.66/92.95 816 : p103-{T}(E50) { 0, 2, 5, 11, 24, 50 }
% 92.66/92.95 817 : p102-{T}(E50) { 0, 2, 5, 11, 24, 50 }
% 92.66/92.95 818 : p4-{T}(E50) { 0, 2, 5, 11, 24, 50 }
% 92.66/92.95 819 : p101-{T}(E50) { 0, 2, 5, 11, 24, 50 }
% 92.66/92.95 820 : p3-{T}(E50) { 0, 2, 5, 11, 24, 50 }
% 92.66/92.95 821 : p100-{T}(E50) { 0, 2, 5, 11, 24, 50 }
% 92.66/92.95 822 : #-{T} E51 { 0, 2, 5, 12, 25, 51 }
% 92.66/92.95 823 : pppp1-{T}(E51,E25) { 0, 2, 5, 12, 25, 51 }
% 92.66/92.95 824 : r1-{T}(E51,E51) { 0, 2, 5, 12, 25, 51 }
% 92.66/92.95 825 : p105-{T}(E51) { 0, 2, 5, 12, 25, 51 }
% 92.66/92.95 826 : p6-{T}(E51) { 0, 2, 5, 12, 25, 51 }
% 92.66/92.95 827 : r1-{T}(E25,E51) { 0, 2, 5, 12, 25, 51 }
% 92.66/92.95 828 : r1-{T}(E5,E51) { 0, 2, 5, 12, 25, 51 }
% 92.66/92.95 829 : r1-{T}(E1,E51) { 0, 2, 5, 12, 25, 51 }
% 92.66/92.95 830 : r1-{T}(E2,E51) { 0, 2, 5, 12, 25, 51 }
% 92.66/92.95 831 : pppp10-{T}(E51) { 0, 2, 5, 12, 25, 51 }
% 92.66/92.95 832 : r1-{T}(E12,E51) { 0, 2, 5, 12, 25, 51 }
% 92.66/92.95 833 : p104-{T}(E51) { 0, 2, 5, 12, 25, 51 }
% 92.66/92.95 834 : p103-{T}(E51) { 0, 2, 5, 12, 25, 51 }
% 92.66/92.95 835 : p5-{T}(E51) { 0, 2, 5, 12, 25, 51 }
% 92.66/92.95 836 : p102-{T}(E51) { 0, 2, 5, 12, 25, 51 }
% 92.66/92.95 837 : p101-{T}(E51) { 0, 2, 5, 12, 25, 51 }
% 92.66/92.95 838 : p3-{T}(E51) { 0, 2, 5, 12, 25, 51 }
% 92.66/92.95 839 : p100-{T}(E51) { 0, 2, 5, 12, 25, 51 }
% 92.66/92.95 840 : #-{T} E52 { 0, 2, 5, 12, 25, 52 }
% 92.66/92.95 841 : pppp0-{T}(E52,E25) { 0, 2, 5, 12, 25, 52 }
% 92.66/92.95 842 : r1-{T}(E52,E52) { 0, 2, 5, 12, 25, 52 }
% 92.66/92.95 843 : p105-{T}(E52) { 0, 2, 5, 12, 25, 52 }
% 92.66/92.95 844 : r1-{T}(E25,E52) { 0, 2, 5, 12, 25, 52 }
% 92.66/92.95 845 : r1-{T}(E5,E52) { 0, 2, 5, 12, 25, 52 }
% 92.66/92.95 846 : r1-{T}(E1,E52) { 0, 2, 5, 12, 25, 52 }
% 92.66/92.95 847 : r1-{T}(E2,E52) { 0, 2, 5, 12, 25, 52 }
% 92.66/92.95 848 : pppp10-{T}(E52) { 0, 2, 5, 12, 25, 52 }
% 92.66/92.95 849 : r1-{T}(E12,E52) { 0, 2, 5, 12, 25, 52 }
% 92.66/92.95 850 : p104-{T}(E52) { 0, 2, 5, 12, 25, 52 }
% 92.66/92.95 851 : p103-{T}(E52) { 0, 2, 5, 12, 25, 52 }
% 92.66/92.95 852 : p5-{T}(E52) { 0, 2, 5, 12, 25, 52 }
% 92.66/92.95 853 : p102-{T}(E52) { 0, 2, 5, 12, 25, 52 }
% 92.66/92.95 854 : p101-{T}(E52) { 0, 2, 5, 12, 25, 52 }
% 92.66/92.95 855 : p3-{T}(E52) { 0, 2, 5, 12, 25, 52 }
% 92.66/92.95 856 : p100-{T}(E52) { 0, 2, 5, 12, 25, 52 }
% 92.66/92.95 857 : #-{T} E53 { 0, 2, 5, 12, 26, 53 }
% 92.66/92.95 858 : pppp1-{T}(E53,E26) { 0, 2, 5, 12, 26, 53 }
% 92.66/92.95 859 : r1-{T}(E53,E53) { 0, 2, 5, 12, 26, 53 }
% 92.66/92.95 860 : p105-{T}(E53) { 0, 2, 5, 12, 26, 53 }
% 92.66/92.95 861 : p6-{T}(E53) { 0, 2, 5, 12, 26, 53 }
% 92.66/92.95 862 : r1-{T}(E26,E53) { 0, 2, 5, 12, 26, 53 }
% 92.66/92.95 863 : r1-{T}(E5,E53) { 0, 2, 5, 12, 26, 53 }
% 92.66/92.95 864 : r1-{T}(E1,E53) { 0, 2, 5, 12, 26, 53 }
% 92.66/92.95 865 : r1-{T}(E2,E53) { 0, 2, 5, 12, 26, 53 }
% 92.66/92.95 866 : pppp10-{T}(E53) { 0, 2, 5, 12, 26, 53 }
% 92.66/92.95 867 : r1-{T}(E12,E53) { 0, 2, 5, 12, 26, 53 }
% 92.66/92.95 868 : p104-{T}(E53) { 0, 2, 5, 12, 26, 53 }
% 92.66/92.95 869 : p103-{T}(E53) { 0, 2, 5, 12, 26, 53 }
% 92.66/92.95 870 : p102-{T}(E53) { 0, 2, 5, 12, 26, 53 }
% 92.66/92.95 871 : p101-{T}(E53) { 0, 2, 5, 12, 26, 53 }
% 92.66/92.95 872 : p3-{T}(E53) { 0, 2, 5, 12, 26, 53 }
% 92.66/92.95 873 : p100-{T}(E53) { 0, 2, 5, 12, 26, 53 }
% 92.66/92.95 874 : #-{T} E54 { 0, 2, 5, 12, 26, 54 }
% 92.66/92.95 875 : pppp0-{T}(E54,E26) { 0, 2, 5, 12, 26, 54 }
% 92.66/92.95 876 : r1-{T}(E54,E54) { 0, 2, 5, 12, 26, 54 }
% 92.66/92.95 877 : p105-{T}(E54) { 0, 2, 5, 12, 26, 54 }
% 92.66/92.95 878 : r1-{T}(E26,E54) { 0, 2, 5, 12, 26, 54 }
% 92.66/92.95 879 : r1-{T}(E5,E54) { 0, 2, 5, 12, 26, 54 }
% 92.66/92.95 880 : r1-{T}(E1,E54) { 0, 2, 5, 12, 26, 54 }
% 92.66/92.95 881 : r1-{T}(E2,E54) { 0, 2, 5, 12, 26, 54 }
% 92.66/92.95 882 : pppp10-{T}(E54) { 0, 2, 5, 12, 26, 54 }
% 92.66/92.95 883 : r1-{T}(E12,E54) { 0, 2, 5, 12, 26, 54 }
% 92.66/92.95 884 : p104-{T}(E54) { 0, 2, 5, 12, 26, 54 }
% 92.66/92.95 885 : p103-{T}(E54) { 0, 2, 5, 12, 26, 54 }
% 92.66/92.95 886 : p102-{T}(E54) { 0, 2, 5, 12, 26, 54 }
% 92.66/92.95 887 : p101-{T}(E54) { 0, 2, 5, 12, 26, 54 }
% 92.66/92.95 888 : p3-{T}(E54) { 0, 2, 5, 12, 26, 54 }
% 92.66/92.95 889 : p100-{T}(E54) { 0, 2, 5, 12, 26, 54 }
% 92.66/92.95 890 : #-{T} E55 { 0, 2, 6, 13, 27, 55 }
% 92.66/92.95 891 : pppp1-{T}(E55,E27) { 0, 2, 6, 13, 27, 55 }
% 92.66/92.95 892 : r1-{T}(E55,E55) { 0, 2, 6, 13, 27, 55 }
% 92.66/92.95 893 : p105-{T}(E55) { 0, 2, 6, 13, 27, 55 }
% 92.66/92.95 894 : p6-{T}(E55) { 0, 2, 6, 13, 27, 55 }
% 92.66/92.95 895 : r1-{T}(E27,E55) { 0, 2, 6, 13, 27, 55 }
% 92.66/92.95 896 : r1-{T}(E6,E55) { 0, 2, 6, 13, 27, 55 }
% 92.66/92.95 897 : r1-{T}(E1,E55) { 0, 2, 6, 13, 27, 55 }
% 92.66/92.95 898 : r1-{T}(E2,E55) { 0, 2, 6, 13, 27, 55 }
% 92.66/92.95 899 : pppp10-{T}(E55) { 0, 2, 6, 13, 27, 55 }
% 92.66/92.95 900 : r1-{T}(E13,E55) { 0, 2, 6, 13, 27, 55 }
% 92.66/92.95 901 : p104-{T}(E55) { 0, 2, 6, 13, 27, 55 }
% 92.66/92.95 902 : p103-{T}(E55) { 0, 2, 6, 13, 27, 55 }
% 92.66/92.95 903 : p5-{T}(E55) { 0, 2, 6, 13, 27, 55 }
% 92.66/92.95 904 : p102-{T}(E55) { 0, 2, 6, 13, 27, 55 }
% 92.66/92.95 905 : p4-{T}(E55) { 0, 2, 6, 13, 27, 55 }
% 92.66/92.95 906 : p101-{T}(E55) { 0, 2, 6, 13, 27, 55 }
% 92.66/92.95 907 : p100-{T}(E55) { 0, 2, 6, 13, 27, 55 }
% 92.66/92.95 908 : #-{T} E56 { 0, 2, 6, 13, 27, 56 }
% 92.66/92.95 909 : pppp0-{T}(E56,E27) { 0, 2, 6, 13, 27, 56 }
% 92.66/92.95 910 : r1-{T}(E56,E56) { 0, 2, 6, 13, 27, 56 }
% 92.66/92.95 911 : p105-{T}(E56) { 0, 2, 6, 13, 27, 56 }
% 92.66/92.95 912 : r1-{T}(E27,E56) { 0, 2, 6, 13, 27, 56 }
% 92.66/92.95 913 : r1-{T}(E6,E56) { 0, 2, 6, 13, 27, 56 }
% 92.66/92.95 914 : r1-{T}(E1,E56) { 0, 2, 6, 13, 27, 56 }
% 92.66/92.95 915 : r1-{T}(E2,E56) { 0, 2, 6, 13, 27, 56 }
% 92.66/92.95 916 : pppp10-{T}(E56) { 0, 2, 6, 13, 27, 56 }
% 92.66/92.95 917 : r1-{T}(E13,E56) { 0, 2, 6, 13, 27, 56 }
% 92.66/92.95 918 : p104-{T}(E56) { 0, 2, 6, 13, 27, 56 }
% 92.66/92.95 919 : p103-{T}(E56) { 0, 2, 6, 13, 27, 56 }
% 92.66/92.95 920 : p5-{T}(E56) { 0, 2, 6, 13, 27, 56 }
% 92.66/92.95 921 : p102-{T}(E56) { 0, 2, 6, 13, 27, 56 }
% 92.66/92.95 922 : p4-{T}(E56) { 0, 2, 6, 13, 27, 56 }
% 92.66/92.95 923 : p101-{T}(E56) { 0, 2, 6, 13, 27, 56 }
% 92.66/92.95 924 : p100-{T}(E56) { 0, 2, 6, 13, 27, 56 }
% 92.66/92.95 925 : #-{T} E57 { 0, 2, 6, 13, 28, 57 }
% 92.66/92.95 926 : pppp1-{T}(E57,E28) { 0, 2, 6, 13, 28, 57 }
% 92.66/92.95 927 : r1-{T}(E57,E57) { 0, 2, 6, 13, 28, 57 }
% 92.66/92.95 928 : p105-{T}(E57) { 0, 2, 6, 13, 28, 57 }
% 92.66/92.95 929 : p6-{T}(E57) { 0, 2, 6, 13, 28, 57 }
% 92.66/92.95 930 : r1-{T}(E28,E57) { 0, 2, 6, 13, 28, 57 }
% 92.66/92.95 931 : r1-{T}(E6,E57) { 0, 2, 6, 13, 28, 57 }
% 92.66/92.95 932 : r1-{T}(E1,E57) { 0, 2, 6, 13, 28, 57 }
% 92.66/92.95 933 : r1-{T}(E2,E57) { 0, 2, 6, 13, 28, 57 }
% 92.66/92.95 934 : pppp10-{T}(E57) { 0, 2, 6, 13, 28, 57 }
% 92.66/92.95 935 : r1-{T}(E13,E57) { 0, 2, 6, 13, 28, 57 }
% 92.66/92.95 936 : p104-{T}(E57) { 0, 2, 6, 13, 28, 57 }
% 92.66/92.95 937 : p103-{T}(E57) { 0, 2, 6, 13, 28, 57 }
% 92.66/92.95 938 : p102-{T}(E57) { 0, 2, 6, 13, 28, 57 }
% 92.66/92.95 939 : p4-{T}(E57) { 0, 2, 6, 13, 28, 57 }
% 92.66/92.95 940 : p101-{T}(E57) { 0, 2, 6, 13, 28, 57 }
% 92.66/92.95 941 : p100-{T}(E57) { 0, 2, 6, 13, 28, 57 }
% 92.66/92.95 942 : #-{T} E58 { 0, 2, 6, 13, 28, 58 }
% 92.66/92.95 943 : pppp0-{T}(E58,E28) { 0, 2, 6, 13, 28, 58 }
% 92.66/92.95 944 : r1-{T}(E58,E58) { 0, 2, 6, 13, 28, 58 }
% 92.66/92.95 945 : p105-{T}(E58) { 0, 2, 6, 13, 28, 58 }
% 92.66/92.95 946 : r1-{T}(E28,E58) { 0, 2, 6, 13, 28, 58 }
% 92.66/92.95 947 : r1-{T}(E6,E58) { 0, 2, 6, 13, 28, 58 }
% 92.66/92.95 948 : r1-{T}(E1,E58) { 0, 2, 6, 13, 28, 58 }
% 92.66/92.95 949 : r1-{T}(E2,E58) { 0, 2, 6, 13, 28, 58 }
% 92.66/92.95 950 : pppp10-{T}(E58) { 0, 2, 6, 13, 28, 58 }
% 92.66/92.95 951 : r1-{T}(E13,E58) { 0, 2, 6, 13, 28, 58 }
% 92.66/92.95 952 : p104-{T}(E58) { 0, 2, 6, 13, 28, 58 }
% 92.66/92.95 953 : p103-{T}(E58) { 0, 2, 6, 13, 28, 58 }
% 92.66/92.95 954 : p102-{T}(E58) { 0, 2, 6, 13, 28, 58 }
% 92.66/92.95 955 : p4-{T}(E58) { 0, 2, 6, 13, 28, 58 }
% 92.66/92.95 956 : p101-{T}(E58) { 0, 2, 6, 13, 28, 58 }
% 92.66/92.95 957 : p100-{T}(E58) { 0, 2, 6, 13, 28, 58 }
% 92.66/92.95 958 : #-{T} E59 { 0, 2, 6, 14, 29, 59 }
% 92.66/92.95 959 : pppp1-{T}(E59,E29) { 0, 2, 6, 14, 29, 59 }
% 92.66/92.95 960 : r1-{T}(E59,E59) { 0, 2, 6, 14, 29, 59 }
% 92.66/92.95 961 : p105-{T}(E59) { 0, 2, 6, 14, 29, 59 }
% 92.66/92.95 962 : p6-{T}(E59) { 0, 2, 6, 14, 29, 59 }
% 92.66/92.95 963 : r1-{T}(E29,E59) { 0, 2, 6, 14, 29, 59 }
% 92.66/92.95 964 : r1-{T}(E6,E59) { 0, 2, 6, 14, 29, 59 }
% 92.66/92.95 965 : r1-{T}(E2,E59) { 0, 2, 6, 14, 29, 59 }
% 92.66/92.95 966 : r1-{T}(E1,E59) { 0, 2, 6, 14, 29, 59 }
% 92.66/92.95 967 : r1-{T}(E14,E59) { 0, 2, 6, 14, 29, 59 }
% 92.66/92.95 968 : pppp10-{T}(E59) { 0, 2, 6, 14, 29, 59 }
% 92.66/92.95 969 : p104-{T}(E59) { 0, 2, 6, 14, 29, 59 }
% 92.66/92.95 970 : p103-{T}(E59) { 0, 2, 6, 14, 29, 59 }
% 92.66/92.95 971 : p5-{T}(E59) { 0, 2, 6, 14, 29, 59 }
% 92.66/92.95 972 : p102-{T}(E59) { 0, 2, 6, 14, 29, 59 }
% 92.66/92.95 973 : p101-{T}(E59) { 0, 2, 6, 14, 29, 59 }
% 92.66/92.95 974 : p100-{T}(E59) { 0, 2, 6, 14, 29, 59 }
% 92.66/92.95 975 : #-{T} E60 { 0, 2, 6, 14, 29, 60 }
% 92.66/92.95 976 : pppp0-{T}(E60,E29) { 0, 2, 6, 14, 29, 60 }
% 92.66/92.95 977 : r1-{T}(E60,E60) { 0, 2, 6, 14, 29, 60 }
% 92.66/92.95 978 : p105-{T}(E60) { 0, 2, 6, 14, 29, 60 }
% 92.66/92.95 979 : r1-{T}(E29,E60) { 0, 2, 6, 14, 29, 60 }
% 92.66/92.95 980 : r1-{T}(E6,E60) { 0, 2, 6, 14, 29, 60 }
% 92.66/92.95 981 : r1-{T}(E2,E60) { 0, 2, 6, 14, 29, 60 }
% 92.66/92.95 982 : r1-{T}(E1,E60) { 0, 2, 6, 14, 29, 60 }
% 92.66/92.95 983 : r1-{T}(E14,E60) { 0, 2, 6, 14, 29, 60 }
% 92.66/92.95 984 : pppp10-{T}(E60) { 0, 2, 6, 14, 29, 60 }
% 92.66/92.95 985 : p104-{T}(E60) { 0, 2, 6, 14, 29, 60 }
% 92.66/92.95 986 : p103-{T}(E60) { 0, 2, 6, 14, 29, 60 }
% 92.66/92.95 987 : p5-{T}(E60) { 0, 2, 6, 14, 29, 60 }
% 92.66/92.95 988 : p102-{T}(E60) { 0, 2, 6, 14, 29, 60 }
% 92.66/92.95 989 : p101-{T}(E60) { 0, 2, 6, 14, 29, 60 }
% 92.66/92.95 990 : p100-{T}(E60) { 0, 2, 6, 14, 29, 60 }
% 92.66/92.95 991 : #-{T} E61 { 0, 2, 6, 14, 30, 61 }
% 92.66/92.95 992 : pppp1-{T}(E61,E30) { 0, 2, 6, 14, 30, 61 }
% 92.66/92.95 993 : r1-{T}(E61,E61) { 0, 2, 6, 14, 30, 61 }
% 92.66/92.95 994 : p105-{T}(E61) { 0, 2, 6, 14, 30, 61 }
% 92.66/92.95 995 : p6-{T}(E61) { 0, 2, 6, 14, 30, 61 }
% 92.66/92.95 996 : r1-{T}(E30,E61) { 0, 2, 6, 14, 30, 61 }
% 92.66/92.95 997 : r1-{T}(E6,E61) { 0, 2, 6, 14, 30, 61 }
% 92.66/92.95 998 : r1-{T}(E2,E61) { 0, 2, 6, 14, 30, 61 }
% 92.66/92.95 999 : r1-{T}(E1,E61) { 0, 2, 6, 14, 30, 61 }
% 92.66/92.95 1000 : r1-{T}(E14,E61) { 0, 2, 6, 14, 30, 61 }
% 92.66/92.95 1001 : pppp10-{T}(E61) { 0, 2, 6, 14, 30, 61 }
% 92.66/92.95 1002 : p104-{T}(E61) { 0, 2, 6, 14, 30, 61 }
% 92.66/92.95 1003 : p103-{T}(E61) { 0, 2, 6, 14, 30, 61 }
% 92.66/92.95 1004 : p102-{T}(E61) { 0, 2, 6, 14, 30, 61 }
% 92.66/92.95 1005 : p101-{T}(E61) { 0, 2, 6, 14, 30, 61 }
% 92.66/92.95 1006 : p100-{T}(E61) { 0, 2, 6, 14, 30, 61 }
% 92.66/92.95 1007 : #-{T} E62 { 0, 2, 6, 14, 30, 62 }
% 92.66/92.95 1008 : pppp0-{T}(E62,E30) { 0, 2, 6, 14, 30, 62 }
% 92.66/92.95 1009 : r1-{T}(E62,E62) { 0, 2, 6, 14, 30, 62 }
% 92.66/92.95 1010 : p105-{T}(E62) { 0, 2, 6, 14, 30, 62 }
% 92.66/92.95 1011 : r1-{T}(E30,E62) { 0, 2, 6, 14, 30, 62 }
% 92.66/92.95 1012 : r1-{T}(E6,E62) { 0, 2, 6, 14, 30, 62 }
% 92.66/92.95 1013 : r1-{T}(E2,E62) { 0, 2, 6, 14, 30, 62 }
% 92.66/92.95 1014 : r1-{T}(E1,E62) { 0, 2, 6, 14, 30, 62 }
% 92.66/92.95 1015 : r1-{T}(E14,E62) { 0, 2, 6, 14, 30, 62 }
% 92.66/92.95 1016 : pppp10-{T}(E62) { 0, 2, 6, 14, 30, 62 }
% 92.66/92.95 1017 : p104-{T}(E62) { 0, 2, 6, 14, 30, 62 }
% 92.66/92.95 1018 : p103-{T}(E62) { 0, 2, 6, 14, 30, 62 }
% 92.66/92.95 1019 : p102-{T}(E62) { 0, 2, 6, 14, 30, 62 }
% 92.66/92.95 1020 : p101-{T}(E62) { 0, 2, 6, 14, 30, 62 }
% 92.66/92.95 1021 : p100-{T}(E62) { 0, 2, 6, 14, 30, 62 }
% 92.66/92.95
% 92.66/92.95
% 92.66/92.95 % SZS output end Model for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 92.66/92.95
% 92.66/92.95 randbase = 1
%------------------------------------------------------------------------------