----- SUMMARY FOR THEOREM CUP-OP3B IN DIRECTORY Q:\cup -----

% CUP-OP3B.IN                 1999 July 22

formula_list(sos).
% negation of Theorem CUP-OP3B
-(all x y (member(pair(x,y),CUP) -> 
           equal(union(first(x),second(x)),y))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Thu Jul 22 13:03:00 1999

Length of proof is 8. Level of proof is 4.

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

1 [] -member(x,y) | -subclass(y,z) | member(x,z).
11 [] equal(pairset(singleton(x),pairset(x,singleton(y))),pair(x,y)).
15 [] -member(x,cart(y,z)) | equal(pair(first(x),second(x)),x).
252 [] member(pair(x,y),V).
264 [] equal(pair(first(x),second(x)),x) | equal(first(x),x).
265 [] equal(pair(first(x),second(x)),x) | equal(second(x),x).
776 [] -member(pair(x,y),cart(cart(V,V),V))
           | -member(pair(y,second(x)),z)
           | -member(pair(first(x),y),u) | member(x,composite(z,u)).
2035 [] subclass(CUP,cart(cart(V,V),V)).
2038 [] -member(pair(pair(x,y),z),CUP) | equal(union(x,y),z).
2039 [] member(pair($c2,$c1),CUP).
2040 [] -equal(union(first($c2),second($c2)),$c1).
2042 [] equal(pairset(singleton(x),pairset(x,singleton(y))),
          pair(x,y)).
2144 [] equal(R(V),V).
2256 [] equal(composite(x,V),cart(V,R(x))).
2739 [ur,2039,1,2035] member(pair($c2,$c1),cart(cart(V,V),V)).
2745 [ur,2040,2038] -member(pair(pair(first($c2),second($c2)),
          $c1),CUP).
2754 [ur,2739,776,252,252,demod,2256,2144] member($c2,cart(V,V)).
2772,2771 [para_into,2745.1.1.1,265.1.1,unit_del,2039] 
          equal(second($c2),$c2).
2774,2773 [para_into,2745.1.1.1,264.1.1,unit_del,2039] 
          equal(first($c2),$c2).
2775 [para_into,2745.1.1.1,11.1.2,demod,2774,2774,2772,2042] 
          -member(pair(pair($c2,$c2),$c1),CUP).
2779,2778 [ur,2754,15,demod,2774,2772] equal(pair($c2,$c2),$c2).
2782 [back_demod,2775,demod,2779] -member(pair($c2,$c1),CUP).
2783 [binary,2782.1,2039.1] $F.

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

clauses generated    6442
Kbytes malloced      2011
user CPU time           2.09  seconds