list(usable).
disjoint(x,0).                                                   % DJ-1
disjoint(x,complement(x)).                                       % DJ-2
-disjoint(x,x) | equal(x,0).                                     % DJ-3A  
-equal(x,0) | disjoint(x,x).                                     % DJ-3B
-disjoint(x,y) | disjoint(y,x).                                  % DJ-4
equal(notsub(singleton(0),0),0).                                 % LEMMA
-subclass(x,y) | disjoint(x,complement(y)).                      % DJ-5A
-disjoint(x,complement(y)) | subclass(x,y).                      % DJ-5B
-disjoint(x,y) | subclass(x,complement(y)).                      % DJ-5C
-member(x,y) | -disjoint(singleton(x),y).                        % DJ-6A
member(x,y) | disjoint(singleton(x),y).                          % DJ-6B
-subclass(x,y) | -disjoint(y,z) | disjoint(x,z).                 % DJ-8
member(notsub(x,complement(y)),x) | disjoint(x,y).               % DJ-C-1
member(notsub(x,complement(y)),y) | disjoint(x,y).               % DJ-C-2
-member(x,D(y)) | -disjoint(y,cart(singleton(x),V)).             % DJ-10B
member(y,D(x)) | disjoint(x,cart(singleton(y),V)).               % DJ-10C
-disjoint(x,y) | -disjoint(z,y) | disjoint(union(x,z),y).        % DJ-7
-disjoint(x,cart(y,z)) | equal(restrict(x,y,z),0).               % DJ-9A
-equal(restrict(x,y,z),0) | disjoint(x,cart(y,z)).               % DJ-9B
end_of_list.

list(demodulators).
equal(notsub(singleton(0),0),0).                                 % LEMMA
end_of_list.