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

17 files changed, 8 insertions, 2186 deletions

diff --git a/proofs/signatures/drat.plf b/proofs/signatures/drat.plf
index 2f70bbfbd..ad3c8ec8d 100644
--- a/proofs/signatures/drat.plf
+++ b/proofs/signatures/drat.plf
@@ -1,4 +1,4 @@
-; Depends on lrat.plf
+; Deps: lrat.plf
 ;
 ; Implementation of DRAT checking.
 ;
diff --git a/proofs/signatures/drat_test.plf b/proofs/signatures/drat_test.plf
deleted file mode 100644
index 2ede6df34..000000000
--- a/proofs/signatures/drat_test.plf
+++ /dev/null
@@ -1,434 +0,0 @@
-;depends on 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/proofs/signatures/er.plf b/proofs/signatures/er.plf
index 9fcc9d4e8..6a8a059a2 100644
--- a/proofs/signatures/er.plf
+++ b/proofs/signatures/er.plf
@@ -1,4 +1,4 @@
-; Depends on sat.plf
+; Deps: sat.plf
 
 ; This file exists to support the **definition introduction** (or **extension**)
 ; rule in the paper:
diff --git a/proofs/signatures/er_test.plf b/proofs/signatures/er_test.plf
deleted file mode 100644
index 1b5117a70..000000000
--- a/proofs/signatures/er_test.plf
+++ /dev/null
@@ -1,89 +0,0 @@
-; Depends on 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/proofs/signatures/ex-mem.plf b/proofs/signatures/ex-mem.plf
deleted file mode 100644
index 7e143c5b6..000000000
--- a/proofs/signatures/ex-mem.plf
+++ /dev/null
@@ -1,62 +0,0 @@
-(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/proofs/signatures/ex_bv.plf b/proofs/signatures/ex_bv.plf
deleted file mode 100644
index 332d7765c..000000000
--- a/proofs/signatures/ex_bv.plf
+++ /dev/null
@@ -1,58 +0,0 @@
-; (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/proofs/signatures/example-arrays.plf b/proofs/signatures/example-arrays.plf
deleted file mode 100644
index 03dc0831c..000000000
--- a/proofs/signatures/example-arrays.plf
+++ /dev/null
@@ -1,139 +0,0 @@
-; to check, run : lfscc sat.plf smt.plf th_base.plf th_arrays.plf example-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/proofs/signatures/example-quant.plf b/proofs/signatures/example-quant.plf
deleted file mode 100644
index 086633be9..000000000
--- a/proofs/signatures/example-quant.plf
+++ /dev/null
@@ -1,95 +0,0 @@
-; to check, run : lfsc sat.plf smt.plf th_base.plf example.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/proofs/signatures/example.plf b/proofs/signatures/example.plf
deleted file mode 100644
index ab690eb51..000000000
--- a/proofs/signatures/example.plf
+++ /dev/null
@@ -1,116 +0,0 @@
-; to check, run : lfsc sat.plf smt.plf th_base.plf example.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/proofs/signatures/lrat.plf b/proofs/signatures/lrat.plf
index d16791624..b5d46be43 100644
--- a/proofs/signatures/lrat.plf
+++ b/proofs/signatures/lrat.plf
@@ -2,7 +2,7 @@
 ; LRAT format detailed in "Efficient Certified RAT Verification"
 ; Link: https://www.cs.utexas.edu/~marijn/publications/lrat.pdf
 ; Author: aozdemir
-; Depends On: sat.plf, smt.plf
+; Deps: sat.plf smt.plf
 
 
 ; A general note about the design of the side conditions:
diff --git a/proofs/signatures/lrat_test.plf b/proofs/signatures/lrat_test.plf
deleted file mode 100644
index 0663a08f7..000000000
--- a/proofs/signatures/lrat_test.plf
+++ /dev/null
@@ -1,891 +0,0 @@
-(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/proofs/signatures/smt.plf b/proofs/signatures/smt.plf
index 57dc5bd1e..9f6e71986 100644
--- a/proofs/signatures/smt.plf
+++ b/proofs/signatures/smt.plf
@@ -3,7 +3,7 @@
 ; SMT syntax and semantics (not theory-specific)
 ;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-; depends on sat.plf
+; Deps: sat.plf
 
 (declare formula type)
 (declare th_holds (! f formula type))
diff --git a/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf
index acfbd2f3b..5517d9a4f 100644
--- a/proofs/signatures/th_arrays.plf
+++ b/proofs/signatures/th_arrays.plf
@@ -3,7 +3,7 @@
 ; Theory of Arrays
 ;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-; depends on : th_base.plf
+; Deps: th_base.plf
 
 ; sorts
 
diff --git a/proofs/signatures/th_base.plf b/proofs/signatures/th_base.plf
index d6b283752..d5182007e 100644
--- a/proofs/signatures/th_base.plf
+++ b/proofs/signatures/th_base.plf
@@ -5,7 +5,7 @@
 ; Theory of Equality and Congruence Closure
 ;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-; depends on : smt.plf
+; Deps: smt.plf
 
 ; sorts :
 
diff --git a/proofs/signatures/th_lira.plf b/proofs/signatures/th_lira.plf
index 70cdfc733..af326bf27 100644
--- a/proofs/signatures/th_lira.plf
+++ b/proofs/signatures/th_lira.plf
@@ -1,4 +1,4 @@
-; Depends on th_real.plf, th_int.plf, smt.plf, sat.plf
+; Deps: th_real.plf th_int.plf smt.plf sat.plf
 
 ; Some axiom arguments are marked "; Omit", because they can be deduced from
 ; other arguments and should be replaced with a "_" when invoking the axiom.
diff --git a/proofs/signatures/th_lira_test.plf b/proofs/signatures/th_lira_test.plf
deleted file mode 100644
index 91d626bba..000000000
--- a/proofs/signatures/th_lira_test.plf
+++ /dev/null
@@ -1,294 +0,0 @@
-; Depends On: 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)))))
-  )))
-  )))
-  )))
-  ))
-)
diff --git a/proofs/signatures/th_real.plf b/proofs/signatures/th_real.plf
index 112328b63..dfedb28ed 100644
--- a/proofs/signatures/th_real.plf
+++ b/proofs/signatures/th_real.plf
@@ -1,4 +1,4 @@
-; Depends On: th_smt.plf
+; Deps: smt.plf
 (declare Real sort)
 
 (define arithpred_Real (! x (term Real)