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