diff --git a/src/sat/smt/tseitin_proof_checker.cpp b/src/sat/smt/tseitin_proof_checker.cpp
index e54c2d3bc..cef7f4641 100644
--- a/src/sat/smt/tseitin_proof_checker.cpp
+++ b/src/sat/smt/tseitin_proof_checker.cpp
@@ -16,6 +16,7 @@ Author:
 
 --*/
 
+#include "ast/ast_pp.h"
 #include "sat/smt/tseitin_proof_checker.h"
 
 namespace tseitin {
@@ -43,16 +44,17 @@ namespace tseitin {
         if (!main_expr)
             return false;
 
-        expr* a;
+        expr* a, * x, * y, *z;
 
         // (or (and a b) (not a) (not b))
+        // (or (and (not a) b) a (not b))
         if (m.is_and(main_expr)) {            
             scoped_mark sm(*this);
             for (expr* arg : *jst)
-                if (m.is_not(arg, arg))
-                    mark(arg);
+                complement_mark(arg);
+
             for (expr* arg : *to_app(main_expr)) {
-                if (!is_marked(arg))
+                if (!is_complement(arg))
                     return false;
             }
             return true;
@@ -62,15 +64,54 @@ namespace tseitin {
         if (m.is_or(main_expr)) {            
             scoped_mark sm(*this);
             for (expr* arg : *jst)
-                if (m.is_not(arg, arg))
-                    mark(arg);
-            for (expr* arg : *to_app(main_expr)) {
-                if (is_marked(arg))
-                    return true;
-            }
+                complement_mark(arg);
+            for (expr* arg : *to_app(main_expr)) 
+                if (is_complement(arg))
+                    return true;            
             return false;
         }
+        // (or (= a b) a b)
+        // (or (= a b) (not a) (not b))
+        // (or (= (not a) b) a (not b))
+        if (m.is_eq(main_expr, x, y) && m.is_bool(x)) {
+            scoped_mark sm(*this);
+            for (expr* arg : *jst)
+                complement_mark(arg);
+            if (is_marked(x) && is_marked(y))
+                return true;
+            if (is_complement(x) && is_complement(y))
+                return true;
+        }
+
+        // (or (if a b c) (not b) (not c))
+        // (or (if a b c) a (not c))
+        // (or (if a b c) (not a) (not b))
+        if (m.is_ite(main_expr, x, y, z) && m.is_bool(z)) {
+            scoped_mark sm(*this);
+            for (expr* arg : *jst)
+                complement_mark(arg);
+            if (is_marked(x) && is_complement(z))
+                return true;
+            if (is_complement(x) && is_complement(y))
+                return true;
+            if (is_complement(y) && is_complement(z))
+                return true;
+            IF_VERBOSE(0, verbose_stream() << mk_pp(main_expr, m) << "\n");
+        }
         
+
+        // (or (=> a b) a)
+        // (or (=> a b) (not b))
+        if (m.is_implies(main_expr, x, y)) {
+            scoped_mark sm(*this);
+            for (expr* arg : *jst)
+                complement_mark(arg);
+            if (is_marked(x))
+                return true;
+            if (is_complement(y))
+                return true;
+        }       
+
         if (m.is_not(main_expr, a)) {
             
             // (or (not a) a')
@@ -99,11 +140,46 @@ namespace tseitin {
                 return true;
             }
 
+            // (or (not (= a b) (not a) b)
+            if (m.is_eq(a, x, y) && m.is_bool(x)) {
+                scoped_mark sm(*this);                
+                for (expr* arg : *jst)
+                    complement_mark(arg);
+                if (is_marked(x) && is_complement(y))
+                    return true;
+                if (is_marked(y) & is_complement(x))
+                    return true;
+            }
+
+            // (or (not (if a b c)) (not a) b)
+            // (or (not (if a b c)) a c)
+            if (m.is_ite(a, x, y, z) && m.is_bool(z)) {
+                scoped_mark sm(*this);
+                for (expr* arg : *jst)
+                    complement_mark(arg);
+                if (is_complement(x) && is_marked(y))
+                    return true;
+                if (is_marked(x) && is_marked(z))
+                    return true;
+                if (is_marked(y) && is_marked(z))
+                    return true;
+            }   
+
+            // (or (not (=> a b)) b (not a))
+            if (m.is_implies(a, x, y)) {
+                scoped_mark sm(*this);
+                for (expr* arg : *jst)
+                    complement_mark(arg);
+                if (is_complement(x) && is_marked(y))
+                    return true;
+            }
+
+            IF_VERBOSE(0, verbose_stream() << "miss " << mk_pp(main_expr, m) << "\n");
+
 #if 0
             if (m.is_implies(a))
                 return false;
-            if (m.is_eq(a))
-                return false;
+
             if (m.is_ite(a))
                 return false;
             if (m.is_distinct(a))
diff --git a/src/sat/smt/tseitin_proof_checker.h b/src/sat/smt/tseitin_proof_checker.h
index 40d0f1d6b..de5978ac3 100644
--- a/src/sat/smt/tseitin_proof_checker.h
+++ b/src/sat/smt/tseitin_proof_checker.h
@@ -29,14 +29,33 @@ namespace tseitin {
         ast_manager& m;
 
         expr_fast_mark1 m_mark;
+        expr_fast_mark2 m_nmark;
         bool equiv(expr* a, expr* b);
         
         void mark(expr* a) { m_mark.mark(a); }
         bool is_marked(expr* a) { return m_mark.is_marked(a); }
+
+        void nmark(expr* a) { m_nmark.mark(a); }
+        bool is_nmarked(expr* a) { return m_nmark.is_marked(a); }
+
+        void complement_mark(expr* a) {
+            if (m.is_not(a, a))
+                m_nmark.mark(a);
+            else
+                m_mark.mark(a);
+        }
+
+        bool is_complement(expr* a) {
+            if (m.is_not(a, a))
+                return is_marked(a);
+            else
+                return is_nmarked(a);
+        }
+
         struct scoped_mark {
             proof_checker& pc;
             scoped_mark(proof_checker& pc): pc(pc) {}
-            ~scoped_mark() { pc.m_mark.reset(); }
+            ~scoped_mark() { pc.m_mark.reset(); pc.m_nmark.reset(); }
         };
     public:
         proof_checker(ast_manager& m): 
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 2f513170e..48ba17128 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -124,6 +124,14 @@ struct goal2sat::imp : public sat::sat_internalizer {
         return nullptr;
     }
 
+    euf::th_proof_hint* mk_tseitin(sat::literal a, sat::literal b, sat::literal c) {
+        if (m_euf && ensure_euf()->use_drat()) {
+            sat::literal lits[3] = { a, b, c };
+            return ensure_euf()->mk_smt_hint(m_tseitin, 3, lits);
+        }
+        return nullptr;
+    }
+
     sat::status mk_status(euf::th_proof_hint* ph = nullptr) const {
         return sat::status::th(m_is_redundant, m.get_basic_family_id(), ph);
     }
@@ -522,13 +530,13 @@ struct goal2sat::imp : public sat::sat_internalizer {
             sat::bool_var k = add_var(false, n);
             sat::literal  l(k, false);
             cache(n, l);
-            mk_clause(~l, ~c, t);
-            mk_clause(~l,  c, e);
-            mk_clause(l,  ~c, ~t);
-            mk_clause(l,   c, ~e);
+            mk_clause(~l, ~c, t, mk_tseitin(~l, ~c, t));
+            mk_clause(~l,  c, e, mk_tseitin(~l, c, e));
+            mk_clause(l,  ~c, ~t, mk_tseitin(l, ~c, ~t));
+            mk_clause(l,   c, ~e, mk_tseitin(l, c, ~e));
             if (m_ite_extra) {
-                mk_clause(~t, ~e, l);
-                mk_clause(t,  e, ~l);
+                mk_clause(~t, ~e, l, mk_tseitin(~t, ~e, l));
+                mk_clause(t,  e, ~l, mk_tseitin(t, e, ~l));
             }
             if (aig()) aig()->add_ite(l, c, t, e);
             if (sign)
@@ -555,8 +563,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
             sat::literal  l(k, false);
             cache(t, l);
             // l <=> ~lit
-            mk_clause(lit, l);
-            mk_clause(~lit, ~l);
+            mk_clause(lit, l, mk_tseitin(lit, l));
+            mk_clause(~lit, ~l, mk_tseitin(~lit, ~l));
             if (sign)
                 l.neg();
             m_result_stack.push_back(l);
@@ -587,9 +595,9 @@ struct goal2sat::imp : public sat::sat_internalizer {
             sat::literal  l(k, false);
             cache(t, l);
             // l <=> (l1 => l2)
-            mk_clause(~l, ~l1, l2);
-            mk_clause(l1, l);
-            mk_clause(~l2, l);
+            mk_clause(~l, ~l1, l2, mk_tseitin(~l, ~l1, l2));
+            mk_clause(l1, l, mk_tseitin(l1, l));
+            mk_clause(~l2, l, mk_tseitin(~l2, l));
             if (sign)
                 l.neg();
             m_result_stack.push_back(l);
@@ -625,10 +633,10 @@ struct goal2sat::imp : public sat::sat_internalizer {
             sat::literal  l(k, false);
             if (m.is_xor(t))
                 l1.neg();
-            mk_clause(~l, l1, ~l2);
-            mk_clause(~l, ~l1, l2);
-            mk_clause(l, l1, l2);
-            mk_clause(l, ~l1, ~l2);
+            mk_clause(~l,  l1, ~l2, mk_tseitin(~l, l1, ~l2));
+            mk_clause(~l, ~l1,  l2, mk_tseitin(~l, ~l1, l2));
+            mk_clause(l,   l1,  l2, mk_tseitin(l, l1, l2));
+            mk_clause(l,  ~l1, ~l2, mk_tseitin(l, ~l1, ~l2));
             if (aig()) aig()->add_iff(l, l1, l2);
 
             cache(t, l);