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 :