diff --git a/src/ast/rewriter/finite_set_axioms.cpp b/src/ast/rewriter/finite_set_axioms.cpp
index 3d2a8d222..5231849bf 100644
--- a/src/ast/rewriter/finite_set_axioms.cpp
+++ b/src/ast/rewriter/finite_set_axioms.cpp
@@ -24,6 +24,11 @@ Revision History:
 #include "ast/array_decl_plugin.h"
 #include "ast/rewriter/finite_set_axioms.h"
 
+
+std::ostream& operator<<(std::ostream& out, theory_axiom const& ax) {
+    return out << "axiom";
+}
+
 // a ~ set.empty => not (x in a)
 // x is an element, generate axiom that x is not in any empty set of x's type
 void finite_set_axioms::in_empty_axiom(expr *x) {
@@ -33,9 +38,9 @@ void finite_set_axioms::in_empty_axiom(expr *x) {
     expr_ref empty_set(u.mk_empty(elem_sort), m);
     expr_ref x_in_empty(u.mk_in(x, empty_set), m);
     
-    expr_ref_vector clause(m);
-    clause.push_back(m.mk_not(x_in_empty));
-    m_add_clause(clause);
+    theory_axiom ax(m, "finite-set", "in-empty");
+    ax.clause.push_back(m.mk_not(x_in_empty));
+    m_add_clause(ax);
 }
 
 // a := set.union(b, c) 
@@ -44,30 +49,29 @@ void finite_set_axioms::in_union_axiom(expr *x, expr *a) {
     expr* b = nullptr, *c = nullptr;
     if (!u.is_union(a, b, c))
         return;
-    
-    expr_ref_vector clause(m);
+
+    theory_axiom ax(m, "finite-set", "in-union");
     expr_ref x_in_a(u.mk_in(x, a), m);
     expr_ref x_in_b(u.mk_in(x, b), m);
     expr_ref x_in_c(u.mk_in(x, c), m);
     
     // (x in a) => (x in b) or (x in c)
-    expr_ref_vector clause1(m);
-    clause1.push_back(m.mk_not(x_in_a));
-    clause1.push_back(x_in_b);
-    clause1.push_back(x_in_c);
-    m_add_clause(clause1);
-    
+    ax.clause.push_back(m.mk_not(x_in_a));
+    ax.clause.push_back(x_in_b);
+    ax.clause.push_back(x_in_c);
+    m_add_clause(ax);
+
     // (x in b) => (x in a)
-    expr_ref_vector clause2(m);
-    clause2.push_back(m.mk_not(x_in_b));
-    clause2.push_back(x_in_a);
-    m_add_clause(clause2);
-    
+    theory_axiom ax2(m, "finite-set", "in-union");
+    ax2.clause.push_back(m.mk_not(x_in_b));
+    ax2.clause.push_back(x_in_a);
+    m_add_clause(ax2);
+
     // (x in c) => (x in a)
-    expr_ref_vector clause3(m);
-    clause3.push_back(m.mk_not(x_in_c));
-    clause3.push_back(x_in_a);
-    m_add_clause(clause3);
+    theory_axiom ax3(m, "finite-set", "in-union");
+    ax3.clause.push_back(m.mk_not(x_in_c));
+    ax3.clause.push_back(x_in_a);
+    m_add_clause(ax3);
 }
 
 // a := set.intersect(b, c)
@@ -82,23 +86,23 @@ void finite_set_axioms::in_intersect_axiom(expr *x, expr *a) {
     expr_ref x_in_c(u.mk_in(x, c), m);
     
     // (x in a) => (x in b)
-    expr_ref_vector clause1(m);
-    clause1.push_back(m.mk_not(x_in_a));
-    clause1.push_back(x_in_b);
-    m_add_clause(clause1);
-    
+    theory_axiom ax1(m, "finite-set", "in-intersect");
+    ax1.clause.push_back(m.mk_not(x_in_a));
+    ax1.clause.push_back(x_in_b);
+    m_add_clause(ax1);
+
     // (x in a) => (x in c)
-    expr_ref_vector clause2(m);
-    clause2.push_back(m.mk_not(x_in_a));
-    clause2.push_back(x_in_c);
-    m_add_clause(clause2);
-    
+    theory_axiom ax2(m, "finite-set", "in-intersect");
+    ax2.clause.push_back(m.mk_not(x_in_a));
+    ax2.clause.push_back(x_in_c);
+    m_add_clause(ax2);
+
     // (x in b) and (x in c) => (x in a)
-    expr_ref_vector clause3(m);
-    clause3.push_back(m.mk_not(x_in_b));
-    clause3.push_back(m.mk_not(x_in_c));
-    clause3.push_back(x_in_a);
-    m_add_clause(clause3);
+    theory_axiom ax3(m, "finite-set", "in-intersect");
+    ax3.clause.push_back(m.mk_not(x_in_b));
+    ax3.clause.push_back(m.mk_not(x_in_c));
+    ax3.clause.push_back(x_in_a);
+    m_add_clause(ax3);
 }
 
 // a := set.difference(b, c)
@@ -113,23 +117,23 @@ void finite_set_axioms::in_difference_axiom(expr *x, expr *a) {
     expr_ref x_in_c(u.mk_in(x, c), m);
     
     // (x in a) => (x in b)
-    expr_ref_vector clause1(m);
-    clause1.push_back(m.mk_not(x_in_a));
-    clause1.push_back(x_in_b);
-    m_add_clause(clause1);
+    theory_axiom ax1(m, "finite-set", "in-difference");
+    ax1.clause.push_back(m.mk_not(x_in_a));
+    ax1.clause.push_back(x_in_b);
+    m_add_clause(ax1);
     
     // (x in a) => not (x in c)
-    expr_ref_vector clause2(m);
-    clause2.push_back(m.mk_not(x_in_a));
-    clause2.push_back(m.mk_not(x_in_c));
-    m_add_clause(clause2);
-    
+    theory_axiom ax2(m, "finite-set", "in-difference");
+    ax2.clause.push_back(m.mk_not(x_in_a));
+    ax2.clause.push_back(m.mk_not(x_in_c));
+    m_add_clause(ax2);
+
     // (x in b) and not (x in c) => (x in a)
-    expr_ref_vector clause3(m);
-    clause3.push_back(m.mk_not(x_in_b));
-    clause3.push_back(x_in_c);
-    clause3.push_back(x_in_a);
-    m_add_clause(clause3);
+    theory_axiom ax3(m, "finite-set", "in-difference");
+    ax3.clause.push_back(m.mk_not(x_in_b));
+    ax3.clause.push_back(x_in_c);
+    ax3.clause.push_back(x_in_a);
+    m_add_clause(ax3);
 }
 
 // a := set.singleton(b)
@@ -141,27 +145,27 @@ void finite_set_axioms::in_singleton_axiom(expr *x, expr *a) {
     
     expr_ref x_in_a(u.mk_in(x, a), m);
 
+    theory_axiom ax(m, "finite-set", "in-singleton");
     if (x == b) {
         // If x and b are syntactically identical, then (x in a) is always true
-        expr_ref_vector clause(m);
-        clause.push_back(x_in_a);
-        m_add_clause(clause);
+
+        ax.clause.push_back(x_in_a);
+        m_add_clause(ax);
         return;
     }
 
     expr_ref x_eq_b(m.mk_eq(x, b), m);
     
     // (x in a) => (x == b)
-    expr_ref_vector clause1(m);
-    clause1.push_back(m.mk_not(x_in_a));
-    clause1.push_back(x_eq_b);
-    m_add_clause(clause1);
-    
+    ax.clause.push_back(m.mk_not(x_in_a));
+    ax.clause.push_back(x_eq_b);
+    m_add_clause(ax);
+    ax.clause.reset();
+
     // (x == b) => (x in a)
-    expr_ref_vector clause2(m);
-    clause2.push_back(m.mk_not(x_eq_b));
-    clause2.push_back(x_in_a);
-    m_add_clause(clause2);
+    ax.clause.push_back(m.mk_not(x_eq_b));
+    ax.clause.push_back(x_in_a);
+    m_add_clause(ax);
 }
 
 // a := set.range(lo, hi)
@@ -177,23 +181,23 @@ void finite_set_axioms::in_range_axiom(expr *x, expr *a) {
     expr_ref x_le_hi(arith.mk_le(x, hi), m);
     
     // (x in a) => (lo <= x)
-    expr_ref_vector clause1(m);
-    clause1.push_back(m.mk_not(x_in_a));
-    clause1.push_back(lo_le_x);
-    m_add_clause(clause1);
-    
+    theory_axiom ax1(m, "finite-set", "in-range");
+    ax1.clause.push_back(m.mk_not(x_in_a));
+    ax1.clause.push_back(lo_le_x);
+    m_add_clause(ax1);
+
     // (x in a) => (x <= hi)
-    expr_ref_vector clause2(m);
-    clause2.push_back(m.mk_not(x_in_a));
-    clause2.push_back(x_le_hi);
-    m_add_clause(clause2);
-    
+    theory_axiom ax2(m, "finite-set", "in-range");
+    ax2.clause.push_back(m.mk_not(x_in_a));
+    ax2.clause.push_back(x_le_hi);
+    m_add_clause(ax2);
+
     // (lo <= x) and (x <= hi) => (x in a)
-    expr_ref_vector clause3(m);
-    clause3.push_back(m.mk_not(lo_le_x));
-    clause3.push_back(m.mk_not(x_le_hi));
-    clause3.push_back(x_in_a);
-    m_add_clause(clause3);
+    theory_axiom ax3(m, "finite-set", "in-range");
+    ax3.clause.push_back(m.mk_not(lo_le_x));
+    ax3.clause.push_back(m.mk_not(x_le_hi));
+    ax3.clause.push_back(x_in_a);
+    m_add_clause(ax3);
 }
 
 // a := set.map(f, b)
@@ -224,10 +228,10 @@ void finite_set_axioms::in_map_image_axiom(expr *x, expr *a) {
     expr_ref fx_in_a(u.mk_in(fx, a), m);
     
     // (x in b) => f(x) in a
-    expr_ref_vector clause(m);
-    clause.push_back(m.mk_not(x_in_b));
-    clause.push_back(fx_in_a);
-    m_add_clause(clause);
+    theory_axiom ax(m, "finite-set", "in-map-image");
+    ax.clause.push_back(m.mk_not(x_in_b));
+    ax.clause.push_back(fx_in_a);
+    m_add_clause(ax);
 }
 
 // a := set.filter(p, b)
@@ -245,23 +249,23 @@ void finite_set_axioms::in_filter_axiom(expr *x, expr *a) {
     expr_ref px(autil.mk_select(p, x), m);
     
     // (x in a) => (x in b)
-    expr_ref_vector clause1(m);
-    clause1.push_back(m.mk_not(x_in_a));
-    clause1.push_back(x_in_b);
-    m_add_clause(clause1);
-    
+    theory_axiom ax1(m, "finite-set", "in-filter");
+    ax1.clause.push_back(m.mk_not(x_in_a));
+    ax1.clause.push_back(x_in_b);
+    m_add_clause(ax1);
+
     // (x in a) => p(x)
-    expr_ref_vector clause2(m);
-    clause2.push_back(m.mk_not(x_in_a));
-    clause2.push_back(px);
-    m_add_clause(clause2);
-    
+    theory_axiom ax2(m, "finite-set", "in-filter");
+    ax2.clause.push_back(m.mk_not(x_in_a));
+    ax2.clause.push_back(px);
+    m_add_clause(ax2);
+
     // (x in b) and p(x) => (x in a)
-    expr_ref_vector clause3(m);
-    clause3.push_back(m.mk_not(x_in_b));
-    clause3.push_back(m.mk_not(px));
-    clause3.push_back(x_in_a);
-    m_add_clause(clause3);
+    theory_axiom ax3(m, "finite-set", "in-filter");
+    ax3.clause.push_back(m.mk_not(x_in_b));
+    ax3.clause.push_back(m.mk_not(px));
+    ax3.clause.push_back(x_in_a);
+    m_add_clause(ax3);
 }
 
 // a := set.singleton(b)
@@ -275,10 +279,10 @@ void finite_set_axioms::size_singleton_axiom(expr *a) {
     expr_ref size_a(u.mk_size(a), m);
     expr_ref one(arith.mk_int(1), m);
     expr_ref eq(m.mk_eq(size_a, one), m);
-    
-    expr_ref_vector clause(m);
-    clause.push_back(eq);
-    m_add_clause(clause);
+
+    theory_axiom ax(m, "finite-set", "size-singleton");
+    ax.clause.push_back(eq);
+    m_add_clause(ax);
 }
 
 void finite_set_axioms::subset_axiom(expr* a) {
@@ -288,16 +292,16 @@ void finite_set_axioms::subset_axiom(expr* a) {
     
     expr_ref intersect_bc(u.mk_intersect(b, c), m);
     expr_ref eq(m.mk_eq(intersect_bc, b), m);
-    
-    expr_ref_vector clause1(m);
-    clause1.push_back(m.mk_not(a));
-    clause1.push_back(eq);
-    m_add_clause(clause1);
-    
-    expr_ref_vector clause2(m);
-    clause2.push_back(a);
-    clause2.push_back(m.mk_not(eq));
-    m_add_clause(clause2);
+
+    theory_axiom ax1(m, "finite-set", "subset");
+    ax1.clause.push_back(m.mk_not(a));
+    ax1.clause.push_back(eq);
+    m_add_clause(ax1);
+
+    theory_axiom ax2(m, "finite-set", "subset");
+    ax2.clause.push_back(a);
+    ax2.clause.push_back(m.mk_not(eq));
+    m_add_clause(ax2);
 }
 
 void finite_set_axioms::extensionality_axiom(expr *a, expr* b) {
@@ -309,8 +313,15 @@ void finite_set_axioms::extensionality_axiom(expr *a, expr* b) {
     expr_ref diff_in_b(u.mk_in(diff_ab, b), m);
     
     // (a != b) => (x in diff_ab != x in diff_ba)
-    expr_ref_vector clause(m);
-    clause.push_back(a_eq_b);
-    clause.push_back(m.mk_not(m.mk_iff(diff_in_a, diff_in_b)));
-    m_add_clause(clause);   
+    theory_axiom ax(m, "finite-set", "extensionality");
+    ax.clause.push_back(a_eq_b);
+    ax.clause.push_back(m.mk_not(diff_in_a));
+    ax.clause.push_back(m.mk_not(diff_in_b));
+    m_add_clause(ax);
+
+    theory_axiom ax2(m, "finite-set", "extensionality");
+    ax2.clause.push_back(m.mk_not(a_eq_b));
+    ax2.clause.push_back(diff_in_a);
+    ax2.clause.push_back(diff_in_b);
+    m_add_clause(ax2);
 }
\ No newline at end of file
diff --git a/src/ast/rewriter/finite_set_axioms.h b/src/ast/rewriter/finite_set_axioms.h
index 99eb39066..d2d17c49c 100644
--- a/src/ast/rewriter/finite_set_axioms.h
+++ b/src/ast/rewriter/finite_set_axioms.h
@@ -12,17 +12,39 @@ Abstract:
        
 --*/
 
+struct theory_axiom {
+    expr_ref_vector   clause;
+    vector<parameter> params;
+    unsigned          weight = 0; // can be used to prioritize instantiation of axioms
+    theory_axiom(ast_manager& m, symbol const& th): clause(m) {
+        params.push_back(parameter(th));
+    }
+    theory_axiom(ast_manager &m, symbol const &th, symbol const& rule) : clause(m) {
+        params.push_back(parameter(th));
+        params.push_back(parameter(rule));
+    }
+    theory_axiom(ast_manager &m, char const *th, char const *rule) : clause(m) {
+        params.push_back(parameter(symbol(th)));
+        params.push_back(parameter(symbol(rule)));
+    }
+    theory_axiom(ast_manager &m) : clause(m) {
+    }
+};
+
+std::ostream &operator<<(std::ostream &out, theory_axiom const &ax);
+
+
 class finite_set_axioms {
     ast_manager&    m;
     finite_set_util u;
 
-    std::function<void(expr_ref_vector const &)> m_add_clause;
+    std::function<void(theory_axiom const &)> m_add_clause;
 
 public:
 
     finite_set_axioms(ast_manager &m) : m(m), u(m) {}
 
-    void set_add_clause(std::function<void(expr_ref_vector const &)> &ac) {
+    void set_add_clause(std::function<void(theory_axiom const &)> &ac) {
         m_add_clause = ac;
     }
 
diff --git a/src/smt/smt_clause_proof.cpp b/src/smt/smt_clause_proof.cpp
index bc4105e13..99085455f 100644
--- a/src/smt/smt_clause_proof.cpp
+++ b/src/smt/smt_clause_proof.cpp
@@ -158,8 +158,10 @@ namespace smt {
         for (literal l : ante)
             m_lits.push_back(ctx.literal2expr(~l));
         m_lits.push_back(ctx.literal2expr(lit));
-        proof_ref pr(m.mk_app(symbol("smt"), 0, nullptr, m.mk_proof_sort()), m);
-        update(clause_proof::status::th_lemma, m_lits, pr);
+        auto st = clause_proof::status::th_lemma;
+        auto pr = justification2proof(st, &const_cast<justification &>(jst));
+        // proof_ref pr(m.mk_app(symbol("smt"), 0, nullptr, m.mk_proof_sort()), m);
+        update(st, m_lits, pr);
     }
 
     void clause_proof::del(clause& c) {
diff --git a/src/smt/smt_justification.cpp b/src/smt/smt_justification.cpp
index cea8558ed..44a3ecffb 100644
--- a/src/smt/smt_justification.cpp
+++ b/src/smt/smt_justification.cpp
@@ -351,8 +351,9 @@ namespace smt {
 
     proof * ext_theory_propagation_justification::mk_proof(conflict_resolution & cr) {
         ptr_buffer<proof> prs;
-        if (!antecedent2proof(cr, prs))
+        if (!antecedent2proof(cr, prs)) {
             return nullptr;
+        }
         context & ctx = cr.get_context();
         ast_manager & m = cr.get_manager();
         expr_ref fact(m);
diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp
index fbcec80b4..2713c55fb 100644
--- a/src/smt/theory_finite_set.cpp
+++ b/src/smt/theory_finite_set.cpp
@@ -29,9 +29,9 @@ namespace smt {
         m_axioms(m), m_find(*this)
     {
         // Setup the add_clause callback for axioms
-        std::function<void(expr_ref_vector const &)> add_clause_fn = 
-            [this](expr_ref_vector const& clause) {
-                this->add_clause(clause);
+        std::function<void(theory_axiom const &)> add_clause_fn =
+            [this](theory_axiom const &ax) {
+                this->add_clause(ax);
             };
         m_axioms.set_add_clause(add_clause_fn);
     }
@@ -101,7 +101,7 @@ namespace smt {
                 ctx.push_trail(push_back_trail(m_var_data[v]->m_parent_setops));
             }
         }
-        else if (u.is_map(e) || u.is_select(e)) {
+        else if (u.is_map(e) || u.is_filter(e)) {
             NOT_IMPLEMENTED_YET();
         }
         return r;
@@ -322,7 +322,8 @@ namespace smt {
         for (unsigned i = 0; i < m_clauses.watch[idx].size(); ++i) {
             TRACE(finite_set, tout << " watch[" << i << "] size: " << m_clauses.watch[i].size() << "\n";);
             auto clause_idx = m_clauses.watch[idx][i];
-            auto &clause = m_clauses.axioms[clause_idx];
+            auto &ax = m_clauses.axioms[clause_idx];
+            auto &clause = ax.clause;
             if (any_of(clause, [&](expr *lit) { return ctx.find_assignment(lit) == l_true; })) {
                 TRACE(finite_set, tout << "  satisfied\n";);
                 m_clauses.watch[idx][j++] = clause_idx;
@@ -398,7 +399,8 @@ namespace smt {
 
     void theory_finite_set::activate_clause(unsigned clause_idx) {
         TRACE(finite_set, tout << "activate_clause: " << clause_idx << "\n";);
-        auto &clause = m_clauses.axioms[clause_idx];
+        auto &ax = m_clauses.axioms[clause_idx];
+        auto &clause = ax.clause;
         if (any_of(clause, [&](expr *e) { return ctx.find_assignment(e) == l_true; }))
             return;
         if (clause.size() <= 1) {
@@ -444,7 +446,8 @@ namespace smt {
             unsigned index;
             unwatch_clause(theory_finite_set &th, unsigned index) : th(th), index(index) {}
             void undo() override {
-                auto &clause = th.m_clauses.axioms[index];
+                auto &ax = th.m_clauses.axioms[index];
+                auto &clause = ax.clause;
                 expr *w1 = clause.get(0);
                 expr *w2 = clause.get(1);
                 bool w1neg = th.m.is_not(w1, w1);
@@ -566,10 +569,10 @@ namespace smt {
         }        
     }
 
-    void theory_finite_set::add_clause(expr_ref_vector const& clause) {
-        TRACE(finite_set, tout << "add_clause: " << clause << "\n");
+    void theory_finite_set::add_clause(theory_axiom const& ax) {
+        TRACE(finite_set, tout << "add_clause: " << ax << "\n");
         ctx.push_trail(push_back_vector(m_clauses.axioms));
-        m_clauses.axioms.push_back(clause);
+        m_clauses.axioms.push_back(ax);
         m_stats.m_num_axioms_created++;
     }
 
@@ -689,7 +692,8 @@ namespace smt {
         return false;
     }
 
-    bool theory_finite_set::assert_clause(expr_ref_vector const &clause) {
+    bool theory_finite_set::assert_clause(theory_axiom const &ax) {
+        auto const &clause = ax.clause;
         expr *unit = nullptr;
         unsigned undef_count = 0;
         for (auto e : clause) {
@@ -708,14 +712,28 @@ namespace smt {
         if (undef_count == 1) {
             TRACE(finite_set, tout << " propagate unit: " << mk_pp(unit, m) << "\n" << clause << "\n";);
             auto lit = mk_literal(unit);
-            literal_vector core;
+            literal_vector antecedent;
             for (auto e : clause) {
                 if (e != unit)
-                    core.push_back(~mk_literal(e));
+                    antecedent.push_back(~mk_literal(e));
             }
             m_stats.m_num_axioms_propagated++;
-            ctx.assign(lit, ctx.mk_justification(
-                                theory_propagation_justification(get_id(), ctx, core.size(), core.data(), lit)));
+            enode_pair_vector eqs;
+            auto just = ext_theory_propagation_justification(get_id(), ctx, antecedent.size(), antecedent.data(), eqs.size(), eqs.data(), lit, ax.params.size(),
+                                                       ax.params.data());
+            auto bjust = ctx.mk_justification(just);
+            if (ctx.clause_proof_active()) {
+                // assume all justifications is a non-empty list of symbol parameters
+                proof_ref pr(m);
+                expr_ref_vector args(m);
+                for (unsigned i = 1; i < ax.params.size(); ++i) 
+                    args.push_back(m.mk_app(ax.params[i].get_symbol(), 0, nullptr, m.mk_proof_sort()));                    
+                pr = m.mk_app(ax.params[0].get_symbol(), args.size(), args.data(), m.mk_proof_sort());
+                justification_proof_wrapper jp(ctx, pr.get(), false);
+                ctx.get_clause_proof().propagate(lit, jp, antecedent);
+                jp.del_eh(m);
+            }
+            ctx.assign(lit, bjust);                                
             return true;
         }
         bool is_conflict = (undef_count == 0);
@@ -727,7 +745,7 @@ namespace smt {
         literal_vector lclause;
         for (auto e : clause)
             lclause.push_back(mk_literal(e));
-        ctx.mk_th_axiom(get_id(), lclause);
+        ctx.mk_th_axiom(get_id(), lclause, ax.params.size(), ax.params.data());
         return true;
     }
 
diff --git a/src/smt/theory_finite_set.h b/src/smt/theory_finite_set.h
index 7ee4ec564..28ded4c51 100644
--- a/src/smt/theory_finite_set.h
+++ b/src/smt/theory_finite_set.h
@@ -107,7 +107,7 @@ namespace smt {
         };
 
         struct theory_clauses {
-            vector<expr_ref_vector> axioms;            // vector of created theory axioms
+            vector<theory_axiom>    axioms;            // vector of created theory axioms
             unsigned                aqhead = 0;        // queue head of created axioms
             unsigned_vector         squeue;            // propagation queue of axioms to be added to the solver
             unsigned                sqhead = 0;        // head into propagation queue axioms to be added to solver
@@ -172,8 +172,8 @@ namespace smt {
 
         // Helper methods for axiom instantiation
         void add_membership_axioms(expr* elem, expr* set);
-        void add_clause(expr_ref_vector const& clause);
-        bool assert_clause(expr_ref_vector const &clause);
+        void add_clause(theory_axiom const& ax);
+        bool assert_clause(theory_axiom const &ax);
         void activate_clause(unsigned index);
         bool activate_unasserted_clause();
         void add_immediate_axioms(app *atom);