1680 lines
36 KiB
Racket
1680 lines
36 KiB
Racket
#lang rosette/safe
|
|
(define scwp 3)
|
|
(define crmb 5)
|
|
(define nttr 3)
|
|
(define dddm 2)
|
|
(define chsm (* crmb scwp))
|
|
(define sclr (* dddm nttr))
|
|
(define wtrh (+ sclr chsm))
|
|
(define qbzv 1)
|
|
(define btqt (+ qbzv wtrh))
|
|
(define hzlh 2)
|
|
(define tdlw 3)
|
|
(define wqfz 4)
|
|
(define pbhg 2)
|
|
(define bfvd 7)
|
|
(define drdl (* hzlh btqt))
|
|
(define bbjs 7)
|
|
(define mtjq 2)
|
|
(define svdw 4)
|
|
(define vzgb 12)
|
|
(define nztj (+ wqfz tdlw))
|
|
(define cgvv (* bfvd pbhg))
|
|
(define mrlq (+ bbjs drdl))
|
|
(define mnlp (+ svdw mtjq))
|
|
(define dfgh 7)
|
|
(define flhf 3)
|
|
(define jnll (* nztj vzgb))
|
|
(define qpbz 3)
|
|
(define zswl 3)
|
|
(define chfs (- mrlq cgvv))
|
|
(define cdqv (+ dfgh mnlp))
|
|
(define wfbz 2)
|
|
(define qmcb 17)
|
|
(define qtfp 2)
|
|
(define bjfh 3)
|
|
(define tpwq (/ jnll flhf))
|
|
(define hpvb (* zswl qpbz))
|
|
(define-symbolic humn integer?)
|
|
(define mfmt (* cdqv chfs))
|
|
(define szmm 3)
|
|
(define sbvl 3)
|
|
(define rmvt 3)
|
|
(define bvvl 20)
|
|
(define gvbp 3)
|
|
(define vzgd (+ qmcb wfbz))
|
|
(define thpg 4)
|
|
(define gzwh (* bjfh qtfp))
|
|
(define cnmq 8)
|
|
(define gpzn (+ hpvb tpwq))
|
|
(define tfwb 2)
|
|
(define fbcd (+ mfmt humn))
|
|
(define qnds (* sbvl szmm))
|
|
(define nqpr 3)
|
|
(define rllb 3)
|
|
(define rncj 5)
|
|
(define zttf 3)
|
|
(define lpjr (+ bvvl rmvt))
|
|
(define fzwr 5)
|
|
(define bwnc 2)
|
|
(define fbrf 3)
|
|
(define stlr (* vzgd gvbp))
|
|
(define hmfb 4)
|
|
(define lrdn 3)
|
|
(define mlrz 2)
|
|
(define dqhh (* gzwh thpg))
|
|
(define dncw 5)
|
|
(define mthn 2)
|
|
(define pbzb 2)
|
|
(define ggpn 11)
|
|
(define zhpq (* gpzn cnmq))
|
|
(define rddj (/ fbcd tfwb))
|
|
(define ldzb (* nqpr qnds))
|
|
(define qnhq (* rncj rllb))
|
|
(define zhqg (* lpjr zttf))
|
|
(define mhnm (+ bwnc fzwr))
|
|
(define pnwz (/ stlr fbrf))
|
|
(define nrps (+ lrdn hmfb))
|
|
(define dfzw 2)
|
|
(define smqg 14)
|
|
(define snlb 4)
|
|
(define mtsv 3)
|
|
(define qfjg 1)
|
|
(define ltzm 12)
|
|
(define cmnv 7)
|
|
(define tcqz (+ dqhh mlrz))
|
|
(define hrmz (* mthn dncw))
|
|
(define phrv 3)
|
|
(define wzdj 3)
|
|
(define hbwh (+ ggpn pbzb))
|
|
(define ncsp (- rddj zhpq))
|
|
(define tvrd (+ qnhq ldzb))
|
|
(define dqnv (* mhnm zhqg))
|
|
(define wqqv (* nrps pnwz))
|
|
(define lvrc 4)
|
|
(define vszg (/ smqg dfzw))
|
|
(define rmrj (+ mtsv snlb))
|
|
(define djjs (+ ltzm qfjg))
|
|
(define tqzf 3)
|
|
(define pmds 3)
|
|
(define rtmt 12)
|
|
(define hbhz 18)
|
|
(define zvvd (- tcqz cmnv))
|
|
(define hlzp (+ phrv hrmz))
|
|
(define gwmr (* hbwh wzdj))
|
|
(define wglc 14)
|
|
(define bntz (* tvrd ncsp))
|
|
(define gcvn (+ wqqv dqnv))
|
|
(define hwvf (+ vszg lvrc))
|
|
(define fpsh 2)
|
|
(define rlqm 2)
|
|
(define vnpq (+ djjs rmrj))
|
|
(define ggnd 3)
|
|
(define lhvt (* pmds tqzf))
|
|
(define gztl 11)
|
|
(define pwlh (+ hbhz rtmt))
|
|
(define qmvq (* hlzp zvvd))
|
|
(define lgpg (+ wglc gwmr))
|
|
(define qhlj (+ gcvn bntz))
|
|
(define jcch 2)
|
|
(define cbfh 2)
|
|
(define flrw 3)
|
|
(define cjlm 6)
|
|
(define pszs 4)
|
|
(define cgvr 3)
|
|
(define sbwd 4)
|
|
(define ppcl 3)
|
|
(define jbvq 7)
|
|
(define bdmw (* fpsh hwvf))
|
|
(define zzqd (/ vnpq rlqm))
|
|
(define pnwv (* lhvt ggnd))
|
|
(define bqtp 2)
|
|
(define zspm 5)
|
|
(define lbtn 8)
|
|
(define vsmt (+ pwlh gztl))
|
|
(define vjwz 2)
|
|
(define chlt 4)
|
|
(define znfq 2)
|
|
(define jcjf (+ lgpg qmvq))
|
|
(define fwbm (* jcch qhlj))
|
|
(define rpbg 1)
|
|
(define pwgj (* flrw cbfh))
|
|
(define bcnd 13)
|
|
(define mrmm (* pszs cjlm))
|
|
(define smld 2)
|
|
(define qhwm 3)
|
|
(define rbbh 13)
|
|
(define dgbr (* sbwd cgvr))
|
|
(define bfgp (* jbvq ppcl))
|
|
(define mdld (+ zzqd bdmw))
|
|
(define lccn 5)
|
|
(define bvjd 2)
|
|
(define dhts 8)
|
|
(define fjcg 2)
|
|
(define rzsn 5)
|
|
(define dflc 2)
|
|
(define cvvv (* bqtp pnwv))
|
|
(define csml (* lbtn zspm))
|
|
(define pjsp 5)
|
|
(define mwjg (* vjwz vsmt))
|
|
(define zjvz (* znfq chlt))
|
|
(define wghf (- fwbm jcjf))
|
|
(define snvw 3)
|
|
(define cshj (+ pwgj rpbg))
|
|
(define tqfr (+ mrmm bcnd))
|
|
(define mdjm 3)
|
|
(define lbqn 5)
|
|
(define hrjj 2)
|
|
(define pvcn (* qhwm smld))
|
|
(define smwb (+ dgbr rbbh))
|
|
(define frst 5)
|
|
(define mtdh 8)
|
|
(define szvb (+ mdld bfgp))
|
|
(define nvhn 2)
|
|
(define zpht 10)
|
|
(define rdpb 10)
|
|
(define cmnt (+ bvjd lccn))
|
|
(define ncgd 3)
|
|
(define fmvc (* fjcg dhts))
|
|
(define shpt 2)
|
|
(define pwlt 5)
|
|
(define pmqh (* dflc rzsn))
|
|
(define zdrh (+ csml cvvv))
|
|
(define ljzj 15)
|
|
(define mfts (* mwjg pjsp))
|
|
(define ltmj (/ wghf zjvz))
|
|
(define hvsd 3)
|
|
(define sqsc 5)
|
|
(define jhvm 16)
|
|
(define wbnh (* cshj snvw))
|
|
(define qllm 3)
|
|
(define cbgj (* mdjm tqfr))
|
|
(define cnvb (* hrjj lbqn))
|
|
(define qqtm 3)
|
|
(define czst (- smwb pvcn))
|
|
(define vdzv 5)
|
|
(define vhzf 2)
|
|
(define ltdq 4)
|
|
(define zbqq (* mtdh frst))
|
|
(define lsnd 1)
|
|
(define pzvr 3)
|
|
(define cdwt 6)
|
|
(define rtgr (* nvhn szvb))
|
|
(define jmwl (* rdpb zpht))
|
|
(define qplw (* ncgd cmnt))
|
|
(define svvh (* shpt fmvc))
|
|
(define vnvr (* pmqh pwlt))
|
|
(define rwjc (+ ljzj zdrh))
|
|
(define pzzg (- ltmj mfts))
|
|
(define gzmv 3)
|
|
(define plfd (* sqsc hvsd))
|
|
(define ggbp (+ wbnh jhvm))
|
|
(define wflc (/ cbgj qllm))
|
|
(define rrqr 2)
|
|
(define lwlc (* qqtm cnvb))
|
|
(define hlms 11)
|
|
(define lrsc (* vdzv czst))
|
|
(define wtbs (* ltdq vhzf))
|
|
(define crcm (+ lsnd zbqq))
|
|
(define cchg 2)
|
|
(define zbnt 3)
|
|
(define mjmv (+ cdwt pzvr))
|
|
(define bcmp 2)
|
|
(define fnws (+ jmwl rtgr))
|
|
(define nzdj (+ svvh qplw))
|
|
(define lnqm (+ rwjc vnvr))
|
|
(define flhd 3)
|
|
(define lqrf 2)
|
|
(define ntqb (* gzmv pzzg))
|
|
(define zfbq (* ggbp plfd))
|
|
(define jbsh 2)
|
|
(define czpd 4)
|
|
(define rvvn (* rrqr wflc))
|
|
(define fzgj 4)
|
|
(define mrrt 7)
|
|
(define nvdh 3)
|
|
(define jzdn 2)
|
|
(define jvfw (+ hlms lwlc))
|
|
(define rndt (+ wtbs lrsc))
|
|
(define mggl (* cchg crcm))
|
|
(define ngbz 2)
|
|
(define jcdb (* mjmv zbnt))
|
|
(define qljb 3)
|
|
(define bmsf (/ fnws bcmp))
|
|
(define zwqw (- lnqm nzdj))
|
|
(define rjfh 5)
|
|
(define dnwd (* lqrf flhd))
|
|
(define qlqt (+ zfbq ntqb))
|
|
(define llnl 3)
|
|
(define jbcl 3)
|
|
(define gwhs (* czpd jbsh))
|
|
(define wqpv (* fzgj rvvn))
|
|
(define mwgb (* nvdh mrrt))
|
|
(define ntnh (* jvfw jzdn))
|
|
(define cspp (+ mggl rndt))
|
|
(define wbsb (* jcdb ngbz))
|
|
(define gvgp 3)
|
|
(define pnvs (* bmsf qljb))
|
|
(define tldn (* rjfh zwqw))
|
|
(define bgwj (/ qlqt dnwd))
|
|
(define szwj 3)
|
|
(define vwhb 2)
|
|
(define zsns 2)
|
|
(define glpw 8)
|
|
(define jnzr 5)
|
|
(define fzml 11)
|
|
(define nzzv (* jbcl llnl))
|
|
(define jqcf 3)
|
|
(define jdjq 4)
|
|
(define vrbh (/ wqpv gwhs))
|
|
(define rrgh 2)
|
|
(define ncrt (+ ntnh mwgb))
|
|
(define cbdr (+ wbsb cspp))
|
|
(define cqcg 3)
|
|
(define grcv (* pnvs gvgp))
|
|
(define wggq (+ bgwj tldn))
|
|
(define snbl (* vwhb szwj))
|
|
(define dzwg 4)
|
|
(define wnvf 8)
|
|
(define wrll 2)
|
|
(define bbhp 2)
|
|
(define drlt 5)
|
|
(define tjqj (* glpw zsns))
|
|
(define twcj 3)
|
|
(define vldc 2)
|
|
(define snff 4)
|
|
(define rhtv (* fzml jnzr))
|
|
(define cftm 18)
|
|
(define svhz (* jqcf nzzv))
|
|
(define swmh (+ vrbh jdjq))
|
|
(define qbqm 10)
|
|
(define tftg 1)
|
|
(define tjch (* ncrt rrgh))
|
|
(define mqrm (* cqcg cbdr))
|
|
(define vgjq 2)
|
|
(define mhbr (+ wggq grcv))
|
|
(define dfql (* dzwg snbl))
|
|
(define ccfw 8)
|
|
(define vsgw 3)
|
|
(define ltds (* wrll wnvf))
|
|
(define mqnl (* drlt bbhp))
|
|
(define lljf 3)
|
|
(define lslq 1)
|
|
(define ndnm 8)
|
|
(define qbjm 12)
|
|
(define cmtm (* twcj tjqj))
|
|
(define vhtl (* snff vldc))
|
|
(define nfhf 5)
|
|
(define lpvs 9)
|
|
(define jmcp 2)
|
|
(define jzlv (* cftm rhtv))
|
|
(define vjzr (+ swmh svhz))
|
|
(define rlrb (+ tftg qbqm))
|
|
(define zdsr 2)
|
|
(define vnft (+ mqrm tjch))
|
|
(define bjcs (/ mhbr vgjq))
|
|
(define qrll 2)
|
|
(define rdpg 7)
|
|
(define wpgm 5)
|
|
(define cdvv 4)
|
|
(define bpnt (+ ccfw dfql))
|
|
(define jscq 1)
|
|
(define fmwn 2)
|
|
(define qbvr (- ltds vsgw))
|
|
(define wgvv 2)
|
|
(define tsbf (+ lljf mqnl))
|
|
(define crnb (+ ndnm lslq))
|
|
(define jlmb (- cmtm qbjm))
|
|
(define qrch (+ nfhf vhtl))
|
|
(define mfrc (+ jmcp lpvs))
|
|
(define wjgf 2)
|
|
(define bcqm (+ vjzr jzlv))
|
|
(define hpmw (* zdsr rlrb))
|
|
(define vhrn (- bjcs vnft))
|
|
(define gcqh 3)
|
|
(define nhpf (+ rdpg qrll))
|
|
(define spcf (* cdvv wpgm))
|
|
(define lfhb (+ jscq bpnt))
|
|
(define btqb 3)
|
|
(define cldm 4)
|
|
(define hhjc (+ qbvr fmwn))
|
|
(define wcdm (* tsbf wgvv))
|
|
(define zcgs (* jlmb crnb))
|
|
(define mpfm (* mfrc qrch))
|
|
(define dqnp (/ bcqm wjgf))
|
|
(define wdqj (* vhrn hpmw))
|
|
(define vmzc (* nhpf gcqh))
|
|
(define jhlw 9)
|
|
(define zwqn (+ lfhb spcf))
|
|
(define bqht (* cldm btqb))
|
|
(define svzv 2)
|
|
(define zbhw (+ wcdm hhjc))
|
|
(define zvqs 11)
|
|
(define mwmp 6)
|
|
(define nvpd 3)
|
|
(define qrln 2)
|
|
(define wtnp 3)
|
|
(define rtjb 2)
|
|
(define brmz (+ mpfm zcgs))
|
|
(define jjjj 2)
|
|
(define rbmm 2)
|
|
(define fwrh (- wdqj dqnp))
|
|
(define vfzw (* jhlw vmzc))
|
|
(define vvbz (* bqht zwqn))
|
|
(define pvfv 2)
|
|
(define mrlc (* zbhw svzv))
|
|
(define rqbd 3)
|
|
(define pfdc (+ mwmp zvqs))
|
|
(define wgbc 3)
|
|
(define lqfq 3)
|
|
(define ztwb 9)
|
|
(define ljtp 16)
|
|
(define tnfz (* qrln nvpd))
|
|
(define ljnf (* rtjb wtnp))
|
|
(define nqpq 2)
|
|
(define vcqw (* jjjj brmz))
|
|
(define wrmw (* fwrh rbmm))
|
|
(define nrqr (+ vvbz vfzw))
|
|
(define mjmt 4)
|
|
(define nhjt 2)
|
|
(define vjjw (/ mrlc pvfv))
|
|
(define jmcf 12)
|
|
(define twjq 2)
|
|
(define brst 5)
|
|
(define swhh 2)
|
|
(define fqbj (* pfdc rqbd))
|
|
(define bjnj 2)
|
|
(define lpfz (* lqfq wgbc))
|
|
(define jqtj 5)
|
|
(define lbzn 2)
|
|
(define thcc (+ ljtp ztwb))
|
|
(define slnh (* ljnf tnfz))
|
|
(define sgpj 11)
|
|
(define fjzz 8)
|
|
(define wjzv (/ vcqw nqpq))
|
|
(define qcnv (+ nrqr wrmw))
|
|
(define csnf 1)
|
|
(define qfzb (+ nhjt mjmt))
|
|
(define lrcj 19)
|
|
(define qhnd 3)
|
|
(define hbqm 1)
|
|
(define zfmv 10)
|
|
(define dhfw (+ jmcf vjjw))
|
|
(define nlth 2)
|
|
(define hpmm 3)
|
|
(define gjzv (* brst twjq))
|
|
(define zmvz (* fqbj swhh))
|
|
(define bhvg (+ lpfz bjnj))
|
|
(define dbgp (* lbzn jqtj))
|
|
(define mwrt (+ slnh thcc))
|
|
(define dmtd (+ fjzz sgpj))
|
|
(define jnnp 3)
|
|
(define jqzv 2)
|
|
(define ddtd (+ qcnv wjzv))
|
|
(define hnlf 5)
|
|
(define cvvw 2)
|
|
(define rjdp (+ qfzb csnf))
|
|
(define sshm (* qhnd lrcj))
|
|
(define dqjz 7)
|
|
(define mlwr (+ zfmv hbqm))
|
|
(define mmnw 3)
|
|
(define zbzf (* nlth dhfw))
|
|
(define bcsc 6)
|
|
(define qlvz (+ gjzv hpmm))
|
|
(define nqpv (+ bhvg zmvz))
|
|
(define zncl (+ mwrt dbgp))
|
|
(define rrnt (* jnnp dmtd))
|
|
(define rhcv (/ ddtd jqzv))
|
|
(define btbn (* cvvw hnlf))
|
|
(define zwbh (* sshm rjdp))
|
|
(define jjrh (* mlwr dqjz))
|
|
(define vthd (* zbzf mmnw))
|
|
(define dspn (+ qlvz bcsc))
|
|
(define zwgg 5)
|
|
(define ttdb (+ zncl nqpv))
|
|
(define mrnr 2)
|
|
(define zvrq 5)
|
|
(define ffqs (- rhcv rrnt))
|
|
(define lbvn (+ zwbh btbn))
|
|
(define jswz (- vthd jjrh))
|
|
(define dvwj (* zwgg dspn))
|
|
(define djgb (+ mrnr ttdb))
|
|
(define lqcm (/ ffqs zvrq))
|
|
(define szcv (+ jswz lbvn))
|
|
(define snbm 4)
|
|
(define qgtc 3)
|
|
(define tprm 2)
|
|
(define mgjl 3)
|
|
(define gzbv (+ djgb dvwj))
|
|
(define mfhg 2)
|
|
(define hndh 2)
|
|
(define lmcj (+ szcv lqcm))
|
|
(define svst (+ qgtc snbm))
|
|
(define fdmf 3)
|
|
(define lmht 7)
|
|
(define jhwn (* mgjl tprm))
|
|
(define cfdl (* mfhg gzbv))
|
|
(define hjfj (* lmcj hndh))
|
|
(define lqdf 2)
|
|
(define qvfg (* fdmf svst))
|
|
(define dfdl 3)
|
|
(define bdgd 2)
|
|
(define mhlj 4)
|
|
(define ftvm 3)
|
|
(define qdrc 17)
|
|
(define mdrm (+ jhwn lmht))
|
|
(define rgpt 4)
|
|
(define cclc (+ hjfj cfdl))
|
|
(define mpnj 2)
|
|
(define btfl (+ qvfg lqdf))
|
|
(define dtfz (* bdgd dfdl))
|
|
(define scrz 2)
|
|
(define drrq 13)
|
|
(define brqb 4)
|
|
(define rmzw (+ ftvm mhlj))
|
|
(define jplv 3)
|
|
(define nqzz 11)
|
|
(define wqlh 16)
|
|
(define trpt (* mdrm qdrc))
|
|
(define jflm (/ cclc rgpt))
|
|
(define cjlh (* btfl mpnj))
|
|
(define ntmt 3)
|
|
(define hplt 11)
|
|
(define dqnh 2)
|
|
(define qflq (* scrz dtfz))
|
|
(define nwqz 1)
|
|
(define smdh 4)
|
|
(define pnvc (* brqb drrq))
|
|
(define bzqw 2)
|
|
(define tbqq (* jplv rmzw))
|
|
(define przh (+ wqlh nqzz))
|
|
(define jqsn 15)
|
|
(define mdht (- jflm trpt))
|
|
(define vrpp 10)
|
|
(define msdr 3)
|
|
(define crmw (+ ntmt cjlh))
|
|
(define sszh 2)
|
|
(define rvnh 3)
|
|
(define nzbz (* dqnh hplt))
|
|
(define tcgm 2)
|
|
(define lhgv (+ nwqz qflq))
|
|
(define bhrb (/ pnvc smdh))
|
|
(define gmhz 4)
|
|
(define fvhm 7)
|
|
(define mqvg (- tbqq bzqw))
|
|
(define gwlm 2)
|
|
(define wpqd (* jqsn przh))
|
|
(define nmvn (* vrpp mdht))
|
|
(define pzcc 5)
|
|
(define vwht 3)
|
|
(define cnhr 3)
|
|
(define smft (* crmw msdr))
|
|
(define tzcd 1)
|
|
(define plzd (* rvnh sszh))
|
|
(define lqft (* tcgm nzbz))
|
|
(define ffbb 2)
|
|
(define tctd 13)
|
|
(define ttwm 5)
|
|
(define fqjd 2)
|
|
(define qlzt 12)
|
|
(define sntb (* bhrb lhgv))
|
|
(define zvmv (* fvhm gmhz))
|
|
(define jlnf 3)
|
|
(define mqlt (* gwlm mqvg))
|
|
(define qdnl (- nmvn wpqd))
|
|
(define gzpf 2)
|
|
(define wjzd (* vwht pzcc))
|
|
(define tgvp (/ smft cnhr))
|
|
(define vwpq 2)
|
|
(define ntpj 4)
|
|
(define ffmp (+ plzd tzcd))
|
|
(define cvfw 3)
|
|
(define qwqw 5)
|
|
(define llhb 3)
|
|
(define jgnj 4)
|
|
(define lbbj 2)
|
|
(define vfwd 5)
|
|
(define bbzc (* ffbb lqft))
|
|
(define rvhn (* ttwm tctd))
|
|
(define cjbz (* qlzt fqjd))
|
|
(define wqdj (+ zvmv sntb))
|
|
(define qvvc 8)
|
|
(define mqgl (* mqlt jlnf))
|
|
(define rzbj 17)
|
|
(define bdtp (* gzpf qdnl))
|
|
(define ctjq (* tgvp wjzd))
|
|
(define rfbw (+ ntpj vwpq))
|
|
(define nsqq (* cvfw ffmp))
|
|
(define bppp (* llhb qwqw))
|
|
(define fbtc 2)
|
|
(define vfrh 9)
|
|
(define vrjj (* lbbj jgnj))
|
|
(define nrvw 2)
|
|
(define wjds 3)
|
|
(define fhdz 6)
|
|
(define bnjt 1)
|
|
(define ztdn 2)
|
|
(define rsqz (- bbzc vfwd))
|
|
(define ptdz 2)
|
|
(define tqst (+ cjbz rvhn))
|
|
(define nzlr 2)
|
|
(define dcfw (* qvvc wqdj))
|
|
(define sqdd (+ rzbj mqgl))
|
|
(define jtrg 7)
|
|
(define nwdv 3)
|
|
(define bcng (+ ctjq bdtp))
|
|
(define qqnm (- nsqq rfbw))
|
|
(define glqw 3)
|
|
(define dfrb (+ fbtc bppp))
|
|
(define ghvn (+ vrjj vfrh))
|
|
(define fngd (* wjds nrvw))
|
|
(define pjjj (+ bnjt fhdz))
|
|
(define rfcm (* rsqz ztdn))
|
|
(define rqpj (* tqst ptdz))
|
|
(define ffvs 2)
|
|
(define bcnp (/ dcfw nzlr))
|
|
(define snhd (* jtrg sqdd))
|
|
(define qpqs (/ bcng nwdv))
|
|
(define nwhm 3)
|
|
(define fjrq 6)
|
|
(define pbgr (* glqw qqnm))
|
|
(define wbbf (* ghvn dfrb))
|
|
(define lccp 3)
|
|
(define zhrs (+ pjjj fngd))
|
|
(define qbmm (+ rqpj rfcm))
|
|
(define dbfd (/ bcnp ffvs))
|
|
(define hjmp 6)
|
|
(define shcg (- qpqs snhd))
|
|
(define hnlj 5)
|
|
(define pnpc 5)
|
|
(define hmvq 17)
|
|
(define qrnj (* fjrq nwhm))
|
|
(define vgsm 5)
|
|
(define qhtv 5)
|
|
(define fqbl (+ wbbf pbgr))
|
|
(define ppts (* zhrs lccp))
|
|
(define ghvl (+ dbfd qbmm))
|
|
(define tpjw (/ shcg hjmp))
|
|
(define nmlt (* pnpc hnlj))
|
|
(define dngq 2)
|
|
(define dwnz 2)
|
|
(define pzpp 5)
|
|
(define rrnp (+ qrnj hmvq))
|
|
(define snwm 6)
|
|
(define nhnp 13)
|
|
(define npnf 1)
|
|
(define cvgt (* qhtv vgsm))
|
|
(define rpbm 3)
|
|
(define mwqc 2)
|
|
(define jmnj (+ ppts fqbl))
|
|
(define fjld (+ tpjw ghvl))
|
|
(define dqzt 5)
|
|
(define sdsl 2)
|
|
(define drhw (* dngq nmlt))
|
|
(define wpbs 2)
|
|
(define nnhm (* pzpp dwnz))
|
|
(define zdhf 2)
|
|
(define sjrh 7)
|
|
(define dbvt 3)
|
|
(define zvvp 3)
|
|
(define wlmv 4)
|
|
(define pnwh 2)
|
|
(define zmtg 8)
|
|
(define hpzh (+ snwm rrnp))
|
|
(define hzvm (+ npnf nhnp))
|
|
(define qjqw 2)
|
|
(define qspw 4)
|
|
(define bmwf (* rpbm cvgt))
|
|
(define hgzs 3)
|
|
(define tcjb 12)
|
|
(define cgwj 3)
|
|
(define grcn 13)
|
|
(define zprq (* jmnj mwqc))
|
|
(define lhpf (* dqzt fjld))
|
|
(define bwqm 19)
|
|
(define lrlg 10)
|
|
(define gmzh (/ drhw sdsl))
|
|
(define hhbn 4)
|
|
(define rmvq 2)
|
|
(define rdhg (* nnhm wpbs))
|
|
(define dqld (* sjrh zdhf))
|
|
(define swhz (* zvvp dbvt))
|
|
(define qqwz (* pnwh wlmv))
|
|
(define prbr (- hpzh zmtg))
|
|
(define tpmp (* qjqw hzvm))
|
|
(define fszd (+ bmwf qspw))
|
|
(define nqhg (+ tcjb hgzs))
|
|
(define cgcc 6)
|
|
(define frqq 4)
|
|
(define qvpv (* grcn cgwj))
|
|
(define chpt 2)
|
|
(define ppwc (- lhpf zprq))
|
|
(define vtnq 5)
|
|
(define twtb 3)
|
|
(define smrq (+ lrlg bwqm))
|
|
(define lqrr (* hhbn gmzh))
|
|
(define mfnh (* rdhg rmvq))
|
|
(define whbb 8)
|
|
(define rwbg 2)
|
|
(define pgbv (+ swhz dqld))
|
|
(define brfj (+ prbr qqwz))
|
|
(define vdsz 3)
|
|
(define wjtc (+ fszd tpmp))
|
|
(define llfg (* cgcc nqhg))
|
|
(define wpvg (* qvpv frqq))
|
|
(define mpvz (* ppwc chpt))
|
|
(define lwhp 5)
|
|
(define fqwz (+ twtb vtnq))
|
|
(define qgtf 6)
|
|
(define jvqz 1)
|
|
(define lqgr 9)
|
|
(define jfld 4)
|
|
(define gptt 2)
|
|
(define vrmt (- lqrr smrq))
|
|
(define vlgn 2)
|
|
(define gcmv (* whbb mfnh))
|
|
(define nqms 5)
|
|
(define hzmn (+ pgbv rwbg))
|
|
(define fwjg (* vdsz brfj))
|
|
(define gtqh 8)
|
|
(define mqcv 2)
|
|
(define vcwt (+ llfg wjtc))
|
|
(define cddt 6)
|
|
(define qlmg (+ mpvz wpvg))
|
|
(define bfzd 17)
|
|
(define tlmq (* fqwz lwhp))
|
|
(define nzcv 6)
|
|
(define qffb (+ jvqz qgtf))
|
|
(define pwqg 17)
|
|
(define mmps (* jfld lqgr))
|
|
(define hzjj 3)
|
|
(define rbsf 3)
|
|
(define wqnp 12)
|
|
(define jdsc 15)
|
|
(define frjl 2)
|
|
(define ldbp (+ vrmt gptt))
|
|
(define rmqt (/ gcmv vlgn))
|
|
(define vwdl (* hzmn nqms))
|
|
(define rfcq 6)
|
|
(define zrwb (* gtqh fwjg))
|
|
(define wcfj 2)
|
|
(define rsdv (* vcwt mqcv))
|
|
(define gmpl (/ qlmg cddt))
|
|
(define gmzt (* tlmq bfzd))
|
|
(define fbqs 11)
|
|
(define ltsl 2)
|
|
(define sgjm 8)
|
|
(define jfqs 15)
|
|
(define wfds 3)
|
|
(define rwcd (+ qffb nzcv))
|
|
(define jqhr 4)
|
|
(define bbcn 8)
|
|
(define rvlz 3)
|
|
(define llqs (+ mmps pwqg))
|
|
(define qwnt 2)
|
|
(define lfrb (* rbsf hzjj))
|
|
(define bngr 5)
|
|
(define tpjp (* jdsc wqnp))
|
|
(define grww 2)
|
|
(define vnbv (* ldbp frjl))
|
|
(define dmsz (+ vwdl rmqt))
|
|
(define vvgt (/ zrwb rfcq))
|
|
(define wpdn (* rsdv wcfj))
|
|
(define lrqh (+ gmzt gmpl))
|
|
(define wnjc 2)
|
|
(define fpwz (* ltsl fbqs))
|
|
(define fwmw (+ jfqs sgjm))
|
|
(define lltp (* rwcd wfds))
|
|
(define ftbq 5)
|
|
(define vclb (+ bbcn jqhr))
|
|
(define hrtz (* llqs rvlz))
|
|
(define wcmz 3)
|
|
(define cfbh 4)
|
|
(define qncp 3)
|
|
(define pvcs 4)
|
|
(define pnrv (- lfrb qwnt))
|
|
(define bcgz (/ tpjp bngr))
|
|
(define crrj (/ vnbv grww))
|
|
(define mlgj (+ vvgt dmsz))
|
|
(define bqvg (+ lrqh wpdn))
|
|
(define hjmr 3)
|
|
(define pvwn (* fpwz wnjc))
|
|
(define fhjz 2)
|
|
(define jbsn 3)
|
|
(define bmzw 5)
|
|
(define qtmp 2)
|
|
(define mstm 2)
|
|
(define fgbm (+ lltp fwmw))
|
|
(define llpf 2)
|
|
(define hhws (+ vclb ftbq))
|
|
(define ftmn (* wcmz hrtz))
|
|
(define qtvv 2)
|
|
(define fvsb (* qncp cfbh))
|
|
(define shtz (+ pnrv pvcs))
|
|
(define twsj 5)
|
|
(define slmm (+ crrj bcgz))
|
|
(define ftzc 2)
|
|
(define lpzb (+ bqvg mlgj))
|
|
(define jlwb 3)
|
|
(define jqrl (+ pvwn hjmr))
|
|
(define ddln 1)
|
|
(define tmhl (* jbsn fhjz))
|
|
(define nvrb 3)
|
|
(define cvnr (+ qtmp bmzw))
|
|
(define lhfr (/ fgbm mstm))
|
|
(define jgld 5)
|
|
(define thlz 2)
|
|
(define flvw 5)
|
|
(define qldj 2)
|
|
(define swsv 7)
|
|
(define drvt (* hhws llpf))
|
|
(define sflt (+ qtvv ftmn))
|
|
(define chfz 3)
|
|
(define qmzt 9)
|
|
(define zbbf (+ shtz fvsb))
|
|
(define jmqh 14)
|
|
(define fmbj (* slmm twsj))
|
|
(define mqfd (/ lpzb ftzc))
|
|
(define htgm 3)
|
|
(define wgsb (* jqrl jlwb))
|
|
(define ndsm (+ tmhl ddln))
|
|
(define bnmb (* cvnr nvrb))
|
|
(define vsqt 5)
|
|
(define ngbg (* jgld lhfr))
|
|
(define nbbd (* flvw thlz))
|
|
(define bndd 7)
|
|
(define pbvh 3)
|
|
(define pnfb 3)
|
|
(define bgzz (* swsv qldj))
|
|
(define jpvr (+ sflt drvt))
|
|
(define wqfg (* qmzt chfz))
|
|
(define vzcr (+ jmqh zbbf))
|
|
(define gbgs (- mqfd fmbj))
|
|
(define phwc 10)
|
|
(define zrbc 3)
|
|
(define pmfh 3)
|
|
(define lrbp (/ wgsb htgm))
|
|
(define mddc 2)
|
|
(define vspf (+ bnmb ndsm))
|
|
(define gvmj (/ ngbg vsqt))
|
|
(define brqh (+ bndd nbbd))
|
|
(define fcql 20)
|
|
(define jfsr 8)
|
|
(define blnq 6)
|
|
(define sdrn 9)
|
|
(define mpws (* pnfb pbvh))
|
|
(define jpcd 2)
|
|
(define qnbn (- jpvr bgzz))
|
|
(define ncnm (* vzcr wqfg))
|
|
(define pgtq (* phwc gbgs))
|
|
(define dqsv (* pmfh zrbc))
|
|
(define gdmv 5)
|
|
(define nmlg 2)
|
|
(define nvjf (* mddc lrbp))
|
|
(define hrbr (+ gvmj vspf))
|
|
(define ndmd 2)
|
|
(define fhtw (+ fcql brqh))
|
|
(define nfbp 2)
|
|
(define vpvl (* blnq jfsr))
|
|
(define cvqf (* mpws sdrn))
|
|
(define fmvw (* qnbn jpcd))
|
|
(define vhqz (- pgtq ncnm))
|
|
(define tvgm (* gdmv dqsv))
|
|
(define lvtv (/ nvjf nmlg))
|
|
(define qlzg 2)
|
|
(define jzvg 5)
|
|
(define fzdg 2)
|
|
(define jvsz (* ndmd hrbr))
|
|
(define blgg 15)
|
|
(define qqpl 5)
|
|
(define zmlh (* nfbp fhtw))
|
|
(define nnsc (+ cvqf vpvl))
|
|
(define tptf 3)
|
|
(define jjvz (+ vhqz fmvw))
|
|
(define ndpf 10)
|
|
(define vwmr (+ lvtv tvgm))
|
|
(define rthb 2)
|
|
(define shwr 5)
|
|
(define lzgm (+ jzvg qlzg))
|
|
(define fpvs (/ jvsz fzdg))
|
|
(define glqr (* qqpl blgg))
|
|
(define rtpz (+ nnsc zmlh))
|
|
(define qwcl (/ jjvz tptf))
|
|
(define blmp (* vwmr ndpf))
|
|
(define hbzt (+ shwr rthb))
|
|
(define mfsz (* fpvs lzgm))
|
|
(define fqgl 3)
|
|
(define ccjf 13)
|
|
(define csln 17)
|
|
(define hqdv 5)
|
|
(define tzcl 2)
|
|
(define fvrg 3)
|
|
(define dpmg 3)
|
|
(define vtgj 5)
|
|
(define tqzv (+ rtpz glqr))
|
|
(define wzsh 3)
|
|
(define sdhj 2)
|
|
(define zdfg (+ blmp qwcl))
|
|
(define wfms 2)
|
|
(define hnqc (/ mfsz hbzt))
|
|
(define djrh (* ccjf fqgl))
|
|
(define tdrq (* hqdv csln))
|
|
(define nrsd 10)
|
|
(define dcpm 3)
|
|
(define lqml 4)
|
|
(define hgnr 9)
|
|
(define wfnm (* fvrg tzcl))
|
|
(define cfmw 1)
|
|
(define wcfp 3)
|
|
(define nght 2)
|
|
(define pvtb 2)
|
|
(define qqdn 3)
|
|
(define gppj 1)
|
|
(define rnbs (+ vtgj dpmg))
|
|
(define gqgh (* wzsh tqzv))
|
|
(define nqlh (* zdfg sdhj))
|
|
(define frlv 3)
|
|
(define mttr (* hnqc wfms))
|
|
(define tpnf 15)
|
|
(define gqrp (+ tdrq djrh))
|
|
(define zptr 3)
|
|
(define ndgh 4)
|
|
(define jbwd 6)
|
|
(define lwld 1)
|
|
(define qwqq 2)
|
|
(define ltgf 3)
|
|
(define pqsr 2)
|
|
(define vcfm 5)
|
|
(define qpct 3)
|
|
(define pbdd (* dcpm nrsd))
|
|
(define trbs 2)
|
|
(define hdrj 5)
|
|
(define bnws 2)
|
|
(define fjzn (+ hgnr lqml))
|
|
(define sbpp 17)
|
|
(define zgzs 3)
|
|
(define gzwm 2)
|
|
(define ssnq (+ cfmw wfnm))
|
|
(define lfhp (* nght wcfp))
|
|
(define ntsl 1)
|
|
(define qsml 18)
|
|
(define cnzj (* qqdn pvtb))
|
|
(define qpdv 15)
|
|
(define dtzl (+ rnbs gppj))
|
|
(define twwv 19)
|
|
(define hnbn 2)
|
|
(define qfss 10)
|
|
(define zhmb 15)
|
|
(define lmjg 4)
|
|
(define bpgp (- nqlh gqgh))
|
|
(define rvjf (* mttr frlv))
|
|
(define jszj (+ gqrp tpnf))
|
|
(define qtgd 2)
|
|
(define sfcv 7)
|
|
(define mgsl 2)
|
|
(define vlqd (* ndgh zptr))
|
|
(define frjj 9)
|
|
(define dptm 6)
|
|
(define mnzz (+ lwld jbwd))
|
|
(define rwzt (* ltgf qwqq))
|
|
(define qlmw (+ vcfm pqsr))
|
|
(define mmbs 3)
|
|
(define wsnf 4)
|
|
(define mnpl (- pbdd qpct))
|
|
(define wrbf 2)
|
|
(define cprm 4)
|
|
(define pnmc 13)
|
|
(define frrn 3)
|
|
(define qmgt 3)
|
|
(define hdff 4)
|
|
(define lvbp (+ hdrj trbs))
|
|
(define ptwr 7)
|
|
(define btzg 5)
|
|
(define rbqt 5)
|
|
(define wfnl 5)
|
|
(define nzhf (* fjzn bnws))
|
|
(define gggh 3)
|
|
(define vvjg (* zgzs sbpp))
|
|
(define sdjb (* ssnq gzwm))
|
|
(define wlfp (+ ntsl lfhp))
|
|
(define ndtz (+ cnzj qsml))
|
|
(define nchp (+ dtzl qpdv))
|
|
(define dgvh 3)
|
|
(define pgfr 3)
|
|
(define bnfz 2)
|
|
(define qdrg 5)
|
|
(define csdf 2)
|
|
(define mfmc (* hnbn twwv))
|
|
(define qlvg 2)
|
|
(define pdbt 11)
|
|
(define dphz 3)
|
|
(define ccbp 4)
|
|
(define wfjn 5)
|
|
(define vrct 2)
|
|
(define rqsw 5)
|
|
(define bhzq (* zhmb qfss))
|
|
(define jwjj 15)
|
|
(define jsrb 13)
|
|
(define vdjz 4)
|
|
(define vfgt 7)
|
|
(define dgpr (/ bpgp lmjg))
|
|
(define cwvl (+ jszj rvjf))
|
|
(define nzdz (+ sfcv qtgd))
|
|
(define bdqg 2)
|
|
(define rlvd (/ vlqd mgsl))
|
|
(define csfh 2)
|
|
(define hjqq 11)
|
|
(define pfvz 2)
|
|
(define pcwz (* dptm frjj))
|
|
(define stzl (+ rwzt mnzz))
|
|
(define dnzc (* mmbs qlmw))
|
|
(define tbqc 2)
|
|
(define qcnn (- mnpl wsnf))
|
|
(define zzpd 2)
|
|
(define ldbg (* cprm wrbf))
|
|
(define rnns (* frrn pnmc))
|
|
(define qfrg (* hdff qmgt))
|
|
(define rlqh (* ptwr lvbp))
|
|
(define rdfn (* rbqt btzg))
|
|
(define jtvw (- nzhf wfnl))
|
|
(define mnrr (/ vvjg gggh))
|
|
(define vqlt 2)
|
|
(define blgf 3)
|
|
(define bsqn (+ wlfp sdjb))
|
|
(define tsqc 2)
|
|
(define dswn 11)
|
|
(define hstj 2)
|
|
(define szhq (* nchp ndtz))
|
|
(define mqzw 2)
|
|
(define lzhf 5)
|
|
(define zjcn (* pgfr dgvh))
|
|
(define pzqv 3)
|
|
(define jvqf 2)
|
|
(define shrh 13)
|
|
(define nqgr 4)
|
|
(define rzcm 6)
|
|
(define rqss 3)
|
|
(define rvhs 2)
|
|
(define svwg 4)
|
|
(define dfps 5)
|
|
(define wnjl 9)
|
|
(define wrst (+ qdrg bnfz))
|
|
(define rffd (/ mfmc csdf))
|
|
(define zpqd 2)
|
|
(define znjr 2)
|
|
(define wrvl (* pdbt qlvg))
|
|
(define gbtc 3)
|
|
(define pvfm 2)
|
|
(define ngfs (* ccbp dphz))
|
|
(define sstg (+ vrct wfjn))
|
|
(define cjvp 2)
|
|
(define jvrt (/ bhzq rqsw))
|
|
(define zjpc 4)
|
|
(define jclb 2)
|
|
(define zqpw (+ jsrb jwjj))
|
|
(define tlnz (* vfgt vdjz))
|
|
(define ghfr 2)
|
|
(define pnvd (+ cwvl dgpr))
|
|
(define mcfr 1)
|
|
(define lrvc 10)
|
|
(define djgh (+ bdqg nzdz))
|
|
(define gfbw (+ csfh rlvd))
|
|
(define gvww 2)
|
|
(define mgmw (* pfvz hjqq))
|
|
(define dbfm 9)
|
|
(define bblh 1)
|
|
(define slww (+ stzl pcwz))
|
|
(define fzrd 2)
|
|
(define nhfw (+ tbqc dnzc))
|
|
(define vrcl 5)
|
|
(define mpst (* zzpd qcnn))
|
|
(define hjgd 12)
|
|
(define nbcb (+ rnns ldbg))
|
|
(define rgzs 3)
|
|
(define gnsc 2)
|
|
(define cfzf (+ rlqh qfrg))
|
|
(define trpv 7)
|
|
(define bnmf (* jtvw rdfn))
|
|
(define nrjc 2)
|
|
(define pwln (* vqlt mnrr))
|
|
(define qrsg 3)
|
|
(define wrpp 14)
|
|
(define jfcd (/ bsqn blgf))
|
|
(define smsm 4)
|
|
(define qwqc 3)
|
|
(define zslv 3)
|
|
(define smnv 3)
|
|
(define jrvp 17)
|
|
(define ltsv 3)
|
|
(define ltnz (* dswn tsqc))
|
|
(define vdbp 1)
|
|
(define hfbh 16)
|
|
(define dpvl 8)
|
|
(define wslz (/ szhq hstj))
|
|
(define nfgv (+ lzhf mqzw))
|
|
(define vszd 12)
|
|
(define fsrm (* pzqv zjcn))
|
|
(define rpbj (* shrh jvqf))
|
|
(define zdnh 11)
|
|
(define jwqg 2)
|
|
(define lghm 2)
|
|
(define ftjv 3)
|
|
(define mrtq (* rzcm nqgr))
|
|
(define frjp 17)
|
|
(define cdnm 3)
|
|
(define jtvm 9)
|
|
(define nlgg (* rvhs rqss))
|
|
(define lbbv 3)
|
|
(define cstb (* dfps svwg))
|
|
(define tdjh (* wrst wnjl))
|
|
(define plvw (* zpqd rffd))
|
|
(define csgr (/ wrvl znjr))
|
|
(define cjhz (* pvfm gbtc))
|
|
(define vtdp 10)
|
|
(define lrgv 2)
|
|
(define tsft (+ sstg ngfs))
|
|
(define vtns (/ jvrt cjvp))
|
|
(define gzrs (* jclb zjpc))
|
|
(define jnwv (* tlnz zqpw))
|
|
(define jdbp (* pnvd ghfr))
|
|
(define spjg 5)
|
|
(define sdgs 5)
|
|
(define vvzh 6)
|
|
(define qhvn 3)
|
|
(define pjrt 1)
|
|
(define sqzp 5)
|
|
(define npcs (+ lrvc mcfr))
|
|
(define hhcv 2)
|
|
(define qmjq 5)
|
|
(define ghqp 5)
|
|
(define dlgc (+ gfbw djgh))
|
|
(define jlqg 4)
|
|
(define rbtb (/ mgmw gvww))
|
|
(define vwvc 17)
|
|
(define jpzw 3)
|
|
(define fqlp (+ bblh dbfm))
|
|
(define gtwd 2)
|
|
(define fzdp (* fzrd slww))
|
|
(define sphc (* vrcl nhfw))
|
|
(define jrgs (+ hjgd mpst))
|
|
(define mqzp 2)
|
|
(define nssr 3)
|
|
(define cstm (* rgzs nbcb))
|
|
(define fnrh 2)
|
|
(define ghtd (* cfzf gnsc))
|
|
(define dggg (/ bnmf trpv))
|
|
(define psfp 3)
|
|
(define ppll 5)
|
|
(define dpqz 3)
|
|
(define pqqj 2)
|
|
(define vmjn 12)
|
|
(define bsvc (/ pwln nrjc))
|
|
(define hqbd 4)
|
|
(define gmln 2)
|
|
(define wcpr 5)
|
|
(define vvvb (- wrpp qrsg))
|
|
(define rnnq 3)
|
|
(define rrmg 19)
|
|
(define zmmd (+ smsm jfcd))
|
|
(define sbqm 3)
|
|
(define vznc 2)
|
|
(define gpdf (* zslv qwqc))
|
|
(define qnld (* jrvp smnv))
|
|
(define zssf 5)
|
|
(define twjs (- ltnz ltsv))
|
|
(define wmzt 3)
|
|
(define mfql 3)
|
|
(define qwnz (+ hfbh vdbp))
|
|
(define nvjh 6)
|
|
(define tvrz (/ wslz dpvl))
|
|
(define nfvj 4)
|
|
(define lhmd (+ vszd nfgv))
|
|
(define rzzg (+ rpbj fsrm))
|
|
(define bsmm 2)
|
|
(define snmq (+ jwqg zdnh))
|
|
(define hfvj 2)
|
|
(define tlzh 11)
|
|
(define bftg (* ftjv lghm))
|
|
(define rmfv 5)
|
|
(define mspl 5)
|
|
(define vffj (+ frjp mrtq))
|
|
(define zrnr 2)
|
|
(define bcbw (* jtvm cdnm))
|
|
(define trft (* lbbv nlgg))
|
|
(define bnwj 2)
|
|
(define jdfj 15)
|
|
(define rqbq 2)
|
|
(define gnzq 5)
|
|
(define drln 6)
|
|
(define rwth (+ tdjh cstb))
|
|
(define llcn 4)
|
|
(define jdgq 2)
|
|
(define vhds 12)
|
|
(define ptnv (+ csgr plvw))
|
|
(define rfjw 13)
|
|
(define lflj (* vtdp cjhz))
|
|
(define hfbg 2)
|
|
(define ctqb (* tsft lrgv))
|
|
(define wgvj 4)
|
|
(define pmng (+ gzrs vtns))
|
|
(define hzrc (+ jdbp jnwv))
|
|
(define fvph 3)
|
|
(define nnmh 5)
|
|
(define jbrp 11)
|
|
(define ffnn 3)
|
|
(define znlh 4)
|
|
(define ndcd (* sdgs spjg))
|
|
(define bnlr (* qhvn vvzh))
|
|
(define jjwr 6)
|
|
(define fbpz (+ sqzp pjrt))
|
|
(define cqmq 13)
|
|
(define flcb 2)
|
|
(define tqlp 2)
|
|
(define dsgt (* hhcv npcs))
|
|
(define vbvt (* ghqp qmjq))
|
|
(define pgdw 4)
|
|
(define mtfr (* jlqg dlgc))
|
|
(define nbfg (* vwvc rbtb))
|
|
(define qhzd (+ fqlp jpzw))
|
|
(define dwdd (/ fzdp gtwd))
|
|
(define qgwg (+ jrgs sphc))
|
|
(define pdmb 2)
|
|
(define ftqd (* nssr mqzp))
|
|
(define mrjc (* fnrh cstm))
|
|
(define dpgl 2)
|
|
(define mspb (+ dggg ghtd))
|
|
(define bjbr 3)
|
|
(define njcj (* ppll psfp))
|
|
(define czvm 18)
|
|
(define fvng 19)
|
|
(define zwwb (* pqqj dpqz))
|
|
(define vdgt 5)
|
|
(define vzrz (+ bsvc vmjn))
|
|
(define gnjq 2)
|
|
(define tfpw (* gmln hqbd))
|
|
(define dczh (* vvvb wcpr))
|
|
(define mbqs (* rrmg rnnq))
|
|
(define npvl (* sbqm zmmd))
|
|
(define glts (- gpdf vznc))
|
|
(define wnbb (+ zssf qnld))
|
|
(define nlst (+ wmzt twjs))
|
|
(define rfcv (* qwnz mfql))
|
|
(define fbjn (/ tvrz nvjh))
|
|
(define rlbp 1)
|
|
(define jhzw 5)
|
|
(define jwwv 2)
|
|
(define crrm 2)
|
|
(define bsnq 3)
|
|
(define hncq 11)
|
|
(define rqfq (* lhmd nfvj))
|
|
(define mvnc 2)
|
|
(define mhdn (* bsmm rzzg))
|
|
(define vmnc 5)
|
|
(define nwwb (* hfvj snmq))
|
|
(define clbn 2)
|
|
(define wbvt (+ bftg tlzh))
|
|
(define hgwm (* mspl rmfv))
|
|
(define ptvh 3)
|
|
(define gcmz (* zrnr vffj))
|
|
(define nzwc 3)
|
|
(define hpdh 2)
|
|
(define nsfm 4)
|
|
(define wlqd 2)
|
|
(define sqml 7)
|
|
(define pchr (+ trft bcbw))
|
|
(define cbjl (* jdfj bnwj))
|
|
(define tsms (* gnzq rqbq))
|
|
(define gfml 4)
|
|
(define qfln 3)
|
|
(define vlmc 4)
|
|
(define wclq (+ rwth drln))
|
|
(define rpwz 3)
|
|
(define cvhn (* jdgq llcn))
|
|
(define qpqb (+ ptnv vhds))
|
|
(define vjgb 3)
|
|
(define bhvr (+ lflj rfjw))
|
|
(define zbhj (* ctqb hfbg))
|
|
(define rhwm 4)
|
|
(define zlpv (* pmng wgvj))
|
|
(define nrqv (* fvph hzrc))
|
|
(define wwtj 5)
|
|
(define wnzr (* jbrp nnmh))
|
|
(define jqqs (+ znlh ffnn))
|
|
(define pfml (+ bnlr ndcd))
|
|
(define slpm (* fbpz jjwr))
|
|
(define zglw (* flcb cqmq))
|
|
(define tfdv 2)
|
|
(define wgcm (/ dsgt tqlp))
|
|
(define cprt 3)
|
|
(define jfvq (+ pgdw vbvt))
|
|
(define zgdb 2)
|
|
(define mvgg (+ nbfg mtfr))
|
|
(define drrf 9)
|
|
(define wsml 3)
|
|
(define fcgs 7)
|
|
(define wlpd 2)
|
|
(define bwff (+ dwdd qhzd))
|
|
(define pgrc (* pdmb qgwg))
|
|
(define dsqb (/ mrjc ftqd))
|
|
(define vvhm (* mspb dpgl))
|
|
(define qrgn 5)
|
|
(define rzjm 5)
|
|
(define djqq 4)
|
|
(define rsnp 3)
|
|
(define cgcz (- njcj bjbr))
|
|
(define jdsd 5)
|
|
(define scdn 6)
|
|
(define bmlj (+ fvng czvm))
|
|
(define ldtj 2)
|
|
(define cpqv 15)
|
|
(define qgnb (+ vdgt zwwb))
|
|
(define nlsw (* gnjq vzrz))
|
|
(define brfc (- dczh tfpw))
|
|
(define lzzh 11)
|
|
(define vntv (* npvl mbqs))
|
|
(define rbpq (* wnbb glts))
|
|
(define hmfd 2)
|
|
(define qlvw (+ rfcv nlst))
|
|
(define wbgs 3)
|
|
(define ngzt (+ rlbp fbjn))
|
|
(define mlbw (* jwwv jhzw))
|
|
(define lqqh 5)
|
|
(define vmgn 1)
|
|
(define mwwr (* bsnq crrm))
|
|
(define wltv (- rqfq hncq))
|
|
(define rctr (* mhdn mvnc))
|
|
(define rgrp 7)
|
|
(define gssz (* nwwb vmnc))
|
|
(define spgw (* wbvt clbn))
|
|
(define pgvq (* ptvh hgwm))
|
|
(define tpdj 9)
|
|
(define sqmd 2)
|
|
(define mffc 3)
|
|
(define rjrt (* nzwc gcmz))
|
|
(define jffq 3)
|
|
(define rlcw 2)
|
|
(define bvdb 2)
|
|
(define hzcm 4)
|
|
(define bhmz 3)
|
|
(define lqdc 5)
|
|
(define tsjq (* nsfm hpdh))
|
|
(define ttvz 2)
|
|
(define cnln (* sqml wlqd))
|
|
(define fjgh (+ cbjl pchr))
|
|
(define nttd 9)
|
|
(define zrpj (* gfml tsms))
|
|
(define pjss 2)
|
|
(define hcpf 4)
|
|
(define hzpr 5)
|
|
(define wphq 5)
|
|
(define zjmw 3)
|
|
(define scdt (* vlmc qfln))
|
|
(define cgnr 4)
|
|
(define bdcm 2)
|
|
(define bnvg 3)
|
|
(define tvtj 13)
|
|
(define hsmp (* rpwz wclq))
|
|
(define mvmz (* qpqb cvhn))
|
|
(define tfjw (* bhvr vjgb))
|
|
(define bcdf (* rhwm zbhj))
|
|
(define zngg 4)
|
|
(define dbcs (- nrqv zlpv))
|
|
(define mrvr 3)
|
|
(define dcph 4)
|
|
(define hgls (/ wnzr wwtj))
|
|
(define qqpt 5)
|
|
(define nmts (* pfml jqqs))
|
|
(define mhzn (* zglw slpm))
|
|
(define bghp (* wgcm tfdv))
|
|
(define blbc (* jfvq cprt))
|
|
(define mdpg 2)
|
|
(define sgzh (* mvgg zgdb))
|
|
(define rdbs (* wsml drrf))
|
|
(define lpjq (* wlpd fcgs))
|
|
(define bqnn (- pgrc bwff))
|
|
(define qbwf (- vvhm dsqb))
|
|
(define gjmt 3)
|
|
(define tdhw (* rzjm qrgn))
|
|
(define pdbc (* rsnp djqq))
|
|
(define chvq (+ jdsd cgcz))
|
|
(define swds (+ bmlj scdn))
|
|
(define vlhc 13)
|
|
(define pjds (+ cpqv ldtj))
|
|
(define vfhg (- nlsw qgnb))
|
|
(define zcgn (* lzzh brfc))
|
|
(define dzlc (+ rbpq vntv))
|
|
(define bpwd 2)
|
|
(define qdfp (* qlvw hmfd))
|
|
(define stqc 5)
|
|
(define djff 12)
|
|
(define swpl 2)
|
|
(define nvjl (* ngzt wbgs))
|
|
(define bbzt 8)
|
|
(define fjnh 5)
|
|
(define dsng 5)
|
|
(define pwpn 3)
|
|
(define drgv 3)
|
|
(define gfrq 4)
|
|
(define fjps 5)
|
|
(define ppfs 5)
|
|
(define stcv 3)
|
|
(define dzvg 2)
|
|
(define fhmz 2)
|
|
(define drnb (* lqqh mlbw))
|
|
(define lpqs 1)
|
|
(define trdj 10)
|
|
(define rtbm 3)
|
|
(define bssd 2)
|
|
(define fvzw (+ mwwr vmgn))
|
|
(define bcpn 7)
|
|
(define dcbt (+ rctr wltv))
|
|
(define smwv (+ gssz rgrp))
|
|
(define qgjf (+ pgvq spgw))
|
|
(define nfhw 2)
|
|
(define ngzp 11)
|
|
(define qrpv (* sqmd tpdj))
|
|
(define qfsz 2)
|
|
(define cdtq (/ rjrt mffc))
|
|
(define mwdl (* rlcw jffq))
|
|
(define sdwj 2)
|
|
(define sbtd 3)
|
|
(define bcww 11)
|
|
(define phjj (* hzcm bvdb))
|
|
(define mvmj (* lqdc bhmz))
|
|
(define gbzd (* ttvz tsjq))
|
|
(define snfj 1)
|
|
(define nlts (- fjgh cnln))
|
|
(define hqbb 2)
|
|
(define hmqr (- zrpj nttd))
|
|
(define ngps 11)
|
|
(define fbgc 2)
|
|
(define mtwg (* hcpf pjss))
|
|
(define zshp (* wphq hzpr))
|
|
(define rrll (* scdt zjmw))
|
|
(define hrtv (* bdcm cgnr))
|
|
(define tzth (* tvtj bnvg))
|
|
(define nlcv 5)
|
|
(define lfpz (+ mvmz hsmp))
|
|
(define rscq (+ bcdf tfjw))
|
|
(define hsbr (/ dbcs zngg))
|
|
(define jddd (+ dcph mrvr))
|
|
(define mgsz (* qqpt hgls))
|
|
(define qbgj (+ mhzn nmts))
|
|
(define dqcj (+ blbc bghp))
|
|
(define mbvg (/ sgzh mdpg))
|
|
(define gtbs 13)
|
|
(define tlwr 3)
|
|
(define lhsw (+ lpjq rdbs))
|
|
(define zrfw 7)
|
|
(define sdmb 15)
|
|
(define chvn 3)
|
|
(define rtnf (+ qbwf bqnn))
|
|
(define mwms 2)
|
|
(define wmdp (- tdhw gjmt))
|
|
(define bshp (+ chvq pdbc))
|
|
(define djmr 2)
|
|
(define nbpq 2)
|
|
(define ztrt (* vlhc swds))
|
|
(define bnzl (* vfhg pjds))
|
|
(define ztpd (+ dzlc zcgn))
|
|
(define tnbt (* qdfp bpwd))
|
|
(define qnvn 2)
|
|
(define gjbv (* djff stqc))
|
|
(define jzcd (- nvjl swpl))
|
|
(define jhgd (* fjnh bbzt))
|
|
(define vhhz (* pwpn dsng))
|
|
(define wjmq 6)
|
|
(define lvcn 4)
|
|
(define lrzn (+ gfrq drgv))
|
|
(define cbqn (* ppfs fjps))
|
|
(define rmmz 2)
|
|
(define tbdh (* dzvg stcv))
|
|
(define tfqh 5)
|
|
(define gvfn (/ drnb fhmz))
|
|
(define slds 2)
|
|
(define mswh 5)
|
|
(define bjwg (+ trdj lpqs))
|
|
(define dlws (* bssd rtbm))
|
|
(define mcht 2)
|
|
(define gznh 7)
|
|
(define sjcd (* bcpn fvzw))
|
|
(define rdnj (+ smwv dcbt))
|
|
(define hcdz (* nfhw qgjf))
|
|
(define bwwc 3)
|
|
(define rhqj (+ qrpv ngzp))
|
|
(define twdf 2)
|
|
(define mfst (/ cdtq qfsz))
|
|
(define zhgt 3)
|
|
(define wtlg 19)
|
|
(define tjtl 7)
|
|
(define zmdq (+ sdwj mwdl))
|
|
(define qcml 3)
|
|
(define zphs (+ bcww sbtd))
|
|
(define wvfb (+ mvmj phjj))
|
|
(define vjbz 5)
|
|
(define fjvg (+ snfj gbzd))
|
|
(define zvqw 4)
|
|
(define ppwz (* hqbb nlts))
|
|
(define ftzm 3)
|
|
(define cdpw (* ngps hmqr))
|
|
(define cwhc 3)
|
|
(define jbtg 9)
|
|
(define gzgm 4)
|
|
(define vhwz (+ mtwg fbgc))
|
|
(define rccr 2)
|
|
(define jdcd 3)
|
|
(define gwpm (+ rrll zshp))
|
|
(define btwt (* tzth hrtv))
|
|
(define mmtj 6)
|
|
(define ppjl (/ lfpz nlcv))
|
|
(define wszm (+ hsbr rscq))
|
|
(define bzdh 2)
|
|
(define hslj (* mgsz jddd))
|
|
(define ltqr (+ dqcj qbgj))
|
|
(define dbcw (* gtbs mbvg))
|
|
(define nnzp (* lhsw tlwr))
|
|
(define tbwl (* sdmb zrfw))
|
|
(define dshq (* rtnf chvn))
|
|
(define tqfz (/ wmdp mwms))
|
|
(define msmm (* djmr bshp))
|
|
(define fzvh (* ztrt nbpq))
|
|
(define sjfs (- ztpd bnzl))
|
|
(define pmlg 8)
|
|
(define lgrj (* qnvn tnbt))
|
|
(define rtmh 15)
|
|
(define bvfr (+ jzcd gjbv))
|
|
(define fsgb (+ vhhz jhgd))
|
|
(define qcfn (* lvcn wjmq))
|
|
(define lrlz 1)
|
|
(define nltq (- cbqn lrzn))
|
|
(define wfld 8)
|
|
(define zfjw (+ tbdh rmmz))
|
|
(define mrwz 12)
|
|
(define lclg 8)
|
|
(define mdnp (* gvfn tfqh))
|
|
(define ffqr 16)
|
|
(define qfqz (* mswh slds))
|
|
(define pjlz 2)
|
|
(define nldv 4)
|
|
(define tzhp 15)
|
|
(define ppsl (+ dlws bjwg))
|
|
(define rjbz (* gznh mcht))
|
|
(define rswn 5)
|
|
(define hcfs 2)
|
|
(define hlmn (+ rdnj sjcd))
|
|
(define qmpm (* bwwc hcdz))
|
|
(define svvq (* twdf rhqj))
|
|
(define fddw (* zhgt mfst))
|
|
(define gdgd 7)
|
|
(define jfrn 3)
|
|
(define rjtc (+ tjtl wtlg))
|
|
(define lfjp 3)
|
|
(define nfnw 2)
|
|
(define cblz 5)
|
|
(define flhs (+ qcml zmdq))
|
|
(define snsc 2)
|
|
(define hnst (+ wvfb zphs))
|
|
(define chtt 2)
|
|
(define wtlq 3)
|
|
(define hrcp (* fjvg vjbz))
|
|
(define vcpt (* ppwz zvqw))
|
|
(define mzfn (* cdpw ftzm))
|
|
(define rwsm 10)
|
|
(define jfmb (* jbtg cwhc))
|
|
(define sgvm (* vhwz gzgm))
|
|
(define dbht (* jdcd rccr))
|
|
(define jdmt (- btwt gwpm))
|
|
(define brqv 2)
|
|
(define gnrj (* ppjl mmtj))
|
|
(define lbgc (* bzdh wszm))
|
|
(define hmrs (* ltqr hslj))
|
|
(define rvmp (* nnzp dbcw))
|
|
(define lhml 7)
|
|
(define zscd (* dshq tbwl))
|
|
(define dnvm (- msmm tqfz))
|
|
(define cdvw (+ sjfs fzvh))
|
|
(define vwdt (/ lgrj pmlg))
|
|
(define drct (+ bvfr rtmh))
|
|
(define vzts 6)
|
|
(define nqsl (+ qcfn fsgb))
|
|
(define wzfr (+ nltq lrlz))
|
|
(define qznt (* zfjw wfld))
|
|
(define cscm (* lclg mrwz))
|
|
(define wchl (+ ffqr mdnp))
|
|
(define rbzl (* pjlz qfqz))
|
|
(define zqjp (- tzhp nldv))
|
|
(define lddq (+ rjbz ppsl))
|
|
(define lwsn (+ hcfs rswn))
|
|
(define jdrg (+ qmpm hlmn))
|
|
(define tdnf 4)
|
|
(define djjd (+ fddw svvq))
|
|
(define lbzc (* jfrn gdgd))
|
|
(define qvbn 2)
|
|
(define fhzm (+ lfjp rjtc))
|
|
(define cwjp 9)
|
|
(define zvst 3)
|
|
(define bvzn 2)
|
|
(define stcr (+ cblz nfnw))
|
|
(define dmrn 9)
|
|
(define crqg 3)
|
|
(define qssh 5)
|
|
(define jtcf 4)
|
|
(define mnhf 3)
|
|
(define phbh (* snsc flhs))
|
|
(define nzbp (* chtt hnst))
|
|
(define vtvn (* hrcp wtlq))
|
|
(define gtwp 3)
|
|
(define ffnt (+ mzfn vcpt))
|
|
(define svcp (+ jfmb rwsm))
|
|
(define grdf (+ dbht sgvm))
|
|
(define mpjj 10)
|
|
(define dvnh (* brqv jdmt))
|
|
(define cgnv 2)
|
|
(define wttp (- lbgc gnrj))
|
|
(define pcvv (+ rvmp hmrs))
|
|
(define szlh 2)
|
|
(define ztct (/ zscd lhml))
|
|
(define jbqf (* cdvw dnvm))
|
|
(define jgzl (+ drct vwdt))
|
|
(define ztzq (- nqsl vzts))
|
|
(define hvtv (* qznt wzfr))
|
|
(define sfmn (+ wchl cscm))
|
|
(define fpcs 5)
|
|
(define fnqf 2)
|
|
(define bqld (+ zqjp rbzl))
|
|
(define wtwb 2)
|
|
(define hcqw 14)
|
|
(define pmwl (* lwsn lddq))
|
|
(define rwmq (* tdnf jdrg))
|
|
(define vjtf (* lbzc djjd))
|
|
(define ddmr (+ fhzm qvbn))
|
|
(define cdnp (* zvst cwjp))
|
|
(define vtjg (* stcr bvzn))
|
|
(define jjgt (* crqg dmrn))
|
|
(define pcgq (* jtcf qssh))
|
|
(define wpcs (* phbh mnhf))
|
|
(define lncn 1)
|
|
(define jstb 5)
|
|
(define nvlv 17)
|
|
(define tmhg (- vtvn nzbp))
|
|
(define qzpn 2)
|
|
(define smhv (* ffnt gtwp))
|
|
(define zsvh (+ grdf svcp))
|
|
(define dhpp 2)
|
|
(define jvgd (- dvnh mpjj))
|
|
(define qmqt (/ wttp cgnv))
|
|
(define wzdv 3)
|
|
(define wfbp 2)
|
|
(define mnhc (* szlh pcvv))
|
|
(define mwrc 2)
|
|
(define twtq (- jbqf ztct))
|
|
(define ndph (* ztzq jgzl))
|
|
(define zzcv 14)
|
|
(define cllb 3)
|
|
(define sqcb (+ sfmn hvtv))
|
|
(define lwlb 5)
|
|
(define tzls (+ fnqf fpcs))
|
|
(define ztqg (* wtwb bqld))
|
|
(define jcgh (* pmwl hcqw))
|
|
(define wwqp (+ vjtf rwmq))
|
|
(define tjwt 16)
|
|
(define ndlf (+ cdnp ddmr))
|
|
(define bnfp 13)
|
|
(define mqph (+ jjgt vtjg))
|
|
(define bncr (- wpcs pcgq))
|
|
(define slpc (+ jstb lncn))
|
|
(define bfpq (* tmhg nvlv))
|
|
(define fctt (* smhv qzpn))
|
|
(define fwzf 4)
|
|
(define hqjt 7)
|
|
(define dchw 4)
|
|
(define dhqh (* dhpp zsvh))
|
|
(define hjlz (+ qmqt jvgd))
|
|
(define psfr (* wfbp wzdv))
|
|
(define fvsf 2)
|
|
(define pmrt (* mwrc mnhc))
|
|
(define qlnr (+ ndph twtq))
|
|
(define pznf (* cllb zzcv))
|
|
(define jmbs (* lwlb sqcb))
|
|
(define cbjq (- ztqg tzls))
|
|
(define jnqv (+ wwqp jcgh))
|
|
(define jmbp 4)
|
|
(define qrzq 2)
|
|
(define bpjf (+ ndlf tjwt))
|
|
(define mtnb (* mqph bnfp))
|
|
(define jjbm (* slpc bncr))
|
|
(define jvtz (+ fctt bfpq))
|
|
(define gqpj (+ hqjt fwzf))
|
|
(define lvhm (* dhqh dchw))
|
|
(define tnnt (+ psfr hjlz))
|
|
(define pfpt (* pmrt fvsf))
|
|
(define djpm (* pznf qlnr))
|
|
(define mzzd 3)
|
|
(define hcsc 5)
|
|
(define zrnz (* cbjq jmbs))
|
|
(define cnbg (* jmbp jnqv))
|
|
(define jtjd 6)
|
|
(define rcmc (/ bpjf qrzq))
|
|
(define cpdf (* jjbm mtnb))
|
|
(define qvpw (* gqpj jvtz))
|
|
(define mldc 3)
|
|
(define swfp (+ tnnt lvhm))
|
|
(define nhcr 3)
|
|
(define sbpb (* djpm pfpt))
|
|
(define bhgh (* hcsc mzzd))
|
|
(define bhpw (+ cnbg zrnz))
|
|
(define rtsd (+ rcmc jtjd))
|
|
(define qjrs (+ qvpw cpdf))
|
|
(define zpbt (/ swfp mldc))
|
|
(define fhjc (/ sbpb nhcr))
|
|
(define cgvs 7)
|
|
(define gdpg 8)
|
|
(define nwbt (* bhpw bhgh))
|
|
(define hmrz (* qjrs rtsd))
|
|
(define wdwf (- fhjc zpbt))
|
|
(define rzff (+ gdpg cgvs))
|
|
(define fcgj (* hmrz nwbt))
|
|
(define bsbd (* rzff wdwf))
|
|
(define root (+ bsbd fcgj))
|
|
(evaluate humn (solve (assert (eq? bsbd fcgj))))
|