----- SUMMARY FOR THEOREM FS-CO IN DIRECTORY Q:\fs -----

% FS-CO.IN                 2000 February 25

formula_list(sos).
% negation of Theorem FS-CO
-(all x y (member(pair(x,y),cart(FUNS,FUNS)) -> 
           member(composite(x,y),FUNS))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Fri Feb 25 23:03:15 2000

Length of proof is 8. Level of proof is 3.

---------------- PROOF ----------------

1 [] -member(x,y) | -subclass(y,z) | member(x,z).
13 [] -member(pair(u,v),cart(x,y)) | member(v,y).
289 [] subclass(cart(x,y),cart(V,V)).
371 [] -member(pair(x,y),z) | -subclass(z,cart(V,V))
           | member(x,D(z)).
1103 [] -FUNCTION(x) | -FUNCTION(y) | FUNCTION(composite(x,y)).
1335 [] -member(pair(x,y),cart(V,V)) | member(composite(x,y),V).
2274 [] -FUNCTION(x) | -member(x,V) | member(x,FUNS).
2280 [] -member(x,FUNS) | FUNCTION(x).
2281 [] member(pair($c2,$c1),cart(FUNS,FUNS)).
2282 [] -member(composite($c2,$c1),FUNS).
2368 [] equal(D(cart(x,x)),x).
3049 [ur,2281,371,289,demod,2368] member($c2,FUNS).
3050 [ur,2281,13] member($c1,FUNS).
3051 [ur,2281,1,289] member(pair($c2,$c1),cart(V,V)).
3052 [ur,3049,2280] FUNCTION($c2).
3056 [ur,3050,2280] FUNCTION($c1).
3061 [ur,3051,1335] member(composite($c2,$c1),V).
3066 [ur,3056,1103,3052] FUNCTION(composite($c2,$c1)).
3071 [ur,3061,2274,2282] -FUNCTION(composite($c2,$c1)).
3072 [binary,3071.1,3066.1] $F.

------------ end of proof -------------

clauses generated   17829
Kbytes malloced      2203
user CPU time           3.30  seconds