added disjointness axioms
more minimal imports