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

% CUP-SW.IN                 1999 September 23

formula_list(sos).
% negation of Theorem CUP-SW
-equal(composite(CUP,SWAP),CUP).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Thu Sep 23 20:51:48 1999

Length of proof is 19. Level of proof is 8.

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

1 [] -member(x,y) | -subclass(y,z) | member(x,z).
2 [] member(notsub(x,y),x) | subclass(x,y).
3 [] -member(notsub(x,y),y) | subclass(x,y).
15 [] -member(x,cart(y,z)) | equal(pair(first(x),second(x)),x).
78 [] equal(x,x).
248 [] member(pair(pair(x,y),pair(z,u)),cart(V,V)).
282 [] -member(x,cart(cart(V,V),V)) | equal(pair(pair(first(first(x)),
          second(first(x))),second(x)),x).
289 [] subclass(cart(x,y),cart(V,V)).
290 [] -member(u,x) | -member(v,y) | member(pair(u,v),cart(V,V)).
299 [] -member(x,cart(y,z)) | member(first(x),y).
300 [] -member(x,cart(y,z)) | member(second(x),z).
382 [] -member(x,y) | -member(x,cart(V,V)) | member(first(x),D(y)).
456 [] -member(x,y) | -member(x,cart(V,V)) | member(second(x),R(y)).
747 [] -member(pair(x,y),z) | -member(pair(x,y),cart(V,V))
           | -member(pair(y,u),v) | -member(pair(y,u),cart(V,V))
           | member(pair(x,u),composite(v,z)).
950 [] -subclass(x,composite(x,y)) | -subclass(composite(y,y),Id)
           | equal(composite(x,y),x).
1141 [] subclass(id(x),Id).
1930 [] -member(pair(x,y),cart(V,V)) | member(pair(pair(x,y),pair(y,x)),
          SWAP).
2874 [] subclass(CUP,cart(cart(V,V),V)).
2877 [] -member(pair(pair(x,y),z),CUP) | equal(union(x,y),z).
2879 [] -member(pair(x,y),cart(V,V)) | member(pair(pair(x,y),union(x,y)),
          CUP).
2880 [] -equal(composite(CUP,SWAP),CUP).
2927 [] equal(union(x,y),union(y,x)).
2967 [] equal(D(cart(x,x)),x).
2988 [] equal(R(cart(x,x)),x).
3539 [] equal(composite(SWAP,SWAP),id(cart(V,V))).
3823 [] equal(notsub(CUP,composite(CUP,SWAP)),n$).
3824 [] equal(first(n$),f$).
3825 [] equal(second(n$),s$).
3826 [] equal(first(f$),ff$).
3827 [] equal(second(f$),sf$).
3828 [para_into,2880.1.1,950.3.1,demod,3539,unit_del,78,1141] 
          -subclass(CUP,composite(CUP,SWAP)).
3833 [ur,3828,3,demod,3823] -member(n$,composite(CUP,SWAP)).
3834 [ur,3828,2,demod,3823] member(n$,CUP).
3845 [ur,3834,1,2874] member(n$,cart(cart(V,V),V)).
3866 [ur,3845,300,demod,3825] member(s$,V).
3867 [ur,3845,299,demod,3824] member(f$,cart(V,V)).
3869,3868 [ur,3845,282,demod,3824,3826,3824,3827,3825,flip.1] 
          equal(n$,pair(pair(ff$,sf$),s$)).
3875 [back_demod,3834,demod,3869] member(pair(pair(ff$,sf$),s$),CUP).
3876 [back_demod,3833,demod,3869] 
          -member(pair(pair(ff$,sf$),s$),composite(CUP,SWAP)).
3891 [ur,3867,456,3867,demod,3827,2988] member(sf$,V).
3892 [ur,3867,382,3867,demod,3826,2967] member(ff$,V).
3897,3896 [ur,3867,15,demod,3826,3827,flip.1] 
          equal(f$,pair(ff$,sf$)).
3898 [ur,3867,1,289,demod,3897] member(pair(ff$,sf$),cart(V,V)).
3905,3904 [para_from,3868.1.2,2877.1.1,demod,3869,unit_del,3875] 
          equal(union(ff$,sf$),s$).
3943 [ur,3892,290,3891] member(pair(sf$,ff$),cart(V,V)).
3949 [para_from,3896.1.2,1930.2.1.1,demod,3897,unit_del,3898] 
          member(pair(pair(ff$,sf$),pair(sf$,ff$)),SWAP).
4091 [ur,3943,2879,demod,2927,3905] 
          member(pair(pair(sf$,ff$),s$),CUP).
4102 [ur,3943,290,3866] member(pair(pair(sf$,ff$),s$),cart(V,V)).
4476 [ur,4091,747,3949,248,3876] 
          -member(pair(pair(sf$,ff$),s$),cart(V,V)).
4477 [binary,4476.1,4102.1] $F.

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

clauses generated  344254
Kbytes malloced      2905
user CPU time          53.28  seconds