%------------------------------------------------------------------------------
% File : Geo-III---2018C
% Problem : RNG132-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : geo -tptp_input -nonempty -inputfile %s
% Computer : n029.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 06:50:04 PM UTC 2026
% Result : Satisfiable 119.10s 119.35s
% Output : Model 119.10s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : RNG132-1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.12 % Command : geo -tptp_input -nonempty -inputfile %s
% 0.17/0.34 % Computer : n029.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Tue May 5 05:16:14 EDT 2026
% 0.17/0.34 % CPUTime :
% 119.10/119.35 GeoParameters:
% 119.10/119.35
% 119.10/119.35 tptp_input = 1
% 119.10/119.35 tptp_output = 0
% 119.10/119.35 nonempty = 1
% 119.10/119.35 inputfile = /export/starexec/sandbox2/benchmark/theBenchmark.p
% 119.10/119.35 includepath = /export/starexec/sandbox2/solver/bin/../../benchmark/
% 119.10/119.35
% 119.10/119.35
% 119.10/119.35 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 119.10/119.35 % SZS output start Model for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 119.10/119.35
% 119.10/119.35 Interpretation 100:
% 119.10/119.35 Guesses:
% 119.10/119.35 0 : guesser 1, 0, ( | 1, 0 ), 0, 1m59s old, 0 lemmas
% 119.10/119.35 1 : guesser 14, 12, ( | 1, 2, 0 ), 58, 43s old, 0 lemmas
% 119.10/119.35 2 : guesser 15, 13, ( | 0, 2, 1 ), 58, 43s old, 0 lemmas
% 119.10/119.35 3 : guesser 16, 14, ( | 1, 2, 0 ), 58, 43s old, 0 lemmas
% 119.10/119.35 4 : guesser 17, 15, ( | 0, 2, 1 ), 58, 43s old, 0 lemmas
% 119.10/119.35 5 : guesser 18, 16, ( | 0, 2, 1 ), 58, 43s old, 0 lemmas
% 119.10/119.35 6 : guesser 19, 17, ( | 0, 2, 1 ), 58, 43s old, 0 lemmas
% 119.10/119.35 7 : guesser 20, 18, ( | 0, 2, 1 ), 58, 43s old, 0 lemmas
% 119.10/119.35 8 : guesser 21, 19, ( | 1, 2, 0 ), 58, 43s old, 0 lemmas
% 119.10/119.35 9 : guesser 22, 20, ( 0 | 2, 1 ), 58, 43s old, 1 lemmas
% 119.10/119.35 10 : guesser 65, 62, ( 1 | 0, 3, 2 ), 94, 14s old, 3 lemmas
% 119.10/119.35 11 : guesser 75, 72, ( 1, 0 | 3, 2 ), 96, 14s old, 1 lemmas
% 119.10/119.35 12 : guesser 151, 147, ( 0, 3 | 2, 4, 1 ), 97, 14s old, 1 lemmas
% 119.10/119.35 13 : guesser 152, 148, ( 1, 0, 3 | 4, 2 ), 98, 14s old, 2 lemmas
% 119.10/119.35
% 119.10/119.35 Elements:
% 119.10/119.35 { E0, E1, E2, E3, E4 }
% 119.10/119.35
% 119.10/119.35 Atoms:
% 119.10/119.35 0 : #-{T} E0 { }
% 119.10/119.35 1 : #-{T} E1 { 0 }
% 119.10/119.35 2 : P_zero-{T}(E1) { 0 }
% 119.10/119.35 3 : P_minus-{T}(E1,E1) { 0 }
% 119.10/119.35 4 : P_plus-{T}(E1,E1,E1) { 0 }
% 119.10/119.35 5 : P_sum4-{T}(E1,E1,E1,E1,E1) { 0 }
% 119.10/119.35 6 : P_plus-{T}(E0,E1,E0) { 0 }
% 119.10/119.35 7 : P_plus-{T}(E1,E0,E0) { 0 }
% 119.10/119.35 8 : P_sum4-{T}(E0,E1,E1,E1,E0) { 0 }
% 119.10/119.35 9 : P_sum4-{T}(E1,E0,E1,E1,E0) { 0 }
% 119.10/119.35 10 : P_sum4-{T}(E1,E1,E0,E1,E0) { 0 }
% 119.10/119.35 11 : P_sum4-{T}(E1,E1,E1,E0,E0) { 0 }
% 119.10/119.35 12 : P_sq-{T}(E1,E1) { 0 }
% 119.10/119.35 13 : P_times-{T}(E1,E1,E1) { 0 }
% 119.10/119.35 14 : P_a1-{T}(E1) { 1 }
% 119.10/119.35 15 : P_a2-{T}(E0) { 2 }
% 119.10/119.35 16 : P_a3-{T}(E1) { 3 }
% 119.10/119.35 17 : P_a4-{T}(E0) { 4 }
% 119.10/119.35 18 : P_b1-{T}(E0) { 5 }
% 119.10/119.35 19 : P_b2-{T}(E0) { 6 }
% 119.10/119.35 20 : P_b3-{T}(E0) { 7 }
% 119.10/119.35 21 : P_b4-{T}(E1) { 8 }
% 119.10/119.35 22 : #-{T} E2 { 9 }
% 119.10/119.35 23 : P_minus-{T}(E0,E2) { 9 }
% 119.10/119.35 24 : P_plus-{T}(E0,E2,E1) { 0, 9 }
% 119.10/119.35 25 : P_plus-{T}(E2,E1,E2) { 0, 9 }
% 119.10/119.35 26 : P_plus-{T}(E1,E2,E2) { 0, 9 }
% 119.10/119.35 27 : P_sum4-{T}(E2,E1,E1,E1,E2) { 0, 9 }
% 119.10/119.35 28 : P_plus-{T}(E2,E0,E1) { 0, 9 }
% 119.10/119.35 29 : P_sum4-{T}(E1,E2,E1,E1,E2) { 0, 9 }
% 119.10/119.35 30 : P_sum4-{T}(E2,E0,E1,E1,E1) { 0, 9 }
% 119.10/119.35 31 : P_sum4-{T}(E0,E2,E1,E1,E1) { 0, 9 }
% 119.10/119.35 32 : P_sum4-{T}(E2,E1,E0,E1,E1) { 0, 9 }
% 119.10/119.35 33 : P_sum4-{T}(E2,E2,E0,E1,E2) { 0, 9 }
% 119.10/119.35 34 : P_sum4-{T}(E0,E2,E0,E1,E0) { 0, 9 }
% 119.10/119.35 35 : P_sum4-{T}(E1,E2,E0,E1,E1) { 0, 9 }
% 119.10/119.35 36 : P_sum4-{T}(E2,E1,E1,E0,E1) { 0, 9 }
% 119.10/119.35 37 : P_sum4-{T}(E2,E2,E1,E0,E2) { 0, 9 }
% 119.10/119.35 38 : P_sum4-{T}(E0,E2,E1,E0,E0) { 0, 9 }
% 119.10/119.35 39 : P_sum4-{T}(E1,E2,E1,E0,E1) { 0, 9 }
% 119.10/119.35 40 : P_sum4-{T}(E1,E1,E0,E2,E1) { 0, 9 }
% 119.10/119.35 41 : P_sum4-{T}(E2,E1,E0,E2,E2) { 0, 9 }
% 119.10/119.35 42 : P_sum4-{T}(E0,E1,E0,E2,E0) { 0, 9 }
% 119.10/119.35 43 : P_sum4-{T}(E2,E0,E0,E2,E1) { 0, 9 }
% 119.10/119.35 44 : P_sum4-{T}(E1,E0,E0,E2,E0) { 0, 9 }
% 119.10/119.35 45 : P_sum4-{T}(E1,E2,E0,E2,E2) { 0, 9 }
% 119.10/119.35 46 : P_sum4-{T}(E0,E2,E0,E2,E1) { 0, 9 }
% 119.10/119.35 47 : P_sum4-{T}(E0,E0,E2,E1,E0) { 0, 9 }
% 119.10/119.35 48 : P_sum4-{T}(E1,E0,E2,E1,E1) { 0, 9 }
% 119.10/119.35 49 : P_sum4-{T}(E2,E0,E2,E1,E2) { 0, 9 }
% 119.10/119.35 50 : P_sum4-{T}(E0,E1,E2,E1,E1) { 0, 9 }
% 119.10/119.35 51 : P_sum4-{T}(E1,E1,E2,E1,E2) { 0, 9 }
% 119.10/119.35 52 : P_sum4-{T}(E2,E0,E1,E2,E2) { 0, 9 }
% 119.10/119.35 53 : P_sum4-{T}(E0,E0,E1,E2,E0) { 0, 9 }
% 119.10/119.35 54 : P_sum4-{T}(E1,E0,E1,E2,E1) { 0, 9 }
% 119.10/119.35 55 : P_sum4-{T}(E1,E1,E1,E2,E2) { 0, 9 }
% 119.10/119.35 56 : P_sum4-{T}(E0,E1,E1,E2,E1) { 0, 9 }
% 119.10/119.35 57 : P_sum4-{T}(E1,E2,E2,E0,E2) { 0, 9 }
% 119.10/119.35 58 : P_sum4-{T}(E0,E2,E2,E0,E1) { 0, 9 }
% 119.10/119.35 59 : P_sum4-{T}(E0,E1,E2,E0,E0) { 0, 9 }
% 119.10/119.35 60 : P_sum4-{T}(E1,E1,E2,E0,E1) { 0, 9 }
% 119.10/119.35 61 : P_sum4-{T}(E2,E1,E2,E0,E2) { 0, 9 }
% 119.10/119.35 62 : P_sum4-{T}(E1,E0,E2,E0,E0) { 0, 9 }
% 119.10/119.35 63 : P_sum4-{T}(E2,E0,E2,E0,E1) { 0, 9 }
% 119.10/119.35 64 : P_minus-{T}(E2,E0) { 0, 9 }
% 119.10/119.35 65 : P_sq-{T}(E0,E0) { 10 }
% 119.10/119.35 66 : P_times-{T}(E0,E0,E0) { 0, 10 }
% 119.10/119.35 67 : P_times-{T}(E0,E1,E1) { 0, 9, 10 }
% 119.10/119.35 68 : P_times-{T}(E1,E0,E1) { 0, 9, 10 }
% 119.10/119.35 69 : P_times-{T}(E0,E2,E2) { 0, 9, 10 }
% 119.10/119.35 70 : P_times-{T}(E2,E0,E2) { 0, 9, 10 }
% 119.10/119.35 71 : P_times-{T}(E1,E2,E1) { 0, 9, 10 }
% 119.10/119.35 72 : P_times-{T}(E2,E1,E1) { 0, 9, 10 }
% 119.10/119.35 73 : P_times-{T}(E2,E2,E0) { 0, 9, 10 }
% 119.10/119.35 74 : P_sq-{T}(E2,E0) { 0, 9, 10 }
% 119.10/119.35 75 : #-{T} E3 { 11 }
% 119.10/119.35 76 : P_plus-{T}(E0,E0,E3) { 11 }
% 119.10/119.35 77 : P_plus-{T}(E3,E1,E3) { 0, 11 }
% 119.10/119.35 78 : P_plus-{T}(E1,E3,E3) { 0, 11 }
% 119.10/119.35 79 : P_sum4-{T}(E0,E0,E1,E1,E3) { 0, 11 }
% 119.10/119.35 80 : P_sum4-{T}(E3,E1,E1,E1,E3) { 0, 11 }
% 119.10/119.35 81 : P_plus-{T}(E2,E3,E0) { 0, 9, 11 }
% 119.10/119.35 82 : P_times-{T}(E0,E3,E3) { 0, 10, 11 }
% 119.10/119.35 83 : P_sum4-{T}(E1,E3,E1,E1,E3) { 0, 11 }
% 119.10/119.35 84 : P_plus-{T}(E3,E2,E0) { 0, 9, 11 }
% 119.10/119.35 85 : P_sum4-{T}(E1,E2,E2,E3,E1) { 0, 9, 11 }
% 119.10/119.35 86 : P_sum4-{T}(E0,E1,E0,E1,E3) { 0, 11 }
% 119.10/119.35 87 : P_sum4-{T}(E1,E2,E3,E2,E1) { 0, 9, 11 }
% 119.10/119.35 88 : P_times-{T}(E3,E0,E3) { 0, 10, 11 }
% 119.10/119.35 89 : P_sum4-{T}(E1,E0,E0,E1,E3) { 0, 11 }
% 119.10/119.35 90 : P_sum4-{T}(E0,E2,E3,E2,E0) { 0, 9, 11 }
% 119.10/119.35 91 : P_times-{T}(E1,E3,E1) { 0, 9, 10, 11 }
% 119.10/119.35 92 : P_sum4-{T}(E0,E1,E1,E0,E3) { 0, 11 }
% 119.10/119.35 93 : P_sum4-{T}(E0,E2,E2,E3,E0) { 0, 9, 11 }
% 119.10/119.35 94 : P_times-{T}(E3,E1,E1) { 0, 9, 10, 11 }
% 119.10/119.35 95 : P_sum4-{T}(E1,E0,E1,E0,E3) { 0, 11 }
% 119.10/119.35 96 : P_sum4-{T}(E2,E2,E0,E0,E1) { 0, 9, 11 }
% 119.10/119.35 97 : P_sum4-{T}(E1,E1,E0,E0,E3) { 0, 11 }
% 119.10/119.35 98 : P_sum4-{T}(E1,E3,E2,E1,E0) { 0, 9, 11 }
% 119.10/119.35 99 : P_sum4-{T}(E1,E1,E1,E3,E3) { 0, 11 }
% 119.10/119.35 100 : P_sum4-{T}(E1,E1,E3,E1,E3) { 0, 11 }
% 119.10/119.35 101 : P_sum4-{T}(E2,E3,E1,E1,E0) { 0, 9, 11 }
% 119.10/119.35 102 : P_sum4-{T}(E1,E3,E1,E2,E0) { 0, 9, 11 }
% 119.10/119.35 103 : P_sum4-{T}(E3,E2,E1,E1,E0) { 0, 9, 11 }
% 119.10/119.35 104 : P_sum4-{T}(E1,E2,E1,E3,E0) { 0, 9, 11 }
% 119.10/119.35 105 : P_sum4-{T}(E2,E0,E0,E1,E0) { 0, 9, 11 }
% 119.10/119.35 106 : P_sum4-{T}(E1,E2,E3,E1,E0) { 0, 9, 11 }
% 119.10/119.35 107 : P_sum4-{T}(E3,E2,E0,E1,E3) { 0, 9, 11 }
% 119.10/119.35 108 : P_sum4-{T}(E1,E2,E0,E0,E0) { 0, 9, 11 }
% 119.10/119.35 109 : P_sum4-{T}(E2,E0,E1,E0,E0) { 0, 9, 11 }
% 119.10/119.35 110 : P_sum4-{T}(E1,E1,E3,E2,E0) { 0, 9, 11 }
% 119.10/119.35 111 : P_sum4-{T}(E3,E2,E1,E0,E3) { 0, 9, 11 }
% 119.10/119.35 112 : P_sum4-{T}(E1,E1,E2,E3,E0) { 0, 9, 11 }
% 119.10/119.35 113 : P_sum4-{T}(E3,E1,E0,E2,E3) { 0, 9, 11 }
% 119.10/119.35 114 : P_sum4-{T}(E1,E3,E2,E0,E3) { 0, 9, 11 }
% 119.10/119.35 115 : P_sum4-{T}(E0,E0,E0,E2,E3) { 0, 9, 11 }
% 119.10/119.35 116 : P_sum4-{T}(E1,E3,E0,E2,E3) { 0, 9, 11 }
% 119.10/119.35 117 : P_sum4-{T}(E2,E3,E0,E2,E0) { 0, 9, 11 }
% 119.10/119.35 118 : P_sum4-{T}(E1,E0,E3,E2,E3) { 0, 9, 11 }
% 119.10/119.35 119 : P_sum4-{T}(E3,E2,E0,E2,E0) { 0, 9, 11 }
% 119.10/119.35 120 : P_sum4-{T}(E1,E0,E2,E3,E3) { 0, 9, 11 }
% 119.10/119.35 121 : P_sum4-{T}(E3,E1,E2,E1,E0) { 0, 9, 11 }
% 119.10/119.35 122 : P_sum4-{T}(E2,E1,E1,E3,E0) { 0, 9, 11 }
% 119.10/119.35 123 : P_sum4-{T}(E0,E3,E2,E1,E3) { 0, 9, 11 }
% 119.10/119.35 124 : P_sum4-{T}(E2,E1,E3,E1,E0) { 0, 9, 11 }
% 119.10/119.35 125 : P_sum4-{T}(E2,E3,E2,E1,E1) { 0, 9, 11 }
% 119.10/119.35 126 : P_sum4-{T}(E2,E1,E0,E0,E0) { 0, 9, 11 }
% 119.10/119.35 127 : P_sum4-{T}(E3,E0,E2,E1,E3) { 0, 9, 11 }
% 119.10/119.35 128 : P_sum4-{T}(E2,E3,E2,E0,E0) { 0, 9, 11 }
% 119.10/119.35 129 : P_sum4-{T}(E3,E1,E1,E2,E0) { 0, 9, 11 }
% 119.10/119.35 130 : P_sum4-{T}(E2,E0,E3,E2,E0) { 0, 9, 11 }
% 119.10/119.35 131 : P_sum4-{T}(E2,E3,E1,E2,E1) { 0, 9, 11 }
% 119.10/119.35 132 : P_sum4-{T}(E2,E0,E2,E3,E0) { 0, 9, 11 }
% 119.10/119.35 133 : P_sum4-{T}(E0,E3,E1,E2,E3) { 0, 9, 11 }
% 119.10/119.35 134 : P_sum4-{T}(E2,E2,E1,E3,E1) { 0, 9, 11 }
% 119.10/119.35 135 : P_sum4-{T}(E3,E0,E1,E2,E3) { 0, 9, 11 }
% 119.10/119.35 136 : P_sum4-{T}(E2,E2,E3,E1,E1) { 0, 9, 11 }
% 119.10/119.35 137 : P_sum4-{T}(E3,E2,E2,E0,E0) { 0, 9, 11 }
% 119.10/119.35 138 : P_sum4-{T}(E2,E1,E2,E3,E1) { 0, 9, 11 }
% 119.10/119.35 139 : P_sum4-{T}(E3,E1,E2,E0,E3) { 0, 9, 11 }
% 119.10/119.35 140 : P_sum4-{T}(E2,E1,E3,E2,E1) { 0, 9, 11 }
% 119.10/119.35 141 : P_sum4-{T}(E0,E0,E2,E0,E3) { 0, 9, 11 }
% 119.10/119.35 142 : P_sum4-{T}(E0,E2,E0,E0,E3) { 0, 9, 11 }
% 119.10/119.35 143 : P_sum4-{T}(E0,E2,E3,E1,E3) { 0, 9, 11 }
% 119.10/119.35 144 : P_sum4-{T}(E0,E2,E1,E3,E3) { 0, 9, 11 }
% 119.10/119.35 145 : P_sum4-{T}(E0,E1,E2,E3,E3) { 0, 9, 11 }
% 119.10/119.35 146 : P_sum4-{T}(E3,E2,E2,E3,E3) { 0, 9, 11 }
% 119.10/119.35 147 : P_sum4-{T}(E2,E2,E2,E3,E2) { 0, 9, 11 }
% 119.10/119.35 148 : P_sum4-{T}(E0,E1,E3,E2,E3) { 0, 9, 11 }
% 119.10/119.35 149 : P_sum4-{T}(E3,E2,E3,E2,E3) { 0, 9, 11 }
% 119.10/119.35 150 : P_sum4-{T}(E2,E2,E3,E2,E2) { 0, 9, 11 }
% 119.10/119.35 151 : P_sum4-{T}(E0,E0,E0,E0,E2) { 12 }
% 119.10/119.35 152 : #-{T} E4 { 0, 13 }
% 119.10/119.35 153 : P_sum4-{T}(E0,E0,E0,E1,E4) { 0, 13 }
% 119.10/119.35 154 : P_plus-{T}(E4,E1,E4) { 0, 13 }
% 119.10/119.35 155 : P_plus-{T}(E0,E3,E4) { 0, 11, 13 }
% 119.10/119.35 156 : P_plus-{T}(E1,E4,E4) { 0, 13 }
% 119.10/119.35 157 : P_sum4-{T}(E4,E1,E1,E1,E4) { 0, 13 }
% 119.10/119.35 158 : P_sum4-{T}(E1,E4,E1,E1,E4) { 0, 13 }
% 119.10/119.35 159 : P_plus-{T}(E3,E0,E4) { 0, 11, 13 }
% 119.10/119.35 160 : P_sum4-{T}(E1,E1,E1,E4,E4) { 0, 13 }
% 119.10/119.35 161 : P_plus-{T}(E2,E4,E3) { 0, 9, 11, 13 }
% 119.10/119.35 162 : P_times-{T}(E0,E4,E4) { 0, 10, 11, 13 }
% 119.10/119.35 163 : P_sum4-{T}(E1,E1,E4,E1,E4) { 0, 13 }
% 119.10/119.35 164 : P_plus-{T}(E4,E2,E3) { 0, 9, 11, 13 }
% 119.10/119.35 165 : P_sum4-{T}(E4,E2,E0,E1,E4) { 0, 9, 13 }
% 119.10/119.35 166 : P_sum4-{T}(E1,E4,E0,E2,E4) { 0, 9, 13 }
% 119.10/119.35 167 : P_times-{T}(E4,E0,E4) { 0, 10, 11, 13 }
% 119.10/119.35 168 : P_sum4-{T}(E4,E2,E1,E0,E4) { 0, 9, 13 }
% 119.10/119.35 169 : P_sum4-{T}(E1,E4,E2,E0,E4) { 0, 9, 13 }
% 119.10/119.35 170 : P_times-{T}(E1,E4,E1) { 0, 9, 10, 11, 13 }
% 119.10/119.35 171 : P_sum4-{T}(E4,E1,E0,E2,E4) { 0, 9, 13 }
% 119.10/119.35 172 : P_sum4-{T}(E1,E3,E0,E1,E4) { 0, 11, 13 }
% 119.10/119.35 173 : P_times-{T}(E4,E1,E1) { 0, 9, 10, 11, 13 }
% 119.10/119.35 174 : P_sum4-{T}(E4,E0,E2,E1,E4) { 0, 9, 13 }
% 119.10/119.35 175 : P_sum4-{T}(E1,E3,E1,E0,E4) { 0, 11, 13 }
% 119.10/119.35 176 : P_plus-{T}(E0,E4,E2) { 0, 11, 12, 13 }
% 119.10/119.35 177 : P_sum4-{T}(E4,E0,E1,E2,E4) { 0, 9, 13 }
% 119.10/119.35 178 : P_sum4-{T}(E1,E0,E0,E0,E4) { 0, 11, 13 }
% 119.10/119.35 179 : P_plus-{T}(E4,E0,E2) { 0, 11, 12, 13 }
% 119.10/119.35 180 : P_sum4-{T}(E4,E1,E2,E0,E4) { 0, 9, 13 }
% 119.10/119.35 181 : P_sum4-{T}(E1,E0,E1,E3,E4) { 0, 11, 13 }
% 119.10/119.35 182 : P_plus-{T}(E3,E3,E2) { 0, 11, 12, 13 }
% 119.10/119.35 183 : P_sum4-{T}(E3,E0,E1,E1,E4) { 0, 11, 13 }
% 119.10/119.35 184 : P_sum4-{T}(E1,E0,E3,E1,E4) { 0, 11, 13 }
% 119.10/119.35 185 : P_plus-{T}(E4,E3,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 186 : P_sum4-{T}(E0,E3,E1,E1,E4) { 0, 11, 13 }
% 119.10/119.35 187 : P_sum4-{T}(E1,E1,E3,E0,E4) { 0, 11, 13 }
% 119.10/119.35 188 : P_plus-{T}(E3,E4,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 189 : P_sum4-{T}(E3,E1,E0,E1,E4) { 0, 11, 13 }
% 119.10/119.35 190 : P_sum4-{T}(E1,E1,E0,E3,E4) { 0, 11, 13 }
% 119.10/119.35 191 : P_plus-{T}(E4,E4,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 192 : P_sum4-{T}(E3,E1,E1,E0,E4) { 0, 11, 13 }
% 119.10/119.35 193 : P_sum4-{T}(E1,E4,E1,E2,E3) { 0, 9, 11, 13 }
% 119.10/119.35 194 : P_plus-{T}(E2,E2,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 195 : P_sum4-{T}(E0,E0,E1,E0,E4) { 0, 11, 13 }
% 119.10/119.35 196 : P_sum4-{T}(E1,E4,E2,E1,E3) { 0, 9, 11, 13 }
% 119.10/119.35 197 : P_minus-{T}(E4,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 198 : P_sum4-{T}(E0,E1,E0,E0,E4) { 0, 11, 13 }
% 119.10/119.35 199 : P_sum4-{T}(E1,E2,E0,E3,E3) { 0, 9, 11, 13 }
% 119.10/119.35 200 : P_minus-{T}(E3,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 201 : P_sum4-{T}(E0,E1,E3,E1,E4) { 0, 11, 13 }
% 119.10/119.35 202 : P_sum4-{T}(E1,E2,E4,E1,E3) { 0, 9, 11, 13 }
% 119.10/119.35 203 : P_times-{T}(E3,E3,E2) { 0, 10, 11, 12, 13 }
% 119.10/119.35 204 : P_sum4-{T}(E0,E1,E1,E3,E4) { 0, 11, 13 }
% 119.10/119.35 205 : P_sum4-{T}(E1,E2,E3,E0,E3) { 0, 9, 11, 13 }
% 119.10/119.35 206 : P_sq-{T}(E3,E2) { 0, 10, 11, 12, 13 }
% 119.10/119.35 207 : P_sum4-{T}(E2,E4,E1,E1,E3) { 0, 9, 11, 13 }
% 119.10/119.35 208 : P_sum4-{T}(E1,E2,E1,E4,E3) { 0, 9, 11, 13 }
% 119.10/119.35 209 : P_times-{T}(E2,E3,E4) { 0, 9, 10, 11, 12, 13 }
% 119.10/119.35 210 : P_sum4-{T}(E4,E2,E1,E1,E3) { 0, 9, 11, 13 }
% 119.10/119.35 211 : P_sum4-{T}(E1,E1,E4,E2,E3) { 0, 9, 11, 13 }
% 119.10/119.35 212 : P_times-{T}(E3,E2,E4) { 0, 9, 10, 11, 12, 13 }
% 119.10/119.35 213 : P_sum4-{T}(E2,E3,E0,E1,E3) { 0, 9, 11, 13 }
% 119.10/119.35 214 : P_sum4-{T}(E1,E1,E2,E4,E3) { 0, 9, 11, 13 }
% 119.10/119.35 215 : P_times-{T}(E4,E2,E3) { 0, 9, 10, 11, 12, 13 }
% 119.10/119.35 216 : P_sum4-{T}(E2,E3,E1,E0,E3) { 0, 9, 11, 13 }
% 119.10/119.35 217 : P_sum4-{T}(E1,E2,E4,E2,E0) { 0, 9, 11, 13 }
% 119.10/119.35 218 : P_times-{T}(E2,E4,E3) { 0, 9, 10, 11, 12, 13 }
% 119.10/119.35 219 : P_sum4-{T}(E2,E4,E0,E2,E3) { 0, 9, 11, 13 }
% 119.10/119.35 220 : P_sum4-{T}(E1,E2,E2,E4,E0) { 0, 9, 11, 13 }
% 119.10/119.35 221 : P_times-{T}(E4,E3,E0) { 0, 9, 10, 11, 12, 13 }
% 119.10/119.35 222 : P_sum4-{T}(E3,E0,E0,E2,E4) { 0, 9, 11, 13 }
% 119.10/119.35 223 : P_sum4-{T}(E1,E0,E2,E4,E4) { 0, 9, 11, 13 }
% 119.10/119.35 224 : P_times-{T}(E3,E4,E0) { 0, 9, 10, 11, 12, 13 }
% 119.10/119.35 225 : P_sum4-{T}(E4,E2,E0,E2,E3) { 0, 9, 11, 13 }
% 119.10/119.35 226 : P_sum4-{T}(E1,E0,E4,E2,E4) { 0, 9, 11, 13 }
% 119.10/119.35 227 : P_times-{T}(E4,E4,E2) { 0, 9, 10, 11, 12, 13 }
% 119.10/119.35 228 : P_sum4-{T}(E0,E3,E0,E2,E4) { 0, 9, 11, 13 }
% 119.10/119.35 229 : P_sum4-{T}(E1,E3,E3,E2,E4) { 0, 9, 11, 13 }
% 119.10/119.35 230 : P_sq-{T}(E4,E2) { 0, 9, 10, 11, 12, 13 }
% 119.10/119.35 231 : P_sum4-{T}(E4,E1,E2,E1,E3) { 0, 9, 11, 13 }
% 119.10/119.35 232 : P_sum4-{T}(E1,E3,E2,E3,E4) { 0, 9, 11, 13 }
% 119.10/119.35 233 : P_sum4-{T}(E0,E4,E2,E1,E4) { 0, 9, 11, 13 }
% 119.10/119.35 234 : P_sum4-{T}(E0,E2,E4,E2,E3) { 0, 9, 11, 13 }
% 119.10/119.35 235 : P_sum4-{T}(E2,E4,E2,E1,E0) { 0, 9, 11, 13 }
% 119.10/119.35 236 : P_sum4-{T}(E0,E2,E2,E4,E3) { 0, 9, 11, 13 }
% 119.10/119.35 237 : P_sum4-{T}(E3,E3,E2,E1,E4) { 0, 9, 11, 13 }
% 119.10/119.35 238 : P_sum4-{T}(E2,E4,E1,E2,E0) { 0, 9, 11, 13 }
% 119.10/119.35 239 : P_sum4-{T}(E4,E1,E1,E2,E3) { 0, 9, 11, 13 }
% 119.10/119.35 240 : P_sum4-{T}(E2,E2,E0,E3,E0) { 0, 9, 11, 13 }
% 119.10/119.35 241 : P_sum4-{T}(E0,E4,E1,E2,E4) { 0, 9, 11, 13 }
% 119.10/119.35 242 : P_sum4-{T}(E2,E2,E4,E1,E0) { 0, 9, 11, 13 }
% 119.10/119.35 243 : P_sum4-{T}(E3,E3,E1,E2,E4) { 0, 9, 11, 13 }
% 119.10/119.35 244 : P_sum4-{T}(E2,E2,E3,E0,E0) { 0, 9, 11, 13 }
% 119.10/119.35 245 : P_sum4-{T}(E2,E4,E2,E0,E3) { 0, 9, 11, 13 }
% 119.10/119.35 246 : P_sum4-{T}(E2,E2,E1,E4,E0) { 0, 9, 11, 13 }
% 119.10/119.35 247 : P_sum4-{T}(E3,E0,E2,E0,E4) { 0, 9, 11, 13 }
% 119.10/119.35 248 : P_sum4-{T}(E2,E1,E4,E2,E0) { 0, 9, 11, 13 }
% 119.10/119.35 249 : P_sum4-{T}(E4,E2,E2,E0,E3) { 0, 9, 11, 13 }
% 119.10/119.35 250 : P_sum4-{T}(E2,E1,E2,E4,E0) { 0, 9, 11, 13 }
% 119.10/119.35 251 : P_sum4-{T}(E0,E3,E2,E0,E4) { 0, 9, 11, 13 }
% 119.10/119.35 252 : P_sum4-{T}(E2,E2,E2,E4,E1) { 0, 9, 11, 13 }
% 119.10/119.35 253 : P_sum4-{T}(E3,E2,E0,E0,E4) { 0, 9, 11, 13 }
% 119.10/119.35 254 : P_sum4-{T}(E2,E2,E4,E2,E1) { 0, 9, 11, 13 }
% 119.10/119.35 255 : P_sum4-{T}(E2,E0,E0,E0,E3) { 0, 9, 11, 13 }
% 119.10/119.35 256 : P_sum4-{T}(E2,E1,E0,E3,E3) { 0, 9, 11, 13 }
% 119.10/119.35 257 : P_sum4-{T}(E3,E2,E3,E1,E4) { 0, 9, 11, 13 }
% 119.10/119.35 258 : P_sum4-{T}(E2,E1,E4,E1,E3) { 0, 9, 11, 13 }
% 119.10/119.35 259 : P_sum4-{T}(E2,E0,E3,E1,E3) { 0, 9, 11, 13 }
% 119.10/119.35 260 : P_sum4-{T}(E2,E1,E3,E0,E3) { 0, 9, 11, 13 }
% 119.10/119.35 261 : P_sum4-{T}(E3,E2,E1,E3,E4) { 0, 9, 11, 13 }
% 119.10/119.35 262 : P_sum4-{T}(E2,E1,E1,E4,E3) { 0, 9, 11, 13 }
% 119.10/119.35 263 : P_sum4-{T}(E2,E0,E1,E3,E3) { 0, 9, 11, 13 }
% 119.10/119.35 264 : P_sum4-{T}(E2,E0,E4,E2,E3) { 0, 9, 11, 13 }
% 119.10/119.35 265 : P_sum4-{T}(E3,E1,E2,E3,E4) { 0, 9, 11, 13 }
% 119.10/119.35 266 : P_sum4-{T}(E2,E0,E2,E4,E3) { 0, 9, 11, 13 }
% 119.10/119.35 267 : P_sum4-{T}(E0,E0,E2,E3,E4) { 0, 9, 11, 13 }
% 119.10/119.35 268 : P_sum4-{T}(E2,E3,E3,E2,E3) { 0, 9, 11, 13 }
% 119.10/119.35 269 : P_sum4-{T}(E2,E3,E2,E3,E3) { 0, 9, 11, 13 }
% 119.10/119.35 270 : P_sum4-{T}(E4,E2,E2,E3,E4) { 0, 9, 11, 13 }
% 119.10/119.35 271 : P_sum4-{T}(E1,E1,E3,E4,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 272 : P_sum4-{T}(E3,E1,E3,E2,E4) { 0, 9, 11, 13 }
% 119.10/119.35 273 : P_sum4-{T}(E1,E1,E4,E3,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 274 : P_sum4-{T}(E0,E0,E3,E2,E4) { 0, 9, 11, 13 }
% 119.10/119.35 275 : P_sum4-{T}(E1,E3,E2,E2,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 276 : P_sum4-{T}(E4,E2,E3,E2,E4) { 0, 9, 11, 13 }
% 119.10/119.35 277 : P_sum4-{T}(E1,E3,E3,E0,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 278 : P_sum4-{T}(E0,E2,E0,E3,E4) { 0, 9, 11, 13 }
% 119.10/119.35 279 : P_sum4-{T}(E1,E3,E1,E4,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 280 : P_sum4-{T}(E0,E2,E1,E4,E4) { 0, 9, 11, 13 }
% 119.10/119.35 281 : P_sum4-{T}(E1,E3,E0,E3,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 282 : P_sum4-{T}(E0,E2,E3,E0,E4) { 0, 9, 11, 13 }
% 119.10/119.35 283 : P_sum4-{T}(E1,E3,E4,E1,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 284 : P_sum4-{T}(E3,E2,E2,E4,E4) { 0, 9, 11, 13 }
% 119.10/119.35 285 : P_sum4-{T}(E1,E4,E4,E2,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 286 : P_sum4-{T}(E0,E1,E2,E4,E4) { 0, 9, 11, 13 }
% 119.10/119.35 287 : P_sum4-{T}(E1,E4,E2,E4,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 288 : P_sum4-{T}(E3,E2,E4,E2,E4) { 0, 9, 11, 13 }
% 119.10/119.35 289 : P_sum4-{T}(E1,E4,E1,E3,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 290 : P_sum4-{T}(E0,E1,E4,E2,E4) { 0, 9, 11, 13 }
% 119.10/119.35 291 : P_sum4-{T}(E1,E4,E3,E1,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 292 : P_sum4-{T}(E0,E2,E4,E1,E4) { 0, 9, 11, 13 }
% 119.10/119.35 293 : P_sum4-{T}(E1,E4,E0,E0,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 294 : P_sum4-{T}(E4,E0,E1,E1,E2) { 0, 11, 12, 13 }
% 119.10/119.35 295 : P_sum4-{T}(E1,E0,E3,E3,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 296 : P_sum4-{T}(E0,E4,E1,E1,E2) { 0, 11, 12, 13 }
% 119.10/119.35 297 : P_sum4-{T}(E1,E0,E4,E0,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 298 : P_sum4-{T}(E3,E3,E1,E1,E2) { 0, 11, 12, 13 }
% 119.10/119.35 299 : P_sum4-{T}(E1,E0,E0,E4,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 300 : P_sum4-{T}(E4,E1,E0,E1,E2) { 0, 11, 12, 13 }
% 119.10/119.35 301 : P_sum4-{T}(E1,E2,E4,E4,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 302 : P_sum4-{T}(E0,E3,E0,E1,E2) { 0, 11, 12, 13 }
% 119.10/119.35 303 : P_sum4-{T}(E1,E0,E3,E4,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 304 : P_sum4-{T}(E3,E0,E0,E1,E2) { 0, 11, 12, 13 }
% 119.10/119.35 305 : P_sum4-{T}(E1,E0,E4,E3,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 306 : P_sum4-{T}(E4,E1,E1,E0,E2) { 0, 11, 12, 13 }
% 119.10/119.35 307 : P_sum4-{T}(E1,E4,E2,E2,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 308 : P_sum4-{T}(E0,E3,E1,E0,E2) { 0, 11, 12, 13 }
% 119.10/119.35 309 : P_sum4-{T}(E1,E4,E3,E0,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 310 : P_sum4-{T}(E3,E0,E1,E0,E2) { 0, 11, 12, 13 }
% 119.10/119.35 311 : P_sum4-{T}(E1,E4,E1,E4,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 312 : P_sum4-{T}(E3,E1,E0,E0,E2) { 0, 11, 12, 13 }
% 119.10/119.35 313 : P_sum4-{T}(E1,E4,E0,E3,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 314 : P_sum4-{T}(E0,E0,E1,E3,E2) { 0, 11, 12, 13 }
% 119.10/119.35 315 : P_sum4-{T}(E1,E4,E4,E1,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 316 : P_sum4-{T}(E3,E1,E1,E3,E2) { 0, 11, 12, 13 }
% 119.10/119.35 317 : P_sum4-{T}(E1,E1,E4,E4,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 318 : P_sum4-{T}(E0,E1,E0,E3,E2) { 0, 11, 12, 13 }
% 119.10/119.35 319 : P_sum4-{T}(E1,E3,E3,E3,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 320 : P_sum4-{T}(E0,E1,E3,E0,E2) { 0, 11, 12, 13 }
% 119.10/119.35 321 : P_sum4-{T}(E1,E3,E4,E0,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 322 : P_sum4-{T}(E0,E1,E4,E1,E2) { 0, 11, 12, 13 }
% 119.10/119.35 323 : P_sum4-{T}(E1,E3,E0,E4,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 324 : P_sum4-{T}(E0,E1,E1,E4,E2) { 0, 11, 12, 13 }
% 119.10/119.35 325 : P_sum4-{T}(E1,E2,E3,E4,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 326 : P_sum4-{T}(E0,E0,E3,E1,E2) { 0, 11, 12, 13 }
% 119.10/119.35 327 : P_sum4-{T}(E1,E2,E4,E3,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 328 : P_sum4-{T}(E3,E1,E3,E1,E2) { 0, 11, 12, 13 }
% 119.10/119.35 329 : P_sum4-{T}(E1,E3,E1,E3,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 330 : P_sum4-{T}(E4,E4,E1,E1,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 331 : P_sum4-{T}(E1,E3,E3,E1,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 332 : P_sum4-{T}(E3,E4,E1,E1,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 333 : P_sum4-{T}(E4,E1,E3,E4,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 334 : P_sum4-{T}(E4,E3,E1,E1,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 335 : P_sum4-{T}(E4,E1,E4,E3,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 336 : P_sum4-{T}(E2,E2,E1,E1,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 337 : P_sum4-{T}(E4,E3,E2,E2,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 338 : P_sum4-{T}(E1,E4,E0,E1,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 339 : P_sum4-{T}(E4,E3,E3,E0,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 340 : P_sum4-{T}(E0,E4,E0,E1,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 341 : P_sum4-{T}(E4,E3,E1,E4,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 342 : P_sum4-{T}(E2,E4,E0,E1,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 343 : P_sum4-{T}(E4,E3,E0,E3,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 344 : P_sum4-{T}(E4,E4,E0,E1,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 345 : P_sum4-{T}(E4,E3,E4,E1,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 346 : P_sum4-{T}(E3,E4,E0,E1,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 347 : P_sum4-{T}(E4,E4,E0,E0,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 348 : P_sum4-{T}(E4,E3,E0,E1,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 349 : P_sum4-{T}(E4,E4,E4,E2,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 350 : P_sum4-{T}(E3,E3,E0,E1,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 351 : P_sum4-{T}(E4,E4,E2,E4,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 352 : P_sum4-{T}(E4,E0,E0,E1,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 353 : P_sum4-{T}(E4,E4,E1,E3,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 354 : P_sum4-{T}(E3,E4,E1,E0,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 355 : P_sum4-{T}(E4,E4,E3,E1,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 356 : P_sum4-{T}(E1,E4,E1,E0,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 357 : P_sum4-{T}(E4,E0,E3,E3,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 358 : P_sum4-{T}(E0,E4,E1,E0,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 359 : P_sum4-{T}(E4,E0,E4,E0,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 360 : P_sum4-{T}(E2,E4,E1,E0,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 361 : P_sum4-{T}(E4,E0,E0,E4,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 362 : P_sum4-{T}(E4,E4,E1,E0,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 363 : P_sum4-{T}(E4,E2,E4,E4,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 364 : P_sum4-{T}(E4,E3,E1,E0,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 365 : P_sum4-{T}(E3,E1,E3,E4,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 366 : P_sum4-{T}(E3,E3,E1,E0,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 367 : P_sum4-{T}(E3,E1,E4,E3,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 368 : P_sum4-{T}(E4,E0,E1,E0,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 369 : P_sum4-{T}(E3,E3,E2,E2,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 370 : P_sum4-{T}(E2,E2,E0,E2,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 371 : P_sum4-{T}(E3,E3,E3,E0,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 372 : P_sum4-{T}(E4,E0,E0,E2,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 373 : P_sum4-{T}(E3,E3,E1,E4,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 374 : P_sum4-{T}(E0,E4,E0,E2,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 375 : P_sum4-{T}(E3,E3,E0,E3,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 376 : P_sum4-{T}(E4,E4,E0,E2,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 377 : P_sum4-{T}(E3,E3,E4,E1,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 378 : P_sum4-{T}(E3,E4,E0,E2,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 379 : P_sum4-{T}(E3,E4,E1,E3,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 380 : P_sum4-{T}(E4,E3,E0,E2,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 381 : P_sum4-{T}(E3,E4,E3,E1,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 382 : P_sum4-{T}(E3,E3,E0,E2,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 383 : P_sum4-{T}(E3,E4,E0,E0,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 384 : P_sum4-{T}(E0,E2,E2,E1,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 385 : P_sum4-{T}(E3,E4,E4,E2,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 386 : P_sum4-{T}(E2,E2,E2,E1,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 387 : P_sum4-{T}(E3,E4,E2,E4,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 388 : P_sum4-{T}(E1,E2,E2,E1,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 389 : P_sum4-{T}(E3,E0,E3,E3,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 390 : P_sum4-{T}(E4,E2,E2,E1,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 391 : P_sum4-{T}(E3,E0,E4,E0,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 392 : P_sum4-{T}(E3,E2,E2,E1,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 393 : P_sum4-{T}(E3,E0,E0,E4,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 394 : P_sum4-{T}(E4,E4,E2,E1,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 395 : P_sum4-{T}(E3,E2,E4,E4,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 396 : P_sum4-{T}(E3,E4,E2,E1,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 397 : P_sum4-{T}(E2,E1,E3,E4,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 398 : P_sum4-{T}(E2,E1,E2,E1,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 399 : P_sum4-{T}(E2,E1,E4,E3,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 400 : P_sum4-{T}(E4,E3,E2,E1,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 401 : P_sum4-{T}(E2,E3,E3,E0,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 402 : P_sum4-{T}(E4,E2,E1,E2,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 403 : P_sum4-{T}(E2,E3,E1,E4,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 404 : P_sum4-{T}(E3,E2,E1,E2,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 405 : P_sum4-{T}(E2,E3,E0,E3,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 406 : P_sum4-{T}(E0,E2,E1,E2,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 407 : P_sum4-{T}(E2,E3,E4,E1,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 408 : P_sum4-{T}(E2,E2,E1,E2,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 409 : P_sum4-{T}(E2,E3,E2,E2,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 410 : P_sum4-{T}(E1,E2,E1,E2,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 411 : P_sum4-{T}(E2,E4,E4,E2,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 412 : P_sum4-{T}(E4,E4,E1,E2,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 413 : P_sum4-{T}(E2,E4,E2,E4,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 414 : P_sum4-{T}(E3,E4,E1,E2,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 415 : P_sum4-{T}(E2,E4,E1,E3,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 416 : P_sum4-{T}(E2,E1,E1,E2,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 417 : P_sum4-{T}(E2,E4,E3,E1,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 418 : P_sum4-{T}(E4,E3,E1,E2,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 419 : P_sum4-{T}(E2,E4,E0,E0,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 420 : P_sum4-{T}(E2,E2,E2,E0,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 421 : P_sum4-{T}(E2,E0,E0,E4,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 422 : P_sum4-{T}(E4,E0,E2,E0,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 423 : P_sum4-{T}(E2,E0,E3,E3,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 424 : P_sum4-{T}(E4,E4,E2,E0,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 425 : P_sum4-{T}(E2,E0,E4,E0,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 426 : P_sum4-{T}(E3,E4,E2,E0,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 427 : P_sum4-{T}(E2,E2,E4,E4,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 428 : P_sum4-{T}(E0,E4,E2,E0,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 429 : P_sum4-{T}(E0,E1,E3,E4,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 430 : P_sum4-{T}(E4,E3,E2,E0,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 431 : P_sum4-{T}(E0,E1,E4,E3,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 432 : P_sum4-{T}(E3,E3,E2,E0,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 433 : P_sum4-{T}(E0,E3,E3,E0,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 434 : P_sum4-{T}(E4,E2,E0,E0,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 435 : P_sum4-{T}(E0,E3,E1,E4,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 436 : P_sum4-{T}(E0,E4,E0,E0,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 437 : P_sum4-{T}(E0,E3,E0,E3,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 438 : P_sum4-{T}(E3,E3,E0,E0,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 439 : P_sum4-{T}(E0,E3,E4,E1,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 440 : P_sum4-{T}(E1,E3,E0,E0,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 441 : P_sum4-{T}(E0,E3,E2,E2,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 442 : P_sum4-{T}(E0,E3,E0,E0,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 443 : P_sum4-{T}(E0,E4,E4,E2,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 444 : P_sum4-{T}(E2,E3,E0,E0,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 445 : P_sum4-{T}(E0,E4,E2,E4,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 446 : P_sum4-{T}(E4,E3,E0,E0,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 447 : P_sum4-{T}(E0,E4,E1,E3,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 448 : P_sum4-{T}(E4,E0,E0,E0,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 449 : P_sum4-{T}(E0,E4,E3,E1,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 450 : P_sum4-{T}(E3,E0,E0,E0,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 451 : P_sum4-{T}(E0,E0,E3,E3,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 452 : P_sum4-{T}(E4,E1,E0,E0,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 453 : P_sum4-{T}(E0,E0,E4,E0,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 454 : P_sum4-{T}(E4,E2,E3,E1,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 455 : P_sum4-{T}(E0,E0,E0,E4,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 456 : P_sum4-{T}(E4,E3,E3,E1,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 457 : P_sum4-{T}(E0,E2,E4,E4,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 458 : P_sum4-{T}(E3,E3,E3,E1,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 459 : P_sum4-{T}(E4,E0,E3,E4,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 460 : P_sum4-{T}(E0,E3,E3,E1,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 461 : P_sum4-{T}(E4,E0,E4,E3,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 462 : P_sum4-{T}(E2,E3,E3,E1,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 463 : P_sum4-{T}(E4,E4,E2,E2,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 464 : P_sum4-{T}(E4,E0,E3,E1,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 465 : P_sum4-{T}(E4,E4,E3,E0,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 466 : P_sum4-{T}(E3,E0,E3,E1,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 467 : P_sum4-{T}(E4,E4,E1,E4,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 468 : P_sum4-{T}(E4,E1,E3,E1,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 469 : P_sum4-{T}(E4,E4,E0,E3,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 470 : P_sum4-{T}(E4,E2,E1,E3,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 471 : P_sum4-{T}(E4,E4,E4,E1,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 472 : P_sum4-{T}(E4,E3,E1,E3,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 473 : P_sum4-{T}(E4,E1,E4,E4,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 474 : P_sum4-{T}(E3,E3,E1,E3,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 475 : P_sum4-{T}(E4,E1,E3,E2,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 476 : P_sum4-{T}(E0,E3,E1,E3,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 477 : P_sum4-{T}(E4,E1,E2,E3,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 478 : P_sum4-{T}(E2,E3,E1,E3,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 479 : P_sum4-{T}(E4,E3,E3,E3,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 480 : P_sum4-{T}(E4,E0,E1,E3,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 481 : P_sum4-{T}(E4,E3,E4,E0,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 482 : P_sum4-{T}(E3,E0,E1,E3,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 483 : P_sum4-{T}(E4,E3,E0,E4,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 484 : P_sum4-{T}(E4,E1,E1,E3,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 485 : P_sum4-{T}(E4,E2,E4,E2,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 486 : P_sum4-{T}(E2,E4,E2,E3,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 487 : P_sum4-{T}(E4,E2,E2,E4,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 488 : P_sum4-{T}(E4,E4,E2,E3,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 489 : P_sum4-{T}(E3,E0,E3,E4,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 490 : P_sum4-{T}(E3,E4,E2,E3,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 491 : P_sum4-{T}(E3,E0,E4,E3,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 492 : P_sum4-{T}(E1,E4,E2,E3,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 493 : P_sum4-{T}(E3,E4,E2,E2,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 494 : P_sum4-{T}(E0,E4,E2,E3,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 495 : P_sum4-{T}(E3,E4,E3,E0,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 496 : P_sum4-{T}(E4,E3,E2,E3,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 497 : P_sum4-{T}(E3,E4,E1,E4,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 498 : P_sum4-{T}(E3,E3,E2,E3,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 499 : P_sum4-{T}(E3,E4,E0,E3,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 500 : P_sum4-{T}(E0,E3,E2,E3,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 501 : P_sum4-{T}(E3,E4,E4,E1,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 502 : P_sum4-{T}(E4,E0,E2,E3,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 503 : P_sum4-{T}(E3,E1,E4,E4,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 504 : P_sum4-{T}(E3,E0,E2,E3,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 505 : P_sum4-{T}(E3,E3,E3,E3,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 506 : P_sum4-{T}(E1,E4,E3,E2,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 507 : P_sum4-{T}(E3,E3,E4,E0,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 508 : P_sum4-{T}(E0,E4,E3,E2,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 509 : P_sum4-{T}(E3,E3,E0,E4,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 510 : P_sum4-{T}(E2,E4,E3,E2,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 511 : P_sum4-{T}(E2,E0,E3,E4,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 512 : P_sum4-{T}(E4,E4,E3,E2,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 513 : P_sum4-{T}(E2,E0,E4,E3,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 514 : P_sum4-{T}(E3,E4,E3,E2,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 515 : P_sum4-{T}(E2,E4,E3,E0,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 516 : P_sum4-{T}(E4,E3,E3,E2,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 517 : P_sum4-{T}(E2,E4,E1,E4,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 518 : P_sum4-{T}(E3,E3,E3,E2,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 519 : P_sum4-{T}(E2,E4,E0,E3,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 520 : P_sum4-{T}(E0,E3,E3,E2,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 521 : P_sum4-{T}(E2,E4,E4,E1,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 522 : P_sum4-{T}(E4,E0,E3,E2,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 523 : P_sum4-{T}(E2,E4,E2,E2,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 524 : P_sum4-{T}(E3,E0,E3,E2,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 525 : P_sum4-{T}(E2,E1,E4,E4,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 526 : P_sum4-{T}(E4,E2,E4,E1,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 527 : P_sum4-{T}(E2,E3,E0,E4,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 528 : P_sum4-{T}(E3,E2,E4,E1,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 529 : P_sum4-{T}(E2,E3,E3,E3,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 530 : P_sum4-{T}(E4,E1,E4,E1,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 531 : P_sum4-{T}(E2,E3,E4,E0,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 532 : P_sum4-{T}(E3,E1,E4,E1,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 533 : P_sum4-{T}(E0,E0,E3,E4,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 534 : P_sum4-{T}(E0,E4,E4,E1,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 535 : P_sum4-{T}(E0,E0,E4,E3,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 536 : P_sum4-{T}(E3,E0,E4,E1,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 537 : P_sum4-{T}(E0,E4,E3,E0,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 538 : P_sum4-{T}(E1,E0,E4,E1,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 539 : P_sum4-{T}(E0,E4,E1,E4,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 540 : P_sum4-{T}(E0,E0,E4,E1,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 541 : P_sum4-{T}(E0,E4,E0,E3,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 542 : P_sum4-{T}(E2,E0,E4,E1,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 543 : P_sum4-{T}(E0,E4,E2,E2,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 544 : P_sum4-{T}(E4,E0,E4,E1,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 545 : P_sum4-{T}(E0,E1,E4,E4,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 546 : P_sum4-{T}(E4,E2,E0,E3,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 547 : P_sum4-{T}(E0,E3,E3,E3,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 548 : P_sum4-{T}(E3,E2,E0,E3,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 549 : P_sum4-{T}(E0,E3,E4,E0,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 550 : P_sum4-{T}(E4,E1,E0,E3,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 551 : P_sum4-{T}(E0,E3,E0,E4,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 552 : P_sum4-{T}(E3,E1,E0,E3,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 553 : P_sum4-{T}(E1,E3,E4,E2,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 554 : P_sum4-{T}(E4,E0,E0,E3,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 555 : P_sum4-{T}(E1,E3,E2,E4,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 556 : P_sum4-{T}(E3,E0,E0,E3,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 557 : P_sum4-{T}(E1,E4,E4,E4,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 558 : P_sum4-{T}(E1,E0,E0,E3,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 559 : P_sum4-{T}(E1,E0,E2,E2,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 560 : P_sum4-{T}(E0,E0,E0,E3,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 561 : P_sum4-{T}(E1,E0,E3,E0,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 562 : P_sum4-{T}(E2,E0,E0,E3,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 563 : P_sum4-{T}(E1,E0,E1,E4,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 564 : P_sum4-{T}(E3,E2,E1,E4,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 565 : P_sum4-{T}(E1,E1,E3,E3,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 566 : P_sum4-{T}(E4,E2,E1,E4,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 567 : P_sum4-{T}(E1,E1,E4,E0,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 568 : P_sum4-{T}(E4,E1,E1,E4,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 569 : P_sum4-{T}(E1,E1,E0,E4,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 570 : P_sum4-{T}(E3,E1,E1,E4,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 571 : P_sum4-{T}(E4,E2,E3,E4,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 572 : P_sum4-{T}(E2,E0,E1,E4,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 573 : P_sum4-{T}(E4,E2,E4,E3,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 574 : P_sum4-{T}(E4,E0,E1,E4,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 575 : P_sum4-{T}(E4,E3,E4,E2,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 576 : P_sum4-{T}(E3,E0,E1,E4,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 577 : P_sum4-{T}(E4,E3,E2,E4,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 578 : P_sum4-{T}(E0,E0,E1,E4,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 579 : P_sum4-{T}(E4,E4,E4,E4,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 580 : P_sum4-{T}(E4,E2,E3,E0,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 581 : P_sum4-{T}(E4,E0,E2,E2,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 582 : P_sum4-{T}(E3,E2,E3,E0,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 583 : P_sum4-{T}(E4,E0,E3,E0,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 584 : P_sum4-{T}(E4,E1,E3,E0,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 585 : P_sum4-{T}(E4,E1,E3,E3,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 586 : P_sum4-{T}(E3,E1,E3,E0,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 587 : P_sum4-{T}(E4,E1,E4,E0,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 588 : P_sum4-{T}(E0,E0,E3,E0,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 589 : P_sum4-{T}(E4,E1,E0,E4,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 590 : P_sum4-{T}(E2,E0,E3,E0,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 591 : P_sum4-{T}(E3,E2,E3,E4,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 592 : P_sum4-{T}(E3,E0,E3,E0,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 593 : P_sum4-{T}(E3,E2,E4,E3,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 594 : P_sum4-{T}(E0,E3,E2,E4,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 595 : P_sum4-{T}(E3,E3,E4,E2,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 596 : P_sum4-{T}(E2,E3,E2,E4,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 597 : P_sum4-{T}(E3,E3,E2,E4,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 598 : P_sum4-{T}(E4,E0,E2,E4,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 599 : P_sum4-{T}(E3,E4,E4,E4,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 600 : P_sum4-{T}(E3,E0,E2,E4,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 601 : P_sum4-{T}(E3,E0,E2,E2,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 602 : P_sum4-{T}(E0,E0,E2,E4,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 603 : P_sum4-{T}(E3,E1,E3,E3,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 604 : P_sum4-{T}(E4,E1,E2,E4,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 605 : P_sum4-{T}(E3,E1,E4,E0,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 606 : P_sum4-{T}(E3,E1,E2,E4,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 607 : P_sum4-{T}(E3,E1,E0,E4,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 608 : P_sum4-{T}(E0,E3,E4,E2,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 609 : P_sum4-{T}(E2,E2,E3,E4,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 610 : P_sum4-{T}(E2,E3,E4,E2,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 611 : P_sum4-{T}(E2,E2,E4,E3,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 612 : P_sum4-{T}(E4,E0,E4,E2,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 613 : P_sum4-{T}(E2,E4,E4,E4,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 614 : P_sum4-{T}(E3,E0,E4,E2,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 615 : P_sum4-{T}(E2,E0,E2,E2,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 616 : P_sum4-{T}(E0,E0,E4,E2,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 617 : P_sum4-{T}(E2,E1,E4,E0,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 618 : P_sum4-{T}(E4,E1,E4,E2,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 619 : P_sum4-{T}(E2,E1,E0,E4,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 620 : P_sum4-{T}(E3,E1,E4,E2,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 621 : P_sum4-{T}(E2,E1,E3,E3,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 622 : P_sum4-{T}(E2,E2,E0,E4,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 623 : P_sum4-{T}(E0,E2,E3,E4,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 624 : P_sum4-{T}(E1,E2,E0,E4,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 625 : P_sum4-{T}(E0,E2,E4,E3,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 626 : P_sum4-{T}(E4,E2,E0,E4,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 627 : P_sum4-{T}(E0,E4,E4,E4,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 628 : P_sum4-{T}(E3,E2,E0,E4,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 629 : P_sum4-{T}(E0,E0,E2,E2,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 630 : P_sum4-{T}(E0,E2,E0,E4,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 631 : P_sum4-{T}(E0,E1,E3,E3,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 632 : P_sum4-{T}(E0,E4,E0,E4,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 633 : P_sum4-{T}(E0,E1,E4,E0,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 634 : P_sum4-{T}(E2,E4,E0,E4,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 635 : P_sum4-{T}(E0,E1,E0,E4,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 636 : P_sum4-{T}(E1,E4,E0,E4,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 637 : P_sum4-{T}(E1,E4,E3,E3,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 638 : P_sum4-{T}(E4,E4,E0,E4,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 639 : P_sum4-{T}(E1,E4,E4,E0,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 640 : P_sum4-{T}(E3,E4,E0,E4,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 641 : P_sum4-{T}(E1,E2,E2,E2,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 642 : P_sum4-{T}(E3,E2,E4,E0,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 643 : P_sum4-{T}(E1,E0,E4,E4,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 644 : P_sum4-{T}(E0,E2,E4,E0,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 645 : P_sum4-{T}(E1,E3,E3,E4,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 646 : P_sum4-{T}(E2,E2,E4,E0,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 647 : P_sum4-{T}(E1,E3,E4,E3,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 648 : P_sum4-{T}(E1,E2,E4,E0,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 649 : P_sum4-{T}(E4,E4,E3,E3,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 650 : P_sum4-{T}(E4,E2,E4,E0,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 651 : P_sum4-{T}(E4,E4,E4,E0,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 652 : P_sum4-{T}(E3,E4,E4,E0,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 653 : P_sum4-{T}(E4,E2,E2,E2,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 654 : P_sum4-{T}(E0,E4,E4,E0,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 655 : P_sum4-{T}(E4,E0,E4,E4,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 656 : P_sum4-{T}(E2,E4,E4,E0,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 657 : P_sum4-{T}(E4,E3,E3,E4,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 658 : P_sum4-{T}(E4,E2,E3,E3,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 659 : P_sum4-{T}(E4,E3,E4,E3,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 660 : P_sum4-{T}(E3,E2,E3,E3,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 661 : P_sum4-{T}(E3,E4,E3,E3,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 662 : P_sum4-{T}(E0,E2,E3,E3,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 663 : P_sum4-{T}(E3,E2,E2,E2,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 664 : P_sum4-{T}(E2,E2,E3,E3,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 665 : P_sum4-{T}(E3,E0,E4,E4,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 666 : P_sum4-{T}(E1,E2,E3,E3,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 667 : P_sum4-{T}(E3,E3,E3,E4,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 668 : P_sum4-{T}(E0,E4,E3,E3,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 669 : P_sum4-{T}(E3,E3,E4,E3,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 670 : P_sum4-{T}(E2,E4,E3,E3,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 671 : P_sum4-{T}(E4,E4,E4,E3,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 672 : P_sum4-{T}(E2,E2,E2,E2,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 673 : P_sum4-{T}(E3,E4,E4,E3,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 674 : P_sum4-{T}(E2,E0,E4,E4,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 675 : P_sum4-{T}(E0,E4,E4,E3,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 676 : P_sum4-{T}(E2,E3,E3,E4,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 677 : P_sum4-{T}(E2,E4,E4,E3,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 678 : P_sum4-{T}(E2,E3,E4,E3,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 679 : P_sum4-{T}(E1,E4,E4,E3,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 680 : P_sum4-{T}(E0,E2,E2,E2,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 681 : P_sum4-{T}(E0,E3,E4,E3,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 682 : P_sum4-{T}(E0,E0,E4,E4,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 683 : P_sum4-{T}(E4,E4,E3,E4,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 684 : P_sum4-{T}(E0,E3,E3,E4,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 685 : P_sum4-{T}(E3,E4,E3,E4,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 686 : P_sum4-{T}(E1,E3,E4,E4,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 687 : P_sum4-{T}(E0,E4,E3,E4,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 688 : P_sum4-{T}(E1,E1,E2,E2,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 689 : P_sum4-{T}(E2,E4,E3,E4,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 690 : P_sum4-{T}(E1,E4,E3,E4,E4) { 0, 9, 11, 12, 13 }
% 119.10/119.35 691 : P_sum4-{T}(E0,E3,E4,E4,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 692 : P_sum4-{T}(E4,E3,E4,E4,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 693 : P_sum4-{T}(E2,E3,E4,E4,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35 694 : P_sum4-{T}(E4,E1,E2,E2,E0) { 0, 9, 11, 12, 13 }
% 119.10/119.35 695 : P_sum4-{T}(E3,E3,E4,E4,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 696 : P_sum4-{T}(E3,E1,E2,E2,E1) { 0, 9, 11, 12, 13 }
% 119.10/119.35 697 : P_sum4-{T}(E0,E1,E2,E2,E2) { 0, 9, 11, 12, 13 }
% 119.10/119.35 698 : P_sum4-{T}(E2,E1,E2,E2,E3) { 0, 9, 11, 12, 13 }
% 119.10/119.35
% 119.10/119.35
% 119.10/119.35 % SZS output end Model for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 119.10/119.35
% 119.10/119.35 randbase = 1
%------------------------------------------------------------------------------