O
rdered_
R
esolution_
P
rover
Map2
Lazy_List_Liminf
Lazy_List_Chain
Clausal_Logic
Herbrand_Interpretation
Abstract_Substitution
Inference_System
Ground_Resolution_Model
Unordered_Ground_Resolution
Ordered_Ground_Resolution
Proving_Process
Standard_Redundancy
FO_Ordered_Resolution
FO_Ordered_Resolution_Prover