%------------------------------------------------------------------------------
% File : Geo-III---2018C
% Problem : LCL663+1.020 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : geo -tptp_input -nonempty -inputfile %s
% Computer : n019.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:43 PM UTC 2026
% Result : CounterSatisfiable 12.47s 12.79s
% Output : Model 12.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL663+1.020 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : geo -tptp_input -nonempty -inputfile %s
% 0.10/0.36 % Computer : n019.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 : Fri Sep 4 19:57:08 UTC 2026
% 0.10/0.37 % CPUTime :
% 12.47/12.79 GeoParameters:
% 12.47/12.79
% 12.47/12.79 tptp_input = 1
% 12.47/12.79 tptp_output = 0
% 12.47/12.79 nonempty = 1
% 12.47/12.79 inputfile = /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.47/12.79 includepath = /export/starexec/sandbox2/solver/bin/../../benchmark/
% 12.47/12.79
% 12.47/12.79
% 12.47/12.79 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.47/12.79 % SZS output start Model for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.47/12.79
% 12.47/12.79 Interpretation 14:
% 12.47/12.79 Guesses:
% 12.47/12.79 0 : guesser 2, 1, ( | 1, 0 ), 0, 11s old, 0 lemmas
% 12.47/12.79 1 : guesser 7, 5, ( | 0, 2, 1 ), 1, 11s old, 0 lemmas
% 12.47/12.79 2 : guesser 10, 8, ( | 0, 2, 1 ), 1, 11s old, 0 lemmas
% 12.47/12.79 3 : guesser 12, 10, ( | 1, 2, 0 ), 2, 10s old, 0 lemmas
% 12.47/12.79 4 : guesser 13, 11, ( | 0, 2, 1 ), 2, 10s old, 0 lemmas
% 12.47/12.79 5 : guesser 14, 12, ( | 1, 2, 0 ), 2, 10s old, 0 lemmas
% 12.47/12.79 6 : guesser 15, 13, ( | 0, 2, 1 ), 2, 10s old, 0 lemmas
% 12.47/12.79 7 : guesser 16, 14, ( | 1, 2, 0 ), 2, 10s old, 0 lemmas
% 12.47/12.79 8 : guesser 17, 15, ( | 1, 2, 0 ), 2, 10s old, 0 lemmas
% 12.47/12.79 9 : guesser 18, 16, ( | 1, 2, 0 ), 2, 10s old, 0 lemmas
% 12.47/12.79 10 : guesser 19, 17, ( | 0, 2, 1 ), 2, 10s old, 0 lemmas
% 12.47/12.79 11 : guesser 20, 18, ( | 0, 2, 1 ), 2, 10s old, 0 lemmas
% 12.47/12.79 12 : guesser 21, 19, ( | 0, 2, 1 ), 2, 10s old, 0 lemmas
% 12.47/12.79 13 : guesser 22, 20, ( | 0, 2, 1 ), 2, 10s old, 0 lemmas
% 12.47/12.79 14 : guesser 23, 21, ( | 0, 2, 1 ), 2, 10s old, 0 lemmas
% 12.47/12.79 15 : guesser 24, 22, ( | 0, 2, 1 ), 2, 10s old, 0 lemmas
% 12.47/12.79 16 : guesser 25, 23, ( | 0, 2, 1 ), 2, 10s old, 0 lemmas
% 12.47/12.79 17 : guesser 26, 24, ( | 1, 2, 0 ), 2, 10s old, 0 lemmas
% 12.47/12.79 18 : guesser 27, 25, ( | 0, 2, 1 ), 2, 10s old, 0 lemmas
% 12.47/12.79 19 : guesser 28, 26, ( | 0, 2, 1 ), 2, 10s old, 0 lemmas
% 12.47/12.79 20 : guesser 29, 27, ( | 1, 2, 0 ), 2, 10s old, 0 lemmas
% 12.47/12.79 21 : guesser 32, 30, ( | 0, 2, 1 ), 2, 10s old, 0 lemmas
% 12.47/12.79 22 : guesser 33, 31, ( | 1, 2, 0 ), 2, 10s old, 0 lemmas
% 12.47/12.79 23 : guesser 34, 32, ( | 1, 2, 0 ), 2, 10s old, 0 lemmas
% 12.47/12.79 24 : guesser 35, 33, ( | 1, 2, 0 ), 2, 10s old, 0 lemmas
% 12.47/12.79 25 : guesser 36, 34, ( | 0, 2, 1 ), 2, 10s old, 0 lemmas
% 12.47/12.79 26 : guesser 37, 35, ( | 0, 2, 1 ), 2, 10s old, 0 lemmas
% 12.47/12.79 27 : guesser 38, 36, ( | 1, 2, 0 ), 2, 10s old, 0 lemmas
% 12.47/12.79 28 : guesser 39, 37, ( | 0, 2, 1 ), 2, 10s old, 0 lemmas
% 12.47/12.79 29 : guesser 40, 38, ( | 1, 2, 0 ), 2, 10s old, 0 lemmas
% 12.47/12.79 30 : guesser 41, 39, ( | 1, 2, 0 ), 2, 10s old, 0 lemmas
% 12.47/12.79 31 : guesser 42, 40, ( | 1, 2, 0 ), 2, 10s old, 0 lemmas
% 12.47/12.79 32 : guesser 43, 41, ( | 1, 2, 0 ), 2, 10s old, 0 lemmas
% 12.47/12.79 33 : guesser 44, 42, ( | 0, 2, 1 ), 2, 10s old, 0 lemmas
% 12.47/12.79 34 : guesser 45, 43, ( | 1, 2, 0 ), 2, 10s old, 0 lemmas
% 12.47/12.79 35 : guesser 46, 44, ( | 0, 2, 1 ), 2, 10s old, 0 lemmas
% 12.47/12.79 36 : guesser 47, 45, ( | 1, 2, 0 ), 2, 10s old, 0 lemmas
% 12.47/12.79 37 : guesser 48, 46, ( | 1, 2, 0 ), 2, 10s old, 0 lemmas
% 12.47/12.79 38 : guesser 49, 47, ( | 1, 2, 0 ), 2, 10s old, 0 lemmas
% 12.47/12.79 39 : guesser 50, 48, ( | 0, 2, 1 ), 2, 10s old, 0 lemmas
% 12.47/12.79 40 : guesser 51, 49, ( | 1, 2, 0 ), 2, 10s old, 0 lemmas
% 12.47/12.79 41 : guesser 54, 52, ( | 0, 2, 1 ), 3, 9s old, 0 lemmas
% 12.47/12.79 42 : guesser 55, 53, ( | 1, 2, 0 ), 3, 9s old, 0 lemmas
% 12.47/12.79 43 : guesser 56, 54, ( | 0, 2, 1 ), 3, 9s old, 0 lemmas
% 12.47/12.79 44 : guesser 57, 55, ( | 0, 2, 1 ), 3, 9s old, 0 lemmas
% 12.47/12.79 45 : guesser 58, 56, ( | 1, 2, 0 ), 3, 9s old, 0 lemmas
% 12.47/12.79 46 : guesser 59, 57, ( | 0, 2, 1 ), 3, 9s old, 0 lemmas
% 12.47/12.79 47 : guesser 60, 58, ( | 1, 2, 0 ), 3, 9s old, 0 lemmas
% 12.47/12.79 48 : guesser 61, 59, ( | 0, 2, 1 ), 3, 9s old, 0 lemmas
% 12.47/12.79 49 : guesser 62, 60, ( | 0, 2, 1 ), 3, 9s old, 0 lemmas
% 12.47/12.79 50 : guesser 63, 61, ( | 0, 2, 1 ), 3, 9s old, 0 lemmas
% 12.47/12.79 51 : guesser 64, 62, ( | 0, 2, 1 ), 3, 9s old, 0 lemmas
% 12.47/12.79 52 : guesser 65, 63, ( | 1, 2, 0 ), 3, 9s old, 0 lemmas
% 12.47/12.79 53 : guesser 66, 64, ( | 0, 2, 1 ), 3, 9s old, 0 lemmas
% 12.47/12.79 54 : guesser 67, 65, ( | 0, 2, 1 ), 3, 9s old, 0 lemmas
% 12.47/12.79 55 : guesser 68, 66, ( | 1, 2, 0 ), 3, 9s old, 0 lemmas
% 12.47/12.79 56 : guesser 69, 67, ( | 1, 2, 0 ), 3, 9s old, 0 lemmas
% 12.47/12.79 57 : guesser 70, 68, ( | 1, 2, 0 ), 3, 9s old, 0 lemmas
% 12.47/12.79 58 : guesser 71, 69, ( | 0, 2, 1 ), 3, 9s old, 0 lemmas
% 12.47/12.79 59 : guesser 72, 70, ( | 1, 2, 0 ), 3, 9s old, 0 lemmas
% 12.47/12.79 60 : guesser 73, 71, ( | 1, 2, 0 ), 3, 9s old, 0 lemmas
% 12.47/12.79 61 : guesser 74, 72, ( | 0, 2, 1 ), 3, 9s old, 0 lemmas
% 12.47/12.79 62 : guesser 75, 73, ( | 1, 2, 0 ), 3, 9s old, 0 lemmas
% 12.47/12.79 63 : guesser 76, 74, ( | 0, 2, 1 ), 3, 9s old, 0 lemmas
% 12.47/12.79 64 : guesser 77, 75, ( | 1, 2, 0 ), 3, 9s old, 0 lemmas
% 12.47/12.79 65 : guesser 78, 76, ( | 0, 2, 1 ), 3, 9s old, 0 lemmas
% 12.47/12.79 66 : guesser 79, 77, ( | 0, 2, 1 ), 3, 9s old, 0 lemmas
% 12.47/12.79 67 : guesser 80, 78, ( | 0, 2, 1 ), 3, 9s old, 0 lemmas
% 12.47/12.79 68 : guesser 81, 79, ( | 1, 2, 0 ), 3, 9s old, 0 lemmas
% 12.47/12.79 69 : guesser 82, 80, ( | 1, 2, 0 ), 3, 9s old, 0 lemmas
% 12.47/12.79 70 : guesser 83, 81, ( | 0, 2, 1 ), 3, 9s old, 0 lemmas
% 12.47/12.79 71 : guesser 84, 82, ( | 0, 2, 1 ), 3, 9s old, 0 lemmas
% 12.47/12.79 72 : guesser 85, 83, ( | 0, 2, 1 ), 3, 9s old, 0 lemmas
% 12.47/12.79 73 : guesser 86, 84, ( | 1, 2, 0 ), 3, 9s old, 0 lemmas
% 12.47/12.79 74 : guesser 87, 85, ( | 1, 2, 0 ), 3, 9s old, 0 lemmas
% 12.47/12.79 75 : guesser 88, 86, ( | 0, 2, 1 ), 3, 9s old, 0 lemmas
% 12.47/12.79 76 : guesser 89, 87, ( | 1, 2, 0 ), 3, 9s old, 0 lemmas
% 12.47/12.79 77 : guesser 92, 90, ( | 0, 2, 1 ), 4, 8s old, 0 lemmas
% 12.47/12.79 78 : guesser 93, 91, ( | 0, 2, 1 ), 4, 8s old, 0 lemmas
% 12.47/12.79 79 : guesser 94, 92, ( | 0, 2, 1 ), 4, 8s old, 0 lemmas
% 12.47/12.79 80 : guesser 95, 93, ( | 1, 2, 0 ), 4, 8s old, 0 lemmas
% 12.47/12.79 81 : guesser 96, 94, ( | 1, 2, 0 ), 4, 8s old, 0 lemmas
% 12.47/12.79 82 : guesser 97, 95, ( | 1, 2, 0 ), 4, 8s old, 0 lemmas
% 12.47/12.79 83 : guesser 98, 96, ( | 0, 2, 1 ), 4, 8s old, 0 lemmas
% 12.47/12.79 84 : guesser 99, 97, ( | 0, 2, 1 ), 4, 8s old, 0 lemmas
% 12.47/12.79 85 : guesser 100, 98, ( | 1, 2, 0 ), 4, 8s old, 0 lemmas
% 12.47/12.79 86 : guesser 101, 99, ( | 1, 2, 0 ), 4, 8s old, 0 lemmas
% 12.47/12.79 87 : guesser 102, 100, ( | 0, 2, 1 ), 4, 8s old, 0 lemmas
% 12.47/12.79 88 : guesser 103, 101, ( | 0, 2, 1 ), 4, 8s old, 0 lemmas
% 12.47/12.79 89 : guesser 104, 102, ( | 1, 2, 0 ), 4, 8s old, 0 lemmas
% 12.47/12.79 90 : guesser 105, 103, ( | 0, 2, 1 ), 4, 8s old, 0 lemmas
% 12.47/12.79 91 : guesser 106, 104, ( | 0, 2, 1 ), 4, 8s old, 0 lemmas
% 12.47/12.79 92 : guesser 107, 105, ( | 0, 2, 1 ), 4, 8s old, 0 lemmas
% 12.47/12.79 93 : guesser 108, 106, ( | 1, 2, 0 ), 4, 8s old, 0 lemmas
% 12.47/12.79 94 : guesser 109, 107, ( | 1, 2, 0 ), 4, 8s old, 0 lemmas
% 12.47/12.79 95 : guesser 110, 108, ( | 1, 2, 0 ), 4, 8s old, 0 lemmas
% 12.47/12.79 96 : guesser 111, 109, ( | 1, 2, 0 ), 4, 8s old, 0 lemmas
% 12.47/12.79 97 : guesser 112, 110, ( | 1, 2, 0 ), 4, 8s old, 0 lemmas
% 12.47/12.79 98 : guesser 113, 111, ( | 1, 2, 0 ), 4, 8s old, 0 lemmas
% 12.47/12.79 99 : guesser 114, 112, ( | 1, 2, 0 ), 4, 8s old, 0 lemmas
% 12.47/12.79 100 : guesser 115, 113, ( | 1, 2, 0 ), 4, 8s old, 0 lemmas
% 12.47/12.79 101 : guesser 116, 114, ( | 0, 2, 1 ), 4, 8s old, 0 lemmas
% 12.47/12.79 102 : guesser 117, 115, ( | 0, 2, 1 ), 4, 8s old, 0 lemmas
% 12.47/12.79 103 : guesser 118, 116, ( | 1, 2, 0 ), 4, 8s old, 0 lemmas
% 12.47/12.79 104 : guesser 119, 117, ( | 0, 2, 1 ), 4, 8s old, 0 lemmas
% 12.47/12.79 105 : guesser 120, 118, ( | 1, 2, 0 ), 4, 8s old, 0 lemmas
% 12.47/12.79 106 : guesser 121, 119, ( | 1, 2, 0 ), 4, 8s old, 0 lemmas
% 12.47/12.79 107 : guesser 122, 120, ( | 1, 2, 0 ), 4, 8s old, 0 lemmas
% 12.47/12.79 108 : guesser 123, 121, ( | 1, 2, 0 ), 4, 8s old, 0 lemmas
% 12.47/12.79 109 : guesser 124, 122, ( | 0, 2, 1 ), 4, 8s old, 0 lemmas
% 12.47/12.79 110 : guesser 125, 123, ( | 1, 2, 0 ), 4, 8s old, 0 lemmas
% 12.47/12.79 111 : guesser 126, 124, ( | 0, 2, 1 ), 4, 8s old, 0 lemmas
% 12.47/12.79 112 : guesser 129, 127, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 113 : guesser 130, 128, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 114 : guesser 131, 129, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 115 : guesser 132, 130, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 116 : guesser 133, 131, ( | 0, 2, 1 ), 5, 7s old, 0 lemmas
% 12.47/12.79 117 : guesser 134, 132, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 118 : guesser 135, 133, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 119 : guesser 136, 134, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 120 : guesser 137, 135, ( | 0, 2, 1 ), 5, 7s old, 0 lemmas
% 12.47/12.79 121 : guesser 138, 136, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 122 : guesser 139, 137, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 123 : guesser 140, 138, ( | 0, 2, 1 ), 5, 7s old, 0 lemmas
% 12.47/12.79 124 : guesser 141, 139, ( | 0, 2, 1 ), 5, 7s old, 0 lemmas
% 12.47/12.79 125 : guesser 142, 140, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 126 : guesser 143, 141, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 127 : guesser 144, 142, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 128 : guesser 145, 143, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 129 : guesser 146, 144, ( | 0, 2, 1 ), 5, 7s old, 0 lemmas
% 12.47/12.79 130 : guesser 147, 145, ( | 0, 2, 1 ), 5, 7s old, 0 lemmas
% 12.47/12.79 131 : guesser 148, 146, ( | 0, 2, 1 ), 5, 7s old, 0 lemmas
% 12.47/12.79 132 : guesser 149, 147, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 133 : guesser 150, 148, ( | 0, 2, 1 ), 5, 7s old, 0 lemmas
% 12.47/12.79 134 : guesser 151, 149, ( | 0, 2, 1 ), 5, 7s old, 0 lemmas
% 12.47/12.79 135 : guesser 152, 150, ( | 0, 2, 1 ), 5, 7s old, 0 lemmas
% 12.47/12.79 136 : guesser 153, 151, ( | 0, 2, 1 ), 5, 7s old, 0 lemmas
% 12.47/12.79 137 : guesser 154, 152, ( | 0, 2, 1 ), 5, 7s old, 0 lemmas
% 12.47/12.79 138 : guesser 155, 153, ( | 0, 2, 1 ), 5, 7s old, 0 lemmas
% 12.47/12.79 139 : guesser 156, 154, ( | 0, 2, 1 ), 5, 7s old, 0 lemmas
% 12.47/12.79 140 : guesser 157, 155, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 141 : guesser 158, 156, ( | 0, 2, 1 ), 5, 7s old, 0 lemmas
% 12.47/12.79 142 : guesser 159, 157, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 143 : guesser 160, 158, ( | 0, 2, 1 ), 5, 7s old, 0 lemmas
% 12.47/12.79 144 : guesser 161, 159, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 145 : guesser 162, 160, ( | 0, 2, 1 ), 5, 7s old, 0 lemmas
% 12.47/12.79 146 : guesser 163, 161, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 147 : guesser 164, 162, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 148 : guesser 165, 163, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 149 : guesser 166, 164, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 150 : guesser 167, 165, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 151 : guesser 168, 166, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 152 : guesser 169, 167, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 153 : guesser 170, 168, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 154 : guesser 171, 169, ( | 0, 2, 1 ), 5, 7s old, 0 lemmas
% 12.47/12.79 155 : guesser 172, 170, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 156 : guesser 173, 171, ( | 0, 2, 1 ), 5, 7s old, 0 lemmas
% 12.47/12.79 157 : guesser 174, 172, ( | 1, 2, 0 ), 5, 7s old, 0 lemmas
% 12.47/12.79 158 : guesser 175, 173, ( | 0, 2, 1 ), 5, 7s old, 0 lemmas
% 12.47/12.79 159 : guesser 176, 174, ( | 0, 2, 1 ), 5, 7s old, 0 lemmas
% 12.47/12.79 160 : guesser 177, 175, ( | 0, 2, 1 ), 5, 6s old, 0 lemmas
% 12.47/12.79 161 : guesser 178, 176, ( | 0, 2, 1 ), 5, 6s old, 0 lemmas
% 12.47/12.79 162 : guesser 179, 177, ( | 0, 2, 1 ), 5, 6s old, 0 lemmas
% 12.47/12.79 163 : guesser 180, 178, ( | 0, 2, 1 ), 5, 6s old, 0 lemmas
% 12.47/12.79 164 : guesser 181, 179, ( | 1, 2, 0 ), 5, 6s old, 0 lemmas
% 12.47/12.79 165 : guesser 182, 180, ( | 0, 2, 1 ), 5, 6s old, 0 lemmas
% 12.47/12.79 166 : guesser 183, 181, ( | 0, 2, 1 ), 5, 6s old, 0 lemmas
% 12.47/12.79 167 : guesser 184, 182, ( | 1, 2, 0 ), 5, 6s old, 0 lemmas
% 12.47/12.79 168 : guesser 185, 183, ( | 1, 2, 0 ), 5, 6s old, 0 lemmas
% 12.47/12.79 169 : guesser 186, 184, ( | 1, 2, 0 ), 5, 6s old, 0 lemmas
% 12.47/12.79 170 : guesser 187, 185, ( | 0, 2, 1 ), 5, 6s old, 0 lemmas
% 12.47/12.79 171 : guesser 188, 186, ( | 0, 1 ), 5, 6s old, 0 lemmas
% 12.47/12.79 172 : guesser 189, 187, ( | 0, 1 ), 5, 6s old, 0 lemmas
% 12.47/12.79 173 : guesser 190, 188, ( | 1, 2, 0 ), 5, 6s old, 0 lemmas
% 12.47/12.79 174 : guesser 193, 191, ( | 0, 2, 1 ), 6, 6s old, 0 lemmas
% 12.47/12.79 175 : guesser 194, 192, ( | 0, 2, 1 ), 6, 6s old, 0 lemmas
% 12.47/12.79 176 : guesser 195, 193, ( | 0, 2, 1 ), 6, 6s old, 0 lemmas
% 12.47/12.79 177 : guesser 196, 194, ( | 1, 2, 0 ), 6, 6s old, 0 lemmas
% 12.47/12.79 178 : guesser 197, 195, ( | 1, 2, 0 ), 6, 6s old, 0 lemmas
% 12.47/12.79 179 : guesser 198, 196, ( | 1, 2, 0 ), 6, 6s old, 0 lemmas
% 12.47/12.79 180 : guesser 199, 197, ( | 0, 2, 1 ), 6, 6s old, 0 lemmas
% 12.47/12.79 181 : guesser 200, 198, ( | 1, 2, 0 ), 6, 6s old, 0 lemmas
% 12.47/12.79 182 : guesser 201, 199, ( | 0, 2, 1 ), 6, 6s old, 0 lemmas
% 12.47/12.79 183 : guesser 202, 200, ( | 0, 2, 1 ), 6, 6s old, 0 lemmas
% 12.47/12.79 184 : guesser 203, 201, ( | 0, 2, 1 ), 6, 6s old, 0 lemmas
% 12.47/12.79 185 : guesser 204, 202, ( | 1, 2, 0 ), 6, 6s old, 0 lemmas
% 12.47/12.79 186 : guesser 205, 203, ( | 1, 2, 0 ), 6, 6s old, 0 lemmas
% 12.47/12.79 187 : guesser 206, 204, ( | 1, 2, 0 ), 6, 6s old, 0 lemmas
% 12.47/12.79 188 : guesser 207, 205, ( | 1, 2, 0 ), 6, 6s old, 0 lemmas
% 12.47/12.79 189 : guesser 208, 206, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 190 : guesser 209, 207, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 191 : guesser 210, 208, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 192 : guesser 211, 209, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 193 : guesser 212, 210, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 194 : guesser 213, 211, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 195 : guesser 214, 212, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 196 : guesser 215, 213, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 197 : guesser 216, 214, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 198 : guesser 217, 215, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 199 : guesser 218, 216, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 200 : guesser 219, 217, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 201 : guesser 220, 218, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 202 : guesser 221, 219, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 203 : guesser 222, 220, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 204 : guesser 223, 221, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 205 : guesser 224, 222, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 206 : guesser 225, 223, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 207 : guesser 226, 224, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 208 : guesser 227, 225, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 209 : guesser 228, 226, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 210 : guesser 229, 227, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 211 : guesser 230, 228, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 212 : guesser 231, 229, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 213 : guesser 232, 230, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 214 : guesser 233, 231, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 215 : guesser 234, 232, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 216 : guesser 235, 233, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 217 : guesser 236, 234, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 218 : guesser 237, 235, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 219 : guesser 238, 236, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 220 : guesser 239, 237, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 221 : guesser 240, 238, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 222 : guesser 241, 239, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 223 : guesser 242, 240, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 224 : guesser 243, 241, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 225 : guesser 244, 242, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 226 : guesser 245, 243, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 227 : guesser 246, 244, ( | 0, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 228 : guesser 247, 245, ( | 0, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 229 : guesser 248, 246, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 230 : guesser 249, 247, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 231 : guesser 250, 248, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 232 : guesser 251, 249, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 233 : guesser 252, 250, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 234 : guesser 253, 251, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 235 : guesser 254, 252, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 236 : guesser 255, 253, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 237 : guesser 256, 254, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 238 : guesser 257, 255, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 239 : guesser 258, 256, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 240 : guesser 259, 257, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 241 : guesser 260, 258, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 242 : guesser 261, 259, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 243 : guesser 262, 260, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 244 : guesser 263, 261, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 245 : guesser 264, 262, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 246 : guesser 265, 263, ( | 1, 2, 0 ), 6, 5s old, 0 lemmas
% 12.47/12.79 247 : guesser 266, 264, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 248 : guesser 267, 265, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 249 : guesser 268, 266, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 250 : guesser 269, 267, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 251 : guesser 270, 268, ( | 0, 2, 1 ), 6, 5s old, 0 lemmas
% 12.47/12.79 252 : guesser 271, 269, ( | 1, 2, 0 ), 6, 4s old, 0 lemmas
% 12.47/12.79 253 : guesser 272, 270, ( | 0, 1 ), 6, 4s old, 0 lemmas
% 12.47/12.79 254 : guesser 273, 271, ( | 0, 2, 1 ), 6, 4s old, 0 lemmas
% 12.47/12.79 255 : guesser 276, 274, ( | 0, 1 ), 7, 4s old, 0 lemmas
% 12.47/12.79 256 : guesser 277, 275, ( | 0, 2, 1 ), 7, 4s old, 0 lemmas
% 12.47/12.79 257 : guesser 278, 276, ( | 0, 2, 1 ), 7, 4s old, 0 lemmas
% 12.47/12.79 258 : guesser 279, 277, ( | 1, 2, 0 ), 7, 4s old, 0 lemmas
% 12.47/12.79 259 : guesser 280, 278, ( | 1, 2, 0 ), 7, 4s old, 0 lemmas
% 12.47/12.79 260 : guesser 281, 279, ( | 1, 2, 0 ), 7, 4s old, 0 lemmas
% 12.47/12.79 261 : guesser 282, 280, ( | 0, 2, 1 ), 7, 4s old, 0 lemmas
% 12.47/12.79 262 : guesser 283, 281, ( | 0, 2, 1 ), 7, 4s old, 0 lemmas
% 12.47/12.79 263 : guesser 284, 282, ( | 1, 2, 0 ), 7, 4s old, 0 lemmas
% 12.47/12.79 264 : guesser 285, 283, ( | 0, 2, 1 ), 7, 4s old, 0 lemmas
% 12.47/12.79 265 : guesser 286, 284, ( | 1, 2, 0 ), 7, 4s old, 0 lemmas
% 12.47/12.79 266 : guesser 287, 285, ( | 1, 2, 0 ), 7, 4s old, 0 lemmas
% 12.47/12.79 267 : guesser 288, 286, ( | 0, 2, 1 ), 7, 4s old, 0 lemmas
% 12.47/12.79 268 : guesser 289, 287, ( | 0, 2, 1 ), 7, 4s old, 0 lemmas
% 12.47/12.79 269 : guesser 290, 288, ( | 1, 2, 0 ), 7, 4s old, 0 lemmas
% 12.47/12.79 270 : guesser 291, 289, ( | 1, 2, 0 ), 7, 4s old, 0 lemmas
% 12.47/12.79 271 : guesser 292, 290, ( | 1, 2, 0 ), 7, 4s old, 0 lemmas
% 12.47/12.79 272 : guesser 293, 291, ( | 1, 2, 0 ), 7, 4s old, 0 lemmas
% 12.47/12.79 273 : guesser 294, 292, ( | 0, 2, 1 ), 7, 4s old, 0 lemmas
% 12.47/12.79 274 : guesser 295, 293, ( | 1, 2, 0 ), 7, 4s old, 0 lemmas
% 12.47/12.79 275 : guesser 296, 294, ( | 1, 2, 0 ), 7, 4s old, 0 lemmas
% 12.47/12.79 276 : guesser 297, 295, ( | 1, 2, 0 ), 7, 4s old, 0 lemmas
% 12.47/12.79 277 : guesser 298, 296, ( | 0, 2, 1 ), 7, 4s old, 0 lemmas
% 12.47/12.79 278 : guesser 299, 297, ( | 0, 2, 1 ), 7, 4s old, 0 lemmas
% 12.47/12.79 279 : guesser 300, 298, ( | 1, 2, 0 ), 7, 4s old, 0 lemmas
% 12.47/12.79 280 : guesser 301, 299, ( | 0, 2, 1 ), 7, 4s old, 0 lemmas
% 12.47/12.79 281 : guesser 302, 300, ( | 1, 2, 0 ), 7, 4s old, 0 lemmas
% 12.47/12.79 282 : guesser 303, 301, ( | 1, 2, 0 ), 7, 4s old, 0 lemmas
% 12.47/12.79 283 : guesser 304, 302, ( | 0, 2, 1 ), 7, 4s old, 0 lemmas
% 12.47/12.79 284 : guesser 305, 303, ( | 1, 2, 0 ), 7, 4s old, 0 lemmas
% 12.47/12.79 285 : guesser 306, 304, ( | 1, 2, 0 ), 7, 4s old, 0 lemmas
% 12.47/12.79 286 : guesser 307, 305, ( | 0, 2, 1 ), 7, 4s old, 0 lemmas
% 12.47/12.79 287 : guesser 308, 306, ( | 1, 2, 0 ), 7, 4s old, 0 lemmas
% 12.47/12.79 288 : guesser 309, 307, ( | 1, 2, 0 ), 7, 3s old, 0 lemmas
% 12.47/12.79 289 : guesser 310, 308, ( | 1, 2, 0 ), 7, 3s old, 0 lemmas
% 12.47/12.79 290 : guesser 311, 309, ( | 1, 2, 0 ), 7, 3s old, 0 lemmas
% 12.47/12.79 291 : guesser 312, 310, ( | 0, 2, 1 ), 7, 3s old, 0 lemmas
% 12.47/12.79 292 : guesser 313, 311, ( | 0, 2, 1 ), 7, 3s old, 0 lemmas
% 12.47/12.79 293 : guesser 314, 312, ( | 0, 2, 1 ), 7, 3s old, 0 lemmas
% 12.47/12.79 294 : guesser 315, 313, ( | 0, 2, 1 ), 7, 3s old, 0 lemmas
% 12.47/12.79 295 : guesser 316, 314, ( | 0, 2, 1 ), 7, 3s old, 0 lemmas
% 12.47/12.79 296 : guesser 317, 315, ( | 0, 1 ), 7, 3s old, 0 lemmas
% 12.47/12.79 297 : guesser 318, 316, ( | 0, 2, 1 ), 7, 3s old, 0 lemmas
% 12.47/12.79 298 : guesser 319, 317, ( | 0, 1 ), 7, 3s old, 0 lemmas
% 12.47/12.79 299 : guesser 320, 318, ( | 0, 2, 1 ), 7, 3s old, 0 lemmas
% 12.47/12.79 300 : guesser 323, 321, ( | 0, 2, 1 ), 8, 3s old, 0 lemmas
% 12.47/12.79 301 : guesser 324, 322, ( | 1, 2, 0 ), 8, 3s old, 0 lemmas
% 12.47/12.79 302 : guesser 325, 323, ( | 1, 2, 0 ), 8, 3s old, 0 lemmas
% 12.47/12.79 303 : guesser 326, 324, ( | 0, 2, 1 ), 8, 3s old, 0 lemmas
% 12.47/12.79 304 : guesser 327, 325, ( | 1, 2, 0 ), 8, 3s old, 0 lemmas
% 12.47/12.79 305 : guesser 328, 326, ( | 1, 2, 0 ), 8, 3s old, 0 lemmas
% 12.47/12.79 306 : guesser 329, 327, ( | 1, 2, 0 ), 8, 3s old, 0 lemmas
% 12.47/12.79 307 : guesser 330, 328, ( | 1, 2, 0 ), 8, 3s old, 0 lemmas
% 12.47/12.79 308 : guesser 331, 329, ( | 1, 2, 0 ), 8, 3s old, 0 lemmas
% 12.47/12.79 309 : guesser 332, 330, ( | 0, 2, 1 ), 8, 3s old, 0 lemmas
% 12.47/12.79 310 : guesser 333, 331, ( | 0, 2, 1 ), 8, 3s old, 0 lemmas
% 12.47/12.79 311 : guesser 334, 332, ( | 0, 2, 1 ), 8, 3s old, 0 lemmas
% 12.47/12.79 312 : guesser 335, 333, ( | 1, 2, 0 ), 8, 3s old, 0 lemmas
% 12.47/12.79 313 : guesser 336, 334, ( | 0, 2, 1 ), 8, 3s old, 0 lemmas
% 12.47/12.79 314 : guesser 337, 335, ( | 1, 2, 0 ), 8, 3s old, 0 lemmas
% 12.47/12.79 315 : guesser 338, 336, ( | 1, 2, 0 ), 8, 3s old, 0 lemmas
% 12.47/12.79 316 : guesser 339, 337, ( | 1, 2, 0 ), 8, 3s old, 0 lemmas
% 12.47/12.79 317 : guesser 340, 338, ( | 1, 2, 0 ), 8, 3s old, 0 lemmas
% 12.47/12.79 318 : guesser 341, 339, ( | 0, 2, 1 ), 8, 3s old, 0 lemmas
% 12.47/12.79 319 : guesser 342, 340, ( | 0, 2, 1 ), 8, 3s old, 0 lemmas
% 12.47/12.79 320 : guesser 345, 343, ( | 0, 2, 1 ), 9, 2s old, 0 lemmas
% 12.47/12.79 321 : guesser 346, 344, ( | 0, 2, 1 ), 9, 2s old, 0 lemmas
% 12.47/12.79 322 : guesser 347, 345, ( | 1, 2, 0 ), 9, 2s old, 0 lemmas
% 12.47/12.79 323 : guesser 348, 346, ( | 0, 2, 1 ), 9, 2s old, 0 lemmas
% 12.47/12.79 324 : guesser 349, 347, ( | 1, 2, 0 ), 9, 2s old, 0 lemmas
% 12.47/12.79 325 : guesser 350, 348, ( | 1, 2, 0 ), 9, 2s old, 0 lemmas
% 12.47/12.79 326 : guesser 351, 349, ( | 0, 2, 1 ), 9, 2s old, 0 lemmas
% 12.47/12.79 327 : guesser 352, 350, ( | 0, 2, 1 ), 9, 2s old, 0 lemmas
% 12.47/12.79 328 : guesser 353, 351, ( | 0, 2, 1 ), 9, 2s old, 0 lemmas
% 12.47/12.79 329 : guesser 354, 352, ( | 0, 2, 1 ), 9, 2s old, 0 lemmas
% 12.47/12.79 330 : guesser 355, 353, ( | 1, 2, 0 ), 9, 2s old, 0 lemmas
% 12.47/12.79 331 : guesser 356, 354, ( | 0, 2, 1 ), 9, 2s old, 0 lemmas
% 12.47/12.79 332 : guesser 357, 355, ( | 0, 2, 1 ), 9, 2s old, 0 lemmas
% 12.47/12.79 333 : guesser 358, 356, ( | 1, 2, 0 ), 9, 2s old, 0 lemmas
% 12.47/12.79 334 : guesser 359, 357, ( | 0, 2, 1 ), 9, 2s old, 0 lemmas
% 12.47/12.79 335 : guesser 362, 360, ( | 0, 2, 1 ), 10, 2s old, 0 lemmas
% 12.47/12.79 336 : guesser 363, 361, ( | 0, 2, 1 ), 10, 2s old, 0 lemmas
% 12.47/12.79 337 : guesser 364, 362, ( | 1, 2, 0 ), 10, 2s old, 0 lemmas
% 12.47/12.79 338 : guesser 365, 363, ( | 0, 2, 1 ), 10, 2s old, 0 lemmas
% 12.47/12.79 339 : guesser 366, 364, ( | 1, 2, 0 ), 10, 2s old, 0 lemmas
% 12.47/12.79 340 : guesser 367, 365, ( | 0, 2, 1 ), 10, 2s old, 0 lemmas
% 12.47/12.79 341 : guesser 368, 366, ( | 0, 2, 1 ), 10, 2s old, 0 lemmas
% 12.47/12.79 342 : guesser 369, 367, ( | 0, 2, 1 ), 10, 2s old, 0 lemmas
% 12.47/12.79 343 : guesser 370, 368, ( | 0, 2, 1 ), 10, 2s old, 0 lemmas
% 12.47/12.79 344 : guesser 371, 369, ( | 1, 2, 0 ), 10, 2s old, 0 lemmas
% 12.47/12.79 345 : guesser 372, 370, ( | 1, 2, 0 ), 10, 2s old, 0 lemmas
% 12.47/12.79 346 : guesser 373, 371, ( | 0, 2, 1 ), 10, 2s old, 0 lemmas
% 12.47/12.79 347 : guesser 374, 372, ( | 1, 2, 0 ), 10, 1s old, 0 lemmas
% 12.47/12.79 348 : guesser 375, 373, ( | 1, 2, 0 ), 10, 1s old, 0 lemmas
% 12.47/12.79 349 : guesser 376, 374, ( | 0, 2, 1 ), 10, 1s old, 0 lemmas
% 12.47/12.79 350 : guesser 379, 377, ( | 1, 2, 0 ), 11, 1s old, 0 lemmas
% 12.47/12.79 351 : guesser 380, 378, ( | 1, 2, 0 ), 11, 1s old, 0 lemmas
% 12.47/12.79 352 : guesser 381, 379, ( | 1, 2, 0 ), 11, 1s old, 0 lemmas
% 12.47/12.79 353 : guesser 382, 380, ( | 1, 2, 0 ), 11, 1s old, 0 lemmas
% 12.47/12.79 354 : guesser 383, 381, ( | 1, 2, 0 ), 11, 1s old, 0 lemmas
% 12.47/12.79 355 : guesser 384, 382, ( | 0, 2, 1 ), 11, 1s old, 0 lemmas
% 12.47/12.79 356 : guesser 385, 383, ( | 1, 2, 0 ), 11, 1s old, 0 lemmas
% 12.47/12.79 357 : guesser 386, 384, ( | 1, 2, 0 ), 11, 1s old, 0 lemmas
% 12.47/12.79 358 : guesser 387, 385, ( | 1, 2, 0 ), 11, 1s old, 0 lemmas
% 12.47/12.79 359 : guesser 388, 386, ( | 1, 2, 0 ), 11, 1s old, 0 lemmas
% 12.47/12.79 360 : guesser 389, 387, ( | 0, 2, 1 ), 11, 1s old, 0 lemmas
% 12.47/12.79 361 : guesser 390, 388, ( | 1, 2, 0 ), 11, 1s old, 0 lemmas
% 12.47/12.79 362 : guesser 393, 391, ( | 1, 2, 0 ), 12, 1s old, 0 lemmas
% 12.47/12.79 363 : guesser 394, 392, ( | 0, 2, 1 ), 12, 1s old, 0 lemmas
% 12.47/12.79 364 : guesser 395, 393, ( | 1, 2, 0 ), 12, 1s old, 0 lemmas
% 12.47/12.79 365 : guesser 396, 394, ( | 1, 2, 0 ), 12, 0s old, 0 lemmas
% 12.47/12.79 366 : guesser 397, 395, ( | 1, 2, 0 ), 12, 0s old, 0 lemmas
% 12.47/12.79 367 : guesser 398, 396, ( | 1, 2, 0 ), 12, 0s old, 0 lemmas
% 12.47/12.79 368 : guesser 399, 397, ( | 0, 2, 1 ), 12, 0s old, 0 lemmas
% 12.47/12.79 369 : guesser 400, 398, ( | 0, 2, 1 ), 12, 0s old, 0 lemmas
% 12.47/12.79 370 : guesser 401, 399, ( | 1, 2, 0 ), 12, 0s old, 0 lemmas
% 12.47/12.79 371 : guesser 404, 402, ( | 0, 2, 1 ), 13, 0s old, 0 lemmas
% 12.47/12.79 372 : guesser 405, 403, ( | 1, 2, 0 ), 13, 0s old, 0 lemmas
% 12.47/12.79 373 : guesser 406, 404, ( | 1, 2, 0 ), 13, 0s old, 0 lemmas
% 12.47/12.79 374 : guesser 407, 405, ( | 1, 2, 0 ), 13, 0s old, 0 lemmas
% 12.47/12.79 375 : guesser 408, 406, ( | 1, 2, 0 ), 13, 0s old, 0 lemmas
% 12.47/12.79 376 : guesser 409, 407, ( | 1, 2, 0 ), 13, 0s old, 0 lemmas
% 12.47/12.79 377 : guesser 410, 408, ( | 0, 2, 1 ), 13, 0s old, 0 lemmas
% 12.47/12.79 378 : guesser 411, 409, ( | 0, 2, 1 ), 13, 0s old, 0 lemmas
% 12.47/12.79 379 : guesser 412, 410, ( | 1, 2, 0 ), 13, 0s old, 0 lemmas
% 12.47/12.79 380 : guesser 415, 413, ( | 1, 2, 0 ), 14, 0s old, 0 lemmas
% 12.47/12.79 381 : guesser 416, 414, ( | 1, 2, 0 ), 14, 0s old, 0 lemmas
% 12.47/12.79 382 : guesser 417, 415, ( | 1, 2, 0 ), 14, 0s old, 0 lemmas
% 12.47/12.79 383 : guesser 418, 416, ( | 0, 2, 1 ), 14, 0s old, 0 lemmas
% 12.47/12.79 384 : guesser 419, 417, ( | 1, 2, 0 ), 14, 0s old, 0 lemmas
% 12.47/12.79 385 : guesser 420, 418, ( | 1, 2, 0 ), 14, 0s old, 0 lemmas
% 12.47/12.79 386 : guesser 421, 419, ( | 0, 2, 1 ), 14, 0s old, 0 lemmas
% 12.47/12.79 387 : guesser 422, 420, ( | 0, 1 ), 14, 0s old, 0 lemmas
% 12.47/12.79 388 : guesser 423, 421, ( | 0, 1 ), 14, 0s old, 0 lemmas
% 12.47/12.79 389 : guesser 424, 422, ( | 1, 2, 0 ), 14, 0s old, 0 lemmas
% 12.47/12.79 390 : guesser 425, 423, ( | 0, 2, 1 ), 14, 0s old, 0 lemmas
% 12.47/12.79
% 12.47/12.79 Elements:
% 12.47/12.79 { E0, E1 }
% 12.47/12.79
% 12.47/12.79 Atoms:
% 12.47/12.79 0 : #-{T} E0 { }
% 12.47/12.79 1 : r1-{T}(E0,E0) { }
% 12.47/12.79 2 : #-{T} E1 { 0 }
% 12.47/12.79 3 : pppp191-{T}(E1) { 0 }
% 12.47/12.79 4 : r1-{T}(E1,E1) { 0 }
% 12.47/12.79 5 : pppp190-{T}(E1) { 0 }
% 12.47/12.79 6 : pppp192-{T}(E1) { 0 }
% 12.47/12.79 7 : pppp189-{T}(E0,E1) { 0, 1 }
% 12.47/12.79 8 : r1-{T}(E1,E0) { 0, 1 }
% 12.47/12.79 9 : pppp192-{T}(E0) { 0, 1 }
% 12.47/12.79 10 : pppp188-{T}(E0,E1) { 0, 2 }
% 12.47/12.79 11 : pppp193-{T}(E0) { 0, 1, 2 }
% 12.47/12.79 12 : pppp186-{T}(E1,E1) { 0, 3 }
% 12.47/12.79 13 : pppp183-{T}(E0,E1) { 0, 4 }
% 12.47/12.79 14 : pppp179-{T}(E1,E1) { 0, 5 }
% 12.47/12.79 15 : pppp174-{T}(E0,E1) { 0, 6 }
% 12.47/12.79 16 : pppp168-{T}(E1,E1) { 0, 7 }
% 12.47/12.79 17 : pppp161-{T}(E1,E1) { 0, 8 }
% 12.47/12.79 18 : pppp153-{T}(E1,E1) { 0, 9 }
% 12.47/12.79 19 : pppp144-{T}(E0,E1) { 0, 10 }
% 12.47/12.79 20 : pppp134-{T}(E1,E0) { 0, 11 }
% 12.47/12.79 21 : pppp123-{T}(E0,E1) { 0, 12 }
% 12.47/12.79 22 : pppp111-{T}(E1,E0) { 0, 13 }
% 12.47/12.79 23 : pppp98-{T}(E0,E1) { 0, 14 }
% 12.47/12.79 24 : pppp84-{T}(E1,E0) { 0, 15 }
% 12.47/12.79 25 : pppp69-{T}(E0,E1) { 0, 16 }
% 12.47/12.79 26 : pppp53-{T}(E1,E1) { 0, 17 }
% 12.47/12.79 27 : pppp36-{T}(E0,E1) { 0, 18 }
% 12.47/12.79 28 : pppp18-{T}(E1,E0) { 0, 19 }
% 12.47/12.79 29 : pppp189-{T}(E1,E0) { 0, 1, 20 }
% 12.47/12.79 30 : r1-{T}(E0,E1) { 0, 1, 20 }
% 12.47/12.79 31 : pppp193-{T}(E1) { 0, 1, 2, 20 }
% 12.47/12.79 32 : pppp188-{T}(E0,E0) { 0, 1, 21 }
% 12.47/12.79 33 : pppp186-{T}(E0,E1) { 0, 1, 22 }
% 12.47/12.79 34 : pppp183-{T}(E1,E0) { 0, 1, 23 }
% 12.47/12.79 35 : pppp179-{T}(E0,E1) { 0, 1, 24 }
% 12.47/12.79 36 : pppp174-{T}(E0,E0) { 0, 1, 25 }
% 12.47/12.79 37 : pppp168-{T}(E0,E0) { 0, 1, 26 }
% 12.47/12.79 38 : pppp161-{T}(E1,E0) { 0, 1, 27 }
% 12.47/12.79 39 : pppp153-{T}(E0,E0) { 0, 1, 28 }
% 12.47/12.79 40 : pppp144-{T}(E1,E0) { 0, 1, 29 }
% 12.47/12.79 41 : pppp134-{T}(E0,E1) { 0, 1, 30 }
% 12.47/12.79 42 : pppp123-{T}(E1,E0) { 0, 1, 31 }
% 12.47/12.79 43 : pppp111-{T}(E0,E1) { 0, 1, 32 }
% 12.47/12.79 44 : pppp98-{T}(E0,E0) { 0, 1, 33 }
% 12.47/12.79 45 : pppp84-{T}(E0,E1) { 0, 1, 34 }
% 12.47/12.79 46 : pppp69-{T}(E0,E0) { 0, 1, 35 }
% 12.47/12.79 47 : pppp53-{T}(E0,E1) { 0, 1, 36 }
% 12.47/12.79 48 : pppp36-{T}(E1,E0) { 0, 1, 37 }
% 12.47/12.79 49 : pppp18-{T}(E0,E1) { 0, 1, 38 }
% 12.47/12.79 50 : pppp187-{T}(E0,E0) { 0, 1, 2, 39 }
% 12.47/12.79 51 : pppp185-{T}(E1,E1) { 0, 3, 40 }
% 12.47/12.79 52 : pppp194-{T}(E1) { 0, 3, 40 }
% 12.47/12.79 53 : pppp194-{T}(E0) { 0, 1, 3, 40 }
% 12.47/12.79 54 : pppp185-{T}(E0,E0) { 0, 1, 3, 41 }
% 12.47/12.79 55 : pppp182-{T}(E0,E1) { 0, 4, 42 }
% 12.47/12.79 56 : pppp178-{T}(E0,E1) { 0, 5, 43 }
% 12.47/12.79 57 : pppp178-{T}(E0,E0) { 0, 1, 5, 44 }
% 12.47/12.79 58 : pppp173-{T}(E0,E1) { 0, 6, 45 }
% 12.47/12.79 59 : pppp167-{T}(E0,E1) { 0, 7, 46 }
% 12.47/12.79 60 : pppp167-{T}(E1,E0) { 0, 1, 7, 47 }
% 12.47/12.79 61 : pppp160-{T}(E1,E0) { 0, 8, 48 }
% 12.47/12.79 62 : pppp152-{T}(E0,E1) { 0, 9, 49 }
% 12.47/12.79 63 : pppp160-{T}(E0,E0) { 0, 1, 8, 50 }
% 12.47/12.79 64 : pppp152-{T}(E0,E0) { 0, 1, 9, 51 }
% 12.47/12.79 65 : pppp143-{T}(E0,E1) { 0, 10, 52 }
% 12.47/12.79 66 : pppp133-{T}(E0,E0) { 0, 11, 53 }
% 12.47/12.79 67 : pppp122-{T}(E0,E0) { 0, 12, 54 }
% 12.47/12.79 68 : pppp110-{T}(E1,E0) { 0, 13, 55 }
% 12.47/12.79 69 : pppp97-{T}(E0,E1) { 0, 14, 56 }
% 12.47/12.79 70 : pppp83-{T}(E1,E0) { 0, 15, 57 }
% 12.47/12.79 71 : pppp68-{T}(E0,E0) { 0, 16, 58 }
% 12.47/12.79 72 : pppp52-{T}(E1,E1) { 0, 17, 59 }
% 12.47/12.79 73 : pppp35-{T}(E0,E1) { 0, 18, 60 }
% 12.47/12.79 74 : pppp17-{T}(E0,E0) { 0, 19, 61 }
% 12.47/12.79 75 : pppp52-{T}(E1,E0) { 0, 1, 17, 62 }
% 12.47/12.79 76 : pppp187-{T}(E0,E1) { 0, 1, 2, 20, 63 }
% 12.47/12.79 77 : pppp182-{T}(E1,E1) { 0, 1, 4, 20, 64 }
% 12.47/12.79 78 : pppp173-{T}(E1,E0) { 0, 1, 6, 20, 65 }
% 12.47/12.79 79 : pppp143-{T}(E1,E0) { 0, 1, 10, 20, 66 }
% 12.47/12.79 80 : pppp133-{T}(E0,E1) { 0, 1, 11, 20, 67 }
% 12.47/12.79 81 : pppp122-{T}(E1,E1) { 0, 1, 12, 20, 68 }
% 12.47/12.79 82 : pppp110-{T}(E1,E1) { 0, 1, 13, 20, 69 }
% 12.47/12.79 83 : pppp97-{T}(E1,E0) { 0, 1, 14, 20, 70 }
% 12.47/12.79 84 : pppp83-{T}(E0,E1) { 0, 1, 15, 20, 71 }
% 12.47/12.79 85 : pppp68-{T}(E1,E0) { 0, 1, 16, 20, 72 }
% 12.47/12.79 86 : pppp35-{T}(E1,E1) { 0, 1, 18, 20, 73 }
% 12.47/12.79 87 : pppp17-{T}(E1,E1) { 0, 1, 19, 20, 74 }
% 12.47/12.79 88 : pppp184-{T}(E0,E1) { 0, 3, 40, 75 }
% 12.47/12.79 89 : pppp181-{T}(E1,E1) { 0, 4, 42, 76 }
% 12.47/12.79 90 : pppp195-{T}(E1) { 0, 4, 42, 76 }
% 12.47/12.79 91 : pppp195-{T}(E0) { 0, 1, 4, 42, 76 }
% 12.47/12.79 92 : pppp184-{T}(E0,E0) { 0, 1, 3, 40, 77 }
% 12.47/12.79 93 : pppp181-{T}(E0,E0) { 0, 1, 4, 42, 78 }
% 12.47/12.79 94 : pppp177-{T}(E0,E0) { 0, 5, 43, 79 }
% 12.47/12.79 95 : pppp177-{T}(E1,E1) { 0, 1, 5, 20, 43, 80 }
% 12.47/12.79 96 : pppp172-{T}(E1,E1) { 0, 6, 45, 81 }
% 12.47/12.79 97 : pppp166-{T}(E0,E1) { 0, 7, 46, 82 }
% 12.47/12.79 98 : pppp172-{T}(E0,E0) { 0, 1, 6, 45, 83 }
% 12.47/12.79 99 : pppp166-{T}(E1,E0) { 0, 1, 7, 20, 46, 84 }
% 12.47/12.79 100 : pppp159-{T}(E1,E0) { 0, 8, 48, 85 }
% 12.47/12.79 101 : pppp159-{T}(E1,E1) { 0, 1, 8, 20, 48, 86 }
% 12.47/12.79 102 : pppp151-{T}(E0,E0) { 0, 9, 49, 87 }
% 12.47/12.79 103 : pppp142-{T}(E0,E1) { 0, 10, 52, 88 }
% 12.47/12.79 104 : pppp151-{T}(E1,E1) { 0, 1, 9, 20, 49, 89 }
% 12.47/12.79 105 : pppp142-{T}(E0,E0) { 0, 1, 10, 52, 90 }
% 12.47/12.79 106 : pppp132-{T}(E0,E0) { 0, 11, 53, 91 }
% 12.47/12.79 107 : pppp132-{T}(E1,E0) { 0, 1, 11, 20, 53, 92 }
% 12.47/12.79 108 : pppp121-{T}(E1,E0) { 0, 12, 54, 93 }
% 12.47/12.79 109 : pppp109-{T}(E1,E1) { 0, 13, 55, 94 }
% 12.47/12.79 110 : pppp121-{T}(E1,E1) { 0, 1, 12, 20, 54, 95 }
% 12.47/12.79 111 : pppp109-{T}(E0,E1) { 0, 1, 13, 55, 96 }
% 12.47/12.79 112 : pppp96-{T}(E1,E1) { 0, 14, 56, 97 }
% 12.47/12.79 113 : pppp96-{T}(E1,E0) { 0, 1, 14, 56, 98 }
% 12.47/12.79 114 : pppp82-{T}(E1,E1) { 0, 15, 57, 99 }
% 12.47/12.79 115 : pppp67-{T}(E1,E0) { 0, 16, 58, 100 }
% 12.47/12.79 116 : pppp82-{T}(E0,E0) { 0, 1, 15, 57, 101 }
% 12.47/12.79 117 : pppp67-{T}(E0,E1) { 0, 1, 16, 20, 58, 102 }
% 12.47/12.79 118 : pppp51-{T}(E1,E1) { 0, 17, 59, 103 }
% 12.47/12.79 119 : pppp51-{T}(E0,E0) { 0, 1, 17, 59, 104 }
% 12.47/12.79 120 : pppp34-{T}(E1,E1) { 0, 18, 60, 105 }
% 12.47/12.79 121 : pppp16-{T}(E0,E1) { 0, 19, 61, 106 }
% 12.47/12.79 122 : pppp34-{T}(E1,E0) { 0, 1, 18, 60, 107 }
% 12.47/12.79 123 : pppp16-{T}(E1,E1) { 0, 1, 19, 20, 61, 108 }
% 12.47/12.79 124 : pppp180-{T}(E0,E1) { 0, 4, 42, 76, 109 }
% 12.47/12.79 125 : pppp180-{T}(E1,E0) { 0, 1, 4, 42, 76, 110 }
% 12.47/12.79 126 : pppp176-{T}(E0,E0) { 0, 5, 43, 79, 111 }
% 12.47/12.79 127 : pppp196-{T}(E0) { 0, 1, 5, 43, 79, 111 }
% 12.47/12.79 128 : pppp196-{T}(E1) { 0, 1, 5, 20, 43, 79, 111 }
% 12.47/12.79 129 : pppp176-{T}(E1,E1) { 0, 1, 5, 20, 43, 79, 112 }
% 12.47/12.79 130 : pppp171-{T}(E1,E1) { 0, 6, 45, 81, 113 }
% 12.47/12.79 131 : pppp165-{T}(E1,E1) { 0, 7, 46, 82, 114 }
% 12.47/12.79 132 : pppp171-{T}(E0,E1) { 0, 1, 6, 45, 81, 115 }
% 12.47/12.79 133 : pppp165-{T}(E0,E0) { 0, 1, 7, 46, 82, 116 }
% 12.47/12.79 134 : pppp158-{T}(E1,E1) { 0, 8, 48, 85, 117 }
% 12.47/12.79 135 : pppp158-{T}(E0,E1) { 0, 1, 8, 48, 85, 118 }
% 12.47/12.79 136 : pppp150-{T}(E1,E0) { 0, 9, 49, 87, 119 }
% 12.47/12.79 137 : pppp141-{T}(E0,E0) { 0, 10, 52, 88, 120 }
% 12.47/12.79 138 : pppp150-{T}(E1,E1) { 0, 1, 9, 20, 49, 87, 121 }
% 12.47/12.79 139 : pppp141-{T}(E1,E1) { 0, 1, 10, 20, 52, 88, 122 }
% 12.47/12.79 140 : pppp131-{T}(E0,E0) { 0, 11, 53, 91, 123 }
% 12.47/12.79 141 : pppp131-{T}(E0,E1) { 0, 1, 11, 20, 53, 91, 124 }
% 12.47/12.79 142 : pppp120-{T}(E1,E1) { 0, 12, 54, 93, 125 }
% 12.47/12.79 143 : pppp108-{T}(E1,E1) { 0, 13, 55, 94, 126 }
% 12.47/12.79 144 : pppp120-{T}(E0,E1) { 0, 1, 12, 54, 93, 127 }
% 12.47/12.79 145 : pppp108-{T}(E1,E0) { 0, 1, 13, 55, 94, 128 }
% 12.47/12.79 146 : pppp95-{T}(E1,E0) { 0, 14, 56, 97, 129 }
% 12.47/12.79 147 : pppp95-{T}(E0,E0) { 0, 1, 14, 56, 97, 130 }
% 12.47/12.79 148 : pppp81-{T}(E0,E1) { 0, 15, 57, 99, 131 }
% 12.47/12.79 149 : pppp66-{T}(E1,E1) { 0, 16, 58, 100, 132 }
% 12.47/12.79 150 : pppp81-{T}(E0,E0) { 0, 1, 15, 57, 99, 133 }
% 12.47/12.79 151 : pppp66-{T}(E0,E0) { 0, 1, 16, 58, 100, 134 }
% 12.47/12.79 152 : pppp50-{T}(E0,E1) { 0, 17, 59, 103, 135 }
% 12.47/12.79 153 : pppp50-{T}(E0,E0) { 0, 1, 17, 59, 103, 136 }
% 12.47/12.79 154 : pppp33-{T}(E1,E0) { 0, 18, 60, 105, 137 }
% 12.47/12.79 155 : pppp15-{T}(E0,E1) { 0, 19, 61, 106, 138 }
% 12.47/12.79 156 : pppp33-{T}(E0,E0) { 0, 1, 18, 60, 105, 139 }
% 12.47/12.79 157 : pppp15-{T}(E1,E0) { 0, 1, 19, 61, 106, 140 }
% 12.47/12.79 158 : pppp175-{T}(E0,E0) { 0, 1, 5, 43, 79, 111, 141 }
% 12.47/12.79 159 : pppp175-{T}(E1,E1) { 0, 1, 5, 20, 43, 79, 111, 142 }
% 12.47/12.79 160 : pppp170-{T}(E0,E1) { 0, 6, 45, 81, 113, 143 }
% 12.47/12.79 161 : pppp164-{T}(E1,E1) { 0, 7, 46, 82, 114, 144 }
% 12.47/12.79 162 : pppp170-{T}(E0,E0) { 0, 1, 6, 45, 81, 113, 145 }
% 12.47/12.79 163 : pppp164-{T}(E0,E1) { 0, 1, 7, 46, 82, 114, 146 }
% 12.47/12.79 164 : pppp157-{T}(E1,E1) { 0, 8, 48, 85, 117, 147 }
% 12.47/12.79 165 : pppp157-{T}(E1,E0) { 0, 1, 8, 48, 85, 117, 148 }
% 12.47/12.79 166 : pppp149-{T}(E1,E1) { 0, 9, 49, 87, 119, 149 }
% 12.47/12.79 167 : pppp140-{T}(E1,E0) { 0, 10, 52, 88, 120, 150 }
% 12.47/12.79 168 : pppp149-{T}(E0,E1) { 0, 1, 9, 49, 87, 119, 151 }
% 12.47/12.79 169 : pppp140-{T}(E1,E1) { 0, 1, 10, 20, 52, 88, 120, 152 }
% 12.47/12.79 170 : pppp130-{T}(E0,E1) { 0, 11, 53, 91, 123, 153 }
% 12.47/12.79 171 : pppp130-{T}(E1,E0) { 0, 1, 11, 20, 53, 91, 123, 154 }
% 12.47/12.79 172 : pppp119-{T}(E1,E1) { 0, 12, 54, 93, 125, 155 }
% 12.47/12.79 173 : pppp107-{T}(E1,E0) { 0, 13, 55, 94, 126, 156 }
% 12.47/12.79 174 : pppp119-{T}(E1,E0) { 0, 1, 12, 54, 93, 125, 157 }
% 12.47/12.79 175 : pppp107-{T}(E0,E0) { 0, 1, 13, 55, 94, 126, 158 }
% 12.47/12.79 176 : pppp94-{T}(E0,E0) { 0, 14, 56, 97, 129, 159 }
% 12.47/12.79 177 : pppp94-{T}(E0,E1) { 0, 1, 14, 20, 56, 97, 129, 160 }
% 12.47/12.79 178 : pppp80-{T}(E0,E0) { 0, 15, 57, 99, 131, 161 }
% 12.47/12.79 179 : pppp65-{T}(E0,E1) { 0, 16, 58, 100, 132, 162 }
% 12.47/12.79 180 : pppp80-{T}(E1,E0) { 0, 1, 15, 20, 57, 99, 131, 163 }
% 12.47/12.79 181 : pppp65-{T}(E1,E0) { 0, 1, 16, 58, 100, 132, 164 }
% 12.47/12.79 182 : pppp49-{T}(E0,E0) { 0, 17, 59, 103, 135, 165 }
% 12.47/12.79 183 : pppp49-{T}(E1,E0) { 0, 1, 17, 20, 59, 103, 135, 166 }
% 12.47/12.79 184 : pppp32-{T}(E1,E0) { 0, 18, 60, 105, 137, 167 }
% 12.47/12.79 185 : pppp14-{T}(E0,E1) { 0, 19, 61, 106, 138, 168 }
% 12.47/12.79 186 : pppp32-{T}(E1,E1) { 0, 1, 18, 20, 60, 105, 137, 169 }
% 12.47/12.79 187 : pppp14-{T}(E1,E0) { 0, 1, 19, 20, 61, 106, 138, 170 }
% 12.47/12.79 188 : pppp197-{T}(E0) { 0, 6, 45, 81, 113, 143, 171 }
% 12.47/12.79 189 : pppp197-{T}(E1) { 0, 1, 6, 20, 45, 81, 113, 143, 172 }
% 12.47/12.79 190 : pppp163-{T}(E1,E1) { 0, 7, 46, 82, 114, 144, 173 }
% 12.47/12.79 191 : pppp198-{T}(E1) { 0, 7, 46, 82, 114, 144, 173 }
% 12.47/12.79 192 : pppp198-{T}(E0) { 0, 1, 7, 46, 82, 114, 144, 173 }
% 12.47/12.79 193 : pppp163-{T}(E0,E0) { 0, 1, 7, 46, 82, 114, 144, 174 }
% 12.47/12.79 194 : pppp156-{T}(E1,E0) { 0, 8, 48, 85, 117, 147, 175 }
% 12.47/12.79 195 : pppp148-{T}(E0,E1) { 0, 9, 49, 87, 119, 149, 176 }
% 12.47/12.79 196 : pppp156-{T}(E0,E1) { 0, 1, 8, 48, 85, 117, 147, 177 }
% 12.47/12.79 197 : pppp148-{T}(E1,E0) { 0, 1, 9, 49, 87, 119, 149, 178 }
% 12.47/12.79 198 : pppp139-{T}(E1,E1) { 0, 10, 52, 88, 120, 150, 179 }
% 12.47/12.79 199 : pppp139-{T}(E0,E0) { 0, 1, 10, 52, 88, 120, 150, 180 }
% 12.47/12.79 200 : pppp129-{T}(E1,E1) { 0, 11, 53, 91, 123, 153, 181 }
% 12.47/12.79 201 : pppp118-{T}(E1,E0) { 0, 12, 54, 93, 125, 155, 182 }
% 12.47/12.79 202 : pppp129-{T}(E0,E0) { 0, 1, 11, 53, 91, 123, 153, 183 }
% 12.47/12.79 203 : pppp118-{T}(E0,E0) { 0, 1, 12, 54, 93, 125, 155, 184 }
% 12.47/12.79 204 : pppp106-{T}(E1,E0) { 0, 13, 55, 94, 126, 156, 185 }
% 12.47/12.79 205 : pppp106-{T}(E1,E1) { 0, 1, 13, 20, 55, 94, 126, 156, 186 }
% 12.47/12.79 206 : pppp93-{T}(E0,E1) { 0, 14, 56, 97, 129, 159, 187 }
% 12.47/12.79 207 : pppp79-{T}(E1,E0) { 0, 15, 57, 99, 131, 161, 188 }
% 12.47/12.79 208 : pppp93-{T}(E1,E1) { 0, 1, 14, 20, 56, 97, 129, 159, 189 }
% 12.47/12.79 209 : pppp79-{T}(E0,E1) { 0, 1, 15, 20, 57, 99, 131, 161, 190 }
% 12.47/12.79 210 : pppp64-{T}(E0,E1) { 0, 16, 58, 100, 132, 162, 191 }
% 12.47/12.79 211 : pppp64-{T}(E1,E1) { 0, 1, 16, 20, 58, 100, 132, 162, 192 }
% 12.47/12.79 212 : pppp48-{T}(E1,E0) { 0, 17, 59, 103, 135, 165, 193 }
% 12.47/12.79 213 : pppp31-{T}(E1,E1) { 0, 18, 60, 105, 137, 167, 194 }
% 12.47/12.79 214 : pppp48-{T}(E1,E1) { 0, 1, 17, 20, 59, 103, 135, 165, 195 }
% 12.47/12.79 215 : pppp31-{T}(E0,E1) { 0, 1, 18, 60, 105, 137, 167, 196 }
% 12.47/12.79 216 : pppp13-{T}(E1,E1) { 0, 19, 61, 106, 138, 168, 197 }
% 12.47/12.79 217 : pppp13-{T}(E1,E0) { 0, 1, 19, 61, 106, 138, 168, 198 }
% 12.47/12.79 218 : pppp169-{T}(E1,E0) { 0, 6, 45, 81, 113, 143, 171, 199 }
% 12.47/12.79 219 : pppp162-{T}(E1,E1) { 0, 7, 46, 82, 114, 144, 173, 200 }
% 12.47/12.79 220 : pppp169-{T}(E0,E1) { 0, 1, 6, 20, 45, 81, 113, 143, 172, 201 }
% 12.47/12.79 221 : pppp162-{T}(E1,E0) { 0, 1, 7, 46, 82, 114, 144, 173, 202 }
% 12.47/12.79 222 : pppp155-{T}(E0,E0) { 0, 8, 48, 85, 117, 147, 175, 203 }
% 12.47/12.79 223 : pppp155-{T}(E1,E1) { 0, 1, 8, 20, 48, 85, 117, 147, 175, 204 }
% 12.47/12.79 224 : pppp147-{T}(E0,E0) { 0, 9, 49, 87, 119, 149, 176, 205 }
% 12.47/12.79 225 : pppp138-{T}(E0,E1) { 0, 10, 52, 88, 120, 150, 179, 206 }
% 12.47/12.79 226 : pppp147-{T}(E1,E0) { 0, 1, 9, 20, 49, 87, 119, 149, 176, 207 }
% 12.47/12.79 227 : pppp138-{T}(E0,E0) { 0, 1, 10, 52, 88, 120, 150, 179, 208 }
% 12.47/12.79 228 : pppp128-{T}(E1,E1) { 0, 11, 53, 91, 123, 153, 181, 209 }
% 12.47/12.79 229 : pppp128-{T}(E0,E1) { 0, 1, 11, 53, 91, 123, 153, 181, 210 }
% 12.47/12.79 230 : pppp117-{T}(E1,E0) { 0, 12, 54, 93, 125, 155, 182, 211 }
% 12.47/12.79 231 : pppp105-{T}(E1,E0) { 0, 13, 55, 94, 126, 156, 185, 212 }
% 12.47/12.79 232 : pppp117-{T}(E0,E1) { 0, 1, 12, 20, 54, 93, 125, 155, 182, 213 }
% 12.47/12.79 233 : pppp105-{T}(E0,E1) { 0, 1, 13, 55, 94, 126, 156, 185, 214 }
% 12.47/12.79 234 : pppp92-{T}(E0,E1) { 0, 14, 56, 97, 129, 159, 187, 215 }
% 12.47/12.79 235 : pppp92-{T}(E1,E0) { 0, 1, 14, 56, 97, 129, 159, 187, 216 }
% 12.47/12.79 236 : pppp78-{T}(E1,E0) { 0, 15, 57, 99, 131, 161, 188, 217 }
% 12.47/12.79 237 : pppp63-{T}(E0,E1) { 0, 16, 58, 100, 132, 162, 191, 218 }
% 12.47/12.79 238 : pppp78-{T}(E0,E1) { 0, 1, 15, 57, 99, 131, 161, 188, 219 }
% 12.47/12.79 239 : pppp63-{T}(E0,E0) { 0, 1, 16, 58, 100, 132, 162, 191, 220 }
% 12.47/12.79 240 : pppp47-{T}(E1,E1) { 0, 17, 59, 103, 135, 165, 193, 221 }
% 12.47/12.79 241 : pppp47-{T}(E0,E0) { 0, 1, 17, 59, 103, 135, 165, 193, 222 }
% 12.47/12.79 242 : pppp30-{T}(E0,E1) { 0, 18, 60, 105, 137, 167, 194, 223 }
% 12.47/12.79 243 : pppp12-{T}(E1,E0) { 0, 19, 61, 106, 138, 168, 197, 224 }
% 12.47/12.79 244 : pppp30-{T}(E0,E0) { 0, 1, 18, 60, 105, 137, 167, 194, 225 }
% 12.47/12.79 245 : pppp12-{T}(E0,E1) { 0, 1, 19, 61, 106, 138, 168, 197, 226 }
% 12.47/12.79 246 : pppp199-{T}(E0) { 0, 8, 48, 85, 117, 147, 175, 203, 227 }
% 12.47/12.79 247 : pppp199-{T}(E1) { 0, 1, 8, 20, 48, 85, 117, 147, 175, 203, 228 }
% 12.47/12.79 248 : pppp146-{T}(E1,E0) { 0, 9, 49, 87, 119, 149, 176, 205, 229 }
% 12.47/12.79 249 : pppp137-{T}(E0,E0) { 0, 10, 52, 88, 120, 150, 179, 206, 230 }
% 12.47/12.79 250 : pppp146-{T}(E1,E1) { 0, 1, 9, 20, 49, 87, 119, 149, 176, 205, 231 }
% 12.47/12.79 251 : pppp137-{T}(E1,E1) { 0, 1, 10, 20, 52, 88, 120, 150, 179, 206, 232 }
% 12.47/12.79 252 : pppp127-{T}(E0,E1) { 0, 11, 53, 91, 123, 153, 181, 209, 233 }
% 12.47/12.79 253 : pppp127-{T}(E1,E0) { 0, 1, 11, 53, 91, 123, 153, 181, 209, 234 }
% 12.47/12.79 254 : pppp116-{T}(E1,E1) { 0, 12, 54, 93, 125, 155, 182, 211, 235 }
% 12.47/12.79 255 : pppp104-{T}(E0,E0) { 0, 13, 55, 94, 126, 156, 185, 212, 236 }
% 12.47/12.79 256 : pppp116-{T}(E0,E0) { 0, 1, 12, 54, 93, 125, 155, 182, 211, 237 }
% 12.47/12.79 257 : pppp104-{T}(E1,E1) { 0, 1, 13, 20, 55, 94, 126, 156, 185, 212, 238 }
% 12.47/12.79 258 : pppp91-{T}(E0,E0) { 0, 14, 56, 97, 129, 159, 187, 215, 239 }
% 12.47/12.79 259 : pppp91-{T}(E1,E1) { 0, 1, 14, 20, 56, 97, 129, 159, 187, 215, 240 }
% 12.47/12.79 260 : pppp77-{T}(E1,E0) { 0, 15, 57, 99, 131, 161, 188, 217, 241 }
% 12.47/12.79 261 : pppp62-{T}(E0,E0) { 0, 16, 58, 100, 132, 162, 191, 218, 242 }
% 12.47/12.79 262 : pppp77-{T}(E0,E1) { 0, 1, 15, 20, 57, 99, 131, 161, 188, 217, 243 }
% 12.47/12.79 263 : pppp62-{T}(E1,E1) { 0, 1, 16, 20, 58, 100, 132, 162, 191, 218, 244 }
% 12.47/12.79 264 : pppp46-{T}(E0,E1) { 0, 17, 59, 103, 135, 165, 193, 221, 245 }
% 12.47/12.79 265 : pppp46-{T}(E1,E0) { 0, 1, 17, 59, 103, 135, 165, 193, 221, 246 }
% 12.47/12.79 266 : pppp29-{T}(E0,E0) { 0, 18, 60, 105, 137, 167, 194, 223, 247 }
% 12.47/12.79 267 : pppp11-{T}(E0,E0) { 0, 19, 61, 106, 138, 168, 197, 224, 248 }
% 12.47/12.79 268 : pppp29-{T}(E1,E0) { 0, 1, 18, 20, 60, 105, 137, 167, 194, 223, 249 }
% 12.47/12.79 269 : pppp11-{T}(E0,E1) { 0, 1, 19, 20, 61, 106, 138, 168, 197, 224, 250 }
% 12.47/12.79 270 : pppp154-{T}(E0,E0) { 0, 8, 48, 85, 117, 147, 175, 203, 227, 251 }
% 12.47/12.79 271 : pppp154-{T}(E1,E1) { 0, 1, 8, 20, 48, 85, 117, 147, 175, 203, 228, 252 }
% 12.47/12.79 272 : pppp200-{T}(E1) { 0, 9, 49, 87, 119, 149, 176, 205, 229, 253 }
% 12.47/12.79 273 : pppp136-{T}(E0,E0) { 0, 10, 52, 88, 120, 150, 179, 206, 230, 254 }
% 12.47/12.79 274 : pppp201-{T}(E0) { 0, 1, 10, 52, 88, 120, 150, 179, 206, 230, 254 }
% 12.47/12.79 275 : pppp201-{T}(E1) { 0, 1, 10, 20, 52, 88, 120, 150, 179, 206, 230, 254 }
% 12.47/12.79 276 : pppp200-{T}(E0) { 0, 1, 9, 49, 87, 119, 149, 176, 205, 229, 255 }
% 12.47/12.79 277 : pppp136-{T}(E0,E1) { 0, 1, 10, 20, 52, 88, 120, 150, 179, 206, 230, 256 }
% 12.47/12.79 278 : pppp126-{T}(E0,E0) { 0, 11, 53, 91, 123, 153, 181, 209, 233, 257 }
% 12.47/12.79 279 : pppp126-{T}(E1,E1) { 0, 1, 11, 20, 53, 91, 123, 153, 181, 209, 233, 258 }
% 12.47/12.79 280 : pppp115-{T}(E1,E1) { 0, 12, 54, 93, 125, 155, 182, 211, 235, 259 }
% 12.47/12.79 281 : pppp103-{T}(E0,E1) { 0, 13, 55, 94, 126, 156, 185, 212, 236, 260 }
% 12.47/12.79 282 : pppp115-{T}(E0,E0) { 0, 1, 12, 54, 93, 125, 155, 182, 211, 235, 261 }
% 12.47/12.79 283 : pppp103-{T}(E1,E0) { 0, 1, 13, 20, 55, 94, 126, 156, 185, 212, 236, 262 }
% 12.47/12.79 284 : pppp90-{T}(E1,E0) { 0, 14, 56, 97, 129, 159, 187, 215, 239, 263 }
% 12.47/12.79 285 : pppp90-{T}(E0,E1) { 0, 1, 14, 20, 56, 97, 129, 159, 187, 215, 239, 264 }
% 12.47/12.79 286 : pppp76-{T}(E1,E1) { 0, 15, 57, 99, 131, 161, 188, 217, 241, 265 }
% 12.47/12.79 287 : pppp61-{T}(E1,E0) { 0, 16, 58, 100, 132, 162, 191, 218, 242, 266 }
% 12.47/12.79 288 : pppp76-{T}(E0,E0) { 0, 1, 15, 57, 99, 131, 161, 188, 217, 241, 267 }
% 12.47/12.79 289 : pppp61-{T}(E0,E1) { 0, 1, 16, 20, 58, 100, 132, 162, 191, 218, 242, 268 }
% 12.47/12.79 290 : pppp45-{T}(E0,E1) { 0, 17, 59, 103, 135, 165, 193, 221, 245, 269 }
% 12.47/12.79 291 : pppp45-{T}(E1,E1) { 0, 1, 17, 20, 59, 103, 135, 165, 193, 221, 245, 270 }
% 12.47/12.79 292 : pppp28-{T}(E1,E0) { 0, 18, 60, 105, 137, 167, 194, 223, 247, 271 }
% 12.47/12.79 293 : pppp10-{T}(E0,E1) { 0, 19, 61, 106, 138, 168, 197, 224, 248, 272 }
% 12.47/12.79 294 : pppp28-{T}(E0,E1) { 0, 1, 18, 20, 60, 105, 137, 167, 194, 223, 247, 273 }
% 12.47/12.79 295 : pppp10-{T}(E1,E1) { 0, 1, 19, 20, 61, 106, 138, 168, 197, 224, 248, 274 }
% 12.47/12.79 296 : pppp145-{T}(E1,E1) { 0, 9, 49, 87, 119, 149, 176, 205, 229, 253, 275 }
% 12.47/12.79 297 : pppp135-{T}(E1,E0) { 0, 1, 10, 52, 88, 120, 150, 179, 206, 230, 254, 276 }
% 12.47/12.79 298 : pppp145-{T}(E0,E0) { 0, 1, 9, 49, 87, 119, 149, 176, 205, 229, 255, 277 }
% 12.47/12.79 299 : pppp125-{T}(E0,E0) { 0, 11, 53, 91, 123, 153, 181, 209, 233, 257, 278 }
% 12.47/12.79 300 : pppp135-{T}(E1,E1) { 0, 1, 10, 20, 52, 88, 120, 150, 179, 206, 230, 254, 279 }
% 12.47/12.79 301 : pppp125-{T}(E0,E1) { 0, 1, 11, 20, 53, 91, 123, 153, 181, 209, 233, 257, 280 }
% 12.47/12.79 302 : pppp114-{T}(E1,E1) { 0, 12, 54, 93, 125, 155, 182, 211, 235, 259, 281 }
% 12.47/12.79 303 : pppp114-{T}(E0,E1) { 0, 1, 12, 54, 93, 125, 155, 182, 211, 235, 259, 282 }
% 12.47/12.79 304 : pppp102-{T}(E0,E1) { 0, 13, 55, 94, 126, 156, 185, 212, 236, 260, 283 }
% 12.47/12.79 305 : pppp89-{T}(E1,E1) { 0, 14, 56, 97, 129, 159, 187, 215, 239, 263, 284 }
% 12.47/12.79 306 : pppp102-{T}(E1,E0) { 0, 1, 13, 55, 94, 126, 156, 185, 212, 236, 260, 285 }
% 12.47/12.79 307 : pppp89-{T}(E0,E0) { 0, 1, 14, 56, 97, 129, 159, 187, 215, 239, 263, 286 }
% 12.47/12.79 308 : pppp75-{T}(E1,E1) { 0, 15, 57, 99, 131, 161, 188, 217, 241, 265, 287 }
% 12.47/12.79 309 : pppp75-{T}(E1,E0) { 0, 1, 15, 57, 99, 131, 161, 188, 217, 241, 265, 288 }
% 12.47/12.79 310 : pppp60-{T}(E1,E1) { 0, 16, 58, 100, 132, 162, 191, 218, 242, 266, 289 }
% 12.47/12.79 311 : pppp44-{T}(E1,E1) { 0, 17, 59, 103, 135, 165, 193, 221, 245, 269, 290 }
% 12.47/12.79 312 : pppp60-{T}(E0,E0) { 0, 1, 16, 58, 100, 132, 162, 191, 218, 242, 266, 291 }
% 12.47/12.79 313 : pppp44-{T}(E0,E0) { 0, 1, 17, 59, 103, 135, 165, 193, 221, 245, 269, 292 }
% 12.47/12.79 314 : pppp27-{T}(E1,E0) { 0, 18, 60, 105, 137, 167, 194, 223, 247, 271, 293 }
% 12.47/12.79 315 : pppp27-{T}(E0,E0) { 0, 1, 18, 60, 105, 137, 167, 194, 223, 247, 271, 294 }
% 12.47/12.79 316 : pppp9-{T}(E0,E1) { 0, 19, 61, 106, 138, 168, 197, 224, 248, 272, 295 }
% 12.47/12.79 317 : pppp202-{T}(E0) { 0, 11, 53, 91, 123, 153, 181, 209, 233, 257, 278, 296 }
% 12.47/12.79 318 : pppp9-{T}(E0,E0) { 0, 1, 19, 61, 106, 138, 168, 197, 224, 248, 272, 297 }
% 12.47/12.79 319 : pppp202-{T}(E1) { 0, 1, 11, 20, 53, 91, 123, 153, 181, 209, 233, 257, 278, 298 }
% 12.47/12.79 320 : pppp113-{T}(E0,E1) { 0, 12, 54, 93, 125, 155, 182, 211, 235, 259, 281, 299 }
% 12.47/12.79 321 : pppp203-{T}(E0) { 0, 1, 12, 54, 93, 125, 155, 182, 211, 235, 259, 281, 299 }
% 12.47/12.79 322 : pppp203-{T}(E1) { 0, 1, 12, 20, 54, 93, 125, 155, 182, 211, 235, 259, 281, 299 }
% 12.47/12.79 323 : pppp113-{T}(E0,E0) { 0, 1, 12, 54, 93, 125, 155, 182, 211, 235, 259, 281, 300 }
% 12.47/12.79 324 : pppp101-{T}(E0,E1) { 0, 13, 55, 94, 126, 156, 185, 212, 236, 260, 283, 301 }
% 12.47/12.79 325 : pppp88-{T}(E1,E1) { 0, 14, 56, 97, 129, 159, 187, 215, 239, 263, 284, 302 }
% 12.47/12.79 326 : pppp101-{T}(E1,E0) { 0, 1, 13, 20, 55, 94, 126, 156, 185, 212, 236, 260, 283, 303 }
% 12.47/12.79 327 : pppp88-{T}(E1,E0) { 0, 1, 14, 56, 97, 129, 159, 187, 215, 239, 263, 284, 304 }
% 12.47/12.79 328 : pppp74-{T}(E1,E1) { 0, 15, 57, 99, 131, 161, 188, 217, 241, 265, 287, 305 }
% 12.47/12.79 329 : pppp74-{T}(E0,E1) { 0, 1, 15, 57, 99, 131, 161, 188, 217, 241, 265, 287, 306 }
% 12.47/12.79 330 : pppp59-{T}(E1,E1) { 0, 16, 58, 100, 132, 162, 191, 218, 242, 266, 289, 307 }
% 12.47/12.79 331 : pppp43-{T}(E1,E1) { 0, 17, 59, 103, 135, 165, 193, 221, 245, 269, 290, 308 }
% 12.47/12.79 332 : pppp59-{T}(E0,E0) { 0, 1, 16, 58, 100, 132, 162, 191, 218, 242, 266, 289, 309 }
% 12.47/12.79 333 : pppp43-{T}(E0,E0) { 0, 1, 17, 59, 103, 135, 165, 193, 221, 245, 269, 290, 310 }
% 12.47/12.79 334 : pppp26-{T}(E0,E0) { 0, 18, 60, 105, 137, 167, 194, 223, 247, 271, 293, 311 }
% 12.47/12.79 335 : pppp26-{T}(E1,E1) { 0, 1, 18, 20, 60, 105, 137, 167, 194, 223, 247, 271, 293, 312 }
% 12.47/12.79 336 : pppp8-{T}(E0,E0) { 0, 19, 61, 106, 138, 168, 197, 224, 248, 272, 295, 313 }
% 12.47/12.79 337 : pppp124-{T}(E1,E0) { 0, 11, 53, 91, 123, 153, 181, 209, 233, 257, 278, 296, 314 }
% 12.47/12.79 338 : pppp8-{T}(E1,E1) { 0, 1, 19, 20, 61, 106, 138, 168, 197, 224, 248, 272, 295, 315 }
% 12.47/12.79 339 : pppp124-{T}(E1,E1) { 0, 1, 11, 20, 53, 91, 123, 153, 181, 209, 233, 257, 278, 298, 316 }
% 12.47/12.79 340 : pppp112-{T}(E1,E0) { 0, 1, 12, 54, 93, 125, 155, 182, 211, 235, 259, 281, 299, 317 }
% 12.47/12.79 341 : pppp112-{T}(E0,E1) { 0, 1, 12, 20, 54, 93, 125, 155, 182, 211, 235, 259, 281, 299, 318 }
% 12.47/12.79 342 : pppp100-{T}(E0,E1) { 0, 13, 55, 94, 126, 156, 185, 212, 236, 260, 283, 301, 319 }
% 12.47/12.79 343 : pppp204-{T}(E0) { 0, 1, 13, 55, 94, 126, 156, 185, 212, 236, 260, 283, 301, 319 }
% 12.47/12.79 344 : pppp204-{T}(E1) { 0, 1, 13, 20, 55, 94, 126, 156, 185, 212, 236, 260, 283, 301, 319 }
% 12.47/12.79 345 : pppp100-{T}(E0,E0) { 0, 1, 13, 55, 94, 126, 156, 185, 212, 236, 260, 283, 301, 320 }
% 12.47/12.79 346 : pppp87-{T}(E1,E0) { 0, 14, 56, 97, 129, 159, 187, 215, 239, 263, 284, 302, 321 }
% 12.47/12.79 347 : pppp73-{T}(E1,E1) { 0, 15, 57, 99, 131, 161, 188, 217, 241, 265, 287, 305, 322 }
% 12.47/12.79 348 : pppp87-{T}(E0,E0) { 0, 1, 14, 56, 97, 129, 159, 187, 215, 239, 263, 284, 302, 323 }
% 12.47/12.79 349 : pppp73-{T}(E1,E0) { 0, 1, 15, 57, 99, 131, 161, 188, 217, 241, 265, 287, 305, 324 }
% 12.47/12.79 350 : pppp58-{T}(E1,E1) { 0, 16, 58, 100, 132, 162, 191, 218, 242, 266, 289, 307, 325 }
% 12.47/12.80 351 : pppp58-{T}(E0,E0) { 0, 1, 16, 58, 100, 132, 162, 191, 218, 242, 266, 289, 307, 326 }
% 12.47/12.80 352 : pppp42-{T}(E0,E1) { 0, 17, 59, 103, 135, 165, 193, 221, 245, 269, 290, 308, 327 }
% 12.47/12.80 353 : pppp25-{T}(E0,E0) { 0, 18, 60, 105, 137, 167, 194, 223, 247, 271, 293, 311, 328 }
% 12.47/12.80 354 : pppp42-{T}(E0,E0) { 0, 1, 17, 59, 103, 135, 165, 193, 221, 245, 269, 290, 308, 329 }
% 12.47/12.80 355 : pppp25-{T}(E1,E1) { 0, 1, 18, 20, 60, 105, 137, 167, 194, 223, 247, 271, 293, 311, 330 }
% 12.47/12.80 356 : pppp7-{T}(E0,E0) { 0, 19, 61, 106, 138, 168, 197, 224, 248, 272, 295, 313, 331 }
% 12.47/12.80 357 : pppp7-{T}(E0,E1) { 0, 1, 19, 20, 61, 106, 138, 168, 197, 224, 248, 272, 295, 313, 332 }
% 12.47/12.80 358 : pppp99-{T}(E1,E0) { 0, 1, 13, 55, 94, 126, 156, 185, 212, 236, 260, 283, 301, 319, 333 }
% 12.47/12.80 359 : pppp86-{T}(E0,E0) { 0, 14, 56, 97, 129, 159, 187, 215, 239, 263, 284, 302, 321, 334 }
% 12.47/12.80 360 : pppp205-{T}(E0) { 0, 1, 14, 56, 97, 129, 159, 187, 215, 239, 263, 284, 302, 321, 334 }
% 12.47/12.80 361 : pppp205-{T}(E1) { 0, 1, 14, 20, 56, 97, 129, 159, 187, 215, 239, 263, 284, 302, 321, 334 }
% 12.47/12.80 362 : pppp99-{T}(E0,E1) { 0, 1, 13, 20, 55, 94, 126, 156, 185, 212, 236, 260, 283, 301, 319, 335 }
% 12.47/12.80 363 : pppp86-{T}(E0,E1) { 0, 1, 14, 20, 56, 97, 129, 159, 187, 215, 239, 263, 284, 302, 321, 336 }
% 12.47/12.80 364 : pppp72-{T}(E1,E1) { 0, 15, 57, 99, 131, 161, 188, 217, 241, 265, 287, 305, 322, 337 }
% 12.47/12.80 365 : pppp72-{T}(E0,E0) { 0, 1, 15, 57, 99, 131, 161, 188, 217, 241, 265, 287, 305, 322, 338 }
% 12.47/12.80 366 : pppp57-{T}(E1,E1) { 0, 16, 58, 100, 132, 162, 191, 218, 242, 266, 289, 307, 325, 339 }
% 12.47/12.80 367 : pppp41-{T}(E0,E0) { 0, 17, 59, 103, 135, 165, 193, 221, 245, 269, 290, 308, 327, 340 }
% 12.47/12.80 368 : pppp57-{T}(E0,E0) { 0, 1, 16, 58, 100, 132, 162, 191, 218, 242, 266, 289, 307, 325, 341 }
% 12.47/12.80 369 : pppp41-{T}(E1,E0) { 0, 1, 17, 20, 59, 103, 135, 165, 193, 221, 245, 269, 290, 308, 327, 342 }
% 12.47/12.80 370 : pppp24-{T}(E0,E0) { 0, 18, 60, 105, 137, 167, 194, 223, 247, 271, 293, 311, 328, 343 }
% 12.47/12.80 371 : pppp24-{T}(E1,E1) { 0, 1, 18, 20, 60, 105, 137, 167, 194, 223, 247, 271, 293, 311, 328, 344 }
% 12.47/12.80 372 : pppp6-{T}(E0,E1) { 0, 19, 61, 106, 138, 168, 197, 224, 248, 272, 295, 313, 331, 345 }
% 12.47/12.80 373 : pppp85-{T}(E0,E0) { 0, 1, 14, 56, 97, 129, 159, 187, 215, 239, 263, 284, 302, 321, 334, 346 }
% 12.47/12.80 374 : pppp6-{T}(E1,E1) { 0, 1, 19, 20, 61, 106, 138, 168, 197, 224, 248, 272, 295, 313, 331, 347 }
% 12.47/12.80 375 : pppp85-{T}(E1,E1) { 0, 1, 14, 20, 56, 97, 129, 159, 187, 215, 239, 263, 284, 302, 321, 334, 348 }
% 12.47/12.80 376 : pppp71-{T}(E0,E1) { 0, 15, 57, 99, 131, 161, 188, 217, 241, 265, 287, 305, 322, 337, 349 }
% 12.47/12.80 377 : pppp206-{T}(E1) { 0, 1, 15, 20, 57, 99, 131, 161, 188, 217, 241, 265, 287, 305, 322, 337, 349 }
% 12.47/12.80 378 : pppp206-{T}(E0) { 0, 1, 15, 57, 99, 131, 161, 188, 217, 241, 265, 287, 305, 322, 337, 349 }
% 12.47/12.80 379 : pppp71-{T}(E1,E0) { 0, 1, 15, 57, 99, 131, 161, 188, 217, 241, 265, 287, 305, 322, 337, 350 }
% 12.47/12.80 380 : pppp56-{T}(E1,E1) { 0, 16, 58, 100, 132, 162, 191, 218, 242, 266, 289, 307, 325, 339, 351 }
% 12.47/12.80 381 : pppp40-{T}(E1,E0) { 0, 17, 59, 103, 135, 165, 193, 221, 245, 269, 290, 308, 327, 340, 352 }
% 12.47/12.80 382 : pppp56-{T}(E0,E1) { 0, 1, 16, 58, 100, 132, 162, 191, 218, 242, 266, 289, 307, 325, 339, 353 }
% 12.47/12.80 383 : pppp40-{T}(E1,E1) { 0, 1, 17, 20, 59, 103, 135, 165, 193, 221, 245, 269, 290, 308, 327, 340, 354 }
% 12.47/12.80 384 : pppp23-{T}(E0,E0) { 0, 18, 60, 105, 137, 167, 194, 223, 247, 271, 293, 311, 328, 343, 355 }
% 12.47/12.80 385 : pppp23-{T}(E1,E1) { 0, 1, 18, 20, 60, 105, 137, 167, 194, 223, 247, 271, 293, 311, 328, 343, 356 }
% 12.47/12.80 386 : pppp5-{T}(E1,E1) { 0, 19, 61, 106, 138, 168, 197, 224, 248, 272, 295, 313, 331, 345, 357 }
% 12.47/12.80 387 : pppp70-{T}(E1,E0) { 0, 1, 15, 57, 99, 131, 161, 188, 217, 241, 265, 287, 305, 322, 337, 349, 358 }
% 12.47/12.80 388 : pppp5-{T}(E1,E0) { 0, 1, 19, 61, 106, 138, 168, 197, 224, 248, 272, 295, 313, 331, 345, 359 }
% 12.47/12.80 389 : pppp70-{T}(E0,E1) { 0, 1, 15, 20, 57, 99, 131, 161, 188, 217, 241, 265, 287, 305, 322, 337, 349, 360 }
% 12.47/12.80 390 : pppp55-{T}(E1,E1) { 0, 16, 58, 100, 132, 162, 191, 218, 242, 266, 289, 307, 325, 339, 351, 361 }
% 12.47/12.80 391 : pppp207-{T}(E0) { 0, 1, 16, 58, 100, 132, 162, 191, 218, 242, 266, 289, 307, 325, 339, 351, 361 }
% 12.47/12.80 392 : pppp207-{T}(E1) { 0, 1, 16, 20, 58, 100, 132, 162, 191, 218, 242, 266, 289, 307, 325, 339, 351, 361 }
% 12.47/12.80 393 : pppp55-{T}(E1,E0) { 0, 1, 16, 58, 100, 132, 162, 191, 218, 242, 266, 289, 307, 325, 339, 351, 362 }
% 12.47/12.80 394 : pppp39-{T}(E1,E0) { 0, 17, 59, 103, 135, 165, 193, 221, 245, 269, 290, 308, 327, 340, 352, 363 }
% 12.47/12.80 395 : pppp22-{T}(E1,E0) { 0, 18, 60, 105, 137, 167, 194, 223, 247, 271, 293, 311, 328, 343, 355, 364 }
% 12.47/12.80 396 : pppp39-{T}(E0,E1) { 0, 1, 17, 59, 103, 135, 165, 193, 221, 245, 269, 290, 308, 327, 340, 352, 365 }
% 12.47/12.80 397 : pppp22-{T}(E1,E1) { 0, 1, 18, 20, 60, 105, 137, 167, 194, 223, 247, 271, 293, 311, 328, 343, 355, 366 }
% 12.47/12.80 398 : pppp4-{T}(E1,E1) { 0, 19, 61, 106, 138, 168, 197, 224, 248, 272, 295, 313, 331, 345, 357, 367 }
% 12.47/12.80 399 : pppp4-{T}(E0,E0) { 0, 1, 19, 61, 106, 138, 168, 197, 224, 248, 272, 295, 313, 331, 345, 357, 368 }
% 12.47/12.80 400 : pppp54-{T}(E0,E0) { 0, 1, 16, 58, 100, 132, 162, 191, 218, 242, 266, 289, 307, 325, 339, 351, 361, 369 }
% 12.47/12.80 401 : pppp38-{T}(E1,E0) { 0, 17, 59, 103, 135, 165, 193, 221, 245, 269, 290, 308, 327, 340, 352, 363, 370 }
% 12.47/12.80 402 : pppp208-{T}(E1) { 0, 17, 59, 103, 135, 165, 193, 221, 245, 269, 290, 308, 327, 340, 352, 363, 370 }
% 12.47/12.80 403 : pppp208-{T}(E0) { 0, 1, 17, 59, 103, 135, 165, 193, 221, 245, 269, 290, 308, 327, 340, 352, 363, 370 }
% 12.47/12.80 404 : pppp54-{T}(E0,E1) { 0, 1, 16, 20, 58, 100, 132, 162, 191, 218, 242, 266, 289, 307, 325, 339, 351, 361, 371 }
% 12.47/12.80 405 : pppp38-{T}(E1,E1) { 0, 1, 17, 20, 59, 103, 135, 165, 193, 221, 245, 269, 290, 308, 327, 340, 352, 363, 372 }
% 12.47/12.80 406 : pppp21-{T}(E1,E1) { 0, 18, 60, 105, 137, 167, 194, 223, 247, 271, 293, 311, 328, 343, 355, 364, 373 }
% 12.47/12.80 407 : pppp21-{T}(E0,E1) { 0, 1, 18, 60, 105, 137, 167, 194, 223, 247, 271, 293, 311, 328, 343, 355, 364, 374 }
% 12.47/12.80 408 : pppp3-{T}(E1,E1) { 0, 19, 61, 106, 138, 168, 197, 224, 248, 272, 295, 313, 331, 345, 357, 367, 375 }
% 12.47/12.80 409 : pppp37-{T}(E1,E1) { 0, 17, 59, 103, 135, 165, 193, 221, 245, 269, 290, 308, 327, 340, 352, 363, 370, 376 }
% 12.57/12.81 410 : pppp3-{T}(E0,E0) { 0, 1, 19, 61, 106, 138, 168, 197, 224, 248, 272, 295, 313, 331, 345, 357, 367, 377 }
% 12.57/12.81 411 : pppp37-{T}(E0,E0) { 0, 1, 17, 59, 103, 135, 165, 193, 221, 245, 269, 290, 308, 327, 340, 352, 363, 370, 378 }
% 12.57/12.81 412 : pppp20-{T}(E1,E1) { 0, 18, 60, 105, 137, 167, 194, 223, 247, 271, 293, 311, 328, 343, 355, 364, 373, 379 }
% 12.57/12.81 413 : pppp209-{T}(E1) { 0, 18, 60, 105, 137, 167, 194, 223, 247, 271, 293, 311, 328, 343, 355, 364, 373, 379 }
% 12.57/12.81 414 : pppp209-{T}(E0) { 0, 1, 18, 60, 105, 137, 167, 194, 223, 247, 271, 293, 311, 328, 343, 355, 364, 373, 379 }
% 12.57/12.81 415 : pppp20-{T}(E1,E0) { 0, 1, 18, 60, 105, 137, 167, 194, 223, 247, 271, 293, 311, 328, 343, 355, 364, 373, 380 }
% 12.57/12.81 416 : pppp2-{T}(E1,E1) { 0, 19, 61, 106, 138, 168, 197, 224, 248, 272, 295, 313, 331, 345, 357, 367, 375, 381 }
% 12.57/12.81 417 : pppp19-{T}(E1,E1) { 0, 18, 60, 105, 137, 167, 194, 223, 247, 271, 293, 311, 328, 343, 355, 364, 373, 379, 382 }
% 12.57/12.81 418 : pppp2-{T}(E0,E0) { 0, 1, 19, 61, 106, 138, 168, 197, 224, 248, 272, 295, 313, 331, 345, 357, 367, 375, 383 }
% 12.57/12.81 419 : pppp19-{T}(E1,E0) { 0, 1, 18, 60, 105, 137, 167, 194, 223, 247, 271, 293, 311, 328, 343, 355, 364, 373, 379, 384 }
% 12.57/12.81 420 : pppp1-{T}(E1,E1) { 0, 19, 61, 106, 138, 168, 197, 224, 248, 272, 295, 313, 331, 345, 357, 367, 375, 381, 385 }
% 12.57/12.81 421 : pppp1-{T}(E0,E0) { 0, 1, 19, 61, 106, 138, 168, 197, 224, 248, 272, 295, 313, 331, 345, 357, 367, 375, 381, 386 }
% 12.57/12.81 422 : pppp210-{T}(E1) { 0, 19, 61, 106, 138, 168, 197, 224, 248, 272, 295, 313, 331, 345, 357, 367, 375, 381, 385, 387 }
% 12.57/12.81 423 : pppp210-{T}(E0) { 0, 1, 19, 61, 106, 138, 168, 197, 224, 248, 272, 295, 313, 331, 345, 357, 367, 375, 381, 385, 388 }
% 12.57/12.81 424 : pppp0-{T}(E1,E1) { 0, 19, 61, 106, 138, 168, 197, 224, 248, 272, 295, 313, 331, 345, 357, 367, 375, 381, 385, 387, 389 }
% 12.57/12.81 425 : pppp0-{T}(E0,E0) { 0, 1, 19, 61, 106, 138, 168, 197, 224, 248, 272, 295, 313, 331, 345, 357, 367, 375, 381, 385, 388, 390 }
% 12.57/12.81
% 12.57/12.81
% 12.57/12.81 % SZS output end Model for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.57/12.81
% 12.57/12.81 randbase = 1
%------------------------------------------------------------------------------