From 2713bbcb4044ca18eb3071a8efea7ad097a6693b Mon Sep 17 00:00:00 2001
From: Richard Qin <richard.qin.x@gmail.com>
Date: Sat, 4 Apr 2026 03:02:48 +0800
Subject: feat: implement clause subsumption and tautology detection logic with
 associated unit tests

---
 proofsearch/CMakeLists.txt | 1 +
 1 file changed, 1 insertion(+)

(limited to 'proofsearch/CMakeLists.txt')

diff --git a/proofsearch/CMakeLists.txt b/proofsearch/CMakeLists.txt
index edeb6b7..1b6473e 100644
--- a/proofsearch/CMakeLists.txt
+++ b/proofsearch/CMakeLists.txt
@@ -77,6 +77,7 @@ set(ATP_SOURCES
     src/infer/resolution.cc
     src/index/discrim_tree.cc
     src/simplify/subsumption.cc
+    src/simplify/tautology.cc
     src/search/prover.cc
     src/proof/proof_trace.cc
     src/rewrite/ordering.cc
-- 
cgit v1.2.3