i i i i i i i ooooo o ooooooo ooooo ooooo
I I I I I I I 8 8 8 8 8 o 8 8
I \ `+' / I 8 8 8 8 8 8
\ `-+-' / 8 8 8 ooooo 8oooo
`-__|__-' 8 8 8 8 8
| 8 o 8 8 o 8 8
------+------ ooooo 8oooooo ooo8ooo ooooo 8
Welcome to GNU CLISP 2.47 (2008-10-23)
Copyright (c) Bruno Haible, Michael Stoll 1992, 1993
Copyright (c) Bruno Haible, Marcus Daniels 1994-1997
Copyright (c) Bruno Haible, Pierpaolo Bernardi, Sam Steingold 1998
Copyright (c) Bruno Haible, Sam Steingold 1999-2000
Copyright (c) Sam Steingold, Bruno Haible 2001-2008
Type :h and hit Enter for context help.
Milawa Proof Checker.
13520> DEFINE FOUR-NATS-MEASURE
;; Reading from Proofs/level10/admit-four-nats-measure.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
13521> VERIFY FOUR-NATS-MEASURE
;; Reading from Proofs/level10/thm-four-nats-measure.proof
;; Reading the file took 0.18 seconds
;; Checking the proof took 3.40 seconds
;; VERIFY took 3.60 seconds
13522> VERIFY ORDP-OF-FOUR-NATS-MEASURE
;; Reading from Proofs/level10/thm-ordp-of-four-nats-measure.proof
;; Reading the file took 1.72 seconds
;; Checking the proof took 34.40 seconds
;; VERIFY took 36.13 seconds
13523> VERIFY ORD<-OF-FOUR-NATS-MEASURE
;; Reading from Proofs/level10/thm-ord_lt_-of-four-nats-measure.proof
;; Reading the file took 1.42 seconds
;; Checking the proof took 37.53 seconds
;; VERIFY took 38.98 seconds
13524> DEFINE RW.CRESULT
;; Reading from Proofs/level10/admit-rw.cresult.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13525> VERIFY RW.CRESULT
;; Reading from Proofs/level10/thm-rw.cresult.proof
;; Reading the file took 0.23 seconds
;; Checking the proof took 3.34 seconds
;; VERIFY took 3.58 seconds
13526> DEFINE RW.CRESULT->DATA
;; Reading from Proofs/level10/admit-rw.cresult-_gt_data.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13527> VERIFY RW.CRESULT->DATA
;; Reading from Proofs/level10/thm-rw.cresult-_gt_data.proof
;; Reading the file took 0.23 seconds
;; Checking the proof took 3.35 seconds
;; VERIFY took 3.59 seconds
13528> DEFINE RW.CRESULT->CACHE
;; Reading from Proofs/level10/admit-rw.cresult-_gt_cache.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13529> VERIFY RW.CRESULT->CACHE
;; Reading from Proofs/level10/thm-rw.cresult-_gt_cache.proof
;; Reading the file took 0.23 seconds
;; Checking the proof took 3.35 seconds
;; VERIFY took 3.59 seconds
13530> DEFINE RW.CRESULT->ALIMITEDP
;; Reading from Proofs/level10/admit-rw.cresult-_gt_alimitedp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13531> VERIFY RW.CRESULT->ALIMITEDP
;; Reading from Proofs/level10/thm-rw.cresult-_gt_alimitedp.proof
;; Reading the file took 0.19 seconds
;; Checking the proof took 3.36 seconds
;; VERIFY took 3.56 seconds
13532> VERIFY RW.CRESULT-UNDER-IFF
;; Reading from Proofs/level10/thm-rw.cresult-under-iff.proof
;; Reading the file took 1.47 seconds
;; Checking the proof took 18.47 seconds
;; VERIFY took 19.95 seconds
13533> VERIFY RW.CRESULT->DATA-OF-RW.CRESULT
;; Reading from Proofs/level10/thm-rw.cresult-_gt_data-of-rw.cresult.proof
;; Reading the file took 1.61 seconds
;; Checking the proof took 18.85 seconds
;; VERIFY took 20.46 seconds
13534> VERIFY RW.CRESULT->CACHE-OF-RW.CRESULT
;; Reading from Proofs/level10/thm-rw.cresult-_gt_cache-of-rw.cresult.proof
;; Reading the file took 1.66 seconds
;; Checking the proof took 19.13 seconds
;; VERIFY took 20.80 seconds
13535> VERIFY RW.CRESULT->ALIMITEDP-OF-RW.CRESULT
;; Reading from Proofs/level10/thm-rw.cresult-_gt_alimitedp-of-rw.cresult.proof
;; Reading the file took 1.42 seconds
;; Checking the proof took 18.84 seconds
;; VERIFY took 20.27 seconds
13536> DEFINE RW.HYPRESULT
;; Reading from Proofs/level10/admit-rw.hypresult.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13537> VERIFY RW.HYPRESULT
;; Reading from Proofs/level10/thm-rw.hypresult.proof
;; Reading the file took 0.50 seconds
;; Checking the proof took 3.38 seconds
;; VERIFY took 3.89 seconds
13538> DEFINE RW.HYPRESULT->SUCCESSP
;; Reading from Proofs/level10/admit-rw.hypresult-_gt_successp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13539> VERIFY RW.HYPRESULT->SUCCESSP
;; Reading from Proofs/level10/thm-rw.hypresult-_gt_successp.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.40 seconds
;; VERIFY took 3.63 seconds
13540> DEFINE RW.HYPRESULT->TRACES
;; Reading from Proofs/level10/admit-rw.hypresult-_gt_traces.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13541> VERIFY RW.HYPRESULT->TRACES
;; Reading from Proofs/level10/thm-rw.hypresult-_gt_traces.proof
;; Reading the file took 0.25 seconds
;; Checking the proof took 3.40 seconds
;; VERIFY took 3.67 seconds
13542> DEFINE RW.HYPRESULT->CACHE
;; Reading from Proofs/level10/admit-rw.hypresult-_gt_cache.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13543> VERIFY RW.HYPRESULT->CACHE
;; Reading from Proofs/level10/thm-rw.hypresult-_gt_cache.proof
;; Reading the file took 0.21 seconds
;; Checking the proof took 3.38 seconds
;; VERIFY took 3.60 seconds
13544> DEFINE RW.HYPRESULT->ALIMITEDP
;; Reading from Proofs/level10/admit-rw.hypresult-_gt_alimitedp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13545> VERIFY RW.HYPRESULT->ALIMITEDP
;; Reading from Proofs/level10/thm-rw.hypresult-_gt_alimitedp.proof
;; Reading the file took 0.25 seconds
;; Checking the proof took 3.40 seconds
;; VERIFY took 3.66 seconds
13546> VERIFY RW.HYPRESULT-UNDER-IFF
;; Reading from Proofs/level10/thm-rw.hypresult-under-iff.proof
;; Reading the file took 1.63 seconds
;; Checking the proof took 18.84 seconds
;; VERIFY took 20.48 seconds
13547> VERIFY RW.HYPRESULT->SUCCESSP-OF-RW.HYPRESULT
;; Reading from Proofs/level10/thm-rw.hypresult-_gt_successp-of-rw.hypresult.proof
;; Reading the file took 1.62 seconds
;; Checking the proof took 19.14 seconds
;; VERIFY took 20.77 seconds
13548> VERIFY RW.HYPRESULT->TRACES-OF-RW.HYPRESULT
;; Reading from Proofs/level10/thm-rw.hypresult-_gt_traces-of-rw.hypresult.proof
;; Reading the file took 1.44 seconds
;; Checking the proof took 18.90 seconds
;; VERIFY took 20.35 seconds
13549> VERIFY RW.HYPRESULT->CACHE-OF-RW.HYPRESULT
;; Reading from Proofs/level10/thm-rw.hypresult-_gt_cache-of-rw.hypresult.proof
;; Reading the file took 1.64 seconds
;; Checking the proof took 19.13 seconds
;; VERIFY took 20.79 seconds
13550> VERIFY RW.HYPRESULT->ALIMITEDP-OF-RW.HYPRESULT
;; Reading from Proofs/level10/thm-rw.hypresult-_gt_alimitedp-of-rw.hypresult.proof
;; Reading the file took 1.42 seconds
;; Checking the proof took 18.89 seconds
;; VERIFY took 20.32 seconds
13551> DEFINE RW.FLAG-CREWRITE
;; Reading from Proofs/level10/admit-rw.flag-crewrite.proofs
;; Reading the file took 2.62 seconds
;; Checking the proofs took 746.29 seconds
;; DEFINE took 837.63 seconds
13552> VERIFY RW.FLAG-CREWRITE
;; Reading from Proofs/level10/thm-rw.flag-crewrite.proof
;; Reading the file took 0.25 seconds
;; Checking the proof took 3.64 seconds
;; VERIFY took 4.14 seconds
13553> VERIFY RW.FLAG-CREWRITE-OF-TERM-REDUCTION
;; Reading from Proofs/level10/thm-rw.flag-crewrite-of-term-reduction.proof
;; Reading the file took 1.55 seconds
;; Checking the proof took 26.71 seconds
;; VERIFY took 28.27 seconds
13554> VERIFY RW.FLAG-CREWRITE-OF-LIST-REDUCTION
;; Reading from Proofs/level10/thm-rw.flag-crewrite-of-list-reduction.proof
;; Reading the file took 1.52 seconds
;; Checking the proof took 26.67 seconds
;; VERIFY took 28.21 seconds
13555> VERIFY RW.FLAG-CREWRITE-OF-RULE-REDUCTION
;; Reading from Proofs/level10/thm-rw.flag-crewrite-of-rule-reduction.proof
;; Reading the file took 1.48 seconds
;; Checking the proof took 26.64 seconds
;; VERIFY took 28.14 seconds
13556> VERIFY RW.FLAG-CREWRITE-OF-RULES-REDUCTION
;; Reading from Proofs/level10/thm-rw.flag-crewrite-of-rules-reduction.proof
;; Reading the file took 1.48 seconds
;; Checking the proof took 26.67 seconds
;; VERIFY took 28.15 seconds
13557> VERIFY RW.FLAG-CREWRITE-OF-HYP-REDUCTION
;; Reading from Proofs/level10/thm-rw.flag-crewrite-of-hyp-reduction.proof
;; Reading the file took 1.49 seconds
;; Checking the proof took 26.67 seconds
;; VERIFY took 28.17 seconds
13558> VERIFY RW.FLAG-CREWRITE-OF-HYPS-REDUCTION
;; Reading from Proofs/level10/thm-rw.flag-crewrite-of-hyps-reduction.proof
;; Reading the file took 1.47 seconds
;; Checking the proof took 26.35 seconds
;; VERIFY took 27.84 seconds
13559> DEFINE RW.CREWRITE-CORE
;; Reading from Proofs/level10/admit-rw.crewrite-core.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13560> VERIFY RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-rw.crewrite-core.proof
;; Reading the file took 0.24 seconds
;; Checking the proof took 3.40 seconds
;; VERIFY took 3.65 seconds
13561> DEFINE RW.CREWRITE-CORE-LIST
;; Reading from Proofs/level10/admit-rw.crewrite-core-list.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
13562> VERIFY RW.CREWRITE-CORE-LIST
;; Reading from Proofs/level10/thm-rw.crewrite-core-list.proof
;; Reading the file took 0.24 seconds
;; Checking the proof took 3.39 seconds
;; VERIFY took 3.64 seconds
13563> DEFINE RW.CREWRITE-TRY-RULE
;; Reading from Proofs/level10/admit-rw.crewrite-try-rule.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13564> VERIFY RW.CREWRITE-TRY-RULE
;; Reading from Proofs/level10/thm-rw.crewrite-try-rule.proof
;; Reading the file took 0.25 seconds
;; Checking the proof took 3.42 seconds
;; VERIFY took 3.68 seconds
13565> DEFINE RW.CREWRITE-TRY-RULES
;; Reading from Proofs/level10/admit-rw.crewrite-try-rules.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
13566> VERIFY RW.CREWRITE-TRY-RULES
;; Reading from Proofs/level10/thm-rw.crewrite-try-rules.proof
;; Reading the file took 0.19 seconds
;; Checking the proof took 3.40 seconds
;; VERIFY took 3.61 seconds
13567> DEFINE RW.CREWRITE-TRY-MATCH
;; Reading from Proofs/level10/admit-rw.crewrite-try-match.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13568> VERIFY RW.CREWRITE-TRY-MATCH
;; Reading from Proofs/level10/thm-rw.crewrite-try-match.proof
;; Reading the file took 0.24 seconds
;; Checking the proof took 3.40 seconds
;; VERIFY took 3.65 seconds
13569> DEFINE RW.CREWRITE-TRY-MATCHES
;; Reading from Proofs/level10/admit-rw.crewrite-try-matches.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13570> VERIFY RW.CREWRITE-TRY-MATCHES
;; Reading from Proofs/level10/thm-rw.crewrite-try-matches.proof
;; Reading the file took 0.28 seconds
;; Checking the proof took 3.41 seconds
;; VERIFY took 3.70 seconds
13571> DEFINE RW.CREWRITE-RELIEVE-HYP
;; Reading from Proofs/level10/admit-rw.crewrite-relieve-hyp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13572> VERIFY RW.CREWRITE-RELIEVE-HYP
;; Reading from Proofs/level10/thm-rw.crewrite-relieve-hyp.proof
;; Reading the file took 0.25 seconds
;; Checking the proof took 3.40 seconds
;; VERIFY took 3.66 seconds
13573> DEFINE RW.CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/admit-rw.crewrite-relieve-hyps.proofs
;; Reading the file took 0.03 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.04 seconds
13574> VERIFY RW.CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-rw.crewrite-relieve-hyps.proof
;; Reading the file took 0.23 seconds
;; Checking the proof took 3.43 seconds
;; VERIFY took 3.67 seconds
13575> VERIFY RW.FLAG-CREWRITE-OF-TERM
;; Reading from Proofs/level10/thm-rw.flag-crewrite-of-term.proof
;; Reading the file took 1.48 seconds
;; Checking the proof took 18.84 seconds
;; VERIFY took 20.33 seconds
13576> VERIFY RW.FLAG-CREWRITE-OF-LIST
;; Reading from Proofs/level10/thm-rw.flag-crewrite-of-list.proof
;; Reading the file took 1.60 seconds
;; Checking the proof took 19.08 seconds
;; VERIFY took 20.69 seconds
13577> VERIFY RW.FLAG-CREWRITE-OF-RULE
;; Reading from Proofs/level10/thm-rw.flag-crewrite-of-rule.proof
;; Reading the file took 1.64 seconds
;; Checking the proof took 19.34 seconds
;; VERIFY took 20.99 seconds
13578> VERIFY RW.FLAG-CREWRITE-OF-RULES
;; Reading from Proofs/level10/thm-rw.flag-crewrite-of-rules.proof
;; Reading the file took 1.45 seconds
;; Checking the proof took 19.08 seconds
;; VERIFY took 20.53 seconds
13579> VERIFY RW.FLAG-CREWRITE-OF-MATCH
;; Reading from Proofs/level10/thm-rw.flag-crewrite-of-match.proof
;; Reading the file took 1.66 seconds
;; Checking the proof took 19.30 seconds
;; VERIFY took 20.97 seconds
13580> VERIFY RW.FLAG-CREWRITE-OF-MATCHES
;; Reading from Proofs/level10/thm-rw.flag-crewrite-of-matches.proof
;; Reading the file took 1.51 seconds
;; Checking the proof took 19.04 seconds
;; VERIFY took 20.56 seconds
13581> VERIFY RW.FLAG-CREWRITE-OF-HYP
;; Reading from Proofs/level10/thm-rw.flag-crewrite-of-hyp.proof
;; Reading the file took 1.68 seconds
;; Checking the proof took 19.35 seconds
;; VERIFY took 21.04 seconds
13582> VERIFY RW.FLAG-CREWRITE-OF-HYPS
;; Reading from Proofs/level10/thm-rw.flag-crewrite-of-hyps.proof
;; Reading the file took 1.47 seconds
;; Checking the proof took 19.11 seconds
;; VERIFY took 20.58 seconds
13583> VERIFY EQUAL-WITH-QUOTED-LIST-OF-NIL
;; Reading from Proofs/level10/thm-equal-with-quoted-list-of-nil.proof
;; Reading the file took 1.66 seconds
;; Checking the proof took 19.60 seconds
;; VERIFY took 21.28 seconds
13584> VERIFY DEFINITION-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-definition-of-rw.crewrite-core.proof
;; Reading the file took 3.64 seconds
;; Checking the proof took 523.53 seconds
;; VERIFY took 527.44 seconds
13585> VERIFY DEFINITION-OF-RW.CREWRITE-CORE-LIST
;; Reading from Proofs/level10/thm-definition-of-rw.crewrite-core-list.proof
;; Reading the file took 1.13 seconds
;; Checking the proof took 47.68 seconds
;; VERIFY took 48.83 seconds
13586> VERIFY DEFINITION-OF-RW.CREWRITE-TRY-RULE
;; Reading from Proofs/level10/thm-definition-of-rw.crewrite-try-rule.proof
;; Reading the file took 1.53 seconds
;; Checking the proof took 43.44 seconds
;; VERIFY took 44.98 seconds
13587> VERIFY DEFINITION-OF-RW.CREWRITE-TRY-RULES
;; Reading from Proofs/level10/thm-definition-of-rw.crewrite-try-rules.proof
;; Reading the file took 1.52 seconds
;; Checking the proof took 47.73 seconds
;; VERIFY took 49.27 seconds
13588> VERIFY DEFINITION-OF-RW.CREWRITE-TRY-MATCH
;; Reading from Proofs/level10/thm-definition-of-rw.crewrite-try-match.proof
;; Reading the file took 1.52 seconds
;; Checking the proof took 45.57 seconds
;; VERIFY took 47.11 seconds
13589> VERIFY DEFINITION-OF-RW.CREWRITE-TRY-MATCHES
;; Reading from Proofs/level10/thm-definition-of-rw.crewrite-try-matches.proof
;; Reading the file took 1.55 seconds
;; Checking the proof took 47.79 seconds
;; VERIFY took 49.35 seconds
13590> VERIFY DEFINITION-OF-RW.CREWRITE-RELIEVE-HYP
;; Reading from Proofs/level10/thm-definition-of-rw.crewrite-relieve-hyp.proof
;; Reading the file took 1.58 seconds
;; Checking the proof took 567.54 seconds
;; VERIFY took 569.21 seconds
13591> VERIFY DEFINITION-OF-RW.CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-definition-of-rw.crewrite-relieve-hyps.proof
;; Reading the file took 1.52 seconds
;; Checking the proof took 47.51 seconds
;; VERIFY took 49.04 seconds
13592> VERIFY RW.CREWRITE-CORE-LIST-WHEN-NOT-CONSP
;; Reading from Proofs/level10/thm-rw.crewrite-core-list-when-not-consp.proof
;; Reading the file took 1.50 seconds
;; Checking the proof took 27.06 seconds
;; VERIFY took 28.58 seconds
13593> VERIFY RW.CREWRITE-CORE-LIST-OF-CONS
;; Reading from Proofs/level10/thm-rw.crewrite-core-list-of-cons.proof
;; Reading the file took 1.46 seconds
;; Checking the proof took 26.83 seconds
;; VERIFY took 28.30 seconds
13594> VERIFY TRUE-LISTP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-CORE-LIST
;; Reading from Proofs/level10/thm-true-listp-of-rw.cresult-_gt_data-of-rw.crewrite-core-list.proof
;; Reading the file took 1.50 seconds
;; Checking the proof took 20.10 seconds
;; VERIFY took 21.61 seconds
13595> VERIFY LEN-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-CORE-LIST$
;; Reading from Proofs/level10/thm-len-of-rw.cresult-_gt_data-of-rw.crewrite-core-list$.proof
;; Reading the file took 1.56 seconds
;; Checking the proof took 20.24 seconds
;; VERIFY took 21.80 seconds
13596> VERIFY RW.CREWRITE-TRY-RULES-WHEN-NOT-CONSP
;; Reading from Proofs/level10/thm-rw.crewrite-try-rules-when-not-consp.proof
;; Reading the file took 1.65 seconds
;; Checking the proof took 27.16 seconds
;; VERIFY took 28.81 seconds
13597> VERIFY RW.CREWRITE-TRY-RULES-OF-CONS
;; Reading from Proofs/level10/thm-rw.crewrite-try-rules-of-cons.proof
;; Reading the file took 1.56 seconds
;; Checking the proof took 26.95 seconds
;; VERIFY took 28.52 seconds
13598> VERIFY RW.CREWRITE-TRY-MATCHES-WHEN-NOT-CONSP
;; Reading from Proofs/level10/thm-rw.crewrite-try-matches-when-not-consp.proof
;; Reading the file took 1.48 seconds
;; Checking the proof took 27.02 seconds
;; VERIFY took 28.51 seconds
13599> VERIFY RW.CREWRITE-TRY-MATCHES-OF-CONS
;; Reading from Proofs/level10/thm-rw.crewrite-try-matches-of-cons.proof
;; Reading the file took 1.48 seconds
;; Checking the proof took 26.43 seconds
;; VERIFY took 27.92 seconds
13600> VERIFY RW.CREWRITE-RELIEVE-HYPS-WHEN-NOT-CONSP
;; Reading from Proofs/level10/thm-rw.crewrite-relieve-hyps-when-not-consp.proof
;; Reading the file took 1.52 seconds
;; Checking the proof took 27.11 seconds
;; VERIFY took 28.64 seconds
13601> VERIFY RW.CREWRITE-RELIEVE-HYPS-OF-CONS
;; Reading from Proofs/level10/thm-rw.crewrite-relieve-hyps-of-cons.proof
;; Reading the file took 1.49 seconds
;; Checking the proof took 27.00 seconds
;; VERIFY took 28.50 seconds
13602> VERIFY BOOLEANP-OF-RW.HYPRESULT->SUCCESSP-OF-RW.CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-booleanp-of-rw.hypresult-_gt_successp-of-rw.crewrite-relieve-hyps.proof
;; Reading the file took 1.48 seconds
;; Checking the proof took 21.76 seconds
;; VERIFY took 23.25 seconds
13603> VERIFY ZP-OF-ONE-PLUS
;; Reading from Proofs/level10/thm-zp-of-one-plus.proof
;; Reading the file took 1.44 seconds
;; Checking the proof took 19.17 seconds
;; VERIFY took 20.63 seconds
13604> VERIFY LEMMA-FOR-FORCING-RW.TRACEP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-lemma-for-forcing-rw.tracep-of-rw.cresult-_gt_data-of-rw.crewrite-core.proof
;; Reading the file took 47.90 seconds
;; Checking the proof took 4550.30 seconds
;; VERIFY took 4600.19 seconds
13605> VERIFY FORCING-RW.TRACEP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-forcing-rw.tracep-of-rw.cresult-_gt_data-of-rw.crewrite-core.proof
;; Reading the file took 0.94 seconds
;; Checking the proof took 23.87 seconds
;; VERIFY took 24.83 seconds
13606> VERIFY FORCING-RW.CACHEP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-forcing-rw.cachep-of-rw.cresult-_gt_cache-of-rw.crewrite-core.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 23.24 seconds
;; VERIFY took 24.16 seconds
13607> VERIFY FORCING-RW.TRACE-LISTP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-CORE-LIST
;; Reading from Proofs/level10/thm-forcing-rw.trace-listp-of-rw.cresult-_gt_data-of-rw.crewrite-core-list.proof
;; Reading the file took 1.12 seconds
;; Checking the proof took 25.52 seconds
;; VERIFY took 26.66 seconds
13608> VERIFY FORCING-RW.CACHEP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-CORE-LIST
;; Reading from Proofs/level10/thm-forcing-rw.cachep-of-rw.cresult-_gt_cache-of-rw.crewrite-core-list.proof
;; Reading the file took 1.21 seconds
;; Checking the proof took 25.25 seconds
;; VERIFY took 26.48 seconds
13609> VERIFY FORCING-RW.TRACEP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-RULE
;; Reading from Proofs/level10/thm-forcing-rw.tracep-of-rw.cresult-_gt_data-of-rw.crewrite-try-rule.proof
;; Reading the file took 1.13 seconds
;; Checking the proof took 22.84 seconds
;; VERIFY took 23.99 seconds
13610> VERIFY FORCING-RW.CACHEP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-TRY-RULE
;; Reading from Proofs/level10/thm-forcing-rw.cachep-of-rw.cresult-_gt_cache-of-rw.crewrite-try-rule.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 22.60 seconds
;; VERIFY took 23.53 seconds
13611> VERIFY FORCING-RW.TRACEP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-RULES
;; Reading from Proofs/level10/thm-forcing-rw.tracep-of-rw.cresult-_gt_data-of-rw.crewrite-try-rules.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 24.07 seconds
;; VERIFY took 24.97 seconds
13612> VERIFY FORCING-RW.CACHEP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-TRY-RULES
;; Reading from Proofs/level10/thm-forcing-rw.cachep-of-rw.cresult-_gt_cache-of-rw.crewrite-try-rules.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 23.45 seconds
;; VERIFY took 24.35 seconds
13613> VERIFY FORCING-RW.TRACEP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-MATCH
;; Reading from Proofs/level10/thm-forcing-rw.tracep-of-rw.cresult-_gt_data-of-rw.crewrite-try-match.proof
;; Reading the file took 1.15 seconds
;; Checking the proof took 22.90 seconds
;; VERIFY took 24.07 seconds
13614> VERIFY FORCING-RW.CACHEP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-TRY-MATCH
;; Reading from Proofs/level10/thm-forcing-rw.cachep-of-rw.cresult-_gt_cache-of-rw.crewrite-try-match.proof
;; Reading the file took 1.15 seconds
;; Checking the proof took 22.25 seconds
;; VERIFY took 23.42 seconds
13615> VERIFY FORCING-RW.TRACEP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-MATCHES
;; Reading from Proofs/level10/thm-forcing-rw.tracep-of-rw.cresult-_gt_data-of-rw.crewrite-try-matches.proof
;; Reading the file took 1.22 seconds
;; Checking the proof took 22.75 seconds
;; VERIFY took 23.99 seconds
13616> VERIFY FORCING-RW.CACHEP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-TRY-MATCHES
;; Reading from Proofs/level10/thm-forcing-rw.cachep-of-rw.cresult-_gt_cache-of-rw.crewrite-try-matches.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 22.77 seconds
;; VERIFY took 23.68 seconds
13617> VERIFY FORCING-RW.TRACEP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-RELIEVE-HYP
;; Reading from Proofs/level10/thm-forcing-rw.tracep-of-rw.cresult-_gt_data-of-rw.crewrite-relieve-hyp.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 26.92 seconds
;; VERIFY took 27.84 seconds
13618> VERIFY FORCING-RW.CACHEP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-RELIEVE-HYP
;; Reading from Proofs/level10/thm-forcing-rw.cachep-of-rw.cresult-_gt_cache-of-rw.crewrite-relieve-hyp.proof
;; Reading the file took 0.87 seconds
;; Checking the proof took 25.71 seconds
;; VERIFY took 26.60 seconds
13619> VERIFY FORCING-RW.TRACE-LISTP-OF-RW.HYPRESULT->TRACES-OF-RW.CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-forcing-rw.trace-listp-of-rw.hypresult-_gt_traces-of-rw.crewrite-relieve-hyps.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 26.73 seconds
;; VERIFY took 27.67 seconds
13620> VERIFY FORCING-RW.CACHEP-OF-RW.HYPRESULT->CACHE-OF-RW.CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-forcing-rw.cachep-of-rw.hypresult-_gt_cache-of-rw.crewrite-relieve-hyps.proof
;; Reading the file took 1.18 seconds
;; Checking the proof took 25.52 seconds
;; VERIFY took 26.72 seconds
13621> VERIFY LEMMA-FOR-FORCING-RW.TRACE->IFFP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-lemma-for-forcing-rw.trace-_gt_iffp-of-rw.cresult-_gt_data-of-rw.crewrite-core.proof
;; Reading the file took 39.37 seconds
;; Checking the proof took 29066.03 seconds
;; VERIFY took 29106.44 seconds
13622> VERIFY FORCING-RW.TRACE->IFFP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-forcing-rw.trace-_gt_iffp-of-rw.cresult-_gt_data-of-rw.crewrite-core.proof
;; Reading the file took 1.15 seconds
;; Checking the proof took 22.11 seconds
;; VERIFY took 23.27 seconds
13623> VERIFY FORCING-RW.TRACE-LIST-IFFPS-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-CORE-LIST
;; Reading from Proofs/level10/thm-forcing-rw.trace-list-iffps-of-rw.cresult-_gt_data-of-rw.crewrite-core-list.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 23.78 seconds
;; VERIFY took 24.72 seconds
13624> VERIFY FORCING-RW.TRACE->IFFP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-RULE
;; Reading from Proofs/level10/thm-forcing-rw.trace-_gt_iffp-of-rw.cresult-_gt_data-of-rw.crewrite-try-rule.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 21.70 seconds
;; VERIFY took 22.60 seconds
13625> VERIFY FORCING-RW.TRACE->IFFP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-RULES
;; Reading from Proofs/level10/thm-forcing-rw.trace-_gt_iffp-of-rw.cresult-_gt_data-of-rw.crewrite-try-rules.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 22.17 seconds
;; VERIFY took 23.08 seconds
13626> VERIFY FORCING-RW.TRACE->IFFP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-MATCH
;; Reading from Proofs/level10/thm-forcing-rw.trace-_gt_iffp-of-rw.cresult-_gt_data-of-rw.crewrite-try-match.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 21.52 seconds
;; VERIFY took 22.43 seconds
13627> VERIFY FORCING-RW.TRACE->IFFP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-MATCHES
;; Reading from Proofs/level10/thm-forcing-rw.trace-_gt_iffp-of-rw.cresult-_gt_data-of-rw.crewrite-try-matches.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 21.85 seconds
;; VERIFY took 22.76 seconds
13628> VERIFY FORCING-RW.TRACE->IFFP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-RELIEVE-HYP
;; Reading from Proofs/level10/thm-forcing-rw.trace-_gt_iffp-of-rw.cresult-_gt_data-of-rw.crewrite-relieve-hyp.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 23.94 seconds
;; VERIFY took 24.84 seconds
13629> VERIFY FORCING-RW.TRACE-LIST-IFFPS-OF-RW.HYPRESULT->TRACES-OF-RW.CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-forcing-rw.trace-list-iffps-of-rw.hypresult-_gt_traces-of-rw.crewrite-relieve-hyps.proof
;; Reading the file took 1.09 seconds
;; Checking the proof took 23.80 seconds
;; VERIFY took 24.91 seconds
13630> VERIFY LEMMA-FOR-FORCING-RW.TRACE->HYPBOX-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-lemma-for-forcing-rw.trace-_gt_hypbox-of-rw.cresult-_gt_data-of-rw.crewrite-core.proof
;; Reading the file took 51.48 seconds
;; Checking the proof took 4971.38 seconds
;; VERIFY took 5025.06 seconds
13631> VERIFY FORCING-RW.TRACE->HYPBOX-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-forcing-rw.trace-_gt_hypbox-of-rw.cresult-_gt_data-of-rw.crewrite-core.proof
;; Reading the file took 0.98 seconds
;; Checking the proof took 24.06 seconds
;; VERIFY took 25.06 seconds
13632> VERIFY FORCING-RW.CACHE-ASSMSP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-forcing-rw.cache-assmsp-of-rw.cresult-_gt_cache-of-rw.crewrite-core.proof
;; Reading the file took 0.87 seconds
;; Checking the proof took 23.57 seconds
;; VERIFY took 24.45 seconds
13633> VERIFY FORCING-RW.TRACE-LIST-HYPBOXES-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-CORE-LIST
;; Reading from Proofs/level10/thm-forcing-rw.trace-list-hypboxes-of-rw.cresult-_gt_data-of-rw.crewrite-core-list.proof
;; Reading the file took 1.18 seconds
;; Checking the proof took 27.89 seconds
;; VERIFY took 29.10 seconds
13634> VERIFY FORCING-RW.CACHE-ASSMSP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-CORE-LIST
;; Reading from Proofs/level10/thm-forcing-rw.cache-assmsp-of-rw.cresult-_gt_cache-of-rw.crewrite-core-list.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 26.84 seconds
;; VERIFY took 27.74 seconds
13635> VERIFY FORCING-RW.TRACE->HYPBOX-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-RULE
;; Reading from Proofs/level10/thm-forcing-rw.trace-_gt_hypbox-of-rw.cresult-_gt_data-of-rw.crewrite-try-rule.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 22.75 seconds
;; VERIFY took 23.66 seconds
13636> VERIFY FORCING-RW.CACHE-ASSMSP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-TRY-RULE
;; Reading from Proofs/level10/thm-forcing-rw.cache-assmsp-of-rw.cresult-_gt_cache-of-rw.crewrite-try-rule.proof
;; Reading the file took 1.18 seconds
;; Checking the proof took 22.64 seconds
;; VERIFY took 23.84 seconds
13637> VERIFY FORCING-RW.TRACE->HYPBOX-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-RULES
;; Reading from Proofs/level10/thm-forcing-rw.trace-_gt_hypbox-of-rw.cresult-_gt_data-of-rw.crewrite-try-rules.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 24.40 seconds
;; VERIFY took 25.30 seconds
13638> VERIFY FORCING-RW.CACHE-ASSMSP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-TRY-RULES
;; Reading from Proofs/level10/thm-forcing-rw.cache-assmsp-of-rw.cresult-_gt_cache-of-rw.crewrite-try-rules.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 23.74 seconds
;; VERIFY took 24.65 seconds
13639> VERIFY FORCING-RW.TRACE->HYPBOX-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-MATCH
;; Reading from Proofs/level10/thm-forcing-rw.trace-_gt_hypbox-of-rw.cresult-_gt_data-of-rw.crewrite-try-match.proof
;; Reading the file took 1.16 seconds
;; Checking the proof took 23.23 seconds
;; VERIFY took 24.42 seconds
13640> VERIFY FORCING-RW.CACHE-ASSMSP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-TRY-MATCH
;; Reading from Proofs/level10/thm-forcing-rw.cache-assmsp-of-rw.cresult-_gt_cache-of-rw.crewrite-try-match.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 22.82 seconds
;; VERIFY took 23.72 seconds
13641> VERIFY FORCING-RW.TRACE->HYPBOX-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-MATCHES
;; Reading from Proofs/level10/thm-forcing-rw.trace-_gt_hypbox-of-rw.cresult-_gt_data-of-rw.crewrite-try-matches.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 23.13 seconds
;; VERIFY took 24.03 seconds
13642> VERIFY FORCING-RW.CACHE-ASSMSP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-TRY-MATCHES
;; Reading from Proofs/level10/thm-forcing-rw.cache-assmsp-of-rw.cresult-_gt_cache-of-rw.crewrite-try-matches.proof
;; Reading the file took 1.17 seconds
;; Checking the proof took 22.79 seconds
;; VERIFY took 23.97 seconds
13643> VERIFY FORCING-RW.TRACE->HYPBOX-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-RELIEVE-HYP
;; Reading from Proofs/level10/thm-forcing-rw.trace-_gt_hypbox-of-rw.cresult-_gt_data-of-rw.crewrite-relieve-hyp.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 27.61 seconds
;; VERIFY took 28.52 seconds
13644> VERIFY FORCING-RW.CACHE-ASSMSP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-RELIEVE-HYP
;; Reading from Proofs/level10/thm-forcing-rw.cache-assmsp-of-rw.cresult-_gt_cache-of-rw.crewrite-relieve-hyp.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 26.54 seconds
;; VERIFY took 27.46 seconds
13645> VERIFY FORCING-RW.TRACE-LIST-HYPBOXES-OF-RW.HYPRESULT->TRACES-OF-RW.CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-forcing-rw.trace-list-hypboxes-of-rw.hypresult-_gt_traces-of-rw.crewrite-relieve-hyps.proof
;; Reading the file took 1.20 seconds
;; Checking the proof took 27.82 seconds
;; VERIFY took 29.04 seconds
13646> VERIFY FORCING-RW.CACHE-ASSMSP-OF-RW.HYPRSEULT->CACHE-OF-RW.CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-forcing-rw.cache-assmsp-of-rw.hyprseult-_gt_cache-of-rw.crewrite-relieve-hyps.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 26.68 seconds
;; VERIFY took 27.58 seconds
13647> VERIFY LEMMA-FOR-FORCING-RW.TRACE->LHS-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-lemma-for-forcing-rw.trace-_gt_lhs-of-rw.cresult-_gt_data-of-rw.crewrite-core.proof
;; Reading the file took 51.19 seconds
;; Checking the proof took 5616.55 seconds
;; VERIFY took 5670.01 seconds
13648> VERIFY FORCING-RW.TRACE->LHS-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-forcing-rw.trace-_gt_lhs-of-rw.cresult-_gt_data-of-rw.crewrite-core.proof
;; Reading the file took 0.97 seconds
;; Checking the proof took 23.81 seconds
;; VERIFY took 24.80 seconds
13649> VERIFY FORCING-RW.CACHE-LHSES-OKP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-forcing-rw.cache-lhses-okp-of-rw.cresult-_gt_cache-of-rw.crewrite-core.proof
;; Reading the file took 1.10 seconds
;; Checking the proof took 23.35 seconds
;; VERIFY took 24.47 seconds
13650> VERIFY FORCING-RW.TRACE-LIST-LHSES-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-CORE-LIST
;; Reading from Proofs/level10/thm-forcing-rw.trace-list-lhses-of-rw.cresult-_gt_data-of-rw.crewrite-core-list.proof
;; Reading the file took 1.10 seconds
;; Checking the proof took 27.40 seconds
;; VERIFY took 28.52 seconds
13651> VERIFY FORCING-RW.CACHE-LHSES-OKP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-CORE-LIST
;; Reading from Proofs/level10/thm-forcing-rw.cache-lhses-okp-of-rw.cresult-_gt_cache-of-rw.crewrite-core-list.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 26.32 seconds
;; VERIFY took 27.22 seconds
13652> VERIFY FORCING-RW.TRACE->LHS-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-RULE
;; Reading from Proofs/level10/thm-forcing-rw.trace-_gt_lhs-of-rw.cresult-_gt_data-of-rw.crewrite-try-rule.proof
;; Reading the file took 1.41 seconds
;; Checking the proof took 23.11 seconds
;; VERIFY took 24.53 seconds
13653> VERIFY FORCING-RW.CACHE-LHSES-OKP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-TRY-RULE
;; Reading from Proofs/level10/thm-forcing-rw.cache-lhses-okp-of-rw.cresult-_gt_cache-of-rw.crewrite-try-rule.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 22.68 seconds
;; VERIFY took 23.60 seconds
13654> VERIFY FORCING-RW.TRACE->LHS-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-RULES
;; Reading from Proofs/level10/thm-forcing-rw.trace-_gt_lhs-of-rw.cresult-_gt_data-of-rw.crewrite-try-rules.proof
;; Reading the file took 1.10 seconds
;; Checking the proof took 23.62 seconds
;; VERIFY took 24.74 seconds
13655> VERIFY FORCING-RW.CACHE-LHSES-OKP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-TRY-RULES
;; Reading from Proofs/level10/thm-forcing-rw.cache-lhses-okp-of-rw.cresult-_gt_cache-of-rw.crewrite-try-rules.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 23.71 seconds
;; VERIFY took 24.61 seconds
13656> VERIFY FORCING-RW.TRACE->LHS-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-MATCH
;; Reading from Proofs/level10/thm-forcing-rw.trace-_gt_lhs-of-rw.cresult-_gt_data-of-rw.crewrite-try-match.proof
;; Reading the file took 1.15 seconds
;; Checking the proof took 23.08 seconds
;; VERIFY took 24.25 seconds
13657> VERIFY FORCING-RW.CACHE-LHSES-OKP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-TRY-MATCH
;; Reading from Proofs/level10/thm-forcing-rw.cache-lhses-okp-of-rw.cresult-_gt_cache-of-rw.crewrite-try-match.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 22.90 seconds
;; VERIFY took 23.83 seconds
13658> VERIFY FORCING-RW.TRACE->LHS-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-MATCHES
;; Reading from Proofs/level10/thm-forcing-rw.trace-_gt_lhs-of-rw.cresult-_gt_data-of-rw.crewrite-try-matches.proof
;; Reading the file took 1.11 seconds
;; Checking the proof took 23.31 seconds
;; VERIFY took 24.44 seconds
13659> VERIFY FORCING-RW.CACHE-LHSES-OKP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-TRY-MATCHES
;; Reading from Proofs/level10/thm-forcing-rw.cache-lhses-okp-of-rw.cresult-_gt_cache-of-rw.crewrite-try-matches.proof
;; Reading the file took 0.94 seconds
;; Checking the proof took 22.16 seconds
;; VERIFY took 23.12 seconds
13660> VERIFY FORCING-RW.TRACE->LHS-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-RELIEVE-HYP
;; Reading from Proofs/level10/thm-forcing-rw.trace-_gt_lhs-of-rw.cresult-_gt_data-of-rw.crewrite-relieve-hyp.proof
;; Reading the file took 1.11 seconds
;; Checking the proof took 27.84 seconds
;; VERIFY took 28.97 seconds
13661> VERIFY FORCING-RW.CACHE-LHSES-OKP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-RELIEVE-HYP
;; Reading from Proofs/level10/thm-forcing-rw.cache-lhses-okp-of-rw.cresult-_gt_cache-of-rw.crewrite-relieve-hyp.proof
;; Reading the file took 1.10 seconds
;; Checking the proof took 26.65 seconds
;; VERIFY took 27.76 seconds
13662> VERIFY FORCING-RW.TRACE-LIST-LHSES-OF-RW.HYPRESULT->TRACES-OF-RW.CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-forcing-rw.trace-list-lhses-of-rw.hypresult-_gt_traces-of-rw.crewrite-relieve-hyps.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 27.66 seconds
;; VERIFY took 28.58 seconds
13663> VERIFY FORCING-RW.CACHE-LHSES-OKP-OF-RW.HYPRESULT->CACHE-OF-RW.CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-forcing-rw.cache-lhses-okp-of-rw.hypresult-_gt_cache-of-rw.crewrite-relieve-hyps.proof
;; Reading the file took 1.10 seconds
;; Checking the proof took 26.45 seconds
;; VERIFY took 27.56 seconds
13664> VERIFY FORCING-RW.TRACE->RHS-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-RELIEVE-HYP
;; Reading from Proofs/level10/thm-forcing-rw.trace-_gt_rhs-of-rw.cresult-_gt_data-of-rw.crewrite-relieve-hyp.proof
;; Reading the file took 1.10 seconds
;; Checking the proof took 351.12 seconds
;; VERIFY took 352.24 seconds
13665> VERIFY FORCING-RW.TRACE-LIST-RHSES-OF-RW.HYPRESULT->TRACES-OF-RW.CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-forcing-rw.trace-list-rhses-of-rw.hypresult-_gt_traces-of-rw.crewrite-relieve-hyps.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 30.81 seconds
;; VERIFY took 31.73 seconds
13666> VERIFY LEMMA-2-FOR-FORCING-RW.TRACE-OKP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-lemma-2-for-forcing-rw.trace-okp-of-rw.cresult-_gt_data-of-rw.crewrite-core.proof
;; Reading the file took 1.13 seconds
;; Checking the proof took 27.10 seconds
;; VERIFY took 28.24 seconds
13667> VERIFY LEMMA-FOR-FORCING-RW.TRACE-OKP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-lemma-for-forcing-rw.trace-okp-of-rw.cresult-_gt_data-of-rw.crewrite-core.proof
;; Reading the file took 73.09 seconds
;; Checking the proof took 6382.78 seconds
;; VERIFY took 6457.99 seconds
13668> VERIFY FORCING-RW.TRACE-OKP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-forcing-rw.trace-okp-of-rw.cresult-_gt_data-of-rw.crewrite-core.proof
;; Reading the file took 0.97 seconds
;; Checking the proof took 31.21 seconds
;; VERIFY took 32.19 seconds
13669> VERIFY FORCING-RW.CACHE-TRACES-OKP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-forcing-rw.cache-traces-okp-of-rw.cresult-_gt_cache-of-rw.crewrite-core.proof
;; Reading the file took 1.17 seconds
;; Checking the proof took 31.05 seconds
;; VERIFY took 32.24 seconds
13670> VERIFY FORCING-RW.TRACE-LIST-OKP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-CORE-LIST
;; Reading from Proofs/level10/thm-forcing-rw.trace-list-okp-of-rw.cresult-_gt_data-of-rw.crewrite-core-list.proof
;; Reading the file took 0.93 seconds
;; Checking the proof took 36.11 seconds
;; VERIFY took 37.05 seconds
13671> VERIFY FORCING-RW.CACHE-TRACES-OKP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-CORE-LIST
;; Reading from Proofs/level10/thm-forcing-rw.cache-traces-okp-of-rw.cresult-_gt_cache-of-rw.crewrite-core-list.proof
;; Reading the file took 1.22 seconds
;; Checking the proof took 35.16 seconds
;; VERIFY took 36.39 seconds
13672> VERIFY FORCING-RW.TRACE-OKP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-RULE
;; Reading from Proofs/level10/thm-forcing-rw.trace-okp-of-rw.cresult-_gt_data-of-rw.crewrite-try-rule.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 30.68 seconds
;; VERIFY took 31.59 seconds
13673> VERIFY FORCING-RW.CACHE-TRACES-OKP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-TRY-RULE
;; Reading from Proofs/level10/thm-forcing-rw.cache-traces-okp-of-rw.cresult-_gt_cache-of-rw.crewrite-try-rule.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 29.79 seconds
;; VERIFY took 30.73 seconds
13674> VERIFY FORCING-RW.TRACE-OKP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-RULES
;; Reading from Proofs/level10/thm-forcing-rw.trace-okp-of-rw.cresult-_gt_data-of-rw.crewrite-try-rules.proof
;; Reading the file took 1.19 seconds
;; Checking the proof took 32.09 seconds
;; VERIFY took 33.30 seconds
13675> VERIFY FORCING-RW.CACHE-TRACES-OKP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-TRY-RULES
;; Reading from Proofs/level10/thm-forcing-rw.cache-traces-okp-of-rw.cresult-_gt_cache-of-rw.crewrite-try-rules.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 31.29 seconds
;; VERIFY took 32.21 seconds
13676> VERIFY FORCING-RW.TRACE-OKP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-MATCH
;; Reading from Proofs/level10/thm-forcing-rw.trace-okp-of-rw.cresult-_gt_data-of-rw.crewrite-try-match.proof
;; Reading the file took 1.24 seconds
;; Checking the proof took 32.96 seconds
;; VERIFY took 34.24 seconds
13677> VERIFY FORCING-RW.CACHE-TRACES-OKP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-TRY-MATCH
;; Reading from Proofs/level10/thm-forcing-rw.cache-traces-okp-of-rw.cresult-_gt_cache-of-rw.crewrite-try-match.proof
;; Reading the file took 0.93 seconds
;; Checking the proof took 31.39 seconds
;; VERIFY took 32.35 seconds
13678> VERIFY FORCING-RW.TRACE-OKP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-MATCHES
;; Reading from Proofs/level10/thm-forcing-rw.trace-okp-of-rw.cresult-_gt_data-of-rw.crewrite-try-matches.proof
;; Reading the file took 1.20 seconds
;; Checking the proof took 32.94 seconds
;; VERIFY took 34.17 seconds
13679> VERIFY FORCING-RW.CACHE-TRACES-OKP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-TRY-MATCHES
;; Reading from Proofs/level10/thm-forcing-rw.cache-traces-okp-of-rw.cresult-_gt_cache-of-rw.crewrite-try-matches.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 32.01 seconds
;; VERIFY took 32.92 seconds
13680> VERIFY FORCING-RW.TRACE-OKP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-RELIEVE-HYP
;; Reading from Proofs/level10/thm-forcing-rw.trace-okp-of-rw.cresult-_gt_data-of-rw.crewrite-relieve-hyp.proof
;; Reading the file took 1.20 seconds
;; Checking the proof took 36.78 seconds
;; VERIFY took 38.00 seconds
13681> VERIFY FORCING-RW.CACHE-TRACES-OKP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-RELIEVE-HYP
;; Reading from Proofs/level10/thm-forcing-rw.cache-traces-okp-of-rw.cresult-_gt_cache-of-rw.crewrite-relieve-hyp.proof
;; Reading the file took 0.93 seconds
;; Checking the proof took 35.08 seconds
;; VERIFY took 36.03 seconds
13682> VERIFY FORCING-RW.TRACE-LIST-OKP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-forcing-rw.trace-list-okp-of-rw.cresult-_gt_cache-of-rw.crewrite-relieve-hyps.proof
;; Reading the file took 1.22 seconds
;; Checking the proof took 36.92 seconds
;; VERIFY took 38.16 seconds
13683> VERIFY FORCING-RW.CACHE-TRACES-OKP-OF-RW.HYPRESULT->CACHE-OF-RW.CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-forcing-rw.cache-traces-okp-of-rw.hypresult-_gt_cache-of-rw.crewrite-relieve-hyps.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 35.13 seconds
;; VERIFY took 36.05 seconds
13684> VERIFY LEMMA-FOR-FORCING-RW.TRACE-ATBLP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-lemma-for-forcing-rw.trace-atblp-of-rw.cresult-_gt_data-of-rw.crewrite-core.proof
;; Reading the file took 55.25 seconds
;; Checking the proof took 6168.46 seconds
;; VERIFY took 6226.20 seconds
13685> VERIFY FORCING-RW.TRACE-ATBLP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-forcing-rw.trace-atblp-of-rw.cresult-_gt_data-of-rw.crewrite-core.proof
;; Reading the file took 1.00 seconds
;; Checking the proof took 35.04 seconds
;; VERIFY took 36.06 seconds
13686> VERIFY FORCING-RW.CACHE-ATBLP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-forcing-rw.cache-atblp-of-rw.cresult-_gt_cache-of-rw.crewrite-core.proof
;; Reading the file took 1.12 seconds
;; Checking the proof took 34.58 seconds
;; VERIFY took 35.73 seconds
13687> VERIFY FORCING-RW.TRACE-LIST-ATBLP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-CORE-LIST
;; Reading from Proofs/level10/thm-forcing-rw.trace-list-atblp-of-rw.cresult-_gt_data-of-rw.crewrite-core-list.proof
;; Reading the file took 0.93 seconds
;; Checking the proof took 50.10 seconds
;; VERIFY took 51.06 seconds
13688> VERIFY FORCING-RW.CACHE-ATBLP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-CORE-LIST
;; Reading from Proofs/level10/thm-forcing-rw.cache-atblp-of-rw.cresult-_gt_cache-of-rw.crewrite-core-list.proof
;; Reading the file took 1.11 seconds
;; Checking the proof took 47.68 seconds
;; VERIFY took 48.81 seconds
13689> VERIFY FORCING-RW.TRACE-ATBLP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-RULE
;; Reading from Proofs/level10/thm-forcing-rw.trace-atblp-of-rw.cresult-_gt_data-of-rw.crewrite-try-rule.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 30.83 seconds
;; VERIFY took 31.77 seconds
13690> VERIFY FORCING-RW.CACHE-ATBLP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-TRY-RULE
;; Reading from Proofs/level10/thm-forcing-rw.cache-atblp-of-rw.cresult-_gt_cache-of-rw.crewrite-try-rule.proof
;; Reading the file took 1.11 seconds
;; Checking the proof took 30.33 seconds
;; VERIFY took 31.46 seconds
13691> VERIFY FORCING-RW.TRACE-ATBLP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-RULES
;; Reading from Proofs/level10/thm-forcing-rw.trace-atblp-of-rw.cresult-_gt_data-of-rw.crewrite-try-rules.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 35.26 seconds
;; VERIFY took 36.21 seconds
13692> VERIFY FORCING-RW.CACHE-ATBLP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-TRY-RULES
;; Reading from Proofs/level10/thm-forcing-rw.cache-atblp-of-rw.cresult-_gt_cache-of-rw.crewrite-try-rules.proof
;; Reading the file took 1.12 seconds
;; Checking the proof took 34.20 seconds
;; VERIFY took 35.34 seconds
13693> VERIFY FORCING-RW.TRACE-ATBLP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-MATCH
;; Reading from Proofs/level10/thm-forcing-rw.trace-atblp-of-rw.cresult-_gt_data-of-rw.crewrite-try-match.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 28.99 seconds
;; VERIFY took 29.91 seconds
13694> VERIFY FORCING-RW.CACHE-ATBLP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-TRY-MATCH
;; Reading from Proofs/level10/thm-forcing-rw.cache-atblp-of-rw.cresult-_gt_cache-of-rw.crewrite-try-match.proof
;; Reading the file took 1.16 seconds
;; Checking the proof took 28.47 seconds
;; VERIFY took 29.66 seconds
13695> VERIFY FORCING-RW.TRACE-ATBLP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-MATCHES
;; Reading from Proofs/level10/thm-forcing-rw.trace-atblp-of-rw.cresult-_gt_data-of-rw.crewrite-try-matches.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 30.56 seconds
;; VERIFY took 31.48 seconds
13696> VERIFY FORCING-RW.CACHE-ATBLP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-TRY-MATCHES
;; Reading from Proofs/level10/thm-forcing-rw.cache-atblp-of-rw.cresult-_gt_cache-of-rw.crewrite-try-matches.proof
;; Reading the file took 1.12 seconds
;; Checking the proof took 29.42 seconds
;; VERIFY took 30.56 seconds
13697> VERIFY FORCING-RW.TRACE-ATBLP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-RELIEVE-HYP
;; Reading from Proofs/level10/thm-forcing-rw.trace-atblp-of-rw.cresult-_gt_data-of-rw.crewrite-relieve-hyp.proof
;; Reading the file took 1.13 seconds
;; Checking the proof took 43.17 seconds
;; VERIFY took 44.33 seconds
13698> VERIFY FORCING-RW.CACHE-ATBLP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-RELIEVE-HYP
;; Reading from Proofs/level10/thm-forcing-rw.cache-atblp-of-rw.cresult-_gt_data-of-rw.crewrite-relieve-hyp.proof
;; Reading the file took 1.12 seconds
;; Checking the proof took 42.09 seconds
;; VERIFY took 43.23 seconds
13699> VERIFY FORCING-RW.TRACE-LIST-ATBLP-OF-RW.HYPRESULT->TRACES-OF-RW.CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-forcing-rw.trace-list-atblp-of-rw.hypresult-_gt_traces-of-rw.crewrite-relieve-hyps.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 44.35 seconds
;; VERIFY took 45.28 seconds
13700> VERIFY FORCING-RW.CACHE-ATBLP-OF-RW.HYPRESULT->CACHE-OF-RW.CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-forcing-rw.cache-atblp-of-rw.hypresult-_gt_cache-of-rw.crewrite-relieve-hyps.proof
;; Reading the file took 1.14 seconds
;; Checking the proof took 42.29 seconds
;; VERIFY took 43.46 seconds
13701> VERIFY LEMMA-FOR-FORCING-RW.TRACE-ENV-OKP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-lemma-for-forcing-rw.trace-env-okp-of-rw.cresult-_gt_data-of-rw.crewrite-core.proof
;; Reading the file took 88.13 seconds
;; Checking the proof took 7329.27 seconds
;; VERIFY took 7419.92 seconds
13702> VERIFY FORCING-RW.TRACE-ENV-OKP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-forcing-rw.trace-env-okp-of-rw.cresult-_gt_data-of-rw.crewrite-core.proof
;; Reading the file took 0.96 seconds
;; Checking the proof took 47.87 seconds
;; VERIFY took 48.85 seconds
13703> VERIFY FORCING-RW.CACHE-ENV-OKP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-forcing-rw.cache-env-okp-of-rw.cresult-_gt_cache-of-rw.crewrite-core.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 47.19 seconds
;; VERIFY took 48.12 seconds
13704> VERIFY FORCING-RW.TRACE-LIST-ENV-OKP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-CORE-LIST
;; Reading from Proofs/level10/thm-forcing-rw.trace-list-env-okp-of-rw.cresult-_gt_data-of-rw.crewrite-core-list.proof
;; Reading the file took 1.26 seconds
;; Checking the proof took 67.31 seconds
;; VERIFY took 68.60 seconds
13705> VERIFY FORCING-RW.CACHE-ENV-OKP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-CORE-LIST
;; Reading from Proofs/level10/thm-forcing-rw.cache-env-okp-of-rw.cresult-_gt_cache-of-rw.crewrite-core-list.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 65.70 seconds
;; VERIFY took 66.64 seconds
13706> VERIFY FORCING-RW.TRACE-ENV-OKP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-RULE
;; Reading from Proofs/level10/thm-forcing-rw.trace-env-okp-of-rw.cresult-_gt_data-of-rw.crewrite-try-rule.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 34.89 seconds
;; VERIFY took 35.82 seconds
13707> VERIFY FORCING-RW.CACHE-ENV-OKP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-TRY-RULE
;; Reading from Proofs/level10/thm-forcing-rw.cache-env-okp-of-rw.cresult-_gt_cache-of-rw.crewrite-try-rule.proof
;; Reading the file took 1.21 seconds
;; Checking the proof took 34.13 seconds
;; VERIFY took 35.37 seconds
13708> VERIFY FORCING-RW.TRACE-ENV-OKP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-RULES
;; Reading from Proofs/level10/thm-forcing-rw.trace-env-okp-of-rw.cresult-_gt_data-of-rw.crewrite-try-rules.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 47.03 seconds
;; VERIFY took 47.98 seconds
13709> VERIFY FORCING-RW.CACHE-ENV-OKP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-TRY-RULES
;; Reading from Proofs/level10/thm-forcing-rw.cache-env-okp-of-rw.cresult-_gt_cache-of-rw.crewrite-try-rules.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 45.01 seconds
;; VERIFY took 45.94 seconds
13710> VERIFY FORCING-RW.TRACE-ENV-OKP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-MATCH
;; Reading from Proofs/level10/thm-forcing-rw.trace-env-okp-of-rw.cresult-_gt_data-of-rw.crewrite-try-match.proof
;; Reading the file took 1.23 seconds
;; Checking the proof took 31.90 seconds
;; VERIFY took 33.16 seconds
13711> VERIFY FORCING-RW.CACHE-ENV-OKP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-TRY-MATCH
;; Reading from Proofs/level10/thm-forcing-rw.cache-env-okp-of-rw.cresult-_gt_cache-of-rw.crewrite-try-match.proof
;; Reading the file took 1.26 seconds
;; Checking the proof took 31.48 seconds
;; VERIFY took 32.77 seconds
13712> VERIFY FORCING-RW.TRACE-ENV-OKP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-TRY-MATCHES
;; Reading from Proofs/level10/thm-forcing-rw.trace-env-okp-of-rw.cresult-_gt_data-of-rw.crewrite-try-matches.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 33.84 seconds
;; VERIFY took 34.78 seconds
13713> VERIFY FORCING-RW.CACHE-ENV-OKP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-TRY-MATCHES
;; Reading from Proofs/level10/thm-forcing-rw.cache-env-okp-of-rw.cresult-_gt_cache-of-rw.crewrite-try-matches.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 32.45 seconds
;; VERIFY took 33.39 seconds
13714> VERIFY FORCING-RW.TRACE-ENV-OKP-OF-RW.CRESULT->DATA-OF-RW.CREWRITE-RELIEVE-HYP
;; Reading from Proofs/level10/thm-forcing-rw.trace-env-okp-of-rw.cresult-_gt_data-of-rw.crewrite-relieve-hyp.proof
;; Reading the file took 0.93 seconds
;; Checking the proof took 55.02 seconds
;; VERIFY took 55.97 seconds
13715> VERIFY FORCING-RW.CACHE-ENV-OKP-OF-RW.CRESULT->CACHE-OF-RW.CREWRITE-RELIEVE-HYP
;; Reading from Proofs/level10/thm-forcing-rw.cache-env-okp-of-rw.cresult-_gt_cache-of-rw.crewrite-relieve-hyp.proof
;; Reading the file took 1.25 seconds
;; Checking the proof took 51.95 seconds
;; VERIFY took 53.22 seconds
13716> VERIFY FORCING-RW.TRACE-LIST-ENV-OKP-OF-RW.HYPRESULT->TRACES-OF-RW.CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-forcing-rw.trace-list-env-okp-of-rw.hypresult-_gt_traces-of-rw.crewrite-relieve-hyps.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 55.51 seconds
;; VERIFY took 56.45 seconds
13717> VERIFY FORCING-RW.CACHE-ENV-OKP-OF-RW.HYPRESULT->CACHE-OF-RW.CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-forcing-rw.cache-env-okp-of-rw.hypresult-_gt_cache-of-rw.crewrite-relieve-hyps.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 52.50 seconds
;; VERIFY took 53.44 seconds
13718> VERIFY MAP-LISTP-WHEN-LOGIC.SIGMA-LISTP
;; Reading from Proofs/level10/thm-map-listp-when-logic.sigma-listp.proof
;; Reading the file took 1.26 seconds
;; Checking the proof took 19.69 seconds
;; VERIFY took 20.96 seconds
13719> DEFINE RW.CREWRITE
;; Reading from Proofs/level10/admit-rw.crewrite.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13720> VERIFY RW.CREWRITE
;; Reading from Proofs/level10/thm-rw.crewrite.proof
;; Reading the file took 0.21 seconds
;; Checking the proof took 3.35 seconds
;; VERIFY took 3.57 seconds
13721> VERIFY FORCING-RW.TRACEP-OF-RW.CREWRITE
;; Reading from Proofs/level10/thm-forcing-rw.tracep-of-rw.crewrite.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 18.72 seconds
;; VERIFY took 19.63 seconds
13722> VERIFY FORCING-RW.TRACE->HYPBOX-OF-RW.CREWRITE
;; Reading from Proofs/level10/thm-forcing-rw.trace-_gt_hypbox-of-rw.crewrite.proof
;; Reading the file took 0.94 seconds
;; Checking the proof took 18.68 seconds
;; VERIFY took 19.63 seconds
13723> VERIFY FORCING-RW.TRACE->LHS-OF-RW.CREWRITE
;; Reading from Proofs/level10/thm-forcing-rw.trace-_gt_lhs-of-rw.crewrite.proof
;; Reading the file took 1.10 seconds
;; Checking the proof took 18.42 seconds
;; VERIFY took 19.53 seconds
13724> VERIFY FORCING-RW.TRACE->IFFP-OF-RW.CREWRITE
;; Reading from Proofs/level10/thm-forcing-rw.trace-_gt_iffp-of-rw.crewrite.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 18.76 seconds
;; VERIFY took 19.68 seconds
13725> VERIFY FORCING-RW.TRACE-ATBLP-OF-RW.CREWRITE
;; Reading from Proofs/level10/thm-forcing-rw.trace-atblp-of-rw.crewrite.proof
;; Reading the file took 1.01 seconds
;; Checking the proof took 18.82 seconds
;; VERIFY took 19.85 seconds
13726> VERIFY FORCING-RW.TRACE-OKP-OF-RW.CREWRITE
;; Reading from Proofs/level10/thm-forcing-rw.trace-okp-of-rw.crewrite.proof
;; Reading the file took 1.22 seconds
;; Checking the proof took 18.61 seconds
;; VERIFY took 19.84 seconds
13727> VERIFY FORCING-RW.TRACE-ENV-OKP-OF-RW.CREWRITE
;; Reading from Proofs/level10/thm-forcing-rw.trace-env-okp-of-rw.crewrite.proof
;; Reading the file took 1.22 seconds
;; Checking the proof took 18.75 seconds
;; VERIFY took 19.99 seconds
13728> DEFINE RW.FAST-FLAG-CREWRITE
;; Reading from Proofs/level10/admit-rw.fast-flag-crewrite.proofs
;; Reading the file took 1.71 seconds
;; Checking the proofs took 738.45 seconds
WARNING in RW.FAST-FLAG-CREWRITE :
variable HYPBOX is not used.
Misspelled or missing IGNORE declaration?
WARNING in RW.FAST-FLAG-CREWRITE :
variable HYPBOX is not used.
Misspelled or missing IGNORE declaration?
WARNING in RW.FAST-FLAG-CREWRITE :
variable HYPBOX is not used.
Misspelled or missing IGNORE declaration?
;; DEFINE took 744.36 seconds
13729> VERIFY RW.FAST-FLAG-CREWRITE
;; Reading from Proofs/level10/thm-rw.fast-flag-crewrite.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.66 seconds
;; VERIFY took 4.13 seconds
13730> VERIFY RW.FAST-FLAG-CREWRITE-OF-TERM-REDUCTION
;; Reading from Proofs/level10/thm-rw.fast-flag-crewrite-of-term-reduction.proof
;; Reading the file took 1.18 seconds
;; Checking the proof took 35.10 seconds
;; VERIFY took 36.29 seconds
13731> VERIFY RW.FAST-FLAG-CREWRITE-OF-LIST-REDUCTION
;; Reading from Proofs/level10/thm-rw.fast-flag-crewrite-of-list-reduction.proof
;; Reading the file took 1.43 seconds
;; Checking the proof took 26.54 seconds
;; VERIFY took 27.98 seconds
13732> VERIFY RW.FAST-FLAG-CREWRITE-OF-RULE-REDUCTION
;; Reading from Proofs/level10/thm-rw.fast-flag-crewrite-of-rule-reduction.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 25.96 seconds
;; VERIFY took 26.85 seconds
13733> VERIFY RW.FAST-FLAG-CREWRITE-OF-RULES-REDUCTION
;; Reading from Proofs/level10/thm-rw.fast-flag-crewrite-of-rules-reduction.proof
;; Reading the file took 1.25 seconds
;; Checking the proof took 26.49 seconds
;; VERIFY took 27.75 seconds
13734> VERIFY RW.FAST-FLAG-CREWRITE-OF-HYP-REDUCTION
;; Reading from Proofs/level10/thm-rw.fast-flag-crewrite-of-hyp-reduction.proof
;; Reading the file took 0.87 seconds
;; Checking the proof took 27.36 seconds
;; VERIFY took 28.24 seconds
13735> VERIFY RW.FAST-FLAG-CREWRITE-OF-HYPS-REDUCTION
;; Reading from Proofs/level10/thm-rw.fast-flag-crewrite-of-hyps-reduction.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 26.61 seconds
;; VERIFY took 27.50 seconds
13736> DEFINE RW.FAST-CREWRITE-CORE
;; Reading from Proofs/level10/admit-rw.fast-crewrite-core.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13737> VERIFY RW.FAST-CREWRITE-CORE
;; Reading from Proofs/level10/thm-rw.fast-crewrite-core.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.69 seconds
;; VERIFY took 3.91 seconds
13738> DEFINE RW.FAST-CREWRITE-CORE-LIST
;; Reading from Proofs/level10/admit-rw.fast-crewrite-core-list.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13739> VERIFY RW.FAST-CREWRITE-CORE-LIST
;; Reading from Proofs/level10/thm-rw.fast-crewrite-core-list.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.39 seconds
;; VERIFY took 3.62 seconds
13740> DEFINE RW.FAST-CREWRITE-TRY-RULE
;; Reading from Proofs/level10/admit-rw.fast-crewrite-try-rule.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13741> VERIFY RW.FAST-CREWRITE-TRY-RULE
;; Reading from Proofs/level10/thm-rw.fast-crewrite-try-rule.proof
;; Reading the file took 0.21 seconds
;; Checking the proof took 3.39 seconds
;; VERIFY took 3.61 seconds
13742> DEFINE RW.FAST-CREWRITE-TRY-RULES
;; Reading from Proofs/level10/admit-rw.fast-crewrite-try-rules.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13743> VERIFY RW.FAST-CREWRITE-TRY-RULES
;; Reading from Proofs/level10/thm-rw.fast-crewrite-try-rules.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.60 seconds
;; VERIFY took 3.83 seconds
13744> DEFINE RW.FAST-CREWRITE-TRY-MATCH
;; Reading from Proofs/level10/admit-rw.fast-crewrite-try-match.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13745> VERIFY RW.FAST-CREWRITE-TRY-MATCH
;; Reading from Proofs/level10/thm-rw.fast-crewrite-try-match.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.39 seconds
;; VERIFY took 3.62 seconds
13746> DEFINE RW.FAST-CREWRITE-TRY-MATCHES
;; Reading from Proofs/level10/admit-rw.fast-crewrite-try-matches.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13747> VERIFY RW.FAST-CREWRITE-TRY-MATCHES
;; Reading from Proofs/level10/thm-rw.fast-crewrite-try-matches.proof
;; Reading the file took 0.21 seconds
;; Checking the proof took 3.39 seconds
;; VERIFY took 3.62 seconds
13748> DEFINE RW.FAST-CREWRITE-RELIEVE-HYP
;; Reading from Proofs/level10/admit-rw.fast-crewrite-relieve-hyp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13749> VERIFY RW.FAST-CREWRITE-RELIEVE-HYP
;; Reading from Proofs/level10/thm-rw.fast-crewrite-relieve-hyp.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.60 seconds
;; VERIFY took 3.84 seconds
13750> DEFINE RW.FAST-CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/admit-rw.fast-crewrite-relieve-hyps.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13751> VERIFY RW.FAST-CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-rw.fast-crewrite-relieve-hyps.proof
;; Reading the file took 0.26 seconds
;; Checking the proof took 3.38 seconds
;; VERIFY took 3.65 seconds
13752> VERIFY RW.FAST-FLAG-CREWRITE-OF-TERM
;; Reading from Proofs/level10/thm-rw.fast-flag-crewrite-of-term.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 26.40 seconds
;; VERIFY took 27.31 seconds
13753> VERIFY RW.FAST-FLAG-CREWRITE-OF-LIST
;; Reading from Proofs/level10/thm-rw.fast-flag-crewrite-of-list.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 26.14 seconds
;; VERIFY took 27.03 seconds
13754> VERIFY RW.FAST-FLAG-CREWRITE-OF-RULE
;; Reading from Proofs/level10/thm-rw.fast-flag-crewrite-of-rule.proof
;; Reading the file took 1.23 seconds
;; Checking the proof took 26.23 seconds
;; VERIFY took 27.47 seconds
13755> VERIFY RW.FAST-FLAG-CREWRITE-OF-RULES
;; Reading from Proofs/level10/thm-rw.fast-flag-crewrite-of-rules.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 26.14 seconds
;; VERIFY took 27.04 seconds
13756> VERIFY RW.FAST-FLAG-CREWRITE-OF-MATCH
;; Reading from Proofs/level10/thm-rw.fast-flag-crewrite-of-match.proof
;; Reading the file took 1.21 seconds
;; Checking the proof took 25.99 seconds
;; VERIFY took 27.21 seconds
13757> VERIFY RW.FAST-FLAG-CREWRITE-OF-MATCHES
;; Reading from Proofs/level10/thm-rw.fast-flag-crewrite-of-matches.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 26.26 seconds
;; VERIFY took 27.15 seconds
13758> VERIFY RW.FAST-FLAG-CREWRITE-OF-HYP
;; Reading from Proofs/level10/thm-rw.fast-flag-crewrite-of-hyp.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 26.13 seconds
;; VERIFY took 27.05 seconds
13759> VERIFY RW.FAST-FLAG-CREWRITE-OF-HYPS
;; Reading from Proofs/level10/thm-rw.fast-flag-crewrite-of-hyps.proof
;; Reading the file took 1.22 seconds
;; Checking the proof took 26.15 seconds
;; VERIFY took 27.39 seconds
13760> VERIFY DEFINITION-OF-RW.FAST-CREWRITE-CORE
;; Reading from Proofs/level10/thm-definition-of-rw.fast-crewrite-core.proof
;; Reading the file took 2.33 seconds
;; Checking the proof took 509.04 seconds
;; VERIFY took 511.54 seconds
13761> VERIFY DEFINITION-OF-RW.FAST-CREWRITE-CORE-LIST
;; Reading from Proofs/level10/thm-definition-of-rw.fast-crewrite-core-list.proof
;; Reading the file took 1.21 seconds
;; Checking the proof took 69.56 seconds
;; VERIFY took 70.79 seconds
13762> VERIFY DEFINITION-OF-RW.FAST-CREWRITE-TRY-RULE
;; Reading from Proofs/level10/thm-definition-of-rw.fast-crewrite-try-rule.proof
;; Reading the file took 1.22 seconds
;; Checking the proof took 44.46 seconds
;; VERIFY took 45.69 seconds
13763> VERIFY DEFINITION-OF-RW.FAST-CREWRITE-TRY-RULES
;; Reading from Proofs/level10/thm-definition-of-rw.fast-crewrite-try-rules.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 69.06 seconds
;; VERIFY took 69.97 seconds
13764> VERIFY DEFINITION-OF-RW.FAST-CREWRITE-TRY-MATCH
;; Reading from Proofs/level10/thm-definition-of-rw.fast-crewrite-try-match.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 62.95 seconds
;; VERIFY took 63.87 seconds
13765> VERIFY DEFINITION-OF-RW.FAST-CREWRITE-TRY-MATCHES
;; Reading from Proofs/level10/thm-definition-of-rw.fast-crewrite-try-matches.proof
;; Reading the file took 1.23 seconds
;; Checking the proof took 68.78 seconds
;; VERIFY took 70.03 seconds
13766> VERIFY DEFINITION-OF-RW.FAST-CREWRITE-RELIEVE-HYP
;; Reading from Proofs/level10/thm-definition-of-rw.fast-crewrite-relieve-hyp.proof
;; Reading the file took 1.30 seconds
;; Checking the proof took 588.85 seconds
;; VERIFY took 590.24 seconds
13767> VERIFY DEFINITION-OF-RW.FAST-CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-definition-of-rw.fast-crewrite-relieve-hyps.proof
;; Reading the file took 0.95 seconds
;; Checking the proof took 67.73 seconds
;; VERIFY took 68.69 seconds
13768> VERIFY RW.FAST-CREWRITE-CORE-LIST-WHEN-NOT-CONSP
;; Reading from Proofs/level10/thm-rw.fast-crewrite-core-list-when-not-consp.proof
;; Reading the file took 1.23 seconds
;; Checking the proof took 26.47 seconds
;; VERIFY took 27.71 seconds
13769> VERIFY RW.FAST-CREWRITE-CORE-LIST-OF-CONS
;; Reading from Proofs/level10/thm-rw.fast-crewrite-core-list-of-cons.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 26.62 seconds
;; VERIFY took 27.51 seconds
13770> VERIFY LEN-OF-RW.FTRACES->RHSES-OF-RW.CRESULT->DATA-OF-RW.FAST-CREWRITE-CORE-LIST$
;; Reading from Proofs/level10/thm-len-of-rw.ftraces-_gt_rhses-of-rw.cresult-_gt_data-of-rw.fast-crewrite-core-list$.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 20.02 seconds
;; VERIFY took 20.92 seconds
13771> VERIFY RW.FAST-CREWRITE-TRY-RULES-WHEN-NOT-CONSP
;; Reading from Proofs/level10/thm-rw.fast-crewrite-try-rules-when-not-consp.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 26.39 seconds
;; VERIFY took 27.31 seconds
13772> VERIFY RW.FAST-CREWRITE-TRY-RULES-OF-CONS
;; Reading from Proofs/level10/thm-rw.fast-crewrite-try-rules-of-cons.proof
;; Reading the file took 1.22 seconds
;; Checking the proof took 26.36 seconds
;; VERIFY took 27.60 seconds
13773> VERIFY RW.FAST-CREWRITE-TRY-MATCHES-WHEN-NOT-CONSP
;; Reading from Proofs/level10/thm-rw.fast-crewrite-try-matches-when-not-consp.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 26.77 seconds
;; VERIFY took 27.67 seconds
13774> VERIFY RW.FAST-CREWRITE-TRY-MATCHES-OF-CONS
;; Reading from Proofs/level10/thm-rw.fast-crewrite-try-matches-of-cons.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 26.24 seconds
;; VERIFY took 27.16 seconds
13775> VERIFY RW.FAST-CREWRITE-RELIEVE-HYPS-WHEN-NOT-CONSP
;; Reading from Proofs/level10/thm-rw.fast-crewrite-relieve-hyps-when-not-consp.proof
;; Reading the file took 1.22 seconds
;; Checking the proof took 26.55 seconds
;; VERIFY took 27.78 seconds
13776> VERIFY RW.FAST-CREWRITE-RELIEVE-HYPS-OF-CONS
;; Reading from Proofs/level10/thm-rw.fast-crewrite-relieve-hyps-of-cons.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 26.23 seconds
;; VERIFY took 27.15 seconds
13777> VERIFY BOOLEANP-OF-RW.HYPRESULT->SUCCESSP-OF-RW.FAST-CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-booleanp-of-rw.hypresult-_gt_successp-of-rw.fast-crewrite-relieve-hyps.proof
;; Reading the file took 1.21 seconds
;; Checking the proof took 21.53 seconds
;; VERIFY took 22.75 seconds
13778> VERIFY LEMMA-FOR-FORCING-RW.FTRACEP-OF-RW.CRESULT->DATA-OF-RW.FAST-CREWRITE-CORE
;; Reading from Proofs/level10/thm-lemma-for-forcing-rw.ftracep-of-rw.cresult-_gt_data-of-rw.fast-crewrite-core.proof
;; Reading the file took 56.01 seconds
;; Checking the proof took 4831.21 seconds
;; VERIFY took 4888.75 seconds
13779> VERIFY FORCING-RW.FTRACEP-OF-RW.CRESULT->DATA-OF-RW.FAST-CREWRITE-CORE
;; Reading from Proofs/level10/thm-forcing-rw.ftracep-of-rw.cresult-_gt_data-of-rw.fast-crewrite-core.proof
;; Reading the file took 1.20 seconds
;; Checking the proof took 23.81 seconds
;; VERIFY took 25.03 seconds
13780> VERIFY FORCING-RW.FAST-CACHEP-OF-RW.CRESULT->CACHE-OF-RW.FAST-CREWRITE-CORE
;; Reading from Proofs/level10/thm-forcing-rw.fast-cachep-of-rw.cresult-_gt_cache-of-rw.fast-crewrite-core.proof
;; Reading the file took 1.23 seconds
;; Checking the proof took 23.79 seconds
;; VERIFY took 25.03 seconds
13781> VERIFY FORCING-RW.FTRACESP-OF-RW.CRESULT->DATA-OF-RW.FAST-CREWRITE-CORE-LIST
;; Reading from Proofs/level10/thm-forcing-rw.ftracesp-of-rw.cresult-_gt_data-of-rw.fast-crewrite-core-list.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 26.89 seconds
;; VERIFY took 27.82 seconds
13782> VERIFY FORCING-RW.FAST-CACHEP-OF-RW.CRESULT->CACHE-OF-RW.FAST-CREWRITE-CORE-LIST
;; Reading from Proofs/level10/thm-forcing-rw.fast-cachep-of-rw.cresult-_gt_cache-of-rw.fast-crewrite-core-list.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 26.47 seconds
;; VERIFY took 27.38 seconds
13783> VERIFY FORCING-RW.FTRACEP-OF-RW.CRESULT->DATA-OF-RW.FAST-CREWRITE-TRY-RULE
;; Reading from Proofs/level10/thm-forcing-rw.ftracep-of-rw.cresult-_gt_data-of-rw.fast-crewrite-try-rule.proof
;; Reading the file took 0.99 seconds
;; Checking the proof took 23.33 seconds
;; VERIFY took 24.34 seconds
13784> VERIFY FORCING-RW.FAST-CACHEP-OF-RW.CRESULT->CACHE-OF-RW.FAST-CREWRITE-TRY-RULE
;; Reading from Proofs/level10/thm-forcing-rw.fast-cachep-of-rw.cresult-_gt_cache-of-rw.fast-crewrite-try-rule.proof
;; Reading the file took 1.21 seconds
;; Checking the proof took 22.66 seconds
;; VERIFY took 23.89 seconds
13785> VERIFY FORCING-RW.FTRACEP-OF-RW.CRESULT->DATA-OF-RW.FAST-CREWRITE-TRY-RULES
;; Reading from Proofs/level10/thm-forcing-rw.ftracep-of-rw.cresult-_gt_data-of-rw.fast-crewrite-try-rules.proof
;; Reading the file took 1.19 seconds
;; Checking the proof took 24.39 seconds
;; VERIFY took 25.60 seconds
13786> VERIFY FORCING-RW.FAST-CACHEP-OF-RW.CRESULT->CACHE-OF-RW.FAST-CREWRITE-TRY-RULES
;; Reading from Proofs/level10/thm-forcing-rw.fast-cachep-of-rw.cresult-_gt_cache-of-rw.fast-crewrite-try-rules.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 24.00 seconds
;; VERIFY took 24.92 seconds
13787> VERIFY FORCING-RW.FTRACEP-OF-RW.CRESULT->DATA-OF-RW.FAST-CREWRITE-TRY-MATCH
;; Reading from Proofs/level10/thm-forcing-rw.ftracep-of-rw.cresult-_gt_data-of-rw.fast-crewrite-try-match.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 23.51 seconds
;; VERIFY took 24.44 seconds
13788> VERIFY FORCING-RW.FAST-CACHEP-OF-RW.CRESULT->CACHE-OF-RW.FAST-CREWRITE-TRY-MATCH
;; Reading from Proofs/level10/thm-forcing-rw.fast-cachep-of-rw.cresult-_gt_cache-of-rw.fast-crewrite-try-match.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 23.02 seconds
;; VERIFY took 23.94 seconds
13789> VERIFY FORCING-RW.FTRACEP-OF-RW.CRESULT->DATA-OF-RW.FAST-CREWRITE-TRY-MATCHES
;; Reading from Proofs/level10/thm-forcing-rw.ftracep-of-rw.cresult-_gt_data-of-rw.fast-crewrite-try-matches.proof
;; Reading the file took 1.22 seconds
;; Checking the proof took 23.26 seconds
;; VERIFY took 24.50 seconds
13790> VERIFY FORCING-RW.FAST-CACHEP-OF-RW.CRESULT->CACHE-OF-RW.FAST-CREWRITE-TRY-MATCHES
;; Reading from Proofs/level10/thm-forcing-rw.fast-cachep-of-rw.cresult-_gt_cache-of-rw.fast-crewrite-try-matches.proof
;; Reading the file took 1.18 seconds
;; Checking the proof took 23.12 seconds
;; VERIFY took 24.31 seconds
13791> VERIFY FORCING-RW.FTRACEP-OF-RW.CRESULT->DATA-OF-RW.FAST-CREWRITE-RELIEVE-HYP
;; Reading from Proofs/level10/thm-forcing-rw.ftracep-of-rw.cresult-_gt_data-of-rw.fast-crewrite-relieve-hyp.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 27.26 seconds
;; VERIFY took 28.19 seconds
13792> VERIFY FORCING-RW.FAST-CACHEP-OF-RW.CRESULT->CACHE-OF-RW.FAST-CREWRITE-RELIEVE-HYP
;; Reading from Proofs/level10/thm-forcing-rw.fast-cachep-of-rw.cresult-_gt_cache-of-rw.fast-crewrite-relieve-hyp.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 25.96 seconds
;; VERIFY took 26.89 seconds
13793> VERIFY FORCING-RW.FTRACESP-OF-RW.HYPRESULT->TRACES-OF-RW.FAST-CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-forcing-rw.ftracesp-of-rw.hypresult-_gt_traces-of-rw.fast-crewrite-relieve-hyps.proof
;; Reading the file took 1.23 seconds
;; Checking the proof took 26.98 seconds
;; VERIFY took 28.22 seconds
13794> VERIFY FORCING-RW.FAST-CACHEP-OF-RW.HYPRESULT->CACHE-OF-RW.FAST-CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-forcing-rw.fast-cachep-of-rw.hypresult-_gt_cache-of-rw.fast-crewrite-relieve-hyps.proof
;; Reading the file took 1.23 seconds
;; Checking the proof took 26.17 seconds
;; VERIFY took 27.42 seconds
13795> VERIFY LEMMA-FOR-RW.TRACE-FAST-IMAGE-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-lemma-for-rw.trace-fast-image-of-rw.crewrite-core.proof
;; Reading the file took 85.46 seconds
;; Checking the proof took 11475.87 seconds
;; VERIFY took 11563.62 seconds
13796> VERIFY RW.TRACE-FAST-IMAGE-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-rw.trace-fast-image-of-rw.crewrite-core.proof
;; Reading the file took 1.25 seconds
;; Checking the proof took 30.59 seconds
;; VERIFY took 31.86 seconds
13797> VERIFY RW.CACHE-FAST-IMAGE-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-rw.cache-fast-image-of-rw.crewrite-core.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 30.02 seconds
;; VERIFY took 30.95 seconds
13798> VERIFY RW.CRESULT->ALIMITEDP-OF-RW.CREWRITE-CORE
;; Reading from Proofs/level10/thm-rw.cresult-_gt_alimitedp-of-rw.crewrite-core.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 30.07 seconds
;; VERIFY took 30.99 seconds
13799> VERIFY RW.TRACE-LIST-FAST-IMAGE-OF-RW.CREWRITE-CORE-LIST
;; Reading from Proofs/level10/thm-rw.trace-list-fast-image-of-rw.crewrite-core-list.proof
;; Reading the file took 1.23 seconds
;; Checking the proof took 38.22 seconds
;; VERIFY took 39.46 seconds
13800> VERIFY RW.CACHE-FAST-IMAGE-OF-RW.CREWRITE-CORE-LIST
;; Reading from Proofs/level10/thm-rw.cache-fast-image-of-rw.crewrite-core-list.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 37.48 seconds
;; VERIFY took 38.41 seconds
13801> VERIFY RW.CRESULT->ALIMITEDP-OF-RW.CREWRITE-CORE-LIST
;; Reading from Proofs/level10/thm-rw.cresult-_gt_alimitedp-of-rw.crewrite-core-list.proof
;; Reading the file took 1.24 seconds
;; Checking the proof took 37.05 seconds
;; VERIFY took 38.31 seconds
13802> VERIFY RW.CREWRITE-TRY-RULE-UNDER-IFF
;; Reading from Proofs/level10/thm-rw.crewrite-try-rule-under-iff.proof
;; Reading the file took 0.93 seconds
;; Checking the proof took 28.95 seconds
;; VERIFY took 29.89 seconds
13803> VERIFY RW.TRACE-FAST-IMAGE-OF-RW.CREWRITE-TRY-RULE
;; Reading from Proofs/level10/thm-rw.trace-fast-image-of-rw.crewrite-try-rule.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 28.45 seconds
;; VERIFY took 29.36 seconds
13804> VERIFY RW.CACHE-FAST-IMAGE-OF-RW.CREWRITE-TRY-RULE
;; Reading from Proofs/level10/thm-rw.cache-fast-image-of-rw.crewrite-try-rule.proof
;; Reading the file took 1.18 seconds
;; Checking the proof took 28.15 seconds
;; VERIFY took 29.34 seconds
13805> VERIFY RW.CRESULT->ALIMITEDP-OF-RW.CREWRITE-TRY-RULE
;; Reading from Proofs/level10/thm-rw.cresult-_gt_alimitedp-of-rw.crewrite-try-rule.proof
;; Reading the file took 0.96 seconds
;; Checking the proof took 27.96 seconds
;; VERIFY took 28.93 seconds
13806> VERIFY RW.CREWRITE-TRY-RULES-UNDER-IFF
;; Reading from Proofs/level10/thm-rw.crewrite-try-rules-under-iff.proof
;; Reading the file took 1.23 seconds
;; Checking the proof took 31.22 seconds
;; VERIFY took 32.47 seconds
13807> VERIFY RW.TRACE-FAST-IMAGE-OF-RW.CREWRITE-TRY-RULES
;; Reading from Proofs/level10/thm-rw.trace-fast-image-of-rw.crewrite-try-rules.proof
;; Reading the file took 0.93 seconds
;; Checking the proof took 30.79 seconds
;; VERIFY took 31.74 seconds
13808> VERIFY RW.CACHE-FAST-IMAGE-OF-RW.CREWRITE-TRY-RULES
;; Reading from Proofs/level10/thm-rw.cache-fast-image-of-rw.crewrite-try-rules.proof
;; Reading the file took 1.17 seconds
;; Checking the proof took 29.49 seconds
;; VERIFY took 30.67 seconds
13809> VERIFY RW.CRESULT->ALIMITEDP-OF-RW.CREWRITE-TRY-RULES
;; Reading from Proofs/level10/thm-rw.cresult-_gt_alimitedp-of-rw.crewrite-try-rules.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 30.55 seconds
;; VERIFY took 31.47 seconds
13810> VERIFY RW.CREWRITE-TRY-MATCH-UNDER-IFF
;; Reading from Proofs/level10/thm-rw.crewrite-try-match-under-iff.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 29.33 seconds
;; VERIFY took 30.26 seconds
13811> VERIFY RW.TRACE-FAST-IMAGE-OF-RW.CREWRITE-TRY-MATCH
;; Reading from Proofs/level10/thm-rw.trace-fast-image-of-rw.crewrite-try-match.proof
;; Reading the file took 1.21 seconds
;; Checking the proof took 29.00 seconds
;; VERIFY took 30.23 seconds
13812> VERIFY RW.CACHE-FAST-IMAGE-OF-RW.CREWRITE-TRY-MATCH
;; Reading from Proofs/level10/thm-rw.cache-fast-image-of-rw.crewrite-try-match.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 28.56 seconds
;; VERIFY took 29.50 seconds
13813> VERIFY RW.CRESULT->ALIMITEDP-OF-RW.CREWRITE-TRY-MATCH
;; Reading from Proofs/level10/thm-rw.cresult-_gt_alimitedp-of-rw.crewrite-try-match.proof
;; Reading the file took 1.29 seconds
;; Checking the proof took 28.35 seconds
;; VERIFY took 29.66 seconds
13814> VERIFY RW.CREWRITE-TRY-MATCHES-UNDER-IFF
;; Reading from Proofs/level10/thm-rw.crewrite-try-matches-under-iff.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 29.27 seconds
;; VERIFY took 30.21 seconds
13815> VERIFY RW.TRACE-FAST-IMAGE-OF-RW.CREWRITE-TRY-MATCHES
;; Reading from Proofs/level10/thm-rw.trace-fast-image-of-rw.crewrite-try-matches.proof
;; Reading the file took 1.21 seconds
;; Checking the proof took 28.95 seconds
;; VERIFY took 30.19 seconds
13816> VERIFY RW.CACHE-FAST-IMAGE-OF-RW.CREWRITE-TRY-MATCHES
;; Reading from Proofs/level10/thm-rw.cache-fast-image-of-rw.crewrite-try-matches.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 28.42 seconds
;; VERIFY took 29.34 seconds
13817> VERIFY RW.CRESULT->ALIMITEDP-OF-RW.CREWRITE-TRY-MATCHES
;; Reading from Proofs/level10/thm-rw.cresult-_gt_alimitedp-of-rw.crewrite-try-matches.proof
;; Reading the file took 1.17 seconds
;; Checking the proof took 28.37 seconds
;; VERIFY took 29.56 seconds
13818> VERIFY RW.CREWRITE-RELIEVE-HYP-UNDER-IFF
;; Reading from Proofs/level10/thm-rw.crewrite-relieve-hyp-under-iff.proof
;; Reading the file took 0.98 seconds
;; Checking the proof took 40.08 seconds
;; VERIFY took 41.07 seconds
13819> VERIFY RW.TRACE-FAST-IMAGE-OF-RW.CREWRITE-RELIEVE-HYP
;; Reading from Proofs/level10/thm-rw.trace-fast-image-of-rw.crewrite-relieve-hyp.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 37.99 seconds
;; VERIFY took 38.92 seconds
13820> VERIFY RW.CACHE-FAST-IMAGE-OF-RW.CREWRITE-RELIEVE-HYP
;; Reading from Proofs/level10/thm-rw.cache-fast-image-of-rw.crewrite-relieve-hyp.proof
;; Reading the file took 1.22 seconds
;; Checking the proof took 37.48 seconds
;; VERIFY took 38.71 seconds
13821> VERIFY RW.CRESULT->ALIMITEDP-OF-RW.CREWRITE-RELIEVE-HYP
;; Reading from Proofs/level10/thm-rw.cresult-_gt_alimitedp-of-rw.crewrite-relieve-hyp.proof
;; Reading the file took 1.21 seconds
;; Checking the proof took 37.14 seconds
;; VERIFY took 38.37 seconds
13822> VERIFY RW.HYPRESULT->SUCCESSP-OF-RW.CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-rw.hypresult-_gt_successp-of-rw.crewrite-relieve-hyps.proof
;; Reading the file took 0.95 seconds
;; Checking the proof took 40.49 seconds
;; VERIFY took 41.46 seconds
13823> VERIFY RW.TRACE-LIST-FAST-IMAGE-OF-RW.CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-rw.trace-list-fast-image-of-rw.crewrite-relieve-hyps.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 38.77 seconds
;; VERIFY took 39.70 seconds
13824> VERIFY RW.CACHE-FAST-IMAGE-OF-RW.CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-rw.cache-fast-image-of-rw.crewrite-relieve-hyps.proof
;; Reading the file took 1.21 seconds
;; Checking the proof took 37.90 seconds
;; VERIFY took 39.13 seconds
13825> VERIFY RW.HYPRESULT->ALIMITEDP-OF-RW.CREWRITE-RELIEVE-HYPS
;; Reading from Proofs/level10/thm-rw.hypresult-_gt_alimitedp-of-rw.crewrite-relieve-hyps.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 37.60 seconds
;; VERIFY took 38.53 seconds
13826> VERIFY RW.FTRACE->RHS-OF-RW.FAST-CREWRITE-CORE
;; Reading from Proofs/level10/thm-rw.ftrace-_gt_rhs-of-rw.fast-crewrite-core.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 27.15 seconds
;; VERIFY took 28.06 seconds
13827> DEFINE RW.FAST-CREWRITE
;; Reading from Proofs/level10/admit-rw.fast-crewrite.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13828> VERIFY RW.FAST-CREWRITE
;; Reading from Proofs/level10/thm-rw.fast-crewrite.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.41 seconds
;; VERIFY took 3.64 seconds
13829> VERIFY RW.FTRACEP-OF-RW.FAST-CREWRITE
;; Reading from Proofs/level10/thm-rw.ftracep-of-rw.fast-crewrite.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 26.63 seconds
;; VERIFY took 27.54 seconds
13830> VERIFY RW.TRACE-FAST-IMAGE-OF-RW.CREWRITE
;; Reading from Proofs/level10/thm-rw.trace-fast-image-of-rw.crewrite.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 26.61 seconds
;; VERIFY took 27.51 seconds
13831> VERIFY RW.FTRACE->RHS-OF-RW.FAST-CREWRITE
;; Reading from Proofs/level10/thm-rw.ftrace-_gt_rhs-of-rw.fast-crewrite.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 26.86 seconds
;; VERIFY took 27.75 seconds
13832> VERIFY RW.FTRACE->FGOALS-OF-RW.FAST-CREWRITE
;; Reading from Proofs/level10/thm-rw.ftrace-_gt_fgoals-of-rw.fast-crewrite.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 26.74 seconds
;; VERIFY took 27.64 seconds
13833> VERIFY RW.CCSTEP->CLAUSE-PRIME-UNDER-IFF
;; Reading from Proofs/level10/thm-rw.ccstep-_gt_clause-prime-under-iff.proof
;; Reading the file took 0.87 seconds
;; Checking the proof took 26.18 seconds
;; VERIFY took 27.06 seconds
13834> VERIFY FORCING-RW.EQTRACE-OKP-OF-RW.ASSMS->CONTRADICTION-AND-RW.ASSMS->HYPBOX-FREE
;; Reading from Proofs/level10/thm-forcing-rw.eqtrace-okp-of-rw.assms-_gt_contradiction-and-rw.assms-_gt_hypbox-free.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 18.52 seconds
;; VERIFY took 19.44 seconds
13835> VERIFY FORCING-RW.EQTRACE-ATBLP-OF-RW.ASSMS->CONTRADICTION-OF-RW.ASSUME-RIGHT
;; Reading from Proofs/level10/thm-forcing-rw.eqtrace-atblp-of-rw.assms-_gt_contradiction-of-rw.assume-right.proof
;; Reading the file took 1.17 seconds
;; Checking the proof took 26.07 seconds
;; VERIFY took 27.26 seconds
13836> VERIFY FORCING-RW.EQTRACE-ATBLP-OF-RW.ASSMS->CONTRADICTION-OF-RW.ASSUME-RIGHT-LIST
;; Reading from Proofs/level10/thm-forcing-rw.eqtrace-atblp-of-rw.assms-_gt_contradiction-of-rw.assume-right-list.proof
;; Reading the file took 1.27 seconds
;; Checking the proof took 25.07 seconds
;; VERIFY took 26.36 seconds
13837> VERIFY FORCING-RW.EQTRACE-ATBLP-OF-RW.ASSMS->CONTRADICTION-OF-RW.ASSUME-LEFT
;; Reading from Proofs/level10/thm-forcing-rw.eqtrace-atblp-of-rw.assms-_gt_contradiction-of-rw.assume-left.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 26.28 seconds
;; VERIFY took 27.19 seconds
13838> VERIFY FORCING-RW.EQTRACE-ATBLP-OF-RW.ASSMS->CONTRADICTION-OF-RW.ASSUME-LEFT-LIST
;; Reading from Proofs/level10/thm-forcing-rw.eqtrace-atblp-of-rw.assms-_gt_contradiction-of-rw.assume-left-list.proof
;; Reading the file took 0.94 seconds
;; Checking the proof took 24.99 seconds
;; VERIFY took 25.95 seconds
13839> DEFINE RW.CREWRITE-TAKE-STEP
;; Reading from Proofs/level10/admit-rw.crewrite-take-step.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
13840> VERIFY RW.CREWRITE-TAKE-STEP
;; Reading from Proofs/level10/thm-rw.crewrite-take-step.proof
;; Reading the file took 0.20 seconds
;; Checking the proof took 3.62 seconds
;; VERIFY took 3.84 seconds
13841> VERIFY FORCING-RW.CCSTEPP-OF-RW.CREWRITE-TAKE-STEP
;; Reading from Proofs/level10/thm-forcing-rw.ccstepp-of-rw.crewrite-take-step.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 21.18 seconds
;; VERIFY took 22.09 seconds
13842> VERIFY FORCING-RW.TRACE-OKP-OF-RW.CCSTEP->TRACE-OF-RW.CREWRITE-TAKE-STEP
;; Reading from Proofs/level10/thm-forcing-rw.trace-okp-of-rw.ccstep-_gt_trace-of-rw.crewrite-take-step.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 18.90 seconds
;; VERIFY took 19.80 seconds
13843> VERIFY FORCING-RW.TRACE-ATBLP-OF-RW.CCSTEP->TRACE-OF-RW.CREWRITE-TAKE-STEP
;; Reading from Proofs/level10/thm-forcing-rw.trace-atblp-of-rw.ccstep-_gt_trace-of-rw.crewrite-take-step.proof
;; Reading the file took 1.18 seconds
;; Checking the proof took 19.27 seconds
;; VERIFY took 20.47 seconds
13844> VERIFY FORCING-RW.CCSTEP-TRACE-ENV-OKP-OF-RW.CCSTEP->TRACE-OF-RW.CREWRITE-TAKE-STEP
;; Reading from Proofs/level10/thm-forcing-rw.ccstep-trace-env-okp-of-rw.ccstep-_gt_trace-of-rw.crewrite-take-step.proof
;; Reading the file took 0.87 seconds
;; Checking the proof took 19.20 seconds
;; VERIFY took 20.10 seconds
13845> VERIFY FORCING-RW.EQTRACE-ATBLP-OF-RW.CCSTEP->CONTRADICTION-OF-RW.CREWRITE-TAKE-STEP
;; Reading from Proofs/level10/thm-forcing-rw.eqtrace-atblp-of-rw.ccstep-_gt_contradiction-of-rw.crewrite-take-step.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 19.15 seconds
;; VERIFY took 20.07 seconds
13846> VERIFY FORCING-LOGIC.TERM-ATBLP-OF-RW.CCSTEP->TERM-OF-RW.CREWRITE-TAKE-STEP
;; Reading from Proofs/level10/thm-forcing-logic.term-atblp-of-rw.ccstep-_gt_term-of-rw.crewrite-take-step.proof
;; Reading the file took 1.18 seconds
;; Checking the proof took 18.76 seconds
;; VERIFY took 19.96 seconds
13847> VERIFY FORCING-RW.HYPBOX-ATBLP-OF-RW.CCSTEP->HYPBOX-OF-RW.CREWRITE-TAKE-STEP
;; Reading from Proofs/level10/thm-forcing-rw.hypbox-atblp-of-rw.ccstep-_gt_hypbox-of-rw.crewrite-take-step.proof
;; Reading the file took 0.87 seconds
;; Checking the proof took 18.89 seconds
;; VERIFY took 19.78 seconds
13848> DEFINE RW.CREWRITE-CLAUSE-AUX
;; Reading from Proofs/level10/admit-rw.crewrite-clause-aux.proofs
;; Reading the file took 1.18 seconds
;; Checking the proofs took 37.56 seconds
;; DEFINE took 38.80 seconds
13849> VERIFY RW.CREWRITE-CLAUSE-AUX
;; Reading from Proofs/level10/thm-rw.crewrite-clause-aux.proof
;; Reading the file took 0.20 seconds
;; Checking the proof took 3.37 seconds
;; VERIFY took 3.58 seconds
13850> VERIFY FORCING-RW.CCSTEP-LISTP-OF-RW.CREWRITE-CLAUSE-AUX
;; Reading from Proofs/level10/thm-forcing-rw.ccstep-listp-of-rw.crewrite-clause-aux.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 21.91 seconds
;; VERIFY took 22.81 seconds
13851> VERIFY FORCING-RW.TRACE-LIST-OKP-OF-RW.CCSTEP-LIST-GATHER-TRACES-OF-RW.CREWRITE-CLAUSE-AUX
;; Reading from Proofs/level10/thm-forcing-rw.trace-list-okp-of-rw.ccstep-list-gather-traces-of-rw.crewrite-clause-aux.proof
;; Reading the file took 1.21 seconds
;; Checking the proof took 22.99 seconds
;; VERIFY took 24.21 seconds
13852> VERIFY FORCING-RW.TRACE-LIST-ATBLP-OF-RW.CCSTEP-LIST-GATHER-TRACES-OF-RW.CREWRITE-CLAUSE-AUX
;; Reading from Proofs/level10/thm-forcing-rw.trace-list-atblp-of-rw.ccstep-list-gather-traces-of-rw.crewrite-clause-aux.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 27.05 seconds
;; VERIFY took 27.97 seconds
13853> VERIFY FORCING-RW.TRACE-LIST-ENV-OKP-OF-RW.CCSTEP-LIST-GATHER-TRACES-OF-RW.CREWRITE-CLAUSE-AUX
;; Reading from Proofs/level10/thm-forcing-rw.trace-list-env-okp-of-rw.ccstep-list-gather-traces-of-rw.crewrite-clause-aux.proof
;; Reading the file took 0.95 seconds
;; Checking the proof took 29.21 seconds
;; VERIFY took 30.19 seconds
13854> VERIFY LEMMA-FOR-FORCING-RW.CCSTEP-LIST->COMPATIBLEP-OF-RW.CREWRITE-CLAUSE-AUX
;; Reading from Proofs/level10/thm-lemma-for-forcing-rw.ccstep-list-_gt_compatiblep-of-rw.crewrite-clause-aux.proof
;; Reading the file took 1.21 seconds
;; Checking the proof took 31.58 seconds
;; VERIFY took 32.81 seconds
13855> VERIFY FORCING-RW.CCSTEP-LIST->COMPATIBLEP-OF-RW.CREWRITE-CLAUSE-AUX
;; Reading from Proofs/level10/thm-forcing-rw.ccstep-list-_gt_compatiblep-of-rw.crewrite-clause-aux.proof
;; Reading the file took 1.22 seconds
;; Checking the proof took 46.32 seconds
;; VERIFY took 47.57 seconds
13856> VERIFY FORCING-RW.CCSTEP-LIST->ORIGINAL-GOAL-OF-RW.CREWRITE-CLAUSE-AUX
;; Reading from Proofs/level10/thm-forcing-rw.ccstep-list-_gt_original-goal-of-rw.crewrite-clause-aux.proof
;; Reading the file took 1.29 seconds
;; Checking the proof took 57.04 seconds
;; VERIFY took 58.35 seconds
13857> VERIFY CONSP-OF-RW.CREWRITE-CLAUSE-AUX
;; Reading from Proofs/level10/thm-consp-of-rw.crewrite-clause-aux.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 30.04 seconds
;; VERIFY took 30.94 seconds
13858> VERIFY LEMMA-FOR-FORCING-RW.CCSTEP->TERMINALP-OF-CAR-OF-RW.CREWRITE-CLAUSE-AUX
;; Reading from Proofs/level10/thm-lemma-for-forcing-rw.ccstep-_gt_terminalp-of-car-of-rw.crewrite-clause-aux.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 26.70 seconds
;; VERIFY took 27.59 seconds
13859> VERIFY FORCING-RW.CCSTEP->TERMINALP-OF-CAR-OF-RW.CREWRITE-CLAUSE-AUX
;; Reading from Proofs/level10/thm-forcing-rw.ccstep-_gt_terminalp-of-car-of-rw.crewrite-clause-aux.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 55.93 seconds
;; VERIFY took 56.87 seconds
13860> VERIFY FORCING-RW.EQTRACE-LIST-ATBLP-OF-RW.CCSTEP-LIST-GATHER-CONTRADICTIONS-OF-RW.CREWRITE-CLAUSE-AUX
;; Reading from Proofs/level10/thm-forcing-rw.eqtrace-list-atblp-of-rw.ccstep-list-gather-contradictions-of-rw.crewrite-clause-aux.proof
;; Reading the file took 1.27 seconds
;; Checking the proof took 41.14 seconds
;; VERIFY took 42.43 seconds
13861> VERIFY FORCING-LOGIC.TERM-LIST-ATBLP-OF-RW.CCSTEP-LIST-TERMS-OF-RW.CREWRITE-CLAUSE-AUX
;; Reading from Proofs/level10/thm-forcing-logic.term-list-atblp-of-rw.ccstep-list-terms-of-rw.crewrite-clause-aux.proof
;; Reading the file took 1.25 seconds
;; Checking the proof took 38.50 seconds
;; VERIFY took 39.77 seconds
13862> VERIFY FORCING-RW.HYPBOX-LIST-ATBLP-OF-RW.CCSTEP-LIST-HYPBOXES-OF-RW.CREWRITE-CLAUSE-AUX
;; Reading from Proofs/level10/thm-forcing-rw.hypbox-list-atblp-of-rw.ccstep-list-hypboxes-of-rw.crewrite-clause-aux.proof
;; Reading the file took 1.30 seconds
;; Checking the proof took 42.59 seconds
;; VERIFY took 43.91 seconds
13863> DEFINE RW.CREWRITE-CLAUSE
;; Reading from Proofs/level10/admit-rw.crewrite-clause.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13864> VERIFY RW.CREWRITE-CLAUSE
;; Reading from Proofs/level10/thm-rw.crewrite-clause.proof
;; Reading the file took 0.20 seconds
;; Checking the proof took 3.37 seconds
;; VERIFY took 3.59 seconds
13865> VERIFY FORCING-RW.CCSTEP-LISTP-OF-RW.CREWRITE-CLAUSE
;; Reading from Proofs/level10/thm-forcing-rw.ccstep-listp-of-rw.crewrite-clause.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 18.59 seconds
;; VERIFY took 19.49 seconds
13866> VERIFY FORCING-RW.CCSTEP-LISTP-OF-RW.CREWRITE-CLAUSE-FREE
;; Reading from Proofs/level10/thm-forcing-rw.ccstep-listp-of-rw.crewrite-clause-free.proof
;; Reading the file took 1.18 seconds
;; Checking the proof took 18.74 seconds
;; VERIFY took 19.94 seconds
13867> VERIFY FORCING-RW.TRACE-LIST-OKP-OF-RW.CCSTEP-LIST-GATHER-TRACES-OF-RW.CREWRITE-CLAUSE
;; Reading from Proofs/level10/thm-forcing-rw.trace-list-okp-of-rw.ccstep-list-gather-traces-of-rw.crewrite-clause.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 18.63 seconds
;; VERIFY took 19.52 seconds
13868> VERIFY FORCING-RW.TRACE-LIST-OKP-OF-RW.CCSTEP-LIST-GATHER-TRACES-OF-RW.CREWRITE-CLAUSE-FREE
;; Reading from Proofs/level10/thm-forcing-rw.trace-list-okp-of-rw.ccstep-list-gather-traces-of-rw.crewrite-clause-free.proof
;; Reading the file took 1.19 seconds
;; Checking the proof took 18.79 seconds
;; VERIFY took 20.00 seconds
13869> VERIFY FORCING-RW.TRACE-LIST-ATBLP-OF-RW.CCSTEP-LIST-GATHER-TRACES-OF-RW.CREWRITE-CLAUSE
;; Reading from Proofs/level10/thm-forcing-rw.trace-list-atblp-of-rw.ccstep-list-gather-traces-of-rw.crewrite-clause.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 18.73 seconds
;; VERIFY took 19.64 seconds
13870> VERIFY FORCING-RW.TRACE-LIST-ATBLP-OF-RW.CCSTEP-LIST-GATHER-TRACES-OF-RW.CREWRITE-CLAUSE-FREE
;; Reading from Proofs/level10/thm-forcing-rw.trace-list-atblp-of-rw.ccstep-list-gather-traces-of-rw.crewrite-clause-free.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 18.68 seconds
;; VERIFY took 19.59 seconds
13871> VERIFY FORCING-RW.TRACE-LIST-ENV-OKP-OF-RW.CCSTEP-LIST-GATHER-TRACES-OF-RW.CREWRITE-CLAUSE
;; Reading from Proofs/level10/thm-forcing-rw.trace-list-env-okp-of-rw.ccstep-list-gather-traces-of-rw.crewrite-clause.proof
;; Reading the file took 1.18 seconds
;; Checking the proof took 18.80 seconds
;; VERIFY took 20.00 seconds
13872> VERIFY FORCING-RW.TRACE-LIST-ENV-OKP-OF-RW.CCSTEP-LIST-GATHER-TRACES-OF-RW.CREWRITE-CLAUSE-FREE
;; Reading from Proofs/level10/thm-forcing-rw.trace-list-env-okp-of-rw.ccstep-list-gather-traces-of-rw.crewrite-clause-free.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 18.86 seconds
;; VERIFY took 19.76 seconds
13873> VERIFY FORCING-RW.CCSTEP-LIST->COMPATIBLEP-OF-RW.CREWRITE-CLAUSE
;; Reading from Proofs/level10/thm-forcing-rw.ccstep-list-_gt_compatiblep-of-rw.crewrite-clause.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 18.66 seconds
;; VERIFY took 19.55 seconds
13874> VERIFY LEMMA-FOR-FORCING-RW.CCSTEP-LIST->ORIGINAL-GOAL-OF-RW.CREWRITE-CLAUSE
;; Reading from Proofs/level10/thm-lemma-for-forcing-rw.ccstep-list-_gt_original-goal-of-rw.crewrite-clause.proof
;; Reading the file took 1.20 seconds
;; Checking the proof took 26.99 seconds
;; VERIFY took 28.20 seconds
13875> VERIFY FORCING-RW.CCSTEP-LIST->ORIGINAL-GOAL-OF-RW.CREWRITE-CLAUSE
;; Reading from Proofs/level10/thm-forcing-rw.ccstep-list-_gt_original-goal-of-rw.crewrite-clause.proof
;; Reading the file took 1.20 seconds
;; Checking the proof took 26.09 seconds
;; VERIFY took 27.31 seconds
13876> VERIFY FORCING-CONSP-OF-RW.CREWRITE-CLAUSE
;; Reading from Proofs/level10/thm-forcing-consp-of-rw.crewrite-clause.proof
;; Reading the file took 1.20 seconds
;; Checking the proof took 18.77 seconds
;; VERIFY took 19.98 seconds
13877> VERIFY FORCING-RW.CCSTEP->RESULT-GOAL-OF-CAR-OF-CDR-OF-RW.CREWRITE-CLAUSE
;; Reading from Proofs/level10/thm-forcing-rw.ccstep-_gt_result-goal-of-car-of-cdr-of-rw.crewrite-clause.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 18.93 seconds
;; VERIFY took 19.83 seconds
13878> VERIFY FORCING-RW.CCSTEP->TERMINALP-OF-CAR-OF-RW.CREWRITE-CLAUSE
;; Reading from Proofs/level10/thm-forcing-rw.ccstep-_gt_terminalp-of-car-of-rw.crewrite-clause.proof
;; Reading the file took 1.19 seconds
;; Checking the proof took 18.77 seconds
;; VERIFY took 19.98 seconds
13879> VERIFY FORCING-RW.EQTRACE-LIST-ATBLP-OF-RW.CCSTEP-LIST-GATHER-CONTRADICTIONS-OF-RW.CREWRITE-CLAUSE
;; Reading from Proofs/level10/thm-forcing-rw.eqtrace-list-atblp-of-rw.ccstep-list-gather-contradictions-of-rw.crewrite-clause.proof
;; Reading the file took 0.93 seconds
;; Checking the proof took 18.75 seconds
;; VERIFY took 19.71 seconds
13880> VERIFY FORCING-LOGIC.TERM-LIST-ATBLP-OF-RW.CCSTEP-LIST-TERMS-OF-RW.CREWRITE-CLAUSE
;; Reading from Proofs/level10/thm-forcing-logic.term-list-atblp-of-rw.ccstep-list-terms-of-rw.crewrite-clause.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 18.65 seconds
;; VERIFY took 19.55 seconds
13881> VERIFY FORCING-RW.HYPBOX-LIST-ATBLP-OF-RW.CCSTEP-LIST-HYPBOXES-OF-RW.CREWRITE-CLAUSE
;; Reading from Proofs/level10/thm-forcing-rw.hypbox-list-atblp-of-rw.ccstep-list-hypboxes-of-rw.crewrite-clause.proof
;; Reading the file took 1.18 seconds
;; Checking the proof took 18.75 seconds
;; VERIFY took 19.94 seconds
13882> DEFINE RW.CREWRITE-CLAUSE-BLDR
;; Reading from Proofs/level10/admit-rw.crewrite-clause-bldr.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13883> VERIFY RW.CREWRITE-CLAUSE-BLDR
;; Reading from Proofs/level10/thm-rw.crewrite-clause-bldr.proof
;; Reading the file took 0.19 seconds
;; Checking the proof took 3.35 seconds
;; VERIFY took 3.55 seconds
13884> VERIFY FORCING-LOGIC.APPEALP-OF-RW.CREWRITE-CLAUSE-BLDR
;; Reading from Proofs/level10/thm-forcing-logic.appealp-of-rw.crewrite-clause-bldr.proof
;; Reading the file took 1.08 seconds
;; Checking the proof took 18.96 seconds
;; VERIFY took 20.08 seconds
13885> VERIFY FORCING-LOGIC.CONCLUSION-OF-RW.CREWRITE-CLAUSE-BLDR
;; Reading from Proofs/level10/thm-forcing-logic.conclusion-of-rw.crewrite-clause-bldr.proof
;; Reading the file took 1.19 seconds
;; Checking the proof took 19.58 seconds
;; VERIFY took 20.79 seconds
13886> VERIFY FORCING-LOGIC.PROOFP-OF-RW.CREWRITE-CLAUSE-BLDR
;; Reading from Proofs/level10/thm-forcing-logic.proofp-of-rw.crewrite-clause-bldr.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 20.81 seconds
;; VERIFY took 21.83 seconds
13887> DEFINE RW.CREWRITE-CLAUSE-LIST
;; Reading from Proofs/level10/admit-rw.crewrite-clause-list.proofs
;; Reading the file took 1.17 seconds
;; Checking the proofs took 37.70 seconds
;; DEFINE took 38.88 seconds
13888> VERIFY RW.CREWRITE-CLAUSE-LIST
;; Reading from Proofs/level10/thm-rw.crewrite-clause-list.proof
;; Reading the file took 0.21 seconds
;; Checking the proof took 3.37 seconds
;; VERIFY took 3.60 seconds
13889> DEFINE RW.FAST-CREWRITE-CLAUSE-LIST$
;; Reading from Proofs/level10/admit-rw.fast-crewrite-clause-list$.proofs
;; Reading the file took 0.87 seconds
;; Checking the proofs took 37.44 seconds
;; DEFINE took 38.32 seconds
13890> VERIFY RW.FAST-CREWRITE-CLAUSE-LIST$
;; Reading from Proofs/level10/thm-rw.fast-crewrite-clause-list$.proof
;; Reading the file took 0.20 seconds
;; Checking the proof took 3.64 seconds
;; VERIFY took 3.86 seconds
13891> VERIFY RW.CREWRITE-CLAUSE-LIST-WHEN-NOT-CONSP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-list-when-not-consp.proof
;; Reading the file took 0.87 seconds
;; Checking the proof took 26.49 seconds
;; VERIFY took 27.37 seconds
13892> VERIFY RW.CREWRITE-CLAUSE-LIST-OF-CONS
;; Reading from Proofs/level10/thm-rw.crewrite-clause-list-of-cons.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 26.48 seconds
;; VERIFY took 27.40 seconds
13893> VERIFY TRUE-LISTP-OF-RW.CREWRITE-CLAUSE-LIST
;; Reading from Proofs/level10/thm-true-listp-of-rw.crewrite-clause-list.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 19.56 seconds
;; VERIFY took 20.48 seconds
13894> VERIFY LEN-OF-RW.CREWRITE-CLAUSE-LIST
;; Reading from Proofs/level10/thm-len-of-rw.crewrite-clause-list.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 19.62 seconds
;; VERIFY took 20.52 seconds
13895> VERIFY CONSP-OF-RW.CREWRITE-CLAUSE-LIST
;; Reading from Proofs/level10/thm-consp-of-rw.crewrite-clause-list.proof
;; Reading the file took 1.19 seconds
;; Checking the proof took 19.93 seconds
;; VERIFY took 21.13 seconds
13896> VERIFY CAR-OF-RW.CREWRITE-CLAUSE-LIST
;; Reading from Proofs/level10/thm-car-of-rw.crewrite-clause-list.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 18.87 seconds
;; VERIFY took 19.76 seconds
13897> VERIFY CDR-OF-RW.CREWRITE-CLAUSE-LIST
;; Reading from Proofs/level10/thm-cdr-of-rw.crewrite-clause-list.proof
;; Reading the file took 1.18 seconds
;; Checking the proof took 18.69 seconds
;; VERIFY took 19.88 seconds
13898> VERIFY RW.CREWRITE-CLAUSE-LIST-UNDER-IFF
;; Reading from Proofs/level10/thm-rw.crewrite-clause-list-under-iff.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 18.82 seconds
;; VERIFY took 19.73 seconds
13899> VERIFY RW.CREWRITE-CLAUSE-LIST-OF-LIST-FIX
;; Reading from Proofs/level10/thm-rw.crewrite-clause-list-of-list-fix.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 19.45 seconds
;; VERIFY took 20.35 seconds
13900> VERIFY RW.CREWRITE-CLAUSE-LIST-OF-APP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-list-of-app.proof
;; Reading the file took 1.17 seconds
;; Checking the proof took 19.65 seconds
;; VERIFY took 20.83 seconds
13901> VERIFY REV-OF-RW.CREWRITE-CLAUSE-LIST
;; Reading from Proofs/level10/thm-rev-of-rw.crewrite-clause-list.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 19.89 seconds
;; VERIFY took 20.81 seconds
13902> VERIFY RW.CREWRITE-CLAUSE-LIST-OF-REV
;; Reading from Proofs/level10/thm-rw.crewrite-clause-list-of-rev.proof
;; Reading the file took 0.87 seconds
;; Checking the proof took 18.63 seconds
;; VERIFY took 19.52 seconds
13903> VERIFY FIRSTN-OF-RW.CREWRITE-CLAUSE-LIST
;; Reading from Proofs/level10/thm-firstn-of-rw.crewrite-clause-list.proof
;; Reading the file took 1.17 seconds
;; Checking the proof took 27.57 seconds
;; VERIFY took 28.75 seconds
13904> VERIFY RESTN-OF-RW.CREWRITE-CLAUSE-LIST
;; Reading from Proofs/level10/thm-restn-of-rw.crewrite-clause-list.proof
;; Reading the file took 1.17 seconds
;; Checking the proof took 26.94 seconds
;; VERIFY took 28.11 seconds
13905> VERIFY MEMBERP-OF-RW.CREWRITE-CLAUSE-IN-RW.CREWRITE-CLAUSE-LIST-WHEN-MEMBERP
;; Reading from Proofs/level10/thm-memberp-of-rw.crewrite-clause-in-rw.crewrite-clause-list-when-memberp.proof
;; Reading the file took 1.20 seconds
;; Checking the proof took 19.81 seconds
;; VERIFY took 21.02 seconds
13906> VERIFY SUBSETP-OF-RW.CREWRITE-CLAUSE-LISTS-WHEN-SUBSETP
;; Reading from Proofs/level10/thm-subsetp-of-rw.crewrite-clause-lists-when-subsetp.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 19.85 seconds
;; VERIFY took 20.74 seconds
13907> VERIFY RW.FAST-CREWRITE-CLAUSE-LIST$-REMOVAL
;; Reading from Proofs/level10/thm-rw.fast-crewrite-clause-list$-removal.proof
;; Reading the file took 1.18 seconds
;; Checking the proof took 27.82 seconds
;; VERIFY took 29.02 seconds
13908> VERIFY FORCING-CONS-LISTP-OF-RW.CREWRITE-CLAUSE-LIST
;; Reading from Proofs/level10/thm-forcing-cons-listp-of-rw.crewrite-clause-list.proof
;; Reading the file took 1.18 seconds
;; Checking the proof took 19.87 seconds
;; VERIFY took 21.06 seconds
13909> VERIFY FORCING-RW.CCSTEP-LIST-LISTP-OF-RW.CREWRITE-CLAUSE-LIST
;; Reading from Proofs/level10/thm-forcing-rw.ccstep-list-listp-of-rw.crewrite-clause-list.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 20.54 seconds
;; VERIFY took 21.44 seconds
13910> VERIFY FORCING-RW.CCSTEP-LIST-LISTP-OF-RW.CREWRITE-CLAUSE-LIST-FREE
;; Reading from Proofs/level10/thm-forcing-rw.ccstep-list-listp-of-rw.crewrite-clause-list-free.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 18.69 seconds
;; VERIFY took 19.59 seconds
13911> VERIFY FORCING-RW.TRACE-LIST-ATBLP-OF-RW.CCSTEP-LIST-LIST-GATHER-TRACES-OF-RW.CREWRITE-CLAUSE-LIST
;; Reading from Proofs/level10/thm-forcing-rw.trace-list-atblp-of-rw.ccstep-list-list-gather-traces-of-rw.crewrite-clause-list.proof
;; Reading the file took 1.18 seconds
;; Checking the proof took 21.57 seconds
;; VERIFY took 22.77 seconds
13912> VERIFY FORCING-RW.TRACE-LIST-ATBLP-OF-RW.CCSTEP-LIST-LIST-GATHER-TRACES-OF-RW.CREWRITE-CLAUSE-LIST-FREE
;; Reading from Proofs/level10/thm-forcing-rw.trace-list-atblp-of-rw.ccstep-list-list-gather-traces-of-rw.crewrite-clause-list-free.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 18.75 seconds
;; VERIFY took 19.65 seconds
13913> DEFINE RW.CCSTEP-LIST-LIST-TERMINALP
;; Reading from Proofs/level10/admit-rw.ccstep-list-list-terminalp.proofs
;; Reading the file took 1.20 seconds
;; Checking the proofs took 37.68 seconds
;; DEFINE took 38.91 seconds
13914> VERIFY RW.CCSTEP-LIST-LIST-TERMINALP
;; Reading from Proofs/level10/thm-rw.ccstep-list-list-terminalp.proof
;; Reading the file took 0.20 seconds
;; Checking the proof took 3.39 seconds
;; VERIFY took 3.60 seconds
13915> VERIFY RW.CCSTEP-LIST-LIST-TERMINALP-WHEN-NOT-CONSP
;; Reading from Proofs/level10/thm-rw.ccstep-list-list-terminalp-when-not-consp.proof
;; Reading the file took 0.87 seconds
;; Checking the proof took 26.27 seconds
;; VERIFY took 27.15 seconds
13916> VERIFY RW.CCSTEP-LIST-LIST-TERMINALP-OF-CONS
;; Reading from Proofs/level10/thm-rw.ccstep-list-list-terminalp-of-cons.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 26.35 seconds
;; VERIFY took 27.26 seconds
13917> VERIFY RW.CCSTEP-LIST-LIST-TERMINALP-OF-RW.CREWRITE-CLAUSE-LIST
;; Reading from Proofs/level10/thm-rw.ccstep-list-list-terminalp-of-rw.crewrite-clause-list.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 20.35 seconds
;; VERIFY took 21.25 seconds
13918> DEFINE RW.CCSTEP-LIST-LIST-OBLIGATIONS
;; Reading from Proofs/level10/admit-rw.ccstep-list-list-obligations.proofs
;; Reading the file took 1.18 seconds
;; Checking the proofs took 56.68 seconds
;; DEFINE took 57.95 seconds
13919> VERIFY RW.CCSTEP-LIST-LIST-OBLIGATIONS
;; Reading from Proofs/level10/thm-rw.ccstep-list-list-obligations.proof
;; Reading the file took 0.21 seconds
;; Checking the proof took 3.39 seconds
;; VERIFY took 3.62 seconds
13920> VERIFY TRUE-LISTP-OF-RW.CCSTEP-LIST-LIST-OBLIGATIONS
;; Reading from Proofs/level10/thm-true-listp-of-rw.ccstep-list-list-obligations.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 27.95 seconds
;; VERIFY took 28.85 seconds
13921> VERIFY FORCING-CONS-LISTP-OF-RW.CCSTEP-LIST-LIST-OBLIGATIONS
;; Reading from Proofs/level10/thm-forcing-cons-listp-of-rw.ccstep-list-list-obligations.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 30.30 seconds
;; VERIFY took 31.22 seconds
13922> VERIFY FORCING-LOGIC.TERM-LIST-LISTP-OF-RW.CCSTEP-LIST-LIST-OBLIGATIONS
;; Reading from Proofs/level10/thm-forcing-logic.term-list-listp-of-rw.ccstep-list-list-obligations.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 29.67 seconds
;; VERIFY took 30.58 seconds
13923> VERIFY FORCING-LOGIC.TERM-LIST-LISTP-OF-RW.CCSTEP-LIST-LIST-OBLIGATIONS-FREE
;; Reading from Proofs/level10/thm-forcing-logic.term-list-listp-of-rw.ccstep-list-list-obligations-free.proof
;; Reading the file took 0.88 seconds
;; Checking the proof took 18.75 seconds
;; VERIFY took 19.64 seconds
13924> DEFINE RW.CREWRITE-CLAUSE-LIST-BLDR
;; Reading from Proofs/level10/admit-rw.crewrite-clause-list-bldr.proofs
;; Reading the file took 1.19 seconds
;; Checking the proofs took 56.61 seconds
;; DEFINE took 57.85 seconds
13925> VERIFY RW.CREWRITE-CLAUSE-LIST-BLDR
;; Reading from Proofs/level10/thm-rw.crewrite-clause-list-bldr.proof
;; Reading the file took 0.25 seconds
;; Checking the proof took 3.41 seconds
;; VERIFY took 3.68 seconds
13926> VERIFY FORCING-LOGIC.APPEAL-LISTP-OF-RW.CREWRITE-CLAUSE-LIST-BLDR
;; Reading from Proofs/level10/thm-forcing-logic.appeal-listp-of-rw.crewrite-clause-list-bldr.proof
;; Reading the file took 1.10 seconds
;; Checking the proof took 55.82 seconds
;; VERIFY took 56.94 seconds
13927> VERIFY FORCING-LOGIC.STRIP-CONCLUSIONS-OF-RW.CREWRITE-CLAUSE-LIST-BLDR
;; Reading from Proofs/level10/thm-forcing-logic.strip-conclusions-of-rw.crewrite-clause-list-bldr.proof
;; Reading the file took 1.03 seconds
;; Checking the proof took 59.17 seconds
;; VERIFY took 60.22 seconds
13928> VERIFY FORCING-LOGIC.PROOF-LISTP-OF-RW.CREWRITE-CLAUSE-LIST-BLDR
;; Reading from Proofs/level10/thm-forcing-logic.proof-listp-of-rw.crewrite-clause-list-bldr.proof
;; Reading the file took 1.71 seconds
;; Checking the proof took 291.11 seconds
;; VERIFY took 292.94 seconds
13929> DEFINE RW.CREWRITE-RECORDS-SHOW-PROGRESSP
;; Reading from Proofs/level10/admit-rw.crewrite-records-show-progressp.proofs
;; Reading the file took 0.89 seconds
;; Checking the proofs took 37.82 seconds
;; DEFINE took 38.72 seconds
13930> VERIFY RW.CREWRITE-RECORDS-SHOW-PROGRESSP
;; Reading from Proofs/level10/thm-rw.crewrite-records-show-progressp.proof
;; Reading the file took 0.20 seconds
;; Checking the proof took 3.40 seconds
;; VERIFY took 3.62 seconds
13931> DEFINE RW.FAST-CCSTEPP
;; Reading from Proofs/level10/admit-rw.fast-ccstepp.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
13932> VERIFY RW.FAST-CCSTEPP
;; Reading from Proofs/level10/thm-rw.fast-ccstepp.proof
;; Reading the file took 0.26 seconds
;; Checking the proof took 3.68 seconds
;; VERIFY took 3.95 seconds
13933> DEFINE RW.FAST-CCSTEP
;; Reading from Proofs/level10/admit-rw.fast-ccstep.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13934> VERIFY RW.FAST-CCSTEP
;; Reading from Proofs/level10/thm-rw.fast-ccstep.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.44 seconds
;; VERIFY took 3.66 seconds
13935> DEFINE RW.FAST-CCSTEP->CONTRADICTIONP
;; Reading from Proofs/level10/admit-rw.fast-ccstep-_gt_contradictionp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13936> VERIFY RW.FAST-CCSTEP->CONTRADICTIONP
;; Reading from Proofs/level10/thm-rw.fast-ccstep-_gt_contradictionp.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.43 seconds
;; VERIFY took 3.66 seconds
13937> DEFINE RW.FAST-CCSTEP->FTRACE
;; Reading from Proofs/level10/admit-rw.fast-ccstep-_gt_ftrace.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13938> VERIFY RW.FAST-CCSTEP->FTRACE
;; Reading from Proofs/level10/thm-rw.fast-ccstep-_gt_ftrace.proof
;; Reading the file took 0.40 seconds
;; Checking the proof took 3.43 seconds
;; VERIFY took 3.84 seconds
13939> VERIFY RW.FAST-CCSTEP->CONTRADICTIONP-OF-RW.FAST-CCSTEP
;; Reading from Proofs/level10/thm-rw.fast-ccstep-_gt_contradictionp-of-rw.fast-ccstep.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 26.73 seconds
;; VERIFY took 27.63 seconds
13940> VERIFY RW.FAST-CCSTEP->FTRACE-OF-RW.FAST-CCSTEP
;; Reading from Proofs/level10/thm-rw.fast-ccstep-_gt_ftrace-of-rw.fast-ccstep.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 26.75 seconds
;; VERIFY took 27.66 seconds
13941> VERIFY BOOLEANP-OF-RW.FAST-CCSTEPP
;; Reading from Proofs/level10/thm-booleanp-of-rw.fast-ccstepp.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 27.13 seconds
;; VERIFY took 28.04 seconds
13942> VERIFY RW.FAST-CCSTEPP-OF-RW.FAST-CCSTEP
;; Reading from Proofs/level10/thm-rw.fast-ccstepp-of-rw.fast-ccstep.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 26.97 seconds
;; VERIFY took 27.87 seconds
13943> VERIFY BOOLEANP-OF-RW.FAST-CCSTEP->CONTRADICTIONP
;; Reading from Proofs/level10/thm-booleanp-of-rw.fast-ccstep-_gt_contradictionp.proof
;; Reading the file took 1.20 seconds
;; Checking the proof took 26.77 seconds
;; VERIFY took 27.98 seconds
13944> VERIFY RW.FTRACEP-OF-RW.FAST-CCSTEP->FTRACE
;; Reading from Proofs/level10/thm-rw.ftracep-of-rw.fast-ccstep-_gt_ftrace.proof
;; Reading the file took 1.20 seconds
;; Checking the proof took 26.68 seconds
;; VERIFY took 27.90 seconds
13945> DEFINE RW.CCSTEP-FAST-IMAGE
;; Reading from Proofs/level10/admit-rw.ccstep-fast-image.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13946> VERIFY RW.CCSTEP-FAST-IMAGE
;; Reading from Proofs/level10/thm-rw.ccstep-fast-image.proof
;; Reading the file took 0.21 seconds
;; Checking the proof took 3.70 seconds
;; VERIFY took 3.92 seconds
13947> VERIFY RW.FAST-CCSTEPP-OF-RW.CCSTEP-FAST-IMAGE
;; Reading from Proofs/level10/thm-rw.fast-ccstepp-of-rw.ccstep-fast-image.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 26.84 seconds
;; VERIFY took 27.75 seconds
13948> VERIFY RW.FAST-CCSTEP->CONTRADICTIONP-OF-RW.CCSTEP-FAST-IMAGE
;; Reading from Proofs/level10/thm-rw.fast-ccstep-_gt_contradictionp-of-rw.ccstep-fast-image.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 26.79 seconds
;; VERIFY took 27.71 seconds
13949> VERIFY RW.FAST-CCSTEP->FTRACE-OF-RW.CCSTEP-FAST-IMAGE
;; Reading from Proofs/level10/thm-rw.fast-ccstep-_gt_ftrace-of-rw.ccstep-fast-image.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 26.73 seconds
;; VERIFY took 27.64 seconds
13950> DEFINE RW.FAST-CREWRITE-TAKE-STEP
;; Reading from Proofs/level10/admit-rw.fast-crewrite-take-step.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13951> VERIFY RW.FAST-CREWRITE-TAKE-STEP
;; Reading from Proofs/level10/thm-rw.fast-crewrite-take-step.proof
;; Reading the file took 0.21 seconds
;; Checking the proof took 3.42 seconds
;; VERIFY took 3.65 seconds
13952> VERIFY RW.FAST-CCSTEPP-OF-RW.FAST-CREWRITE-TAKE-STEP
;; Reading from Proofs/level10/thm-rw.fast-ccstepp-of-rw.fast-crewrite-take-step.proof
;; Reading the file took 1.15 seconds
;; Checking the proof took 26.87 seconds
;; VERIFY took 28.04 seconds
13953> VERIFY RW.CCSTEP-FAST-IMAGE-OF-RW.CREWRITE-TAKE-STEP
;; Reading from Proofs/level10/thm-rw.ccstep-fast-image-of-rw.crewrite-take-step.proof
;; Reading the file took 1.26 seconds
;; Checking the proof took 44.78 seconds
;; VERIFY took 46.05 seconds
13954> VERIFY RW.FAST-CCSTEP->CONTRADICTIONP-OF-RW.FAST-CREWRITE-TAKE-STEP
;; Reading from Proofs/level10/thm-rw.fast-ccstep-_gt_contradictionp-of-rw.fast-crewrite-take-step.proof
;; Reading the file took 0.93 seconds
;; Checking the proof took 26.92 seconds
;; VERIFY took 27.87 seconds
13955> VERIFY RW.FAST-CCSTEP->FTRACE-OF-RW.FAST-CREWRITE-TAKE-STEP
;; Reading from Proofs/level10/thm-rw.fast-ccstep-_gt_ftrace-of-rw.fast-crewrite-take-step.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 35.86 seconds
;; VERIFY took 36.78 seconds
13956> DEFINE RW.FAST-CCSTEP->PROVEDP
;; Reading from Proofs/level10/admit-rw.fast-ccstep-_gt_provedp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.03 seconds
13957> VERIFY RW.FAST-CCSTEP->PROVEDP
;; Reading from Proofs/level10/thm-rw.fast-ccstep-_gt_provedp.proof
;; Reading the file took 0.52 seconds
;; Checking the proof took 3.44 seconds
;; VERIFY took 3.97 seconds
13958> VERIFY RW.FAST-CCSTEP->PROVEDP-OF-RW.CCSTEP-FAST-IMAGE
;; Reading from Proofs/level10/thm-rw.fast-ccstep-_gt_provedp-of-rw.ccstep-fast-image.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 26.85 seconds
;; VERIFY took 27.75 seconds
13959> VERIFY RW.FAST-CCSTEP->CONTRADICTIONP-WHEN-NOT-RW.FAST-CCSTEP->PROVEDP
;; Reading from Proofs/level10/thm-rw.fast-ccstep-_gt_contradictionp-when-not-rw.fast-ccstep-_gt_provedp.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 26.88 seconds
;; VERIFY took 27.81 seconds
13960> VERIFY RW.FAST-CCSTEP->PROVEDP-OF-RW.FAST-CREWRITE-TAKE-STEP
;; Reading from Proofs/level10/thm-rw.fast-ccstep-_gt_provedp-of-rw.fast-crewrite-take-step.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 26.95 seconds
;; VERIFY took 27.86 seconds
13961> DEFINE RW.FAST-CCSTEP->T1PRIME
;; Reading from Proofs/level10/admit-rw.fast-ccstep-_gt_t1prime.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13962> VERIFY RW.FAST-CCSTEP->T1PRIME
;; Reading from Proofs/level10/thm-rw.fast-ccstep-_gt_t1prime.proof
;; Reading the file took 0.21 seconds
;; Checking the proof took 3.43 seconds
;; VERIFY took 3.66 seconds
13963> VERIFY RW.FAST-CCSTEP->T1PRIME-OF-RW.CCSTEP-FAST-IMAGE
;; Reading from Proofs/level10/thm-rw.fast-ccstep-_gt_t1prime-of-rw.ccstep-fast-image.proof
;; Reading the file took 1.19 seconds
;; Checking the proof took 26.60 seconds
;; VERIFY took 27.80 seconds
13964> VERIFY LOGIC.TERMP-OF-RW.FAST-CCSTEP->T1PRIME
;; Reading from Proofs/level10/thm-logic.termp-of-rw.fast-ccstep-_gt_t1prime.proof
;; Reading the file took 1.21 seconds
;; Checking the proof took 26.57 seconds
;; VERIFY took 27.79 seconds
13965> VERIFY RW.FAST-CCSTEP->T1PRIME-OF-RW.FAST-CREWRITE-TAKE-STEP
;; Reading from Proofs/level10/thm-rw.fast-ccstep-_gt_t1prime-of-rw.fast-crewrite-take-step.proof
;; Reading the file took 1.19 seconds
;; Checking the proof took 34.59 seconds
;; VERIFY took 35.80 seconds
13966> DEFINE RW.CREWRITE-CLAUSE-AUX-PROVEDP
;; Reading from Proofs/level10/admit-rw.crewrite-clause-aux-provedp.proofs
;; Reading the file took 1.22 seconds
;; Checking the proofs took 38.43 seconds
;; DEFINE took 39.70 seconds
13967> VERIFY RW.CREWRITE-CLAUSE-AUX-PROVEDP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-aux-provedp.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.43 seconds
;; VERIFY took 3.67 seconds
13968> DEFINE RW.CREWRITE-CLAUSE-AUX-TODO-PRIMES
;; Reading from Proofs/level10/admit-rw.crewrite-clause-aux-todo-primes.proofs
;; Reading the file took 0.89 seconds
;; Checking the proofs took 38.19 seconds
;; DEFINE took 39.11 seconds
13969> VERIFY RW.CREWRITE-CLAUSE-AUX-TODO-PRIMES
;; Reading from Proofs/level10/thm-rw.crewrite-clause-aux-todo-primes.proof
;; Reading the file took 0.50 seconds
;; Checking the proof took 3.44 seconds
;; VERIFY took 3.95 seconds
13970> DEFINE RW.CREWRITE-CLAUSE-AUX-FGOALS
;; Reading from Proofs/level10/admit-rw.crewrite-clause-aux-fgoals.proofs
;; Reading the file took 0.89 seconds
;; Checking the proofs took 38.31 seconds
;; DEFINE took 39.27 seconds
13971> VERIFY RW.CREWRITE-CLAUSE-AUX-FGOALS
;; Reading from Proofs/level10/thm-rw.crewrite-clause-aux-fgoals.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.68 seconds
;; VERIFY took 3.91 seconds
13972> DEFINE RW.CREWRITE-CLAUSE-AUX-NOACC
;; Reading from Proofs/level10/admit-rw.crewrite-clause-aux-noacc.proofs
;; Reading the file took 0.89 seconds
;; Checking the proofs took 38.44 seconds
;; DEFINE took 39.38 seconds
13973> VERIFY RW.CREWRITE-CLAUSE-AUX-NOACC
;; Reading from Proofs/level10/thm-rw.crewrite-clause-aux-noacc.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.45 seconds
;; VERIFY took 3.68 seconds
13974> VERIFY CONSP-OF-RW.CREWRITE-CLAUSE-AUX-NOACC
;; Reading from Proofs/level10/thm-consp-of-rw.crewrite-clause-aux-noacc.proof
;; Reading the file took 1.19 seconds
;; Checking the proof took 28.24 seconds
;; VERIFY took 29.44 seconds
13975> VERIFY RW.CREWRITE-CLAUSE-AUX-REMOVAL
;; Reading from Proofs/level10/thm-rw.crewrite-clause-aux-removal.proof
;; Reading the file took 1.26 seconds
;; Checking the proof took 36.22 seconds
;; VERIFY took 37.49 seconds
13976> VERIFY CAR-OF-APP
;; Reading from Proofs/level10/thm-car-of-app.proof
;; Reading the file took 1.34 seconds
;; Checking the proof took 19.35 seconds
;; VERIFY took 20.70 seconds
13977> VERIFY CDR-OF-APP
;; Reading from Proofs/level10/thm-cdr-of-app.proof
;; Reading the file took 0.99 seconds
;; Checking the proof took 19.32 seconds
;; VERIFY took 20.33 seconds
13978> VERIFY RW.CREWRITE-CLAUSE-AUX-PROVEDP-CORRECT
;; Reading from Proofs/level10/thm-rw.crewrite-clause-aux-provedp-correct.proof
;; Reading the file took 1.09 seconds
;; Checking the proof took 35.40 seconds
;; VERIFY took 36.50 seconds
13979> VERIFY CONSP-OF-RW.CREWRITE-CLAUSE-AUX-TODO-PRIMES
;; Reading from Proofs/level10/thm-consp-of-rw.crewrite-clause-aux-todo-primes.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 27.69 seconds
;; VERIFY took 28.61 seconds
13980> VERIFY RW.CCSTEP->CLAUSE-PRIME-OF-RW.CREWRITE-TAKE-STEP
;; Reading from Proofs/level10/thm-rw.ccstep-_gt_clause-prime-of-rw.crewrite-take-step.proof
;; Reading the file took 0.93 seconds
;; Checking the proof took 27.93 seconds
;; VERIFY took 28.88 seconds
13981> VERIFY RW.CREWRITE-CLAUSE-AUX-TODO-PRIMES-CORRECT
;; Reading from Proofs/level10/thm-rw.crewrite-clause-aux-todo-primes-correct.proof
;; Reading the file took 0.97 seconds
;; Checking the proof took 47.96 seconds
;; VERIFY took 48.95 seconds
13982> VERIFY TRUE-LISTP-OF-RW.CREWRITE-CLAUSE-AUX-FGOALS
;; Reading from Proofs/level10/thm-true-listp-of-rw.crewrite-clause-aux-fgoals.proof
;; Reading the file took 1.29 seconds
;; Checking the proof took 27.61 seconds
;; VERIFY took 28.92 seconds
13983> VERIFY RW.CREWRITE-CLAUSE-AUX-FGOALS-CORRECT
;; Reading from Proofs/level10/thm-rw.crewrite-clause-aux-fgoals-correct.proof
;; Reading the file took 1.27 seconds
;; Checking the proof took 35.80 seconds
;; VERIFY took 37.07 seconds
13984> DEFINE RW.FAST-CREWRITE-CLAUSE-AUX
;; Reading from Proofs/level10/admit-rw.fast-crewrite-clause-aux.proofs
;; Reading the file took 0.92 seconds
;; Checking the proofs took 38.83 seconds
;; DEFINE took 39.77 seconds
13985> VERIFY RW.FAST-CREWRITE-CLAUSE-AUX
;; Reading from Proofs/level10/thm-rw.fast-crewrite-clause-aux.proof
;; Reading the file took 0.52 seconds
;; Checking the proof took 3.45 seconds
;; VERIFY took 3.99 seconds
13986> VERIFY PROVEDP-OF-RW.FAST-CREWRITE-CLAUSE-AUX
;; Reading from Proofs/level10/thm-provedp-of-rw.fast-crewrite-clause-aux.proof
;; Reading the file took 0.97 seconds
;; Checking the proof took 50.15 seconds
;; VERIFY took 51.13 seconds
13987> VERIFY CLAUSE-PRIME-OF-RW.FAST-CREWRITE-CLAUSE-AUX
;; Reading from Proofs/level10/thm-clause-prime-of-rw.fast-crewrite-clause-aux.proof
;; Reading the file took 1.37 seconds
;; Checking the proof took 61.04 seconds
;; VERIFY took 62.43 seconds
13988> VERIFY FORCED-GOALS-OF-RW.FAST-CREWRITE-CLAUSE-AUX
;; Reading from Proofs/level10/thm-forced-goals-of-rw.fast-crewrite-clause-aux.proof
;; Reading the file took 1.01 seconds
;; Checking the proof took 58.16 seconds
;; VERIFY took 59.19 seconds
13989> DEFINE RW.FAST-CREWRITE-CLAUSE
;; Reading from Proofs/level10/admit-rw.fast-crewrite-clause.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
13990> VERIFY RW.FAST-CREWRITE-CLAUSE
;; Reading from Proofs/level10/thm-rw.fast-crewrite-clause.proof
;; Reading the file took 0.57 seconds
;; Checking the proof took 3.45 seconds
;; VERIFY took 4.03 seconds
13991> VERIFY FIRST-OF-RW.FAST-CREWRITE-CLAUSE
;; Reading from Proofs/level10/thm-first-of-rw.fast-crewrite-clause.proof
;; Reading the file took 0.93 seconds
;; Checking the proof took 26.84 seconds
;; VERIFY took 27.79 seconds
13992> VERIFY SECOND-OF-RW.FAST-CREWRITE-CLAUSE
;; Reading from Proofs/level10/thm-second-of-rw.fast-crewrite-clause.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 27.47 seconds
;; VERIFY took 28.40 seconds
13993> VERIFY THIRD-OF-RW.FAST-CREWRITE-CLAUSE
;; Reading from Proofs/level10/thm-third-of-rw.fast-crewrite-clause.proof
;; Reading the file took 1.03 seconds
;; Checking the proof took 27.02 seconds
;; VERIFY took 28.07 seconds
13994> VERIFY NTH-OF-CONS-WHEN-CONSTANTP
;; Reading from Proofs/level10/thm-nth-of-cons-when-constantp.proof
;; Reading the file took 0.94 seconds
;; Checking the proof took 27.03 seconds
;; VERIFY took 27.98 seconds
13995> VERIFY RW.CREWRITE-CLAUSE-AUX-OF-NIL
;; Reading from Proofs/level10/thm-rw.crewrite-clause-aux-of-nil.proof
;; Reading the file took 0.94 seconds
;; Checking the proof took 26.88 seconds
;; VERIFY took 27.83 seconds
13996> VERIFY RW.CREWRITE-CLAUSE-OF-NIL
;; Reading from Proofs/level10/thm-rw.crewrite-clause-of-nil.proof
;; Reading the file took 1.25 seconds
;; Checking the proof took 26.69 seconds
;; VERIFY took 27.95 seconds
13997> VERIFY TACTIC.WORLD->INDEX-UNDER-IFF
;; Reading from Proofs/level10/thm-tactic.world-_gt_index-under-iff.proof
;; Reading the file took 1.22 seconds
;; Checking the proof took 26.72 seconds
;; VERIFY took 27.95 seconds
13998> VERIFY TACTIC.FIND-WORLD-OF-NIL
;; Reading from Proofs/level10/thm-tactic.find-world-of-nil.proof
;; Reading the file took 1.27 seconds
;; Checking the proof took 27.54 seconds
;; VERIFY took 28.82 seconds
13999> DEFINE RW.MAKE-CREWRITE-CLAUSE-PLAN
;; Reading from Proofs/level10/admit-rw.make-crewrite-clause-plan.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.12 seconds
14000> VERIFY RW.MAKE-CREWRITE-CLAUSE-PLAN
;; Reading from Proofs/level10/thm-rw.make-crewrite-clause-plan.proof
;; Reading the file took 0.50 seconds
;; Checking the proof took 3.47 seconds
;; VERIFY took 4.00 seconds
14001> DEFINE RW.CREWRITE-CLAUSE-PLANP
;; Reading from Proofs/level10/admit-rw.crewrite-clause-planp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.12 seconds
14002> VERIFY RW.CREWRITE-CLAUSE-PLANP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-planp.proof
;; Reading the file took 0.23 seconds
;; Checking the proof took 3.48 seconds
;; VERIFY took 3.75 seconds
14003> DEFINE RW.CREWRITE-CLAUSE-PLAN-OKP
;; Reading from Proofs/level10/admit-rw.crewrite-clause-plan-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.03 seconds
14004> VERIFY RW.CREWRITE-CLAUSE-PLAN-OKP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-okp.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.65 seconds
;; VERIFY took 3.90 seconds
14005> DEFINE RW.CREWRITE-CLAUSE-PLAN-ATBLP
;; Reading from Proofs/level10/admit-rw.crewrite-clause-plan-atblp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
14006> VERIFY RW.CREWRITE-CLAUSE-PLAN-ATBLP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-atblp.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.43 seconds
;; VERIFY took 3.66 seconds
14007> DEFINE RW.CREWRITE-CLAUSE-PLAN->PROGRESSP
;; Reading from Proofs/level10/admit-rw.crewrite-clause-plan-_gt_progressp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
14008> VERIFY RW.CREWRITE-CLAUSE-PLAN->PROGRESSP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-_gt_progressp.proof
;; Reading the file took 0.23 seconds
;; Checking the proof took 3.43 seconds
;; VERIFY took 3.68 seconds
14009> DEFINE RW.CREWRITE-CLAUSE-PLAN->CLAUSE
;; Reading from Proofs/level10/admit-rw.crewrite-clause-plan-_gt_clause.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
14010> VERIFY RW.CREWRITE-CLAUSE-PLAN->CLAUSE
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-_gt_clause.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.62 seconds
;; VERIFY took 3.85 seconds
14011> DEFINE RW.CREWRITE-CLAUSE-PLAN->PROVEDP
;; Reading from Proofs/level10/admit-rw.crewrite-clause-plan-_gt_provedp.proofs
;; Reading the file took 0.02 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.03 seconds
14012> VERIFY RW.CREWRITE-CLAUSE-PLAN->PROVEDP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-_gt_provedp.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.46 seconds
;; VERIFY took 3.69 seconds
14013> DEFINE RW.CREWRITE-CLAUSE-PLAN->CLAUSE-PRIME
;; Reading from Proofs/level10/admit-rw.crewrite-clause-plan-_gt_clause-prime.proofs
;; Reading the file took 0.03 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.04 seconds
14014> VERIFY RW.CREWRITE-CLAUSE-PLAN->CLAUSE-PRIME
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-_gt_clause-prime.proof
;; Reading the file took 0.25 seconds
;; Checking the proof took 3.42 seconds
;; VERIFY took 3.68 seconds
14015> DEFINE RW.CREWRITE-CLAUSE-PLAN->FORCED-GOALS
;; Reading from Proofs/level10/admit-rw.crewrite-clause-plan-_gt_forced-goals.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
14016> VERIFY RW.CREWRITE-CLAUSE-PLAN->FORCED-GOALS
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-_gt_forced-goals.proof
;; Reading the file took 0.42 seconds
;; Checking the proof took 3.44 seconds
;; VERIFY took 3.87 seconds
14017> DEFINE RW.CREWRITE-CLAUSE-PLAN-COMPILER
;; Reading from Proofs/level10/admit-rw.crewrite-clause-plan-compiler.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
14018> VERIFY RW.CREWRITE-CLAUSE-PLAN-COMPILER
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-compiler.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.47 seconds
;; VERIFY took 3.70 seconds
14019> VERIFY LEMMA-1-FOR-RW.CREWRITE-CLAUSE-PLAN
;; Reading from Proofs/level10/thm-lemma-1-for-rw.crewrite-clause-plan.proof
;; Reading the file took 1.13 seconds
;; Checking the proof took 19.34 seconds
;; VERIFY took 20.48 seconds
14020> VERIFY LEMMA-2-FOR-RW.CREWRITE-CLAUSE-PLAN
;; Reading from Proofs/level10/thm-lemma-2-for-rw.crewrite-clause-plan.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 19.31 seconds
;; VERIFY took 20.24 seconds
14021> VERIFY LEMMA-3-FOR-RW.CREWRITE-CLAUSE-PLAN
;; Reading from Proofs/level10/thm-lemma-3-for-rw.crewrite-clause-plan.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 19.15 seconds
;; VERIFY took 20.08 seconds
14022> VERIFY LEMMA-4-FOR-RW.CREWRITE-CLAUSE-PLAN
;; Reading from Proofs/level10/thm-lemma-4-for-rw.crewrite-clause-plan.proof
;; Reading the file took 1.18 seconds
;; Checking the proof took 19.23 seconds
;; VERIFY took 20.42 seconds
14023> VERIFY LEMMA-5-FOR-RW.CREWRITE-CLAUSE-PLAN
;; Reading from Proofs/level10/thm-lemma-5-for-rw.crewrite-clause-plan.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 19.45 seconds
;; VERIFY took 20.37 seconds
14024> VERIFY LEMMA-6-FOR-RW.CREWRITE-CLAUSE-PLAN
;; Reading from Proofs/level10/thm-lemma-6-for-rw.crewrite-clause-plan.proof
;; Reading the file took 1.38 seconds
;; Checking the proof took 19.26 seconds
;; VERIFY took 20.65 seconds
14025> VERIFY LEMMA-7-FOR-RW.CREWRITE-CLAUSE-PLAN
;; Reading from Proofs/level10/thm-lemma-7-for-rw.crewrite-clause-plan.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 19.20 seconds
;; VERIFY took 20.12 seconds
14026> VERIFY LEMMA-8-FOR-RW.CREWRITE-CLAUSE-PLAN
;; Reading from Proofs/level10/thm-lemma-8-for-rw.crewrite-clause-plan.proof
;; Reading the file took 1.26 seconds
;; Checking the proof took 19.71 seconds
;; VERIFY took 20.98 seconds
14027> VERIFY LEMMA-9-FOR-RW.CREWRITE-CLAUSE-PLAN
;; Reading from Proofs/level10/thm-lemma-9-for-rw.crewrite-clause-plan.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 19.33 seconds
;; VERIFY took 20.24 seconds
14028> VERIFY LEMMA-10-FOR-RW.CREWRITE-CLAUSE-PLAN
;; Reading from Proofs/level10/thm-lemma-10-for-rw.crewrite-clause-plan.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 19.15 seconds
;; VERIFY took 20.06 seconds
14029> VERIFY LEMMA-11-FOR-RW.CREWRITE-CLAUSE-PLAN
;; Reading from Proofs/level10/thm-lemma-11-for-rw.crewrite-clause-plan.proof
;; Reading the file took 1.18 seconds
;; Checking the proof took 19.20 seconds
;; VERIFY took 20.39 seconds
14030> VERIFY BOOLEANP-OF-RW.CREWRITE-CLAUSE-PLANP
;; Reading from Proofs/level10/thm-booleanp-of-rw.crewrite-clause-planp.proof
;; Reading the file took 0.95 seconds
;; Checking the proof took 23.74 seconds
;; VERIFY took 24.70 seconds
14031> VERIFY BOOLEANP-OF-RW.CREWRITE-CLAUSE-PLAN-OKP
;; Reading from Proofs/level10/thm-booleanp-of-rw.crewrite-clause-plan-okp.proof
;; Reading the file took 1.21 seconds
;; Checking the proof took 19.75 seconds
;; VERIFY took 20.96 seconds
14032> VERIFY BOOLEANP-OF-RW.CREWRITE-CLAUSE-PLAN-ATBLP
;; Reading from Proofs/level10/thm-booleanp-of-rw.crewrite-clause-plan-atblp.proof
;; Reading the file took 0.96 seconds
;; Checking the proof took 19.11 seconds
;; VERIFY took 20.08 seconds
14033> VERIFY CONSP-OF-RW.CREWRITE-CLAUSE-PLAN->CLAUSE-PRIME
;; Reading from Proofs/level10/thm-consp-of-rw.crewrite-clause-plan-_gt_clause-prime.proof
;; Reading the file took 1.26 seconds
;; Checking the proof took 19.51 seconds
;; VERIFY took 20.78 seconds
14034> VERIFY LOGIC.TERM-LISTP-OF-RW.CREWRITE-CLAUSE-PLAN->CLAUSE-PRIME
;; Reading from Proofs/level10/thm-logic.term-listp-of-rw.crewrite-clause-plan-_gt_clause-prime.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 19.62 seconds
;; VERIFY took 20.53 seconds
14035> VERIFY TRUE-LISTP-OF-RW.CREWRITE-CLAUSE-PLAN->FORCED-GOALS
;; Reading from Proofs/level10/thm-true-listp-of-rw.crewrite-clause-plan-_gt_forced-goals.proof
;; Reading the file took 1.21 seconds
;; Checking the proof took 20.59 seconds
;; VERIFY took 21.81 seconds
14036> VERIFY LOGIC.FORMULA-LISTP-OF-RW.CREWRITE-CLAUSE-PLAN->FORCED-GOALS
;; Reading from Proofs/level10/thm-logic.formula-listp-of-rw.crewrite-clause-plan-_gt_forced-goals.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 20.36 seconds
;; VERIFY took 21.26 seconds
14037> VERIFY LOGIC.FORMULA-LIST-ATBLP-OF-RW.CREWRITE-CLAUSE-PLAN->FORCED-GOALS
;; Reading from Proofs/level10/thm-logic.formula-list-atblp-of-rw.crewrite-clause-plan-_gt_forced-goals.proof
;; Reading the file took 0.99 seconds
;; Checking the proof took 26.97 seconds
;; VERIFY took 27.99 seconds
14038> VERIFY RW.CREWRITE-CLAUSE-PLAN->CLAUSE-OF-RW.MAKE-CREWRITE-CLAUSE-PLAN
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-_gt_clause-of-rw.make-crewrite-clause-plan.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 20.27 seconds
;; VERIFY took 21.19 seconds
14039> VERIFY RW.CREWRITE-CLAUSE-PLANP-OF-RW.MAKE-CREWRITE-CLAUSE-PLAN
;; Reading from Proofs/level10/thm-rw.crewrite-clause-planp-of-rw.make-crewrite-clause-plan.proof
;; Reading the file took 1.01 seconds
;; Checking the proof took 216.74 seconds
;; VERIFY took 217.76 seconds
14040> VERIFY RW.CREWRITE-CLAUSE-PLAN-OKP-OF-RW.MAKE-CREWRITE-CLAUSE-PLAN
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-okp-of-rw.make-crewrite-clause-plan.proof
;; Reading the file took 1.18 seconds
;; Checking the proof took 57.04 seconds
;; VERIFY took 58.24 seconds
14041> VERIFY RW.CREWRITE-CLAUSE-PLAN-ATBLP-OF-RW.MAKE-CREWRITE-CLAUSE-PLAN
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-atblp-of-rw.make-crewrite-clause-plan.proof
;; Reading the file took 1.20 seconds
;; Checking the proof took 20.58 seconds
;; VERIFY took 21.79 seconds
14042> VERIFY LOGIC.APPEALP-OF-RW.CREWRITE-CLAUSE-PLAN-COMPILER
;; Reading from Proofs/level10/thm-logic.appealp-of-rw.crewrite-clause-plan-compiler.proof
;; Reading the file took 0.96 seconds
;; Checking the proof took 24.39 seconds
;; VERIFY took 25.37 seconds
14043> VERIFY LOGIC.CONCLUSION-OF-RW.CREWRITE-CLAUSE-PLAN-COMPILER
;; Reading from Proofs/level10/thm-logic.conclusion-of-rw.crewrite-clause-plan-compiler.proof
;; Reading the file took 1.32 seconds
;; Checking the proof took 30.78 seconds
;; VERIFY took 32.12 seconds
14044> VERIFY LOGIC.PROOFP-OF-RW.CREWRITE-CLAUSE-PLAN-COMPILER
;; Reading from Proofs/level10/thm-logic.proofp-of-rw.crewrite-clause-plan-compiler.proof
;; Reading the file took 1.04 seconds
;; Checking the proof took 41.23 seconds
;; VERIFY took 42.38 seconds
14045> DEFINE RW.CREWRITE-CLAUSE-PLAN-LISTP
;; Reading from Proofs/level10/admit-rw.crewrite-clause-plan-listp.proofs
;; Reading the file took 0.94 seconds
;; Checking the proofs took 38.60 seconds
;; DEFINE took 39.56 seconds
14046> VERIFY RW.CREWRITE-CLAUSE-PLAN-LISTP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-listp.proof
;; Reading the file took 0.25 seconds
;; Checking the proof took 3.47 seconds
;; VERIFY took 3.73 seconds
14047> VERIFY RW.CREWRITE-CLAUSE-PLAN-LISTP-WHEN-NOT-CONSP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-listp-when-not-consp.proof
;; Reading the file took 1.19 seconds
;; Checking the proof took 26.64 seconds
;; VERIFY took 27.84 seconds
14048> VERIFY RW.CREWRITE-CLAUSE-PLAN-LISTP-OF-CONS
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-listp-of-cons.proof
;; Reading the file took 1.19 seconds
;; Checking the proof took 27.00 seconds
;; VERIFY took 28.21 seconds
14049> VERIFY BOOLEANP-OF-RW.CREWRITE-CLAUSE-PLAN-LISTP
;; Reading from Proofs/level10/thm-booleanp-of-rw.crewrite-clause-plan-listp.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 20.16 seconds
;; VERIFY took 21.07 seconds
14050> VERIFY RW.CREWRITE-CLAUSE-PLAN-LISTP-OF-LIST-FIX
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-listp-of-list-fix.proof
;; Reading the file took 0.94 seconds
;; Checking the proof took 20.56 seconds
;; VERIFY took 21.51 seconds
14051> VERIFY RW.CREWRITE-CLAUSE-PLAN-LISTP-OF-APP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-listp-of-app.proof
;; Reading the file took 1.25 seconds
;; Checking the proof took 21.66 seconds
;; VERIFY took 22.92 seconds
14052> VERIFY RW.CREWRITE-CLAUSE-PLAN-LISTP-OF-REV
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-listp-of-rev.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 20.69 seconds
;; VERIFY took 21.61 seconds
14053> VERIFY RW.CREWRITE-CLAUSE-PLANP-OF-CAR-WHEN-RW.CREWRITE-CLAUSE-PLAN-LISTP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-planp-of-car-when-rw.crewrite-clause-plan-listp.proof
;; Reading the file took 1.30 seconds
;; Checking the proof took 19.41 seconds
;; VERIFY took 20.72 seconds
14054> VERIFY RW.CREWRITE-CLAUSE-PLAN-LISTP-OF-CDR-WHEN-RW.CREWRITE-CLAUSE-PLAN-LISTP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-listp-of-cdr-when-rw.crewrite-clause-plan-listp.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 19.37 seconds
;; VERIFY took 20.29 seconds
14055> VERIFY RW.CREWRITE-CLAUSE-PLANP-WHEN-MEMBERP-OF-RW.CREWRITE-CLAUSE-PLAN-LISTP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-planp-when-memberp-of-rw.crewrite-clause-plan-listp.proof
;; Reading the file took 1.20 seconds
;; Checking the proof took 20.52 seconds
;; VERIFY took 21.74 seconds
14056> VERIFY RW.CREWRITE-CLAUSE-PLANP-WHEN-MEMBERP-OF-RW.CREWRITE-CLAUSE-PLAN-LISTP-ALT
;; Reading from Proofs/level10/thm-rw.crewrite-clause-planp-when-memberp-of-rw.crewrite-clause-plan-listp-alt.proof
;; Reading the file took 0.93 seconds
;; Checking the proof took 19.36 seconds
;; VERIFY took 20.31 seconds
14057> VERIFY RW.CREWRITE-CLAUSE-PLAN-LISTP-OF-REMOVE-ALL-WHEN-RW.CREWRITE-CLAUSE-PLAN-LISTP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-listp-of-remove-all-when-rw.crewrite-clause-plan-listp.proof
;; Reading the file took 0.93 seconds
;; Checking the proof took 20.25 seconds
;; VERIFY took 21.19 seconds
14058> VERIFY RW.CREWRITE-CLAUSE-PLAN-LISTP-OF-REMOVE-DUPLICATES
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-listp-of-remove-duplicates.proof
;; Reading the file took 1.22 seconds
;; Checking the proof took 20.65 seconds
;; VERIFY took 21.88 seconds
14059> VERIFY RW.CREWRITE-CLAUSE-PLAN-LISTP-OF-DIFFERENCE-WHEN-RW.CREWRITE-CLAUSE-PLAN-LISTP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-listp-of-difference-when-rw.crewrite-clause-plan-listp.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 20.18 seconds
;; VERIFY took 21.09 seconds
14060> VERIFY RW.CREWRITE-CLAUSE-PLAN-LISTP-OF-SUBSETP-WHEN-RW.CREWRITE-CLAUSE-PLAN-LISTP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-listp-of-subsetp-when-rw.crewrite-clause-plan-listp.proof
;; Reading the file took 1.28 seconds
;; Checking the proof took 20.48 seconds
;; VERIFY took 21.77 seconds
14061> VERIFY RW.CREWRITE-CLAUSE-PLAN-LISTP-OF-SUBSETP-WHEN-RW.CREWRITE-CLAUSE-PLAN-LISTP-ALT
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-listp-of-subsetp-when-rw.crewrite-clause-plan-listp-alt.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 19.17 seconds
;; VERIFY took 20.10 seconds
14062> VERIFY RW.CREWRITE-CLAUSE-PLAN-LISTP-OF-REPEAT
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-listp-of-repeat.proof
;; Reading the file took 1.19 seconds
;; Checking the proof took 26.87 seconds
;; VERIFY took 28.07 seconds
14063> DEFINE RW.CREWRITE-CLAUSE-PLAN-LIST-OKP
;; Reading from Proofs/level10/admit-rw.crewrite-clause-plan-list-okp.proofs
;; Reading the file took 1.22 seconds
;; Checking the proofs took 38.53 seconds
;; DEFINE took 39.76 seconds
14064> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-OKP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-okp.proof
;; Reading the file took 0.30 seconds
;; Checking the proof took 3.46 seconds
;; VERIFY took 3.78 seconds
14065> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-OKP-WHEN-NOT-CONSP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-okp-when-not-consp.proof
;; Reading the file took 1.17 seconds
;; Checking the proof took 26.81 seconds
;; VERIFY took 28.00 seconds
14066> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-OKP-OF-CONS
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-okp-of-cons.proof
;; Reading the file took 1.22 seconds
;; Checking the proof took 26.81 seconds
;; VERIFY took 28.04 seconds
14067> VERIFY BOOLEANP-OF-RW.CREWRITE-CLAUSE-PLAN-LIST-OKP
;; Reading from Proofs/level10/thm-booleanp-of-rw.crewrite-clause-plan-list-okp.proof
;; Reading the file took 1.21 seconds
;; Checking the proof took 20.16 seconds
;; VERIFY took 21.38 seconds
14068> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-OKP-OF-LIST-FIX
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-okp-of-list-fix.proof
;; Reading the file took 0.95 seconds
;; Checking the proof took 20.60 seconds
;; VERIFY took 21.56 seconds
14069> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-OKP-OF-APP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-okp-of-app.proof
;; Reading the file took 1.36 seconds
;; Checking the proof took 21.75 seconds
;; VERIFY took 23.12 seconds
14070> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-OKP-OF-REV
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-okp-of-rev.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 20.77 seconds
;; VERIFY took 21.69 seconds
14071> VERIFY RW.CREWRITE-CLAUSE-PLAN-OKP-OF-CAR-WHEN-RW.CREWRITE-CLAUSE-PLAN-LIST-OKP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-okp-of-car-when-rw.crewrite-clause-plan-list-okp.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 19.37 seconds
;; VERIFY took 20.29 seconds
14072> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-OKP-OF-CDR-WHEN-RW.CREWRITE-CLAUSE-PLAN-LIST-OKP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-okp-of-cdr-when-rw.crewrite-clause-plan-list-okp.proof
;; Reading the file took 1.21 seconds
;; Checking the proof took 19.33 seconds
;; VERIFY took 20.55 seconds
14073> VERIFY RW.CREWRITE-CLAUSE-PLAN-OKP-WHEN-MEMBERP-OF-RW.CREWRITE-CLAUSE-PLAN-LIST-OKP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-okp-when-memberp-of-rw.crewrite-clause-plan-list-okp.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 20.37 seconds
;; VERIFY took 21.29 seconds
14074> VERIFY RW.CREWRITE-CLAUSE-PLAN-OKP-WHEN-MEMBERP-OF-RW.CREWRITE-CLAUSE-PLAN-LIST-OKP-ALT
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-okp-when-memberp-of-rw.crewrite-clause-plan-list-okp-alt.proof
;; Reading the file took 1.23 seconds
;; Checking the proof took 19.34 seconds
;; VERIFY took 20.58 seconds
14075> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-OKP-OF-REMOVE-ALL-WHEN-RW.CREWRITE-CLAUSE-PLAN-LIST-OKP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-okp-of-remove-all-when-rw.crewrite-clause-plan-list-okp.proof
;; Reading the file took 0.95 seconds
;; Checking the proof took 20.02 seconds
;; VERIFY took 20.98 seconds
14076> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-OKP-OF-REMOVE-DUPLICATES
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-okp-of-remove-duplicates.proof
;; Reading the file took 1.22 seconds
;; Checking the proof took 20.68 seconds
;; VERIFY took 21.91 seconds
14077> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-OKP-OF-DIFFERENCE-WHEN-RW.CREWRITE-CLAUSE-PLAN-LIST-OKP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-okp-of-difference-when-rw.crewrite-clause-plan-list-okp.proof
;; Reading the file took 0.96 seconds
;; Checking the proof took 20.31 seconds
;; VERIFY took 21.28 seconds
14078> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-OKP-OF-SUBSETP-WHEN-RW.CREWRITE-CLAUSE-PLAN-LIST-OKP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-okp-of-subsetp-when-rw.crewrite-clause-plan-list-okp.proof
;; Reading the file took 1.21 seconds
;; Checking the proof took 20.65 seconds
;; VERIFY took 21.88 seconds
14079> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-OKP-OF-SUBSETP-WHEN-RW.CREWRITE-CLAUSE-PLAN-LIST-OKP-ALT
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-okp-of-subsetp-when-rw.crewrite-clause-plan-list-okp-alt.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 19.31 seconds
;; VERIFY took 20.23 seconds
14080> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-OKP-OF-REPEAT
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-okp-of-repeat.proof
;; Reading the file took 0.93 seconds
;; Checking the proof took 27.97 seconds
;; VERIFY took 28.91 seconds
14081> DEFINE RW.CREWRITE-CLAUSE-PLAN-LIST-ATBLP
;; Reading from Proofs/level10/admit-rw.crewrite-clause-plan-list-atblp.proofs
;; Reading the file took 1.24 seconds
;; Checking the proofs took 38.78 seconds
;; DEFINE took 40.03 seconds
14082> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-ATBLP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-atblp.proof
;; Reading the file took 0.26 seconds
;; Checking the proof took 3.47 seconds
;; VERIFY took 3.74 seconds
14083> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-ATBLP-WHEN-NOT-CONSP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-atblp-when-not-consp.proof
;; Reading the file took 0.96 seconds
;; Checking the proof took 27.08 seconds
;; VERIFY took 28.06 seconds
14084> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-ATBLP-OF-CONS
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-atblp-of-cons.proof
;; Reading the file took 0.97 seconds
;; Checking the proof took 27.02 seconds
;; VERIFY took 28.00 seconds
14085> VERIFY BOOLEANP-OF-RW.CREWRITE-CLAUSE-PLAN-LIST-ATBLP
;; Reading from Proofs/level10/thm-booleanp-of-rw.crewrite-clause-plan-list-atblp.proof
;; Reading the file took 1.24 seconds
;; Checking the proof took 20.29 seconds
;; VERIFY took 21.54 seconds
14086> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-ATBLP-OF-LIST-FIX
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-atblp-of-list-fix.proof
;; Reading the file took 0.93 seconds
;; Checking the proof took 20.69 seconds
;; VERIFY took 21.63 seconds
14087> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-ATBLP-OF-APP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-atblp-of-app.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 21.59 seconds
;; VERIFY took 22.52 seconds
14088> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-ATBLP-OF-REV
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-atblp-of-rev.proof
;; Reading the file took 1.23 seconds
;; Checking the proof took 20.14 seconds
;; VERIFY took 21.38 seconds
14089> VERIFY RW.CREWRITE-CLAUSE-PLAN-ATBLP-OF-CAR-WHEN-RW.CREWRITE-CLAUSE-PLAN-LIST-ATBLP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-atblp-of-car-when-rw.crewrite-clause-plan-list-atblp.proof
;; Reading the file took 0.93 seconds
;; Checking the proof took 19.41 seconds
;; VERIFY took 20.35 seconds
14090> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-ATBLP-OF-CDR-WHEN-RW.CREWRITE-CLAUSE-PLAN-LIST-ATBLP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-atblp-of-cdr-when-rw.crewrite-clause-plan-list-atblp.proof
;; Reading the file took 1.26 seconds
;; Checking the proof took 19.33 seconds
;; VERIFY took 20.61 seconds
14091> VERIFY RW.CREWRITE-CLAUSE-PLAN-ATBLP-WHEN-MEMBERP-OF-RW.CREWRITE-CLAUSE-PLAN-LIST-ATBLP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-atblp-when-memberp-of-rw.crewrite-clause-plan-list-atblp.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 20.38 seconds
;; VERIFY took 21.31 seconds
14092> VERIFY RW.CREWRITE-CLAUSE-PLAN-ATBLP-WHEN-MEMBERP-OF-RW.CREWRITE-CLAUSE-PLAN-LIST-ATBLP-ALT
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-atblp-when-memberp-of-rw.crewrite-clause-plan-list-atblp-alt.proof
;; Reading the file took 1.21 seconds
;; Checking the proof took 19.47 seconds
;; VERIFY took 20.69 seconds
14093> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-ATBLP-OF-REMOVE-ALL-WHEN-RW.CREWRITE-CLAUSE-PLAN-LIST-ATBLP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-atblp-of-remove-all-when-rw.crewrite-clause-plan-list-atblp.proof
;; Reading the file took 0.96 seconds
;; Checking the proof took 20.35 seconds
;; VERIFY took 21.33 seconds
14094> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-ATBLP-OF-REMOVE-DUPLICATES
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-atblp-of-remove-duplicates.proof
;; Reading the file took 0.95 seconds
;; Checking the proof took 20.60 seconds
;; VERIFY took 21.56 seconds
14095> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-ATBLP-OF-DIFFERENCE-WHEN-RW.CREWRITE-CLAUSE-PLAN-LIST-ATBLP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-atblp-of-difference-when-rw.crewrite-clause-plan-list-atblp.proof
;; Reading the file took 1.19 seconds
;; Checking the proof took 20.28 seconds
;; VERIFY took 21.48 seconds
14096> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-ATBLP-OF-SUBSETP-WHEN-RW.CREWRITE-CLAUSE-PLAN-LIST-ATBLP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-atblp-of-subsetp-when-rw.crewrite-clause-plan-list-atblp.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 20.48 seconds
;; VERIFY took 21.40 seconds
14097> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-ATBLP-OF-SUBSETP-WHEN-RW.CREWRITE-CLAUSE-PLAN-LIST-ATBLP-ALT
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-atblp-of-subsetp-when-rw.crewrite-clause-plan-list-atblp-alt.proof
;; Reading the file took 1.22 seconds
;; Checking the proof took 19.29 seconds
;; VERIFY took 20.52 seconds
14098> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-ATBLP-OF-REPEAT
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-atblp-of-repeat.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 27.90 seconds
;; VERIFY took 28.83 seconds
14099> DEFINE RW.MAKE-CREWRITE-CLAUSE-PLAN-LIST
;; Reading from Proofs/level10/admit-rw.make-crewrite-clause-plan-list.proofs
;; Reading the file took 0.90 seconds
;; Checking the proofs took 38.56 seconds
;; DEFINE took 39.47 seconds
14100> VERIFY RW.MAKE-CREWRITE-CLAUSE-PLAN-LIST
;; Reading from Proofs/level10/thm-rw.make-crewrite-clause-plan-list.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.73 seconds
;; VERIFY took 3.96 seconds
14101> DEFINE RW.FAST-MAKE-CREWRITE-CLAUSE-PLAN-LIST$
;; Reading from Proofs/level10/admit-rw.fast-make-crewrite-clause-plan-list$.proofs
;; Reading the file took 0.97 seconds
;; Checking the proofs took 38.13 seconds
;; DEFINE took 39.10 seconds
14102> VERIFY RW.FAST-MAKE-CREWRITE-CLAUSE-PLAN-LIST$
;; Reading from Proofs/level10/thm-rw.fast-make-crewrite-clause-plan-list$.proof
;; Reading the file took 0.24 seconds
;; Checking the proof took 3.47 seconds
;; VERIFY took 3.72 seconds
14103> VERIFY RW.MAKE-CREWRITE-CLAUSE-PLAN-LIST-WHEN-NOT-CONSP
;; Reading from Proofs/level10/thm-rw.make-crewrite-clause-plan-list-when-not-consp.proof
;; Reading the file took 1.17 seconds
;; Checking the proof took 27.19 seconds
;; VERIFY took 28.37 seconds
14104> VERIFY RW.MAKE-CREWRITE-CLAUSE-PLAN-LIST-OF-CONS
;; Reading from Proofs/level10/thm-rw.make-crewrite-clause-plan-list-of-cons.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 27.25 seconds
;; VERIFY took 28.17 seconds
14105> VERIFY TRUE-LISTP-OF-RW.MAKE-CREWRITE-CLAUSE-PLAN-LIST
;; Reading from Proofs/level10/thm-true-listp-of-rw.make-crewrite-clause-plan-list.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 20.06 seconds
;; VERIFY took 20.98 seconds
14106> VERIFY LEN-OF-RW.MAKE-CREWRITE-CLAUSE-PLAN-LIST
;; Reading from Proofs/level10/thm-len-of-rw.make-crewrite-clause-plan-list.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 20.19 seconds
;; VERIFY took 21.12 seconds
14107> VERIFY CONSP-OF-RW.MAKE-CREWRITE-CLAUSE-PLAN-LIST
;; Reading from Proofs/level10/thm-consp-of-rw.make-crewrite-clause-plan-list.proof
;; Reading the file took 1.21 seconds
;; Checking the proof took 20.48 seconds
;; VERIFY took 21.70 seconds
14108> VERIFY CAR-OF-RW.MAKE-CREWRITE-CLAUSE-PLAN-LIST
;; Reading from Proofs/level10/thm-car-of-rw.make-crewrite-clause-plan-list.proof
;; Reading the file took 0.93 seconds
;; Checking the proof took 19.34 seconds
;; VERIFY took 20.29 seconds
14109> VERIFY CDR-OF-RW.MAKE-CREWRITE-CLAUSE-PLAN-LIST
;; Reading from Proofs/level10/thm-cdr-of-rw.make-crewrite-clause-plan-list.proof
;; Reading the file took 1.21 seconds
;; Checking the proof took 19.36 seconds
;; VERIFY took 20.58 seconds
14110> VERIFY RW.MAKE-CREWRITE-CLAUSE-PLAN-LIST-UNDER-IFF
;; Reading from Proofs/level10/thm-rw.make-crewrite-clause-plan-list-under-iff.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 19.34 seconds
;; VERIFY took 20.27 seconds
14111> VERIFY RW.MAKE-CREWRITE-CLAUSE-PLAN-LIST-OF-LIST-FIX
;; Reading from Proofs/level10/thm-rw.make-crewrite-clause-plan-list-of-list-fix.proof
;; Reading the file took 1.23 seconds
;; Checking the proof took 20.09 seconds
;; VERIFY took 21.34 seconds
14112> VERIFY RW.MAKE-CREWRITE-CLAUSE-PLAN-LIST-OF-APP
;; Reading from Proofs/level10/thm-rw.make-crewrite-clause-plan-list-of-app.proof
;; Reading the file took 0.96 seconds
;; Checking the proof took 20.22 seconds
;; VERIFY took 21.19 seconds
14113> VERIFY REV-OF-RW.MAKE-CREWRITE-CLAUSE-PLAN-LIST
;; Reading from Proofs/level10/thm-rev-of-rw.make-crewrite-clause-plan-list.proof
;; Reading the file took 1.23 seconds
;; Checking the proof took 20.53 seconds
;; VERIFY took 21.77 seconds
14114> VERIFY RW.MAKE-CREWRITE-CLAUSE-PLAN-LIST-OF-REV
;; Reading from Proofs/level10/thm-rw.make-crewrite-clause-plan-list-of-rev.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 19.31 seconds
;; VERIFY took 20.21 seconds
14115> VERIFY FIRSTN-OF-RW.MAKE-CREWRITE-CLAUSE-PLAN-LIST
;; Reading from Proofs/level10/thm-firstn-of-rw.make-crewrite-clause-plan-list.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 28.53 seconds
;; VERIFY took 29.44 seconds
14116> VERIFY RESTN-OF-RW.MAKE-CREWRITE-CLAUSE-PLAN-LIST
;; Reading from Proofs/level10/thm-restn-of-rw.make-crewrite-clause-plan-list.proof
;; Reading the file took 1.21 seconds
;; Checking the proof took 27.76 seconds
;; VERIFY took 28.98 seconds
14117> VERIFY MEMBERP-OF-RW.MAKE-CREWRITE-CLAUSE-PLAN-IN-RW.MAKE-CREWRITE-CLAUSE-PLAN-LIST-WHEN-MEMBERP
;; Reading from Proofs/level10/thm-memberp-of-rw.make-crewrite-clause-plan-in-rw.make-crewrite-clause-plan-list-when-memberp.proof
;; Reading the file took 1.23 seconds
;; Checking the proof took 20.50 seconds
;; VERIFY took 21.75 seconds
14118> VERIFY SUBSETP-OF-RW.MAKE-CREWRITE-CLAUSE-PLAN-LISTS-WHEN-SUBSETP
;; Reading from Proofs/level10/thm-subsetp-of-rw.make-crewrite-clause-plan-lists-when-subsetp.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 20.54 seconds
;; VERIFY took 21.47 seconds
14119> VERIFY RW.FAST-MAKE-CREWRITE-CLAUSE-PLAN-LIST$-REMOVAL
;; Reading from Proofs/level10/thm-rw.fast-make-crewrite-clause-plan-list$-removal.proof
;; Reading the file took 1.22 seconds
;; Checking the proof took 28.74 seconds
;; VERIFY took 29.97 seconds
14120> DEFINE RW.CREWRITE-CLAUSE-PLAN-LIST->PROGRESSP
;; Reading from Proofs/level10/admit-rw.crewrite-clause-plan-list-_gt_progressp.proofs
;; Reading the file took 1.21 seconds
;; Checking the proofs took 38.83 seconds
;; DEFINE took 40.05 seconds
14121> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST->PROGRESSP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-_gt_progressp.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.48 seconds
;; VERIFY took 3.71 seconds
14122> DEFINE RW.CREWRITE-CLAUSE-PLAN-LIST->CLAUSES
;; Reading from Proofs/level10/admit-rw.crewrite-clause-plan-list-_gt_clauses.proofs
;; Reading the file took 0.96 seconds
;; Checking the proofs took 38.48 seconds
;; DEFINE took 39.45 seconds
14123> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST->CLAUSES
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-_gt_clauses.proof
;; Reading the file took 0.49 seconds
;; Checking the proof took 3.48 seconds
;; VERIFY took 3.98 seconds
14124> DEFINE RW.FAST-CREWRITE-CLAUSE-PLAN-LIST->CLAUSES$
;; Reading from Proofs/level10/admit-rw.fast-crewrite-clause-plan-list-_gt_clauses$.proofs
;; Reading the file took 0.90 seconds
;; Checking the proofs took 38.46 seconds
;; DEFINE took 39.36 seconds
14125> VERIFY RW.FAST-CREWRITE-CLAUSE-PLAN-LIST->CLAUSES$
;; Reading from Proofs/level10/thm-rw.fast-crewrite-clause-plan-list-_gt_clauses$.proof
;; Reading the file took 0.25 seconds
;; Checking the proof took 3.73 seconds
;; VERIFY took 4.00 seconds
14126> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST->CLAUSES-WHEN-NOT-CONSP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-_gt_clauses-when-not-consp.proof
;; Reading the file took 0.89 seconds
;; Checking the proof took 27.16 seconds
;; VERIFY took 28.07 seconds
14127> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST->CLAUSES-OF-CONS
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-_gt_clauses-of-cons.proof
;; Reading the file took 0.93 seconds
;; Checking the proof took 26.78 seconds
;; VERIFY took 27.72 seconds
14128> VERIFY TRUE-LISTP-OF-RW.CREWRITE-CLAUSE-PLAN-LIST->CLAUSES
;; Reading from Proofs/level10/thm-true-listp-of-rw.crewrite-clause-plan-list-_gt_clauses.proof
;; Reading the file took 0.97 seconds
;; Checking the proof took 20.03 seconds
;; VERIFY took 21.01 seconds
14129> VERIFY LEN-OF-RW.CREWRITE-CLAUSE-PLAN-LIST->CLAUSES
;; Reading from Proofs/level10/thm-len-of-rw.crewrite-clause-plan-list-_gt_clauses.proof
;; Reading the file took 1.23 seconds
;; Checking the proof took 20.30 seconds
;; VERIFY took 21.54 seconds
14130> VERIFY CONSP-OF-RW.CREWRITE-CLAUSE-PLAN-LIST->CLAUSES
;; Reading from Proofs/level10/thm-consp-of-rw.crewrite-clause-plan-list-_gt_clauses.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 20.47 seconds
;; VERIFY took 21.40 seconds
14131> VERIFY CAR-OF-RW.CREWRITE-CLAUSE-PLAN-LIST->CLAUSES
;; Reading from Proofs/level10/thm-car-of-rw.crewrite-clause-plan-list-_gt_clauses.proof
;; Reading the file took 1.21 seconds
;; Checking the proof took 19.53 seconds
;; VERIFY took 20.75 seconds
14132> VERIFY CDR-OF-RW.CREWRITE-CLAUSE-PLAN-LIST->CLAUSES
;; Reading from Proofs/level10/thm-cdr-of-rw.crewrite-clause-plan-list-_gt_clauses.proof
;; Reading the file took 0.93 seconds
;; Checking the proof took 19.45 seconds
;; VERIFY took 20.40 seconds
14133> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST->CLAUSES-UNDER-IFF
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-_gt_clauses-under-iff.proof
;; Reading the file took 0.93 seconds
;; Checking the proof took 19.34 seconds
;; VERIFY took 20.28 seconds
14134> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST->CLAUSES-OF-LIST-FIX
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-_gt_clauses-of-list-fix.proof
;; Reading the file took 1.25 seconds
;; Checking the proof took 20.06 seconds
;; VERIFY took 21.32 seconds
14135> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST->CLAUSES-OF-APP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-_gt_clauses-of-app.proof
;; Reading the file took 0.95 seconds
;; Checking the proof took 20.13 seconds
;; VERIFY took 21.09 seconds
14136> VERIFY REV-OF-RW.CREWRITE-CLAUSE-PLAN-LIST->CLAUSES
;; Reading from Proofs/level10/thm-rev-of-rw.crewrite-clause-plan-list-_gt_clauses.proof
;; Reading the file took 1.26 seconds
;; Checking the proof took 20.43 seconds
;; VERIFY took 21.70 seconds
14137> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST->CLAUSES-OF-REV
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-_gt_clauses-of-rev.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 19.26 seconds
;; VERIFY took 20.19 seconds
14138> VERIFY FIRSTN-OF-RW.CREWRITE-CLAUSE-PLAN-LIST->CLAUSES
;; Reading from Proofs/level10/thm-firstn-of-rw.crewrite-clause-plan-list-_gt_clauses.proof
;; Reading the file took 1.26 seconds
;; Checking the proof took 28.42 seconds
;; VERIFY took 29.70 seconds
14139> VERIFY RESTN-OF-RW.CREWRITE-CLAUSE-PLAN-LIST->CLAUSES
;; Reading from Proofs/level10/thm-restn-of-rw.crewrite-clause-plan-list-_gt_clauses.proof
;; Reading the file took 1.25 seconds
;; Checking the proof took 27.77 seconds
;; VERIFY took 29.03 seconds
14140> VERIFY MEMBERP-OF-RW.CREWRITE-CLAUSE-PLAN->CLAUSE-IN-RW.CREWRITE-CLAUSE-PLAN-LIST->CLAUSES-WHEN-MEMBERP
;; Reading from Proofs/level10/thm-memberp-of-rw.crewrite-clause-plan-_gt_clause-in-rw.crewrite-clause-plan-list-_gt_clauses-when-memberp.proof
;; Reading the file took 1.24 seconds
;; Checking the proof took 20.47 seconds
;; VERIFY took 21.72 seconds
14141> VERIFY SUBSETP-OF-RW.CREWRITE-CLAUSE-PLAN-LIST->CLAUSESS-WHEN-SUBSETP
;; Reading from Proofs/level10/thm-subsetp-of-rw.crewrite-clause-plan-list-_gt_clausess-when-subsetp.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 20.23 seconds
;; VERIFY took 21.16 seconds
14142> VERIFY RW.FAST-CREWRITE-CLAUSE-PLAN-LIST->CLAUSES$-REMOVAL
;; Reading from Proofs/level10/thm-rw.fast-crewrite-clause-plan-list-_gt_clauses$-removal.proof
;; Reading the file took 1.25 seconds
;; Checking the proof took 28.66 seconds
;; VERIFY took 29.92 seconds
14143> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST->CLAUSES-OF-RW.MAKE-CREWRITE-CLAUSE-PLAN-LIST
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-_gt_clauses-of-rw.make-crewrite-clause-plan-list.proof
;; Reading the file took 1.45 seconds
;; Checking the proof took 19.95 seconds
;; VERIFY took 21.41 seconds
14144> DEFINE RW.CREWRITE-CLAUSE-PLAN-LIST->CLAUSES-PRIME
;; Reading from Proofs/level10/admit-rw.crewrite-clause-plan-list-_gt_clauses-prime.proofs
;; Reading the file took 0.91 seconds
;; Checking the proofs took 58.09 seconds
;; DEFINE took 59.02 seconds
14145> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST->CLAUSES-PRIME
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-_gt_clauses-prime.proof
;; Reading the file took 0.23 seconds
;; Checking the proof took 3.72 seconds
;; VERIFY took 3.97 seconds
14146> VERIFY CONS-LISTP-OF-RW.CREWRITE-CLAUSE-PLAN-LIST->CLAUSES-PRIME
;; Reading from Proofs/level10/thm-cons-listp-of-rw.crewrite-clause-plan-list-_gt_clauses-prime.proof
;; Reading the file took 0.94 seconds
;; Checking the proof took 28.53 seconds
;; VERIFY took 29.48 seconds
14147> VERIFY LOGIC.TERM-LIST-LISTP-OF-RW.CREWRITE-CLAUSE-PLAN-LIST->CLAUSES-PRIME
;; Reading from Proofs/level10/thm-logic.term-list-listp-of-rw.crewrite-clause-plan-list-_gt_clauses-prime.proof
;; Reading the file took 0.96 seconds
;; Checking the proof took 28.45 seconds
;; VERIFY took 29.42 seconds
14148> DEFINE RW.CREWRITE-CLAUSE-PLAN-LIST->FORCED-GOALS
;; Reading from Proofs/level10/admit-rw.crewrite-clause-plan-list-_gt_forced-goals.proofs
;; Reading the file took 0.91 seconds
;; Checking the proofs took 38.66 seconds
;; DEFINE took 39.58 seconds
14149> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST->FORCED-GOALS
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-_gt_forced-goals.proof
;; Reading the file took 0.25 seconds
;; Checking the proof took 3.73 seconds
;; VERIFY took 3.99 seconds
14150> VERIFY TRUE-LISTP-OF-RW.CREWRITE-CLAUSE-PLAN-LIST->FORCED-GOALS
;; Reading from Proofs/level10/thm-true-listp-of-rw.crewrite-clause-plan-list-_gt_forced-goals.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 27.90 seconds
;; VERIFY took 28.83 seconds
14151> VERIFY LOGIC.FORMULA-LISTP-OF-RW.CREWRITE-CLAUSE-PLAN-LIST->FORCED-GOALS
;; Reading from Proofs/level10/thm-logic.formula-listp-of-rw.crewrite-clause-plan-list-_gt_forced-goals.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 28.30 seconds
;; VERIFY took 29.23 seconds
14152> VERIFY LOGIC.FORMULA-LIST-ATBLP-OF-RW.CREWRITE-CLAUSE-PLAN-LIST->FORCED-GOALS
;; Reading from Proofs/level10/thm-logic.formula-list-atblp-of-rw.crewrite-clause-plan-list-_gt_forced-goals.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 33.37 seconds
;; VERIFY took 34.31 seconds
14153> VERIFY RW.CREWRITE-CLAUSE-PLAN-LISTP-OF-RW.MAKE-CREWRITE-CLAUSE-PLAN-LIST
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-listp-of-rw.make-crewrite-clause-plan-list.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 20.99 seconds
;; VERIFY took 21.91 seconds
14154> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-OKP-OF-RW.MAKE-CREWRITE-CLAUSE-PLAN-LIST
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-okp-of-rw.make-crewrite-clause-plan-list.proof
;; Reading the file took 1.22 seconds
;; Checking the proof took 21.07 seconds
;; VERIFY took 22.31 seconds
14155> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-ATBLP-OF-RW.MAKE-CREWRITE-CLAUSE-PLAN-LIST
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-atblp-of-rw.make-crewrite-clause-plan-list.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 20.37 seconds
;; VERIFY took 21.30 seconds
14156> DEFINE RW.CREWRITE-CLAUSE-PLAN-LIST-COMPILER
;; Reading from Proofs/level10/admit-rw.crewrite-clause-plan-list-compiler.proofs
;; Reading the file took 1.23 seconds
;; Checking the proofs took 58.37 seconds
;; DEFINE took 59.61 seconds
14157> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-COMPILER
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-compiler.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.49 seconds
;; VERIFY took 3.73 seconds
14158> VERIFY LOGIC.APPEAL-LISTP-OF-RW.CREWRITE-CLAUSE-PLAN-LIST-COMPILER
;; Reading from Proofs/level10/thm-logic.appeal-listp-of-rw.crewrite-clause-plan-list-compiler.proof
;; Reading the file took 1.25 seconds
;; Checking the proof took 60.42 seconds
;; VERIFY took 61.69 seconds
14159> VERIFY LOGIC.STRIP-CONCLUSIONS-OF-RW.CREWRITE-CLAUSE-PLAN-LIST-COMPILER
;; Reading from Proofs/level10/thm-logic.strip-conclusions-of-rw.crewrite-clause-plan-list-compiler.proof
;; Reading the file took 0.97 seconds
;; Checking the proof took 67.10 seconds
;; VERIFY took 68.09 seconds
14160> VERIFY LOGIC.PROOF-LISTP-OF-RW.CREWRITE-CLAUSE-PLAN-LIST-COMPILER
;; Reading from Proofs/level10/thm-logic.proof-listp-of-rw.crewrite-clause-plan-list-compiler.proof
;; Reading the file took 1.09 seconds
;; Checking the proof took 246.03 seconds
;; VERIFY took 247.24 seconds
14161> VERIFY RW.CREWRITE-CLAUSE-PLAN-ATBLP-REMOVAL
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-atblp-removal.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 27.22 seconds
;; VERIFY took 28.13 seconds
14162> VERIFY RW.CREWRITE-CLAUSE-PLAN-LIST-ATBLP-REMOVAL
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-list-atblp-removal.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 36.10 seconds
;; VERIFY took 37.02 seconds
14163> VERIFY CONSP-OF-RW.CREWRITE-CLAUSE-PLAN->CLAUSE
;; Reading from Proofs/level10/thm-consp-of-rw.crewrite-clause-plan-_gt_clause.proof
;; Reading the file took 0.93 seconds
;; Checking the proof took 26.94 seconds
;; VERIFY took 27.88 seconds
14164> VERIFY LOGIC.TERM-LISTP-OF-RW.CREWRITE-CLAUSE-PLAN->CLAUSE
;; Reading from Proofs/level10/thm-logic.term-listp-of-rw.crewrite-clause-plan-_gt_clause.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 27.60 seconds
;; VERIFY took 28.52 seconds
14165> DEFINE RW.CREWRITE-CLAUSE-PLAN-COMPILER-OKP
;; Reading from Proofs/level10/admit-rw.crewrite-clause-plan-compiler-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.03 seconds
14166> VERIFY RW.CREWRITE-CLAUSE-PLAN-COMPILER-OKP
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-compiler-okp.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.48 seconds
;; VERIFY took 3.73 seconds
14167> VERIFY BOOLEANP-OF-RW.CREWRITE-CLAUSE-PLAN-COMPILER-OKP
;; Reading from Proofs/level10/thm-booleanp-of-rw.crewrite-clause-plan-compiler-okp.proof
;; Reading the file took 1.18 seconds
;; Checking the proof took 20.42 seconds
;; VERIFY took 21.61 seconds
14168> VERIFY RW.CREWRITE-CLAUSE-PLAN-COMPILER-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level10/thm-rw.crewrite-clause-plan-compiler-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 19.66 seconds
;; VERIFY took 20.58 seconds
14169> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-RW.CREWRITE-CLAUSE-PLAN-COMPILER-OKP
;; Reading from Proofs/level10/thm-lemma-1-for-soundness-of-rw.crewrite-clause-plan-compiler-okp.proof
;; Reading the file took 1.21 seconds
;; Checking the proof took 21.68 seconds
;; VERIFY took 22.92 seconds
14170> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-RW.CREWRITE-CLAUSE-PLAN-COMPILER-OKP
;; Reading from Proofs/level10/thm-lemma-2-for-soundness-of-rw.crewrite-clause-plan-compiler-okp.proof
;; Reading the file took 0.94 seconds
;; Checking the proof took 32.23 seconds
;; VERIFY took 33.29 seconds
14171> VERIFY FORCING-SOUNDNESS-OF-RW.CREWRITE-CLAUSE-PLAN-COMPILER-OKP
;; Reading from Proofs/level10/thm-forcing-soundness-of-rw.crewrite-clause-plan-compiler-okp.proof
;; Reading the file took 1.03 seconds
;; Checking the proof took 82.90 seconds
;; VERIFY took 84.04 seconds
14172> DEFINE LEVEL10.STEP-OKP
;; Reading from Proofs/level10/admit-level10.step-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
14173> VERIFY LEVEL10.STEP-OKP
;; Reading from Proofs/level10/thm-level10.step-okp.proof
;; Reading the file took 0.25 seconds
;; Checking the proof took 3.72 seconds
;; VERIFY took 3.98 seconds
14174> VERIFY SOUNDNESS-OF-LEVEL10.STEP-OKP
;; Reading from Proofs/level10/thm-soundness-of-level10.step-okp.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 20.00 seconds
;; VERIFY took 21.04 seconds
14175> VERIFY LEVEL10.STEP-OKP-WHEN-LEVEL9.STEP-OKP
;; Reading from Proofs/level10/thm-level10.step-okp-when-level9.step-okp.proof
;; Reading the file took 1.29 seconds
;; Checking the proof took 100.22 seconds
;; VERIFY took 101.52 seconds
14176> VERIFY LEVEL10.STEP-OKP-WHEN-NOT-CONSP
;; Reading from Proofs/level10/thm-level10.step-okp-when-not-consp.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 27.43 seconds
;; VERIFY took 28.36 seconds
14177> DEFINE LEVEL10.FLAG-PROOFP-AUX
;; Reading from Proofs/level10/admit-level10.flag-proofp-aux.proofs
;; Reading the file took 0.99 seconds
;; Checking the proofs took 78.41 seconds
;; DEFINE took 79.42 seconds
14178> VERIFY LEVEL10.FLAG-PROOFP-AUX
;; Reading from Proofs/level10/thm-level10.flag-proofp-aux.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.75 seconds
;; VERIFY took 3.98 seconds
14179> DEFINE LEVEL10.PROOFP-AUX
;; Reading from Proofs/level10/admit-level10.proofp-aux.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
14180> VERIFY LEVEL10.PROOFP-AUX
;; Reading from Proofs/level10/thm-level10.proofp-aux.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.48 seconds
;; VERIFY took 3.71 seconds
14181> DEFINE LEVEL10.PROOF-LISTP-AUX
;; Reading from Proofs/level10/admit-level10.proof-listp-aux.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
14182> VERIFY LEVEL10.PROOF-LISTP-AUX
;; Reading from Proofs/level10/thm-level10.proof-listp-aux.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.48 seconds
;; VERIFY took 3.71 seconds
14183> VERIFY DEFINITION-OF-LEVEL10.PROOFP-AUX
;; Reading from Proofs/level10/thm-definition-of-level10.proofp-aux.proof
;; Reading the file took 1.11 seconds
;; Checking the proof took 35.02 seconds
;; VERIFY took 36.14 seconds
14184> VERIFY DEFINITION-OF-LEVEL10.PROOF-LISTP-AUX
;; Reading from Proofs/level10/thm-definition-of-level10.proof-listp-aux.proof
;; Reading the file took 1.30 seconds
;; Checking the proof took 35.21 seconds
;; VERIFY took 36.53 seconds
14185> VERIFY LEVEL10.PROOFP-AUX-WHEN-NOT-CONSP
;; Reading from Proofs/level10/thm-level10.proofp-aux-when-not-consp.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 27.26 seconds
;; VERIFY took 28.18 seconds
14186> VERIFY LEVEL10.PROOF-LISTP-AUX-WHEN-NOT-CONSP
;; Reading from Proofs/level10/thm-level10.proof-listp-aux-when-not-consp.proof
;; Reading the file took 1.22 seconds
;; Checking the proof took 26.52 seconds
;; VERIFY took 27.75 seconds
14187> VERIFY LEVEL10.PROOF-LISTP-AUX-OF-CONS
;; Reading from Proofs/level10/thm-level10.proof-listp-aux-of-cons.proof
;; Reading the file took 1.23 seconds
;; Checking the proof took 27.03 seconds
;; VERIFY took 28.27 seconds
14188> VERIFY LEMMA-FOR-BOOLEANP-OF-LEVEL10.PROOFP-AUX
;; Reading from Proofs/level10/thm-lemma-for-booleanp-of-level10.proofp-aux.proof
;; Reading the file took 1.24 seconds
;; Checking the proof took 40.50 seconds
;; VERIFY took 41.75 seconds
14189> VERIFY BOOLEANP-OF-LEVEL10.PROOFP-AUX
;; Reading from Proofs/level10/thm-booleanp-of-level10.proofp-aux.proof
;; Reading the file took 1.24 seconds
;; Checking the proof took 19.89 seconds
;; VERIFY took 21.14 seconds
14190> VERIFY BOOLEANP-OF-LEVEL10.PROOF-LISTP-AUX
;; Reading from Proofs/level10/thm-booleanp-of-level10.proof-listp-aux.proof
;; Reading the file took 1.14 seconds
;; Checking the proof took 19.71 seconds
;; VERIFY took 20.86 seconds
14191> VERIFY LEVEL10.PROOF-LISTP-AUX-OF-LIST-FIX
;; Reading from Proofs/level10/thm-level10.proof-listp-aux-of-list-fix.proof
;; Reading the file took 0.93 seconds
;; Checking the proof took 20.86 seconds
;; VERIFY took 21.80 seconds
14192> VERIFY LEVEL10.PROOF-LISTP-AUX-OF-APP
;; Reading from Proofs/level10/thm-level10.proof-listp-aux-of-app.proof
;; Reading the file took 1.20 seconds
;; Checking the proof took 21.93 seconds
;; VERIFY took 23.15 seconds
14193> VERIFY LEVEL10.PROOF-LISTP-AUX-OF-REV
;; Reading from Proofs/level10/thm-level10.proof-listp-aux-of-rev.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 20.98 seconds
;; VERIFY took 21.89 seconds
14194> VERIFY LEVEL10.PROOFP-AUX-OF-CAR-WHEN-LEVEL10.PROOF-LISTP-AUX
;; Reading from Proofs/level10/thm-level10.proofp-aux-of-car-when-level10.proof-listp-aux.proof
;; Reading the file took 1.22 seconds
;; Checking the proof took 19.59 seconds
;; VERIFY took 20.82 seconds
14195> VERIFY LEVEL10.PROOF-LISTP-AUX-OF-CDR-WHEN-LEVEL10.PROOF-LISTP-AUX
;; Reading from Proofs/level10/thm-level10.proof-listp-aux-of-cdr-when-level10.proof-listp-aux.proof
;; Reading the file took 0.93 seconds
;; Checking the proof took 19.47 seconds
;; VERIFY took 20.41 seconds
14196> VERIFY LEVEL10.PROOFP-AUX-WHEN-MEMBERP-OF-LEVEL10.PROOF-LISTP-AUX
;; Reading from Proofs/level10/thm-level10.proofp-aux-when-memberp-of-level10.proof-listp-aux.proof
;; Reading the file took 1.22 seconds
;; Checking the proof took 20.52 seconds
;; VERIFY took 21.75 seconds
14197> VERIFY LEVEL10.PROOFP-AUX-WHEN-MEMBERP-OF-LEVEL10.PROOF-LISTP-AUX-ALT
;; Reading from Proofs/level10/thm-level10.proofp-aux-when-memberp-of-level10.proof-listp-aux-alt.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 19.43 seconds
;; VERIFY took 20.36 seconds
14198> VERIFY LEVEL10.PROOF-LISTP-AUX-OF-REMOVE-ALL-WHEN-LEVEL10.PROOF-LISTP-AUX
;; Reading from Proofs/level10/thm-level10.proof-listp-aux-of-remove-all-when-level10.proof-listp-aux.proof
;; Reading the file took 1.21 seconds
;; Checking the proof took 20.45 seconds
;; VERIFY took 21.67 seconds
14199> VERIFY LEVEL10.PROOF-LISTP-AUX-OF-REMOVE-DUPLICATES
;; Reading from Proofs/level10/thm-level10.proof-listp-aux-of-remove-duplicates.proof
;; Reading the file took 0.97 seconds
;; Checking the proof took 20.71 seconds
;; VERIFY took 21.70 seconds
14200> VERIFY LEVEL10.PROOF-LISTP-AUX-OF-DIFFERENCE-WHEN-LEVEL10.PROOF-LISTP-AUX
;; Reading from Proofs/level10/thm-level10.proof-listp-aux-of-difference-when-level10.proof-listp-aux.proof
;; Reading the file took 1.31 seconds
;; Checking the proof took 20.54 seconds
;; VERIFY took 21.87 seconds
14201> VERIFY LEVEL10.PROOF-LISTP-AUX-OF-SUBSETP-WHEN-LEVEL10.PROOF-LISTP-AUX
;; Reading from Proofs/level10/thm-level10.proof-listp-aux-of-subsetp-when-level10.proof-listp-aux.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 20.71 seconds
;; VERIFY took 21.64 seconds
14202> VERIFY LEVEL10.PROOF-LISTP-AUX-OF-SUBSETP-WHEN-LEVEL10.PROOF-LISTP-AUX-ALT
;; Reading from Proofs/level10/thm-level10.proof-listp-aux-of-subsetp-when-level10.proof-listp-aux-alt.proof
;; Reading the file took 0.90 seconds
;; Checking the proof took 19.27 seconds
;; VERIFY took 20.19 seconds
14203> VERIFY LEVEL10.PROOF-LISTP-AUX-OF-REPEAT
;; Reading from Proofs/level10/thm-level10.proof-listp-aux-of-repeat.proof
;; Reading the file took 1.18 seconds
;; Checking the proof took 28.35 seconds
;; VERIFY took 29.54 seconds
14204> VERIFY LEMMA-FOR-LOGIC.PROVABLEP-WHEN-LEVEL10.PROOFP-AUX
;; Reading from Proofs/level10/thm-lemma-for-logic.provablep-when-level10.proofp-aux.proof
;; Reading the file took 2.03 seconds
;; Checking the proof took 216.11 seconds
;; VERIFY took 218.27 seconds
14205> VERIFY LOGIC.PROVABLEP-WHEN-LEVEL10.PROOFP-AUX
;; Reading from Proofs/level10/thm-logic.provablep-when-level10.proofp-aux.proof
;; Reading the file took 0.92 seconds
;; Checking the proof took 26.82 seconds
;; VERIFY took 27.86 seconds
14206> VERIFY LOGIC.PROVABLE-LISTP-WHEN-LEVEL10.PROOF-LISTP-AUX
;; Reading from Proofs/level10/thm-logic.provable-listp-when-level10.proof-listp-aux.proof
;; Reading the file took 1.23 seconds
;; Checking the proof took 26.98 seconds
;; VERIFY took 28.33 seconds
14207> VERIFY LEMMA-FOR-LEVEL10.PROOFP-AUX-WHEN-LOGIC.PROOFP
;; Reading from Proofs/level10/thm-lemma-for-level10.proofp-aux-when-logic.proofp.proof
;; Reading the file took 0.94 seconds
;; Checking the proof took 55.63 seconds
;; VERIFY took 56.59 seconds
14208> VERIFY LEVEL10.PROOFP-AUX-WHEN-LOGIC.PROOFP
;; Reading from Proofs/level10/thm-level10.proofp-aux-when-logic.proofp.proof
;; Reading the file took 1.20 seconds
;; Checking the proof took 19.75 seconds
;; VERIFY took 20.96 seconds
14209> VERIFY LEVEL10.PROOF-LISTP-AUX-WHEN-LOGIC.PROOF-LISTP
;; Reading from Proofs/level10/thm-level10.proof-listp-aux-when-logic.proof-listp.proof
;; Reading the file took 1.04 seconds
;; Checking the proof took 19.67 seconds
;; VERIFY took 20.73 seconds
14210> VERIFY FORCING-LEVEL10.PROOFP-AUX-OF-LOGIC.PROVABLE-WITNESS
;; Reading from Proofs/level10/thm-forcing-level10.proofp-aux-of-logic.provable-witness.proof
;; Reading the file took 0.91 seconds
;; Checking the proof took 27.35 seconds
;; VERIFY took 28.28 seconds
14211> DEFINE LEVEL10.STATIC-CHECKSP
;; Reading from Proofs/level10/admit-level10.static-checksp.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.13 seconds
14212> VERIFY LEVEL10.STATIC-CHECKSP
;; Reading from Proofs/level10/thm-level10.static-checksp.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.85 seconds
;; VERIFY took 4.20 seconds
14213> DEFINE LEVEL10.PROOFP
;; Reading from Proofs/level10/admit-level10.proofp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.03 seconds
14214> VERIFY LEVEL10.PROOFP
;; Reading from Proofs/level10/thm-level10.proofp.proof
;; Reading the file took 0.23 seconds
;; Checking the proof took 3.52 seconds
;; VERIFY took 3.77 seconds
14215> VERIFY BOOLEANP-OF-LEVEL10.PROOFP
;; Reading from Proofs/level10/thm-booleanp-of-level10.proofp.proof
;; Reading the file took 0.99 seconds
;; Checking the proof took 94.88 seconds
;; VERIFY took 95.88 seconds
14216> VERIFY LOGIC.PROVABLEP-WHEN-LEVEL10.PROOFP
;; Reading from Proofs/level10/thm-logic.provablep-when-level10.proofp.proof
;; Reading the file took 2.06 seconds
;; Checking the proof took 176.16 seconds
;; VERIFY took 178.23 seconds
14217> VERIFY INSTALL-NEW-PROOFP-LEVEL10.PROOFP
;; Reading from Proofs/level10/thm-install-new-proofp-level10.proofp.proof
;; Reading the file took 1.20 seconds
;; Checking the proof took 19.56 seconds
;; VERIFY took 20.77 seconds
14218 > SWITCH LEVEL10.PROOFP
;; SWITCH took 0.00 seconds
14219 > FINISH level10
;; Wrote the memory image into level10.lhug-clisp (26,074,112 bytes)
Bytes permanently allocated: 157,304
Bytes currently in use: 25,909,640
Bytes available until next GC: 6,474,450
Bye.
real 1706m14.915s
user 1698m9.988s
sys 7m33.140s