+composition-decomposition optimization for deterministic reasoning
small changes
Context are now marked as "saturated" when saturation is over. Use this
flag not to change saturated contexts when checking subsumtpions.