rwxr-xr-x 4273/0      0 Aug  4 23:29 1993 ATP_problems/
rw-r--r-- 4273/0   3672 Aug  4 23:17 1993 ATP_problems/README
rwxr-xr-x 4273/0      0 Aug  4 23:23 1993 ATP_problems/algebra/
rw-r--r-- 4273/0   2048 Aug  4 23:17 1993 ATP_problems/algebra/README
rwxr-xr-x 4273/0      0 Aug  4 23:19 1993 ATP_problems/algebra/boolean/
rw-r--r-- 4273/0   2259 Aug  4 23:17 1993 ATP_problems/algebra/boolean/README
rw-r--r-- 4273/0    787 Aug  4 23:17 1993 ATP_problems/algebra/boolean/prob1.desc
rw-r--r-- 4273/0   2511 Aug  4 23:17 1993 ATP_problems/algebra/boolean/prob1.ver1.clauses
rw-r--r-- 4273/0   2600 Aug  4 23:17 1993 ATP_problems/algebra/boolean/prob1.ver1.in
rw-r--r-- 4273/0   2547 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob1.ver1.out
rw-r--r-- 4273/0   1246 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob1.ver2.clauses
rw-r--r-- 4273/0   1902 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob1.ver2.in
rw-r--r-- 4273/0   2072 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob1.ver2.out
rw-r--r-- 4273/0   1285 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob2.desc
rw-r--r-- 4273/0   2355 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob2_part1.ver1.clauses
rw-r--r-- 4273/0   2591 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob2_part1.ver1.in
rw-r--r-- 4273/0   3781 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob2_part1.ver1.out
rw-r--r-- 4273/0   1036 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob2_part1.ver2.clauses
rw-r--r-- 4273/0   1859 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob2_part1.ver2.in
rw-r--r-- 4273/0   2912 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob2_part1.ver2.out
rw-r--r-- 4273/0   2423 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob2_part2.ver1.clauses
rw-r--r-- 4273/0   2542 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob2_part2.ver1.in
rw-r--r-- 4273/0   3725 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob2_part2.ver1.out
rw-r--r-- 4273/0   1034 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob2_part2.ver2.clauses
rw-r--r-- 4273/0   1710 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob2_part2.ver2.in
rw-r--r-- 4273/0   3487 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob2_part2.ver2.out
rw-r--r-- 4273/0   1253 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob3.desc
rw-r--r-- 4273/0   2364 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob3_part1.ver1.clauses
rw-r--r-- 4273/0   2548 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob3_part1.ver1.in
rw-r--r-- 4273/0   2568 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob3_part1.ver1.out
rw-r--r-- 4273/0   1468 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob3_part1.ver2.clauses
rw-r--r-- 4273/0   1682 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob3_part1.ver2.in
rw-r--r-- 4273/0   3152 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob3_part1.ver2.out
rw-r--r-- 4273/0   1261 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob4.desc
rw-r--r-- 4273/0   2366 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob3_part2.ver1.clauses
rw-r--r-- 4273/0   2555 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob3_part2.ver1.in
rw-r--r-- 4273/0   2602 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob3_part2.ver1.out
rw-r--r-- 4273/0   1469 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob3_part2.ver2.clauses
rw-r--r-- 4273/0   1683 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob3_part2.ver2.in
rw-r--r-- 4273/0   2916 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob3_part2.ver2.out
rw-r--r-- 4273/0   2384 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob4_part1.ver1.clauses
rw-r--r-- 4273/0   2474 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob4_part1.ver1.in
rw-r--r-- 4273/0   2467 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob4_part1.ver1.out
rw-r--r-- 4273/0   1484 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob4_part1.ver2.clauses
rw-r--r-- 4273/0   1698 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob4_part1.ver2.in
rw-r--r-- 4273/0   3186 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob4_part1.ver2.out
rw-r--r-- 4273/0   2360 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob4_part2.ver1.clauses
rw-r--r-- 4273/0   2449 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob4_part2.ver1.in
rw-r--r-- 4273/0   2518 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob4_part2.ver1.out
rw-r--r-- 4273/0   1484 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob4_part2.ver2.clauses
rw-r--r-- 4273/0   1698 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob4_part2.ver2.in
rw-r--r-- 4273/0   3459 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob4_part2.ver2.out
rw-r--r-- 4273/0    737 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob7.desc
rw-r--r-- 4273/0   2392 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob7.ver1.clauses
rw-r--r-- 4273/0   2486 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob7.ver1.in
rw-r--r-- 4273/0   3279 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob7.ver1.out
rw-r--r-- 4273/0   1461 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob7.ver2.clauses
rw-r--r-- 4273/0   1675 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob7.ver2.in
rw-r--r-- 4273/0   2726 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob7.ver2.out
rw-r--r-- 4273/0    722 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob8.desc
rw-r--r-- 4273/0   2370 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob8.ver1.clauses
rw-r--r-- 4273/0   2594 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob8.ver1.in
rw-r--r-- 4273/0   2613 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob8.ver1.out
rw-r--r-- 4273/0   1085 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob8.ver2.clauses
rw-r--r-- 4273/0   1694 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob8.ver2.in
rw-r--r-- 4273/0   2863 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob8.ver2.out
rw-r--r-- 4273/0    727 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob9.desc
rw-r--r-- 4273/0   2451 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob9.ver1.clauses
rw-r--r-- 4273/0   2546 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob9.ver1.in
rw-r--r-- 4273/0   2533 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob9.ver1.out
rw-r--r-- 4273/0   1153 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob9.ver2.clauses
rw-r--r-- 4273/0   1330 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob9.ver2.in
rw-r--r-- 4273/0   1551 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob9.ver2.out
rw-r--r-- 4273/0    721 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob_10.desc
rw-r--r-- 4273/0   2283 Aug  4 23:18 1993 ATP_problems/algebra/boolean/prob_10.ver1.clauses
rw-r--r-- 4273/0   2511 Aug  4 23:19 1993 ATP_problems/algebra/boolean/prob_10.ver1.in
rw-r--r-- 4273/0   3098 Aug  4 23:19 1993 ATP_problems/algebra/boolean/prob_10.ver1.out
rw-r--r-- 4273/0   1142 Aug  4 23:19 1993 ATP_problems/algebra/boolean/prob_10.ver2.clauses
rw-r--r-- 4273/0   1317 Aug  4 23:19 1993 ATP_problems/algebra/boolean/prob_10.ver2.in
rw-r--r-- 4273/0   2092 Aug  4 23:19 1993 ATP_problems/algebra/boolean/prob_10.ver2.out
rwxr-xr-x 4273/0      0 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/
rw-r--r-- 4273/0   3467 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/README
rw-r--r-- 4273/0   2435 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/axioms.mitchell
rw-r--r-- 4273/0   1157 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/axioms.quaife
rw-r--r-- 4273/0   3245 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/axioms.scott
rw-r--r-- 4273/0   1001 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p1.desc
rw-r--r-- 4273/0   2759 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p1.ver1.clauses
rw-r--r-- 4273/0   3064 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p1.ver1.in
rw-r--r-- 4273/0   3876 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p1.ver1.out
rw-r--r-- 4273/0   1207 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p1.ver2.clauses
rw-r--r-- 4273/0   1572 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p1.ver2.in
rw-r--r-- 4273/0   2441 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p1.ver2.out
rw-r--r-- 4273/0   2437 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p1.ver3.clauses
rw-r--r-- 4273/0   2691 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p1.ver3.in
rw-r--r-- 4273/0   2984 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p1.ver3.out
rw-r--r-- 4273/0    774 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p10.desc
rw-r--r-- 4273/0   2351 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p10.ver1.clauses
rw-r--r-- 4273/0   2516 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p10.ver1.in
rw-r--r-- 4273/0   3471 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p10.ver1.out
rw-r--r-- 4273/0   2349 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p10.ver3.clauses
rw-r--r-- 4273/0   2683 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p10.ver3.in
rw-r--r-- 4273/0   2487 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p10.ver3.out
rw-r--r-- 4273/0    972 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p11.desc
rw-r--r-- 4273/0   2311 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p11.ver1.clauses
rw-r--r-- 4273/0   2405 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p11.ver1.in
rw-r--r-- 4273/0   3015 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p11.ver1.out
rw-r--r-- 4273/0    899 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p11.ver2.clauses
rw-r--r-- 4273/0   1244 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p11.ver2.in
rw-r--r-- 4273/0   2432 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p11.ver2.out
rw-r--r-- 4273/0   2334 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p11.ver3.clauses
rw-r--r-- 4273/0   2544 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p11.ver3.in
rw-r--r-- 4273/0   2275 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p11.ver3.out
rw-r--r-- 4273/0    753 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p12.desc
rw-r--r-- 4273/0   2311 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p12.ver1.clauses
rw-r--r-- 4273/0   2405 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p12.ver1.in
rw-r--r-- 4273/0   3011 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p12.ver1.out
rw-r--r-- 4273/0   2335 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p12.ver3.clauses
rw-r--r-- 4273/0   2668 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p12.ver3.in
rw-r--r-- 4273/0   2364 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p12.ver3.out
rw-r--r-- 4273/0    753 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p13.desc
rw-r--r-- 4273/0   2311 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p13.ver1.clauses
rw-r--r-- 4273/0   2405 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p13.ver1.in
rw-r--r-- 4273/0   3011 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p13.ver1.out
rw-r--r-- 4273/0   2331 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p13.ver3.clauses
rw-r--r-- 4273/0   2629 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p13.ver3.in
rw-r--r-- 4273/0   2533 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p13.ver3.out
rw-r--r-- 4273/0    972 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p14.desc
rw-r--r-- 4273/0   2311 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p14.ver1.clauses
rw-r--r-- 4273/0   2405 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p14.ver1.in
rw-r--r-- 4273/0   3016 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p14.ver1.out
rw-r--r-- 4273/0    900 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p14.ver2.clauses
rw-r--r-- 4273/0   1244 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p14.ver2.in
rw-r--r-- 4273/0   2432 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p14.ver2.out
rw-r--r-- 4273/0   2332 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p14.ver3.clauses
rw-r--r-- 4273/0   2666 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p14.ver3.in
rw-r--r-- 4273/0   2398 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p14.ver3.out
rw-r--r-- 4273/0   2401 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p15.desc
rw-r--r-- 4273/0   1869 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p15.related.clauses
rw-r--r-- 4273/0   2358 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p15.related.in
rw-r--r-- 4273/0   4351 Aug  4 23:19 1993 ATP_problems/algebra/category.theory/p15.related.out
rw-r--r-- 4273/0   2728 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p15.ver1.clauses
rw-r--r-- 4273/0   2901 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p15.ver1.in
rw-r--r-- 4273/0   3461 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p15.ver1.out
rw-r--r-- 4273/0    982 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p15.ver2.clauses
rw-r--r-- 4273/0   1336 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p15.ver2.in
rw-r--r-- 4273/0   2318 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p15.ver2.out
rw-r--r-- 4273/0   2644 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p15.ver3.no1.clauses
rw-r--r-- 4273/0   2845 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p15.ver3.no1.in
rw-r--r-- 4273/0   3414 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p15.ver3.no1.out
rw-r--r-- 4273/0   2368 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p15.ver3.no2.clauses
rw-r--r-- 4273/0   2536 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p15.ver3.no2.in
rw-r--r-- 4273/0   2371 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p15.ver3.no2.out
rw-r--r-- 4273/0   2368 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p15.ver3.no3.clauses
rw-r--r-- 4273/0   2548 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p15.ver3.no3.in
rw-r--r-- 4273/0   2363 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p15.ver3.no3.out
rw-r--r-- 4273/0   2352 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p15.ver3.no4.clauses
rw-r--r-- 4273/0   2586 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p15.ver3.no4.in
rw-r--r-- 4273/0   2189 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p15.ver3.no4.out
rw-r--r-- 4273/0    559 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p16.desc
rw-r--r-- 4273/0   2326 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p16.ver3.clauses
rw-r--r-- 4273/0   2499 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p16.ver3.in
rw-r--r-- 4273/0   2422 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p16.ver3.out
rw-r--r-- 4273/0    559 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p17.desc
rw-r--r-- 4273/0   2325 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p17.ver3.clauses
rw-r--r-- 4273/0   2498 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p17.ver3.in
rw-r--r-- 4273/0   2424 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p17.ver3.out
rw-r--r-- 4273/0    803 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p18.desc
rw-r--r-- 4273/0   2530 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p18.ver1.in
rw-r--r-- 4273/0   2365 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p18.ver1.clauses
rw-r--r-- 4273/0   2942 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p18.ver1.out
rw-r--r-- 4273/0   2364 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p18.ver3.clauses
rw-r--r-- 4273/0   2537 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p18.ver3.in
rw-r--r-- 4273/0   3852 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p18.ver3.out
rw-r--r-- 4273/0   1070 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p2.desc
rw-r--r-- 4273/0   2487 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p2.ver1.clauses
rw-r--r-- 4273/0   2789 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p2.ver1.in
rw-r--r-- 4273/0   4230 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p2.ver1.out
rw-r--r-- 4273/0   1350 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p2.ver2.clauses
rw-r--r-- 4273/0   1715 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p2.ver2.in
rw-r--r-- 4273/0   2508 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p2.ver2.out
rw-r--r-- 4273/0   2479 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p2.ver3.clauses
rw-r--r-- 4273/0   2775 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p2.ver3.in
rw-r--r-- 4273/0   3331 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p2.ver3.out
rw-r--r-- 4273/0   1002 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p3.desc
rw-r--r-- 4273/0   2828 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p3.ver1.clauses
rw-r--r-- 4273/0   3132 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p3.ver1.in
rw-r--r-- 4273/0   3864 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p3.ver1.out
rw-r--r-- 4273/0   1206 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p3.ver2.clauses
rw-r--r-- 4273/0   1571 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p3.ver2.in
rw-r--r-- 4273/0   2441 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p3.ver2.out
rw-r--r-- 4273/0   2442 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p3.ver3.clauses
rw-r--r-- 4273/0   2696 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p3.ver3.in
rw-r--r-- 4273/0   2867 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p3.ver3.out
rw-r--r-- 4273/0   1032 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p4.desc
rw-r--r-- 4273/0   2566 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p4.ver1.clauses
rw-r--r-- 4273/0   2870 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p4.ver1.in
rw-r--r-- 4273/0   4230 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p4.ver1.out
rw-r--r-- 4273/0   1325 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p4.ver2.clauses
rw-r--r-- 4273/0   1690 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p4.ver2.in
rw-r--r-- 4273/0   2535 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p4.ver2.out
rw-r--r-- 4273/0   2487 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p4.ver3.clauses
rw-r--r-- 4273/0   2784 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p4.ver3.in
rw-r--r-- 4273/0   3314 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p4.ver3.out
rw-r--r-- 4273/0    767 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p5.desc
rw-r--r-- 4273/0   2505 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p5.ver1.clauses
rw-r--r-- 4273/0   2667 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p5.ver1.in
rw-r--r-- 4273/0   3246 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p5.ver1.out
rw-r--r-- 4273/0   2451 Aug  4 23:20 1993 ATP_problems/algebra/category.theory/p5.ver3.clauses
rw-r--r-- 4273/0   2622 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p5.ver3.in
rw-r--r-- 4273/0   3519 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p5.ver3.out
rw-r--r-- 4273/0    766 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p6.desc
rw-r--r-- 4273/0   2368 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p6.ver1.clauses
rw-r--r-- 4273/0   2533 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p6.ver1.in
rw-r--r-- 4273/0   3247 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p6.ver1.out
rw-r--r-- 4273/0   2444 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p6.ver3.clauses
rw-r--r-- 4273/0   2617 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p6.ver3.in
rw-r--r-- 4273/0   3481 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p6.ver3.out
rw-r--r-- 4273/0    771 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p7.desc
rw-r--r-- 4273/0   2386 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p7.ver1.clauses
rw-r--r-- 4273/0   2551 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p7.ver1.in
rw-r--r-- 4273/0   3094 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p7.ver1.out
rw-r--r-- 4273/0   2453 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p7.ver3.clauses
rw-r--r-- 4273/0   2634 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p7.ver3.in
rw-r--r-- 4273/0   1978 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p7.ver3.out
rw-r--r-- 4273/0    576 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p8.desc
rw-r--r-- 4273/0   2382 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p8.ver1.clauses
rw-r--r-- 4273/0   2547 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p8.ver1.in
rw-r--r-- 4273/0   3473 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p8.ver1.out
rw-r--r-- 4273/0    769 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p9.desc
rw-r--r-- 4273/0   2349 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p9.ver1.clauses
rw-r--r-- 4273/0   2514 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p9.ver1.in
rw-r--r-- 4273/0   3507 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p9.ver1.out
rw-r--r-- 4273/0   2340 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p9.ver3.clauses
rw-r--r-- 4273/0   2673 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p9.ver3.in
rw-r--r-- 4273/0   2487 Aug  4 23:21 1993 ATP_problems/algebra/category.theory/p9.ver3.out
rwxr-xr-x 4273/0      0 Aug  4 23:22 1993 ATP_problems/algebra/groups/
rw-r--r-- 4273/0   1597 Aug  4 23:21 1993 ATP_problems/algebra/groups/Group.ax.eq.clauses
rw-r--r-- 4273/0   2730 Aug  4 23:21 1993 ATP_problems/algebra/groups/Group.ax.g.clauses
rw-r--r-- 4273/0   1635 Aug  4 23:21 1993 ATP_problems/algebra/groups/Group.ax.p.clauses
rw-r--r-- 4273/0    779 Aug  4 23:21 1993 ATP_problems/algebra/groups/Lemmas.eq.clauses
rw-r--r-- 4273/0    878 Aug  4 23:21 1993 ATP_problems/algebra/groups/Lemmas.p.clauses
rw-r--r-- 4273/0   4296 Aug  4 23:21 1993 ATP_problems/algebra/groups/README
rw-r--r-- 4273/0    792 Aug  4 23:21 1993 ATP_problems/algebra/groups/commutator.desc
rw-r--r-- 4273/0   1754 Aug  4 23:21 1993 ATP_problems/algebra/groups/commutator.ver1.clauses
rw-r--r-- 4273/0   2039 Aug  4 23:21 1993 ATP_problems/algebra/groups/commutator.ver1.in
rw-r--r-- 4273/0   1598 Aug  4 23:21 1993 ATP_problems/algebra/groups/commutator.ver2.clauses
rw-r--r-- 4273/0   1848 Aug  4 23:21 1993 ATP_problems/algebra/groups/commutator.ver2.in
rw-r--r-- 4273/0    730 Aug  4 23:21 1993 ATP_problems/algebra/groups/cyclic.desc
rw-r--r-- 4273/0   3819 Aug  4 23:21 1993 ATP_problems/algebra/groups/cyclic.ver3.in
rw-r--r-- 4273/0   4657 Aug  4 23:21 1993 ATP_problems/algebra/groups/cyclic.ver3.out
rw-r--r-- 4273/0    544 Aug  4 23:21 1993 ATP_problems/algebra/groups/ident1.desc
rw-r--r-- 4273/0   1804 Aug  4 23:21 1993 ATP_problems/algebra/groups/ident1.ver1.clauses
rw-r--r-- 4273/0   1942 Aug  4 23:21 1993 ATP_problems/algebra/groups/ident1.ver1.in
rw-r--r-- 4273/0   7513 Aug  4 23:21 1993 ATP_problems/algebra/groups/ident1.ver1.out
rw-r--r-- 4273/0    693 Aug  4 23:21 1993 ATP_problems/algebra/groups/ident2.desc
rw-r--r-- 4273/0   2025 Aug  4 23:21 1993 ATP_problems/algebra/groups/ident2.ver1.clauses
rw-r--r-- 4273/0   2162 Aug  4 23:21 1993 ATP_problems/algebra/groups/ident2.ver1.in
rw-r--r-- 4273/0   7982 Aug  4 23:21 1993 ATP_problems/algebra/groups/ident2.ver1.out
rw-r--r-- 4273/0   1646 Aug  4 23:21 1993 ATP_problems/algebra/groups/index.desc
rw-r--r-- 4273/0   3030 Aug  4 23:21 1993 ATP_problems/algebra/groups/index.ver1.clauses
rw-r--r-- 4273/0   3427 Aug  4 23:21 1993 ATP_problems/algebra/groups/index.ver1.in
rw-r--r-- 4273/0   4390 Aug  4 23:21 1993 ATP_problems/algebra/groups/index.ver1.out
rw-r--r-- 4273/0   2707 Aug  4 23:21 1993 ATP_problems/algebra/groups/index.ver2.clauses
rw-r--r-- 4273/0   3044 Aug  4 23:21 1993 ATP_problems/algebra/groups/index.ver2.in
rw-r--r-- 4273/0    426 Aug  4 23:21 1993 ATP_problems/algebra/groups/invers1.desc
rw-r--r-- 4273/0   1790 Aug  4 23:21 1993 ATP_problems/algebra/groups/invers1.ver1.clauses
rw-r--r-- 4273/0   1927 Aug  4 23:21 1993 ATP_problems/algebra/groups/invers1.ver1.in
rw-r--r-- 4273/0   8624 Aug  4 23:21 1993 ATP_problems/algebra/groups/invers1.ver1.out
rw-r--r-- 4273/0    517 Aug  4 23:21 1993 ATP_problems/algebra/groups/invers2.desc
rw-r--r-- 4273/0   1906 Aug  4 23:21 1993 ATP_problems/algebra/groups/invers2.ver1.in
rw-r--r-- 4273/0   1678 Aug  4 23:21 1993 ATP_problems/algebra/groups/invers2.ver1.clauses
rw-r--r-- 4273/0   7991 Aug  4 23:21 1993 ATP_problems/algebra/groups/invers2.ver1.out
rw-r--r-- 4273/0   1643 Aug  4 23:21 1993 ATP_problems/algebra/groups/order2.desc
rw-r--r-- 4273/0   3314 Aug  4 23:21 1993 ATP_problems/algebra/groups/order2.ver3.clauses
rw-r--r-- 4273/0   3646 Aug  4 23:21 1993 ATP_problems/algebra/groups/order2.ver3.in
rw-r--r-- 4273/0   5641 Aug  4 23:21 1993 ATP_problems/algebra/groups/order2.ver3.out
rw-r--r-- 4273/0   4524 Aug  4 23:21 1993 ATP_problems/algebra/groups/order2.ver4.clauses
rw-r--r-- 4273/0   4897 Aug  4 23:21 1993 ATP_problems/algebra/groups/order2.ver4.in
rw-r--r-- 4273/0   5773 Aug  4 23:21 1993 ATP_problems/algebra/groups/order2.ver4.out
rw-r--r-- 4273/0   1623 Aug  4 23:21 1993 ATP_problems/algebra/groups/order3.desc
rw-r--r-- 4273/0   3532 Aug  4 23:21 1993 ATP_problems/algebra/groups/order3.ver3.clauses
rw-r--r-- 4273/0   3864 Aug  4 23:21 1993 ATP_problems/algebra/groups/order3.ver3.in
rw-r--r-- 4273/0   5487 Aug  4 23:21 1993 ATP_problems/algebra/groups/order3.ver3.out
rw-r--r-- 4273/0   5359 Aug  4 23:22 1993 ATP_problems/algebra/groups/order3.ver4.clauses
rw-r--r-- 4273/0   5923 Aug  4 23:22 1993 ATP_problems/algebra/groups/order3.ver4.in
rw-r--r-- 4273/0   6732 Aug  4 23:22 1993 ATP_problems/algebra/groups/order3.ver4.out
rw-r--r-- 4273/0    621 Aug  4 23:22 1993 ATP_problems/algebra/groups/xsquared.desc
rw-r--r-- 4273/0   1682 Aug  4 23:22 1993 ATP_problems/algebra/groups/xsquared.ver1.clauses
rw-r--r-- 4273/0   1961 Aug  4 23:22 1993 ATP_problems/algebra/groups/xsquared.ver1.in
rw-r--r-- 4273/0   7897 Aug  4 23:22 1993 ATP_problems/algebra/groups/xsquared.ver1.out
rw-r--r-- 4273/0   1536 Aug  4 23:22 1993 ATP_problems/algebra/groups/xsquared.ver2.clauses
rw-r--r-- 4273/0   1785 Aug  4 23:22 1993 ATP_problems/algebra/groups/xsquared.ver2.in
rw-r--r-- 4273/0  10666 Aug  4 23:22 1993 ATP_problems/algebra/groups/xsquared.ver2.out
rwxr-xr-x 4273/0      0 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/
rw-r--r-- 4273/0   2847 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/README
rw-r--r-- 4273/0   1798 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/axioms.ver1
rw-r--r-- 4273/0   1285 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/axioms.ver2
rw-r--r-- 4273/0   1506 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/axioms.ver3
rw-r--r-- 4273/0    715 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp1.desc
rw-r--r-- 4273/0   1518 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp1.ver1.clauses
rw-r--r-- 4273/0   1583 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp1.ver1.in
rw-r--r-- 4273/0   2272 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp1.ver1.out
rw-r--r-- 4273/0   1062 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp1.ver2.clauses
rw-r--r-- 4273/0   1127 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp1.ver2.in
rw-r--r-- 4273/0   1852 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp1.ver2.out
rw-r--r-- 4273/0   1017 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp1.ver3.clauses
rw-r--r-- 4273/0   1146 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp1.ver3.in
rw-r--r-- 4273/0   1768 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp1.ver3.out
rw-r--r-- 4273/0    842 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp10.desc
rw-r--r-- 4273/0   1745 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp10.ver1.clauses
rw-r--r-- 4273/0   2075 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp10.ver1.in
rw-r--r-- 4273/0   3288 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp10.ver1.out
rw-r--r-- 4273/0   1338 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp10.ver2.clauses
rw-r--r-- 4273/0   1584 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp10.ver2.in
rw-r--r-- 4273/0    969 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp10.ver2.out
rw-r--r-- 4273/0   1251 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp10.ver3.clauses
rw-r--r-- 4273/0   1614 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp10.ver3.in
rw-r--r-- 4273/0   3193 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp10.ver3.out
rw-r--r-- 4273/0    933 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp11.desc
rw-r--r-- 4273/0   2443 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp11.ver1.clauses
rw-r--r-- 4273/0   2906 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp11.ver1.in
rw-r--r-- 4273/0   3072 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp11.ver1.out
rw-r--r-- 4273/0   1580 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp11.ver2.clauses
rw-r--r-- 4273/0   1915 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp11.ver2.in
rw-r--r-- 4273/0   4244 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp11.ver2.out
rw-r--r-- 4273/0   1535 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp11.ver3.clauses
rw-r--r-- 4273/0   2138 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp11.ver3.in
rw-r--r-- 4273/0   2773 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp11.ver3.out
rw-r--r-- 4273/0    715 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp2.desc
rw-r--r-- 4273/0   1518 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp2.ver1.clauses
rw-r--r-- 4273/0   1582 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp2.ver1.in
rw-r--r-- 4273/0   2272 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp2.ver1.out
rw-r--r-- 4273/0   1126 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp2.ver2.in
rw-r--r-- 4273/0   1061 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp2.ver2.clauses
rw-r--r-- 4273/0   1922 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp2.ver2.out
rw-r--r-- 4273/0   1018 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp2.ver3.clauses
rw-r--r-- 4273/0   1147 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp2.ver3.in
rw-r--r-- 4273/0   1769 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp2.ver3.out
rw-r--r-- 4273/0    754 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp3.desc
rw-r--r-- 4273/0   1555 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp3.ver1.clauses
rw-r--r-- 4273/0   1621 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp3.ver1.in
rw-r--r-- 4273/0  16354 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp3.ver1.out
rw-r--r-- 4273/0   1106 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp3.ver2.clauses
rw-r--r-- 4273/0   1296 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp3.ver2.in
rw-r--r-- 4273/0  19650 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp3.ver2.out
rw-r--r-- 4273/0   1017 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp3.ver3.clauses
rw-r--r-- 4273/0   1249 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp3.ver3.in
rw-r--r-- 4273/0   2174 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp3.ver3.out
rw-r--r-- 4273/0    774 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp4.desc
rw-r--r-- 4273/0   1634 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp4.ver1.clauses
rw-r--r-- 4273/0   1734 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp4.ver1.in
rw-r--r-- 4273/0  13077 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp4.ver1.out
rw-r--r-- 4273/0   1106 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp4.ver2.clauses
rw-r--r-- 4273/0   1296 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp4.ver2.in
rw-r--r-- 4273/0   3045 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp4.ver2.out
rw-r--r-- 4273/0   1040 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp4.ver3.clauses
rw-r--r-- 4273/0   1286 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp4.ver3.in
rw-r--r-- 4273/0   2415 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp4.ver3.out
rw-r--r-- 4273/0    795 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp5.desc
rw-r--r-- 4273/0   1533 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp5.ver1.clauses
rw-r--r-- 4273/0   1613 Aug  4 23:22 1993 ATP_problems/algebra/henkin.models/hp5.ver1.in
rw-r--r-- 4273/0   2929 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp5.ver1.out
rw-r--r-- 4273/0   1117 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp5.ver2.clauses
rw-r--r-- 4273/0   1326 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp5.ver2.in
rw-r--r-- 4273/0   9300 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp5.ver2.out
rw-r--r-- 4273/0   1043 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp5.ver3.clauses
rw-r--r-- 4273/0   1306 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp5.ver3.in
rw-r--r-- 4273/0   2305 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp5.ver3.out
rw-r--r-- 4273/0    804 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp6.desc
rw-r--r-- 4273/0   1703 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp6.ver1.clauses
rw-r--r-- 4273/0   1887 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp6.ver1.in
rw-r--r-- 4273/0   3190 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp6.ver1.out
rw-r--r-- 4273/0   1151 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp6.ver2.clauses
rw-r--r-- 4273/0   1374 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp6.ver2.in
rw-r--r-- 4273/0   2806 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp6.ver2.out
rw-r--r-- 4273/0   1072 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp6.ver3.clauses
rw-r--r-- 4273/0   1308 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp6.ver3.in
rw-r--r-- 4273/0   2502 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp6.ver3.out
rw-r--r-- 4273/0    827 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp7.desc
rw-r--r-- 4273/0   1703 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp7.ver1.clauses
rw-r--r-- 4273/0   1927 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp7.ver1.in
rw-r--r-- 4273/0   2914 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp7.ver1.out
rw-r--r-- 4273/0   1253 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp7.ver2.clauses
rw-r--r-- 4273/0   1506 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp7.ver2.in
rw-r--r-- 4273/0   2421 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp7.ver2.out
rw-r--r-- 4273/0   1103 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp7.ver3.clauses
rw-r--r-- 4273/0   1365 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp7.ver3.in
rw-r--r-- 4273/0   2240 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp7.ver3.out
rw-r--r-- 4273/0    784 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp8.desc
rw-r--r-- 4273/0   1554 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp8.ver1.clauses
rw-r--r-- 4273/0   1635 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp8.ver1.in
rw-r--r-- 4273/0  25857 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp8.ver1.out
rw-r--r-- 4273/0   1151 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp8.ver2.clauses
rw-r--r-- 4273/0   1358 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp8.ver2.in
rw-r--r-- 4273/0   4202 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp8.ver2.out
rw-r--r-- 4273/0   1048 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp8.ver3.clauses
rw-r--r-- 4273/0   1297 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp8.ver3.in
rw-r--r-- 4273/0   2046 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp8.ver3.out
rw-r--r-- 4273/0    791 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp9.desc
rw-r--r-- 4273/0   1738 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp9.ver1.clauses
rw-r--r-- 4273/0   2068 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp9.ver1.in
rw-r--r-- 4273/0   3230 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp9.ver1.out
rw-r--r-- 4273/0   1277 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp9.ver2.clauses
rw-r--r-- 4273/0   1500 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp9.ver2.in
rw-r--r-- 4273/0   3570 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp9.ver2.out
rw-r--r-- 4273/0   1239 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp9.ver3.clauses
rw-r--r-- 4273/0   1517 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp9.ver3.in
rw-r--r-- 4273/0   2980 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/hp9.ver3.out
rw-r--r-- 4273/0    547 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/new.desc
rw-r--r-- 4273/0   1516 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/new.ver1.clauses
rw-r--r-- 4273/0   1580 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/new.ver1.in
rw-r--r-- 4273/0   2665 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/new.ver1.out
rw-r--r-- 4273/0   1059 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/new.ver2.clauses
rw-r--r-- 4273/0   1152 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/new.ver2.in
rw-r--r-- 4273/0   1891 Aug  4 23:23 1993 ATP_problems/algebra/henkin.models/new.ver2.out
rwxr-xr-x 4273/0      0 Aug  4 23:23 1993 ATP_problems/algebra/lattices/
rw-r--r-- 4273/0   1748 Aug  4 23:23 1993 ATP_problems/algebra/lattices/README
rw-r--r-- 4273/0   3369 Aug  4 23:23 1993 ATP_problems/algebra/lattices/SAMslemma.desc
rw-r--r-- 4273/0   4317 Aug  4 23:23 1993 ATP_problems/algebra/lattices/SAMslemma.ver1.clauses
rw-r--r-- 4273/0   4212 Aug  4 23:23 1993 ATP_problems/algebra/lattices/SAMslemma.ver1.in
rw-r--r-- 4273/0   4584 Aug  4 23:23 1993 ATP_problems/algebra/lattices/SAMslemma.ver1.out
rwxr-xr-x 4273/0      0 Aug  4 23:24 1993 ATP_problems/algebra/rings/
rw-r--r-- 4273/0   2749 Aug  4 23:23 1993 ATP_problems/algebra/rings/README
rw-r--r-- 4273/0   2327 Aug  4 23:23 1993 ATP_problems/algebra/rings/Ring.axioms.clauses
rw-r--r-- 4273/0    905 Aug  4 23:23 1993 ATP_problems/algebra/rings/Ring.lemmas.clauses
rw-r--r-- 4273/0   1208 Aug  4 23:23 1993 ATP_problems/algebra/rings/Stickel.eq.clauses
rw-r--r-- 4273/0   1403 Aug  4 23:23 1993 ATP_problems/algebra/rings/Stickel.p.clauses
rw-r--r-- 4273/0   1657 Aug  4 23:23 1993 ATP_problems/algebra/rings/commute.desc
rw-r--r-- 4273/0   2220 Aug  4 23:23 1993 ATP_problems/algebra/rings/commute.proofs
rw-r--r-- 4273/0   3281 Aug  4 23:23 1993 ATP_problems/algebra/rings/commute.ver1.clauses
rw-r--r-- 4273/0   3529 Aug  4 23:23 1993 ATP_problems/algebra/rings/commute.ver1.in
rw-r--r-- 4273/0  77661 Aug  4 23:23 1993 ATP_problems/algebra/rings/commute.ver1.out
rw-r--r-- 4273/0   1823 Aug  4 23:23 1993 ATP_problems/algebra/rings/commute.ver2.clauses
rw-r--r-- 4273/0   2451 Aug  4 23:23 1993 ATP_problems/algebra/rings/commute.ver2.in
rw-r--r-- 4273/0 263261 Aug  4 23:23 1993 ATP_problems/algebra/rings/commute.ver2.out
rw-r--r-- 4273/0   2488 Aug  4 23:23 1993 ATP_problems/algebra/rings/commute.ver3.clauses
rw-r--r-- 4273/0   2576 Aug  4 23:24 1993 ATP_problems/algebra/rings/commute.ver3.in
rw-r--r-- 4273/0  63382 Aug  4 23:24 1993 ATP_problems/algebra/rings/commute.ver3.out
rw-r--r-- 4273/0   2566 Aug  4 23:24 1993 ATP_problems/algebra/rings/commute.ver4.clauses
rw-r--r-- 4273/0   2756 Aug  4 23:24 1993 ATP_problems/algebra/rings/commute.ver4.in
rw-r--r-- 4273/0  59307 Aug  4 23:24 1993 ATP_problems/algebra/rings/commute.ver4.out
rw-r--r-- 4273/0   1601 Aug  4 23:24 1993 ATP_problems/algebra/rings/lemma.desc
rw-r--r-- 4273/0   2828 Aug  4 23:24 1993 ATP_problems/algebra/rings/lemma.ver1.clauses
rw-r--r-- 4273/0   3393 Aug  4 23:24 1993 ATP_problems/algebra/rings/lemma.ver1.in
rw-r--r-- 4273/0   4736 Aug  4 23:24 1993 ATP_problems/algebra/rings/lemma.ver1.out
rw-r--r-- 4273/0   1616 Aug  4 23:24 1993 ATP_problems/algebra/rings/lemma.ver2.clauses
rw-r--r-- 4273/0   2219 Aug  4 23:24 1993 ATP_problems/algebra/rings/lemma.ver2.in
rw-r--r-- 4273/0   3751 Aug  4 23:24 1993 ATP_problems/algebra/rings/lemma.ver2.out
rw-r--r-- 4273/0   2398 Aug  4 23:24 1993 ATP_problems/algebra/rings/lemma.ver3.clauses
rw-r--r-- 4273/0   2485 Aug  4 23:24 1993 ATP_problems/algebra/rings/lemma.ver3.in
rw-r--r-- 4273/0  66208 Aug  4 23:24 1993 ATP_problems/algebra/rings/lemma.ver3.out
rw-r--r-- 4273/0   2477 Aug  4 23:24 1993 ATP_problems/algebra/rings/lemma.ver4.clauses
rw-r--r-- 4273/0   2665 Aug  4 23:24 1993 ATP_problems/algebra/rings/lemma.ver4.in
rw-r--r-- 4273/0  63547 Aug  4 23:24 1993 ATP_problems/algebra/rings/lemma.ver4.out
rw-r--r-- 4273/0    715 Aug  4 23:24 1993 ATP_problems/algebra/rings/minuses.desc
rw-r--r-- 4273/0   2176 Aug  4 23:24 1993 ATP_problems/algebra/rings/minuses.ver1.clauses
rw-r--r-- 4273/0   2264 Aug  4 23:24 1993 ATP_problems/algebra/rings/minuses.ver1.in
rw-r--r-- 4273/0  57054 Aug  4 23:24 1993 ATP_problems/algebra/rings/minuses.ver1.out
rw-r--r-- 4273/0   2256 Aug  4 23:24 1993 ATP_problems/algebra/rings/minuses.ver2.clauses
rw-r--r-- 4273/0   2442 Aug  4 23:24 1993 ATP_problems/algebra/rings/minuses.ver2.in
rw-r--r-- 4273/0   4537 Aug  4 23:24 1993 ATP_problems/algebra/rings/minuses.ver2.out
rw-r--r-- 4273/0    748 Aug  4 23:24 1993 ATP_problems/algebra/rings/zero.desc
rw-r--r-- 4273/0   2112 Aug  4 23:24 1993 ATP_problems/algebra/rings/zero.ver1.clauses
rw-r--r-- 4273/0   2177 Aug  4 23:24 1993 ATP_problems/algebra/rings/zero.ver1.in
rw-r--r-- 4273/0   3930 Aug  4 23:24 1993 ATP_problems/algebra/rings/zero.ver1.out
rw-r--r-- 4273/0   2141 Aug  4 23:24 1993 ATP_problems/algebra/rings/zero.ver2.clauses
rw-r--r-- 4273/0   2231 Aug  4 23:24 1993 ATP_problems/algebra/rings/zero.ver2.in
rw-r--r-- 4273/0   3985 Aug  4 23:24 1993 ATP_problems/algebra/rings/zero.ver2.out
rwxr-xr-x 4273/0      0 Aug  4 23:24 1993 ATP_problems/analysis/
rw-r--r-- 4273/0   1868 Aug  4 23:24 1993 ATP_problems/analysis/README
rwxr-xr-x 4273/0      0 Aug  4 23:24 1993 ATP_problems/analysis/limits/
rw-r--r-- 4273/0   1994 Aug  4 23:24 1993 ATP_problems/analysis/limits/README
rw-r--r-- 4273/0   1657 Aug  4 23:24 1993 ATP_problems/analysis/limits/axioms.clauses
rw-r--r-- 4273/0   1077 Aug  4 23:24 1993 ATP_problems/analysis/limits/prob1.desc
rw-r--r-- 4273/0   1286 Aug  4 23:24 1993 ATP_problems/analysis/limits/prob1.ver1.clauses
rw-r--r-- 4273/0   1377 Aug  4 23:24 1993 ATP_problems/analysis/limits/prob1.ver1.in
rw-r--r-- 4273/0  69963 Aug  4 23:24 1993 ATP_problems/analysis/limits/prob1.ver1.out
rw-r--r-- 4273/0   2081 Aug  4 23:24 1993 ATP_problems/analysis/limits/prob1.ver2.clauses
rw-r--r-- 4273/0   2182 Aug  4 23:24 1993 ATP_problems/analysis/limits/prob1.ver2.in
rw-r--r-- 4273/0  70955 Aug  4 23:24 1993 ATP_problems/analysis/limits/prob1.ver2.out
rw-r--r-- 4273/0    640 Aug  4 23:24 1993 ATP_problems/analysis/limits/prob2.desc
rw-r--r-- 4273/0   1191 Aug  4 23:24 1993 ATP_problems/analysis/limits/prob2.ver1.clauses
rw-r--r-- 4273/0   1281 Aug  4 23:24 1993 ATP_problems/analysis/limits/prob2.ver1.in
rw-r--r-- 4273/0  69854 Aug  4 23:24 1993 ATP_problems/analysis/limits/prob2.ver1.out
rwxr-xr-x 4273/0      0 Aug  4 23:24 1993 ATP_problems/circuits/
rw-r--r-- 4273/0   2184 Aug  4 23:24 1993 ATP_problems/circuits/README
rw-r--r-- 4273/0    450 Aug  4 23:24 1993 ATP_problems/circuits/design_or.desc
rw-r--r-- 4273/0    608 Aug  4 23:24 1993 ATP_problems/circuits/design_or.ver1
rw-r--r-- 4273/0    506 Aug  4 23:24 1993 ATP_problems/circuits/design_or.ver1.clauses
rw-r--r-- 4273/0   3143 Aug  4 23:24 1993 ATP_problems/circuits/design_or.ver1.out
rw-r--r-- 4273/0    518 Aug  4 23:24 1993 ATP_problems/circuits/intchg_val.desc
rw-r--r-- 4273/0   1910 Aug  4 23:24 1993 ATP_problems/circuits/intchg_val.ver1
rw-r--r-- 4273/0   1771 Aug  4 23:24 1993 ATP_problems/circuits/intchg_val.ver1.clauses
rw-r--r-- 4273/0   4186 Aug  4 23:24 1993 ATP_problems/circuits/intchg_val.ver1.out
rw-r--r-- 4273/0    533 Aug  4 23:24 1993 ATP_problems/circuits/interchange.desc
rw-r--r-- 4273/0   3288 Aug  4 23:24 1993 ATP_problems/circuits/interchange.ver1.clauses
rw-r--r-- 4273/0   3392 Aug  4 23:24 1993 ATP_problems/circuits/interchange.ver1.in
rw-r--r-- 4273/0   6891 Aug  4 23:24 1993 ATP_problems/circuits/interchange.ver1.out
rw-r--r-- 4273/0   1045 Aug  4 23:24 1993 ATP_problems/circuits/two.inverter.desc
rw-r--r-- 4273/0    848 Aug  4 23:24 1993 ATP_problems/circuits/two.inverter.val.desc
rw-r--r-- 4273/0   1950 Aug  4 23:24 1993 ATP_problems/circuits/two.inverter.val.ver1.clauses
rw-r--r-- 4273/0   2046 Aug  4 23:24 1993 ATP_problems/circuits/two.inverter.val.ver1.in
rw-r--r-- 4273/0   4235 Aug  4 23:24 1993 ATP_problems/circuits/two.inverter.val.ver1.out
rw-r--r-- 4273/0   2550 Aug  4 23:24 1993 ATP_problems/circuits/two.inverter.ver1.clauses
rw-r--r-- 4273/0   2660 Aug  4 23:24 1993 ATP_problems/circuits/two.inverter.ver1.in
rw-r--r-- 4273/0    143 Aug  4 23:24 1993 ATP_problems/circuits/two.inverter.ver1.out
rw-r--r-- 4273/0   2422 Aug  4 23:24 1993 ATP_problems/circuits/two.inverter.ver2.clauses
rw-r--r-- 4273/0   2524 Aug  4 23:24 1993 ATP_problems/circuits/two.inverter.ver2.in
rw-r--r-- 4273/0    143 Aug  4 23:24 1993 ATP_problems/circuits/two.inverter.ver2.out
rwxr-xr-x 4273/0      0 Aug  4 23:25 1993 ATP_problems/geometry/
rw-r--r-- 4273/0   3876 Aug  4 23:25 1993 ATP_problems/geometry/README
rw-r--r-- 4273/0   5075 Aug  4 23:25 1993 ATP_problems/geometry/axioms.ver1
rw-r--r-- 4273/0   3568 Aug  4 23:25 1993 ATP_problems/geometry/axioms.ver2
rw-r--r-- 4273/0   3655 Aug  4 23:25 1993 ATP_problems/geometry/axioms.ver3
rw-r--r-- 4273/0   2881 Aug  4 23:25 1993 ATP_problems/geometry/e1.1.proof
rw-r--r-- 4273/0    919 Aug  4 23:25 1993 ATP_problems/geometry/t1.desc
rw-r--r-- 4273/0   4971 Aug  4 23:25 1993 ATP_problems/geometry/t1.ver1.clauses
rw-r--r-- 4273/0   3892 Aug  4 23:25 1993 ATP_problems/geometry/t1.ver1.in
rw-r--r-- 4273/0   4620 Aug  4 23:25 1993 ATP_problems/geometry/t1.ver1.out
rw-r--r-- 4273/0    996 Aug  4 23:25 1993 ATP_problems/geometry/t10.desc
rw-r--r-- 4273/0   5185 Aug  4 23:25 1993 ATP_problems/geometry/t10.ver1.clauses
rw-r--r-- 4273/0   4544 Aug  4 23:25 1993 ATP_problems/geometry/t10.ver1.in
rw-r--r-- 4273/0   5245 Aug  4 23:25 1993 ATP_problems/geometry/t10.ver1.out
rw-r--r-- 4273/0   1047 Aug  4 23:25 1993 ATP_problems/geometry/t11.desc
rw-r--r-- 4273/0   4985 Aug  4 23:25 1993 ATP_problems/geometry/t11.ver1.clauses
rw-r--r-- 4273/0   4362 Aug  4 23:25 1993 ATP_problems/geometry/t11.ver1.in
rw-r--r-- 4273/0   4026 Aug  4 23:25 1993 ATP_problems/geometry/t11.ver1.out
rw-r--r-- 4273/0   3535 Aug  4 23:25 1993 ATP_problems/geometry/t11.ver2.clauses
rw-r--r-- 4273/0   4045 Aug  4 23:25 1993 ATP_problems/geometry/t11.ver2.in
rw-r--r-- 4273/0   2947 Aug  4 23:25 1993 ATP_problems/geometry/t11.ver2.out
rw-r--r-- 4273/0   3518 Aug  4 23:25 1993 ATP_problems/geometry/t11.ver3.clauses
rw-r--r-- 4273/0   4107 Aug  4 23:25 1993 ATP_problems/geometry/t11.ver3.in
rw-r--r-- 4273/0   3015 Aug  4 23:25 1993 ATP_problems/geometry/t11.ver3.out
rw-r--r-- 4273/0    993 Aug  4 23:25 1993 ATP_problems/geometry/t12.desc
rw-r--r-- 4273/0   5626 Aug  4 23:25 1993 ATP_problems/geometry/t12.ver1.clauses
rw-r--r-- 4273/0   6317 Aug  4 23:25 1993 ATP_problems/geometry/t12.ver1.in
rw-r--r-- 4273/0   3706 Aug  4 23:25 1993 ATP_problems/geometry/t12.ver1.out
rw-r--r-- 4273/0   1032 Aug  4 23:25 1993 ATP_problems/geometry/t13.desc
rw-r--r-- 4273/0   5694 Aug  4 23:25 1993 ATP_problems/geometry/t13.ver1.clauses
rw-r--r-- 4273/0   6236 Aug  4 23:25 1993 ATP_problems/geometry/t13.ver1.in
rw-r--r-- 4273/0   5136 Aug  4 23:25 1993 ATP_problems/geometry/t13.ver1.out
rw-r--r-- 4273/0    913 Aug  4 23:25 1993 ATP_problems/geometry/t2.desc
rw-r--r-- 4273/0   4772 Aug  4 23:25 1993 ATP_problems/geometry/t2.ver1.clauses
rw-r--r-- 4273/0   3730 Aug  4 23:25 1993 ATP_problems/geometry/t2.ver1.in
rw-r--r-- 4273/0   3682 Aug  4 23:25 1993 ATP_problems/geometry/t2.ver1.out
rw-r--r-- 4273/0    913 Aug  4 23:25 1993 ATP_problems/geometry/t3.desc
rw-r--r-- 4273/0   3615 Aug  4 23:25 1993 ATP_problems/geometry/t3.ver1.clauses
rw-r--r-- 4273/0   3915 Aug  4 23:25 1993 ATP_problems/geometry/t3.ver1.in
rw-r--r-- 4273/0   3600 Aug  4 23:25 1993 ATP_problems/geometry/t3.ver1.out
rw-r--r-- 4273/0    864 Aug  4 23:25 1993 ATP_problems/geometry/t4.desc
rw-r--r-- 4273/0   5384 Aug  4 23:25 1993 ATP_problems/geometry/t4.ver1.clauses
rw-r--r-- 4273/0   6166 Aug  4 23:25 1993 ATP_problems/geometry/t4.ver1.in
rw-r--r-- 4273/0   5411 Aug  4 23:25 1993 ATP_problems/geometry/t4.ver1.out
rw-r--r-- 4273/0    921 Aug  4 23:25 1993 ATP_problems/geometry/t5.desc
rw-r--r-- 4273/0   5436 Aug  4 23:25 1993 ATP_problems/geometry/t5.ver1.clauses
rw-r--r-- 4273/0   6218 Aug  4 23:25 1993 ATP_problems/geometry/t5.ver1.in
rw-r--r-- 4273/0   5410 Aug  4 23:25 1993 ATP_problems/geometry/t5.ver1.out
rw-r--r-- 4273/0   1019 Aug  4 23:25 1993 ATP_problems/geometry/t6.desc
rw-r--r-- 4273/0   5128 Aug  4 23:25 1993 ATP_problems/geometry/t6.ver1.clauses
rw-r--r-- 4273/0   4035 Aug  4 23:25 1993 ATP_problems/geometry/t6.ver1.in
rw-r--r-- 4273/0   4362 Aug  4 23:25 1993 ATP_problems/geometry/t6.ver1.out
rw-r--r-- 4273/0   1062 Aug  4 23:25 1993 ATP_problems/geometry/t7.desc
rw-r--r-- 4273/0   3820 Aug  4 23:25 1993 ATP_problems/geometry/t7.ver1.clauses
rw-r--r-- 4273/0   4217 Aug  4 23:25 1993 ATP_problems/geometry/t7.ver1.in
rw-r--r-- 4273/0   4018 Aug  4 23:25 1993 ATP_problems/geometry/t7.ver1.out
rw-r--r-- 4273/0   1005 Aug  4 23:25 1993 ATP_problems/geometry/t8.desc
rw-r--r-- 4273/0   5135 Aug  4 23:25 1993 ATP_problems/geometry/t8.ver1.clauses
rw-r--r-- 4273/0   4283 Aug  4 23:25 1993 ATP_problems/geometry/t8.ver1.in
rw-r--r-- 4273/0   5508 Aug  4 23:25 1993 ATP_problems/geometry/t8.ver1.out
rw-r--r-- 4273/0    950 Aug  4 23:25 1993 ATP_problems/geometry/t9.desc
rw-r--r-- 4273/0   5852 Aug  4 23:25 1993 ATP_problems/geometry/t9.ver1.clauses
rw-r--r-- 4273/0   6717 Aug  4 23:25 1993 ATP_problems/geometry/t9.ver1.in
rw-r--r-- 4273/0   4667 Aug  4 23:25 1993 ATP_problems/geometry/t9.ver1.out
rwxr-xr-x 4273/0      0 Aug  4 23:25 1993 ATP_problems/logic.problems/
rw-r--r-- 4273/0   1964 Aug  4 23:25 1993 ATP_problems/logic.problems/README
rwxr-xr-x 4273/0      0 Aug  4 23:26 1993 ATP_problems/logic.problems/morgan/
rw-r--r-- 4273/0   2609 Aug  4 23:25 1993 ATP_problems/logic.problems/morgan/README
rw-r--r-- 4273/0   1339 Aug  4 23:25 1993 ATP_problems/logic.problems/morgan/morgan.five.desc
rw-r--r-- 4273/0    925 Aug  4 23:25 1993 ATP_problems/logic.problems/morgan/morgan.five.ver1.clauses
rw-r--r-- 4273/0    991 Aug  4 23:25 1993 ATP_problems/logic.problems/morgan/morgan.five.ver1.in
rw-r--r-- 4273/0   3055 Aug  4 23:25 1993 ATP_problems/logic.problems/morgan/morgan.five.ver1.out
rw-r--r-- 4273/0   1003 Aug  4 23:25 1993 ATP_problems/logic.problems/morgan/morgan.five.ver2.clauses
rw-r--r-- 4273/0   1069 Aug  4 23:25 1993 ATP_problems/logic.problems/morgan/morgan.five.ver2.in
rw-r--r-- 4273/0    157 Aug  4 23:25 1993 ATP_problems/logic.problems/morgan/morgan.five.ver2.out
rw-r--r-- 4273/0    924 Aug  4 23:25 1993 ATP_problems/logic.problems/morgan/morgan.four.desc
rw-r--r-- 4273/0    987 Aug  4 23:25 1993 ATP_problems/logic.problems/morgan/morgan.four.ver1.clauses
rw-r--r-- 4273/0   1053 Aug  4 23:25 1993 ATP_problems/logic.problems/morgan/morgan.four.ver1.in
rw-r--r-- 4273/0   3152 Aug  4 23:25 1993 ATP_problems/logic.problems/morgan/morgan.four.ver1.out
rw-r--r-- 4273/0    870 Aug  4 23:25 1993 ATP_problems/logic.problems/morgan/morgan.one.desc
rw-r--r-- 4273/0    915 Aug  4 23:25 1993 ATP_problems/logic.problems/morgan/morgan.one.ver1.clauses
rw-r--r-- 4273/0    981 Aug  4 23:25 1993 ATP_problems/logic.problems/morgan/morgan.one.ver1.in
rw-r--r-- 4273/0   2860 Aug  4 23:25 1993 ATP_problems/logic.problems/morgan/morgan.one.ver1.out
rw-r--r-- 4273/0    884 Aug  4 23:25 1993 ATP_problems/logic.problems/morgan/morgan.six.desc
rw-r--r-- 4273/0    903 Aug  4 23:25 1993 ATP_problems/logic.problems/morgan/morgan.six.ver1.clauses
rw-r--r-- 4273/0    957 Aug  4 23:25 1993 ATP_problems/logic.problems/morgan/morgan.six.ver1.in
rw-r--r-- 4273/0    156 Aug  4 23:25 1993 ATP_problems/logic.problems/morgan/morgan.six.ver1.out
rw-r--r-- 4273/0   1317 Aug  4 23:25 1993 ATP_problems/logic.problems/morgan/morgan.three.desc
rw-r--r-- 4273/0   1120 Aug  4 23:25 1993 ATP_problems/logic.problems/morgan/morgan.three.ver1.clauses
rw-r--r-- 4273/0   1192 Aug  4 23:25 1993 ATP_problems/logic.problems/morgan/morgan.three.ver1.in
rw-r--r-- 4273/0   2787 Aug  4 23:25 1993 ATP_problems/logic.problems/morgan/morgan.three.ver1.out
rw-r--r-- 4273/0   1083 Aug  4 23:26 1993 ATP_problems/logic.problems/morgan/morgan.three.ver2.clauses
rw-r--r-- 4273/0   1155 Aug  4 23:26 1993 ATP_problems/logic.problems/morgan/morgan.three.ver2.in
rw-r--r-- 4273/0   2786 Aug  4 23:26 1993 ATP_problems/logic.problems/morgan/morgan.three.ver2.out
rw-r--r-- 4273/0    917 Aug  4 23:26 1993 ATP_problems/logic.problems/morgan/morgan.two.desc
rw-r--r-- 4273/0    986 Aug  4 23:26 1993 ATP_problems/logic.problems/morgan/morgan.two.ver1.clauses
rw-r--r-- 4273/0   1052 Aug  4 23:26 1993 ATP_problems/logic.problems/morgan/morgan.two.ver1.in
rw-r--r-- 4273/0   3150 Aug  4 23:26 1993 ATP_problems/logic.problems/morgan/morgan.two.ver1.out
rwxr-xr-x 4273/0      0 Aug  4 23:26 1993 ATP_problems/miscellany/
rw-r--r-- 4273/0   1865 Aug  4 23:26 1993 ATP_problems/miscellany/README
rwxr-xr-x 4273/0      0 Aug  4 23:26 1993 ATP_problems/miscellany/wang/
rw-r--r-- 4273/0   2087 Aug  4 23:26 1993 ATP_problems/miscellany/wang/README
rw-r--r-- 4273/0    937 Aug  4 23:26 1993 ATP_problems/miscellany/wang/exq1.desc
rw-r--r-- 4273/0   1153 Aug  4 23:26 1993 ATP_problems/miscellany/wang/exq1.ver1.clauses
rw-r--r-- 4273/0   1186 Aug  4 23:26 1993 ATP_problems/miscellany/wang/exq1.ver1.in
rw-r--r-- 4273/0   4483 Aug  4 23:26 1993 ATP_problems/miscellany/wang/exq1.ver1.out
rw-r--r-- 4273/0   1153 Aug  4 23:26 1993 ATP_problems/miscellany/wang/exq1.ver2.clauses
rw-r--r-- 4273/0   1275 Aug  4 23:26 1993 ATP_problems/miscellany/wang/exq1.ver2.in
rw-r--r-- 4273/0   4322 Aug  4 23:26 1993 ATP_problems/miscellany/wang/exq1.ver2.out
rw-r--r-- 4273/0    981 Aug  4 23:26 1993 ATP_problems/miscellany/wang/exq2.desc
rw-r--r-- 4273/0   1165 Aug  4 23:26 1993 ATP_problems/miscellany/wang/exq2.ver1.clauses
rw-r--r-- 4273/0   1198 Aug  4 23:26 1993 ATP_problems/miscellany/wang/exq2.ver1.in
rw-r--r-- 4273/0   4340 Aug  4 23:26 1993 ATP_problems/miscellany/wang/exq2.ver1.out
rw-r--r-- 4273/0   1165 Aug  4 23:26 1993 ATP_problems/miscellany/wang/exq2.ver2.clauses
rw-r--r-- 4273/0   1258 Aug  4 23:26 1993 ATP_problems/miscellany/wang/exq2.ver2.in
rw-r--r-- 4273/0  62871 Aug  4 23:26 1993 ATP_problems/miscellany/wang/exq2.ver2.out
rw-r--r-- 4273/0    978 Aug  4 23:26 1993 ATP_problems/miscellany/wang/exq3.desc
rw-r--r-- 4273/0   1117 Aug  4 23:26 1993 ATP_problems/miscellany/wang/exq3.ver1.clauses
rw-r--r-- 4273/0   1151 Aug  4 23:26 1993 ATP_problems/miscellany/wang/exq3.ver1.in
rw-r--r-- 4273/0   4281 Aug  4 23:26 1993 ATP_problems/miscellany/wang/exq3.ver1.out
rw-r--r-- 4273/0   1117 Aug  4 23:26 1993 ATP_problems/miscellany/wang/exq3.ver2.clauses
rw-r--r-- 4273/0   1211 Aug  4 23:26 1993 ATP_problems/miscellany/wang/exq3.ver2.in
rw-r--r-- 4273/0  64641 Aug  4 23:26 1993 ATP_problems/miscellany/wang/exq3.ver2.out
rwxr-xr-x 4273/0      0 Aug  4 23:26 1993 ATP_problems/pelletier/
rw-r--r-- 4273/0   3909 Aug  4 23:26 1993 ATP_problems/pelletier/README
rw-r--r-- 4273/0    358 Aug  4 23:26 1993 ATP_problems/pelletier/p35.clauses
rw-r--r-- 4273/0    390 Aug  4 23:26 1993 ATP_problems/pelletier/p35.desc
rw-r--r-- 4273/0    449 Aug  4 23:26 1993 ATP_problems/pelletier/p35.in
rw-r--r-- 4273/0   1669 Aug  4 23:26 1993 ATP_problems/pelletier/p35.out
rw-r--r-- 4273/0    588 Aug  4 23:26 1993 ATP_problems/pelletier/p36.clauses
rw-r--r-- 4273/0    497 Aug  4 23:26 1993 ATP_problems/pelletier/p36.desc
rw-r--r-- 4273/0    680 Aug  4 23:26 1993 ATP_problems/pelletier/p36.in
rw-r--r-- 4273/0   2058 Aug  4 23:26 1993 ATP_problems/pelletier/p36.out
rw-r--r-- 4273/0    689 Aug  4 23:26 1993 ATP_problems/pelletier/p37.clauses
rw-r--r-- 4273/0    523 Aug  4 23:26 1993 ATP_problems/pelletier/p37.desc
rw-r--r-- 4273/0    780 Aug  4 23:26 1993 ATP_problems/pelletier/p37.in
rw-r--r-- 4273/0   1846 Aug  4 23:26 1993 ATP_problems/pelletier/p37.out
rw-r--r-- 4273/0    968 Aug  4 23:26 1993 ATP_problems/pelletier/p38.desc
rw-r--r-- 4273/0    902 Aug  4 23:26 1993 ATP_problems/pelletier/p38a.clauses
rw-r--r-- 4273/0    999 Aug  4 23:26 1993 ATP_problems/pelletier/p38a.in
rw-r--r-- 4273/0   3991 Aug  4 23:26 1993 ATP_problems/pelletier/p38a.out
rw-r--r-- 4273/0    930 Aug  4 23:26 1993 ATP_problems/pelletier/p38b.clauses
rw-r--r-- 4273/0   1064 Aug  4 23:26 1993 ATP_problems/pelletier/p38b.in
rw-r--r-- 4273/0   3287 Aug  4 23:26 1993 ATP_problems/pelletier/p38b.out
rw-r--r-- 4273/0    491 Aug  4 23:26 1993 ATP_problems/pelletier/p39.clauses
rw-r--r-- 4273/0    509 Aug  4 23:26 1993 ATP_problems/pelletier/p39.desc
rw-r--r-- 4273/0    582 Aug  4 23:26 1993 ATP_problems/pelletier/p39.in
rw-r--r-- 4273/0   1705 Aug  4 23:26 1993 ATP_problems/pelletier/p39.out
rw-r--r-- 4273/0    599 Aug  4 23:26 1993 ATP_problems/pelletier/p40.clauses
rw-r--r-- 4273/0    577 Aug  4 23:26 1993 ATP_problems/pelletier/p40.desc
rw-r--r-- 4273/0    690 Aug  4 23:26 1993 ATP_problems/pelletier/p40.in
rw-r--r-- 4273/0   1966 Aug  4 23:26 1993 ATP_problems/pelletier/p40.out
rw-r--r-- 4273/0    804 Aug  4 23:26 1993 ATP_problems/pelletier/p41.clauses
rw-r--r-- 4273/0    769 Aug  4 23:26 1993 ATP_problems/pelletier/p41.desc
rw-r--r-- 4273/0    896 Aug  4 23:26 1993 ATP_problems/pelletier/p41.in
rw-r--r-- 4273/0   1834 Aug  4 23:26 1993 ATP_problems/pelletier/p41.out
rw-r--r-- 4273/0    547 Aug  4 23:26 1993 ATP_problems/pelletier/p42.clauses
rw-r--r-- 4273/0    575 Aug  4 23:26 1993 ATP_problems/pelletier/p42.desc
rw-r--r-- 4273/0    625 Aug  4 23:26 1993 ATP_problems/pelletier/p42.in
rw-r--r-- 4273/0   1722 Aug  4 23:26 1993 ATP_problems/pelletier/p42.out
rw-r--r-- 4273/0    612 Aug  4 23:26 1993 ATP_problems/pelletier/p43.clauses
rw-r--r-- 4273/0    628 Aug  4 23:26 1993 ATP_problems/pelletier/p43.desc
rw-r--r-- 4273/0    702 Aug  4 23:26 1993 ATP_problems/pelletier/p43.in
rw-r--r-- 4273/0   2503 Aug  4 23:26 1993 ATP_problems/pelletier/p43.out
rw-r--r-- 4273/0    598 Aug  4 23:26 1993 ATP_problems/pelletier/p44.clauses
rw-r--r-- 4273/0    477 Aug  4 23:26 1993 ATP_problems/pelletier/p44.desc
rw-r--r-- 4273/0    676 Aug  4 23:26 1993 ATP_problems/pelletier/p44.in
rw-r--r-- 4273/0   1846 Aug  4 23:26 1993 ATP_problems/pelletier/p44.out
rw-r--r-- 4273/0    791 Aug  4 23:26 1993 ATP_problems/pelletier/p45.clauses
rw-r--r-- 4273/0    562 Aug  4 23:26 1993 ATP_problems/pelletier/p45.desc
rw-r--r-- 4273/0    868 Aug  4 23:26 1993 ATP_problems/pelletier/p45.in
rw-r--r-- 4273/0   2384 Aug  4 23:26 1993 ATP_problems/pelletier/p45.out
rw-r--r-- 4273/0    738 Aug  4 23:26 1993 ATP_problems/pelletier/p46.clauses
rw-r--r-- 4273/0    549 Aug  4 23:26 1993 ATP_problems/pelletier/p46.desc
rw-r--r-- 4273/0    837 Aug  4 23:26 1993 ATP_problems/pelletier/p46.in
rw-r--r-- 4273/0   2272 Aug  4 23:26 1993 ATP_problems/pelletier/p46.out
rwxr-xr-x 4273/0      0 Aug  4 23:26 1993 ATP_problems/prog.verification/
rw-r--r-- 4273/0   1767 Aug  4 23:27 1993 ATP_problems/prog.verification/README
rwxr-xr-x 4273/0      0 Aug  4 23:28 1993 ATP_problems/puzzles/
rw-r--r-- 4273/0   2219 Aug  4 23:27 1993 ATP_problems/puzzles/README
rwxr-xr-x 4273/0      0 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/
rw-r--r-- 4273/0   2077 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/README
rw-r--r-- 4273/0   1067 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/animals.desc
rw-r--r-- 4273/0   1697 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/animals.ver1.clauses
rw-r--r-- 4273/0   1834 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/animals.ver1.in
rw-r--r-- 4273/0   3296 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/animals.ver1.out
rw-r--r-- 4273/0   3194 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/boys.desc
rw-r--r-- 4273/0   4513 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/boys.ver1.clauses
rw-r--r-- 4273/0   4598 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/boys.ver1.in
rw-r--r-- 4273/0  22120 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/boys.ver1.out
rw-r--r-- 4273/0   1177 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/ggson.desc
rw-r--r-- 4273/0   1849 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/ggson.ver1.clauses
rw-r--r-- 4273/0   1954 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/ggson.ver1.in
rw-r--r-- 4273/0  15410 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/ggson.ver1.out
rw-r--r-- 4273/0   1221 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/letters.desc
rw-r--r-- 4273/0   1293 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/letters.ver1.clauses
rw-r--r-- 4273/0   1360 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/letters.ver1.in
rw-r--r-- 4273/0   6916 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/letters.ver1.out
rw-r--r-- 4273/0   1045 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/lizard.desc
rw-r--r-- 4273/0   1477 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/lizard.ver1.clauses
rw-r--r-- 4273/0   1544 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/lizard.ver1.in
rw-r--r-- 4273/0  26630 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/lizard.ver1.out
rw-r--r-- 4273/0   1213 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/pigs.desc
rw-r--r-- 4273/0   1769 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/pigs.ver1.clauses
rw-r--r-- 4273/0   1819 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/pigs.ver1.in
rw-r--r-- 4273/0   4135 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/pigs.ver1.out
rw-r--r-- 4273/0   1319 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/winds.desc
rw-r--r-- 4273/0   1674 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/winds.ver1.clauses
rw-r--r-- 4273/0   1743 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/winds.ver1.in
rw-r--r-- 4273/0   3631 Aug  4 23:27 1993 ATP_problems/puzzles/carroll/winds.ver1.out
rwxr-xr-x 4273/0      0 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/
rw-r--r-- 4273/0   2752 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/README
rw-r--r-- 4273/0    536 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird1.desc
rw-r--r-- 4273/0   1054 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird1.ver1.clauses
rw-r--r-- 4273/0   1429 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird1.ver1.in
rw-r--r-- 4273/0   2820 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird1.ver1.out
rw-r--r-- 4273/0    505 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird2.desc
rw-r--r-- 4273/0    974 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird2.ver1.clauses
rw-r--r-- 4273/0   1380 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird2.ver1.in
rw-r--r-- 4273/0   2988 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird2.ver1.out
rw-r--r-- 4273/0    682 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird4.desc
rw-r--r-- 4273/0   1305 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird4.ver1.clauses
rw-r--r-- 4273/0   1623 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird4.ver1.in
rw-r--r-- 4273/0   3029 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird4.ver1.out
rw-r--r-- 4273/0   1634 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird4.ver2.clauses
rw-r--r-- 4273/0   1919 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird4.ver2.in
rw-r--r-- 4273/0   3314 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird4.ver2.out
rw-r--r-- 4273/0    522 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird5.desc
rw-r--r-- 4273/0   1015 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird5.ver1.clauses
rw-r--r-- 4273/0   1335 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird5.ver1.in
rw-r--r-- 4273/0   2854 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird5.ver1.out
rw-r--r-- 4273/0    509 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird6.desc
rw-r--r-- 4273/0   1134 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird6.ver1.clauses
rw-r--r-- 4273/0   1446 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird6.ver1.in
rw-r--r-- 4273/0   2999 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird6.ver1.out
rw-r--r-- 4273/0    494 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird7.desc
rw-r--r-- 4273/0    959 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird7.ver1.clauses
rw-r--r-- 4273/0   1261 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird7.ver1.in
rw-r--r-- 4273/0   2687 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird7.ver1.out
rw-r--r-- 4273/0    483 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird8.desc
rw-r--r-- 4273/0   1096 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird8.ver1.clauses
rw-r--r-- 4273/0   1442 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird8.ver1.in
rw-r--r-- 4273/0   2802 Aug  4 23:27 1993 ATP_problems/puzzles/combinators/bird8.ver1.out
rwxr-xr-x 4273/0      0 Aug  4 23:27 1993 ATP_problems/puzzles/gen.test/
rw-r--r-- 4273/0   1718 Aug  4 23:27 1993 ATP_problems/puzzles/gen.test/README
rw-r--r-- 4273/0    827 Aug  4 23:27 1993 ATP_problems/puzzles/gen.test/interns.desc
rw-r--r-- 4273/0   2334 Aug  4 23:27 1993 ATP_problems/puzzles/gen.test/interns.ver1.clauses
rw-r--r-- 4273/0   2401 Aug  4 23:27 1993 ATP_problems/puzzles/gen.test/interns.ver1.in
rw-r--r-- 4273/0   8364 Aug  4 23:27 1993 ATP_problems/puzzles/gen.test/interns.ver1.out
rwxr-xr-x 4273/0      0 Aug  4 23:28 1993 ATP_problems/puzzles/miscell/
rw-r--r-- 4273/0   1883 Aug  4 23:27 1993 ATP_problems/puzzles/miscell/README
rw-r--r-- 4273/0    718 Aug  4 23:27 1993 ATP_problems/puzzles/miscell/barber.desc
rw-r--r-- 4273/0    982 Aug  4 23:27 1993 ATP_problems/puzzles/miscell/barber.ver1.clauses
rw-r--r-- 4273/0   1040 Aug  4 23:27 1993 ATP_problems/puzzles/miscell/barber.ver1.in
rw-r--r-- 4273/0   4864 Aug  4 23:27 1993 ATP_problems/puzzles/miscell/barber.ver1.out
rw-r--r-- 4273/0    897 Aug  4 23:27 1993 ATP_problems/puzzles/miscell/boxes.desc
rw-r--r-- 4273/0   1884 Aug  4 23:27 1993 ATP_problems/puzzles/miscell/boxes.ver1.clauses
rw-r--r-- 4273/0   1950 Aug  4 23:27 1993 ATP_problems/puzzles/miscell/boxes.ver1.in
rw-r--r-- 4273/0   3934 Aug  4 23:27 1993 ATP_problems/puzzles/miscell/boxes.ver1.out
rw-r--r-- 4273/0   1431 Aug  4 23:27 1993 ATP_problems/puzzles/miscell/houses.desc
rw-r--r-- 4273/0   9884 Aug  4 23:27 1993 ATP_problems/puzzles/miscell/houses.ver1.clauses
rw-r--r-- 4273/0  10110 Aug  4 23:27 1993 ATP_problems/puzzles/miscell/houses.ver1.in
rw-r--r-- 4273/0  25546 Aug  4 23:28 1993 ATP_problems/puzzles/miscell/houses.ver1.out
rw-r--r-- 4273/0    905 Aug  4 23:28 1993 ATP_problems/puzzles/miscell/jobs.desc
rw-r--r-- 4273/0   4405 Aug  4 23:28 1993 ATP_problems/puzzles/miscell/jobs.ver1.clauses
rw-r--r-- 4273/0   4474 Aug  4 23:28 1993 ATP_problems/puzzles/miscell/jobs.ver1.in
rw-r--r-- 4273/0   6418 Aug  4 23:28 1993 ATP_problems/puzzles/miscell/jobs.ver1.out
rw-r--r-- 4273/0   1451 Aug  4 23:28 1993 ATP_problems/puzzles/miscell/steamroller.desc
rw-r--r-- 4273/0   2215 Aug  4 23:28 1993 ATP_problems/puzzles/miscell/steamroller.ver1.clauses
rw-r--r-- 4273/0   2333 Aug  4 23:28 1993 ATP_problems/puzzles/miscell/steamroller.ver1.in
rw-r--r-- 4273/0   4951 Aug  4 23:28 1993 ATP_problems/puzzles/miscell/steamroller.ver1.out
rw-r--r-- 4273/0   1909 Aug  4 23:28 1993 ATP_problems/puzzles/miscell/steamroller.ver2.clauses
rw-r--r-- 4273/0   1977 Aug  4 23:28 1993 ATP_problems/puzzles/miscell/steamroller.ver2.in
rw-r--r-- 4273/0   3773 Aug  4 23:28 1993 ATP_problems/puzzles/miscell/steamroller.ver2.out
rwxr-xr-x 4273/0      0 Aug  4 23:28 1993 ATP_problems/puzzles/space.state/
rw-r--r-- 4273/0   1810 Aug  4 23:28 1993 ATP_problems/puzzles/space.state/README
rw-r--r-- 4273/0    916 Aug  4 23:28 1993 ATP_problems/puzzles/space.state/chekndom.desc
rw-r--r-- 4273/0   3085 Aug  4 23:28 1993 ATP_problems/puzzles/space.state/chekndom.ver1.clauses
rw-r--r-- 4273/0   3192 Aug  4 23:28 1993 ATP_problems/puzzles/space.state/chekndom.ver1.in
rw-r--r-- 4273/0  70191 Aug  4 23:28 1993 ATP_problems/puzzles/space.state/chekndom.ver1.out
rw-r--r-- 4273/0   3198 Aug  4 23:28 1993 ATP_problems/puzzles/space.state/chekndom.ver2.clauses
rw-r--r-- 4273/0   3302 Aug  4 23:28 1993 ATP_problems/puzzles/space.state/chekndom.ver2.in
rw-r--r-- 4273/0   4920 Aug  4 23:28 1993 ATP_problems/puzzles/space.state/chekndom.ver2.out
rw-r--r-- 4273/0    904 Aug  4 23:28 1993 ATP_problems/puzzles/space.state/mission.desc
rw-r--r-- 4273/0   3919 Aug  4 23:28 1993 ATP_problems/puzzles/space.state/mission.ver1.clauses
rw-r--r-- 4273/0   4017 Aug  4 23:28 1993 ATP_problems/puzzles/space.state/mission.ver1.in
rw-r--r-- 4273/0   5808 Aug  4 23:28 1993 ATP_problems/puzzles/space.state/mission.ver1.out
rw-r--r-- 4273/0   4209 Aug  4 23:28 1993 ATP_problems/puzzles/space.state/mission.ver2.clauses
rw-r--r-- 4273/0   4282 Aug  4 23:28 1993 ATP_problems/puzzles/space.state/mission.ver2.in
rw-r--r-- 4273/0   7874 Aug  4 23:28 1993 ATP_problems/puzzles/space.state/mission.ver2.out
rwxr-xr-x 4273/0      0 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/
rw-r--r-- 4273/0   2408 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/README
rw-r--r-- 4273/0   1266 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/knightknave.clauses
rw-r--r-- 4273/0    422 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/knightknave.desc
rw-r--r-- 4273/0   1426 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/knightknave.in
rw-r--r-- 4273/0   7595 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/knightknave.out
rw-r--r-- 4273/0   1568 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/mars_venus.clauses
rw-r--r-- 4273/0    723 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/mars_venus.desc
rw-r--r-- 4273/0   1733 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/mars_venus.in
rw-r--r-- 4273/0   9796 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/mars_venus.out
rw-r--r-- 4273/0   1652 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/mars_venus2.clauses
rw-r--r-- 4273/0    687 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/mars_venus2.desc
rw-r--r-- 4273/0   1817 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/mars_venus2.in
rw-r--r-- 4273/0  16158 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/mars_venus2.out
rw-r--r-- 4273/0   1161 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/oona.clauses
rw-r--r-- 4273/0    933 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/oona.desc
rw-r--r-- 4273/0   1246 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/oona.in
rw-r--r-- 4273/0   5919 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/oona.out
rw-r--r-- 4273/0    870 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/tandl.desc
rw-r--r-- 4273/0   1294 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/tandl.ver1.clauses
rw-r--r-- 4273/0   1364 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/tandl.ver1.in
rw-r--r-- 4273/0   4297 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/tandl.ver1.out
rw-r--r-- 4273/0   1033 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/tandl27.desc
rw-r--r-- 4273/0   1600 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/tandl27.ver1.clauses
rw-r--r-- 4273/0   1694 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/tandl27.ver1.in
rw-r--r-- 4273/0   8496 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/tandl27.ver1.out
rw-r--r-- 4273/0    832 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/tandl31.desc
rw-r--r-- 4273/0   2781 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/tandl31.ver1.clauses
rw-r--r-- 4273/0   2849 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/tandl31.ver1.in
rw-r--r-- 4273/0   6984 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/tandl31.ver1.out
rw-r--r-- 4273/0    854 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/tandl35.desc
rw-r--r-- 4273/0   2439 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/tandl35.ver1.clauses
rw-r--r-- 4273/0   2533 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/tandl35.ver1.in
rw-r--r-- 4273/0  20199 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/tandl35.ver1.out
rw-r--r-- 4273/0    850 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/tandl39.desc
rw-r--r-- 4273/0   2570 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/tandl39.ver1.clauses
rw-r--r-- 4273/0   2636 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/tandl39.ver1.in
rw-r--r-- 4273/0  12118 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/tandl39.ver1.out
rw-r--r-- 4273/0    882 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/tandl42.desc
rw-r--r-- 4273/0   2525 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/tandl42.ver1.clauses
rw-r--r-- 4273/0   2615 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/tandl42.ver1.in
rw-r--r-- 4273/0  22797 Aug  4 23:28 1993 ATP_problems/puzzles/truth.lies/tandl42.ver1.out
rwxr-xr-x 4273/0      0 Aug  4 23:29 1993 ATP_problems/set.theory/
rw-r--r-- 4273/0   1979 Aug  4 23:28 1993 ATP_problems/set.theory/README
rwxr-xr-x 4273/0      0 Aug  4 23:29 1993 ATP_problems/set.theory/godel/
rw-r--r-- 4273/0   2612 Aug  4 23:28 1993 ATP_problems/set.theory/godel/README
rw-r--r-- 4273/0   9226 Aug  4 23:28 1993 ATP_problems/set.theory/godel/axioms.clauses
rw-r--r-- 4273/0    783 Aug  4 23:28 1993 ATP_problems/set.theory/godel/compl.desc
rw-r--r-- 4273/0   9417 Aug  4 23:28 1993 ATP_problems/set.theory/godel/compl.ver1.clauses
rw-r--r-- 4273/0   9869 Aug  4 23:28 1993 ATP_problems/set.theory/godel/compl.ver1.in
rw-r--r-- 4273/0   3099 Aug  4 23:28 1993 ATP_problems/set.theory/godel/compl.ver2.clauses
rw-r--r-- 4273/0   3299 Aug  4 23:28 1993 ATP_problems/set.theory/godel/compl.ver2.in
rw-r--r-- 4273/0    778 Aug  4 23:29 1993 ATP_problems/set.theory/godel/inters.desc
rw-r--r-- 4273/0   9419 Aug  4 23:29 1993 ATP_problems/set.theory/godel/inters.ver1.clauses
rw-r--r-- 4273/0   9872 Aug  4 23:29 1993 ATP_problems/set.theory/godel/inters.ver1.in
rw-r--r-- 4273/0   2927 Aug  4 23:29 1993 ATP_problems/set.theory/godel/inters.ver2.clauses
rw-r--r-- 4273/0   3342 Aug  4 23:29 1993 ATP_problems/set.theory/godel/inters.ver2.in
rw-r--r-- 4273/0    828 Aug  4 23:29 1993 ATP_problems/set.theory/godel/subset.desc
rw-r--r-- 4273/0   9459 Aug  4 23:29 1993 ATP_problems/set.theory/godel/subset.ver1.clauses
rw-r--r-- 4273/0   9912 Aug  4 23:29 1993 ATP_problems/set.theory/godel/subset.ver1.in
rw-r--r-- 4273/0   3463 Aug  4 23:29 1993 ATP_problems/set.theory/godel/subset.ver2.clauses
rw-r--r-- 4273/0   3746 Aug  4 23:29 1993 ATP_problems/set.theory/godel/subset.ver2.in
rw-r--r-- 4273/0    766 Aug  4 23:29 1993 ATP_problems/set.theory/godel/union.desc
rw-r--r-- 4273/0   9408 Aug  4 23:29 1993 ATP_problems/set.theory/godel/union.ver1.clauses
rw-r--r-- 4273/0   9860 Aug  4 23:29 1993 ATP_problems/set.theory/godel/union.ver1.in
rw-r--r-- 4273/0   3289 Aug  4 23:29 1993 ATP_problems/set.theory/godel/union.ver2.clauses
rw-r--r-- 4273/0   3572 Aug  4 23:29 1993 ATP_problems/set.theory/godel/union.ver2.in
rwxr-xr-x 4273/0      0 Aug  4 23:29 1993 ATP_problems/set.theory/naive/
rw-r--r-- 4273/0   2318 Aug  4 23:29 1993 ATP_problems/set.theory/naive/README
rw-r--r-- 4273/0   2271 Aug  4 23:29 1993 ATP_problems/set.theory/naive/axioms.clauses
rw-r--r-- 4273/0    481 Aug  4 23:29 1993 ATP_problems/set.theory/naive/compl.desc
rw-r--r-- 4273/0   2242 Aug  4 23:29 1993 ATP_problems/set.theory/naive/compl.ver1.clauses
rw-r--r-- 4273/0   2441 Aug  4 23:29 1993 ATP_problems/set.theory/naive/compl.ver1.in
rw-r--r-- 4273/0    471 Aug  4 23:29 1993 ATP_problems/set.theory/naive/inters.desc
rw-r--r-- 4273/0   2240 Aug  4 23:29 1993 ATP_problems/set.theory/naive/inters.ver1.clauses
rw-r--r-- 4273/0   2438 Aug  4 23:29 1993 ATP_problems/set.theory/naive/inters.ver1.in
rw-r--r-- 4273/0    499 Aug  4 23:29 1993 ATP_problems/set.theory/naive/subset.desc
rw-r--r-- 4273/0   2248 Aug  4 23:29 1993 ATP_problems/set.theory/naive/subset.ver1.clauses
rw-r--r-- 4273/0   2400 Aug  4 23:29 1993 ATP_problems/set.theory/naive/subset.ver1.in
rw-r--r-- 4273/0   4161 Aug  4 23:29 1993 ATP_problems/set.theory/naive/subset.ver1.out
rw-r--r-- 4273/0    464 Aug  4 23:29 1993 ATP_problems/set.theory/naive/union.desc
rw-r--r-- 4273/0   2236 Aug  4 23:29 1993 ATP_problems/set.theory/naive/union.ver1.clauses
rw-r--r-- 4273/0   2434 Aug  4 23:29 1993 ATP_problems/set.theory/naive/union.ver1.in
rwxr-xr-x 4273/0      0 Aug  4 23:30 1993 ATP_problems/topology/
rw-r--r-- 4273/0   6016 Aug  4 23:29 1993 ATP_problems/topology/README
rw-r--r-- 4273/0   7927 Aug  4 23:29 1993 ATP_problems/topology/axioms.clauses
rw-r--r-- 4273/0   5184 Aug  4 23:29 1993 ATP_problems/topology/axioms.decl
rw-r--r-- 4273/0   3541 Aug  4 23:29 1993 ATP_problems/topology/defs.first_order
rw-r--r-- 4273/0   1481 Aug  4 23:29 1993 ATP_problems/topology/demods.first_order
rw-r--r-- 4273/0   5119 Aug  4 23:29 1993 ATP_problems/topology/equality_ax.first_order
rw-r--r-- 4273/0   1592 Aug  4 23:29 1993 ATP_problems/topology/lemma1.clauses
rw-r--r-- 4273/0    570 Aug  4 23:29 1993 ATP_problems/topology/lemma1.desc
rw-r--r-- 4273/0   1774 Aug  4 23:29 1993 ATP_problems/topology/lemma1.in
rw-r--r-- 4273/0   1907 Aug  4 23:29 1993 ATP_problems/topology/lemma1.pf
rw-r--r-- 4273/0    823 Aug  4 23:29 1993 ATP_problems/topology/lemma10.clauses
rw-r--r-- 4273/0    637 Aug  4 23:29 1993 ATP_problems/topology/lemma10.desc
rw-r--r-- 4273/0    734 Aug  4 23:29 1993 ATP_problems/topology/lemma11.clauses
rw-r--r-- 4273/0    753 Aug  4 23:29 1993 ATP_problems/topology/lemma11.desc
rw-r--r-- 4273/0    557 Aug  4 23:29 1993 ATP_problems/topology/lemma12.clauses
rw-r--r-- 4273/0    519 Aug  4 23:29 1993 ATP_problems/topology/lemma12.desc
rw-r--r-- 4273/0    501 Aug  4 23:29 1993 ATP_problems/topology/lemma13.clauses
rw-r--r-- 4273/0    486 Aug  4 23:29 1993 ATP_problems/topology/lemma13.desc
rw-r--r-- 4273/0    356 Aug  4 23:29 1993 ATP_problems/topology/lemma14.clauses
rw-r--r-- 4273/0    471 Aug  4 23:29 1993 ATP_problems/topology/lemma14.desc
rw-r--r-- 4273/0    618 Aug  4 23:29 1993 ATP_problems/topology/lemma15.clauses
rw-r--r-- 4273/0    459 Aug  4 23:29 1993 ATP_problems/topology/lemma15.desc
rw-r--r-- 4273/0    412 Aug  4 23:29 1993 ATP_problems/topology/lemma16.clauses
rw-r--r-- 4273/0    486 Aug  4 23:29 1993 ATP_problems/topology/lemma16.desc
rw-r--r-- 4273/0   2147 Aug  4 23:29 1993 ATP_problems/topology/lemma17.clauses
rw-r--r-- 4273/0    681 Aug  4 23:29 1993 ATP_problems/topology/lemma17.desc
rw-r--r-- 4273/0    377 Aug  4 23:29 1993 ATP_problems/topology/lemma18.clauses
rw-r--r-- 4273/0    474 Aug  4 23:29 1993 ATP_problems/topology/lemma18.desc
rw-r--r-- 4273/0    344 Aug  4 23:29 1993 ATP_problems/topology/lemma19.clauses
rw-r--r-- 4273/0    434 Aug  4 23:29 1993 ATP_problems/topology/lemma19.desc
rw-r--r-- 4273/0   5745 Aug  4 23:29 1993 ATP_problems/topology/lemma1a.clauses
rw-r--r-- 4273/0    514 Aug  4 23:29 1993 ATP_problems/topology/lemma1a.desc
rw-r--r-- 4273/0   6319 Aug  4 23:29 1993 ATP_problems/topology/lemma1a.in
rw-r--r-- 4273/0   7963 Aug  4 23:29 1993 ATP_problems/topology/lemma1a.pf
rw-r--r-- 4273/0   5755 Aug  4 23:29 1993 ATP_problems/topology/lemma1b.clauses
rw-r--r-- 4273/0    491 Aug  4 23:29 1993 ATP_problems/topology/lemma1b.desc
rw-r--r-- 4273/0   6450 Aug  4 23:29 1993 ATP_problems/topology/lemma1b.in
rw-r--r-- 4273/0   8567 Aug  4 23:29 1993 ATP_problems/topology/lemma1b.pf
rw-r--r-- 4273/0   1795 Aug  4 23:29 1993 ATP_problems/topology/lemma1c.clauses
rw-r--r-- 4273/0    519 Aug  4 23:29 1993 ATP_problems/topology/lemma1c.desc
rw-r--r-- 4273/0   2158 Aug  4 23:29 1993 ATP_problems/topology/lemma1c.in
rw-r--r-- 4273/0   6006 Aug  4 23:29 1993 ATP_problems/topology/lemma1c.pf
rw-r--r-- 4273/0   5808 Aug  4 23:29 1993 ATP_problems/topology/lemma1d.clauses
rw-r--r-- 4273/0    523 Aug  4 23:29 1993 ATP_problems/topology/lemma1d.desc
rw-r--r-- 4273/0   6534 Aug  4 23:29 1993 ATP_problems/topology/lemma1d.in
rw-r--r-- 4273/0   8940 Aug  4 23:29 1993 ATP_problems/topology/lemma1d.pf
rw-r--r-- 4273/0    446 Aug  4 23:29 1993 ATP_problems/topology/lemma2.clauses
rw-r--r-- 4273/0    443 Aug  4 23:29 1993 ATP_problems/topology/lemma2.desc
rw-r--r-- 4273/0    302 Aug  4 23:29 1993 ATP_problems/topology/lemma20.clauses
rw-r--r-- 4273/0    426 Aug  4 23:29 1993 ATP_problems/topology/lemma20.desc
rw-r--r-- 4273/0    311 Aug  4 23:29 1993 ATP_problems/topology/lemma21.clauses
rw-r--r-- 4273/0    427 Aug  4 23:29 1993 ATP_problems/topology/lemma21.desc
rw-r--r-- 4273/0    395 Aug  4 23:29 1993 ATP_problems/topology/lemma22.clauses
rw-r--r-- 4273/0    434 Aug  4 23:29 1993 ATP_problems/topology/lemma22.desc
rw-r--r-- 4273/0    408 Aug  4 23:29 1993 ATP_problems/topology/lemma23.clauses
rw-r--r-- 4273/0    479 Aug  4 23:30 1993 ATP_problems/topology/lemma23.desc
rw-r--r-- 4273/0    476 Aug  4 23:30 1993 ATP_problems/topology/lemma3.clauses
rw-r--r-- 4273/0    544 Aug  4 23:30 1993 ATP_problems/topology/lemma3.desc
rw-r--r-- 4273/0    461 Aug  4 23:30 1993 ATP_problems/topology/lemma4.clauses
rw-r--r-- 4273/0    487 Aug  4 23:30 1993 ATP_problems/topology/lemma4.desc
rw-r--r-- 4273/0    466 Aug  4 23:30 1993 ATP_problems/topology/lemma5.clauses
rw-r--r-- 4273/0    467 Aug  4 23:30 1993 ATP_problems/topology/lemma5.desc
rw-r--r-- 4273/0    421 Aug  4 23:30 1993 ATP_problems/topology/lemma6.clauses
rw-r--r-- 4273/0    523 Aug  4 23:30 1993 ATP_problems/topology/lemma6.desc
rw-r--r-- 4273/0    388 Aug  4 23:30 1993 ATP_problems/topology/lemma7.clauses
rw-r--r-- 4273/0    416 Aug  4 23:30 1993 ATP_problems/topology/lemma7.desc
rw-r--r-- 4273/0    383 Aug  4 23:30 1993 ATP_problems/topology/lemma8.clauses
rw-r--r-- 4273/0    475 Aug  4 23:30 1993 ATP_problems/topology/lemma8.desc
rw-r--r-- 4273/0   1149 Aug  4 23:30 1993 ATP_problems/topology/lemma9.clauses
rw-r--r-- 4273/0    616 Aug  4 23:30 1993 ATP_problems/topology/lemma9.desc
rw-r--r-- 4273/0   1845 Aug  4 23:30 1993 ATP_problems/topology/set_assump.clauses
rw-r--r-- 4273/0   1727 Aug  4 23:30 1993 ATP_problems/topology/set_assump.first_order