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

% CRS-AP1.IN                 2000 August 7

formula_list(sos).
% negation of Theorem CRS-AP1
-(all x (member(x,cart(V,V)) -> equal(apply(CROSS,x),cross(first(x),second(x))))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Mon Aug 07 14:32:33 2000

Length of proof is 5. Level of proof is 5.

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

1791 [] -FUNCTION(x) | -member(pair(y,z),composite(u,x))
           | member(pair(apply(x,y),z),u).
1813 [] -FUNCTION(x) | -member(y,D(x)) | member(pair(y,apply(x,y)),
          x).
2426 [] FUNCTION(CART).
2431 [] -member(x,cart(V,V)) | equal(apply(CART,x),
          cart(first(x),second(x))).
2502 [] -member(pair(x,y),IMAGE(z)) | equal(image(z,x),y).
2605 [] equal(composite(IMAGE(TWIST),CART),CROSS).
2606 [] FUNCTION(CROSS).
2607 [] equal(D(CROSS),cart(V,V)).
2608 [] member($c1,cart(V,V)).
2609 [] -equal(apply(CROSS,$c1),cross(first($c1),second($c1))).
3411 [] equal(image(TWIST,cart(x,y)),cross(x,y)).
3477 [para_into,2608.1.2,2607.1.2] member($c1,D(CROSS)).
3478 [ur,3477,1813,2606] member(pair($c1,apply(CROSS,$c1)),CROSS).
3481 [para_into,3478.1.2,2605.1.2] 
          member(pair($c1,apply(CROSS,$c1)),
          composite(IMAGE(TWIST),CART)).
3484 [ur,3481,1791,2426] 
          member(pair(apply(CART,$c1),apply(CROSS,$c1)),
          IMAGE(TWIST)).
3487 [ur,3484,2502] equal(image(TWIST,apply(CART,$c1)),
          apply(CROSS,$c1)).
3489 [para_into,3487.1.1.2,2431.2.1,demod,3411,unit_del,2609,2608] 
          $F.

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

clauses generated   12519
Kbytes malloced      2554
user CPU time           2.96  seconds