A Disjoint propagation is a prepossessing stage that propagates the disjoint and incomplete constraint within the problematic class hierarchy cycles. Its aim to strengthen the scope of the FiniteSat algorithm. Currently the FiniteSatUSE tool include an implementation for the disjoint propagation part. The FiniteSatUSE tool suggests activating this if the detection method returns a positive answer and the examined class diagram includes problematic class hierarchy cycles
. Users can also activate interdependently this method.