From 6c3adf6a75239adaec4ece3e91fe7efba83f69a3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 16 Jun 2006 09:03:24 +0000 Subject: [PATCH] added log.120.orsay.txt and comparison --- .../matita/tests/TPTP/log.120.orsay.txt | 698 ++++++++++++++++++ ...og.300.26-5.menvcorti_VS_log.120.orsay.ods | Bin 0 -> 37636 bytes helm/software/matita/tests/TPTP/try.sh | 6 +- 3 files changed, 702 insertions(+), 2 deletions(-) create mode 100644 helm/software/matita/tests/TPTP/log.120.orsay.txt create mode 100644 helm/software/matita/tests/TPTP/log.300.26-5.menvcorti_VS_log.120.orsay.ods diff --git a/helm/software/matita/tests/TPTP/log.120.orsay.txt b/helm/software/matita/tests/TPTP/log.120.orsay.txt new file mode 100644 index 000000000..2bf838a67 --- /dev/null +++ b/helm/software/matita/tests/TPTP/log.120.orsay.txt @@ -0,0 +1,698 @@ +Unsatisfiable/ALG005-1.ma ... OK TIME NEEDED: 31.22 Rating : 0.07 1 +Unsatisfiable/ALG006-1.ma ... OK TIME NEEDED: 2.24 Rating : 0.00 2 +Unsatisfiable/ALG007-1.ma ... OK TIME NEEDED: 3.39 Rating : 0.00 3 +Unsatisfiable/BOO001-1.ma ... OK TIME NEEDED: 0.98 Rating : 0.00 4 +Unsatisfiable/BOO002-1.ma ... OK TIME NEEDED: 9.58 Rating : 0.07 5 +Unsatisfiable/BOO002-2.ma ... OK TIME NEEDED: 6.35 Rating : 0.00 6 +Unsatisfiable/BOO003-2.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 7 +Unsatisfiable/BOO003-4.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 8 +Unsatisfiable/BOO004-2.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 9 +Unsatisfiable/BOO004-4.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 10 +Unsatisfiable/BOO005-2.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 11 +Unsatisfiable/BOO005-4.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 12 +Unsatisfiable/BOO006-2.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 13 +Unsatisfiable/BOO006-4.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 14 +Unsatisfiable/BOO007-2.ma ... FAIL Rating : 0.14 15 +Unsatisfiable/BOO007-4.ma ... OK TIME NEEDED: 63.00 Rating : 0.07 16 +Unsatisfiable/BOO008-2.ma ... FAIL Rating : 0.07 17 +Unsatisfiable/BOO008-4.ma ... OK TIME NEEDED: 23.48 Rating : 0.00 18 +Unsatisfiable/BOO009-2.ma ... OK TIME NEEDED: 0.17 Rating : 0.00 19 +Unsatisfiable/BOO009-4.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 20 +Unsatisfiable/BOO010-2.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 21 +Unsatisfiable/BOO010-4.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 22 +Unsatisfiable/BOO011-2.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 23 +Unsatisfiable/BOO011-4.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 24 +Unsatisfiable/BOO012-2.ma ... OK TIME NEEDED: 0.26 Rating : 0.00 25 +Unsatisfiable/BOO012-4.ma ... OK TIME NEEDED: 0.35 Rating : 0.00 26 +Unsatisfiable/BOO013-2.ma ... OK TIME NEEDED: 0.31 Rating : 0.00 27 +Unsatisfiable/BOO013-4.ma ... OK TIME NEEDED: 0.55 Rating : 0.00 28 +Unsatisfiable/BOO014-2.ma ... OK TIME NEEDED: 3.38 Rating : 0.00 29 +Unsatisfiable/BOO014-4.ma ... OK TIME NEEDED: 16.30 Rating : 0.00 30 +Unsatisfiable/BOO015-2.ma ... OK TIME NEEDED: 1.98 Rating : 0.00 31 +Unsatisfiable/BOO015-4.ma ... OK TIME NEEDED: 16.72 Rating : 0.00 32 +Unsatisfiable/BOO016-2.ma ... OK TIME NEEDED: 0.23 Rating : 0.00 33 +Unsatisfiable/BOO017-2.ma ... OK TIME NEEDED: 0.51 Rating : 0.00 34 +Unsatisfiable/BOO018-4.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 35 +Unsatisfiable/BOO021-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.07 36 +Unsatisfiable/BOO022-1.ma ... FAIL Rating : 0.07 37 +Unsatisfiable/BOO023-1.ma ... FAIL Rating : 0.50 38 +Unsatisfiable/BOO024-1.ma ... OK TIME NEEDED: 2.11 Rating : 0.00 39 +Unsatisfiable/BOO025-1.ma ... OK TIME NEEDED: 4.28 Rating : 0.07 40 +Unsatisfiable/BOO026-1.ma ... OK Rating : 0.07 41 +Unsatisfiable/BOO028-1.ma ... FAIL Rating : 0.07 42 +Unsatisfiable/BOO029-1.ma ... OK TIME NEEDED: 85.32 Rating : 0.00 43 +Unsatisfiable/BOO031-1.ma ... FAIL Rating : 0.21 44 +Unsatisfiable/BOO034-1.ma ... OK TIME NEEDED: 16.86 Rating : 0.21 45 +Unsatisfiable/BOO067-1.ma ... FAIL Rating : 0.21 46 +Unsatisfiable/BOO068-1.ma ... OK TIME NEEDED: 1.54 Rating : 0.00 47 +Unsatisfiable/BOO069-1.ma ... OK TIME NEEDED: 0.82 Rating : 0.00 48 +Unsatisfiable/BOO070-1.ma ... OK TIME NEEDED: 1.74 Rating : 0.00 49 +Unsatisfiable/BOO071-1.ma ... OK TIME NEEDED: 0.82 Rating : 0.00 50 +Unsatisfiable/BOO072-1.ma ... FAIL Rating : 0.07 51 +Unsatisfiable/BOO073-1.ma ... FAIL Rating : 0.36 52 +Unsatisfiable/BOO074-1.ma ... FAIL Rating : 0.07 53 +Unsatisfiable/BOO075-1.ma ... OK TIME NEEDED: 0.61 Rating : 0.00 54 +Unsatisfiable/BOO076-1.ma ... FAIL Rating : 0.71 55 +Unsatisfiable/COL001-1.ma ... OK TIME NEEDED: 79.85 Rating : 0.07 56 +Unsatisfiable/COL001-2.ma ... OK TIME NEEDED: 5.70 Rating : 0.07 57 +Unsatisfiable/COL002-1.ma ... OK TIME NEEDED: 2.99 Rating : 0.00 58 +Unsatisfiable/COL002-4.ma ... FAIL Rating : 0.07 59 +Unsatisfiable/COL002-5.ma ... FAIL Rating : 0.43 60 +Unsatisfiable/COL003-1.ma ... FAIL Rating : 0.79 61 +Unsatisfiable/COL004-1.ma ... FAIL Rating : 0.57 62 +Unsatisfiable/COL004-3.ma ... OK TIME NEEDED: 0.01 Rating : 0.21 63 +Unsatisfiable/COL006-1.ma ... FAIL Rating : 0.57 64 +Unsatisfiable/COL006-5.ma ... FAIL Rating : 0.64 65 +Unsatisfiable/COL006-6.ma ... FAIL Rating : 0.64 66 +Unsatisfiable/COL006-7.ma ... FAIL Rating : 0.64 67 +Unsatisfiable/COL007-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 68 +Unsatisfiable/COL008-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 69 +Unsatisfiable/COL009-1.ma ... OK TIME NEEDED: 5.59 Rating : 0.07 70 +Unsatisfiable/COL010-1.ma ... OK TIME NEEDED: 1.01 Rating : 0.07 71 +Unsatisfiable/COL011-1.ma ... FAIL Rating : 0.36 72 +Unsatisfiable/COL012-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 73 +Unsatisfiable/COL013-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 74 +Unsatisfiable/COL014-1.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 75 +Unsatisfiable/COL015-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 76 +Unsatisfiable/COL016-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 77 +Unsatisfiable/COL017-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 78 +Unsatisfiable/COL018-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 79 +Unsatisfiable/COL019-1.ma ... FAIL Rating : 0.00 80 +Unsatisfiable/COL020-1.ma ... FAIL Rating : 0.07 81 +Unsatisfiable/COL021-1.ma ... OK TIME NEEDED: 0.28 Rating : 0.00 82 +Unsatisfiable/COL022-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 83 +Unsatisfiable/COL023-1.ma ... FAIL Rating : 0.00 84 +Unsatisfiable/COL024-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 85 +Unsatisfiable/COL025-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 86 +Unsatisfiable/COL026-1.ma ... FAIL Rating : 0.07 87 +Unsatisfiable/COL027-1.ma ... FAIL Rating : 0.00 88 +Unsatisfiable/COL029-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 89 +Unsatisfiable/COL030-1.ma ... OK TIME NEEDED: 0.26 Rating : 0.14 90 +Unsatisfiable/COL031-1.ma ... OK TIME NEEDED: 0.12 Rating : 0.00 91 +Unsatisfiable/COL032-1.ma ... FAIL Rating : 0.14 92 +Unsatisfiable/COL033-1.ma ... FAIL Rating : 0.07 93 +Unsatisfiable/COL034-1.ma ... FAIL Rating : 0.43 94 +Unsatisfiable/COL035-1.ma ... FAIL Rating : 0.14 95 +Unsatisfiable/COL036-1.ma ... FAIL Rating : 0.57 96 +Unsatisfiable/COL037-1.ma ... FAIL Rating : 0.29 97 +Unsatisfiable/COL038-1.ma ... FAIL Rating : 0.64 98 +Unsatisfiable/COL039-1.ma ... FAIL Rating : 0.00 99 +Unsatisfiable/COL041-1.ma ... FAIL Rating : 0.36 100 +Unsatisfiable/COL042-1.ma ... FAIL Rating : 0.86 101 +Unsatisfiable/COL042-6.ma ... FAIL Rating : 0.14 102 +Unsatisfiable/COL042-7.ma ... FAIL Rating : 0.14 103 +Unsatisfiable/COL042-8.ma ... FAIL Rating : 0.14 104 +Unsatisfiable/COL042-9.ma ... FAIL Rating : 0.14 105 +Unsatisfiable/COL043-1.ma ... FAIL Rating : 0.86 106 +Unsatisfiable/COL043-3.ma ... FAIL Rating : 0.71 107 +Unsatisfiable/COL044-1.ma ... FAIL Rating : 0.21 108 +Unsatisfiable/COL044-6.ma ... FAIL Rating : 0.64 109 +Unsatisfiable/COL044-7.ma ... FAIL Rating : 0.50 110 +Unsatisfiable/COL044-8.ma ... FAIL Rating : 0.71 111 +Unsatisfiable/COL044-9.ma ... FAIL Rating : 0.64 112 +Unsatisfiable/COL045-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 113 +Unsatisfiable/COL046-1.ma ... FAIL Rating : 0.64 114 +Unsatisfiable/COL048-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 115 +Unsatisfiable/COL049-1.ma ... FAIL Rating : 0.29 116 +Unsatisfiable/COL050-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 117 +Unsatisfiable/COL051-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 118 +Unsatisfiable/COL052-1.ma ... FAIL Rating : 0.00 119 +Unsatisfiable/COL053-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 120 +Unsatisfiable/COL056-1.ma ... FAIL Rating : 0.07 121 +Unsatisfiable/COL057-1.ma ... FAIL Rating : 0.36 122 +Unsatisfiable/COL058-1.ma ... FAIL Rating : 0.00 123 +Unsatisfiable/COL058-2.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 124 +Unsatisfiable/COL058-3.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 125 +Unsatisfiable/COL059-1.ma ... FAIL Rating : 0.00 126 +Unsatisfiable/COL060-1.ma ... FAIL Rating : 0.36 127 +Unsatisfiable/COL060-2.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 128 +Unsatisfiable/COL060-3.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 129 +Unsatisfiable/COL061-1.ma ... FAIL Rating : 0.36 130 +Unsatisfiable/COL061-2.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 131 +Unsatisfiable/COL061-3.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 132 +Unsatisfiable/COL062-1.ma ... FAIL Rating : 0.50 133 +Unsatisfiable/COL062-2.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 134 +Unsatisfiable/COL062-3.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 135 +Unsatisfiable/COL063-1.ma ... FAIL Rating : 0.50 136 +Unsatisfiable/COL063-2.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 137 +Unsatisfiable/COL063-3.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 138 +Unsatisfiable/COL063-4.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 139 +Unsatisfiable/COL063-5.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 140 +Unsatisfiable/COL063-6.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 141 +Unsatisfiable/COL064-1.ma ... FAIL Rating : 0.64 142 +Unsatisfiable/COL064-2.ma ... OK TIME NEEDED: 0.00 Rating : 0.07 143 +Unsatisfiable/COL064-3.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 144 +Unsatisfiable/COL064-4.ma ... OK TIME NEEDED: 0.00 Rating : 0.07 145 +Unsatisfiable/COL064-5.ma ... OK TIME NEEDED: 0.00 Rating : 0.07 146 +Unsatisfiable/COL064-6.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 147 +Unsatisfiable/COL064-7.ma ... OK TIME NEEDED: 0.00 Rating : 0.07 148 +Unsatisfiable/COL064-8.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 149 +Unsatisfiable/COL064-9.ma ... OK TIME NEEDED: 0.00 Rating : 0.07 150 +Unsatisfiable/COL065-1.ma ... FAIL Rating : 0.71 151 +Unsatisfiable/COL066-1.ma ... FAIL Rating : 0.93 152 +Unsatisfiable/COL066-2.ma ... OK TIME NEEDED: 1.31 Rating : 0.00 153 +Unsatisfiable/COL066-3.ma ... OK TIME NEEDED: 1.31 Rating : 0.00 154 +Unsatisfiable/COL070-1.ma ... FAIL Rating : 0.07 155 +Unsatisfiable/COL075-2.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 156 +Unsatisfiable/COL083-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 157 +Unsatisfiable/COL084-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 158 +Unsatisfiable/COL085-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 159 +Unsatisfiable/COL086-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 160 +Unsatisfiable/GRP001-2.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 161 +Unsatisfiable/GRP001-4.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 162 +Unsatisfiable/GRP002-2.ma ... OK TIME NEEDED: 7.77 Rating : 0.00 163 +Unsatisfiable/GRP002-3.ma ... OK TIME NEEDED: 13.93 Rating : 0.00 164 +Unsatisfiable/GRP002-4.ma ... OK TIME NEEDED: 12.69 Rating : 0.00 165 +Unsatisfiable/GRP010-4.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 166 +Unsatisfiable/GRP011-4.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 167 +Unsatisfiable/GRP012-4.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 168 +Unsatisfiable/GRP014-1.ma ... FAIL Rating : 0.14 169 +Unsatisfiable/GRP022-2.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 170 +Unsatisfiable/GRP023-2.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 171 +Unsatisfiable/GRP024-5.ma ... FAIL Rating : 0.50 172 +Unsatisfiable/GRP114-1.ma ... OK TIME NEEDED: 8.76 Rating : 0.29 173 +Unsatisfiable/GRP115-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 174 +Unsatisfiable/GRP116-1.ma ... OK TIME NEEDED: 0.62 Rating : 0.00 175 +Unsatisfiable/GRP117-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 176 +Unsatisfiable/GRP118-1.ma ... OK TIME NEEDED: 0.40 Rating : 0.00 177 +Unsatisfiable/GRP119-1.ma ... OK TIME NEEDED: 37.45 Rating : 0.00 178 +Unsatisfiable/GRP120-1.ma ... OK TIME NEEDED: 54.47 Rating : 0.00 179 +Unsatisfiable/GRP121-1.ma ... OK TIME NEEDED: 37.92 Rating : 0.00 180 +Unsatisfiable/GRP122-1.ma ... OK Rating : 0.07 181 +Unsatisfiable/GRP136-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 182 +Unsatisfiable/GRP137-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 183 +Unsatisfiable/GRP138-1.ma ... OK TIME NEEDED: 1.85 Rating : 0.00 184 +Unsatisfiable/GRP139-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 185 +Unsatisfiable/GRP140-1.ma ... OK TIME NEEDED: 2.00 Rating : 0.00 186 +Unsatisfiable/GRP141-1.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 187 +Unsatisfiable/GRP142-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 188 +Unsatisfiable/GRP143-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 189 +Unsatisfiable/GRP144-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 190 +Unsatisfiable/GRP145-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 191 +Unsatisfiable/GRP146-1.ma ... OK TIME NEEDED: 0.15 Rating : 0.00 192 +Unsatisfiable/GRP147-1.ma ... OK TIME NEEDED: 1.11 Rating : 0.00 193 +Unsatisfiable/GRP148-1.ma ... OK TIME NEEDED: 0.86 Rating : 0.00 194 +Unsatisfiable/GRP149-1.ma ... OK TIME NEEDED: 0.15 Rating : 0.00 195 +Unsatisfiable/GRP150-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 196 +Unsatisfiable/GRP151-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 197 +Unsatisfiable/GRP152-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 198 +Unsatisfiable/GRP153-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 199 +Unsatisfiable/GRP154-1.ma ... OK TIME NEEDED: 0.25 Rating : 0.00 200 +Unsatisfiable/GRP155-1.ma ... OK TIME NEEDED: 0.33 Rating : 0.00 201 +Unsatisfiable/GRP156-1.ma ... OK TIME NEEDED: 0.36 Rating : 0.00 202 +Unsatisfiable/GRP157-1.ma ... OK TIME NEEDED: 0.15 Rating : 0.00 203 +Unsatisfiable/GRP158-1.ma ... OK TIME NEEDED: 0.19 Rating : 0.00 204 +Unsatisfiable/GRP159-1.ma ... OK TIME NEEDED: 0.14 Rating : 0.00 205 +Unsatisfiable/GRP160-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 206 +Unsatisfiable/GRP161-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 207 +Unsatisfiable/GRP162-1.ma ... OK TIME NEEDED: 0.16 Rating : 0.00 208 +Unsatisfiable/GRP163-1.ma ... OK TIME NEEDED: 0.22 Rating : 0.00 209 +Unsatisfiable/GRP164-1.ma ... FAIL Rating : 0.93 210 +Unsatisfiable/GRP164-2.ma ... FAIL Rating : 0.93 211 +Unsatisfiable/GRP165-1.ma ... FAIL Rating : 0.00 212 +Unsatisfiable/GRP165-2.ma ... FAIL Rating : 0.00 213 +Unsatisfiable/GRP166-1.ma ... OK TIME NEEDED: 6.44 Rating : 0.00 214 +Unsatisfiable/GRP166-2.ma ... OK TIME NEEDED: 3.78 Rating : 0.00 215 +Unsatisfiable/GRP166-3.ma ... FAIL Rating : 0.00 216 +Unsatisfiable/GRP166-4.ma ... FAIL Rating : 0.00 217 +Unsatisfiable/GRP167-1.ma ... OK TIME NEEDED: 3.08 Rating : 0.21 218 +Unsatisfiable/GRP167-2.ma ... OK TIME NEEDED: 3.04 Rating : 0.21 219 +Unsatisfiable/GRP167-3.ma ... FAIL Rating : 0.50 220 +Unsatisfiable/GRP167-4.ma ... FAIL Rating : 0.43 221 +Unsatisfiable/GRP167-5.ma ... OK TIME NEEDED: 0.73 Rating : 0.14 222 +Unsatisfiable/GRP168-1.ma ... OK TIME NEEDED: 0.26 Rating : 0.07 223 +Unsatisfiable/GRP168-2.ma ... OK TIME NEEDED: 0.36 Rating : 0.07 224 +Unsatisfiable/GRP169-1.ma ... OK TIME NEEDED: 53.35 Rating : 0.00 225 +Unsatisfiable/GRP169-2.ma ... OK TIME NEEDED: 53.41 Rating : 0.00 226 +Unsatisfiable/GRP170-1.ma ... FAIL Rating : 0.00 227 +Unsatisfiable/GRP170-2.ma ... FAIL Rating : 0.00 228 +Unsatisfiable/GRP170-3.ma ... FAIL Rating : 0.00 229 +Unsatisfiable/GRP170-4.ma ... FAIL Rating : 0.00 230 +Unsatisfiable/GRP171-1.ma ... OK TIME NEEDED: 0.34 Rating : 0.00 231 +Unsatisfiable/GRP171-2.ma ... OK TIME NEEDED: 0.36 Rating : 0.00 232 +Unsatisfiable/GRP172-1.ma ... OK TIME NEEDED: 0.47 Rating : 0.00 233 +Unsatisfiable/GRP172-2.ma ... OK TIME NEEDED: 0.42 Rating : 0.00 234 +Unsatisfiable/GRP173-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 235 +Unsatisfiable/GRP174-1.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 236 +Unsatisfiable/GRP175-1.ma ... FAIL Rating : 0.00 237 +Unsatisfiable/GRP175-2.ma ... FAIL Rating : 0.00 238 +Unsatisfiable/GRP175-3.ma ... FAIL Rating : 0.00 239 +Unsatisfiable/GRP175-4.ma ... FAIL Rating : 0.00 240 +Unsatisfiable/GRP176-1.ma ... OK TIME NEEDED: 0.29 Rating : 0.00 241 +Unsatisfiable/GRP176-2.ma ... OK TIME NEEDED: 0.30 Rating : 0.00 242 +Unsatisfiable/GRP177-2.ma ... FAIL Rating : 0.21 243 +Unsatisfiable/GRP178-1.ma ... FAIL Rating : 0.14 244 +Unsatisfiable/GRP178-2.ma ... FAIL Rating : 0.14 245 +Unsatisfiable/GRP179-1.ma ... FAIL Rating : 0.50 246 +Unsatisfiable/GRP179-2.ma ... FAIL Rating : 0.50 247 +Unsatisfiable/GRP179-3.ma ... FAIL Rating : 0.36 248 +Unsatisfiable/GRP180-1.ma ... FAIL Rating : 0.50 249 +Unsatisfiable/GRP180-2.ma ... FAIL Rating : 0.43 250 +Unsatisfiable/GRP181-1.ma ... FAIL Rating : 0.71 251 +Unsatisfiable/GRP181-2.ma ... FAIL Rating : 0.71 252 +Unsatisfiable/GRP181-3.ma ... OK TIME NEEDED: 1.55 Rating : 0.43 253 +Unsatisfiable/GRP181-4.ma ... OK TIME NEEDED: 3.54 Rating : 0.43 254 +Unsatisfiable/GRP182-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 255 +Unsatisfiable/GRP182-2.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 256 +Unsatisfiable/GRP182-3.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 257 +Unsatisfiable/GRP182-4.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 258 +Unsatisfiable/GRP183-1.ma ... FAIL Rating : 0.43 259 +Unsatisfiable/GRP183-2.ma ... FAIL Rating : 0.43 260 +Unsatisfiable/GRP183-3.ma ... FAIL Rating : 0.43 261 +Unsatisfiable/GRP183-4.ma ... FAIL Rating : 0.36 262 +Unsatisfiable/GRP184-1.ma ... FAIL Rating : 0.29 263 +Unsatisfiable/GRP184-2.ma ... FAIL Rating : 0.14 264 +Unsatisfiable/GRP184-3.ma ... FAIL Rating : 0.21 265 +Unsatisfiable/GRP184-4.ma ... FAIL Rating : 0.00 266 +Unsatisfiable/GRP185-1.ma ... FAIL Rating : 0.07 267 +Unsatisfiable/GRP185-2.ma ... FAIL Rating : 0.07 268 +Unsatisfiable/GRP185-3.ma ... FAIL Rating : 0.21 269 +Unsatisfiable/GRP185-4.ma ... FAIL Rating : 0.21 270 +Unsatisfiable/GRP186-1.ma ... FAIL Rating : 0.57 271 +Unsatisfiable/GRP186-2.ma ... FAIL Rating : 0.36 272 +Unsatisfiable/GRP186-3.ma ... OK TIME NEEDED: 0.17 Rating : 0.00 273 +Unsatisfiable/GRP186-4.ma ... OK TIME NEEDED: 0.20 Rating : 0.00 274 +Unsatisfiable/GRP187-1.ma ... FAIL Rating : 0.64 275 +Unsatisfiable/GRP188-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 276 +Unsatisfiable/GRP188-2.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 277 +Unsatisfiable/GRP189-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 278 +Unsatisfiable/GRP189-2.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 279 +Unsatisfiable/GRP190-1.ma ... OK TIME NEEDED: 109.81 Rating : 0.00 280 +Unsatisfiable/GRP190-2.ma ... OK TIME NEEDED: 109.16 Rating : 0.00 281 +Unsatisfiable/GRP191-1.ma ... OK TIME NEEDED: 108.35 Rating : 0.00 282 +Unsatisfiable/GRP191-2.ma ... OK TIME NEEDED: 108.91 Rating : 0.00 283 +Unsatisfiable/GRP192-1.ma ... OK TIME NEEDED: 0.17 Rating : 0.07 284 +Unsatisfiable/GRP193-1.ma ... FAIL Rating : 0.00 285 +Unsatisfiable/GRP193-2.ma ... FAIL Rating : 0.00 286 +Unsatisfiable/GRP195-1.ma ... FAIL Rating : 0.00 287 +Unsatisfiable/GRP196-1.ma ... FAIL Rating : 0.93 288 +Unsatisfiable/GRP200-1.ma ... FAIL Rating : 0.29 289 +Unsatisfiable/GRP201-1.ma ... FAIL Rating : 0.36 290 +Unsatisfiable/GRP202-1.ma ... FAIL Rating : 0.43 291 +Unsatisfiable/GRP203-1.ma ... FAIL Rating : 0.21 292 +Unsatisfiable/GRP205-1.ma ... FAIL Rating : 0.43 293 +Unsatisfiable/GRP206-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 294 +Unsatisfiable/GRP403-1.ma ... OK TIME NEEDED: 48.77 Rating : 0.07 295 +Unsatisfiable/GRP404-1.ma ... FAIL Rating : 0.21 296 +Unsatisfiable/GRP405-1.ma ... FAIL Rating : 0.21 297 +Unsatisfiable/GRP406-1.ma ... FAIL Rating : 0.00 298 +Unsatisfiable/GRP407-1.ma ... FAIL Rating : 0.00 299 +Unsatisfiable/GRP408-1.ma ... FAIL Rating : 0.00 300 +Unsatisfiable/GRP409-1.ma ... OK TIME NEEDED: 7.50 Rating : 0.00 301 +Unsatisfiable/GRP410-1.ma ... OK TIME NEEDED: 12.23 Rating : 0.21 302 +Unsatisfiable/GRP411-1.ma ... OK TIME NEEDED: 13.76 Rating : 0.21 303 +Unsatisfiable/GRP412-1.ma ... OK TIME NEEDED: 105.80 Rating : 0.00 304 +Unsatisfiable/GRP413-1.ma ... FAIL Rating : 0.07 305 +Unsatisfiable/GRP414-1.ma ... FAIL Rating : 0.07 306 +Unsatisfiable/GRP415-1.ma ... FAIL Rating : 0.00 307 +Unsatisfiable/GRP416-1.ma ... FAIL Rating : 0.07 308 +Unsatisfiable/GRP417-1.ma ... FAIL Rating : 0.14 309 +Unsatisfiable/GRP418-1.ma ... FAIL Rating : 0.07 310 +Unsatisfiable/GRP419-1.ma ... FAIL Rating : 0.29 311 +Unsatisfiable/GRP420-1.ma ... FAIL Rating : 0.36 312 +Unsatisfiable/GRP421-1.ma ... FAIL Rating : 0.14 313 +Unsatisfiable/GRP422-1.ma ... FAIL Rating : 0.29 314 +Unsatisfiable/GRP423-1.ma ... FAIL Rating : 0.36 315 +Unsatisfiable/GRP424-1.ma ... OK TIME NEEDED: 20.70 Rating : 0.00 316 +Unsatisfiable/GRP425-1.ma ... OK TIME NEEDED: 21.22 Rating : 0.07 317 +Unsatisfiable/GRP426-1.ma ... FAIL Rating : 0.14 318 +Unsatisfiable/GRP427-1.ma ... FAIL Rating : 0.00 319 +Unsatisfiable/GRP428-1.ma ... FAIL Rating : 0.00 320 +Unsatisfiable/GRP429-1.ma ... FAIL Rating : 0.14 321 +Unsatisfiable/GRP430-1.ma ... OK TIME NEEDED: 32.43 Rating : 0.00 322 +Unsatisfiable/GRP431-1.ma ... OK TIME NEEDED: 29.82 Rating : 0.00 323 +Unsatisfiable/GRP432-1.ma ... OK TIME NEEDED: 35.35 Rating : 0.00 324 +Unsatisfiable/GRP433-1.ma ... FAIL Rating : 0.00 325 +Unsatisfiable/GRP434-1.ma ... FAIL Rating : 0.00 326 +Unsatisfiable/GRP435-1.ma ... FAIL Rating : 0.00 327 +Unsatisfiable/GRP436-1.ma ... OK Rating : 0.07 328 +Unsatisfiable/GRP437-1.ma ... OK Rating : 0.07 329 +Unsatisfiable/GRP438-1.ma ... OK Rating : 0.07 330 +Unsatisfiable/GRP439-1.ma ... OK TIME NEEDED: 33.82 Rating : 0.07 331 +Unsatisfiable/GRP440-1.ma ... FAIL Rating : 0.14 332 +Unsatisfiable/GRP441-1.ma ... FAIL Rating : 0.21 333 +Unsatisfiable/GRP442-1.ma ... FAIL Rating : 0.14 334 +Unsatisfiable/GRP443-1.ma ... FAIL Rating : 0.07 335 +Unsatisfiable/GRP444-1.ma ... FAIL Rating : 0.21 336 +Unsatisfiable/GRP445-1.ma ... OK TIME NEEDED: 0.20 Rating : 0.00 337 +Unsatisfiable/GRP446-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 338 +Unsatisfiable/GRP447-1.ma ... OK TIME NEEDED: 0.91 Rating : 0.14 339 +Unsatisfiable/GRP448-1.ma ... OK TIME NEEDED: 0.21 Rating : 0.00 340 +Unsatisfiable/GRP449-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 341 +Unsatisfiable/GRP450-1.ma ... OK TIME NEEDED: 0.88 Rating : 0.07 342 +Unsatisfiable/GRP451-1.ma ... OK TIME NEEDED: 0.16 Rating : 0.00 343 +Unsatisfiable/GRP452-1.ma ... OK TIME NEEDED: 1.67 Rating : 0.14 344 +Unsatisfiable/GRP453-1.ma ... OK TIME NEEDED: 3.25 Rating : 0.21 345 +Unsatisfiable/GRP454-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 346 +Unsatisfiable/GRP455-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 347 +Unsatisfiable/GRP456-1.ma ... OK TIME NEEDED: 0.26 Rating : 0.07 348 +Unsatisfiable/GRP457-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 349 +Unsatisfiable/GRP458-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 350 +Unsatisfiable/GRP459-1.ma ... OK TIME NEEDED: 0.27 Rating : 0.00 351 +Unsatisfiable/GRP460-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 352 +Unsatisfiable/GRP461-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 353 +Unsatisfiable/GRP462-1.ma ... OK TIME NEEDED: 0.32 Rating : 0.00 354 +Unsatisfiable/GRP463-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 355 +Unsatisfiable/GRP464-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 356 +Unsatisfiable/GRP465-1.ma ... OK TIME NEEDED: 0.32 Rating : 0.00 357 +Unsatisfiable/GRP466-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 358 +Unsatisfiable/GRP467-1.ma ... OK TIME NEEDED: 0.46 Rating : 0.00 359 +Unsatisfiable/GRP468-1.ma ... OK TIME NEEDED: 3.08 Rating : 0.00 360 +Unsatisfiable/GRP469-1.ma ... FAIL Rating : 0.21 361 +Unsatisfiable/GRP470-1.ma ... FAIL Rating : 0.21 362 +Unsatisfiable/GRP471-1.ma ... FAIL Rating : 0.21 363 +Unsatisfiable/GRP472-1.ma ... OK TIME NEEDED: 71.72 Rating : 0.07 364 +Unsatisfiable/GRP473-1.ma ... OK TIME NEEDED: 67.69 Rating : 0.07 365 +Unsatisfiable/GRP474-1.ma ... OK TIME NEEDED: 92.99 Rating : 0.07 366 +Unsatisfiable/GRP475-1.ma ... OK TIME NEEDED: 89.99 Rating : 0.21 367 +Unsatisfiable/GRP476-1.ma ... OK TIME NEEDED: 89.69 Rating : 0.21 368 +Unsatisfiable/GRP477-1.ma ... OK TIME NEEDED: 94.31 Rating : 0.21 369 +Unsatisfiable/GRP478-1.ma ... OK TIME NEEDED: 28.41 Rating : 0.14 370 +Unsatisfiable/GRP479-1.ma ... OK TIME NEEDED: 24.83 Rating : 0.14 371 +Unsatisfiable/GRP480-1.ma ... OK TIME NEEDED: 35.92 Rating : 0.21 372 +Unsatisfiable/GRP481-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 373 +Unsatisfiable/GRP482-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 374 +Unsatisfiable/GRP483-1.ma ... OK TIME NEEDED: 0.58 Rating : 0.00 375 +Unsatisfiable/GRP484-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 376 +Unsatisfiable/GRP485-1.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 377 +Unsatisfiable/GRP486-1.ma ... OK TIME NEEDED: 0.68 Rating : 0.00 378 +Unsatisfiable/GRP487-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 379 +Unsatisfiable/GRP488-1.ma ... OK TIME NEEDED: 0.85 Rating : 0.00 380 +Unsatisfiable/GRP489-1.ma ... OK TIME NEEDED: 1.76 Rating : 0.00 381 +Unsatisfiable/GRP490-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 382 +Unsatisfiable/GRP491-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 383 +Unsatisfiable/GRP492-1.ma ... OK TIME NEEDED: 0.42 Rating : 0.00 384 +Unsatisfiable/GRP493-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 385 +Unsatisfiable/GRP494-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 386 +Unsatisfiable/GRP495-1.ma ... OK TIME NEEDED: 0.33 Rating : 0.00 387 +Unsatisfiable/GRP496-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 388 +Unsatisfiable/GRP497-1.ma ... OK TIME NEEDED: 0.15 Rating : 0.00 389 +Unsatisfiable/GRP498-1.ma ... OK TIME NEEDED: 0.38 Rating : 0.00 390 +Unsatisfiable/GRP499-1.ma ... OK TIME NEEDED: 42.38 Rating : 0.00 391 +Unsatisfiable/GRP500-1.ma ... OK TIME NEEDED: 19.75 Rating : 0.07 392 +Unsatisfiable/GRP501-1.ma ... OK TIME NEEDED: 53.98 Rating : 0.14 393 +Unsatisfiable/GRP502-1.ma ... FAIL Rating : 0.14 394 +Unsatisfiable/GRP503-1.ma ... FAIL Rating : 0.14 395 +Unsatisfiable/GRP504-1.ma ... FAIL Rating : 0.14 396 +Unsatisfiable/GRP505-1.ma ... FAIL Rating : 0.50 397 +Unsatisfiable/GRP506-1.ma ... FAIL Rating : 0.64 398 +Unsatisfiable/GRP507-1.ma ... FAIL Rating : 0.57 399 +Unsatisfiable/GRP508-1.ma ... FAIL Rating : 0.57 400 +Unsatisfiable/GRP509-1.ma ... OK TIME NEEDED: 0.67 Rating : 0.00 401 +Unsatisfiable/GRP510-1.ma ... OK TIME NEEDED: 0.12 Rating : 0.00 402 +Unsatisfiable/GRP511-1.ma ... OK TIME NEEDED: 1.62 Rating : 0.00 403 +Unsatisfiable/GRP512-1.ma ... OK TIME NEEDED: 0.18 Rating : 0.00 404 +Unsatisfiable/GRP513-1.ma ... OK TIME NEEDED: 1.39 Rating : 0.00 405 +Unsatisfiable/GRP514-1.ma ... OK TIME NEEDED: 0.17 Rating : 0.00 406 +Unsatisfiable/GRP515-1.ma ... OK TIME NEEDED: 0.38 Rating : 0.00 407 +Unsatisfiable/GRP516-1.ma ... OK TIME NEEDED: 0.17 Rating : 0.00 408 +Unsatisfiable/GRP517-1.ma ... OK TIME NEEDED: 1.54 Rating : 0.00 409 +Unsatisfiable/GRP518-1.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 410 +Unsatisfiable/GRP519-1.ma ... OK TIME NEEDED: 2.18 Rating : 0.00 411 +Unsatisfiable/GRP520-1.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 412 +Unsatisfiable/GRP521-1.ma ... OK TIME NEEDED: 0.12 Rating : 0.00 413 +Unsatisfiable/GRP522-1.ma ... OK TIME NEEDED: 0.23 Rating : 0.00 414 +Unsatisfiable/GRP523-1.ma ... OK TIME NEEDED: 2.41 Rating : 0.00 415 +Unsatisfiable/GRP524-1.ma ... OK TIME NEEDED: 0.36 Rating : 0.00 416 +Unsatisfiable/GRP525-1.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 417 +Unsatisfiable/GRP526-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 418 +Unsatisfiable/GRP527-1.ma ... OK TIME NEEDED: 1.19 Rating : 0.00 419 +Unsatisfiable/GRP528-1.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 420 +Unsatisfiable/GRP529-1.ma ... OK TIME NEEDED: 0.07 Rating : 0.00 421 +Unsatisfiable/GRP530-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 422 +Unsatisfiable/GRP531-1.ma ... OK TIME NEEDED: 0.51 Rating : 0.00 423 +Unsatisfiable/GRP532-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 424 +Unsatisfiable/GRP533-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 425 +Unsatisfiable/GRP534-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 426 +Unsatisfiable/GRP535-1.ma ... OK TIME NEEDED: 0.73 Rating : 0.00 427 +Unsatisfiable/GRP536-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 428 +Unsatisfiable/GRP537-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 429 +Unsatisfiable/GRP538-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 430 +Unsatisfiable/GRP539-1.ma ... OK TIME NEEDED: 2.32 Rating : 0.00 431 +Unsatisfiable/GRP540-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 432 +Unsatisfiable/GRP541-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 433 +Unsatisfiable/GRP542-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 434 +Unsatisfiable/GRP543-1.ma ... OK TIME NEEDED: 0.35 Rating : 0.00 435 +Unsatisfiable/GRP544-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 436 +Unsatisfiable/GRP545-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 437 +Unsatisfiable/GRP546-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 438 +Unsatisfiable/GRP547-1.ma ... OK TIME NEEDED: 0.47 Rating : 0.00 439 +Unsatisfiable/GRP548-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 440 +Unsatisfiable/GRP549-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 441 +Unsatisfiable/GRP550-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.07 442 +Unsatisfiable/GRP551-1.ma ... OK TIME NEEDED: 0.37 Rating : 0.00 443 +Unsatisfiable/GRP552-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 444 +Unsatisfiable/GRP553-1.ma ... OK TIME NEEDED: 0.18 Rating : 0.00 445 +Unsatisfiable/GRP554-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 446 +Unsatisfiable/GRP555-1.ma ... OK TIME NEEDED: 3.47 Rating : 0.00 447 +Unsatisfiable/GRP556-1.ma ... OK TIME NEEDED: 0.67 Rating : 0.00 448 +Unsatisfiable/GRP557-1.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 449 +Unsatisfiable/GRP558-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 450 +Unsatisfiable/GRP559-1.ma ... OK TIME NEEDED: 2.54 Rating : 0.00 451 +Unsatisfiable/GRP560-1.ma ... OK TIME NEEDED: 0.20 Rating : 0.00 452 +Unsatisfiable/GRP561-1.ma ... OK TIME NEEDED: 0.17 Rating : 0.00 453 +Unsatisfiable/GRP562-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 454 +Unsatisfiable/GRP563-1.ma ... OK TIME NEEDED: 1.50 Rating : 0.00 455 +Unsatisfiable/GRP564-1.ma ... OK TIME NEEDED: 0.17 Rating : 0.00 456 +Unsatisfiable/GRP565-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 457 +Unsatisfiable/GRP566-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 458 +Unsatisfiable/GRP567-1.ma ... OK TIME NEEDED: 2.58 Rating : 0.14 459 +Unsatisfiable/GRP568-1.ma ... OK TIME NEEDED: 0.24 Rating : 0.14 460 +Unsatisfiable/GRP569-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 461 +Unsatisfiable/GRP570-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 462 +Unsatisfiable/GRP571-1.ma ... OK TIME NEEDED: 0.85 Rating : 0.14 463 +Unsatisfiable/GRP572-1.ma ... OK TIME NEEDED: 0.23 Rating : 0.07 464 +Unsatisfiable/GRP573-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 465 +Unsatisfiable/GRP574-1.ma ... OK TIME NEEDED: 0.17 Rating : 0.00 466 +Unsatisfiable/GRP575-1.ma ... OK TIME NEEDED: 2.01 Rating : 0.14 467 +Unsatisfiable/GRP576-1.ma ... OK TIME NEEDED: 0.29 Rating : 0.00 468 +Unsatisfiable/GRP577-1.ma ... OK TIME NEEDED: 0.07 Rating : 0.00 469 +Unsatisfiable/GRP578-1.ma ... OK TIME NEEDED: 0.24 Rating : 0.00 470 +Unsatisfiable/GRP579-1.ma ... OK TIME NEEDED: 4.20 Rating : 0.07 471 +Unsatisfiable/GRP580-1.ma ... OK TIME NEEDED: 0.40 Rating : 0.00 472 +Unsatisfiable/GRP581-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 473 +Unsatisfiable/GRP582-1.ma ... OK TIME NEEDED: 0.18 Rating : 0.00 474 +Unsatisfiable/GRP583-1.ma ... OK TIME NEEDED: 1.43 Rating : 0.07 475 +Unsatisfiable/GRP584-1.ma ... OK TIME NEEDED: 0.20 Rating : 0.00 476 +Unsatisfiable/GRP585-1.ma ... OK TIME NEEDED: 0.18 Rating : 0.00 477 +Unsatisfiable/GRP586-1.ma ... OK TIME NEEDED: 0.35 Rating : 0.00 478 +Unsatisfiable/GRP587-1.ma ... OK TIME NEEDED: 8.87 Rating : 0.00 479 +Unsatisfiable/GRP588-1.ma ... OK TIME NEEDED: 0.76 Rating : 0.00 480 +Unsatisfiable/GRP589-1.ma ... OK TIME NEEDED: 0.17 Rating : 0.00 481 +Unsatisfiable/GRP590-1.ma ... OK TIME NEEDED: 0.16 Rating : 0.00 482 +Unsatisfiable/GRP591-1.ma ... OK TIME NEEDED: 10.79 Rating : 0.07 483 +Unsatisfiable/GRP592-1.ma ... OK TIME NEEDED: 0.21 Rating : 0.07 484 +Unsatisfiable/GRP593-1.ma ... OK TIME NEEDED: 1.28 Rating : 0.00 485 +Unsatisfiable/GRP594-1.ma ... OK TIME NEEDED: 0.75 Rating : 0.00 486 +Unsatisfiable/GRP595-1.ma ... OK TIME NEEDED: 0.19 Rating : 0.07 487 +Unsatisfiable/GRP596-1.ma ... OK TIME NEEDED: 0.29 Rating : 0.07 488 +Unsatisfiable/GRP597-1.ma ... OK TIME NEEDED: 0.58 Rating : 0.00 489 +Unsatisfiable/GRP598-1.ma ... OK TIME NEEDED: 0.23 Rating : 0.07 490 +Unsatisfiable/GRP599-1.ma ... OK TIME NEEDED: 1.68 Rating : 0.07 491 +Unsatisfiable/GRP600-1.ma ... OK TIME NEEDED: 0.37 Rating : 0.07 492 +Unsatisfiable/GRP601-1.ma ... OK TIME NEEDED: 1.47 Rating : 0.07 493 +Unsatisfiable/GRP602-1.ma ... OK TIME NEEDED: 0.48 Rating : 0.07 494 +Unsatisfiable/GRP603-1.ma ... OK TIME NEEDED: 0.48 Rating : 0.07 495 +Unsatisfiable/GRP604-1.ma ... OK TIME NEEDED: 0.52 Rating : 0.07 496 +Unsatisfiable/GRP605-1.ma ... OK TIME NEEDED: 1.64 Rating : 0.00 497 +Unsatisfiable/GRP606-1.ma ... OK TIME NEEDED: 0.42 Rating : 0.00 498 +Unsatisfiable/GRP607-1.ma ... OK TIME NEEDED: 3.85 Rating : 0.00 499 +Unsatisfiable/GRP608-1.ma ... OK TIME NEEDED: 0.56 Rating : 0.00 500 +Unsatisfiable/GRP609-1.ma ... OK TIME NEEDED: 2.09 Rating : 0.07 501 +Unsatisfiable/GRP610-1.ma ... OK TIME NEEDED: 0.44 Rating : 0.07 502 +Unsatisfiable/GRP611-1.ma ... OK TIME NEEDED: 2.08 Rating : 0.00 503 +Unsatisfiable/GRP612-1.ma ... OK TIME NEEDED: 0.44 Rating : 0.07 504 +Unsatisfiable/GRP613-1.ma ... OK TIME NEEDED: 0.58 Rating : 0.00 505 +Unsatisfiable/GRP614-1.ma ... OK TIME NEEDED: 0.26 Rating : 0.00 506 +Unsatisfiable/GRP615-1.ma ... OK TIME NEEDED: 1.33 Rating : 0.07 507 +Unsatisfiable/GRP616-1.ma ... OK TIME NEEDED: 0.26 Rating : 0.00 508 +Unsatisfiable/LAT006-1.ma ... OK TIME NEEDED: 8.77 Rating : 0.14 509 +Unsatisfiable/LAT007-1.ma ... OK TIME NEEDED: 76.98 Rating : 0.36 510 +Unsatisfiable/LAT008-1.ma ... OK TIME NEEDED: 0.46 Rating : 0.07 511 +Unsatisfiable/LAT009-1.ma ... FAIL Rating : 0.00 512 +Unsatisfiable/LAT010-1.ma ... FAIL Rating : 0.00 513 +Unsatisfiable/LAT011-1.ma ... OK TIME NEEDED: 84.39 Rating : 0.07 514 +Unsatisfiable/LAT012-1.ma ... OK TIME NEEDED: 7.89 Rating : 0.00 515 +Unsatisfiable/LAT013-1.ma ... OK TIME NEEDED: 59.75 Rating : 0.14 516 +Unsatisfiable/LAT014-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 517 +Unsatisfiable/LAT017-1.ma ... FAIL Rating : 0.71 518 +Unsatisfiable/LAT018-1.ma ... FAIL Rating : 0.93 519 +Unsatisfiable/LAT019-1.ma ... FAIL Rating : 0.00 520 +Unsatisfiable/LAT020-1.ma ... FAIL Rating : 0.50 521 +Unsatisfiable/LAT021-1.ma ... FAIL Rating : 0.00 522 +Unsatisfiable/LAT022-1.ma ... FAIL Rating : 0.21 523 +Unsatisfiable/LAT023-1.ma ... FAIL Rating : 0.21 524 +Unsatisfiable/LAT026-1.ma ... OK TIME NEEDED: 37.10 Rating : 0.14 525 +Unsatisfiable/LAT027-1.ma ... FAIL Rating : 0.07 526 +Unsatisfiable/LAT028-1.ma ... OK TIME NEEDED: 99.40 Rating : 0.00 527 +Unsatisfiable/LAT031-1.ma ... OK TIME NEEDED: 19.14 Rating : 0.00 528 +Unsatisfiable/LAT032-1.ma ... OK TIME NEEDED: 10.64 Rating : 0.00 529 +Unsatisfiable/LAT033-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 530 +Unsatisfiable/LAT034-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 531 +Unsatisfiable/LAT038-1.ma ... FAIL Rating : 0.43 532 +Unsatisfiable/LAT039-1.ma ... OK TIME NEEDED: 0.22 Rating : 0.00 533 +Unsatisfiable/LAT039-2.ma ... OK TIME NEEDED: 0.22 Rating : 0.00 534 +Unsatisfiable/LAT040-1.ma ... OK TIME NEEDED: 4.10 Rating : 0.00 535 +Unsatisfiable/LAT042-1.ma ... OK TIME NEEDED: 65.92 Rating : 0.00 536 +Unsatisfiable/LAT043-1.ma ... OK TIME NEEDED: 67.86 Rating : 0.00 537 +Unsatisfiable/LAT044-1.ma ... OK TIME NEEDED: 89.67 Rating : 0.14 538 +Unsatisfiable/LAT045-1.ma ... OK TIME NEEDED: 0.35 Rating : 0.07 539 +Unsatisfiable/LAT070-1.ma ... FAIL Rating : 0.93 540 +Unsatisfiable/LAT072-1.ma ... FAIL Rating : 1.00 541 +Unsatisfiable/LAT074-1.ma ... FAIL Rating : 1.00 542 +Unsatisfiable/LAT075-1.ma ... FAIL Rating : 1.00 543 +Unsatisfiable/LAT076-1.ma ... FAIL Rating : 1.00 544 +Unsatisfiable/LAT077-1.ma ... FAIL Rating : 1.00 545 +Unsatisfiable/LAT078-1.ma ... FAIL Rating : 1.00 546 +Unsatisfiable/LAT079-1.ma ... FAIL Rating : 1.00 547 +Unsatisfiable/LAT080-1.ma ... FAIL Rating : 0.36 548 +Unsatisfiable/LAT081-1.ma ... FAIL Rating : 0.57 549 +Unsatisfiable/LAT082-1.ma ... FAIL Rating : 0.64 550 +Unsatisfiable/LAT083-1.ma ... FAIL Rating : 0.36 551 +Unsatisfiable/LAT084-1.ma ... FAIL Rating : 0.50 552 +Unsatisfiable/LAT085-1.ma ... FAIL Rating : 0.57 553 +Unsatisfiable/LAT086-1.ma ... FAIL Rating : 0.50 554 +Unsatisfiable/LAT087-1.ma ... FAIL Rating : 0.43 555 +Unsatisfiable/LAT088-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 556 +Unsatisfiable/LAT089-1.ma ... OK TIME NEEDED: 1.23 Rating : 0.00 557 +Unsatisfiable/LAT090-1.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 558 +Unsatisfiable/LAT091-1.ma ... OK TIME NEEDED: 9.54 Rating : 0.07 559 +Unsatisfiable/LAT092-1.ma ... FAIL Rating : 0.36 560 +Unsatisfiable/LAT093-1.ma ... FAIL Rating : 0.43 561 +Unsatisfiable/LAT094-1.ma ... FAIL Rating : 0.36 562 +Unsatisfiable/LAT095-1.ma ... FAIL Rating : 0.43 563 +Unsatisfiable/LAT096-1.ma ... FAIL Rating : 0.36 564 +Unsatisfiable/LAT097-1.ma ... FAIL Rating : 0.36 565 +Unsatisfiable/LAT138-1.ma ... FAIL Rating : 1.00 566 +Unsatisfiable/LAT139-1.ma ... FAIL Rating : 1.00 567 +Unsatisfiable/LAT140-1.ma ... FAIL Rating : 1.00 568 +Unsatisfiable/LAT141-1.ma ... FAIL Rating : 1.00 569 +Unsatisfiable/LAT142-1.ma ... FAIL Rating : 0.64 570 +Unsatisfiable/LAT143-1.ma ... FAIL Rating : 0.14 571 +Unsatisfiable/LAT144-1.ma ... FAIL Rating : 0.86 572 +Unsatisfiable/LAT145-1.ma ... FAIL Rating : 0.93 573 +Unsatisfiable/LAT146-1.ma ... FAIL Rating : 0.79 574 +Unsatisfiable/LAT147-1.ma ... FAIL Rating : 0.79 575 +Unsatisfiable/LAT148-1.ma ... FAIL Rating : 0.71 576 +Unsatisfiable/LAT149-1.ma ... FAIL Rating : 0.93 577 +Unsatisfiable/LAT150-1.ma ... FAIL Rating : 0.86 578 +Unsatisfiable/LAT151-1.ma ... FAIL Rating : 0.86 579 +Unsatisfiable/LAT152-1.ma ... FAIL Rating : 0.79 580 +Unsatisfiable/LAT153-1.ma ... FAIL Rating : 0.93 581 +Unsatisfiable/LAT154-1.ma ... FAIL Rating : 0.79 582 +Unsatisfiable/LAT155-1.ma ... FAIL Rating : 0.86 583 +Unsatisfiable/LAT156-1.ma ... FAIL Rating : 0.64 584 +Unsatisfiable/LAT157-1.ma ... FAIL Rating : 0.86 585 +Unsatisfiable/LAT158-1.ma ... FAIL Rating : 0.93 586 +Unsatisfiable/LAT159-1.ma ... FAIL Rating : 0.86 587 +Unsatisfiable/LAT160-1.ma ... FAIL Rating : 0.64 588 +Unsatisfiable/LAT161-1.ma ... FAIL Rating : 1.00 589 +Unsatisfiable/LAT162-1.ma ... FAIL Rating : 0.86 590 +Unsatisfiable/LAT163-1.ma ... FAIL Rating : 0.93 591 +Unsatisfiable/LAT164-1.ma ... FAIL Rating : 0.93 592 +Unsatisfiable/LAT165-1.ma ... FAIL Rating : 0.93 593 +Unsatisfiable/LAT166-1.ma ... FAIL Rating : 0.93 594 +Unsatisfiable/LAT167-1.ma ... FAIL Rating : 0.93 595 +Unsatisfiable/LAT168-1.ma ... FAIL Rating : 0.14 596 +Unsatisfiable/LAT169-1.ma ... FAIL Rating : 0.86 597 +Unsatisfiable/LAT170-1.ma ... FAIL Rating : 0.79 598 +Unsatisfiable/LAT171-1.ma ... FAIL Rating : 0.50 599 +Unsatisfiable/LAT172-1.ma ... FAIL Rating : 0.93 600 +Unsatisfiable/LAT173-1.ma ... FAIL Rating : 0.93 601 +Unsatisfiable/LAT174-1.ma ... FAIL Rating : 0.79 602 +Unsatisfiable/LAT175-1.ma ... FAIL Rating : 0.93 603 +Unsatisfiable/LAT176-1.ma ... FAIL Rating : 0.93 604 +Unsatisfiable/LAT177-1.ma ... FAIL Rating : 1.00 605 +Unsatisfiable/LCL109-2.ma ... FAIL Rating : 0.29 606 +Unsatisfiable/LCL109-6.ma ... FAIL Rating : 0.14 607 +Unsatisfiable/LCL110-2.ma ... OK TIME NEEDED: 0.27 Rating : 0.00 608 +Unsatisfiable/LCL111-2.ma ... OK TIME NEEDED: 7.03 Rating : 0.07 609 +Unsatisfiable/LCL112-2.ma ... OK TIME NEEDED: 0.27 Rating : 0.00 610 +Unsatisfiable/LCL113-2.ma ... OK TIME NEEDED: 0.29 Rating : 0.00 611 +Unsatisfiable/LCL114-2.ma ... OK TIME NEEDED: 0.36 Rating : 0.00 612 +Unsatisfiable/LCL115-2.ma ... OK TIME NEEDED: 0.59 Rating : 0.00 613 +Unsatisfiable/LCL116-2.ma ... OK TIME NEEDED: 4.90 Rating : 0.00 614 +Unsatisfiable/LCL132-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 615 +Unsatisfiable/LCL133-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 616 +Unsatisfiable/LCL134-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 617 +Unsatisfiable/LCL135-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 618 +Unsatisfiable/LCL138-1.ma ... FAIL Rating : 0.21 619 +Unsatisfiable/LCL139-1.ma ... OK TIME NEEDED: 0.34 Rating : 0.00 620 +Unsatisfiable/LCL140-1.ma ... OK TIME NEEDED: 0.28 Rating : 0.00 621 +Unsatisfiable/LCL141-1.ma ... OK TIME NEEDED: 0.59 Rating : 0.00 622 +Unsatisfiable/LCL153-1.ma ... OK TIME NEEDED: 0.31 Rating : 0.00 623 +Unsatisfiable/LCL154-1.ma ... OK TIME NEEDED: 0.27 Rating : 0.00 624 +Unsatisfiable/LCL155-1.ma ... OK TIME NEEDED: 0.29 Rating : 0.00 625 +Unsatisfiable/LCL156-1.ma ... OK TIME NEEDED: 0.27 Rating : 0.00 626 +Unsatisfiable/LCL157-1.ma ... OK TIME NEEDED: 0.27 Rating : 0.00 627 +Unsatisfiable/LCL158-1.ma ... OK TIME NEEDED: 0.31 Rating : 0.00 628 +Unsatisfiable/LCL159-1.ma ... OK TIME NEEDED: 6.15 Rating : 0.00 629 +Unsatisfiable/LCL160-1.ma ... FAIL Rating : 0.14 630 +Unsatisfiable/LCL161-1.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 631 +Unsatisfiable/LCL162-1.ma ... FAIL Rating : 0.00 632 +Unsatisfiable/LCL163-1.ma ... OK TIME NEEDED: 5.06 Rating : 0.14 633 +Unsatisfiable/LCL164-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 634 +Unsatisfiable/LDA001-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 635 +Unsatisfiable/LDA002-1.ma ... OK TIME NEEDED: 22.13 Rating : 0.00 636 +Unsatisfiable/LDA007-3.ma ... OK TIME NEEDED: 0.13 Rating : 0.00 637 +Unsatisfiable/RNG007-4.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 638 +Unsatisfiable/RNG008-3.ma ... OK TIME NEEDED: 2.32 Rating : 0.07 639 +Unsatisfiable/RNG008-4.ma ... OK TIME NEEDED: 4.42 Rating : 0.07 640 +Unsatisfiable/RNG008-7.ma ... OK TIME NEEDED: 15.93 Rating : 0.07 641 +Unsatisfiable/RNG009-5.ma ... FAIL Rating : 0.50 642 +Unsatisfiable/RNG009-7.ma ... FAIL Rating : 0.50 643 +Unsatisfiable/RNG011-5.ma ... OK TIME NEEDED: 0.19 Rating : 0.00 644 +Unsatisfiable/RNG012-6.ma ... OK TIME NEEDED: 71.73 Rating : 0.00 645 +Unsatisfiable/RNG013-6.ma ... OK TIME NEEDED: 71.74 Rating : 0.00 646 +Unsatisfiable/RNG014-6.ma ... OK TIME NEEDED: 67.79 Rating : 0.00 647 +Unsatisfiable/RNG015-6.ma ... OK TIME NEEDED: 69.34 Rating : 0.00 648 +Unsatisfiable/RNG016-6.ma ... OK TIME NEEDED: 71.94 Rating : 0.00 649 +Unsatisfiable/RNG017-6.ma ... OK TIME NEEDED: 71.63 Rating : 0.00 650 +Unsatisfiable/RNG018-6.ma ... OK TIME NEEDED: 68.25 Rating : 0.00 651 +Unsatisfiable/RNG019-6.ma ... FAIL Rating : 0.21 652 +Unsatisfiable/RNG019-7.ma ... FAIL Rating : 0.21 653 +Unsatisfiable/RNG020-6.ma ... FAIL Rating : 0.29 654 +Unsatisfiable/RNG020-7.ma ... FAIL Rating : 0.21 655 +Unsatisfiable/RNG021-6.ma ... FAIL Rating : 0.14 656 +Unsatisfiable/RNG021-7.ma ... FAIL Rating : 0.21 657 +Unsatisfiable/RNG023-6.ma ... OK TIME NEEDED: 0.16 Rating : 0.00 658 +Unsatisfiable/RNG023-7.ma ... OK TIME NEEDED: 0.27 Rating : 0.00 659 +Unsatisfiable/RNG024-6.ma ... OK TIME NEEDED: 0.16 Rating : 0.00 660 +Unsatisfiable/RNG024-7.ma ... OK TIME NEEDED: 0.41 Rating : 0.00 661 +Unsatisfiable/RNG025-4.ma ... FAIL Rating : 0.29 662 +Unsatisfiable/RNG025-5.ma ... FAIL Rating : 0.36 663 +Unsatisfiable/RNG025-6.ma ... FAIL Rating : 0.29 664 +Unsatisfiable/RNG025-7.ma ... FAIL Rating : 0.43 665 +Unsatisfiable/RNG026-6.ma ... FAIL Rating : 0.57 666 +Unsatisfiable/RNG026-7.ma ... FAIL Rating : 0.50 667 +Unsatisfiable/RNG027-5.ma ... FAIL Rating : 0.86 668 +Unsatisfiable/RNG027-7.ma ... FAIL Rating : 0.86 669 +Unsatisfiable/RNG027-8.ma ... FAIL Rating : 0.86 670 +Unsatisfiable/RNG027-9.ma ... FAIL Rating : 0.86 671 +Unsatisfiable/RNG028-5.ma ... FAIL Rating : 0.86 672 +Unsatisfiable/RNG028-7.ma ... FAIL Rating : 0.86 673 +Unsatisfiable/RNG028-8.ma ... FAIL Rating : 0.86 674 +Unsatisfiable/RNG028-9.ma ... FAIL Rating : 0.86 675 +Unsatisfiable/RNG029-5.ma ... FAIL Rating : 0.86 676 +Unsatisfiable/RNG029-6.ma ... FAIL Rating : 0.86 677 +Unsatisfiable/RNG029-7.ma ... FAIL Rating : 0.86 678 +Unsatisfiable/RNG035-7.ma ... FAIL Rating : 0.86 679 +Unsatisfiable/ROB001-1.ma ... FAIL Rating : 1.00 680 +Unsatisfiable/ROB002-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 681 +Unsatisfiable/ROB003-1.ma ... OK TIME NEEDED: 72.86 Rating : 0.00 682 +Unsatisfiable/ROB004-1.ma ... OK TIME NEEDED: 99.80 Rating : 0.00 683 +Unsatisfiable/ROB005-1.ma ... FAIL Rating : 0.07 684 +Unsatisfiable/ROB006-1.ma ... FAIL Rating : 0.86 685 +Unsatisfiable/ROB006-2.ma ... FAIL Rating : 0.86 686 +Unsatisfiable/ROB008-1.ma ... OK TIME NEEDED: 67.56 Rating : 0.00 687 +Unsatisfiable/ROB009-1.ma ... OK TIME NEEDED: 80.05 Rating : 0.00 688 +Unsatisfiable/ROB010-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 689 +Unsatisfiable/ROB013-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 690 +Unsatisfiable/ROB022-1.ma ... FAIL Rating : 0.00 691 +Unsatisfiable/ROB023-1.ma ... FAIL Rating : 0.00 692 +Unsatisfiable/ROB026-1.ma ... FAIL Rating : 0.86 693 +Unsatisfiable/ROB030-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 694 +Unsatisfiable/ROB031-1.ma ... FAIL Rating : 1.00 695 +Unsatisfiable/ROB032-1.ma ... FAIL Rating : 1.00 696 +Unsatisfiable/SYN080-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 697 +Unsatisfiable/SYN083-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 698 diff --git a/helm/software/matita/tests/TPTP/log.300.26-5.menvcorti_VS_log.120.orsay.ods b/helm/software/matita/tests/TPTP/log.300.26-5.menvcorti_VS_log.120.orsay.ods new file mode 100644 index 0000000000000000000000000000000000000000..8cf343101a70fe069dba3503f21d8b2120861833 GIT binary patch literal 37636 zcmZ^~1yt2d*9S^>r-a0j5)crSkVX&*0qHI&4-(QHhX#?5ZV{wIy5WFIm(q=t2nPu% zsXGUJzx#gQy4SUM^jY(tJ$q*NZ*SC;&@m`bkbeZ9jywo?B@)R4{*C;>0Y7#x?JQk9 z9WBiq9bdhCVdnDE!JgO6-h#)$%=x7=kAtJ7y@kUIS36647anIvCrdL6XB$gP7q$OI z6Oj3zKP2E^j~(o-URt|4T~l-B=e_wF2b_oG;D0^^|G)=7FC6S$kmNn=ULjg%tLJ-O zub=r{M(+5fR5DW0YK7P;mEr2uiIFFblP8H;s|eGx*Y(Wb`?@R0VsJ0B{gT^M>mA3= zK9Yt|GmFq z4()%BB`=S@`5c<~ANpVH4<0YJdmNn%9taKl`5d17?OK~opJXh*y7-ZH@%KWg{%5_( z#mUa0kORX)yT{ewR+vuA@AlK(?Q|grMw6?I!@=EO4u7rZFIO+Z+FM&hTiZQSE|&Ky z7@oSh-qUB=!gUYFZj z-N`ZYT?_tp{0E1_lWkt-yN(W5O}1f1UKcARlHzU6XYvQT%gep(zs}mv9giJ8oA{af zJs7?`-`&|+jK2J_n>{Jseg*!+xZdV= zc(pt4!otO5i;?(%|H1lTcexv`P~g#gt*5b%uPt%;r9#Vjfjh5+SR0+;rE<&pbXUJM zqyG;Fs+m>+f#< zpx%q(-A8=_xYnEnZAy|zP#Lu@!!1|7vo)&6!UHo^Y=O0zo_u@JX^au z={A|0nV0+l1od}5DlB=ugtxqXRnlbd*O&hG(+(XI0;k2clilsVO2^4zwyT`M6>V)R zL+EB)oLmkH`FkCo?6&jzd$n9D8ahmg z|J@M%+wbqS*Fs*}`>XD*am&sXTF~Xw%xWc9p5e$AyUL+POi^q4sYdh0p~ML--Hkq0 z(Mj4;=W(Y@TYUpargwMI;e2|w#MbnoYUq4ZNR#CG!Acb4<@tN>CRe%R-)!!u-N!M> zLJpEG9*4X8{K{9mJKgemD{tcEUFS5T^$J%Q8GdG;4Evw_derRYS&wVTOcuV$Z|JUHbR;F=Vv(E|nZu(h|-swtz z%!{GfF!y=d4-VnCcjB`yMO~cF`@8z7C0p8B{0~-|?alTtqS`Ng4%}lL7#SsaOv~Sg zCI7~LymmNEEZO4iaker1XMgkKyvYw&NqFPsUP+ic;M>>p^u+f##_wHk4)wD5-?-h2 zsH@*I%o;5hyW`!GXT4X|SDSSlWHF?E3Z+{WS^XhWZw%x)1kt z?|UKRkBj3Pfw}L4j>G1m-bn&;)sYL;DaO}OcN$# zAMSWb7CU6VylnaG;c>dMvevb@V0?9c5mut&XWDdeiRjvzG^&U`-Hx<%2wg5Go-gm2 zHEH!Zc)Y&9m11Djx7}oZ-d`=G^ZV})|I6hl9`jdzMi{OBCk98$6^wqTwZn~DuYCn<|+kFmpnSG`XH(j-QwVcZzsUAu8GO|o3NA(x4Ync3H8%rK83qmaT zUm+GR{vKbQxL^Hg_q#}!yqx#9xH7#upuSoI;#%+GZ97Yz^}o8LmhARBcyM%_eF5h! zuP5iZn!4QITpN4maCL#GxH|jor_yl2-d~k1x_g}4d@j~@JQ#Jg?03xj!QZZkam(n( z2^-wun?u{#@#59qU-Gk4-C!Q=jF=*BKe>|H+E_Z+ zuv*#F5fTiV`)`bfYU70-Jz%4yea+Q7GSz?VU~{o(YOF+e9vhpeFRoiSK3n(D`+|iUZNdG~iEsmjy06A<{szrQ z?o=9F5=}D&**zES<`YD+u6D2H$G72zWrLv~-RuSrGB}-sjJ}p9e*OMy;XAbB`C1z20=B6ob)CsjK$qhjdl-zNOQ6nR9RI(wCkYXW`KBty`gE8Pq=0lYA=_SYR{X zfsut}NzP=?mWJZpnucP7wzjv9#x~V(|G;ieInB9}&GE&1LbS&w*~ZwuamnMG%2MX< zBXVA$F%b@$RIs6>ckEfA!3%9VjK;^GEj=No!(hysO5S5*TJDln6GSCpTCdO{M|qYr z)30ng_So99x2x|M>xwq`axmyEca73Zmi=U$z8TDElS{90p3?bDf+dAo(SABC=M_Uj zw5IY8Mz~I_uqrp{fy8#>T6}0d!~Go|f!dEKOP=eawS&Llcy$g#A97Weg_gcEeco`o z?E`Vf{mTNY8j#+8*Dg^zaCYYVHH}eyTa>2oH`cA@K2vnqC)=Svd2r2E#fQ(^U&mvi zvR1em5w$}%)A02IWfjS!r}3n;jj;>4N2@sou0(@vq{4q z5|)%$oW4+$AHiVLPLTGj*vL)-RLbaOS6yHMU69zLrFZM!L-=Sig- z|J>@C-=1OUq>qoS8ywWuRl1IAY99~hcA+Fm&P%$yhVvS$7B7AZ31 z`i;nzMMriBTdULMf0qU?kV@+{GkJBJRLo%3dN)*AdTL|P?SFYiw=d|Sk|!~LLFD-O zfE%`6R!h$Q+EZ5T2qm_Er9y`|K-`pl<@myjBWScS1HpA-w%IABw<+WOVxPNn)fJl` zs~LvxduGK7iNWb(Lm~4#KZK&?;L=z6yvN75uk&nuD-*r?bx{(UkohnSlK}m(e&l2| zSp~QVIf|$FrPo8$DGVYZ@nS zy_FnNdjTi?yR)G=y~Nd8p4fw7ADs0Vr?n)GIOcmz|Luai$Yb1Yj-f^|T5`l}W$ zTk&#-(JzdBB-Mg_q>=8!2Fa6QjIYUwN}d52KS`yh(WRtf+Kt6gjsjK&F%0?0Q;Nja zUAHUj_$Uj>Ghh8U@0}sZb${5*oIClDnjdY?(e96n-5(D-xj*VOaQosF)QZ8bbLBtavoR0DL2r_M8HRM zD81mLTGRoo(&^skJMIj1bwBs=cCb!G3U?Qvi_;>w2S91fr3b*pDDgQb-l}c$ckTb_ z^nPwFjkn%N=eNOhZXeD2I^#1^p;DQ=0e7|gPd2}oJ+1&KIn&Dq~gHXoXz4-F1|ZJb8otL?=bp%5A>lM=2MbB24(m~Cy2 z3aUNL0FKfwpefY?9atnI*0UV3G+YWZxjyr@_yjpC>^Dl2iWcZX-^!$(3h7uKl57JH zK@%9<1SEnZH5T1&9F6h-2F(h29lyU^FiSsxeX$lxeX1kjWJ!YesQY5BjJT`C=trGoNT#1Cr~Pz@AdKMqs#m_Ft>D1 zaZ&k!Yb&W9rmThUL?-@1_FhwB3O9sfi^`%3e7+x9G*NcM;D$im$C9K>=S|jrI!8{L z5Q62T3T`6RsV+KK{yMAniy9e1x%unIzO-fbUL%3gLhl#Zc;UYMmJ>ws^KGrMG*AD4 zU4tlj*?{KQm(rZ#;YYs~dh*dYRqOf+xulh3)u?E3?(I!(72+$|)!xpTmXH}JhKr7s zKb&;#Ge5~7qo3C!ZdiVfshe3k6n2HL#KG&5=E1zD4r~cCHu*=zb^~= zS4t5-{O~L4&|Kck-zHQ;Of<)`Fac_^FLFqoy32#qsR4{%=QeDnRcyB^(i^o`^lpn4 zs6621a3Ii$xNm6I+8LsaogeH-Dm{u`n6ALkVN$_>;?-d+AtMv|Q;KBp)mr~XDqez6 zKuNG-V%gC>^Sh{qvTAjxBuhUkbm&m*Ob3#mDZDaWn{U|v`XVuXCz@xab*r30Vzr-EsHyYsfTsmz;Xr>9((Tmi4&Z1OZ<2@u2L=PV{e1 z(zgC2_-k)pXJ*k@CZI^Os5qWLP!0I$aQLsjnMWsN?G8f+dHi(Bo)yuuf{u?{6fyRy z*lJL#GYFsRQj;dwp?q#S*&4@^qSHk@9C{_FhK2d@Y+YHkZ^lhGxxkK`22P0JB(3SE za^)j$s-><%!`%TKQU*9u`?u<&zQW|9Of~joHJ-m!jAvdrp&Ow?CM|~{_x`!iyWp=T z6RiKjYw3zLnG3%?Qh&$6ihQxWgqs%|!c)~0QYo4dE6`NPAR|r4$8u6UKjeI< z3$+emFQzNdw9C>cW>Ja2=~G7+VZHQ9oWUt-^nEq^#*5=v#P$T$7P9@m>AmXs`e=co zOm=uqsWFK!cvxR5wPtHphGIGsO}jQPP1g5vNDU6B0uRF{A_HZgw{C>Xjju1~D#D_| zbGRRp@BqaqijLKHRVkYPnF&1@Pvyj&V}@0YNjZkK8|MqkKo3Ro-R@Wv4`!3hyOSl?2?>fgHK4p*NY+%N?Z ze#B45_fF)mL2|iTSqk8F>zST^HmN{oDV!OWfDlnE6yr8dHUss2F>L|kKV0J#1- z6WUjkZ2k3%i%yeT-WYbbW?Gy&e$;Ps9wk->av8L^wcs7*q{e{7;*#h>!$et_h7BFL zW6}}240QAy4sh}{;2fWu63PZ*=8rhnkp19iQZ#8bXoqzSe7ou=o9#YRAr?|ID3os?M}oNM3NGeBx`j|13eNRu>Uk5iu4wJLVj zEp${o?enGh30lRq5wrj!Fe5|0QVC%j3em*(rAeO_^ts(KEOQWIEB^}^1+L#x_zsW>ix3&Mdn)syT)Pjnd>}MycXxk1y|HL&|AQGo$LsxV`|V8xqoXPebVVIq7@4M?4#)W zTnBV7$6<+O$_-~2M^-HZtaFh#ef-$3xqw3u;XW9D8kI=>1rZH}3Yp9nC&sc}`{cBn zaEd53mG!<8J2OcBv`m%>h!e^b2((!}DBo@3o#`xH(3pLeG?W$V+QrbY0E)ESwd2B} zwfS!7p)-T%kIOI!u6ObM+oi3Y(;6p&SjXq8B};gWVObQYM&#eBNSHLErx$n>x>l3k z?WB*}f9*WDk`=VPi^MshCF~ji6 zg|~X|vk4hH;?z~eFR@sJL_Wd5mf@0t;So{I>6uuk&w0V^+B8)st}8lAI-`#Wwo!zm+)OY(rBAoAvz}*_jrgoPf8iz(5;MuC6_PZ zKfzKDp&VGc&2I(=*~AuUn6heD3gSE8lRUF<8`&-n!Y=lovACQkHQ7D1!<{LJYQ85H z$Q64IeB??5UOBynigB3olP-pe`?KA)Z^9=@M#Dp&w}h&WFq3QULKz!*^^bgcdcCB& znF5Abw}&uyhB4+N6NpHoe^TYUoM4RKE1doA$K@dY;YI!MPu;jt@H}(id7M_rU5fGX z?FZbcs(W5Kzu3wP3i8bKe$WH6W-oKebC^_B*ydoAomZi1&dN?u*?zImI#3Cn?{eG@ zgf#o+^h8RLl16h-U`CzOIfC;I^Mh=TJ6xeE~i zIEU`rJEABCnyOj((9&=M($R34=N93rBWADj6cIdiE*fnKG#u>Xf4^%ybvvVor@YGo zp?%J$$h?Q!REBTsp8o?4+vh!0JjkMcm`N{A8j?$j`GJ5eI|mPo(nlYw*9)uHK3lp9 z5+o~o$LTQ*i-a_Fe&JH__^rHg%#A?iW?$2u$PN;ukTFAVguMBeAHF?S{n+j7i*IQ- zAz;Ys`76NC^xe|=gEHRlwv(P%y>{8sPDq-T2=#jM+J5#z5L~j3#5gyeGu2;kN~`1r zTnh{HGy6|j_uwU$+;r2*Kf$rH63nZzGU4G*#-hk%d|*ULm2R%N=~B%M51eMPqcd=5 z!D(*KN5WOr5U?3>ME$)XjmP$9W3l8#%n;f*Iz_@g+()CgnT0cdvfbhqzrR|iN+1$< z3*7lI_cKX$P7rIU5m*{2w+@**(qm??l97FoYm`9wgIu#Y$4%ASE%~4n@W8bys||Qq z4Xpw^sJO`EsIWKTVkr?bG$MlJRWM=z>#ZCffOS(`TOF`ev-Rmtz3+BU#1s&%4fU6| zKzjh7B2z1>*BsLQHWKkdJ|z4$>2tm2F@!8)AGg>@w>cl`-sC3UrTHq`j8ir=BK%2B z6u+_$3`#w*qsZ>bpwygY%2}t%M+t!g!OY0vvPnn-4Cc6|+nAc+5oaCoZAysCwaDJz zk&qS&13U_akrO0knQ_()gI!%JUH8Hp@3?u< z^An1&6p0@v;t;svHaiEN2}n0WNabYj^vOkV0MRHa*AGGur`FR1RK*Qk2i;|}N;sLz zp)-r_Fx+q(aAFEdq&7Gaz%8Xm^JQrr8sxhH+PJ9tC8+^DHsC36bKX#8=OA-0=Gma{tTp%8zDFb!QIWXxI8aDIue|2caG1>9g6xEuKHCJsZ9{lH5Ok zBfn$mN!s)AX})QUuhwjL8z<@6wX>L_2F@as(xU9ytwn!E9j9!n`$pXm9 zG~o^i81NjJyEE-nYotxJ6zq}0cA_3Bzo_(f+jy3*|NPEutb=uj0kC@24eSe;;?WD%n~fbxDV!UOJVea zO+;$3V3TM7!j#?FTk2yufyJ+NevEW2#FB!MKq9k8Um1*}zO*B2Eizvzq@Fl!9AfiC*0S+=J^9*K_Mc(Kg-hG^#)+)A`8V`X zCmDpnCmG`qN3fapNuYp)beOUld?y%Bg*a-0;bBRA4A>6^i!*Z1!6I-0?zLU)+Sxl^ zJf#Z~)Y?&ow~(=NtrIBl4h$x+RmQu~CEbTgGf}(lrD8;wt?|Oa0F!;!LYHuYx>}I& zoOe#NZi;OR!+}KlK7@7;i-H2gGY+iG5h*0=ux>N+t))SWUQS9_P4d-i))+!%kPDZifxn@|;=Q12}lI$n6qT}6DwHr;)*e!iK zKI%pu2<<1dgsmUsV|Y?rHtyz_8pUxWb>xX@`Rz;t;!?mOiF#kteU=GB>;SNBBU`L6|_`AcoN1mVUCv`os|} z-=2o}U=khf2ed=t`JX7&rxnAzVeO12465(#g?^Vj5qG)kSiQ%hSM3{LN~*vQVl%H| zJn$4vAbzcE<|bmr2+WW&0wlfWRgB)$H7g6(KA= zv8x?X`)R643S$VE9je+AFgt9N+orq@&2_?*I2&laZ0HOkwr;OsR(H^>WgnPhayWiv zFQg36=38Hz{#s@_Ln>Y(@H5(aD$OY4!*uvLEz)`RRUn;b4ki7bEFy&OPpS&0tvK1F zO#ZizG~YeAY~<+QhWBYp&8yU)Nl2HW)WEtZV{{$0)v$&Y4rg)>gN^V>-L}SQ?d96u zB2{c{>qf=gGG)sl4A&$LL%o?g3`gc#snP|8e&m>4VHQ`48d=rC99aE5sX zDhTrKs+rpUjB5N82XHx48hR z$>M)S+E-c1FXZ9*O(?kvo%A6~E~%*0^T!g>2$Y(juJ@rK{lDOMGkl%P8>Ptyq|-Dp z*$rZ7>u{jDQ%fIO+8PsXhgUL_Mo*#Q(e2|xv2$+IlM2qA%D`7b?}gKq*Qk-aevH(1 z3ZYe??R;Du#9?&CmL$5;66ur!wZ1<;bx{>N)l+%SMa}^#;3aPZD&QrzLq+KiM=WDZ zq2l+aWIiu(no!h1c)*qLp1hX6@k8MarsUz~b#j-6L5^R3lzbuAJOlN>F%|N^s!(7Z&t zP5totR|8ZRsVzmN^YY|)%798HPtj>S3MyqwOzdDxBR(y+>bNeRTVe2DdoW5}2TUgJ zhQ6= z>C&`o;z`i2BwMphAq1)sM}r4ci|ZlBsD*Erph`Xwzdz)Xa-p0`FyH9Rp6~p0FZ`Q# zTRby-Gzm*=CcYl_4Y2uV8>-Fp$yXETD$^`G3sP4drRsQHVAF4yrk?UeETGJ^>_0(? z_th|V1EvzO4anX>=>=qwrUDhRSS$?V(WISQuTB2FKAeGQ;&@3dy9esE87&IlM7QDa zAA>pbUv1qFNQ^;Q*vu3xzo0TvF5^*D(@clM``(S+&##NC;Seu$x6ze?`;)UKh@7#R z8#l4C*5TZ8WNuya=v{evCJirRm6kDUdFCRf{YY z6VN}{v*X*}C)&n<(V>U%2&87NjadK1sfV98z^%GdzKY+qB2nkwo`Z2x>jB5|T%<2@ z54T8bVUhP-Ty#lcSSNqw@z!#}PL;Wo|KT9b;Z6i!5Q$m8>t4~S9NU}lCoD1iWu@P5zlQ-qJQM5a@rL+EfZgf>_E4~LhVc1Ue$m{8Pb5tg<-Al1jC5@O@ibDgj5a$bjWPeU%a{8Xz;3${ufAW3c@XKt-X3EN z*U^+dFvOYSUdM*agJ|p*@XZdC27k@ig{Rm$Tze%?pjEbm>lkuN7)5RvWd*a`PwS_5 z|2%Ehq`bxT%}!QR5dD{1F3m136swYENfbq4z|?N)t5?&YeYSn|HASb#n}QP3X6dA` zuE~XNl8l1c?W0XW%ABI&FYY?Z-~(bUKZFQ*~M>fDzxxL82Tjz&Q>E|^F^Aqc3vl_HXJ!9K_FUsg0qvy5q@xz z7(}#gDCelcQW0LrEeu4k^be?@zNIOzkTbW@@x-z6Vm?1Ici`w~ z(vxj~S$WD!n~5Lf3?M9$--N}=bm+ygfBqPO>}c(J6)cxQUpg@H4oPW;fEkflr(r-? z)7q{Y`+x80&~~iU3+$hfqChDB_Nn+m%ux!_n)csFMC9 z_E(EGg6HOp)>9bf#9`^k;g%J->XfzWG=iG4wS5$ULk%#8TXGF27+QRVOXF`5Da5;3 zE-c);^e;k(?-%Xf+t|B@y=?IQo{_0Znkg2f1!PlJ0i6auuryQ~EU!*@y~#t+1JOqJ zb!K2aG(R3od0hBut?5K_8}bM|g}MAF$SJlmqZ3*fTt^c09*RB6vmN5_94-?HHZUlU zQf1}sv;~UnNns2WdH)V;#rT_9cxPkg%jvm@*4+WaKt5-)jU+gN|2Ox`i@GbCzWF{&f;VpDiTM_GQHrubs)9?G0| zcDIcK$DR9w+68o#Jz=Eb+YF@9w@~|bfC6IVkd|uq`XGpH@M3x>)uwB-jEkrtjKCC} z9-jj9lFSLjtk*~V0r%maU!~^Z{5s<3m z5QTgNDoD@WFdm6o&Lga9O^K6P8^0vW2l8f&Fqq!|yGy2c%Fn1wCiug(TGN9f`dY0m z{qTm_DQ7E6w8Cx3kObx4AqjFetk)#oQ5wccL@q@JlaMB2%FnA%0JBC`!|zn?DiLoc zT(9{6j0=Zo&G{c6zo2D2!Z95Qvy$H{DNd=8NMB$3KcsI9XXE)hGMQ%+q!~S_06<$( z8wv(?5=}Cvn9f#x8=`MHi1K+mT|oRU7dE4#dztK%-X?PjS)i$MYUA=|k&*M=$0Q23 zK$41)5WGxIAr^!%&F>p@o(?Rl_AI*no1a`_)rk0LJwKw#a-S831QNB?-tBSoM=QY5hIlv(;unSrAuAD>ilJCvwtO) zJoCtY#8ru%bh4Vf;-iiOco@j66p(d^kbfwV4pJWub$yR6HZ$trf9N zNt(F!WL_l!6o$NgNWbIok!#pk3%C}}xYlb#VjJwdmcftnMC*!TM72)he>)xUmG3=Gc7;P zIEL$!{s4>%c~W)xve>qU9ph1v>{J+%T&Kj1Ue)-u*cmy(4$8!1(!9#Na|&bvvRFk= zHTNN7k7e(~%fDxkkhblKiN8pBvGn%-kQY(Gj6|451U=B0aH2Iw0LWU)&vaQ4n6>ds@yFBt4fw3Pw4ztI`G zikJzk%VLtDai0M#E-3|iV5r8h=q1O+`!gfBR@Jb(p9br7hpVO=l-L`FXi7tVt~?zHJFfi+EQIIftuX3$!| zgvg5~s$Kv>-bYWM2gvPqNSPE@klg^D*ns9^K8>XG93iW_TqK@s*F~-MO;M|hcr`*( zW*RR`JwrfV+VMjBp{|Y%D;J3Z*Y#I5H!3Tp`*y6rOCGH_ z8liu?maccXj`r)HvEZ2j7+Extj{lDTh$<|bWhf#`eNTAI{X0mfuCv_;K%_+ zs=1f83J-1pkbW2-#s|Tgjn>VY=Jndgo76-UfjeB*opeLf z7&t9pL5epP^wRyVK@3LitmNAYNSVp%BwE$5leqUXB4k z+n{_7Ji%BCWa8qONZ%f^#H{P>L!Dd%1G?&?7KghpLdsM7h{W!XK|YUs2^}YKK!8-8 zCGT^W^==R3MpQnfid{9_OdS(?C z71AdD;iovuI3#uqDM9bJL_l-;Ln*+Ss~B0&?uWD!v!4|Y^}%IMC$gR$@wC6!pZ7GB!UW(6`_*eWzpUnr;N$2S7JyF6HLC zu5s#e0Rcl469X_yOE1Cp+>9yNzyVjSwo=SFXx|dd1U!yy5aa|AE!LKt%teQ>8qK*O zHJY#?^vZf}kk=5mt6gG_Do3wDN z)cu+6{7kOzm2UM1+mHJ}-_B6cu-xRn_Akf3ci^?e1>HiqJ4q;=fif_CG#gy&3$m|k zi8}M^s<@zL?Ipzc4Qf`W?;0}SaqS7b+zH_0#*QOq8Cy6iu*E`Y!`&&xtTJ3cwm_w{uUnvhsqeZXY&9!-x6;I;v=AV3e+*&api2-b^61Y?>tf8r z)#jZDE13&F^hD{YB1QMVI7% z9MwF1yZ7|%v_$+1S>!rK7+8l5wVJ_iH)3h%hv*OQ0`x;n+rlHfuv87WewkB@vP^!( ze0iSK1l@dw^G~zb{-rpVAV*Vtz6)}u#JB33FP9m&mKmFUPr4&_L9P@|6asRk%$8i3 zvv<**2bLAx)1|j4&NtH|j=W0c!?`tgH>!z@b{U?jRXimFX6f}j9<=q!z&J!0*XhcB z>Ft)N&2)j*KQF7T8ZKrZYUshjGPu!1QU?eWF9EU-Qnrlilx+wYGf3H%JShG9N@-ir zchalHdlTXB42x;sPu$U^62%*tURGMN5*~GrdPXVB0y5tgRJkfp%wvtveMQk@pTF40 zNS>E~Tgri1p(lSL$P9g8JATpXMGWJ|2p!i{%C58}BWDKjL+J6FB)MB<$UVZ`y%ktC ztj5zhvtXte+kydndC0qDsLA5PSz{f?_w5CA(Hpcgx(7t)58S z9&ne5xo-g0&Urik+xLlTCx(wsvlZ5BvK}DAlnv|D@PYZUqT=t=9F}Gjyq`OI$-({& zG~NK(fNZ=uRxYV{JEa{+#m`>$zErV@yRJf_Kx+^vUWP|Yq~u`XmI4lh`~DR{oIc`vFWDcwA!sZ9L2Y}_VF1(52G-cy8tXEso)_hyb06jtC7{cD3JV&L>$Gd6L)kEaKEt=%+f?K%a|8nDHEn*|8 z)8d=aE^^t5%SDrp%&V-)jgrL=xiPImd<$_nD~ zf)#JBlA2>c`V7cqKGz0x-(n!yy5> z?c8aLW}B>SPN^y`V)u3cO|z#2hPz#Fu>o3iy=A1_Zupndut(yoBx@zb9uI`mHn}OY z(CDT!#p^NYX?2)y{Z%oR#=utFBys>$yeX)CZ$J`5?(4X zE?W2PgAHqVZrQ^UUO6gIHxHm#jv`_G0fOSzN*lWDac_>YIX|ru_0`eq+r|K6Ku!__ z$@ioGrOVjGi$4_8$KAIndDbDv0QS2??Ss1e7u6Vo#-nB@w*9@mQ85f7e`8cJTps^F zvW)?VMU$N8gMYFWoB6uY$DqsweiNyLBK5&_Ycvn25b%56X5Z>WbdEUmBXVqPhZ6tK z5yl=hc0-BckF;Swr=ZT3q_;t4J)isY){S(jU0wx+;3|T*IxAeziVOz`OgNQX3n-NC zam>s!86R`i;CKw13ocZHzaW&q^*jwrVUC};iPypJr>wZMlD+uvBp;x7Z*K|c37k}Y zvK>62r&gmO3gO4#+WoAHN&14V8eOg2fyWXHavxmHDuC?84Q}%y{F7x~TP@ykB6}le z@T$JGb2Aw;a7Cl+c(3HV$26A6FL6@f37Iy=cL(oK%%}$a6xsb}q-?XFJwo zdJj(qN*q4&qsQcFsg*q-|5E_2g$YRpyqnC0PMn9jZ35*0EQ+l75!FKEa zr+JQM$ z4ghqs6!ptCK;N)NXo{YZGwbvLK;O=8cq*odws9FmAEsMBA~ng z{rcV;r3@=6wK8&Sa6xtkgOmF_bjh;0-JrE-*heDk7Zd)30Cnvc zSRuv;$&q^dJxlS_m)Re2`Hy6cqe(os0*-6Le*muldrko=A<#CLKo1tG9ec#97qc{O z%3A*)$B40e?HB_uaKXZcT#T9pr(p@^4_w7F~l7jAoUPRaSh- z=z-j1T4>Z803ZXe({tl>=-V%AL+_q=(4o*w}roh-=tAn z=ImH4Ql6<@a} zY=r*9rHd97)D>JLxR0*u{v04O&;+z0mLEY}-a7dD-I-8!xU4~zWE1ECz!$P^+P%W; z;zGmC9bkFzXtVK2-o~|MiGy3fq%nVoWTF4j!zej7ue0kPZLZcb3! zJL-PdueJ8?wWRunv78M>>84iDzN1Rh!U@FICUX)@a1cQ*E1*MtSMr+W{Tr622-lKb z>?Ma4wxc%=XoH6hUfT2K0#0&GDF$zbNQlGNQ%zGIRu3Yc@!6rAQZHcZ$E??Kq)}&W zw@vK{l!dR8{;z(Rqtt_8OuE;%sR?cA6XN} zzpVE12(X=0w#3aUv?a|g$GHua7A5gSiVHoV0MI6q5}hJcb+6#)EH!##~ zzUXu)3l9bcwWP)Zy7ov+fe_EY$T6!GN_qrkg-1+*u_7FzFXjKx-;NScbloj-J4?{y zQdhrD|Ke}bKkbz~Z7RdKMaR6Ib~Y zXTp$Evfm_b){H$EQTj?ki&3I1P*rj9&^1lXP!_ODk5Mac=@@T_IKOhGHteGX180%I zg9b+gWB8hc(*%joE7zDBT?I%8M)aXjG#*R@B&~DG2y{ruXPIJ=Day*-u|mm}mAP(8 zgguVfFD2?f9@3oZwixdqXwv2s;Ao*?x;4tm&F&Mpg{#Vk9>J0e8eu335N7E?lm|iR z+Nb*4D{xaRbF%v(a>iZ)Qp5`cgQi7~OpGL11yDrT!N4w!O=g9rRb~1kla4+B0cr$} zd+%h^G`I;1INEUv6t>U=6nIX&rwLe;1dX-`_%(eR?tk=?2-4l2Fz#lUikQdSu}>@z zjKrI5`6$dCYVf1S5`%7bdSDWPk|h>4H;pzH;FSjh`1%f*OP_K|2Ju;n-$sH&DeqVC^@t6Tu6HRx9dUmn zl)}RD{@i^I@^MO@H(?h9n%)D!t|5cwt|85Scve!fmI68U>}jYsnH;KZObB_9-H@aQ z*Y2%cX|9+u4fB?*0t-xzsHgKPb!cT`Nqu-k@{qKFrezO1>on@ArP|zQ$NHllRHFgh z=5%ceHpyP^OlAK9xNHC=pZN4TY1>BK?D8GP7xT6`dd+P!soIODb`;wLI{keNpwr)4 z8K%J*KlGJ=E(VvDg#3Y--s?(9au+UhFpH3DKtaAru34XBe+UE@Hz}TRc-!5kT0OH+rFF=(*mRdW7VP(bVhYaUbxb+= z7gO+kgzQ>e;ghXI=Pk*TWgDvmJ-v;)zQR+;vf(F;kTo<+i=p zH>(j1zF9{T=-tA>a5XyQaB#@X&2Vt5lpVRNX#ewxkiGL%>C@`OHcKIhKQP=Txl=Hz zbzL`{PlIXzWk!&rW^il5OLG8LI8`Z1-5|N*YAdG+Mv$7o1mv%zo4AM1S=Z}Xb!eC@ z*I1so-mAUZbR9q^L4uDApdnjng|kbdgq2HaIR-JNdJXi3g|qp19eSkj>#72o);E1| z**b!mJ{z;^Pzv;k&oLNQn$Fx+*Iq@|3iTYkH>9$Hk~z`mlX_jYJn!P~t6LTtT#I2J zSbwfTLNc&^AckSM(i;5CVE4>Sx;`tp$_BG0vCX;;!V8LQkUQVKzTXi+%h+yCpl0M@ zUc&tO-8g{Se9Dcb0LV-!oOpi$7NOS7yWcGT&l(L=5e-%C(8_cBvu>+L zac>~GRk}s95$0>;nx#3qsxnUos|#JT-Z+UCd92CuUz3f0{;xpj;Ye?kz8g`Vs8|oa zAfciBkCy%Sci-(^lkr2d`{vIR#9GRq1} zxWa~C>xx^#vBh9(9q%B|PDtDIe%CCqft<1NbK_-|Oe$Na@-w45EEZV~h zUtxez<~vK|V>nWGrtr@~!Xb_@ALPhDjpcG+6&h+En~Ex%ZeaL3z!hbVFwITx%-FHY zuA&EjIFS-Zr*6onjU)~X#EtSqCLsAzZeBBvt*YVLUmBZ8Wd)~J)_A$H!HCwcK*afKA zvJwCqS-tSuP>b2&4<}>Hop}G^T?MYY` zG+==V(`WVS^CWWswY(mT$2_2xgB`3Xdl=9T3H4qlzT51U4t=Dv{@9gP1jf}Rfc)vi z==l;ffKBHsPo`}0aMGg=ZfO^Je?YXPRQ=j#(z!A}IboznE&?jOf=m+!v~J-1rkIW= zeM`@|Kx9NZGBWgedxvyhGv7ah7=66H=sV^VB^l%8()x zpY610(n8+_q-^NBpi;INjqOP9&I!>OnKZo{LS8&14(yy}ej-4}gHjH>{73w_R^<4+ zA1%~4?NY^c_6M1$FY(mlEzj9(%q+hN?EE!=|4Jx#4rT`G0R&#C8HhP+ES=sh zU?3jC3#3>xzqd}m-zdE4dU!ez>%4w?t0^8L1`}}~^4_rI{BY(Mh|bC0(kq49m5H~a z4TEWWHw%aKH|#;qE0o(Q?khM8Su`_cf2NsOBxqj3pR6HllJTXuUBAhm$pj@{@;^k= z%6n}4zU(vsh&>nwer$edXlCRzPd=vlZ(h=s%BNw$zsy^@kQTcF4Zu+R_=l|+3ZH(Onfuh8N4fgVQAF#tRVj4py_nRtDvGVNsjC3TS-YX20|&m1f=(B+ZYzh)bB zlL=KSP3F!Nmhh)&7>=*lR6a5!(n*dm0K^8sVc!6X5tN3B)0bNFR6GN}dAq)-_>&r0 zUx_OMcxw`@+X6gpx~&QRIA-A6Chdi$M`5{0R%5)`DMSg@cVWN#E>vtjm-kKyzDqpy zHeFm{NyqYiuXYwd1%3{@A9h<+lnnUV)pS*kL%7M*xlyp+lgQ+5*q1p1p zmKy988?e2?0yGtBXNMo=$8YxII&SgHtojVL5{Y9voc?>h1`hshEJ=W(0@YE#=>D!I zs@U<7K~SHt$!&M}O37{&Mm(#?jqxS;@}0C9O=!d8%lsPCEs$??F;t{uSr)y)TCpUo zz7l~XjYkFxlve>u2ropS_2vLlMjxE`@$Y&EZp_o)N~{&myCA$@vF{_#S~{ynQ8KIM z)m#y5wf~ZtiuoY*3s9-ppo$SP%_>x-GEg7-7JS(BqL~SiAuA2*7Fs^?7c=Ax{L+W= zEbQ%z(+n?nCLwfysQJ|IZGd+G3A_bTlQ1$MIA~F1okrK&0u?e~ zSKI}?f`Xk)O4j7!KR6F%_%MLN0mBCr4qa}5uNh&`uG9DV7pm8FQR#=AfX4wC<)?DK zi~&%hC=v|~Ad2GpJ*^~CbcikZIGM3klC5Gr$w%2rSR@Fxa7O79u!V!YMv?FG?R*7C(GCAAOXQ$iw^~ zN*__gmnrD#gJmz!IUmAwPJ%x==dCra=Vea@KR3UoJ|c|_)88P8R&W@ch5>Rmw4n3(o~s`?@7(XTQi?W7**k{-l)$nRMSj8DGJyX^4PHE4+jiv%_WkZGV( z0ERmhW8+xfQ{>yVSv=8bPYt4*ZU%FYF%)BhlO@ozXwX9k_YN@JvkNH!I&(i9TOi#N zaynwnsU>$Te#)u$ZbgO56M+GY7#P80ESi9kc_%cB9Ja?{{3b{v6Nu^2sdpZdJmW$f zq}^V23O6xZn(ibt!tP|wU^<{y!0!{Hzz%~hpra_*0$TE0GsJy0RVeAdiIf^5UL_tt zjjdCIXF%rtaL!l#@&&6sj*=M6b3z=DweJbpbKehdcwv7)V-)c=^xh##v@EEwz0emi zLE#qo@4=nXVE}dd=KEOZr=KM=mxuj{JoVOO zMcbZ4j4c|r_2NU-vLVdd5>zQmqGW---A+H8o=srN7Fg%82C}t9hXIQ@dnG*0G*=>P zV0mWqT}7o~% zFM{x+#AZWG_kc=mvm$**uE|&046Z5+_@=Tealuy{jpF<`q6>PIwNzk{stj}s3*%GjfjKW&&f(py0(0>dg~rzi>C7nefk zmMAi?r*=~F$c2+N7Qh3RtJV)|G9LaP(UpfoiTu*CqO$bhJlo-U+CS0VLB9OOIo9s&yc z1!Vlyf_v#8xu$-``z0BQdd2tcP%eL#;sX~bmw#Kv6xkSU(KP7SIb+j{84p!kYxYvz zIj&75Wo8%b-MdILIgJftGJ=nky?}V@8aK0wuUyj7rhj(t$NC{h8(DXR4EKemtY=0O zJDOV}YN}a8n7r5?(2tyH96wX%63#!q991}*;m%s>`cNhFI+UKNA{F8kSYdKuR(xI) zvW1kAbJPjHeCMj@k8{j%`yGkFXrEHckI2aO0VHbc#K%)T&6m6f|=$|+;Agt z$I**8fGRyB0Pf7rk1>G_Pv{%Le1fgRn%$yo-ZO>LyP=wwe;j<+067)-focKa7&!R+ zK&X@--V+NJRV@G9i|Hx0CtX^EdkEE37{e29jyYpJiU+o+GX!!Iw`F8ccklkl5)d-O z@w53NFLGzq`p$U8)!iRMe(?NBRa^Rdd4E({wKU06D z;$YzR8TBIVC}y)pRhiK7YJEQ8+0zS&n}o7cJfe?)a{nbK4jAB8zY$N*j<$ZQB`d1J zQLY`}raw{zcpYzC0pOdZy#zc|Q>f2wJ5_|A96h?cSPJN72bz)J7TeP*7ngRAv@doK z%&Q;+z`7YA`W$$NLP;65^|>Xt22{iev%}T#(n9f}wO337G#>yS&i0zutLWJ_dTM?w zwx;x~wG@yyd6-7?O@8s2Y$MFpI|8%yF4_ikjJu^S`l{8mZ+ZAQb&+aBl4~IeYXkD{ zCnf|*P*GO`AyCmam$)_TAGWqiW@d_ya-eZi>PX4PMr)Pj;Q8lG9yS&+1n>&ipDNdp zAISk};TFvz@Uy)S$BtB=D1GjBE2oE@?~Je(@G=_f`ulLWw^NE3+VK?$A7+Igtj!y} zk97mvNU-0L0w86G4neewFb$a>pw2UomSTkKsk8TE%aUburc?8UHaU~^I1W8ewe5aV z-+MSHPf-n&T2!D!@d2e43g`B6Nvx8Q%;PCg8YpP<1l4GpTQ7u#0`Sy=NW2t^5f{$4 zcstcR-}O}PwapxJgcJdEV@6zx@n)6PJRs*Dw0ytoq%FTz14hD*rT}mXbZj&oLil8P z2g8@F=McP2eXgBs6gP3_?N-x2Ae!7p=w=(e?PZ)$T)iw745;0}9NG;ymtKbSl~%~J zRS1!FJZQE${TO16KshXh%LB?`EkYkgIAR9fA`0rKfXwd2Yc?yi!aH9acs8H&ge*HQ zKd-TSziN>#3AM4@$*O^|{I%Pc^wZQ z<*9N4IhzX@0dyJ_a9C6NB~+#+8oTKP^llqI{87#mOF5>+P84ENzZ_z9= zbi8O~ZeVdF7%Yw_Btv{WU`q?<+ix^utBw_!w3AY_wx`7tQt9}|b#D*C2(~9j2}>S9 z;RwslfG10aV@%vHCi-1}mC^@p<`y68xNDdDNhg_lRJtTHyJ)LDtaALfz`=WJtge_@ zm!!0OSZ8$UuJdpO>M_AZV84q0JzapIVRS;BmOobACR2)Dj0y&svjG(o8py#)Yzsi< zs@m^-=*n=4fZZ2FILQ0Wnk!?{AW92q3*XhirWZScQL|(8e`ovjN}VW8qV(ojD*$r< z4^QppSrSAHxNb-!V<4GoOF2M3!Il~A%`)4o(I>n^c83l})dHaKuK=wSFnNQ1qwuW^ z+PV&8A8B!L%)vt>7(ts7&~0J7?&kevehd|Inm*|O{JVfm4fxp~06!bB`w9e9bH5i# zz5h9SBpuEEcl-vx-nd+8`kpKG-e)A2;IH@%e{%izCzNv13Mp~3)N<0$a1j6IM7e2? zbc)4wEaN+iq5~!u(>heU7 zF4_||pkq*CwJ37^!oxDK>9f<1pYF7%Ldr#82f`iLfdCjmdREw}W3v@Mlq1s6|DtgR zB10#_X|7ZYm{o-ToK?n>vEM(e^JBDJ;)lKM?}4B9wjRvM*V`d;EW+(J1qWk%b9W;c z+BE=}D@Zb)|MFdCoO%#kC%FVMxk|3(al*6{yX7FCCJOOM2vW2Tc+k3{V?U0B!dgQ*4^TQ^Jo{Sli? zH%l=aGuEb9iFI3WA5 zf<1_S7u+nf>XB#$2IUcKP`Km3pr|^4;2@(%Os_X}Q+AJ;UUxTvAze~jcnOmhpe^@Y z$eRZ(5B~@M|7KWDnq`{6NZ$G1MpApQsRoe$wf`pn|NqM}(?eGlB0saMp>8QY1B*a2 z@;d^JrBv)hEYl|BNJurGVv#T_%U6_&@E|!@@E|FCSnwbYDe8vm7%H_r5IsmCzAB(|Fx)b8cfK z40*~3v1IkSB-jhOK)F8Xc(;I+Hvz6nNJPX+=4?;D>-u7^1G8_qFRRb$a*I~iI^RVk z0XzJMYZ=fb`QMu0h;13Mad8BezmK|09IXNjKzD&+)DILRp!9v%`-BOg@M+e0_k%As z54_nRXW&T2c-l@4gMFuVp%DmDg);kX1}y_OYXAU#tckMxuJMca0?IZ0Wb*dC=wTp# z+Y8+VQXN#AUvXbp>d7`Et)mR)r=HSxSo(#qk3~kxj>cQ}&>rVG&=EjH1!`bc0Js26 z+(&cNGUVSj4pPx*OLmjj+U>t<2NuNSwK+g@bd4eY=ZI zbgrKQhvsz(S9hb&V0iJz2RC6GW+Y;c`!9|SCNc*(cLoDV{rRWg_-(>tbs&~YA`nNT z!mt$&p&NW>TyW``3wNdoQS&Q-RdY^#NkHJvH6Yjrt_$?;tj+re7<#)AilhTP4-O16 zr_ra(#VTP)De~nFQaYghxUMQAvwD{K&{W(RIP*J#oB*01irfU0QT4~J{pZ#60Ys}) zJCwqmWEs`7A)BRWgFr3~R&sv>4a=nB@J{>g%-!YpQVu)HQDnfCC!?B%zkcLuI=lwP z>5=Zefxt@DAsS)C1DO1b=1SUj_+qc_7y@d{I~0Nh(DfuN)->2>GYsw^4%-+?hEc$0 zgPbY@OtScD8oK%k2H~Jp81lvqOvA7M0nGh=MOUqDdG%zG)huN7F?U0SV1;3PyeaJ4 z#?M(OC_kNcB9t~Sh+{5J4uEZfR|vor7HYw>qSQ0LKM*MXMDwu~V&{9*6$Xrt(+=F9 zi~XRkxS=oz%^&c}pwQuX&*1i420LQpIN;{!IN32*K}Bp78l4*)u98GP$IG|oj(gR> zUQlT@L<|8Ge{+-WI7V{IfTIF0aQk>8po3o8#{=mR| zdI888(aEr`Nd|KNXT2ee+ueQ1OYGe2v3H*B-{+@_$8|Rv5dPd`=5gSr_bSH?!VF4( z>UZP_MavD4uFrP(7yH>fA1aX#CKq6)ACIL67B(4}+qSz|$s_HCZg1=PMt52l3FQOjUj9uo z$JlZH<~kX$7e<<*c%p?IzuwOdWvS3cjyKXgt&4c#m0CfYDeG> z2E>;f0GR-h;FXqjQ0hAoak!yAp@%Bjus_{vNm*!g-QF*D3eft#46%8TT^vA+-WiahC8A{4RiYo#e0nk3dc%X~p zf75|R2Ui^jC9nfdYQoa{Mue4Z+1SUOS|W>3H}xv8pc&vPK}3;Sq#?W>L~Rizqy)u2 zwc%o{fwrAg05OcZAd5}v5@Faj*jW(GY7iWPVxA)rRDfb|g(M2!Y@p4HvOE4-9Mq7+9cFD?S*)3$8wg`opU(?-|8g zxxM>dsEeNMI;kbB5>y>zMmtqbV8{n;5<%TflPo}!CSL~Jn#B5Q^J~vV6hEzJm<#HQ zu`B)c!?RJd-AX1`SfiF;jY8hLY1B+DgQ4xOg6|)6-}@|;6ZnI7M&HAjJ4Elfegzy* z{hLM*-PTY2o0O5D@SFpU1DLN%itW=^HILFZXQV@|btD`hW57lmAes#V6(DnoIGB?z z^Yf_NU0;nVi*>;=u>s>Qkd2c^-#BFS(%~{$17%hS_*;PBalpL;79r3j=y*&eOi=+K zR3Fn}nf7iFD$?5#dc`K)Cj;$=?NsAZNO>XY(nzit^kIyelBEPv)Ue6pyn_GzC9(}N zDm`(GIp@@Z20BMRefa4$o9ETp@IDkFHJ(q|(dB_u0n7pM@ zG;M|)Uyw={WT(B$0FtJ{wuvf0u?K;ugv^m2WvU>p&?~1as(KU`1r+9&5WTDo?l(F{ zh_(b$0J~5!(Bz@JxMLYYjhe~{zz7()+fIRFBv$A0v(^@Hx}VD z1TH1|@42AP<@rT3f}^TovNx{5DL0D7MNKLd8EG-Ovju5;*c=RNSpOZqFWot)L?BB= z)Ng<;phTQEK2sDW0 zzn$d+k$%iSS$qFJDHdY@Y~`R$PycR{LHl$q5|@5UJP3uBv?aN{lis_;QzRd4#g8!R zccOk&xzJlxKk*fxh$bHeuZw3w$;LxUxAqchhJoj9Bnv{DG=j1 z07`?&W5mD-gGM6-*3m=1V8u5qL8fbhK2k60Lo{R81BZW2K%HTi1Uf*jQK)k09&G}q zb9)X2erA;R0W`*LBQrM5<#x?IrwlWzItBK}kbW?u--=p-8O^ov6m5XaHBGKmG4jdd z+0U6IxGzBNmv7I&obFtqiRYBiA-iYI&ORm7292YvX1;C^FvF$77%h-JP9CJLWwLHi zUkN08Oh`TeNW1)uw7mnEqJ(8EBF)e}2-6%mN8!!o&P2+j&Y$*=8e@q>>TYvZuRFAr zg3TWlA_jIGS3eOG==o%ZO0^h4`pWa`{Y|(-5j%nS3A;>bYjHZ@UW<`$M@^UXJBpjm zp#aU4vEA+|YrXnMKo9}`1{+{w3SdQ^WsREEJ0026o0?>*MpRmyIc}-866l(M5YNIo z2G<0LB<(rmz?VPODaYiA*^*$|Hy!)~CYYCSrFO&zs~az2O@JhtM0No3EzC>!vbgaC z%Do*?E<=NIZ@(&%1MpvCyl`pmZhZqvu~aR`X%z7H- z+cSNW=I(q#uG!>+Q+h|31=ty=F#Y7pH4|Mw8_W9;C=q+4}lnB3MHxo}#s_O}bG& z#OyMNY2uV)PNuNP^ck-1wGvlX`2333ivgo!dIpQyf5(9EFsagc*Y|8kV}ICZ#=Cw+ zN(9pU%0tyGNva}>I{X%DoYp&zj#?dzy0t>`Pchk;L^5|7J>Dd%X>$(C?Dmve7#oj2 zZYW|rRC=SPK9#^U^X5lsyWFm3R;Q-vOJw=fZS)5v-VB9_4$LcBZz$e}u1KO^Hn_Se zZ^$e@xqmyh^Jh@R7&cMF%Zfag4@$3lWrQEoz44ZP=csC zjaXAiD3qv6J_(ZQ;$GH-q*#P}{5mtVuJCYhK)-H59%kjFh zbvp9-iDopFZS6CUFTKbVa*_!B3n}4}!9qgqmhW5(%pr~xigb#tJ68VU4g*fiR4>J3 z(+S(xunf&j$5Wa-J-rx3@LO|3^C+bavDjO14r8R?z0MB`yo$cI-}BdeG^%YQr%Aht zsiS4OoAT90?eYEa$QD=Y^T)lm**zQa9JcEDuhr*k;`ute9~5uvkQaFNpdF*dawE4S z<%)^C71{k7-aqqH6$3uxdMl-bC8_1sH^I|1k!m&S0s>0c3Sw?k9eG=hU2iR$N9L*f zJ0F;2zkjRH3F_plA5lGEo6LEAyIEM$Yu}jm`DL*N5#_oA$^xYn+>;&+Qx!uly{l4L~Q*3PC zwj-}+m^-|{O;MkzrEbw*^{eRnMp3*lny^vXv(jBfj1*x@KX7u+dI<&lp%5|r4 z=Gk7zqpzjrugHCwS6K^{mcQ)sQ1VU9nWh#^;0-+VB05(VaL`yMPm(3FCkwrM%1)si zrIbb^<)x&0cDkJ)Q)HLWPNB&^(3jV_A6bmCX)T7qm0Mz1Cwj#9z9GG1>zd)Eblo~c zJu}(h(3g|CZ#aGa{jKkj!D}>}nQZX*{6Xrt;t$5jdyQrX_TLKqES9n&UwS3~yugU} z-Y-t+?KYX&UA!M&ml~Aaib|<81D!E?stLg;DH}S&wq8^h{n9U<43xA*kanRodw6U~29(cCl_6=FJ36x{z8Fn+TV zgZ{xT`ZRSmgl^gVPr(1kT}>UGz*V0D5LPA@2)U`9vAv0AsgNvgLER~5dv#E_K z^h#1EW>zLv=09nnHT=J=6g2JMRkF9Y|5riKHrzB3Rva4(3kUPfcL@3KUinA&3I6FT z=t~9pVXrnfwKE0xpV~VLDuA~s!20s$ZA>f_vX*u(?&SY`pzq*lZ)Ixi%*@HnLLuT} zX=B33&BMdO&-@>+yLr7axQP{dRV$;3p|hzVs39jK_>YxSm6e5;orRZ`{dc~9rsFp; z=KbF?u=297@^WzSGyi!AO=V+fXYK;Fc0p4+Ml}`Kvw!_`Qv*{IOJ^`+7>zxQfh-`% z`n$mY`1zk{O@3bqE2yZ-0$vJh*`EymdUlh=#mUr>(Ztlu($3U`9F`C|#RMQyc4qeE ztPpU$DD21oV=}h?yJYPDcgZ;ZmF!8qR_Yeo=v>aCj9%`zg`Rb`G1zch`|C^wQ#XDvNN=_abkA<^G_xRJ99a8 zbZ%9{AN6MXRTNrOI+kozi41|!x+ssT%(zY&Wr!(crmL`GOiN=atK!k(Sze`=PS?K+ z5_WCX8T@gbaqW}gwdgf?-m=-c*}Qo*aEbRzG2Q=^gb^JbJupAG7@p+<(T(hca*0;7 zu2)o~qo=f}_!XLaQ}XTuuJNwnXukTMoT?M@TJn|?wtRh;lZZ+dh%!s9zWlUCJe5wE zR-#7Csud_ejAb zH832keDhO$vZeQ7{TJ<=eUA*d{!OFLrDY{Ye}jH@H-$BI%73Kl$0Sq2)*c6~OT^gM z@7{2i+`)#y=idA&u497C+5Ksu5!|$>-d*=HS3;%-(1(uURIc?EqOoMY27JDq9KC6d z${r#-ls|qoCHyHCE9sqSmZIy>ez2cc$y7klRarvB7M0PY?IP}@Rrs0Nb!jcK{;Eiw z`zetL#@83iT=(Q36FX@Mo!z+>`}*nbk%O0Aq+$$T=s2?`=~(L{te~jn-c0mFqJh@= zsK}Q+xQQgLPX@9AuI?-hhOGzx^8Qx1zx@1j$1#1LJ+;2`lRdNYf!!V|^a#KA-9NaB z!@JDSWm|kJM;*G#6IUK0mOENA;GbZDs8n$GUiUakQ0p+hHpqN=*5pgS{%uU4dDITs@H;HM%FQ?i2F_zXqVz4?*3Vd-r=)nk1D0lL5q&gYrRPpdiE`W`SW_VHk zP8sA(PheK<%eG7%b$=|?z2bJpSNz~@Q$Q&BIe3PE`F-bfXhxnh{nLYeHj6`N{O1$YhJi6=*_7eJVX}r(D=h4C2 zJ1_W4gdMdU8x@fS>tgk!hwv&$W_@FedGX==`fbI+3JAY#UByT+k&6YRg%LH+_X#&e zl^%QJKHB*Xg)0Lpjxo16!E}`aJbV1gt2f^w9^6;AMJs4+a)ziG3inZX&%DJ7a0<_0 zbiAj=qFeR6_?6y!#&blT0+*-nu~_MreZt)Qa!#n*?jbW2CJQ!f-JuW}{Jhd&s+EM$ z@C0F{^=%Ya68#Ut6^gA*dn{Vg94Dd!^Cllflb;Qu@CWRB;NDGSyTaK1CVLxvlm6pP zy@8R~0@^g2u`vW>UL+>^7v+Z=7L;6*$KE;l`^)`le%^_`6+a&KZO}3Lowtk!d>lk! z&iRrn)zI^eBex+6HBDqI)vrbq&Gu++e^O<2yK(bD9RzjZ;ya$0+Wj-N@_K4Ivd{Ms z1RrPaI{UfSv3zAUkvfeNY3NbpS&|)VY@Oy7yl-;L=$Vf0>*wijGu<5g?+vo6$CP zwD$y~9`LE%&0R}G8n(U42}nyYa|jN2q9vrJ<((nm7GZU^cABinu>H#%kOGTqC3q_j zS`UBJe;_^V#ALOO$0|RU$!;sLXgF)`(tVymq~j-dHLu5odl60ltY|ABmWb> zf^%oB?+xmqj6ddxe6Xqzi@p`xwt2I0jEtj)an4+nvrp3-k;NS3t>i}(=nQE3vcWH} zlQbF_NDBFo zCx;v*>%mRdd|`{H>0+pEY_l>G;T?}{;|(sEoP+1AVqWA2)|otLy+!YnRTG!@NGhl8 zLHFc{2o&5^*mvREcI(LO((laOF6b}W zSZnstw^5PmPMO*L#eeRM$0%Y@Zx4LjSIB5Rcmjfcp872JfBW{W)}hS4k7|+Numpdt ze%1oFtE-EUJTTlIYtE|6`?Ifik!H+@Qpu3M#DiB$jot9tNHVHVUP~kdv94_}a##7h zd|=`>F4F>G2)lJ(op*OxR*6ncf-k_ch7TclB$4zoYBC2kOlrFsX}dSWC3f$1BG$|O zNt(~kOWsjm4VxA{PaQKkY_(Y(F!Z#%U;8tjE_bLq@dX12V5%TrD5%;KhALcOE_aLQ z%vgLwCK65sWhRR9akz(y9Hx}Jh)73EgYuIsQmOh+cW?EmYbZy&$PFY2(mT$wD$i59 zWu8sqoFjy(ELBOq`s}Izk+euKgc0tkpWs_BamEK(MXY#N`03>)WzU79v0aDx`ZXRc zGqX`W8m4{uRQj709bV8n=?F4WMSW1$+nEN&ya~}rx0p{q*Ixb5em(Yn+`?7QjEx~^ ziU=>+hvbryY5kU_Ysv>o#+>BWA^Kb1w=wNr7W5_O&k)#Wvz)TMr!&vcH;dWmnavlo z))nskBs0TK+M~+fx%HJ7&((b7aL5gFs@+&Y@qam3;5l}LAP�+nbfr>Em4s zR5{nP`&&EJ-@{lOkYk@~yvkUKPPgk-L7rtv?X<^TUet^6Ibmu|Fb_0#9vvSYUCk*9 z4o2)A&SVz+2mhNj%p^_s_S!K7qGVv_S5vl3a_!b)ZPo*oM%||mCEX? zSA8`{h2Ta#(X|`?jk)hdqCT97{jgiVR#myWSh-YVoA!3FvE2u|7cPZ`%k5-_-A2vd-HlZrochvs6 zTB@hGSi_`H7aeUgF4LzLade{ITAmf=zL zEaakiu`)%yMt8=i<~;JKGbTiVFZj#Up-$Iy!1U!l0%sZ2nYu{4)iPRPO23Bh7mGkT1LNgqf3K zvuRFFIM;|#i34%f_?x^sVjZZ*y?HWyGTR9*T(zR}6<6XBmae(!Z(b{xMd=fdKCFAN ziYJ;d783DTdno>PFxS#kvDs~v0$IGZ!ByNzrf_A(xZ5PT4_s}S(OyvmLF9bSu@7&`;v$$kvc56g7Jn(~5gP7ZnJQTrbf1m$fI>&dI7qHMe&^|ZnNnui`gECJcC~ZrqeG`!AJaRx{3XOHIICR` zr;^P-B~}(-elZh2KpEc-qzOrC^6eE)uUpI^HmVnDe8x`wA==w_IkN5eO7omg*}>xD zN{$ZNGViyuuHEnN&%S92f4Wy0kpXH`Dh(brq))TQ_8^>e*fDN|jm*cR{iJOp{-MKi|n z7p3E_dsl?R3^q-MV)$M>{k{v)M2PR6IFHyEViA7Zs`S;XWiL$pB$#3QRV5_p8{c{B zCzqlKgxWK2l8JjI);^crpS21)y7E%&anRwvr{M)WF1Xv96_?$=KgIUdBCO@!I|I5X zgkX;MZN!dGzY7pg%f(GT=b2!@Frm$ut@(XiPmR-$`3S49xo!q3b zRvatpQ`ap?gm!C6d&t}{{IBC->@KeBBK#BX8kqtV#Xc0E&qsZQd}`vJ1Gx|ADym~)L>bRLW!M~^ zWtk^^q={QTv9(pTA~Z+O&I!rudbIo9YP<<@*=ZM&MPGoc}SugA|vaI z+mEy&r&PMBqZQi579?M!MPi1vN*hM-y|{#NQaleMyt~YJ#H}S*fA?Ai+d`tHXc@AO7+hOSO+~~Ir=OB|#U+o5l>Mxl2Rz{>R3z~dN=YJ6r685zC z;OM+apgMVj5M4cm?#h53(f#U#eKtuqbMKwac#stmkBEuc?P_`QA@`g)o_i|1%mut5 zWhZm#hj)wy$}jt7rwDh3 z(N?X+=dyNfPbzD>H;^29bSFpbPvKyMuoa#C8ieN@$#fFw>V(pf_&_Zu z)Io;DykkIGSu7!Z?QYx$iEf!?o4j#D?P4ij(UwJvknJL3Cf$yJdlV%d z=iEc=Q16+3U;cCZG_8}=ObmIh=bD;Lu`#FSJX;~D=(C}s-a_UYiO8DIPCN^Vu}vp0 ztkBCp(o*@vb(1jkpebYW9BR*a!Uvy9e}YJSX{VAG(~HqLPq$3zt&PxVTW{rjCsexfbH8G_hyL zpGK_^_{`1Tf)X>HW93n{i}be&d5wo2gj9u}DA`6Z@eZ;d&g(;bJ`7(|H_JSqZ4s7Q zOM1A^Lji6vl)ZGk249>~nZ=J}(Xy6uJvoJ^U^`W+ML8XV!+q@rBl1hX93FuWj&S zd@qbes;#u9%?q%+Ud%!@x8X6O<%r_E;DEVyrA)7VL&xQWw zmq&T$gOus=(YJQUTyo&>o_A;CRNZ%JgPVxI5AB_uLY~r93Q?&B9x1>v2(~Ow-_#0exT1zi9{4hod zeS|6+D?F5wU1dp7qR0t>#O1pd{lYxQIm4Cz<6 zKcJm8j2ESfYGU?$`m;+|ZEvLh;>QOrU4KFcxqSpSdWT58+pWVo&(~%Qn#2uFCG2W( zy+v)69$Fm0I}G&K50@5tkh<2TpScLpg}SG9S07I}-2F5KU&`H|miT=)Xe5i8C*E!w zi5HH$M|o1&T6@|Q&Wz>D!?xVa_@G(A*Z7Ex$+nxMD6vPBoo+OraB%W?kdr!(%&4M< zYkl=hgeomieN)4IvhDBonEk-$MjwBhRE0@0YJxxhz1mp!i9m^g-jAhtz7KidX~=a+ z7KN9-YUC4r`hP$Y~+=fNAv-k5zI}_%FXY^=JaqU&Ev9&G$As^?06y{OLXASly9F+aNFdvLYiOHFuUT{ zcL7<(3+1UR7}a8J>;APF5*(cM{r}VcbO-EDa^kAOj8gJXnQaa2EX_=voS`PXveA7YZupW!i3n$rtDa=#?Wg}cLGTb;hEzqrY_)itU+ zTgm9$&f9k$*szIN>D*BXGE7!qJ+_Z2oD}s$KhaU4T$A^OV)kt5aTM{#eH? z_(U~R8JzNxyfh-G(}hhuot{sq=FM$*!I%mM)@Bz3!K193??l&~D}}S|9@5ao%P_6> zOd-TvBx{6lQay4-(WvuhKyLaej%ZLiV6p#jbLO%uA!P(-jqo*h;NQ?csG;gr4glYb?d_a_brU+&|C#Y`doPrV^Y0Ib-QUEV zKlz}~p#}b@HTd88ww&PLpcbe9R@&d^DAerq?@yiE|7?W%Q}&<6{yp2FXYRj0*Wv#> lf&Vk--@^u74gdaRM*a_LLs1491)2<6_yQPloM`B`{{`<^iPQi9 literal 0 HcmV?d00001 diff --git a/helm/software/matita/tests/TPTP/try.sh b/helm/software/matita/tests/TPTP/try.sh index 12fc7effe..e55733bff 100755 --- a/helm/software/matita/tests/TPTP/try.sh +++ b/helm/software/matita/tests/TPTP/try.sh @@ -8,6 +8,7 @@ fi mkdir -p logs +i=1 for X in $TODO; do echo -n "$X ... " LOGNAME=logs/log.`basename $X` @@ -15,8 +16,9 @@ for X in $TODO; do RATING=`grep "Rating" $X | sed 's/v.*//' | sed 's/(\*//'` if [ `grep "Found a proof" $LOGNAME | wc -l` -gt 0 ]; then TIME=`grep "TIME NEEDED" $LOGNAME` - echo OK $TIME $RATING + echo OK $TIME $RATING $i else - echo FAIL $RATING + echo FAIL $RATING $i fi + i=`expr $i + 1` done -- 2.39.2