Abstract_Renaming_Apart

Ordered_Resolution_Prover_Extra

SCL_FOL

Correct_Termination

Trail_Induced_Ordering

Initial_Literals_Generalize_Learned_Literals

Multiset_Order_Extra

Non_Redundancy

Wellfounded_Extra

Termination

Completeness

Invariants