From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 16 Jun 2006 09:03:24 +0000 (+0000)
Subject: added log.120.orsay.txt and comparison
X-Git-Tag: 0.4.95@7852~1310
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0729078e9768a1b66ad92b22b687fbd611415d3f;p=helm.git

added log.120.orsay.txt and comparison
---

diff --git a/matita/tests/TPTP/log.120.orsay.txt b/matita/tests/TPTP/log.120.orsay.txt
new file mode 100644
index 000000000..2bf838a67
--- /dev/null
+++ b/matita/tests/TPTP/log.120.orsay.txt
@@ -0,0 +1,698 @@
+Unsatisfiable/ALG005-1.ma ... OK TIME NEEDED: 31.22 Rating : 0.07 1
+Unsatisfiable/ALG006-1.ma ... OK TIME NEEDED: 2.24 Rating : 0.00 2
+Unsatisfiable/ALG007-1.ma ... OK TIME NEEDED: 3.39 Rating : 0.00 3
+Unsatisfiable/BOO001-1.ma ... OK TIME NEEDED: 0.98 Rating : 0.00 4
+Unsatisfiable/BOO002-1.ma ... OK TIME NEEDED: 9.58 Rating : 0.07 5
+Unsatisfiable/BOO002-2.ma ... OK TIME NEEDED: 6.35 Rating : 0.00 6
+Unsatisfiable/BOO003-2.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 7
+Unsatisfiable/BOO003-4.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 8
+Unsatisfiable/BOO004-2.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 9
+Unsatisfiable/BOO004-4.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 10
+Unsatisfiable/BOO005-2.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 11
+Unsatisfiable/BOO005-4.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 12
+Unsatisfiable/BOO006-2.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 13
+Unsatisfiable/BOO006-4.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 14
+Unsatisfiable/BOO007-2.ma ... FAIL Rating : 0.14 15
+Unsatisfiable/BOO007-4.ma ... OK TIME NEEDED: 63.00 Rating : 0.07 16
+Unsatisfiable/BOO008-2.ma ... FAIL Rating : 0.07 17
+Unsatisfiable/BOO008-4.ma ... OK TIME NEEDED: 23.48 Rating : 0.00 18
+Unsatisfiable/BOO009-2.ma ... OK TIME NEEDED: 0.17 Rating : 0.00 19
+Unsatisfiable/BOO009-4.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 20
+Unsatisfiable/BOO010-2.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 21
+Unsatisfiable/BOO010-4.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 22
+Unsatisfiable/BOO011-2.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 23
+Unsatisfiable/BOO011-4.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 24
+Unsatisfiable/BOO012-2.ma ... OK TIME NEEDED: 0.26 Rating : 0.00 25
+Unsatisfiable/BOO012-4.ma ... OK TIME NEEDED: 0.35 Rating : 0.00 26
+Unsatisfiable/BOO013-2.ma ... OK TIME NEEDED: 0.31 Rating : 0.00 27
+Unsatisfiable/BOO013-4.ma ... OK TIME NEEDED: 0.55 Rating : 0.00 28
+Unsatisfiable/BOO014-2.ma ... OK TIME NEEDED: 3.38 Rating : 0.00 29
+Unsatisfiable/BOO014-4.ma ... OK TIME NEEDED: 16.30 Rating : 0.00 30
+Unsatisfiable/BOO015-2.ma ... OK TIME NEEDED: 1.98 Rating : 0.00 31
+Unsatisfiable/BOO015-4.ma ... OK TIME NEEDED: 16.72 Rating : 0.00 32
+Unsatisfiable/BOO016-2.ma ... OK TIME NEEDED: 0.23 Rating : 0.00 33
+Unsatisfiable/BOO017-2.ma ... OK TIME NEEDED: 0.51 Rating : 0.00 34
+Unsatisfiable/BOO018-4.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 35
+Unsatisfiable/BOO021-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.07 36
+Unsatisfiable/BOO022-1.ma ... FAIL Rating : 0.07 37
+Unsatisfiable/BOO023-1.ma ... FAIL Rating : 0.50 38
+Unsatisfiable/BOO024-1.ma ... OK TIME NEEDED: 2.11 Rating : 0.00 39
+Unsatisfiable/BOO025-1.ma ... OK TIME NEEDED: 4.28 Rating : 0.07 40
+Unsatisfiable/BOO026-1.ma ... OK Rating : 0.07 41
+Unsatisfiable/BOO028-1.ma ... FAIL Rating : 0.07 42
+Unsatisfiable/BOO029-1.ma ... OK TIME NEEDED: 85.32 Rating : 0.00 43
+Unsatisfiable/BOO031-1.ma ... FAIL Rating : 0.21 44
+Unsatisfiable/BOO034-1.ma ... OK TIME NEEDED: 16.86 Rating : 0.21 45
+Unsatisfiable/BOO067-1.ma ... FAIL Rating : 0.21 46
+Unsatisfiable/BOO068-1.ma ... OK TIME NEEDED: 1.54 Rating : 0.00 47
+Unsatisfiable/BOO069-1.ma ... OK TIME NEEDED: 0.82 Rating : 0.00 48
+Unsatisfiable/BOO070-1.ma ... OK TIME NEEDED: 1.74 Rating : 0.00 49
+Unsatisfiable/BOO071-1.ma ... OK TIME NEEDED: 0.82 Rating : 0.00 50
+Unsatisfiable/BOO072-1.ma ... FAIL Rating : 0.07 51
+Unsatisfiable/BOO073-1.ma ... FAIL Rating : 0.36 52
+Unsatisfiable/BOO074-1.ma ... FAIL Rating : 0.07 53
+Unsatisfiable/BOO075-1.ma ... OK TIME NEEDED: 0.61 Rating : 0.00 54
+Unsatisfiable/BOO076-1.ma ... FAIL Rating : 0.71 55
+Unsatisfiable/COL001-1.ma ... OK TIME NEEDED: 79.85 Rating : 0.07 56
+Unsatisfiable/COL001-2.ma ... OK TIME NEEDED: 5.70 Rating : 0.07 57
+Unsatisfiable/COL002-1.ma ... OK TIME NEEDED: 2.99 Rating : 0.00 58
+Unsatisfiable/COL002-4.ma ... FAIL Rating : 0.07 59
+Unsatisfiable/COL002-5.ma ... FAIL Rating : 0.43 60
+Unsatisfiable/COL003-1.ma ... FAIL Rating : 0.79 61
+Unsatisfiable/COL004-1.ma ... FAIL Rating : 0.57 62
+Unsatisfiable/COL004-3.ma ... OK TIME NEEDED: 0.01 Rating : 0.21 63
+Unsatisfiable/COL006-1.ma ... FAIL Rating : 0.57 64
+Unsatisfiable/COL006-5.ma ... FAIL Rating : 0.64 65
+Unsatisfiable/COL006-6.ma ... FAIL Rating : 0.64 66
+Unsatisfiable/COL006-7.ma ... FAIL Rating : 0.64 67
+Unsatisfiable/COL007-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 68
+Unsatisfiable/COL008-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 69
+Unsatisfiable/COL009-1.ma ... OK TIME NEEDED: 5.59 Rating : 0.07 70
+Unsatisfiable/COL010-1.ma ... OK TIME NEEDED: 1.01 Rating : 0.07 71
+Unsatisfiable/COL011-1.ma ... FAIL Rating : 0.36 72
+Unsatisfiable/COL012-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 73
+Unsatisfiable/COL013-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 74
+Unsatisfiable/COL014-1.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 75
+Unsatisfiable/COL015-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 76
+Unsatisfiable/COL016-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 77
+Unsatisfiable/COL017-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 78
+Unsatisfiable/COL018-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 79
+Unsatisfiable/COL019-1.ma ... FAIL Rating : 0.00 80
+Unsatisfiable/COL020-1.ma ... FAIL Rating : 0.07 81
+Unsatisfiable/COL021-1.ma ... OK TIME NEEDED: 0.28 Rating : 0.00 82
+Unsatisfiable/COL022-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 83
+Unsatisfiable/COL023-1.ma ... FAIL Rating : 0.00 84
+Unsatisfiable/COL024-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 85
+Unsatisfiable/COL025-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 86
+Unsatisfiable/COL026-1.ma ... FAIL Rating : 0.07 87
+Unsatisfiable/COL027-1.ma ... FAIL Rating : 0.00 88
+Unsatisfiable/COL029-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 89
+Unsatisfiable/COL030-1.ma ... OK TIME NEEDED: 0.26 Rating : 0.14 90
+Unsatisfiable/COL031-1.ma ... OK TIME NEEDED: 0.12 Rating : 0.00 91
+Unsatisfiable/COL032-1.ma ... FAIL Rating : 0.14 92
+Unsatisfiable/COL033-1.ma ... FAIL Rating : 0.07 93
+Unsatisfiable/COL034-1.ma ... FAIL Rating : 0.43 94
+Unsatisfiable/COL035-1.ma ... FAIL Rating : 0.14 95
+Unsatisfiable/COL036-1.ma ... FAIL Rating : 0.57 96
+Unsatisfiable/COL037-1.ma ... FAIL Rating : 0.29 97
+Unsatisfiable/COL038-1.ma ... FAIL Rating : 0.64 98
+Unsatisfiable/COL039-1.ma ... FAIL Rating : 0.00 99
+Unsatisfiable/COL041-1.ma ... FAIL Rating : 0.36 100
+Unsatisfiable/COL042-1.ma ... FAIL Rating : 0.86 101
+Unsatisfiable/COL042-6.ma ... FAIL Rating : 0.14 102
+Unsatisfiable/COL042-7.ma ... FAIL Rating : 0.14 103
+Unsatisfiable/COL042-8.ma ... FAIL Rating : 0.14 104
+Unsatisfiable/COL042-9.ma ... FAIL Rating : 0.14 105
+Unsatisfiable/COL043-1.ma ... FAIL Rating : 0.86 106
+Unsatisfiable/COL043-3.ma ... FAIL Rating : 0.71 107
+Unsatisfiable/COL044-1.ma ... FAIL Rating : 0.21 108
+Unsatisfiable/COL044-6.ma ... FAIL Rating : 0.64 109
+Unsatisfiable/COL044-7.ma ... FAIL Rating : 0.50 110
+Unsatisfiable/COL044-8.ma ... FAIL Rating : 0.71 111
+Unsatisfiable/COL044-9.ma ... FAIL Rating : 0.64 112
+Unsatisfiable/COL045-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 113
+Unsatisfiable/COL046-1.ma ... FAIL Rating : 0.64 114
+Unsatisfiable/COL048-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 115
+Unsatisfiable/COL049-1.ma ... FAIL Rating : 0.29 116
+Unsatisfiable/COL050-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 117
+Unsatisfiable/COL051-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 118
+Unsatisfiable/COL052-1.ma ... FAIL Rating : 0.00 119
+Unsatisfiable/COL053-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 120
+Unsatisfiable/COL056-1.ma ... FAIL Rating : 0.07 121
+Unsatisfiable/COL057-1.ma ... FAIL Rating : 0.36 122
+Unsatisfiable/COL058-1.ma ... FAIL Rating : 0.00 123
+Unsatisfiable/COL058-2.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 124
+Unsatisfiable/COL058-3.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 125
+Unsatisfiable/COL059-1.ma ... FAIL Rating : 0.00 126
+Unsatisfiable/COL060-1.ma ... FAIL Rating : 0.36 127
+Unsatisfiable/COL060-2.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 128
+Unsatisfiable/COL060-3.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 129
+Unsatisfiable/COL061-1.ma ... FAIL Rating : 0.36 130
+Unsatisfiable/COL061-2.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 131
+Unsatisfiable/COL061-3.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 132
+Unsatisfiable/COL062-1.ma ... FAIL Rating : 0.50 133
+Unsatisfiable/COL062-2.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 134
+Unsatisfiable/COL062-3.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 135
+Unsatisfiable/COL063-1.ma ... FAIL Rating : 0.50 136
+Unsatisfiable/COL063-2.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 137
+Unsatisfiable/COL063-3.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 138
+Unsatisfiable/COL063-4.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 139
+Unsatisfiable/COL063-5.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 140
+Unsatisfiable/COL063-6.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 141
+Unsatisfiable/COL064-1.ma ... FAIL Rating : 0.64 142
+Unsatisfiable/COL064-2.ma ... OK TIME NEEDED: 0.00 Rating : 0.07 143
+Unsatisfiable/COL064-3.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 144
+Unsatisfiable/COL064-4.ma ... OK TIME NEEDED: 0.00 Rating : 0.07 145
+Unsatisfiable/COL064-5.ma ... OK TIME NEEDED: 0.00 Rating : 0.07 146
+Unsatisfiable/COL064-6.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 147
+Unsatisfiable/COL064-7.ma ... OK TIME NEEDED: 0.00 Rating : 0.07 148
+Unsatisfiable/COL064-8.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 149
+Unsatisfiable/COL064-9.ma ... OK TIME NEEDED: 0.00 Rating : 0.07 150
+Unsatisfiable/COL065-1.ma ... FAIL Rating : 0.71 151
+Unsatisfiable/COL066-1.ma ... FAIL Rating : 0.93 152
+Unsatisfiable/COL066-2.ma ... OK TIME NEEDED: 1.31 Rating : 0.00 153
+Unsatisfiable/COL066-3.ma ... OK TIME NEEDED: 1.31 Rating : 0.00 154
+Unsatisfiable/COL070-1.ma ... FAIL Rating : 0.07 155
+Unsatisfiable/COL075-2.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 156
+Unsatisfiable/COL083-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 157
+Unsatisfiable/COL084-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 158
+Unsatisfiable/COL085-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 159
+Unsatisfiable/COL086-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 160
+Unsatisfiable/GRP001-2.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 161
+Unsatisfiable/GRP001-4.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 162
+Unsatisfiable/GRP002-2.ma ... OK TIME NEEDED: 7.77 Rating : 0.00 163
+Unsatisfiable/GRP002-3.ma ... OK TIME NEEDED: 13.93 Rating : 0.00 164
+Unsatisfiable/GRP002-4.ma ... OK TIME NEEDED: 12.69 Rating : 0.00 165
+Unsatisfiable/GRP010-4.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 166
+Unsatisfiable/GRP011-4.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 167
+Unsatisfiable/GRP012-4.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 168
+Unsatisfiable/GRP014-1.ma ... FAIL Rating : 0.14 169
+Unsatisfiable/GRP022-2.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 170
+Unsatisfiable/GRP023-2.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 171
+Unsatisfiable/GRP024-5.ma ... FAIL Rating : 0.50 172
+Unsatisfiable/GRP114-1.ma ... OK TIME NEEDED: 8.76 Rating : 0.29 173
+Unsatisfiable/GRP115-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 174
+Unsatisfiable/GRP116-1.ma ... OK TIME NEEDED: 0.62 Rating : 0.00 175
+Unsatisfiable/GRP117-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 176
+Unsatisfiable/GRP118-1.ma ... OK TIME NEEDED: 0.40 Rating : 0.00 177
+Unsatisfiable/GRP119-1.ma ... OK TIME NEEDED: 37.45 Rating : 0.00 178
+Unsatisfiable/GRP120-1.ma ... OK TIME NEEDED: 54.47 Rating : 0.00 179
+Unsatisfiable/GRP121-1.ma ... OK TIME NEEDED: 37.92 Rating : 0.00 180
+Unsatisfiable/GRP122-1.ma ... OK Rating : 0.07 181
+Unsatisfiable/GRP136-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 182
+Unsatisfiable/GRP137-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 183
+Unsatisfiable/GRP138-1.ma ... OK TIME NEEDED: 1.85 Rating : 0.00 184
+Unsatisfiable/GRP139-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 185
+Unsatisfiable/GRP140-1.ma ... OK TIME NEEDED: 2.00 Rating : 0.00 186
+Unsatisfiable/GRP141-1.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 187
+Unsatisfiable/GRP142-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 188
+Unsatisfiable/GRP143-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 189
+Unsatisfiable/GRP144-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 190
+Unsatisfiable/GRP145-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 191
+Unsatisfiable/GRP146-1.ma ... OK TIME NEEDED: 0.15 Rating : 0.00 192
+Unsatisfiable/GRP147-1.ma ... OK TIME NEEDED: 1.11 Rating : 0.00 193
+Unsatisfiable/GRP148-1.ma ... OK TIME NEEDED: 0.86 Rating : 0.00 194
+Unsatisfiable/GRP149-1.ma ... OK TIME NEEDED: 0.15 Rating : 0.00 195
+Unsatisfiable/GRP150-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 196
+Unsatisfiable/GRP151-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 197
+Unsatisfiable/GRP152-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 198
+Unsatisfiable/GRP153-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 199
+Unsatisfiable/GRP154-1.ma ... OK TIME NEEDED: 0.25 Rating : 0.00 200
+Unsatisfiable/GRP155-1.ma ... OK TIME NEEDED: 0.33 Rating : 0.00 201
+Unsatisfiable/GRP156-1.ma ... OK TIME NEEDED: 0.36 Rating : 0.00 202
+Unsatisfiable/GRP157-1.ma ... OK TIME NEEDED: 0.15 Rating : 0.00 203
+Unsatisfiable/GRP158-1.ma ... OK TIME NEEDED: 0.19 Rating : 0.00 204
+Unsatisfiable/GRP159-1.ma ... OK TIME NEEDED: 0.14 Rating : 0.00 205
+Unsatisfiable/GRP160-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 206
+Unsatisfiable/GRP161-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 207
+Unsatisfiable/GRP162-1.ma ... OK TIME NEEDED: 0.16 Rating : 0.00 208
+Unsatisfiable/GRP163-1.ma ... OK TIME NEEDED: 0.22 Rating : 0.00 209
+Unsatisfiable/GRP164-1.ma ... FAIL Rating : 0.93 210
+Unsatisfiable/GRP164-2.ma ... FAIL Rating : 0.93 211
+Unsatisfiable/GRP165-1.ma ... FAIL Rating : 0.00 212
+Unsatisfiable/GRP165-2.ma ... FAIL Rating : 0.00 213
+Unsatisfiable/GRP166-1.ma ... OK TIME NEEDED: 6.44 Rating : 0.00 214
+Unsatisfiable/GRP166-2.ma ... OK TIME NEEDED: 3.78 Rating : 0.00 215
+Unsatisfiable/GRP166-3.ma ... FAIL Rating : 0.00 216
+Unsatisfiable/GRP166-4.ma ... FAIL Rating : 0.00 217
+Unsatisfiable/GRP167-1.ma ... OK TIME NEEDED: 3.08 Rating : 0.21 218
+Unsatisfiable/GRP167-2.ma ... OK TIME NEEDED: 3.04 Rating : 0.21 219
+Unsatisfiable/GRP167-3.ma ... FAIL Rating : 0.50 220
+Unsatisfiable/GRP167-4.ma ... FAIL Rating : 0.43 221
+Unsatisfiable/GRP167-5.ma ... OK TIME NEEDED: 0.73 Rating : 0.14 222
+Unsatisfiable/GRP168-1.ma ... OK TIME NEEDED: 0.26 Rating : 0.07 223
+Unsatisfiable/GRP168-2.ma ... OK TIME NEEDED: 0.36 Rating : 0.07 224
+Unsatisfiable/GRP169-1.ma ... OK TIME NEEDED: 53.35 Rating : 0.00 225
+Unsatisfiable/GRP169-2.ma ... OK TIME NEEDED: 53.41 Rating : 0.00 226
+Unsatisfiable/GRP170-1.ma ... FAIL Rating : 0.00 227
+Unsatisfiable/GRP170-2.ma ... FAIL Rating : 0.00 228
+Unsatisfiable/GRP170-3.ma ... FAIL Rating : 0.00 229
+Unsatisfiable/GRP170-4.ma ... FAIL Rating : 0.00 230
+Unsatisfiable/GRP171-1.ma ... OK TIME NEEDED: 0.34 Rating : 0.00 231
+Unsatisfiable/GRP171-2.ma ... OK TIME NEEDED: 0.36 Rating : 0.00 232
+Unsatisfiable/GRP172-1.ma ... OK TIME NEEDED: 0.47 Rating : 0.00 233
+Unsatisfiable/GRP172-2.ma ... OK TIME NEEDED: 0.42 Rating : 0.00 234
+Unsatisfiable/GRP173-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 235
+Unsatisfiable/GRP174-1.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 236
+Unsatisfiable/GRP175-1.ma ... FAIL Rating : 0.00 237
+Unsatisfiable/GRP175-2.ma ... FAIL Rating : 0.00 238
+Unsatisfiable/GRP175-3.ma ... FAIL Rating : 0.00 239
+Unsatisfiable/GRP175-4.ma ... FAIL Rating : 0.00 240
+Unsatisfiable/GRP176-1.ma ... OK TIME NEEDED: 0.29 Rating : 0.00 241
+Unsatisfiable/GRP176-2.ma ... OK TIME NEEDED: 0.30 Rating : 0.00 242
+Unsatisfiable/GRP177-2.ma ... FAIL Rating : 0.21 243
+Unsatisfiable/GRP178-1.ma ... FAIL Rating : 0.14 244
+Unsatisfiable/GRP178-2.ma ... FAIL Rating : 0.14 245
+Unsatisfiable/GRP179-1.ma ... FAIL Rating : 0.50 246
+Unsatisfiable/GRP179-2.ma ... FAIL Rating : 0.50 247
+Unsatisfiable/GRP179-3.ma ... FAIL Rating : 0.36 248
+Unsatisfiable/GRP180-1.ma ... FAIL Rating : 0.50 249
+Unsatisfiable/GRP180-2.ma ... FAIL Rating : 0.43 250
+Unsatisfiable/GRP181-1.ma ... FAIL Rating : 0.71 251
+Unsatisfiable/GRP181-2.ma ... FAIL Rating : 0.71 252
+Unsatisfiable/GRP181-3.ma ... OK TIME NEEDED: 1.55 Rating : 0.43 253
+Unsatisfiable/GRP181-4.ma ... OK TIME NEEDED: 3.54 Rating : 0.43 254
+Unsatisfiable/GRP182-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 255
+Unsatisfiable/GRP182-2.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 256
+Unsatisfiable/GRP182-3.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 257
+Unsatisfiable/GRP182-4.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 258
+Unsatisfiable/GRP183-1.ma ... FAIL Rating : 0.43 259
+Unsatisfiable/GRP183-2.ma ... FAIL Rating : 0.43 260
+Unsatisfiable/GRP183-3.ma ... FAIL Rating : 0.43 261
+Unsatisfiable/GRP183-4.ma ... FAIL Rating : 0.36 262
+Unsatisfiable/GRP184-1.ma ... FAIL Rating : 0.29 263
+Unsatisfiable/GRP184-2.ma ... FAIL Rating : 0.14 264
+Unsatisfiable/GRP184-3.ma ... FAIL Rating : 0.21 265
+Unsatisfiable/GRP184-4.ma ... FAIL Rating : 0.00 266
+Unsatisfiable/GRP185-1.ma ... FAIL Rating : 0.07 267
+Unsatisfiable/GRP185-2.ma ... FAIL Rating : 0.07 268
+Unsatisfiable/GRP185-3.ma ... FAIL Rating : 0.21 269
+Unsatisfiable/GRP185-4.ma ... FAIL Rating : 0.21 270
+Unsatisfiable/GRP186-1.ma ... FAIL Rating : 0.57 271
+Unsatisfiable/GRP186-2.ma ... FAIL Rating : 0.36 272
+Unsatisfiable/GRP186-3.ma ... OK TIME NEEDED: 0.17 Rating : 0.00 273
+Unsatisfiable/GRP186-4.ma ... OK TIME NEEDED: 0.20 Rating : 0.00 274
+Unsatisfiable/GRP187-1.ma ... FAIL Rating : 0.64 275
+Unsatisfiable/GRP188-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 276
+Unsatisfiable/GRP188-2.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 277
+Unsatisfiable/GRP189-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 278
+Unsatisfiable/GRP189-2.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 279
+Unsatisfiable/GRP190-1.ma ... OK TIME NEEDED: 109.81 Rating : 0.00 280
+Unsatisfiable/GRP190-2.ma ... OK TIME NEEDED: 109.16 Rating : 0.00 281
+Unsatisfiable/GRP191-1.ma ... OK TIME NEEDED: 108.35 Rating : 0.00 282
+Unsatisfiable/GRP191-2.ma ... OK TIME NEEDED: 108.91 Rating : 0.00 283
+Unsatisfiable/GRP192-1.ma ... OK TIME NEEDED: 0.17 Rating : 0.07 284
+Unsatisfiable/GRP193-1.ma ... FAIL Rating : 0.00 285
+Unsatisfiable/GRP193-2.ma ... FAIL Rating : 0.00 286
+Unsatisfiable/GRP195-1.ma ... FAIL Rating : 0.00 287
+Unsatisfiable/GRP196-1.ma ... FAIL Rating : 0.93 288
+Unsatisfiable/GRP200-1.ma ... FAIL Rating : 0.29 289
+Unsatisfiable/GRP201-1.ma ... FAIL Rating : 0.36 290
+Unsatisfiable/GRP202-1.ma ... FAIL Rating : 0.43 291
+Unsatisfiable/GRP203-1.ma ... FAIL Rating : 0.21 292
+Unsatisfiable/GRP205-1.ma ... FAIL Rating : 0.43 293
+Unsatisfiable/GRP206-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 294
+Unsatisfiable/GRP403-1.ma ... OK TIME NEEDED: 48.77 Rating : 0.07 295
+Unsatisfiable/GRP404-1.ma ... FAIL Rating : 0.21 296
+Unsatisfiable/GRP405-1.ma ... FAIL Rating : 0.21 297
+Unsatisfiable/GRP406-1.ma ... FAIL Rating : 0.00 298
+Unsatisfiable/GRP407-1.ma ... FAIL Rating : 0.00 299
+Unsatisfiable/GRP408-1.ma ... FAIL Rating : 0.00 300
+Unsatisfiable/GRP409-1.ma ... OK TIME NEEDED: 7.50 Rating : 0.00 301
+Unsatisfiable/GRP410-1.ma ... OK TIME NEEDED: 12.23 Rating : 0.21 302
+Unsatisfiable/GRP411-1.ma ... OK TIME NEEDED: 13.76 Rating : 0.21 303
+Unsatisfiable/GRP412-1.ma ... OK TIME NEEDED: 105.80 Rating : 0.00 304
+Unsatisfiable/GRP413-1.ma ... FAIL Rating : 0.07 305
+Unsatisfiable/GRP414-1.ma ... FAIL Rating : 0.07 306
+Unsatisfiable/GRP415-1.ma ... FAIL Rating : 0.00 307
+Unsatisfiable/GRP416-1.ma ... FAIL Rating : 0.07 308
+Unsatisfiable/GRP417-1.ma ... FAIL Rating : 0.14 309
+Unsatisfiable/GRP418-1.ma ... FAIL Rating : 0.07 310
+Unsatisfiable/GRP419-1.ma ... FAIL Rating : 0.29 311
+Unsatisfiable/GRP420-1.ma ... FAIL Rating : 0.36 312
+Unsatisfiable/GRP421-1.ma ... FAIL Rating : 0.14 313
+Unsatisfiable/GRP422-1.ma ... FAIL Rating : 0.29 314
+Unsatisfiable/GRP423-1.ma ... FAIL Rating : 0.36 315
+Unsatisfiable/GRP424-1.ma ... OK TIME NEEDED: 20.70 Rating : 0.00 316
+Unsatisfiable/GRP425-1.ma ... OK TIME NEEDED: 21.22 Rating : 0.07 317
+Unsatisfiable/GRP426-1.ma ... FAIL Rating : 0.14 318
+Unsatisfiable/GRP427-1.ma ... FAIL Rating : 0.00 319
+Unsatisfiable/GRP428-1.ma ... FAIL Rating : 0.00 320
+Unsatisfiable/GRP429-1.ma ... FAIL Rating : 0.14 321
+Unsatisfiable/GRP430-1.ma ... OK TIME NEEDED: 32.43 Rating : 0.00 322
+Unsatisfiable/GRP431-1.ma ... OK TIME NEEDED: 29.82 Rating : 0.00 323
+Unsatisfiable/GRP432-1.ma ... OK TIME NEEDED: 35.35 Rating : 0.00 324
+Unsatisfiable/GRP433-1.ma ... FAIL Rating : 0.00 325
+Unsatisfiable/GRP434-1.ma ... FAIL Rating : 0.00 326
+Unsatisfiable/GRP435-1.ma ... FAIL Rating : 0.00 327
+Unsatisfiable/GRP436-1.ma ... OK Rating : 0.07 328
+Unsatisfiable/GRP437-1.ma ... OK Rating : 0.07 329
+Unsatisfiable/GRP438-1.ma ... OK Rating : 0.07 330
+Unsatisfiable/GRP439-1.ma ... OK TIME NEEDED: 33.82 Rating : 0.07 331
+Unsatisfiable/GRP440-1.ma ... FAIL Rating : 0.14 332
+Unsatisfiable/GRP441-1.ma ... FAIL Rating : 0.21 333
+Unsatisfiable/GRP442-1.ma ... FAIL Rating : 0.14 334
+Unsatisfiable/GRP443-1.ma ... FAIL Rating : 0.07 335
+Unsatisfiable/GRP444-1.ma ... FAIL Rating : 0.21 336
+Unsatisfiable/GRP445-1.ma ... OK TIME NEEDED: 0.20 Rating : 0.00 337
+Unsatisfiable/GRP446-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 338
+Unsatisfiable/GRP447-1.ma ... OK TIME NEEDED: 0.91 Rating : 0.14 339
+Unsatisfiable/GRP448-1.ma ... OK TIME NEEDED: 0.21 Rating : 0.00 340
+Unsatisfiable/GRP449-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 341
+Unsatisfiable/GRP450-1.ma ... OK TIME NEEDED: 0.88 Rating : 0.07 342
+Unsatisfiable/GRP451-1.ma ... OK TIME NEEDED: 0.16 Rating : 0.00 343
+Unsatisfiable/GRP452-1.ma ... OK TIME NEEDED: 1.67 Rating : 0.14 344
+Unsatisfiable/GRP453-1.ma ... OK TIME NEEDED: 3.25 Rating : 0.21 345
+Unsatisfiable/GRP454-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 346
+Unsatisfiable/GRP455-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 347
+Unsatisfiable/GRP456-1.ma ... OK TIME NEEDED: 0.26 Rating : 0.07 348
+Unsatisfiable/GRP457-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 349
+Unsatisfiable/GRP458-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 350
+Unsatisfiable/GRP459-1.ma ... OK TIME NEEDED: 0.27 Rating : 0.00 351
+Unsatisfiable/GRP460-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 352
+Unsatisfiable/GRP461-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 353
+Unsatisfiable/GRP462-1.ma ... OK TIME NEEDED: 0.32 Rating : 0.00 354
+Unsatisfiable/GRP463-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 355
+Unsatisfiable/GRP464-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 356
+Unsatisfiable/GRP465-1.ma ... OK TIME NEEDED: 0.32 Rating : 0.00 357
+Unsatisfiable/GRP466-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 358
+Unsatisfiable/GRP467-1.ma ... OK TIME NEEDED: 0.46 Rating : 0.00 359
+Unsatisfiable/GRP468-1.ma ... OK TIME NEEDED: 3.08 Rating : 0.00 360
+Unsatisfiable/GRP469-1.ma ... FAIL Rating : 0.21 361
+Unsatisfiable/GRP470-1.ma ... FAIL Rating : 0.21 362
+Unsatisfiable/GRP471-1.ma ... FAIL Rating : 0.21 363
+Unsatisfiable/GRP472-1.ma ... OK TIME NEEDED: 71.72 Rating : 0.07 364
+Unsatisfiable/GRP473-1.ma ... OK TIME NEEDED: 67.69 Rating : 0.07 365
+Unsatisfiable/GRP474-1.ma ... OK TIME NEEDED: 92.99 Rating : 0.07 366
+Unsatisfiable/GRP475-1.ma ... OK TIME NEEDED: 89.99 Rating : 0.21 367
+Unsatisfiable/GRP476-1.ma ... OK TIME NEEDED: 89.69 Rating : 0.21 368
+Unsatisfiable/GRP477-1.ma ... OK TIME NEEDED: 94.31 Rating : 0.21 369
+Unsatisfiable/GRP478-1.ma ... OK TIME NEEDED: 28.41 Rating : 0.14 370
+Unsatisfiable/GRP479-1.ma ... OK TIME NEEDED: 24.83 Rating : 0.14 371
+Unsatisfiable/GRP480-1.ma ... OK TIME NEEDED: 35.92 Rating : 0.21 372
+Unsatisfiable/GRP481-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 373
+Unsatisfiable/GRP482-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 374
+Unsatisfiable/GRP483-1.ma ... OK TIME NEEDED: 0.58 Rating : 0.00 375
+Unsatisfiable/GRP484-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 376
+Unsatisfiable/GRP485-1.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 377
+Unsatisfiable/GRP486-1.ma ... OK TIME NEEDED: 0.68 Rating : 0.00 378
+Unsatisfiable/GRP487-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 379
+Unsatisfiable/GRP488-1.ma ... OK TIME NEEDED: 0.85 Rating : 0.00 380
+Unsatisfiable/GRP489-1.ma ... OK TIME NEEDED: 1.76 Rating : 0.00 381
+Unsatisfiable/GRP490-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 382
+Unsatisfiable/GRP491-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 383
+Unsatisfiable/GRP492-1.ma ... OK TIME NEEDED: 0.42 Rating : 0.00 384
+Unsatisfiable/GRP493-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.00 385
+Unsatisfiable/GRP494-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 386
+Unsatisfiable/GRP495-1.ma ... OK TIME NEEDED: 0.33 Rating : 0.00 387
+Unsatisfiable/GRP496-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 388
+Unsatisfiable/GRP497-1.ma ... OK TIME NEEDED: 0.15 Rating : 0.00 389
+Unsatisfiable/GRP498-1.ma ... OK TIME NEEDED: 0.38 Rating : 0.00 390
+Unsatisfiable/GRP499-1.ma ... OK TIME NEEDED: 42.38 Rating : 0.00 391
+Unsatisfiable/GRP500-1.ma ... OK TIME NEEDED: 19.75 Rating : 0.07 392
+Unsatisfiable/GRP501-1.ma ... OK TIME NEEDED: 53.98 Rating : 0.14 393
+Unsatisfiable/GRP502-1.ma ... FAIL Rating : 0.14 394
+Unsatisfiable/GRP503-1.ma ... FAIL Rating : 0.14 395
+Unsatisfiable/GRP504-1.ma ... FAIL Rating : 0.14 396
+Unsatisfiable/GRP505-1.ma ... FAIL Rating : 0.50 397
+Unsatisfiable/GRP506-1.ma ... FAIL Rating : 0.64 398
+Unsatisfiable/GRP507-1.ma ... FAIL Rating : 0.57 399
+Unsatisfiable/GRP508-1.ma ... FAIL Rating : 0.57 400
+Unsatisfiable/GRP509-1.ma ... OK TIME NEEDED: 0.67 Rating : 0.00 401
+Unsatisfiable/GRP510-1.ma ... OK TIME NEEDED: 0.12 Rating : 0.00 402
+Unsatisfiable/GRP511-1.ma ... OK TIME NEEDED: 1.62 Rating : 0.00 403
+Unsatisfiable/GRP512-1.ma ... OK TIME NEEDED: 0.18 Rating : 0.00 404
+Unsatisfiable/GRP513-1.ma ... OK TIME NEEDED: 1.39 Rating : 0.00 405
+Unsatisfiable/GRP514-1.ma ... OK TIME NEEDED: 0.17 Rating : 0.00 406
+Unsatisfiable/GRP515-1.ma ... OK TIME NEEDED: 0.38 Rating : 0.00 407
+Unsatisfiable/GRP516-1.ma ... OK TIME NEEDED: 0.17 Rating : 0.00 408
+Unsatisfiable/GRP517-1.ma ... OK TIME NEEDED: 1.54 Rating : 0.00 409
+Unsatisfiable/GRP518-1.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 410
+Unsatisfiable/GRP519-1.ma ... OK TIME NEEDED: 2.18 Rating : 0.00 411
+Unsatisfiable/GRP520-1.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 412
+Unsatisfiable/GRP521-1.ma ... OK TIME NEEDED: 0.12 Rating : 0.00 413
+Unsatisfiable/GRP522-1.ma ... OK TIME NEEDED: 0.23 Rating : 0.00 414
+Unsatisfiable/GRP523-1.ma ... OK TIME NEEDED: 2.41 Rating : 0.00 415
+Unsatisfiable/GRP524-1.ma ... OK TIME NEEDED: 0.36 Rating : 0.00 416
+Unsatisfiable/GRP525-1.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 417
+Unsatisfiable/GRP526-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 418
+Unsatisfiable/GRP527-1.ma ... OK TIME NEEDED: 1.19 Rating : 0.00 419
+Unsatisfiable/GRP528-1.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 420
+Unsatisfiable/GRP529-1.ma ... OK TIME NEEDED: 0.07 Rating : 0.00 421
+Unsatisfiable/GRP530-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 422
+Unsatisfiable/GRP531-1.ma ... OK TIME NEEDED: 0.51 Rating : 0.00 423
+Unsatisfiable/GRP532-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 424
+Unsatisfiable/GRP533-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 425
+Unsatisfiable/GRP534-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 426
+Unsatisfiable/GRP535-1.ma ... OK TIME NEEDED: 0.73 Rating : 0.00 427
+Unsatisfiable/GRP536-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 428
+Unsatisfiable/GRP537-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 429
+Unsatisfiable/GRP538-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 430
+Unsatisfiable/GRP539-1.ma ... OK TIME NEEDED: 2.32 Rating : 0.00 431
+Unsatisfiable/GRP540-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 432
+Unsatisfiable/GRP541-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 433
+Unsatisfiable/GRP542-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 434
+Unsatisfiable/GRP543-1.ma ... OK TIME NEEDED: 0.35 Rating : 0.00 435
+Unsatisfiable/GRP544-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 436
+Unsatisfiable/GRP545-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 437
+Unsatisfiable/GRP546-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 438
+Unsatisfiable/GRP547-1.ma ... OK TIME NEEDED: 0.47 Rating : 0.00 439
+Unsatisfiable/GRP548-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 440
+Unsatisfiable/GRP549-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 441
+Unsatisfiable/GRP550-1.ma ... OK TIME NEEDED: 0.02 Rating : 0.07 442
+Unsatisfiable/GRP551-1.ma ... OK TIME NEEDED: 0.37 Rating : 0.00 443
+Unsatisfiable/GRP552-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 444
+Unsatisfiable/GRP553-1.ma ... OK TIME NEEDED: 0.18 Rating : 0.00 445
+Unsatisfiable/GRP554-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 446
+Unsatisfiable/GRP555-1.ma ... OK TIME NEEDED: 3.47 Rating : 0.00 447
+Unsatisfiable/GRP556-1.ma ... OK TIME NEEDED: 0.67 Rating : 0.00 448
+Unsatisfiable/GRP557-1.ma ... OK TIME NEEDED: 0.11 Rating : 0.00 449
+Unsatisfiable/GRP558-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 450
+Unsatisfiable/GRP559-1.ma ... OK TIME NEEDED: 2.54 Rating : 0.00 451
+Unsatisfiable/GRP560-1.ma ... OK TIME NEEDED: 0.20 Rating : 0.00 452
+Unsatisfiable/GRP561-1.ma ... OK TIME NEEDED: 0.17 Rating : 0.00 453
+Unsatisfiable/GRP562-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 454
+Unsatisfiable/GRP563-1.ma ... OK TIME NEEDED: 1.50 Rating : 0.00 455
+Unsatisfiable/GRP564-1.ma ... OK TIME NEEDED: 0.17 Rating : 0.00 456
+Unsatisfiable/GRP565-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 457
+Unsatisfiable/GRP566-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 458
+Unsatisfiable/GRP567-1.ma ... OK TIME NEEDED: 2.58 Rating : 0.14 459
+Unsatisfiable/GRP568-1.ma ... OK TIME NEEDED: 0.24 Rating : 0.14 460
+Unsatisfiable/GRP569-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 461
+Unsatisfiable/GRP570-1.ma ... OK TIME NEEDED: 0.04 Rating : 0.00 462
+Unsatisfiable/GRP571-1.ma ... OK TIME NEEDED: 0.85 Rating : 0.14 463
+Unsatisfiable/GRP572-1.ma ... OK TIME NEEDED: 0.23 Rating : 0.07 464
+Unsatisfiable/GRP573-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 465
+Unsatisfiable/GRP574-1.ma ... OK TIME NEEDED: 0.17 Rating : 0.00 466
+Unsatisfiable/GRP575-1.ma ... OK TIME NEEDED: 2.01 Rating : 0.14 467
+Unsatisfiable/GRP576-1.ma ... OK TIME NEEDED: 0.29 Rating : 0.00 468
+Unsatisfiable/GRP577-1.ma ... OK TIME NEEDED: 0.07 Rating : 0.00 469
+Unsatisfiable/GRP578-1.ma ... OK TIME NEEDED: 0.24 Rating : 0.00 470
+Unsatisfiable/GRP579-1.ma ... OK TIME NEEDED: 4.20 Rating : 0.07 471
+Unsatisfiable/GRP580-1.ma ... OK TIME NEEDED: 0.40 Rating : 0.00 472
+Unsatisfiable/GRP581-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 473
+Unsatisfiable/GRP582-1.ma ... OK TIME NEEDED: 0.18 Rating : 0.00 474
+Unsatisfiable/GRP583-1.ma ... OK TIME NEEDED: 1.43 Rating : 0.07 475
+Unsatisfiable/GRP584-1.ma ... OK TIME NEEDED: 0.20 Rating : 0.00 476
+Unsatisfiable/GRP585-1.ma ... OK TIME NEEDED: 0.18 Rating : 0.00 477
+Unsatisfiable/GRP586-1.ma ... OK TIME NEEDED: 0.35 Rating : 0.00 478
+Unsatisfiable/GRP587-1.ma ... OK TIME NEEDED: 8.87 Rating : 0.00 479
+Unsatisfiable/GRP588-1.ma ... OK TIME NEEDED: 0.76 Rating : 0.00 480
+Unsatisfiable/GRP589-1.ma ... OK TIME NEEDED: 0.17 Rating : 0.00 481
+Unsatisfiable/GRP590-1.ma ... OK TIME NEEDED: 0.16 Rating : 0.00 482
+Unsatisfiable/GRP591-1.ma ... OK TIME NEEDED: 10.79 Rating : 0.07 483
+Unsatisfiable/GRP592-1.ma ... OK TIME NEEDED: 0.21 Rating : 0.07 484
+Unsatisfiable/GRP593-1.ma ... OK TIME NEEDED: 1.28 Rating : 0.00 485
+Unsatisfiable/GRP594-1.ma ... OK TIME NEEDED: 0.75 Rating : 0.00 486
+Unsatisfiable/GRP595-1.ma ... OK TIME NEEDED: 0.19 Rating : 0.07 487
+Unsatisfiable/GRP596-1.ma ... OK TIME NEEDED: 0.29 Rating : 0.07 488
+Unsatisfiable/GRP597-1.ma ... OK TIME NEEDED: 0.58 Rating : 0.00 489
+Unsatisfiable/GRP598-1.ma ... OK TIME NEEDED: 0.23 Rating : 0.07 490
+Unsatisfiable/GRP599-1.ma ... OK TIME NEEDED: 1.68 Rating : 0.07 491
+Unsatisfiable/GRP600-1.ma ... OK TIME NEEDED: 0.37 Rating : 0.07 492
+Unsatisfiable/GRP601-1.ma ... OK TIME NEEDED: 1.47 Rating : 0.07 493
+Unsatisfiable/GRP602-1.ma ... OK TIME NEEDED: 0.48 Rating : 0.07 494
+Unsatisfiable/GRP603-1.ma ... OK TIME NEEDED: 0.48 Rating : 0.07 495
+Unsatisfiable/GRP604-1.ma ... OK TIME NEEDED: 0.52 Rating : 0.07 496
+Unsatisfiable/GRP605-1.ma ... OK TIME NEEDED: 1.64 Rating : 0.00 497
+Unsatisfiable/GRP606-1.ma ... OK TIME NEEDED: 0.42 Rating : 0.00 498
+Unsatisfiable/GRP607-1.ma ... OK TIME NEEDED: 3.85 Rating : 0.00 499
+Unsatisfiable/GRP608-1.ma ... OK TIME NEEDED: 0.56 Rating : 0.00 500
+Unsatisfiable/GRP609-1.ma ... OK TIME NEEDED: 2.09 Rating : 0.07 501
+Unsatisfiable/GRP610-1.ma ... OK TIME NEEDED: 0.44 Rating : 0.07 502
+Unsatisfiable/GRP611-1.ma ... OK TIME NEEDED: 2.08 Rating : 0.00 503
+Unsatisfiable/GRP612-1.ma ... OK TIME NEEDED: 0.44 Rating : 0.07 504
+Unsatisfiable/GRP613-1.ma ... OK TIME NEEDED: 0.58 Rating : 0.00 505
+Unsatisfiable/GRP614-1.ma ... OK TIME NEEDED: 0.26 Rating : 0.00 506
+Unsatisfiable/GRP615-1.ma ... OK TIME NEEDED: 1.33 Rating : 0.07 507
+Unsatisfiable/GRP616-1.ma ... OK TIME NEEDED: 0.26 Rating : 0.00 508
+Unsatisfiable/LAT006-1.ma ... OK TIME NEEDED: 8.77 Rating : 0.14 509
+Unsatisfiable/LAT007-1.ma ... OK TIME NEEDED: 76.98 Rating : 0.36 510
+Unsatisfiable/LAT008-1.ma ... OK TIME NEEDED: 0.46 Rating : 0.07 511
+Unsatisfiable/LAT009-1.ma ... FAIL Rating : 0.00 512
+Unsatisfiable/LAT010-1.ma ... FAIL Rating : 0.00 513
+Unsatisfiable/LAT011-1.ma ... OK TIME NEEDED: 84.39 Rating : 0.07 514
+Unsatisfiable/LAT012-1.ma ... OK TIME NEEDED: 7.89 Rating : 0.00 515
+Unsatisfiable/LAT013-1.ma ... OK TIME NEEDED: 59.75 Rating : 0.14 516
+Unsatisfiable/LAT014-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 517
+Unsatisfiable/LAT017-1.ma ... FAIL Rating : 0.71 518
+Unsatisfiable/LAT018-1.ma ... FAIL Rating : 0.93 519
+Unsatisfiable/LAT019-1.ma ... FAIL Rating : 0.00 520
+Unsatisfiable/LAT020-1.ma ... FAIL Rating : 0.50 521
+Unsatisfiable/LAT021-1.ma ... FAIL Rating : 0.00 522
+Unsatisfiable/LAT022-1.ma ... FAIL Rating : 0.21 523
+Unsatisfiable/LAT023-1.ma ... FAIL Rating : 0.21 524
+Unsatisfiable/LAT026-1.ma ... OK TIME NEEDED: 37.10 Rating : 0.14 525
+Unsatisfiable/LAT027-1.ma ... FAIL Rating : 0.07 526
+Unsatisfiable/LAT028-1.ma ... OK TIME NEEDED: 99.40 Rating : 0.00 527
+Unsatisfiable/LAT031-1.ma ... OK TIME NEEDED: 19.14 Rating : 0.00 528
+Unsatisfiable/LAT032-1.ma ... OK TIME NEEDED: 10.64 Rating : 0.00 529
+Unsatisfiable/LAT033-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 530
+Unsatisfiable/LAT034-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 531
+Unsatisfiable/LAT038-1.ma ... FAIL Rating : 0.43 532
+Unsatisfiable/LAT039-1.ma ... OK TIME NEEDED: 0.22 Rating : 0.00 533
+Unsatisfiable/LAT039-2.ma ... OK TIME NEEDED: 0.22 Rating : 0.00 534
+Unsatisfiable/LAT040-1.ma ... OK TIME NEEDED: 4.10 Rating : 0.00 535
+Unsatisfiable/LAT042-1.ma ... OK TIME NEEDED: 65.92 Rating : 0.00 536
+Unsatisfiable/LAT043-1.ma ... OK TIME NEEDED: 67.86 Rating : 0.00 537
+Unsatisfiable/LAT044-1.ma ... OK TIME NEEDED: 89.67 Rating : 0.14 538
+Unsatisfiable/LAT045-1.ma ... OK TIME NEEDED: 0.35 Rating : 0.07 539
+Unsatisfiable/LAT070-1.ma ... FAIL Rating : 0.93 540
+Unsatisfiable/LAT072-1.ma ... FAIL Rating : 1.00 541
+Unsatisfiable/LAT074-1.ma ... FAIL Rating : 1.00 542
+Unsatisfiable/LAT075-1.ma ... FAIL Rating : 1.00 543
+Unsatisfiable/LAT076-1.ma ... FAIL Rating : 1.00 544
+Unsatisfiable/LAT077-1.ma ... FAIL Rating : 1.00 545
+Unsatisfiable/LAT078-1.ma ... FAIL Rating : 1.00 546
+Unsatisfiable/LAT079-1.ma ... FAIL Rating : 1.00 547
+Unsatisfiable/LAT080-1.ma ... FAIL Rating : 0.36 548
+Unsatisfiable/LAT081-1.ma ... FAIL Rating : 0.57 549
+Unsatisfiable/LAT082-1.ma ... FAIL Rating : 0.64 550
+Unsatisfiable/LAT083-1.ma ... FAIL Rating : 0.36 551
+Unsatisfiable/LAT084-1.ma ... FAIL Rating : 0.50 552
+Unsatisfiable/LAT085-1.ma ... FAIL Rating : 0.57 553
+Unsatisfiable/LAT086-1.ma ... FAIL Rating : 0.50 554
+Unsatisfiable/LAT087-1.ma ... FAIL Rating : 0.43 555
+Unsatisfiable/LAT088-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 556
+Unsatisfiable/LAT089-1.ma ... OK TIME NEEDED: 1.23 Rating : 0.00 557
+Unsatisfiable/LAT090-1.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 558
+Unsatisfiable/LAT091-1.ma ... OK TIME NEEDED: 9.54 Rating : 0.07 559
+Unsatisfiable/LAT092-1.ma ... FAIL Rating : 0.36 560
+Unsatisfiable/LAT093-1.ma ... FAIL Rating : 0.43 561
+Unsatisfiable/LAT094-1.ma ... FAIL Rating : 0.36 562
+Unsatisfiable/LAT095-1.ma ... FAIL Rating : 0.43 563
+Unsatisfiable/LAT096-1.ma ... FAIL Rating : 0.36 564
+Unsatisfiable/LAT097-1.ma ... FAIL Rating : 0.36 565
+Unsatisfiable/LAT138-1.ma ... FAIL Rating : 1.00 566
+Unsatisfiable/LAT139-1.ma ... FAIL Rating : 1.00 567
+Unsatisfiable/LAT140-1.ma ... FAIL Rating : 1.00 568
+Unsatisfiable/LAT141-1.ma ... FAIL Rating : 1.00 569
+Unsatisfiable/LAT142-1.ma ... FAIL Rating : 0.64 570
+Unsatisfiable/LAT143-1.ma ... FAIL Rating : 0.14 571
+Unsatisfiable/LAT144-1.ma ... FAIL Rating : 0.86 572
+Unsatisfiable/LAT145-1.ma ... FAIL Rating : 0.93 573
+Unsatisfiable/LAT146-1.ma ... FAIL Rating : 0.79 574
+Unsatisfiable/LAT147-1.ma ... FAIL Rating : 0.79 575
+Unsatisfiable/LAT148-1.ma ... FAIL Rating : 0.71 576
+Unsatisfiable/LAT149-1.ma ... FAIL Rating : 0.93 577
+Unsatisfiable/LAT150-1.ma ... FAIL Rating : 0.86 578
+Unsatisfiable/LAT151-1.ma ... FAIL Rating : 0.86 579
+Unsatisfiable/LAT152-1.ma ... FAIL Rating : 0.79 580
+Unsatisfiable/LAT153-1.ma ... FAIL Rating : 0.93 581
+Unsatisfiable/LAT154-1.ma ... FAIL Rating : 0.79 582
+Unsatisfiable/LAT155-1.ma ... FAIL Rating : 0.86 583
+Unsatisfiable/LAT156-1.ma ... FAIL Rating : 0.64 584
+Unsatisfiable/LAT157-1.ma ... FAIL Rating : 0.86 585
+Unsatisfiable/LAT158-1.ma ... FAIL Rating : 0.93 586
+Unsatisfiable/LAT159-1.ma ... FAIL Rating : 0.86 587
+Unsatisfiable/LAT160-1.ma ... FAIL Rating : 0.64 588
+Unsatisfiable/LAT161-1.ma ... FAIL Rating : 1.00 589
+Unsatisfiable/LAT162-1.ma ... FAIL Rating : 0.86 590
+Unsatisfiable/LAT163-1.ma ... FAIL Rating : 0.93 591
+Unsatisfiable/LAT164-1.ma ... FAIL Rating : 0.93 592
+Unsatisfiable/LAT165-1.ma ... FAIL Rating : 0.93 593
+Unsatisfiable/LAT166-1.ma ... FAIL Rating : 0.93 594
+Unsatisfiable/LAT167-1.ma ... FAIL Rating : 0.93 595
+Unsatisfiable/LAT168-1.ma ... FAIL Rating : 0.14 596
+Unsatisfiable/LAT169-1.ma ... FAIL Rating : 0.86 597
+Unsatisfiable/LAT170-1.ma ... FAIL Rating : 0.79 598
+Unsatisfiable/LAT171-1.ma ... FAIL Rating : 0.50 599
+Unsatisfiable/LAT172-1.ma ... FAIL Rating : 0.93 600
+Unsatisfiable/LAT173-1.ma ... FAIL Rating : 0.93 601
+Unsatisfiable/LAT174-1.ma ... FAIL Rating : 0.79 602
+Unsatisfiable/LAT175-1.ma ... FAIL Rating : 0.93 603
+Unsatisfiable/LAT176-1.ma ... FAIL Rating : 0.93 604
+Unsatisfiable/LAT177-1.ma ... FAIL Rating : 1.00 605
+Unsatisfiable/LCL109-2.ma ... FAIL Rating : 0.29 606
+Unsatisfiable/LCL109-6.ma ... FAIL Rating : 0.14 607
+Unsatisfiable/LCL110-2.ma ... OK TIME NEEDED: 0.27 Rating : 0.00 608
+Unsatisfiable/LCL111-2.ma ... OK TIME NEEDED: 7.03 Rating : 0.07 609
+Unsatisfiable/LCL112-2.ma ... OK TIME NEEDED: 0.27 Rating : 0.00 610
+Unsatisfiable/LCL113-2.ma ... OK TIME NEEDED: 0.29 Rating : 0.00 611
+Unsatisfiable/LCL114-2.ma ... OK TIME NEEDED: 0.36 Rating : 0.00 612
+Unsatisfiable/LCL115-2.ma ... OK TIME NEEDED: 0.59 Rating : 0.00 613
+Unsatisfiable/LCL116-2.ma ... OK TIME NEEDED: 4.90 Rating : 0.00 614
+Unsatisfiable/LCL132-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 615
+Unsatisfiable/LCL133-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 616
+Unsatisfiable/LCL134-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 617
+Unsatisfiable/LCL135-1.ma ... OK TIME NEEDED: 0.06 Rating : 0.00 618
+Unsatisfiable/LCL138-1.ma ... FAIL Rating : 0.21 619
+Unsatisfiable/LCL139-1.ma ... OK TIME NEEDED: 0.34 Rating : 0.00 620
+Unsatisfiable/LCL140-1.ma ... OK TIME NEEDED: 0.28 Rating : 0.00 621
+Unsatisfiable/LCL141-1.ma ... OK TIME NEEDED: 0.59 Rating : 0.00 622
+Unsatisfiable/LCL153-1.ma ... OK TIME NEEDED: 0.31 Rating : 0.00 623
+Unsatisfiable/LCL154-1.ma ... OK TIME NEEDED: 0.27 Rating : 0.00 624
+Unsatisfiable/LCL155-1.ma ... OK TIME NEEDED: 0.29 Rating : 0.00 625
+Unsatisfiable/LCL156-1.ma ... OK TIME NEEDED: 0.27 Rating : 0.00 626
+Unsatisfiable/LCL157-1.ma ... OK TIME NEEDED: 0.27 Rating : 0.00 627
+Unsatisfiable/LCL158-1.ma ... OK TIME NEEDED: 0.31 Rating : 0.00 628
+Unsatisfiable/LCL159-1.ma ... OK TIME NEEDED: 6.15 Rating : 0.00 629
+Unsatisfiable/LCL160-1.ma ... FAIL Rating : 0.14 630
+Unsatisfiable/LCL161-1.ma ... OK TIME NEEDED: 0.09 Rating : 0.00 631
+Unsatisfiable/LCL162-1.ma ... FAIL Rating : 0.00 632
+Unsatisfiable/LCL163-1.ma ... OK TIME NEEDED: 5.06 Rating : 0.14 633
+Unsatisfiable/LCL164-1.ma ... OK TIME NEEDED: 0.10 Rating : 0.00 634
+Unsatisfiable/LDA001-1.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 635
+Unsatisfiable/LDA002-1.ma ... OK TIME NEEDED: 22.13 Rating : 0.00 636
+Unsatisfiable/LDA007-3.ma ... OK TIME NEEDED: 0.13 Rating : 0.00 637
+Unsatisfiable/RNG007-4.ma ... OK TIME NEEDED: 0.03 Rating : 0.00 638
+Unsatisfiable/RNG008-3.ma ... OK TIME NEEDED: 2.32 Rating : 0.07 639
+Unsatisfiable/RNG008-4.ma ... OK TIME NEEDED: 4.42 Rating : 0.07 640
+Unsatisfiable/RNG008-7.ma ... OK TIME NEEDED: 15.93 Rating : 0.07 641
+Unsatisfiable/RNG009-5.ma ... FAIL Rating : 0.50 642
+Unsatisfiable/RNG009-7.ma ... FAIL Rating : 0.50 643
+Unsatisfiable/RNG011-5.ma ... OK TIME NEEDED: 0.19 Rating : 0.00 644
+Unsatisfiable/RNG012-6.ma ... OK TIME NEEDED: 71.73 Rating : 0.00 645
+Unsatisfiable/RNG013-6.ma ... OK TIME NEEDED: 71.74 Rating : 0.00 646
+Unsatisfiable/RNG014-6.ma ... OK TIME NEEDED: 67.79 Rating : 0.00 647
+Unsatisfiable/RNG015-6.ma ... OK TIME NEEDED: 69.34 Rating : 0.00 648
+Unsatisfiable/RNG016-6.ma ... OK TIME NEEDED: 71.94 Rating : 0.00 649
+Unsatisfiable/RNG017-6.ma ... OK TIME NEEDED: 71.63 Rating : 0.00 650
+Unsatisfiable/RNG018-6.ma ... OK TIME NEEDED: 68.25 Rating : 0.00 651
+Unsatisfiable/RNG019-6.ma ... FAIL Rating : 0.21 652
+Unsatisfiable/RNG019-7.ma ... FAIL Rating : 0.21 653
+Unsatisfiable/RNG020-6.ma ... FAIL Rating : 0.29 654
+Unsatisfiable/RNG020-7.ma ... FAIL Rating : 0.21 655
+Unsatisfiable/RNG021-6.ma ... FAIL Rating : 0.14 656
+Unsatisfiable/RNG021-7.ma ... FAIL Rating : 0.21 657
+Unsatisfiable/RNG023-6.ma ... OK TIME NEEDED: 0.16 Rating : 0.00 658
+Unsatisfiable/RNG023-7.ma ... OK TIME NEEDED: 0.27 Rating : 0.00 659
+Unsatisfiable/RNG024-6.ma ... OK TIME NEEDED: 0.16 Rating : 0.00 660
+Unsatisfiable/RNG024-7.ma ... OK TIME NEEDED: 0.41 Rating : 0.00 661
+Unsatisfiable/RNG025-4.ma ... FAIL Rating : 0.29 662
+Unsatisfiable/RNG025-5.ma ... FAIL Rating : 0.36 663
+Unsatisfiable/RNG025-6.ma ... FAIL Rating : 0.29 664
+Unsatisfiable/RNG025-7.ma ... FAIL Rating : 0.43 665
+Unsatisfiable/RNG026-6.ma ... FAIL Rating : 0.57 666
+Unsatisfiable/RNG026-7.ma ... FAIL Rating : 0.50 667
+Unsatisfiable/RNG027-5.ma ... FAIL Rating : 0.86 668
+Unsatisfiable/RNG027-7.ma ... FAIL Rating : 0.86 669
+Unsatisfiable/RNG027-8.ma ... FAIL Rating : 0.86 670
+Unsatisfiable/RNG027-9.ma ... FAIL Rating : 0.86 671
+Unsatisfiable/RNG028-5.ma ... FAIL Rating : 0.86 672
+Unsatisfiable/RNG028-7.ma ... FAIL Rating : 0.86 673
+Unsatisfiable/RNG028-8.ma ... FAIL Rating : 0.86 674
+Unsatisfiable/RNG028-9.ma ... FAIL Rating : 0.86 675
+Unsatisfiable/RNG029-5.ma ... FAIL Rating : 0.86 676
+Unsatisfiable/RNG029-6.ma ... FAIL Rating : 0.86 677
+Unsatisfiable/RNG029-7.ma ... FAIL Rating : 0.86 678
+Unsatisfiable/RNG035-7.ma ... FAIL Rating : 0.86 679
+Unsatisfiable/ROB001-1.ma ... FAIL Rating : 1.00 680
+Unsatisfiable/ROB002-1.ma ... OK TIME NEEDED: 0.05 Rating : 0.00 681
+Unsatisfiable/ROB003-1.ma ... OK TIME NEEDED: 72.86 Rating : 0.00 682
+Unsatisfiable/ROB004-1.ma ... OK TIME NEEDED: 99.80 Rating : 0.00 683
+Unsatisfiable/ROB005-1.ma ... FAIL Rating : 0.07 684
+Unsatisfiable/ROB006-1.ma ... FAIL Rating : 0.86 685
+Unsatisfiable/ROB006-2.ma ... FAIL Rating : 0.86 686
+Unsatisfiable/ROB008-1.ma ... OK TIME NEEDED: 67.56 Rating : 0.00 687
+Unsatisfiable/ROB009-1.ma ... OK TIME NEEDED: 80.05 Rating : 0.00 688
+Unsatisfiable/ROB010-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 689
+Unsatisfiable/ROB013-1.ma ... OK TIME NEEDED: 0.01 Rating : 0.00 690
+Unsatisfiable/ROB022-1.ma ... FAIL Rating : 0.00 691
+Unsatisfiable/ROB023-1.ma ... FAIL Rating : 0.00 692
+Unsatisfiable/ROB026-1.ma ... FAIL Rating : 0.86 693
+Unsatisfiable/ROB030-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 694
+Unsatisfiable/ROB031-1.ma ... FAIL Rating : 1.00 695
+Unsatisfiable/ROB032-1.ma ... FAIL Rating : 1.00 696
+Unsatisfiable/SYN080-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 697
+Unsatisfiable/SYN083-1.ma ... OK TIME NEEDED: 0.00 Rating : 0.00 698
diff --git a/matita/tests/TPTP/log.300.26-5.menvcorti_VS_log.120.orsay.ods b/matita/tests/TPTP/log.300.26-5.menvcorti_VS_log.120.orsay.ods
new file mode 100644
index 000000000..8cf343101
Binary files /dev/null and b/matita/tests/TPTP/log.300.26-5.menvcorti_VS_log.120.orsay.ods differ
diff --git a/matita/tests/TPTP/try.sh b/matita/tests/TPTP/try.sh
index 12fc7effe..e55733bff 100755
--- a/matita/tests/TPTP/try.sh
+++ b/matita/tests/TPTP/try.sh
@@ -8,6 +8,7 @@ fi
 
 mkdir -p logs
 
+i=1
 for X in $TODO; do
   echo -n "$X ... "
   LOGNAME=logs/log.`basename $X`
@@ -15,8 +16,9 @@ for X in $TODO; do
   RATING=`grep "Rating" $X | sed 's/v.*//' | sed 's/(\*//'`
   if [ `grep "Found a proof" $LOGNAME | wc -l` -gt 0 ]; then
     TIME=`grep "TIME NEEDED" $LOGNAME`
-    echo OK $TIME $RATING
+    echo OK $TIME $RATING $i
   else
-    echo FAIL $RATING
+    echo FAIL $RATING $i
   fi
+  i=`expr $i + 1`
 done