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

% FS-CP.IN                 2001 April 26

formula_list(sos).
% negation of Theorem FS-CP
-(all x y (member(x,V) -> member(cart(x,singleton(y)),FUNS))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Thu Apr 26 17:28:04 2001

Length of proof is 4. Level of proof is 3.

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

222 [] member(singleton(x),V).
506 [] -member(x,image(y,singleton(z))) | member(pair(z,x),y).
565 [] -member(x,V) | equal(image(V,singleton(x)),V).
1199 [] FUNCTION(cart(x,singleton(y))).
1423 [] -member(pair(x,y),cart(V,V)) | member(cart(x,y),V).
2703 [] -FUNCTION(x) | -member(x,V) | member(x,FUNS).
2704 [] member($c2,V).
2705 [] -member(cart($c2,singleton($c1)),FUNS).
2729 [] equal(intersection(V,x),x).
2731 [] equal(intersection(x,x),x).
2852 [] equal(image(cart(x,y),z),intersection(y,
          image(V,intersection(x,z)))).
3605,3604 [ur,2704,565] equal(image(V,singleton($c2)),V).
3608 [ur,2705,2703,1199] -member(cart($c2,singleton($c1)),V).
3613 [ur,3608,1423] -member(pair($c2,singleton($c1)),cart(V,V)).
3626 [ur,3613,506,demod,2852,2729,3605,2731] 
          -member(singleton($c1),V).
3627 [binary,3626.1,222.1] $F.

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

clauses generated   18202
Kbytes malloced      2650
user CPU time           3.84  seconds