%------------------------------------------------------------------------------
% File : Geo-III---2018C
% Problem : LCL637+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : geo -tptp_input -nonempty -inputfile %s
% Computer : n003.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:30 PM UTC 2026
% Result : CounterSatisfiable 136.94s 137.27s
% Output : Model 136.94s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL637+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : geo -tptp_input -nonempty -inputfile %s
% 0.07/0.32 % Computer : n003.cluster.edu
% 0.07/0.32 % Model : x86_64 x86_64
% 0.07/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.32 % Memory : 8046.5625MB
% 0.07/0.32 % OS : Linux 6.8.0-71-generic
% 0.07/0.32 % CPULimit : 300
% 0.07/0.32 % WCLimit : 300
% 0.07/0.32 % DateTime : Sat Sep 5 08:26:50 UTC 2026
% 0.07/0.33 % CPUTime :
% 136.94/137.27 GeoParameters:
% 136.94/137.27
% 136.94/137.27 tptp_input = 1
% 136.94/137.27 tptp_output = 0
% 136.94/137.27 nonempty = 1
% 136.94/137.27 inputfile = /export/starexec/sandbox/benchmark/theBenchmark.p
% 136.94/137.27 includepath = /export/starexec/sandbox/solver/bin/../../benchmark/
% 136.94/137.27
% 136.94/137.27
% 136.94/137.27 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 136.94/137.27 % SZS output start Model for /export/starexec/sandbox/benchmark/theBenchmark.p
% 136.94/137.27
% 136.94/137.27 Interpretation 1201:
% 136.94/137.27 Guesses:
% 136.94/137.27 0 : guesser 1, 0, ( | 1, 0 ), 0, 2m16s old, 0 lemmas
% 136.94/137.27 1 : guesser 7, 5, ( | 0, 2, 1 ), 2, 2m16s old, 0 lemmas
% 136.94/137.27 2 : guesser 15, 13, ( 0 | 2, 1 ), 5, 2m16s old, 1 lemmas
% 136.94/137.27 3 : guesser 23, 20, ( 1, 0 | 3, 2 ), 8, 2m16s old, 2 lemmas
% 136.94/137.27 4 : guesser 34, 30, ( 3, 2, 1 | 4, 0 ), 24, 2m16s old, 3 lemmas
% 136.94/137.27 5 : guesser 44, 39, ( 3, 0, 2, 4 | 5, 1 ), 60, 2m15s old, 2 lemmas
% 136.94/137.27 6 : guesser 54, 48, ( 1, 0, 5, 4, 3 | 6, 2 ), 63, 2m15s old, 4 lemmas
% 136.94/137.27 7 : guesser 63, 56, ( 0, 4, 1, 5, 2, 6 | 7, 3 ), 67, 2m15s old, 6 lemmas
% 136.94/137.27 8 : guesser 76, 68, ( 6, 5, 4, 3, 2, 1, 0 | 8, 7 ), 183, 2m10s old, 6 lemmas
% 136.94/137.27 9 : guesser 88, 79, ( 6, 5, 4, 3, 2, 1, 0, 8 | 9, 7 ), 266, 2m6s old, 7 lemmas
% 136.94/137.27 10 : guesser 100, 90, ( 2, 9, 6, 3, 0, 7, 4, 1, 8 | 10, 5 ), 272, 2m6s old, 8 lemmas
% 136.94/137.27 11 : guesser 111, 100, ( 0, 8, 5, 2, 10, 7, 4, 1, 9, 6 | 11, 3 ), 279, 2m5s old, 7 lemmas
% 136.94/137.27 12 : guesser 123, 111, ( 7, 6, 5, 4, 3, 2, 1, 0, 11, 10, 9 | 12, 8 ), 286, 2m5s old, 8 lemmas
% 136.94/137.27 13 : guesser 134, 121, ( 2, 12, 9, 6, 3, 0, 10, 7, 4, 1, 11, 8 | 13, 5 ), 293, 2m5s old, 6 lemmas
% 136.94/137.27 14 : guesser 145, 131, ( 1, 12, 9, 6, 3, 0, 11, 8, 5, 2, 13, 10, 7 | 14, 4 ), 299, 2m4s old, 7 lemmas
% 136.94/137.27 15 : guesser 155, 140, ( 11, 13, 0, 2, 4, 6, 8, 10, 12, 14, 1, 3, 5, 7 | 15, 9 ), 306, 2m4s old, 8 lemmas
% 136.94/137.27 16 : guesser 170, 154, ( 4, 11, 2, 9, 0, 7, 14, 5, 12, 3, 10, 1, 8, 15, 6 | 16, 13 ), 443, 1m52s old, 9 lemmas
% 136.94/137.27 17 : guesser 184, 167, ( 5, 16, 10, 4, 15, 9, 3, 14, 8, 2, 13, 7, 1, 12, 6, 0 | 17, 11 ), 716, 1m24s old, 9 lemmas
% 136.94/137.27 18 : guesser 198, 180, ( 16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0 | 18, 17 ), 724, 1m23s old, 7 lemmas
% 136.94/137.27 19 : guesser 211, 192, ( 7, 1, 14, 8, 2, 15, 9, 3, 16, 10, 4, 17, 11, 5, 18, 12, 6, 0 | 19, 13 ), 731, 1m23s old, 7 lemmas
% 136.94/137.27 20 : guesser 225, 205, ( 2, 9, 16, 3, 10, 17, 4, 11, 18, 5, 12, 19, 6, 13, 0, 7, 14, 1, 8 | 20, 15 ), 738, 1m22s old, 8 lemmas
% 136.94/137.27 21 : guesser 238, 217, ( 16, 6, 17, 7, 18, 8, 19, 9, 20, 10, 0, 11, 1, 12, 2, 13, 3, 14, 4, 15 | 21, 5 ), 746, 1m22s old, 8 lemmas
% 136.94/137.27 22 : guesser 251, 229, ( 17, 14, 11, 8, 5, 2, 21, 18, 15, 12, 9, 6, 3, 0, 19, 16, 13, 10, 7, 4, 1 | 22, 20 ), 754, 1m21s old, 9 lemmas
% 136.94/137.27 23 : guesser 263, 240, ( 11, 13, 15, 17, 19, 21, 0, 2, 4, 6, 8, 10, 12, 14, 16, 18, 20, 22, 1, 3, 5, 7 | 23, 9 ), 763, 1m20s old, 8 lemmas
% 136.94/137.27 24 : guesser 277, 253, ( 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 ), 770, 1m20s old, 11 lemmas
% 136.94/137.27 25 : guesser 290, 265, ( 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 ), 779, 1m19s old, 12 lemmas
% 136.94/137.27 26 : guesser 303, 277, ( 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 ), 789, 1m18s old, 10 lemmas
% 136.94/137.27 27 : guesser 315, 288, ( 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 ), 798, 1m17s old, 8 lemmas
% 136.94/137.27 28 : guesser 328, 300, ( 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 ), 806, 1m16s old, 10 lemmas
% 136.94/137.27 29 : guesser 340, 311, ( 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 ), 815, 1m15s old, 8 lemmas
% 136.94/137.27 30 : guesser 352, 322, ( 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 ), 823, 1m14s old, 9 lemmas
% 136.94/137.27 31 : guesser 363, 332, ( 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 ), 832, 1m13s old, 9 lemmas
% 136.94/137.27 32 : guesser 378, 346, ( 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 ), 841, 1m12s old, 11 lemmas
% 136.94/137.27 33 : guesser 392, 359, ( 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 ), 851, 1m11s old, 11 lemmas
% 136.94/137.27 34 : guesser 406, 372, ( 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 ), 861, 1m9s old, 13 lemmas
% 136.94/137.27 35 : guesser 419, 384, ( 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 ), 872, 1m8s old, 12 lemmas
% 136.94/137.27 36 : guesser 433, 397, ( 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 ), 883, 1m6s old, 13 lemmas
% 136.94/137.27 37 : guesser 446, 409, ( 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 ), 894, 1m5s old, 13 lemmas
% 136.94/137.27 38 : guesser 459, 421, ( 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 ), 906, 1m3s old, 12 lemmas
% 136.94/137.27 39 : guesser 471, 432, ( 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 ), 918, 1m1s old, 13 lemmas
% 136.94/137.27 40 : guesser 485, 445, ( 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 ), 930, 59s old, 12 lemmas
% 136.94/137.27 41 : guesser 498, 457, ( 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 ), 940, 58s old, 13 lemmas
% 136.94/137.27 42 : guesser 511, 469, ( 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 ), 952, 56s old, 12 lemmas
% 136.94/137.27 43 : guesser 523, 480, ( 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 ), 963, 54s old, 10 lemmas
% 136.94/137.27 44 : guesser 536, 492, ( 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 ), 974, 52s old, 12 lemmas
% 136.94/137.27 45 : guesser 548, 503, ( 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 ), 985, 50s old, 12 lemmas
% 136.94/137.27 46 : guesser 560, 514, ( 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 ), 996, 48s old, 13 lemmas
% 136.94/137.27 47 : guesser 571, 524, ( 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 ), 1009, 46s old, 12 lemmas
% 136.94/137.27 48 : guesser 585, 537, ( 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 ), 1020, 43s old, 14 lemmas
% 136.94/137.27 49 : guesser 598, 549, ( 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 ), 1033, 40s old, 13 lemmas
% 136.94/137.27 50 : guesser 611, 561, ( 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 ), 1047, 37s old, 15 lemmas
% 136.94/137.27 51 : guesser 623, 572, ( 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 ), 1060, 35s old, 12 lemmas
% 136.94/137.27 52 : guesser 636, 584, ( 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 ), 1073, 32s old, 11 lemmas
% 136.94/137.27 53 : guesser 648, 595, ( 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 ), 1083, 30s old, 12 lemmas
% 136.94/137.27 54 : guesser 660, 606, ( 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 ), 1094, 27s old, 12 lemmas
% 136.94/137.27 55 : guesser 671, 616, ( 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 ), 1105, 24s old, 11 lemmas
% 136.94/137.27 56 : guesser 684, 628, ( 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 ), 1116, 22s old, 14 lemmas
% 136.94/137.27 57 : guesser 696, 639, ( 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 ), 1130, 18s old, 13 lemmas
% 136.94/137.27 58 : guesser 708, 650, ( 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 ), 1142, 15s old, 12 lemmas
% 136.94/137.27 59 : guesser 719, 660, ( 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 ), 1154, 12s old, 12 lemmas
% 136.94/137.27 60 : guesser 731, 671, ( 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 ), 1166, 9s old, 11 lemmas
% 136.94/137.27 61 : guesser 742, 681, ( 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 ), 1176, 6s old, 13 lemmas
% 136.94/137.27 62 : guesser 753, 691, ( 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 ), 1190, 3s old, 11 lemmas
% 136.94/137.27
% 136.94/137.27 Elements:
% 136.94/137.27 { 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 }
% 136.94/137.27
% 136.94/137.27 Atoms:
% 136.94/137.27 0 : #-{T} E0 { }
% 136.94/137.27 1 : #-{T} E1 { 0 }
% 136.94/137.27 2 : pppp66-{T}(E1) { 0 }
% 136.94/137.27 3 : pppp65-{T}(E1) { 0 }
% 136.94/137.27 4 : p100-{T}(E1) { 0 }
% 136.94/137.27 5 : pppp67-{T}(E1) { 0 }
% 136.94/137.27 6 : pppp68-{T}(E1) { 0 }
% 136.94/137.27 7 : pppp64-{T}(E1,E0) { 0, 1 }
% 136.94/137.27 8 : p101-{T}(E0) { 0, 1 }
% 136.94/137.27 9 : p2-{T}(E0) { 0, 1 }
% 136.94/137.27 10 : r1-{T}(E1,E0) { 0, 1 }
% 136.94/137.27 11 : pppp54-{T}(E0) { 0, 1 }
% 136.94/137.27 12 : p100-{T}(E0) { 0, 1 }
% 136.94/137.27 13 : pppp79-{T}(E0) { 0, 1 }
% 136.94/137.27 14 : pppp80-{T}(E0) { 0, 1 }
% 136.94/137.27 15 : #-{T} E2 { 0, 2 }
% 136.94/137.27 16 : pppp63-{T}(E1,E2) { 0, 2 }
% 136.94/137.27 17 : p101-{T}(E2) { 0, 2 }
% 136.94/137.27 18 : r1-{T}(E1,E2) { 0, 2 }
% 136.94/137.27 19 : pppp54-{T}(E2) { 0, 2 }
% 136.94/137.27 20 : p100-{T}(E2) { 0, 2 }
% 136.94/137.27 21 : pppp79-{T}(E2) { 0, 2 }
% 136.94/137.27 22 : pppp80-{T}(E2) { 0, 2 }
% 136.94/137.27 23 : #-{T} E3 { 0, 1, 3 }
% 136.94/137.27 24 : pppp51-{T}(E3,E0) { 0, 1, 3 }
% 136.94/137.27 25 : p102-{T}(E3) { 0, 1, 3 }
% 136.94/137.27 26 : p3-{T}(E3) { 0, 1, 3 }
% 136.94/137.27 27 : r1-{T}(E0,E3) { 0, 1, 3 }
% 136.94/137.27 28 : pppp43-{T}(E3) { 0, 1, 3 }
% 136.94/137.27 29 : p101-{T}(E3) { 0, 1, 3 }
% 136.94/137.27 30 : p100-{T}(E3) { 0, 1, 3 }
% 136.94/137.27 31 : p2-{T}(E3) { 0, 1, 3 }
% 136.94/137.27 32 : pppp91-{T}(E3) { 0, 1, 3 }
% 136.94/137.27 33 : pppp92-{T}(E3) { 0, 1, 3 }
% 136.94/137.27 34 : #-{T} E4 { 0, 1, 4 }
% 136.94/137.27 35 : pppp50-{T}(E4,E0) { 0, 1, 4 }
% 136.94/137.27 36 : p102-{T}(E4) { 0, 1, 4 }
% 136.94/137.27 37 : r1-{T}(E0,E4) { 0, 1, 4 }
% 136.94/137.27 38 : pppp43-{T}(E4) { 0, 1, 4 }
% 136.94/137.27 39 : p101-{T}(E4) { 0, 1, 4 }
% 136.94/137.27 40 : p100-{T}(E4) { 0, 1, 4 }
% 136.94/137.27 41 : p2-{T}(E4) { 0, 1, 4 }
% 136.94/137.27 42 : pppp91-{T}(E4) { 0, 1, 4 }
% 136.94/137.27 43 : pppp92-{T}(E4) { 0, 1, 4 }
% 136.94/137.27 44 : #-{T} E5 { 0, 2, 5 }
% 136.94/137.27 45 : pppp51-{T}(E5,E2) { 0, 2, 5 }
% 136.94/137.27 46 : p102-{T}(E5) { 0, 2, 5 }
% 136.94/137.27 47 : p3-{T}(E5) { 0, 2, 5 }
% 136.94/137.27 48 : r1-{T}(E2,E5) { 0, 2, 5 }
% 136.94/137.27 49 : pppp43-{T}(E5) { 0, 2, 5 }
% 136.94/137.27 50 : p101-{T}(E5) { 0, 2, 5 }
% 136.94/137.27 51 : pppp91-{T}(E5) { 0, 2, 5 }
% 136.94/137.27 52 : pppp92-{T}(E5) { 0, 2, 5 }
% 136.94/137.27 53 : p100-{T}(E5) { 0, 2, 5 }
% 136.94/137.27 54 : #-{T} E6 { 0, 2, 6 }
% 136.94/137.27 55 : pppp50-{T}(E6,E2) { 0, 2, 6 }
% 136.94/137.27 56 : p102-{T}(E6) { 0, 2, 6 }
% 136.94/137.27 57 : r1-{T}(E2,E6) { 0, 2, 6 }
% 136.94/137.27 58 : pppp43-{T}(E6) { 0, 2, 6 }
% 136.94/137.27 59 : p101-{T}(E6) { 0, 2, 6 }
% 136.94/137.27 60 : pppp91-{T}(E6) { 0, 2, 6 }
% 136.94/137.27 61 : pppp92-{T}(E6) { 0, 2, 6 }
% 136.94/137.27 62 : p100-{T}(E6) { 0, 2, 6 }
% 136.94/137.27 63 : #-{T} E7 { 0, 1, 3, 7 }
% 136.94/137.27 64 : pppp38-{T}(E3,E7) { 0, 1, 3, 7 }
% 136.94/137.27 65 : p103-{T}(E7) { 0, 1, 3, 7 }
% 136.94/137.27 66 : p4-{T}(E7) { 0, 1, 3, 7 }
% 136.94/137.27 67 : r1-{T}(E3,E7) { 0, 1, 3, 7 }
% 136.94/137.27 68 : pppp32-{T}(E7) { 0, 1, 3, 7 }
% 136.94/137.27 69 : p102-{T}(E7) { 0, 1, 3, 7 }
% 136.94/137.27 70 : p101-{T}(E7) { 0, 1, 3, 7 }
% 136.94/137.27 71 : p3-{T}(E7) { 0, 1, 3, 7 }
% 136.94/137.27 72 : p100-{T}(E7) { 0, 1, 3, 7 }
% 136.94/137.27 73 : p2-{T}(E7) { 0, 1, 3, 7 }
% 136.94/137.27 74 : pppp103-{T}(E7) { 0, 1, 3, 7 }
% 136.94/137.27 75 : pppp104-{T}(E7) { 0, 1, 3, 7 }
% 136.94/137.27 76 : #-{T} E8 { 0, 1, 3, 8 }
% 136.94/137.27 77 : pppp37-{T}(E3,E8) { 0, 1, 3, 8 }
% 136.94/137.27 78 : p103-{T}(E8) { 0, 1, 3, 8 }
% 136.94/137.27 79 : r1-{T}(E3,E8) { 0, 1, 3, 8 }
% 136.94/137.27 80 : pppp32-{T}(E8) { 0, 1, 3, 8 }
% 136.94/137.27 81 : p102-{T}(E8) { 0, 1, 3, 8 }
% 136.94/137.27 82 : pppp103-{T}(E8) { 0, 1, 3, 8 }
% 136.94/137.27 83 : p101-{T}(E8) { 0, 1, 3, 8 }
% 136.94/137.27 84 : p3-{T}(E8) { 0, 1, 3, 8 }
% 136.94/137.27 85 : p100-{T}(E8) { 0, 1, 3, 8 }
% 136.94/137.27 86 : p2-{T}(E8) { 0, 1, 3, 8 }
% 136.94/137.27 87 : pppp104-{T}(E8) { 0, 1, 3, 8 }
% 136.94/137.27 88 : #-{T} E9 { 0, 1, 4, 9 }
% 136.94/137.27 89 : pppp38-{T}(E4,E9) { 0, 1, 4, 9 }
% 136.94/137.27 90 : p103-{T}(E9) { 0, 1, 4, 9 }
% 136.94/137.27 91 : p4-{T}(E9) { 0, 1, 4, 9 }
% 136.94/137.27 92 : r1-{T}(E4,E9) { 0, 1, 4, 9 }
% 136.94/137.27 93 : pppp32-{T}(E9) { 0, 1, 4, 9 }
% 136.94/137.27 94 : p102-{T}(E9) { 0, 1, 4, 9 }
% 136.94/137.27 95 : pppp103-{T}(E9) { 0, 1, 4, 9 }
% 136.94/137.27 96 : pppp104-{T}(E9) { 0, 1, 4, 9 }
% 136.94/137.27 97 : p101-{T}(E9) { 0, 1, 4, 9 }
% 136.94/137.27 98 : p100-{T}(E9) { 0, 1, 4, 9 }
% 136.94/137.27 99 : p2-{T}(E9) { 0, 1, 4, 9 }
% 136.94/137.27 100 : #-{T} E10 { 0, 1, 4, 10 }
% 136.94/137.27 101 : pppp37-{T}(E4,E10) { 0, 1, 4, 10 }
% 136.94/137.27 102 : p103-{T}(E10) { 0, 1, 4, 10 }
% 136.94/137.27 103 : r1-{T}(E4,E10) { 0, 1, 4, 10 }
% 136.94/137.27 104 : pppp32-{T}(E10) { 0, 1, 4, 10 }
% 136.94/137.27 105 : p102-{T}(E10) { 0, 1, 4, 10 }
% 136.94/137.27 106 : pppp103-{T}(E10) { 0, 1, 4, 10 }
% 136.94/137.27 107 : pppp104-{T}(E10) { 0, 1, 4, 10 }
% 136.94/137.27 108 : p101-{T}(E10) { 0, 1, 4, 10 }
% 136.94/137.27 109 : p100-{T}(E10) { 0, 1, 4, 10 }
% 136.94/137.27 110 : p2-{T}(E10) { 0, 1, 4, 10 }
% 136.94/137.27 111 : #-{T} E11 { 0, 2, 5, 11 }
% 136.94/137.27 112 : pppp38-{T}(E5,E11) { 0, 2, 5, 11 }
% 136.94/137.27 113 : p103-{T}(E11) { 0, 2, 5, 11 }
% 136.94/137.27 114 : p4-{T}(E11) { 0, 2, 5, 11 }
% 136.94/137.27 115 : r1-{T}(E5,E11) { 0, 2, 5, 11 }
% 136.94/137.27 116 : pppp32-{T}(E11) { 0, 2, 5, 11 }
% 136.94/137.27 117 : p102-{T}(E11) { 0, 2, 5, 11 }
% 136.94/137.27 118 : pppp103-{T}(E11) { 0, 2, 5, 11 }
% 136.94/137.27 119 : pppp104-{T}(E11) { 0, 2, 5, 11 }
% 136.94/137.27 120 : p101-{T}(E11) { 0, 2, 5, 11 }
% 136.94/137.27 121 : p3-{T}(E11) { 0, 2, 5, 11 }
% 136.94/137.27 122 : p100-{T}(E11) { 0, 2, 5, 11 }
% 136.94/137.27 123 : #-{T} E12 { 0, 2, 5, 12 }
% 136.94/137.27 124 : pppp37-{T}(E5,E12) { 0, 2, 5, 12 }
% 136.94/137.27 125 : p103-{T}(E12) { 0, 2, 5, 12 }
% 136.94/137.27 126 : r1-{T}(E5,E12) { 0, 2, 5, 12 }
% 136.94/137.27 127 : pppp32-{T}(E12) { 0, 2, 5, 12 }
% 136.94/137.27 128 : p102-{T}(E12) { 0, 2, 5, 12 }
% 136.94/137.27 129 : pppp103-{T}(E12) { 0, 2, 5, 12 }
% 136.94/137.27 130 : pppp104-{T}(E12) { 0, 2, 5, 12 }
% 136.94/137.27 131 : p101-{T}(E12) { 0, 2, 5, 12 }
% 136.94/137.27 132 : p3-{T}(E12) { 0, 2, 5, 12 }
% 136.94/137.27 133 : p100-{T}(E12) { 0, 2, 5, 12 }
% 136.94/137.27 134 : #-{T} E13 { 0, 2, 6, 13 }
% 136.94/137.27 135 : pppp38-{T}(E6,E13) { 0, 2, 6, 13 }
% 136.94/137.27 136 : p103-{T}(E13) { 0, 2, 6, 13 }
% 136.94/137.27 137 : p4-{T}(E13) { 0, 2, 6, 13 }
% 136.94/137.27 138 : r1-{T}(E6,E13) { 0, 2, 6, 13 }
% 136.94/137.27 139 : pppp32-{T}(E13) { 0, 2, 6, 13 }
% 136.94/137.27 140 : p102-{T}(E13) { 0, 2, 6, 13 }
% 136.94/137.27 141 : pppp103-{T}(E13) { 0, 2, 6, 13 }
% 136.94/137.27 142 : pppp104-{T}(E13) { 0, 2, 6, 13 }
% 136.94/137.27 143 : p101-{T}(E13) { 0, 2, 6, 13 }
% 136.94/137.27 144 : p100-{T}(E13) { 0, 2, 6, 13 }
% 136.94/137.27 145 : #-{T} E14 { 0, 2, 6, 14 }
% 136.94/137.27 146 : pppp37-{T}(E6,E14) { 0, 2, 6, 14 }
% 136.94/137.27 147 : p103-{T}(E14) { 0, 2, 6, 14 }
% 136.94/137.27 148 : r1-{T}(E6,E14) { 0, 2, 6, 14 }
% 136.94/137.27 149 : pppp32-{T}(E14) { 0, 2, 6, 14 }
% 136.94/137.27 150 : p102-{T}(E14) { 0, 2, 6, 14 }
% 136.94/137.27 151 : pppp103-{T}(E14) { 0, 2, 6, 14 }
% 136.94/137.27 152 : pppp104-{T}(E14) { 0, 2, 6, 14 }
% 136.94/137.27 153 : p101-{T}(E14) { 0, 2, 6, 14 }
% 136.94/137.27 154 : p100-{T}(E14) { 0, 2, 6, 14 }
% 136.94/137.27 155 : #-{T} E15 { 0, 1, 3, 7, 15 }
% 136.94/137.27 156 : pppp25-{T}(E15,E7) { 0, 1, 3, 7, 15 }
% 136.94/137.27 157 : p104-{T}(E15) { 0, 1, 3, 7, 15 }
% 136.94/137.27 158 : p5-{T}(E15) { 0, 1, 3, 7, 15 }
% 136.94/137.27 159 : r1-{T}(E7,E15) { 0, 1, 3, 7, 15 }
% 136.94/137.27 160 : pppp21-{T}(E15) { 0, 1, 3, 7, 15 }
% 136.94/137.27 161 : p103-{T}(E15) { 0, 1, 3, 7, 15 }
% 136.94/137.27 162 : p102-{T}(E15) { 0, 1, 3, 7, 15 }
% 136.94/137.27 163 : p4-{T}(E15) { 0, 1, 3, 7, 15 }
% 136.94/137.27 164 : p101-{T}(E15) { 0, 1, 3, 7, 15 }
% 136.94/137.27 165 : p3-{T}(E15) { 0, 1, 3, 7, 15 }
% 136.94/137.27 166 : p100-{T}(E15) { 0, 1, 3, 7, 15 }
% 136.94/137.27 167 : p2-{T}(E15) { 0, 1, 3, 7, 15 }
% 136.94/137.27 168 : pppp115-{T}(E15) { 0, 1, 3, 7, 15 }
% 136.94/137.27 169 : pppp116-{T}(E15) { 0, 1, 3, 7, 15 }
% 136.94/137.27 170 : #-{T} E16 { 0, 1, 3, 7, 16 }
% 136.94/137.27 171 : pppp24-{T}(E16,E7) { 0, 1, 3, 7, 16 }
% 136.94/137.27 172 : p104-{T}(E16) { 0, 1, 3, 7, 16 }
% 136.94/137.27 173 : r1-{T}(E7,E16) { 0, 1, 3, 7, 16 }
% 136.94/137.27 174 : pppp21-{T}(E16) { 0, 1, 3, 7, 16 }
% 136.94/137.27 175 : p103-{T}(E16) { 0, 1, 3, 7, 16 }
% 136.94/137.27 176 : p102-{T}(E16) { 0, 1, 3, 7, 16 }
% 136.94/137.27 177 : p4-{T}(E16) { 0, 1, 3, 7, 16 }
% 136.94/137.27 178 : p101-{T}(E16) { 0, 1, 3, 7, 16 }
% 136.94/137.27 179 : p3-{T}(E16) { 0, 1, 3, 7, 16 }
% 136.94/137.27 180 : p100-{T}(E16) { 0, 1, 3, 7, 16 }
% 136.94/137.27 181 : p2-{T}(E16) { 0, 1, 3, 7, 16 }
% 136.94/137.27 182 : pppp116-{T}(E16) { 0, 1, 3, 7, 16 }
% 136.94/137.27 183 : pppp115-{T}(E16) { 0, 1, 3, 7, 16 }
% 136.94/137.27 184 : #-{T} E17 { 0, 1, 3, 8, 17 }
% 136.94/137.27 185 : pppp25-{T}(E17,E8) { 0, 1, 3, 8, 17 }
% 136.94/137.27 186 : p104-{T}(E17) { 0, 1, 3, 8, 17 }
% 136.94/137.27 187 : p5-{T}(E17) { 0, 1, 3, 8, 17 }
% 136.94/137.27 188 : r1-{T}(E8,E17) { 0, 1, 3, 8, 17 }
% 136.94/137.27 189 : pppp21-{T}(E17) { 0, 1, 3, 8, 17 }
% 136.94/137.27 190 : p103-{T}(E17) { 0, 1, 3, 8, 17 }
% 136.94/137.27 191 : pppp115-{T}(E17) { 0, 1, 3, 8, 17 }
% 136.94/137.27 192 : pppp116-{T}(E17) { 0, 1, 3, 8, 17 }
% 136.94/137.27 193 : p102-{T}(E17) { 0, 1, 3, 8, 17 }
% 136.94/137.27 194 : p101-{T}(E17) { 0, 1, 3, 8, 17 }
% 136.94/137.27 195 : p3-{T}(E17) { 0, 1, 3, 8, 17 }
% 136.94/137.27 196 : p100-{T}(E17) { 0, 1, 3, 8, 17 }
% 136.94/137.27 197 : p2-{T}(E17) { 0, 1, 3, 8, 17 }
% 136.94/137.27 198 : #-{T} E18 { 0, 1, 3, 8, 18 }
% 136.94/137.27 199 : pppp24-{T}(E18,E8) { 0, 1, 3, 8, 18 }
% 136.94/137.27 200 : p104-{T}(E18) { 0, 1, 3, 8, 18 }
% 136.94/137.27 201 : r1-{T}(E8,E18) { 0, 1, 3, 8, 18 }
% 136.94/137.27 202 : pppp21-{T}(E18) { 0, 1, 3, 8, 18 }
% 136.94/137.27 203 : p103-{T}(E18) { 0, 1, 3, 8, 18 }
% 136.94/137.27 204 : pppp116-{T}(E18) { 0, 1, 3, 8, 18 }
% 136.94/137.27 205 : pppp115-{T}(E18) { 0, 1, 3, 8, 18 }
% 136.94/137.27 206 : p102-{T}(E18) { 0, 1, 3, 8, 18 }
% 136.94/137.27 207 : p101-{T}(E18) { 0, 1, 3, 8, 18 }
% 136.94/137.27 208 : p3-{T}(E18) { 0, 1, 3, 8, 18 }
% 136.94/137.27 209 : p100-{T}(E18) { 0, 1, 3, 8, 18 }
% 136.94/137.27 210 : p2-{T}(E18) { 0, 1, 3, 8, 18 }
% 136.94/137.27 211 : #-{T} E19 { 0, 1, 4, 9, 19 }
% 136.94/137.27 212 : pppp25-{T}(E19,E9) { 0, 1, 4, 9, 19 }
% 136.94/137.27 213 : p104-{T}(E19) { 0, 1, 4, 9, 19 }
% 136.94/137.27 214 : p5-{T}(E19) { 0, 1, 4, 9, 19 }
% 136.94/137.27 215 : r1-{T}(E9,E19) { 0, 1, 4, 9, 19 }
% 136.94/137.27 216 : pppp21-{T}(E19) { 0, 1, 4, 9, 19 }
% 136.94/137.27 217 : p103-{T}(E19) { 0, 1, 4, 9, 19 }
% 136.94/137.27 218 : pppp115-{T}(E19) { 0, 1, 4, 9, 19 }
% 136.94/137.27 219 : pppp116-{T}(E19) { 0, 1, 4, 9, 19 }
% 136.94/137.27 220 : p102-{T}(E19) { 0, 1, 4, 9, 19 }
% 136.94/137.27 221 : p4-{T}(E19) { 0, 1, 4, 9, 19 }
% 136.94/137.27 222 : p101-{T}(E19) { 0, 1, 4, 9, 19 }
% 136.94/137.27 223 : p100-{T}(E19) { 0, 1, 4, 9, 19 }
% 136.94/137.27 224 : p2-{T}(E19) { 0, 1, 4, 9, 19 }
% 136.94/137.27 225 : #-{T} E20 { 0, 1, 4, 9, 20 }
% 136.94/137.27 226 : pppp24-{T}(E20,E9) { 0, 1, 4, 9, 20 }
% 136.94/137.27 227 : p104-{T}(E20) { 0, 1, 4, 9, 20 }
% 136.94/137.27 228 : r1-{T}(E9,E20) { 0, 1, 4, 9, 20 }
% 136.94/137.27 229 : pppp21-{T}(E20) { 0, 1, 4, 9, 20 }
% 136.94/137.27 230 : p103-{T}(E20) { 0, 1, 4, 9, 20 }
% 136.94/137.27 231 : pppp116-{T}(E20) { 0, 1, 4, 9, 20 }
% 136.94/137.27 232 : pppp115-{T}(E20) { 0, 1, 4, 9, 20 }
% 136.94/137.27 233 : p102-{T}(E20) { 0, 1, 4, 9, 20 }
% 136.94/137.27 234 : p4-{T}(E20) { 0, 1, 4, 9, 20 }
% 136.94/137.27 235 : p101-{T}(E20) { 0, 1, 4, 9, 20 }
% 136.94/137.27 236 : p100-{T}(E20) { 0, 1, 4, 9, 20 }
% 136.94/137.27 237 : p2-{T}(E20) { 0, 1, 4, 9, 20 }
% 136.94/137.27 238 : #-{T} E21 { 0, 1, 4, 10, 21 }
% 136.94/137.27 239 : pppp25-{T}(E21,E10) { 0, 1, 4, 10, 21 }
% 136.94/137.27 240 : p104-{T}(E21) { 0, 1, 4, 10, 21 }
% 136.94/137.27 241 : p5-{T}(E21) { 0, 1, 4, 10, 21 }
% 136.94/137.27 242 : r1-{T}(E10,E21) { 0, 1, 4, 10, 21 }
% 136.94/137.27 243 : pppp21-{T}(E21) { 0, 1, 4, 10, 21 }
% 136.94/137.27 244 : p103-{T}(E21) { 0, 1, 4, 10, 21 }
% 136.94/137.27 245 : pppp115-{T}(E21) { 0, 1, 4, 10, 21 }
% 136.94/137.27 246 : pppp116-{T}(E21) { 0, 1, 4, 10, 21 }
% 136.94/137.27 247 : p102-{T}(E21) { 0, 1, 4, 10, 21 }
% 136.94/137.27 248 : p101-{T}(E21) { 0, 1, 4, 10, 21 }
% 136.94/137.27 249 : p100-{T}(E21) { 0, 1, 4, 10, 21 }
% 136.94/137.27 250 : p2-{T}(E21) { 0, 1, 4, 10, 21 }
% 136.94/137.27 251 : #-{T} E22 { 0, 1, 4, 10, 22 }
% 136.94/137.27 252 : pppp24-{T}(E22,E10) { 0, 1, 4, 10, 22 }
% 136.94/137.27 253 : p104-{T}(E22) { 0, 1, 4, 10, 22 }
% 136.94/137.27 254 : r1-{T}(E10,E22) { 0, 1, 4, 10, 22 }
% 136.94/137.27 255 : pppp21-{T}(E22) { 0, 1, 4, 10, 22 }
% 136.94/137.27 256 : p103-{T}(E22) { 0, 1, 4, 10, 22 }
% 136.94/137.27 257 : pppp116-{T}(E22) { 0, 1, 4, 10, 22 }
% 136.94/137.27 258 : pppp115-{T}(E22) { 0, 1, 4, 10, 22 }
% 136.94/137.27 259 : p102-{T}(E22) { 0, 1, 4, 10, 22 }
% 136.94/137.27 260 : p101-{T}(E22) { 0, 1, 4, 10, 22 }
% 136.94/137.27 261 : p100-{T}(E22) { 0, 1, 4, 10, 22 }
% 136.94/137.27 262 : p2-{T}(E22) { 0, 1, 4, 10, 22 }
% 136.94/137.27 263 : #-{T} E23 { 0, 2, 5, 11, 23 }
% 136.94/137.27 264 : pppp25-{T}(E23,E11) { 0, 2, 5, 11, 23 }
% 136.94/137.27 265 : p104-{T}(E23) { 0, 2, 5, 11, 23 }
% 136.94/137.27 266 : p5-{T}(E23) { 0, 2, 5, 11, 23 }
% 136.94/137.27 267 : r1-{T}(E11,E23) { 0, 2, 5, 11, 23 }
% 136.94/137.27 268 : pppp21-{T}(E23) { 0, 2, 5, 11, 23 }
% 136.94/137.27 269 : p103-{T}(E23) { 0, 2, 5, 11, 23 }
% 136.94/137.27 270 : pppp115-{T}(E23) { 0, 2, 5, 11, 23 }
% 136.94/137.27 271 : pppp116-{T}(E23) { 0, 2, 5, 11, 23 }
% 136.94/137.27 272 : p102-{T}(E23) { 0, 2, 5, 11, 23 }
% 136.94/137.27 273 : p4-{T}(E23) { 0, 2, 5, 11, 23 }
% 136.94/137.27 274 : p101-{T}(E23) { 0, 2, 5, 11, 23 }
% 136.94/137.27 275 : p3-{T}(E23) { 0, 2, 5, 11, 23 }
% 136.94/137.27 276 : p100-{T}(E23) { 0, 2, 5, 11, 23 }
% 136.94/137.27 277 : #-{T} E24 { 0, 2, 5, 11, 24 }
% 136.94/137.27 278 : pppp24-{T}(E24,E11) { 0, 2, 5, 11, 24 }
% 136.94/137.27 279 : p104-{T}(E24) { 0, 2, 5, 11, 24 }
% 136.94/137.27 280 : r1-{T}(E11,E24) { 0, 2, 5, 11, 24 }
% 136.94/137.27 281 : pppp21-{T}(E24) { 0, 2, 5, 11, 24 }
% 136.94/137.27 282 : p103-{T}(E24) { 0, 2, 5, 11, 24 }
% 136.94/137.27 283 : pppp116-{T}(E24) { 0, 2, 5, 11, 24 }
% 136.94/137.27 284 : pppp115-{T}(E24) { 0, 2, 5, 11, 24 }
% 136.94/137.27 285 : p102-{T}(E24) { 0, 2, 5, 11, 24 }
% 136.94/137.27 286 : p4-{T}(E24) { 0, 2, 5, 11, 24 }
% 136.94/137.27 287 : p101-{T}(E24) { 0, 2, 5, 11, 24 }
% 136.94/137.27 288 : p3-{T}(E24) { 0, 2, 5, 11, 24 }
% 136.94/137.27 289 : p100-{T}(E24) { 0, 2, 5, 11, 24 }
% 136.94/137.27 290 : #-{T} E25 { 0, 2, 5, 12, 25 }
% 136.94/137.27 291 : pppp25-{T}(E25,E12) { 0, 2, 5, 12, 25 }
% 136.94/137.27 292 : p104-{T}(E25) { 0, 2, 5, 12, 25 }
% 136.94/137.27 293 : p5-{T}(E25) { 0, 2, 5, 12, 25 }
% 136.94/137.27 294 : r1-{T}(E12,E25) { 0, 2, 5, 12, 25 }
% 136.94/137.27 295 : pppp21-{T}(E25) { 0, 2, 5, 12, 25 }
% 136.94/137.27 296 : p103-{T}(E25) { 0, 2, 5, 12, 25 }
% 136.94/137.27 297 : pppp115-{T}(E25) { 0, 2, 5, 12, 25 }
% 136.94/137.27 298 : pppp116-{T}(E25) { 0, 2, 5, 12, 25 }
% 136.94/137.27 299 : p102-{T}(E25) { 0, 2, 5, 12, 25 }
% 136.94/137.27 300 : p101-{T}(E25) { 0, 2, 5, 12, 25 }
% 136.94/137.27 301 : p3-{T}(E25) { 0, 2, 5, 12, 25 }
% 136.94/137.27 302 : p100-{T}(E25) { 0, 2, 5, 12, 25 }
% 136.94/137.27 303 : #-{T} E26 { 0, 2, 5, 12, 26 }
% 136.94/137.27 304 : pppp24-{T}(E26,E12) { 0, 2, 5, 12, 26 }
% 136.94/137.27 305 : p104-{T}(E26) { 0, 2, 5, 12, 26 }
% 136.94/137.27 306 : r1-{T}(E12,E26) { 0, 2, 5, 12, 26 }
% 136.94/137.27 307 : pppp21-{T}(E26) { 0, 2, 5, 12, 26 }
% 136.94/137.27 308 : p103-{T}(E26) { 0, 2, 5, 12, 26 }
% 136.94/137.27 309 : pppp116-{T}(E26) { 0, 2, 5, 12, 26 }
% 136.94/137.27 310 : pppp115-{T}(E26) { 0, 2, 5, 12, 26 }
% 136.94/137.27 311 : p102-{T}(E26) { 0, 2, 5, 12, 26 }
% 136.94/137.27 312 : p101-{T}(E26) { 0, 2, 5, 12, 26 }
% 136.94/137.27 313 : p3-{T}(E26) { 0, 2, 5, 12, 26 }
% 136.94/137.27 314 : p100-{T}(E26) { 0, 2, 5, 12, 26 }
% 136.94/137.27 315 : #-{T} E27 { 0, 2, 6, 13, 27 }
% 136.94/137.27 316 : pppp25-{T}(E27,E13) { 0, 2, 6, 13, 27 }
% 136.94/137.27 317 : p104-{T}(E27) { 0, 2, 6, 13, 27 }
% 136.94/137.27 318 : p5-{T}(E27) { 0, 2, 6, 13, 27 }
% 136.94/137.27 319 : r1-{T}(E13,E27) { 0, 2, 6, 13, 27 }
% 136.94/137.27 320 : pppp21-{T}(E27) { 0, 2, 6, 13, 27 }
% 136.94/137.27 321 : p103-{T}(E27) { 0, 2, 6, 13, 27 }
% 136.94/137.27 322 : pppp115-{T}(E27) { 0, 2, 6, 13, 27 }
% 136.94/137.27 323 : pppp116-{T}(E27) { 0, 2, 6, 13, 27 }
% 136.94/137.27 324 : p102-{T}(E27) { 0, 2, 6, 13, 27 }
% 136.94/137.27 325 : p4-{T}(E27) { 0, 2, 6, 13, 27 }
% 136.94/137.27 326 : p101-{T}(E27) { 0, 2, 6, 13, 27 }
% 136.94/137.27 327 : p100-{T}(E27) { 0, 2, 6, 13, 27 }
% 136.94/137.27 328 : #-{T} E28 { 0, 2, 6, 13, 28 }
% 136.94/137.27 329 : pppp24-{T}(E28,E13) { 0, 2, 6, 13, 28 }
% 136.94/137.27 330 : p104-{T}(E28) { 0, 2, 6, 13, 28 }
% 136.94/137.27 331 : r1-{T}(E13,E28) { 0, 2, 6, 13, 28 }
% 136.94/137.27 332 : pppp21-{T}(E28) { 0, 2, 6, 13, 28 }
% 136.94/137.27 333 : p103-{T}(E28) { 0, 2, 6, 13, 28 }
% 136.94/137.27 334 : pppp116-{T}(E28) { 0, 2, 6, 13, 28 }
% 136.94/137.27 335 : pppp115-{T}(E28) { 0, 2, 6, 13, 28 }
% 136.94/137.27 336 : p102-{T}(E28) { 0, 2, 6, 13, 28 }
% 136.94/137.27 337 : p4-{T}(E28) { 0, 2, 6, 13, 28 }
% 136.94/137.27 338 : p101-{T}(E28) { 0, 2, 6, 13, 28 }
% 136.94/137.27 339 : p100-{T}(E28) { 0, 2, 6, 13, 28 }
% 136.94/137.27 340 : #-{T} E29 { 0, 2, 6, 14, 29 }
% 136.94/137.27 341 : pppp25-{T}(E29,E14) { 0, 2, 6, 14, 29 }
% 136.94/137.27 342 : p104-{T}(E29) { 0, 2, 6, 14, 29 }
% 136.94/137.27 343 : p5-{T}(E29) { 0, 2, 6, 14, 29 }
% 136.94/137.27 344 : r1-{T}(E14,E29) { 0, 2, 6, 14, 29 }
% 136.94/137.27 345 : pppp21-{T}(E29) { 0, 2, 6, 14, 29 }
% 136.94/137.27 346 : p103-{T}(E29) { 0, 2, 6, 14, 29 }
% 136.94/137.27 347 : pppp115-{T}(E29) { 0, 2, 6, 14, 29 }
% 136.94/137.27 348 : pppp116-{T}(E29) { 0, 2, 6, 14, 29 }
% 136.94/137.27 349 : p102-{T}(E29) { 0, 2, 6, 14, 29 }
% 136.94/137.27 350 : p101-{T}(E29) { 0, 2, 6, 14, 29 }
% 136.94/137.27 351 : p100-{T}(E29) { 0, 2, 6, 14, 29 }
% 136.94/137.27 352 : #-{T} E30 { 0, 2, 6, 14, 30 }
% 136.94/137.27 353 : pppp24-{T}(E30,E14) { 0, 2, 6, 14, 30 }
% 136.94/137.27 354 : p104-{T}(E30) { 0, 2, 6, 14, 30 }
% 136.94/137.27 355 : r1-{T}(E14,E30) { 0, 2, 6, 14, 30 }
% 136.94/137.27 356 : pppp21-{T}(E30) { 0, 2, 6, 14, 30 }
% 136.94/137.27 357 : p103-{T}(E30) { 0, 2, 6, 14, 30 }
% 136.94/137.27 358 : pppp116-{T}(E30) { 0, 2, 6, 14, 30 }
% 136.94/137.27 359 : pppp115-{T}(E30) { 0, 2, 6, 14, 30 }
% 136.94/137.27 360 : p102-{T}(E30) { 0, 2, 6, 14, 30 }
% 136.94/137.27 361 : p101-{T}(E30) { 0, 2, 6, 14, 30 }
% 136.94/137.27 362 : p100-{T}(E30) { 0, 2, 6, 14, 30 }
% 136.94/137.27 363 : #-{T} E31 { 0, 1, 3, 7, 15, 31 }
% 136.94/137.27 364 : pppp12-{T}(E15,E31) { 0, 1, 3, 7, 15, 31 }
% 136.94/137.27 365 : p105-{T}(E31) { 0, 1, 3, 7, 15, 31 }
% 136.94/137.27 366 : p6-{T}(E31) { 0, 1, 3, 7, 15, 31 }
% 136.94/137.27 367 : r1-{T}(E15,E31) { 0, 1, 3, 7, 15, 31 }
% 136.94/137.27 368 : pppp10-{T}(E31) { 0, 1, 3, 7, 15, 31 }
% 136.94/137.27 369 : p104-{T}(E31) { 0, 1, 3, 7, 15, 31 }
% 136.94/137.27 370 : p103-{T}(E31) { 0, 1, 3, 7, 15, 31 }
% 136.94/137.27 371 : p5-{T}(E31) { 0, 1, 3, 7, 15, 31 }
% 136.94/137.27 372 : p102-{T}(E31) { 0, 1, 3, 7, 15, 31 }
% 136.94/137.27 373 : p4-{T}(E31) { 0, 1, 3, 7, 15, 31 }
% 136.94/137.27 374 : p101-{T}(E31) { 0, 1, 3, 7, 15, 31 }
% 136.94/137.27 375 : p3-{T}(E31) { 0, 1, 3, 7, 15, 31 }
% 136.94/137.27 376 : p100-{T}(E31) { 0, 1, 3, 7, 15, 31 }
% 136.94/137.27 377 : p2-{T}(E31) { 0, 1, 3, 7, 15, 31 }
% 136.94/137.27 378 : #-{T} E32 { 0, 1, 3, 7, 15, 32 }
% 136.94/137.27 379 : pppp11-{T}(E15,E32) { 0, 1, 3, 7, 15, 32 }
% 136.94/137.27 380 : p105-{T}(E32) { 0, 1, 3, 7, 15, 32 }
% 136.94/137.27 381 : r1-{T}(E15,E32) { 0, 1, 3, 7, 15, 32 }
% 136.94/137.27 382 : pppp10-{T}(E32) { 0, 1, 3, 7, 15, 32 }
% 136.94/137.27 383 : p104-{T}(E32) { 0, 1, 3, 7, 15, 32 }
% 136.94/137.27 384 : p103-{T}(E32) { 0, 1, 3, 7, 15, 32 }
% 136.94/137.27 385 : p5-{T}(E32) { 0, 1, 3, 7, 15, 32 }
% 136.94/137.27 386 : p102-{T}(E32) { 0, 1, 3, 7, 15, 32 }
% 136.94/137.27 387 : p4-{T}(E32) { 0, 1, 3, 7, 15, 32 }
% 136.94/137.27 388 : p101-{T}(E32) { 0, 1, 3, 7, 15, 32 }
% 136.94/137.27 389 : p3-{T}(E32) { 0, 1, 3, 7, 15, 32 }
% 136.94/137.27 390 : p100-{T}(E32) { 0, 1, 3, 7, 15, 32 }
% 136.94/137.27 391 : p2-{T}(E32) { 0, 1, 3, 7, 15, 32 }
% 136.94/137.27 392 : #-{T} E33 { 0, 1, 3, 7, 16, 33 }
% 136.94/137.27 393 : pppp12-{T}(E16,E33) { 0, 1, 3, 7, 16, 33 }
% 136.94/137.27 394 : p105-{T}(E33) { 0, 1, 3, 7, 16, 33 }
% 136.94/137.27 395 : p6-{T}(E33) { 0, 1, 3, 7, 16, 33 }
% 136.94/137.27 396 : r1-{T}(E16,E33) { 0, 1, 3, 7, 16, 33 }
% 136.94/137.27 397 : pppp10-{T}(E33) { 0, 1, 3, 7, 16, 33 }
% 136.94/137.27 398 : p104-{T}(E33) { 0, 1, 3, 7, 16, 33 }
% 136.94/137.27 399 : p103-{T}(E33) { 0, 1, 3, 7, 16, 33 }
% 136.94/137.27 400 : p102-{T}(E33) { 0, 1, 3, 7, 16, 33 }
% 136.94/137.27 401 : p4-{T}(E33) { 0, 1, 3, 7, 16, 33 }
% 136.94/137.27 402 : p101-{T}(E33) { 0, 1, 3, 7, 16, 33 }
% 136.94/137.27 403 : p3-{T}(E33) { 0, 1, 3, 7, 16, 33 }
% 136.94/137.27 404 : p100-{T}(E33) { 0, 1, 3, 7, 16, 33 }
% 136.94/137.27 405 : p2-{T}(E33) { 0, 1, 3, 7, 16, 33 }
% 136.94/137.27 406 : #-{T} E34 { 0, 1, 3, 7, 16, 34 }
% 136.94/137.27 407 : pppp11-{T}(E16,E34) { 0, 1, 3, 7, 16, 34 }
% 136.94/137.27 408 : p105-{T}(E34) { 0, 1, 3, 7, 16, 34 }
% 136.94/137.27 409 : r1-{T}(E16,E34) { 0, 1, 3, 7, 16, 34 }
% 136.94/137.27 410 : pppp10-{T}(E34) { 0, 1, 3, 7, 16, 34 }
% 136.94/137.27 411 : p104-{T}(E34) { 0, 1, 3, 7, 16, 34 }
% 136.94/137.27 412 : p103-{T}(E34) { 0, 1, 3, 7, 16, 34 }
% 136.94/137.27 413 : p102-{T}(E34) { 0, 1, 3, 7, 16, 34 }
% 136.94/137.27 414 : p4-{T}(E34) { 0, 1, 3, 7, 16, 34 }
% 136.94/137.27 415 : p101-{T}(E34) { 0, 1, 3, 7, 16, 34 }
% 136.94/137.27 416 : p3-{T}(E34) { 0, 1, 3, 7, 16, 34 }
% 136.94/137.27 417 : p100-{T}(E34) { 0, 1, 3, 7, 16, 34 }
% 136.94/137.27 418 : p2-{T}(E34) { 0, 1, 3, 7, 16, 34 }
% 136.94/137.27 419 : #-{T} E35 { 0, 1, 3, 8, 17, 35 }
% 136.94/137.27 420 : pppp12-{T}(E17,E35) { 0, 1, 3, 8, 17, 35 }
% 136.94/137.27 421 : p105-{T}(E35) { 0, 1, 3, 8, 17, 35 }
% 136.94/137.27 422 : p6-{T}(E35) { 0, 1, 3, 8, 17, 35 }
% 136.94/137.27 423 : r1-{T}(E17,E35) { 0, 1, 3, 8, 17, 35 }
% 136.94/137.27 424 : pppp10-{T}(E35) { 0, 1, 3, 8, 17, 35 }
% 136.94/137.27 425 : p104-{T}(E35) { 0, 1, 3, 8, 17, 35 }
% 136.94/137.27 426 : p103-{T}(E35) { 0, 1, 3, 8, 17, 35 }
% 136.94/137.27 427 : p5-{T}(E35) { 0, 1, 3, 8, 17, 35 }
% 136.94/137.27 428 : p102-{T}(E35) { 0, 1, 3, 8, 17, 35 }
% 136.94/137.27 429 : p101-{T}(E35) { 0, 1, 3, 8, 17, 35 }
% 136.94/137.27 430 : p3-{T}(E35) { 0, 1, 3, 8, 17, 35 }
% 136.94/137.27 431 : p100-{T}(E35) { 0, 1, 3, 8, 17, 35 }
% 136.94/137.27 432 : p2-{T}(E35) { 0, 1, 3, 8, 17, 35 }
% 136.94/137.27 433 : #-{T} E36 { 0, 1, 3, 8, 17, 36 }
% 136.94/137.27 434 : pppp11-{T}(E17,E36) { 0, 1, 3, 8, 17, 36 }
% 136.94/137.27 435 : p105-{T}(E36) { 0, 1, 3, 8, 17, 36 }
% 136.94/137.27 436 : r1-{T}(E17,E36) { 0, 1, 3, 8, 17, 36 }
% 136.94/137.27 437 : pppp10-{T}(E36) { 0, 1, 3, 8, 17, 36 }
% 136.94/137.27 438 : p104-{T}(E36) { 0, 1, 3, 8, 17, 36 }
% 136.94/137.27 439 : p103-{T}(E36) { 0, 1, 3, 8, 17, 36 }
% 136.94/137.27 440 : p5-{T}(E36) { 0, 1, 3, 8, 17, 36 }
% 136.94/137.27 441 : p102-{T}(E36) { 0, 1, 3, 8, 17, 36 }
% 136.94/137.27 442 : p101-{T}(E36) { 0, 1, 3, 8, 17, 36 }
% 136.94/137.27 443 : p3-{T}(E36) { 0, 1, 3, 8, 17, 36 }
% 136.94/137.27 444 : p100-{T}(E36) { 0, 1, 3, 8, 17, 36 }
% 136.94/137.27 445 : p2-{T}(E36) { 0, 1, 3, 8, 17, 36 }
% 136.94/137.27 446 : #-{T} E37 { 0, 1, 3, 8, 18, 37 }
% 136.94/137.27 447 : pppp12-{T}(E18,E37) { 0, 1, 3, 8, 18, 37 }
% 136.94/137.27 448 : p105-{T}(E37) { 0, 1, 3, 8, 18, 37 }
% 136.94/137.27 449 : p6-{T}(E37) { 0, 1, 3, 8, 18, 37 }
% 136.94/137.27 450 : r1-{T}(E18,E37) { 0, 1, 3, 8, 18, 37 }
% 136.94/137.27 451 : pppp10-{T}(E37) { 0, 1, 3, 8, 18, 37 }
% 136.94/137.27 452 : p104-{T}(E37) { 0, 1, 3, 8, 18, 37 }
% 136.94/137.27 453 : p103-{T}(E37) { 0, 1, 3, 8, 18, 37 }
% 136.94/137.27 454 : p102-{T}(E37) { 0, 1, 3, 8, 18, 37 }
% 136.94/137.27 455 : p101-{T}(E37) { 0, 1, 3, 8, 18, 37 }
% 136.94/137.27 456 : p3-{T}(E37) { 0, 1, 3, 8, 18, 37 }
% 136.94/137.27 457 : p100-{T}(E37) { 0, 1, 3, 8, 18, 37 }
% 136.94/137.27 458 : p2-{T}(E37) { 0, 1, 3, 8, 18, 37 }
% 136.94/137.27 459 : #-{T} E38 { 0, 1, 3, 8, 18, 38 }
% 136.94/137.27 460 : pppp11-{T}(E18,E38) { 0, 1, 3, 8, 18, 38 }
% 136.94/137.27 461 : p105-{T}(E38) { 0, 1, 3, 8, 18, 38 }
% 136.94/137.27 462 : r1-{T}(E18,E38) { 0, 1, 3, 8, 18, 38 }
% 136.94/137.27 463 : pppp10-{T}(E38) { 0, 1, 3, 8, 18, 38 }
% 136.94/137.27 464 : p104-{T}(E38) { 0, 1, 3, 8, 18, 38 }
% 136.94/137.27 465 : p103-{T}(E38) { 0, 1, 3, 8, 18, 38 }
% 136.94/137.27 466 : p102-{T}(E38) { 0, 1, 3, 8, 18, 38 }
% 136.94/137.27 467 : p101-{T}(E38) { 0, 1, 3, 8, 18, 38 }
% 136.94/137.27 468 : p3-{T}(E38) { 0, 1, 3, 8, 18, 38 }
% 136.94/137.27 469 : p100-{T}(E38) { 0, 1, 3, 8, 18, 38 }
% 136.94/137.27 470 : p2-{T}(E38) { 0, 1, 3, 8, 18, 38 }
% 136.94/137.27 471 : #-{T} E39 { 0, 1, 4, 9, 19, 39 }
% 136.94/137.27 472 : pppp12-{T}(E19,E39) { 0, 1, 4, 9, 19, 39 }
% 136.94/137.27 473 : p105-{T}(E39) { 0, 1, 4, 9, 19, 39 }
% 136.94/137.27 474 : p6-{T}(E39) { 0, 1, 4, 9, 19, 39 }
% 136.94/137.27 475 : r1-{T}(E19,E39) { 0, 1, 4, 9, 19, 39 }
% 136.94/137.27 476 : pppp10-{T}(E39) { 0, 1, 4, 9, 19, 39 }
% 136.94/137.27 477 : p104-{T}(E39) { 0, 1, 4, 9, 19, 39 }
% 136.94/137.27 478 : p103-{T}(E39) { 0, 1, 4, 9, 19, 39 }
% 136.94/137.27 479 : p5-{T}(E39) { 0, 1, 4, 9, 19, 39 }
% 136.94/137.27 480 : p102-{T}(E39) { 0, 1, 4, 9, 19, 39 }
% 136.94/137.27 481 : p4-{T}(E39) { 0, 1, 4, 9, 19, 39 }
% 136.94/137.27 482 : p101-{T}(E39) { 0, 1, 4, 9, 19, 39 }
% 136.94/137.27 483 : p100-{T}(E39) { 0, 1, 4, 9, 19, 39 }
% 136.94/137.27 484 : p2-{T}(E39) { 0, 1, 4, 9, 19, 39 }
% 136.94/137.27 485 : #-{T} E40 { 0, 1, 4, 9, 19, 40 }
% 136.94/137.27 486 : pppp11-{T}(E19,E40) { 0, 1, 4, 9, 19, 40 }
% 136.94/137.27 487 : p105-{T}(E40) { 0, 1, 4, 9, 19, 40 }
% 136.94/137.27 488 : r1-{T}(E19,E40) { 0, 1, 4, 9, 19, 40 }
% 136.94/137.27 489 : pppp10-{T}(E40) { 0, 1, 4, 9, 19, 40 }
% 136.94/137.27 490 : p104-{T}(E40) { 0, 1, 4, 9, 19, 40 }
% 136.94/137.27 491 : p103-{T}(E40) { 0, 1, 4, 9, 19, 40 }
% 136.94/137.27 492 : p5-{T}(E40) { 0, 1, 4, 9, 19, 40 }
% 136.94/137.27 493 : p102-{T}(E40) { 0, 1, 4, 9, 19, 40 }
% 136.94/137.27 494 : p4-{T}(E40) { 0, 1, 4, 9, 19, 40 }
% 136.94/137.27 495 : p101-{T}(E40) { 0, 1, 4, 9, 19, 40 }
% 136.94/137.27 496 : p100-{T}(E40) { 0, 1, 4, 9, 19, 40 }
% 136.94/137.27 497 : p2-{T}(E40) { 0, 1, 4, 9, 19, 40 }
% 136.94/137.27 498 : #-{T} E41 { 0, 1, 4, 9, 20, 41 }
% 136.94/137.27 499 : pppp12-{T}(E20,E41) { 0, 1, 4, 9, 20, 41 }
% 136.94/137.27 500 : p105-{T}(E41) { 0, 1, 4, 9, 20, 41 }
% 136.94/137.27 501 : p6-{T}(E41) { 0, 1, 4, 9, 20, 41 }
% 136.94/137.27 502 : r1-{T}(E20,E41) { 0, 1, 4, 9, 20, 41 }
% 136.94/137.27 503 : pppp10-{T}(E41) { 0, 1, 4, 9, 20, 41 }
% 136.94/137.27 504 : p104-{T}(E41) { 0, 1, 4, 9, 20, 41 }
% 136.94/137.27 505 : p103-{T}(E41) { 0, 1, 4, 9, 20, 41 }
% 136.94/137.27 506 : p102-{T}(E41) { 0, 1, 4, 9, 20, 41 }
% 136.94/137.27 507 : p4-{T}(E41) { 0, 1, 4, 9, 20, 41 }
% 136.94/137.27 508 : p101-{T}(E41) { 0, 1, 4, 9, 20, 41 }
% 136.94/137.27 509 : p100-{T}(E41) { 0, 1, 4, 9, 20, 41 }
% 136.94/137.27 510 : p2-{T}(E41) { 0, 1, 4, 9, 20, 41 }
% 136.94/137.27 511 : #-{T} E42 { 0, 1, 4, 9, 20, 42 }
% 136.94/137.27 512 : pppp11-{T}(E20,E42) { 0, 1, 4, 9, 20, 42 }
% 136.94/137.27 513 : p105-{T}(E42) { 0, 1, 4, 9, 20, 42 }
% 136.94/137.27 514 : r1-{T}(E20,E42) { 0, 1, 4, 9, 20, 42 }
% 136.94/137.27 515 : pppp10-{T}(E42) { 0, 1, 4, 9, 20, 42 }
% 136.94/137.27 516 : p104-{T}(E42) { 0, 1, 4, 9, 20, 42 }
% 136.94/137.27 517 : p103-{T}(E42) { 0, 1, 4, 9, 20, 42 }
% 136.94/137.27 518 : p102-{T}(E42) { 0, 1, 4, 9, 20, 42 }
% 136.94/137.27 519 : p4-{T}(E42) { 0, 1, 4, 9, 20, 42 }
% 136.94/137.27 520 : p101-{T}(E42) { 0, 1, 4, 9, 20, 42 }
% 136.94/137.27 521 : p100-{T}(E42) { 0, 1, 4, 9, 20, 42 }
% 136.94/137.27 522 : p2-{T}(E42) { 0, 1, 4, 9, 20, 42 }
% 136.94/137.27 523 : #-{T} E43 { 0, 1, 4, 10, 21, 43 }
% 136.94/137.27 524 : pppp12-{T}(E21,E43) { 0, 1, 4, 10, 21, 43 }
% 136.94/137.27 525 : p105-{T}(E43) { 0, 1, 4, 10, 21, 43 }
% 136.94/137.27 526 : p6-{T}(E43) { 0, 1, 4, 10, 21, 43 }
% 136.94/137.27 527 : r1-{T}(E21,E43) { 0, 1, 4, 10, 21, 43 }
% 136.94/137.27 528 : pppp10-{T}(E43) { 0, 1, 4, 10, 21, 43 }
% 136.94/137.27 529 : p104-{T}(E43) { 0, 1, 4, 10, 21, 43 }
% 136.94/137.27 530 : p103-{T}(E43) { 0, 1, 4, 10, 21, 43 }
% 136.94/137.27 531 : p5-{T}(E43) { 0, 1, 4, 10, 21, 43 }
% 136.94/137.27 532 : p102-{T}(E43) { 0, 1, 4, 10, 21, 43 }
% 136.94/137.27 533 : p101-{T}(E43) { 0, 1, 4, 10, 21, 43 }
% 136.94/137.27 534 : p100-{T}(E43) { 0, 1, 4, 10, 21, 43 }
% 136.94/137.27 535 : p2-{T}(E43) { 0, 1, 4, 10, 21, 43 }
% 136.94/137.27 536 : #-{T} E44 { 0, 1, 4, 10, 21, 44 }
% 136.94/137.27 537 : pppp11-{T}(E21,E44) { 0, 1, 4, 10, 21, 44 }
% 136.94/137.27 538 : p105-{T}(E44) { 0, 1, 4, 10, 21, 44 }
% 136.94/137.27 539 : r1-{T}(E21,E44) { 0, 1, 4, 10, 21, 44 }
% 136.94/137.27 540 : pppp10-{T}(E44) { 0, 1, 4, 10, 21, 44 }
% 136.94/137.27 541 : p104-{T}(E44) { 0, 1, 4, 10, 21, 44 }
% 136.94/137.27 542 : p103-{T}(E44) { 0, 1, 4, 10, 21, 44 }
% 136.94/137.27 543 : p5-{T}(E44) { 0, 1, 4, 10, 21, 44 }
% 136.94/137.27 544 : p102-{T}(E44) { 0, 1, 4, 10, 21, 44 }
% 136.94/137.27 545 : p101-{T}(E44) { 0, 1, 4, 10, 21, 44 }
% 136.94/137.27 546 : p100-{T}(E44) { 0, 1, 4, 10, 21, 44 }
% 136.94/137.27 547 : p2-{T}(E44) { 0, 1, 4, 10, 21, 44 }
% 136.94/137.27 548 : #-{T} E45 { 0, 1, 4, 10, 22, 45 }
% 136.94/137.27 549 : pppp12-{T}(E22,E45) { 0, 1, 4, 10, 22, 45 }
% 136.94/137.27 550 : p105-{T}(E45) { 0, 1, 4, 10, 22, 45 }
% 136.94/137.27 551 : p6-{T}(E45) { 0, 1, 4, 10, 22, 45 }
% 136.94/137.27 552 : r1-{T}(E22,E45) { 0, 1, 4, 10, 22, 45 }
% 136.94/137.27 553 : pppp10-{T}(E45) { 0, 1, 4, 10, 22, 45 }
% 136.94/137.27 554 : p104-{T}(E45) { 0, 1, 4, 10, 22, 45 }
% 136.94/137.27 555 : p103-{T}(E45) { 0, 1, 4, 10, 22, 45 }
% 136.94/137.27 556 : p102-{T}(E45) { 0, 1, 4, 10, 22, 45 }
% 136.94/137.27 557 : p101-{T}(E45) { 0, 1, 4, 10, 22, 45 }
% 136.94/137.27 558 : p100-{T}(E45) { 0, 1, 4, 10, 22, 45 }
% 136.94/137.27 559 : p2-{T}(E45) { 0, 1, 4, 10, 22, 45 }
% 136.94/137.27 560 : #-{T} E46 { 0, 1, 4, 10, 22, 46 }
% 136.94/137.27 561 : pppp11-{T}(E22,E46) { 0, 1, 4, 10, 22, 46 }
% 136.94/137.27 562 : p105-{T}(E46) { 0, 1, 4, 10, 22, 46 }
% 136.94/137.27 563 : r1-{T}(E22,E46) { 0, 1, 4, 10, 22, 46 }
% 136.94/137.27 564 : pppp10-{T}(E46) { 0, 1, 4, 10, 22, 46 }
% 136.94/137.27 565 : p104-{T}(E46) { 0, 1, 4, 10, 22, 46 }
% 136.94/137.27 566 : p103-{T}(E46) { 0, 1, 4, 10, 22, 46 }
% 136.94/137.27 567 : p102-{T}(E46) { 0, 1, 4, 10, 22, 46 }
% 136.94/137.27 568 : p101-{T}(E46) { 0, 1, 4, 10, 22, 46 }
% 136.94/137.27 569 : p100-{T}(E46) { 0, 1, 4, 10, 22, 46 }
% 136.94/137.27 570 : p2-{T}(E46) { 0, 1, 4, 10, 22, 46 }
% 136.94/137.27 571 : #-{T} E47 { 0, 2, 5, 11, 23, 47 }
% 136.94/137.27 572 : pppp12-{T}(E23,E47) { 0, 2, 5, 11, 23, 47 }
% 136.94/137.27 573 : p105-{T}(E47) { 0, 2, 5, 11, 23, 47 }
% 136.94/137.27 574 : p6-{T}(E47) { 0, 2, 5, 11, 23, 47 }
% 136.94/137.27 575 : r1-{T}(E23,E47) { 0, 2, 5, 11, 23, 47 }
% 136.94/137.27 576 : pppp10-{T}(E47) { 0, 2, 5, 11, 23, 47 }
% 136.94/137.27 577 : p104-{T}(E47) { 0, 2, 5, 11, 23, 47 }
% 136.94/137.27 578 : p103-{T}(E47) { 0, 2, 5, 11, 23, 47 }
% 136.94/137.27 579 : p5-{T}(E47) { 0, 2, 5, 11, 23, 47 }
% 136.94/137.27 580 : p102-{T}(E47) { 0, 2, 5, 11, 23, 47 }
% 136.94/137.27 581 : p4-{T}(E47) { 0, 2, 5, 11, 23, 47 }
% 136.94/137.27 582 : p101-{T}(E47) { 0, 2, 5, 11, 23, 47 }
% 136.94/137.27 583 : p3-{T}(E47) { 0, 2, 5, 11, 23, 47 }
% 136.94/137.27 584 : p100-{T}(E47) { 0, 2, 5, 11, 23, 47 }
% 136.94/137.27 585 : #-{T} E48 { 0, 2, 5, 11, 23, 48 }
% 136.94/137.27 586 : pppp11-{T}(E23,E48) { 0, 2, 5, 11, 23, 48 }
% 136.94/137.27 587 : p105-{T}(E48) { 0, 2, 5, 11, 23, 48 }
% 136.94/137.27 588 : r1-{T}(E23,E48) { 0, 2, 5, 11, 23, 48 }
% 136.94/137.27 589 : pppp10-{T}(E48) { 0, 2, 5, 11, 23, 48 }
% 136.94/137.27 590 : p104-{T}(E48) { 0, 2, 5, 11, 23, 48 }
% 136.94/137.27 591 : p103-{T}(E48) { 0, 2, 5, 11, 23, 48 }
% 136.94/137.27 592 : p5-{T}(E48) { 0, 2, 5, 11, 23, 48 }
% 136.94/137.27 593 : p102-{T}(E48) { 0, 2, 5, 11, 23, 48 }
% 136.94/137.27 594 : p4-{T}(E48) { 0, 2, 5, 11, 23, 48 }
% 136.94/137.27 595 : p101-{T}(E48) { 0, 2, 5, 11, 23, 48 }
% 136.94/137.27 596 : p3-{T}(E48) { 0, 2, 5, 11, 23, 48 }
% 136.94/137.27 597 : p100-{T}(E48) { 0, 2, 5, 11, 23, 48 }
% 136.94/137.27 598 : #-{T} E49 { 0, 2, 5, 11, 24, 49 }
% 136.94/137.27 599 : pppp12-{T}(E24,E49) { 0, 2, 5, 11, 24, 49 }
% 136.94/137.27 600 : p105-{T}(E49) { 0, 2, 5, 11, 24, 49 }
% 136.94/137.27 601 : p6-{T}(E49) { 0, 2, 5, 11, 24, 49 }
% 136.94/137.27 602 : r1-{T}(E24,E49) { 0, 2, 5, 11, 24, 49 }
% 136.94/137.27 603 : pppp10-{T}(E49) { 0, 2, 5, 11, 24, 49 }
% 136.94/137.27 604 : p104-{T}(E49) { 0, 2, 5, 11, 24, 49 }
% 136.94/137.27 605 : p103-{T}(E49) { 0, 2, 5, 11, 24, 49 }
% 136.94/137.27 606 : p102-{T}(E49) { 0, 2, 5, 11, 24, 49 }
% 136.94/137.27 607 : p4-{T}(E49) { 0, 2, 5, 11, 24, 49 }
% 136.94/137.27 608 : p101-{T}(E49) { 0, 2, 5, 11, 24, 49 }
% 136.94/137.27 609 : p3-{T}(E49) { 0, 2, 5, 11, 24, 49 }
% 136.94/137.27 610 : p100-{T}(E49) { 0, 2, 5, 11, 24, 49 }
% 136.94/137.27 611 : #-{T} E50 { 0, 2, 5, 11, 24, 50 }
% 136.94/137.27 612 : pppp11-{T}(E24,E50) { 0, 2, 5, 11, 24, 50 }
% 136.94/137.27 613 : p105-{T}(E50) { 0, 2, 5, 11, 24, 50 }
% 136.94/137.27 614 : r1-{T}(E24,E50) { 0, 2, 5, 11, 24, 50 }
% 136.94/137.27 615 : pppp10-{T}(E50) { 0, 2, 5, 11, 24, 50 }
% 136.94/137.27 616 : p104-{T}(E50) { 0, 2, 5, 11, 24, 50 }
% 136.94/137.27 617 : p103-{T}(E50) { 0, 2, 5, 11, 24, 50 }
% 136.94/137.27 618 : p102-{T}(E50) { 0, 2, 5, 11, 24, 50 }
% 136.94/137.27 619 : p4-{T}(E50) { 0, 2, 5, 11, 24, 50 }
% 136.94/137.27 620 : p101-{T}(E50) { 0, 2, 5, 11, 24, 50 }
% 136.94/137.27 621 : p3-{T}(E50) { 0, 2, 5, 11, 24, 50 }
% 136.94/137.27 622 : p100-{T}(E50) { 0, 2, 5, 11, 24, 50 }
% 136.94/137.27 623 : #-{T} E51 { 0, 2, 5, 12, 25, 51 }
% 136.94/137.27 624 : pppp12-{T}(E25,E51) { 0, 2, 5, 12, 25, 51 }
% 136.94/137.27 625 : p105-{T}(E51) { 0, 2, 5, 12, 25, 51 }
% 136.94/137.27 626 : p6-{T}(E51) { 0, 2, 5, 12, 25, 51 }
% 136.94/137.27 627 : r1-{T}(E25,E51) { 0, 2, 5, 12, 25, 51 }
% 136.94/137.27 628 : pppp10-{T}(E51) { 0, 2, 5, 12, 25, 51 }
% 136.94/137.27 629 : p104-{T}(E51) { 0, 2, 5, 12, 25, 51 }
% 136.94/137.27 630 : p103-{T}(E51) { 0, 2, 5, 12, 25, 51 }
% 136.94/137.27 631 : p5-{T}(E51) { 0, 2, 5, 12, 25, 51 }
% 136.94/137.27 632 : p102-{T}(E51) { 0, 2, 5, 12, 25, 51 }
% 136.94/137.27 633 : p101-{T}(E51) { 0, 2, 5, 12, 25, 51 }
% 136.94/137.27 634 : p3-{T}(E51) { 0, 2, 5, 12, 25, 51 }
% 136.94/137.27 635 : p100-{T}(E51) { 0, 2, 5, 12, 25, 51 }
% 136.94/137.27 636 : #-{T} E52 { 0, 2, 5, 12, 25, 52 }
% 136.94/137.27 637 : pppp11-{T}(E25,E52) { 0, 2, 5, 12, 25, 52 }
% 136.94/137.27 638 : p105-{T}(E52) { 0, 2, 5, 12, 25, 52 }
% 136.94/137.27 639 : r1-{T}(E25,E52) { 0, 2, 5, 12, 25, 52 }
% 136.94/137.27 640 : pppp10-{T}(E52) { 0, 2, 5, 12, 25, 52 }
% 136.94/137.27 641 : p104-{T}(E52) { 0, 2, 5, 12, 25, 52 }
% 136.94/137.27 642 : p103-{T}(E52) { 0, 2, 5, 12, 25, 52 }
% 136.94/137.27 643 : p5-{T}(E52) { 0, 2, 5, 12, 25, 52 }
% 136.94/137.27 644 : p102-{T}(E52) { 0, 2, 5, 12, 25, 52 }
% 136.94/137.27 645 : p101-{T}(E52) { 0, 2, 5, 12, 25, 52 }
% 136.94/137.27 646 : p3-{T}(E52) { 0, 2, 5, 12, 25, 52 }
% 136.94/137.27 647 : p100-{T}(E52) { 0, 2, 5, 12, 25, 52 }
% 136.94/137.27 648 : #-{T} E53 { 0, 2, 5, 12, 26, 53 }
% 136.94/137.27 649 : pppp12-{T}(E26,E53) { 0, 2, 5, 12, 26, 53 }
% 136.94/137.27 650 : p105-{T}(E53) { 0, 2, 5, 12, 26, 53 }
% 136.94/137.27 651 : p6-{T}(E53) { 0, 2, 5, 12, 26, 53 }
% 136.94/137.27 652 : r1-{T}(E26,E53) { 0, 2, 5, 12, 26, 53 }
% 136.94/137.27 653 : pppp10-{T}(E53) { 0, 2, 5, 12, 26, 53 }
% 136.94/137.27 654 : p104-{T}(E53) { 0, 2, 5, 12, 26, 53 }
% 136.94/137.27 655 : p103-{T}(E53) { 0, 2, 5, 12, 26, 53 }
% 136.94/137.27 656 : p102-{T}(E53) { 0, 2, 5, 12, 26, 53 }
% 136.94/137.27 657 : p101-{T}(E53) { 0, 2, 5, 12, 26, 53 }
% 136.94/137.27 658 : p3-{T}(E53) { 0, 2, 5, 12, 26, 53 }
% 136.94/137.27 659 : p100-{T}(E53) { 0, 2, 5, 12, 26, 53 }
% 136.94/137.27 660 : #-{T} E54 { 0, 2, 5, 12, 26, 54 }
% 136.94/137.27 661 : pppp11-{T}(E26,E54) { 0, 2, 5, 12, 26, 54 }
% 136.94/137.27 662 : p105-{T}(E54) { 0, 2, 5, 12, 26, 54 }
% 136.94/137.27 663 : r1-{T}(E26,E54) { 0, 2, 5, 12, 26, 54 }
% 136.94/137.27 664 : pppp10-{T}(E54) { 0, 2, 5, 12, 26, 54 }
% 136.94/137.27 665 : p104-{T}(E54) { 0, 2, 5, 12, 26, 54 }
% 136.94/137.27 666 : p103-{T}(E54) { 0, 2, 5, 12, 26, 54 }
% 136.94/137.27 667 : p102-{T}(E54) { 0, 2, 5, 12, 26, 54 }
% 136.94/137.27 668 : p101-{T}(E54) { 0, 2, 5, 12, 26, 54 }
% 136.94/137.27 669 : p3-{T}(E54) { 0, 2, 5, 12, 26, 54 }
% 136.94/137.27 670 : p100-{T}(E54) { 0, 2, 5, 12, 26, 54 }
% 136.94/137.27 671 : #-{T} E55 { 0, 2, 6, 13, 27, 55 }
% 136.94/137.27 672 : pppp12-{T}(E27,E55) { 0, 2, 6, 13, 27, 55 }
% 136.94/137.27 673 : p105-{T}(E55) { 0, 2, 6, 13, 27, 55 }
% 136.94/137.27 674 : p6-{T}(E55) { 0, 2, 6, 13, 27, 55 }
% 136.94/137.27 675 : r1-{T}(E27,E55) { 0, 2, 6, 13, 27, 55 }
% 136.94/137.27 676 : pppp10-{T}(E55) { 0, 2, 6, 13, 27, 55 }
% 136.94/137.27 677 : p104-{T}(E55) { 0, 2, 6, 13, 27, 55 }
% 136.94/137.27 678 : p103-{T}(E55) { 0, 2, 6, 13, 27, 55 }
% 136.94/137.27 679 : p5-{T}(E55) { 0, 2, 6, 13, 27, 55 }
% 136.94/137.27 680 : p102-{T}(E55) { 0, 2, 6, 13, 27, 55 }
% 136.94/137.27 681 : p4-{T}(E55) { 0, 2, 6, 13, 27, 55 }
% 136.94/137.27 682 : p101-{T}(E55) { 0, 2, 6, 13, 27, 55 }
% 136.94/137.27 683 : p100-{T}(E55) { 0, 2, 6, 13, 27, 55 }
% 136.94/137.27 684 : #-{T} E56 { 0, 2, 6, 13, 27, 56 }
% 136.94/137.27 685 : pppp11-{T}(E27,E56) { 0, 2, 6, 13, 27, 56 }
% 136.94/137.27 686 : p105-{T}(E56) { 0, 2, 6, 13, 27, 56 }
% 136.94/137.27 687 : r1-{T}(E27,E56) { 0, 2, 6, 13, 27, 56 }
% 136.94/137.27 688 : pppp10-{T}(E56) { 0, 2, 6, 13, 27, 56 }
% 136.94/137.27 689 : p104-{T}(E56) { 0, 2, 6, 13, 27, 56 }
% 136.94/137.27 690 : p103-{T}(E56) { 0, 2, 6, 13, 27, 56 }
% 136.94/137.27 691 : p5-{T}(E56) { 0, 2, 6, 13, 27, 56 }
% 136.94/137.27 692 : p102-{T}(E56) { 0, 2, 6, 13, 27, 56 }
% 136.94/137.27 693 : p4-{T}(E56) { 0, 2, 6, 13, 27, 56 }
% 136.94/137.27 694 : p101-{T}(E56) { 0, 2, 6, 13, 27, 56 }
% 136.94/137.27 695 : p100-{T}(E56) { 0, 2, 6, 13, 27, 56 }
% 136.94/137.27 696 : #-{T} E57 { 0, 2, 6, 13, 28, 57 }
% 136.94/137.27 697 : pppp12-{T}(E28,E57) { 0, 2, 6, 13, 28, 57 }
% 136.94/137.27 698 : p105-{T}(E57) { 0, 2, 6, 13, 28, 57 }
% 136.94/137.27 699 : p6-{T}(E57) { 0, 2, 6, 13, 28, 57 }
% 136.94/137.27 700 : r1-{T}(E28,E57) { 0, 2, 6, 13, 28, 57 }
% 136.94/137.27 701 : pppp10-{T}(E57) { 0, 2, 6, 13, 28, 57 }
% 136.94/137.27 702 : p104-{T}(E57) { 0, 2, 6, 13, 28, 57 }
% 136.94/137.27 703 : p103-{T}(E57) { 0, 2, 6, 13, 28, 57 }
% 136.94/137.27 704 : p102-{T}(E57) { 0, 2, 6, 13, 28, 57 }
% 136.94/137.27 705 : p4-{T}(E57) { 0, 2, 6, 13, 28, 57 }
% 136.94/137.27 706 : p101-{T}(E57) { 0, 2, 6, 13, 28, 57 }
% 136.94/137.27 707 : p100-{T}(E57) { 0, 2, 6, 13, 28, 57 }
% 136.94/137.27 708 : #-{T} E58 { 0, 2, 6, 13, 28, 58 }
% 136.94/137.27 709 : pppp11-{T}(E28,E58) { 0, 2, 6, 13, 28, 58 }
% 136.94/137.27 710 : p105-{T}(E58) { 0, 2, 6, 13, 28, 58 }
% 136.94/137.27 711 : r1-{T}(E28,E58) { 0, 2, 6, 13, 28, 58 }
% 136.94/137.27 712 : pppp10-{T}(E58) { 0, 2, 6, 13, 28, 58 }
% 136.94/137.27 713 : p104-{T}(E58) { 0, 2, 6, 13, 28, 58 }
% 136.94/137.27 714 : p103-{T}(E58) { 0, 2, 6, 13, 28, 58 }
% 136.94/137.27 715 : p102-{T}(E58) { 0, 2, 6, 13, 28, 58 }
% 136.94/137.27 716 : p4-{T}(E58) { 0, 2, 6, 13, 28, 58 }
% 136.94/137.27 717 : p101-{T}(E58) { 0, 2, 6, 13, 28, 58 }
% 136.94/137.27 718 : p100-{T}(E58) { 0, 2, 6, 13, 28, 58 }
% 136.94/137.27 719 : #-{T} E59 { 0, 2, 6, 14, 29, 59 }
% 136.94/137.27 720 : pppp12-{T}(E29,E59) { 0, 2, 6, 14, 29, 59 }
% 136.94/137.27 721 : p105-{T}(E59) { 0, 2, 6, 14, 29, 59 }
% 136.94/137.27 722 : p6-{T}(E59) { 0, 2, 6, 14, 29, 59 }
% 136.94/137.27 723 : r1-{T}(E29,E59) { 0, 2, 6, 14, 29, 59 }
% 136.94/137.27 724 : pppp10-{T}(E59) { 0, 2, 6, 14, 29, 59 }
% 136.94/137.27 725 : p104-{T}(E59) { 0, 2, 6, 14, 29, 59 }
% 136.94/137.27 726 : p103-{T}(E59) { 0, 2, 6, 14, 29, 59 }
% 136.94/137.27 727 : p5-{T}(E59) { 0, 2, 6, 14, 29, 59 }
% 136.94/137.27 728 : p102-{T}(E59) { 0, 2, 6, 14, 29, 59 }
% 136.94/137.27 729 : p101-{T}(E59) { 0, 2, 6, 14, 29, 59 }
% 136.94/137.27 730 : p100-{T}(E59) { 0, 2, 6, 14, 29, 59 }
% 136.94/137.27 731 : #-{T} E60 { 0, 2, 6, 14, 29, 60 }
% 136.94/137.27 732 : pppp11-{T}(E29,E60) { 0, 2, 6, 14, 29, 60 }
% 136.94/137.27 733 : p105-{T}(E60) { 0, 2, 6, 14, 29, 60 }
% 136.94/137.27 734 : r1-{T}(E29,E60) { 0, 2, 6, 14, 29, 60 }
% 136.94/137.27 735 : pppp10-{T}(E60) { 0, 2, 6, 14, 29, 60 }
% 136.94/137.27 736 : p104-{T}(E60) { 0, 2, 6, 14, 29, 60 }
% 136.94/137.27 737 : p103-{T}(E60) { 0, 2, 6, 14, 29, 60 }
% 136.94/137.27 738 : p5-{T}(E60) { 0, 2, 6, 14, 29, 60 }
% 136.94/137.27 739 : p102-{T}(E60) { 0, 2, 6, 14, 29, 60 }
% 136.94/137.27 740 : p101-{T}(E60) { 0, 2, 6, 14, 29, 60 }
% 136.94/137.27 741 : p100-{T}(E60) { 0, 2, 6, 14, 29, 60 }
% 136.94/137.27 742 : #-{T} E61 { 0, 2, 6, 14, 30, 61 }
% 136.94/137.27 743 : pppp12-{T}(E30,E61) { 0, 2, 6, 14, 30, 61 }
% 136.94/137.27 744 : p105-{T}(E61) { 0, 2, 6, 14, 30, 61 }
% 136.94/137.27 745 : p6-{T}(E61) { 0, 2, 6, 14, 30, 61 }
% 136.94/137.27 746 : r1-{T}(E30,E61) { 0, 2, 6, 14, 30, 61 }
% 136.94/137.27 747 : pppp10-{T}(E61) { 0, 2, 6, 14, 30, 61 }
% 136.94/137.27 748 : p104-{T}(E61) { 0, 2, 6, 14, 30, 61 }
% 136.94/137.27 749 : p103-{T}(E61) { 0, 2, 6, 14, 30, 61 }
% 136.94/137.27 750 : p102-{T}(E61) { 0, 2, 6, 14, 30, 61 }
% 136.94/137.27 751 : p101-{T}(E61) { 0, 2, 6, 14, 30, 61 }
% 136.94/137.27 752 : p100-{T}(E61) { 0, 2, 6, 14, 30, 61 }
% 136.94/137.27 753 : #-{T} E62 { 0, 2, 6, 14, 30, 62 }
% 136.94/137.27 754 : pppp11-{T}(E30,E62) { 0, 2, 6, 14, 30, 62 }
% 136.94/137.27 755 : p105-{T}(E62) { 0, 2, 6, 14, 30, 62 }
% 136.94/137.27 756 : r1-{T}(E30,E62) { 0, 2, 6, 14, 30, 62 }
% 136.94/137.27 757 : pppp10-{T}(E62) { 0, 2, 6, 14, 30, 62 }
% 136.94/137.28 758 : p104-{T}(E62) { 0, 2, 6, 14, 30, 62 }
% 136.94/137.28 759 : p103-{T}(E62) { 0, 2, 6, 14, 30, 62 }
% 136.94/137.28 760 : p102-{T}(E62) { 0, 2, 6, 14, 30, 62 }
% 136.94/137.28 761 : p101-{T}(E62) { 0, 2, 6, 14, 30, 62 }
% 136.94/137.28 762 : p100-{T}(E62) { 0, 2, 6, 14, 30, 62 }
% 136.94/137.28
% 136.94/137.28
% 136.94/137.28 % SZS output end Model for /export/starexec/sandbox/benchmark/theBenchmark.p
% 136.94/137.28
% 136.94/137.28 randbase = 1
%------------------------------------------------------------------------------