----- SUMMARY FOR THEOREM CRS-FU IN DIRECTORY Q:\cross -----

% CRS-FU.IN                 2000 August 6

formula_list(sos).
% Definition DEF-CRS of the binary function CROSS
equal(composite(IMAGE(TWIST),CART),CROSS).
% negation of Theorem CRS-FU
-FUNCTION(CROSS).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Sun Aug 06 22:32:26 2000

Length of proof is 0. Level of proof is 0.

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

1123 [] -FUNCTION(x) | -FUNCTION(y) | FUNCTION(composite(x,y)).
2426 [] FUNCTION(CART).
2519 [] FUNCTION(IMAGE(x)).
2605 [] equal(composite(IMAGE(TWIST),CART),CROSS).
2606 [] -FUNCTION(CROSS).
3474 [para_from,2605.1.1,1123.3.1,unit_del,2519,2426,2606] $F.

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

clauses generated     156
Kbytes malloced      2522
user CPU time           1.92  seconds