S
imple_
C
lause_
L
earning
Abstract_Renaming_Apart
Ordered_Resolution_Prover_Extra
SCL_FOL
Correct_Termination
Trail_Induced_Ordering
Initial_Literals_Generalize_Learned_Literals
Non_Redundancy
Wellfounded_Extra
Termination
Completeness
Invariants