Processing utilities
Warning: the kernel parameter max_map_count=65536 is less than the 191488+
pages usable by Scieneer Common Lisp.  It is recommended that max_map_count be
increased to at least 191488.  This can be done with either:
   sysctl -w vm.max_map_count=191488
   echo 191488 > /proc/sys/vm/max_map_count
Scieneer Common Lisp 1.3.9
Copyright (c) 2000-2008, Scieneer Pty Ltd. All Rights Reserved.
Restricted noncommercial license. Licensed to Jared Davis.
Loaded subsystems:
    Compiler 1.0, target AMD64
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.00 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.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 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
Compiling LAMBDA (X Y): 
Compiling Top-Level Form: 
;; DEFINE took 0.07 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.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 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.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 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.00 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.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.00 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.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
17> VERIFY THEOREM-IF-REDUX-ELSE
;; Reading from Proofs/utilities/thm-theorem-if-redux-else.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.05 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.01 seconds
19> VERIFY THEOREM-IF-REDUX-NIL
;; Reading from Proofs/utilities/thm-theorem-if-redux-nil.proof
;; Reading the file took 0.00 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.01 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.01 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
26> VERIFY THEOREM-IFF-BOTH-FALSE
;; Reading from Proofs/utilities/thm-theorem-iff-both-false.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 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.00 seconds
28> VERIFY THEOREM-IFF-FALSE-TRUE
;; Reading from Proofs/utilities/thm-theorem-iff-false-true.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.05 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.00 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.01 seconds
31> VERIFY THEOREM-IFF-NIL-WHEN-NIL
;; Reading from Proofs/utilities/thm-theorem-iff-nil-when-nil.proof
;; Reading the file took 0.00 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.01 seconds
33> VERIFY THEOREM-IFF-NIL-OR-T
;; Reading from Proofs/utilities/thm-theorem-iff-nil-or-t.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 seconds
34> VERIFY THEOREM-REFLEXIVITY-OF-IFF
;; Reading from Proofs/utilities/thm-theorem-reflexivity-of-iff.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
35> VERIFY THEOREM-SYMMETRY-OF-IFF
;; Reading from Proofs/utilities/thm-theorem-symmetry-of-iff.proof
;; Reading the file took 0.00 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.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 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.00 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.01 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.01 seconds
40> VERIFY THEOREM-IFF-CONGRUENT-IFF-1
;; Reading from Proofs/utilities/thm-theorem-iff-congruent-iff-1.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.05 seconds
41> VERIFY THEOREM-TRANSITIVITY-OF-IFF
;; Reading from Proofs/utilities/thm-theorem-transitivity-of-iff.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 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.00 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.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 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.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.01 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.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
49> VERIFY THEOREM-IFF-WHEN-NOT-NIL
;; Reading from Proofs/utilities/thm-theorem-iff-when-not-nil.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.00 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.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
54> VERIFY THEOREM-CONS-IS-NOT-NIL
;; Reading from Proofs/utilities/thm-theorem-cons-is-not-nil.proof
;; Reading the file took 0.00 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.00 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
57> VERIFY RW.EQTRACE-CONTRADICTION-LEMMA1
;; Reading from Proofs/utilities/thm-rw.eqtrace-contradiction-lemma1.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.00 seconds
;; VERIFY took 0.02 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.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.05 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.05 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.00 seconds
;; VERIFY took 0.02 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.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.01 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.01 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.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 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.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 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.01 seconds
72> VERIFY RW.COMPILE-NOT-LEMMA1
;; Reading from Proofs/utilities/thm-rw.compile-not-lemma1.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
73> VERIFY CLAUSE.THEOREM-AUX-SPLIT-POSITIVE
;; Reading from Proofs/utilities/thm-clause.theorem-aux-split-positive.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.02 seconds
75> VERIFY CLAUSE.CASES-LEMMA
;; Reading from Proofs/utilities/thm-clause.cases-lemma.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.00 seconds
;; Checking the proofs took 0.00 seconds
Compiling LAMBDA (X Y): 
Compiling Top-Level Form: 
;; DEFINE took 0.00 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.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 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.00 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.00 seconds
;; VERIFY took 0.02 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.02 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 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.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 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.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 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.00 seconds
;; Checking the proofs took 0.00 seconds
Compiling LAMBDA (A B): 
Compiling Top-Level Form: 
;; 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.00 seconds
;; Checking the proofs took 0.00 seconds
Compiling LAMBDA (A B): 
Compiling Top-Level Form: 
;; DEFINE took 0.00 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.00 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
Compiling LAMBDA (A B C): 
Compiling Top-Level Form: 
;; 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.00 seconds
;; Checking the proofs took 0.00 seconds
Compiling LAMBDA (X): 
Compiling Top-Level Form: 
;; DEFINE took 0.00 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.45 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 1.18 seconds
98> VERIFY BOOLEANP-OF-BOOLEANP
;; Reading from Proofs/utilities/thm-booleanp-of-booleanp.proof
;; Reading the file took 0.11 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.30 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.01 seconds
;; VERIFY took 0.06 seconds
100> VERIFY BOOLEANP-OF-NOT
;; Reading from Proofs/utilities/thm-booleanp-of-not.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.14 seconds
101> VERIFY BOOLEANP-OF-IFF
;; Reading from Proofs/utilities/thm-booleanp-of-iff.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.09 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.01 seconds
;; VERIFY took 0.04 seconds
103> VERIFY EQUAL-OF-NIL-ONE
;; Reading from Proofs/utilities/thm-equal-of-nil-one.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.07 seconds
104> VERIFY EQUAL-OF-NIL-TWO
;; Reading from Proofs/utilities/thm-equal-of-nil-two.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.06 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.00 seconds
;; VERIFY took 0.02 seconds
106> VERIFY IFF-OF-NIL-TWO
;; Reading from Proofs/utilities/thm-iff-of-nil-two.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
107> VERIFY IFF-OF-T-LEFT
;; Reading from Proofs/utilities/thm-iff-of-t-left.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
108> VERIFY IFF-OF-T-RIGHT
;; Reading from Proofs/utilities/thm-iff-of-t-right.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
109> VERIFY BOOLEANP-OF-CONSP
;; Reading from Proofs/utilities/thm-booleanp-of-consp.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.18 seconds
110> VERIFY CAR-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-car-when-not-consp.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.11 seconds
111> VERIFY CDR-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-cdr-when-not-consp.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.12 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.00 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.04 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.00 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.23 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.65 seconds
116> VERIFY BOOLEANP-OF-SYMBOLP
;; Reading from Proofs/utilities/thm-booleanp-of-symbolp.proof
;; Reading the file took 0.17 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.22 seconds
117> VERIFY BOOLEANP-OF-SYMBOL-<
;; Reading from Proofs/utilities/thm-booleanp-of-symbol-_lt_.proof
;; Reading the file took 0.11 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.18 seconds
118> VERIFY IRREFLEXIVITY-OF-SYMBOL-<
;; Reading from Proofs/utilities/thm-irreflexivity-of-symbol-_lt_.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
119> VERIFY ANTISYMMETRY-OF-SYMBOL-<
;; Reading from Proofs/utilities/thm-antisymmetry-of-symbol-_lt_.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.06 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.01 seconds
;; VERIFY took 0.07 seconds
121> VERIFY TRICHOTOMY-OF-SYMBOL-<
;; Reading from Proofs/utilities/thm-trichotomy-of-symbol-_lt_.proof
;; Reading the file took 0.27 seconds
;; Checking the proof took 0.23 seconds
;; VERIFY took 1.06 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.03 seconds
;; VERIFY took 0.21 seconds
123> VERIFY SYMBOL-<-COMPLETION-RIGHT
;; Reading from Proofs/utilities/thm-symbol-_lt_-completion-right.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.17 seconds
124> VERIFY BOOLEANP-OF-NATP
;; Reading from Proofs/utilities/thm-booleanp-of-natp.proof
;; Reading the file took 0.09 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.14 seconds
125> VERIFY SYMBOLP-WHEN-NATP-CHEAP
;; Reading from Proofs/utilities/thm-symbolp-when-natp-cheap.proof
;; Reading the file took 0.11 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.15 seconds
126> VERIFY SYMBOLP-WHEN-CONSP-CHEAP
;; Reading from Proofs/utilities/thm-symbolp-when-consp-cheap.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.07 seconds
127> VERIFY CONSP-WHEN-NATP-CHEAP
;; Reading from Proofs/utilities/thm-consp-when-natp-cheap.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.06 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.01 seconds
;; VERIFY took 0.10 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.01 seconds
;; VERIFY took 0.09 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.01 seconds
;; VERIFY took 0.07 seconds
131> VERIFY CONS-UNDER-IFF
;; Reading from Proofs/utilities/thm-cons-under-iff.proof
;; Reading the file took 0.13 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.14 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.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 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.03 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 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.01 seconds
;; VERIFY took 0.05 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.06 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.08 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.07 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.09 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.07 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.09 seconds
138> VERIFY CAR-WHEN-SYMBOLP-CHEAP
;; Reading from Proofs/utilities/thm-car-when-symbolp-cheap.proof
;; Reading the file took 0.09 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.16 seconds
139> VERIFY NOT-OF-NOT-UNDER-IFF
;; Reading from Proofs/utilities/thm-not-of-not-under-iff.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.07 seconds
140> VERIFY IMPLIES-OF-SELF
;; Reading from Proofs/utilities/thm-implies-of-self.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
141> VERIFY IMPLIES-OF-T-LEFT
;; Reading from Proofs/utilities/thm-implies-of-t-left.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
142> VERIFY IMPLIES-OF-T-RIGHT
;; Reading from Proofs/utilities/thm-implies-of-t-right.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
143> VERIFY IMPLIES-OF-NIL-LEFT
;; Reading from Proofs/utilities/thm-implies-of-nil-left.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
144> VERIFY IMPLIES-OF-NIL-RIGHT
;; Reading from Proofs/utilities/thm-implies-of-nil-right.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
145> VERIFY BOOLEANP-OF-IMPLIES
;; Reading from Proofs/utilities/thm-booleanp-of-implies.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.08 seconds
146> VERIFY NATP-OF-NFIX
;; Reading from Proofs/utilities/thm-natp-of-nfix.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.14 seconds
147> VERIFY NFIX-WHEN-NATP-CHEAP
;; Reading from Proofs/utilities/thm-nfix-when-natp-cheap.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
148> VERIFY NFIX-WHEN-NOT-NATP-CHEAP
;; Reading from Proofs/utilities/thm-nfix-when-not-natp-cheap.proof
;; Reading the file took 0.13 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.16 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.02 seconds
;; VERIFY took 0.07 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.05 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.05 seconds
151> VERIFY EQUAL-OF-ZERO-AND-NFIX
;; Reading from Proofs/utilities/thm-equal-of-zero-and-nfix.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.09 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.00 seconds
;; VERIFY took 0.03 seconds
153> VERIFY ZP-WHEN-NATP-CHEAP
;; Reading from Proofs/utilities/thm-zp-when-natp-cheap.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
154> VERIFY ZP-WHEN-NOT-NATP-CHEAP
;; Reading from Proofs/utilities/thm-zp-when-not-natp-cheap.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.09 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.01 seconds
;; VERIFY took 0.07 seconds
156> VERIFY NFIX-OF-NFIX
;; Reading from Proofs/utilities/thm-nfix-of-nfix.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.05 seconds
157> VERIFY NATP-WHEN-NOT-ZP-CHEAP
;; Reading from Proofs/utilities/thm-natp-when-not-zp-cheap.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.07 seconds
158> VERIFY NATP-WHEN-ZP-CHEAP
;; Reading from Proofs/utilities/thm-natp-when-zp-cheap.proof
;; Reading the file took 0.15 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.26 seconds
159> VERIFY NFIX-WHEN-ZP-CHEAP
;; Reading from Proofs/utilities/thm-nfix-when-zp-cheap.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.06 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.18 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.28 seconds
161> VERIFY NATP-OF-PLUS
;; Reading from Proofs/utilities/thm-natp-of-plus.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
162> VERIFY PLUS-UNDER-IFF
;; Reading from Proofs/utilities/thm-plus-under-iff.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.11 seconds
163> VERIFY COMMUTATIVITY-OF-+
;; Reading from Proofs/utilities/thm-commutativity-of-+.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
164> VERIFY ASSOCIATIVITY-OF-+
;; Reading from Proofs/utilities/thm-associativity-of-+.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
165> VERIFY COMMUTATIVITY-OF-+-TWO
;; Reading from Proofs/utilities/thm-commutativity-of-+-two.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
167> VERIFY PLUS-COMPLETION-LEFT
;; Reading from Proofs/utilities/thm-plus-completion-left.proof
;; Reading the file took 0.52 seconds
;; Checking the proof took 0.38 seconds
;; VERIFY took 1.87 seconds
168> VERIFY PLUS-COMPLETION-RIGHT
;; Reading from Proofs/utilities/thm-plus-completion-right.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.12 seconds
169> VERIFY PLUS-OF-ZERO-RIGHT
;; Reading from Proofs/utilities/thm-plus-of-zero-right.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.12 seconds
170> VERIFY PLUS-OF-ZERO-LEFT
;; Reading from Proofs/utilities/thm-plus-of-zero-left.proof
;; Reading the file took 0.11 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.13 seconds
171> VERIFY PLUS-WHEN-ZP-LEFT-CHEAP
;; Reading from Proofs/utilities/thm-plus-when-zp-left-cheap.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.17 seconds
172> VERIFY PLUS-WHEN-ZP-RIGHT-CHEAP
;; Reading from Proofs/utilities/thm-plus-when-zp-right-cheap.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.18 seconds
173> VERIFY PLUS-OF-NFIX-LEFT
;; Reading from Proofs/utilities/thm-plus-of-nfix-left.proof
;; Reading the file took 0.13 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.25 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.04 seconds
;; VERIFY took 0.22 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.02 seconds
;; VERIFY took 0.10 seconds
176> VERIFY IRREFLEXIVITY-OF-<
;; Reading from Proofs/utilities/thm-irreflexivity-of-_lt_.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
177> VERIFY LESS-OF-ZERO-RIGHT
;; Reading from Proofs/utilities/thm-less-of-zero-right.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.02 seconds
;; VERIFY took 0.08 seconds
179> VERIFY LESS-WHEN-ZP-RIGHT-CHEAP
;; Reading from Proofs/utilities/thm-less-when-zp-right-cheap.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.17 seconds
180> VERIFY LESS-OF-ZERO-LEFT
;; Reading from Proofs/utilities/thm-less-of-zero-left.proof
;; Reading the file took 0.11 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.29 seconds
181> VERIFY LESS-COMPLETION-LEFT
;; Reading from Proofs/utilities/thm-less-completion-left.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.15 seconds
182> VERIFY LESS-WHEN-ZP-LEFT-CHEAP
;; Reading from Proofs/utilities/thm-less-when-zp-left-cheap.proof
;; Reading the file took 0.11 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.31 seconds
183> VERIFY LESS-OF-NFIX-LEFT
;; Reading from Proofs/utilities/thm-less-of-nfix-left.proof
;; Reading the file took 0.09 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.23 seconds
184> VERIFY LESS-OF-NFIX-RIGHT
;; Reading from Proofs/utilities/thm-less-of-nfix-right.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.07 seconds
185> VERIFY TRANSITIVITY-OF-<
;; Reading from Proofs/utilities/thm-transitivity-of-_lt_.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.07 seconds
186> VERIFY ANTISYMMETRY-OF-<
;; Reading from Proofs/utilities/thm-antisymmetry-of-_lt_.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.17 seconds
187> VERIFY TRICHOTOMY-OF-<
;; Reading from Proofs/utilities/thm-trichotomy-of-_lt_.proof
;; Reading the file took 0.32 seconds
;; Checking the proof took 0.19 seconds
;; VERIFY took 0.98 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.01 seconds
;; VERIFY took 0.06 seconds
189> VERIFY LESS-OF-ONE-RIGHT
;; Reading from Proofs/utilities/thm-less-of-one-right.proof
;; Reading the file took 0.14 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.33 seconds
190> VERIFY LESS-OF-ONE-LEFT
;; Reading from Proofs/utilities/thm-less-of-one-left.proof
;; Reading the file took 0.19 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.49 seconds
191> VERIFY TRANSITIVITY-OF-<-TWO
;; Reading from Proofs/utilities/thm-transitivity-of-_lt_-two.proof
;; Reading the file took 0.75 seconds
;; Checking the proof took 0.44 seconds
;; VERIFY took 2.38 seconds
192> VERIFY TRANSITIVITY-OF-<-THREE
;; Reading from Proofs/utilities/thm-transitivity-of-_lt_-three.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.11 seconds
193> VERIFY TRANSITIVITY-OF-<-FOUR
;; Reading from Proofs/utilities/thm-transitivity-of-_lt_-four.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.08 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.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.01 seconds
;; VERIFY took 0.05 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.00 seconds
;; VERIFY took 0.02 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.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 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.01 seconds
;; VERIFY took 0.02 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.01 seconds
;; VERIFY took 0.03 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.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 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.01 seconds
;; VERIFY took 0.04 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.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.00 seconds
;; VERIFY took 0.01 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.00 seconds
;; VERIFY took 0.02 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.06 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.15 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.04 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.09 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.04 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.12 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.05 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.12 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.08 seconds
;; VERIFY took 0.33 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.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.09 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.07 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.26 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.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.09 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.08 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.34 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.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.10 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.18 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.45 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.01 seconds
;; VERIFY took 0.07 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.29 seconds
;; Checking the proof took 0.24 seconds
;; VERIFY took 1.13 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 1.00 seconds
;; Checking the proof took 0.66 seconds
;; VERIFY took 3.32 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.17 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.44 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.03 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.09 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.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
232> VERIFY SQUEEZE-LAW-ONE
;; Reading from Proofs/utilities/thm-squeeze-law-one.proof
;; Reading the file took 0.77 seconds
;; Checking the proof took 0.49 seconds
;; VERIFY took 2.49 seconds
233> VERIFY SQUEEZE-LAW-TWO
;; Reading from Proofs/utilities/thm-squeeze-law-two.proof
;; Reading the file took 0.29 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.83 seconds
234> VERIFY SQUEEZE-LAW-THREE
;; Reading from Proofs/utilities/thm-squeeze-law-three.proof
;; Reading the file took 0.28 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.86 seconds
235> VERIFY NATP-OF-MINUS
;; Reading from Proofs/utilities/thm-natp-of-minus.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
236> VERIFY MINUS-UNDER-IFF
;; Reading from Proofs/utilities/thm-minus-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
237> VERIFY MINUS-WHEN-NOT-LESS
;; Reading from Proofs/utilities/thm-minus-when-not-less.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.08 seconds
238> VERIFY MINUS-OF-SELF
;; Reading from Proofs/utilities/thm-minus-of-self.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
239> VERIFY MINUS-OF-ZERO-LEFT
;; Reading from Proofs/utilities/thm-minus-of-zero-left.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.05 seconds
;; VERIFY took 0.23 seconds
241> VERIFY MINUS-OF-ZERO-RIGHT
;; Reading from Proofs/utilities/thm-minus-of-zero-right.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.17 seconds
242> VERIFY MINUS-CANCELS-SUMMAND-LEFT
;; Reading from Proofs/utilities/thm-minus-cancels-summand-left.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.20 seconds
;; Checking the proof took 0.14 seconds
;; VERIFY took 0.62 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.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 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.03 seconds
;; VERIFY took 0.12 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.03 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.10 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.04 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.11 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.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 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.04 seconds
;; VERIFY took 0.16 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.15 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.39 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.04 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.11 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.02 seconds
;; VERIFY took 0.09 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.02 seconds
;; VERIFY took 0.09 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.02 seconds
;; VERIFY took 0.09 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.03 seconds
;; VERIFY took 0.10 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.14 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.35 seconds
257> VERIFY MINUS-WHEN-ZP-LEFT-CHEAP
;; Reading from Proofs/utilities/thm-minus-when-zp-left-cheap.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 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.02 seconds
;; VERIFY took 0.11 seconds
259> VERIFY MINUS-OF-NFIX-LEFT
;; Reading from Proofs/utilities/thm-minus-of-nfix-left.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.09 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.02 seconds
;; VERIFY took 0.10 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.03 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.06 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.04 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.11 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.15 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.49 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.09 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.34 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
;; Reading the file took 4.09 seconds
;; Checking the proof took 2.60 seconds
;; VERIFY took 13.96 seconds
266> VERIFY GATHER-CONSTANTS-FROM-EQUAL-OF-PLUS-AND-PLUS
;; Reading from Proofs/utilities/thm-gather-constants-from-equal-of-plus-and-plus.proof
;; Reading the file took 0.21 seconds
;; Checking the proof took 0.34 seconds
;; VERIFY took 1.41 seconds
267> VERIFY GATHER-CONSTANTS-FROM-EQUAL-OF-PLUS
;; Reading from Proofs/utilities/thm-gather-constants-from-equal-of-plus.proof
;; Reading the file took 0.78 seconds
;; Checking the proof took 0.50 seconds
;; VERIFY took 2.40 seconds
268> VERIFY GATHER-CONSTANTS-FROM-MINUS-OF-PLUS
;; Reading from Proofs/utilities/thm-gather-constants-from-minus-of-plus.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.72 seconds
269> VERIFY GATHER-CONSTANTS-FROM-MINUS-OF-PLUS-TWO
;; Reading from Proofs/utilities/thm-gather-constants-from-minus-of-plus-two.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.33 seconds
270> VERIFY GATHER-CONSTANTS-FROM-MINUS-OF-PLUS-AND-PLUS
;; Reading from Proofs/utilities/thm-gather-constants-from-minus-of-plus-and-plus.proof
;; Reading the file took 0.97 seconds
;; Checking the proof took 0.82 seconds
;; VERIFY took 3.74 seconds
271> VERIFY NOT-EQUAL-WHEN-LESS
;; Reading from Proofs/utilities/thm-not-equal-when-less.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
272> VERIFY NOT-EQUAL-WHEN-LESS-TWO
;; Reading from Proofs/utilities/thm-not-equal-when-less-two.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
273> VERIFY a <= d, b+c <= e --> b+a+c <= d+e
;; Reading from Proofs/utilities/thm-a_sp__lt__eq__sp_d,_sp_b+c_sp__lt__eq__sp_e_sp_--_gt__sp_b+a+c_sp__lt__eq__sp_d+e.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.10 seconds
274> VERIFY (< (+ a b) (+ c b d))
;; Reading from Proofs/utilities/thm-_lp__lt__sp__lp_+_sp_a_sp_b_rp__sp__lp_+_sp_c_sp_b_sp_d_rp__rp_.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
275> VERIFY (< (+ a b c)) (+ d c))
;; Reading from Proofs/utilities/thm-_lp__lt__sp__lp_+_sp_a_sp_b_sp_c_rp__rp__sp__lp_+_sp_d_sp_c_rp__rp_.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.06 seconds
276> VERIFY a <= b, b <= c --> a < 1+c
;; Reading from Proofs/utilities/thm-a_sp__lt__eq__sp_b,_sp_b_sp__lt__eq__sp_c_sp_--_gt__sp_a_sp__lt__sp_1+c.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.10 seconds
277> VERIFY b <= c, a <= b --> a < 1+c
;; Reading from Proofs/utilities/thm-b_sp__lt__eq__sp_c,_sp_a_sp__lt__eq__sp_b_sp_--_gt__sp_a_sp__lt__sp_1+c.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.09 seconds
278> VERIFY NATP-OF-MAX
;; Reading from Proofs/utilities/thm-natp-of-max.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
279> VERIFY EQUAL-OF-MAX-AND-ZERO
;; Reading from Proofs/utilities/thm-equal-of-max-and-zero.proof
;; Reading the file took 0.11 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.31 seconds
280> VERIFY MAX-OF-ZERO-LEFT
;; Reading from Proofs/utilities/thm-max-of-zero-left.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
281> VERIFY MAX-OF-ZERO-RIGHT
;; Reading from Proofs/utilities/thm-max-of-zero-right.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
282> VERIFY NATP-OF-MIN
;; Reading from Proofs/utilities/thm-natp-of-min.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
283> VERIFY EQUAL-OF-MIN-AND-ZERO
;; Reading from Proofs/utilities/thm-equal-of-min-and-zero.proof
;; Reading the file took 0.13 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.36 seconds
284> VERIFY MIN-OF-ZERO-LEFT
;; Reading from Proofs/utilities/thm-min-of-zero-left.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
285> VERIFY MIN-OF-ZERO-RIGHT
;; Reading from Proofs/utilities/thm-min-of-zero-right.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
286> VERIFY ORDP
;; Reading from Proofs/utilities/thm-ordp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
287> VERIFY ORD<
;; Reading from Proofs/utilities/thm-ord_lt_.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
288> VERIFY RANK
;; Reading from Proofs/utilities/thm-rank.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
289> VERIFY ORD<-WHEN-NATURALS
;; Reading from Proofs/utilities/thm-ord_lt_-when-naturals.proof
;; Reading the file took 0.27 seconds
;; Checking the proof took 0.28 seconds
;; VERIFY took 1.24 seconds
290> VERIFY ORDP-WHEN-NATP
;; Reading from Proofs/utilities/thm-ordp-when-natp.proof
;; Reading the file took 0.32 seconds
;; Checking the proof took 0.32 seconds
;; VERIFY took 1.50 seconds
291> VERIFY NATP-OF-RANK
;; Reading from Proofs/utilities/thm-natp-of-rank.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
292> VERIFY RANK-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-rank-when-not-consp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
293> VERIFY RANK-OF-CONS
;; Reading from Proofs/utilities/thm-rank-of-cons.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
294> VERIFY (< 0 (rank x))
;; Reading from Proofs/utilities/thm-_lp__lt__sp_0_sp__lp_rank_sp_x_rp__rp_.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.17 seconds
295> VERIFY ORDP-OF-RANK
;; Reading from Proofs/utilities/thm-ordp-of-rank.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
296> VERIFY RANK-OF-CAR
;; Reading from Proofs/utilities/thm-rank-of-car.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.17 seconds
297> VERIFY RANK-OF-CAR-WEAK
;; Reading from Proofs/utilities/thm-rank-of-car-weak.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.12 seconds
298> VERIFY RANK-OF-CDR
;; Reading from Proofs/utilities/thm-rank-of-cdr.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.17 seconds
299> VERIFY RANK-OF-CDR-WEAK
;; Reading from Proofs/utilities/thm-rank-of-cdr-weak.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.12 seconds
300> VERIFY RANK-OF-SECOND
;; Reading from Proofs/utilities/thm-rank-of-second.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.14 seconds
301> VERIFY RANK-OF-SECOND-WEAK
;; Reading from Proofs/utilities/thm-rank-of-second-weak.proof
;; Reading the file took 0.09 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.35 seconds
302> VERIFY RANK-OF-THIRD
;; Reading from Proofs/utilities/thm-rank-of-third.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.15 seconds
303> VERIFY RANK-OF-THIRD-WEAK
;; Reading from Proofs/utilities/thm-rank-of-third-weak.proof
;; Reading the file took 0.10 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.38 seconds
304> VERIFY RANK-OF-FOURTH
;; Reading from Proofs/utilities/thm-rank-of-fourth.proof
;; Reading the file took 0.15 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.26 seconds
305> VERIFY RANK-OF-FOURTH-WEAK
;; Reading from Proofs/utilities/thm-rank-of-fourth-weak.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.28 seconds
306> VERIFY BOOLEANP-OF-ORD<
;; Reading from Proofs/utilities/thm-booleanp-of-ord_lt_.proof
;; Reading the file took 0.27 seconds
;; Checking the proof took 0.34 seconds
;; VERIFY took 1.37 seconds
307> VERIFY BOOLEANP-OF-ORDP
;; Reading from Proofs/utilities/thm-booleanp-of-ordp.proof
;; Reading the file took 0.49 seconds
;; Checking the proof took 0.59 seconds
;; VERIFY took 2.66 seconds
308> DEFINE TWO-NATS-MEASURE
;; Reading from Proofs/utilities/admit-two-nats-measure.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
Compiling LAMBDA (A B): 
Compiling Top-Level Form: 
;; DEFINE took 0.04 seconds
309> VERIFY TWO-NATS-MEASURE
;; Reading from Proofs/utilities/thm-two-nats-measure.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
310> VERIFY ORDP-OF-TWO-NATS-MEASURE
;; Reading from Proofs/utilities/thm-ordp-of-two-nats-measure.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.31 seconds
311> VERIFY ORD<-OF-TWO-NATS-MEASURE
;; Reading from Proofs/utilities/thm-ord_lt_-of-two-nats-measure.proof
;; Reading the file took 0.18 seconds
;; Checking the proof took 0.22 seconds
;; VERIFY took 0.74 seconds
312> DEFINE THREE-NATS-MEASURE
;; Reading from Proofs/utilities/admit-three-nats-measure.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
Compiling LAMBDA (A B C): 
Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
313> VERIFY THREE-NATS-MEASURE
;; Reading from Proofs/utilities/thm-three-nats-measure.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
314> VERIFY ORDP-OF-THREE-NATS-MEASURE
;; Reading from Proofs/utilities/thm-ordp-of-three-nats-measure.proof
;; Reading the file took 0.20 seconds
;; Checking the proof took 0.20 seconds
;; VERIFY took 0.78 seconds
315> VERIFY ORD<-OF-THREE-NATS-MEASURE
;; Reading from Proofs/utilities/thm-ord_lt_-of-three-nats-measure.proof
;; Reading the file took 0.43 seconds
;; Checking the proof took 0.75 seconds
;; VERIFY took 2.41 seconds
316> DEFINE LEN
;; Reading from Proofs/utilities/admit-len.proofs
;; Reading the file took 0.04 seconds
;; Checking the proofs took 0.02 seconds
;; DEFINE took 0.08 seconds
317> VERIFY LEN
;; Reading from Proofs/utilities/thm-len.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
318> VERIFY LEN-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-len-when-not-consp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
319> VERIFY LEN-OF-CONS
;; Reading from Proofs/utilities/thm-len-of-cons.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
320> VERIFY NATP-OF-LEN
;; Reading from Proofs/utilities/thm-natp-of-len.proof
;; Reading the file took 0.15 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.45 seconds
321> VERIFY NATP-OF-LEN-FREE
;; Reading from Proofs/utilities/thm-natp-of-len-free.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
322> VERIFY LEN-UNDER-IFF
;; Reading from Proofs/utilities/thm-len-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
323> VERIFY (< 0 (len x))
;; Reading from Proofs/utilities/thm-_lp__lt__sp_0_sp__lp_len_sp_x_rp__rp_.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.11 seconds
324> VERIFY (< 1 (len x))
;; Reading from Proofs/utilities/thm-_lp__lt__sp_1_sp__lp_len_sp_x_rp__rp_.proof
;; Reading the file took 0.20 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.56 seconds
325> VERIFY DECREMENT-LEN-WHEN-CONSP
;; Reading from Proofs/utilities/thm-decrement-len-when-consp.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.15 seconds
326> VERIFY EQUAL-OF-LEN-AND-ZERO
;; Reading from Proofs/utilities/thm-equal-of-len-and-zero.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.10 seconds
327> VERIFY [OUTSIDE]EQUAL-OF-LEN-AND-ZERO-ALT
;; Reading from Proofs/utilities/thm-_lbr_outside_rbr_equal-of-len-and-zero-alt.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 seconds
328> VERIFY CONSP-OF-CDR-WHEN-LEN-TWO-CHEAP
;; Reading from Proofs/utilities/thm-consp-of-cdr-when-len-two-cheap.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.17 seconds
329> VERIFY CONSP-OF-CDR-WITH-LEN-FREE
;; Reading from Proofs/utilities/thm-consp-of-cdr-with-len-free.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
330> VERIFY CONSP-OF-CDR-OF-CDR-WITH-LEN-FREE
;; Reading from Proofs/utilities/thm-consp-of-cdr-of-cdr-with-len-free.proof
;; Reading the file took 0.09 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.25 seconds
331> VERIFY CONSP-OF-CDR-OF-CDR-OF-CDR-WITH-LEN-FREE
;; Reading from Proofs/utilities/thm-consp-of-cdr-of-cdr-of-cdr-with-len-free.proof
;; Reading the file took 0.17 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.46 seconds
332> VERIFY CDR-UNDER-IFF-WITH-LEN-FREE-IN-BOUND
;; Reading from Proofs/utilities/thm-cdr-under-iff-with-len-free-in-bound.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.07 seconds
333> VERIFY CDR-OF-CDR-UNDER-IFF-WITH-LEN-FREE-IN-BOUND
;; Reading from Proofs/utilities/thm-cdr-of-cdr-under-iff-with-len-free-in-bound.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.16 seconds
334> VERIFY CDR-OF-CDR-OF-CDR-UNDER-IFF-WITH-LEN-FREE-IN-BOUND
;; Reading from Proofs/utilities/thm-cdr-of-cdr-of-cdr-under-iff-with-len-free-in-bound.proof
;; Reading the file took 0.09 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.22 seconds
335> VERIFY CDR-OF-CDR-WITH-LEN-FREE-PAST-THE-END
;; Reading from Proofs/utilities/thm-cdr-of-cdr-with-len-free-past-the-end.proof
;; Reading the file took 0.09 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.22 seconds
336> VERIFY CDR-OF-CDR-OF-CDR-WITH-LEN-FREE-PAST-THE-END
;; Reading from Proofs/utilities/thm-cdr-of-cdr-of-cdr-with-len-free-past-the-end.proof
;; Reading the file took 0.13 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.33 seconds
337> VERIFY LEN-2-WHEN-NOT-CDR-OF-CDR
;; Reading from Proofs/utilities/thm-len-2-when-not-cdr-of-cdr.proof
;; Reading the file took 0.17 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.44 seconds
338> VERIFY EQUAL-WHEN-LENGTH-DIFFERENT
;; Reading from Proofs/utilities/thm-equal-when-length-different.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
339> VERIFY EQUAL-OF-2-AND-LEN
;; Reading from Proofs/utilities/thm-equal-of-2-and-len.proof
;; Reading the file took 0.15 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.45 seconds
340> VERIFY EQUAL-OF-3-AND-LEN
;; Reading from Proofs/utilities/thm-equal-of-3-and-len.proof
;; Reading the file took 0.25 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.79 seconds
341> VERIFY CONSP-WHEN-CONSP-OF-CDR-CHEAP
;; Reading from Proofs/utilities/thm-consp-when-consp-of-cdr-cheap.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.07 seconds
342> DEFINE FAST-LEN
;; Reading from Proofs/utilities/admit-fast-len.proofs
;; Reading the file took 0.03 seconds
;; Checking the proofs took 0.02 seconds
Compiling LAMBDA (X ACC): 
Compiling Top-Level Form: 
;; DEFINE took 0.09 seconds
343> VERIFY FAST-LEN
;; Reading from Proofs/utilities/thm-fast-len.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
344> VERIFY FAST-LEN-REMOVAL
;; Reading from Proofs/utilities/thm-fast-len-removal.proof
;; Reading the file took 0.24 seconds
;; Checking the proof took 0.22 seconds
;; VERIFY took 0.90 seconds
345> DEFINE SAME-LENGTHP
;; Reading from Proofs/utilities/admit-same-lengthp.proofs
;; Reading the file took 0.04 seconds
;; Checking the proofs took 0.03 seconds
Compiling LAMBDA (X Y): 
Compiling Top-Level Form: 
;; DEFINE took 0.12 seconds
346> VERIFY SAME-LENGTHP
;; Reading from Proofs/utilities/thm-same-lengthp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
347> VERIFY SAME-LENGTHP-REMOVAL
;; Reading from Proofs/utilities/thm-same-lengthp-removal.proof
;; Reading the file took 0.32 seconds
;; Checking the proof took 0.29 seconds
;; VERIFY took 1.20 seconds
348> DEFINE TRUE-LISTP
;; Reading from Proofs/utilities/admit-true-listp.proofs
;; Reading the file took 0.03 seconds
;; Checking the proofs took 0.02 seconds
;; DEFINE took 0.08 seconds
349> VERIFY TRUE-LISTP
;; Reading from Proofs/utilities/thm-true-listp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
350> VERIFY TRUE-LISTP-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-true-listp-when-not-consp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.06 seconds
351> VERIFY TRUE-LISTP-OF-CONS
;; Reading from Proofs/utilities/thm-true-listp-of-cons.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
352> VERIFY BOOLEANP-OF-TRUE-LISTP
;; Reading from Proofs/utilities/thm-booleanp-of-true-listp.proof
;; Reading the file took 0.14 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.44 seconds
353> VERIFY TRUE-LISTP-OF-CDR
;; Reading from Proofs/utilities/thm-true-listp-of-cdr.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.10 seconds
354> VERIFY CONSP-WHEN-TRUE-LISTP-CHEAP
;; Reading from Proofs/utilities/thm-consp-when-true-listp-cheap.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.15 seconds
355> VERIFY LIST-OF-FIRST-AND-SECOND-WHEN-LEN-2
;; Reading from Proofs/utilities/thm-list-of-first-and-second-when-len-2.proof
;; Reading the file took 0.21 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.62 seconds
356> VERIFY LIST-OF-FIRST-AND-SECOND-AND-THIRD-WHEN-LEN-3
;; Reading from Proofs/utilities/thm-list-of-first-and-second-and-third-when-len-3.proof
;; Reading the file took 0.32 seconds
;; Checking the proof took 0.23 seconds
;; VERIFY took 1.02 seconds
357> VERIFY CDR-WHEN-TRUE-LISTP-WITH-LEN-FREE-PAST-THE-END
;; Reading from Proofs/utilities/thm-cdr-when-true-listp-with-len-free-past-the-end.proof
;; Reading the file took 0.13 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.35 seconds
358> VERIFY CDR-OF-CDR-WHEN-TRUE-LISTP-WITH-LEN-FREE-PAST-THE-END
;; Reading from Proofs/utilities/thm-cdr-of-cdr-when-true-listp-with-len-free-past-the-end.proof
;; Reading the file took 0.20 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.54 seconds
359> VERIFY CDR-OF-CDR-OF-CDR-WHEN-TRUE-LISTP-WITH-LEN-FREE-PAST-THE-END
;; Reading from Proofs/utilities/thm-cdr-of-cdr-of-cdr-when-true-listp-with-len-free-past-the-end.proof
;; Reading the file took 0.31 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.79 seconds
360> VERIFY CDR-UNDER-IFF-WHEN-TRUE-LISTP-WITH-LEN-FREE
;; Reading from Proofs/utilities/thm-cdr-under-iff-when-true-listp-with-len-free.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.14 seconds
361> VERIFY CDR-OF-CDR-UNDER-IFF-WHEN-TRUE-LISTP-WITH-LEN-FREE
;; Reading from Proofs/utilities/thm-cdr-of-cdr-under-iff-when-true-listp-with-len-free.proof
;; Reading the file took 0.17 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.46 seconds
362> VERIFY CDR-OF-CDR-OF-CDR-UNDER-IFF-WHEN-TRUE-LISTP-WITH-LEN-FREE
;; Reading from Proofs/utilities/thm-cdr-of-cdr-of-cdr-under-iff-when-true-listp-with-len-free.proof
;; Reading the file took 0.29 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.79 seconds
363> VERIFY LESS-OF-LEN-OF-CDR-AND-LEN
;; Reading from Proofs/utilities/thm-less-of-len-of-cdr-and-len.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.11 seconds
364> DEFINE LIST-FIX
;; Reading from Proofs/utilities/admit-list-fix.proofs
;; Reading the file took 0.03 seconds
;; Checking the proofs took 0.02 seconds
;; DEFINE took 0.08 seconds
365> VERIFY LIST-FIX
;; Reading from Proofs/utilities/thm-list-fix.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
366> VERIFY LIST-FIX-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-list-fix-when-not-consp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
367> VERIFY LIST-FIX-OF-CONS
;; Reading from Proofs/utilities/thm-list-fix-of-cons.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
368> VERIFY CAR-OF-LIST-FIX
;; Reading from Proofs/utilities/thm-car-of-list-fix.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.06 seconds
369> VERIFY CDR-OF-LIST-FIX
;; Reading from Proofs/utilities/thm-cdr-of-list-fix.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.07 seconds
370> VERIFY CONSP-OF-LIST-FIX
;; Reading from Proofs/utilities/thm-consp-of-list-fix.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.08 seconds
371> VERIFY LIST-FIX-UNDER-IFF
;; Reading from Proofs/utilities/thm-list-fix-under-iff.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.07 seconds
372> VERIFY LEN-OF-LIST-FIX
;; Reading from Proofs/utilities/thm-len-of-list-fix.proof
;; Reading the file took 0.15 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.47 seconds
373> VERIFY TRUE-LISTP-OF-LIST-FIX
;; Reading from Proofs/utilities/thm-true-listp-of-list-fix.proof
;; Reading the file took 0.15 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.45 seconds
374> VERIFY LIST-FIX-WHEN-TRUE-LISTP
;; Reading from Proofs/utilities/thm-list-fix-when-true-listp.proof
;; Reading the file took 0.29 seconds
;; Checking the proof took 0.20 seconds
;; VERIFY took 0.87 seconds
375> VERIFY CDR-OF-LIST-FIX-UNDER-IFF
;; Reading from Proofs/utilities/thm-cdr-of-list-fix-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
376> VERIFY EQUAL-OF-LIST-FIX-AND-SELF
;; Reading from Proofs/utilities/thm-equal-of-list-fix-and-self.proof
;; Reading the file took 0.30 seconds
;; Checking the proof took 0.23 seconds
;; VERIFY took 0.98 seconds
377> DEFINE MEMBERP
;; Reading from Proofs/utilities/admit-memberp.proofs
;; Reading the file took 0.04 seconds
;; Checking the proofs took 0.04 seconds
;; DEFINE took 0.13 seconds
378> VERIFY MEMBERP
;; Reading from Proofs/utilities/thm-memberp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
379> VERIFY MEMBERP-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-memberp-when-not-consp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
380> VERIFY MEMBERP-OF-CONS
;; Reading from Proofs/utilities/thm-memberp-of-cons.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.10 seconds
381> VERIFY BOOLEANP-OF-MEMBERP
;; Reading from Proofs/utilities/thm-booleanp-of-memberp.proof
;; Reading the file took 0.18 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.52 seconds
382> VERIFY MEMBERP-OF-LIST-FIX
;; Reading from Proofs/utilities/thm-memberp-of-list-fix.proof
;; Reading the file took 0.42 seconds
;; Checking the proof took 0.34 seconds
;; VERIFY took 1.54 seconds
383> VERIFY MEMBERP-WHEN-MEMBERP-OF-CDR
;; Reading from Proofs/utilities/thm-memberp-when-memberp-of-cdr.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.12 seconds
384> VERIFY MEMBERP-OF-CAR
;; Reading from Proofs/utilities/thm-memberp-of-car.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.10 seconds
385> VERIFY MEMBERP-OF-SECOND
;; Reading from Proofs/utilities/thm-memberp-of-second.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.08 seconds
386> VERIFY CAR-WHEN-MEMBERP-OF-SINGLETON-LIST-CHEAP
;; Reading from Proofs/utilities/thm-car-when-memberp-of-singleton-list-cheap.proof
;; Reading the file took 0.09 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.23 seconds
387> VERIFY CAR-WHEN-MEMBERP-AND-NOT-MEMBERP-OF-CDR-CHEAP
;; Reading from Proofs/utilities/thm-car-when-memberp-and-not-memberp-of-cdr-cheap.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.21 seconds
388> VERIFY CONSP-WHEN-MEMBERP-CHEAP
;; Reading from Proofs/utilities/thm-consp-when-memberp-cheap.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.07 seconds
389> VERIFY CONSP-OF-CDR-WHEN-MEMBERP-NOT-CAR-CHEAP
;; Reading from Proofs/utilities/thm-consp-of-cdr-when-memberp-not-car-cheap.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.13 seconds
390> VERIFY RANK-WHEN-MEMBERP
;; Reading from Proofs/utilities/thm-rank-when-memberp.proof
;; Reading the file took 0.28 seconds
;; Checking the proof took 0.25 seconds
;; VERIFY took 0.98 seconds
391> VERIFY RANK-WHEN-MEMBERP-WEAK
;; Reading from Proofs/utilities/thm-rank-when-memberp-weak.proof
;; Reading the file took 0.18 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.59 seconds
392> DEFINE SUBSETP
;; Reading from Proofs/utilities/admit-subsetp.proofs
;; Reading the file took 0.04 seconds
;; Checking the proofs took 0.03 seconds
;; DEFINE took 0.12 seconds
393> VERIFY SUBSETP
;; Reading from Proofs/utilities/thm-subsetp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
394> VERIFY SUBSETP-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-subsetp-when-not-consp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
395> VERIFY SUBSETP-OF-CONS
;; Reading from Proofs/utilities/thm-subsetp-of-cons.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.08 seconds
396> VERIFY BOOLEANP-OF-SUBSETP
;; Reading from Proofs/utilities/thm-booleanp-of-subsetp.proof
;; Reading the file took 0.18 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.50 seconds
397> VERIFY SUBSETP-WHEN-NOT-CONSP-TWO
;; Reading from Proofs/utilities/thm-subsetp-when-not-consp-two.proof
;; Reading the file took 0.30 seconds
;; Checking the proof took 0.26 seconds
;; VERIFY took 1.06 seconds
398> VERIFY SUBSETP-OF-CONS-TWO
;; Reading from Proofs/utilities/thm-subsetp-of-cons-two.proof
;; Reading the file took 0.29 seconds
;; Checking the proof took 0.25 seconds
;; VERIFY took 1.04 seconds
399> VERIFY SUBSETP-OF-LIST-FIX-ONE
;; Reading from Proofs/utilities/thm-subsetp-of-list-fix-one.proof
;; Reading the file took 0.44 seconds
;; Checking the proof took 0.33 seconds
;; VERIFY took 1.54 seconds
400> VERIFY SUBSETP-OF-LIST-FIX-TWO
;; Reading from Proofs/utilities/thm-subsetp-of-list-fix-two.proof
;; Reading the file took 0.42 seconds
;; Checking the proof took 0.33 seconds
;; VERIFY took 1.51 seconds
401> VERIFY SUBSETP-OF-CDR
;; Reading from Proofs/utilities/thm-subsetp-of-cdr.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.13 seconds
402> VERIFY IN-SUPERSET-WHEN-IN-SUBSET-ONE
;; Reading from Proofs/utilities/thm-in-superset-when-in-subset-one.proof
;; Reading the file took 0.33 seconds
;; Checking the proof took 0.26 seconds
;; VERIFY took 1.14 seconds
403> VERIFY IN-SUPERSET-WHEN-IN-SUBSET-TWO
;; Reading from Proofs/utilities/thm-in-superset-when-in-subset-two.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
404> VERIFY NOT-IN-SUBSET-WHEN-NOT-IN-SUPERSET-ONE
;; Reading from Proofs/utilities/thm-not-in-subset-when-not-in-superset-one.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
405> VERIFY NOT-IN-SUBSET-WHEN-NOT-IN-SUPERSET-TWO
;; Reading from Proofs/utilities/thm-not-in-subset-when-not-in-superset-two.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
406> VERIFY CONSP-WHEN-NONEMPTY-SUBSET-CHEAP
;; Reading from Proofs/utilities/thm-consp-when-nonempty-subset-cheap.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.10 seconds
407> VERIFY SUBSETP-REFLEXIVE
;; Reading from Proofs/utilities/thm-subsetp-reflexive.proof
;; Reading the file took 0.15 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.47 seconds
408> VERIFY SUBSETP-TRANSITIVE-ONE
;; Reading from Proofs/utilities/thm-subsetp-transitive-one.proof
;; Reading the file took 0.31 seconds
;; Checking the proof took 0.27 seconds
;; VERIFY took 1.15 seconds
409> VERIFY SUBSETP-TRANSITIVE-TWO
;; Reading from Proofs/utilities/thm-subsetp-transitive-two.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
410> DEFINE SUBSETP-BADGUY
;; Reading from Proofs/utilities/admit-subsetp-badguy.proofs
;; Reading the file took 0.04 seconds
;; Checking the proofs took 0.03 seconds
Compiling LAMBDA (X Y): 
Compiling Top-Level Form: 
;; DEFINE took 0.13 seconds
411> VERIFY SUBSETP-BADGUY
;; Reading from Proofs/utilities/thm-subsetp-badguy.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
412> VERIFY SUBSETP-BADGUY-MEMBERSHIP-PROPERTY
;; Reading from Proofs/utilities/thm-subsetp-badguy-membership-property.proof
;; Reading the file took 1.27 seconds
;; Checking the proof took 1.69 seconds
;; VERIFY took 7.20 seconds
413> VERIFY SUBSETP-BADGUY-UNDER-IFF
;; Reading from Proofs/utilities/thm-subsetp-badguy-under-iff.proof
;; Reading the file took 0.20 seconds
;; Checking the proof took 0.23 seconds
;; VERIFY took 0.92 seconds
414> VERIFY EQUAL-OF-CDR-AND-SELF
;; Reading from Proofs/utilities/thm-equal-of-cdr-and-self.proof
;; Reading the file took 0.16 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.51 seconds
415> DEFINE APP
;; Reading from Proofs/utilities/admit-app.proofs
;; Reading the file took 0.03 seconds
;; Checking the proofs took 0.02 seconds
;; DEFINE took 0.09 seconds
416> VERIFY APP
;; Reading from Proofs/utilities/thm-app.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
417> VERIFY APP-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-app-when-not-consp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.06 seconds
418> VERIFY APP-OF-CONS
;; Reading from Proofs/utilities/thm-app-of-cons.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
419> VERIFY APP-OF-LIST-FIX-ONE
;; Reading from Proofs/utilities/thm-app-of-list-fix-one.proof
;; Reading the file took 0.15 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.47 seconds
420> VERIFY APP-OF-LIST-FIX-TWO
;; Reading from Proofs/utilities/thm-app-of-list-fix-two.proof
;; Reading the file took 0.14 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.46 seconds
421> VERIFY APP-WHEN-NOT-CONSP-TWO
;; Reading from Proofs/utilities/thm-app-when-not-consp-two.proof
;; Reading the file took 0.20 seconds
;; Checking the proof took 0.18 seconds
;; VERIFY took 0.68 seconds
422> VERIFY APP-OF-SINGLETON-LIST-CHEAP
;; Reading from Proofs/utilities/thm-app-of-singleton-list-cheap.proof
;; Reading the file took 0.15 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.52 seconds
423> VERIFY TRUE-LISTP-OF-APP
;; Reading from Proofs/utilities/thm-true-listp-of-app.proof
;; Reading the file took 0.16 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.48 seconds
424> VERIFY APP-OF-APP
;; Reading from Proofs/utilities/thm-app-of-app.proof
;; Reading the file took 0.15 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.49 seconds
425> VERIFY MEMBERP-OF-APP
;; Reading from Proofs/utilities/thm-memberp-of-app.proof
;; Reading the file took 0.84 seconds
;; Checking the proof took 0.70 seconds
;; VERIFY took 3.07 seconds
426> VERIFY CONSP-OF-APP
;; Reading from Proofs/utilities/thm-consp-of-app.proof
;; Reading the file took 0.09 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.24 seconds
427> VERIFY APP-UNDER-IFF
;; Reading from Proofs/utilities/thm-app-under-iff.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.20 seconds
428> VERIFY LEN-OF-APP
;; Reading from Proofs/utilities/thm-len-of-app.proof
;; Reading the file took 0.17 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.57 seconds
429> VERIFY SUBSETP-OF-APP-ONE
;; Reading from Proofs/utilities/thm-subsetp-of-app-one.proof
;; Reading the file took 0.75 seconds
;; Checking the proof took 0.57 seconds
;; VERIFY took 2.66 seconds
430> VERIFY SUBSETP-OF-APP-TWO
;; Reading from Proofs/utilities/thm-subsetp-of-app-two.proof
;; Reading the file took 0.14 seconds
;; Checking the proof took 0.14 seconds
;; VERIFY took 0.58 seconds
431> VERIFY SUBSETP-OF-APP-THREE
;; Reading from Proofs/utilities/thm-subsetp-of-app-three.proof
;; Reading the file took 0.16 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.65 seconds
432> VERIFY SUBSETP-OF-APP-WHEN-SUBSETS
;; Reading from Proofs/utilities/thm-subsetp-of-app-when-subsets.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 1.00 seconds
;; VERIFY took 5.02 seconds
433> VERIFY SUBSETP-OF-SYMMETRIC-APPS
;; Reading from Proofs/utilities/thm-subsetp-of-symmetric-apps.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.20 seconds
434> VERIFY WEIRDO-RULE-FOR-SUBSETP-OF-APP-ONE
;; Reading from Proofs/utilities/thm-weirdo-rule-for-subsetp-of-app-one.proof
;; Reading the file took 0.17 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.54 seconds
435> VERIFY WEIRDO-RULE-FOR-SUBSETP-OF-APP-TWO
;; Reading from Proofs/utilities/thm-weirdo-rule-for-subsetp-of-app-two.proof
;; Reading the file took 0.20 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.67 seconds
436> VERIFY CDR-OF-APP-WHEN-X-IS-CONSP
;; Reading from Proofs/utilities/thm-cdr-of-app-when-x-is-consp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.06 seconds
437> VERIFY CAR-OF-APP-WHEN-X-IS-CONSP
;; Reading from Proofs/utilities/thm-car-of-app-when-x-is-consp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
438> VERIFY MEMBERP-OF-APP-ONTO-SINGLETON
;; Reading from Proofs/utilities/thm-memberp-of-app-onto-singleton.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.23 seconds
439> VERIFY SUBSETP-OF-APP-ONTO-SINGLETON-WITH-CONS
;; Reading from Proofs/utilities/thm-subsetp-of-app-onto-singleton-with-cons.proof
;; Reading the file took 0.44 seconds
;; Checking the proof took 0.70 seconds
;; VERIFY took 2.83 seconds
440> VERIFY SUBSETP-OF-CONS-WITH-APP-ONTO-SINGLETON
;; Reading from Proofs/utilities/thm-subsetp-of-cons-with-app-onto-singleton.proof
;; Reading the file took 0.26 seconds
;; Checking the proof took 0.46 seconds
;; VERIFY took 1.81 seconds
441> VERIFY SUBSETP-OF-CONS-OF-APP-OF-APP-ONE
;; Reading from Proofs/utilities/thm-subsetp-of-cons-of-app-of-app-one.proof
;; Reading the file took 0.20 seconds
;; Checking the proof took 0.26 seconds
;; VERIFY took 1.09 seconds
442> VERIFY SUBSETP-OF-CONS-OF-APP-OF-APP-TWO
;; Reading from Proofs/utilities/thm-subsetp-of-cons-of-app-of-app-two.proof
;; Reading the file took 0.17 seconds
;; Checking the proof took 0.29 seconds
;; VERIFY took 1.16 seconds
443> VERIFY SUBSETP-OF-APP-OF-APP-WHEN-SUBSETP-ONE
;; Reading from Proofs/utilities/thm-subsetp-of-app-of-app-when-subsetp-one.proof
;; Reading the file took 0.21 seconds
;; Checking the proof took 0.24 seconds
;; VERIFY took 1.08 seconds
444> VERIFY SUBSETP-OF-APP-OF-APP-WHEN-SUBSETP-TWO
;; Reading from Proofs/utilities/thm-subsetp-of-app-of-app-when-subsetp-two.proof
;; Reading the file took 0.21 seconds
;; Checking the proof took 0.24 seconds
;; VERIFY took 1.08 seconds
445> VERIFY APP-OF-CONS-OF-LIST-FIX-RIGHT
;; Reading from Proofs/utilities/thm-app-of-cons-of-list-fix-right.proof
;; Reading the file took 0.17 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.58 seconds
446> VERIFY APP-OF-CONS-WHEN-NOT-CONSP-RIGHT
;; Reading from Proofs/utilities/thm-app-of-cons-when-not-consp-right.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 0.23 seconds
;; VERIFY took 0.83 seconds
447> VERIFY EQUAL-OF-APP-AND-APP-WHEN-EQUAL-LENS
;; Reading from Proofs/utilities/thm-equal-of-app-and-app-when-equal-lens.proof
;; Reading the file took 4.14 seconds
;; Checking the proof took 5.23 seconds
;; VERIFY took 23.00 seconds
448> VERIFY LEMMA-FOR-EQUAL-OF-APP-AND-SELF
;; Reading from Proofs/utilities/thm-lemma-for-equal-of-app-and-self.proof
;; Reading the file took 0.23 seconds
;; Checking the proof took 0.24 seconds
;; VERIFY took 0.86 seconds
449> VERIFY EQUAL-OF-APP-AND-SELF
;; Reading from Proofs/utilities/thm-equal-of-app-and-self.proof
;; Reading the file took 0.28 seconds
;; Checking the proof took 0.30 seconds
;; VERIFY took 1.08 seconds
450> DEFINE REV
;; Reading from Proofs/utilities/admit-rev.proofs
;; Reading the file took 0.03 seconds
;; Checking the proofs took 0.02 seconds
;; DEFINE took 0.09 seconds
451> VERIFY REV
;; Reading from Proofs/utilities/thm-rev.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
452> VERIFY REV-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-rev-when-not-consp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
453> VERIFY REV-OF-CONS
;; Reading from Proofs/utilities/thm-rev-of-cons.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
454> VERIFY REV-OF-LIST-FIX
;; Reading from Proofs/utilities/thm-rev-of-list-fix.proof
;; Reading the file took 0.19 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.60 seconds
455> VERIFY TRUE-LISTP-OF-REV
;; Reading from Proofs/utilities/thm-true-listp-of-rev.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.08 seconds
456> VERIFY REV-UNDER-IFF
;; Reading from Proofs/utilities/thm-rev-under-iff.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.08 seconds
457> VERIFY LEN-OF-REV
;; Reading from Proofs/utilities/thm-len-of-rev.proof
;; Reading the file took 0.15 seconds
;; Checking the proof took 0.14 seconds
;; VERIFY took 0.50 seconds
458> VERIFY MEMBERP-OF-REV
;; Reading from Proofs/utilities/thm-memberp-of-rev.proof
;; Reading the file took 0.48 seconds
;; Checking the proof took 0.37 seconds
;; VERIFY took 1.58 seconds
459> VERIFY MEMBERP-OF-FIRST-OF-REV
;; Reading from Proofs/utilities/thm-memberp-of-first-of-rev.proof
;; Reading the file took 0.32 seconds
;; Checking the proof took 0.31 seconds
;; VERIFY took 1.14 seconds
460> VERIFY SUBSETP-OF-REV-ONE
;; Reading from Proofs/utilities/thm-subsetp-of-rev-one.proof
;; Reading the file took 0.77 seconds
;; Checking the proof took 0.80 seconds
;; VERIFY took 3.61 seconds
461> VERIFY SUBSETP-OF-REV-TWO
;; Reading from Proofs/utilities/thm-subsetp-of-rev-two.proof
;; Reading the file took 0.60 seconds
;; Checking the proof took 0.59 seconds
;; VERIFY took 2.62 seconds
462> VERIFY LEMMA-FOR-REV-OF-REV
;; Reading from Proofs/utilities/thm-lemma-for-rev-of-rev.proof
;; Reading the file took 0.60 seconds
;; Checking the proof took 0.76 seconds
;; VERIFY took 2.87 seconds
463> VERIFY REV-OF-REV
;; Reading from Proofs/utilities/thm-rev-of-rev.proof
;; Reading the file took 0.14 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.45 seconds
464> VERIFY REV-OF-APP
;; Reading from Proofs/utilities/thm-rev-of-app.proof
;; Reading the file took 0.15 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.50 seconds
465> VERIFY SUBSETP-OF-APP-OF-REV-OF-SELF-ONE
;; Reading from Proofs/utilities/thm-subsetp-of-app-of-rev-of-self-one.proof
;; Reading the file took 0.23 seconds
;; Checking the proof took 0.20 seconds
;; VERIFY took 0.76 seconds
466> VERIFY SUBSETP-OF-APP-OF-REV-OF-SELF-TWO
;; Reading from Proofs/utilities/thm-subsetp-of-app-of-rev-of-self-two.proof
;; Reading the file took 0.21 seconds
;; Checking the proof took 0.18 seconds
;; VERIFY took 0.71 seconds
467> DEFINE REVAPPEND
;; Reading from Proofs/utilities/admit-revappend.proofs
;; Reading the file took 0.03 seconds
;; Checking the proofs took 0.02 seconds
Compiling LAMBDA (X Y): 
Compiling Top-Level Form: 
;; DEFINE took 0.09 seconds
468> VERIFY REVAPPEND
;; Reading from Proofs/utilities/thm-revappend.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
469> VERIFY REVAPPEND-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-revappend-when-not-consp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
470> VERIFY REVAPPEND-OF-CONS
;; Reading from Proofs/utilities/thm-revappend-of-cons.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
471> VERIFY FORCING-REVAPPEND-REMOVAL
;; Reading from Proofs/utilities/thm-forcing-revappend-removal.proof
;; Reading the file took 0.23 seconds
;; Checking the proof took 0.23 seconds
;; VERIFY took 0.87 seconds
472> DEFINE FAST-REV
;; Reading from Proofs/utilities/admit-fast-rev.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
Compiling LAMBDA (X): 
Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
473> VERIFY FAST-REV
;; Reading from Proofs/utilities/thm-fast-rev.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
474> VERIFY FAST-REV-REMOVAL
;; Reading from Proofs/utilities/thm-fast-rev-removal.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
475> DEFINE FAST-APP
;; Reading from Proofs/utilities/admit-fast-app.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
Compiling LAMBDA (X Y): 
Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
476> VERIFY FAST-APP
;; Reading from Proofs/utilities/thm-fast-app.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
477> VERIFY FAST-APP-REMOVAL
;; Reading from Proofs/utilities/thm-fast-app-removal.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.10 seconds
478> DEFINE REMOVE-ALL
;; Reading from Proofs/utilities/admit-remove-all.proofs
;; Reading the file took 0.07 seconds
;; Checking the proofs took 0.07 seconds
;; DEFINE took 0.24 seconds
479> VERIFY REMOVE-ALL
;; Reading from Proofs/utilities/thm-remove-all.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
480> VERIFY REMOVE-ALL-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-remove-all-when-not-consp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
481> VERIFY REMOVE-ALL-OF-CONS
;; Reading from Proofs/utilities/thm-remove-all-of-cons.proof
;; Reading the file took 0.11 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.43 seconds
482> VERIFY REMOVE-ALL-OF-LIST-FIX
;; Reading from Proofs/utilities/thm-remove-all-of-list-fix.proof
;; Reading the file took 0.19 seconds
;; Checking the proof took 0.14 seconds
;; VERIFY took 0.56 seconds
483> VERIFY TRUE-LISTP-OF-REMOVE-ALL
;; Reading from Proofs/utilities/thm-true-listp-of-remove-all.proof
;; Reading the file took 0.16 seconds
;; Checking the proof took 0.14 seconds
;; VERIFY took 0.51 seconds
484> VERIFY MEMBERP-OF-REMOVE-ALL
;; Reading from Proofs/utilities/thm-memberp-of-remove-all.proof
;; Reading the file took 1.01 seconds
;; Checking the proof took 0.82 seconds
;; VERIFY took 3.59 seconds
485> VERIFY REMOVE-ALL-OF-APP
;; Reading from Proofs/utilities/thm-remove-all-of-app.proof
;; Reading the file took 0.18 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.65 seconds
486> VERIFY REV-OF-REMOVE-ALL
;; Reading from Proofs/utilities/thm-rev-of-remove-all.proof
;; Reading the file took 0.26 seconds
;; Checking the proof took 0.24 seconds
;; VERIFY took 0.91 seconds
487> VERIFY SUBSETP-OF-REMOVE-ALL-WITH-X
;; Reading from Proofs/utilities/thm-subsetp-of-remove-all-with-x.proof
;; Reading the file took 0.21 seconds
;; Checking the proof took 0.18 seconds
;; VERIFY took 0.66 seconds
488> VERIFY SUBSETP-OF-REMOVE-ALL-WITH-REMOVE-ALL
;; Reading from Proofs/utilities/thm-subsetp-of-remove-all-with-remove-all.proof
;; Reading the file took 0.32 seconds
;; Checking the proof took 0.38 seconds
;; VERIFY took 1.67 seconds
489> VERIFY SUBSETP-OF-REMOVE-ALL-WHEN-SUBSETP
;; Reading from Proofs/utilities/thm-subsetp-of-remove-all-when-subsetp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
490> VERIFY REMOVE-ALL-OF-NON-MEMBERP
;; Reading from Proofs/utilities/thm-remove-all-of-non-memberp.proof
;; Reading the file took 0.27 seconds
;; Checking the proof took 0.26 seconds
;; VERIFY took 0.97 seconds
491> VERIFY REMOVE-ALL-OF-REMOVE-ALL
;; Reading from Proofs/utilities/thm-remove-all-of-remove-all.proof
;; Reading the file took 0.30 seconds
;; Checking the proof took 0.27 seconds
;; VERIFY took 1.11 seconds
492> VERIFY SUBSETP-OF-CONS-AND-REMOVE-ALL-TWO
;; Reading from Proofs/utilities/thm-subsetp-of-cons-and-remove-all-two.proof
;; Reading the file took 0.54 seconds
;; Checking the proof took 0.80 seconds
;; VERIFY took 2.96 seconds
493> VERIFY LEMMA-FOR-EQUAL-OF-LEN-OF-REMOVE-ALL-AND-LEN
;; Reading from Proofs/utilities/thm-lemma-for-equal-of-len-of-remove-all-and-len.proof
;; Reading the file took 0.45 seconds
;; Checking the proof took 0.44 seconds
;; VERIFY took 1.67 seconds
494> VERIFY EQUAL-OF-LEN-OF-REMOVE-ALL-AND-LEN
;; Reading from Proofs/utilities/thm-equal-of-len-of-remove-all-and-len.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.08 seconds
495> DEFINE FAST-REMOVE-ALL$
;; Reading from Proofs/utilities/admit-fast-remove-all$.proofs
;; Reading the file took 0.06 seconds
;; Checking the proofs took 0.07 seconds
Compiling LAMBDA (A X ACC): 
Compiling Top-Level Form: 
;; DEFINE took 0.23 seconds
496> VERIFY FAST-REMOVE-ALL$
;; Reading from Proofs/utilities/thm-fast-remove-all$.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
497> VERIFY FAST-REMOVE-ALL$-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-fast-remove-all$-when-not-consp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.06 seconds
498> VERIFY FAST-REMOVE-ALL$-OF-CONS
;; Reading from Proofs/utilities/thm-fast-remove-all$-of-cons.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.12 seconds
499> VERIFY FORCING-FAST-REMOVE-ALL$-REMOVAL
;; Reading from Proofs/utilities/thm-forcing-fast-remove-all$-removal.proof
;; Reading the file took 0.61 seconds
;; Checking the proof took 0.70 seconds
;; VERIFY took 2.63 seconds
500> DEFINE DISJOINTP
;; Reading from Proofs/utilities/admit-disjointp.proofs
;; Reading the file took 0.04 seconds
;; Checking the proofs took 0.04 seconds
Compiling LAMBDA (X Y): 
Compiling Top-Level Form: 
;; DEFINE took 0.13 seconds
501> VERIFY DISJOINTP
;; Reading from Proofs/utilities/thm-disjointp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
502> VERIFY DISJOINTP-WHEN-NOT-CONSP-ONE
;; Reading from Proofs/utilities/thm-disjointp-when-not-consp-one.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.05 seconds
503> VERIFY DISJOINTP-OF-CONS-ONE
;; Reading from Proofs/utilities/thm-disjointp-of-cons-one.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.10 seconds
504> VERIFY BOOLEANP-OF-DISJOINTP
;; Reading from Proofs/utilities/thm-booleanp-of-disjointp.proof
;; Reading the file took 0.16 seconds
;; Checking the proof took 0.14 seconds
;; VERIFY took 0.50 seconds
505> VERIFY DISJOINTP-WHEN-NOT-CONSP-TWO
;; Reading from Proofs/utilities/thm-disjointp-when-not-consp-two.proof
;; Reading the file took 0.21 seconds
;; Checking the proof took 0.20 seconds
;; VERIFY took 0.73 seconds
506> VERIFY DISJOINTP-OF-CONS-TWO
;; Reading from Proofs/utilities/thm-disjointp-of-cons-two.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 1.00 seconds
;; VERIFY took 3.96 seconds
507> VERIFY SYMMETRY-OF-DISJOINTP
;; Reading from Proofs/utilities/thm-symmetry-of-disjointp.proof
;; Reading the file took 0.48 seconds
;; Checking the proof took 0.35 seconds
;; VERIFY took 1.53 seconds
508> VERIFY DISJOINTP-OF-LIST-FIX-ONE
;; Reading from Proofs/utilities/thm-disjointp-of-list-fix-one.proof
;; Reading the file took 0.43 seconds
;; Checking the proof took 0.40 seconds
;; VERIFY took 1.64 seconds
509> VERIFY DISJOINTP-OF-LIST-FIX-TWO
;; Reading from Proofs/utilities/thm-disjointp-of-list-fix-two.proof
;; Reading the file took 0.14 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.58 seconds
510> VERIFY DISJOINTP-OF-SINGLETON-ONE
;; Reading from Proofs/utilities/thm-disjointp-of-singleton-one.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.09 seconds
511> VERIFY DISJOINTP-OF-SINGLETON-TWO
;; Reading from Proofs/utilities/thm-disjointp-of-singleton-two.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.09 seconds
512> VERIFY DISJOINTP-WHEN-COMMON-MEMBER-ONE
;; Reading from Proofs/utilities/thm-disjointp-when-common-member-one.proof
;; Reading the file took 0.40 seconds
;; Checking the proof took 0.35 seconds
;; VERIFY took 1.45 seconds
513> VERIFY DISJOINTP-WHEN-COMMON-MEMBER-TWO
;; Reading from Proofs/utilities/thm-disjointp-when-common-member-two.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
514> VERIFY DISJOINTP-OF-APP-TWO
;; Reading from Proofs/utilities/thm-disjointp-of-app-two.proof
;; Reading the file took 1.10 seconds
;; Checking the proof took 1.24 seconds
;; VERIFY took 5.23 seconds
515> VERIFY DISJOINTP-OF-APP-ONE
;; Reading from Proofs/utilities/thm-disjointp-of-app-one.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.07 seconds
516> VERIFY DISJOINTP-OF-REV-TWO
;; Reading from Proofs/utilities/thm-disjointp-of-rev-two.proof
;; Reading the file took 0.44 seconds
;; Checking the proof took 0.40 seconds
;; VERIFY took 1.64 seconds
517> VERIFY DISJOINTP-OF-REV-ONE
;; Reading from Proofs/utilities/thm-disjointp-of-rev-one.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
518> VERIFY DISJOINTP-WHEN-SUBSETP-OF-DISJOINTP-ONE
;; Reading from Proofs/utilities/thm-disjointp-when-subsetp-of-disjointp-one.proof
;; Reading the file took 0.33 seconds
;; Checking the proof took 0.33 seconds
;; VERIFY took 1.28 seconds
519> VERIFY DISJOINTP-WHEN-SUBSETP-OF-DISJOINTP-TWO
;; Reading from Proofs/utilities/thm-disjointp-when-subsetp-of-disjointp-two.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.06 seconds
520> VERIFY DISJOINTP-WHEN-SUBSETP-OF-DISJOINTP-THREE
;; Reading from Proofs/utilities/thm-disjointp-when-subsetp-of-disjointp-three.proof
;; Reading the file took 0.36 seconds
;; Checking the proof took 0.33 seconds
;; VERIFY took 1.29 seconds
521> VERIFY DISJOINTP-WHEN-SUBSETP-OF-DISJOINTP-FOUR
;; Reading from Proofs/utilities/thm-disjointp-when-subsetp-of-disjointp-four.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.06 seconds
522> VERIFY DISJOINTP-WHEN-SUBSETP-OF-OTHER-ONE
;; Reading from Proofs/utilities/thm-disjointp-when-subsetp-of-other-one.proof
;; Reading the file took 0.28 seconds
;; Checking the proof took 0.30 seconds
;; VERIFY took 1.06 seconds
523> VERIFY DISJOINTP-WHEN-SUBSETP-OF-OTHER-TWO
;; Reading from Proofs/utilities/thm-disjointp-when-subsetp-of-other-two.proof
;; Reading the file took 0.28 seconds
;; Checking the proof took 0.29 seconds
;; VERIFY took 1.06 seconds
524> VERIFY MEMBERP-WHEN-DISJOINTP-ONE
;; Reading from Proofs/utilities/thm-memberp-when-disjointp-one.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 0.25 seconds
;; VERIFY took 0.90 seconds
525> VERIFY MEMBERP-WHEN-DISJOINTP-TWO
;; Reading from Proofs/utilities/thm-memberp-when-disjointp-two.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
526> DEFINE UNIQUEP
;; Reading from Proofs/utilities/admit-uniquep.proofs
;; Reading the file took 0.04 seconds
;; Checking the proofs took 0.04 seconds
;; DEFINE took 0.13 seconds
527> VERIFY UNIQUEP
;; Reading from Proofs/utilities/thm-uniquep.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
528> VERIFY UNIQUEP-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-uniquep-when-not-consp.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.07 seconds
529> VERIFY UNIQUEP-OF-CONS
;; Reading from Proofs/utilities/thm-uniquep-of-cons.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.10 seconds
530> VERIFY UNIQUEP-OF-LIST-FIX
;; Reading from Proofs/utilities/thm-uniquep-of-list-fix.proof
;; Reading the file took 0.14 seconds
;; Checking the proof took 0.14 seconds
;; VERIFY took 0.46 seconds
531> VERIFY BOOLEANP-OF-UNIQUEP
;; Reading from Proofs/utilities/thm-booleanp-of-uniquep.proof
;; Reading the file took 0.16 seconds
;; Checking the proof took 0.14 seconds
;; VERIFY took 0.50 seconds
532> VERIFY UNIQUEP-OF-CDR-WHEN-UNIQUEP
;; Reading from Proofs/utilities/thm-uniquep-of-cdr-when-uniquep.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.13 seconds
533> VERIFY MEMBERP-OF-CAR-IN-CDR-WHEN-UNIQUEP
;; Reading from Proofs/utilities/thm-memberp-of-car-in-cdr-when-uniquep.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.10 seconds
534> DEFINE DIFFERENCE
;; Reading from Proofs/utilities/admit-difference.proofs
;; Reading the file took 0.08 seconds
;; Checking the proofs took 0.07 seconds
;; DEFINE took 0.25 seconds
535> VERIFY DIFFERENCE
;; Reading from Proofs/utilities/thm-difference.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
536> VERIFY DIFFERENCE-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-difference-when-not-consp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
537> VERIFY DIFFERENCE-OF-CONS
;; Reading from Proofs/utilities/thm-difference-of-cons.proof
;; Reading the file took 0.11 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.44 seconds
538> VERIFY TRUE-LISTP-OF-DIFFERENCE
;; Reading from Proofs/utilities/thm-true-listp-of-difference.proof
;; Reading the file took 0.16 seconds
;; Checking the proof took 0.14 seconds
;; VERIFY took 0.51 seconds
539> VERIFY DIFFERENCE-OF-LIST-FIX-ONE
;; Reading from Proofs/utilities/thm-difference-of-list-fix-one.proof
;; Reading the file took 0.15 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.52 seconds
540> VERIFY DIFFERENCE-OF-LIST-FIX-TWO
;; Reading from Proofs/utilities/thm-difference-of-list-fix-two.proof
;; Reading the file took 0.14 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.51 seconds
541> VERIFY DIFFERENCE-OF-APP-ONE
;; Reading from Proofs/utilities/thm-difference-of-app-one.proof
;; Reading the file took 0.17 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.60 seconds
542> VERIFY DIFFERENCE-OF-DIFFERENCE
;; Reading from Proofs/utilities/thm-difference-of-difference.proof
;; Reading the file took 0.35 seconds
;; Checking the proof took 0.37 seconds
;; VERIFY took 1.48 seconds
543> VERIFY REV-OF-DIFFERENCE
;; Reading from Proofs/utilities/thm-rev-of-difference.proof
;; Reading the file took 0.23 seconds
;; Checking the proof took 0.24 seconds
;; VERIFY took 0.84 seconds
544> VERIFY DIFFERENCE-OF-REV
;; Reading from Proofs/utilities/thm-difference-of-rev.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
545> VERIFY DIFFERENCE-OF-REV-TWO
;; Reading from Proofs/utilities/thm-difference-of-rev-two.proof
;; Reading the file took 0.15 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.51 seconds
546> VERIFY MEMBERP-OF-DIFFERENCE
;; Reading from Proofs/utilities/thm-memberp-of-difference.proof
;; Reading the file took 1.00 seconds
;; Checking the proof took 0.84 seconds
;; VERIFY took 3.62 seconds
547> VERIFY DIFFERENCE-WHEN-SUBSETP
;; Reading from Proofs/utilities/thm-difference-when-subsetp.proof
;; Reading the file took 0.20 seconds
;; Checking the proof took 0.19 seconds
;; VERIFY took 0.68 seconds
548> VERIFY SUBSETP-WITH-APP-OF-DIFFERENCE-ONTO-TAKEAWAY
;; Reading from Proofs/utilities/thm-subsetp-with-app-of-difference-onto-takeaway.proof
;; Reading the file took 0.25 seconds
;; Checking the proof took 0.25 seconds
;; VERIFY took 0.93 seconds
549> DEFINE FAST-DIFFERENCE$
;; Reading from Proofs/utilities/admit-fast-difference$.proofs
;; Reading the file took 0.07 seconds
;; Checking the proofs took 0.07 seconds
Compiling LAMBDA (X Y ACC): 
Compiling Top-Level Form: 
;; DEFINE took 0.25 seconds
550> VERIFY FAST-DIFFERENCE$
;; Reading from Proofs/utilities/thm-fast-difference$.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
551> VERIFY FAST-DIFFERENCE$-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-fast-difference$-when-not-consp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.06 seconds
552> VERIFY FAST-DIFFERENCE$-OF-CONS
;; Reading from Proofs/utilities/thm-fast-difference$-of-cons.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.13 seconds
553> VERIFY FORCING-FAST-DIFFERENCE$-REMOVAL
;; Reading from Proofs/utilities/thm-forcing-fast-difference$-removal.proof
;; Reading the file took 0.58 seconds
;; Checking the proof took 0.72 seconds
;; VERIFY took 2.59 seconds
554> DEFINE REMOVE-DUPLICATES
;; Reading from Proofs/utilities/admit-remove-duplicates.proofs
;; Reading the file took 0.08 seconds
;; Checking the proofs took 0.08 seconds
;; DEFINE took 0.27 seconds
555> VERIFY REMOVE-DUPLICATES
;; Reading from Proofs/utilities/thm-remove-duplicates.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
556> VERIFY REMOVE-DUPLICATES-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-remove-duplicates-when-not-consp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
557> VERIFY REMOVE-DUPLICATES-OF-CONS
;; Reading from Proofs/utilities/thm-remove-duplicates-of-cons.proof
;; Reading the file took 0.11 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.44 seconds
558> VERIFY TRUE-LISTP-OF-REMOVE-DUPLICATES
;; Reading from Proofs/utilities/thm-true-listp-of-remove-duplicates.proof
;; Reading the file took 0.16 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.51 seconds
559> VERIFY LEN-OF-REMOVE-DUPLICATES
;; Reading from Proofs/utilities/thm-len-of-remove-duplicates.proof
;; Reading the file took 0.16 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.57 seconds
560> VERIFY REMOVE-DUPLICATES-OF-LIST-FIX
;; Reading from Proofs/utilities/thm-remove-duplicates-of-list-fix.proof
;; Reading the file took 0.15 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.52 seconds
561> VERIFY MEMBERP-OF-REMOVE-DUPLICATES
;; Reading from Proofs/utilities/thm-memberp-of-remove-duplicates.proof
;; Reading the file took 0.59 seconds
;; Checking the proof took 0.45 seconds
;; VERIFY took 1.88 seconds
562> VERIFY SUBSETP-OF-REMOVE-DUPLICATES-ONE
;; Reading from Proofs/utilities/thm-subsetp-of-remove-duplicates-one.proof
;; Reading the file took 0.70 seconds
;; Checking the proof took 0.94 seconds
;; VERIFY took 3.70 seconds
563> VERIFY SUBSETP-OF-REMOVE-DUPLICATES-TWO
;; Reading from Proofs/utilities/thm-subsetp-of-remove-duplicates-two.proof
;; Reading the file took 0.55 seconds
;; Checking the proof took 0.68 seconds
;; VERIFY took 2.63 seconds
564> VERIFY SUBSETP-OF-CONS-ONTO-REMOVE-DUPLICATES
;; Reading from Proofs/utilities/thm-subsetp-of-cons-onto-remove-duplicates.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.19 seconds
565> DEFINE TUPLEP
;; Reading from Proofs/utilities/admit-tuplep.proofs
;; Reading the file took 0.05 seconds
;; Checking the proofs took 0.06 seconds
;; DEFINE took 0.19 seconds
566> VERIFY TUPLEP
;; Reading from Proofs/utilities/thm-tuplep.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
567> VERIFY TUPLEP-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-tuplep-when-not-consp.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.17 seconds
568> VERIFY TUPLEP-WHEN-ZP
;; Reading from Proofs/utilities/thm-tuplep-when-zp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.06 seconds
569> VERIFY TUPLEP-OF-CONS
;; Reading from Proofs/utilities/thm-tuplep-of-cons.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.12 seconds
570> VERIFY BOOLEANP-OF-TUPLEP
;; Reading from Proofs/utilities/thm-booleanp-of-tuplep.proof
;; Reading the file took 0.20 seconds
;; Checking the proof took 0.20 seconds
;; VERIFY took 0.67 seconds
571> VERIFY TRUE-LISTP-WHEN-TUPLEP
;; Reading from Proofs/utilities/thm-true-listp-when-tuplep.proof
;; Reading the file took 0.53 seconds
;; Checking the proof took 0.56 seconds
;; VERIFY took 1.96 seconds
572> VERIFY LEN-WHEN-TUPLEP
;; Reading from Proofs/utilities/thm-len-when-tuplep.proof
;; Reading the file took 0.70 seconds
;; Checking the proof took 0.75 seconds
;; VERIFY took 2.70 seconds
573> VERIFY TUPLEP-OF-LEN
;; Reading from Proofs/utilities/thm-tuplep-of-len.proof
;; Reading the file took 0.46 seconds
;; Checking the proof took 0.52 seconds
;; VERIFY took 1.82 seconds
574> VERIFY TUPLEP-WHEN-TRUE-LISTP
;; Reading from Proofs/utilities/thm-tuplep-when-true-listp.proof
;; Reading the file took 0.57 seconds
;; Checking the proof took 0.66 seconds
;; VERIFY took 2.41 seconds
575> VERIFY CONSP-OF-CDR-WHEN-TUPLEP-2-CHEAP
;; Reading from Proofs/utilities/thm-consp-of-cdr-when-tuplep-2-cheap.proof
;; Reading the file took 0.09 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.23 seconds
576> VERIFY CONSP-OF-CDR-WHEN-TUPLEP-3-CHEAP
;; Reading from Proofs/utilities/thm-consp-of-cdr-when-tuplep-3-cheap.proof
;; Reading the file took 0.09 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.24 seconds
577> VERIFY CONSP-OF-CDR-OF-CDR-WHEN-TUPLEP-3-CHEAP
;; Reading from Proofs/utilities/thm-consp-of-cdr-of-cdr-when-tuplep-3-cheap.proof
;; Reading the file took 0.15 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.38 seconds
578> DEFINE REPEAT
;; Reading from Proofs/utilities/admit-repeat.proofs
;; Reading the file took 0.05 seconds
;; Checking the proofs took 0.05 seconds
;; DEFINE took 0.15 seconds
579> VERIFY REPEAT
;; Reading from Proofs/utilities/thm-repeat.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
580> VERIFY REPEAT-OF-ZERO
;; Reading from Proofs/utilities/thm-repeat-of-zero.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
581> VERIFY REPEAT-OF-ONE
;; Reading from Proofs/utilities/thm-repeat-of-one.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
582> VERIFY CONSP-OF-REPEAT
;; Reading from Proofs/utilities/thm-consp-of-repeat.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.12 seconds
583> VERIFY REPEAT-UNDER-IFF
;; Reading from Proofs/utilities/thm-repeat-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
584> VERIFY CAR-OF-REPEAT
;; Reading from Proofs/utilities/thm-car-of-repeat.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.10 seconds
585> VERIFY CDR-OF-REPEAT
;; Reading from Proofs/utilities/thm-cdr-of-repeat.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.11 seconds
586> VERIFY REPEAT-OF-NFIX
;; Reading from Proofs/utilities/thm-repeat-of-nfix.proof
;; Reading the file took 0.20 seconds
;; Checking the proof took 0.23 seconds
;; VERIFY took 0.77 seconds
587> VERIFY LEN-OF-REPEAT
;; Reading from Proofs/utilities/thm-len-of-repeat.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 0.26 seconds
;; VERIFY took 0.82 seconds
588> VERIFY TRUE-LISTP-OF-REPEAT
;; Reading from Proofs/utilities/thm-true-listp-of-repeat.proof
;; Reading the file took 0.12 seconds
;; Checking the proof took 0.14 seconds
;; VERIFY took 0.45 seconds
589> VERIFY MEMBERP-OF-REPEAT
;; Reading from Proofs/utilities/thm-memberp-of-repeat.proof
;; Reading the file took 0.70 seconds
;; Checking the proof took 0.77 seconds
;; VERIFY took 2.81 seconds
590> VERIFY APP-OF-REPEAT
;; Reading from Proofs/utilities/thm-app-of-repeat.proof
;; Reading the file took 0.51 seconds
;; Checking the proof took 0.51 seconds
;; VERIFY took 1.85 seconds
591> VERIFY LEMMA-FOR-REV-OF-REPEAT
;; Reading from Proofs/utilities/thm-lemma-for-rev-of-repeat.proof
;; Reading the file took 0.33 seconds
;; Checking the proof took 0.51 seconds
;; VERIFY took 1.66 seconds
592> VERIFY REV-OF-REPEAT
;; Reading from Proofs/utilities/thm-rev-of-repeat.proof
;; Reading the file took 0.20 seconds
;; Checking the proof took 0.25 seconds
;; VERIFY took 0.78 seconds
593> DEFINE NTH
;; Reading from Proofs/utilities/admit-nth.proofs
;; Reading the file took 0.04 seconds
;; Checking the proofs took 0.04 seconds
Compiling LAMBDA (N X): 
Compiling Top-Level Form: 
;; DEFINE took 0.13 seconds
594> VERIFY NTH
;; Reading from Proofs/utilities/thm-nth.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
595> VERIFY NTH-WHEN-ZP
;; Reading from Proofs/utilities/thm-nth-when-zp.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.13 seconds
596> VERIFY NTH-OF-NFIX
;; Reading from Proofs/utilities/thm-nth-of-nfix.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.09 seconds
597> VERIFY NTH-OF-LIST-FIX
;; Reading from Proofs/utilities/thm-nth-of-list-fix.proof
;; Reading the file took 0.19 seconds
;; Checking the proof took 0.29 seconds
;; VERIFY took 0.91 seconds
598> VERIFY NTH-WHEN-INDEX-TOO-LARGE
;; Reading from Proofs/utilities/thm-nth-when-index-too-large.proof
;; Reading the file took 0.33 seconds
;; Checking the proof took 0.45 seconds
;; VERIFY took 1.46 seconds
599> VERIFY NTH-OF-INCREMENT
;; Reading from Proofs/utilities/thm-nth-of-increment.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.24 seconds
600> VERIFY NTH-OF-APP
;; Reading from Proofs/utilities/thm-nth-of-app.proof
;; Reading the file took 1.19 seconds
;; Checking the proof took 1.98 seconds
;; VERIFY took 6.60 seconds
601> VERIFY NTH-OF-REV
;; Reading from Proofs/utilities/thm-nth-of-rev.proof
;; Reading the file took 1.04 seconds
;; Checking the proof took 1.25 seconds
;; VERIFY took 4.22 seconds
602> VERIFY MEMBERP-OF-NTH
;; Reading from Proofs/utilities/thm-memberp-of-nth.proof
;; Reading the file took 0.57 seconds
;; Checking the proof took 0.76 seconds
;; VERIFY took 2.58 seconds
603> VERIFY DISJOINTP-OF-REMOVE-ALL-OF-REMOVE-ALL-WHEN-DISJOINTP-RIGHT
;; Reading from Proofs/utilities/thm-disjointp-of-remove-all-of-remove-all-when-disjointp-right.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
604> VERIFY DISJOINTP-OF-REMOVE-ALL-WHEN-DISJOINTP-LEFT
;; Reading from Proofs/utilities/thm-disjointp-of-remove-all-when-disjointp-left.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
605> VERIFY UNIQUEP-OF-APP
;; Reading from Proofs/utilities/thm-uniquep-of-app.proof
;; Reading the file took 1.11 seconds
;; Checking the proof took 1.31 seconds
;; VERIFY took 5.08 seconds
606> VERIFY UNIQUEP-OF-REV
;; Reading from Proofs/utilities/thm-uniquep-of-rev.proof
;; Reading the file took 0.43 seconds
;; Checking the proof took 0.43 seconds
;; VERIFY took 1.62 seconds
607> VERIFY UNIQUEP-OF-REMOVE-ALL-WHEN-UNIQUEP
;; Reading from Proofs/utilities/thm-uniquep-of-remove-all-when-uniquep.proof
;; Reading the file took 0.29 seconds
;; Checking the proof took 0.29 seconds
;; VERIFY took 1.01 seconds
608> VERIFY UNIQUEP-OF-DIFFERENCE-WHEN-UNIQUEP
;; Reading from Proofs/utilities/thm-uniquep-of-difference-when-uniquep.proof
;; Reading the file took 0.28 seconds
;; Checking the proof took 0.27 seconds
;; VERIFY took 0.98 seconds
609> VERIFY DISJOINTP-OF-DIFFERENCE-WITH-Y
;; Reading from Proofs/utilities/thm-disjointp-of-difference-with-y.proof
;; Reading the file took 0.20 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.58 seconds
610> VERIFY DISJOINTP-OF-DIFFERENCE-WITH-Y-ALT
;; Reading from Proofs/utilities/thm-disjointp-of-difference-with-y-alt.proof
;; Reading the file took 0.18 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.56 seconds
611> VERIFY UNIQUEP-OF-REMOVE-DUPLICATES
;; Reading from Proofs/utilities/thm-uniquep-of-remove-duplicates.proof
;; Reading the file took 0.17 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.53 seconds
612> VERIFY REMOVE-DUPLICATES-OF-DIFFERENCE
;; Reading from Proofs/utilities/thm-remove-duplicates-of-difference.proof
;; Reading the file took 0.32 seconds
;; Checking the proof took 0.34 seconds
;; VERIFY took 1.28 seconds
613> VERIFY REMOVE-DUPLICATES-WHEN-UNIQUE
;; Reading from Proofs/utilities/thm-remove-duplicates-when-unique.proof
;; Reading the file took 0.25 seconds
;; Checking the proof took 0.27 seconds
;; VERIFY took 0.93 seconds
614> VERIFY APP-OF-REMOVE-DUPLICATES-WITH-UNIQUE-AND-DISJOINT
;; Reading from Proofs/utilities/thm-app-of-remove-duplicates-with-unique-and-disjoint.proof
;; Reading the file took 0.43 seconds
;; Checking the proof took 0.49 seconds
;; VERIFY took 1.79 seconds
615> VERIFY REMOVE-DUPLICATES-OF-REMOVE-ALL
;; Reading from Proofs/utilities/thm-remove-duplicates-of-remove-all.proof
;; Reading the file took 0.33 seconds
;; Checking the proof took 0.36 seconds
;; VERIFY took 1.30 seconds
616> VERIFY SUBSETP-OF-REMOVE-ALL-OF-REMOVE-DUPLICATES
;; Reading from Proofs/utilities/thm-subsetp-of-remove-all-of-remove-duplicates.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.13 seconds
617> VERIFY EQUAL-OF-NTHS-WHEN-UNIQUEP
;; Reading from Proofs/utilities/thm-equal-of-nths-when-uniquep.proof
./final-checks.sh: line 70:  9428 Segmentation fault      nice ./milawa-$LISPNAME "$CURR.$EXT" <"Proofs/$NEXT.events"

Error: utilities.lhug-scl 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?