YES bcxccxaaxabxcbxcaxbaxcaxacxcaxcaxabxabxccx2.1abxccxcaxabxacxcaxbaxcaxcbxcaxaaxabxbcxccxcaxccxacxabxbaxabxcbxabxaaxccx2aaxccxcbxabxbaxabxacxabxcaxccxbcxccxaaxabxcbxcaxbaxcaxacxcaxcaxabxabxccxcbxccxbaxccxacxccx2aaxccx5cbxabx7baxabx9acxabx15caxccx0bcxccx0aaxabx12cbxcax7baxcax1acxcax15caxabx9abxccx0cbxccx0baxccx0acxccx0accx915acxccxcccx915ccax9151caxccxcccx915bccx916bcxccxcccx916abax916abxccxccax9161caxccxcccx916bccx916bcxccxcccx916abax9161baxccxaccx916acxccxcccx916cccx917ccax9171caxccxcccx917ccxabxabxccxccxaccx919abax9191baxccxaccx919bccx920bcxccxcccx920caax9201aaxccxcccx920cccx921abax921abxccxccax9211caxccxcccx921cccx921abax9211baxccxaccx921acxccxcccx921bccx922bcxccxcccx922ccax9221caxccxcccx922aabx923aaxccxccbx923abbx923abxccxccbx923aabx923aaxabxabbx923abbx923babx924baxcaxcabx924ccbx9241cbxabxcabx924babx924baxccxccbx924ccbx924abxcaxcaxabxabxabxabxccxccxcaxcaxccxccxaabx926aaxccxccbx926cabx926caxccxccbx926aabx926aaxabxabbx926cabx926caxabxabbx926abxabxccxccxccxaabx928aaxccxccbx928ccbx928cabx929abax929abxccxccax9291caxabxcabx929cabx929caxccxccbx929abax9291baxabxaabx929aaxccxccbx929cabx929caxabxabbx929abxccxccbx929abax9291baxabxaabx929aaxccxccbx929cabx929caxabxabbx929abax9291baxabxaabx929aaxabxabbx929cabx9291abxccxcccx929abax929abxccxccax9291caxccxcccx929cabx9291abxccxcccx929abax9291baxccxaccx929acxccxcccx929cabx929caxccxccbx9291cbxccxcccx929abax929abxccxccax9291caxccxcccx929cabx929caxccxccbx9291cbxccxcccx929abax9291baxccxaccx929acxccxcccx929cabx929caxccxccbx9291cbxcaxccax929abax929abxccxccax929cabx929caxccxccbx9291cbxcaxccax929abax9291baxcaxacax929acxccxccax929cabx930caax9301aaxabxcabx930cabx9301abxccxcccx930caax9301aaxccxcccx930abxcaxcaxabxabxabxabxccxccxcaxcaxccxccxaabx932aaxccxccbx932ccax9321caxabxcabx932caxccxccbx932aabx932aaxabxabbx932abxccxccbx932ccax9321caxabxcabx932caxccxccbx932aabx932aaxabxabbx932ccax9321caxabxcabx932caxabxabbx932aabx932aaxccxccbx9321cbxabxcabx932ccax9321caxabxcabx932aabx932aaxccxccbx9321cbxcaxccax932ccax932aabx932aaxccxccbx9321cbxccxcccx932ccax9321caxccxcccx932aabx932aaxccxccbx9321cbxccxcccx932ccax9321caxabxcabx9321abxccxcccx932aabx9321abxccxaccx932acxccxcccx932ccax9321caxccxcccx932aabx9321abxccxaccx932acxccxcccx932ccax9321caxabxcabx9321abxccxcccx932cabx933ccax9331caxabxcabx933cabx9331abxccxcccx933ccax9331caxccxcccx933abxabxccxccxccxaabx935aaxccxccbx9351cbxccxcccx935cccx935aabx9351abxccxaccx935acxccxcccx935cccx935babx936baxcaxcabx9361abxccxcccx936abcx936abxccxcccx936babx936baxcaxcabx9361abxccxcccx936abcx9361bcxccxaccx936acxccxcccx936babx9361abxccxbccx936bcxccxcccx936abcx936abxccxcccx936babx9361abxccxbccx936bcxccxcccx936abcx9361bcxccxaccx936acxccxcccx936babx936baxccxccbx9361cbxccxcccx936abcx936abxccxcccx936babx936baxccxccbx9361cbxccxcccx936abcx9361bcxccxaccx936acxccxcccx936cabx9371abxccxcccx937cccx937aabx9381abxccxaccx938abcx9381bcxccxaccx938babx939baxcaxcabx939cacx9391acxabxcabx939abxcaxcaxabxabxabxabxccxccxcaxcaxccxccxcabx9411abxccxcccx941abcx941abxccxcccx941babx942baxcaxcabx9421abxccxcccx942cccx942babx9421abxccxbccx942bcxccxcccx942cccx942babx942baxccxccbx9421cbxccxcccx942cccx942abxabxccxccxccxaccx944abax9441baxccxaccx944bccx945bcxccxcccx945ccax9451caxccxcccx945accx946acxccxcccx946caax9461aaxccxcccx946ccxabxabxccxccxaccx948acxccxcccx948ccax9481caxccxcccx948cccx949abcx949abxccxcccx949cccx950cacx950caxccxcccx950accx951acxccxcccx951cccx951cccx952cccx952abxabxccxccxccxaabx954aaxccxccbx954ccax9541caxabxcabx954caxccxccbx954aabx954aaxabxabbx954abxccxccbx954ccax9541caxabxcabx954caxccxccbx954aabx954aaxabxabbx954ccax9541caxabxcabx954caxabxabbx954aabx954aaxccxccbx9541cbxabxcabx954ccax9541caxabxcabx954aabx954aaxccxccbx9541cbxcaxccax954ccax954aabx954aaxccxccbx9541cbxccxcccx954ccax9541caxccxcccx954aabx954aaxccxccbx9541cbxccxcccx954ccax9541caxabxcabx9541abxccxcccx954aabx9541abxccxaccx954acxccxcccx954ccax9541caxccxcccx954aabx9541abxccxaccx954acxccxcccx954ccax9541caxabxcabx9541abxccxcccx954babx955baxabxabbx955abax9551baxabxaabx955aaxabxabbx955babx955baxcaxcabx955caxabxabbx955abax9551baxabxaabx955aaxabxabbx955babx955baxcaxcabx955abax955abxccxccax9551caxabxcabx955babx955baxccxccbx9551cbxabxcabx955abax955abxccxccax9551caxabxcabx955babx955baxccxccbx955abax9551baxabxaabx955aaxccxccbx955babx955baxabxabbx955abxccxccbx955abax9551baxabxaabx955aaxccxccbx955babx955baxcaxcabx955caxccxccbx955abax9551baxabxaabx955aaxccxccbx955babx955baxcaxcabx9551abxccxcccx955abax955abxccxccax9551caxccxcccx955babx955baxcaxcabx9551abxccxcccx955abax9551baxccxaccx955acxccxcccx955babx9551abxccxbccx955bcxccxcccx955abax955abxccxccax9551caxccxcccx955babx9551abxccxbccx955bcxccxcccx955abax9551baxccxaccx955acxccxcccx955babx955baxccxccbx9551cbxccxcccx955abax955abxccxccax9551caxccxcccx955babx955baxccxccbx9551cbxccxcccx955abax9551baxccxaccx955acxccxcccx955babx955baxccxccbx9551cbxcaxccax955abax955abxccxccax955babx955baxccxccbx9551cbxcaxccax955abax9551baxcaxacax955acxccxccax955cabx956ccax9561caxabxcabx956cabx9561abxccxcccx956ccax9561caxccxcccx956aabx957abax9571baxabxaabx957aabx9571abxccxaccx957abax9571baxccxaccx957babx958baxcaxcabx958caax9581aaxabxcabx958cabx959abax959abxccxccax9591caxabxcabx959cabx959caxccxccbx959abax9591baxabxaabx959aaxccxccbx959cabx959caxabxabbx959abxccxccbx959abax9591baxabxaabx959aaxccxccbx959cabx959caxabxabbx959abax9591baxabxaabx959aaxabxabbx959cabx9591abxccxcccx959abax959abxccxccax9591caxccxcccx959cabx9591abxccxcccx959abax9591baxccxaccx959acxccxcccx959cabx959caxccxccbx9591cbxccxcccx959abax959abxccxccax9591caxccxcccx959cabx959caxccxccbx9591cbxccxcccx959abax9591baxccxaccx959acxccxcccx959cabx959caxccxccbx9591cbxcaxccax959abax959abxccxccax959cabx959caxccxccbx9591cbxcaxccax959abax9591baxcaxacax959acxccxccax959babx960baxcaxcabx960ccax9601caxabxcabx960caxcaxccxccxabxabxccxccxcaxcaxabxabxabxacax962acxccxccax962abbx962abxccxccbx9621cbxcaxccax962acax962acxabxabax962abxccxccax962abbx962abxccxccbx9621cbxcaxccax962acax962acxcaxcaax962caxccxccax962abbx962abxccxccbx9621cbxcaxccax962acax9621caxccxaccx962acxccxcccx962abbx962abxccxccbx9621cbxccxcccx962acax962acxcaxcaax9621aaxccxcccx962abbx962abxccxccbx9621cbxccxcccx962acax962acxccxccax9621caxccxcccx962abbx962abxccxccbx9621cbxccxcccx962acax962acxcaxcaax9621aaxabxcabx962abbx962abxccxccbx9621cbxabxcabx962acax962acxccxccax9621caxabxcabx962abbx962abxccxccbx9621cbxabxcabx962acax9621caxabxaabx962aaxccxccbx962abbx962abxccxccbx962acax9621caxabxaabx962aaxabxabbx962abbx962bcax963bcxccxccax963ccbx9631cbxcaxccax963acax964acxccxccax964cabx964caxccxccbx9641cbxcaxccax964acax964acxabxabax964abxccxccax964cabx964caxccxccbx9641cbxcaxccax964acax964acxcaxcaax964caxccxccax964cabx964caxccxccbx9641cbxcaxccax964acax9641caxccxaccx964acxccxcccx964cabx9641abxccxcccx964acax9641caxccxaccx964acxccxcccx964cabx964caxccxccbx9641cbxccxcccx964acax964acxcaxcaax9641aaxccxcccx964cabx9641abxccxcccx964acax964acxcaxcaax9641aaxccxcccx964cabx964caxccxccbx9641cbxccxcccx964acax964acxccxccax9641caxccxcccx964cabx9641abxccxcccx964acax964acxccxccax9641caxccxcccx964cabx964caxccxccbx9641cbxccxcccx964acax964acxcaxcaax9641aaxabxcabx964cabx964acax964acxccxccax9641caxabxcabx964cabx964acax9641caxabxaabx964aaxccxccbx964cabx964caxccxccbx964acax9641caxabxaabx964aaxccxccbx964cabx964caxabxabbx964abxccxccbx964acax9641caxabxaabx964aaxabxabbx964cabx964caxabxabbx964caxcaxccxccxccxacax966acxccxccax966ccbx9661cbxcaxccax966ccax967abax967abxccxccax967caxcaxccxccxabxabxccxccxcaxcaxabxabxabxccax969caax969caxccxccax969ccax9691caxccxcccx969caax9691aaxccxcccx969ccax9691caxabxcabx969caax9691aaxabxcabx969acax970acxccxccax970ccax970ccax971ccax971caxcaxccxccxccxacax9731caxccxaccx973acxccxcccx973cccx973acax973acxcaxcaax9731aaxccxcccx973cccx973acax973acxccxccax9731caxccxcccx973cccx973bcax9741caxccxbccx974bcxccxcccx974abcx974abxccxcccx974bcax9741caxccxbccx974bcxccxcccx974abcx9741bcxccxaccx974acxccxcccx974bcax974bcxccxccax9741caxccxcccx974abcx974abxccxcccx974bcax974bcxccxccax9741caxccxcccx974abcx9741bcxccxaccx974acxccxcccx974caxcaxccxccxabxabxccxccxcaxcaxabxabxabxccax9761caxccxcccx976cccx976acax9771caxccxaccx977abcx9771bcxccxaccx977bcax978bcxccxccax978cacx9781acxcaxccax978ccax9791caxccxcccx979abcx979abxccxcccx979bcax9801caxccxbccx980bcxccxcccx980cccx980bcax980bcxccxccax9801caxccxcccx980cccx980caxcaxccxccxccxaabx982abax9821baxabxaabx982aabx9821abxccxaccx982abax9821baxccxaccx982abxabxccxccxccxbabx984baxcaxcabx984ccax9841caxabxcabx984aabx985caax985caxabxabax9851baxabxaabx985aabx985aaxccxccbx985caax9851aaxabxcabx985caxccxccbx985aabx985aaxabxabbx985abxccxccbx985caax9851aaxabxcabx985caxccxccbx985aabx985aaxabxabbx985caax9851aaxabxcabx985caxabxabbx985aabx9851abxccxaccx985caax985caxabxabax9851baxccxaccx985aabx985aaxccxccbx9851cbxabxcabx985caax9851aaxabxcabx985aabx985aaxccxccbx9851cbxabxcabx985caax985caxccxccax9851caxabxcabx985aabx985aaxccxccbx9851cbxcaxccax985caax985caxccxccax985aabx985aaxccxccbx9851cbxcaxccax985caax985caxabxabax985abxccxccax985aabx985aaxccxccbx9851cbxccxcccx985caax9851aaxccxcccx985aabx985aaxccxccbx9851cbxccxcccx985caax985caxccxccax9851caxccxcccx985aabx985aaxccxccbx9851cbxccxcccx985caax9851aaxabxcabx9851abxccxcccx985aabx9851abxccxaccx985acxccxcccx985caax9851aaxccxcccx985aabx9851abxccxaccx985acxccxcccx985caax985caxccxccax9851caxccxcccx985aabx9851abxccxaccx985acxccxcccx985caax9851aaxabxcabx9851abxccxcccx985aabx986aaxccxccbx986ccax9861caxabxcabx986caxccxccbx986aabx986aaxabxabbx986abxccxccbx986ccax9861caxabxcabx986caxccxccbx986aabx986aaxabxabbx986ccax9861caxabxcabx986caxabxabbx986aabx986aaxccxccbx9861cbxabxcabx986ccax9861caxabxcabx986aabx986aaxccxccbx9861cbxcaxccax986ccax986aabx986aaxccxccbx9861cbxccxcccx986ccax9861caxccxcccx986aabx986aaxccxccbx9861cbxccxcccx986ccax9861caxabxcabx9861abxccxcccx986aabx9861abxccxaccx986acxccxcccx986ccax9861caxccxcccx986aabx9861abxccxaccx986acxccxcccx986ccax9861caxabxcabx9861abxccxcccx986accx987acxccxcccx987ccbx9871cbxccxcccx987bccx988bcxccxcccx988abbx988abxccxccbx9881cbxccxcccx988cccx989ccbx9891cbxccxcccx989accx990acxccxcccx990abbx990abxccxccbx9901cbxccxcccx990accx990acxabxabcx990abxccxcccx990abbx990abxccxccbx9901cbxccxcccx990accx990acxcaxcacx990caxccxcccx990abbx990abxccxccbx9901cbxccxcccx990accx990acxcaxcacx9901acxabxcabx990abbx990abxccxccbx9901cbxabxcabx990accx990acxcaxcacx9901acxcaxccax990abbx990abxccxccbx9901cbxcaxccax990bccx991bcxccxcccx991cabx9911abxccxcccx991cccx992abbx992abxccxccbx9921cbxccxcccx992bccx993bcxccxcccx993ccbx9931cbxccxcccx993ccxabxabxccxccxaccx995acxccxcccx995abbx995abxccxccbx9951cbxccxcccx995accx995acxabxabcx995abxccxcccx995abbx995abxccxccbx9951cbxccxcccx995accx995acxcaxcacx995caxccxcccx995abbx995abxccxccbx9951cbxccxcccx995accx995acxcaxcacx9951acxabxcabx995abbx995abxccxccbx9951cbxabxcabx995accx995acxcaxcacx9951acxcaxccax995abbx995abxccxccbx9951cbxcaxccax995bccx996bcxccxcccx996ccbx9961cbxccxcccx996ccxcaxcaxccxccxaccx998acxccxcccx998cabx9981abxccxcccx998accx999acxccxcccx999ccbx9991cbxccxcccx999cccx1000abax1000abxccxccax10001caxccxcccx1000cccx1000abax10001baxccxaccx1000acxccxcccx1000ccxabxabxccxccxcccx1002caax10021aaxccxcccx1002ccxcaxcaxccxccxaccx1004acxccxcccx1004ccax10041caxccxcccx1004cccx1005ccax10051caxccxcccx1005accx1006acxccxcccx1006cccx1006bccx1007bcxccxcccx1007abcx1007abxccxcccx1007ccxabxabxccxccxcccx1009cccx1009accx1010abcx10101bcxccxaccx1010accx1010acxabxabcx1010abcx1010accx1010acxccxcccx1010abcx1010abxccxcccx1010bccx1011bcxccxcccx1011cacx1011caxccxcccx1011ccxcaxcaxccxccxcccx1013abcx1013abxccxcccx1013bccx1014bcxccxcccx1014cccx1014csicsi 1.2.5 [hg: unknown](sorted -ms*; ( ((cr -kb;((( matrix -dim 1 -ib 3 -ob 5 | matrix -dim 2 -ib 2 -ob 3 | matrix -dim 3 -ib 1 -ob 1 | matrix -dim 3 -ib 1 -ob 3 | fail)[2]*);((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])! || (rev;((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])!)))))! || ((if linear then cr -closed -m -1;closed -strongly 7 else fail) || (if left-linear then cr -closed -m -1;(closed -development) else fail))! || (if linear then (cr -dup;(( lpo -quasi || (matrix -dim 1 -ib 3 -ob 4 | matrix -dim 2 -ib 2 -ob 2 | matrix -dim 3 -ib 1 -ob 2 | arctic -dim 2 -ib 2 -ob 2) || (if duplicating then fail else (bounds -rt || bounds -rt -qc))[1] || poly -ib 2 -ob 4 -nl2 -heuristic 1 || fail )[5]*);shift -lstar);(rule_labeling | rule_labeling -left)?;decreasing else fail)! || (if left-linear then (cr -dup;(( lpo -quasi || (matrix -dim 1 -ib 3 -ob 4 | matrix -dim 2 -ib 2 -ob 2 | matrix -dim 3 -ib 1 -ob 2 | arctic -dim 2 -ib 2 -ob 2) || (if duplicating then fail else (bounds -rt || bounds -rt -qc))[1] || poly -ib 2 -ob 4 -nl2 -heuristic 1 || fail )[5]*);shift -lstar);(rule_labeling | rule_labeling -left)?;decreasing else fail)! || (cr -cpcs2 -cpcscert; ((( matrix -dim 1 -ib 3 -ob 5 | matrix -dim 2 -ib 2 -ob 3 | matrix -dim 3 -ib 1 -ob 1 | matrix -dim 3 -ib 1 -ob 3 | fail)[2]*);((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])! || (rev;((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])!)))))!) || (( (nonconfluence -steps 0 -tcap -fun | nonconfluence -steps 2 -tcap -fun | nonconfluence -steps 25 -width 1 -tcap -fun) || (nonconfluence -steps 2 -tcap -var | nonconfluence -steps 25 -width 1 -tcap -var) || (nonconfluence -steps 0 -tree -cert -fun | nonconfluence -steps 0 -tree -cert -var | nonconfluence -steps 1 -tree -cert -fun | nonconfluence -steps 1 -tree -cert -var | nonconfluence -steps 2 -tree -cert -fun | nonconfluence -steps 2 -tree -cert -var | nonconfluence -steps 25 -tree -cert -fun | nonconfluence -steps 25 -tree -cert -var) )[6] | ((cr -m -1 -force);(redundant -narrowfwd -narrowbwd -size 7)))3*! || (((cr -m -1 -force);(redundant -remove 4)); ((cr -kb;((( matrix -dim 1 -ib 3 -ob 5 | matrix -dim 2 -ib 2 -ob 3 | matrix -dim 3 -ib 1 -ob 1 | matrix -dim 3 -ib 1 -ob 3 | fail)[2]*);((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])! || (rev;((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])!)))))! || ((if linear then cr -closed -m -1;closed -strongly 7 else fail) || (if left-linear then cr -closed -m -1;(closed -development) else fail))! || (if linear then (cr -dup;(( lpo -quasi || (matrix -dim 1 -ib 3 -ob 4 | matrix -dim 2 -ib 2 -ob 2 | matrix -dim 3 -ib 1 -ob 2 | arctic -dim 2 -ib 2 -ob 2) || (if duplicating then fail else (bounds -rt || bounds -rt -qc))[1] || poly -ib 2 -ob 4 -nl2 -heuristic 1 || fail )[5]*);shift -lstar);(rule_labeling | rule_labeling -left)?;decreasing else fail)! || (if left-linear then (cr -dup;(( lpo -quasi || (matrix -dim 1 -ib 3 -ob 4 | matrix -dim 2 -ib 2 -ob 2 | matrix -dim 3 -ib 1 -ob 2 | arctic -dim 2 -ib 2 -ob 2) || (if duplicating then fail else (bounds -rt || bounds -rt -qc))[1] || poly -ib 2 -ob 4 -nl2 -heuristic 1 || fail )[5]*);shift -lstar);(rule_labeling | rule_labeling -left)?;decreasing else fail)! || (cr -cpcs2 -cpcscert; ((( matrix -dim 1 -ib 3 -ob 5 | matrix -dim 2 -ib 2 -ob 3 | matrix -dim 3 -ib 1 -ob 1 | matrix -dim 3 -ib 1 -ob 3 | fail)[2]*);((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])! || (rev;((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])!)))))!))! || (((cr -force -redundant);(redundant)); ((cr -kb;((( matrix -dim 1 -ib 3 -ob 5 | matrix -dim 2 -ib 2 -ob 3 | matrix -dim 3 -ib 1 -ob 1 | matrix -dim 3 -ib 1 -ob 3 | fail)[2]*);((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])! || (rev;((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])!)))))! || ((if linear then cr -closed -m -1;closed -strongly 7 else fail) || (if left-linear then cr -closed -m -1;(closed -development) else fail))! || (if linear then (cr -dup;(( lpo -quasi || (matrix -dim 1 -ib 3 -ob 4 | matrix -dim 2 -ib 2 -ob 2 | matrix -dim 3 -ib 1 -ob 2 | arctic -dim 2 -ib 2 -ob 2) || (if duplicating then fail else (bounds -rt || bounds -rt -qc))[1] || poly -ib 2 -ob 4 -nl2 -heuristic 1 || fail )[5]*);shift -lstar);(rule_labeling | rule_labeling -left)?;decreasing else fail)! || (if left-linear then (cr -dup;(( lpo -quasi || (matrix -dim 1 -ib 3 -ob 4 | matrix -dim 2 -ib 2 -ob 2 | matrix -dim 3 -ib 1 -ob 2 | arctic -dim 2 -ib 2 -ob 2) || (if duplicating then fail else (bounds -rt || bounds -rt -qc))[1] || poly -ib 2 -ob 4 -nl2 -heuristic 1 || fail )[5]*);shift -lstar);(rule_labeling | rule_labeling -left)?;decreasing else fail)! || (cr -cpcs2 -cpcscert; ((( matrix -dim 1 -ib 3 -ob 5 | matrix -dim 2 -ib 2 -ob 3 | matrix -dim 3 -ib 1 -ob 1 | matrix -dim 3 -ib 1 -ob 3 | fail)[2]*);((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])! || (rev;((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])!)))))!)[15]?)3*! || (((cr -m -1 -force -redundant);(redundant -rhs)); ((cr -kb;((( matrix -dim 1 -ib 3 -ob 5 | matrix -dim 2 -ib 2 -ob 3 | matrix -dim 3 -ib 1 -ob 1 | matrix -dim 3 -ib 1 -ob 3 | fail)[2]*);((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])! || (rev;((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])!)))))! || ((if linear then cr -closed -m -1;closed -strongly 7 else fail) || (if left-linear then cr -closed -m -1;(closed -development) else fail))! || (if linear then (cr -dup;(( lpo -quasi || (matrix -dim 1 -ib 3 -ob 4 | matrix -dim 2 -ib 2 -ob 2 | matrix -dim 3 -ib 1 -ob 2 | arctic -dim 2 -ib 2 -ob 2) || (if duplicating then fail else (bounds -rt || bounds -rt -qc))[1] || poly -ib 2 -ob 4 -nl2 -heuristic 1 || fail )[5]*);shift -lstar);(rule_labeling | rule_labeling -left)?;decreasing else fail)! || (if left-linear then (cr -dup;(( lpo -quasi || (matrix -dim 1 -ib 3 -ob 4 | matrix -dim 2 -ib 2 -ob 2 | matrix -dim 3 -ib 1 -ob 2 | arctic -dim 2 -ib 2 -ob 2) || (if duplicating then fail else (bounds -rt || bounds -rt -qc))[1] || poly -ib 2 -ob 4 -nl2 -heuristic 1 || fail )[5]*);shift -lstar);(rule_labeling | rule_labeling -left)?;decreasing else fail)! || (cr -cpcs2 -cpcscert; ((( matrix -dim 1 -ib 3 -ob 5 | matrix -dim 2 -ib 2 -ob 3 | matrix -dim 3 -ib 1 -ob 1 | matrix -dim 3 -ib 1 -ob 3 | fail)[2]*);((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])! || (rev;((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])!)))))!)[15]?)3*! ))[54]