aoc2022/day21/part2.maude
2022-12-21 18:02:33 +01:00

2376 lines
49 KiB
Text

fmod EQN is
protecting NAT + QID .
sorts Eqn Op Term Side .
op _:_ : Side Side -> Eqn [ctor comm prec 40] .
subsorts Nat Qid < Term < Side .
ops _+_ : Term Term -> Side [ctor ditto] .
ops _*_ : Term Term -> Side [ctor ditto] .
op _-_ : Term Term -> Side [ctor prec 33] .
op _/_ : Term Term -> Side [ctor prec 31] .
vars M N : Nat .
eq M / N = M quo N .
ceq M - N = sd(M, N) if M >= N .
endfm
view Eqn from TRIV to EQN is sort Elt to Eqn . endv
fmod SOL is
protecting NAT + QID .
sort Sol .
op _:=_ : Qid Nat -> Sol [ctor prec 40] .
endfm
view Sol from TRIV to SOL is sort Elt to Sol . endv
fmod EQN-SET is protecting SET{Eqn} * (sort Set{Eqn} to Eqns) . endfm
fmod SOL-SET is protecting SET{Sol} * (sort Set{Sol} to Sols) . endfm
fmod STATE is
protecting EQN-SET + SOL-SET .
sort State .
subsort Nat < State .
op _;_ : Eqns Sols -> State [ctor prec 127 format (d d n d)] .
var X : Qid .
var N : Nat .
var Eq : Eqn .
var Eqs : Eqns .
op subst : Eqns Qid Nat -> Eqns .
eq subst(empty, X, N) = empty .
eq subst((Eq, Eqs), X, N) = subst1(Eq, X, N), subst(Eqs, X, N) .
vars E1 E2 : Side .
op subst1 : Eqn Qid Nat -> Eqn .
eq subst1(E1 : E2, X, N) = subst0(E1, X, N) : subst0(E2, X, N) .
var M : Nat .
var Y : Qid .
vars S T : Term .
op subst0 : Side Qid Nat -> Side .
eq subst0(M, X, N) = M .
eq subst0(X, X, N) = N .
eq subst0(Y, X, N) = Y [owise] .
eq subst0(S + T, X, N) = subst0(S, X, N) + subst0(T, X, N) .
eq subst0(S - T, X, N) = subst0(S, X, N) - subst0(T, X, N) .
eq subst0(S * T, X, N) = subst0(S, X, N) * subst0(T, X, N) .
eq subst0(S / T, X, N) = subst0(S, X, N) / subst0(T, X, N) .
endfm
mod REDUCE is
protecting STATE .
vars X Y : Qid .
vars M N : Nat .
var Eqs : Eqns .
var Sols : Sols .
rl [done] : Eqs ; 'humn := N, Sols => N .
rl [subst] : (X : N), Eqs ; Sols => subst(Eqs, X, N) ; Sols, (X := N).
rl [var] : M : X + N => X : M - N .
rl [var] : M : X - N => X : M + N .
rl [var] : M : N - X => X : N - M .
rl [var] : M : X * N => X : M / N .
rl [var] : M : X / N => X : M * N .
rl [var] : M : N / X => X : N / M .
endm
mod PUZZLE is
protecting EQN-SET + REDUCE .
--- put the input here in this format:
--- ① a quote before each name
--- ② space before `:`
--- ③ comma separated
op puzzle : -> Eqns .
eq puzzle = --- {{{
'mmdf : 'ltmz - 'gffq,
'rrsc : 'fqnp + 'dhrs,
'btrn : 10,
'root : 'vtsj + 'tfjf,
'mqjw : 5,
'qplt : 'tpfl * 'vmpn,
'dpsb : 2,
'wbmh : 'mgct + 'ttqh,
'wwwt : 'rwfc * 'bdcj,
'gznp : 'mhdc * 'cnsq,
'qnvr : 'bggv * 'zgmr,
'bmct : 3,
'nwtt : 2,
'jmsd : 3,
'sshh : 'plsq + 'jqlh,
'hpwq : 2,
'gjjm : 13,
'bssn : 'gccb + 'twsr,
'dqpm : 3,
'vhlr : 'cbjg * 'bmbp,
'wzvz : 'gssr * 'swss,
'mmwg : 'hfft * 'plhg,
'hmvt : 'gcpc * 'nfvm,
'jhdb : 2,
'zzns : 2,
'mzmq : 'cqwp * 'qdch,
'cfwz : 3,
'rftm : 2,
'bspj : 'mcsp * 'hjbt,
'fswg : 1,
'lzmd : 'czrb + 'wfsm,
'pmmd : 13,
'rzng : 12,
'fvrj : 'jvpq + 'qtpv,
'wbvd : 'gcbj + 'tgbc,
'qtjt : 'blmq + 'zjlp,
'wptj : 'bfgv + 'qgpd,
'zbzz : 4,
'hgdb : 5,
'frqp : 7,
'nrct : 'qfdv - 'gqvc,
'mfjc : 'plcb + 'chdh,
'tglv : 2,
'tfvb : 'qjzq + 'ffqg,
'ttgt : 5,
'zcwg : 15,
'fnnr : 'fggv + 'bcst,
'lrbf : 5,
'gssr : 'bdcw + 'lrhn,
'fmsh : 3,
'jsjf : 3,
'tgvn : 1,
'fzpp : 'djzm + 'vtcf,
'nmfs : 'tfvd * 'gbdg,
'rqjg : 2,
'jbsr : 'jhrl * 'vzzg,
'mgct : 'zpgt * 'gshd,
'zltc : 5,
'lhpl : 2,
'gpbc : 'mlwp * 'zvgg,
'tzjj : 'ntvq * 'hcsb,
'dcml : 2,
'hbrc : 4,
'qqft : 'qlrl - 'hnsz,
'wzwq : 'msjs * 'fqqc,
'tcrr : 'hqct * 'pnjc,
'vfdd : 3,
'lqfr : 9,
'drzv : 'pmhd * 'dvtm,
'cwtd : 2,
'vqjj : 12,
'mqdc : 3,
'nrrv : 'hgpq * 'jzzz,
'tpcc : 'pgbf + 'sccw,
'qcdm : 'hsjn * 'fmmc,
'rnjh : 1,
'dwff : 17,
'hltf : 'jwst * 'mmtr,
'plhj : 'mvps * 'fnnr,
'vjjj : 'rdcn + 'zjsd,
'nvns : 4,
'qvwr : 'dqsz * 'zsvv,
'twsr : 'rhsw / 'ggww,
'sdcp : 3,
'lsrp : 3,
'gcpc : 'hmdl * 'trqf,
'vfsh : 3,
'thwh : 6,
'qmlz : 2,
'ftbb : 'twsn + 'shgj,
'smfj : 18,
'czrb : 'wpcp * 'zmtl,
'chtz : 2,
'htqd : 'mqcb + 'mftg,
'pmhd : 9,
'hnfj : 'qvwr + 'znqf,
'jdnl : 3,
'hfft : 3,
'fjtj : 2,
'hmbb : 'qwjw / 'bfhq,
'hhlp : 'lhgm + 'bfjd,
'spwt : 'gcvl * 'zshg,
'cjtq : 3,
'thjt : 'fvvv * 'fnjm,
'vmpn : 6,
'grfl : 14,
'tnjl : 6,
'bjnj : 5,
'dqsz : 3,
'czfr : 4,
'whqz : 'zrbm + 'hqfs,
'bbml : 'npqw + 'bsml,
'htsl : 2,
'jhch : 4,
'wmcj : 2,
'ggmh : 10,
'htgz : 11,
'jwnc : 11,
'zqnq : 5,
'btrz : 'tqhq - 'smlb,
'lswh : 8,
'vdgj : 'sbct * 'dnsr,
'trvq : 'vhlq - 'gclz,
'gcqd : 'zcwd * 'nnsw,
'znnd : 'tfhf + 'sczv,
'frdf : 2,
'zjjv : 'bvfm * 'sgwf,
'qmgg : 10,
'jfrc : 17,
'tzlf : 10,
'gjgl : 'ghrf * 'jthm,
'wtwj : 5,
'rwzl : 3,
'rgfp : 2,
'tmcs : 'sgwt - 'nnnj,
'dpjm : 'nqhp + 'rhch,
'cfvn : 8,
'gcvl : 2,
'gffq : 1,
'ftdf : 'lhmc + 'dvzc,
'vbdr : 6,
'lqpd : 3,
'cppp : 4,
'sjnh : 'zhvw * 'gnhj,
'fsjc : 'jbsr + 'qmhj,
'tvbw : 1,
'sqwr : 'szrr * 'npzw,
'bmbp : 2,
'wwmg : 'hqzb / 'hzhc,
'ttqh : 5,
'hgcb : 'lmcc * 'sdcp,
'hhcn : 'twwd + 'nrnw,
'wnds : 'lvlb + 'qpgs,
'fwmt : 2,
'lvtz : 'wgwl * 'swvg,
'gsrh : 14,
'bqdz : 'rprf + 'wgmn,
'zfrl : 3,
'djpf : 9,
'mwrg : 'pndf * 'ghrg,
'njnc : 'fmcv * 'lfzn,
'sswz : 'trgb * 'tntl,
'qwls : 5,
'gjcd : 'sshh + 'wtgw,
'qpgj : 'vmms * 'qrrm,
'vmjb : 'pfqq + 'ctfp,
'gbdg : 2,
'gqrb : 'dltm * 'ljsv,
'zcwd : 4,
'grpv : 2,
'nrlp : 'rflp * 'njsf,
'qjpz : 7,
'rcmh : 2,
'lstf : 2,
'ffqc : 'rrnm * 'vmzz,
'vhgr : 'ftfs + 'gqlb,
'wzhw : 4,
'zsnf : 'jqlb * 'zgpc,
'drhd : 'ntmt * 'tbpg,
'shvg : 'wrrg * 'rpbj,
'gmzc : 2,
'hbnf : 5,
'dqrq : 4,
'ffhr : 2,
'dmff : 'grcn / 'lbts,
'vvht : 3,
'bnfw : 'cfwz * 'mdst,
'dzqd : 'fqnw + 'bdcq,
'bwvt : 'vwbv + 'szdv,
'ghtf : 2,
'fzbz : 'rmqf - 'dqrt,
'bmzp : 3,
'cfgb : 'zdjc * 'pdjc,
'hzvq : 'nhnb * 'fsgp,
'rqfp : 'lwbv + 'pqwf,
'qzrl : 'smcl * 'fcsz,
'gcdl : 4,
'zlmv : 5,
'ttrp : 6,
'msgf : 'bpgr - 'vjmr,
'jnmv : 7,
'fpsh : 6,
'jmfv : 3,
'ppss : 1,
'trmc : 13,
'rwjf : 2,
'bjbc : 'rfzc * 'mrjb,
'zpnd : 5,
'pvvg : 2,
'brbf : 14,
'nvpd : 3,
'hqfs : 2,
'cwfv : 'vttc * 'wlbf,
'nwjp : 'bnhq + 'ztqh,
'djwq : 'ljgp * 'mhhs,
'mdst : 4,
'fqrn : 'ghjs + 'rpzb,
'vtsj : 'pzgz * 'stbs,
'nwrw : 'vtht * 'zbpb,
'zfwz : 4,
'bqgh : 'nnbc * 'wvlt,
'jzlc : 'vmct + 'dbrl,
'plhg : 3,
'qmst : 19,
'jjrb : 2,
'mjwp : 4,
'rnzg : 1,
'prft : 4,
'ljwm : 'bwvt * 'mvvj,
'vggf : 'ppss + 'thrl,
'rczr : 4,
'vwhw : 'sscm * 'jhvv,
'lpft : 'rnlb + 'fmdj,
'dqld : 'zghf + 'ddsc,
'blnr : 'zqdl + 'sjdh,
'pcwl : 3,
'ddss : 'hzrj + 'zbrm,
'rqjs : 3,
'bvgj : 16,
'wjtb : 'wpcg + 'tqvp,
'lpcp : 3,
'tcfd : 2,
'srzv : 'cjhr * 'zfwz,
'rflp : 4,
'qqwl : 3,
'szrp : 7,
'sdng : 2,
'mvvc : 'hlzf + 'qdjf,
'hsnl : 10,
'vwld : 11,
'zldw : 20,
'gwnt : 4,
'cqtt : 11,
'fpzj : 'pqhq + 'rnzg,
'zlvj : 'cmjm * 'bmct,
'zwsl : 2,
'jjtj : 2,
'hctd : 'wwct / 'ltmc,
'tzth : 'fmcs + 'jdnl,
'tvtw : 1,
'nwrq : 12,
'sqhm : 2,
'zmtl : 4,
'pqhq : 6,
'vcmv : 'lqnz / 'vmtt,
'hsqr : 'cmmm + 'grsm,
'hgfp : 'ztng * 'hcln,
'bhzz : 2,
'qbvr : 6,
'hcqd : 'hqjd + 'fztg,
'mwdq : 2,
'mpzt : 'wpqg + 'ctwd,
'bvgp : 'fpzj + 'szfw,
'nwrh : 4,
'wwbm : 'lqtf - 'mbfc,
'mbbg : 'tmfm / 'cnwh,
'sgfc : 'gspv * 'tjnn,
'cjjm : 'qzqn * 'vjfd,
'ffnr : 2,
'vwqj : 'zzng * 'mtqr,
'tljd : 'wjfb * 'tzbd,
'gjhs : 'tldh * 'frdf,
'mjsm : 'qsnd * 'phsj,
'dqpw : 14,
'pwnq : 'dhls + 'wbsq,
'pqwf : 1,
'dnsr : 2,
'bqlp : 'vfzr * 'czfm,
'csnz : 'gcdl + 'bswp,
'pnfn : 'jwrm * 'tzlf,
'tptw : 'jgjr + 'fvsj,
'rmcc : 'vdgj + 'jrrt,
'jdjq : 1,
'qnlm : 'gmdh * 'szfl,
'cjvp : 1,
'sncz : 'phzg * 'bdrl,
'lvmg : 'vjjj * 'qnct,
'vmgj : 'cddd / 'mwtg,
'glrl : 'cmfg * 'mdmp,
'pdcb : 'dtjv + 'qtgr,
'vjcq : 2,
'dclv : 'jtvh / 'vspb,
'qprb : 3,
'wfrd : 'ffhr * 'bhnc,
'fwgz : 'fcmq - 'gbrh,
'mjhg : 3,
'jfgf : 5,
'clcb : 4,
'tpfl : 11,
'jdjj : 'fbvn + 'fdlp,
'lmgh : 3,
'jrjv : 'hpjl * 'jjtj,
'mnzg : 'pvwc * 'wdtq,
'pppv : 2,
'mhmr : 'vhfw * 'lqpd,
'tfwh : 'tspq + 'tthb,
'gvvc : 'svvg + 'njbd,
'nlsl : 16,
'lcwt : 'jhgg * 'prdq,
'wpqg : 'dmpq * 'mntd,
'wbzz : 'smpq / 'mjwp,
'rzhb : 2,
'gqnz : 2,
'bpmm : 5,
'rhch : 'bjff * 'bvsc,
'hpsh : 3,
'zsvw : 14,
'tpdd : 3,
'zpgf : 2,
'zbjj : 'hrrr * 'npnw,
'zcdl : 5,
'djpd : 'vmpz - 'ddbg,
'mfzd : 2,
'pcdv : 'jmpp * 'dzwl,
'wvhc : 'ddvd + 'vwhw,
'gfbv : 'ddvs - 'tptw,
'zrcv : 'mbbg * 'gccc,
'fzdd : 2,
'ztng : 2,
'twsp : 'znjz * 'jsnt,
'wjwh : 'njnc * 'mrpn,
'mqwc : 'vbrt * 'dbbg,
'shjl : 4,
'gbrh : 3,
'wtdg : 'hdpp / 'mlpr,
'gtrb : 'cgmm + 'tdhr,
'ljgp : 'hncw - 'mjwm,
'hmdl : 3,
'qsvs : 3,
'bpgr : 'jfrc * 'dqpm,
'nblh : 'nfmp * 'zlmv,
'bvcn : 'lvsc * 'jtzc,
'nqvs : 'jbns * 'lfjv,
'zcrp : 16,
'rrwv : 'dhsc * 'tfvb,
'ljsv : 'jrjv + 'dhfl,
'smqp : 'grtq * 'dnsz,
'jvcj : 'cqps * 'ltgw,
'gqlv : 4,
'wsgw : 'wtdg * 'fgwd,
'pbbg : 13,
'qgtc : 'vzwf + 'vwqj,
'lvqt : 'dgpr * 'dqrq,
'rwmh : 'cbsc + 'rcnr,
'vmvq : 'bwml + 'mnrs,
'cjwz : 'rczl + 'wjwh,
'pjrv : 14,
'fhrn : 2,
'qdjf : 'gcgw * 'djbd,
'pzqb : 'ffqp * 'qwlw,
'plch : 2,
'vhvm : 4,
'lqnz : 'dhhs * 'jjhn,
'twnd : 'wztf - 'hzmr,
'dpvj : 9,
'mpfv : 'pshn - 'cfgb,
'svvg : 3,
'szdv : 5,
'wvrl : 5,
'mhhc : 'vvsw * 'jwzw,
'dfcj : 3,
'lnsn : 3,
'fmmc : 2,
'smlb : 'bfvn + 'mszc,
'pgcr : 'zzdb * 'hssn,
'fbvn : 'htdn + 'hgbg,
'hnvn : 'zpnd * 'bpqh,
'mffz : 3,
'trpg : 'bwlt - 'czhw,
'vqmd : 3,
'qdtd : 9,
'gwbs : 'mhmr * 'qcjv,
'njsf : 2,
'qscr : 'fvgf + 'wssc,
'spdg : 11,
'qdhp : 'gcqr * 'bssn,
'lhdn : 1,
'mgjv : 'lbsz * 'frmc,
'bhts : 'sdng * 'cgrp,
'mvdm : 17,
'jhtl : 9,
'djzt : 4,
'wwqd : 3,
'wgmn : 'spcl * 'vwld,
'fqlj : 2,
'lvdg : 'rrwv / 'zdgg,
'dgpl : 'qtps * 'cgsw,
'vgtj : 3,
'rtdf : 'fzbj * 'rwwg,
'cwcc : 4,
'zwlj : 8,
'nqhp : 'jcjh + 'bjbm,
'psfs : 10,
'bnct : 'rzcl / 'qsvs,
'wngr : 2,
'vgfl : 'dldw * 'tbpp,
'rnfs : 5,
'bfvz : 2,
'pnbj : 'tdfw * 'cfvn,
'cfng : 2,
'gvqp : 2,
'hglm : 5,
'mcsp : 'jnmz * 'hjns,
'hnlp : 'mqdc * 'mmqz,
'mrpq : 'thgq * 'qvnn,
'tmfm : 'ffzp * 'zwmp,
'jgvh : 4,
'ddsc : 19,
'hlzf : 'cjwz / 'dqnl,
'nspt : 7,
'pnjc : 7,
'pzbl : 3,
'hwjd : 2,
'spbg : 2,
'dvpq : 5,
'nnlr : 6,
'sfjj : 4,
'hjbt : 'tsth * 'vhtr,
'ltvl : 'tjrn + 'bfvz,
'djvd : 'fvrj + 'bpmp,
'tdfw : 'ftdf + 'qlrc,
'qhth : 'jlnt - 'zpzs,
'zrbm : 9,
'bpsf : 'cfvp * 'cbzp,
'nltn : 6,
'bdpz : 1,
'smss : 5,
'cfdh : 'gvvb * 'flcr,
'cqps : 3,
'hncg : 5,
'ffnb : 'qprb + 'clcb,
'vjsn : 'mhvb * 'pfsb,
'wtnp : 4,
'tsvd : 'gfbv * 'zlzg,
'zrwc : 'zfwt + 'rzng,
'vbvb : 3,
'mszc : 'pqdn + 'qgfw,
'mwqz : 'qhhz + 'fwlg,
'ddbg : 'mwmz + 'hplc,
'jtvh : 'vbpr * 'vdqr,
'tfll : 'cmjr * 'rjzn,
'gbmw : 'rhdr - 'bjbc,
'frfg : 'mgrb * 'plch,
'nqgv : 9,
'qmqm : 'cmzh * 'gbff,
'jvzj : 1,
'plsr : 'dpvj * 'hsbz,
'gqvj : 'sjwg + 'gwnt,
'rpbj : 2,
'hgvz : 15,
'shgj : 'cnlp - 'vbpv,
'szfl : 5,
'fnrz : 'ggmh + 'dwjw,
'dmhw : 11,
'nmrm : 'rdjm + 'llnn,
'zfwt : 'fzdg / 'qjvh,
'fsld : 13,
'fwlg : 'plzb + 'bstd,
'vtjj : 4,
'tmbl : 'qczb * 'cwdv,
'zsdb : 'znnd * 'qqht,
'lfsp : 'rlst + 'mjvw,
'bmqd : 'nrct * 'mwqb,
'cthr : 7,
'vcvf : 'hqst * 'mbtd,
'ghjs : 16,
'zshg : 'qggh + 'hgfp,
'dnhb : 5,
'pvfl : 'gmjq / 'jwfb,
'ncqs : 3,
'vcnt : 17,
'zvgg : 'btrn + 'pvnd,
'gwsv : 1,
'qhhz : 2,
'bpnd : 'jqtf + 'zglf,
'rpzb : 'wpsf * 'pchr,
'vlcd : 19,
'hqsh : 6,
'ccgn : 'hbrc + 'rdwf,
'rlgm : 'fsqw * 'tcrr,
'rrjs : 3,
'jlbg : 4,
'ghlt : 'jfcf * 'gvqp,
'mtsq : 4,
'bbhr : 'dzhn * 'wshv,
'jsnt : 'nhwp + 'vjcq,
'fmgj : 11,
'fgdc : 2,
'phsj : 3,
'lqds : 2,
'jmpp : 2,
'mtst : 2,
'mhhs : 'jbwj - 'zltc,
'hqgl : 'tbjl * 'zgft,
'dgft : 'jfqh + 'qhdw,
'qslr : 'ztcw - 'dprz,
'pntq : 'pzmt - 'dwmh,
'cmsr : 'fmmg + 'sswz,
'vlrh : 'tmtq * 'fjtj,
'lnrl : 'dpgh + 'mvdc,
'srgw : 1,
'dcnz : 3,
'qhdw : 'dgzv * 'sctc,
'vfpw : 12,
'lbnd : 'cqdv + 'gwwg,
'phwp : 'ngvc * 'mplv,
'rwfc : 'bgvs + 'tlmr,
'zczh : 'qblp + 'prft,
'chdh : 2,
'hnvh : 2,
'ngvc : 'vpph + 'fwjw,
'gwvd : 'nndv / 'rzhs,
'mrjb : 4,
'pnds : 3,
'qrqg : 2,
'vsts : 'lpft * 'lstf,
'rtrz : 1,
'tjrn : 9,
'sczv : 4,
'bsrg : 14,
'rsdc : 'plsr + 'hmbb,
'mgzz : 2,
'mwmd : 8,
'lqhw : 'ntzn * 'qsbd,
'chqc : 2,
'qgvq : 5,
'vqjq : 'hsrc * 'mwdb,
'sbct : 6,
'gsqj : 1,
'fqmw : 4,
'vqlh : 'ncqw + 'vmjb,
'jmrl : 'jpsn + 'gtph,
'hdsb : 1,
'ztqh : 'sjjd * 'gmcj,
'mbpc : 'vqmd + 'pvqp,
'hgbg : 'fnhr + 'pmzv,
'wljp : 2,
'pfjl : 3,
'dnpj : 2,
'dprt : 5,
'gbjv : 2,
'hvrl : 'pvvg * 'hdzh,
'ddvd : 'fwgz + 'cpzp,
'dbjv : 'gwvd + 'fdqb,
'bhcm : 'cbdm * 'vbfb,
'trgb : 11,
'dfvc : 'gwcn * 'hrrb,
'jzzz : 14,
'nsgz : 2,
'nrnw : 'mwmd * 'hnvn,
'tjbp : 'psln + 'zqgr,
'rzpr : 'hcjw * 'mrbs,
'vfcp : 5,
'trth : 1,
'zdtg : 'jjps + 'lvtz,
'wbfw : 3,
'jcjh : 'vtzc * 'mstb,
'dqrt : 5,
'ddhp : 'ldqh + 'pzqb,
'qzqn : 2,
'rtgt : 6,
'nlhz : 10,
'gwhb : 5,
'hpzj : 3,
'jqgz : 7,
'lzft : 3,
'mvmj : 7,
'gpnq : 2,
'zdvl : 20,
'lztm : 2,
'wsps : 3,
'ncdg : 19,
'fpwl : 2,
'vsqh : 18,
'ssbd : 'pqgh * 'jhfd,
'bdrl : 2,
'gzht : 'gqlv * 'cqtt,
'ztsq : 'lmgz * 'ftns,
'hbng : 'nmsf + 'lnfw,
'fnhr : 'hqbm - 'fpld,
'ctwd : 'gqrb / 'gpsq,
'bcst : 'glhs * 'gzng,
'dfdf : 'tvww * 'gwbm,
'cmfl : 2,
'rplw : 'qrqg * 'mvmj,
'jjps : 'npmq * 'cwhb,
'qgpd : 12,
'rcnr : 11,
'cfss : 2,
'fhwt : 2,
'fjgf : 2,
'zpgt : 4,
'rsst : 2,
'rrnm : 2,
'hhhb : 'ptbz + 'msqt,
'qqwf : 'lsss * 'jhtl,
'njpm : 'dbdq / 'jjtf,
'dvzc : 'blmn * 'drrp,
'rdrf : 'tsln * 'tnnl,
'ntvq : 'vnqg * 'zvvg,
'npzw : 'hgcb - 'pqjh,
'cmmm : 2,
'cbpf : 3,
'lhfr : 4,
'dmvl : 13,
'grcn : 'vcvf * 'cthr,
'zdpz : 'hmvt * 'fqrn,
'sttj : 1,
'jqlh : 5,
'ngcw : 2,
'zdjc : 'crfc + 'bvqt,
'hzhc : 2,
'wwjt : 1,
'mdrh : 'smqp + 'swjh,
'rjnf : 'zqrl - 'fnwg,
'mcwl : 'btfd * 'hvqm,
'fnhw : 2,
'fbwn : 2,
'vmtf : 'fdth * 'mmwg,
'jpnr : 2,
'mvrq : 2,
'tvdh : 2,
'hplc : 'wwqd * 'jrjj,
'hzmt : 'srzv + 'hhcn,
'fqrv : 'lgtr + 'rgmq,
'vjgf : 5,
'qlwt : 'trdn + 'csgg,
'fncb : 'bnct - 'bffj,
'bwwz : 'mwwp * 'jrsg,
'ddhq : 3,
'gmjq : 'rwzg + 'cmzb,
'prhl : 'vtmf * 'bmph,
'nslt : 'hgbp + 'hghn,
'brgb : 'srdb * 'wgjf,
'prcg : 8,
'ppqd : 1,
'vnqg : 4,
'mshw : 'vptd * 'pntq,
'vsgs : 'wnjf * 'lsqz,
'rnng : 2,
'pfvp : 4,
'tsth : 2,
'tcbl : 2,
'mftg : 6,
'blmq : 'gtpr * 'vcnt,
'gzwz : 4,
'fjtl : 'jpnr * 'pwdp,
'qqrq : 3,
'zbrm : 'rlsh * 'lgpq,
'pvnd : 'dcmz * 'rvrb,
'nbvr : 4,
'nhnb : 2,
'mhpm : 'flgs * 'tswc,
'http : 'zvhf - 'dwff,
'fcmq : 'jbrr * 'mhnh,
'lnhm : 'ntft + 'mzrw,
'rqzn : 'lrqz * 'vvqp,
'drsf : 2,
'fglm : 'qgpl + 'qclh,
'vcgp : 'gjjm * 'jhtm,
'dfww : 'qrsv + 'fhll,
'fmcs : 4,
'vctl : 7,
'dldw : 2,
'bsml : 6,
'hwss : 'bpmm + 'hpwq,
'ccfj : 'qjnv * 'mjtf,
'bjff : 'nmcg * 'cdcw,
'qnnc : 'nmfs + 'fdct,
'qwjw : 'jdjj * 'dpsb,
'gcgw : 'jhdb * 'hvpw,
'vtzb : 'fnhw * 'nwnp,
'nnhs : 4,
'fncs : 'lnvf / 'hbpf,
'mdln : 8,
'tfmq : 4,
'pzgz : 'ggzv * 'nmgc,
'jmfz : 'fpnw + 'dswd,
'hrrr : 'hsfl + 'gwhr,
'rbps : 2,
'rzjl : 5,
'grln : 'rpbs + 'hchs,
'gbzz : 'vsrp + 'mnlv,
'fblm : 'twtq + 'rvzz,
'wpjj : 5,
'qgpl : 'htrm * 'dzql,
'gpqf : 6,
'gcbj : 1,
'szrr : 4,
'vqzb : 6,
'clqz : 11,
'hflf : 2,
'nwbr : 'bsrt + 'csgq,
'plwq : 2,
'qpsh : 2,
'nsrj : 5,
'hqpd : 2,
'mwsh : 'jhgq * 'fbwn,
'pcpw : 4,
'dmgn : 3,
'srdb : 'ddhq * 'pntj,
'cjhr : 'lbmp * 'nbvr,
'lvlb : 9,
'bhtd : 'dqqf - 'hdsb,
'ljpq : 'qlwt + 'hclw,
'gvmf : 'lsdh + 'wfgh,
'rjmh : 'nspt * 'gjcd,
'cfdv : 'qvbz * 'nzwn,
'hnlm : 'zdpz - 'gtnl,
'jbsc : 'nnhs + 'nmhs,
'fwjw : 1,
'zvgw : 'mffr * 'wwhr,
'dqnl : 2,
'mmqz : 'qrvh * 'gbtw,
'qqrd : 'lfzd / 'wscd,
'jcgl : 'jpmw + 'nfch,
'ntzn : 5,
'vpsr : 5,
'pdsf : 5,
'jzcz : 2,
'qgft : 5,
'mjtf : 9,
'plsq : 2,
'zctw : 'pvfw + 'tfwh,
'bfhw : 'bhqt + 'mtfj,
'prlw : 9,
'bdsv : 2,
'pfmz : 3,
'vjmr : 'zcdl * 'nrcz,
'ccjt : 2,
'gsgw : 2,
'fpld : 8,
'hdjj : 'nzhv + 'nslt,
'nhwp : 'whgv - 'pfmz,
'cwhz : 'trth + 'chwr,
'qjnv : 3,
'bmfn : 2,
'zlzg : 2,
'cghl : 2,
'nttw : 'nrlp + 'pwhw,
'qchg : 17,
'dhhs : 'crnb + 'cfmj,
'btjh : 17,
'mwdb : 5,
'fmsg : 'rwzl * 'mbdg,
'ghbj : 9,
'wswg : 1,
'rjmr : 'qmtl * 'rwmv,
'vrmq : 'tvct + 'zzsc,
'hsjn : 'dtjg + 'cwsf,
'wqwp : 'stsp * 'fmgj,
'gcnq : 3,
'cfvr : 'qgpr * 'dsdz,
'bzqz : 'rpmz - 'phvj,
'jlnt : 'wdnp + 'bvpm,
'qnwn : 'jcsh + 'nwjp,
'vltf : 5,
'rjsz : 17,
'blcz : 'wmhg * 'brgv,
'trsf : 'cfvr * 'lnsn,
'tspv : 'bvgj - 'gnvl,
'pmsw : 2,
'mwdw : 'spbg * 'tmpj,
'wtgw : 'ffnb * 'zvtp,
'hwcn : 2,
'vvdd : 2,
'tlmr : 'wvch / 'dprt,
'mctg : 10,
'hghn : 6,
'rvbr : 'cghl * 'zctw,
'vptd : 4,
'tmmg : 'jszq - 'ftbb,
'tvlj : 2,
'nfmp : 4,
'mjwm : 'rrvs / 'jtpv,
'hgjg : 'zcbl / 'qnlz,
'jfqh : 'zfrl + 'zfsj,
'dgzv : 2,
'hchs : 2,
'chcj : 4,
'sfhw : 'vqds + 'phns,
'wwtf : 'bprp + 'sdpv,
'lvhz : 2,
'gcmm : 1,
'cbqj : 'bpqf + 'cwqr,
'dwcw : 'jjzs + 'jlnn,
'fqwc : 8,
'rzrg : 'drhd * 'lnfh,
'qhgh : 'sgrm * 'lmgh,
'tswc : 3,
'phgh : 'pjgw + 'mwrg,
'jzvp : 'tqdp + 'svhb,
'zcbl : 'bvmz - 'qcdm,
'nfwj : 'czfr * 'pztb,
'vjwh : 'tqnz * 'lpmz,
'qlzf : 4,
'tbcq : 'bhzw * 'tnjl,
'bvsc : 2,
'fmrz : 'hfmn + 'bcsq,
'qdpw : 19,
'zqmh : 'tqsp + 'gwgs,
'fwwp : 'lfsp * 'nwtt,
'lvqc : 2,
'srqg : 5,
'nznd : 'sqrm * 'dnff,
'sscs : 'drvg * 'ljwn,
'lcwb : 6,
'qzww : 'mgzz * 'glrm,
'dnzm : 'zrcv * 'zjgf,
'zbdv : 2,
'nggm : 'qqft * 'jzvp,
'rrcq : 12,
'ggww : 3,
'bqfn : 'wngr * 'csnz,
'zglh : 10,
'vbgd : 5,
'rqvt : 2,
'jcps : 15,
'crnb : 8,
'hvhf : 'lcww / 'mwdq,
'cbzp : 5,
'jsdn : 3,
'tsnb : 5,
'cwhb : 19,
'fbvm : 'frfg * 'mqjw,
'qdlc : 4,
'jwbt : 3,
'phgc : 'jtzv * 'rrsc,
'lqld : 2,
'lvcv : 'snlt + 'humn,
'pwhw : 'wdvc + 'jhch,
'rwmv : 'mbdn * 'rqll,
'bstd : 'prhl + 'phpm,
'rjnw : 2,
'cbdm : 9,
'wrtf : 10,
'vdrh : 'vjgr / 'ccss,
'vpzw : 2,
'hbpf : 2,
'nbcn : 'lgdl * 'sscs,
'nfvm : 'swbc * 'ffrv,
'nwwn : 'dmhw * 'lqds,
'tftz : 'qfrh * 'wnpn,
'ncqw : 'mhpm * 'rcvm,
'vtcf : 'tpjg * 'ddhp,
'wnwz : 5,
'bfjd : 'jhlv * 'mhlj,
'jglg : 'hlvc * 'cfss,
'jlnn : 4,
'vllm : 2,
'ltgw : 2,
'trqf : 2,
'gsrr : 'btrz * 'bzdz,
'dqvg : 5,
'bhqt : 14,
'hdcb : 20,
'wvch : 'dbjv * 'tlsf,
'zqrl : 'vbfd / 'zhcr,
'rmjh : 3,
'gwcn : 2,
'hqbm : 'qsms * 'hffl,
'vpnw : 'jdjq + 'hdcb,
'pvbl : 'wbfw * 'chqc,
'rzpg : 4,
'spcw : 'qnww + 'cddm,
'hlbj : 'jnwz / 'mdmc,
'pcvn : 'tjjg * 'msbl,
'frvm : 15,
'mfdd : 2,
'jdpv : 3,
'mgfl : 2,
'hwjn : 3,
'npnp : 'qgft * 'tlwt,
'hmfv : 'ghlt / 'tzsn,
'tbjl : 3,
'ffhq : 4,
'ngqf : 'gsmz / 'ffhq,
'cnsq : 'mqpl + 'trfv,
'mzml : 7,
'chwr : 8,
'bqgt : 'hwjj - 'zsdb,
'bpqh : 3,
'sdzj : 'jvfq + 'grmf,
'ncrq : 'blrm + 'hpzj,
'tbpg : 19,
'vjrs : 3,
'zsbm : 'zqqm * 'mttr,
'lmcc : 'wzsj + 'bzrp,
'qfdv : 10,
'jjrj : 19,
'plqd : 9,
'bfmg : 'rqfp + 'stdh,
'fsfb : 3,
'jsvh : 17,
'nwpw : 'mngl + 'zhmn,
'svzr : 2,
'gqlr : 'bpww / 'svbt,
'wrzj : 'wzvz * 'rmhf,
'jqlb : 4,
'jjzl : 3,
'wvlt : 5,
'fggv : 'tlzs * 'rzjl,
'mbdn : 'lrbf + 'sfzw,
'gvgj : 'nwwq - 'vbsb,
'qfqf : 3,
'fmcv : 'sqcs * 'cnqb,
'hdrl : 3,
'bgvs : 'zldw + 'ffqc,
'lpvm : 'bjsn * 'qvvm,
'tqnz : 7,
'dmfc : 3,
'jnmz : 10,
'dqvs : 'jqhj * 'mpfj,
'lmrp : 'lvqc * 'gsrh,
'zvhf : 'hvrl * 'tqrn,
'lnvf : 'dfdf - 'bhcm,
'gmcj : 'cftm - 'fvfl,
'vmrv : 2,
'llpw : 'hfjt * 'qnhl,
'zqqm : 13,
'hgbp : 8,
'dsdz : 4,
'wcbz : 3,
'vnbl : 5,
'pqjh : 2,
'vwvf : 'gzwz * 'chln,
'fvfl : 5,
'gcvg : 3,
'gfld : 'vpsr + 'zsnf,
'hwwm : 3,
'jpsn : 'sqfv * 'vbcq,
'nlhq : 6,
'dcff : 2,
'bprp : 'pclm + 'lprb,
'cfvp : 4,
'gdqs : 'dqvs + 'tgqs,
'dpmq : 2,
'fzbj : 'qnvr / 'vbgd,
'ghtc : 3,
'wpbd : 5,
'cgqt : 'qvrb + 'lqfr,
'bfgv : 'rjnw + 'hsjt,
'bcgj : 3,
'tgfm : 'bntg * 'cvrj,
'bpcq : 'vtdm * 'czdd,
'htrm : 6,
'qrsv : 3,
'cmfg : 'shvg / 'cfng,
'ntmt : 2,
'zvpz : 'ppwn + 'frqp,
'rlph : 14,
'ghvr : 'drsj + 'gcsc,
'dgvb : 'spcw - 'dmtz,
'grmf : 3,
'ghrf : 'sttj + 'vmrb,
'ftns : 'fbvm + 'qqwf,
'gccc : 2,
'hqjd : 14,
'bfvn : 'nsgz * 'dqld,
'mffr : 5,
'njbd : 'tpdd * 'vtjj,
'hsdw : 4,
'snwt : 5,
'pdjc : 5,
'rfzc : 7,
'mlnr : 'fsjc * 'zbzz,
'mqhr : 11,
'rgfd : 'jcnl * 'llvh,
'snpf : 6,
'wmcc : 3,
'gpsq : 2,
'dbdq : 'bzgl - 'blcz,
'mbdg : 'nmpg * 'qqcj,
'bmph : 2,
'snlt : 'wfpt * 'gdqs,
'hqct : 3,
'pztb : 'pgnm * 'tvlj,
'vbpr : 'mcqz * 'wvhc,
'ccss : 2,
'mpdc : 'mbwp + 'tzfb,
'zqrp : 'sfvb + 'vgfl,
'zgjm : 7,
'hvqm : 5,
'glrm : 'cdfr - 'dgfs,
'ghmg : 2,
'ztcw : 'wmcj * 'hnct,
'rchh : 3,
'bgnl : 'bqtp + 'htqn,
'rqmw : 'vghj + 'pmsw,
'clzh : 'rnng + 'qqgq,
'mrlh : 'vrlw * 'tjzz,
'dlgc : 'npmv - 'spwt,
'nrqp : 6,
'jwrm : 'pdzv * 'lcgr,
'sscm : 9,
'csgq : 'ldcc * 'vbvb,
'hpth : 5,
'wcnv : 'ttrp * 'szrn,
'svhb : 'rwwb + 'bfrn,
'dcbz : 2,
'czrw : 2,
'pfrg : 2,
'msjs : 'tmcv * 'swpl,
'dqmd : 3,
'rnlb : 'fwbq + 'gtrb,
'sgrm : 'tsjs + 'pzhv,
'smgn : 6,
'tcjz : 4,
'brvz : 'slqh * 'swct,
'zjqp : 'qbvr * 'ctjh,
'lbts : 2,
'gnhj : 2,
'jhgq : 10,
'hclw : 5,
'rdcn : 'snhv * 'fnrz,
'hbmn : 8,
'fzdg : 'zwsl * 'vlcd,
'tgqs : 9,
'zggz : 'vpnm + 'vbtz,
'sfvb : 4,
'hdtv : 10,
'hnct : 'fwwp + 'hlcv,
'vmhm : 'dfww * 'gclj,
'nwnp : 'cvzq + 'jvzj,
'fdth : 'pcvn + 'fzfj,
'hrrb : 'mwqz + 'lnrl,
'stsp : 2,
'snhv : 4,
'ghlz : 7,
'vbrt : 'cnqt - 'hcgw,
'tqdp : 1,
'nzhv : 'zsvw + 'gjss,
'trrb : 2,
'dgcw : 5,
'hwjj : 'dsss * 'jsdc,
'lpcd : 9,
'hzrj : 'zsbm / 'jbdf,
'nvvn : 'spdg + 'shsp,
'zgsm : 'trpg * 'nztv,
'dhrs : 6,
'tvww : 'zhph - 'mrbn,
'bwtb : 'vgll + 'ssjd,
'rdzt : 'fblm + 'tjwb,
'cqzn : 'nnvg * 'pzvh,
'zsdp : 'wsjv * 'trrb,
'vrpp : 'ptdv * 'gqnz,
'bqtp : 'pcdv * 'hvmr,
'jrrp : 2,
'scfm : 'fzbz * 'dhwt,
'dtqz : 'jrbd * 'rtfn,
'vtwp : 'gtsh * 'vdhg,
'jgcs : 'tjrv * 'phwp,
'mbcl : 2,
'tpdb : 8,
'sfcl : 4,
'cgsw : 2,
'qnhl : 2,
'qbqr : 1,
'vbjz : 11,
'vjjr : 'pnsp + 'qtbv,
'tgzb : 'dfcs * 'rczr,
'dldb : 'pdsf + 'vsgs,
'hcjw : 'bhhl * 'wrjc,
'jftv : 2,
'cdfr : 'qscr * 'msjz,
'jccs : 'psrf * 'fpqb,
'mvhw : 'njvs + 'qhwq,
'ptbz : 4,
'bpmp : 'zvhr * 'sqwr,
'cgrp : 'rmqt + 'dtwc,
'tzsn : 2,
'vhlq : 8,
'lwtd : 2,
'pzms : 4,
'cddm : 2,
'gsmz : 'hglb + 'bhnt,
'thdr : 'mqhr * 'bgnl,
'wpcg : 20,
'nmgc : 2,
'ftfs : 'fncb / 'blph,
'hcsb : 2,
'djzm : 'rwjf * 'ptnl,
'zbpb : 2,
'tdlr : 'vjpr + 'rlgm,
'qrzr : 'qljn + 'tfmq,
'nqsp : 1,
'vqds : 'lztm + 'prlw,
'dflv : 'tvbw + 'zlqg,
'hcgw : 'zmsn * 'dqmd,
'tjwb : 'jwnc * 'qmqm,
'spjj : 'hhln * 'vfcp,
'tbfl : 'zzns * 'bvll,
'mzrw : 'cpgw * 'dbns,
'qtpv : 'plhj + 'pnbj,
'njhp : 'spjj * 'vqwg,
'fztg : 'rwcn + 'rlph,
'mjcq : 'qtjt / 'llng,
'lqtf : 'bscq * 'vwsz,
'zdgg : 2,
'jlfd : 'vtwp + 'gcqd,
'nlnw : 3,
'gdbp : 6,
'jzjz : 2,
'dvtm : 'dldb + 'zbtg,
'bqrl : 2,
'pdrw : 'mjcq + 'nnrf,
'dnqc : 'lzft * 'dlgt,
'wvms : 'mcfs * 'mdhp,
'twtq : 'hgvz * 'tqtz,
'nbhz : 2,
'jtzq : 3,
'lpmz : 4,
'qnsd : 6,
'vqwg : 'tlzj + 'vmtf,
'lgjc : 3,
'bpgb : 8,
'qrrm : 5,
'pjqd : 2,
'zqcj : 'gmrd + 'njhp,
'tfvd : 'hncg + 'vjgf,
'dvhr : 'tbdd * 'fjtl,
'gcsb : 'sfdq + 'rtdf,
'nnqv : 6,
'rzpt : 6,
'frmc : 'tlrl + 'zcdt,
'mrcl : 9,
'tfvl : 'vjlq * 'ftzp,
'lprj : 3,
'dvss : 'gsqj + 'vqzb,
'shsp : 12,
'tzdq : 'lffs + 'qvgh,
'gdnz : 13,
'vzwc : 'jwhh * 'http,
'gshd : 2,
'dgpr : 6,
'fpqb : 5,
'hfgg : 1,
'qqrt : 'mdln + 'zsfp,
'mjvw : 'wcch * 'mfjh,
'wdtq : 16,
'lntf : 'bhtd * 'dmvl,
'fdtl : 2,
'nbnm : 3,
'qclh : 'zbcv / 'ngcw,
'jvpq : 'lrwm * 'dpjm,
'vsqw : 'tvdh * 'wzhw,
'bdcq : 'hdrl * 'fwhd,
'qlpp : 'sssm * 'zldn,
'fmwg : 3,
'hzmr : 'jglg + 'srlg,
'ddnh : 'clzh * 'wdzp,
'qbpm : 3,
'bjsn : 2,
'phvj : 1,
'fdct : 'bhts / 'dzrl,
'zgpc : 3,
'slqh : 'wcbz + 'vcnh,
'brgv : 'blrt + 'nznd,
'rprf : 'zqnq * 'gzht,
'bnbh : 2,
'qwlw : 'gfld * 'pppv,
'mhvv : 'qqrd + 'jnmv,
'mvvj : 'dcnz + 'nvns,
'jwzw : 6,
'dtfd : 2,
'rmhf : 'zbwn - 'vmff,
'dzbs : 3,
'pwdp : 4,
'hfjt : 'mnnh * 'htgz,
'nhpj : 'hzvq / 'qzvq,
'jtzv : 2,
'vbsb : 3,
'sqrm : 5,
'twss : 2,
'lsdh : 'fdph - 'grvv,
'tvct : 5,
'qrvh : 2,
'jrsg : 3,
'rdjm : 'mfjc + 'jjrj,
'htdw : 2,
'cftm : 'hwss + 'zqmh,
'trdn : 'lprc + 'lqhw,
'hncw : 'fzpp / 'ghlz,
'njrq : 8,
'cqdv : 'prcg + 'gdhf,
'rhdr : 'tjbp * 'jtzq,
'wjdl : 'fgdc * 'zjdc,
'hsrc : 2,
'cslm : 3,
'ldnv : 5,
'mhdc : 2,
'dbft : 8,
'bnfh : 'vrmq + 'hlbj,
'phpm : 20,
'rzcl : 'djwq + 'wwwt,
'wwct : 'dmqb * 'lbnd,
'qfrh : 2,
'rjvc : 1,
'rtfn : 2,
'qqqt : 'hflf * 'jzlc,
'nsfb : 4,
'ghvv : 4,
'ggzv : 3,
'qfwz : 4,
'nmcg : 5,
'hmhq : 'gtdm * 'jtsp,
'msqt : 'qbpm * 'djpf,
'lcgq : 'pbww * 'vdcb,
'sbtf : 4,
'bvqt : 18,
'jbcn : 'lnhm + 'gbzz,
'nhwn : 'vmgj * 'mwrv,
'cmzb : 'rsrn * 'fspc,
'blrt : 'rchh + 'lcwt,
'phns : 6,
'zbwn : 'rfbm * 'htqd,
'hjlb : 3,
'zhsc : 2,
'sqrr : 'qqrt * 'wcnv,
'hlvc : 'zvgw + 'rtgt,
'lcgr : 'whqz + 'fwmt,
'bntg : 2,
'qcvd : 'pdcb - 'brnh,
'mlhd : 5,
'ldqh : 'qqrq * 'mrpq,
'lhmc : 'ghvr * 'trbq,
'jqhj : 2,
'gjss : 3,
'czdd : 2,
'drrp : 7,
'jwmw : 'dwcw * 'tfpn,
'drsj : 'dfvc + 'zgng,
'jnqc : 'rqjs + 'mnbw,
'djtv : 'qjpz * 'dbnr,
'hfgc : 3,
'djsd : 5,
'tpvl : 'lzmd * 'wljp,
'mnlw : 3,
'fgwd : 'vggf * 'zqvd,
'jcsh : 'jjhq + 'drzv,
'bpww : 'gwbs + 'bqgt,
'gvvb : 2,
'rrvz : 20,
'fbsw : 6,
'pntj : 2,
'pzvh : 'cqcr * 'gdnz,
'qgsj : 'jcbz + 'dclv,
'dzhn : 'bnfw - 'fhgz,
'tvzn : 'wrzj * 'qrpv,
'fthp : 'vpht + 'ngqf,
'jjzt : 4,
'phzg : 'ccfj + 'zdvl,
'zsfp : 1,
'llrm : 12,
'rzrd : 'mjsm + 'tfvl,
'dszv : 2,
'vttc : 'fqcp * 'jjlq,
'vvjt : 7,
'zvht : 'ghfw + 'dnjs,
'ztwf : 3,
'psrf : 5,
'qhpf : 'fdng + 'ppsr,
'wrbw : 'hgdb + 'mvtr,
'hbvh : 'rcfm - 'scfm,
'zqms : 'cvnr / 'hjcj,
'lcnq : 'zdtg * 'sldz,
'bfhq : 2,
'fmdj : 'bcwv * 'dcml,
'shqv : 2,
'pzmt : 9,
'qqht : 'pcpw + 'grhg,
'wrjc : 5,
'hcln : 'btsm + 'rsst,
'vrlw : 'tdjt + 'rggj,
'mcqz : 3,
'dzjr : 3,
'cdpt : 1,
'pmpn : 2,
'hvfj : 'bghf - 'qpqw,
'rntm : 'vfdd * 'hqpd,
'httn : 7,
'qpqw : 5,
'tlwt : 11,
'nnrf : 'hfbh + 'lgnb,
'cmjm : 'wsps * 'cjtq,
'qvbz : 4,
'vbfd : 'vlrh + 'ljwm,
'pgnm : 'hvhf * 'pfrg,
'rwwg : 5,
'fnwg : 'zcrp * 'bfhw,
'gqvc : 3,
'svwq : 'qwvw + 'czrw,
'bmdf : 1,
'vmrb : 'snht + 'bvgh,
'tztt : 7,
'hmtf : 'rmcs + 'shjl,
'fsqw : 2,
'rpmz : 'hjmn * 'mbpc,
'lwns : 'smss + 'gmzc,
'ftds : 5,
'fdng : 'tjjd * 'hdjh,
'wsjv : 'vpzw + 'bwwz,
'nvcv : 14,
'dssf : 'vwvf * 'sfjj,
'rnsd : 'mmdf * 'bqrl,
'bzbw : 4,
'sjmf : 12,
'hvmr : 2,
'qgfw : 7,
'shvp : 3,
'cgmm : 3,
'hfbh : 5,
'ccns : 5,
'tfhf : 3,
'whgv : 'cdtv * 'qlzf,
'plfl : 16,
'rdzf : 15,
'gjvm : 2,
'gdhf : 1,
'tntl : 2,
'bcwv : 'hnvh * 'vgtj,
'mbtd : 'zfdh * 'vnbl,
'tdjq : 4,
'lrwm : 'gpqf * 'tzlw,
'mbfc : 10,
'ccbt : 'ztmg + 'qctc,
'vsrp : 'hfcp * 'zpgf,
'njvs : 'hwcn * 'fqrv,
'cfmj : 'nlfp + 'vfpw,
'nqgr : 'grpv * 'qwll,
'jfmb : 'rjsz + 'pnqj,
'swvg : 'djnc * 'tcjz,
'lbmp : 4,
'trfv : 11,
'ffqp : 4,
'lnfh : 4,
'dqqt : 'pmpn * 'dmgn,
'tzfb : 'rhwd * 'mcgv,
'clrf : 3,
'zzjj : 'hwjn * 'shqv,
'lgtr : 'vhqq + 'fqwc,
'lbsz : 3,
'ztmg : 15,
'wjfb : 'gwsv + 'nwrw,
'gqwq : 9,
'cqqp : 6,
'bhwq : 'tcnm + 'fswg,
'svbt : 2,
'rdfp : 3,
'tmpj : 3,
'zvhr : 'hnfj * 'zqms,
'vdhg : 3,
'cnwh : 6,
'mngl : 'hbnf * 'mwsh,
'vmwl : 'wcbl + 'lfzl,
'vbpv : 'sncz * 'vllm,
'cbjm : 'wghv + 'mhft,
'hsjt : 7,
'csrp : 'tsws - 'vzcw,
'jhlv : 'pnds * 'pbbg,
'qjvh : 2,
'jnjf : 5,
'cwwr : 11,
'hnsz : 12,
'qpgs : 4,
'cwbc : 4,
'sjjd : 2,
'ljgh : 2,
'tnrv : 2,
'cmdm : 'tqgj * 'wbzz,
'qvvm : 'zjjd + 'lwpb,
'zhbp : 5,
'swct : 'ddhf + 'svzr,
'dpgh : 'dzjr * 'jrjz,
'tspq : 'qcmw + 'srgw,
'rcpf : 5,
'qpnw : 12,
'tzlw : 'jdpb + 'gznp,
'qfhr : 5,
'gtsh : 2,
'nrcz : 2,
'lqpj : 4,
'bwml : 'rqnj * 'nwmp,
'hgpq : 19,
'qrlh : 'qfhr + 'brrb,
'rwcn : 'lmgl * 'rmjh,
'htdn : 'bvgp * 'mjhg,
'sjdh : 2,
'vtbd : 2,
'rdwf : 3,
'wshv : 7,
'dhls : 'cljw * 'lwtd,
'lsss : 9,
'zhvw : 'gsrr - 'bspj,
'dtjg : 'dfbp * 'fmht,
'szrn : 'gsgw * 'httl,
'zsvv : 'tbcq / 'jnpg,
'pdwh : 2,
'zjzc : 'fmrz + 'hwwm,
'zjsd : 'brbf + 'rnqs,
'cbzh : 'dfcj * 'rsdc,
'pvzr : 7,
'zgmr : 5,
'fwwv : 2,
'hjmn : 2,
'mplv : 'lzhl + 'nlhq,
'zndl : 3,
'mvps : 'nwpw - 'szrp,
'vdhn : 'mlnr + 'hzmt,
'cpzp : 'nttw * 'psfs,
'cdtv : 3,
'vpph : 'tpwg * 'qwrl,
'prff : 'vsts / 'lrbj,
'mrbn : 'cwbc * 'rvhl,
'npmv : 'vrmf * 'lpqr,
'fdlp : 'qnlm + 'trpp,
'shts : 'jbcn * 'cpwf,
'wfpt : 'rjrn + 'grqv,
'pvfw : 'mnlw * 'mfdd,
'dppw : 'bnfh * 'rqjg,
'jhrl : 2,
'cjcb : 5,
'mtfj : 2,
'znqf : 5,
'fvvv : 2,
'vwvm : 'cmfl * 'wwtf,
'zhcr : 3,
'bhnc : 'qdhp / 'ljgh,
'bvgh : 'bsrg / 'dfqd,
'dtwc : 'fbsw + 'rjvc,
'mrhz : 'zwlj * 'hnnq,
'cbnm : 3,
'qwrl : 3,
'chln : 8,
'dbnr : 3,
'sqfv : 5,
'gclj : 3,
'tcrs : 2,
'jnpg : 2,
'stdh : 9,
'jrjz : 'lhdn + 'qnsd,
'blph : 'pgtn / 'tglv,
'nztv : 'nqgr / 'dcbz,
'wghv : 'fqdq - 'hctd,
'cvdm : 2,
'trtd : 'snwt * 'zhhd,
'shpn : 'cwfv - 'pdrw,
'gwbm : 3,
'vqdl : 5,
'dgmq : 'wcqv + 'cjvp,
'mwvv : 14,
'smpq : 'phgc * 'ssjq,
'rhwd : 5,
'nsrd : 'jnhh + 'clqz,
'jthm : 5,
'pqdn : 'drsf + 'bqfn,
'dbns : 3,
'zvtp : 'vvdd * 'lprj,
'qwgp : 'llpw * 'wmtq,
'jrbd : 3,
'zvmz : 'shvp + 'fqmw,
'pmvd : 'hglm + 'zmjm,
'nnbc : 'tftz + 'gcmm,
'vspb : 2,
'swnt : 'jccs + 'tsnb,
'qvzr : 13,
'jrrt : 'zhbp * 'wpbd,
'ffzp : 'qhth * 'jwbt,
'mstb : 4,
'lzhl : 1,
'gtdm : 4,
'bhhl : 2,
'fnnl : 'pmmd + 'ltvl,
'fqcp : 2,
'rqll : 'hltf + 'mqwc,
'nfch : 'rzhb * 'csrp,
'bbfd : 'ztwf * 'sqps,
'mwtg : 5,
'rgmq : 2,
'zzzq : 6,
'wdzp : 'zjqc * 'sfcl,
'dzrl : 2,
'ptnl : 'bgwr - 'sgfc,
'bnhq : 'zzpg + 'trtd,
'wnjf : 'gvsg + 'wlfn,
'zbcv : 'mzmq + 'wvms,
'blmn : 'jjzf / 'chtz,
'vghj : 'zhsc * 'wdzs,
'rvth : 7,
'qsms : 5,
'tfjf : 'rjmr * 'mgjv,
'jhtm : 5,
'tlsj : 'nlnw + 'pfvp,
'nlph : 'rmcc * 'srtp,
'jwhh : 'qgvq + 'ghbj,
'lfzl : 'bwtb + 'nvcv,
'rfbm : 'jmrl * 'qwht,
'gzng : 2,
'wdzs : 'fqmp * 'mtsq,
'dwvt : 'zgjm * 'wcqf,
'znnm : 3,
'vjpr : 'mtst * 'jqgz,
'wpsf : 'zzzq + 'jdrt,
'lgnb : 'qwgp / 'wjdl,
'npmr : 'twss * 'jsjf,
'btfd : 3,
'qzvq : 2,
'lbbp : 'rdzf * 'lvcv,
'jjsn : 'cfcv - 'djsj,
'tsws : 'tsvd / 'bqnq,
'cfwv : 3,
'mrpn : 'bmqd / 'jftv,
'jjhq : 'msgf + 'rrvz,
'twsn : 'tjqt * 'ddss,
'ttnb : 'zvpz + 'trmc,
'lfzn : 3,
'zzpg : 'jlhl * 'zjjv,
'qdch : 5,
'srlg : 'qnnc * 'nwrh,
'nbln : 4,
'rqnj : 3,
'nmsf : 3,
'phcc : 15,
'tjjd : 3,
'nfht : 2,
'rhsw : 'psgg * 'jvcj,
'wfgh : 'qmlz + 'mpdc,
'tjnn : 'hfgg + 'hmtf,
'lprc : 1,
'twwd : 'jfgf + 'gbjv,
'jgbf : 'vbdr * 'jcps,
'zpzs : 'gtwc + 'brgb,
'flcr : 'fcdz * 'jzcz,
'wlld : 12,
'wvjw : 2,
'lqgt : 'sjrn + 'tnbf,
'nndv : 'wwbm * 'jnqc,
'brrb : 'fqlj + 'vgqn,
'sqps : 'mzml * 'fvwp,
'jshc : 4,
'jvrl : 'wdhz * 'nbhz,
'jjhn : 2,
'lddm : 2,
'mnph : 2,
'whfp : 'mhmb - 'vjfw,
'vbfb : 3,
'gpgd : 'pjrv / 'gjvm,
'llng : 3,
'hwzq : 3,
'dfcs : 8,
'gjmt : 2,
'vgqn : 'gcrn * 'jmfv,
'qgpr : 2,
'nnsw : 4,
'dwsp : 1,
'rcvm : 'glwb * 'qchg,
'vshw : 4,
'ssjq : 2,
'jzhj : 'rzrd + 'qdlc,
'bzdz : 'rzpt * 'djzt,
'mttr : 'lwns * 'gcnq,
'hjqz : 'lplf * 'zpqm,
'tthb : 12,
'rrqd : 3,
'dswd : 'zbdv * 'lpvm,
'mjvf : 3,
'pvwc : 3,
'ltmc : 2,
'qljn : 'wzcw - 'zbhf,
'wnbr : 'whfp / 'nrqp,
'hdpp : 'nltn * 'mzrr,
'zjjd : 'pzms * 'zpgv,
'jjlq : 4,
'npqw : 'cfwv + 'lhdv,
'rfjz : 15,
'qwvw : 'jjzl + 'jgvh,
'sgwt : 'hfgc * 'jjfm,
'zzdb : 'zqzz + 'mwvv,
'bdcj : 13,
'wpwg : 'mrcl + 'mshw,
'rjrn : 12,
'rnqs : 7,
'mhlj : 'djpd / 'fpwl,
'dnsz : 11,
'tgwh : 'gzcr + 'tpvl,
'gmdh : 5,
'grsm : 'fhwt * 'tnbc,
'tqsp : 2,
'zmsh : 'gjll * 'ghtc,
'qctc : 'zzjj * 'snpf,
'gcsc : 19,
'swbc : 3,
'wgwl : 5,
'ppgm : 4,
'vjfd : 12,
'znjz : 'tbvm + 'ghmg,
'rcfm : 'vqdl * 'tfll,
'tqhq : 'fthp / 'httn,
'gtwc : 'mrcq * 'zcnj,
'ncnt : 2,
'mfjh : 2,
'lmgq : 'hqsh * 'ldnr,
'tdrc : 5,
'hpjz : 'hrcf - 'qfwz,
'dmpq : 2,
'tjqt : 2,
'nlfp : 'qhlq + 'tgvn,
'qlrc : 'nbnm * 'lgwq,
'fwhd : 'dszv * 'hdsc,
'vwbv : 'cfdv * 'jzjz,
'jhgg : 'smgn + 'qgtc,
'hdsc : 'mfrz + 'dnhb,
'ffqg : 16,
'hgdq : 8,
'pndf : 8,
'zmsn : 5,
'glhs : 'dslm * 'mfgm,
'dpgc : 5,
'gvsg : 'ccns * 'lvhz,
'hllj : 'rgfp * 'rwmh,
'ctfp : 'nwwn + 'vmwl,
'wmhg : 2,
'sjwg : 2,
'jfps : 'frvm * 'llrm,
'llvh : 17,
'nmpg : 3,
'hhln : 5,
'tbpp : 9,
'lmgz : 2,
'mfrz : 6,
'tmtq : 'jgcs + 'hgjg,
'trpp : 'tbfl + 'jlbg,
'wztf : 'lpcd * 'vhgr,
'hjcj : 3,
'nffs : 'qrbh * 'lsrp,
'tmcv : 2,
'pchr : 'mgfl + 'djsd,
'vhtr : 13,
'fdsz : 'wmvs + 'npmr,
'gqlb : 'wzjb - 'cfgp,
'qnlz : 3,
'qtps : 'zqpc + 'mnph,
'qsnd : 3,
'tlrs : 'gqws + 'hrdb,
'ctjh : 6,
'hfmn : 'hwzq + 'bhwq,
'gtrq : 2,
'mdmp : 13,
'bhzw : 2,
'hqst : 7,
'smcl : 2,
'cwmm : 3,
'fvwp : 13,
'pqgh : 'rqmw / 'plwq,
'wdvc : 2,
'lhsn : 2,
'lpqr : 'zvht + 'rgfd,
'cfcv : 'nhwv * 'vmvq,
'vpht : 'cgqt * 'hcqd,
'qnct : 2,
'bwlt : 'wlld * 'dnpj,
'dbbg : 6,
'rsrn : 'lnhv + 'wzwq,
'cjld : 3,
'dnjs : 'hhrs + 'zjqp,
'dprz : 'vzwc / 'vmtj,
'bqnq : 2,
'grvv : 'wjtb / 'tnrv,
'glwb : 3,
'cqwp : 5,
'fqmp : 4,
'dmtz : 2,
'fvdg : 8,
'gwgs : 'bhmg * 'qrjj,
'jvdg : 'mwdw * 'btjh,
'bcsq : 'wpws - 'nsrj,
'sccw : 'bjnj * 'tzjj,
'jtpv : 6,
'jsdc : 'wnbr + 'mvvc,
'dbrl : 'jbsc + 'tgwh,
'hsbz : 'tdjq + 'nblh,
'tbdd : 'gjgl + 'gqlr,
'vjlq : 3,
'rczl : 'qvzr * 'cwtd,
'htqn : 'rqzn - 'dtqz,
'vljw : 5,
'tqvp : 6,
'dtjv : 'mpzt / 'bzbw,
'llnn : 2,
'dgfs : 3,
'mzrr : 'fvdg + 'dvss,
'lrqz : 5,
'jcbz : 'ttnb * 'mnsz,
'dvbv : 'wtwj * 'dtfd,
'dcmz : 3,
'bwqd : 'rdzp * 'tgcm,
'csgg : 3,
'vbcq : 2,
'qmtl : 'qsgm + 'jfps,
'jwfb : 5,
'mwwp : 'dwsp + 'hmhq,
'jpmw : 'djvd * 'sqhm,
'lgpq : 'nshj + 'swnt,
'bfrl : 2,
'lgdl : 3,
'vvgb : 'dflv * 'sdzj,
'cvzq : 18,
'ptdv : 14,
'pnqj : 2,
'clwj : 'gwts + 'tmcs,
'qvgh : 2,
'mntd : 'thjt + 'wswg,
'dzql : 3,
'fpnw : 'fmsh * 'nwbr,
'lprb : 4,
'qgfd : 4,
'gwwg : 'jlgr * 'sfhw,
'qvmf : 2,
'mcfs : 'bvcn - 'dcpr,
'vzwf : 1,
'zfsj : 4,
'plzb : 1,
'gcrn : 9,
'zdlf : 'nhwn + 'hdjj,
'vqgg : 'lscg * 'jrrp,
'mqcb : 1,
'jvpl : 4,
'mtqr : 20,
'lljq : 'zglh + 'mvdm,
'jnwz : 'hhhb * 'vdqm,
'rlsh : 2,
'gnvl : 3,
'fhgz : 1,
'ljwn : 9,
'qzbs : 'jdpv * 'fmwg,
'dzwl : 'bfmz + 'rzfp,
'cdmm : 3,
'hspl : 5,
'zgft : 'vshw + 'tspv,
'qrpv : 'vdhn * 'ssbd,
'sgwf : 5,
'zglf : 'ncdg + 'tqrt,
'wlfn : 1,
'vzcw : 'rdzt * 'rznq,
'tqtz : 'pdwh + 'ftds,
'bfmz : 'gqvj * 'lhsn,
'grtq : 3,
'mhnh : 2,
'ntft : 1,
'jnhh : 2,
'lwpb : 19,
'rbnh : 'nwrq + 'vmrz,
'mnlv : 'tzdq * 'mgdj,
'tjzz : 2,
'zhhd : 'lcnq / 'zqrv,
'zqdl : 9,
'hdjh : 'zczh + 'mmrc,
'zqzz : 9,
'vrmf : 3,
'qmhj : 'lgbz + 'bpnd,
'mcgv : 'zdmf + 'jlfd,
'zcnj : 2,
'dlgt : 'zjzt - 'pvbl,
'vvqp : 5,
'gqws : 'cfdh + 'grln,
'fqqc : 2,
'jbns : 2,
'tldh : 4,
'qnww : 'wmcc * 'qwls,
'gjll : 7,
'gclz : 1,
'djbd : 'rzrc * 'qgls,
'stpp : 'pjfs + 'bvjs,
'lmgl : 'gwhb + 'gdbp,
'vtll : 'sqrr + 'sjnh,
'zmvv : 'vwvm * 'vhld,
'fmht : 'mhvv + 'smfj,
'ghfw : 'dqpw + 'hdtv,
'jcnl : 2,
'gzsf : 'mlhd * 'fbzd,
'zjzt : 'dmff / 'rnfs,
'ldnr : 4,
'qggh : 6,
'qczb : 2,
'zmjm : 'ncnt + 'zlvj,
'nwmp : 'ljpq + 'fvzg,
'dhwt : 3,
'tgcm : 3,
'vmrz : 'cjjm + 'vcmv,
'qvnn : 3,
'cpwf : 'vvjt + 'vljw,
'dgjs : 5,
'ssjd : 6,
'zqpc : 5,
'nmhs : 'njrq + 'tvtw,
'nhwv : 5,
'stbs : 'pvfl + 'mbrm,
'bvjs : 'shpn * 'hnlp,
'wcch : 'zjzc + 'vbzl,
'qrbh : 'nzzm + 'bqhb,
'bjbm : 13,
'pjgw : 'lmgq * 'qdtd,
'mnbw : 4,
'dffm : 6,
'lvsc : 2,
'sjrn : 'qnwn * 'hbvh,
'jvfq : 4,
'cvrj : 13,
'sqcs : 2,
'tnnl : 'bgrr + 'dgvb,
'httl : 3,
'plvh : 2,
'vmtj : 2,
'qsbd : 2,
'fdqb : 'srqg + 'rtrz,
'qjzq : 'lcwb + 'zrwc,
'vgll : 'wbbf + 'cmdm,
'gslb : 'gbss * 'swbb,
'rjgm : 4,
'bzgl : 'vtll / 'sggz,
'hvpw : 4,
'rrvs : 'bdmh * 'qszw,
'mlpr : 2,
'rzrc : 3,
'tpwg : 2,
'bdcw : 3,
'cstf : 'gcsb + 'vcgp,
'tcnm : 'bmfn * 'cwmm,
'tjrv : 'cbnm + 'wrtf,
'fcsz : 'rvbr + 'znnm,
'cljw : 4,
'fspc : 12,
'tlzs : 17,
'bggv : 'nlsl + 'cbqj,
'jbdf : 7,
'bqhb : 18,
'wdhz : 13,
'jbrr : 7,
'jjfm : 10,
'cwvg : 'tpcc + 'tljd,
'qblp : 'djtv * 'hspl,
'vmff : 'hjqz * 'vszq,
'vmms : 5,
'jjtf : 2,
'vbzl : 'cvdm + 'bqgh,
'gbff : 'nmrm + 'dssf,
'vmzz : 'wvrl + 'dqqt,
'jszq : 'bpgb * 'jzgr,
'vfnl : 'jvdg - 'qdpw,
'pfqq : 'lntf + 'wqwp,
'mbwp : 'bbhr / 'fdsz,
'fsmp : 3,
'fmmg : 4,
'mdmf : 'nbcn * 'tgfm,
'vhqq : 'jnfg + 'gjhs,
'fqnp : 17,
'bvfm : 6,
'pfsb : 5,
'bvll : 7,
'wbrh : 'rjmh - 'bbnz,
'jqtf : 'pjst * 'fpsh,
'fzfj : 'bpcq + 'ttgt,
'nzwn : 4,
'wzcw : 'dgjs * 'wnwz,
'rwwb : 5,
'vmct : 'wtsl + 'tgzb,
'tnbc : 'phcc + 'plvh,
'vcnh : 'tcfd * 'chcj,
'vrhn : 'cdmm * 'vdrh,
'pmzv : 'gtrq * 'hsdw,
'ltmz : 'nsfb * 'rgsj,
'mhft : 'rzrg + 'vvgb,
'bhnt : 'hhlp / 'fnql,
'mwqb : 2,
'fbzd : 7,
'wgjf : 8,
'pvqp : 'dgpl * 'mbcl,
'zjgf : 'rrqd * 'wrzp,
'rtmm : 'vmhm * 'qpnw,
'pzhv : 'zmsh + 'bcpw,
'djsj : 'vqjq * 'zdlf,
'bgwr : 'rjnf * 'dzbs,
'qhlq : 16,
'ddvs : 'stpp + 'zqcj,
'bvpm : 'rtmm + 'cstf,
'zpgv : 6,
'dnff : 13,
'zpqm : 2,
'gbtw : 11,
'bcpw : 6,
'cwqr : 2,
'tqrn : 11,
'mwmz : 'mctg + 'wwjt,
'zwmp : 2,
'bscq : 3,
'gzcr : 'fnnl + 'wpwg,
'dcpr : 3,
'wbsq : 'ccgn + 'zqrp,
'wscd : 2,
'qwht : 'fglm + 'qvmf,
'bdmh : 'mjvf * 'mfzd,
'qqcj : 3,
'rznq : 2,
'msjz : 2,
'cbjg : 6,
'cwdv : 7,
'zqvd : 6,
'tdhr : 7,
'ldcc : 'wtnp + 'mffz,
'rjzn : 'mhhc + 'wbvd,
'vtht : 'lqpj + 'vjsn,
'snht : 'lgjc * 'jsvh,
'zdmf : 3,
'cdgw : 9,
'wcqf : 'tlsj * 'cbpf,
'jbwj : 'rplw * 'hbjl,
'gccb : 'rqqq + 'bqlp,
'htmb : 20,
'qsgm : 'vjmg * 'rpnf,
'qcjv : 7,
'vjmg : 'vrpp + 'vjrs,
'nnnj : 4,
'mbrm : 'pcwl * 'dlgc,
'fqdq : 'rcmh * 'lvmg,
'mpfj : 11,
'gtpr : 2,
'sssm : 'gvgj * 'qgfd,
'rpnf : 'rfjz + 'sbtf,
'lgbz : 2,
'tfpn : 'pfjl + 'rpgm,
'wdnp : 'qpgj * 'bsjm,
'wcqv : 'qpsh * 'qfqf,
'gcqr : 2,
'jdpb : 5,
'tlrl : 'lqgt + 'jcgl,
'tqgj : 3,
'vlvg : 'bmdf + 'rntm,
'pdzv : 2,
'qcmw : 6,
'hdzh : 4,
'dqqf : 8,
'fnjm : 'sjmf + 'mrhz,
'bsrt : 'lcgq * 'plfl,
'zldn : 2,
'zcdt : 'zbjj * 'zsdp,
'dlds : 2,
'jwst : 'cwcc + 'gpgd,
'zlqg : 'qlpp / 'wrbw,
'dwmh : 2,
'qszw : 'qhpf - 'twsp,
'thrl : 8,
'pbww : 4,
'gmsf : 7,
'sdpv : 20,
'rgvj : 'cwvg + 'trsf,
'qrjj : 5,
'wtsl : 3,
'rpbs : 'dppw - 'mdrh,
'hrdb : 'vfnl * 'nfht,
'wnpn : 3,
'mnnh : 2,
'mlwp : 3,
'crfc : 'bnbh * 'vhvm,
'rzfp : 1,
'tdjt : 'lvqt + 'pwnq,
'jdrt : 1,
'wfsm : 20,
'hqzb : 14,
'nzzm : 'vrhn + 'bpsf,
'gspv : 'rnsd + 'dqvg,
'bnwr : 'fdtl * 'bgwn,
'wpws : 'fjgf * 'jfmb,
'tsjs : 'zgsm - 'ccbt,
'vfzr : 2,
'rpgm : 'vtbd * 'ncrq,
'ghrg : 5,
'mhvb : 2,
'cqcr : 2,
'vqjh : 'lbbp - 'tlrs,
'nwwq : 'nhpj - 'cdgw,
'jhfd : 'cbzh + 'wbrh,
'sggz : 6,
'dltm : 4,
'wrrg : 7,
'npnw : 11,
'vtdm : 'vsqw - 'rnjh,
'lrbj : 2,
'vhld : 'cwhz * 'cppp,
'brdd : 'vqjj / 'tcrs,
'lfjv : 'gpnq * 'gbmw,
'srtp : 'dpgc + 'lddm,
'bffj : 'nggm + 'szmg,
'bvmz : 'vqjh / 'gjmt,
'lnfw : 20,
'szmg : 'tbjv * 'gvmf,
'hpjl : 4,
'wssc : 3,
'jtsp : 4,
'wzjb : 'qzrl * 'qzbs,
'qgls : 'jvpl * 'lwdd,
'drvg : 3,
'lrhn : 'vqnw + 'vpnw,
'vmtt : 2,
'jzgr : 'njpm + 'gslb,
'hbjl : 2,
'rggj : 'lvdg + 'tpdb,
'bhmg : 3,
'gccv : 1,
'hjns : 3,
'rzhs : 7,
'prdq : 'bhzz + 'vlvg,
'fnql : 5,
'cdcw : 19,
'fqnw : 'fwwv * 'glrl,
'tqrt : 'nvvn + 'ldnv,
'zzsc : 'nffs / 'cslm,
'jrjj : 4,
'lrwd : 'nbln * 'qzww,
'plcb : 'fzdd * 'prff,
'vszq : 'rzpr + 'rdrf,
'fvzg : 4,
'hhrs : 7,
'zqrv : 3,
'dpsp : 13,
'nshj : 'bzqz - 'htmb,
'vgmj : 'dnqc * 'wpjj,
'swpl : 4,
'ftzp : 3,
'lnhv : 16,
'dsss : 5,
'zvvg : 2,
'mnsz : 4,
'cnqt : 'lmrp * 'lzvs,
'rtlb : 'ddnh + 'dgft,
'pjfs : 'vjjw * 'hbmn,
'jlhl : 'qgfz * 'pjqd,
'hglb : 'ccjt * 'twnd,
'lwbv : 'bdsv * 'nwng,
'cfgp : 'hmfv * 'gqwq,
'flgs : 3,
'bbnz : 'qcvd + 'lvzt,
'lscg : 'dwvt + 'clwj,
'vmpz : 'qplt + 'qmst,
'rlst : 'jjsn / 'fsmp,
'fsgp : 'gpbc / 'qqwl,
'whzt : 3,
'zhmn : 'rbnh * 'rbps,
'grhg : 3,
'mrcq : 'hpth + 'ghtf,
'qhwq : 'cjld * 'lpcp,
'tgbc : 'blnr + 'gccv,
'wpcp : 3,
'sfzw : 3,
'rwzg : 'tvzn - 'dvhr,
'jnfg : 'dvbv + 'shtp,
'zjqc : 2,
'dfqd : 2,
'lgwq : 'hpjz + 'qqqt,
'vdcb : 2,
'hfcp : 'zzfr + 'thwh,
'jfcf : 'hfvw + 'qmgg,
'zjlp : 'mjnz + 'npnp,
'gwts : 6,
'zbhf : 'bdpz + 'dgcw,
'vzzg : 'trvq * 'wvjw,
'sldz : 3,
'wbbf : 14,
'psgg : 20,
'mgrb : 5,
'vtmf : 'jjzt + 'dgmq,
'jhvv : 'vltf * 'ffnr,
'qwll : 'bwqd - 'fhrn,
'dmqb : 2,
'dfbp : 3,
'blrm : 4,
'dhsc : 2,
'zfdh : 2,
'rqqq : 3,
'djnc : 2,
'qtgr : 18,
'nrfc : 1,
'trbq : 3,
'tsln : 3,
'hfvw : 'hwjd + 'gmsf,
'cmjr : 2,
'vjfw : 'bnwr / 'tcbl,
'hsfl : 'nfwj + 'zmvv,
'wzsj : 5,
'lplf : 5,
'vwsz : 'hjlb + 'dbft,
'jlgr : 2,
'zgng : 'pnfn - 'brdd,
'bpqf : 5,
'dslm : 'pgcr + 'zcwg,
'fcdz : 'hsqr + 'cdpt,
'cnpg : 7,
'rdzp : 3,
'ddhf : 5,
'lfzd : 20,
'mjnz : 'hbng * 'tdrc,
'gtnl : 'rrjs * 'cwwr,
'zhph : 'dpsp * 'jmsd,
'mwrv : 3,
'vjjw : 'vqlh + 'wsgw,
'swss : 'gvvc + 'vtzb,
'qvrb : 2,
'bzrp : 'dpmq * 'whzt,
'vbtz : 2,
'zqgr : 17,
'vpnm : 5,
'mmtr : 'vsqh + 'fsld,
'gmrd : 'bqdz - 'dzqd,
'hlcv : 'nqvs + 'mpfv,
'tpjg : 3,
'gbss : 2,
'psln : 'vfsh * 'lhfr,
'dhfl : 'pmvd / 'htsl,
'tbjv : 3,
'qqgq : 5,
'bgrr : 4,
'pgbf : 'svwq + 'lqld,
'czfm : 14,
'pjst : 2,
'vdqm : 3,
'rmqf : 'wnds * 'ppgm,
'cddd : 'mnzg + 'vctl,
'mrbs : 'vhlr - 'nqsp,
'mqpl : 'ghvv * 'jjrb,
'lffs : 'fncs / 'pzbl,
'pgtn : 'wwgh * 'ncqs,
'rmcs : 'nnqv + 'cmsr,
'tlsf : 5,
'zbtg : 'nlhz * 'bbml,
'swjh : 'vmrv * 'jshc,
'pclm : 'rjgm + 'rdfp,
'hssn : 2,
'zghf : 4,
'pshn : 'jwmw + 'vddl,
'fdph : 'ppqd + 'cqzn,
'fhll : 4,
'bsjm : 4,
'bghf : 'gzsf - 'nqgv,
'bgwn : 'nlph + 'lrwd,
'jjzs : 14,
'vdqr : 2,
'lhdv : 4,
'szfw : 16,
'humn : 870,
'lwdd : 2,
'grqv : 'nnlr + 'rcpf,
'wmtq : 12,
'nwng : 10,
'wqnd : 'qgsj + 'nrrv,
'lvzt : 20,
'mvtr : 3,
'cpgw : 'tmbl / 'bfrl,
'wwhr : 'hqgl - 'hsnl,
'rmqt : 'jsdn + 'nsrd,
'cnqb : 4,
'hrcf : 'zvmz + 'qrlh,
'qlrl : 'bfmg + 'pvzr,
'jjzf : 'phgh + 'jgbf,
'bcgw : 3,
'mnrs : 'vjjr / 'cjcb,
'tlzj : 'rtlb + 'cbjm,
'lsqz : 16,
'vtzc : 'dlds * 'rvth,
'ppwn : 'tzth * 'fsfb,
'mdhp : 3,
'hnnq : 2,
'jgjr : 'shts - 'bbfd,
'nnvg : 2,
'wlbf : 'mtqj + 'tdlr,
'npmq : 3,
'fvgf : 10,
'wcbl : 'wbmh * 'llhn,
'mfgm : 2,
'msbl : 5,
'vvsw : 5,
'spcl : 'lswh * 'wwmg,
'qgfz : 'hvfj + 'jzhj,
'mvdc : 'grfl / 'rqvt,
'bfrn : 1,
'czhw : 1,
'gwhr : 'wfrd + 'jmfz,
'vhfw : 'zndl + 'jvrl,
'mmrc : 'lljq * 'rzpg,
'thgq : 'tztt + 'rrcq,
'zzfr : 'nrfc + 'cqqp,
'qtbv : 'tmmg + 'hllj,
'tzbd : 2,
'cwsf : 'mvrq * 'dmfc,
'tnbf : 'mdmf * 'hnlm,
'rvhl : 2,
'zjdc : 4,
'wwgh : 4,
'jtzc : 5,
'fvsj : 'dnzm - 'vgmj,
'wmvs : 1,
'brnh : 6,
'llhn : 2,
'tbvm : 'bcgw * 'dvpq,
'lhgm : 'vqgg + 'wqnd,
'vddl : 'wptj * 'cnpg,
'cmzh : 4,
'pnsp : 'thdr + 'brvz,
'sfdq : 'nvpd * 'bmzp,
'bswp : 7,
'sctc : 3,
'gtph : 'vbjz * 'clrf,
'mtqj : 'gcvg + 'hgdq,
'lcww : 'dcff * 'qrzr,
'cvnr : 'mvhw * 'vvht,
'cnlp : 'qhgh + 'mrlh,
'vjgr : 'plqd * 'lhpl,
'ffrv : 2,
'btsm : 'bcgj * 'hpsh,
'rgsj : 2,
'hffl : 5,
'cbsc : 'ztsq / 'htdw,
'shtp : 1,
'rvzz : 'rgvj * 'rftm,
'swbb : 'mcwl + 'vjwh,
'mhmb : 'qslr / 'jnjf,
'fwbq : 1,
'tjjg : 2,
'rvrb : 'qbqr + 'dffm,
'zzng : 2,
'vqnw : 5,
'mgdj : 5,
'ppsr : 'fmsg * 'zggz,
'wrzp : 5,
'lzvs : 2,
'dwjw : 10,
'mdmc : 3 .
--- }}}
vars S T : Term .
vars M N : Nat .
var Eqs : Eqns .
op part2 : Eqns -> Eqns .
eq part2(('root : S + T, 'humn : N, Eqs)) = (S : T), Eqs .
eq part2(Eqs) = Eqs [owise] .
op start : -> State .
eq start = part2(puzzle) ; empty .
endm
***(
Maude> rew start .
==========================================
rewrite in RUN-PUZZLE : start .
rewrites: 13503002 in 2740ms cpu (2740ms real) (4928102 rewrites/second)
result NzNat: 3353687996514
)
--- vim: set fdm=marker :