[optimized] (lambda (k737) (let ((k738 (##core#lambda (r739) (let ((k741 (##core#lambda (r742) (let ((k744 (##core#lambda (r745) (let ((k747 (##core#lambda (r748) (let ((k750 (##core#lambda (r751) (let ((t753 (set! flush-output-port #f flush-output))) (let ((t754 (set! current-jiffy #f current-milliseconds))) (let ((t755 (set! jiffies-per-second #f (lambda (k757) (k757 1000))))) (let ((t758 (set! current-second #f current-seconds))) (let ((t759 (set! inexact #f exact->inexact))) (let ((t760 (set! exact #f inexact->exact))) (let ((t761 (set! square #f (lambda (k763 x61) (k763 (##core#inline_allocate ("C_a_i_times" 4) x61 x61)))))) (let ((t767 (set! exact-integer? #f integer?))) (let ((t768 (set! this-scheme-implementation-name #f (lambda (k770) (let ((k775 (##core#lambda (r776) (string-append k770 "chicken-" r776)))) (chicken-version k775)))))) (let ((t778 (set! main #f (lambda (k780) (let ((k781 (##core#lambda (r782) (let ((count66 r782)) (let ((k784 (##core#lambda (r785) (let ((input67 r785)) (let ((k787 (##core#lambda (r788) (let ((output68 r788)) (let ((k790 (##core#lambda (r791) (let ((s269 r791)) (let ((k793 (##core#lambda (r794) (let ((k800 (##core#lambda (r801) (let ((a803 (lambda (k805) (let ((k806 (##core#lambda (r807) (let ((k813 (##core#lambda (r814) (test-boyer k805 alist term r814)))) (hide k813 count66 input67))))) (setup-boyer k806))))) (let ((a816 (lambda (k818 rewrites73) (let ((r823 (##core#inline "C_i_numberp" rewrites73))) (k818 (##core#cond r823 (##core#inline "C_i_nequalp" rewrites73 output68) #f)))))) (run-r7rs-benchmark k780 r801 count66 a803 a816)))))) (string-append k800 "sboyer" ":" r794 ":" s269))))) (number->string k793 input67)))))) (number->string k790 count66)))))) (read k787)))))) (read k784)))))) (read k781)))))) (let ((t828 (set! alist #f '((x f (plus (plus a b) (plus c (zero)))) (y f (times (times a b) (plus c d))) (z f (reverse (append (append a b) (nil)))) (u equal (plus a b) (difference x y)) (w lessp (remainder a b) (member a (length b))))))) (let ((t829 (set! term #f '(implies (and (implies x y) (and (implies y z) (and (implies z u) (implies u w)))) (implies x w))))) (let ((setup79 (##core#undefined))) (let ((add-lemma-lst80 (##core#undefined))) (let ((add-lemma81 (##core#undefined))) (let ((translate-term82 (##core#undefined))) (let ((translate-args83 (##core#undefined))) (let ((untranslate-term84 (##core#undefined))) (let ((put85 (##core#undefined))) (let ((get86 (##core#undefined))) (let ((symbol->symbol-record87 (##core#undefined))) (let ((*symbol-records-alist*88 (##core#undefined))) (let ((get-lemmas91 (##core#undefined))) (let ((test94 (##core#undefined))) (let ((translate-alist95 (##core#undefined))) (let ((apply-subst96 (##core#undefined))) (let ((apply-subst-lst97 (##core#undefined))) (let ((tautp98 (##core#undefined))) (let ((tautologyp99 (##core#undefined))) (let ((if-constructor100 (##core#undefined))) (let ((rewrite-count101 (##core#undefined))) (let ((scons102 (##core#undefined))) (let ((rewrite103 (##core#undefined))) (let ((rewrite-args104 (##core#undefined))) (let ((rewrite-with-lemmas105 (##core#undefined))) (let ((unify-subst106 (##core#undefined))) (let ((one-way-unify107 (##core#undefined))) (let ((one-way-unify1108 (##core#undefined))) (let ((one-way-unify1-lst109 (##core#undefined))) (let ((falsep110 (##core#undefined))) (let ((truep111 (##core#undefined))) (let ((false-term112 (##core#undefined))) (let ((true-term113 (##core#undefined))) (let ((trans-of-implies1115 (##core#undefined))) (let ((term-equal?116 (##core#undefined))) (let ((term-args-equal?117 (##core#undefined))) (let ((term-member?118 (##core#undefined))) (let ((t830 (set! setup79 #f (lambda (k832) (add-lemma-lst80 k832 '((equal (compile form) (reverse (codegen (optimize form) (nil)))) (equal (eqp x y) (equal (fix x) (fix y))) (equal (greaterp x y) (lessp y x)) (equal (lesseqp x y) (not (lessp y x))) (equal (greatereqp x y) (not (lessp x y))) (equal (boolean x) (or (equal x (t)) (equal x (f)))) (equal (iff x y) (and (implies x y) (implies y x))) (equal (even1 x) (if (zerop x) (t) (odd (_1- x)))) (equal (countps- l pred) (countps-loop l pred (zero))) (equal (fact- i) (fact-loop i 1)) (equal (reverse- x) (reverse-loop x (nil))) (equal (divides x y) (zerop (remainder y x))) (equal (assume-true var alist) (cons (cons var (t)) alist)) (equal (assume-false var alist) (cons (cons var (f)) alist)) (equal (tautology-checker x) (tautologyp (normalize x) (nil))) (equal (falsify x) (falsify1 (normalize x) (nil))) (equal (prime x) (and (not (zerop x)) (not (equal x (add1 (zero)))) (prime1 x (_1- x)))) (equal (and p q) (if p (if q (t) (f)) (f))) (equal (or p q) (if p (t) (if q (t) (f)))) (equal (not p) (if p (f) (t))) (equal (implies p q) (if p (if q (t) (f)) (t))) (equal (fix x) (if (numberp x) x (zero))) (equal (if (if a b c) d e) (if a (if b d e) (if c d e))) (equal (zerop x) (or (equal x (zero)) (not (numberp x)))) (equal (plus (plus x y) z) (plus x (plus y z))) (equal (equal (plus a b) (zero)) (and (zerop a) (zerop b))) (equal (difference x x) (zero)) (equal (equal (plus a b) (plus a c)) (equal (fix b) (fix c))) (equal (equal (zero) (difference x y)) (not (lessp y x))) (equal (equal x (difference x y)) (and (numberp x) (or (equal x (zero)) (zerop y)))) (equal (meaning (plus-tree (append x y)) a) (plus (meaning (plus-tree x) a) (meaning (plus-tree y) a))) (equal (meaning (plus-tree (plus-fringe x)) a) (fix (meaning x a))) (equal (append (append x y) z) (append x (append y z))) (equal (reverse (append a b)) (append (reverse b) (reverse a))) (equal (times x (plus y z)) (plus (times x y) (times x z))) (equal (times (times x y) z) (times x (times y z))) (equal (equal (times x y) (zero)) (or (zerop x) (zerop y))) (equal (exec (append x y) pds envrn) (exec y (exec x pds envrn) envrn)) (equal (mc-flatten x y) (append (flatten x) y)) (equal (member x (append a b)) (or (member x a) (member x b))) (equal (member x (reverse y)) (member x y)) (equal (length (reverse x)) (length x)) (equal (member a (intersect b c)) (and (member a b) (member a c))) (equal (nth (zero) i) (zero)) (equal (exp i (plus j k)) (times (exp i j) (exp i k))) (equal (exp i (times j k)) (exp (exp i j) k)) (equal (reverse-loop x y) (append (reverse x) y)) (equal (reverse-loop x (nil)) (reverse x)) (equal (count-list z (sort-lp x y)) (plus (count-list z x) (count-list z y))) (equal (equal (append a b) (append a c)) (equal b c)) (equal (plus (remainder x y) (times y (quotient x y))) (fix x)) (equal (power-eval (big-plus1 l i base) base) (plus (power-eval l base) i)) (equal (power-eval (big-plus x y i base) base) (plus i (plus (power-eval x base) (power-eval y base)))) (equal (remainder y 1) (zero)) (equal (lessp (remainder x y) y) (not (zerop y))) (equal (remainder x x) (zero)) (equal (lessp (quotient i j) i) (and (not (zerop i)) (or (zerop j) (not (equal j 1))))) (equal (lessp (remainder x y) x) (and (not (zerop y)) (not (zerop x)) (not (lessp x y)))) (equal (power-eval (power-rep i base) base) (fix i)) (equal (power-eval (big-plus (power-rep i base) (power-rep j base) (zero) base) base) (plus i j)) (equal (gcd x y) (gcd y x)) (equal (nth (append a b) i) (append (nth a i) (nth b (difference i (length a))))) (equal (difference (plus x y) x) (fix y)) (equal (difference (plus y x) x) (fix y)) (equal (difference (plus x y) (plus x z)) (difference y z)) (equal (times x (difference c w)) (difference (times c x) (times w x))) (equal (remainder (times x z) z) (zero)) (equal (difference (plus b (plus a c)) a) (plus b c)) (equal (difference (add1 (plus y z)) z) (add1 y)) (equal (lessp (plus x y) (plus x z)) (lessp y z)) (equal (lessp (times x z) (times y z)) (and (not (zerop z)) (lessp x y))) (equal (lessp y (plus x y)) (not (zerop x))) (equal (gcd (times x z) (times y z)) (times z (gcd x y))) (equal (value (normalize x) a) (value x a)) (equal (equal (flatten x) (cons y (nil))) (and (nlistp x) (equal x y))) (equal (listp (gopher x)) (listp x)) (equal (samefringe x y) (equal (flatten x) (flatten y))) (equal (equal (greatest-factor x y) (zero)) (and (or (zerop y) (equal y 1)) (equal x (zero)))) (equal (equal (greatest-factor x y) 1) (equal x 1)) (equal (numberp (greatest-factor x y)) (not (and (or (zerop y) (equal y 1)) (not (numberp x))))) (equal (times-list (append x y)) (times (times-list x) (times-list y))) (equal (prime-list (append x y)) (and (prime-list x) (prime-list y))) (equal (equal z (times w z)) (and (numberp z) (or (equal z (zero)) (equal w 1)))) (equal (greatereqp x y) (not (lessp x y))) (equal (equal x (times x y)) (or (equal x (zero)) (and (numberp x) (equal y 1)))) (equal (remainder (times y x) y) (zero)) (equal (equal (times a b) 1) (and (not (equal a (zero))) (not (equal b (zero))) (numberp a) (numberp b) (equal (_1- a) (zero)) (equal (_1- b) (zero)))) (equal (lessp (length (delete x l)) (length l)) (member x l)) (equal (sort2 (delete x l)) (delete x (sort2 l))) (equal (dsort x) (sort2 x)) (equal (length (cons x1 (cons x2 (cons x3 (cons x4 (cons x5 (cons x6 x7))))))) (plus 6 (length x7))) (equal (difference (add1 (add1 x)) 2) (fix x)) (equal (quotient (plus x (plus x y)) 2) (plus x (quotient y 2))) (equal (sigma (zero) i) (quotient (times i (add1 i)) 2)) (equal (plus x (add1 y)) (if (numberp y) (add1 (plus x y)) (add1 x))) (equal (equal (difference x y) (difference z y)) (if (lessp x y) (not (lessp y z)) (if (lessp z y) (not (lessp y x)) (equal (fix x) (fix z))))) (equal (meaning (plus-tree (delete x y)) a) (if (member x y) (difference (meaning (plus-tree y) a) (meaning x a)) (meaning (plus-tree y) a))) (equal (times x (add1 y)) (if (numberp y) (plus x (times x y)) (fix x))) (equal (nth (nil) i) (if (zerop i) (nil) (zero))) (equal (last (append a b)) (if (listp b) (last b) (if (listp a) (cons (car (last a)) b) b))) (equal (equal (lessp x y) z) (if (lessp x y) (equal (t) z) (equal (f) z))) (equal (assignment x (append a b)) (if (assignedp x a) (assignment x a) (assignment x b))) (equal (car (gopher x)) (if (listp x) (car (flatten x)) (zero))) (equal (flatten (cdr (gopher x))) (if (listp x) (cdr (flatten x)) (cons (zero) (nil)))) (equal (quotient (times y x) y) (if (zerop y) (zero) (fix x))) (equal (get j (set i val mem)) (if (eqp j i) val (get j mem))))))))) (let ((t836 (set! add-lemma-lst80 #f (lambda (k838 lst119) (if (##core#inline "C_i_nullp" lst119) (k838 #t) (let ((k845 (##core#lambda (r846) (let ((r853 (##core#inline "C_i_cdr" lst119))) (add-lemma-lst80 k838 r853))))) (let ((r857 (##core#inline "C_i_car" lst119))) (add-lemma81 k845 r857)))))))) (let ((t859 (set! add-lemma81 #f (lambda (k861 term125) (let ((k865 (##core#lambda (r866) (if r866 (let ((r897 (##core#inline "C_i_cadr" term125))) (let ((r873 (##core#inline "C_i_car" r897))) (let ((a871 r873)) (let ((k880 (##core#lambda (r881) (let ((a879 r881)) (let ((k884 (##core#lambda (r885) (let ((r877 (##core#inline_allocate ("C_a_i_cons" 3) a879 r885))) (put85 k861 a871 r877))))) (let ((r893 (##core#inline "C_i_cadr" term125))) (let ((r889 (##core#inline "C_i_car" r893))) (get86 k884 r889)))))))) (translate-term82 k880 term125))))) (error k861 #f "ADD-LEMMA did not like term: " term125))))) (if (##core#inline "C_i_pairp" term125) (let ((r920 (##core#inline "C_i_car" term125))) (let ((r909 (##core#inline "C_eqp" r920 'equal))) (if r909 (let ((r916 (##core#inline "C_i_cadr" term125))) (k865 (##core#inline "C_i_pairp" r916))) (k865 #f)))) (k865 #f))))))) (let ((t922 (set! translate-term82 #f (lambda (k924 term132) (if (##core#inline "C_i_pairp" term132) (let ((k935 (##core#lambda (r936) (let ((a934 r936)) (let ((k939 (##core#lambda (r940) (k924 (##core#inline_allocate ("C_a_i_cons" 3) a934 r940))))) (let ((r944 (##core#inline "C_i_cdr" term132))) (translate-args83 k939 r944))))))) (let ((r948 (##core#inline "C_i_car" term132))) (symbol->symbol-record87 k935 r948))) (k924 term132)))))) (let ((t954 (set! translate-args83 #f (lambda (k956 lst137) (if (##core#inline "C_i_nullp" lst137) (k956 '()) (let ((k967 (##core#lambda (r968) (let ((a966 r968)) (let ((k971 (##core#lambda (r972) (k956 (##core#inline_allocate ("C_a_i_cons" 3) a966 r972))))) (let ((r976 (##core#inline "C_i_cdr" lst137))) (translate-args83 k971 r976))))))) (let ((r980 (##core#inline "C_i_car" lst137))) (translate-term82 k967 r980)))))))) (let ((t982 (set! untranslate-term84 #f (lambda (k984 term142) (if (##core#inline "C_i_pairp" term142) (let ((r1047 (##core#inline "C_i_car" term142))) (let ((r996 (##core#inline "C_i_vector_ref" r1047 0))) (let ((a994 r996)) (let ((r1000 (##core#inline_allocate ("C_a_i_cons" 3) (##core#undefined) '()))) (let ((g154162 r1000)) (let ((g153163 g154162)) (let ((g155164 untranslate-term84)) (let ((r1003 (##core#inline "C_i_cdr" term142))) (let ((r1006 (##core#inline "C_i_check_list_2" r1003 'map))) (let ((k1008 (##core#lambda (r1009) (k984 (##core#inline_allocate ("C_a_i_cons" 3) a994 r1009))))) (let ((map-loop149166 (##core#undefined))) (let ((t1011 (set! map-loop149166 #f (lambda (k1013 g161167) (if (##core#inline "C_i_pairp" g161167) (let ((k1035 (##core#lambda (r1036) (let ((r1021 (##core#inline_allocate ("C_a_i_cons" 3) r1036 '()))) (let ((r1024 (##core#inline "C_i_setslot" g154162 1 r1021))) (let ((t1026 (set! g154162 #f r1021))) (let ((r1032 (##core#inline "C_slot" g161167 1))) (map-loop149166 k1013 r1032)))))))) (let ((r1040 (##core#inline "C_slot" g161167 0))) (g155164 k1035 r1040))) (k1013 (##core#inline "C_slot" g153163 1))))))) (map-loop149166 k1008 r1003))))))))))))) (k984 term142)))))) (let ((t1053 (set! put85 #f (lambda (k1055 sym173 value175) (let ((k1060 (##core#lambda (r1061) (let ((k1105 k1055)) (let ((lemmas184 value175)) (k1105 (##core#inline "C_i_vector_set" r1061 1 lemmas184))))))) (symbol->symbol-record87 k1060 sym173)))))) (let ((t1063 (set! get86 #f (lambda (k1065 sym176) (let ((k1070 (##core#lambda (r1071) (get-lemmas91 k1065 r1071)))) (symbol->symbol-record87 k1070 sym176)))))) (let ((t1073 (set! symbol->symbol-record87 #f (lambda (k1075 sym178) (let ((r1077 (##core#inline "C_i_assq" sym178 *symbol-records-alist*88))) (if r1077 (k1075 (##core#inline "C_i_cdr" r1077)) (let ((sym182 sym178)) (let ((r1086 (##core#inline_allocate ("C_a_i_vector2" 3) sym182 '()))) (let ((r1094 (##core#inline_allocate ("C_a_i_cons" 3) sym178 r1086))) (let ((r1090 (##core#inline_allocate ("C_a_i_cons" 3) r1094 *symbol-records-alist*88))) (let ((t1088 (set! *symbol-records-alist*88 #f r1090))) (k1075 r1086)))))))))))) (let ((t1096 (set! *symbol-records-alist*88 #t '()))) (let ((t1109 (set! get-lemmas91 #f (lambda (k1111 symbol-record185) (k1111 (##core#inline "C_i_vector_ref" symbol-record185 1)))))) (let ((t1127 (set! test94 #f (lambda (k1129 alist189 term190 n191) (let ((k1130 (##core#lambda (r1131) (tautp98 k1129 r1131)))) (let ((k1137 (##core#lambda (r1138) (let ((a1136 r1138)) (let ((k1141 (##core#lambda (r1142) (apply-subst96 k1130 a1136 r1142)))) (let ((k1145 (##core#lambda (r1146) (translate-term82 k1141 r1146)))) (let ((doloop193194 (##core#undefined))) (let ((t1148 (set! doloop193194 #f (lambda (k1150 term195 n196) (if (##core#inline "C_i_zerop" n196) (k1150 term195) (let ((r1162 (##core#inline_allocate ("C_a_i_list3" 9) 'or term195 '(f)))) (let ((r1166 (##core#inline_allocate ("C_a_i_minus" 4) n196 1))) (doloop193194 k1150 r1162 r1166)))))))) (doloop193194 k1145 term190 n191))))))))) (translate-alist95 k1137 alist189))))))) (let ((t1168 (set! translate-alist95 #f (lambda (k1170 alist198) (if (##core#inline "C_i_nullp" alist198) (k1170 '()) (let ((r1194 (##core#inline "C_i_caar" alist198))) (let ((a1192 r1194)) (let ((k1197 (##core#lambda (r1198) (let ((r1182 (##core#inline_allocate ("C_a_i_cons" 3) a1192 r1198))) (let ((a1180 r1182)) (let ((k1185 (##core#lambda (r1186) (k1170 (##core#inline_allocate ("C_a_i_cons" 3) a1180 r1186))))) (let ((r1190 (##core#inline "C_i_cdr" alist198))) (translate-alist95 k1185 r1190)))))))) (let ((r1202 (##core#inline "C_i_cdar" alist198))) (translate-term82 k1197 r1202)))))))))) (let ((t1204 (set! apply-subst96 #f (lambda (k1206 alist203 term204) (if (##core#inline "C_i_pairp" term204) (let ((r1227 (##core#inline "C_i_car" term204))) (let ((a1225 r1227)) (let ((k1230 (##core#lambda (r1231) (k1206 (##core#inline_allocate ("C_a_i_cons" 3) a1225 r1231))))) (let ((r1235 (##core#inline "C_i_cdr" term204))) (apply-subst-lst97 k1230 alist203 r1235))))) (let ((r1214 (##core#inline "C_i_assq" term204 alist203))) (k1206 (##core#cond r1214 (##core#inline "C_i_cdr" r1214) term204)))))))) (let ((t1241 (set! apply-subst-lst97 #f (lambda (k1243 alist210 lst211) (if (##core#inline "C_i_nullp" lst211) (k1243 '()) (let ((k1254 (##core#lambda (r1255) (let ((a1253 r1255)) (let ((k1258 (##core#lambda (r1259) (k1243 (##core#inline_allocate ("C_a_i_cons" 3) a1253 r1259))))) (let ((r1263 (##core#inline "C_i_cdr" lst211))) (apply-subst-lst97 k1258 alist210 r1263))))))) (let ((r1267 (##core#inline "C_i_car" lst211))) (apply-subst96 k1254 alist210 r1267)))))))) (let ((t1269 (set! tautp98 #f (lambda (k1271 x216) (let ((k1276 (##core#lambda (r1277) (tautologyp99 k1271 r1277 '() '())))) (rewrite103 k1276 x216)))))) (let ((t1279 (set! tautologyp99 #f (lambda (k1281 x217 true-lst218 false-lst219) (let ((k1285 (##core#lambda (r1286) (if r1286 (k1281 #t) (let ((k1291 (##core#lambda (r1292) (if r1292 (k1281 #f) (if (##core#inline "C_i_pairp" x217) (let ((r1375 (##core#inline "C_i_car" x217))) (let ((r1304 (##core#inline "C_eqp" r1375 if-constructor100))) (if r1304 (let ((k1309 (##core#lambda (r1310) (if r1310 (let ((r1317 (##core#inline "C_i_caddr" x217))) (tautologyp99 k1281 r1317 true-lst218 false-lst219)) (let ((k1322 (##core#lambda (r1323) (if r1323 (let ((r1330 (##core#inline "C_i_cadddr" x217))) (tautologyp99 k1281 r1330 true-lst218 false-lst219)) (let ((k1335 (##core#lambda (r1336) (if r1336 (let ((r1343 (##core#inline "C_i_cadddr" x217))) (let ((r1351 (##core#inline "C_i_cadr" x217))) (let ((r1347 (##core#inline_allocate ("C_a_i_cons" 3) r1351 false-lst219))) (tautologyp99 k1281 r1343 true-lst218 r1347)))) (k1281 #f))))) (let ((r1355 (##core#inline "C_i_caddr" x217))) (let ((r1363 (##core#inline "C_i_cadr" x217))) (let ((r1359 (##core#inline_allocate ("C_a_i_cons" 3) r1363 true-lst218))) (tautologyp99 k1335 r1355 r1359 false-lst219))))))))) (let ((r1367 (##core#inline "C_i_cadr" x217))) (falsep110 k1322 r1367 false-lst219))))))) (let ((r1371 (##core#inline "C_i_cadr" x217))) (truep111 k1309 r1371 true-lst218))) (k1281 #f)))) (k1281 #f)))))) (falsep110 k1291 x217 false-lst219)))))) (truep111 k1285 x217 true-lst218)))))) (let ((t1381 (set! if-constructor100 #f '*))) (let ((t1382 (set! rewrite-count101 #t 0))) (let ((t1383 (set! scons102 #f (lambda (k1385 x229 y230 original231) (let ((k1389 (##core#lambda (r1390) (k1385 (##core#cond r1390 original231 (##core#inline_allocate ("C_a_i_cons" 3) x229 y230)))))) (let ((r1407 (##core#inline "C_i_car" original231))) (let ((r1396 (##core#inline "C_eqp" x229 r1407))) (if r1396 (let ((r1403 (##core#inline "C_i_cdr" original231))) (k1389 (##core#inline "C_eqp" y230 r1403))) (k1389 #f))))))))) (let ((t1409 (set! rewrite103 #f (lambda (k1411 term233) (let ((r1414 (##core#inline_allocate ("C_a_i_plus" 4) rewrite-count101 1))) (let ((t1412 (set! rewrite-count101 #f r1414))) (if (##core#inline "C_i_pairp" term233) (let ((k1426 (##core#lambda (r1427) (let ((a1425 r1427)) (let ((k1430 (##core#lambda (r1431) (rewrite-with-lemmas105 k1411 a1425 r1431)))) (let ((r1435 (##core#inline "C_i_car" term233))) (get-lemmas91 k1430 r1435))))))) (let ((r1439 (##core#inline "C_i_car" term233))) (let ((a1437 r1439)) (let ((k1442 (##core#lambda (r1443) (scons102 k1426 a1437 r1443 term233)))) (let ((r1447 (##core#inline "C_i_cdr" term233))) (rewrite-args104 k1442 r1447)))))) (k1411 term233)))))))) (let ((t1453 (set! rewrite-args104 #f (lambda (k1455 lst239) (if (##core#inline "C_i_nullp" lst239) (k1455 '()) (let ((k1466 (##core#lambda (r1467) (let ((a1465 r1467)) (let ((k1470 (##core#lambda (r1471) (scons102 k1455 a1465 r1471 lst239)))) (let ((r1475 (##core#inline "C_i_cdr" lst239))) (rewrite-args104 k1470 r1475))))))) (let ((r1479 (##core#inline "C_i_car" lst239))) (rewrite103 k1466 r1479)))))))) (let ((t1481 (set! rewrite-with-lemmas105 #f (lambda (k1483 term244 lst245) (if (##core#inline "C_i_nullp" lst245) (k1483 term244) (let ((k1493 (##core#lambda (r1494) (if r1494 (let ((k1500 (##core#lambda (r1501) (rewrite103 k1483 r1501)))) (let ((r1509 (##core#inline "C_i_car" lst245))) (let ((r1505 (##core#inline "C_i_caddr" r1509))) (apply-subst96 k1500 unify-subst106 r1505)))) (let ((r1516 (##core#inline "C_i_cdr" lst245))) (rewrite-with-lemmas105 k1483 term244 r1516)))))) (let ((r1524 (##core#inline "C_i_car" lst245))) (let ((r1520 (##core#inline "C_i_cadr" r1524))) (one-way-unify107 k1493 term244 r1520))))))))) (let ((t1526 (set! unify-subst106 #f '*))) (let ((t1527 (set! one-way-unify107 #f (lambda (k1529 term1250 term2251) (let ((t1530 (set! unify-subst106 #t '()))) (one-way-unify1108 k1529 term1250 term2251)))))) (let ((t1534 (set! one-way-unify1108 #f (lambda (k1536 term1253 term2254) (if (##core#inline "C_i_pairp" term2254) (if (##core#inline "C_i_pairp" term1253) (let ((r1598 (##core#inline "C_i_car" term1253))) (let ((r1602 (##core#inline "C_i_car" term2254))) (let ((r1583 (##core#inline "C_eqp" r1598 r1602))) (if r1583 (let ((r1590 (##core#inline "C_i_cdr" term1253))) (let ((r1594 (##core#inline "C_i_cdr" term2254))) (one-way-unify1-lst109 k1536 r1590 r1594))) (k1536 #f))))) (k1536 #f)) (let ((r1544 (##core#inline "C_i_assq" term2254 unify-subst106))) (if r1544 (let ((r1554 (##core#inline "C_i_cdr" r1544))) (term-equal?116 k1536 term1253 r1554)) (if (##core#inline "C_i_numberp" term2254) (k1536 (##core#inline "C_i_equalp" term1253 term2254)) (let ((r1571 (##core#inline_allocate ("C_a_i_cons" 3) term2254 term1253))) (let ((r1567 (##core#inline_allocate ("C_a_i_cons" 3) r1571 unify-subst106))) (let ((t1565 (set! unify-subst106 #f r1567))) (k1536 #t)))))))))))) (let ((t1612 (set! one-way-unify1-lst109 #f (lambda (k1614 lst1265 lst2266) (if (##core#inline "C_i_nullp" lst1265) (k1614 (##core#inline "C_i_nullp" lst2266)) (if (##core#inline "C_i_nullp" lst2266) (k1614 #f) (let ((k1633 (##core#lambda (r1634) (if r1634 (let ((r1641 (##core#inline "C_i_cdr" lst1265))) (let ((r1645 (##core#inline "C_i_cdr" lst2266))) (one-way-unify1-lst109 k1614 r1641 r1645))) (k1614 #f))))) (let ((r1649 (##core#inline "C_i_car" lst1265))) (let ((r1653 (##core#inline "C_i_car" lst2266))) (one-way-unify1108 k1633 r1649 r1653)))))))))) (let ((t1655 (set! falsep110 #f (lambda (k1657 x271 lst272) (let ((k1658 (##core#lambda (r1659) (if r1659 (k1657 r1659) (term-member?118 k1657 x271 lst272))))) (term-equal?116 k1658 x271 false-term112)))))) (let ((t1667 (set! truep111 #f (lambda (k1669 x276 lst277) (let ((k1670 (##core#lambda (r1671) (if r1671 (k1669 r1671) (term-member?118 k1669 x276 lst277))))) (term-equal?116 k1670 x276 true-term113)))))) (let ((t1679 (set! false-term112 #f '*))) (let ((t1680 (set! true-term113 #f '*))) (let ((t1699 (set! trans-of-implies1115 #f (lambda (k1701 n282) (let ((r1706 (##core#inline "C_eqp" n282 1))) (if r1706 (k1701 (##core#inline_allocate ("C_a_i_list3" 9) 'implies 0 1)) (let ((r1728 (##core#inline_allocate ("C_a_i_minus" 4) n282 1))) (let ((r1716 (##core#inline_allocate ("C_a_i_list3" 9) 'implies r1728 n282))) (let ((a1714 r1716)) (let ((k1719 (##core#lambda (r1720) (k1701 (##core#inline_allocate ("C_a_i_list3" 9) 'and a1714 r1720))))) (let ((r1724 (##core#inline_allocate ("C_a_i_minus" 4) n282 1))) (trans-of-implies1115 k1719 r1724)))))))))))) (let ((t1730 (set! term-equal?116 #f (lambda (k1732 x287 y288) (if (##core#inline "C_i_pairp" x287) (if (##core#inline "C_i_pairp" y288) (let ((r1764 (##core#inline "C_i_car" x287))) (let ((r1768 (##core#inline "C_i_car" y288))) (let ((r1749 (##core#inline "C_eqp" r1764 r1768))) (if r1749 (let ((r1756 (##core#inline "C_i_cdr" x287))) (let ((r1760 (##core#inline "C_i_cdr" y288))) (term-args-equal?117 k1732 r1756 r1760))) (k1732 #f))))) (k1732 #f)) (k1732 (##core#inline "C_i_equalp" x287 y288))))))) (let ((t1773 (set! term-args-equal?117 #f (lambda (k1775 lst1295 lst2296) (if (##core#inline "C_i_nullp" lst1295) (k1775 (##core#inline "C_i_nullp" lst2296)) (if (##core#inline "C_i_nullp" lst2296) (k1775 #f) (let ((k1794 (##core#lambda (r1795) (if r1795 (let ((r1802 (##core#inline "C_i_cdr" lst1295))) (let ((r1806 (##core#inline "C_i_cdr" lst2296))) (term-args-equal?117 k1775 r1802 r1806))) (k1775 #f))))) (let ((r1810 (##core#inline "C_i_car" lst1295))) (let ((r1814 (##core#inline "C_i_car" lst2296))) (term-equal?116 k1794 r1810 r1814)))))))))) (let ((t1816 (set! term-member?118 #f (lambda (k1818 x301 lst302) (if (##core#inline "C_i_nullp" lst302) (k1818 #f) (let ((k1828 (##core#lambda (r1829) (if r1829 (k1818 #t) (let ((r1836 (##core#inline "C_i_cdr" lst302))) (term-member?118 k1818 x301 r1836)))))) (let ((r1840 (##core#inline "C_i_car" lst302))) (term-equal?116 k1828 x301 r1840)))))))) (let ((t1842 (set! setup-boyer #f (lambda (k1844) (let ((t1845 (set! *symbol-records-alist*88 #t '()))) (let ((k1847 (##core#lambda (r1848) (let ((t1846 (set! if-constructor100 #f r1848))) (let ((k1851 (##core#lambda (r1852) (let ((t1850 (set! false-term112 #f r1852))) (let ((k1855 (##core#lambda (r1856) (let ((t1854 (set! true-term113 #f r1856))) (setup79 k1844))))) (translate-term82 k1855 '(t))))))) (translate-term82 k1851 '(f))))))) (symbol->symbol-record87 k1847 'if))))))) (let ((t1861 (set! test-boyer #f (lambda (k1863 alist311 term312 n313) (let ((t1864 (set! rewrite-count101 #t 0))) (let ((k1865 (##core#lambda (r1866) (k1863 (##core#cond r1866 rewrite-count101 #f))))) (test94 k1865 alist311 term312 n313))))))) (let ((t1871 (set! hide #f (lambda (k1873 r358 x359) (let ((a1877 (lambda (k1879) (let ((a1894 (lambda (k1896 x360) (k1896 x360)))) (let ((r1885 (##core#inline_allocate ("C_a_i_vector2" 3) values a1894))) (let ((r1892 (##core#inline "C_i_lessp" r358 100))) (let ((r1889 (##core#cond r1892 0 1))) ((##core#proc "C_values" #t) k1879 r1885 r1889)))))))) (let ((a1897 (lambda (k1899 v361 i362) (let ((r1901 (##core#inline "C_i_vector_ref" v361 i362))) (r1901 k1899 x359))))) ((##core#proc "C_call_with_values" #t) k1873 a1877 a1897))))))) (let ((t1906 (set! run-r7rs-benchmark #f (lambda (k1908 name366 count367 thunk368 ok?369) (let ((k1923 (##core#lambda (r1924) (let ((k1926 (##core#lambda (r1927) (let ((k1929 (##core#lambda (r1930) (let ((k1932 (##core#lambda (r1933) (let ((k1935 (##core#lambda (r1936) (let ((j/s372 r1936)) (let ((k1938 (##core#lambda (r1939) (let ((t0373 r1939)) (let ((k1941 (##core#lambda (r1942) (let ((j0374 r1942)) (let ((loop375 (##core#undefined))) (let ((t1947 (set! loop375 #f (lambda (k1949 i376 result377) (if (##core#inline "C_i_lessp" i376 count367) (let ((r1961 (##core#inline_allocate ("C_a_i_plus" 4) i376 1))) (let ((a1959 r1961)) (let ((k1964 (##core#lambda (r1965) (loop375 k1949 a1959 r1965)))) (thunk368 k1964)))) (let ((k1970 (##core#lambda (r1971) (if r1971 (let ((k1973 (##core#lambda (r1974) (let ((j1382 r1974)) (let ((k1976 (##core#lambda (r1977) (let ((t1383 r1977)) (let ((r1980 (##core#inline_allocate ("C_a_i_minus" 4) j1382 j0374))) (let ((k1982 (##core#lambda (r1983) (let ((secs385 r1983)) (let ((k1985 (##core#lambda (r1986) (let ((secs2386 r1986)) (let ((k1988 (##core#lambda (r1989) (let ((k1991 (##core#lambda (r1992) (let ((k1994 (##core#lambda (r1995) (let ((k1997 (##core#lambda (r1998) (let ((k2000 (##core#lambda (r2001) (let ((k2003 (##core#lambda (r2004) (let ((k2006 (##core#lambda (r2007) (let ((k2009 (##core#lambda (r2010) (let ((k2012 (##core#lambda (r2013) (let ((k2015 (##core#lambda (r2016) (let ((k2018 (##core#lambda (r2019) (let ((k2021 (##core#lambda (r2022) (let ((k2024 (##core#lambda (r2025) (let ((k2027 (##core#lambda (r2028) (let ((k2030 (##core#lambda (r2031) (k1949 result377)))) (let ((r2035 ##sys#standard-output)) (flush-output-port k2030 ##sys#standard-output)))))) (newline k2027))))) (display k2024 secs385))))) (display k2021 ","))))) (display k2018 name366))))) (display k2015 ","))))) (let ((k2038 (##core#lambda (r2039) (display k2012 r2039)))) (this-scheme-implementation-name k2038)))))) (display k2009 "+!CSVLINE!+"))))) (newline k2006))))) (display k2003 name366))))) (display k2000 ") for "))))) (write k1997 secs2386))))) (display k1994 " seconds ("))))) (write k1991 secs385))))) (display k1988 "Elapsed time: ")))))) (let ((r2043 (##core#inline_allocate ("C_a_i_minus" 4) t1383 t0373))) (let ((k1911 k1985)) (let ((k1916 (##core#lambda (r1917) (k1911 (##core#inline_allocate ("C_a_i_divide" 4) r1917 1000))))) (let ((r1921 (##core#inline_allocate ("C_a_i_times" 4) 1000 r2043))) (round k1916 r1921)))))))))) (let ((r2047 (##core#inline_allocate ("C_a_i_divide" 4) r1980 j/s372))) (inexact k1982 r2047)))))))) (current-second k1976)))))) (current-jiffy k1973)) (let ((k2049 (##core#lambda (r2050) (let ((k2052 (##core#lambda (r2053) (let ((k2055 (##core#lambda (r2056) (let ((k2058 (##core#lambda (r2059) (k1949 result377)))) (let ((r2063 ##sys#standard-output)) (flush-output-port k2058 ##sys#standard-output)))))) (newline k2055))))) (write k2052 result377))))) (display k2049 "ERROR: returned incorrect result: ")))))) (ok?369 k1970 result377))))))) (loop375 k1908 0 #f))))))) (current-jiffy k1941)))))) (current-second k1938)))))) (jiffies-per-second k1935))))) (let ((r2067 ##sys#standard-output)) (flush-output-port k1932 ##sys#standard-output)))))) (newline k1929))))) (display k1926 name366))))) (display k1923 "Running ")))))) (let ((k2069 (##core#lambda (r2070) (let ((k2072 (##core#lambda (r2073) (k737 (##core#undefined))))) (let ((k2075 (##core#lambda (r2076) (r2076 k2072)))) (##sys#implicit-exit-handler k2075)))))) (main k2069))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (##sys#require k750 'vector-lib))))) (##core#callunit "extras" k747))))) (##core#callunit "chicken_2dsyntax" k744))))) (##core#callunit "eval" k741))))) (##core#callunit "library" k738)))