From: Enrico Tassi Date: Mon, 17 Jul 2006 07:50:54 +0000 (+0000) Subject: evvai! X-Git-Tag: 0.4.95@7852~1201 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ae0673037e19c5441e5813bf028361ce45545faf;p=helm.git evvai! --- diff --git a/matita/tests/TPTP/compare.ods b/matita/tests/TPTP/compare.ods index 14d893901..14f552422 100644 Binary files a/matita/tests/TPTP/compare.ods and b/matita/tests/TPTP/compare.ods differ diff --git a/matita/tests/TPTP/log.600.15-7.comedasvn_stampapesomassimoeqinprovanellog b/matita/tests/TPTP/log.600.15-7.comedasvn_stampapesomassimoeqinprovanellog deleted file mode 100644 index d37bf6b12..000000000 --- a/matita/tests/TPTP/log.600.15-7.comedasvn_stampapesomassimoeqinprovanellog +++ /dev/null @@ -1,698 +0,0 @@ -Unsatisfiable/ALG005-1.ma ... OK TIME NEEDED: 72.61 Rating : 0.07 max weight: 21 1 -Unsatisfiable/ALG006-1.ma ... OK TIME NEEDED: 7.07 Rating : 0.00 max weight: 18 2 -Unsatisfiable/ALG007-1.ma ... OK TIME NEEDED: 8.76 Rating : 0.00 max weight: 18 3 -Unsatisfiable/BOO001-1.ma ... OK TIME NEEDED: 0.54 Rating : 0.00 max weight: 21 4 -Unsatisfiable/BOO002-1.ma ... OK TIME NEEDED: 6.47 Rating : 0.07 max weight: 26 5 -Unsatisfiable/BOO002-2.ma ... OK TIME NEEDED: 9.59 Rating : 0.00 max weight: 26 6 -Unsatisfiable/BOO003-2.ma ... OK TIME NEEDED: 0.78 Rating : 0.00 max weight: 13 7 -Unsatisfiable/BOO003-4.ma ... OK TIME NEEDED: 0.48 Rating : 0.00 max weight: 15 8 -Unsatisfiable/BOO004-2.ma ... OK TIME NEEDED: 0.20 Rating : 0.00 max weight: 10 9 -Unsatisfiable/BOO004-4.ma ... OK TIME NEEDED: 0.16 Rating : 0.00 max weight: 10 10 -Unsatisfiable/BOO005-2.ma ... OK TIME NEEDED: 0.32 Rating : 0.00 max weight: 9 11 -Unsatisfiable/BOO005-4.ma ... OK TIME NEEDED: 0.19 Rating : 0.00 max weight: 9 12 -Unsatisfiable/BOO006-2.ma ... OK TIME NEEDED: 1.05 Rating : 0.00 max weight: 17 13 -Unsatisfiable/BOO006-4.ma ... OK TIME NEEDED: 0.70 Rating : 0.00 max weight: 9 14 -Unsatisfiable/BOO007-2.ma ... OK TIME NEEDED: 31.65 Rating : 0.14 max weight: 19 15 -Unsatisfiable/BOO007-4.ma ... OK TIME NEEDED: 27.51 Rating : 0.07 max weight: 19 16 -Unsatisfiable/BOO008-2.ma ... OK TIME NEEDED: 24.61 Rating : 0.07 max weight: 19 17 -Unsatisfiable/BOO008-4.ma ... OK TIME NEEDED: 146.41 Rating : 0.00 max weight: 20 18 -Unsatisfiable/BOO009-2.ma ... OK TIME NEEDED: 1.28 Rating : 0.00 max weight: 14 19 -Unsatisfiable/BOO009-4.ma ... OK TIME NEEDED: 0.26 Rating : 0.00 max weight: 14 20 -Unsatisfiable/BOO010-2.ma ... OK TIME NEEDED: 0.96 Rating : 0.00 max weight: 14 21 -Unsatisfiable/BOO010-4.ma ... OK TIME NEEDED: 0.32 Rating : 0.00 max weight: 14 22 -Unsatisfiable/BOO011-2.ma ... OK TIME NEEDED: 0.08 Rating : 0.00 max weight: 2 23 -Unsatisfiable/BOO011-4.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 max weight: 5 24 -Unsatisfiable/BOO012-2.ma ... OK TIME NEEDED: 0.41 Rating : 0.00 max weight: 18 25 -Unsatisfiable/BOO012-4.ma ... OK TIME NEEDED: 2.11 Rating : 0.00 max weight: 18 26 -Unsatisfiable/BOO013-2.ma ... OK TIME NEEDED: 0.31 Rating : 0.00 max weight: 10 27 -Unsatisfiable/BOO013-4.ma ... OK TIME NEEDED: 2.78 Rating : 0.00 max weight: 16 28 -Unsatisfiable/BOO014-2.ma ... OK TIME NEEDED: 20.42 Rating : 0.00 max weight: 18 29 -Unsatisfiable/BOO014-4.ma ... OK TIME NEEDED: 114.97 Rating : 0.00 max weight: 18 30 -Unsatisfiable/BOO015-2.ma ... OK TIME NEEDED: 15.38 Rating : 0.00 max weight: 18 31 -Unsatisfiable/BOO015-4.ma ... OK TIME NEEDED: 96.29 Rating : 0.00 max weight: 18 32 -Unsatisfiable/BOO016-2.ma ... OK TIME NEEDED: 0.85 Rating : 0.00 max weight: 17 33 -Unsatisfiable/BOO017-2.ma ... OK TIME NEEDED: 1.70 Rating : 0.00 max weight: 16 34 -Unsatisfiable/BOO018-4.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 max weight: 5 35 -Unsatisfiable/BOO021-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.07 max weight: 10 36 -Unsatisfiable/BOO022-1.ma ... OK TIME NEEDED: 65.58 Rating : 0.07 max weight: 18 37 -Unsatisfiable/BOO023-1.ma ... OK TIME NEEDED: 141.40 Rating : 0.50 max weight: 23 38 -Unsatisfiable/BOO024-1.ma ... OK TIME NEEDED: 17.84 Rating : 0.00 max weight: 14 39 -Unsatisfiable/BOO025-1.ma ... OK TIME NEEDED: 37.02 Rating : 0.07 max weight: 32 40 -Unsatisfiable/BOO026-1.ma ... OK TIME NEEDED: 17.55 Rating : 0.07 max weight: 21 41 -Unsatisfiable/BOO028-1.ma ... FAIL Rating : 0.07 42 -Unsatisfiable/BOO029-1.ma ... OK TIME NEEDED: 17.53 Rating : 0.00 max weight: 13 43 -Unsatisfiable/BOO031-1.ma ... FAIL Rating : 0.21 44 -Unsatisfiable/BOO034-1.ma ... OK TIME NEEDED: 0.89 Rating : 0.21 max weight: 20 45 -Unsatisfiable/BOO067-1.ma ... FAIL Rating : 0.21 46 -Unsatisfiable/BOO068-1.ma ... OK TIME NEEDED: 2.99 Rating : 0.00 max weight: 37 47 -Unsatisfiable/BOO069-1.ma ... OK TIME NEEDED: 2.85 Rating : 0.00 max weight: 36 48 -Unsatisfiable/BOO070-1.ma ... OK TIME NEEDED: 2.76 Rating : 0.00 max weight: 37 49 -Unsatisfiable/BOO071-1.ma ... OK TIME NEEDED: 3.18 Rating : 0.00 max weight: 36 50 -Unsatisfiable/BOO072-1.ma ... OK TIME NEEDED: 62.23 Rating : 0.07 max weight: 28 51 -Unsatisfiable/BOO073-1.ma ... FAIL Rating : 0.36 52 -Unsatisfiable/BOO074-1.ma ... OK TIME NEEDED: 99.57 Rating : 0.07 max weight: 27 53 -Unsatisfiable/BOO075-1.ma ... OK TIME NEEDED: 4.04 Rating : 0.00 max weight: 34 54 -Unsatisfiable/BOO076-1.ma ... FAIL Rating : 0.71 55 -Unsatisfiable/COL001-1.ma ... OK TIME NEEDED: 356.14 Rating : 0.07 max weight: 26 56 -Unsatisfiable/COL001-2.ma ... OK TIME NEEDED: 4.21 Rating : 0.07 max weight: 23 57 -Unsatisfiable/COL002-1.ma ... OK TIME NEEDED: 4.18 Rating : 0.00 max weight: 23 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.02 Rating : 0.21 max weight: 20 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 max weight: 0 68 -Unsatisfiable/COL008-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 11 69 -Unsatisfiable/COL009-1.ma ... OK TIME NEEDED: 3.16 Rating : 0.07 max weight: 18 70 -Unsatisfiable/COL010-1.ma ... OK TIME NEEDED: 1.59 Rating : 0.07 max weight: 23 71 -Unsatisfiable/COL011-1.ma ... FAIL Rating : 0.36 72 -Unsatisfiable/COL012-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 73 -Unsatisfiable/COL013-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 0 74 -Unsatisfiable/COL014-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 75 -Unsatisfiable/COL015-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 max weight: 11 76 -Unsatisfiable/COL016-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 0 77 -Unsatisfiable/COL017-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 11 78 -Unsatisfiable/COL018-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 79 -Unsatisfiable/COL019-1.ma ... OK TIME NEEDED: 1.65 Rating : 0.00 max weight: 23 80 -Unsatisfiable/COL020-1.ma ... FAIL Rating : 0.07 81 -Unsatisfiable/COL021-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 max weight: 11 82 -Unsatisfiable/COL022-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 11 83 -Unsatisfiable/COL023-1.ma ... FAIL Rating : 0.00 84 -Unsatisfiable/COL024-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 11 85 -Unsatisfiable/COL025-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 17 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 max weight: 0 89 -Unsatisfiable/COL030-1.ma ... OK TIME NEEDED: 0.18 Rating : 0.14 max weight: 13 90 -Unsatisfiable/COL031-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 0 91 -Unsatisfiable/COL032-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.14 max weight: 0 92 -Unsatisfiable/COL033-1.ma ... OK TIME NEEDED: 4.71 Rating : 0.07 max weight: 16 93 -Unsatisfiable/COL034-1.ma ... OK TIME NEEDED: 0.51 Rating : 0.43 max weight: 0 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 ... OK TIME NEEDED: 5.87 Rating : 0.00 max weight: 11 99 -Unsatisfiable/COL041-1.ma ... OK TIME NEEDED: 0.65 Rating : 0.36 max weight: 0 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.22 Rating : 0.00 max weight: 11 113 -Unsatisfiable/COL046-1.ma ... FAIL Rating : 0.64 114 -Unsatisfiable/COL048-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 17 115 -Unsatisfiable/COL049-1.ma ... OK TIME NEEDED: 5.11 Rating : 0.29 max weight: 17 116 -Unsatisfiable/COL050-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 9 117 -Unsatisfiable/COL051-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 9 118 -Unsatisfiable/COL052-1.ma ... FAIL Rating : 0.00 119 -Unsatisfiable/COL053-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 0 120 -Unsatisfiable/COL056-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.07 max weight: 6 121 -Unsatisfiable/COL057-1.ma ... FAIL Rating : 0.36 122 -Unsatisfiable/COL058-1.ma ... OK TIME NEEDED: 0.32 Rating : 0.00 max weight: 0 123 -Unsatisfiable/COL058-2.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 max weight: 10 124 -Unsatisfiable/COL058-3.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 10 125 -Unsatisfiable/COL059-1.ma ... FAIL Rating : 0.00 126 -Unsatisfiable/COL060-1.ma ... OK TIME NEEDED: 23.48 Rating : 0.36 max weight: 0 127 -Unsatisfiable/COL060-2.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 128 -Unsatisfiable/COL060-3.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 129 -Unsatisfiable/COL061-1.ma ... OK TIME NEEDED: 477.77 Rating : 0.36 max weight: 0 130 -Unsatisfiable/COL061-2.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 131 -Unsatisfiable/COL061-3.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 132 -Unsatisfiable/COL062-1.ma ... FAIL Rating : 0.50 133 -Unsatisfiable/COL062-2.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 134 -Unsatisfiable/COL062-3.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 135 -Unsatisfiable/COL063-1.ma ... FAIL Rating : 0.50 136 -Unsatisfiable/COL063-2.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 137 -Unsatisfiable/COL063-3.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 138 -Unsatisfiable/COL063-4.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 139 -Unsatisfiable/COL063-5.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 140 -Unsatisfiable/COL063-6.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 141 -Unsatisfiable/COL064-1.ma ... FAIL Rating : 0.64 142 -Unsatisfiable/COL064-2.ma ... OK TIME NEEDED: 0.00 Rating : 0.07 max weight: 0 143 -Unsatisfiable/COL064-3.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 144 -Unsatisfiable/COL064-4.ma ... OK TIME NEEDED: 0.00 Rating : 0.07 max weight: 0 145 -Unsatisfiable/COL064-5.ma ... OK TIME NEEDED: 0.00 Rating : 0.07 max weight: 0 146 -Unsatisfiable/COL064-6.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 147 -Unsatisfiable/COL064-7.ma ... OK TIME NEEDED: 0.00 Rating : 0.07 max weight: 0 148 -Unsatisfiable/COL064-8.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 149 -Unsatisfiable/COL064-9.ma ... OK TIME NEEDED: 0.00 Rating : 0.07 max weight: 0 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: 2.51 Rating : 0.00 max weight: 21 153 -Unsatisfiable/COL066-3.ma ... OK TIME NEEDED: 2.07 Rating : 0.00 max weight: 21 154 -Unsatisfiable/COL070-1.ma ... FAIL Rating : 0.07 155 -Unsatisfiable/COL075-2.ma ... OK TIME NEEDED: 0.16 Rating : 0.00 max weight: 23 156 -Unsatisfiable/COL083-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 157 -Unsatisfiable/COL084-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 158 -Unsatisfiable/COL085-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 159 -Unsatisfiable/COL086-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 160 -Unsatisfiable/GRP001-2.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 max weight: 7 161 -Unsatisfiable/GRP001-4.ma ... OK TIME NEEDED: 0.18 Rating : 0.00 max weight: 7 162 -Unsatisfiable/GRP002-2.ma ... OK TIME NEEDED: 31.68 Rating : 0.00 max weight: 22 163 -Unsatisfiable/GRP002-3.ma ... OK TIME NEEDED: 347.29 Rating : 0.00 max weight: 23 164 -Unsatisfiable/GRP002-4.ma ... OK TIME NEEDED: 67.57 Rating : 0.00 max weight: 23 165 -Unsatisfiable/GRP010-4.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 8 166 -Unsatisfiable/GRP011-4.ma ... OK TIME NEEDED: 0.25 Rating : 0.00 max weight: 12 167 -Unsatisfiable/GRP012-4.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 max weight: 8 168 -Unsatisfiable/GRP014-1.ma ... OK TIME NEEDED: 50.29 Rating : 0.14 max weight: 39 169 -Unsatisfiable/GRP022-2.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 9 170 -Unsatisfiable/GRP023-2.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 2 171 -Unsatisfiable/GRP024-5.ma ... FAIL Rating : 0.50 172 -Unsatisfiable/GRP114-1.ma ... OK TIME NEEDED: 215.54 Rating : 0.29 max weight: 18 173 -Unsatisfiable/GRP115-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 18 174 -Unsatisfiable/GRP116-1.ma ... OK TIME NEEDED: 0.15 Rating : 0.00 max weight: 18 175 -Unsatisfiable/GRP117-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 18 176 -Unsatisfiable/GRP118-1.ma ... OK TIME NEEDED: 0.17 Rating : 0.00 max weight: 19 177 -Unsatisfiable/GRP119-1.ma ... OK TIME NEEDED: 54.79 Rating : 0.00 max weight: 68 178 -Unsatisfiable/GRP120-1.ma ... OK TIME NEEDED: 41.58 Rating : 0.00 max weight: 68 179 -Unsatisfiable/GRP121-1.ma ... OK TIME NEEDED: 37.22 Rating : 0.00 max weight: 68 180 -Unsatisfiable/GRP122-1.ma ... OK TIME NEEDED: 38.77 Rating : 0.07 max weight: 69 181 -Unsatisfiable/GRP136-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 max weight: 4 182 -Unsatisfiable/GRP137-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 max weight: 4 183 -Unsatisfiable/GRP138-1.ma ... OK TIME NEEDED: 4.32 Rating : 0.00 max weight: 7 184 -Unsatisfiable/GRP139-1.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 max weight: 16 185 -Unsatisfiable/GRP140-1.ma ... OK TIME NEEDED: 3.11 Rating : 0.00 max weight: 7 186 -Unsatisfiable/GRP141-1.ma ... OK TIME NEEDED: 0.21 Rating : 0.00 max weight: 16 187 -Unsatisfiable/GRP142-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 max weight: 0 188 -Unsatisfiable/GRP143-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 6 189 -Unsatisfiable/GRP144-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 max weight: 6 190 -Unsatisfiable/GRP145-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 16 191 -Unsatisfiable/GRP146-1.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 max weight: 16 192 -Unsatisfiable/GRP147-1.ma ... OK TIME NEEDED: 4.68 Rating : 0.00 max weight: 7 193 -Unsatisfiable/GRP148-1.ma ... OK TIME NEEDED: 3.40 Rating : 0.00 max weight: 7 194 -Unsatisfiable/GRP149-1.ma ... OK TIME NEEDED: 0.24 Rating : 0.00 max weight: 16 195 -Unsatisfiable/GRP150-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 max weight: 6 196 -Unsatisfiable/GRP151-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 0 197 -Unsatisfiable/GRP152-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 max weight: 16 198 -Unsatisfiable/GRP153-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 6 199 -Unsatisfiable/GRP154-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 max weight: 3 200 -Unsatisfiable/GRP155-1.ma ... OK TIME NEEDED: 0.08 Rating : 0.00 max weight: 3 201 -Unsatisfiable/GRP156-1.ma ... OK TIME NEEDED: 0.13 Rating : 0.00 max weight: 4 202 -Unsatisfiable/GRP157-1.ma ... OK TIME NEEDED: 0.08 Rating : 0.00 max weight: 3 203 -Unsatisfiable/GRP158-1.ma ... OK TIME NEEDED: 0.13 Rating : 0.00 max weight: 3 204 -Unsatisfiable/GRP159-1.ma ... OK TIME NEEDED: 0.28 Rating : 0.00 max weight: 7 205 -Unsatisfiable/GRP160-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 0 206 -Unsatisfiable/GRP161-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 max weight: 0 207 -Unsatisfiable/GRP162-1.ma ... OK TIME NEEDED: 0.29 Rating : 0.00 max weight: 7 208 -Unsatisfiable/GRP163-1.ma ... OK TIME NEEDED: 0.43 Rating : 0.00 max weight: 7 209 -Unsatisfiable/GRP164-1.ma ... FAIL Rating : 0.93 210 -Unsatisfiable/GRP164-2.ma ... FAIL Rating : 0.93 211 -Unsatisfiable/GRP165-1.ma ... OK TIME NEEDED: 54.54 Rating : 0.00 max weight: 14 212 -Unsatisfiable/GRP165-2.ma ... OK TIME NEEDED: 51.75 Rating : 0.00 max weight: 15 213 -Unsatisfiable/GRP166-1.ma ... OK TIME NEEDED: 261.59 Rating : 0.00 max weight: 21 214 -Unsatisfiable/GRP166-2.ma ... FAIL Rating : 0.00 215 -Unsatisfiable/GRP166-3.ma ... OK TIME NEEDED: 62.82 Rating : 0.00 max weight: 14 216 -Unsatisfiable/GRP166-4.ma ... OK TIME NEEDED: 52.29 Rating : 0.00 max weight: 15 217 -Unsatisfiable/GRP167-1.ma ... OK TIME NEEDED: 124.19 Rating : 0.21 max weight: 18 218 -Unsatisfiable/GRP167-2.ma ... OK TIME NEEDED: 300.19 Rating : 0.21 max weight: 18 219 -Unsatisfiable/GRP167-3.ma ... OK TIME NEEDED: 311.96 Rating : 0.50 max weight: 14 220 -Unsatisfiable/GRP167-4.ma ... OK TIME NEEDED: 250.37 Rating : 0.43 max weight: 16 221 -Unsatisfiable/GRP167-5.ma ... OK TIME NEEDED: 19.53 Rating : 0.14 max weight: 15 222 -Unsatisfiable/GRP168-1.ma ... OK TIME NEEDED: 0.09 Rating : 0.07 max weight: 3 223 -Unsatisfiable/GRP168-2.ma ... OK TIME NEEDED: 0.09 Rating : 0.07 max weight: 3 224 -Unsatisfiable/GRP169-1.ma ... OK TIME NEEDED: 107.13 Rating : 0.00 max weight: 12 225 -Unsatisfiable/GRP169-2.ma ... OK TIME NEEDED: 114.44 Rating : 0.00 max weight: 13 226 -Unsatisfiable/GRP170-1.ma ... OK TIME NEEDED: 307.40 Rating : 0.00 max weight: 14 227 -Unsatisfiable/GRP170-2.ma ... OK TIME NEEDED: 318.68 Rating : 0.00 max weight: 14 228 -Unsatisfiable/GRP170-3.ma ... OK TIME NEEDED: 339.79 Rating : 0.00 max weight: 14 229 -Unsatisfiable/GRP170-4.ma ... OK TIME NEEDED: 325.63 Rating : 0.00 max weight: 14 230 -Unsatisfiable/GRP171-1.ma ... OK TIME NEEDED: 6.36 Rating : 0.00 max weight: 10 231 -Unsatisfiable/GRP171-2.ma ... OK TIME NEEDED: 6.96 Rating : 0.00 max weight: 10 232 -Unsatisfiable/GRP172-1.ma ... OK TIME NEEDED: 10.72 Rating : 0.00 max weight: 10 233 -Unsatisfiable/GRP172-2.ma ... OK TIME NEEDED: 6.19 Rating : 0.00 max weight: 10 234 -Unsatisfiable/GRP173-1.ma ... OK TIME NEEDED: 15.46 Rating : 0.00 max weight: 11 235 -Unsatisfiable/GRP174-1.ma ... OK TIME NEEDED: 21.49 Rating : 0.00 max weight: 11 236 -Unsatisfiable/GRP175-1.ma ... OK TIME NEEDED: 33.68 Rating : 0.00 max weight: 13 237 -Unsatisfiable/GRP175-2.ma ... OK TIME NEEDED: 41.46 Rating : 0.00 max weight: 14 238 -Unsatisfiable/GRP175-3.ma ... OK TIME NEEDED: 41.14 Rating : 0.00 max weight: 14 239 -Unsatisfiable/GRP175-4.ma ... OK TIME NEEDED: 41.87 Rating : 0.00 max weight: 13 240 -Unsatisfiable/GRP176-1.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 max weight: 0 241 -Unsatisfiable/GRP176-2.ma ... OK TIME NEEDED: 0.08 Rating : 0.00 max weight: 0 242 -Unsatisfiable/GRP177-2.ma ... FAIL Rating : 0.21 243 -Unsatisfiable/GRP178-1.ma ... OK TIME NEEDED: 282.09 Rating : 0.14 max weight: 15 244 -Unsatisfiable/GRP178-2.ma ... OK TIME NEEDED: 297.82 Rating : 0.14 max weight: 15 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: 547.55 Rating : 0.43 max weight: 19 253 -Unsatisfiable/GRP181-4.ma ... FAIL Rating : 0.43 254 -Unsatisfiable/GRP182-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 6 255 -Unsatisfiable/GRP182-2.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 6 256 -Unsatisfiable/GRP182-3.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 max weight: 6 257 -Unsatisfiable/GRP182-4.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 6 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 ... OK TIME NEEDED: 39.14 Rating : 0.00 max weight: 16 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.21 Rating : 0.00 max weight: 9 273 -Unsatisfiable/GRP186-4.ma ... OK TIME NEEDED: 0.13 Rating : 0.00 max weight: 7 274 -Unsatisfiable/GRP187-1.ma ... FAIL Rating : 0.64 275 -Unsatisfiable/GRP188-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 max weight: 16 276 -Unsatisfiable/GRP188-2.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 16 277 -Unsatisfiable/GRP189-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 6 278 -Unsatisfiable/GRP189-2.ma ... OK TIME NEEDED: 0.07 Rating : 0.00 max weight: 6 279 -Unsatisfiable/GRP190-1.ma ... OK TIME NEEDED: 88.61 Rating : 0.00 max weight: 15 280 -Unsatisfiable/GRP190-2.ma ... OK TIME NEEDED: 81.56 Rating : 0.00 max weight: 12 281 -Unsatisfiable/GRP191-1.ma ... OK TIME NEEDED: 106.88 Rating : 0.00 max weight: 12 282 -Unsatisfiable/GRP191-2.ma ... OK TIME NEEDED: 89.87 Rating : 0.00 max weight: 11 283 -Unsatisfiable/GRP192-1.ma ... OK TIME NEEDED: 0.69 Rating : 0.07 max weight: 15 284 -Unsatisfiable/GRP193-1.ma ... OK TIME NEEDED: 70.37 Rating : 0.00 max weight: 16 285 -Unsatisfiable/GRP193-2.ma ... OK TIME NEEDED: 50.43 Rating : 0.00 max weight: 15 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.18 Rating : 0.00 max weight: 12 294 -Unsatisfiable/GRP403-1.ma ... OK TIME NEEDED: 8.97 Rating : 0.07 max weight: 38 295 -Unsatisfiable/GRP404-1.ma ... OK TIME NEEDED: 51.68 Rating : 0.21 max weight: 48 296 -Unsatisfiable/GRP405-1.ma ... OK TIME NEEDED: 33.55 Rating : 0.21 max weight: 39 297 -Unsatisfiable/GRP406-1.ma ... OK TIME NEEDED: 128.40 Rating : 0.00 max weight: 67 298 -Unsatisfiable/GRP407-1.ma ... OK TIME NEEDED: 240.49 Rating : 0.00 max weight: 67 299 -Unsatisfiable/GRP408-1.ma ... OK TIME NEEDED: 243.34 Rating : 0.00 max weight: 68 300 -Unsatisfiable/GRP409-1.ma ... OK TIME NEEDED: 10.16 Rating : 0.00 max weight: 50 301 -Unsatisfiable/GRP410-1.ma ... OK TIME NEEDED: 22.28 Rating : 0.21 max weight: 50 302 -Unsatisfiable/GRP411-1.ma ... OK TIME NEEDED: 19.42 Rating : 0.21 max weight: 51 303 -Unsatisfiable/GRP412-1.ma ... OK TIME NEEDED: 19.16 Rating : 0.00 max weight: 44 304 -Unsatisfiable/GRP413-1.ma ... OK TIME NEEDED: 100.00 Rating : 0.07 max weight: 44 305 -Unsatisfiable/GRP414-1.ma ... OK TIME NEEDED: 62.50 Rating : 0.07 max weight: 45 306 -Unsatisfiable/GRP415-1.ma ... OK TIME NEEDED: 342.07 Rating : 0.00 max weight: 68 307 -Unsatisfiable/GRP416-1.ma ... OK TIME NEEDED: 400.72 Rating : 0.07 max weight: 68 308 -Unsatisfiable/GRP417-1.ma ... OK TIME NEEDED: 388.08 Rating : 0.14 max weight: 69 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 ... OK TIME NEEDED: 3.56 Rating : 0.14 max weight: 71 313 -Unsatisfiable/GRP422-1.ma ... OK TIME NEEDED: 150.83 Rating : 0.29 max weight: 71 314 -Unsatisfiable/GRP423-1.ma ... OK TIME NEEDED: 76.62 Rating : 0.36 max weight: 72 315 -Unsatisfiable/GRP424-1.ma ... OK TIME NEEDED: 11.61 Rating : 0.00 max weight: 63 316 -Unsatisfiable/GRP425-1.ma ... OK TIME NEEDED: 11.20 Rating : 0.07 max weight: 63 317 -Unsatisfiable/GRP426-1.ma ... OK TIME NEEDED: 20.01 Rating : 0.14 max weight: 64 318 -Unsatisfiable/GRP427-1.ma ... OK TIME NEEDED: 31.94 Rating : 0.00 max weight: 38 319 -Unsatisfiable/GRP428-1.ma ... OK TIME NEEDED: 36.60 Rating : 0.00 max weight: 38 320 -Unsatisfiable/GRP429-1.ma ... OK TIME NEEDED: 50.34 Rating : 0.14 max weight: 39 321 -Unsatisfiable/GRP430-1.ma ... OK TIME NEEDED: 17.74 Rating : 0.00 max weight: 42 322 -Unsatisfiable/GRP431-1.ma ... OK TIME NEEDED: 16.07 Rating : 0.00 max weight: 42 323 -Unsatisfiable/GRP432-1.ma ... OK TIME NEEDED: 15.53 Rating : 0.00 max weight: 43 324 -Unsatisfiable/GRP433-1.ma ... OK TIME NEEDED: 4.91 Rating : 0.00 max weight: 22 325 -Unsatisfiable/GRP434-1.ma ... OK TIME NEEDED: 5.55 Rating : 0.00 max weight: 22 326 -Unsatisfiable/GRP435-1.ma ... OK TIME NEEDED: 8.83 Rating : 0.00 max weight: 24 327 -Unsatisfiable/GRP436-1.ma ... OK TIME NEEDED: 36.79 Rating : 0.07 max weight: 55 328 -Unsatisfiable/GRP437-1.ma ... OK TIME NEEDED: 35.27 Rating : 0.07 max weight: 55 329 -Unsatisfiable/GRP438-1.ma ... OK TIME NEEDED: 38.97 Rating : 0.07 max weight: 56 330 -Unsatisfiable/GRP439-1.ma ... OK TIME NEEDED: 13.91 Rating : 0.07 max weight: 48 331 -Unsatisfiable/GRP440-1.ma ... OK TIME NEEDED: 28.28 Rating : 0.14 max weight: 48 332 -Unsatisfiable/GRP441-1.ma ... OK TIME NEEDED: 36.20 Rating : 0.21 max weight: 49 333 -Unsatisfiable/GRP442-1.ma ... OK TIME NEEDED: 163.86 Rating : 0.14 max weight: 38 334 -Unsatisfiable/GRP443-1.ma ... OK TIME NEEDED: 169.09 Rating : 0.07 max weight: 38 335 -Unsatisfiable/GRP444-1.ma ... OK TIME NEEDED: 139.87 Rating : 0.21 max weight: 39 336 -Unsatisfiable/GRP445-1.ma ... OK TIME NEEDED: 0.48 Rating : 0.00 max weight: 15 337 -Unsatisfiable/GRP446-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 max weight: 15 338 -Unsatisfiable/GRP447-1.ma ... OK TIME NEEDED: 1.11 Rating : 0.14 max weight: 16 339 -Unsatisfiable/GRP448-1.ma ... OK TIME NEEDED: 0.33 Rating : 0.00 max weight: 15 340 -Unsatisfiable/GRP449-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 max weight: 15 341 -Unsatisfiable/GRP450-1.ma ... OK TIME NEEDED: 1.05 Rating : 0.07 max weight: 16 342 -Unsatisfiable/GRP451-1.ma ... OK TIME NEEDED: 0.15 Rating : 0.00 max weight: 14 343 -Unsatisfiable/GRP452-1.ma ... OK TIME NEEDED: 1.64 Rating : 0.14 max weight: 21 344 -Unsatisfiable/GRP453-1.ma ... OK TIME NEEDED: 2.88 Rating : 0.21 max weight: 26 345 -Unsatisfiable/GRP454-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 7 346 -Unsatisfiable/GRP455-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 15 347 -Unsatisfiable/GRP456-1.ma ... OK TIME NEEDED: 0.24 Rating : 0.07 max weight: 17 348 -Unsatisfiable/GRP457-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 7 349 -Unsatisfiable/GRP458-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 15 350 -Unsatisfiable/GRP459-1.ma ... OK TIME NEEDED: 0.25 Rating : 0.00 max weight: 17 351 -Unsatisfiable/GRP460-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 7 352 -Unsatisfiable/GRP461-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 max weight: 15 353 -Unsatisfiable/GRP462-1.ma ... OK TIME NEEDED: 0.31 Rating : 0.00 max weight: 16 354 -Unsatisfiable/GRP463-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 7 355 -Unsatisfiable/GRP464-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 max weight: 15 356 -Unsatisfiable/GRP465-1.ma ... OK TIME NEEDED: 0.40 Rating : 0.00 max weight: 16 357 -Unsatisfiable/GRP466-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 max weight: 19 358 -Unsatisfiable/GRP467-1.ma ... OK TIME NEEDED: 0.67 Rating : 0.00 max weight: 19 359 -Unsatisfiable/GRP468-1.ma ... OK TIME NEEDED: 1.07 Rating : 0.00 max weight: 19 360 -Unsatisfiable/GRP469-1.ma ... OK TIME NEEDED: 116.49 Rating : 0.21 max weight: 43 361 -Unsatisfiable/GRP470-1.ma ... OK TIME NEEDED: 123.50 Rating : 0.21 max weight: 43 362 -Unsatisfiable/GRP471-1.ma ... OK TIME NEEDED: 48.37 Rating : 0.21 max weight: 38 363 -Unsatisfiable/GRP472-1.ma ... OK TIME NEEDED: 41.32 Rating : 0.07 max weight: 47 364 -Unsatisfiable/GRP473-1.ma ... OK TIME NEEDED: 37.76 Rating : 0.07 max weight: 47 365 -Unsatisfiable/GRP474-1.ma ... OK TIME NEEDED: 53.59 Rating : 0.07 max weight: 48 366 -Unsatisfiable/GRP475-1.ma ... OK TIME NEEDED: 51.86 Rating : 0.21 max weight: 37 367 -Unsatisfiable/GRP476-1.ma ... OK TIME NEEDED: 37.80 Rating : 0.21 max weight: 37 368 -Unsatisfiable/GRP477-1.ma ... OK TIME NEEDED: 41.41 Rating : 0.21 max weight: 38 369 -Unsatisfiable/GRP478-1.ma ... OK TIME NEEDED: 18.96 Rating : 0.14 max weight: 32 370 -Unsatisfiable/GRP479-1.ma ... OK TIME NEEDED: 19.22 Rating : 0.14 max weight: 32 371 -Unsatisfiable/GRP480-1.ma ... OK TIME NEEDED: 21.92 Rating : 0.21 max weight: 33 372 -Unsatisfiable/GRP481-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 max weight: 20 373 -Unsatisfiable/GRP482-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 21 374 -Unsatisfiable/GRP483-1.ma ... OK TIME NEEDED: 1.16 Rating : 0.00 max weight: 22 375 -Unsatisfiable/GRP484-1.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 max weight: 16 376 -Unsatisfiable/GRP485-1.ma ... OK TIME NEEDED: 0.23 Rating : 0.00 max weight: 17 377 -Unsatisfiable/GRP486-1.ma ... OK TIME NEEDED: 1.23 Rating : 0.00 max weight: 18 378 -Unsatisfiable/GRP487-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 max weight: 15 379 -Unsatisfiable/GRP488-1.ma ... OK TIME NEEDED: 1.17 Rating : 0.00 max weight: 15 380 -Unsatisfiable/GRP489-1.ma ... OK TIME NEEDED: 2.53 Rating : 0.00 max weight: 26 381 -Unsatisfiable/GRP490-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 15 382 -Unsatisfiable/GRP491-1.ma ... OK TIME NEEDED: 0.08 Rating : 0.00 max weight: 16 383 -Unsatisfiable/GRP492-1.ma ... OK TIME NEEDED: 0.36 Rating : 0.00 max weight: 17 384 -Unsatisfiable/GRP493-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 max weight: 16 385 -Unsatisfiable/GRP494-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 17 386 -Unsatisfiable/GRP495-1.ma ... OK TIME NEEDED: 0.27 Rating : 0.00 max weight: 18 387 -Unsatisfiable/GRP496-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 16 388 -Unsatisfiable/GRP497-1.ma ... OK TIME NEEDED: 0.19 Rating : 0.00 max weight: 17 389 -Unsatisfiable/GRP498-1.ma ... OK TIME NEEDED: 0.46 Rating : 0.00 max weight: 18 390 -Unsatisfiable/GRP499-1.ma ... OK TIME NEEDED: 7.75 Rating : 0.00 max weight: 38 391 -Unsatisfiable/GRP500-1.ma ... OK TIME NEEDED: 4.26 Rating : 0.07 max weight: 38 392 -Unsatisfiable/GRP501-1.ma ... OK TIME NEEDED: 87.52 Rating : 0.14 max weight: 39 393 -Unsatisfiable/GRP502-1.ma ... OK TIME NEEDED: 161.64 Rating : 0.14 max weight: 42 394 -Unsatisfiable/GRP503-1.ma ... OK TIME NEEDED: 248.32 Rating : 0.14 max weight: 42 395 -Unsatisfiable/GRP504-1.ma ... OK TIME NEEDED: 247.37 Rating : 0.14 max weight: 43 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: 143.03 Rating : 0.00 max weight: 21 401 -Unsatisfiable/GRP510-1.ma ... OK TIME NEEDED: 0.78 Rating : 0.00 max weight: 21 402 -Unsatisfiable/GRP511-1.ma ... OK TIME NEEDED: 8.71 Rating : 0.00 max weight: 22 403 -Unsatisfiable/GRP512-1.ma ... OK TIME NEEDED: 0.17 Rating : 0.00 max weight: 22 404 -Unsatisfiable/GRP513-1.ma ... OK TIME NEEDED: 57.79 Rating : 0.00 max weight: 16 405 -Unsatisfiable/GRP514-1.ma ... OK TIME NEEDED: 0.17 Rating : 0.00 max weight: 16 406 -Unsatisfiable/GRP515-1.ma ... OK TIME NEEDED: 0.31 Rating : 0.00 max weight: 17 407 -Unsatisfiable/GRP516-1.ma ... OK TIME NEEDED: 0.17 Rating : 0.00 max weight: 17 408 -Unsatisfiable/GRP517-1.ma ... OK TIME NEEDED: 1.38 Rating : 0.00 max weight: 16 409 -Unsatisfiable/GRP518-1.ma ... OK TIME NEEDED: 0.13 Rating : 0.00 max weight: 16 410 -Unsatisfiable/GRP519-1.ma ... OK TIME NEEDED: 0.46 Rating : 0.00 max weight: 17 411 -Unsatisfiable/GRP520-1.ma ... OK TIME NEEDED: 0.18 Rating : 0.00 max weight: 17 412 -Unsatisfiable/GRP521-1.ma ... OK TIME NEEDED: 0.12 Rating : 0.00 max weight: 11 413 -Unsatisfiable/GRP522-1.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 max weight: 12 414 -Unsatisfiable/GRP523-1.ma ... OK TIME NEEDED: 2.70 Rating : 0.00 max weight: 16 415 -Unsatisfiable/GRP524-1.ma ... OK TIME NEEDED: 0.19 Rating : 0.00 max weight: 13 416 -Unsatisfiable/GRP525-1.ma ... OK TIME NEEDED: 0.14 Rating : 0.00 max weight: 10 417 -Unsatisfiable/GRP526-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 max weight: 10 418 -Unsatisfiable/GRP527-1.ma ... OK TIME NEEDED: 9.44 Rating : 0.00 max weight: 16 419 -Unsatisfiable/GRP528-1.ma ... OK TIME NEEDED: 0.19 Rating : 0.00 max weight: 16 420 -Unsatisfiable/GRP529-1.ma ... OK TIME NEEDED: 0.15 Rating : 0.00 max weight: 11 421 -Unsatisfiable/GRP530-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 8 422 -Unsatisfiable/GRP531-1.ma ... OK TIME NEEDED: 2.91 Rating : 0.00 max weight: 16 423 -Unsatisfiable/GRP532-1.ma ... OK TIME NEEDED: 0.15 Rating : 0.00 max weight: 11 424 -Unsatisfiable/GRP533-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 7 425 -Unsatisfiable/GRP534-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 max weight: 11 426 -Unsatisfiable/GRP535-1.ma ... OK TIME NEEDED: 2.82 Rating : 0.00 max weight: 16 427 -Unsatisfiable/GRP536-1.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 max weight: 15 428 -Unsatisfiable/GRP537-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 7 429 -Unsatisfiable/GRP538-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 max weight: 11 430 -Unsatisfiable/GRP539-1.ma ... OK TIME NEEDED: 2.45 Rating : 0.00 max weight: 17 431 -Unsatisfiable/GRP540-1.ma ... OK TIME NEEDED: 0.13 Rating : 0.00 max weight: 11 432 -Unsatisfiable/GRP541-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 7 433 -Unsatisfiable/GRP542-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 max weight: 12 434 -Unsatisfiable/GRP543-1.ma ... OK TIME NEEDED: 0.67 Rating : 0.00 max weight: 16 435 -Unsatisfiable/GRP544-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 13 436 -Unsatisfiable/GRP545-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 7 437 -Unsatisfiable/GRP546-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 12 438 -Unsatisfiable/GRP547-1.ma ... OK TIME NEEDED: 1.70 Rating : 0.00 max weight: 17 439 -Unsatisfiable/GRP548-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 13 440 -Unsatisfiable/GRP549-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 7 441 -Unsatisfiable/GRP550-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.07 max weight: 12 442 -Unsatisfiable/GRP551-1.ma ... OK TIME NEEDED: 0.75 Rating : 0.00 max weight: 16 443 -Unsatisfiable/GRP552-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 max weight: 13 444 -Unsatisfiable/GRP553-1.ma ... OK TIME NEEDED: 0.13 Rating : 0.00 max weight: 15 445 -Unsatisfiable/GRP554-1.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 max weight: 16 446 -Unsatisfiable/GRP555-1.ma ... OK TIME NEEDED: 1.03 Rating : 0.00 max weight: 19 447 -Unsatisfiable/GRP556-1.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 max weight: 15 448 -Unsatisfiable/GRP557-1.ma ... OK TIME NEEDED: 0.16 Rating : 0.00 max weight: 15 449 -Unsatisfiable/GRP558-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 max weight: 15 450 -Unsatisfiable/GRP559-1.ma ... OK TIME NEEDED: 3.08 Rating : 0.00 max weight: 16 451 -Unsatisfiable/GRP560-1.ma ... OK TIME NEEDED: 0.25 Rating : 0.00 max weight: 15 452 -Unsatisfiable/GRP561-1.ma ... OK TIME NEEDED: 0.14 Rating : 0.00 max weight: 17 453 -Unsatisfiable/GRP562-1.ma ... OK TIME NEEDED: 0.07 Rating : 0.00 max weight: 16 454 -Unsatisfiable/GRP563-1.ma ... OK TIME NEEDED: 6.03 Rating : 0.00 max weight: 17 455 -Unsatisfiable/GRP564-1.ma ... OK TIME NEEDED: 0.16 Rating : 0.00 max weight: 17 456 -Unsatisfiable/GRP565-1.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 max weight: 16 457 -Unsatisfiable/GRP566-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 17 458 -Unsatisfiable/GRP567-1.ma ... OK TIME NEEDED: 28.20 Rating : 0.14 max weight: 27 459 -Unsatisfiable/GRP568-1.ma ... OK TIME NEEDED: 0.36 Rating : 0.14 max weight: 27 460 -Unsatisfiable/GRP569-1.ma ... OK TIME NEEDED: 0.07 Rating : 0.00 max weight: 16 461 -Unsatisfiable/GRP570-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 17 462 -Unsatisfiable/GRP571-1.ma ... OK TIME NEEDED: 26.98 Rating : 0.14 max weight: 25 463 -Unsatisfiable/GRP572-1.ma ... OK TIME NEEDED: 0.24 Rating : 0.07 max weight: 18 464 -Unsatisfiable/GRP573-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 16 465 -Unsatisfiable/GRP574-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 max weight: 19 466 -Unsatisfiable/GRP575-1.ma ... OK TIME NEEDED: 46.52 Rating : 0.14 max weight: 25 467 -Unsatisfiable/GRP576-1.ma ... OK TIME NEEDED: 0.35 Rating : 0.00 max weight: 25 468 -Unsatisfiable/GRP577-1.ma ... OK TIME NEEDED: 0.21 Rating : 0.00 max weight: 16 469 -Unsatisfiable/GRP578-1.ma ... OK TIME NEEDED: 0.43 Rating : 0.00 max weight: 17 470 -Unsatisfiable/GRP579-1.ma ... OK TIME NEEDED: 1.66 Rating : 0.07 max weight: 25 471 -Unsatisfiable/GRP580-1.ma ... OK TIME NEEDED: 0.46 Rating : 0.00 max weight: 25 472 -Unsatisfiable/GRP581-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 max weight: 16 473 -Unsatisfiable/GRP582-1.ma ... OK TIME NEEDED: 0.30 Rating : 0.00 max weight: 17 474 -Unsatisfiable/GRP583-1.ma ... OK TIME NEEDED: 2.94 Rating : 0.07 max weight: 19 475 -Unsatisfiable/GRP584-1.ma ... OK TIME NEEDED: 0.23 Rating : 0.00 max weight: 18 476 -Unsatisfiable/GRP585-1.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 max weight: 19 477 -Unsatisfiable/GRP586-1.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 max weight: 19 478 -Unsatisfiable/GRP587-1.ma ... FAIL Rating : 0.00 479 -Unsatisfiable/GRP588-1.ma ... OK TIME NEEDED: 1.47 Rating : 0.00 max weight: 20 480 -Unsatisfiable/GRP589-1.ma ... OK TIME NEEDED: 0.50 Rating : 0.00 max weight: 19 481 -Unsatisfiable/GRP590-1.ma ... OK TIME NEEDED: 0.12 Rating : 0.00 max weight: 19 482 -Unsatisfiable/GRP591-1.ma ... OK TIME NEEDED: 0.64 Rating : 0.07 max weight: 20 483 -Unsatisfiable/GRP592-1.ma ... OK TIME NEEDED: 0.28 Rating : 0.07 max weight: 20 484 -Unsatisfiable/GRP593-1.ma ... OK TIME NEEDED: 2.56 Rating : 0.00 max weight: 16 485 -Unsatisfiable/GRP594-1.ma ... OK TIME NEEDED: 1.16 Rating : 0.00 max weight: 16 486 -Unsatisfiable/GRP595-1.ma ... OK TIME NEEDED: 0.24 Rating : 0.07 max weight: 16 487 -Unsatisfiable/GRP596-1.ma ... OK TIME NEEDED: 0.29 Rating : 0.07 max weight: 16 488 -Unsatisfiable/GRP597-1.ma ... OK TIME NEEDED: 0.62 Rating : 0.00 max weight: 20 489 -Unsatisfiable/GRP598-1.ma ... OK TIME NEEDED: 0.28 Rating : 0.07 max weight: 20 490 -Unsatisfiable/GRP599-1.ma ... OK TIME NEEDED: 2.33 Rating : 0.07 max weight: 21 491 -Unsatisfiable/GRP600-1.ma ... OK TIME NEEDED: 0.36 Rating : 0.07 max weight: 21 492 -Unsatisfiable/GRP601-1.ma ... OK TIME NEEDED: 3.56 Rating : 0.07 max weight: 15 493 -Unsatisfiable/GRP602-1.ma ... OK TIME NEEDED: 0.44 Rating : 0.07 max weight: 16 494 -Unsatisfiable/GRP603-1.ma ... OK TIME NEEDED: 0.56 Rating : 0.07 max weight: 16 495 -Unsatisfiable/GRP604-1.ma ... OK TIME NEEDED: 0.77 Rating : 0.07 max weight: 15 496 -Unsatisfiable/GRP605-1.ma ... OK TIME NEEDED: 1.75 Rating : 0.00 max weight: 19 497 -Unsatisfiable/GRP606-1.ma ... OK TIME NEEDED: 1.62 Rating : 0.00 max weight: 19 498 -Unsatisfiable/GRP607-1.ma ... FAIL Rating : 0.00 499 -Unsatisfiable/GRP608-1.ma ... OK TIME NEEDED: 2.11 Rating : 0.00 max weight: 22 500 -Unsatisfiable/GRP609-1.ma ... OK TIME NEEDED: 2.03 Rating : 0.07 max weight: 15 501 -Unsatisfiable/GRP610-1.ma ... OK TIME NEEDED: 0.50 Rating : 0.07 max weight: 15 502 -Unsatisfiable/GRP611-1.ma ... OK TIME NEEDED: 0.24 Rating : 0.00 max weight: 16 503 -Unsatisfiable/GRP612-1.ma ... OK TIME NEEDED: 0.32 Rating : 0.07 max weight: 16 504 -Unsatisfiable/GRP613-1.ma ... OK TIME NEEDED: 0.78 Rating : 0.00 max weight: 20 505 -Unsatisfiable/GRP614-1.ma ... OK TIME NEEDED: 0.30 Rating : 0.00 max weight: 20 506 -Unsatisfiable/GRP615-1.ma ... OK TIME NEEDED: 1.73 Rating : 0.07 max weight: 21 507 -Unsatisfiable/GRP616-1.ma ... OK TIME NEEDED: 0.32 Rating : 0.00 max weight: 21 508 -Unsatisfiable/LAT006-1.ma ... OK TIME NEEDED: 38.21 Rating : 0.14 max weight: 20 509 -Unsatisfiable/LAT007-1.ma ... OK TIME NEEDED: 97.83 Rating : 0.36 max weight: 19 510 -Unsatisfiable/LAT008-1.ma ... OK TIME NEEDED: 0.82 Rating : 0.07 max weight: 12 511 -Unsatisfiable/LAT009-1.ma ... OK TIME NEEDED: 341.28 Rating : 0.00 max weight: 23 512 -Unsatisfiable/LAT010-1.ma ... FAIL Rating : 0.00 513 -Unsatisfiable/LAT011-1.ma ... FAIL Rating : 0.07 514 -Unsatisfiable/LAT012-1.ma ... OK TIME NEEDED: 4.82 Rating : 0.00 max weight: 14 515 -Unsatisfiable/LAT013-1.ma ... OK TIME NEEDED: 90.79 Rating : 0.14 max weight: 18 516 -Unsatisfiable/LAT014-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 6 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: 20.28 Rating : 0.14 max weight: 16 525 -Unsatisfiable/LAT027-1.ma ... OK TIME NEEDED: 13.64 Rating : 0.07 max weight: 16 526 -Unsatisfiable/LAT028-1.ma ... OK TIME NEEDED: 17.73 Rating : 0.00 max weight: 12 527 -Unsatisfiable/LAT031-1.ma ... OK TIME NEEDED: 0.99 Rating : 0.00 max weight: 9 528 -Unsatisfiable/LAT032-1.ma ... OK TIME NEEDED: 27.63 Rating : 0.00 max weight: 9 529 -Unsatisfiable/LAT033-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 3 530 -Unsatisfiable/LAT034-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 3 531 -Unsatisfiable/LAT038-1.ma ... FAIL Rating : 0.43 532 -Unsatisfiable/LAT039-1.ma ... OK TIME NEEDED: 0.07 Rating : 0.00 max weight: 6 533 -Unsatisfiable/LAT039-2.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 0 534 -Unsatisfiable/LAT040-1.ma ... OK TIME NEEDED: 36.21 Rating : 0.00 max weight: 11 535 -Unsatisfiable/LAT042-1.ma ... OK TIME NEEDED: 1.93 Rating : 0.00 max weight: 9 536 -Unsatisfiable/LAT043-1.ma ... OK TIME NEEDED: 158.67 Rating : 0.00 max weight: 18 537 -Unsatisfiable/LAT044-1.ma ... FAIL Rating : 0.14 538 -Unsatisfiable/LAT045-1.ma ... OK TIME NEEDED: 0.17 Rating : 0.07 max weight: 18 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 ... OK TIME NEEDED: 84.86 Rating : 0.36 max weight: 1061 548 -Unsatisfiable/LAT081-1.ma ... FAIL Rating : 0.57 549 -Unsatisfiable/LAT082-1.ma ... FAIL Rating : 0.64 550 -Unsatisfiable/LAT083-1.ma ... OK TIME NEEDED: 89.00 Rating : 0.36 max weight: 1061 551 -Unsatisfiable/LAT084-1.ma ... FAIL Rating : 0.50 552 -Unsatisfiable/LAT085-1.ma ... FAIL Rating : 0.57 553 -Unsatisfiable/LAT086-1.ma ... OK TIME NEEDED: 573.47 Rating : 0.50 max weight: 1060 554 -Unsatisfiable/LAT087-1.ma ... OK TIME NEEDED: 588.84 Rating : 0.43 max weight: 1060 555 -Unsatisfiable/LAT088-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 16 556 -Unsatisfiable/LAT089-1.ma ... OK TIME NEEDED: 1.68 Rating : 0.00 max weight: 16 557 -Unsatisfiable/LAT090-1.ma ... OK TIME NEEDED: 0.14 Rating : 0.00 max weight: 16 558 -Unsatisfiable/LAT091-1.ma ... OK TIME NEEDED: 16.44 Rating : 0.07 max weight: 21 559 -Unsatisfiable/LAT092-1.ma ... OK TIME NEEDED: 82.68 Rating : 0.36 max weight: 991 560 -Unsatisfiable/LAT093-1.ma ... OK TIME NEEDED: 320.09 Rating : 0.43 max weight: 991 561 -Unsatisfiable/LAT094-1.ma ... OK TIME NEEDED: 97.53 Rating : 0.36 max weight: 991 562 -Unsatisfiable/LAT095-1.ma ... OK TIME NEEDED: 474.76 Rating : 0.43 max weight: 991 563 -Unsatisfiable/LAT096-1.ma ... OK TIME NEEDED: 162.98 Rating : 0.36 max weight: 990 564 -Unsatisfiable/LAT097-1.ma ... OK TIME NEEDED: 115.99 Rating : 0.36 max weight: 990 565 -Unsatisfiable/LAT138-1.ma ... FAIL Rating : 1.00 1 -Unsatisfiable/LAT139-1.ma ... FAIL Rating : 1.00 2 -Unsatisfiable/LAT140-1.ma ... FAIL Rating : 1.00 3 -Unsatisfiable/LAT141-1.ma ... FAIL Rating : 1.00 4 -Unsatisfiable/LAT142-1.ma ... FAIL Rating : 0.64 5 -Unsatisfiable/LAT143-1.ma ... FAIL Rating : 0.14 6 -Unsatisfiable/LAT144-1.ma ... FAIL Rating : 0.86 7 -Unsatisfiable/LAT145-1.ma ... FAIL Rating : 0.93 8 -Unsatisfiable/LAT146-1.ma ... FAIL Rating : 0.79 9 -Unsatisfiable/LAT147-1.ma ... FAIL Rating : 0.79 10 -Unsatisfiable/LAT148-1.ma ... FAIL Rating : 0.71 11 -Unsatisfiable/LAT149-1.ma ... FAIL Rating : 0.93 12 -Unsatisfiable/LAT150-1.ma ... FAIL Rating : 0.86 13 -Unsatisfiable/LAT151-1.ma ... FAIL Rating : 0.86 14 -Unsatisfiable/LAT152-1.ma ... FAIL Rating : 0.79 15 -Unsatisfiable/LAT153-1.ma ... FAIL Rating : 0.93 16 -Unsatisfiable/LAT154-1.ma ... FAIL Rating : 0.79 17 -Unsatisfiable/LAT155-1.ma ... FAIL Rating : 0.86 18 -Unsatisfiable/LAT156-1.ma ... FAIL Rating : 0.64 19 -Unsatisfiable/LAT157-1.ma ... FAIL Rating : 0.86 20 -Unsatisfiable/LAT158-1.ma ... FAIL Rating : 0.93 21 -Unsatisfiable/LAT159-1.ma ... FAIL Rating : 0.86 22 -Unsatisfiable/LAT160-1.ma ... FAIL Rating : 0.64 23 -Unsatisfiable/LAT161-1.ma ... FAIL Rating : 1.00 24 -Unsatisfiable/LAT162-1.ma ... FAIL Rating : 0.86 25 -Unsatisfiable/LAT163-1.ma ... FAIL Rating : 0.93 26 -Unsatisfiable/LAT164-1.ma ... FAIL Rating : 0.93 27 -Unsatisfiable/LAT165-1.ma ... FAIL Rating : 0.93 28 -Unsatisfiable/LAT166-1.ma ... FAIL Rating : 0.93 29 -Unsatisfiable/LAT167-1.ma ... FAIL Rating : 0.93 30 -Unsatisfiable/LAT168-1.ma ... OK TIME NEEDED: 190.30 Rating : 0.14 max weight: 16 31 -Unsatisfiable/LAT169-1.ma ... FAIL Rating : 0.86 32 -Unsatisfiable/LAT170-1.ma ... FAIL Rating : 0.79 33 -Unsatisfiable/LAT171-1.ma ... OK TIME NEEDED: 250.07 Rating : 0.50 max weight: 16 34 -Unsatisfiable/LAT172-1.ma ... FAIL Rating : 0.93 35 -Unsatisfiable/LAT173-1.ma ... FAIL Rating : 0.93 36 -Unsatisfiable/LAT174-1.ma ... FAIL Rating : 0.79 37 -Unsatisfiable/LAT175-1.ma ... FAIL Rating : 0.93 38 -Unsatisfiable/LAT176-1.ma ... FAIL Rating : 0.93 39 -Unsatisfiable/LAT177-1.ma ... FAIL Rating : 1.00 40 -Unsatisfiable/LCL109-2.ma ... FAIL Rating : 0.29 41 -Unsatisfiable/LCL109-6.ma ... FAIL Rating : 0.14 42 -Unsatisfiable/LCL110-2.ma ... OK TIME NEEDED: 1.67 Rating : 0.00 max weight: 12 43 -Unsatisfiable/LCL111-2.ma ... OK TIME NEEDED: 5.31 Rating : 0.07 max weight: 17 44 -Unsatisfiable/LCL112-2.ma ... OK TIME NEEDED: 1.81 Rating : 0.00 max weight: 14 45 -Unsatisfiable/LCL113-2.ma ... OK TIME NEEDED: 1.39 Rating : 0.00 max weight: 12 46 -Unsatisfiable/LCL114-2.ma ... OK TIME NEEDED: 1.90 Rating : 0.00 max weight: 12 47 -Unsatisfiable/LCL115-2.ma ... OK TIME NEEDED: 1.41 Rating : 0.00 max weight: 13 48 -Unsatisfiable/LCL116-2.ma ... OK TIME NEEDED: 5.72 Rating : 0.00 max weight: 13 49 -Unsatisfiable/LCL132-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 max weight: 9 50 -Unsatisfiable/LCL133-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 max weight: 11 51 -Unsatisfiable/LCL134-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 9 52 -Unsatisfiable/LCL135-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 9 53 -Unsatisfiable/LCL138-1.ma ... FAIL Rating : 0.21 54 -Unsatisfiable/LCL139-1.ma ... OK TIME NEEDED: 1.81 Rating : 0.00 max weight: 12 55 -Unsatisfiable/LCL140-1.ma ... OK TIME NEEDED: 1.45 Rating : 0.00 max weight: 14 56 -Unsatisfiable/LCL141-1.ma ... OK TIME NEEDED: 2.09 Rating : 0.00 max weight: 14 57 -Unsatisfiable/LCL153-1.ma ... OK TIME NEEDED: 1.36 Rating : 0.00 max weight: 10 58 -Unsatisfiable/LCL154-1.ma ... OK TIME NEEDED: 10.65 Rating : 0.00 max weight: 12 59 -Unsatisfiable/LCL155-1.ma ... OK TIME NEEDED: 0.14 Rating : 0.00 max weight: 12 60 -Unsatisfiable/LCL156-1.ma ... OK TIME NEEDED: 1.38 Rating : 0.00 max weight: 11 61 -Unsatisfiable/LCL157-1.ma ... OK TIME NEEDED: 1.13 Rating : 0.00 max weight: 12 62 -Unsatisfiable/LCL158-1.ma ... OK TIME NEEDED: 1.87 Rating : 0.00 max weight: 15 63 -Unsatisfiable/LCL159-1.ma ... OK TIME NEEDED: 131.67 Rating : 0.00 max weight: 16 64 -Unsatisfiable/LCL160-1.ma ... FAIL Rating : 0.14 65 -Unsatisfiable/LCL161-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 max weight: 9 66 -Unsatisfiable/LCL162-1.ma ... FAIL Rating : 0.00 67 -Unsatisfiable/LCL163-1.ma ... OK TIME NEEDED: 10.10 Rating : 0.14 max weight: 34 68 -Unsatisfiable/LCL164-1.ma ... OK TIME NEEDED: 0.15 Rating : 0.00 max weight: 12 69 -Unsatisfiable/LDA001-1.ma ... OK TIME NEEDED: 0.13 Rating : 0.00 max weight: 7 70 -Unsatisfiable/LDA002-1.ma ... OK TIME NEEDED: 22.30 Rating : 0.00 max weight: 11 71 -Unsatisfiable/LDA007-3.ma ... OK TIME NEEDED: 0.08 Rating : 0.00 max weight: 8 72 -Unsatisfiable/RNG007-4.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 7 73 -Unsatisfiable/RNG008-3.ma ... OK TIME NEEDED: 17.75 Rating : 0.07 max weight: 17 74 -Unsatisfiable/RNG008-4.ma ... OK TIME NEEDED: 18.52 Rating : 0.07 max weight: 17 75 -Unsatisfiable/RNG008-7.ma ... OK TIME NEEDED: 47.63 Rating : 0.07 max weight: 22 76 -Unsatisfiable/RNG009-5.ma ... FAIL Rating : 0.50 77 -Unsatisfiable/RNG009-7.ma ... FAIL Rating : 0.50 78 -Unsatisfiable/RNG011-5.ma ... OK TIME NEEDED: 0.14 Rating : 0.00 max weight: 0 79 -Unsatisfiable/RNG012-6.ma ... OK TIME NEEDED: 114.29 Rating : 0.00 max weight: 12 80 -Unsatisfiable/RNG013-6.ma ... OK TIME NEEDED: 132.92 Rating : 0.00 max weight: 12 81 -Unsatisfiable/RNG014-6.ma ... OK TIME NEEDED: 145.08 Rating : 0.00 max weight: 12 82 -Unsatisfiable/RNG015-6.ma ... OK TIME NEEDED: 127.35 Rating : 0.00 max weight: 11 83 -Unsatisfiable/RNG016-6.ma ... OK TIME NEEDED: 133.38 Rating : 0.00 max weight: 11 84 -Unsatisfiable/RNG017-6.ma ... OK TIME NEEDED: 120.96 Rating : 0.00 max weight: 11 85 -Unsatisfiable/RNG018-6.ma ... OK TIME NEEDED: 116.44 Rating : 0.00 max weight: 11 86 -Unsatisfiable/RNG019-6.ma ... FAIL Rating : 0.21 87 -Unsatisfiable/RNG019-7.ma ... FAIL Rating : 0.21 88 -Unsatisfiable/RNG020-6.ma ... FAIL Rating : 0.29 89 -Unsatisfiable/RNG020-7.ma ... FAIL Rating : 0.21 90 -Unsatisfiable/RNG021-6.ma ... FAIL Rating : 0.14 91 -Unsatisfiable/RNG021-7.ma ... FAIL Rating : 0.21 92 -Unsatisfiable/RNG023-6.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 max weight: 15 93 -Unsatisfiable/RNG023-7.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 max weight: 15 94 -Unsatisfiable/RNG024-6.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 max weight: 15 95 -Unsatisfiable/RNG024-7.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 max weight: 15 96 -Unsatisfiable/RNG025-4.ma ... FAIL Rating : 0.29 97 -Unsatisfiable/RNG025-5.ma ... FAIL Rating : 0.36 98 -Unsatisfiable/RNG025-6.ma ... FAIL Rating : 0.29 99 -Unsatisfiable/RNG025-7.ma ... FAIL Rating : 0.43 100 -Unsatisfiable/RNG026-6.ma ... FAIL Rating : 0.57 101 -Unsatisfiable/RNG026-7.ma ... FAIL Rating : 0.50 102 -Unsatisfiable/RNG027-5.ma ... FAIL Rating : 0.86 103 -Unsatisfiable/RNG027-7.ma ... FAIL Rating : 0.86 104 -Unsatisfiable/RNG027-8.ma ... FAIL Rating : 0.86 105 -Unsatisfiable/RNG027-9.ma ... FAIL Rating : 0.86 106 -Unsatisfiable/RNG028-5.ma ... FAIL Rating : 0.86 107 -Unsatisfiable/RNG028-7.ma ... FAIL Rating : 0.86 108 -Unsatisfiable/RNG028-8.ma ... FAIL Rating : 0.86 109 -Unsatisfiable/RNG028-9.ma ... FAIL Rating : 0.86 110 -Unsatisfiable/RNG029-5.ma ... FAIL Rating : 0.86 111 -Unsatisfiable/RNG029-6.ma ... FAIL Rating : 0.86 112 -Unsatisfiable/RNG029-7.ma ... FAIL Rating : 0.86 113 -Unsatisfiable/RNG035-7.ma ... FAIL Rating : 0.86 114 -Unsatisfiable/ROB001-1.ma ... FAIL Rating : 1.00 115 -Unsatisfiable/ROB002-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 max weight: 10 116 -Unsatisfiable/ROB003-1.ma ... OK TIME NEEDED: 0.72 Rating : 0.00 max weight: 17 117 -Unsatisfiable/ROB004-1.ma ... OK TIME NEEDED: 66.26 Rating : 0.00 max weight: 22 118 -Unsatisfiable/ROB005-1.ma ... FAIL Rating : 0.07 119 -Unsatisfiable/ROB006-1.ma ... FAIL Rating : 0.86 120 -Unsatisfiable/ROB006-2.ma ... FAIL Rating : 0.86 121 -Unsatisfiable/ROB008-1.ma ... OK TIME NEEDED: 80.62 Rating : 0.00 max weight: 17 122 -Unsatisfiable/ROB009-1.ma ... OK TIME NEEDED: 0.07 Rating : 0.00 max weight: 18 123 -Unsatisfiable/ROB010-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 max weight: 7 124 -Unsatisfiable/ROB013-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 max weight: 8 125 -Unsatisfiable/ROB022-1.ma ... FAIL Rating : 0.00 126 -Unsatisfiable/ROB023-1.ma ... FAIL Rating : 0.00 127 -Unsatisfiable/ROB026-1.ma ... FAIL Rating : 0.86 128 -Unsatisfiable/ROB030-1.ma ... OK TIME NEEDED: 0.44 Rating : 0.00 max weight: 5 129 -Unsatisfiable/ROB031-1.ma ... FAIL Rating : 1.00 130 -Unsatisfiable/ROB032-1.ma ... FAIL Rating : 1.00 131 -Unsatisfiable/SYN080-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 132 -Unsatisfiable/SYN083-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 133 diff --git a/matita/tests/TPTP/log.600.15-7.comedasvn_stampapesomassimoeqinprovanellog.txt b/matita/tests/TPTP/log.600.15-7.comedasvn_stampapesomassimoeqinprovanellog.txt new file mode 100644 index 000000000..d37bf6b12 --- /dev/null +++ b/matita/tests/TPTP/log.600.15-7.comedasvn_stampapesomassimoeqinprovanellog.txt @@ -0,0 +1,698 @@ +Unsatisfiable/ALG005-1.ma ... OK TIME NEEDED: 72.61 Rating : 0.07 max weight: 21 1 +Unsatisfiable/ALG006-1.ma ... OK TIME NEEDED: 7.07 Rating : 0.00 max weight: 18 2 +Unsatisfiable/ALG007-1.ma ... OK TIME NEEDED: 8.76 Rating : 0.00 max weight: 18 3 +Unsatisfiable/BOO001-1.ma ... OK TIME NEEDED: 0.54 Rating : 0.00 max weight: 21 4 +Unsatisfiable/BOO002-1.ma ... OK TIME NEEDED: 6.47 Rating : 0.07 max weight: 26 5 +Unsatisfiable/BOO002-2.ma ... OK TIME NEEDED: 9.59 Rating : 0.00 max weight: 26 6 +Unsatisfiable/BOO003-2.ma ... OK TIME NEEDED: 0.78 Rating : 0.00 max weight: 13 7 +Unsatisfiable/BOO003-4.ma ... OK TIME NEEDED: 0.48 Rating : 0.00 max weight: 15 8 +Unsatisfiable/BOO004-2.ma ... OK TIME NEEDED: 0.20 Rating : 0.00 max weight: 10 9 +Unsatisfiable/BOO004-4.ma ... OK TIME NEEDED: 0.16 Rating : 0.00 max weight: 10 10 +Unsatisfiable/BOO005-2.ma ... OK TIME NEEDED: 0.32 Rating : 0.00 max weight: 9 11 +Unsatisfiable/BOO005-4.ma ... OK TIME NEEDED: 0.19 Rating : 0.00 max weight: 9 12 +Unsatisfiable/BOO006-2.ma ... OK TIME NEEDED: 1.05 Rating : 0.00 max weight: 17 13 +Unsatisfiable/BOO006-4.ma ... OK TIME NEEDED: 0.70 Rating : 0.00 max weight: 9 14 +Unsatisfiable/BOO007-2.ma ... OK TIME NEEDED: 31.65 Rating : 0.14 max weight: 19 15 +Unsatisfiable/BOO007-4.ma ... OK TIME NEEDED: 27.51 Rating : 0.07 max weight: 19 16 +Unsatisfiable/BOO008-2.ma ... OK TIME NEEDED: 24.61 Rating : 0.07 max weight: 19 17 +Unsatisfiable/BOO008-4.ma ... OK TIME NEEDED: 146.41 Rating : 0.00 max weight: 20 18 +Unsatisfiable/BOO009-2.ma ... OK TIME NEEDED: 1.28 Rating : 0.00 max weight: 14 19 +Unsatisfiable/BOO009-4.ma ... OK TIME NEEDED: 0.26 Rating : 0.00 max weight: 14 20 +Unsatisfiable/BOO010-2.ma ... OK TIME NEEDED: 0.96 Rating : 0.00 max weight: 14 21 +Unsatisfiable/BOO010-4.ma ... OK TIME NEEDED: 0.32 Rating : 0.00 max weight: 14 22 +Unsatisfiable/BOO011-2.ma ... OK TIME NEEDED: 0.08 Rating : 0.00 max weight: 2 23 +Unsatisfiable/BOO011-4.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 max weight: 5 24 +Unsatisfiable/BOO012-2.ma ... OK TIME NEEDED: 0.41 Rating : 0.00 max weight: 18 25 +Unsatisfiable/BOO012-4.ma ... OK TIME NEEDED: 2.11 Rating : 0.00 max weight: 18 26 +Unsatisfiable/BOO013-2.ma ... OK TIME NEEDED: 0.31 Rating : 0.00 max weight: 10 27 +Unsatisfiable/BOO013-4.ma ... OK TIME NEEDED: 2.78 Rating : 0.00 max weight: 16 28 +Unsatisfiable/BOO014-2.ma ... OK TIME NEEDED: 20.42 Rating : 0.00 max weight: 18 29 +Unsatisfiable/BOO014-4.ma ... OK TIME NEEDED: 114.97 Rating : 0.00 max weight: 18 30 +Unsatisfiable/BOO015-2.ma ... OK TIME NEEDED: 15.38 Rating : 0.00 max weight: 18 31 +Unsatisfiable/BOO015-4.ma ... OK TIME NEEDED: 96.29 Rating : 0.00 max weight: 18 32 +Unsatisfiable/BOO016-2.ma ... OK TIME NEEDED: 0.85 Rating : 0.00 max weight: 17 33 +Unsatisfiable/BOO017-2.ma ... OK TIME NEEDED: 1.70 Rating : 0.00 max weight: 16 34 +Unsatisfiable/BOO018-4.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 max weight: 5 35 +Unsatisfiable/BOO021-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.07 max weight: 10 36 +Unsatisfiable/BOO022-1.ma ... OK TIME NEEDED: 65.58 Rating : 0.07 max weight: 18 37 +Unsatisfiable/BOO023-1.ma ... OK TIME NEEDED: 141.40 Rating : 0.50 max weight: 23 38 +Unsatisfiable/BOO024-1.ma ... OK TIME NEEDED: 17.84 Rating : 0.00 max weight: 14 39 +Unsatisfiable/BOO025-1.ma ... OK TIME NEEDED: 37.02 Rating : 0.07 max weight: 32 40 +Unsatisfiable/BOO026-1.ma ... OK TIME NEEDED: 17.55 Rating : 0.07 max weight: 21 41 +Unsatisfiable/BOO028-1.ma ... FAIL Rating : 0.07 42 +Unsatisfiable/BOO029-1.ma ... OK TIME NEEDED: 17.53 Rating : 0.00 max weight: 13 43 +Unsatisfiable/BOO031-1.ma ... FAIL Rating : 0.21 44 +Unsatisfiable/BOO034-1.ma ... OK TIME NEEDED: 0.89 Rating : 0.21 max weight: 20 45 +Unsatisfiable/BOO067-1.ma ... FAIL Rating : 0.21 46 +Unsatisfiable/BOO068-1.ma ... OK TIME NEEDED: 2.99 Rating : 0.00 max weight: 37 47 +Unsatisfiable/BOO069-1.ma ... OK TIME NEEDED: 2.85 Rating : 0.00 max weight: 36 48 +Unsatisfiable/BOO070-1.ma ... OK TIME NEEDED: 2.76 Rating : 0.00 max weight: 37 49 +Unsatisfiable/BOO071-1.ma ... OK TIME NEEDED: 3.18 Rating : 0.00 max weight: 36 50 +Unsatisfiable/BOO072-1.ma ... OK TIME NEEDED: 62.23 Rating : 0.07 max weight: 28 51 +Unsatisfiable/BOO073-1.ma ... FAIL Rating : 0.36 52 +Unsatisfiable/BOO074-1.ma ... OK TIME NEEDED: 99.57 Rating : 0.07 max weight: 27 53 +Unsatisfiable/BOO075-1.ma ... OK TIME NEEDED: 4.04 Rating : 0.00 max weight: 34 54 +Unsatisfiable/BOO076-1.ma ... FAIL Rating : 0.71 55 +Unsatisfiable/COL001-1.ma ... OK TIME NEEDED: 356.14 Rating : 0.07 max weight: 26 56 +Unsatisfiable/COL001-2.ma ... OK TIME NEEDED: 4.21 Rating : 0.07 max weight: 23 57 +Unsatisfiable/COL002-1.ma ... OK TIME NEEDED: 4.18 Rating : 0.00 max weight: 23 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.02 Rating : 0.21 max weight: 20 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 max weight: 0 68 +Unsatisfiable/COL008-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 11 69 +Unsatisfiable/COL009-1.ma ... OK TIME NEEDED: 3.16 Rating : 0.07 max weight: 18 70 +Unsatisfiable/COL010-1.ma ... OK TIME NEEDED: 1.59 Rating : 0.07 max weight: 23 71 +Unsatisfiable/COL011-1.ma ... FAIL Rating : 0.36 72 +Unsatisfiable/COL012-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 73 +Unsatisfiable/COL013-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 0 74 +Unsatisfiable/COL014-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 75 +Unsatisfiable/COL015-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 max weight: 11 76 +Unsatisfiable/COL016-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 0 77 +Unsatisfiable/COL017-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 11 78 +Unsatisfiable/COL018-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 79 +Unsatisfiable/COL019-1.ma ... OK TIME NEEDED: 1.65 Rating : 0.00 max weight: 23 80 +Unsatisfiable/COL020-1.ma ... FAIL Rating : 0.07 81 +Unsatisfiable/COL021-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 max weight: 11 82 +Unsatisfiable/COL022-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 11 83 +Unsatisfiable/COL023-1.ma ... FAIL Rating : 0.00 84 +Unsatisfiable/COL024-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 11 85 +Unsatisfiable/COL025-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 17 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 max weight: 0 89 +Unsatisfiable/COL030-1.ma ... OK TIME NEEDED: 0.18 Rating : 0.14 max weight: 13 90 +Unsatisfiable/COL031-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 0 91 +Unsatisfiable/COL032-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.14 max weight: 0 92 +Unsatisfiable/COL033-1.ma ... OK TIME NEEDED: 4.71 Rating : 0.07 max weight: 16 93 +Unsatisfiable/COL034-1.ma ... OK TIME NEEDED: 0.51 Rating : 0.43 max weight: 0 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 ... OK TIME NEEDED: 5.87 Rating : 0.00 max weight: 11 99 +Unsatisfiable/COL041-1.ma ... OK TIME NEEDED: 0.65 Rating : 0.36 max weight: 0 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.22 Rating : 0.00 max weight: 11 113 +Unsatisfiable/COL046-1.ma ... FAIL Rating : 0.64 114 +Unsatisfiable/COL048-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 17 115 +Unsatisfiable/COL049-1.ma ... OK TIME NEEDED: 5.11 Rating : 0.29 max weight: 17 116 +Unsatisfiable/COL050-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 9 117 +Unsatisfiable/COL051-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 9 118 +Unsatisfiable/COL052-1.ma ... FAIL Rating : 0.00 119 +Unsatisfiable/COL053-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 0 120 +Unsatisfiable/COL056-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.07 max weight: 6 121 +Unsatisfiable/COL057-1.ma ... FAIL Rating : 0.36 122 +Unsatisfiable/COL058-1.ma ... OK TIME NEEDED: 0.32 Rating : 0.00 max weight: 0 123 +Unsatisfiable/COL058-2.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 max weight: 10 124 +Unsatisfiable/COL058-3.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 10 125 +Unsatisfiable/COL059-1.ma ... FAIL Rating : 0.00 126 +Unsatisfiable/COL060-1.ma ... OK TIME NEEDED: 23.48 Rating : 0.36 max weight: 0 127 +Unsatisfiable/COL060-2.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 128 +Unsatisfiable/COL060-3.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 129 +Unsatisfiable/COL061-1.ma ... OK TIME NEEDED: 477.77 Rating : 0.36 max weight: 0 130 +Unsatisfiable/COL061-2.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 131 +Unsatisfiable/COL061-3.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 132 +Unsatisfiable/COL062-1.ma ... FAIL Rating : 0.50 133 +Unsatisfiable/COL062-2.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 134 +Unsatisfiable/COL062-3.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 135 +Unsatisfiable/COL063-1.ma ... FAIL Rating : 0.50 136 +Unsatisfiable/COL063-2.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 137 +Unsatisfiable/COL063-3.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 138 +Unsatisfiable/COL063-4.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 139 +Unsatisfiable/COL063-5.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 140 +Unsatisfiable/COL063-6.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 141 +Unsatisfiable/COL064-1.ma ... FAIL Rating : 0.64 142 +Unsatisfiable/COL064-2.ma ... OK TIME NEEDED: 0.00 Rating : 0.07 max weight: 0 143 +Unsatisfiable/COL064-3.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 144 +Unsatisfiable/COL064-4.ma ... OK TIME NEEDED: 0.00 Rating : 0.07 max weight: 0 145 +Unsatisfiable/COL064-5.ma ... OK TIME NEEDED: 0.00 Rating : 0.07 max weight: 0 146 +Unsatisfiable/COL064-6.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 147 +Unsatisfiable/COL064-7.ma ... OK TIME NEEDED: 0.00 Rating : 0.07 max weight: 0 148 +Unsatisfiable/COL064-8.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 149 +Unsatisfiable/COL064-9.ma ... OK TIME NEEDED: 0.00 Rating : 0.07 max weight: 0 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: 2.51 Rating : 0.00 max weight: 21 153 +Unsatisfiable/COL066-3.ma ... OK TIME NEEDED: 2.07 Rating : 0.00 max weight: 21 154 +Unsatisfiable/COL070-1.ma ... FAIL Rating : 0.07 155 +Unsatisfiable/COL075-2.ma ... OK TIME NEEDED: 0.16 Rating : 0.00 max weight: 23 156 +Unsatisfiable/COL083-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 157 +Unsatisfiable/COL084-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 158 +Unsatisfiable/COL085-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 159 +Unsatisfiable/COL086-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 160 +Unsatisfiable/GRP001-2.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 max weight: 7 161 +Unsatisfiable/GRP001-4.ma ... OK TIME NEEDED: 0.18 Rating : 0.00 max weight: 7 162 +Unsatisfiable/GRP002-2.ma ... OK TIME NEEDED: 31.68 Rating : 0.00 max weight: 22 163 +Unsatisfiable/GRP002-3.ma ... OK TIME NEEDED: 347.29 Rating : 0.00 max weight: 23 164 +Unsatisfiable/GRP002-4.ma ... OK TIME NEEDED: 67.57 Rating : 0.00 max weight: 23 165 +Unsatisfiable/GRP010-4.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 8 166 +Unsatisfiable/GRP011-4.ma ... OK TIME NEEDED: 0.25 Rating : 0.00 max weight: 12 167 +Unsatisfiable/GRP012-4.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 max weight: 8 168 +Unsatisfiable/GRP014-1.ma ... OK TIME NEEDED: 50.29 Rating : 0.14 max weight: 39 169 +Unsatisfiable/GRP022-2.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 9 170 +Unsatisfiable/GRP023-2.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 2 171 +Unsatisfiable/GRP024-5.ma ... FAIL Rating : 0.50 172 +Unsatisfiable/GRP114-1.ma ... OK TIME NEEDED: 215.54 Rating : 0.29 max weight: 18 173 +Unsatisfiable/GRP115-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 18 174 +Unsatisfiable/GRP116-1.ma ... OK TIME NEEDED: 0.15 Rating : 0.00 max weight: 18 175 +Unsatisfiable/GRP117-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 18 176 +Unsatisfiable/GRP118-1.ma ... OK TIME NEEDED: 0.17 Rating : 0.00 max weight: 19 177 +Unsatisfiable/GRP119-1.ma ... OK TIME NEEDED: 54.79 Rating : 0.00 max weight: 68 178 +Unsatisfiable/GRP120-1.ma ... OK TIME NEEDED: 41.58 Rating : 0.00 max weight: 68 179 +Unsatisfiable/GRP121-1.ma ... OK TIME NEEDED: 37.22 Rating : 0.00 max weight: 68 180 +Unsatisfiable/GRP122-1.ma ... OK TIME NEEDED: 38.77 Rating : 0.07 max weight: 69 181 +Unsatisfiable/GRP136-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 max weight: 4 182 +Unsatisfiable/GRP137-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 max weight: 4 183 +Unsatisfiable/GRP138-1.ma ... OK TIME NEEDED: 4.32 Rating : 0.00 max weight: 7 184 +Unsatisfiable/GRP139-1.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 max weight: 16 185 +Unsatisfiable/GRP140-1.ma ... OK TIME NEEDED: 3.11 Rating : 0.00 max weight: 7 186 +Unsatisfiable/GRP141-1.ma ... OK TIME NEEDED: 0.21 Rating : 0.00 max weight: 16 187 +Unsatisfiable/GRP142-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 max weight: 0 188 +Unsatisfiable/GRP143-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 6 189 +Unsatisfiable/GRP144-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 max weight: 6 190 +Unsatisfiable/GRP145-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 16 191 +Unsatisfiable/GRP146-1.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 max weight: 16 192 +Unsatisfiable/GRP147-1.ma ... OK TIME NEEDED: 4.68 Rating : 0.00 max weight: 7 193 +Unsatisfiable/GRP148-1.ma ... OK TIME NEEDED: 3.40 Rating : 0.00 max weight: 7 194 +Unsatisfiable/GRP149-1.ma ... OK TIME NEEDED: 0.24 Rating : 0.00 max weight: 16 195 +Unsatisfiable/GRP150-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 max weight: 6 196 +Unsatisfiable/GRP151-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 0 197 +Unsatisfiable/GRP152-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 max weight: 16 198 +Unsatisfiable/GRP153-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 6 199 +Unsatisfiable/GRP154-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 max weight: 3 200 +Unsatisfiable/GRP155-1.ma ... OK TIME NEEDED: 0.08 Rating : 0.00 max weight: 3 201 +Unsatisfiable/GRP156-1.ma ... OK TIME NEEDED: 0.13 Rating : 0.00 max weight: 4 202 +Unsatisfiable/GRP157-1.ma ... OK TIME NEEDED: 0.08 Rating : 0.00 max weight: 3 203 +Unsatisfiable/GRP158-1.ma ... OK TIME NEEDED: 0.13 Rating : 0.00 max weight: 3 204 +Unsatisfiable/GRP159-1.ma ... OK TIME NEEDED: 0.28 Rating : 0.00 max weight: 7 205 +Unsatisfiable/GRP160-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 0 206 +Unsatisfiable/GRP161-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 max weight: 0 207 +Unsatisfiable/GRP162-1.ma ... OK TIME NEEDED: 0.29 Rating : 0.00 max weight: 7 208 +Unsatisfiable/GRP163-1.ma ... OK TIME NEEDED: 0.43 Rating : 0.00 max weight: 7 209 +Unsatisfiable/GRP164-1.ma ... FAIL Rating : 0.93 210 +Unsatisfiable/GRP164-2.ma ... FAIL Rating : 0.93 211 +Unsatisfiable/GRP165-1.ma ... OK TIME NEEDED: 54.54 Rating : 0.00 max weight: 14 212 +Unsatisfiable/GRP165-2.ma ... OK TIME NEEDED: 51.75 Rating : 0.00 max weight: 15 213 +Unsatisfiable/GRP166-1.ma ... OK TIME NEEDED: 261.59 Rating : 0.00 max weight: 21 214 +Unsatisfiable/GRP166-2.ma ... FAIL Rating : 0.00 215 +Unsatisfiable/GRP166-3.ma ... OK TIME NEEDED: 62.82 Rating : 0.00 max weight: 14 216 +Unsatisfiable/GRP166-4.ma ... OK TIME NEEDED: 52.29 Rating : 0.00 max weight: 15 217 +Unsatisfiable/GRP167-1.ma ... OK TIME NEEDED: 124.19 Rating : 0.21 max weight: 18 218 +Unsatisfiable/GRP167-2.ma ... OK TIME NEEDED: 300.19 Rating : 0.21 max weight: 18 219 +Unsatisfiable/GRP167-3.ma ... OK TIME NEEDED: 311.96 Rating : 0.50 max weight: 14 220 +Unsatisfiable/GRP167-4.ma ... OK TIME NEEDED: 250.37 Rating : 0.43 max weight: 16 221 +Unsatisfiable/GRP167-5.ma ... OK TIME NEEDED: 19.53 Rating : 0.14 max weight: 15 222 +Unsatisfiable/GRP168-1.ma ... OK TIME NEEDED: 0.09 Rating : 0.07 max weight: 3 223 +Unsatisfiable/GRP168-2.ma ... OK TIME NEEDED: 0.09 Rating : 0.07 max weight: 3 224 +Unsatisfiable/GRP169-1.ma ... OK TIME NEEDED: 107.13 Rating : 0.00 max weight: 12 225 +Unsatisfiable/GRP169-2.ma ... OK TIME NEEDED: 114.44 Rating : 0.00 max weight: 13 226 +Unsatisfiable/GRP170-1.ma ... OK TIME NEEDED: 307.40 Rating : 0.00 max weight: 14 227 +Unsatisfiable/GRP170-2.ma ... OK TIME NEEDED: 318.68 Rating : 0.00 max weight: 14 228 +Unsatisfiable/GRP170-3.ma ... OK TIME NEEDED: 339.79 Rating : 0.00 max weight: 14 229 +Unsatisfiable/GRP170-4.ma ... OK TIME NEEDED: 325.63 Rating : 0.00 max weight: 14 230 +Unsatisfiable/GRP171-1.ma ... OK TIME NEEDED: 6.36 Rating : 0.00 max weight: 10 231 +Unsatisfiable/GRP171-2.ma ... OK TIME NEEDED: 6.96 Rating : 0.00 max weight: 10 232 +Unsatisfiable/GRP172-1.ma ... OK TIME NEEDED: 10.72 Rating : 0.00 max weight: 10 233 +Unsatisfiable/GRP172-2.ma ... OK TIME NEEDED: 6.19 Rating : 0.00 max weight: 10 234 +Unsatisfiable/GRP173-1.ma ... OK TIME NEEDED: 15.46 Rating : 0.00 max weight: 11 235 +Unsatisfiable/GRP174-1.ma ... OK TIME NEEDED: 21.49 Rating : 0.00 max weight: 11 236 +Unsatisfiable/GRP175-1.ma ... OK TIME NEEDED: 33.68 Rating : 0.00 max weight: 13 237 +Unsatisfiable/GRP175-2.ma ... OK TIME NEEDED: 41.46 Rating : 0.00 max weight: 14 238 +Unsatisfiable/GRP175-3.ma ... OK TIME NEEDED: 41.14 Rating : 0.00 max weight: 14 239 +Unsatisfiable/GRP175-4.ma ... OK TIME NEEDED: 41.87 Rating : 0.00 max weight: 13 240 +Unsatisfiable/GRP176-1.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 max weight: 0 241 +Unsatisfiable/GRP176-2.ma ... OK TIME NEEDED: 0.08 Rating : 0.00 max weight: 0 242 +Unsatisfiable/GRP177-2.ma ... FAIL Rating : 0.21 243 +Unsatisfiable/GRP178-1.ma ... OK TIME NEEDED: 282.09 Rating : 0.14 max weight: 15 244 +Unsatisfiable/GRP178-2.ma ... OK TIME NEEDED: 297.82 Rating : 0.14 max weight: 15 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: 547.55 Rating : 0.43 max weight: 19 253 +Unsatisfiable/GRP181-4.ma ... FAIL Rating : 0.43 254 +Unsatisfiable/GRP182-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 6 255 +Unsatisfiable/GRP182-2.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 6 256 +Unsatisfiable/GRP182-3.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 max weight: 6 257 +Unsatisfiable/GRP182-4.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 6 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 ... OK TIME NEEDED: 39.14 Rating : 0.00 max weight: 16 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.21 Rating : 0.00 max weight: 9 273 +Unsatisfiable/GRP186-4.ma ... OK TIME NEEDED: 0.13 Rating : 0.00 max weight: 7 274 +Unsatisfiable/GRP187-1.ma ... FAIL Rating : 0.64 275 +Unsatisfiable/GRP188-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 max weight: 16 276 +Unsatisfiable/GRP188-2.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 16 277 +Unsatisfiable/GRP189-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 6 278 +Unsatisfiable/GRP189-2.ma ... OK TIME NEEDED: 0.07 Rating : 0.00 max weight: 6 279 +Unsatisfiable/GRP190-1.ma ... OK TIME NEEDED: 88.61 Rating : 0.00 max weight: 15 280 +Unsatisfiable/GRP190-2.ma ... OK TIME NEEDED: 81.56 Rating : 0.00 max weight: 12 281 +Unsatisfiable/GRP191-1.ma ... OK TIME NEEDED: 106.88 Rating : 0.00 max weight: 12 282 +Unsatisfiable/GRP191-2.ma ... OK TIME NEEDED: 89.87 Rating : 0.00 max weight: 11 283 +Unsatisfiable/GRP192-1.ma ... OK TIME NEEDED: 0.69 Rating : 0.07 max weight: 15 284 +Unsatisfiable/GRP193-1.ma ... OK TIME NEEDED: 70.37 Rating : 0.00 max weight: 16 285 +Unsatisfiable/GRP193-2.ma ... OK TIME NEEDED: 50.43 Rating : 0.00 max weight: 15 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.18 Rating : 0.00 max weight: 12 294 +Unsatisfiable/GRP403-1.ma ... OK TIME NEEDED: 8.97 Rating : 0.07 max weight: 38 295 +Unsatisfiable/GRP404-1.ma ... OK TIME NEEDED: 51.68 Rating : 0.21 max weight: 48 296 +Unsatisfiable/GRP405-1.ma ... OK TIME NEEDED: 33.55 Rating : 0.21 max weight: 39 297 +Unsatisfiable/GRP406-1.ma ... OK TIME NEEDED: 128.40 Rating : 0.00 max weight: 67 298 +Unsatisfiable/GRP407-1.ma ... OK TIME NEEDED: 240.49 Rating : 0.00 max weight: 67 299 +Unsatisfiable/GRP408-1.ma ... OK TIME NEEDED: 243.34 Rating : 0.00 max weight: 68 300 +Unsatisfiable/GRP409-1.ma ... OK TIME NEEDED: 10.16 Rating : 0.00 max weight: 50 301 +Unsatisfiable/GRP410-1.ma ... OK TIME NEEDED: 22.28 Rating : 0.21 max weight: 50 302 +Unsatisfiable/GRP411-1.ma ... OK TIME NEEDED: 19.42 Rating : 0.21 max weight: 51 303 +Unsatisfiable/GRP412-1.ma ... OK TIME NEEDED: 19.16 Rating : 0.00 max weight: 44 304 +Unsatisfiable/GRP413-1.ma ... OK TIME NEEDED: 100.00 Rating : 0.07 max weight: 44 305 +Unsatisfiable/GRP414-1.ma ... OK TIME NEEDED: 62.50 Rating : 0.07 max weight: 45 306 +Unsatisfiable/GRP415-1.ma ... OK TIME NEEDED: 342.07 Rating : 0.00 max weight: 68 307 +Unsatisfiable/GRP416-1.ma ... OK TIME NEEDED: 400.72 Rating : 0.07 max weight: 68 308 +Unsatisfiable/GRP417-1.ma ... OK TIME NEEDED: 388.08 Rating : 0.14 max weight: 69 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 ... OK TIME NEEDED: 3.56 Rating : 0.14 max weight: 71 313 +Unsatisfiable/GRP422-1.ma ... OK TIME NEEDED: 150.83 Rating : 0.29 max weight: 71 314 +Unsatisfiable/GRP423-1.ma ... OK TIME NEEDED: 76.62 Rating : 0.36 max weight: 72 315 +Unsatisfiable/GRP424-1.ma ... OK TIME NEEDED: 11.61 Rating : 0.00 max weight: 63 316 +Unsatisfiable/GRP425-1.ma ... OK TIME NEEDED: 11.20 Rating : 0.07 max weight: 63 317 +Unsatisfiable/GRP426-1.ma ... OK TIME NEEDED: 20.01 Rating : 0.14 max weight: 64 318 +Unsatisfiable/GRP427-1.ma ... OK TIME NEEDED: 31.94 Rating : 0.00 max weight: 38 319 +Unsatisfiable/GRP428-1.ma ... OK TIME NEEDED: 36.60 Rating : 0.00 max weight: 38 320 +Unsatisfiable/GRP429-1.ma ... OK TIME NEEDED: 50.34 Rating : 0.14 max weight: 39 321 +Unsatisfiable/GRP430-1.ma ... OK TIME NEEDED: 17.74 Rating : 0.00 max weight: 42 322 +Unsatisfiable/GRP431-1.ma ... OK TIME NEEDED: 16.07 Rating : 0.00 max weight: 42 323 +Unsatisfiable/GRP432-1.ma ... OK TIME NEEDED: 15.53 Rating : 0.00 max weight: 43 324 +Unsatisfiable/GRP433-1.ma ... OK TIME NEEDED: 4.91 Rating : 0.00 max weight: 22 325 +Unsatisfiable/GRP434-1.ma ... OK TIME NEEDED: 5.55 Rating : 0.00 max weight: 22 326 +Unsatisfiable/GRP435-1.ma ... OK TIME NEEDED: 8.83 Rating : 0.00 max weight: 24 327 +Unsatisfiable/GRP436-1.ma ... OK TIME NEEDED: 36.79 Rating : 0.07 max weight: 55 328 +Unsatisfiable/GRP437-1.ma ... OK TIME NEEDED: 35.27 Rating : 0.07 max weight: 55 329 +Unsatisfiable/GRP438-1.ma ... OK TIME NEEDED: 38.97 Rating : 0.07 max weight: 56 330 +Unsatisfiable/GRP439-1.ma ... OK TIME NEEDED: 13.91 Rating : 0.07 max weight: 48 331 +Unsatisfiable/GRP440-1.ma ... OK TIME NEEDED: 28.28 Rating : 0.14 max weight: 48 332 +Unsatisfiable/GRP441-1.ma ... OK TIME NEEDED: 36.20 Rating : 0.21 max weight: 49 333 +Unsatisfiable/GRP442-1.ma ... OK TIME NEEDED: 163.86 Rating : 0.14 max weight: 38 334 +Unsatisfiable/GRP443-1.ma ... OK TIME NEEDED: 169.09 Rating : 0.07 max weight: 38 335 +Unsatisfiable/GRP444-1.ma ... OK TIME NEEDED: 139.87 Rating : 0.21 max weight: 39 336 +Unsatisfiable/GRP445-1.ma ... OK TIME NEEDED: 0.48 Rating : 0.00 max weight: 15 337 +Unsatisfiable/GRP446-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 max weight: 15 338 +Unsatisfiable/GRP447-1.ma ... OK TIME NEEDED: 1.11 Rating : 0.14 max weight: 16 339 +Unsatisfiable/GRP448-1.ma ... OK TIME NEEDED: 0.33 Rating : 0.00 max weight: 15 340 +Unsatisfiable/GRP449-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 max weight: 15 341 +Unsatisfiable/GRP450-1.ma ... OK TIME NEEDED: 1.05 Rating : 0.07 max weight: 16 342 +Unsatisfiable/GRP451-1.ma ... OK TIME NEEDED: 0.15 Rating : 0.00 max weight: 14 343 +Unsatisfiable/GRP452-1.ma ... OK TIME NEEDED: 1.64 Rating : 0.14 max weight: 21 344 +Unsatisfiable/GRP453-1.ma ... OK TIME NEEDED: 2.88 Rating : 0.21 max weight: 26 345 +Unsatisfiable/GRP454-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 7 346 +Unsatisfiable/GRP455-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 15 347 +Unsatisfiable/GRP456-1.ma ... OK TIME NEEDED: 0.24 Rating : 0.07 max weight: 17 348 +Unsatisfiable/GRP457-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 7 349 +Unsatisfiable/GRP458-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 15 350 +Unsatisfiable/GRP459-1.ma ... OK TIME NEEDED: 0.25 Rating : 0.00 max weight: 17 351 +Unsatisfiable/GRP460-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 7 352 +Unsatisfiable/GRP461-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 max weight: 15 353 +Unsatisfiable/GRP462-1.ma ... OK TIME NEEDED: 0.31 Rating : 0.00 max weight: 16 354 +Unsatisfiable/GRP463-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 7 355 +Unsatisfiable/GRP464-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 max weight: 15 356 +Unsatisfiable/GRP465-1.ma ... OK TIME NEEDED: 0.40 Rating : 0.00 max weight: 16 357 +Unsatisfiable/GRP466-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 max weight: 19 358 +Unsatisfiable/GRP467-1.ma ... OK TIME NEEDED: 0.67 Rating : 0.00 max weight: 19 359 +Unsatisfiable/GRP468-1.ma ... OK TIME NEEDED: 1.07 Rating : 0.00 max weight: 19 360 +Unsatisfiable/GRP469-1.ma ... OK TIME NEEDED: 116.49 Rating : 0.21 max weight: 43 361 +Unsatisfiable/GRP470-1.ma ... OK TIME NEEDED: 123.50 Rating : 0.21 max weight: 43 362 +Unsatisfiable/GRP471-1.ma ... OK TIME NEEDED: 48.37 Rating : 0.21 max weight: 38 363 +Unsatisfiable/GRP472-1.ma ... OK TIME NEEDED: 41.32 Rating : 0.07 max weight: 47 364 +Unsatisfiable/GRP473-1.ma ... OK TIME NEEDED: 37.76 Rating : 0.07 max weight: 47 365 +Unsatisfiable/GRP474-1.ma ... OK TIME NEEDED: 53.59 Rating : 0.07 max weight: 48 366 +Unsatisfiable/GRP475-1.ma ... OK TIME NEEDED: 51.86 Rating : 0.21 max weight: 37 367 +Unsatisfiable/GRP476-1.ma ... OK TIME NEEDED: 37.80 Rating : 0.21 max weight: 37 368 +Unsatisfiable/GRP477-1.ma ... OK TIME NEEDED: 41.41 Rating : 0.21 max weight: 38 369 +Unsatisfiable/GRP478-1.ma ... OK TIME NEEDED: 18.96 Rating : 0.14 max weight: 32 370 +Unsatisfiable/GRP479-1.ma ... OK TIME NEEDED: 19.22 Rating : 0.14 max weight: 32 371 +Unsatisfiable/GRP480-1.ma ... OK TIME NEEDED: 21.92 Rating : 0.21 max weight: 33 372 +Unsatisfiable/GRP481-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 max weight: 20 373 +Unsatisfiable/GRP482-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 21 374 +Unsatisfiable/GRP483-1.ma ... OK TIME NEEDED: 1.16 Rating : 0.00 max weight: 22 375 +Unsatisfiable/GRP484-1.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 max weight: 16 376 +Unsatisfiable/GRP485-1.ma ... OK TIME NEEDED: 0.23 Rating : 0.00 max weight: 17 377 +Unsatisfiable/GRP486-1.ma ... OK TIME NEEDED: 1.23 Rating : 0.00 max weight: 18 378 +Unsatisfiable/GRP487-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 max weight: 15 379 +Unsatisfiable/GRP488-1.ma ... OK TIME NEEDED: 1.17 Rating : 0.00 max weight: 15 380 +Unsatisfiable/GRP489-1.ma ... OK TIME NEEDED: 2.53 Rating : 0.00 max weight: 26 381 +Unsatisfiable/GRP490-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 15 382 +Unsatisfiable/GRP491-1.ma ... OK TIME NEEDED: 0.08 Rating : 0.00 max weight: 16 383 +Unsatisfiable/GRP492-1.ma ... OK TIME NEEDED: 0.36 Rating : 0.00 max weight: 17 384 +Unsatisfiable/GRP493-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 max weight: 16 385 +Unsatisfiable/GRP494-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 17 386 +Unsatisfiable/GRP495-1.ma ... OK TIME NEEDED: 0.27 Rating : 0.00 max weight: 18 387 +Unsatisfiable/GRP496-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 16 388 +Unsatisfiable/GRP497-1.ma ... OK TIME NEEDED: 0.19 Rating : 0.00 max weight: 17 389 +Unsatisfiable/GRP498-1.ma ... OK TIME NEEDED: 0.46 Rating : 0.00 max weight: 18 390 +Unsatisfiable/GRP499-1.ma ... OK TIME NEEDED: 7.75 Rating : 0.00 max weight: 38 391 +Unsatisfiable/GRP500-1.ma ... OK TIME NEEDED: 4.26 Rating : 0.07 max weight: 38 392 +Unsatisfiable/GRP501-1.ma ... OK TIME NEEDED: 87.52 Rating : 0.14 max weight: 39 393 +Unsatisfiable/GRP502-1.ma ... OK TIME NEEDED: 161.64 Rating : 0.14 max weight: 42 394 +Unsatisfiable/GRP503-1.ma ... OK TIME NEEDED: 248.32 Rating : 0.14 max weight: 42 395 +Unsatisfiable/GRP504-1.ma ... OK TIME NEEDED: 247.37 Rating : 0.14 max weight: 43 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: 143.03 Rating : 0.00 max weight: 21 401 +Unsatisfiable/GRP510-1.ma ... OK TIME NEEDED: 0.78 Rating : 0.00 max weight: 21 402 +Unsatisfiable/GRP511-1.ma ... OK TIME NEEDED: 8.71 Rating : 0.00 max weight: 22 403 +Unsatisfiable/GRP512-1.ma ... OK TIME NEEDED: 0.17 Rating : 0.00 max weight: 22 404 +Unsatisfiable/GRP513-1.ma ... OK TIME NEEDED: 57.79 Rating : 0.00 max weight: 16 405 +Unsatisfiable/GRP514-1.ma ... OK TIME NEEDED: 0.17 Rating : 0.00 max weight: 16 406 +Unsatisfiable/GRP515-1.ma ... OK TIME NEEDED: 0.31 Rating : 0.00 max weight: 17 407 +Unsatisfiable/GRP516-1.ma ... OK TIME NEEDED: 0.17 Rating : 0.00 max weight: 17 408 +Unsatisfiable/GRP517-1.ma ... OK TIME NEEDED: 1.38 Rating : 0.00 max weight: 16 409 +Unsatisfiable/GRP518-1.ma ... OK TIME NEEDED: 0.13 Rating : 0.00 max weight: 16 410 +Unsatisfiable/GRP519-1.ma ... OK TIME NEEDED: 0.46 Rating : 0.00 max weight: 17 411 +Unsatisfiable/GRP520-1.ma ... OK TIME NEEDED: 0.18 Rating : 0.00 max weight: 17 412 +Unsatisfiable/GRP521-1.ma ... OK TIME NEEDED: 0.12 Rating : 0.00 max weight: 11 413 +Unsatisfiable/GRP522-1.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 max weight: 12 414 +Unsatisfiable/GRP523-1.ma ... OK TIME NEEDED: 2.70 Rating : 0.00 max weight: 16 415 +Unsatisfiable/GRP524-1.ma ... OK TIME NEEDED: 0.19 Rating : 0.00 max weight: 13 416 +Unsatisfiable/GRP525-1.ma ... OK TIME NEEDED: 0.14 Rating : 0.00 max weight: 10 417 +Unsatisfiable/GRP526-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 max weight: 10 418 +Unsatisfiable/GRP527-1.ma ... OK TIME NEEDED: 9.44 Rating : 0.00 max weight: 16 419 +Unsatisfiable/GRP528-1.ma ... OK TIME NEEDED: 0.19 Rating : 0.00 max weight: 16 420 +Unsatisfiable/GRP529-1.ma ... OK TIME NEEDED: 0.15 Rating : 0.00 max weight: 11 421 +Unsatisfiable/GRP530-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 8 422 +Unsatisfiable/GRP531-1.ma ... OK TIME NEEDED: 2.91 Rating : 0.00 max weight: 16 423 +Unsatisfiable/GRP532-1.ma ... OK TIME NEEDED: 0.15 Rating : 0.00 max weight: 11 424 +Unsatisfiable/GRP533-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 7 425 +Unsatisfiable/GRP534-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 max weight: 11 426 +Unsatisfiable/GRP535-1.ma ... OK TIME NEEDED: 2.82 Rating : 0.00 max weight: 16 427 +Unsatisfiable/GRP536-1.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 max weight: 15 428 +Unsatisfiable/GRP537-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 7 429 +Unsatisfiable/GRP538-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 max weight: 11 430 +Unsatisfiable/GRP539-1.ma ... OK TIME NEEDED: 2.45 Rating : 0.00 max weight: 17 431 +Unsatisfiable/GRP540-1.ma ... OK TIME NEEDED: 0.13 Rating : 0.00 max weight: 11 432 +Unsatisfiable/GRP541-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 7 433 +Unsatisfiable/GRP542-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 max weight: 12 434 +Unsatisfiable/GRP543-1.ma ... OK TIME NEEDED: 0.67 Rating : 0.00 max weight: 16 435 +Unsatisfiable/GRP544-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 13 436 +Unsatisfiable/GRP545-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 7 437 +Unsatisfiable/GRP546-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 max weight: 12 438 +Unsatisfiable/GRP547-1.ma ... OK TIME NEEDED: 1.70 Rating : 0.00 max weight: 17 439 +Unsatisfiable/GRP548-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 13 440 +Unsatisfiable/GRP549-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 7 441 +Unsatisfiable/GRP550-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.07 max weight: 12 442 +Unsatisfiable/GRP551-1.ma ... OK TIME NEEDED: 0.75 Rating : 0.00 max weight: 16 443 +Unsatisfiable/GRP552-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 max weight: 13 444 +Unsatisfiable/GRP553-1.ma ... OK TIME NEEDED: 0.13 Rating : 0.00 max weight: 15 445 +Unsatisfiable/GRP554-1.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 max weight: 16 446 +Unsatisfiable/GRP555-1.ma ... OK TIME NEEDED: 1.03 Rating : 0.00 max weight: 19 447 +Unsatisfiable/GRP556-1.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 max weight: 15 448 +Unsatisfiable/GRP557-1.ma ... OK TIME NEEDED: 0.16 Rating : 0.00 max weight: 15 449 +Unsatisfiable/GRP558-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 max weight: 15 450 +Unsatisfiable/GRP559-1.ma ... OK TIME NEEDED: 3.08 Rating : 0.00 max weight: 16 451 +Unsatisfiable/GRP560-1.ma ... OK TIME NEEDED: 0.25 Rating : 0.00 max weight: 15 452 +Unsatisfiable/GRP561-1.ma ... OK TIME NEEDED: 0.14 Rating : 0.00 max weight: 17 453 +Unsatisfiable/GRP562-1.ma ... OK TIME NEEDED: 0.07 Rating : 0.00 max weight: 16 454 +Unsatisfiable/GRP563-1.ma ... OK TIME NEEDED: 6.03 Rating : 0.00 max weight: 17 455 +Unsatisfiable/GRP564-1.ma ... OK TIME NEEDED: 0.16 Rating : 0.00 max weight: 17 456 +Unsatisfiable/GRP565-1.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 max weight: 16 457 +Unsatisfiable/GRP566-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 17 458 +Unsatisfiable/GRP567-1.ma ... OK TIME NEEDED: 28.20 Rating : 0.14 max weight: 27 459 +Unsatisfiable/GRP568-1.ma ... OK TIME NEEDED: 0.36 Rating : 0.14 max weight: 27 460 +Unsatisfiable/GRP569-1.ma ... OK TIME NEEDED: 0.07 Rating : 0.00 max weight: 16 461 +Unsatisfiable/GRP570-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 17 462 +Unsatisfiable/GRP571-1.ma ... OK TIME NEEDED: 26.98 Rating : 0.14 max weight: 25 463 +Unsatisfiable/GRP572-1.ma ... OK TIME NEEDED: 0.24 Rating : 0.07 max weight: 18 464 +Unsatisfiable/GRP573-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 16 465 +Unsatisfiable/GRP574-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 max weight: 19 466 +Unsatisfiable/GRP575-1.ma ... OK TIME NEEDED: 46.52 Rating : 0.14 max weight: 25 467 +Unsatisfiable/GRP576-1.ma ... OK TIME NEEDED: 0.35 Rating : 0.00 max weight: 25 468 +Unsatisfiable/GRP577-1.ma ... OK TIME NEEDED: 0.21 Rating : 0.00 max weight: 16 469 +Unsatisfiable/GRP578-1.ma ... OK TIME NEEDED: 0.43 Rating : 0.00 max weight: 17 470 +Unsatisfiable/GRP579-1.ma ... OK TIME NEEDED: 1.66 Rating : 0.07 max weight: 25 471 +Unsatisfiable/GRP580-1.ma ... OK TIME NEEDED: 0.46 Rating : 0.00 max weight: 25 472 +Unsatisfiable/GRP581-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 max weight: 16 473 +Unsatisfiable/GRP582-1.ma ... OK TIME NEEDED: 0.30 Rating : 0.00 max weight: 17 474 +Unsatisfiable/GRP583-1.ma ... OK TIME NEEDED: 2.94 Rating : 0.07 max weight: 19 475 +Unsatisfiable/GRP584-1.ma ... OK TIME NEEDED: 0.23 Rating : 0.00 max weight: 18 476 +Unsatisfiable/GRP585-1.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 max weight: 19 477 +Unsatisfiable/GRP586-1.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 max weight: 19 478 +Unsatisfiable/GRP587-1.ma ... FAIL Rating : 0.00 479 +Unsatisfiable/GRP588-1.ma ... OK TIME NEEDED: 1.47 Rating : 0.00 max weight: 20 480 +Unsatisfiable/GRP589-1.ma ... OK TIME NEEDED: 0.50 Rating : 0.00 max weight: 19 481 +Unsatisfiable/GRP590-1.ma ... OK TIME NEEDED: 0.12 Rating : 0.00 max weight: 19 482 +Unsatisfiable/GRP591-1.ma ... OK TIME NEEDED: 0.64 Rating : 0.07 max weight: 20 483 +Unsatisfiable/GRP592-1.ma ... OK TIME NEEDED: 0.28 Rating : 0.07 max weight: 20 484 +Unsatisfiable/GRP593-1.ma ... OK TIME NEEDED: 2.56 Rating : 0.00 max weight: 16 485 +Unsatisfiable/GRP594-1.ma ... OK TIME NEEDED: 1.16 Rating : 0.00 max weight: 16 486 +Unsatisfiable/GRP595-1.ma ... OK TIME NEEDED: 0.24 Rating : 0.07 max weight: 16 487 +Unsatisfiable/GRP596-1.ma ... OK TIME NEEDED: 0.29 Rating : 0.07 max weight: 16 488 +Unsatisfiable/GRP597-1.ma ... OK TIME NEEDED: 0.62 Rating : 0.00 max weight: 20 489 +Unsatisfiable/GRP598-1.ma ... OK TIME NEEDED: 0.28 Rating : 0.07 max weight: 20 490 +Unsatisfiable/GRP599-1.ma ... OK TIME NEEDED: 2.33 Rating : 0.07 max weight: 21 491 +Unsatisfiable/GRP600-1.ma ... OK TIME NEEDED: 0.36 Rating : 0.07 max weight: 21 492 +Unsatisfiable/GRP601-1.ma ... OK TIME NEEDED: 3.56 Rating : 0.07 max weight: 15 493 +Unsatisfiable/GRP602-1.ma ... OK TIME NEEDED: 0.44 Rating : 0.07 max weight: 16 494 +Unsatisfiable/GRP603-1.ma ... OK TIME NEEDED: 0.56 Rating : 0.07 max weight: 16 495 +Unsatisfiable/GRP604-1.ma ... OK TIME NEEDED: 0.77 Rating : 0.07 max weight: 15 496 +Unsatisfiable/GRP605-1.ma ... OK TIME NEEDED: 1.75 Rating : 0.00 max weight: 19 497 +Unsatisfiable/GRP606-1.ma ... OK TIME NEEDED: 1.62 Rating : 0.00 max weight: 19 498 +Unsatisfiable/GRP607-1.ma ... FAIL Rating : 0.00 499 +Unsatisfiable/GRP608-1.ma ... OK TIME NEEDED: 2.11 Rating : 0.00 max weight: 22 500 +Unsatisfiable/GRP609-1.ma ... OK TIME NEEDED: 2.03 Rating : 0.07 max weight: 15 501 +Unsatisfiable/GRP610-1.ma ... OK TIME NEEDED: 0.50 Rating : 0.07 max weight: 15 502 +Unsatisfiable/GRP611-1.ma ... OK TIME NEEDED: 0.24 Rating : 0.00 max weight: 16 503 +Unsatisfiable/GRP612-1.ma ... OK TIME NEEDED: 0.32 Rating : 0.07 max weight: 16 504 +Unsatisfiable/GRP613-1.ma ... OK TIME NEEDED: 0.78 Rating : 0.00 max weight: 20 505 +Unsatisfiable/GRP614-1.ma ... OK TIME NEEDED: 0.30 Rating : 0.00 max weight: 20 506 +Unsatisfiable/GRP615-1.ma ... OK TIME NEEDED: 1.73 Rating : 0.07 max weight: 21 507 +Unsatisfiable/GRP616-1.ma ... OK TIME NEEDED: 0.32 Rating : 0.00 max weight: 21 508 +Unsatisfiable/LAT006-1.ma ... OK TIME NEEDED: 38.21 Rating : 0.14 max weight: 20 509 +Unsatisfiable/LAT007-1.ma ... OK TIME NEEDED: 97.83 Rating : 0.36 max weight: 19 510 +Unsatisfiable/LAT008-1.ma ... OK TIME NEEDED: 0.82 Rating : 0.07 max weight: 12 511 +Unsatisfiable/LAT009-1.ma ... OK TIME NEEDED: 341.28 Rating : 0.00 max weight: 23 512 +Unsatisfiable/LAT010-1.ma ... FAIL Rating : 0.00 513 +Unsatisfiable/LAT011-1.ma ... FAIL Rating : 0.07 514 +Unsatisfiable/LAT012-1.ma ... OK TIME NEEDED: 4.82 Rating : 0.00 max weight: 14 515 +Unsatisfiable/LAT013-1.ma ... OK TIME NEEDED: 90.79 Rating : 0.14 max weight: 18 516 +Unsatisfiable/LAT014-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 6 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: 20.28 Rating : 0.14 max weight: 16 525 +Unsatisfiable/LAT027-1.ma ... OK TIME NEEDED: 13.64 Rating : 0.07 max weight: 16 526 +Unsatisfiable/LAT028-1.ma ... OK TIME NEEDED: 17.73 Rating : 0.00 max weight: 12 527 +Unsatisfiable/LAT031-1.ma ... OK TIME NEEDED: 0.99 Rating : 0.00 max weight: 9 528 +Unsatisfiable/LAT032-1.ma ... OK TIME NEEDED: 27.63 Rating : 0.00 max weight: 9 529 +Unsatisfiable/LAT033-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 3 530 +Unsatisfiable/LAT034-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 3 531 +Unsatisfiable/LAT038-1.ma ... FAIL Rating : 0.43 532 +Unsatisfiable/LAT039-1.ma ... OK TIME NEEDED: 0.07 Rating : 0.00 max weight: 6 533 +Unsatisfiable/LAT039-2.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 0 534 +Unsatisfiable/LAT040-1.ma ... OK TIME NEEDED: 36.21 Rating : 0.00 max weight: 11 535 +Unsatisfiable/LAT042-1.ma ... OK TIME NEEDED: 1.93 Rating : 0.00 max weight: 9 536 +Unsatisfiable/LAT043-1.ma ... OK TIME NEEDED: 158.67 Rating : 0.00 max weight: 18 537 +Unsatisfiable/LAT044-1.ma ... FAIL Rating : 0.14 538 +Unsatisfiable/LAT045-1.ma ... OK TIME NEEDED: 0.17 Rating : 0.07 max weight: 18 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 ... OK TIME NEEDED: 84.86 Rating : 0.36 max weight: 1061 548 +Unsatisfiable/LAT081-1.ma ... FAIL Rating : 0.57 549 +Unsatisfiable/LAT082-1.ma ... FAIL Rating : 0.64 550 +Unsatisfiable/LAT083-1.ma ... OK TIME NEEDED: 89.00 Rating : 0.36 max weight: 1061 551 +Unsatisfiable/LAT084-1.ma ... FAIL Rating : 0.50 552 +Unsatisfiable/LAT085-1.ma ... FAIL Rating : 0.57 553 +Unsatisfiable/LAT086-1.ma ... OK TIME NEEDED: 573.47 Rating : 0.50 max weight: 1060 554 +Unsatisfiable/LAT087-1.ma ... OK TIME NEEDED: 588.84 Rating : 0.43 max weight: 1060 555 +Unsatisfiable/LAT088-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 16 556 +Unsatisfiable/LAT089-1.ma ... OK TIME NEEDED: 1.68 Rating : 0.00 max weight: 16 557 +Unsatisfiable/LAT090-1.ma ... OK TIME NEEDED: 0.14 Rating : 0.00 max weight: 16 558 +Unsatisfiable/LAT091-1.ma ... OK TIME NEEDED: 16.44 Rating : 0.07 max weight: 21 559 +Unsatisfiable/LAT092-1.ma ... OK TIME NEEDED: 82.68 Rating : 0.36 max weight: 991 560 +Unsatisfiable/LAT093-1.ma ... OK TIME NEEDED: 320.09 Rating : 0.43 max weight: 991 561 +Unsatisfiable/LAT094-1.ma ... OK TIME NEEDED: 97.53 Rating : 0.36 max weight: 991 562 +Unsatisfiable/LAT095-1.ma ... OK TIME NEEDED: 474.76 Rating : 0.43 max weight: 991 563 +Unsatisfiable/LAT096-1.ma ... OK TIME NEEDED: 162.98 Rating : 0.36 max weight: 990 564 +Unsatisfiable/LAT097-1.ma ... OK TIME NEEDED: 115.99 Rating : 0.36 max weight: 990 565 +Unsatisfiable/LAT138-1.ma ... FAIL Rating : 1.00 1 +Unsatisfiable/LAT139-1.ma ... FAIL Rating : 1.00 2 +Unsatisfiable/LAT140-1.ma ... FAIL Rating : 1.00 3 +Unsatisfiable/LAT141-1.ma ... FAIL Rating : 1.00 4 +Unsatisfiable/LAT142-1.ma ... FAIL Rating : 0.64 5 +Unsatisfiable/LAT143-1.ma ... FAIL Rating : 0.14 6 +Unsatisfiable/LAT144-1.ma ... FAIL Rating : 0.86 7 +Unsatisfiable/LAT145-1.ma ... FAIL Rating : 0.93 8 +Unsatisfiable/LAT146-1.ma ... FAIL Rating : 0.79 9 +Unsatisfiable/LAT147-1.ma ... FAIL Rating : 0.79 10 +Unsatisfiable/LAT148-1.ma ... FAIL Rating : 0.71 11 +Unsatisfiable/LAT149-1.ma ... FAIL Rating : 0.93 12 +Unsatisfiable/LAT150-1.ma ... FAIL Rating : 0.86 13 +Unsatisfiable/LAT151-1.ma ... FAIL Rating : 0.86 14 +Unsatisfiable/LAT152-1.ma ... FAIL Rating : 0.79 15 +Unsatisfiable/LAT153-1.ma ... FAIL Rating : 0.93 16 +Unsatisfiable/LAT154-1.ma ... FAIL Rating : 0.79 17 +Unsatisfiable/LAT155-1.ma ... FAIL Rating : 0.86 18 +Unsatisfiable/LAT156-1.ma ... FAIL Rating : 0.64 19 +Unsatisfiable/LAT157-1.ma ... FAIL Rating : 0.86 20 +Unsatisfiable/LAT158-1.ma ... FAIL Rating : 0.93 21 +Unsatisfiable/LAT159-1.ma ... FAIL Rating : 0.86 22 +Unsatisfiable/LAT160-1.ma ... FAIL Rating : 0.64 23 +Unsatisfiable/LAT161-1.ma ... FAIL Rating : 1.00 24 +Unsatisfiable/LAT162-1.ma ... FAIL Rating : 0.86 25 +Unsatisfiable/LAT163-1.ma ... FAIL Rating : 0.93 26 +Unsatisfiable/LAT164-1.ma ... FAIL Rating : 0.93 27 +Unsatisfiable/LAT165-1.ma ... FAIL Rating : 0.93 28 +Unsatisfiable/LAT166-1.ma ... FAIL Rating : 0.93 29 +Unsatisfiable/LAT167-1.ma ... FAIL Rating : 0.93 30 +Unsatisfiable/LAT168-1.ma ... OK TIME NEEDED: 190.30 Rating : 0.14 max weight: 16 31 +Unsatisfiable/LAT169-1.ma ... FAIL Rating : 0.86 32 +Unsatisfiable/LAT170-1.ma ... FAIL Rating : 0.79 33 +Unsatisfiable/LAT171-1.ma ... OK TIME NEEDED: 250.07 Rating : 0.50 max weight: 16 34 +Unsatisfiable/LAT172-1.ma ... FAIL Rating : 0.93 35 +Unsatisfiable/LAT173-1.ma ... FAIL Rating : 0.93 36 +Unsatisfiable/LAT174-1.ma ... FAIL Rating : 0.79 37 +Unsatisfiable/LAT175-1.ma ... FAIL Rating : 0.93 38 +Unsatisfiable/LAT176-1.ma ... FAIL Rating : 0.93 39 +Unsatisfiable/LAT177-1.ma ... FAIL Rating : 1.00 40 +Unsatisfiable/LCL109-2.ma ... FAIL Rating : 0.29 41 +Unsatisfiable/LCL109-6.ma ... FAIL Rating : 0.14 42 +Unsatisfiable/LCL110-2.ma ... OK TIME NEEDED: 1.67 Rating : 0.00 max weight: 12 43 +Unsatisfiable/LCL111-2.ma ... OK TIME NEEDED: 5.31 Rating : 0.07 max weight: 17 44 +Unsatisfiable/LCL112-2.ma ... OK TIME NEEDED: 1.81 Rating : 0.00 max weight: 14 45 +Unsatisfiable/LCL113-2.ma ... OK TIME NEEDED: 1.39 Rating : 0.00 max weight: 12 46 +Unsatisfiable/LCL114-2.ma ... OK TIME NEEDED: 1.90 Rating : 0.00 max weight: 12 47 +Unsatisfiable/LCL115-2.ma ... OK TIME NEEDED: 1.41 Rating : 0.00 max weight: 13 48 +Unsatisfiable/LCL116-2.ma ... OK TIME NEEDED: 5.72 Rating : 0.00 max weight: 13 49 +Unsatisfiable/LCL132-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 max weight: 9 50 +Unsatisfiable/LCL133-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 max weight: 11 51 +Unsatisfiable/LCL134-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 9 52 +Unsatisfiable/LCL135-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 max weight: 9 53 +Unsatisfiable/LCL138-1.ma ... FAIL Rating : 0.21 54 +Unsatisfiable/LCL139-1.ma ... OK TIME NEEDED: 1.81 Rating : 0.00 max weight: 12 55 +Unsatisfiable/LCL140-1.ma ... OK TIME NEEDED: 1.45 Rating : 0.00 max weight: 14 56 +Unsatisfiable/LCL141-1.ma ... OK TIME NEEDED: 2.09 Rating : 0.00 max weight: 14 57 +Unsatisfiable/LCL153-1.ma ... OK TIME NEEDED: 1.36 Rating : 0.00 max weight: 10 58 +Unsatisfiable/LCL154-1.ma ... OK TIME NEEDED: 10.65 Rating : 0.00 max weight: 12 59 +Unsatisfiable/LCL155-1.ma ... OK TIME NEEDED: 0.14 Rating : 0.00 max weight: 12 60 +Unsatisfiable/LCL156-1.ma ... OK TIME NEEDED: 1.38 Rating : 0.00 max weight: 11 61 +Unsatisfiable/LCL157-1.ma ... OK TIME NEEDED: 1.13 Rating : 0.00 max weight: 12 62 +Unsatisfiable/LCL158-1.ma ... OK TIME NEEDED: 1.87 Rating : 0.00 max weight: 15 63 +Unsatisfiable/LCL159-1.ma ... OK TIME NEEDED: 131.67 Rating : 0.00 max weight: 16 64 +Unsatisfiable/LCL160-1.ma ... FAIL Rating : 0.14 65 +Unsatisfiable/LCL161-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 max weight: 9 66 +Unsatisfiable/LCL162-1.ma ... FAIL Rating : 0.00 67 +Unsatisfiable/LCL163-1.ma ... OK TIME NEEDED: 10.10 Rating : 0.14 max weight: 34 68 +Unsatisfiable/LCL164-1.ma ... OK TIME NEEDED: 0.15 Rating : 0.00 max weight: 12 69 +Unsatisfiable/LDA001-1.ma ... OK TIME NEEDED: 0.13 Rating : 0.00 max weight: 7 70 +Unsatisfiable/LDA002-1.ma ... OK TIME NEEDED: 22.30 Rating : 0.00 max weight: 11 71 +Unsatisfiable/LDA007-3.ma ... OK TIME NEEDED: 0.08 Rating : 0.00 max weight: 8 72 +Unsatisfiable/RNG007-4.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 max weight: 7 73 +Unsatisfiable/RNG008-3.ma ... OK TIME NEEDED: 17.75 Rating : 0.07 max weight: 17 74 +Unsatisfiable/RNG008-4.ma ... OK TIME NEEDED: 18.52 Rating : 0.07 max weight: 17 75 +Unsatisfiable/RNG008-7.ma ... OK TIME NEEDED: 47.63 Rating : 0.07 max weight: 22 76 +Unsatisfiable/RNG009-5.ma ... FAIL Rating : 0.50 77 +Unsatisfiable/RNG009-7.ma ... FAIL Rating : 0.50 78 +Unsatisfiable/RNG011-5.ma ... OK TIME NEEDED: 0.14 Rating : 0.00 max weight: 0 79 +Unsatisfiable/RNG012-6.ma ... OK TIME NEEDED: 114.29 Rating : 0.00 max weight: 12 80 +Unsatisfiable/RNG013-6.ma ... OK TIME NEEDED: 132.92 Rating : 0.00 max weight: 12 81 +Unsatisfiable/RNG014-6.ma ... OK TIME NEEDED: 145.08 Rating : 0.00 max weight: 12 82 +Unsatisfiable/RNG015-6.ma ... OK TIME NEEDED: 127.35 Rating : 0.00 max weight: 11 83 +Unsatisfiable/RNG016-6.ma ... OK TIME NEEDED: 133.38 Rating : 0.00 max weight: 11 84 +Unsatisfiable/RNG017-6.ma ... OK TIME NEEDED: 120.96 Rating : 0.00 max weight: 11 85 +Unsatisfiable/RNG018-6.ma ... OK TIME NEEDED: 116.44 Rating : 0.00 max weight: 11 86 +Unsatisfiable/RNG019-6.ma ... FAIL Rating : 0.21 87 +Unsatisfiable/RNG019-7.ma ... FAIL Rating : 0.21 88 +Unsatisfiable/RNG020-6.ma ... FAIL Rating : 0.29 89 +Unsatisfiable/RNG020-7.ma ... FAIL Rating : 0.21 90 +Unsatisfiable/RNG021-6.ma ... FAIL Rating : 0.14 91 +Unsatisfiable/RNG021-7.ma ... FAIL Rating : 0.21 92 +Unsatisfiable/RNG023-6.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 max weight: 15 93 +Unsatisfiable/RNG023-7.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 max weight: 15 94 +Unsatisfiable/RNG024-6.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 max weight: 15 95 +Unsatisfiable/RNG024-7.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 max weight: 15 96 +Unsatisfiable/RNG025-4.ma ... FAIL Rating : 0.29 97 +Unsatisfiable/RNG025-5.ma ... FAIL Rating : 0.36 98 +Unsatisfiable/RNG025-6.ma ... FAIL Rating : 0.29 99 +Unsatisfiable/RNG025-7.ma ... FAIL Rating : 0.43 100 +Unsatisfiable/RNG026-6.ma ... FAIL Rating : 0.57 101 +Unsatisfiable/RNG026-7.ma ... FAIL Rating : 0.50 102 +Unsatisfiable/RNG027-5.ma ... FAIL Rating : 0.86 103 +Unsatisfiable/RNG027-7.ma ... FAIL Rating : 0.86 104 +Unsatisfiable/RNG027-8.ma ... FAIL Rating : 0.86 105 +Unsatisfiable/RNG027-9.ma ... FAIL Rating : 0.86 106 +Unsatisfiable/RNG028-5.ma ... FAIL Rating : 0.86 107 +Unsatisfiable/RNG028-7.ma ... FAIL Rating : 0.86 108 +Unsatisfiable/RNG028-8.ma ... FAIL Rating : 0.86 109 +Unsatisfiable/RNG028-9.ma ... FAIL Rating : 0.86 110 +Unsatisfiable/RNG029-5.ma ... FAIL Rating : 0.86 111 +Unsatisfiable/RNG029-6.ma ... FAIL Rating : 0.86 112 +Unsatisfiable/RNG029-7.ma ... FAIL Rating : 0.86 113 +Unsatisfiable/RNG035-7.ma ... FAIL Rating : 0.86 114 +Unsatisfiable/ROB001-1.ma ... FAIL Rating : 1.00 115 +Unsatisfiable/ROB002-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 max weight: 10 116 +Unsatisfiable/ROB003-1.ma ... OK TIME NEEDED: 0.72 Rating : 0.00 max weight: 17 117 +Unsatisfiable/ROB004-1.ma ... OK TIME NEEDED: 66.26 Rating : 0.00 max weight: 22 118 +Unsatisfiable/ROB005-1.ma ... FAIL Rating : 0.07 119 +Unsatisfiable/ROB006-1.ma ... FAIL Rating : 0.86 120 +Unsatisfiable/ROB006-2.ma ... FAIL Rating : 0.86 121 +Unsatisfiable/ROB008-1.ma ... OK TIME NEEDED: 80.62 Rating : 0.00 max weight: 17 122 +Unsatisfiable/ROB009-1.ma ... OK TIME NEEDED: 0.07 Rating : 0.00 max weight: 18 123 +Unsatisfiable/ROB010-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 max weight: 7 124 +Unsatisfiable/ROB013-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 max weight: 8 125 +Unsatisfiable/ROB022-1.ma ... FAIL Rating : 0.00 126 +Unsatisfiable/ROB023-1.ma ... FAIL Rating : 0.00 127 +Unsatisfiable/ROB026-1.ma ... FAIL Rating : 0.86 128 +Unsatisfiable/ROB030-1.ma ... OK TIME NEEDED: 0.44 Rating : 0.00 max weight: 5 129 +Unsatisfiable/ROB031-1.ma ... FAIL Rating : 1.00 130 +Unsatisfiable/ROB032-1.ma ... FAIL Rating : 1.00 131 +Unsatisfiable/SYN080-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 132 +Unsatisfiable/SYN083-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 max weight: 0 133