----- SUMMARY FOR THEOREM DK-OM-Q2 IN DIRECTORY Q:\dedekind -----

% DK-OM-Q2.IN                 2000 June 12
% For this proof we left Lemma DK-OM-Q1 in the usable list.

formula_list(sos).
% negation of Theorem DK-OM-Q2
-equal(intersection(Q,cart(omega,omega)),id(omega)).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Mon Jun 12 12:21:05 2000

Length of proof is 6. Level of proof is 6.

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

5 [] -subclass(x,y) | -subclass(y,x) | equal(x,y).
76 [] subclass(x,x).
97 [] -subclass(x,intersection(y,z)) | subclass(x,y).
1002 [] -subclass(x,Id) | -subclass(y,Id)
           | equal(composite(x,y),intersection(x,y)).
1161 [] subclass(id(x),Id).
1199 [] -subclass(x,fix(y)) | subclass(id(x),y).
1217 [] equal(intersection(x,composite(id(y),z)),
          composite(id(y),intersection(x,z))).
3314 [] subclass(intersection(Q,cart(omega,omega)),Id).
3315 [] -equal(intersection(Q,cart(omega,omega)),id(omega)).
3342 [] equal(intersection(V,x),x).
3344 [] equal(intersection(x,x),x).
3534 [] equal(composite(x,cart(y,z)),cart(y,image(x,z))).
3676 [] equal(fix(intersection(x,y)),intersection(fix(x),fix(y))).
3677 [] equal(fix(cart(x,y)),intersection(x,y)).
3685 [] equal(image(id(x),y),intersection(x,y)).
4208 [] equal(fix(Q),V).
4379 [binary,3315.1,5.3] 
          -subclass(intersection(Q,cart(omega,omega)),id(omega))
           | -subclass(id(omega),intersection(Q,cart(omega,omega))).
4381 [binary,4379.1,97.2] 
          -subclass(id(omega),intersection(Q,cart(omega,omega)))
           | -subclass(intersection(Q,cart(omega,omega)),
          intersection(id(omega),x)).
4384 [binary,4381.1,1199.2,demod,3676,4208,3677,3344,3342,unit_del,76] 
          -subclass(intersection(Q,cart(omega,omega)),
          intersection(id(omega),x)).
4403 [para_into,4384.1.2,1002.3.2,unit_del,1161] 
          -subclass(intersection(Q,cart(omega,omega)),
          composite(id(omega),x)) | -subclass(x,Id).
4462 [binary,4403.2,3314.1] 
          -subclass(intersection(Q,cart(omega,omega)),
          composite(id(omega),intersection(Q,cart(omega,omega)))).
4632 [para_into,4462.1.2,1217.1.2,demod,3534,3685,3344] 
          -subclass(intersection(Q,cart(omega,omega)),
          intersection(Q,cart(omega,omega))).
4633 [binary,4632.1,76.1] $F.

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

clauses generated   25355
Kbytes malloced      3161
user CPU time           6.92  seconds