----- SUMMARY FOR THEOREM FS-PC-ID IN DIRECTORY Q:\fs ----- % FS-PC-ID.IN 2000 March 2 formula_list(sos). % negation of Corollary FS-PC-ID -subclass(P(Id),FUNS). end_of_list. ----- Otter 3.0.4, August 1995 ----- The job was started by ??? on ???, Thu Mar 02 16:01:34 2000 Length of proof is 1. Level of proof is 1. ---------------- PROOF ---------------- 966 [] FUNCTION(Id). 2274 [] -FUNCTION(U(x)) | subclass(x,FUNS). 2275 [] -subclass(P(Id),FUNS). 2448 [] equal(U(P(x)),x). 3046 [ur,2275,2274,demod,2448] -FUNCTION(Id). 3047 [binary,3046.1,966.1] $F. ------------ end of proof ------------- clauses generated 1 Kbytes malloced 2171 user CPU time 1.21 seconds