Processing utilities
Milawa Proof Checker.
1> VERIFY THEOREM-SUBSTITUTE-INTO-NOT-PEQUAL
;; Reading from Proofs/utilities/thm-theorem-substitute-into-not-pequal.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
2> VERIFY THEOREM-NOT-T-OR-NOT-NIL
;; Reading from Proofs/utilities/thm-theorem-not-t-or-not-nil.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
5> DEFINE IFF
;; Reading from Proofs/utilities/admit-iff.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
6> VERIFY IFF
;; Reading from Proofs/utilities/thm-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
7> VERIFY THEOREM-COMMUTATIVITY-OF-PEQUAL
;; Reading from Proofs/utilities/thm-theorem-commutativity-of-pequal.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
8> VERIFY THEOREM-TRANSITIVITY-OF-PEQUAL
;; Reading from Proofs/utilities/thm-theorem-transitivity-of-pequal.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
9> VERIFY THEOREM-REFLEXIVITY-OF-EQUAL
;; Reading from Proofs/utilities/thm-theorem-reflexivity-of-equal.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
10> VERIFY THEOREM-EQUAL-NIL-OR-T
;; Reading from Proofs/utilities/thm-theorem-equal-nil-or-t.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
11> VERIFY THEOREM-SYMMETRY-OF-EQUAL
;; Reading from Proofs/utilities/thm-theorem-symmetry-of-equal.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
12> VERIFY THEOREM-TRANSITIVITY-OF-EQUAL
;; Reading from Proofs/utilities/thm-theorem-transitivity-of-equal.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
13> VERIFY THEOREM-EQUAL-OF-EQUAL-AND-T
;; Reading from Proofs/utilities/thm-theorem-equal-of-equal-and-t.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
14> VERIFY THEOREM-IF-REDUX-SAME
;; Reading from Proofs/utilities/thm-theorem-if-redux-same.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
15> VERIFY THEOREM-IF-WHEN-SAME
;; Reading from Proofs/utilities/thm-theorem-if-when-same.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
16> VERIFY THEOREM-IF-REDUX-THEN
;; Reading from Proofs/utilities/thm-theorem-if-redux-then.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
17> VERIFY THEOREM-IF-REDUX-ELSE
;; Reading from Proofs/utilities/thm-theorem-if-redux-else.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
18> VERIFY THEOREM-IF-REDUX-TEST
;; Reading from Proofs/utilities/thm-theorem-if-redux-test.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
19> VERIFY THEOREM-IF-REDUX-NIL
;; Reading from Proofs/utilities/thm-theorem-if-redux-nil.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
20> VERIFY THEOREM-IF-REDUX-T
;; Reading from Proofs/utilities/thm-theorem-if-redux-t.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
21> VERIFY THEOREM-IFF-LHS-FALSE
;; Reading from Proofs/utilities/thm-theorem-iff-lhs-false.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 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.01 seconds
23> VERIFY THEOREM-IFF-RHS-FALSE
;; Reading from Proofs/utilities/thm-theorem-iff-rhs-false.proof
;; Reading the file took 0.00 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.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
28> VERIFY THEOREM-IFF-FALSE-TRUE
;; Reading from Proofs/utilities/thm-theorem-iff-false-true.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
29> VERIFY THEOREM-IFF-T-WHEN-NOT-NIL
;; Reading from Proofs/utilities/thm-theorem-iff-t-when-not-nil.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
30> VERIFY THEOREM-IFF-T-WHEN-NIL
;; Reading from Proofs/utilities/thm-theorem-iff-t-when-nil.proof
;; Reading the file took 0.01 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
32> VERIFY THEOREM-IFF-NIL-WHEN-NOT-NIL
;; Reading from Proofs/utilities/thm-theorem-iff-nil-when-not-nil.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
34> VERIFY THEOREM-REFLEXIVITY-OF-IFF
;; Reading from Proofs/utilities/thm-theorem-reflexivity-of-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
35> VERIFY THEOREM-SYMMETRY-OF-IFF
;; Reading from Proofs/utilities/thm-theorem-symmetry-of-iff.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
38> VERIFY THEOREM-IFF-CONGRUENT-IF-1
;; Reading from Proofs/utilities/thm-theorem-iff-congruent-if-1.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.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.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
41> VERIFY THEOREM-TRANSITIVITY-OF-IFF
;; Reading from Proofs/utilities/thm-theorem-transitivity-of-iff.proof
;; Reading the file took 0.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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.01 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.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
50> VERIFY CLAUSE.THEOREM-STANDARDIZE-EQUAL-X-NIL
;; Reading from Proofs/utilities/thm-clause.theorem-standardize-equal-x-nil.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.00 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.00 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.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
58> VERIFY RW.THEOREM-IFF-IMPLIES-PEQUAL-IF-1
;; Reading from Proofs/utilities/thm-rw.theorem-iff-implies-pequal-if-1.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
59> VERIFY RW.THEOREM-EQUAL-IMPLIES-PEQUAL-IF-2
;; Reading from Proofs/utilities/thm-rw.theorem-equal-implies-pequal-if-2.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.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.01 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.01 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.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
63> VERIFY RW.THEOREM-IFF-IMPLIES-IFF-IF-3
;; Reading from Proofs/utilities/thm-rw.theorem-iff-implies-iff-if-3.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
64> VERIFY RW.THEOREM-IFF-IMPLIES-IFF-IF-COMBINED
;; Reading from Proofs/utilities/thm-rw.theorem-iff-implies-iff-if-combined.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.01 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.00 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.00 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.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 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.02 seconds
71> VERIFY RW.CREWRITE-RULE-LEMMA
;; Reading from Proofs/utilities/thm-rw.crewrite-rule-lemma.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
72> VERIFY RW.COMPILE-NOT-LEMMA1
;; Reading from Proofs/utilities/thm-rw.compile-not-lemma1.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.02 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.01 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
;; DEFINE took 0.00 seconds
78> VERIFY IMPLIES
;; Reading from Proofs/utilities/thm-implies.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
79> VERIFY REFLEXIVITY-OF-EQUAL
;; Reading from Proofs/utilities/thm-reflexivity-of-equal.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.01 seconds
82> VERIFY CONSP-OF-CONS
;; Reading from Proofs/utilities/thm-consp-of-cons.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
83> DEFINE NFIX
;; Reading from Proofs/utilities/admit-nfix.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
84> VERIFY NFIX
;; Reading from Proofs/utilities/thm-nfix.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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
;; DEFINE took 0.00 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.01 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
;; DEFINE took 0.00 seconds
92> VERIFY MAX
;; Reading from Proofs/utilities/thm-max.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
93> DEFINE MAX3
;; Reading from Proofs/utilities/admit-max3.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
94> VERIFY MAX3
;; Reading from Proofs/utilities/thm-max3.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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
;; 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.39 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.59 seconds
98> VERIFY BOOLEANP-OF-BOOLEANP
;; Reading from Proofs/utilities/thm-booleanp-of-booleanp.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.11 seconds
99> VERIFY BOOLEANP-OF-EQUAL
;; Reading from Proofs/utilities/thm-booleanp-of-equal.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.05 seconds
100> VERIFY BOOLEANP-OF-NOT
;; Reading from Proofs/utilities/thm-booleanp-of-not.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.09 seconds
101> VERIFY BOOLEANP-OF-IFF
;; Reading from Proofs/utilities/thm-booleanp-of-iff.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.06 seconds
102> VERIFY BOOLEANP-OF-ZP
;; Reading from Proofs/utilities/thm-booleanp-of-zp.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 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.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 seconds
104> VERIFY EQUAL-OF-NIL-TWO
;; Reading from Proofs/utilities/thm-equal-of-nil-two.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.05 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.01 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.02 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.06 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.06 seconds
109> VERIFY BOOLEANP-OF-CONSP
;; Reading from Proofs/utilities/thm-booleanp-of-consp.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.07 seconds
110> VERIFY CAR-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-car-when-not-consp.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.06 seconds
111> VERIFY CDR-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-cdr-when-not-consp.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.06 seconds
112> VERIFY CAR-OF-CONS
;; Reading from Proofs/utilities/thm-car-of-cons.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
113> VERIFY CDR-OF-CONS
;; Reading from Proofs/utilities/thm-cdr-of-cons.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
114> VERIFY CONS-OF-CAR-AND-CDR
;; Reading from Proofs/utilities/thm-cons-of-car-and-cdr.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
115> VERIFY EQUAL-OF-CONS-REWRITE
;; Reading from Proofs/utilities/thm-equal-of-cons-rewrite.proof
;; Reading the file took 0.24 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.39 seconds
116> VERIFY BOOLEANP-OF-SYMBOLP
;; Reading from Proofs/utilities/thm-booleanp-of-symbolp.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.06 seconds
117> VERIFY BOOLEANP-OF-SYMBOL-<
;; Reading from Proofs/utilities/thm-booleanp-of-symbol-_lt_.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.07 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.04 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.05 seconds
120> VERIFY TRANSITIVITY-OF-SYMBOL-<
;; Reading from Proofs/utilities/thm-transitivity-of-symbol-_lt_.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.05 seconds
121> VERIFY TRICHOTOMY-OF-SYMBOL-<
;; Reading from Proofs/utilities/thm-trichotomy-of-symbol-_lt_.proof
;; Reading the file took 0.26 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.49 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.01 seconds
;; VERIFY took 0.11 seconds
123> VERIFY SYMBOL-<-COMPLETION-RIGHT
;; Reading from Proofs/utilities/thm-symbol-_lt_-completion-right.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.10 seconds
124> VERIFY BOOLEANP-OF-NATP
;; Reading from Proofs/utilities/thm-booleanp-of-natp.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.07 seconds
125> VERIFY SYMBOLP-WHEN-NATP-CHEAP
;; Reading from Proofs/utilities/thm-symbolp-when-natp-cheap.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.05 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.00 seconds
;; VERIFY took 0.04 seconds
127> VERIFY CONSP-WHEN-NATP-CHEAP
;; Reading from Proofs/utilities/thm-consp-when-natp-cheap.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.05 seconds
128> VERIFY BOOLEANP-WHEN-NATP-CHEAP
;; Reading from Proofs/utilities/thm-booleanp-when-natp-cheap.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.08 seconds
129> VERIFY BOOLEANP-WHEN-CONSP-CHEAP
;; Reading from Proofs/utilities/thm-booleanp-when-consp-cheap.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.07 seconds
130> VERIFY SYMBOLP-WHEN-BOOLEANP-CHEAP
;; Reading from Proofs/utilities/thm-symbolp-when-booleanp-cheap.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.00 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.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
132> VERIFY EQUAL-OF-SYMBOL-AND-NON-SYMBOL-CHEAP
;; Reading from Proofs/utilities/thm-equal-of-symbol-and-non-symbol-cheap.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 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.04 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 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.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 seconds
135> VERIFY EQUAL-OF-NON-CONS-AND-CONS-CHEAP
;; Reading from Proofs/utilities/thm-equal-of-non-cons-and-cons-cheap.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 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.04 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.05 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.05 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.06 seconds
138> VERIFY CAR-WHEN-SYMBOLP-CHEAP
;; Reading from Proofs/utilities/thm-car-when-symbolp-cheap.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.08 seconds
139> VERIFY NOT-OF-NOT-UNDER-IFF
;; Reading from Proofs/utilities/thm-not-of-not-under-iff.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
140> VERIFY IMPLIES-OF-SELF
;; Reading from Proofs/utilities/thm-implies-of-self.proof
;; Reading the file took 0.03 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.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
142> VERIFY IMPLIES-OF-T-RIGHT
;; Reading from Proofs/utilities/thm-implies-of-t-right.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
143> VERIFY IMPLIES-OF-NIL-LEFT
;; Reading from Proofs/utilities/thm-implies-of-nil-left.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.00 seconds
;; VERIFY took 0.05 seconds
146> VERIFY NATP-OF-NFIX
;; Reading from Proofs/utilities/thm-natp-of-nfix.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.05 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.00 seconds
;; VERIFY took 0.04 seconds
148> VERIFY NFIX-WHEN-NOT-NATP-CHEAP
;; Reading from Proofs/utilities/thm-nfix-when-not-natp-cheap.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
149> VERIFY EQUAL-OF-NFIX-OF-SELF
;; Reading from Proofs/utilities/thm-equal-of-nfix-of-self.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.06 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
151> VERIFY EQUAL-OF-ZERO-AND-NFIX
;; Reading from Proofs/utilities/thm-equal-of-zero-and-nfix.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.05 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.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.00 seconds
;; VERIFY took 0.04 seconds
154> VERIFY ZP-WHEN-NOT-NATP-CHEAP
;; Reading from Proofs/utilities/thm-zp-when-not-natp-cheap.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 seconds
155> VERIFY ZP-OF-NFIX
;; Reading from Proofs/utilities/thm-zp-of-nfix.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.06 seconds
156> VERIFY NFIX-OF-NFIX
;; Reading from Proofs/utilities/thm-nfix-of-nfix.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
157> VERIFY NATP-WHEN-NOT-ZP-CHEAP
;; Reading from Proofs/utilities/thm-natp-when-not-zp-cheap.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.06 seconds
158> VERIFY NATP-WHEN-ZP-CHEAP
;; Reading from Proofs/utilities/thm-natp-when-zp-cheap.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.09 seconds
159> VERIFY NFIX-WHEN-ZP-CHEAP
;; Reading from Proofs/utilities/thm-nfix-when-zp-cheap.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.12 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.15 seconds
161> VERIFY NATP-OF-PLUS
;; Reading from Proofs/utilities/thm-natp-of-plus.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
162> VERIFY PLUS-UNDER-IFF
;; Reading from Proofs/utilities/thm-plus-under-iff.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 seconds
163> VERIFY COMMUTATIVITY-OF-+
;; Reading from Proofs/utilities/thm-commutativity-of-+.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
164> VERIFY ASSOCIATIVITY-OF-+
;; Reading from Proofs/utilities/thm-associativity-of-+.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.00 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.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
167> VERIFY PLUS-COMPLETION-LEFT
;; Reading from Proofs/utilities/thm-plus-completion-left.proof
;; Reading the file took 0.45 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.94 seconds
168> VERIFY PLUS-COMPLETION-RIGHT
;; Reading from Proofs/utilities/thm-plus-completion-right.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.08 seconds
169> VERIFY PLUS-OF-ZERO-RIGHT
;; Reading from Proofs/utilities/thm-plus-of-zero-right.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.09 seconds
170> VERIFY PLUS-OF-ZERO-LEFT
;; Reading from Proofs/utilities/thm-plus-of-zero-left.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
171> VERIFY PLUS-WHEN-ZP-LEFT-CHEAP
;; Reading from Proofs/utilities/thm-plus-when-zp-left-cheap.proof
;; Reading the file took 0.10 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.14 seconds
172> VERIFY PLUS-WHEN-ZP-RIGHT-CHEAP
;; Reading from Proofs/utilities/thm-plus-when-zp-right-cheap.proof
;; Reading the file took 0.10 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.14 seconds
173> VERIFY PLUS-OF-NFIX-LEFT
;; Reading from Proofs/utilities/thm-plus-of-nfix-left.proof
;; Reading the file took 0.11 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.15 seconds
174> VERIFY PLUS-OF-NFIX-RIGHT
;; Reading from Proofs/utilities/thm-plus-of-nfix-right.proof
;; Reading the file took 0.10 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.15 seconds
175> VERIFY BOOLEANP-OF-<
;; Reading from Proofs/utilities/thm-booleanp-of-_lt_.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.07 seconds
176> VERIFY IRREFLEXIVITY-OF-<
;; Reading from Proofs/utilities/thm-irreflexivity-of-_lt_.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 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.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.06 seconds
179> VERIFY LESS-WHEN-ZP-RIGHT-CHEAP
;; Reading from Proofs/utilities/thm-less-when-zp-right-cheap.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.12 seconds
180> VERIFY LESS-OF-ZERO-LEFT
;; Reading from Proofs/utilities/thm-less-of-zero-left.proof
;; Reading the file took 0.12 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.19 seconds
181> VERIFY LESS-COMPLETION-LEFT
;; Reading from Proofs/utilities/thm-less-completion-left.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.10 seconds
182> VERIFY LESS-WHEN-ZP-LEFT-CHEAP
;; Reading from Proofs/utilities/thm-less-when-zp-left-cheap.proof
;; Reading the file took 0.19 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.26 seconds
183> VERIFY LESS-OF-NFIX-LEFT
;; Reading from Proofs/utilities/thm-less-of-nfix-left.proof
;; Reading the file took 0.11 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.16 seconds
184> VERIFY LESS-OF-NFIX-RIGHT
;; Reading from Proofs/utilities/thm-less-of-nfix-right.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.06 seconds
185> VERIFY TRANSITIVITY-OF-<
;; Reading from Proofs/utilities/thm-transitivity-of-_lt_.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 seconds
186> VERIFY ANTISYMMETRY-OF-<
;; Reading from Proofs/utilities/thm-antisymmetry-of-_lt_.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.11 seconds
187> VERIFY TRICHOTOMY-OF-<
;; Reading from Proofs/utilities/thm-trichotomy-of-_lt_.proof
;; Reading the file took 0.31 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.55 seconds
188> VERIFY ONE-PLUS-TRICK
;; Reading from Proofs/utilities/thm-one-plus-trick.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.05 seconds
189> VERIFY LESS-OF-ONE-RIGHT
;; Reading from Proofs/utilities/thm-less-of-one-right.proof
;; Reading the file took 0.15 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.21 seconds
190> VERIFY LESS-OF-ONE-LEFT
;; Reading from Proofs/utilities/thm-less-of-one-left.proof
;; Reading the file took 0.21 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.31 seconds
191> VERIFY TRANSITIVITY-OF-<-TWO
;; Reading from Proofs/utilities/thm-transitivity-of-_lt_-two.proof
;; Reading the file took 1.79 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 2.37 seconds
192> VERIFY TRANSITIVITY-OF-<-THREE
;; Reading from Proofs/utilities/thm-transitivity-of-_lt_-three.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.08 seconds
193> VERIFY TRANSITIVITY-OF-<-FOUR
;; Reading from Proofs/utilities/thm-transitivity-of-_lt_-four.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 seconds
194> VERIFY (< (+ a b) (+ a c))
;; Reading from Proofs/utilities/thm-_lp__lt__sp__lp_+_sp_a_sp_b_rp__sp__lp_+_sp_a_sp_c_rp__rp_.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.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.00 seconds
;; VERIFY took 0.04 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.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 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.01 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.02 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.00 seconds
;; VERIFY took 0.01 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.02 seconds
;; Checking the proof took 0.00 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.02 seconds
;; Checking the proof took 0.00 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.00 seconds
;; VERIFY took 0.02 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.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 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.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 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.02 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.02 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.08 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.11 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.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.07 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.09 seconds
;; Checking the proof took 0.01 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.06 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.09 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.09 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.19 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.04 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.06 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.08 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.15 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.06 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.08 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.10 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.20 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.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.08 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.20 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.30 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.05 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.28 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.60 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.92 seconds
;; Checking the proof took 0.25 seconds
;; VERIFY took 2.79 seconds
226> VERIFY (= (+ a b) (+ c a))
;; Reading from Proofs/utilities/thm-_lp__eq__sp__lp_+_sp_a_sp_b_rp__sp__lp_+_sp_c_sp_a_rp__rp_.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.02 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.02 seconds
229> VERIFY (= 0 (+ a b))
;; Reading from Proofs/utilities/thm-_lp__eq__sp_0_sp__lp_+_sp_a_sp_b_rp__rp_.proof
;; Reading the file took 0.19 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.29 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.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.08 seconds
231> VERIFY (= (+ a x b) (+ c x d))
;; Reading from Proofs/utilities/thm-_lp__eq__sp__lp_+_sp_a_sp_x_sp_b_rp__sp__lp_+_sp_c_sp_x_sp_d_rp__rp_.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
232> VERIFY SQUEEZE-LAW-ONE
;; Reading from Proofs/utilities/thm-squeeze-law-one.proof
;; Reading the file took 1.74 seconds
;; Checking the proof took 0.18 seconds
;; VERIFY took 2.36 seconds
233> VERIFY SQUEEZE-LAW-TWO
;; Reading from Proofs/utilities/thm-squeeze-law-two.proof
;; Reading the file took 0.31 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.50 seconds
234> VERIFY SQUEEZE-LAW-THREE
;; Reading from Proofs/utilities/thm-squeeze-law-three.proof
;; Reading the file took 0.30 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.51 seconds
235> VERIFY NATP-OF-MINUS
;; Reading from Proofs/utilities/thm-natp-of-minus.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
236> VERIFY MINUS-UNDER-IFF
;; Reading from Proofs/utilities/thm-minus-under-iff.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.00 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.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.07 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.02 seconds
239> VERIFY MINUS-OF-ZERO-LEFT
;; Reading from Proofs/utilities/thm-minus-of-zero-left.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
240> VERIFY MINUS-CANCELS-SUMMAND-RIGHT
;; Reading from Proofs/utilities/thm-minus-cancels-summand-right.proof
;; Reading the file took 0.10 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.16 seconds
241> VERIFY MINUS-OF-ZERO-RIGHT
;; Reading from Proofs/utilities/thm-minus-of-zero-right.proof
;; Reading the file took 0.11 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.15 seconds
242> VERIFY MINUS-CANCELS-SUMMAND-LEFT
;; Reading from Proofs/utilities/thm-minus-cancels-summand-left.proof
;; Reading the file took 0.02 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.23 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.39 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.08 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.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.07 seconds
247> VERIFY (- a (- b c))
;; Reading from Proofs/utilities/thm-_lp_-_sp_a_sp__lp_-_sp_b_sp_c_rp__rp_.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.08 seconds
248> VERIFY (- (- a b) c)
;; Reading from Proofs/utilities/thm-_lp_-_sp__lp_-_sp_a_sp_b_rp__sp_c_rp_.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
249> VERIFY (= (- a b) c)
;; Reading from Proofs/utilities/thm-_lp__eq__sp__lp_-_sp_a_sp_b_rp__sp_c_rp_.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.11 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.03 seconds
;; VERIFY took 0.24 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.07 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.10 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.01 seconds
;; VERIFY took 0.06 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.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.07 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.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.07 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.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.07 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.15 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.22 seconds
257> VERIFY MINUS-WHEN-ZP-LEFT-CHEAP
;; Reading from Proofs/utilities/thm-minus-when-zp-left-cheap.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.00 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.07 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.09 seconds
259> VERIFY MINUS-OF-NFIX-LEFT
;; Reading from Proofs/utilities/thm-minus-of-nfix-left.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.07 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.01 seconds
;; VERIFY took 0.07 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.04 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
262> VERIFY GATHER-CONSTANTS-FROM-LESS-OF-PLUS-TWO
;; Reading from Proofs/utilities/thm-gather-constants-from-less-of-plus-two.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.08 seconds
263> VERIFY GATHER-CONSTANTS-FROM-LESS-OF-PLUS-AND-PLUS
;; Reading from Proofs/utilities/thm-gather-constants-from-less-of-plus-and-plus.proof
;; Reading the file took 0.17 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.30 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.14 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.23 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.19 seconds
;; Checking the proof took 1.00 seconds
;; VERIFY took 7.77 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.30 seconds
;; Checking the proof took 0.14 seconds
;; VERIFY took 0.77 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 1.33 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 1.88 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.06 seconds
;; VERIFY took 0.39 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.09 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.15 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 1.99 seconds
;; Checking the proof took 0.33 seconds
;; VERIFY took 3.04 seconds
271> VERIFY NOT-EQUAL-WHEN-LESS
;; Reading from Proofs/utilities/thm-not-equal-when-less.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 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.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 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.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.07 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.02 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.03 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 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.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.07 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.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.07 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.00 seconds
;; VERIFY took 0.03 seconds
279> VERIFY EQUAL-OF-MAX-AND-ZERO
;; Reading from Proofs/utilities/thm-equal-of-max-and-zero.proof
;; Reading the file took 0.14 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.21 seconds
280> VERIFY MAX-OF-ZERO-LEFT
;; Reading from Proofs/utilities/thm-max-of-zero-left.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.00 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.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
282> VERIFY NATP-OF-MIN
;; Reading from Proofs/utilities/thm-natp-of-min.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.05 seconds
283> VERIFY EQUAL-OF-MIN-AND-ZERO
;; Reading from Proofs/utilities/thm-equal-of-min-and-zero.proof
;; Reading the file took 0.18 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.27 seconds
284> VERIFY MIN-OF-ZERO-LEFT
;; Reading from Proofs/utilities/thm-min-of-zero-left.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 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.01 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.01 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.28 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.67 seconds
290> VERIFY ORDP-WHEN-NATP
;; Reading from Proofs/utilities/thm-ordp-when-natp.proof
;; Reading the file took 0.37 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.83 seconds
291> VERIFY NATP-OF-RANK
;; Reading from Proofs/utilities/thm-natp-of-rank.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 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.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 seconds
293> VERIFY RANK-OF-CONS
;; Reading from Proofs/utilities/thm-rank-of-cons.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 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.07 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.12 seconds
295> VERIFY ORDP-OF-RANK
;; Reading from Proofs/utilities/thm-ordp-of-rank.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 seconds
296> VERIFY RANK-OF-CAR
;; Reading from Proofs/utilities/thm-rank-of-car.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.13 seconds
297> VERIFY RANK-OF-CAR-WEAK
;; Reading from Proofs/utilities/thm-rank-of-car-weak.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.10 seconds
298> VERIFY RANK-OF-CDR
;; Reading from Proofs/utilities/thm-rank-of-cdr.proof
;; Reading the file took 0.09 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.13 seconds
299> VERIFY RANK-OF-CDR-WEAK
;; Reading from Proofs/utilities/thm-rank-of-cdr-weak.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.09 seconds
300> VERIFY RANK-OF-SECOND
;; Reading from Proofs/utilities/thm-rank-of-second.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.10 seconds
301> VERIFY RANK-OF-SECOND-WEAK
;; Reading from Proofs/utilities/thm-rank-of-second-weak.proof
;; Reading the file took 0.11 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.22 seconds
302> VERIFY RANK-OF-THIRD
;; Reading from Proofs/utilities/thm-rank-of-third.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.10 seconds
303> VERIFY RANK-OF-THIRD-WEAK
;; Reading from Proofs/utilities/thm-rank-of-third-weak.proof
;; Reading the file took 0.12 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.23 seconds
304> VERIFY RANK-OF-FOURTH
;; Reading from Proofs/utilities/thm-rank-of-fourth.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.12 seconds
305> VERIFY RANK-OF-FOURTH-WEAK
;; Reading from Proofs/utilities/thm-rank-of-fourth-weak.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.18 seconds
306> VERIFY BOOLEANP-OF-ORD<
;; Reading from Proofs/utilities/thm-booleanp-of-ord_lt_.proof
;; Reading the file took 0.30 seconds
;; Checking the proof took 0.14 seconds
;; VERIFY took 0.74 seconds
307> VERIFY BOOLEANP-OF-ORDP
;; Reading from Proofs/utilities/thm-booleanp-of-ordp.proof
;; Reading the file took 1.19 seconds
;; Checking the proof took 0.25 seconds
;; VERIFY took 2.06 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
;; DEFINE took 0.00 seconds
309> VERIFY TWO-NATS-MEASURE
;; Reading from Proofs/utilities/thm-two-nats-measure.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
310> VERIFY ORDP-OF-TWO-NATS-MEASURE
;; Reading from Proofs/utilities/thm-ordp-of-two-nats-measure.proof
;; Reading the file took 0.15 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.24 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.21 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.43 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
;; DEFINE took 0.00 seconds
313> VERIFY THREE-NATS-MEASURE
;; Reading from Proofs/utilities/thm-three-nats-measure.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
314> VERIFY ORDP-OF-THREE-NATS-MEASURE
;; Reading from Proofs/utilities/thm-ordp-of-three-nats-measure.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.45 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.50 seconds
;; Checking the proof took 0.31 seconds
;; VERIFY took 1.28 seconds
316> DEFINE LEN
;; Reading from Proofs/utilities/admit-len.proofs
;; Reading the file took 0.05 seconds
;; Checking the proofs took 0.01 seconds
;; DEFINE took 0.07 seconds
317> VERIFY LEN
;; Reading from Proofs/utilities/thm-len.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
318> VERIFY LEN-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-len-when-not-consp.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.00 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.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 seconds
320> VERIFY NATP-OF-LEN
;; Reading from Proofs/utilities/thm-natp-of-len.proof
;; Reading the file took 0.17 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.28 seconds
321> VERIFY NATP-OF-LEN-FREE
;; Reading from Proofs/utilities/thm-natp-of-len-free.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 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.04 seconds
;; Checking the proof took 0.00 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.06 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.09 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.21 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.35 seconds
325> VERIFY DECREMENT-LEN-WHEN-CONSP
;; Reading from Proofs/utilities/thm-decrement-len-when-consp.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.11 seconds
326> VERIFY EQUAL-OF-LEN-AND-ZERO
;; Reading from Proofs/utilities/thm-equal-of-len-and-zero.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.07 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.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.09 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.13 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.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 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.12 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.18 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.20 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.31 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.05 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.06 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.01 seconds
;; VERIFY took 0.10 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.10 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.15 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.10 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.15 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.14 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.22 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.19 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.29 seconds
338> VERIFY EQUAL-WHEN-LENGTH-DIFFERENT
;; Reading from Proofs/utilities/thm-equal-when-length-different.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
339> VERIFY EQUAL-OF-2-AND-LEN
;; Reading from Proofs/utilities/thm-equal-of-2-and-len.proof
;; Reading the file took 0.17 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.29 seconds
340> VERIFY EQUAL-OF-3-AND-LEN
;; Reading from Proofs/utilities/thm-equal-of-3-and-len.proof
;; Reading the file took 0.26 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.47 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.04 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.06 seconds
342> DEFINE FAST-LEN
;; Reading from Proofs/utilities/admit-fast-len.proofs
;; Reading the file took 0.04 seconds
;; Checking the proofs took 0.01 seconds
;; DEFINE took 0.06 seconds
343> VERIFY FAST-LEN
;; Reading from Proofs/utilities/thm-fast-len.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 seconds
344> VERIFY FAST-LEN-REMOVAL
;; Reading from Proofs/utilities/thm-fast-len-removal.proof
;; Reading the file took 0.28 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.54 seconds
345> DEFINE SAME-LENGTHP
;; Reading from Proofs/utilities/admit-same-lengthp.proofs
;; Reading the file took 0.05 seconds
;; Checking the proofs took 0.01 seconds
;; DEFINE took 0.08 seconds
346> VERIFY SAME-LENGTHP
;; Reading from Proofs/utilities/thm-same-lengthp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.12 seconds
;; VERIFY took 0.67 seconds
348> DEFINE TRUE-LISTP
;; Reading from Proofs/utilities/admit-true-listp.proofs
;; Reading the file took 0.06 seconds
;; Checking the proofs took 0.01 seconds
;; DEFINE took 0.08 seconds
349> VERIFY TRUE-LISTP
;; Reading from Proofs/utilities/thm-true-listp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
350> VERIFY TRUE-LISTP-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-true-listp-when-not-consp.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
351> VERIFY TRUE-LISTP-OF-CONS
;; Reading from Proofs/utilities/thm-true-listp-of-cons.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
352> VERIFY BOOLEANP-OF-TRUE-LISTP
;; Reading from Proofs/utilities/thm-booleanp-of-true-listp.proof
;; Reading the file took 0.20 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.31 seconds
353> VERIFY TRUE-LISTP-OF-CDR
;; Reading from Proofs/utilities/thm-true-listp-of-cdr.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.08 seconds
354> VERIFY CONSP-WHEN-TRUE-LISTP-CHEAP
;; Reading from Proofs/utilities/thm-consp-when-true-listp-cheap.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.11 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.22 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.37 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.33 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.60 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.15 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.23 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.43 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.56 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.29 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.47 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.07 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.10 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.19 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.30 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.33 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.52 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.06 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.09 seconds
364> DEFINE LIST-FIX
;; Reading from Proofs/utilities/admit-list-fix.proofs
;; Reading the file took 0.05 seconds
;; Checking the proofs took 0.01 seconds
;; DEFINE took 0.07 seconds
365> VERIFY LIST-FIX
;; Reading from Proofs/utilities/thm-list-fix.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
366> VERIFY LIST-FIX-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-list-fix-when-not-consp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 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.02 seconds
;; Checking the proof took 0.00 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.05 seconds
;; Checking the proof took 0.01 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.05 seconds
;; Checking the proof took 0.01 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.08 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.10 seconds
371> VERIFY LIST-FIX-UNDER-IFF
;; Reading from Proofs/utilities/thm-list-fix-under-iff.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.06 seconds
372> VERIFY LEN-OF-LIST-FIX
;; Reading from Proofs/utilities/thm-len-of-list-fix.proof
;; Reading the file took 0.17 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.30 seconds
373> VERIFY TRUE-LISTP-OF-LIST-FIX
;; Reading from Proofs/utilities/thm-true-listp-of-list-fix.proof
;; Reading the file took 0.18 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.29 seconds
374> VERIFY LIST-FIX-WHEN-TRUE-LISTP
;; Reading from Proofs/utilities/thm-list-fix-when-true-listp.proof
;; Reading the file took 0.27 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.49 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.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 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.09 seconds
;; VERIFY took 0.56 seconds
377> DEFINE MEMBERP
;; Reading from Proofs/utilities/admit-memberp.proofs
;; Reading the file took 0.06 seconds
;; Checking the proofs took 0.01 seconds
;; DEFINE took 0.09 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.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 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.01 seconds
;; VERIFY took 0.07 seconds
381> VERIFY BOOLEANP-OF-MEMBERP
;; Reading from Proofs/utilities/thm-booleanp-of-memberp.proof
;; Reading the file took 0.20 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.33 seconds
382> VERIFY MEMBERP-OF-LIST-FIX
;; Reading from Proofs/utilities/thm-memberp-of-list-fix.proof
;; Reading the file took 0.44 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.86 seconds
383> VERIFY MEMBERP-WHEN-MEMBERP-OF-CDR
;; Reading from Proofs/utilities/thm-memberp-when-memberp-of-cdr.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.09 seconds
384> VERIFY MEMBERP-OF-CAR
;; Reading from Proofs/utilities/thm-memberp-of-car.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.08 seconds
385> VERIFY MEMBERP-OF-SECOND
;; Reading from Proofs/utilities/thm-memberp-of-second.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.06 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.10 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.15 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.09 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.14 seconds
388> VERIFY CONSP-WHEN-MEMBERP-CHEAP
;; Reading from Proofs/utilities/thm-consp-when-memberp-cheap.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.09 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.08 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.11 seconds
390> VERIFY RANK-WHEN-MEMBERP
;; Reading from Proofs/utilities/thm-rank-when-memberp.proof
;; Reading the file took 0.29 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.56 seconds
391> VERIFY RANK-WHEN-MEMBERP-WEAK
;; Reading from Proofs/utilities/thm-rank-when-memberp-weak.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.38 seconds
392> DEFINE SUBSETP
;; Reading from Proofs/utilities/admit-subsetp.proofs
;; Reading the file took 0.08 seconds
;; Checking the proofs took 0.01 seconds
;; DEFINE took 0.11 seconds
393> VERIFY SUBSETP
;; Reading from Proofs/utilities/thm-subsetp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
394> VERIFY SUBSETP-WHEN-NOT-CONSP
;; Reading from Proofs/utilities/thm-subsetp-when-not-consp.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
395> VERIFY SUBSETP-OF-CONS
;; Reading from Proofs/utilities/thm-subsetp-of-cons.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.01 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.19 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.31 seconds
397> VERIFY SUBSETP-WHEN-NOT-CONSP-TWO
;; Reading from Proofs/utilities/thm-subsetp-when-not-consp-two.proof
;; Reading the file took 0.32 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.61 seconds
398> VERIFY SUBSETP-OF-CONS-TWO
;; Reading from Proofs/utilities/thm-subsetp-of-cons-two.proof
;; Reading the file took 0.32 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.60 seconds
399> VERIFY SUBSETP-OF-LIST-FIX-ONE
;; Reading from Proofs/utilities/thm-subsetp-of-list-fix-one.proof
;; Reading the file took 0.74 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 1.15 seconds
400> VERIFY SUBSETP-OF-LIST-FIX-TWO
;; Reading from Proofs/utilities/thm-subsetp-of-list-fix-two.proof
;; Reading the file took 0.43 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.85 seconds
401> VERIFY SUBSETP-OF-CDR
;; Reading from Proofs/utilities/thm-subsetp-of-cdr.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.10 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.34 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.64 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.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 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.03 seconds
;; Checking the proof took 0.00 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.03 seconds
;; Checking the proof took 0.00 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.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.08 seconds
407> VERIFY SUBSETP-REFLEXIVE
;; Reading from Proofs/utilities/thm-subsetp-reflexive.proof
;; Reading the file took 0.18 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.30 seconds
408> VERIFY SUBSETP-TRANSITIVE-ONE
;; Reading from Proofs/utilities/thm-subsetp-transitive-one.proof
;; Reading the file took 0.33 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.64 seconds
409> VERIFY SUBSETP-TRANSITIVE-TWO
;; Reading from Proofs/utilities/thm-subsetp-transitive-two.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.05 seconds
410> DEFINE SUBSETP-BADGUY
;; Reading from Proofs/utilities/admit-subsetp-badguy.proofs
;; Reading the file took 0.05 seconds
;; Checking the proofs took 0.01 seconds
;; DEFINE took 0.09 seconds
411> VERIFY SUBSETP-BADGUY
;; Reading from Proofs/utilities/thm-subsetp-badguy.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
412> VERIFY SUBSETP-BADGUY-MEMBERSHIP-PROPERTY
;; Reading from Proofs/utilities/thm-subsetp-badguy-membership-property.proof
;; Reading the file took 2.03 seconds
;; Checking the proof took 0.73 seconds
;; VERIFY took 4.44 seconds
413> VERIFY SUBSETP-BADGUY-UNDER-IFF
;; Reading from Proofs/utilities/thm-subsetp-badguy-under-iff.proof
;; Reading the file took 0.21 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.49 seconds
414> VERIFY EQUAL-OF-CDR-AND-SELF
;; Reading from Proofs/utilities/thm-equal-of-cdr-and-self.proof
;; Reading the file took 0.17 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.31 seconds
415> DEFINE APP
;; Reading from Proofs/utilities/admit-app.proofs
;; Reading the file took 0.05 seconds
;; Checking the proofs took 0.01 seconds
;; DEFINE took 0.07 seconds
416> VERIFY APP
;; Reading from Proofs/utilities/thm-app.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.04 seconds
418> VERIFY APP-OF-CONS
;; Reading from Proofs/utilities/thm-app-of-cons.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
419> VERIFY APP-OF-LIST-FIX-ONE
;; Reading from Proofs/utilities/thm-app-of-list-fix-one.proof
;; Reading the file took 0.17 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.30 seconds
420> VERIFY APP-OF-LIST-FIX-TWO
;; Reading from Proofs/utilities/thm-app-of-list-fix-two.proof
;; Reading the file took 0.16 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.28 seconds
421> VERIFY APP-WHEN-NOT-CONSP-TWO
;; Reading from Proofs/utilities/thm-app-when-not-consp-two.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.40 seconds
422> VERIFY APP-OF-SINGLETON-LIST-CHEAP
;; Reading from Proofs/utilities/thm-app-of-singleton-list-cheap.proof
;; Reading the file took 0.16 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.30 seconds
423> VERIFY TRUE-LISTP-OF-APP
;; Reading from Proofs/utilities/thm-true-listp-of-app.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.34 seconds
424> VERIFY APP-OF-APP
;; Reading from Proofs/utilities/thm-app-of-app.proof
;; Reading the file took 0.18 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.31 seconds
425> VERIFY MEMBERP-OF-APP
;; Reading from Proofs/utilities/thm-memberp-of-app.proof
;; Reading the file took 1.58 seconds
;; Checking the proof took 0.27 seconds
;; VERIFY took 2.42 seconds
426> VERIFY CONSP-OF-APP
;; Reading from Proofs/utilities/thm-consp-of-app.proof
;; Reading the file took 0.12 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.17 seconds
427> VERIFY APP-UNDER-IFF
;; Reading from Proofs/utilities/thm-app-under-iff.proof
;; Reading the file took 0.09 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.14 seconds
428> VERIFY LEN-OF-APP
;; Reading from Proofs/utilities/thm-len-of-app.proof
;; Reading the file took 0.19 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.34 seconds
429> VERIFY SUBSETP-OF-APP-ONE
;; Reading from Proofs/utilities/thm-subsetp-of-app-one.proof
;; Reading the file took 1.43 seconds
;; Checking the proof took 0.22 seconds
;; VERIFY took 2.15 seconds
430> VERIFY SUBSETP-OF-APP-TWO
;; Reading from Proofs/utilities/thm-subsetp-of-app-two.proof
;; Reading the file took 0.16 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.33 seconds
431> VERIFY SUBSETP-OF-APP-THREE
;; Reading from Proofs/utilities/thm-subsetp-of-app-three.proof
;; Reading the file took 0.18 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.38 seconds
432> VERIFY SUBSETP-OF-APP-WHEN-SUBSETS
;; Reading from Proofs/utilities/thm-subsetp-of-app-when-subsets.proof
;; Reading the file took 1.90 seconds
;; Checking the proof took 0.40 seconds
;; VERIFY took 3.52 seconds
433> VERIFY SUBSETP-OF-SYMMETRIC-APPS
;; Reading from Proofs/utilities/thm-subsetp-of-symmetric-apps.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.12 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.18 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.32 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.21 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.39 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.04 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 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.03 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
438> VERIFY MEMBERP-OF-APP-ONTO-SIN

;;; Starting full GC,     547,356,672 bytes allocated.