10#ifndef CPROVER_SOLVERS_SAT_RESOLUTION_PROOF_H
11#define CPROVER_SOLVERS_SAT_RESOLUTION_PROOF_H
37template<
class T=clauset>
std::vector< stept > stepst
void build_core(std::vector< bool > &in_core)
std::vector< T > clausest
std::vector< literalt > bvt
resolution_prooft< clauset > simple_prooft