Add testing infrastructure for LFSC signatures (#4678)

This commit adds testing infrastructure for LFSC signatures that is
enabled when CVC4 is configured with LFSC. The testing infrastructure
adopts run_test.py from https://github.com/CVC4/LFSC with minor
modifications (mainly adding support for a list of include directories
that are searched to resolve *.plf dependencies). The commit uses the
existing examples and test files from proofs/signatures as the initial
set of tests.

Co-authored-by: Alex Ozdemir aozdemir@hmc.edu

12 files changed, 2371 insertions, 0 deletions

diff --git a/test/signatures/CMakeLists.txt b/test/signatures/CMakeLists.txt
new file mode 100644
index 000000000..64da9fad2
--- /dev/null
+++ b/test/signatures/CMakeLists.txt
@@ -0,0 +1,33 @@
+set(lfsc_test_file_list
+  drat_test.plf
+  er_test.plf
+  example-arrays.plf
+  example.plf
+  example-quant.plf
+  ex_bv.plf
+  ex-mem.plf
+  lrat_test.plf
+  th_lira_test.plf
+)
+
+set(test_script ${CMAKE_CURRENT_LIST_DIR}/run_test.py)
+
+macro(lfsc_test file)
+  set(test_name "signatures/${file}")
+  add_test(
+    NAME "${test_name}"
+    COMMAND
+      "${PYTHON_EXECUTABLE}"
+      "${test_script}"
+      "${LFSC_BINARY}"
+      "${CMAKE_CURRENT_LIST_DIR}/${file}"
+      "${CMAKE_SOURCE_DIR}/proofs/signatures"
+    WORKING_DIRECTORY ${CMAKE_CURRENT_LIST_DIR}
+  )
+
+  set_tests_properties("${test_name}" PROPERTIES LABELS "signatures")
+endmacro()
+
+foreach(file ${lfsc_test_file_list})
+  lfsc_test(${file})
+endforeach()
diff --git a/test/signatures/README.md b/test/signatures/README.md
new file mode 100644
index 000000000..4ac8cb131
--- /dev/null
+++ b/test/signatures/README.md
@@ -0,0 +1,32 @@
+# Signature Tests
+
+This directory contains tests of our LFSC proof signatures. To run just the
+tests in this directory, the test label `signatures` can be used (`ctest -L
+signatures`).
+
+## Adding a New Signature Test
+
+To add a new signature test file, add the file to git, for example:
+
+```
+git add test/signatures/new_signature_test.plf
+```
+
+Also add it to [CMakeLists.txt](CMakeLists.txt) in this directory and declare
+the dependencies of the test as explained below.
+
+The signature tests are prefixed with `signatures/`, so the test for
+`example.plf` will have the name `signatures/example.plf`.
+
+## Test Dependencies
+
+Tests can declare the signature files that they depend on using the `; Deps:`
+directive followed by a space-separated list of files. For example:
+
+```
+; Deps: sat.plf smt.plf
+```
+
+indicates that the test depends on `sat.plf` and `smt.plf`. The run script
+automatically searches for the listed files in `proofs/signatures` as well as
+the directory of the test input.
diff --git a/test/signatures/drat_test.plf b/test/signatures/drat_test.plf
new file mode 100644
index 000000000..e5335a6bb
--- /dev/null
+++ b/test/signatures/drat_test.plf
@@ -0,0 +1,434 @@
+; Deps: drat.plf
+(declare TestSuccess type)
+
+; Test for clause_eq
+(declare test_clause_eq
+         (! a clause
+            (! b clause
+               (! result bool
+                  (! (^
+                       (bool_and
+                           (bool_eq (clause_eq a b) result)
+                       (bool_and
+                           (bool_eq (clause_eq b a) result)
+                       (bool_and
+                           (bool_eq (clause_eq a a) tt)
+                           (bool_eq (clause_eq b b) tt))))
+                       tt)
+                        TestSuccess)))))
+
+(check
+  (% a var
+  (% b var
+     (@ c1 (clc (pos a) (clc (neg b) cln))
+     (@ c2 (clc (pos a) (clc (neg b) cln))
+        (: TestSuccess
+           (test_clause_eq c1 c2 tt)))))))
+
+(check
+  (% a var
+  (% b var
+     (@ c1 (clc (neg a) (clc (neg b) cln))
+     (@ c2 (clc (pos a) (clc (neg b) cln))
+        (: TestSuccess
+           (test_clause_eq c1 c2 ff)))))))
+
+(check
+  (% a var
+  (% b var
+     (@ c1 (clc (pos a) (clc (pos b) cln))
+     (@ c2 (clc (pos a) (clc (neg b) cln))
+        (: TestSuccess
+           (test_clause_eq c1 c2 ff)))))))
+
+(check
+  (% a var
+  (% b var
+     (@ c1 (clc (pos a) (clc (pos a) cln))
+     (@ c2 (clc (pos a) (clc (neg b) cln))
+        (: TestSuccess
+           (test_clause_eq c1 c2 ff)))))))
+
+(check
+  (% a var
+  (% b var
+     (@ c1 (clc (neg b) (clc (pos a) (clc (neg a) cln)))
+     (@ c1 (clc (neg a) (clc (neg b) (clc (pos a) cln)))
+        (: TestSuccess
+           (test_clause_eq c1 c2 ff)))))))
+
+
+(check
+  (% a var
+  (% b var
+     (@ c1 (clc (pos a) (clc (pos a) (clc (neg b) cln)))
+     (@ c2 (clc (pos a) (clc (neg b) cln))
+        (: TestSuccess
+           (test_clause_eq c1 c2 tt)))))))
+
+(check
+  (% a var
+  (% b var
+     (@ c1 (clc (pos a) (clc (pos a) (clc (neg b) cln)))
+     (@ c2 (clc (pos a) (clc (neg b) (clc (neg b) cln)))
+        (: TestSuccess
+           (test_clause_eq c1 c2 tt)))))))
+
+(check
+  (% a var
+  (% b var
+     (@ c1 (clc (pos a) (clc (pos a) (clc (neg a) cln)))
+     (@ c2 (clc (pos a) (clc (neg a) (clc (neg a) cln)))
+        (: TestSuccess
+           (test_clause_eq c1 c2 tt)))))))
+
+(check
+  (% a var
+  (% b var
+     (@ c1 cln
+     (@ c2 (clc (pos a) (clc (neg a) (clc (neg a) cln)))
+        (: TestSuccess
+           (test_clause_eq c1 c2 ff)))))))
+
+(declare check_rat
+         (! f cnf
+            (! c clause
+               (! b bool
+                  (! sc (^ (is_rat f c) b)
+                    bottom)))))
+
+(declare trust_cnf (! f cnf (cnf_holds f)))
+
+; RAT Test 1
+; Formula: (-p, -a) ^ (-p, b) ^( b, c) ^ (-c, a)
+; Candidate RAT: (p, a)
+; Answer: true
+(check
+  (% va var
+     (% vb var
+        (% vc var
+           (% vp var
+              (check_rat
+                (cnfc (clc (neg vp) (clc (neg va) cln))
+                      (cnfc (clc (neg vp) (clc (pos vb) cln))
+                            (cnfc (clc (pos vb) (clc (pos vc) cln))
+                                  (cnfc (clc (neg vc) (clc (pos va) cln)) cnfn))))
+                (clc (pos vp) (clc (pos va) cln))
+                tt))))))
+
+; RAT Test 2
+; Formula:
+;  p cnf 4 8
+;  1  2 -3 0
+; -1 -2  3 0
+;  2  3 -4 0
+; -2 -3  4 0
+; -1 -3 -4 0
+;  1  3  4 0
+; -1  2  4 0
+;  1 -2 -4 0
+; Candidate RAT: -1
+(check
+  (% v1 var
+     (% v2 var
+        (% v3 var
+           (% v4 var
+              (check_rat
+                (cnfc (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))
+                      (cnfc (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))
+                      (cnfc (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))
+                      (cnfc (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))
+                      (cnfc (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))
+                      (cnfc (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))
+                      (cnfc (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))
+                      (cnfc (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))
+                      cnfn))))))))
+                (clc (neg v1) cln)
+                tt))))))
+
+; RAT Test 3
+; Formula:
+;  p cnf 4 9
+;  1  2 -3 0
+; -1 -2  3 0
+;  2  3 -4 0
+; -2 -3  4 0
+; -1 -3 -4 0
+;  1  3  4 0
+; -1  2  4 0
+;  1 -2 -4 0
+; -1 0
+; Candidate RAT: 2
+(check
+  (% v1 var
+     (% v2 var
+        (% v3 var
+           (% v4 var
+              (check_rat
+                (cnfc (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))
+                      (cnfc (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))
+                      (cnfc (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))
+                      (cnfc (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))
+                      (cnfc (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))
+                      (cnfc (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))
+                      (cnfc (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))
+                      (cnfc (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))
+                      (cnfc (clc (neg v1) cln)
+                      cnfn)))))))))
+                (clc (pos v2) cln)
+                tt))))))
+
+; RAT Test 4
+; Formula:
+;  p cnf 4 2
+;  2 -3 0
+;  1 -4 0
+; Candidate RAT: 3
+; Answer: false
+(check
+  (% v1 var
+     (% v2 var
+        (% v3 var
+           (% v4 var
+              (check_rat
+                (cnfc (clc (pos v2) (clc (neg v3) cln))
+                      (cnfc (clc (pos v1) (clc (neg v4) cln)) cnfn))
+                (clc (pos v3) cln)
+                ff))))))
+
+
+; DRAT Test 1 (from Example 1 @ https://www.cs.utexas.edu/~marijn/drat-trim/)
+; without deletions
+; Formula:
+;   p cnf 4 8
+;    1  2 -3 0
+;   -1 -2  3 0
+;    2  3 -4 0
+;   -2 -3  4 0
+;   -1 -3 -4 0
+;    1  3  4 0
+;   -1  2  4 0
+;    1 -2 -4
+; Proof:
+;           -1 0
+;            2 0
+;              0
+(check
+  (% v1 var
+     (% v2 var
+        (% v3 var
+           (% v4 var
+              (:
+                (holds cln)
+                (drat_proof_of_bottom _
+                  (trust_cnf (cnfc (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))
+                        (cnfc (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))
+                        (cnfc (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))
+                        (cnfc (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))
+                        (cnfc (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))
+                        (cnfc (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))
+                        (cnfc (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))
+                        (cnfc (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))
+                        cnfn)))))))))
+                  (DRATProofa (clc (neg v1) cln)
+                        (DRATProofa (clc (pos v2) cln)
+                        (DRATProofa cln
+                        DRATProofn))))))))))
+
+
+; DRAT Test 2 (from Example 1 @ https://www.cs.utexas.edu/~marijn/drat-trim/)
+; with deletions
+; Formula:
+;   p cnf 4 8
+;    1  2 -3 0
+;   -1 -2  3 0
+;    2  3 -4 0
+;   -2 -3  4 0
+;   -1 -3 -4 0
+;    1  3  4 0
+;   -1  2  4 0
+;    1 -2 -4
+; Proof:
+;           -1 0
+;   d -1 -2  3 0
+;   d -1 -3 -4 0
+;   d -1  2  4 0
+;            2 0
+;   d  1  2 -3 0
+;   d  2  3 -4 0
+;              0
+(check
+  (% v1 var (% v2 var (% v3 var (% v4 var
+     (: (holds cln)
+       (drat_proof_of_bottom _
+         (trust_cnf 
+         (cnfc (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))
+               (cnfc (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))
+               (cnfc (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))
+               (cnfc (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))
+               (cnfc (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))
+               (cnfc (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))
+               (cnfc (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))
+               (cnfc (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))
+               cnfn)))))))))
+         (DRATProofa (clc (neg v1) cln)
+               (DRATProofd (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))
+               (DRATProofd (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))
+               (DRATProofd (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))
+               (DRATProofa (clc (pos v2) cln)
+               (DRATProofd (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))
+               (DRATProofd (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))
+               (DRATProofa cln
+                DRATProofn)))))))))))))))
+
+; ===================================== ;
+; Test Suite from "Two Flavors of DRAT" ;
+; ===================================== ;
+
+; The paper includes a number of proofs which explore specified and operational
+; DRAT validity.
+
+; Our test predicate for asserting the specified and operational validity of
+; DRAT proofs
+(declare spec_oper_test
+         (! f cnf
+         (! proof DRATProof
+         (! spec_validity bool
+         (! oper_validity bool
+            (! sc (^ (bool_and
+                       (bool_eq (is_specified_drat_proof f proof) spec_validity)
+                       (bool_eq (is_operational_drat_proof f proof) oper_validity)
+                     ) tt)
+         TestSuccess))))))
+
+
+(declare x var)
+(declare y var)
+(declare z var)
+(declare w var)
+(define ex_1_formula
+  (cnfc (clc (pos x) (clc (pos y) (clc (pos z) cln)))
+  (cnfc (clc (neg x) (clc (pos y) (clc (pos z) cln)))
+  (cnfc (clc (pos x) (clc (neg y) (clc (pos z) cln)))
+  (cnfc (clc (neg x) (clc (neg y) (clc (pos z) cln)))
+  (cnfc (clc (pos x) (clc (pos y) (clc (neg z) cln)))
+  (cnfc (clc (neg x) (clc (pos y) (clc (neg z) cln)))
+  (cnfc (clc (pos x) (clc (neg y) (clc (neg z) cln)))
+  (cnfc (clc (neg x) (clc (neg y) (clc (neg z) cln)))
+        cnfn)))))))))
+
+; Spec-valid, operationally-invalid
+(define ex_1_pf_pi
+  (DRATProofa (clc (pos x) (clc (pos y) cln))
+  (DRATProofa (clc (pos x) cln)
+  (DRATProofa (clc (pos w) (clc (neg x) cln))
+  (DRATProofd (clc (pos w) (clc (neg x) cln))
+  (DRATProofa (clc (neg w) (clc (neg x) cln))
+  (DRATProofa (clc (pos w) (clc (pos x) cln))
+  (DRATProofa (clc (pos y) (clc (pos w) cln))
+  (DRATProofa cln
+              DRATProofn)))))))))
+
+(check
+  (: TestSuccess
+     (spec_oper_test ex_1_formula ex_1_pf_pi tt ff)))
+
+; Spec-invalid, operationally valid
+(define ex_1_pf_sigma
+  (DRATProofa (clc (pos x) (clc (pos y) cln))
+  (DRATProofa (clc (pos x) cln)
+  (DRATProofd (clc (pos x) cln)
+  (DRATProofa (clc (pos w) (clc (neg y) cln))
+  (DRATProofa (clc (neg w) (clc (neg y) cln))
+  (DRATProofa (clc (pos w) cln)
+  (DRATProofa cln
+              DRATProofn))))))))
+
+(check
+  (: TestSuccess
+     (spec_oper_test ex_1_formula ex_1_pf_sigma ff tt)))
+
+(declare x1 var)
+(declare x2 var)
+(declare x3 var)
+(declare x4 var)
+(declare x5 var)
+(declare x6 var)
+(declare x7 var)
+(declare x8 var)
+(declare x9 var)
+(declare x10 var)
+
+(define ex_2_formula
+  (cnfc (clc (pos x1) cln)
+  (cnfc (clc (neg x1) (clc (pos x2) cln))
+  (cnfc (clc (neg x1) (clc (neg x2) (clc (pos x3) cln)))
+  (cnfc (clc (neg x1) (clc (neg x3) (clc (pos x4) cln)))
+  (cnfc (clc (pos x5) (clc (pos x6) cln))
+  (cnfc (clc (neg x2) (clc (neg x5) (clc (pos x7) cln)))
+  (cnfc (clc (neg x1) (clc (neg x5) (clc (pos x6) cln)))
+  (cnfc (clc (neg x5) (clc (neg x6) (clc (pos x4) cln)))
+  (cnfc (clc (neg x3) (clc (neg x6) (clc (pos x8) cln)))
+  (cnfc (clc (neg x6) (clc (neg x4) (clc (pos x3) cln)))
+  (cnfc (clc (neg x8) (clc (pos x5) cln))
+  (cnfc (clc (neg x3) (clc (pos x9) (clc (pos x10) cln)))
+  (cnfc (clc (neg x4) (clc (neg x9) (clc (pos x10) cln)))
+  (cnfc (clc (neg x10) (clc (pos x9) cln))
+  (cnfc (clc (neg x9) (clc (pos x7) cln))
+  (cnfc (clc (neg x7) (clc (neg x8) (clc (neg x9) (clc (neg x10) cln))))
+        cnfn)))))))))))))))))
+
+; Spec-valid, operationally-valid
+(define ex_2_pf_tau
+  (DRATProofa (clc (pos x5) cln)
+  (DRATProofa (clc (pos x4) cln)
+  (DRATProofa (clc (pos x9) cln)
+  (DRATProofa cln
+              DRATProofn)))))
+
+(check
+  (: TestSuccess
+     (spec_oper_test ex_2_formula ex_2_pf_tau tt tt)))
+
+; Spec-valid, operationally unspecified in the paper, but its operationally valid.
+(define ex_3_pf_tau_prime
+  (DRATProofa (clc (pos x5) cln)
+  (DRATProofd (clc (neg x1) (clc (pos x2) cln))
+  (DRATProofa (clc (pos x9) cln)
+  (DRATProofa cln
+              DRATProofn)))))
+
+(check
+  (: TestSuccess
+     (spec_oper_test ex_2_formula ex_3_pf_tau_prime tt tt)))
+
+; Spec-invalid, operationally-invalid
+(define ex_4_pf_pi_prime
+  (DRATProofa (clc (pos x) (clc (pos y) cln))
+  (DRATProofa (clc (pos x) cln)
+  (DRATProofa (clc (pos w) (clc (neg x) cln))
+  (DRATProofa (clc (neg w) (clc (neg x) cln))
+  (DRATProofa (clc (pos w) (clc (pos x) cln))
+  (DRATProofa (clc (pos y) (clc (pos w) cln))
+  (DRATProofa cln
+              DRATProofn))))))))
+
+(check
+  (: TestSuccess
+     (spec_oper_test ex_1_formula ex_4_pf_pi_prime ff ff)))
+
+
+; Spec-valid, operationally valid
+(define ex_5_pf_sigma_prime
+  (DRATProofa (clc (pos x) (clc (pos y) cln))
+  (DRATProofa (clc (pos x) cln)
+  (DRATProofa (clc (pos w) (clc (neg y) cln))
+  (DRATProofa (clc (neg w) (clc (neg y) cln))
+  (DRATProofa (clc (pos w) cln)
+  (DRATProofa cln
+              DRATProofn)))))))
+
+(check
+  (: TestSuccess
+     (spec_oper_test ex_1_formula ex_5_pf_sigma_prime tt tt)))
+
diff --git a/test/signatures/er_test.plf b/test/signatures/er_test.plf
new file mode 100644
index 000000000..671efdb46
--- /dev/null
+++ b/test/signatures/er_test.plf
@@ -0,0 +1,89 @@
+; Deps: er.plf
+
+; This is a circuitous proof that uses the definition introduction and
+; unrolling rules
+(check
+  (% v1 var
+  (% v2 var
+    (% pf_c1 (holds (clc (pos v1) (clc (pos v2) cln)))
+    (% pf_c2 (holds (clc (neg v1) (clc (pos v2) cln)))
+    (% pf_c3 (holds (clc (pos v1) (clc (neg v2) cln)))
+    (% pf_c4 (holds (clc (neg v1) (clc (neg v2) cln)))
+       (: (holds cln)
+          (decl_definition
+            (neg v1)
+            (clc (neg v2) cln)
+            (\ v3
+            (\ def3
+              (clausify_definition _ _ _ def3 _
+                (\ pf_c5 ; type: (holds (clc (pos v3) (clc (neg v2) cln)))
+                (\ pf_c6 ; type: (holds (clc (pos v3) (clc (pos v1) cln)))
+                (\ pf_cnf ; type: (common_tail_cnf (clc (neg v2) cln) (clc (neg v3) (clc (neg v1) cln)))
+                  (@ pf_c7 (common_tail_cnf_prove_head _ _ _ pf_cnf)
+                                                                          ; Clauses
+                  (satlem_simplify _ _ _ (R _ _ pf_c1 pf_c2 v1)  (\ pf_c8 ; v2
+                  (satlem_simplify _ _ _ (R _ _ pf_c8 pf_c5 v2)  (\ pf_c9 ; v3
+                  (satlem_simplify _ _ _ (R _ _ pf_c9 pf_c7 v3)  (\ pf_c10 ; ~v2  ~v1
+                  (satlem_simplify _ _ _ (Q _ _ pf_c10 pf_c8 v2)  (\ pf_c11 ; ~v1
+                  (satlem_simplify _ _ _ (Q _ _ pf_c11 pf_c3 v1)  (\ pf_c12 ; ~v2
+                  (satlem_simplify _ _ _ (Q _ _ pf_c12 pf_c8 v2)  (\ pf_c13 ; empty
+                        pf_c13
+                  ))
+                  ))
+                  ))
+                  ))
+                  ))
+                  ))
+                  )
+                )))
+              )
+            ))
+          )
+        )
+    ))))
+  ))
+)
+
+; This is a test of ER proof produced by drat2er on Example 1 from:
+; https://www.cs.utexas.edu/~marijn/drat-trim/
+(check
+  (% v1 var
+  (% v2 var
+  (% v3 var
+  (% v4 var
+    (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))))
+    (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))))
+    (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))))
+    (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))))
+    (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))))
+    (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))))
+    (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))))
+    (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))))
+       (: (holds cln)
+          (decl_definition
+            (neg v1)
+            cln
+            (\ v5
+            (\ def1
+              (clausify_definition _ _ _ def1 _
+                (\ pf_c9 ; type: (holds (clc (pos def1v) cln))
+                (\ pf_c10 ; type: (holds (clc (pos def1v) (clc (pos v1) cln)))
+                (\ idc0 ; type: (common_tail_cnf cln _)
+                  (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c7 v1) (\ pf_c11
+                  (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c5 v1) (\ pf_c12
+                  (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c2 v1) (\ pf_c13
+                  (satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c2 pf_c5 v3) pf_c8 v1) (\ pf_c14
+                  (satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c7 pf_c2 v2) pf_c6 v1) (\ pf_c15
+                  (satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c7 pf_c5 v4) pf_c1 v1) (\ pf_c16
+                  (satlem_simplify _ _ _ (R _ _ (Q _ _ pf_c3 pf_c15 v4) pf_c16 v3) (\ pf_c17
+                  (satlem_simplify _ _ _ (Q _ _ (R _ _ (Q _ _ pf_c4 pf_c15 v3) pf_c14 v4) pf_c17 v2) (\ pf_c18
+                    pf_c18
+                  ))))))))))))))))
+                )))
+              )
+            ))
+          )
+       )
+    ))))))))
+  ))))
+)
diff --git a/test/signatures/ex-mem.plf b/test/signatures/ex-mem.plf
new file mode 100644
index 000000000..87d1053c4
--- /dev/null
+++ b/test/signatures/ex-mem.plf
@@ -0,0 +1,64 @@
+; Deps: sat.plf smt.plf th_base.plf
+
+(check
+(% s sort
+(% a (term s)
+(% b (term s)
+(% c (term s)
+(% f (term (arrow s s))
+
+; -------------------- declaration of input formula -----------------------------------
+
+(% A1 (th_holds (= s a b))
+(% A2 (th_holds (= s b c))
+(% A3 (th_holds (not (= s a c)))
+
+; ------------------- specify that the following is a proof of the empty clause -----------------
+
+(: (holds cln)
+
+; ---------- use atoms (a1, a2, a3) to map theory literals to boolean literals (v1, v2, v3) ------
+
+(decl_atom (= s a b) (\ v1 (\ a1
+(decl_atom (= s b c) (\ v2 (\ a2
+(decl_atom (= s a c) (\ v3 (\ a3
+
+; --------------------------- proof of theory lemma ---------------------------------------------
+
+(satlem _ _ (ast _ _ _ a1 (\ l1 (ast _ _ _ a2 (\ l2 (asf _ _ _ a3 (\ l3  (clausify_false (contra _ (trans _ _ _ _ l1 l2) l3)))))))) (\ CT1
+
+; -------------------- clausification of input formulas -----------------------------------------
+
+(satlem _ _
+(asf _ _ _ a1 (\ l1
+(clausify_false
+  (contra _ A1 l1)
+))) (\ C1
+; C1 is the clause ( v1 )
+
+(satlem _ _
+(asf _ _ _ a2 (\ l2
+(clausify_false
+   (contra _ A2 l2)
+))) (\ C2
+; C2 is the clause ( v2 )
+
+(satlem _ _
+(ast _ _ _ a3 (\ l3
+(clausify_false
+  (contra _ l3 A3)
+))) (\ C3
+; C3 is the clause ( ~v3 )
+
+
+; -------------------- resolution proof ------------------------------------------------------------
+
+(satlem_simplify _ _ _
+
+(R _ _
+(R _ _ C2
+(R _ _ C1 CT1 v1) v2) C3 v3)
+
+(\ x x))
+
+)))))))))))))))))))))))))))
diff --git a/test/signatures/ex_bv.plf b/test/signatures/ex_bv.plf
new file mode 100644
index 000000000..a4f5ad816
--- /dev/null
+++ b/test/signatures/ex_bv.plf
@@ -0,0 +1,60 @@
+; Deps: sat.plf smt.plf th_base.plf th_bv.plf th_bv_bitblast.plf
+
+; (a = b) ^ (a = b & 00000) ^ (b = 11111) is UNSAT
+
+(check
+(% a var_bv
+(% b var_bv
+(% f1 (th_holds (= (BitVec 4) (a_var_bv _ a) (a_var_bv _ b)))
+(% f2 (th_holds (= (BitVec 4) (a_var_bv _ a) (bvand 4 (a_var_bv 4 b) (a_bv _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn)))))))))
+(% f3 (th_holds (= (BitVec 4) (a_var_bv _ b) (a_bv _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))))))
+(: (holds cln)
+
+;; (decl_bv_term_var 5 a (\ ba1
+;; (decl_bv_term_var 5 b (\ ba2
+;; (decl_bv_term_const _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ c (\ ba3
+;; (decl_bv_term_const _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ d (\ ba4
+
+(decl_atom (bitof a 4) (\ v1 (\ a1
+(decl_atom (bitof b 4) (\ v2 (\ a2
+
+; bitblasting terms
+(decl_bblast _ _ _ (bv_bbl_var 4 a _ ) (\ bt1
+(decl_bblast _ _ _ (bv_bbl_var 4 b _ ) (\ bt2
+(decl_bblast _ _ _ (bv_bbl_const 4 _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ bt3
+(decl_bblast _ _ _ (bv_bbl_const 4 _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ bt4
+(decl_bblast _ _ _ (bv_bbl_bvand 4 _ _ _ _ _ bt1 bt3) (\ bt5
+
+; bitblasting formulas
+(th_let_pf _ (bv_bbl_= _ _ _ _ _ _ bt1 bt2) (\ bf1
+(th_let_pf _ (bv_bbl_bvult _ _ _ _ _ _ bt1 bt5) (\ bf2
+(th_let_pf _ (bv_bbl_= _ _ _ _ _ _ bt2 bt4) (\ bf3
+
+; CNFication
+; a.4 V ~b.4
+(satlem _ _
+(asf _ _ _ a1 (\ l1
+(ast _ _ _ a2 (\ l2
+(clausify_false
+  trust
+))))) (\ C2
+
+; ~a.4
+(satlem _ _
+(ast _ _ _ a1 (\ l1
+(clausify_false
+  trust
+))) (\ C3
+
+; b.4
+(satlem _ _
+(asf _ _ _ a2 (\ l2
+(clausify_false
+  trust
+))) (\ C6
+
+
+(satlem_simplify _ _ _
+(R _ _ (R _ _ C6 C2 v2) C3 v1) (\ x x))
+
+)))))))))))))))))))))))))))))))))))))))))))))
diff --git a/test/signatures/example-arrays.plf b/test/signatures/example-arrays.plf
new file mode 100644
index 000000000..0e840274f
--- /dev/null
+++ b/test/signatures/example-arrays.plf
@@ -0,0 +1,139 @@
+; Deps: sat.plf smt.plf th_base.plf th_arrays.plf
+
+; --------------------------------------------------------------------------------
+; literals :
+; L1 : a = write( a, i, read( a, i )
+; L2 : read( a, k ) = read( write( a, i, read( a, i ) ), k )
+; L3 : i = k
+
+; input :
+; ~L1
+
+; (extenstionality) lemma :
+; L1 or ~L2
+
+; theory conflicts :
+; L2 or ~L3
+; L2 or L3
+
+
+;  With the theory lemma, the input is unsatisfiable.
+; --------------------------------------------------------------------------------
+
+
+; (0) -------------------- term declarations -----------------------------------
+
+(check
+(% I sort
+(% E sort
+(% a (term (Array I E))
+(% i (term I)
+
+
+; (1) -------------------- input formula -----------------------------------
+
+(% A1 (th_holds (not (= (Array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i)))))
+
+
+
+
+; (2) ------------------- specify that the following is a proof of the empty clause -----------------
+
+(: (holds cln)
+
+
+
+
+; (3) -------------------- theory lemmas prior to rewriting/preprocess/CNF -----------------
+;     ---  these should introduce (th_holds ...)
+
+
+; extensionality lemma : notice this also introduces skolem k
+(ext _ _ a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i)) (\ k (\ A2
+
+
+
+
+; (4) -------------------- map theory literals to boolean variables
+;     --- maps all theory literals involved in proof to boolean literals
+
+(decl_atom (= (Array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) (\ v1 (\ a1
+(decl_atom (= E (apply _ _ (apply _ _ (read I E) a) k) (apply _ _ (apply _ _ (read I E) (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) k)) (\ v2 (\ a2
+(decl_atom (= I i k) (\ v3 (\ a3
+
+
+
+; (5) -------------------- theory conflicts ---------------------------------------------
+;     ---  these should introduce (holds ...)
+
+(satlem _ _
+(asf _ _ _ a3 (\ l3
+(asf _ _ _ a2 (\ l2
+(clausify_false
+
+   ; use read over write rule "row"
+   (contra _ (symm _ _ _ (row _ _ _ _ a (apply _ _ (apply _ _ (read I E) a) i) l3)) l2)
+
+))))) (\ CT1
+; CT1 is the clause ( v2 V v3 )
+
+(satlem _ _
+(ast _ _ _ a3 (\ l3
+(asf _ _ _ a2 (\ l2
+(clausify_false
+
+   ; use read over write rule "row1"
+   (contra _ (symm _ _ _
+   	     (trans _ _ _ _
+               (symm _ _ _ (cong _ _ _ _ _ _
+               	 (refl _ (apply _ _ (read I E) (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))))
+               	 l3))
+               (trans _ _ _ _
+                 (row1 _ _ a i (apply _ _ (apply _ _ (read I E) a) i))
+                 (cong _ _ _ _ _ _ (refl _ (apply _ _ (read I E) a)) l3)
+                 )))
+            l2)
+
+))))) (\ CT2
+; CT2 is the clause ( v2 V ~v3 )
+
+
+; (6) -------------------- clausification -----------------------------------------
+;     ---  these should introduce (holds ...)
+
+(satlem _ _
+(ast _ _ _ a1 (\ l1
+(clausify_false
+
+; input formula A1 is ( ~a1 )
+; the following is a proof of a1 ^ ( ~a1 ) => false
+
+  (contra _ l1 A1)
+
+))) (\ C1
+; C1 is the clause ( ~v1 )
+
+
+(satlem _ _
+(asf _ _ _ a1 (\ l1
+(ast _ _ _ a2 (\ l2
+(clausify_false
+
+; lemma A2 is ( a1 V ~a2 )
+; the following is a proof of ~a1 ^ a2 ^ ( a1 V ~a2 ) => false
+
+  (contra _ l2 (or_elim_1 _ _ l1 A2))
+
+))))) (\ C2
+; C2 is the clause ( v1 V ~v2 )
+
+
+; (7) -------------------- resolution proof ------------------------------------------------------------
+
+(satlem_simplify _ _ _
+
+(R _ _ (R _ _ CT1 CT2 v3) (R _ _ C2 C1 v1) v2)
+
+(\ x x))
+
+)))))))))))))))))))))))))))
diff --git a/test/signatures/example-quant.plf b/test/signatures/example-quant.plf
new file mode 100644
index 000000000..611fd182c
--- /dev/null
+++ b/test/signatures/example-quant.plf
@@ -0,0 +1,95 @@
+; Deps: sat.plf smt.plf th_base.plf th_quant.plf
+
+; --------------------------------------------------------------------------------
+; literals :
+; L1 : forall x. x != x
+; L2 : t = t
+
+; input :
+; L1
+
+; (instantiation) lemma : 
+; L1 => L2
+
+; theory conflicts :
+; ~L2
+
+
+;  With the theory lemma, the input is unsatisfiable.
+; --------------------------------------------------------------------------------
+
+
+; (0) -------------------- term declarations -----------------------------------
+
+(check
+(% s sort
+(% t (term s)
+
+
+; (1) -------------------- input formula -----------------------------------
+
+(% x (term s)
+(% A1 (th_holds (forall _ x (not (= _ x x))))
+
+
+
+; (2) ------------------- specify that the following is a proof of the empty clause -----------------
+
+(: (holds cln)
+
+
+
+; (3) -------------------- theory lemmas prior to rewriting/preprocess/CNF -----------------
+;     ---  these should introduce (th_holds ...)
+
+
+; instantiation lemma
+(inst _ _ _ t (not (= _ t t)) A1 (\ A2
+
+
+
+
+; (4) -------------------- map theory literals to boolean variables
+;     --- maps all theory literals involved in proof to boolean literals
+
+(decl_atom (forall _ x (not (= _ x x))) (\ v1 (\ a1
+(decl_atom (= _ t t) (\ v2 (\ a2
+
+
+
+
+; (5) -------------------- theory conflicts ---------------------------------------------
+;     ---  these should introduce (holds ...)
+
+(satlem _ _
+(asf _ _ _ a2 (\ l2
+(clausify_false
+
+   (contra _ (refl _ t) l2)
+   
+))) (\ CT1
+; CT1 is the clause ( v2 )
+
+
+; (6) -------------------- clausification -----------------------------------------
+;     ---  these should introduce (holds ...)
+
+(satlem _ _
+(ast _ _ _ a2 (\ l2
+(clausify_false
+
+  (contra _ l2 A2)
+
+))) (\ C1
+; C1 is the clause ( ~v2 )
+
+
+; (7) -------------------- resolution proof ------------------------------------------------------------
+
+(satlem_simplify _ _ _
+
+(R _ _ CT1 C1 v2)
+
+(\ x x))
+
+))))))))))))))))))
diff --git a/test/signatures/example.plf b/test/signatures/example.plf
new file mode 100644
index 000000000..775557fa6
--- /dev/null
+++ b/test/signatures/example.plf
@@ -0,0 +1,116 @@
+; Deps: sat.plf smt.plf th_base.plf
+
+; --------------------------------------------------------------------------------
+; input :
+; ( a = b )
+; ( b = f(c) )
+; ( a != f(c) V a != b )
+
+; theory lemma (by transitivity) :
+; ( a != b V b != f(c) V a = f(c) )
+
+
+;  With the theory lemma, the input is unsatisfiable.
+; --------------------------------------------------------------------------------
+
+
+
+(check
+(% s sort
+(% a (term s)
+(% b (term s)
+(% c (term s)
+(% f (term (arrow s s))
+
+; -------------------- declaration of input formula -----------------------------------
+
+(% A1 (th_holds (= s a b))
+(% A2 (th_holds (= s b (apply _ _ f c)))
+(% A3 (th_holds (or (not (= s a (apply _ _ f c))) (not (= s a b))))
+
+
+; ------------------- specify that the following is a proof of the empty clause -----------------
+
+(: (holds cln)
+
+; ---------- use atoms (a1, a2, a3) to map theory literals to boolean literals (v1, v2, v3) ------
+
+(decl_atom (= s a b) (\ v1 (\ a1
+(decl_atom (= s b (apply _ _ f c)) (\ v2 (\ a2
+(decl_atom (= s a (apply _ _ f c)) (\ v3 (\ a3
+
+
+; --------------------------- proof of theory lemma ---------------------------------------------
+
+(satlem _ _
+(ast _ _ _ a1 (\ l1
+(ast _ _ _ a2 (\ l2
+(asf _ _ _ a3 (\ l3
+(clausify_false
+
+; this should be a proof of l1 ^ l2 ^ ~l3 => false
+; this is done by theory proof rules (currently just use "trust")
+
+  trust
+
+))))))) (\ CT
+; CT is the clause ( ~v1 V ~v2 V v3 )
+
+; -------------------- clausification of input formulas -----------------------------------------
+
+(satlem _ _
+(asf _ _ _ a1 (\ l1
+(clausify_false
+
+; input formula A1 is ( ~l1 )
+; the following should be a proof of l1 ^ ( ~l1 ) => false
+; this is done by natural deduction rules
+
+  (contra _ A1 l1)
+
+))) (\ C1
+; C1 is the clause ( v1 )
+
+
+(satlem _ _
+(asf _ _ _ a2 (\ l2
+(clausify_false
+
+; input formula A2 is ( ~l2 )
+; the following should be a proof of l2 ^ ( ~l2 ) => false
+; this is done by natural deduction rules
+
+   (contra _ A2 l2)
+
+))) (\ C2
+; C2 is the clause ( v2 )
+
+
+(satlem _ _
+(ast _ _ _ a3 (\ l3
+(ast _ _ _ a1 (\ l1
+(clausify_false
+
+; input formula A3 is ( ~a3 V ~a1 )
+; the following should be a proof of a3 ^ a1 ^ ( ~a3 V ~a1 ) => false
+; this is done by natural deduction rules
+
+  (contra _ l1 (or_elim_1 _ _ (not_not_intro _ l3) A3))
+
+))))) (\ C3
+; C3 is the clause ( ~v3 V ~v1 )
+
+
+
+; -------------------- resolution proof ------------------------------------------------------------
+
+(satlem_simplify _ _ _
+
+(R _ _ C1
+(R _ _ C2
+(R _ _ CT C3 v3) v2) v1)
+
+(\ x x))
+
+))))))))))))))))))))))))))
+)
diff --git a/test/signatures/lrat_test.plf b/test/signatures/lrat_test.plf
new file mode 100644
index 000000000..466216ff9
--- /dev/null
+++ b/test/signatures/lrat_test.plf
@@ -0,0 +1,892 @@
+; Deps: lrat.plf
+(declare test_clause_append
+         (! c1 clause
+            (! c2 clause
+               (! cr clause
+                  (! sc (^ (clause_append c1 c2) cr) type)))))
+
+; Test passes if the (test_clause_append ...) application is well-typed.
+(check
+  (% v1 var
+  (% v2 var
+  (% v3 var
+    (test_clause_append
+      (clc (pos v1) (clc (neg v2) cln))
+      (clc (pos v3) (clc (neg v2) cln))
+      (clc (pos v1) (clc (neg v2) (clc (pos v3) (clc (neg v2) cln))))
+    )
+  )))
+)
+
+; Test passes if the (test_clause_append ...) application is well-typed.
+(check
+  (% v2 var
+  (% v3 var
+    (test_clause_append
+      cln
+      (clc (pos v3) (clc (neg v2) cln))
+      (clc (pos v3) (clc (neg v2) cln))
+    )
+  ))
+)
+
+; Test passes if the (test_clause_append ...) application is well-typed.
+(check
+  (% v2 var
+  (% v3 var
+    (test_clause_append
+      (clc (pos v3) (clc (neg v2) cln))
+      cln
+      (clc (pos v3) (clc (neg v2) cln))
+    )
+  ))
+)
+
+(declare test_CMap_remove_many
+         (! is CIList
+            (! cs CMap
+               (! csr CMap
+                  (! sc (^ (CMap_remove_many is cs) csr) type)))))
+
+; Test passes if the (test_CMap_remove_many ...) application is well-typed.
+(check
+  (% v1 var
+  (% v2 var
+  (% v3 var
+  (% v4 var
+    (@ c1 (clc (pos v4) (clc (neg v2) cln))
+    (@ c2 (clc (neg v3) (clc (neg v1) cln))
+    (@ c3 (clc (neg v2) (clc (pos v3) cln))
+    (@ c4 (clc (neg v3) (clc (neg v4) cln))
+      (@ cs_in (CMapc 0 c1 (CMapc 3 c2 (CMapc 4 c3 (CMapc 5 c3 (CMapc 6 c4 CMapn)))))
+      (@ cs_out (CMapc 3 c2 (CMapc 5 c3 CMapn))
+      (@ is_in (CIListc 0 (CIListc 4 (CIListc 6 CIListn)))
+        (test_CMap_remove_many
+          is_in
+          cs_in
+          cs_out
+        )
+      )))
+    ))))
+  ))))
+)
+
+; Test passes if the (test_CMap_remove_many ...) application is well-typed.
+(check
+  (% v1 var
+  (% v2 var
+  (% v3 var
+  (% v4 var
+    (@ c1 (clc (pos v4) (clc (neg v2) cln))
+    (@ c2 (clc (neg v3) (clc (neg v1) cln))
+    (@ c3 (clc (neg v2) (clc (pos v3) cln))
+    (@ c4 (clc (neg v3) (clc (neg v4) cln))
+      (@ cs_in (CMapc 0 c1 (CMapc 3 c2 (CMapc 4 c3 (CMapc 5 c3 (CMapc 6 c4 CMapn)))))
+      (@ cs_out (CMapc 0 c1 (CMapc 3 c2 (CMapc 5 c3 (CMapc 6 c4 CMapn))))
+      (@ is_in (CIListc 4 CIListn)
+        (test_CMap_remove_many
+          is_in
+          cs_in
+          cs_out
+        )
+      )))
+    ))))
+  ))))
+)
+
+(declare test_clause_remove_all
+         (! l lit
+            (! c clause
+               (! c' clause
+                  (! sc (^ (clause_remove_all l c) c') type)))))
+
+; Test passes if the (test_clause_remove_all ...) application is well-typed.
+(check
+  (% v1 var
+  (% v2 var
+  (% v3 var
+  (% v4 var
+    (@ c1 (clc (pos v4) (clc (neg v2) (clc (neg v2) (clc (pos v2) (clc (pos v1) cln)))))
+    (@ c2 (clc (pos v4) (clc (pos v2) (clc (pos v1) cln)))
+      (test_clause_remove_all
+        (neg v2)
+        c1
+        c2
+      )
+    ))
+  ))))
+)
+
+(declare test_collect_resolution_targets
+         (! cs CMap
+            (! c clause
+               (! is CIList
+                  (! sc (^ (collect_resolution_targets cs c) is) type)))))
+
+; Test passes if the (test_collect_resolution_targets ...) application is well-typed.
+(check
+  (% v1 var
+  (% v2 var
+  (% v3 var
+  (% v4 var
+    (@ c1 (clc (pos v3) (clc (neg v2) cln))
+    (@ c2 (clc (neg v3) (clc (neg v1) cln))
+    (@ c3 (clc (neg v2) (clc (pos v3) cln))
+    (@ c4 (clc (neg v3) (clc (pos v3) cln))
+    (@ ct (clc (neg v3) (clc (neg v4) cln))
+      (@ cs_in (CMapc 0 c1 (CMapc 3 c2 (CMapc 4 c3 (CMapc 5 c3 (CMapc 6 c4 CMapn)))))
+      (@ is_out (CIListc 0 (CIListc 4 (CIListc 5 (CIListc 6 CIListn))))
+        (test_collect_resolution_targets
+          cs_in
+          ct
+          is_out
+        )
+      )))
+    ))))
+  ))))
+)
+
+(declare test_resolution_targets_match
+         (! c CIList
+            (! g RATHints
+               (! ans bool
+                  (! sc (^ (resolution_targets_match c g) ans) type)))))
+
+; Test passes if the (test_resolution_targets_match ...) application is well-typed.
+(check
+  (@ idxs_in (CIListc 0 (CIListc 4 (CIListc 5 (CIListc 6 CIListn))))
+  (@ hints_in
+     (RATHintsc 0 Tracen
+     (RATHintsc 4 Tracen
+     (RATHintsc 5 Tracen
+     (RATHintsc 6 Tracen
+     RATHintsn))))
+    (test_resolution_targets_match
+      idxs_in
+      hints_in
+      tt
+    )
+  ))
+)
+
+; Test passes if the (test_resolution_targets_match ...) application is well-typed.
+(check
+  (@ idxs_in (CIListc 0 (CIListc 2 (CIListc 5 (CIListc 6 CIListn))))
+  (@ hints_in
+     (RATHintsc 0 Tracen
+     (RATHintsc 4 Tracen
+     (RATHintsc 5 Tracen
+     (RATHintsc 6 Tracen
+     RATHintsn))))
+    (test_resolution_targets_match
+      idxs_in
+      hints_in
+      ff
+    )
+  ))
+)
+
+(declare test_is_at_trace
+         (! cs CMap
+            (! c clause
+               (! t Trace
+                  (! r UPResult
+                    (! sc (^ (is_at_trace cs c t) r) type))))))
+
+; Test passes if the (test_is_at_trace ...) application is well-typed.
+(check
+  (% v1 var
+  (% v2 var
+  (% v3 var
+  (% v4 var
+    (@ c1 (clc (pos v3) (clc (neg v2) cln))
+    (@ c2 (clc (neg v3) (clc (neg v1) cln))
+    (@ c3 (clc (neg v2) (clc (pos v1) cln))
+    (@ c4 (clc (neg v3) (clc (pos v2) cln))
+      (@ cs (CMapc 0 c1 (CMapc 3 c2 (CMapc 5 c3 (CMapc 6 c4 CMapn))))
+      (@ c  (clc (neg v3) cln)
+      (@ t  (Tracec 3 (Tracec 5 (Tracec 6 Tracen)))
+        (test_is_at_trace
+          cs
+          c
+          t
+          UPR_Bottom
+        )
+      )))
+    ))))
+  ))))
+)
+
+; Test passes if the (test_is_at_trace ...) application is well-typed.
+(check
+  (% v1 var
+  (% v2 var
+  (% v3 var
+  (% v4 var
+    (@ c1 (clc (pos v3) (clc (neg v2) cln))
+    (@ c2 (clc (neg v3) (clc (neg v1) cln))
+    (@ c3 (clc (neg v2) (clc (pos v1) cln))
+    (@ c4 (clc (neg v3) (clc (pos v2) cln))
+      (@ cs (CMapc 0 c1 (CMapc 3 c2 (CMapc 5 c3 (CMapc 6 c4 CMapn))))
+      (@ c  (clc (neg v3) cln)
+      (@ t  (Tracec 3 (Tracec 5 Tracen))
+        (test_is_at_trace
+          cs
+          c
+          t
+          UPR_Ok
+        )
+      )))
+    ))))
+  ))))
+)
+
+; Test passes if the (test_is_at_trace ...) application is well-typed.
+(check
+  (% v1 var
+  (% v2 var
+  (% v3 var
+  (% v4 var
+    (@ c1 (clc (pos v3) (clc (neg v2) cln))
+    (@ c2 (clc (neg v3) (clc (neg v1) cln))
+    (@ c3 (clc (neg v2) (clc (pos v1) cln))
+    (@ c4 (clc (neg v3) (clc (pos v2) cln))
+      (@ cs (CMapc 1 c1 (CMapc 2 c2 (CMapc 3 c3 (CMapc 4 c4 CMapn))))
+      (@ c  (clc (neg v3) cln)
+      (@ t  (Tracec 2 (Tracec 1 Tracen))
+        (test_is_at_trace
+          cs
+          c
+          t
+          UPR_Broken
+        )
+      )))
+    ))))
+  ))))
+)
+
+(declare test_is_rat_trace (! cs CMap
+            (! c clause
+               (! t Trace
+                  (! h RATHints
+                     (! r UPResult
+                       (! sc (^ (is_rat_trace cs c t h) r) type)))))))
+
+; Test passes if the (test_is_rat_trace ...) application is well-typed.
+(check
+  (% v1 var
+  (% v2 var
+  (% v3 var
+  (% v4 var
+    (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))
+    (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))
+    (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))
+    (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))
+    (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))
+    (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))
+    (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))
+    (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))
+      (@ cs (CMapc 1 c1
+            (CMapc 2 c2
+            (CMapc 3 c3
+            (CMapc 4 c4
+            (CMapc 5 c5
+            (CMapc 6 c6
+            (CMapc 7 c7
+            (CMapc 8 c8 CMapn))))))))
+      (@ c  (clc (pos v1) cln)
+      (@ t  Tracen
+      (@ h  (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen))
+            (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen))
+            (RATHintsc 7 (Tracec 6 (Tracec 1 Tracen))
+                       RATHintsn)))
+        (test_is_rat_trace
+          cs
+          c
+          t
+          h
+          UPR_Bottom
+        )
+      ))))
+    ))))))))
+  ))))
+)
+
+; Test passes if the (test_is_rat_trace ...) application is well-typed.
+(check
+  (% v1 var
+  (% v2 var
+  (% v3 var
+  (% v4 var
+    (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))
+    (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))
+    (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))
+    (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))
+    (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))
+    (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))
+    (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))
+    (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))
+      (@ cs (CMapc 1 c1
+            (CMapc 2 c2
+            (CMapc 3 c3
+            (CMapc 4 c4
+            (CMapc 5 c5
+            (CMapc 6 c6
+            (CMapc 7 c7
+            (CMapc 8 c8 CMapn))))))))
+      (@ c  (clc (pos v1) cln)
+      (@ t  Tracen
+      (@ h  (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen))
+            (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen))
+                       RATHintsn))
+        (test_is_rat_trace
+          cs
+          c
+          t
+          h
+          UPR_Broken
+        )
+      ))))
+    ))))))))
+  ))))
+)
+
+; Test passes if the (test_is_rat_trace ...) application is well-typed.
+(check
+  (% v1 var
+  (% v2 var
+  (% v3 var
+  (% v4 var
+    (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))
+    (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))
+    (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))
+    (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))
+    (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))
+    (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))
+    (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))
+    (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))
+      (@ cs (CMapc 1 c1
+            (CMapc 2 c2
+            (CMapc 3 c3
+            (CMapc 4 c4
+            (CMapc 5 c5
+            (CMapc 6 c6
+            (CMapc 7 c7
+            (CMapc 8 c8 CMapn))))))))
+      (@ c  (clc (pos v1) cln)
+      (@ t  Tracen
+      (@ h  (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen))
+            (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen))
+            (RATHintsc 7 (Tracec 3 (Tracec 1 Tracen))
+                       RATHintsn)))
+        (test_is_rat_trace
+          cs
+          c
+          t
+          h
+          UPR_Broken
+        )
+      ))))
+    ))))))))
+  ))))
+)
+
+; Test passes if the (test_is_rat_trace ...) application is well-typed.
+(check
+  (% v1 var
+  (% v2 var
+  (% v3 var
+  (% v4 var
+    (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))
+    (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))
+    (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))
+    (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))
+    (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))
+    (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))
+    (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))
+    (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))
+      (@ cs (CMapc 1 c1
+            (CMapc 2 c2
+            (CMapc 3 c3
+            (CMapc 4 c4
+            (CMapc 5 c5
+            (CMapc 6 c6
+            (CMapc 7 c7
+            (CMapc 8 c8 CMapn))))))))
+      (@ c  (clc (pos v1) cln)
+      (@ t  Tracen
+      (@ h  (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen))
+            (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen))
+            (RATHintsc 7 (Tracec 3 Tracen)
+                       RATHintsn)))
+        (test_is_rat_trace
+          cs
+          c
+          t
+          h
+          UPR_Broken
+        )
+      ))))
+    ))))))))
+  ))))
+)
+
+; Test passes if the (test_is_rat_trace ...) application is well-typed.
+(check
+  (% v1 var
+  (% v2 var
+  (% v3 var
+  (% v4 var
+    (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))
+    (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))
+    (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))
+    (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))
+    (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))
+    (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))
+    (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))
+    (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))
+    (@ c9 (clc (pos v1) cln)
+      (@ cs (CMapc 1 c1
+            (CMapc 2 c2
+            (CMapc 3 c3
+            (CMapc 4 c4
+            (CMapc 5 c5
+            (CMapc 6 c6
+            (CMapc 7 c7
+            (CMapc 8 c8
+            (CMapc 9 c9
+                   CMapn)))))))))
+      (@ c  (clc (pos v2) cln)
+      (@ t  (Tracec 9 (Tracec 7 (Tracec 5 (Tracec 3 Tracen))))
+      (@ h  RATHintsn
+        (test_is_rat_trace
+          cs
+          c
+          t
+          h
+          UPR_Bottom
+        )
+      ))))
+    )))))))))
+  ))))
+)
+
+; Test passes if the (test_is_rat_trace ...) application is well-typed.
+(check
+  (% v1 var
+  (% v2 var
+  (% v3 var
+  (% v4 var
+    (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))
+    (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))
+    (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))
+    (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))
+    (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))
+    (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))
+    (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))
+    (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))
+    (@ c9 (clc (pos v1) cln)
+    (@ c10 (clc (pos v2) cln)
+      (@ cs (CMapc 1 c1
+            (CMapc 2 c2
+            (CMapc 3 c3
+            (CMapc 4 c4
+            (CMapc 5 c5
+            (CMapc 6 c6
+            (CMapc 7 c7
+            (CMapc 8 c8
+            (CMapc 9 c9
+            (CMapc 10 c10
+                   CMapn))))))))))
+      (@ c  cln
+      (@ t  (Tracec 9 (Tracec 10 (Tracec 2 (Tracec 4 (Tracec 5 Tracen)))))
+      (@ h  RATHintsn
+        (test_is_rat_trace
+          cs
+          c
+          t
+          h
+          UPR_Bottom
+        )
+      ))))
+    ))))))))))
+  ))))
+)
+
+(declare test_is_lrat_proof_of_bottom
+            (! f CMap
+               (! p LRATProof
+                  (! r bool
+                     (! sc (^ (is_lrat_proof_of_bottom f p) r) type)))))
+
+; Test passes if the (test_is_lrat_proof_of_bottom ...) application is well-typed.
+(check
+  (% v1 var
+  (% v2 var
+  (% v3 var
+  (% v4 var
+    (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))
+    (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))
+    (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))
+    (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))
+    (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))
+    (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))
+    (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))
+    (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))
+      (@ cs (CMapc 1 c1
+            (CMapc 2 c2
+            (CMapc 3 c3
+            (CMapc 4 c4
+            (CMapc 5 c5
+            (CMapc 6 c6
+            (CMapc 7 c7
+            (CMapc 8 c8
+                   CMapn))))))))
+      (@ p
+            (LRATProofa 9
+                        (clc (pos v1) cln)
+                        Tracen
+                        (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen))
+                          (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen))
+                          (RATHintsc 7 (Tracec 6 (Tracec 1 Tracen))
+                                     RATHintsn)))
+            (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 CIListn)))
+            (LRATProofa 10
+                        (clc (pos v2) cln)
+                        (Tracec 9 (Tracec 7 (Tracec 5 (Tracec 3 Tracen))))
+                        RATHintsn
+            (LRATProofd (CIListc 3 (CIListc 7 CIListn))
+            (LRATProofa 11
+                        cln
+                        (Tracec 9 (Tracec 10 (Tracec 2 (Tracec 4 (Tracec 5 Tracen)))))
+                        RATHintsn
+            LRATProofn)))))
+            (test_is_lrat_proof_of_bottom
+              cs
+              p
+              tt
+            )
+      ))
+    ))))))))
+  ))))
+)
+
+; Test passes if the (test_is_lrat_proof_of_bottom ...) application is well-typed.
+(check
+  (% v1 var
+  (% v2 var
+  (% v3 var
+  (% v4 var
+    (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))
+    (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))
+    (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))
+    (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))
+    (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))
+    (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))
+    (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))
+    (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))
+      (@ cs (CMapc 1 c1
+            (CMapc 2 c2
+            (CMapc 3 c3
+            (CMapc 4 c4
+            (CMapc 5 c5
+            (CMapc 6 c6
+            (CMapc 7 c7
+            (CMapc 8 c8
+                   CMapn))))))))
+      (@ p
+            (LRATProofa 9
+                        (clc (pos v1) cln)
+                        Tracen
+                        (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen))
+                          (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen))
+                          (RATHintsc 7 (Tracec 6 (Tracec 1 Tracen))
+                                     RATHintsn)))
+            (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 CIListn)))
+            (LRATProofa 10
+                        (clc (pos v2) cln)
+                        (Tracec 9 (Tracec 7 (Tracec 5 (Tracec 3 Tracen))))
+                        RATHintsn
+            (LRATProofd (CIListc 3 (CIListc 7 CIListn))
+            (LRATProofa 11
+                        cln
+                        (Tracec 9 (Tracec 10 (Tracec 2 (Tracec 4 Tracen))))
+                        RATHintsn
+            LRATProofn)))))
+            (test_is_lrat_proof_of_bottom
+              cs
+              p
+              ff
+            )
+      ))
+    ))))))))
+  ))))
+)
+
+; Proof from Figure 2 of "Efficient Certified RAT Verification"
+(check
+  (% v1 var
+  (% v2 var
+  (% v3 var
+  (% v4 var
+    (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))))
+    (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))))
+    (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))))
+    (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))))
+    (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))))
+    (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))))
+    (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))))
+    (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))))
+      (@ pf_cmap
+         (CMapc_proof 1 _ _ _ pf_c1
+         (CMapc_proof 2 _ _ _ pf_c2
+         (CMapc_proof 3 _ _ _ pf_c3
+         (CMapc_proof 4 _ _ _ pf_c4
+         (CMapc_proof 5 _ _ _ pf_c5
+         (CMapc_proof 6 _ _ _ pf_c6
+         (CMapc_proof 7 _ _ _ pf_c7
+         (CMapc_proof 8 _ _ _ pf_c8
+                      CMapn_proof))))))))
+      (@ lrat_proof_witness
+            (LRATProofa 9
+                        (clc (pos v1) cln)
+                        Tracen
+                        (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen))
+                          (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen))
+                          (RATHintsc 7 (Tracec 6 (Tracec 1 Tracen))
+                                     RATHintsn)))
+            (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 CIListn)))
+            (LRATProofa 10
+                        (clc (pos v2) cln)
+                        (Tracec 9 (Tracec 7 (Tracec 5 (Tracec 3 Tracen))))
+                        RATHintsn
+            (LRATProofd (CIListc 3 (CIListc 7 CIListn))
+            (LRATProofa 11
+                        cln
+                        (Tracec 9 (Tracec 10 (Tracec 2 (Tracec 4 (Tracec 5 Tracen)))))
+                        RATHintsn
+            LRATProofn)))))
+            (:
+              (holds cln)
+              (lrat_proof_of_bottom _ pf_cmap lrat_proof_witness))
+      ))
+    ))))))))
+  ))))
+)
+
+; Proof from Figure 2 of "Efficient Certified RAT Verification"
+; With duplicates
+(check
+  (% v1 var
+  (% v2 var
+  (% v3 var
+  (% v4 var
+    (% pf_c1 (holds (clc (pos v1) (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))))
+    (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))))
+    (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (pos v3) (clc (pos v3) (clc (neg v4) cln))))))
+    (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))))
+    (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) (clc (neg v4) cln)))))
+    (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v3) (clc (pos v4) cln)))))
+    (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))))
+    (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v2) (clc (neg v4) cln)))))
+      (@ pf_cmap
+         (CMapc_proof 1 _ _ _ pf_c1
+         (CMapc_proof 2 _ _ _ pf_c2
+         (CMapc_proof 3 _ _ _ pf_c3
+         (CMapc_proof 4 _ _ _ pf_c4
+         (CMapc_proof 5 _ _ _ pf_c5
+         (CMapc_proof 6 _ _ _ pf_c6
+         (CMapc_proof 7 _ _ _ pf_c7
+         (CMapc_proof 8 _ _ _ pf_c8
+                      CMapn_proof))))))))
+      (@ lrat_proof_witness
+            (LRATProofa 9
+                        (clc (pos v1) cln)
+                        Tracen
+                        (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen))
+                          (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen))
+                          (RATHintsc 7 (Tracec 6 (Tracec 1 Tracen))
+                                     RATHintsn)))
+            (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 CIListn)))
+            (LRATProofa 10
+                        (clc (pos v2) cln)
+                        (Tracec 9 (Tracec 7 (Tracec 5 (Tracec 3 Tracen))))
+                        RATHintsn
+            (LRATProofd (CIListc 3 (CIListc 7 CIListn))
+            (LRATProofa 11
+                        cln
+                        (Tracec 9 (Tracec 10 (Tracec 2 (Tracec 4 (Tracec 5 Tracen)))))
+                        RATHintsn
+            LRATProofn)))))
+            (:
+              (holds cln)
+              (lrat_proof_of_bottom _ pf_cmap lrat_proof_witness))
+      ))
+    ))))))))
+  ))))
+)
+
+; Clauses 1 and 9 are identical.
+(check
+  (% v1 var
+  (% v2 var
+  (% v3 var
+  (% v4 var
+    (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))))
+    (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))))
+    (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))))
+    (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))))
+    (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))))
+    (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))))
+    (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))))
+    (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))))
+    (% pf_c9 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))))
+      (@ pf_cmap
+         (CMapc_proof 1 _ _ _ pf_c1
+         (CMapc_proof 2 _ _ _ pf_c2
+         (CMapc_proof 3 _ _ _ pf_c3
+         (CMapc_proof 4 _ _ _ pf_c4
+         (CMapc_proof 5 _ _ _ pf_c5
+         (CMapc_proof 6 _ _ _ pf_c6
+         (CMapc_proof 7 _ _ _ pf_c7
+         (CMapc_proof 8 _ _ _ pf_c8
+         (CMapc_proof 9 _ _ _ pf_c9
+                      CMapn_proof)))))))))
+      (@ lrat_proof_witness
+            (LRATProofa 10
+                        (clc (pos v1) cln)
+                        Tracen
+                        (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen))
+                          (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen))
+                          (RATHintsc 7 (Tracec 6 (Tracec 9 Tracen))
+                                     RATHintsn)))
+            (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 (CIListc 9 CIListn))))
+            (LRATProofa 11
+                        (clc (pos v2) cln)
+                        (Tracec 10 (Tracec 7 (Tracec 5 (Tracec 3 Tracen))))
+                        RATHintsn
+            (LRATProofd (CIListc 3 (CIListc 7 CIListn))
+            (LRATProofa 12
+                        cln
+                        (Tracec 10 (Tracec 11 (Tracec 2 (Tracec 4 (Tracec 5 Tracen)))))
+                        RATHintsn
+            LRATProofn)))))
+            (:
+              (holds cln)
+              (lrat_proof_of_bottom _ pf_cmap lrat_proof_witness))
+      ))
+    )))))))))
+  ))))
+)
+
+; Clauses 1 and 9 are logically identical, but the literals have been reordered.
+(check
+  (% v1 var
+  (% v2 var
+  (% v3 var
+  (% v4 var
+    (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))))
+    (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))))
+    (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))))
+    (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))))
+    (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))))
+    (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))))
+    (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))))
+    (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))))
+    (% pf_c9 (holds (clc (neg v3) (clc (pos v2) (clc (pos v1) cln))))
+      (@ pf_cmap
+         (CMapc_proof 1 _ _ _ pf_c1
+         (CMapc_proof 2 _ _ _ pf_c2
+         (CMapc_proof 3 _ _ _ pf_c3
+         (CMapc_proof 4 _ _ _ pf_c4
+         (CMapc_proof 5 _ _ _ pf_c5
+         (CMapc_proof 6 _ _ _ pf_c6
+         (CMapc_proof 7 _ _ _ pf_c7
+         (CMapc_proof 8 _ _ _ pf_c8
+         (CMapc_proof 9 _ _ _ pf_c9
+                      CMapn_proof)))))))))
+      (@ lrat_proof_witness
+            (LRATProofa 10
+                        (clc (pos v1) cln)
+                        Tracen
+                        (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen))
+                          (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen))
+                          (RATHintsc 7 (Tracec 6 (Tracec 9 Tracen))
+                                     RATHintsn)))
+            (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 (CIListc 9 CIListn))))
+            (LRATProofa 11
+                        (clc (pos v2) cln)
+                        (Tracec 10 (Tracec 7 (Tracec 5 (Tracec 3 Tracen))))
+                        RATHintsn
+            (LRATProofd (CIListc 3 (CIListc 7 CIListn))
+            (LRATProofa 12
+                        cln
+                        (Tracec 10 (Tracec 11 (Tracec 2 (Tracec 4 (Tracec 5 Tracen)))))
+                        RATHintsn
+            LRATProofn)))))
+            (:
+              (holds cln)
+              (lrat_proof_of_bottom _ pf_cmap lrat_proof_witness))
+      ))
+    )))))))))
+  ))))
+)
+
+; Proof from Figure 1 of "Efficient Certified RAT Verification"
+(check
+  (% v1 var
+  (% v2 var
+  (% v3 var
+  (% v4 var
+    (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))))
+    (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))))
+    (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))))
+    (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))))
+    (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))))
+    (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))))
+    (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))))
+    (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))))
+      (@ pf_cmap
+         (CMapc_proof 1 _ _ _ pf_c1
+         (CMapc_proof 2 _ _ _ pf_c2
+         (CMapc_proof 3 _ _ _ pf_c3
+         (CMapc_proof 4 _ _ _ pf_c4
+         (CMapc_proof 5 _ _ _ pf_c5
+         (CMapc_proof 6 _ _ _ pf_c6
+         (CMapc_proof 7 _ _ _ pf_c7
+         (CMapc_proof 8 _ _ _ pf_c8
+                      CMapn_proof))))))))
+      (@ lrat_proof_witness
+            (LRATProofa 9
+                        (clc (pos v1) (clc (pos v2) cln))
+                        (Tracec 1 (Tracec 6 (Tracec 3 Tracen)))
+                        RATHintsn
+            (LRATProofd (CIListc 1 CIListn)
+            (LRATProofa 10
+                        (clc (pos v1) (clc (pos v3) cln))
+                        (Tracec 9 (Tracec 8 (Tracec 6 Tracen)))
+                        RATHintsn
+            (LRATProofd (CIListc 6 CIListn)
+            (LRATProofa 11
+                        (clc (pos v1) cln)
+                        (Tracec 10 (Tracec 9 (Tracec 4 (Tracec 8 Tracen))))
+                        RATHintsn
+            (LRATProofd (CIListc 8 (CIListc 9 (CIListc 10 CIListn)))
+            (LRATProofa 12
+                        (clc (pos v2) cln)
+                        (Tracec 11 (Tracec 7 (Tracec 5 (Tracec 3 Tracen))))
+                        RATHintsn
+            (LRATProofd (CIListc 3 (CIListc 7 CIListn))
+            (LRATProofa 13
+                        cln
+                        (Tracec 11 (Tracec 12 (Tracec 2 (Tracec 4 (Tracec 5 Tracen)))))
+                        RATHintsn
+                        LRATProofn
+                        )))))))))
+            (:
+              (holds cln)
+              (lrat_proof_of_bottom _ pf_cmap lrat_proof_witness))
+      ))
+    ))))))))
+  ))))
+)
diff --git a/test/signatures/run_test.py b/test/signatures/run_test.py
new file mode 100755
index 000000000..ac14267e9
--- /dev/null
+++ b/test/signatures/run_test.py
@@ -0,0 +1,123 @@
+#!/usr/bin/env python
+
+import argparse
+import re
+import os.path
+import sys
+import subprocess
+
+
+class TestConfiguration(object):
+    """Represents a test to run."""
+    def __init__(self):
+        """Initialized from program arguments.
+        Exists with code 2 and prints usage message on invalid arguments."""
+        parser = argparse.ArgumentParser(
+            description='Runs `lfscc on a test file.')
+        parser.add_argument('lfscc_binary')
+        parser.add_argument('input')
+        parser.add_argument('include_dirs', nargs='*')
+        args = parser.parse_args()
+
+        self.lfscc = args.lfscc_binary
+        self.dep_graph = DepGraph(args.input, args.include_dirs)
+
+
+class DepGraph(object):
+    """Represents a dependency graph of LFSC input files"""
+    def __init__(self, root_path, include_dirs):
+        """Creates a dependency graph rooted a `root_path`.
+        Computes a root-last topological sort.
+        Exits with exitcode 1 on cyclic dependencies"""
+
+        # Root of the graph
+        self._r = root_path
+
+        # Nodes (paths) that have been visited
+        self._visited = set()
+
+        # Nodes (paths) that have been ordered
+        self._ordered_set = set()
+
+        # The order of nodes (paths). Root is last.
+        self._ordered_paths = []
+
+        self.include_dirs = include_dirs
+
+        # Start DFS topo-order
+        self._visit(root_path)
+
+    def _visit(self, p):
+        """Puts the descendents of p in the order, parent-last"""
+        node = TestFile(p, self.include_dirs)
+        self._visited.add(p)
+        for n in node.dep_paths:
+            if n not in self._ordered_set:
+                if n in self._visited:
+                    # Our child is is an ancestor our ours!?
+                    print("{} and {} are in a dependency cycle".format(p, n))
+                    sys.exit(1)
+                else:
+                    self._visit(n)
+        self._ordered_paths.append(p)
+        self._ordered_set.add(p)
+
+    def getPathsInOrder(self):
+        return self._ordered_paths
+
+
+class TestFile(object):
+    """Represents a testable input file to LFSC"""
+    def __init__(self, path, include_dirs):
+        """Read the file at `path` and determine its immediate dependencies"""
+        self.path = path
+        self._get_config_map()
+        self.deps = self.config_map['deps'].split() if (
+            'deps' in self.config_map) else []
+        self.dir = os.path.dirname(self.path)
+        self.dep_paths = []
+        include_paths = include_dirs + [self.dir]
+        for dep in self.deps:
+            found_dep = False
+            for include_path in include_paths:
+                dep_path = os.path.join(include_path, dep)
+                if os.path.isfile(dep_path):
+                    self.dep_paths.append(dep_path)
+                    found_dep = True
+                    break
+            assert found_dep
+
+    def _get_comment_lines(self):
+        """Return an iterator over comment lines, ;'s included"""
+        with open(self.path, 'r') as test_file:
+            return (line for line in test_file.readlines() if \
+                    re.match(r'^\s*;.*$', line) is not None)
+
+    def _get_config_map(self):
+        """Populate self.config_map.
+        Config variables are set using the syntax
+        ; Var Name Spaces Okay: space separated values"""
+        m = {}
+        for l in self._get_comment_lines():
+            match = re.match(r'^.*;\s*(\w+(?:\s+\w+)*)\s*:(.*)$', l)
+            if match is not None:
+                m[match.group(1).replace(' ', '').lower()] = match.group(2)
+        self.config_map = m
+
+
+def main():
+    configuration = TestConfiguration()
+    cmd = [configuration.lfscc] + configuration.dep_graph.getPathsInOrder()
+    result = subprocess.Popen(cmd,
+                              stderr=subprocess.STDOUT,
+                              stdout=subprocess.PIPE)
+    code = result.wait()
+    if 0 != code:
+        stdout = result.stdout.read()
+        if stdout:
+            print(stdout.decode())
+    return code
+
+
+if __name__ == '__main__':
+    sys.exit(main())
diff --git a/test/signatures/th_lira_test.plf b/test/signatures/th_lira_test.plf
new file mode 100644
index 000000000..d1fbe59f4
--- /dev/null
+++ b/test/signatures/th_lira_test.plf
@@ -0,0 +1,294 @@
+; Deps: th_lira.plf
+;; Proof (from predicates on linear polynomials) that the following imply bottom
+;
+; -x - 1/2 y + 2 >= 0
+;  x +     y - 8 >= 0
+;  x -     y + 0 >= 0
+;
+(check
+  ; Variables
+  (% x real_var
+  (% y real_var
+  ; linear combinations
+  (@ m1 (lc_cons (~ 1/1) (av_from_real x) (lc_cons (~ 1/2) (av_from_real y) lc_null))
+  (@ m2 (lc_cons 1/1 (av_from_real x)     (lc_cons 1/1     (av_from_real y) lc_null))
+  (@ m3 (lc_cons 1/1 (av_from_real x)     (lc_cons (~ 1/1) (av_from_real y) lc_null))
+  ; affine functions
+  (@ p1 (aff_cons 2/1 m1)
+  (@ p2 (aff_cons (~ 8/1) m2)
+  (@ p3 (aff_cons 0/1 m3)
+  ; Proofs of affine bounds
+  (% pf_nonneg_1 (th_holds (bounded_aff p1 bound_non_neg))
+  (% pf_nonneg_2 (th_holds (bounded_aff p2 bound_non_neg))
+  (% pf_nonneg_3 (th_holds (bounded_aff p3 bound_non_neg))
+     (:
+       (th_holds false)
+       (bounded_aff_contra _ _
+         (bounded_aff_add _ _ _ _ _
+           (bounded_aff_mul_c _ _ _ 4/1 pf_nonneg_1)
+           (bounded_aff_add _ _ _ _ _
+             (bounded_aff_mul_c _ _ _ 3/1 pf_nonneg_2)
+             (bounded_aff_add _ _ _ _ _
+               (bounded_aff_mul_c _ _ _ 1/1 pf_nonneg_3)
+               bounded_aff_ax_0_>=_0)))))
+  )))))
+  ))))
+  ))
+)
+
+;; Proof (from predicates on real terms) that the following imply bottom
+;
+; -x - 1/2 y >= 2
+;  x +     y >= 8
+;  x -     y >= 0
+;
+(check
+  ; Declarations
+  ; Variables
+  (% x real_var
+  (% y real_var
+  ; real predicates
+  (@ f1 (>=_Real (+_Real (*_Real (a_real (~ 1/1)) (term_real_var x)) (*_Real (a_real (~ 1/2)) (term_real_var y))) (a_real (~ 2/1)))
+  (@ f2 (>=_Real (+_Real (*_Real (a_real 1/1) (term_real_var x)) (*_Real (a_real 1/1) (term_real_var y))) (a_real 8/1))
+  (@ f3 (>=_Real (+_Real (*_Real (a_real 1/1) (term_real_var x)) (*_Real (a_real (~ 1/1)) (term_real_var y))) (a_real 0/1))
+  ; proof of real predicates
+  (% pf_f1 (th_holds f1)
+  (% pf_f2 (th_holds f2)
+  (% pf_f3 (th_holds f3)
+
+
+  ; Normalization
+  ; real term -> linear polynomial normalization witnesses
+  (@ n1 (aff_>=_from_term  _ _ _
+        (is_aff_- _ _ _ _ _
+          (is_aff_+ _ _ _ _ _
+            (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_real x))
+            (is_aff_mul_c_L _ _ _ (~ 1/2) (is_aff_var_real y)))
+          (is_aff_const (~ 2/1)))
+        pf_f1)
+  (@ n2 (aff_>=_from_term  _ _ _
+        (is_aff_- _ _ _ _ _
+          (is_aff_+ _ _ _ _ _
+            (is_aff_mul_c_L _ _ _ 1/1 (is_aff_var_real x))
+            (is_aff_mul_c_L _ _ _ 1/1 (is_aff_var_real y)))
+          (is_aff_const 8/1))
+        pf_f2)
+  (@ n3 (aff_>=_from_term  _ _ _
+        (is_aff_- _ _ _ _ _
+          (is_aff_+ _ _ _ _ _
+            (is_aff_mul_c_L _ _ _ 1/1 (is_aff_var_real x))
+            (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_real y)))
+          (is_aff_const 0/1))
+        pf_f3)
+
+  ; derivation of a contradiction using farkas coefficients
+    (:
+      (th_holds false)
+      (bounded_aff_contra _ _
+       (bounded_aff_add _ _ _ _ _
+         (bounded_aff_mul_c _ _ _ 4/1 n1)
+         (bounded_aff_add _ _ _ _ _
+           (bounded_aff_mul_c _ _ _ 3/1 n2)
+           (bounded_aff_add _ _ _ _ _
+             (bounded_aff_mul_c _ _ _ 1/1 n3)
+             bounded_aff_ax_0_>=_0)))))
+  )))
+  )))
+  )))
+  ))
+)
+
+;; Term proof, 2 premises of the form (>=), one of the form (not >=)
+;; Proof (from predicates on real terms) that the following imply bottom
+;
+;        -x +     y >=  2
+;         x +     y >=  2
+;     not[        y >= -2] => [y < -2] => [-y > 2]
+;
+(check
+  ; Declarations
+  ; Variables
+  (% x real_var
+  (% y real_var
+  ; real predicates
+  (@ f1 (>=_Real
+          (+_Real (*_Real (a_real (~ 1/1)) (term_real_var x)) (term_real_var y))
+          (a_real 2/1))
+  (@ f2 (>=_Real
+          (+_Real (term_real_var x) (term_real_var y))
+          (a_real 2/1))
+  (@ f3 (not (>=_Real (term_real_var y) (a_real (~ 2/1))))
+
+  ; Normalization
+  ; proof of real predicates
+  (% pf_f1 (th_holds f1)
+  (% pf_f2 (th_holds f2)
+  (% pf_f3 (th_holds f3)
+  ; real term -> linear polynomial normalization witnesses
+  (@ n1 (aff_>=_from_term  _ _ _
+        (is_aff_- _ _ _ _ _
+          (is_aff_+ _ _ _ _ _
+            (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_real x))
+            (is_aff_var_real y))
+          (is_aff_const 2/1))
+        pf_f1)
+  (@ n2 (aff_>=_from_term  _ _ _
+        (is_aff_- _ _ _ _ _
+          (is_aff_+ _ _ _ _ _
+            (is_aff_var_real x)
+            (is_aff_var_real y))
+          (is_aff_const 2/1))
+        pf_f2)
+  (@ n3 (aff_>_from_term _ _ _ _
+        (is_aff_- _ _ _ _ _
+          (is_aff_var_real y)
+          (is_aff_const (~ 2/1)))
+        pf_f3)
+
+  ; derivation of a contradiction using farkas coefficients
+    (:
+      (th_holds false)
+      (bounded_aff_contra _ _
+       (bounded_aff_add _ _ _ _ _
+         (bounded_aff_mul_c _ _ _ 1/1 n1)
+         (bounded_aff_add _ _ _ _ _
+           (bounded_aff_mul_c _ _ _ 1/1 n2)
+           (bounded_aff_add _ _ _ _ _
+             (bounded_aff_mul_c _ _ _ 2/1 n3)
+             bounded_aff_ax_0_>=_0)))))
+  )))
+  )))
+  )))
+  ))
+)
+
+;; Term proof, 2 premises of the form (>=), one of the form (not >=)
+;; x is a real,
+;; y is an integer
+;; Proof (from predicates on real terms) that the following imply bottom
+;
+;        -x +     y >=  2
+;         x +     y >=  2
+;     not[        y >= -2] => [y < -2] => [-y > 2]
+;
+(check
+  ; Declarations
+  ; Variables
+  (% x real_var
+  (% y int_var
+  ; real predicates
+  (@ f1 (>=_Real
+          (+_Real (*_Real (a_real (~ 1/1)) (term_real_var x)) (term_int_to_real (term_int_var y)))
+          (a_real 2/1))
+  (@ f2 (>=_Real
+          (+_Real (term_real_var x) (term_int_to_real (term_int_var y)))
+          (a_real 2/1))
+  (@ f3 (not (>=_IntReal (term_int_var y) (a_real (~ 2/1))))
+
+  ; Normalization
+  ; proof of real predicates
+  (% pf_f1 (th_holds f1)
+  (% pf_f2 (th_holds f2)
+  (% pf_f3 (th_holds f3)
+  ; real term -> linear polynomial normalization witnesses
+  (@ n1 (aff_>=_from_term  _ _ _
+        (is_aff_- _ _ _ _ _
+          (is_aff_+ _ _ _ _ _
+            (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_real x))
+            (is_aff_var_int y))
+          (is_aff_const 2/1))
+        (pf_reified_arith_pred _ _ pf_f1))
+  (@ n2 (aff_>=_from_term  _ _ _
+        (is_aff_- _ _ _ _ _
+          (is_aff_+ _ _ _ _ _
+            (is_aff_var_real x)
+            (is_aff_var_int y))
+          (is_aff_const 2/1))
+        (pf_reified_arith_pred _ _ pf_f2))
+  (@ n3 (aff_>_from_term _ _ _ _
+        (is_aff_- _ _ _ _ _
+          (is_aff_var_int y)
+          (is_aff_const (~ 2/1)))
+        (pf_reified_arith_pred _ _ pf_f3))
+
+  ; derivation of a contradiction using farkas coefficients
+    (:
+      (th_holds false)
+      (bounded_aff_contra _ _
+       (bounded_aff_add _ _ _ _ _
+         (bounded_aff_mul_c _ _ _ 1/1 n1)
+         (bounded_aff_add _ _ _ _ _
+           (bounded_aff_mul_c _ _ _ 1/1 n2)
+           (bounded_aff_add _ _ _ _ _
+             (bounded_aff_mul_c _ _ _ 2/1 n3)
+             bounded_aff_ax_0_>=_0)))))
+  )))
+  )))
+  )))
+  ))
+)
+
+;; Term proof, 2 premises of the form (>=), one of the form (not >=)
+;; x is a real,
+;; y is an integer, and needs tightening
+;; Proof (from predicates on real terms) that the following imply bottom
+;
+;        -x         >=  -1/2
+;         x +     y >=  0
+;     not[        y >=  0] => [y < 0] => [-y >= 1]
+;
+(check
+  ; Declarations
+  ; Variables
+  (% x real_var
+  (% y int_var
+  ; real predicates
+  (@ f1 (>=_Real
+          (*_Real (a_real (~ 1/1)) (term_real_var x))
+          (a_real (~ 1/2)))
+  (@ f2 (>=_Real
+          (+_Real (term_real_var x) (term_int_to_real (term_int_var y)))
+          (a_real 0/1))
+  (@ f3 (not (>=_IntReal (*_Int (a_int 1) (term_int_var y)) (term_int_to_real (a_int 0))))
+
+  ; Normalization
+  ; proof of real predicates
+  (% pf_f1 (th_holds f1)
+  (% pf_f2 (th_holds f2)
+  (% pf_f3 (th_holds f3)
+  ; real term -> linear polynomial normalization witnesses
+  (@ n1 (aff_>=_from_term  _ _ _
+        (is_aff_- _ _ _ _ _
+          (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_real x))
+          (is_aff_const (~ 1/2)))
+        (pf_reified_arith_pred _ _ pf_f1))
+  (@ n2 (aff_>=_from_term  _ _ _
+        (is_aff_- _ _ _ _ _
+          (is_aff_+ _ _ _ _ _
+            (is_aff_var_real x)
+            (is_aff_var_int y))
+          (is_aff_const 0/1))
+        (pf_reified_arith_pred _ _ pf_f2))
+  (@ n3 (aff_>=_from_term _ _ _
+        (is_aff_- _ _ _ _ _
+          (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_int y))
+          (is_aff_const 1/1))
+        (pf_reified_arith_pred _ _
+          (tighten_not_>=_IntInt _ _ _ _ (check_neg_of_greatest_integer_below_int 1 0) pf_f3)))
+
+  ; derivation of a contradiction using farkas coefficients
+    (:
+      (th_holds false)
+      (bounded_aff_contra _ _
+       (bounded_aff_add _ _ _ _ _
+         (bounded_aff_mul_c _ _ _ 1/1 n1)
+         (bounded_aff_add _ _ _ _ _
+           (bounded_aff_mul_c _ _ _ 1/1 n2)
+           (bounded_aff_add _ _ _ _ _
+             (bounded_aff_mul_c _ _ _ 1/1 n3)
+             bounded_aff_ax_0_>=_0)))))
+  )))
+  )))
+  )))
+  ))
+)