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

% CRS-DO.IN                 2000 August 6

formula_list(sos).
% negation of Theorem CRS-DO
-equal(D(CROSS),cart(V,V)).
end_of_list.


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

Length of proof is 2. Level of proof is 2.

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

78 [] equal(x,x).
787 [] equal(D(composite(x,y)),image(inverse(y),D(x))).
2069 [] -FUNCTION(x) | equal(D(VERTSECT(x)),V).
2371 [] FUNCTION(TWIST).
2605 [] equal(composite(IMAGE(TWIST),CART),CROSS).
2607 [] -equal(D(CROSS),cart(V,V)).
2708 [] equal(R(inverse(x)),D(x)).
2723 [] equal(image(x,V),R(x)).
2778 [] equal(P(V),V).
3433 [] equal(D(CART),cart(V,V)).
3474 [] equal(D(IMAGE(x)),P(D(VERTSECT(x)))).
3475 [para_into,2607.1.1.1,2605.1.2] 
          -equal(D(composite(IMAGE(TWIST),CART)),cart(V,V)).
3476 [para_into,3475.1.1,787.1.1,demod,3474] 
          -equal(image(inverse(CART),P(D(VERTSECT(TWIST)))),
          cart(V,V)).
3477 [para_into,3476.1.1.2.1,2069.2.1,demod,
          2778,2723,2708,3433,unit_del,78,2371] $F.

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

clauses generated     702
Kbytes malloced      2554
user CPU time           2.08  seconds