-
Notifications
You must be signed in to change notification settings - Fork 6
/
linear_ari_tptp.list
500 lines (500 loc) · 14.6 KB
/
linear_ari_tptp.list
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
$TPTP/Problems/ARI/ARI001=1.p
$TPTP/Problems/ARI/ARI002=1.p
$TPTP/Problems/ARI/ARI003=1.p
$TPTP/Problems/ARI/ARI004=1.p
$TPTP/Problems/ARI/ARI005=1.p
$TPTP/Problems/ARI/ARI006=1.p
$TPTP/Problems/ARI/ARI007=1.p
$TPTP/Problems/ARI/ARI008=1.p
$TPTP/Problems/ARI/ARI009=1.p
$TPTP/Problems/ARI/ARI010=1.p
$TPTP/Problems/ARI/ARI011=1.p
$TPTP/Problems/ARI/ARI012=1.p
$TPTP/Problems/ARI/ARI013=1.p
$TPTP/Problems/ARI/ARI014=1.p
$TPTP/Problems/ARI/ARI015=1.p
$TPTP/Problems/ARI/ARI016=1.p
$TPTP/Problems/ARI/ARI017=1.p
$TPTP/Problems/ARI/ARI018=1.p
$TPTP/Problems/ARI/ARI019=1.p
$TPTP/Problems/ARI/ARI020=1.p
$TPTP/Problems/ARI/ARI021=1.p
$TPTP/Problems/ARI/ARI022=1.p
$TPTP/Problems/ARI/ARI023=1.p
$TPTP/Problems/ARI/ARI024=1.p
$TPTP/Problems/ARI/ARI025=1.p
$TPTP/Problems/ARI/ARI026=1.p
$TPTP/Problems/ARI/ARI027=1.p
$TPTP/Problems/ARI/ARI028=1.p
$TPTP/Problems/ARI/ARI029=1.p
$TPTP/Problems/ARI/ARI030=1.p
$TPTP/Problems/ARI/ARI031=1.p
$TPTP/Problems/ARI/ARI032=1.p
$TPTP/Problems/ARI/ARI033=1.p
$TPTP/Problems/ARI/ARI034=1.p
$TPTP/Problems/ARI/ARI035=1.p
$TPTP/Problems/ARI/ARI036=1.p
$TPTP/Problems/ARI/ARI037=1.p
$TPTP/Problems/ARI/ARI038=1.p
$TPTP/Problems/ARI/ARI039=1.p
$TPTP/Problems/ARI/ARI040=1.p
$TPTP/Problems/ARI/ARI041=1.p
$TPTP/Problems/ARI/ARI042=1.p
$TPTP/Problems/ARI/ARI043=1.p
$TPTP/Problems/ARI/ARI044=1.p
$TPTP/Problems/ARI/ARI045=1.p
$TPTP/Problems/ARI/ARI046=1.p
$TPTP/Problems/ARI/ARI047=1.p
$TPTP/Problems/ARI/ARI048=1.p
$TPTP/Problems/ARI/ARI049=1.p
$TPTP/Problems/ARI/ARI050=1.p
$TPTP/Problems/ARI/ARI051=1.p
$TPTP/Problems/ARI/ARI052=1.p
$TPTP/Problems/ARI/ARI053=1.p
$TPTP/Problems/ARI/ARI054=1.p
$TPTP/Problems/ARI/ARI055=1.p
$TPTP/Problems/ARI/ARI056=1.p
$TPTP/Problems/ARI/ARI057=1.p
$TPTP/Problems/ARI/ARI058=1.p
$TPTP/Problems/ARI/ARI059=1.p
$TPTP/Problems/ARI/ARI060=1.p
$TPTP/Problems/ARI/ARI061=1.p
$TPTP/Problems/ARI/ARI062=1.p
$TPTP/Problems/ARI/ARI063=1.p
$TPTP/Problems/ARI/ARI064=1.p
$TPTP/Problems/ARI/ARI065=1.p
$TPTP/Problems/ARI/ARI066=1.p
$TPTP/Problems/ARI/ARI067=1.p
$TPTP/Problems/ARI/ARI068=1.p
$TPTP/Problems/ARI/ARI069=1.p
$TPTP/Problems/ARI/ARI070=1.p
$TPTP/Problems/ARI/ARI071=1.p
$TPTP/Problems/ARI/ARI072=1.p
$TPTP/Problems/ARI/ARI073=1.p
$TPTP/Problems/ARI/ARI074=1.p
$TPTP/Problems/ARI/ARI075=1.p
$TPTP/Problems/ARI/ARI076=1.p
$TPTP/Problems/ARI/ARI077=1.p
$TPTP/Problems/ARI/ARI078=1.p
$TPTP/Problems/ARI/ARI079=1.p
$TPTP/Problems/ARI/ARI080=1.p
$TPTP/Problems/ARI/ARI081=1.p
$TPTP/Problems/ARI/ARI082=1.p
$TPTP/Problems/ARI/ARI083=1.p
$TPTP/Problems/ARI/ARI084=1.p
$TPTP/Problems/ARI/ARI085=1.p
$TPTP/Problems/ARI/ARI089=1.p
$TPTP/Problems/ARI/ARI090=1.p
$TPTP/Problems/ARI/ARI091=1.p
$TPTP/Problems/ARI/ARI092=1.p
$TPTP/Problems/ARI/ARI093=1.p
$TPTP/Problems/ARI/ARI094=1.p
$TPTP/Problems/ARI/ARI095=1.p
$TPTP/Problems/ARI/ARI096=1.p
$TPTP/Problems/ARI/ARI097=1.p
$TPTP/Problems/ARI/ARI098=1.p
$TPTP/Problems/ARI/ARI099=1.p
$TPTP/Problems/ARI/ARI100=1.p
$TPTP/Problems/ARI/ARI101=1.p
$TPTP/Problems/ARI/ARI102=1.p
$TPTP/Problems/ARI/ARI103=1.p
$TPTP/Problems/ARI/ARI104=1.p
$TPTP/Problems/ARI/ARI105=1.p
$TPTP/Problems/ARI/ARI106=1.p
$TPTP/Problems/ARI/ARI107=1.p
$TPTP/Problems/ARI/ARI108=1.p
$TPTP/Problems/ARI/ARI109=1.p
$TPTP/Problems/ARI/ARI110=1.p
$TPTP/Problems/ARI/ARI111=1.p
$TPTP/Problems/ARI/ARI112=1.p
$TPTP/Problems/ARI/ARI113=1.p
$TPTP/Problems/ARI/ARI114=1.p
$TPTP/Problems/ARI/ARI115=1.p
$TPTP/Problems/ARI/ARI116=1.p
$TPTP/Problems/ARI/ARI117=1.p
$TPTP/Problems/ARI/ARI121=1.p
$TPTP/Problems/ARI/ARI122=1.p
$TPTP/Problems/ARI/ARI124=1.p
$TPTP/Problems/ARI/ARI128=1.p
$TPTP/Problems/ARI/ARI129=1.p
$TPTP/Problems/ARI/ARI130=1.p
$TPTP/Problems/ARI/ARI131=1.p
$TPTP/Problems/ARI/ARI132=1.p
$TPTP/Problems/ARI/ARI133=1.p
$TPTP/Problems/ARI/ARI162=1.p
$TPTP/Problems/ARI/ARI163=1.p
$TPTP/Problems/ARI/ARI164=1.p
$TPTP/Problems/ARI/ARI165=1.p
$TPTP/Problems/ARI/ARI166=1.p
$TPTP/Problems/ARI/ARI167=1.p
$TPTP/Problems/ARI/ARI172=1.p
$TPTP/Problems/ARI/ARI173=1.p
$TPTP/Problems/ARI/ARI174=1.p
$TPTP/Problems/ARI/ARI175=1.p
$TPTP/Problems/ARI/ARI176=1.p
$TPTP/Problems/ARI/ARI177=1.p
$TPTP/Problems/ARI/ARI178=1.p
$TPTP/Problems/ARI/ARI179=1.p
$TPTP/Problems/ARI/ARI180=1.p
$TPTP/Problems/ARI/ARI181=1.p
$TPTP/Problems/ARI/ARI182=1.p
$TPTP/Problems/ARI/ARI183=1.p
$TPTP/Problems/ARI/ARI184=1.p
$TPTP/Problems/ARI/ARI185=1.p
$TPTP/Problems/ARI/ARI186=1.p
$TPTP/Problems/ARI/ARI187=1.p
$TPTP/Problems/ARI/ARI188=1.p
$TPTP/Problems/ARI/ARI189=1.p
$TPTP/Problems/ARI/ARI190=1.p
$TPTP/Problems/ARI/ARI191=1.p
$TPTP/Problems/ARI/ARI192=1.p
$TPTP/Problems/ARI/ARI193=1.p
$TPTP/Problems/ARI/ARI194=1.p
$TPTP/Problems/ARI/ARI195=1.p
$TPTP/Problems/ARI/ARI196=1.p
$TPTP/Problems/ARI/ARI197=1.p
$TPTP/Problems/ARI/ARI198=1.p
$TPTP/Problems/ARI/ARI199=1.p
$TPTP/Problems/ARI/ARI200=1.p
$TPTP/Problems/ARI/ARI201=1.p
$TPTP/Problems/ARI/ARI202=1.p
$TPTP/Problems/ARI/ARI203=1.p
$TPTP/Problems/ARI/ARI204=1.p
$TPTP/Problems/ARI/ARI205=1.p
$TPTP/Problems/ARI/ARI206=1.p
$TPTP/Problems/ARI/ARI207=1.p
$TPTP/Problems/ARI/ARI208=1.p
$TPTP/Problems/ARI/ARI209=1.p
$TPTP/Problems/ARI/ARI210=1.p
$TPTP/Problems/ARI/ARI211=1.p
$TPTP/Problems/ARI/ARI212=1.p
$TPTP/Problems/ARI/ARI213=1.p
$TPTP/Problems/ARI/ARI214=1.p
$TPTP/Problems/ARI/ARI215=1.p
$TPTP/Problems/ARI/ARI216=1.p
$TPTP/Problems/ARI/ARI217=1.p
$TPTP/Problems/ARI/ARI218=1.p
$TPTP/Problems/ARI/ARI219=1.p
$TPTP/Problems/ARI/ARI220=1.p
$TPTP/Problems/ARI/ARI221=1.p
$TPTP/Problems/ARI/ARI222=1.p
$TPTP/Problems/ARI/ARI223=1.p
$TPTP/Problems/ARI/ARI224=1.p
$TPTP/Problems/ARI/ARI225=1.p
$TPTP/Problems/ARI/ARI226=1.p
$TPTP/Problems/ARI/ARI227=1.p
$TPTP/Problems/ARI/ARI228=1.p
$TPTP/Problems/ARI/ARI229=1.p
$TPTP/Problems/ARI/ARI230=1.p
$TPTP/Problems/ARI/ARI231=1.p
$TPTP/Problems/ARI/ARI232=1.p
$TPTP/Problems/ARI/ARI233=1.p
$TPTP/Problems/ARI/ARI234=1.p
$TPTP/Problems/ARI/ARI235=1.p
$TPTP/Problems/ARI/ARI236=1.p
$TPTP/Problems/ARI/ARI237=1.p
$TPTP/Problems/ARI/ARI238=1.p
$TPTP/Problems/ARI/ARI239=1.p
$TPTP/Problems/ARI/ARI240=1.p
$TPTP/Problems/ARI/ARI241=1.p
$TPTP/Problems/ARI/ARI242=1.p
$TPTP/Problems/ARI/ARI243=1.p
$TPTP/Problems/ARI/ARI244=1.p
$TPTP/Problems/ARI/ARI245=1.p
$TPTP/Problems/ARI/ARI246=1.p
$TPTP/Problems/ARI/ARI247=1.p
$TPTP/Problems/ARI/ARI248=1.p
$TPTP/Problems/ARI/ARI249=1.p
$TPTP/Problems/ARI/ARI250=1.p
$TPTP/Problems/ARI/ARI251=1.p
$TPTP/Problems/ARI/ARI252=1.p
$TPTP/Problems/ARI/ARI253=1.p
$TPTP/Problems/ARI/ARI254=1.p
$TPTP/Problems/ARI/ARI255=1.p
$TPTP/Problems/ARI/ARI256=1.p
$TPTP/Problems/ARI/ARI257=1.p
$TPTP/Problems/ARI/ARI258=1.p
$TPTP/Problems/ARI/ARI259=1.p
$TPTP/Problems/ARI/ARI260=1.p
$TPTP/Problems/ARI/ARI261=1.p
$TPTP/Problems/ARI/ARI262=1.p
$TPTP/Problems/ARI/ARI263=1.p
$TPTP/Problems/ARI/ARI264=1.p
$TPTP/Problems/ARI/ARI265=1.p
$TPTP/Problems/ARI/ARI266=1.p
$TPTP/Problems/ARI/ARI267=1.p
$TPTP/Problems/ARI/ARI268=1.p
$TPTP/Problems/ARI/ARI269=1.p
$TPTP/Problems/ARI/ARI270=1.p
$TPTP/Problems/ARI/ARI271=1.p
$TPTP/Problems/ARI/ARI272=1.p
$TPTP/Problems/ARI/ARI273=1.p
$TPTP/Problems/ARI/ARI274=1.p
$TPTP/Problems/ARI/ARI275=1.p
$TPTP/Problems/ARI/ARI276=1.p
$TPTP/Problems/ARI/ARI277=1.p
$TPTP/Problems/ARI/ARI278=1.p
$TPTP/Problems/ARI/ARI279=1.p
$TPTP/Problems/ARI/ARI280=1.p
$TPTP/Problems/ARI/ARI281=1.p
$TPTP/Problems/ARI/ARI282=1.p
$TPTP/Problems/ARI/ARI283=1.p
$TPTP/Problems/ARI/ARI284=1.p
$TPTP/Problems/ARI/ARI285=1.p
$TPTP/Problems/ARI/ARI286=1.p
$TPTP/Problems/ARI/ARI287=1.p
$TPTP/Problems/ARI/ARI288=1.p
$TPTP/Problems/ARI/ARI289=1.p
$TPTP/Problems/ARI/ARI290=1.p
$TPTP/Problems/ARI/ARI291=1.p
$TPTP/Problems/ARI/ARI292=1.p
$TPTP/Problems/ARI/ARI293=1.p
$TPTP/Problems/ARI/ARI294=1.p
$TPTP/Problems/ARI/ARI295=1.p
$TPTP/Problems/ARI/ARI296=1.p
$TPTP/Problems/ARI/ARI297=1.p
$TPTP/Problems/ARI/ARI298=1.p
$TPTP/Problems/ARI/ARI299=1.p
$TPTP/Problems/ARI/ARI300=1.p
$TPTP/Problems/ARI/ARI301=1.p
$TPTP/Problems/ARI/ARI302=1.p
$TPTP/Problems/ARI/ARI303=1.p
$TPTP/Problems/ARI/ARI304=1.p
$TPTP/Problems/ARI/ARI305=1.p
$TPTP/Problems/ARI/ARI306=1.p
$TPTP/Problems/ARI/ARI307=1.p
$TPTP/Problems/ARI/ARI308=1.p
$TPTP/Problems/ARI/ARI309=1.p
$TPTP/Problems/ARI/ARI310=1.p
$TPTP/Problems/ARI/ARI311=1.p
$TPTP/Problems/ARI/ARI312=1.p
$TPTP/Problems/ARI/ARI313=1.p
$TPTP/Problems/ARI/ARI337=1.p
$TPTP/Problems/ARI/ARI338=1.p
$TPTP/Problems/ARI/ARI339=1.p
$TPTP/Problems/ARI/ARI340=1.p
$TPTP/Problems/ARI/ARI341=1.p
$TPTP/Problems/ARI/ARI342=1.p
$TPTP/Problems/ARI/ARI343=1.p
$TPTP/Problems/ARI/ARI344=1.p
$TPTP/Problems/ARI/ARI345=1.p
$TPTP/Problems/ARI/ARI346=1.p
$TPTP/Problems/ARI/ARI347=1.p
$TPTP/Problems/ARI/ARI348=1.p
$TPTP/Problems/ARI/ARI349=1.p
$TPTP/Problems/ARI/ARI350=1.p
$TPTP/Problems/ARI/ARI351=1.p
$TPTP/Problems/ARI/ARI352=1.p
$TPTP/Problems/ARI/ARI353=1.p
$TPTP/Problems/ARI/ARI354=1.p
$TPTP/Problems/ARI/ARI355=1.p
$TPTP/Problems/ARI/ARI356=1.p
$TPTP/Problems/ARI/ARI357=1.p
$TPTP/Problems/ARI/ARI358=1.p
$TPTP/Problems/ARI/ARI359=1.p
$TPTP/Problems/ARI/ARI360=1.p
$TPTP/Problems/ARI/ARI361=1.p
$TPTP/Problems/ARI/ARI362=1.p
$TPTP/Problems/ARI/ARI363=1.p
$TPTP/Problems/ARI/ARI364=1.p
$TPTP/Problems/ARI/ARI365=1.p
$TPTP/Problems/ARI/ARI366=1.p
$TPTP/Problems/ARI/ARI367=1.p
$TPTP/Problems/ARI/ARI368=1.p
$TPTP/Problems/ARI/ARI369=1.p
$TPTP/Problems/ARI/ARI370=1.p
$TPTP/Problems/ARI/ARI371=1.p
$TPTP/Problems/ARI/ARI372=1.p
$TPTP/Problems/ARI/ARI373=1.p
$TPTP/Problems/ARI/ARI374=1.p
$TPTP/Problems/ARI/ARI375=1.p
$TPTP/Problems/ARI/ARI376=1.p
$TPTP/Problems/ARI/ARI377=1.p
$TPTP/Problems/ARI/ARI378=1.p
$TPTP/Problems/ARI/ARI379=1.p
$TPTP/Problems/ARI/ARI380=1.p
$TPTP/Problems/ARI/ARI381=1.p
$TPTP/Problems/ARI/ARI382=1.p
$TPTP/Problems/ARI/ARI383=1.p
$TPTP/Problems/ARI/ARI384=1.p
$TPTP/Problems/ARI/ARI385=1.p
$TPTP/Problems/ARI/ARI386=1.p
$TPTP/Problems/ARI/ARI387=1.p
$TPTP/Problems/ARI/ARI388=1.p
$TPTP/Problems/ARI/ARI389=1.p
$TPTP/Problems/ARI/ARI390=1.p
$TPTP/Problems/ARI/ARI391=1.p
$TPTP/Problems/ARI/ARI392=1.p
$TPTP/Problems/ARI/ARI393=1.p
$TPTP/Problems/ARI/ARI394=1.p
$TPTP/Problems/ARI/ARI395=1.p
$TPTP/Problems/ARI/ARI396=1.p
$TPTP/Problems/ARI/ARI397=1.p
$TPTP/Problems/ARI/ARI398=1.p
$TPTP/Problems/ARI/ARI399=1.p
$TPTP/Problems/ARI/ARI400=1.p
$TPTP/Problems/ARI/ARI401=1.p
$TPTP/Problems/ARI/ARI402=1.p
$TPTP/Problems/ARI/ARI403=1.p
$TPTP/Problems/ARI/ARI404=1.p
$TPTP/Problems/ARI/ARI405=1.p
$TPTP/Problems/ARI/ARI406=1.p
$TPTP/Problems/ARI/ARI407=1.p
$TPTP/Problems/ARI/ARI408=1.p
$TPTP/Problems/ARI/ARI409=1.p
$TPTP/Problems/ARI/ARI410=1.p
$TPTP/Problems/ARI/ARI411=1.p
$TPTP/Problems/ARI/ARI412=1.p
$TPTP/Problems/ARI/ARI413=1.p
$TPTP/Problems/ARI/ARI414=1.p
$TPTP/Problems/ARI/ARI415=1.p
$TPTP/Problems/ARI/ARI416=1.p
$TPTP/Problems/ARI/ARI417=1.p
$TPTP/Problems/ARI/ARI418=1.p
$TPTP/Problems/ARI/ARI419=1.p
$TPTP/Problems/ARI/ARI420=1.p
$TPTP/Problems/ARI/ARI421=1.p
$TPTP/Problems/ARI/ARI422=1.p
$TPTP/Problems/ARI/ARI423=1.p
$TPTP/Problems/ARI/ARI424=1.p
$TPTP/Problems/ARI/ARI425=1.p
$TPTP/Problems/ARI/ARI426=1.p
$TPTP/Problems/ARI/ARI427=1.p
$TPTP/Problems/ARI/ARI428=1.p
$TPTP/Problems/ARI/ARI429=1.p
$TPTP/Problems/ARI/ARI430=1.p
$TPTP/Problems/ARI/ARI431=1.p
$TPTP/Problems/ARI/ARI432=1.p
$TPTP/Problems/ARI/ARI433=1.p
$TPTP/Problems/ARI/ARI434=1.p
$TPTP/Problems/ARI/ARI435=1.p
$TPTP/Problems/ARI/ARI436=1.p
$TPTP/Problems/ARI/ARI437=1.p
$TPTP/Problems/ARI/ARI438=1.p
$TPTP/Problems/ARI/ARI439=1.p
$TPTP/Problems/ARI/ARI440=1.p
$TPTP/Problems/ARI/ARI441=1.p
$TPTP/Problems/ARI/ARI442=1.p
$TPTP/Problems/ARI/ARI443=1.p
$TPTP/Problems/ARI/ARI444=1.p
$TPTP/Problems/ARI/ARI445=1.p
$TPTP/Problems/ARI/ARI446=1.p
$TPTP/Problems/ARI/ARI447=1.p
$TPTP/Problems/ARI/ARI448=1.p
$TPTP/Problems/ARI/ARI449=1.p
$TPTP/Problems/ARI/ARI450=1.p
$TPTP/Problems/ARI/ARI451=1.p
$TPTP/Problems/ARI/ARI452=1.p
$TPTP/Problems/ARI/ARI453=1.p
$TPTP/Problems/ARI/ARI454=1.p
$TPTP/Problems/ARI/ARI455=1.p
$TPTP/Problems/ARI/ARI456=1.p
$TPTP/Problems/ARI/ARI457=1.p
$TPTP/Problems/ARI/ARI458=1.p
$TPTP/Problems/ARI/ARI459=1.p
$TPTP/Problems/ARI/ARI460=1.p
$TPTP/Problems/ARI/ARI461=1.p
$TPTP/Problems/ARI/ARI462=1.p
$TPTP/Problems/ARI/ARI463=1.p
$TPTP/Problems/ARI/ARI464=1.p
$TPTP/Problems/ARI/ARI488=1.p
$TPTP/Problems/ARI/ARI489=1.p
$TPTP/Problems/ARI/ARI490=1.p
$TPTP/Problems/ARI/ARI491=1.p
$TPTP/Problems/ARI/ARI492=1.p
$TPTP/Problems/ARI/ARI493=1.p
$TPTP/Problems/ARI/ARI494=1.p
$TPTP/Problems/ARI/ARI495=1.p
$TPTP/Problems/ARI/ARI535=1.p
$TPTP/Problems/ARI/ARI537=1.p
$TPTP/Problems/ARI/ARI538=1.p
$TPTP/Problems/ARI/ARI539=1.p
$TPTP/Problems/ARI/ARI540=1.p
$TPTP/Problems/ARI/ARI541=1.p
$TPTP/Problems/ARI/ARI542=1.p
$TPTP/Problems/ARI/ARI543=1.p
$TPTP/Problems/ARI/ARI544=1.p
$TPTP/Problems/ARI/ARI545=1.p
$TPTP/Problems/ARI/ARI546=1.p
$TPTP/Problems/ARI/ARI547=1.p
$TPTP/Problems/ARI/ARI548=1.p
$TPTP/Problems/ARI/ARI549=1.p
$TPTP/Problems/ARI/ARI550=1.p
$TPTP/Problems/ARI/ARI551=1.p
$TPTP/Problems/ARI/ARI552=1.p
$TPTP/Problems/ARI/ARI553=1.p
$TPTP/Problems/ARI/ARI554=1.p
$TPTP/Problems/ARI/ARI555=1.p
$TPTP/Problems/ARI/ARI556=1.p
$TPTP/Problems/ARI/ARI557=1.p
$TPTP/Problems/ARI/ARI558=1.p
$TPTP/Problems/ARI/ARI559=1.p
$TPTP/Problems/ARI/ARI560=1.p
$TPTP/Problems/ARI/ARI561=1.p
$TPTP/Problems/ARI/ARI562=1.p
$TPTP/Problems/ARI/ARI563=1.p
$TPTP/Problems/ARI/ARI564=1.p
$TPTP/Problems/ARI/ARI565=1.p
$TPTP/Problems/ARI/ARI566=1.p
$TPTP/Problems/ARI/ARI567=1.p
$TPTP/Problems/ARI/ARI568=1.p
$TPTP/Problems/ARI/ARI570=1.p
$TPTP/Problems/ARI/ARI571=1.p
$TPTP/Problems/ARI/ARI572=1.p
$TPTP/Problems/ARI/ARI573=1.p
$TPTP/Problems/ARI/ARI574=1.p
$TPTP/Problems/ARI/ARI575=1.p
$TPTP/Problems/ARI/ARI576=1.p
$TPTP/Problems/ARI/ARI577=1.p
$TPTP/Problems/ARI/ARI578=1.p
$TPTP/Problems/ARI/ARI579=2.p
$TPTP/Problems/ARI/ARI579=3.p
$TPTP/Problems/ARI/ARI580=1.p
$TPTP/Problems/ARI/ARI581=1.p
$TPTP/Problems/ARI/ARI582=1.p
$TPTP/Problems/ARI/ARI583=1.p
$TPTP/Problems/ARI/ARI584=1.p
$TPTP/Problems/ARI/ARI585=1.p
$TPTP/Problems/ARI/ARI586=1.p
$TPTP/Problems/ARI/ARI587=1.p
$TPTP/Problems/ARI/ARI588=1.p
$TPTP/Problems/ARI/ARI589=1.p
$TPTP/Problems/ARI/ARI590=1.p
$TPTP/Problems/ARI/ARI591=1.p
$TPTP/Problems/ARI/ARI592=1.p
$TPTP/Problems/ARI/ARI593=1.p
$TPTP/Problems/ARI/ARI594=1.p
$TPTP/Problems/ARI/ARI595=1.p
$TPTP/Problems/ARI/ARI596=1.p
$TPTP/Problems/ARI/ARI597=1.p
$TPTP/Problems/ARI/ARI598=1.p
$TPTP/Problems/ARI/ARI599=1.p
$TPTP/Problems/ARI/ARI601=1.p
$TPTP/Problems/ARI/ARI602=1.p
$TPTP/Problems/ARI/ARI603=1.p
$TPTP/Problems/ARI/ARI604=1.p
$TPTP/Problems/ARI/ARI605=1.p
$TPTP/Problems/ARI/ARI606=1.p
$TPTP/Problems/ARI/ARI607=1.p
$TPTP/Problems/ARI/ARI608=1.p
$TPTP/Problems/ARI/ARI609=1.p
$TPTP/Problems/ARI/ARI610=1.p
$TPTP/Problems/ARI/ARI611=1.p
$TPTP/Problems/ARI/ARI612=1.p
$TPTP/Problems/ARI/ARI613=1.p
$TPTP/Problems/ARI/ARI614=1.p
$TPTP/Problems/ARI/ARI615=1.p
$TPTP/Problems/ARI/ARI616=1.p
$TPTP/Problems/ARI/ARI617=1.p
$TPTP/Problems/ARI/ARI618=1.p
$TPTP/Problems/ARI/ARI619=1.p
$TPTP/Problems/ARI/ARI619=2.p
$TPTP/Problems/ARI/ARI619=3.p
$TPTP/Problems/ARI/ARI620=1.p
$TPTP/Problems/ARI/ARI621=1.p
$TPTP/Problems/ARI/ARI621=2.p
$TPTP/Problems/ARI/ARI621=3.p
$TPTP/Problems/ARI/ARI622=1.p
$TPTP/Problems/ARI/ARI623=1.p
$TPTP/Problems/ARI/ARI624=1.p
$TPTP/Problems/ARI/ARI625=1.p