Study directory Q:\cup    October  4, 1999 @  8:34 am

Theorem groups used in proof for CUP-2.OUT
82: PO-1.USE
307: CP2.USE
752: CO2-A.USE
1381: PSM.USE
2632: ???.USE
2633: sos
2736: IN2-B.DEM
2870: SR1.DEM
3272: DUP.DEM
3301: X2-C.DEM

Theorem groups used in proof for CUP-1.OUT
82: PO-1.USE
718: CO1-B.USE
1381: PSM.USE
2632: ???.USE
2633: sos

Theorem groups used in proof for CUP-OP1.OUT
81: PO-1.USE
82: PO-1.USE
147: LA2.USE
148: LA2.USE
290: CP1.USE
412: IN1.USE
740: CO2-A.USE
1258: RP1.USE
1259: RP1.USE
1874: DUP.USE
1878: DUP.USE
1920: X2-B.USE
2067: IN2-B.DEM
2082: IM2.DEM
2201: SR1.DEM

Theorem groups used in proof for CUP-OP2.OUT
149: LA2.USE
410: IN1.USE
414: IN1.USE
778: CO4-B.USE
780: CO4-B.USE
849: SR1.USE
1948: DUP.USE
1992: X2-B.USE
1993: X2-B.USE
2307: ID-CO.DEM
2694: DUP.DEM

Theorem groups used in proof for CUP-OP3A.OUT
1: AX-A-8.USE
81: PO-1.USE
185: DJ.USE
252: OP1.USE
292: CP1.USE
499: IM1.USE
746: CO2-A.USE
754: CO2-A.USE
1288: RP1.USE
1399: PS1-A.USE
1403: PS1-A.USE
1414: PSM-A.USE
1415: PSM-A.USE
2033: ???.USE
2034: ???.USE
2036: ???.USE
2037: ???.USE
2140: IN2-B.DEM
2146: RA2.DEM
2155: IM2.DEM
2275: SR1.DEM
2698: DUP.DEM

Theorem groups used in proof for CUP-OP4.OUT
5: AX-A-8.USE
21: AX-B-16.USE
81: PO-1.USE
293: CP1.USE
603: SC2.USE
779: CO4-B.USE
781: CO4-B.USE
1401: PS1-A.USE
1402: PS1-A.USE
1413: PSM-A.USE
1778: POW1.USE
2033: ???.USE
2036: ???.USE
2037: ???.USE
2071: C1.DEM
2308: ID-CO.DEM
2318: ID-CO.DEM

Theorem groups used in proof for CUP-FU.OUT
1072: SV.USE
1073: SV.USE
1074: SV.USE
1090: FU1.USE
2075: ???.USE
2080: ???.USE
2082: sos

Theorem groups used in proof for CUP-OP3B.OUT
1: AX-A-8.USE
11: AX-B-16.USE
15: AX-B-16.USE
252: OP1.USE
264: OP2.USE
265: OP2.USE
776: CO4-B.USE
2035: ???.USE
2038: ???.USE
2042: AX-B1.DEM
2144: RA1.DEM
2256: CO2-A.DEM

Theorem groups used in proof for CUP-DO.OUT
1: AX-A-8.USE
2: AX-A-8.USE
3: AX-A-8.USE
5: AX-A-8.USE
15: AX-B-16.USE
292: CP1.USE
374: DO1.USE
2075: ???.USE
2077: ???.USE
2082: ???.USE
2084: sos

Theorem groups used in proof for CUP-3.OUT
82: PO-1.USE
377: DO1.USE
382: DO2.USE
2076: ???.USE
2077: sos

Theorem groups used in proof for CUP-RA.OUT
2: AX-A-8.USE
3: AX-A-8.USE
252: OP1.USE
293: CP1.USE
301: CP1.USE
499: IM1.USE
553: IM2.USE
2075: ???.USE
2082: ???.USE
2085: sos
2114: I1.DEM
2129: U1.DEM
2189: RA1.DEM
2201: IM2.DEM
2217: IM2.DEM

Theorem groups used in proof for CUP-AP.OUT
1: AX-A-8.USE
1093: FU1.USE
1640: AP2.USE
2099: ???.USE
2106: ???.USE
2107: ???.USE

Theorem groups used in proof for CUP-DUP1.OUT
1: AX-A-8.USE
2: AX-A-8.USE
3: AX-A-8.USE
15: AX-B-16.USE
283: OP3.USE
294: CP1.USE
412: IN1.USE
416: IN1.USE
563: IM2.USE
2005: DUP.USE
2106: ???.USE
2107: sos
2151: U1.DEM
2211: RA1.DEM
2223: IM2.DEM
2240: IM2.DEM
2378: ID-CO.DEM
2796: DUP.DEM
2797: DUP.DEM

Theorem groups used in proof for CUP-DUP2.OUT
5: AX-A-8.USE
81: PO-1.USE
82: PO-1.USE
740: CO1-B.USE
741: CO2-A.USE
1091: FU1.USE
2107: ???.USE
2108: ???.USE
2109: sos
2374: ID1.DEM
2803: DUP.DEM

Theorem groups used in proof for CUP-SW.OUT
1: AX-A-8.USE
2: AX-A-8.USE
3: AX-A-8.USE
15: AX-B-16.USE
78: EQ-2.USE
248: OP1.USE
282: OP3.USE
289: CP1.USE
290: CP1.USE
299: CP1.USE
300: CP1.USE
382: DO2-A.USE
456: RA2.USE
747: CO2-A.USE
950: ID-CO.USE
1141: IDX1.USE
1930: SW2.USE
2874: ???.USE
2877: ???.USE
2879: ???.USE
2880: sos
2927: ???.DEM
2967: DO2.DEM
2988: RA2.DEM
3539: SW3-B.DEM

Done!