theory Weidenbach_Book imports Prop_Normalisation Prop_Resolution Prop_Superposition CDCL_NOT DPLL_NOT DPLL_W_Implementation CDCL_W_Implementation CDCL_W_Incremental CDCL_WNOT CDCL_Two_Watched_Literals begin end