Processing utilities
  i i i i i i i       ooooo    o        ooooooo   ooooo   ooooo
  I I I I I I I      8     8   8           8     8     o  8    8
  I  \ `+' /  I      8         8           8     8        8    8
   \  `-+-'  /       8         8           8      ooooo   8oooo
    `-__|__-'        8         8           8           8  8
        |            8     o   8           8     o     8  8
  ------+------       ooooo    8oooooo  ooo8ooo   ooooo   8

Welcome to GNU CLISP 2.48 (2009-07-28) <http://clisp.cons.org/>

Copyright (c) Bruno Haible, Michael Stoll 1992, 1993
Copyright (c) Bruno Haible, Marcus Daniels 1994-1997
Copyright (c) Bruno Haible, Pierpaolo Bernardi, Sam Steingold 1998
Copyright (c) Bruno Haible, Sam Steingold 1999-2000
Copyright (c) Sam Steingold, Bruno Haible 2001-2009

Type :h and hit Enter for context help.

Milawa Proof Checker.
1> VERIFY THEOREM-SUBSTITUTE-INTO-NOT-PEQUAL
;; Reading from Proofs/utilities/thm-theorem-substitute-into-not-pequal.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
2> VERIFY THEOREM-NOT-T-OR-NOT-NIL
;; Reading from Proofs/utilities/thm-theorem-not-t-or-not-nil.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
3> DEFINE NOT
;; Reading from Proofs/utilities/admit-not.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4> VERIFY NOT
;; Reading from Proofs/utilities/thm-not.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
5> DEFINE IFF
;; Reading from Proofs/utilities/admit-iff.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
6> VERIFY IFF
;; Reading from Proofs/utilities/thm-iff.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
7> VERIFY THEOREM-COMMUTATIVITY-OF-PEQUAL
;; Reading from Proofs/utilities/thm-theorem-commutativity-of-pequal.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
8> VERIFY THEOREM-TRANSITIVITY-OF-PEQUAL
;; Reading from Proofs/utilities/thm-theorem-transitivity-of-pequal.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
9> VERIFY THEOREM-REFLEXIVITY-OF-EQUAL
;; Reading from Proofs/utilities/thm-theorem-reflexivity-of-equal.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
10> VERIFY THEOREM-EQUAL-NIL-OR-T
;; Reading from Proofs/utilities/thm-theorem-equal-nil-or-t.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
11> VERIFY THEOREM-SYMMETRY-OF-EQUAL
;; Reading from Proofs/utilities/thm-theorem-symmetry-of-equal.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
12> VERIFY THEOREM-TRANSITIVITY-OF-EQUAL
;; Reading from Proofs/utilities/thm-theorem-transitivity-of-equal.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
13> VERIFY THEOREM-EQUAL-OF-EQUAL-AND-T
;; Reading from Proofs/utilities/thm-theorem-equal-of-equal-and-t.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
14> VERIFY THEOREM-IF-REDUX-SAME
;; Reading from Proofs/utilities/thm-theorem-if-redux-same.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
15> VERIFY THEOREM-IF-WHEN-SAME
;; Reading from Proofs/utilities/thm-theorem-if-when-same.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
16> VERIFY THEOREM-IF-REDUX-THEN
;; Reading from Proofs/utilities/thm-theorem-if-redux-then.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
17> VERIFY THEOREM-IF-REDUX-ELSE
;; Reading from Proofs/utilities/thm-theorem-if-redux-else.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
18> VERIFY THEOREM-IF-REDUX-TEST
;; Reading from Proofs/utilities/thm-theorem-if-redux-test.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
19> VERIFY THEOREM-IF-REDUX-NIL
;; Reading from Proofs/utilities/thm-theorem-if-redux-nil.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
20> VERIFY THEOREM-IF-REDUX-T
;; Reading from Proofs/utilities/thm-theorem-if-redux-t.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
21> VERIFY THEOREM-IFF-LHS-FALSE
;; Reading from Proofs/utilities/thm-theorem-iff-lhs-false.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
22> VERIFY THEOREM-IFF-LHS-TRUE
;; Reading from Proofs/utilities/thm-theorem-iff-lhs-true.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
23> VERIFY THEOREM-IFF-RHS-FALSE
;; Reading from Proofs/utilities/thm-theorem-iff-rhs-false.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
24> VERIFY THEOREM-IFF-RHS-TRUE
;; Reading from Proofs/utilities/thm-theorem-iff-rhs-true.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
25> VERIFY THEOREM-IFF-BOTH-TRUE
;; Reading from Proofs/utilities/thm-theorem-iff-both-true.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
26> VERIFY THEOREM-IFF-BOTH-FALSE
;; Reading from Proofs/utilities/thm-theorem-iff-both-false.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
27> VERIFY THEOREM-IFF-TRUE-FALSE
;; Reading from Proofs/utilities/thm-theorem-iff-true-false.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
28> VERIFY THEOREM-IFF-FALSE-TRUE
;; Reading from Proofs/utilities/thm-theorem-iff-false-true.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
29> VERIFY THEOREM-IFF-T-WHEN-NOT-NIL
;; Reading from Proofs/utilities/thm-theorem-iff-t-when-not-nil.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
30> VERIFY THEOREM-IFF-T-WHEN-NIL
;; Reading from Proofs/utilities/thm-theorem-iff-t-when-nil.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
31> VERIFY THEOREM-IFF-NIL-WHEN-NIL
;; Reading from Proofs/utilities/thm-theorem-iff-nil-when-nil.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
32> VERIFY THEOREM-IFF-NIL-WHEN-NOT-NIL
;; Reading from Proofs/utilities/thm-theorem-iff-nil-when-not-nil.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
33> VERIFY THEOREM-IFF-NIL-OR-T
;; Reading from Proofs/utilities/thm-theorem-iff-nil-or-t.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
34> VERIFY THEOREM-REFLEXIVITY-OF-IFF
;; Reading from Proofs/utilities/thm-theorem-reflexivity-of-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
35> VERIFY THEOREM-SYMMETRY-OF-IFF
;; Reading from Proofs/utilities/thm-theorem-symmetry-of-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
36> VERIFY THEOREM-IFF-CONGRUENCE-LEMMA
;; Reading from Proofs/utilities/thm-theorem-iff-congruence-lemma.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
37> VERIFY THEOREM-IFF-CONGRUENCE-LEMMA-2
;; Reading from Proofs/utilities/thm-theorem-iff-congruence-lemma-2.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
38> VERIFY THEOREM-IFF-CONGRUENT-IF-1
;; Reading from Proofs/utilities/thm-theorem-iff-congruent-if-1.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
39> VERIFY THEOREM-IFF-CONGRUENT-IFF-2
;; Reading from Proofs/utilities/thm-theorem-iff-congruent-iff-2.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
40> VERIFY THEOREM-IFF-CONGRUENT-IFF-1
;; Reading from Proofs/utilities/thm-theorem-iff-congruent-iff-1.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
41> VERIFY THEOREM-TRANSITIVITY-OF-IFF
;; Reading from Proofs/utilities/thm-theorem-transitivity-of-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
42> VERIFY THEOREM-IFF-FROM-PEQUAL
;; Reading from Proofs/utilities/thm-theorem-iff-from-pequal.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
43> VERIFY THEOREM-IFF-FROM-EQUAL
;; Reading from Proofs/utilities/thm-theorem-iff-from-equal.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
44> VERIFY THEOREM-NOT-WHEN-NIL
;; Reading from Proofs/utilities/thm-theorem-not-when-nil.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
45> VERIFY THEOREM-NOT-WHEN-NOT-NIL
;; Reading from Proofs/utilities/thm-theorem-not-when-not-nil.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
46> VERIFY THEOREM-NOT-OF-NOT
;; Reading from Proofs/utilities/thm-theorem-not-of-not.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
47> VERIFY THEOREM-IFF-OF-IF-X-T-NIL
;; Reading from Proofs/utilities/thm-theorem-iff-of-if-x-t-nil.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
48> VERIFY THEOREM-NOT-OF-NOT-UNDER-IFF
;; Reading from Proofs/utilities/thm-theorem-not-of-not-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
49> VERIFY THEOREM-IFF-WHEN-NOT-NIL
;; Reading from Proofs/utilities/thm-theorem-iff-when-not-nil.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
50> VERIFY CLAUSE.THEOREM-STANDARDIZE-EQUAL-X-NIL
;; Reading from Proofs/utilities/thm-clause.theorem-standardize-equal-x-nil.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
51> VERIFY CLAUSE.THEOREM-STANDARDIZE-EQUAL-NIL-X
;; Reading from Proofs/utilities/thm-clause.theorem-standardize-equal-nil-x.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
52> VERIFY CLAUSE.THEOREM-STANDARDIZE-IFF-X-NIL
;; Reading from Proofs/utilities/thm-clause.theorem-standardize-iff-x-nil.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
53> VERIFY CLAUSE.THEOREM-STANDARDIZE-IFF-NIL-X
;; Reading from Proofs/utilities/thm-clause.theorem-standardize-iff-nil-x.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
54> VERIFY THEOREM-CONS-IS-NOT-NIL
;; Reading from Proofs/utilities/thm-theorem-cons-is-not-nil.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
55> VERIFY THEOREM-INEQUALITY-OF-NOT-X-AND-X
;; Reading from Proofs/utilities/thm-theorem-inequality-of-not-x-and-x.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
56> VERIFY THEOREM-NOT-X-AND-X-UNDER-IFF
;; Reading from Proofs/utilities/thm-theorem-not-x-and-x-under-iff.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
57> VERIFY RW.EQTRACE-CONTRADICTION-LEMMA1
;; Reading from Proofs/utilities/thm-rw.eqtrace-contradiction-lemma1.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
58> VERIFY RW.THEOREM-IFF-IMPLIES-PEQUAL-IF-1
;; Reading from Proofs/utilities/thm-rw.theorem-iff-implies-pequal-if-1.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
59> VERIFY RW.THEOREM-EQUAL-IMPLIES-PEQUAL-IF-2
;; Reading from Proofs/utilities/thm-rw.theorem-equal-implies-pequal-if-2.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
60> VERIFY RW.THEOREM-EQUAL-IMPLIES-PEQUAL-IF-3
;; Reading from Proofs/utilities/thm-rw.theorem-equal-implies-pequal-if-3.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
61> VERIFY RW.THEOREM-IFF-IMPLIES-EQUAL-IF-COMBINED
;; Reading from Proofs/utilities/thm-rw.theorem-iff-implies-equal-if-combined.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.08 seconds
62> VERIFY RW.THEOREM-IFF-IMPLIES-IFF-IF-2
;; Reading from Proofs/utilities/thm-rw.theorem-iff-implies-iff-if-2.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
63> VERIFY RW.THEOREM-IFF-IMPLIES-IFF-IF-3
;; Reading from Proofs/utilities/thm-rw.theorem-iff-implies-iff-if-3.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
64> VERIFY RW.THEOREM-IFF-IMPLIES-IFF-IF-COMBINED
;; Reading from Proofs/utilities/thm-rw.theorem-iff-implies-iff-if-combined.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.09 seconds
65> VERIFY RW.THEOREM-IFF-IMPLIES-EQUAL-IF-SPECIALCASE-NIL
;; Reading from Proofs/utilities/thm-rw.theorem-iff-implies-equal-if-specialcase-nil.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 seconds
66> VERIFY RW.THEOREM-IFF-IMPLIES-IFF-IF-SPECIALCASE-NIL
;; Reading from Proofs/utilities/thm-rw.theorem-iff-implies-iff-if-specialcase-nil.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
67> VERIFY RW.THEOREM-IFF-IMPLIES-EQUAL-IF-SPECIALCASE-T
;; Reading from Proofs/utilities/thm-rw.theorem-iff-implies-equal-if-specialcase-t.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
68> VERIFY RW.THEOREM-IFF-IMPLIES-IFF-IF-SPECIALCASE-T
;; Reading from Proofs/utilities/thm-rw.theorem-iff-implies-iff-if-specialcase-t.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
69> VERIFY RW.THEOREM-EQUAL-OF-IF-X-Y-Y
;; Reading from Proofs/utilities/thm-rw.theorem-equal-of-if-x-y-y.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.08 seconds
70> VERIFY RW.THEOREM-IFF-OF-IF-X-Y-Y
;; Reading from Proofs/utilities/thm-rw.theorem-iff-of-if-x-y-y.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.10 seconds
71> VERIFY RW.CREWRITE-RULE-LEMMA
;; Reading from Proofs/utilities/thm-rw.crewrite-rule-lemma.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
72> VERIFY RW.COMPILE-NOT-LEMMA1
;; Reading from Proofs/utilities/thm-rw.compile-not-lemma1.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 seconds
73> VERIFY CLAUSE.THEOREM-AUX-SPLIT-POSITIVE
;; Reading from Proofs/utilities/thm-clause.theorem-aux-split-positive.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
74> VERIFY CLAUSE.THEOREM-AUX-SPLIT-NEGATIVE
;; Reading from Proofs/utilities/thm-clause.theorem-aux-split-negative.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
75> VERIFY CLAUSE.CASES-LEMMA
;; Reading from Proofs/utilities/thm-clause.cases-lemma.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
76> VERIFY TACTIC.FERTILIZE-LEMMA1-HELPER
;; Reading from Proofs/utilities/thm-tactic.fertilize-lemma1-helper.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
77> DEFINE IMPLIES
;; Reading from Proofs/utilities/admit-implies.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
78> VERIFY IMPLIES
;; Reading from Proofs/utilities/thm-implies.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
79> VERIFY REFLEXIVITY-OF-EQUAL
;; Reading from Proofs/utilities/thm-reflexivity-of-equal.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
80> VERIFY SYMMETRY-OF-EQUAL
;; Reading from Proofs/utilities/thm-symmetry-of-equal.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
81> VERIFY EQUAL-OF-T-AND-EQUAL
;; Reading from Proofs/utilities/thm-equal-of-t-and-equal.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.08 seconds
82> VERIFY CONSP-OF-CONS
;; Reading from Proofs/utilities/thm-consp-of-cons.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
83> DEFINE NFIX
;; Reading from Proofs/utilities/admit-nfix.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
84> VERIFY NFIX
;; Reading from Proofs/utilities/thm-nfix.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
85> DEFINE <=
;; Reading from Proofs/utilities/admit-_lt__eq_.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
86> VERIFY <=
;; Reading from Proofs/utilities/thm-_lt__eq_.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
87> DEFINE ZP
;; Reading from Proofs/utilities/admit-zp.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
88> VERIFY ZP
;; Reading from Proofs/utilities/thm-zp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
89> DEFINE MIN
;; Reading from Proofs/utilities/admit-min.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
90> VERIFY MIN
;; Reading from Proofs/utilities/thm-min.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
91> DEFINE MAX
;; Reading from Proofs/utilities/admit-max.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
92> VERIFY MAX
;; Reading from Proofs/utilities/thm-max.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
93> DEFINE MAX3
;; Reading from Proofs/utilities/admit-max3.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
94> VERIFY MAX3
;; Reading from Proofs/utilities/thm-max3.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
95> DEFINE BOOLEANP
;; Reading from Proofs/utilities/admit-booleanp.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
96> VERIFY BOOLEANP
;; Reading from Proofs/utilities/thm-booleanp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
97> VERIFY EQUAL-OF-BOOLEANS-REWRITE
;; Reading from Proofs/utilities/thm-equal-of-booleans-rewrite.proof
;; Reading the file took 0.35 seconds
;; Checking the proof took 0.54 seconds
;; VERIFY took 2.84 seconds
98> VERIFY BOOLEANP-OF-BOOLEANP
;; Reading from Proofs/utilities/thm-booleanp-of-booleanp.proof
;; Reading the file took 0.16 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.59 seconds
99> VERIFY BOOLEANP-OF-EQUAL
;; Reading from Proofs/utilities/thm-booleanp-of-equal.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.18 seconds
100> VERIFY BOOLEANP-OF-NOT
;; Reading from Proofs/utilities/thm-booleanp-of-not.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.33 seconds
101> VERIFY BOOLEANP-OF-IFF
;; Reading from Proofs/utilities/thm-booleanp-of-iff.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.25 seconds
102> VERIFY BOOLEANP-OF-ZP
;; Reading from Proofs/utilities/thm-booleanp-of-zp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.13 seconds
103> VERIFY EQUAL-OF-NIL-ONE
;; Reading from Proofs/utilities/thm-equal-of-nil-one.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.17 seconds
104> VERIFY EQUAL-OF-NIL-TWO
;; Reading from Proofs/utilities/thm-equal-of-nil-two.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.15 seconds
105> VERIFY IFF-OF-NIL-ONE
;; Reading from Proofs/utilities/thm-iff-of-nil-one.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
106> VERIFY IFF-OF-NIL-TWO
;; Reading from Proofs/utilities/thm-iff-of-nil-two.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
107> VERIFY IFF-OF-T-LEFT
;; Reading from Proofs/utilities/thm-iff-of-t-left.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.07 seconds
108> VERIFY IFF-OF-T-RIGHT
;; Reading from Proofs/utilities/thm-iff-of-t-right.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.07 seconds
109> VERIFY BOOLEANP-OF-CONSP
;; Reading from Proofs/utilities/thm-booleanp-of-consp.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.26 seconds
110> VERIFY CAR-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-car-when-not-consp.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.21 seconds
111> VERIFY CDR-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-cdr-when-not-consp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.21 seconds
112> VERIFY CAR-OF-CONS
;; Reading from Proofs/utilities/thm-car-of-cons.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
113> VERIFY CDR-OF-CONS
;; Reading from Proofs/utilities/thm-cdr-of-cons.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.05 seconds
114> VERIFY CONS-OF-CAR-AND-CDR
;; Reading from Proofs/utilities/thm-cons-of-car-and-cdr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.07 seconds
115> VERIFY EQUAL-OF-CONS-REWRITE
;; Reading from Proofs/utilities/thm-equal-of-cons-rewrite.proof
;; Reading the file took 0.19 seconds
;; Checking the proof took 0.44 seconds
;; VERIFY took 1.91 seconds
116> VERIFY BOOLEANP-OF-SYMBOLP
;; Reading from Proofs/utilities/thm-booleanp-of-symbolp.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.33 seconds
117> VERIFY BOOLEANP-OF-SYMBOL-<
;; Reading from Proofs/utilities/thm-booleanp-of-symbol-_lt_.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.30 seconds
118> VERIFY IRREFLEXIVITY-OF-SYMBOL-<
;; Reading from Proofs/utilities/thm-irreflexivity-of-symbol-_lt_.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
119> VERIFY ANTISYMMETRY-OF-SYMBOL-<
;; Reading from Proofs/utilities/thm-antisymmetry-of-symbol-_lt_.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.16 seconds
120> VERIFY TRANSITIVITY-OF-SYMBOL-<
;; Reading from Proofs/utilities/thm-transitivity-of-symbol-_lt_.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.21 seconds
121> VERIFY TRICHOTOMY-OF-SYMBOL-<
;; Reading from Proofs/utilities/thm-trichotomy-of-symbol-_lt_.proof
;; Reading the file took 0.25 seconds
;; Checking the proof took 0.62 seconds
;; VERIFY took 2.81 seconds
122> VERIFY SYMBOL-<-COMPLETION-LEFT
;; Reading from Proofs/utilities/thm-symbol-_lt_-completion-left.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.49 seconds
123> VERIFY SYMBOL-<-COMPLETION-RIGHT
;; Reading from Proofs/utilities/thm-symbol-_lt_-completion-right.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.46 seconds
124> VERIFY BOOLEANP-OF-NATP
;; Reading from Proofs/utilities/thm-booleanp-of-natp.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.28 seconds
125> VERIFY SYMBOLP-WHEN-NATP-CHEAP
;; Reading from Proofs/utilities/thm-symbolp-when-natp-cheap.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.18 seconds
126> VERIFY SYMBOLP-WHEN-CONSP-CHEAP
;; Reading from Proofs/utilities/thm-symbolp-when-consp-cheap.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.16 seconds
127> VERIFY CONSP-WHEN-NATP-CHEAP
;; Reading from Proofs/utilities/thm-consp-when-natp-cheap.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.17 seconds
128> VERIFY BOOLEANP-WHEN-NATP-CHEAP
;; Reading from Proofs/utilities/thm-booleanp-when-natp-cheap.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.21 seconds
129> VERIFY BOOLEANP-WHEN-CONSP-CHEAP
;; Reading from Proofs/utilities/thm-booleanp-when-consp-cheap.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.23 seconds
130> VERIFY SYMBOLP-WHEN-BOOLEANP-CHEAP
;; Reading from Proofs/utilities/thm-symbolp-when-booleanp-cheap.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.19 seconds
131> VERIFY CONS-UNDER-IFF
;; Reading from Proofs/utilities/thm-cons-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.08 seconds
132> VERIFY EQUAL-OF-SYMBOL-AND-NON-SYMBOL-CHEAP
;; Reading from Proofs/utilities/thm-equal-of-symbol-and-non-symbol-cheap.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.16 seconds
133> VERIFY EQUAL-OF-NON-SYMBOL-AND-SYMBOL-CHEAP
;; Reading from Proofs/utilities/thm-equal-of-non-symbol-and-symbol-cheap.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.13 seconds
134> VERIFY EQUAL-OF-CONS-AND-NON-CONS-CHEAP
;; Reading from Proofs/utilities/thm-equal-of-cons-and-non-cons-cheap.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.13 seconds
135> VERIFY EQUAL-OF-NON-CONS-AND-CONS-CHEAP
;; Reading from Proofs/utilities/thm-equal-of-non-cons-and-cons-cheap.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.13 seconds
136> VERIFY EQUAL-OF-NAT-AND-NON-NAT-CHEAP
;; Reading from Proofs/utilities/thm-equal-of-nat-and-non-nat-cheap.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.14 seconds
137> VERIFY EQUAL-OF-NON-NAT-AND-NAT-CHEAP
;; Reading from Proofs/utilities/thm-equal-of-non-nat-and-nat-cheap.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.13 seconds
138> VERIFY CAR-WHEN-SYMBOLP-CHEAP
;; Reading from Proofs/utilities/thm-car-when-symbolp-cheap.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.37 seconds
139> VERIFY NOT-OF-NOT-UNDER-IFF
;; Reading from Proofs/utilities/thm-not-of-not-under-iff.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.10 seconds
140> VERIFY IMPLIES-OF-SELF
;; Reading from Proofs/utilities/thm-implies-of-self.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
141> VERIFY IMPLIES-OF-T-LEFT
;; Reading from Proofs/utilities/thm-implies-of-t-left.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.07 seconds
142> VERIFY IMPLIES-OF-T-RIGHT
;; Reading from Proofs/utilities/thm-implies-of-t-right.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.04 seconds
143> VERIFY IMPLIES-OF-NIL-LEFT
;; Reading from Proofs/utilities/thm-implies-of-nil-left.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
144> VERIFY IMPLIES-OF-NIL-RIGHT
;; Reading from Proofs/utilities/thm-implies-of-nil-right.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.05 seconds
145> VERIFY BOOLEANP-OF-IMPLIES
;; Reading from Proofs/utilities/thm-booleanp-of-implies.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.25 seconds
146> VERIFY NATP-OF-NFIX
;; Reading from Proofs/utilities/thm-natp-of-nfix.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.16 seconds
147> VERIFY NFIX-WHEN-NATP-CHEAP
;; Reading from Proofs/utilities/thm-nfix-when-natp-cheap.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.08 seconds
148> VERIFY NFIX-WHEN-NOT-NATP-CHEAP
;; Reading from Proofs/utilities/thm-nfix-when-not-natp-cheap.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.12 seconds
149> VERIFY EQUAL-OF-NFIX-OF-SELF
;; Reading from Proofs/utilities/thm-equal-of-nfix-of-self.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.21 seconds
150> VERIFY [OUTSIDE]EQUAL-OF-NFIX-OF-SELF-ALT
;; Reading from Proofs/utilities/thm-_lbr_outside_rbr_equal-of-nfix-of-self-alt.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
151> VERIFY EQUAL-OF-ZERO-AND-NFIX
;; Reading from Proofs/utilities/thm-equal-of-zero-and-nfix.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.13 seconds
152> VERIFY [OUTSIDE]EQUAL-OF-ZERO-AND-NFIX-ALT
;; Reading from Proofs/utilities/thm-_lbr_outside_rbr_equal-of-zero-and-nfix-alt.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
153> VERIFY ZP-WHEN-NATP-CHEAP
;; Reading from Proofs/utilities/thm-zp-when-natp-cheap.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.15 seconds
154> VERIFY ZP-WHEN-NOT-NATP-CHEAP
;; Reading from Proofs/utilities/thm-zp-when-not-natp-cheap.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.13 seconds
155> VERIFY ZP-OF-NFIX
;; Reading from Proofs/utilities/thm-zp-of-nfix.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.18 seconds
156> VERIFY NFIX-OF-NFIX
;; Reading from Proofs/utilities/thm-nfix-of-nfix.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
157> VERIFY NATP-WHEN-NOT-ZP-CHEAP
;; Reading from Proofs/utilities/thm-natp-when-not-zp-cheap.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.20 seconds
158> VERIFY NATP-WHEN-ZP-CHEAP
;; Reading from Proofs/utilities/thm-natp-when-zp-cheap.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.36 seconds
159> VERIFY NFIX-WHEN-ZP-CHEAP
;; Reading from Proofs/utilities/thm-nfix-when-zp-cheap.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
160> VERIFY EQUAL-OF-NFIX-WITH-POSITIVE-CONSTANT
;; Reading from Proofs/utilities/thm-equal-of-nfix-with-positive-constant.proof
;; Reading the file took 0.11 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.54 seconds
161> VERIFY NATP-OF-PLUS
;; Reading from Proofs/utilities/thm-natp-of-plus.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
162> VERIFY PLUS-UNDER-IFF
;; Reading from Proofs/utilities/thm-plus-under-iff.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.17 seconds
163> VERIFY COMMUTATIVITY-OF-+
;; Reading from Proofs/utilities/thm-commutativity-of-+.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
164> VERIFY ASSOCIATIVITY-OF-+
;; Reading from Proofs/utilities/thm-associativity-of-+.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
165> VERIFY COMMUTATIVITY-OF-+-TWO
;; Reading from Proofs/utilities/thm-commutativity-of-+-two.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.10 seconds
166> VERIFY GATHER-CONSTANTS-FROM-PLUS-OF-PLUS
;; Reading from Proofs/utilities/thm-gather-constants-from-plus-of-plus.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
167> VERIFY PLUS-COMPLETION-LEFT
;; Reading from Proofs/utilities/thm-plus-completion-left.proof
;; Reading the file took 0.37 seconds
;; Checking the proof took 1.45 seconds
;; VERIFY took 5.95 seconds
168> VERIFY PLUS-COMPLETION-RIGHT
;; Reading from Proofs/utilities/thm-plus-completion-right.proof
;; Reading the file took 0.10 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.44 seconds
169> VERIFY PLUS-OF-ZERO-RIGHT
;; Reading from Proofs/utilities/thm-plus-of-zero-right.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.35 seconds
170> VERIFY PLUS-OF-ZERO-LEFT
;; Reading from Proofs/utilities/thm-plus-of-zero-left.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.12 seconds
171> VERIFY PLUS-WHEN-ZP-LEFT-CHEAP
;; Reading from Proofs/utilities/thm-plus-when-zp-left-cheap.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.49 seconds
172> VERIFY PLUS-WHEN-ZP-RIGHT-CHEAP
;; Reading from Proofs/utilities/thm-plus-when-zp-right-cheap.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.48 seconds
173> VERIFY PLUS-OF-NFIX-LEFT
;; Reading from Proofs/utilities/thm-plus-of-nfix-left.proof
;; Reading the file took 0.09 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.63 seconds
174> VERIFY PLUS-OF-NFIX-RIGHT
;; Reading from Proofs/utilities/thm-plus-of-nfix-right.proof
;; Reading the file took 0.09 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.60 seconds
175> VERIFY BOOLEANP-OF-<
;; Reading from Proofs/utilities/thm-booleanp-of-_lt_.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.28 seconds
176> VERIFY IRREFLEXIVITY-OF-<
;; Reading from Proofs/utilities/thm-irreflexivity-of-_lt_.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
177> VERIFY LESS-OF-ZERO-RIGHT
;; Reading from Proofs/utilities/thm-less-of-zero-right.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.07 seconds
178> VERIFY LESS-COMPLETION-RIGHT
;; Reading from Proofs/utilities/thm-less-completion-right.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.24 seconds
179> VERIFY LESS-WHEN-ZP-RIGHT-CHEAP
;; Reading from Proofs/utilities/thm-less-when-zp-right-cheap.proof
;; Reading the file took 0.11 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.54 seconds
180> VERIFY LESS-OF-ZERO-LEFT
;; Reading from Proofs/utilities/thm-less-of-zero-left.proof
;; Reading the file took 0.12 seconds
;; Checking the proof took 0.20 seconds
;; VERIFY took 0.85 seconds
181> VERIFY LESS-COMPLETION-LEFT
;; Reading from Proofs/utilities/thm-less-completion-left.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.47 seconds
182> VERIFY LESS-WHEN-ZP-LEFT-CHEAP
;; Reading from Proofs/utilities/thm-less-when-zp-left-cheap.proof
;; Reading the file took 0.13 seconds
;; Checking the proof took 0.23 seconds
;; VERIFY took 0.93 seconds
183> VERIFY LESS-OF-NFIX-LEFT
;; Reading from Proofs/utilities/thm-less-of-nfix-left.proof
;; Reading the file took 0.12 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.69 seconds
184> VERIFY LESS-OF-NFIX-RIGHT
;; Reading from Proofs/utilities/thm-less-of-nfix-right.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.21 seconds
185> VERIFY TRANSITIVITY-OF-<
;; Reading from Proofs/utilities/thm-transitivity-of-_lt_.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.24 seconds
186> VERIFY ANTISYMMETRY-OF-<
;; Reading from Proofs/utilities/thm-antisymmetry-of-_lt_.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.14 seconds
;; VERIFY took 0.57 seconds
187> VERIFY TRICHOTOMY-OF-<
;; Reading from Proofs/utilities/thm-trichotomy-of-_lt_.proof
;; Reading the file took 0.27 seconds
;; Checking the proof took 0.67 seconds
;; VERIFY took 2.97 seconds
188> VERIFY ONE-PLUS-TRICK
;; Reading from Proofs/utilities/thm-one-plus-trick.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.19 seconds
189> VERIFY LESS-OF-ONE-RIGHT
;; Reading from Proofs/utilities/thm-less-of-one-right.proof
;; Reading the file took 0.16 seconds
;; Checking the proof took 0.21 seconds
;; VERIFY took 0.93 seconds
190> VERIFY LESS-OF-ONE-LEFT
;; Reading from Proofs/utilities/thm-less-of-one-left.proof
;; Reading the file took 0.20 seconds
;; Checking the proof took 0.32 seconds
;; VERIFY took 1.41 seconds
191> VERIFY TRANSITIVITY-OF-<-TWO
;; Reading from Proofs/utilities/thm-transitivity-of-_lt_-two.proof
;; Reading the file took 0.59 seconds
;; Checking the proof took 1.65 seconds
;; VERIFY took 7.22 seconds
192> VERIFY TRANSITIVITY-OF-<-THREE
;; Reading from Proofs/utilities/thm-transitivity-of-_lt_-three.proof
;; Reading the file took 0.10 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.37 seconds
193> VERIFY TRANSITIVITY-OF-<-FOUR
;; Reading from Proofs/utilities/thm-transitivity-of-_lt_-four.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.17 seconds
194> VERIFY (< (+ a b) (+ a c))
;; Reading from Proofs/utilities/thm-_lp__lt__sp__lp_+_sp_a_sp_b_rp__sp__lp_+_sp_a_sp_c_rp__rp_.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
195> VERIFY (< a (+ a b))
;; Reading from Proofs/utilities/thm-_lp__lt__sp_a_sp__lp_+_sp_a_sp_b_rp__rp_.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.17 seconds
196> VERIFY (< a (+ b a))
;; Reading from Proofs/utilities/thm-_lp__lt__sp_a_sp__lp_+_sp_b_sp_a_rp__rp_.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
197> VERIFY (< (+ a b) a)
;; Reading from Proofs/utilities/thm-_lp__lt__sp__lp_+_sp_a_sp_b_rp__sp_a_rp_.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.14 seconds
198> VERIFY (< (+ b a) a)
;; Reading from Proofs/utilities/thm-_lp__lt__sp__lp_+_sp_b_sp_a_rp__sp_a_rp_.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
199> VERIFY (< a (+ b c a))
;; Reading from Proofs/utilities/thm-_lp__lt__sp_a_sp__lp_+_sp_b_sp_c_sp_a_rp__rp_.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.07 seconds
200> VERIFY (< a (+ b a c))
;; Reading from Proofs/utilities/thm-_lp__lt__sp_a_sp__lp_+_sp_b_sp_a_sp_c_rp__rp_.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.05 seconds
201> VERIFY (< a (+ b c d a))
;; Reading from Proofs/utilities/thm-_lp__lt__sp_a_sp__lp_+_sp_b_sp_c_sp_d_sp_a_rp__rp_.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.08 seconds
202> VERIFY (< a (+ b c a d))
;; Reading from Proofs/utilities/thm-_lp__lt__sp_a_sp__lp_+_sp_b_sp_c_sp_a_sp_d_rp__rp_.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.06 seconds
203> VERIFY (< a (+ b c d e a))
;; Reading from Proofs/utilities/thm-_lp__lt__sp_a_sp__lp_+_sp_b_sp_c_sp_d_sp_e_sp_a_rp__rp_.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.09 seconds
204> VERIFY (< a (+ b c d a e))
;; Reading from Proofs/utilities/thm-_lp__lt__sp_a_sp__lp_+_sp_b_sp_c_sp_d_sp_a_sp_e_rp__rp_.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.09 seconds
205> VERIFY (< a (+ b c d e f a))
;; Reading from Proofs/utilities/thm-_lp__lt__sp_a_sp__lp_+_sp_b_sp_c_sp_d_sp_e_sp_f_sp_a_rp__rp_.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.11 seconds
206> VERIFY (< a (+ b c d e a f))
;; Reading from Proofs/utilities/thm-_lp__lt__sp_a_sp__lp_+_sp_b_sp_c_sp_d_sp_e_sp_a_sp_f_rp__rp_.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.13 seconds
207> VERIFY (< (+ a b) (+ c a))
;; Reading from Proofs/utilities/thm-_lp__lt__sp__lp_+_sp_a_sp_b_rp__sp__lp_+_sp_c_sp_a_rp__rp_.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
208> VERIFY (< (+ b a) (+ c a))
;; Reading from Proofs/utilities/thm-_lp__lt__sp__lp_+_sp_b_sp_a_rp__sp__lp_+_sp_c_sp_a_rp__rp_.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
209> VERIFY (< (+ b a) (+ a c))
;; Reading from Proofs/utilities/thm-_lp__lt__sp__lp_+_sp_b_sp_a_rp__sp__lp_+_sp_a_sp_c_rp__rp_.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
210> VERIFY (< (+ a b) (+ c a d))
;; Reading from Proofs/utilities/thm-_lp__lt__sp__lp_+_sp_a_sp_b_rp__sp__lp_+_sp_c_sp_a_sp_d_rp__rp_.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.06 seconds
211> VERIFY (< (+ b a c) (+ d a))
;; Reading from Proofs/utilities/thm-_lp__lt__sp__lp_+_sp_b_sp_a_sp_c_rp__sp__lp_+_sp_d_sp_a_rp__rp_.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.05 seconds
212> VERIFY a <= b, c != 0 --> a < b+c
;; Reading from Proofs/utilities/thm-a_sp__lt__eq__sp_b,_sp_c_sp_!_eq__sp_0_sp_--_gt__sp_a_sp__lt__sp_b+c.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.39 seconds
213> VERIFY a <= b, c != 0 --> a < c+b
;; Reading from Proofs/utilities/thm-a_sp__lt__eq__sp_b,_sp_c_sp_!_eq__sp_0_sp_--_gt__sp_a_sp__lt__sp_c+b.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.24 seconds
214> VERIFY a <= b, c != 0 --> a < c+b+d
;; Reading from Proofs/utilities/thm-a_sp__lt__eq__sp_b,_sp_c_sp_!_eq__sp_0_sp_--_gt__sp_a_sp__lt__sp_c+b+d.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.39 seconds
215> VERIFY a <= b, c != 0 --> a < c+d+b
;; Reading from Proofs/utilities/thm-a_sp__lt__eq__sp_b,_sp_c_sp_!_eq__sp_0_sp_--_gt__sp_a_sp__lt__sp_c+d+b.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.33 seconds
216> VERIFY c < a, d <= b --> c+d < a+b
;; Reading from Proofs/utilities/thm-c_sp__lt__sp_a,_sp_d_sp__lt__eq__sp_b_sp_--_gt__sp_c+d_sp__lt__sp_a+b.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.29 seconds
;; VERIFY took 1.08 seconds
217> VERIFY c < a, d <= b --> c+d < b+a
;; Reading from Proofs/utilities/thm-c_sp__lt__sp_a,_sp_d_sp__lt__eq__sp_b_sp_--_gt__sp_c+d_sp__lt__sp_b+a.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.29 seconds
218> VERIFY c <= a, d < b --> c+d < a+b
;; Reading from Proofs/utilities/thm-c_sp__lt__eq__sp_a,_sp_d_sp__lt__sp_b_sp_--_gt__sp_c+d_sp__lt__sp_a+b.proof
;; Reading the file took 0.10 seconds
;; Checking the proof took 0.22 seconds
;; VERIFY took 0.89 seconds
219> VERIFY c <= a, d < b --> c+d < b+a
;; Reading from Proofs/utilities/thm-c_sp__lt__eq__sp_a,_sp_d_sp__lt__sp_b_sp_--_gt__sp_c+d_sp__lt__sp_b+a.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.34 seconds
220> VERIFY c <= a, d <= b --> c+d <= a+b
;; Reading from Proofs/utilities/thm-c_sp__lt__eq__sp_a,_sp_d_sp__lt__eq__sp_b_sp_--_gt__sp_c+d_sp__lt__eq__sp_a+b.proof
;; Reading the file took 0.11 seconds
;; Checking the proof took 0.30 seconds
;; VERIFY took 1.13 seconds
221> VERIFY c <= a, d <= b --> c+d <= b+a
;; Reading from Proofs/utilities/thm-c_sp__lt__eq__sp_a,_sp_d_sp__lt__eq__sp_b_sp_--_gt__sp_c+d_sp__lt__eq__sp_b+a.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.30 seconds
222> VERIFY (= a (+ a b))
;; Reading from Proofs/utilities/thm-_lp__eq__sp_a_sp__lp_+_sp_a_sp_b_rp__rp_.proof
;; Reading the file took 0.19 seconds
;; Checking the proof took 0.31 seconds
;; VERIFY took 1.28 seconds
223> VERIFY (= a (+ b a))
;; Reading from Proofs/utilities/thm-_lp__eq__sp_a_sp__lp_+_sp_b_sp_a_rp__rp_.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.22 seconds
224> VERIFY lemma for (= (+ a b) (+ a c))
;; Reading from Proofs/utilities/thm-lemma_sp_for_sp__lp__eq__sp__lp_+_sp_a_sp_b_rp__sp__lp_+_sp_a_sp_c_rp__rp_.proof
;; Reading the file took 0.31 seconds
;; Checking the proof took 0.92 seconds
;; VERIFY took 3.74 seconds
225> VERIFY (= (+ a b) (+ a c))
;; Reading from Proofs/utilities/thm-_lp__eq__sp__lp_+_sp_a_sp_b_rp__sp__lp_+_sp_a_sp_c_rp__rp_.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 2.57 seconds
;; VERIFY took 10.44 seconds
226> VERIFY (= (+ a b) (+ c a))
;; Reading from Proofs/utilities/thm-_lp__eq__sp__lp_+_sp_a_sp_b_rp__sp__lp_+_sp_c_sp_a_rp__rp_.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
227> VERIFY (= (+ b a) (+ c a))
;; Reading from Proofs/utilities/thm-_lp__eq__sp__lp_+_sp_b_sp_a_rp__sp__lp_+_sp_c_sp_a_rp__rp_.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.04 seconds
228> VERIFY (= (+ b a) (+ a c))
;; Reading from Proofs/utilities/thm-_lp__eq__sp__lp_+_sp_b_sp_a_rp__sp__lp_+_sp_a_sp_c_rp__rp_.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
229> VERIFY (= 0 (+ a b))
;; Reading from Proofs/utilities/thm-_lp__eq__sp_0_sp__lp_+_sp_a_sp_b_rp__rp_.proof
;; Reading the file took 0.19 seconds
;; Checking the proof took 0.31 seconds
;; VERIFY took 1.32 seconds
230> VERIFY lemma for (= (+ a x b) (+ c x d))
;; Reading from Proofs/utilities/thm-lemma_sp_for_sp__lp__eq__sp__lp_+_sp_a_sp_x_sp_b_rp__sp__lp_+_sp_c_sp_x_sp_d_rp__rp_.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.31 seconds
231> VERIFY (= (+ a x b) (+ c x d))
;; Reading from Proofs/utilities/thm-_lp__eq__sp__lp_+_sp_a_sp_x_sp_b_rp__sp__lp_+_sp_c_sp_x_sp_d_rp__rp_.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.13 seconds
232> VERIFY SQUEEZE-LAW-ONE
;; Reading from Proofs/utilities/thm-squeeze-law-one.proof
;; Reading the file took 0.64 seconds
;; Checking the proof took 1.84 seconds
;; VERIFY took 7.75 seconds
233> VERIFY SQUEEZE-LAW-TWO
;; Reading from Proofs/utilities/thm-squeeze-law-two.proof
;; Reading the file took 0.26 seconds
;; Checking the proof took 0.64 seconds
;; VERIFY took 2.48 seconds
234> VERIFY SQUEEZE-LAW-THREE
;; Reading from Proofs/utilities/thm-squeeze-law-three.proof
;; Reading the file took 0.27 seconds
;; Checking the proof took 0.64 seconds
;; VERIFY took 2.63 seconds
235> VERIFY NATP-OF-MINUS
;; Reading from Proofs/utilities/thm-natp-of-minus.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
236> VERIFY MINUS-UNDER-IFF
;; Reading from Proofs/utilities/thm-minus-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.14 seconds
237> VERIFY MINUS-WHEN-NOT-LESS
;; Reading from Proofs/utilities/thm-minus-when-not-less.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.24 seconds
238> VERIFY MINUS-OF-SELF
;; Reading from Proofs/utilities/thm-minus-of-self.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
239> VERIFY MINUS-OF-ZERO-LEFT
;; Reading from Proofs/utilities/thm-minus-of-zero-left.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
240> VERIFY MINUS-CANCELS-SUMMAND-RIGHT
;; Reading from Proofs/utilities/thm-minus-cancels-summand-right.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.18 seconds
;; VERIFY took 0.69 seconds
241> VERIFY MINUS-OF-ZERO-RIGHT
;; Reading from Proofs/utilities/thm-minus-of-zero-right.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.52 seconds
242> VERIFY MINUS-CANCELS-SUMMAND-LEFT
;; Reading from Proofs/utilities/thm-minus-cancels-summand-left.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.08 seconds
243> VERIFY (< (- a b) c)
;; Reading from Proofs/utilities/thm-_lp__lt__sp__lp_-_sp_a_sp_b_rp__sp_c_rp_.proof
;; Reading the file took 0.19 seconds
;; Checking the proof took 0.50 seconds
;; VERIFY took 1.88 seconds
244> VERIFY (< a (- b c))
;; Reading from Proofs/utilities/thm-_lp__lt__sp_a_sp__lp_-_sp_b_sp_c_rp__rp_.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 seconds
245> VERIFY (+ a (- b c))
;; Reading from Proofs/utilities/thm-_lp_+_sp_a_sp__lp_-_sp_b_sp_c_rp__rp_.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.35 seconds
246> VERIFY (+ (- a b) c)
;; Reading from Proofs/utilities/thm-_lp_+_sp__lp_-_sp_a_sp_b_rp__sp_c_rp_.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.33 seconds
247> VERIFY (- a (- b c))
;; Reading from Proofs/utilities/thm-_lp_-_sp_a_sp__lp_-_sp_b_sp_c_rp__rp_.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.36 seconds
248> VERIFY (- (- a b) c)
;; Reading from Proofs/utilities/thm-_lp_-_sp__lp_-_sp_a_sp_b_rp__sp_c_rp_.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
249> VERIFY (= (- a b) c)
;; Reading from Proofs/utilities/thm-_lp__eq__sp__lp_-_sp_a_sp_b_rp__sp_c_rp_.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.49 seconds
250> VERIFY (= c (- a b))
;; Reading from Proofs/utilities/thm-_lp__eq__sp_c_sp__lp_-_sp_a_sp_b_rp__rp_.proof
;; Reading the file took 0.14 seconds
;; Checking the proof took 0.31 seconds
;; VERIFY took 1.13 seconds
251> VERIFY (- (+ a b) (+ a c))
;; Reading from Proofs/utilities/thm-_lp_-_sp__lp_+_sp_a_sp_b_rp__sp__lp_+_sp_a_sp_c_rp__rp_.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.35 seconds
252> VERIFY (- (+ a b) (+ c a))
;; Reading from Proofs/utilities/thm-_lp_-_sp__lp_+_sp_a_sp_b_rp__sp__lp_+_sp_c_sp_a_rp__rp_.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.27 seconds
253> VERIFY (- (+ b a) (+ c a))
;; Reading from Proofs/utilities/thm-_lp_-_sp__lp_+_sp_b_sp_a_rp__sp__lp_+_sp_c_sp_a_rp__rp_.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.25 seconds
254> VERIFY (- (+ b a) (+ a c))
;; Reading from Proofs/utilities/thm-_lp_-_sp__lp_+_sp_b_sp_a_rp__sp__lp_+_sp_a_sp_c_rp__rp_.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.25 seconds
255> VERIFY (- (+ a b) (+ c d a))
;; Reading from Proofs/utilities/thm-_lp_-_sp__lp_+_sp_a_sp_b_rp__sp__lp_+_sp_c_sp_d_sp_a_rp__rp_.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.30 seconds
256> VERIFY a < b --> a <= b-1
;; Reading from Proofs/utilities/thm-a_sp__lt__sp_b_sp_--_gt__sp_a_sp__lt__eq__sp_b-1.proof
;; Reading the file took 0.12 seconds
;; Checking the proof took 0.22 seconds
;; VERIFY took 0.95 seconds
257> VERIFY MINUS-WHEN-ZP-LEFT-CHEAP
;; Reading from Proofs/utilities/thm-minus-when-zp-left-cheap.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.16 seconds
258> VERIFY MINUS-WHEN-ZP-RIGHT-CHEAP
;; Reading from Proofs/utilities/thm-minus-when-zp-right-cheap.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.34 seconds
259> VERIFY MINUS-OF-NFIX-LEFT
;; Reading from Proofs/utilities/thm-minus-of-nfix-left.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.27 seconds
260> VERIFY MINUS-OF-NFIX-RIGHT
;; Reading from Proofs/utilities/thm-minus-of-nfix-right.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.30 seconds
261> VERIFY GATHER-CONSTANTS-FROM-LESS-OF-PLUS
;; Reading from Proofs/utilities/thm-gather-constants-from-less-of-plus.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.18 seconds
262> VERIFY GATHER-CONSTANTS-FROM-LESS-OF-PLUS-TWO
;; Reading from Proofs/utilities/thm-gather-constants-from-less-of-plus-two.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.32 seconds
263> VERIFY GATHER-CONSTANTS-FROM-LESS-OF-PLUS-AND-PLUS
;; Reading from Proofs/utilities/thm-gather-constants-from-less-of-plus-and-plus.proof
;; Reading the file took 0.17 seconds
;; Checking the proof took 0.44 seconds
;; VERIFY took 1.54 seconds
264> VERIFY LEMMA-FOR-GATHER-CONSTANTS-FROM-EQUAL-OF-PLUS-AND-PLUS
;; Reading from Proofs/utilities/thm-lemma-for-gather-constants-from-equal-of-plus-and-plus.proof
;; Reading the file took 0.13 seconds
;; Checking the proof took 0.33 seconds
;; VERIFY took 1.14 seconds
265> VERIFY LEMMA2-FOR-GATHER-CONSTANTS-FROM-EQUAL-OF-PLUS-AND-PLUS
;; Reading from Proofs/utilities/thm-lemma2-for-gather-constants-from-equal-of-plus-and-plus.proof

*** - Program stack overflow. RESET
Bye.

Error: utilities.cele-clisp does not exist.

Possible causes:
  - Has someone deleted the file?
  - Has an interrupt been sent, killing the Lisp but not final-checks.sh?
  - Is there a programming error in final-checks.sh?