+val demodulate_tac: dbd:HMysql.dbd -> ProofEngineTypes.tactic
+
+val superposition_tac:
+ target:string -> table:string -> subterms_only:bool ->
+ demod_table:string -> ProofEngineTypes.proof * ProofEngineTypes.goal ->
+ ProofEngineTypes.proof * ProofEngineTypes.goal list
+
+val get_stats: unit -> string