Skip to content

Commit 8d87b04

Browse files
hargoniXDaniel1854
hargoniX
and
Daniel1854
authored
feat: add types (#19)
* feat: add the sort field * feat: infer_sort * feat: make sorts count * feat: extend tptp transformation to recognize props * feat: clause type checker * fix: buggy sort check * check well-typed * new results for full tptp --------- Co-authored-by: Daniel Soukup <d.soukup@campus.lmu.de>
1 parent e6bb27f commit 8d87b04

23 files changed

Lines changed: 3156 additions & 3010 deletions

‎benchmark/contradictory_1.csv‎

Lines changed: 386 additions & 386 deletions
Large diffs are not rendered by default.

‎benchmark/contradictory_1.summary‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
There are:
22
- 23 matching results
33
- 0 non-matching results
4-
- 169 timeout results
5-
- 337 'unknown' results
4+
- 134 timeout results
5+
- 372 'unknown' results

‎benchmark/counter_satisfiable_1.csv‎

Lines changed: 149 additions & 149 deletions
Large diffs are not rendered by default.

‎benchmark/counter_satisfiable_1.summary‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
There are:
2-
- 73 matching results
2+
- 81 matching results
33
- 0 non-matching results
4-
- 767 timeout results
4+
- 759 timeout results
55
- 41 'unknown' results

‎benchmark/satisfiable_1.csv‎

Lines changed: 55 additions & 55 deletions
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,10 @@ CSR010+1.p,StatementFalse,Unknown(Timeout),1.0
88
CSR111+2.p,StatementFalse,Unknown(Timeout),1.0
99
CSR111+3.p,StatementFalse,Unknown(Timeout),1.1
1010
CSR111+4.p,StatementFalse,Unknown(),0.5
11-
CSR111+5.p,StatementFalse,Unknown(),4.5
11+
CSR111+5.p,StatementFalse,Unknown(),4.4
1212
CSR154+1.p,StatementFalse,Unknown(Timeout),1.0
1313
CSR155+1.p,StatementFalse,Unknown(),0.2
14-
CSR156+1.p,StatementFalse,Unknown(),2.1
14+
CSR156+1.p,StatementFalse,Unknown(),2.3
1515
GEG001+1.p,StatementFalse,Unknown(Timeout),1.0
1616
GEO158+1.p,StatementFalse,Unknown(Timeout),1.0
1717
GEO159+1.p,StatementFalse,Unknown(Timeout),1.0
@@ -25,29 +25,29 @@ GRA075+1.p,StatementFalse,Unknown(Timeout),1.0
2525
GRP394+3.p,StatementFalse,Unknown(Timeout),1.1
2626
GRP396+1.p,StatementFalse,Unknown(Timeout),1.0
2727
GRP733+1.p,StatementFalse,Unknown(Timeout),1.1
28-
GRP734+1.p,StatementFalse,Unknown(Timeout),1.1
28+
GRP734+1.p,StatementFalse,Unknown(Timeout),1.0
2929
GRP760+1.p,StatementFalse,Unknown(Timeout),1.1
30-
GRP761+1.p,StatementFalse,Unknown(Timeout),1.1
30+
GRP761+1.p,StatementFalse,Unknown(Timeout),1.0
3131
GRP762+1.p,StatementFalse,Unknown(Timeout),1.1
3232
GRP763+1.p,StatementFalse,Unknown(Timeout),1.1
33-
HAL007+1.p,StatementFalse,Unknown(Timeout),1.1
33+
HAL007+1.p,StatementFalse,Unknown(Timeout),1.0
3434
HWV053+1.p,StatementFalse,Unknown(Timeout),1.1
35-
HWV054+1.p,StatementFalse,Unknown(Timeout),1.0
35+
HWV054+1.p,StatementFalse,Unknown(Timeout),1.1
3636
HWV062+1.p,StatementFalse,Unknown(),0.4
3737
HWV063+1.p,StatementFalse,Unknown(),0.7
3838
HWV066+1.p,StatementFalse,Unknown(),0.3
3939
HWV067+1.p,StatementFalse,Unknown(),0.8
40-
HWV070+1.p,StatementFalse,Unknown(),0.4
40+
HWV070+1.p,StatementFalse,Unknown(),0.3
4141
HWV071+1.p,StatementFalse,Unknown(Timeout),1.0
4242
HWV072+1.p,StatementFalse,Unknown(Timeout),1.0
4343
HWV073+1.p,StatementFalse,Unknown(Timeout),1.0
44-
HWV074+1.p,StatementFalse,Unknown(Timeout),1.0
44+
HWV074+1.p,StatementFalse,Unknown(Timeout),1.1
4545
HWV075+1.p,StatementFalse,Unknown(Timeout),1.1
4646
HWV076+1.p,StatementFalse,Unknown(Timeout),1.0
47-
HWV077+1.p,StatementFalse,Unknown(Timeout),1.0
47+
HWV077+1.p,StatementFalse,Unknown(Timeout),1.1
4848
HWV079+1.p,StatementFalse,Unknown(Timeout),1.0
4949
HWV080+1.p,StatementFalse,Unknown(Timeout),1.0
50-
HWV082+1.p,StatementFalse,Unknown(Timeout),1.0
50+
HWV082+1.p,StatementFalse,Unknown(Timeout),1.1
5151
HWV085+1.p,StatementFalse,Unknown(Timeout),1.0
5252
HWV086+1.p,StatementFalse,Unknown(),0.4
5353
KLE173+1.p,StatementFalse,Unknown(Timeout),1.0
@@ -68,26 +68,26 @@ KRS022+1.p,StatementFalse,StatementFalse,0.0
6868
KRS023+1.p,StatementFalse,StatementFalse,0.0
6969
KRS024+1.p,StatementFalse,StatementFalse,0.0
7070
KRS025+1.p,StatementFalse,StatementFalse,0.0
71-
KRS026+1.p,StatementFalse,ProofFound,0.0
71+
KRS026+1.p,StatementFalse,StatementFalse,0.0
7272
KRS027+1.p,StatementFalse,StatementFalse,0.0
7373
KRS028+1.p,StatementFalse,Unknown(Timeout),1.0
7474
KRS029+1.p,StatementFalse,Unknown(Timeout),1.0
7575
KRS030+1.p,StatementFalse,Unknown(Timeout),1.0
7676
KRS031+1.p,StatementFalse,Unknown(Timeout),1.0
77-
KRS032+1.p,StatementFalse,Unknown(Timeout),1.1
78-
KRS033+1.p,StatementFalse,Unknown(Timeout),2.0
79-
KRS034+1.p,StatementFalse,Unknown(Timeout),1.0
77+
KRS032+1.p,StatementFalse,Unknown(Timeout),1.0
78+
KRS033+1.p,StatementFalse,Unknown(Timeout),1.0
79+
KRS034+1.p,StatementFalse,Unknown(Timeout),1.1
8080
KRS035+1.p,StatementFalse,Unknown(Timeout),1.0
8181
KRS036+1.p,StatementFalse,Unknown(Timeout),1.0
82-
KRS037+1.p,StatementFalse,Unknown(Timeout),1.1
82+
KRS037+1.p,StatementFalse,Unknown(Timeout),1.0
8383
KRS038+1.p,StatementFalse,Unknown(Timeout),1.0
8484
KRS039+1.p,StatementFalse,Unknown(Timeout),1.0
8585
KRS040+1.p,StatementFalse,Unknown(Timeout),1.0
8686
KRS041+1.p,StatementFalse,StatementFalse,0.0
8787
KRS042+1.p,StatementFalse,Unknown(Timeout),1.0
8888
KRS043+1.p,StatementFalse,Unknown(Timeout),1.0
89-
KRS044+1.p,StatementFalse,Unknown(Timeout),1.1
90-
KRS045+1.p,StatementFalse,Unknown(Timeout),1.1
89+
KRS044+1.p,StatementFalse,Unknown(Timeout),1.0
90+
KRS045+1.p,StatementFalse,Unknown(Timeout),1.0
9191
KRS046+1.p,StatementFalse,Unknown(Timeout),1.0
9292
KRS047+1.p,StatementFalse,Unknown(Timeout),1.0
9393
KRS048+1.p,StatementFalse,Unknown(Timeout),1.0
@@ -110,35 +110,35 @@ KRS177+1.p,StatementFalse,Unknown(Timeout),1.0
110110
KRS279+1.p,StatementFalse,Unknown(Timeout),1.0
111111
KRS282+1.p,StatementFalse,Unknown(Timeout),1.1
112112
KRS285+1.p,StatementFalse,Unknown(Timeout),1.2
113-
KRS288+1.p,StatementFalse,Unknown(Timeout),1.2
113+
KRS288+1.p,StatementFalse,Unknown(Timeout),1.3
114114
KRS290+1.p,StatementFalse,Unknown(Timeout),1.2
115115
LCL354+1.p,StatementFalse,Unknown(Timeout),1.0
116-
LCL907+1.p,StatementFalse,Unknown(Timeout),1.0
116+
LCL907+1.p,StatementFalse,Unknown(Timeout),1.1
117117
LCL908+1.p,StatementFalse,Unknown(Timeout),1.0
118-
LCL909+1.p,StatementFalse,Unknown(Timeout),1.1
119-
LCL910+1.p,StatementFalse,Unknown(Timeout),1.0
120-
LCL911+1.p,StatementFalse,Unknown(Timeout),1.1
121-
LCL912+1.p,StatementFalse,Unknown(Timeout),1.1
118+
LCL909+1.p,StatementFalse,Unknown(Timeout),1.0
119+
LCL910+1.p,StatementFalse,Unknown(Timeout),1.1
120+
LCL911+1.p,StatementFalse,Unknown(Timeout),1.0
121+
LCL912+1.p,StatementFalse,Unknown(Timeout),1.0
122122
LCL913+1.p,StatementFalse,Unknown(Timeout),1.1
123123
LCL914+1.p,StatementFalse,Unknown(Timeout),1.1
124124
LCL915+1.p,StatementFalse,Unknown(Timeout),1.1
125-
MED011+1.p,StatementFalse,Unknown(),2.2
125+
MED011+1.p,StatementFalse,Unknown(),2.1
126126
MED012+1.p,StatementFalse,Unknown(Timeout),1.0
127127
MGT066+1.p,StatementFalse,Unknown(Timeout),1.0
128128
MSC009+1.p,StatementFalse,StatementFalse,0.0
129129
MSC014+1.p,StatementFalse,Unknown(Timeout),1.0
130-
NLP263+1.p,StatementFalse,Unknown(),3.9
130+
NLP263+1.p,StatementFalse,Unknown(),3.8
131131
NUN019+1.p,StatementFalse,Unknown(Timeout),1.0
132132
NUN020+1.p,StatementFalse,Unknown(Timeout),1.0
133133
NUN090+1.p,StatementFalse,Unknown(Timeout),1.0
134-
NUN090+2.p,StatementFalse,Unknown(Timeout),1.1
134+
NUN090+2.p,StatementFalse,Unknown(Timeout),1.0
135135
NUN091+1.p,StatementFalse,Unknown(Timeout),1.1
136136
PHI025+1.p,StatementFalse,StatementFalse,0.0
137137
PLA029+2.p,StatementFalse,Unknown(Timeout),1.0
138-
PLA034+1.p,StatementFalse,Unknown(),0.3
138+
PLA034+1.p,StatementFalse,Unknown(),0.2
139139
PLA038+1.p,StatementFalse,Unknown(Timeout),1.1
140140
PLA040+1.p,StatementFalse,Unknown(Timeout),1.1
141-
PLA041+1.p,StatementFalse,Unknown(),0.3
141+
PLA041+1.p,StatementFalse,Unknown(),0.4
142142
PLA043+1.p,StatementFalse,Unknown(),0.2
143143
PLA045+1.p,StatementFalse,Unknown(),0.6
144144
PUZ065+1.p,StatementFalse,Unknown(Timeout),1.0
@@ -158,11 +158,11 @@ REL051+1.p,StatementFalse,Unknown(Timeout),1.0
158158
REL052+1.p,StatementFalse,Unknown(Timeout),1.0
159159
REL053+1.p,StatementFalse,Unknown(Timeout),1.1
160160
RNG127+1.p,StatementFalse,Unknown(Timeout),1.1
161-
SET781+3.p,StatementFalse,Unknown(Timeout),1.1
162-
SET783+1.p,StatementFalse,Unknown(Timeout),1.1
161+
SET781+3.p,StatementFalse,Unknown(Timeout),1.0
162+
SET783+1.p,StatementFalse,Unknown(Timeout),1.0
163163
SET784+1.p,StatementFalse,Unknown(Timeout),1.0
164164
SET785+1.p,StatementFalse,Unknown(Timeout),1.0
165-
SEV435+1.p,StatementFalse,Unknown(),4.3
165+
SEV435+1.p,StatementFalse,Unknown(),4.2
166166
SEV437+1.p,StatementFalse,Unknown(Timeout),1.0
167167
SEV438+1.p,StatementFalse,Unknown(Timeout),1.0
168168
SEV439+1.p,StatementFalse,Unknown(Timeout),1.0
@@ -174,7 +174,7 @@ SWB030+3.p,StatementFalse,Unknown(Timeout),1.0
174174
SWB030+4.p,StatementFalse,Unknown(Timeout),1.0
175175
SWB031+3.p,StatementFalse,Unknown(Timeout),1.0
176176
SWB031+4.p,StatementFalse,Unknown(Timeout),1.0
177-
SWB033+1.p,StatementFalse,Unknown(Timeout),1.1
177+
SWB033+1.p,StatementFalse,Unknown(Timeout),1.2
178178
SWB034+1.p,StatementFalse,Unknown(Timeout),1.0
179179
SWB035+1.p,StatementFalse,Unknown(Timeout),1.0
180180
SWB036+1.p,StatementFalse,Unknown(Timeout),1.0
@@ -187,27 +187,27 @@ SWV017+1.p,StatementFalse,Unknown(Timeout),1.0
187187
SWW103+1.p,StatementFalse,Unknown(Timeout),1.0
188188
SWW673+1.p,StatementFalse,Unknown(Timeout),1.0
189189
SYN000+2.p,StatementFalse,Unknown(),0.0
190-
SYO583+1.p,StatementFalse,Unknown(Timeout),1.2
190+
SYO583+1.p,StatementFalse,Unknown(Timeout),1.3
191191
SYO584+1.p,StatementFalse,Unknown(Timeout),1.1
192192
SYO585+1.p,StatementFalse,Unknown(Timeout),1.1
193193
SYO586+1.p,StatementFalse,Unknown(Timeout),1.1
194194
SYO590+1.p,StatementFalse,Unknown(Timeout),1.1
195195
SYO593+1.p,StatementFalse,Unknown(Timeout),1.0
196196
SYO595+1.p,StatementFalse,Unknown(Timeout),1.1
197197
SYO596+1.p,StatementFalse,Unknown(Timeout),1.1
198-
SYO599+1.p,StatementFalse,Unknown(Timeout),1.2
198+
SYO599+1.p,StatementFalse,Unknown(Timeout),1.3
199199
SYO603+1.p,StatementFalse,Unknown(Timeout),1.0
200200
SYO635+1.p,StatementFalse,Unknown(Timeout),1.0
201201
SYO636+1.p,StatementFalse,Unknown(Timeout),1.0
202202
SYO637+1.p,StatementFalse,Unknown(Timeout),1.0
203-
SYO638+1.p,StatementFalse,Unknown(Timeout),1.1
203+
SYO638+1.p,StatementFalse,Unknown(Timeout),1.0
204204
SYO639+1.p,StatementFalse,StatementFalse,0.0
205-
SYO640+1.p,StatementFalse,Unknown(Timeout),1.2
205+
SYO640+1.p,StatementFalse,Unknown(Timeout),1.1
206206
SYO641+1.p,StatementFalse,StatementFalse,0.0
207207
SYO642+1.p,StatementFalse,Unknown(Timeout),1.0
208208
SYO643+1.p,StatementFalse,Unknown(Timeout),1.0
209209
SYO644+1.p,StatementFalse,Unknown(Timeout),1.0
210-
SYO645+1.p,StatementFalse,Unknown(Timeout),1.0
210+
SYO645+1.p,StatementFalse,Unknown(Timeout),1.6
211211
SYO692+1.p,StatementFalse,Unknown(Timeout),1.0
212212
SYO693+1.p,StatementFalse,Unknown(Timeout),1.0
213213
SYO694+1.p,StatementFalse,Unknown(Timeout),1.0
@@ -216,27 +216,27 @@ SYO696+1.p,StatementFalse,Unknown(Timeout),1.0
216216
SYO697+1.p,StatementFalse,Unknown(Timeout),1.0
217217
SYO698+1.p,StatementFalse,Unknown(Timeout),1.0
218218
SYO699+1.p,StatementFalse,Unknown(Timeout),1.0
219-
SYO700+1.p,StatementFalse,Unknown(Timeout),1.1
219+
SYO700+1.p,StatementFalse,Unknown(Timeout),1.0
220220
SYO701+1.p,StatementFalse,Unknown(Timeout),1.0
221221
SYO702+1.p,StatementFalse,Unknown(Timeout),1.0
222222
SYO703+1.p,StatementFalse,Unknown(Timeout),1.0
223-
SYO704+1.p,StatementFalse,Unknown(Timeout),1.1
223+
SYO704+1.p,StatementFalse,Unknown(Timeout),1.0
224224
SYO705+1.p,StatementFalse,Unknown(Timeout),1.0
225225
SYO706+1.p,StatementFalse,Unknown(Timeout),1.0
226-
SYO707+1.p,StatementFalse,Unknown(Timeout),1.1
226+
SYO707+1.p,StatementFalse,Unknown(Timeout),1.0
227227
SYO708+1.p,StatementFalse,Unknown(Timeout),1.0
228-
SYO709+1.p,StatementFalse,Unknown(Timeout),1.0
228+
SYO709+1.p,StatementFalse,Unknown(Timeout),1.1
229229
SYO710+1.p,StatementFalse,Unknown(Timeout),1.0
230230
SYO711+1.p,StatementFalse,Unknown(Timeout),1.0
231231
SYO712+1.p,StatementFalse,Unknown(Timeout),1.0
232232
SYO713+1.p,StatementFalse,Unknown(Timeout),1.0
233233
SYO714+1.p,StatementFalse,Unknown(Timeout),1.0
234234
SYO715+1.p,StatementFalse,Unknown(Timeout),1.0
235235
SYO716+1.p,StatementFalse,Unknown(Timeout),1.1
236-
SYO717+1.p,StatementFalse,Unknown(Timeout),1.1
236+
SYO717+1.p,StatementFalse,Unknown(Timeout),1.0
237237
SYO718+1.p,StatementFalse,Unknown(Timeout),1.0
238238
SYO719+1.p,StatementFalse,Unknown(Timeout),1.0
239-
SYO720+1.p,StatementFalse,Unknown(Timeout),1.1
239+
SYO720+1.p,StatementFalse,Unknown(Timeout),1.0
240240
SYO721+1.p,StatementFalse,Unknown(Timeout),1.0
241241
SYO722+1.p,StatementFalse,Unknown(Timeout),1.0
242242
SYO723+1.p,StatementFalse,Unknown(Timeout),1.0
@@ -247,30 +247,30 @@ SYO727+1.p,StatementFalse,Unknown(Timeout),1.0
247247
SYO728+1.p,StatementFalse,Unknown(Timeout),1.0
248248
SYO729+1.p,StatementFalse,Unknown(Timeout),1.0
249249
SYO730+1.p,StatementFalse,Unknown(Timeout),1.0
250-
SYO731+1.p,StatementFalse,Unknown(Timeout),1.1
250+
SYO731+1.p,StatementFalse,Unknown(Timeout),1.0
251251
SYO732+1.p,StatementFalse,Unknown(Timeout),1.0
252252
SYO733+1.p,StatementFalse,Unknown(Timeout),1.0
253253
SYO734+1.p,StatementFalse,Unknown(Timeout),1.0
254-
SYO735+1.p,StatementFalse,Unknown(Timeout),1.1
254+
SYO735+1.p,StatementFalse,Unknown(Timeout),1.0
255255
SYO736+1.p,StatementFalse,Unknown(Timeout),1.0
256256
SYO737+1.p,StatementFalse,Unknown(Timeout),1.0
257-
SYO738+1.p,StatementFalse,Unknown(Timeout),1.1
257+
SYO738+1.p,StatementFalse,Unknown(Timeout),1.0
258258
SYO739+1.p,StatementFalse,Unknown(Timeout),1.0
259259
SYO740+1.p,StatementFalse,Unknown(Timeout),1.0
260260
SYO741+1.p,StatementFalse,Unknown(Timeout),1.0
261-
SYO742+1.p,StatementFalse,Unknown(Timeout),1.1
261+
SYO742+1.p,StatementFalse,Unknown(Timeout),1.0
262262
SYO743+1.p,StatementFalse,Unknown(Timeout),1.0
263263
SYO744+1.p,StatementFalse,Unknown(Timeout),1.0
264264
SYO746+1.p,StatementFalse,Unknown(Timeout),1.0
265265
SYO747+1.p,StatementFalse,Unknown(Timeout),1.0
266266
SYO748+1.p,StatementFalse,Unknown(Timeout),1.0
267-
SYO749+1.p,StatementFalse,Unknown(Timeout),1.1
267+
SYO749+1.p,StatementFalse,Unknown(Timeout),1.0
268268
SYO750+1.p,StatementFalse,Unknown(Timeout),1.0
269269
SYO751+1.p,StatementFalse,Unknown(Timeout),1.0
270270
SYO752+1.p,StatementFalse,Unknown(Timeout),1.0
271271
SYO753+1.p,StatementFalse,Unknown(Timeout),1.0
272272
SYO754+1.p,StatementFalse,Unknown(Timeout),1.0
273-
SYO755+1.p,StatementFalse,Unknown(Timeout),1.1
273+
SYO755+1.p,StatementFalse,Unknown(Timeout),1.0
274274
SYO756+1.p,StatementFalse,Unknown(Timeout),1.0
275275
SYO757+1.p,StatementFalse,Unknown(Timeout),1.0
276276
SYO758+1.p,StatementFalse,Unknown(Timeout),1.0
@@ -297,15 +297,15 @@ SYO778+1.p,StatementFalse,Unknown(Timeout),1.0
297297
SYO779+1.p,StatementFalse,Unknown(Timeout),1.0
298298
SYO780+1.p,StatementFalse,Unknown(Timeout),1.0
299299
SYO781+1.p,StatementFalse,Unknown(Timeout),1.0
300-
SYO782+1.p,StatementFalse,Unknown(Timeout),1.1
300+
SYO782+1.p,StatementFalse,Unknown(Timeout),1.0
301301
SYO783+1.p,StatementFalse,Unknown(Timeout),1.0
302302
SYO784+1.p,StatementFalse,Unknown(Timeout),1.0
303-
SYO785+1.p,StatementFalse,Unknown(Timeout),1.0
303+
SYO785+1.p,StatementFalse,Unknown(Timeout),1.1
304304
SYO786+1.p,StatementFalse,Unknown(Timeout),1.0
305305
SYO787+1.p,StatementFalse,Unknown(Timeout),1.0
306306
SYO788+1.p,StatementFalse,Unknown(Timeout),1.0
307307
SYO789+1.p,StatementFalse,Unknown(Timeout),1.0
308-
SYO790+1.p,StatementFalse,Unknown(Timeout),1.1
308+
SYO790+1.p,StatementFalse,Unknown(Timeout),1.0
309309
SYO791+1.p,StatementFalse,Unknown(Timeout),1.0
310310
SYO792+1.p,StatementFalse,Unknown(Timeout),1.0
311311
SYO793+1.p,StatementFalse,Unknown(Timeout),1.0
@@ -323,7 +323,7 @@ SYO804+1.p,StatementFalse,Unknown(Timeout),1.0
323323
SYO805+1.p,StatementFalse,Unknown(Timeout),1.0
324324
SYO806+1.p,StatementFalse,Unknown(Timeout),1.0
325325
SYO807+1.p,StatementFalse,Unknown(Timeout),1.0
326-
SYO808+1.p,StatementFalse,Unknown(Timeout),1.1
326+
SYO808+1.p,StatementFalse,Unknown(Timeout),1.0
327327
SYO809+1.p,StatementFalse,Unknown(Timeout),1.0
328328
SYO810+1.p,StatementFalse,Unknown(Timeout),1.0
329329
SYO811+1.p,StatementFalse,Unknown(Timeout),1.0
@@ -339,7 +339,7 @@ SYO820+1.p,StatementFalse,Unknown(Timeout),1.0
339339
SYO821+1.p,StatementFalse,Unknown(Timeout),1.0
340340
SYO822+1.p,StatementFalse,Unknown(Timeout),1.0
341341
SYO823+1.p,StatementFalse,Unknown(Timeout),1.0
342-
SYO824+1.p,StatementFalse,Unknown(Timeout),1.1
342+
SYO824+1.p,StatementFalse,Unknown(Timeout),1.0
343343
SYO825+1.p,StatementFalse,Unknown(Timeout),1.1
344344
SYO826+1.p,StatementFalse,Unknown(Timeout),1.0
345345
SYO827+1.p,StatementFalse,Unknown(Timeout),1.0
@@ -353,7 +353,7 @@ SYO834+1.p,StatementFalse,Unknown(Timeout),1.1
353353
SYO835+1.p,StatementFalse,Unknown(Timeout),1.1
354354
SYO836+1.p,StatementFalse,Unknown(Timeout),1.0
355355
SYO837+1.p,StatementFalse,Unknown(Timeout),1.0
356-
SYO838+1.p,StatementFalse,Unknown(Timeout),1.1
356+
SYO838+1.p,StatementFalse,Unknown(Timeout),1.0
357357
SYO839+1.p,StatementFalse,Unknown(Timeout),1.0
358358
SYO840+1.p,StatementFalse,Unknown(Timeout),1.0
359359
SYO841+1.p,StatementFalse,Unknown(Timeout),1.0

‎benchmark/satisfiable_1.summary‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
There are:
2-
- 25 matching results
3-
- 1 non-matching results
2+
- 26 matching results
3+
- 0 non-matching results
44
- 306 timeout results
55
- 26 'unknown' results

‎benchmark/theorems.toml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1773,7 +1773,7 @@ result = "UNSAT"
17731773
filename = "problems/tptp-full/CSR/CSR061+3.p"
17741774
result = "UNSAT"
17751775
[problems."CSR061+4"]
1776-
filename = "problems/tptp-full/CSRCSR061+4.p"
1776+
filename = "problems/tptp-full/CSR/CSR061+4.p"
17771777
result = "UNSAT"
17781778
[problems."CSR061+5"]
17791779
filename = "problems/tptp-full/CSR/CSR061+5.p"
@@ -7743,7 +7743,7 @@ result = "UNSAT"
77437743
filename = "problems/tptp-full/LCL/LCL466+1.p"
77447744
result = "UNSAT"
77457745
[problems."LCL467+1"]
7746-
filename = "problems/tptp-full/LCLLCL467+1.p"
7746+
filename = "problems/tptp-full/LCL/LCL467+1.p"
77477747
result = "UNSAT"
77487748
[problems."LCL468+1"]
77497749
filename = "problems/tptp-full/LCL/LCL468+1.p"

0 commit comments

Comments
 (0)