----- SUMMARY FOR THEOREM DJT-SR-1 IN DIRECTORY Q:\djt -----

% DJT-SR-1.IN                 1998 August 23

formula_list(sos).
% negation of Theorem DJT-SR-1
-equal(composite(DISJOINT,S),DISJOINT).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Sun Aug 23 22:27:19 1998

Length of proof is 16. Level of proof is 9.

---------------- 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).
5 [] -subclass(x,y) | -subclass(y,x) | equal(x,y).
15 [] -member(x,cart(y,z)) | equal(pair(first(x),second(x)),x).
193 [] -subclass(x,y) | -disjoint(y,z) | disjoint(x,z).
712 [] subclass(composite(x,y),cart(D(y),V)).
740 [] -member(pair(x,y),composite(z,u))
           | member(pair(x,com(z,u,x,y)),u).
742 [] -member(pair(x,y),composite(z,u))
           | member(pair(com(z,u,x,y),y),z).
800 [] -member(pair(x,y),S) | subclass(x,y).
813 [] -subclass(x,cart(V,V)) | subclass(x,composite(x,S)).
965 [] subclass(DISJOINT,cart(V,V)).
969 [] -member(pair(x,y),DISJOINT) | disjoint(x,y).
970 [] -member(pair(x,y),cart(V,V)) | -disjoint(x,y)
           | member(pair(x,y),DISJOINT).
971 [] -equal(composite(DISJOINT,S),DISJOINT).
1195 [] equal(D(S),V).
1270 [] equal(notsub(composite(DISJOINT,S),DISJOINT),n$).
1271 [] equal(first(n$),f$).
1272 [] equal(second(n$),s$).
1273 [] equal(com(DISJOINT,S,f$,s$),m$).
1274 [binary,971.1,5.3] 
          -subclass(composite(DISJOINT,S),DISJOINT)
           | -subclass(DISJOINT,composite(DISJOINT,S)).
1275 [binary,1274.1,3.2,demod,1270] 
          -subclass(DISJOINT,composite(DISJOINT,S))
           | -member(n$,DISJOINT).
1276 [binary,1274.1,2.2,demod,1270] 
          -subclass(DISJOINT,composite(DISJOINT,S))
           | member(n$,composite(DISJOINT,S)).
1278 [binary,1275.1,813.2,unit_del,965] -member(n$,DISJOINT).
1279 [binary,1276.1,813.2,unit_del,965] 
          member(n$,composite(DISJOINT,S)).
1282 [ur,1279,1,712,demod,1195] member(n$,cart(V,V)).
1289,1288 [binary,1282.1,15.1,demod,1271,1272,flip.1] 
          equal(n$,pair(f$,s$)).
1290 [back_demod,1282,demod,1289] member(pair(f$,s$),cart(V,V)).
1291 [back_demod,1279,demod,1289] 
          member(pair(f$,s$),composite(DISJOINT,S)).
1292 [back_demod,1278,demod,1289] -member(pair(f$,s$),DISJOINT).
1296 [binary,1290.1,970.1,unit_del,1292] -disjoint(f$,s$).
1299 [binary,1291.1,742.1,demod,1273] member(pair(m$,s$),DISJOINT).
1301 [binary,1291.1,740.1,demod,1273] member(pair(f$,m$),S).
1314 [binary,1299.1,969.1] disjoint(m$,s$).
1318 [binary,1301.1,800.1] subclass(f$,m$).
1329 [ur,1314,193,1296] -subclass(f$,m$).
1330 [binary,1329.1,1318.1] $F.

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

clauses generated    6530
Kbytes malloced       926
user CPU time           5.05  seconds