6.81/3.42	YES
6.81/3.42	<?xml version="1.0"?><?xml-stylesheet type="text/xsl" href="cpfHTML.xsl"?>
6.81/3.42	<certificationProblem>
6.81/3.42	 <input>
6.81/3.42	  <ctrsInput>
6.81/3.42	   <conditionalRules>
6.81/3.42	    <conditionalRule>
6.81/3.42	     <rule>
6.81/3.42	      <lhs>
6.81/3.42	       <funapp>
6.81/3.42	        <name>f</name>
6.81/3.42	        <arg>
6.81/3.42	         <var>x</var>
6.81/3.42	        </arg>
6.81/3.42	        <arg>
6.81/3.42	         <var>y</var>
6.81/3.42	        </arg>
6.81/3.42	       </funapp>
6.81/3.42	      </lhs>
6.81/3.42	      <rhs>
6.81/3.42	       <funapp>
6.81/3.42	        <name>g</name>
6.81/3.42	        <arg>
6.81/3.42	         <funapp>
6.81/3.42	          <name>s</name>
6.81/3.42	          <arg>
6.81/3.42	           <var>x</var>
6.81/3.42	          </arg>
6.81/3.42	         </funapp>
6.81/3.42	        </arg>
6.81/3.42	       </funapp>
6.81/3.42	      </rhs>
6.81/3.42	     </rule>
6.81/3.42	     <rule>
6.81/3.42	      <lhs>
6.81/3.42	       <funapp>
6.81/3.42	        <name>c</name>
6.81/3.42	        <arg>
6.81/3.42	         <funapp>
6.81/3.42	          <name>g</name>
6.81/3.42	          <arg>
6.81/3.42	           <var>x</var>
6.81/3.42	          </arg>
6.81/3.42	         </funapp>
6.81/3.42	        </arg>
6.81/3.42	       </funapp>
6.81/3.42	      </lhs>
6.81/3.42	      <rhs>
6.81/3.42	       <funapp>
6.81/3.42	        <name>c</name>
6.81/3.42	        <arg>
6.81/3.42	         <funapp>
6.81/3.42	          <name>a</name>
6.81/3.42	         </funapp>
6.81/3.42	        </arg>
6.81/3.42	       </funapp>
6.81/3.42	      </rhs>
6.81/3.42	     </rule>
6.81/3.42	    </conditionalRule>
6.81/3.42	    <conditionalRule>
6.81/3.42	     <rule>
6.81/3.42	      <lhs>
6.81/3.42	       <funapp>
6.81/3.42	        <name>f</name>
6.81/3.42	        <arg>
6.81/3.42	         <var>x</var>
6.81/3.42	        </arg>
6.81/3.42	        <arg>
6.81/3.42	         <var>y</var>
6.81/3.42	        </arg>
6.81/3.42	       </funapp>
6.81/3.42	      </lhs>
6.81/3.42	      <rhs>
6.81/3.42	       <funapp>
6.81/3.42	        <name>h</name>
6.81/3.42	        <arg>
6.81/3.42	         <funapp>
6.81/3.42	          <name>s</name>
6.81/3.42	          <arg>
6.81/3.42	           <var>x</var>
6.81/3.42	          </arg>
6.81/3.42	         </funapp>
6.81/3.42	        </arg>
6.81/3.42	       </funapp>
6.81/3.42	      </rhs>
6.81/3.42	     </rule>
6.81/3.42	     <rule>
6.81/3.42	      <lhs>
6.81/3.42	       <funapp>
6.81/3.42	        <name>c</name>
6.81/3.42	        <arg>
6.81/3.42	         <funapp>
6.81/3.42	          <name>h</name>
6.81/3.42	          <arg>
6.81/3.42	           <var>x</var>
6.81/3.42	          </arg>
6.81/3.42	         </funapp>
6.81/3.42	        </arg>
6.81/3.42	       </funapp>
6.81/3.42	      </lhs>
6.81/3.42	      <rhs>
6.81/3.42	       <funapp>
6.81/3.42	        <name>c</name>
6.81/3.42	        <arg>
6.81/3.42	         <funapp>
6.81/3.42	          <name>a</name>
6.81/3.42	         </funapp>
6.81/3.42	        </arg>
6.81/3.42	       </funapp>
6.81/3.42	      </rhs>
6.81/3.42	     </rule>
6.81/3.42	    </conditionalRule>
6.81/3.42	    <conditionalRule>
6.81/3.42	     <rule>
6.81/3.42	      <lhs>
6.81/3.42	       <funapp>
6.81/3.42	        <name>g</name>
6.81/3.42	        <arg>
6.81/3.42	         <funapp>
6.81/3.42	          <name>s</name>
6.81/3.42	          <arg>
6.81/3.42	           <var>x</var>
6.81/3.42	          </arg>
6.81/3.42	         </funapp>
6.81/3.42	        </arg>
6.81/3.42	       </funapp>
6.81/3.42	      </lhs>
6.81/3.42	      <rhs>
6.81/3.42	       <var>x</var>
6.81/3.42	      </rhs>
6.81/3.42	     </rule>
6.81/3.42	    </conditionalRule>
6.81/3.42	    <conditionalRule>
6.81/3.42	     <rule>
6.81/3.42	      <lhs>
6.81/3.42	       <funapp>
6.81/3.42	        <name>h</name>
6.81/3.42	        <arg>
6.81/3.42	         <funapp>
6.81/3.42	          <name>s</name>
6.81/3.42	          <arg>
6.81/3.42	           <var>x</var>
6.81/3.42	          </arg>
6.81/3.42	         </funapp>
6.81/3.42	        </arg>
6.81/3.42	       </funapp>
6.81/3.42	      </lhs>
6.81/3.42	      <rhs>
6.81/3.42	       <var>x</var>
6.81/3.42	      </rhs>
6.81/3.42	     </rule>
6.81/3.42	    </conditionalRule>
6.81/3.42	   </conditionalRules>
6.81/3.42	  </ctrsInput>
6.81/3.42	 </input>
6.81/3.42	 <cpfVersion>2.4</cpfVersion>
6.81/3.42	 <proof>
6.81/3.42	  <conditionalCrProof>
6.81/3.42	   <al94>
6.81/3.42	    <quasiReductiveProof>
6.81/3.42	     <unraveling>
6.81/3.42	      <unravelingInformation>
6.81/3.42	       <unravelingEntry>
6.81/3.42	        <conditionalRule>
6.81/3.42	         <rule>
6.81/3.42	          <lhs>
6.81/3.42	           <funapp>
6.81/3.42	            <name>f</name>
6.81/3.42	            <arg>
6.81/3.42	             <var>x</var>
6.81/3.42	            </arg>
6.81/3.42	            <arg>
6.81/3.42	             <var>y</var>
6.81/3.42	            </arg>
6.81/3.42	           </funapp>
6.81/3.42	          </lhs>
6.81/3.42	          <rhs>
6.81/3.42	           <funapp>
6.81/3.42	            <name>g</name>
6.81/3.42	            <arg>
6.81/3.42	             <funapp>
6.81/3.42	              <name>s</name>
6.81/3.42	              <arg>
6.81/3.42	               <var>x</var>
6.81/3.42	              </arg>
6.81/3.42	             </funapp>
6.81/3.42	            </arg>
6.81/3.42	           </funapp>
6.81/3.42	          </rhs>
6.81/3.42	         </rule>
6.81/3.42	         <rule>
6.81/3.42	          <lhs>
6.81/3.42	           <funapp>
6.81/3.42	            <name>c</name>
6.81/3.42	            <arg>
6.81/3.42	             <funapp>
6.81/3.42	              <name>g</name>
6.81/3.42	              <arg>
6.81/3.42	               <var>x</var>
6.81/3.42	              </arg>
6.81/3.42	             </funapp>
6.81/3.42	            </arg>
6.81/3.42	           </funapp>
6.81/3.42	          </lhs>
6.81/3.42	          <rhs>
6.81/3.42	           <funapp>
6.81/3.42	            <name>c</name>
6.81/3.42	            <arg>
6.81/3.42	             <funapp>
6.81/3.42	              <name>a</name>
6.81/3.42	             </funapp>
6.81/3.42	            </arg>
6.81/3.42	           </funapp>
6.81/3.42	          </rhs>
6.81/3.42	         </rule>
6.81/3.42	        </conditionalRule>
6.81/3.42	        <rule>
6.81/3.42	         <lhs>
6.81/3.42	          <funapp>
6.81/3.42	           <name>f</name>
6.81/3.42	           <arg>
6.81/3.42	            <var>x</var>
6.81/3.42	           </arg>
6.81/3.42	           <arg>
6.81/3.42	            <var>y</var>
6.81/3.42	           </arg>
6.81/3.42	          </funapp>
6.81/3.42	         </lhs>
6.81/3.42	         <rhs>
6.81/3.42	          <funapp>
6.81/3.42	           <name>U1</name>
6.81/3.42	           <arg>
6.81/3.42	            <funapp>
6.81/3.42	             <name>c</name>
6.81/3.42	             <arg>
6.81/3.42	              <funapp>
6.81/3.42	               <name>g</name>
6.81/3.42	               <arg>
6.81/3.42	                <var>x</var>
6.81/3.42	               </arg>
6.81/3.42	              </funapp>
6.81/3.42	             </arg>
6.81/3.42	            </funapp>
6.81/3.42	           </arg>
6.81/3.42	           <arg>
6.81/3.42	            <var>x</var>
6.81/3.42	           </arg>
6.81/3.42	           <arg>
6.81/3.42	            <var>y</var>
6.81/3.42	           </arg>
6.81/3.42	          </funapp>
6.81/3.42	         </rhs>
6.81/3.42	        </rule>
6.81/3.42	        <rule>
6.81/3.42	         <lhs>
6.81/3.42	          <funapp>
6.81/3.42	           <name>U1</name>
6.81/3.42	           <arg>
6.81/3.42	            <funapp>
6.81/3.42	             <name>c</name>
6.81/3.42	             <arg>
6.81/3.42	              <funapp>
6.81/3.42	               <name>a</name>
6.81/3.42	              </funapp>
6.81/3.42	             </arg>
6.81/3.42	            </funapp>
6.81/3.42	           </arg>
6.81/3.42	           <arg>
6.81/3.42	            <var>x</var>
6.81/3.42	           </arg>
6.81/3.42	           <arg>
6.81/3.42	            <var>y</var>
6.81/3.42	           </arg>
6.81/3.42	          </funapp>
6.81/3.42	         </lhs>
6.81/3.42	         <rhs>
6.81/3.42	          <funapp>
6.81/3.42	           <name>g</name>
6.81/3.42	           <arg>
6.81/3.42	            <funapp>
6.81/3.42	             <name>s</name>
6.81/3.42	             <arg>
6.81/3.42	              <var>x</var>
6.81/3.42	             </arg>
6.81/3.42	            </funapp>
6.81/3.42	           </arg>
6.81/3.42	          </funapp>
6.81/3.42	         </rhs>
6.81/3.42	        </rule>
6.81/3.42	       </unravelingEntry>
6.81/3.42	       <unravelingEntry>
6.81/3.42	        <conditionalRule>
6.81/3.42	         <rule>
6.81/3.42	          <lhs>
6.81/3.42	           <funapp>
6.81/3.42	            <name>f</name>
6.81/3.42	            <arg>
6.81/3.42	             <var>x</var>
6.81/3.42	            </arg>
6.81/3.42	            <arg>
6.81/3.42	             <var>y</var>
6.81/3.42	            </arg>
6.81/3.42	           </funapp>
6.81/3.42	          </lhs>
6.81/3.42	          <rhs>
6.81/3.42	           <funapp>
6.81/3.42	            <name>h</name>
6.81/3.42	            <arg>
6.81/3.42	             <funapp>
6.81/3.42	              <name>s</name>
6.81/3.42	              <arg>
6.81/3.42	               <var>x</var>
6.81/3.42	              </arg>
6.81/3.42	             </funapp>
6.81/3.42	            </arg>
6.81/3.42	           </funapp>
6.81/3.42	          </rhs>
6.81/3.42	         </rule>
6.81/3.42	         <rule>
6.81/3.42	          <lhs>
6.81/3.42	           <funapp>
6.81/3.42	            <name>c</name>
6.81/3.42	            <arg>
6.81/3.42	             <funapp>
6.81/3.42	              <name>h</name>
6.81/3.42	              <arg>
6.81/3.42	               <var>x</var>
6.81/3.42	              </arg>
6.81/3.42	             </funapp>
6.81/3.42	            </arg>
6.81/3.42	           </funapp>
6.81/3.42	          </lhs>
6.81/3.42	          <rhs>
6.81/3.42	           <funapp>
6.81/3.42	            <name>c</name>
6.81/3.42	            <arg>
6.81/3.42	             <funapp>
6.81/3.42	              <name>a</name>
6.81/3.42	             </funapp>
6.81/3.42	            </arg>
6.81/3.42	           </funapp>
6.81/3.42	          </rhs>
6.81/3.42	         </rule>
6.81/3.42	        </conditionalRule>
6.81/3.42	        <rule>
6.81/3.42	         <lhs>
6.81/3.42	          <funapp>
6.81/3.42	           <name>f</name>
6.81/3.42	           <arg>
6.81/3.42	            <var>x</var>
6.81/3.42	           </arg>
6.81/3.42	           <arg>
6.81/3.42	            <var>y</var>
6.81/3.42	           </arg>
6.81/3.42	          </funapp>
6.81/3.42	         </lhs>
6.81/3.42	         <rhs>
6.81/3.42	          <funapp>
6.81/3.42	           <name>U2</name>
6.81/3.42	           <arg>
6.81/3.42	            <funapp>
6.81/3.42	             <name>c</name>
6.81/3.42	             <arg>
6.81/3.42	              <funapp>
6.81/3.42	               <name>h</name>
6.81/3.42	               <arg>
6.81/3.42	                <var>x</var>
6.81/3.42	               </arg>
6.81/3.42	              </funapp>
6.81/3.42	             </arg>
6.81/3.42	            </funapp>
6.81/3.42	           </arg>
6.81/3.42	           <arg>
6.81/3.42	            <var>x</var>
6.81/3.42	           </arg>
6.81/3.42	           <arg>
6.81/3.42	            <var>y</var>
6.81/3.42	           </arg>
6.81/3.42	          </funapp>
6.81/3.42	         </rhs>
6.81/3.42	        </rule>
6.81/3.42	        <rule>
6.81/3.42	         <lhs>
6.81/3.42	          <funapp>
6.81/3.42	           <name>U2</name>
6.81/3.42	           <arg>
6.81/3.42	            <funapp>
6.81/3.42	             <name>c</name>
6.81/3.42	             <arg>
6.81/3.42	              <funapp>
6.81/3.42	               <name>a</name>
6.81/3.42	              </funapp>
6.81/3.42	             </arg>
6.81/3.42	            </funapp>
6.81/3.42	           </arg>
6.81/3.42	           <arg>
6.81/3.42	            <var>x</var>
6.81/3.42	           </arg>
6.81/3.42	           <arg>
6.81/3.42	            <var>y</var>
6.81/3.42	           </arg>
6.81/3.42	          </funapp>
6.81/3.42	         </lhs>
6.81/3.42	         <rhs>
6.81/3.42	          <funapp>
6.81/3.42	           <name>h</name>
6.81/3.42	           <arg>
6.81/3.42	            <funapp>
6.81/3.42	             <name>s</name>
6.81/3.42	             <arg>
6.81/3.42	              <var>x</var>
6.81/3.42	             </arg>
6.81/3.42	            </funapp>
6.81/3.42	           </arg>
6.81/3.42	          </funapp>
6.81/3.42	         </rhs>
6.81/3.42	        </rule>
6.81/3.42	       </unravelingEntry>
6.81/3.42	       <unravelingEntry>
6.81/3.42	        <conditionalRule>
6.81/3.42	         <rule>
6.81/3.42	          <lhs>
6.81/3.42	           <funapp>
6.81/3.42	            <name>g</name>
6.81/3.42	            <arg>
6.81/3.42	             <funapp>
6.81/3.42	              <name>s</name>
6.81/3.42	              <arg>
6.81/3.42	               <var>x</var>
6.81/3.42	              </arg>
6.81/3.42	             </funapp>
6.81/3.42	            </arg>
6.81/3.42	           </funapp>
6.81/3.42	          </lhs>
6.81/3.42	          <rhs>
6.81/3.42	           <var>x</var>
6.81/3.42	          </rhs>
6.81/3.42	         </rule>
6.81/3.42	        </conditionalRule>
6.81/3.42	        <rule>
6.81/3.42	         <lhs>
6.81/3.42	          <funapp>
6.81/3.42	           <name>g</name>
6.81/3.42	           <arg>
6.81/3.42	            <funapp>
6.81/3.42	             <name>s</name>
6.81/3.42	             <arg>
6.81/3.42	              <var>x</var>
6.81/3.42	             </arg>
6.81/3.42	            </funapp>
6.81/3.42	           </arg>
6.81/3.42	          </funapp>
6.81/3.42	         </lhs>
6.81/3.42	         <rhs>
6.81/3.42	          <var>x</var>
6.81/3.42	         </rhs>
6.81/3.42	        </rule>
6.81/3.42	       </unravelingEntry>
6.81/3.42	       <unravelingEntry>
6.81/3.42	        <conditionalRule>
6.81/3.42	         <rule>
6.81/3.42	          <lhs>
6.81/3.42	           <funapp>
6.81/3.42	            <name>h</name>
6.81/3.42	            <arg>
6.81/3.42	             <funapp>
6.81/3.42	              <name>s</name>
6.81/3.42	              <arg>
6.81/3.42	               <var>x</var>
6.81/3.42	              </arg>
6.81/3.42	             </funapp>
6.81/3.42	            </arg>
6.81/3.42	           </funapp>
6.81/3.42	          </lhs>
6.81/3.42	          <rhs>
6.81/3.42	           <var>x</var>
6.81/3.42	          </rhs>
6.81/3.42	         </rule>
6.81/3.42	        </conditionalRule>
6.81/3.42	        <rule>
6.81/3.42	         <lhs>
6.81/3.42	          <funapp>
6.81/3.42	           <name>h</name>
6.81/3.42	           <arg>
6.81/3.42	            <funapp>
6.81/3.42	             <name>s</name>
6.81/3.42	             <arg>
6.81/3.42	              <var>x</var>
6.81/3.42	             </arg>
6.81/3.42	            </funapp>
6.81/3.42	           </arg>
6.81/3.42	          </funapp>
6.81/3.42	         </lhs>
6.81/3.42	         <rhs>
6.81/3.42	          <var>x</var>
6.81/3.42	         </rhs>
6.81/3.42	        </rule>
6.81/3.42	       </unravelingEntry>
6.81/3.42	      </unravelingInformation>
6.81/3.42	      <trsTerminationProof>
6.81/3.42	       <ruleRemoval>
6.81/3.42	        <orderingConstraintProof>
6.81/3.42	         <redPair>
6.81/3.42	          <interpretation>
6.81/3.42	           <type>
6.81/3.42	            <polynomial>
6.81/3.42	             <domain>
6.81/3.42	              <naturals/>
6.81/3.42	             </domain>
6.81/3.42	             <degree>1</degree>
6.81/3.42	            </polynomial>
6.81/3.42	           </type>
6.81/3.42	           <interpret>
6.81/3.42	            <name>U2</name>
6.81/3.42	            <arity>3</arity>
6.81/3.42	            <polynomial>
6.81/3.42	             <sum>
6.81/3.42	              <polynomial>
6.81/3.42	               <product>
6.81/3.42	                <polynomial>
6.81/3.42	                 <coefficient>
6.81/3.42	                  <integer>2</integer>
6.81/3.42	                 </coefficient>
6.81/3.42	                </polynomial>
6.81/3.42	                <polynomial>
6.81/3.42	                 <variable>1</variable>
6.81/3.42	                </polynomial>
6.81/3.42	               </product>
6.81/3.42	              </polynomial>
6.81/3.42	              <polynomial>
6.81/3.42	               <product>
6.81/3.42	                <polynomial>
6.81/3.42	                 <coefficient>
6.81/3.42	                  <integer>2</integer>
6.81/3.42	                 </coefficient>
6.81/3.42	                </polynomial>
6.81/3.42	                <polynomial>
6.81/3.42	                 <variable>2</variable>
6.81/3.42	                </polynomial>
6.81/3.42	               </product>
6.81/3.42	              </polynomial>
6.81/3.42	              <polynomial>
6.81/3.42	               <product>
6.81/3.42	                <polynomial>
6.81/3.42	                 <coefficient>
6.81/3.42	                  <integer>10</integer>
6.81/3.42	                 </coefficient>
6.81/3.42	                </polynomial>
6.81/3.42	                <polynomial>
6.81/3.42	                 <variable>3</variable>
6.81/3.42	                </polynomial>
6.81/3.42	               </product>
6.81/3.42	              </polynomial>
6.81/3.42	              <polynomial>
6.81/3.42	               <coefficient>
6.81/3.42	                <integer>0</integer>
6.81/3.42	               </coefficient>
6.81/3.42	              </polynomial>
6.81/3.42	             </sum>
6.81/3.42	            </polynomial>
6.81/3.42	           </interpret>
6.81/3.42	           <interpret>
6.81/3.42	            <name>h</name>
6.81/3.42	            <arity>1</arity>
6.81/3.42	            <polynomial>
6.81/3.42	             <sum>
6.81/3.42	              <polynomial>
6.81/3.42	               <product>
6.81/3.42	                <polynomial>
6.81/3.42	                 <coefficient>
6.81/3.42	                  <integer>2</integer>
6.81/3.42	                 </coefficient>
6.81/3.42	                </polynomial>
6.81/3.42	                <polynomial>
6.81/3.42	                 <variable>1</variable>
6.81/3.42	                </polynomial>
6.81/3.42	               </product>
6.81/3.42	              </polynomial>
6.81/3.42	              <polynomial>
6.81/3.42	               <coefficient>
6.81/3.42	                <integer>6</integer>
6.81/3.42	               </coefficient>
6.81/3.42	              </polynomial>
6.81/3.42	             </sum>
6.81/3.42	            </polynomial>
6.81/3.42	           </interpret>
6.81/3.42	           <interpret>
6.81/3.42	            <name>s</name>
6.81/3.42	            <arity>1</arity>
6.81/3.42	            <polynomial>
6.81/3.42	             <sum>
6.81/3.42	              <polynomial>
6.81/3.42	               <product>
6.81/3.42	                <polynomial>
6.81/3.42	                 <coefficient>
6.81/3.42	                  <integer>1</integer>
6.81/3.42	                 </coefficient>
6.81/3.42	                </polynomial>
6.81/3.42	                <polynomial>
6.81/3.42	                 <variable>1</variable>
6.81/3.42	                </polynomial>
6.81/3.42	               </product>
6.81/3.42	              </polynomial>
6.81/3.42	              <polynomial>
6.81/3.42	               <coefficient>
6.81/3.42	                <integer>29</integer>
6.81/3.42	               </coefficient>
6.81/3.42	              </polynomial>
6.81/3.42	             </sum>
6.81/3.42	            </polynomial>
6.81/3.42	           </interpret>
6.81/3.42	           <interpret>
6.81/3.42	            <name>a</name>
6.81/3.42	            <arity>0</arity>
6.81/3.42	            <polynomial>
6.81/3.42	             <sum>
6.81/3.42	              <polynomial>
6.81/3.42	               <coefficient>
6.81/3.42	                <integer>19</integer>
6.81/3.42	               </coefficient>
6.81/3.42	              </polynomial>
6.81/3.42	             </sum>
6.81/3.42	            </polynomial>
6.81/3.42	           </interpret>
6.81/3.42	           <interpret>
6.81/3.42	            <name>U1</name>
6.81/3.42	            <arity>3</arity>
6.81/3.42	            <polynomial>
6.81/3.42	             <sum>
6.81/3.42	              <polynomial>
6.81/3.42	               <product>
6.81/3.42	                <polynomial>
6.81/3.42	                 <coefficient>
6.81/3.42	                  <integer>2</integer>
6.81/3.42	                 </coefficient>
6.81/3.42	                </polynomial>
6.81/3.42	                <polynomial>
6.81/3.42	                 <variable>1</variable>
6.81/3.42	                </polynomial>
6.81/3.42	               </product>
6.81/3.42	              </polynomial>
6.81/3.42	              <polynomial>
6.81/3.42	               <product>
6.81/3.42	                <polynomial>
6.81/3.42	                 <coefficient>
6.81/3.42	                  <integer>2</integer>
6.81/3.42	                 </coefficient>
6.81/3.42	                </polynomial>
6.81/3.42	                <polynomial>
6.81/3.42	                 <variable>2</variable>
6.81/3.42	                </polynomial>
6.81/3.42	               </product>
6.81/3.42	              </polynomial>
6.81/3.42	              <polynomial>
6.81/3.42	               <product>
6.81/3.42	                <polynomial>
6.81/3.42	                 <coefficient>
6.81/3.42	                  <integer>4</integer>
6.81/3.42	                 </coefficient>
6.81/3.42	                </polynomial>
6.81/3.42	                <polynomial>
6.81/3.42	                 <variable>3</variable>
6.81/3.42	                </polynomial>
6.81/3.42	               </product>
6.81/3.42	              </polynomial>
6.81/3.42	              <polynomial>
6.81/3.42	               <coefficient>
6.81/3.42	                <integer>16</integer>
6.81/3.42	               </coefficient>
6.81/3.42	              </polynomial>
6.81/3.42	             </sum>
6.81/3.42	            </polynomial>
6.81/3.42	           </interpret>
6.81/3.42	           <interpret>
6.81/3.42	            <name>c</name>
6.81/3.42	            <arity>1</arity>
6.81/3.42	            <polynomial>
6.81/3.42	             <sum>
6.81/3.42	              <polynomial>
6.81/3.42	               <product>
6.81/3.42	                <polynomial>
6.81/3.42	                 <coefficient>
6.81/3.42	                  <integer>2</integer>
6.81/3.42	                 </coefficient>
6.81/3.42	                </polynomial>
6.81/3.42	                <polynomial>
6.81/3.42	                 <variable>1</variable>
6.81/3.42	                </polynomial>
6.81/3.42	               </product>
6.81/3.42	              </polynomial>
6.81/3.42	              <polynomial>
6.81/3.42	               <coefficient>
6.81/3.42	                <integer>2</integer>
6.81/3.42	               </coefficient>
6.81/3.42	              </polynomial>
6.81/3.42	             </sum>
6.81/3.42	            </polynomial>
6.81/3.42	           </interpret>
6.81/3.42	           <interpret>
6.81/3.42	            <name>g</name>
6.81/3.42	            <arity>1</arity>
6.81/3.42	            <polynomial>
6.81/3.42	             <sum>
6.81/3.42	              <polynomial>
6.81/3.42	               <product>
6.81/3.42	                <polynomial>
6.81/3.42	                 <coefficient>
6.81/3.42	                  <integer>2</integer>
6.81/3.42	                 </coefficient>
6.81/3.42	                </polynomial>
6.81/3.42	                <polynomial>
6.81/3.42	                 <variable>1</variable>
6.81/3.42	                </polynomial>
6.81/3.42	               </product>
6.81/3.42	              </polynomial>
6.81/3.42	              <polynomial>
6.81/3.42	               <coefficient>
6.81/3.42	                <integer>2</integer>
6.81/3.42	               </coefficient>
6.81/3.42	              </polynomial>
6.81/3.42	             </sum>
6.81/3.42	            </polynomial>
6.81/3.42	           </interpret>
6.81/3.42	           <interpret>
6.81/3.42	            <name>f</name>
6.81/3.42	            <arity>2</arity>
6.81/3.42	            <polynomial>
6.81/3.42	             <sum>
6.81/3.42	              <polynomial>
6.81/3.42	               <product>
6.81/3.42	                <polynomial>
6.81/3.42	                 <coefficient>
6.81/3.42	                  <integer>10</integer>
6.81/3.42	                 </coefficient>
6.81/3.42	                </polynomial>
6.81/3.42	                <polynomial>
6.81/3.42	                 <variable>1</variable>
6.81/3.42	                </polynomial>
6.81/3.42	               </product>
6.81/3.42	              </polynomial>
6.81/3.42	              <polynomial>
6.81/3.42	               <product>
6.81/3.42	                <polynomial>
6.81/3.42	                 <coefficient>
6.81/3.42	                  <integer>10</integer>
6.81/3.42	                 </coefficient>
6.81/3.42	                </polynomial>
6.81/3.42	                <polynomial>
6.81/3.42	                 <variable>2</variable>
6.81/3.42	                </polynomial>
6.81/3.42	               </product>
6.81/3.42	              </polynomial>
6.81/3.42	              <polynomial>
6.81/3.42	               <coefficient>
6.81/3.42	                <integer>28</integer>
6.81/3.42	               </coefficient>
6.81/3.42	              </polynomial>
6.81/3.42	             </sum>
6.81/3.42	            </polynomial>
6.81/3.42	           </interpret>
6.81/3.42	          </interpretation>
6.81/3.42	         </redPair>
6.81/3.42	        </orderingConstraintProof>
6.81/3.42	        <trs>
6.81/3.42	         <rules>
6.81/3.42	          <rule>
6.81/3.42	           <lhs>
6.81/3.42	            <funapp>
6.81/3.42	             <name>f</name>
6.81/3.42	             <arg>
6.81/3.42	              <var>x</var>
6.81/3.42	             </arg>
6.81/3.42	             <arg>
6.81/3.42	              <var>y</var>
6.81/3.42	             </arg>
6.81/3.42	            </funapp>
6.81/3.42	           </lhs>
6.81/3.42	           <rhs>
6.81/3.42	            <funapp>
6.81/3.42	             <name>U1</name>
6.81/3.42	             <arg>
6.81/3.42	              <funapp>
6.81/3.42	               <name>c</name>
6.81/3.42	               <arg>
6.81/3.42	                <funapp>
6.81/3.42	                 <name>g</name>
6.81/3.42	                 <arg>
6.81/3.42	                  <var>x</var>
6.81/3.42	                 </arg>
6.81/3.42	                </funapp>
6.81/3.42	               </arg>
6.81/3.42	              </funapp>
6.81/3.42	             </arg>
6.81/3.42	             <arg>
6.81/3.42	              <var>x</var>
6.81/3.42	             </arg>
6.81/3.42	             <arg>
6.81/3.42	              <var>y</var>
6.81/3.42	             </arg>
6.81/3.42	            </funapp>
6.81/3.42	           </rhs>
6.81/3.42	          </rule>
6.81/3.42	          <rule>
6.81/3.42	           <lhs>
6.81/3.42	            <funapp>
6.81/3.42	             <name>f</name>
6.81/3.42	             <arg>
6.81/3.42	              <var>x</var>
6.81/3.42	             </arg>
6.81/3.42	             <arg>
6.81/3.42	              <var>y</var>
6.81/3.42	             </arg>
6.81/3.42	            </funapp>
6.81/3.42	           </lhs>
6.81/3.42	           <rhs>
6.81/3.42	            <funapp>
6.81/3.42	             <name>U2</name>
6.81/3.42	             <arg>
6.81/3.42	              <funapp>
6.81/3.42	               <name>c</name>
6.81/3.42	               <arg>
6.81/3.42	                <funapp>
6.81/3.42	                 <name>h</name>
6.81/3.42	                 <arg>
6.81/3.42	                  <var>x</var>
6.81/3.42	                 </arg>
6.81/3.42	                </funapp>
6.81/3.42	               </arg>
6.81/3.42	              </funapp>
6.81/3.42	             </arg>
6.81/3.42	             <arg>
6.81/3.42	              <var>x</var>
6.81/3.42	             </arg>
6.81/3.42	             <arg>
6.81/3.42	              <var>y</var>
6.81/3.42	             </arg>
6.81/3.42	            </funapp>
6.81/3.42	           </rhs>
6.81/3.42	          </rule>
6.81/3.42	         </rules>
6.81/3.42	        </trs>
6.81/3.42	        <trsTerminationProof>
6.81/3.42	         <ruleRemoval>
6.81/3.42	          <orderingConstraintProof>
6.81/3.42	           <redPair>
6.81/3.42	            <interpretation>
6.81/3.42	             <type>
6.81/3.42	              <polynomial>
6.81/3.42	               <domain>
6.81/3.42	                <naturals/>
6.81/3.42	               </domain>
6.81/3.42	               <degree>1</degree>
6.81/3.42	              </polynomial>
6.81/3.42	             </type>
6.81/3.42	             <interpret>
6.81/3.42	              <name>U2</name>
6.81/3.42	              <arity>3</arity>
6.81/3.42	              <polynomial>
6.81/3.42	               <sum>
6.81/3.42	                <polynomial>
6.81/3.42	                 <product>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <coefficient>
6.81/3.42	                    <integer>9</integer>
6.81/3.42	                   </coefficient>
6.81/3.42	                  </polynomial>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <variable>1</variable>
6.81/3.42	                  </polynomial>
6.81/3.42	                 </product>
6.81/3.42	                </polynomial>
6.81/3.42	                <polynomial>
6.81/3.42	                 <product>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <coefficient>
6.81/3.42	                    <integer>4</integer>
6.81/3.42	                   </coefficient>
6.81/3.42	                  </polynomial>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <variable>2</variable>
6.81/3.42	                  </polynomial>
6.81/3.42	                 </product>
6.81/3.42	                </polynomial>
6.81/3.42	                <polynomial>
6.81/3.42	                 <product>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <coefficient>
6.81/3.42	                    <integer>1</integer>
6.81/3.42	                   </coefficient>
6.81/3.42	                  </polynomial>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <variable>3</variable>
6.81/3.42	                  </polynomial>
6.81/3.42	                 </product>
6.81/3.42	                </polynomial>
6.81/3.42	                <polynomial>
6.81/3.42	                 <coefficient>
6.81/3.42	                  <integer>0</integer>
6.81/3.42	                 </coefficient>
6.81/3.42	                </polynomial>
6.81/3.42	               </sum>
6.81/3.42	              </polynomial>
6.81/3.42	             </interpret>
6.81/3.42	             <interpret>
6.81/3.42	              <name>h</name>
6.81/3.42	              <arity>1</arity>
6.81/3.42	              <polynomial>
6.81/3.42	               <sum>
6.81/3.42	                <polynomial>
6.81/3.42	                 <product>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <coefficient>
6.81/3.42	                    <integer>3</integer>
6.81/3.42	                   </coefficient>
6.81/3.42	                  </polynomial>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <variable>1</variable>
6.81/3.42	                  </polynomial>
6.81/3.42	                 </product>
6.81/3.42	                </polynomial>
6.81/3.42	                <polynomial>
6.81/3.42	                 <coefficient>
6.81/3.42	                  <integer>1</integer>
6.81/3.42	                 </coefficient>
6.81/3.42	                </polynomial>
6.81/3.42	               </sum>
6.81/3.42	              </polynomial>
6.81/3.42	             </interpret>
6.81/3.42	             <interpret>
6.81/3.42	              <name>U1</name>
6.81/3.42	              <arity>3</arity>
6.81/3.42	              <polynomial>
6.81/3.42	               <sum>
6.81/3.42	                <polynomial>
6.81/3.42	                 <product>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <coefficient>
6.81/3.42	                    <integer>2</integer>
6.81/3.42	                   </coefficient>
6.81/3.42	                  </polynomial>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <variable>1</variable>
6.81/3.42	                  </polynomial>
6.81/3.42	                 </product>
6.81/3.42	                </polynomial>
6.81/3.42	                <polynomial>
6.81/3.42	                 <product>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <coefficient>
6.81/3.42	                    <integer>15</integer>
6.81/3.42	                   </coefficient>
6.81/3.42	                  </polynomial>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <variable>2</variable>
6.81/3.42	                  </polynomial>
6.81/3.42	                 </product>
6.81/3.42	                </polynomial>
6.81/3.42	                <polynomial>
6.81/3.42	                 <product>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <coefficient>
6.81/3.42	                    <integer>1</integer>
6.81/3.42	                   </coefficient>
6.81/3.42	                  </polynomial>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <variable>3</variable>
6.81/3.42	                  </polynomial>
6.81/3.42	                 </product>
6.81/3.42	                </polynomial>
6.81/3.42	                <polynomial>
6.81/3.42	                 <coefficient>
6.81/3.42	                  <integer>2</integer>
6.81/3.42	                 </coefficient>
6.81/3.42	                </polynomial>
6.81/3.42	               </sum>
6.81/3.42	              </polynomial>
6.81/3.42	             </interpret>
6.81/3.42	             <interpret>
6.81/3.42	              <name>c</name>
6.81/3.42	              <arity>1</arity>
6.81/3.42	              <polynomial>
6.81/3.42	               <sum>
6.81/3.42	                <polynomial>
6.81/3.42	                 <product>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <coefficient>
6.81/3.42	                    <integer>1</integer>
6.81/3.42	                   </coefficient>
6.81/3.42	                  </polynomial>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <variable>1</variable>
6.81/3.42	                  </polynomial>
6.81/3.42	                 </product>
6.81/3.42	                </polynomial>
6.81/3.42	                <polynomial>
6.81/3.42	                 <coefficient>
6.81/3.42	                  <integer>2</integer>
6.81/3.42	                 </coefficient>
6.81/3.42	                </polynomial>
6.81/3.42	               </sum>
6.81/3.42	              </polynomial>
6.81/3.42	             </interpret>
6.81/3.42	             <interpret>
6.81/3.42	              <name>g</name>
6.81/3.42	              <arity>1</arity>
6.81/3.42	              <polynomial>
6.81/3.42	               <sum>
6.81/3.42	                <polynomial>
6.81/3.42	                 <product>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <coefficient>
6.81/3.42	                    <integer>8</integer>
6.81/3.42	                   </coefficient>
6.81/3.42	                  </polynomial>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <variable>1</variable>
6.81/3.42	                  </polynomial>
6.81/3.42	                 </product>
6.81/3.42	                </polynomial>
6.81/3.42	                <polynomial>
6.81/3.42	                 <coefficient>
6.81/3.42	                  <integer>6</integer>
6.81/3.42	                 </coefficient>
6.81/3.42	                </polynomial>
6.81/3.42	               </sum>
6.81/3.42	              </polynomial>
6.81/3.42	             </interpret>
6.81/3.42	             <interpret>
6.81/3.42	              <name>f</name>
6.81/3.42	              <arity>2</arity>
6.81/3.42	              <polynomial>
6.81/3.42	               <sum>
6.81/3.42	                <polynomial>
6.81/3.42	                 <product>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <coefficient>
6.81/3.42	                    <integer>31</integer>
6.81/3.42	                   </coefficient>
6.81/3.42	                  </polynomial>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <variable>1</variable>
6.81/3.42	                  </polynomial>
6.81/3.42	                 </product>
6.81/3.42	                </polynomial>
6.81/3.42	                <polynomial>
6.81/3.42	                 <product>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <coefficient>
6.81/3.42	                    <integer>1</integer>
6.81/3.42	                   </coefficient>
6.81/3.42	                  </polynomial>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <variable>2</variable>
6.81/3.42	                  </polynomial>
6.81/3.42	                 </product>
6.81/3.42	                </polynomial>
6.81/3.42	                <polynomial>
6.81/3.42	                 <coefficient>
6.81/3.42	                  <integer>27</integer>
6.81/3.42	                 </coefficient>
6.81/3.42	                </polynomial>
6.81/3.42	               </sum>
6.81/3.42	              </polynomial>
6.81/3.42	             </interpret>
6.81/3.42	            </interpretation>
6.81/3.42	           </redPair>
6.81/3.42	          </orderingConstraintProof>
6.81/3.42	          <trs>
6.81/3.42	           <rules>
6.81/3.42	            <rule>
6.81/3.42	             <lhs>
6.81/3.42	              <funapp>
6.81/3.42	               <name>f</name>
6.81/3.42	               <arg>
6.81/3.42	                <var>x</var>
6.81/3.42	               </arg>
6.81/3.42	               <arg>
6.81/3.42	                <var>y</var>
6.81/3.42	               </arg>
6.81/3.42	              </funapp>
6.81/3.42	             </lhs>
6.81/3.42	             <rhs>
6.81/3.42	              <funapp>
6.81/3.42	               <name>U2</name>
6.81/3.42	               <arg>
6.81/3.42	                <funapp>
6.81/3.42	                 <name>c</name>
6.81/3.42	                 <arg>
6.81/3.42	                  <funapp>
6.81/3.42	                   <name>h</name>
6.81/3.42	                   <arg>
6.81/3.42	                    <var>x</var>
6.81/3.42	                   </arg>
6.81/3.42	                  </funapp>
6.81/3.42	                 </arg>
6.81/3.42	                </funapp>
6.81/3.42	               </arg>
6.81/3.42	               <arg>
6.81/3.42	                <var>x</var>
6.81/3.42	               </arg>
6.81/3.42	               <arg>
6.81/3.42	                <var>y</var>
6.81/3.42	               </arg>
6.81/3.42	              </funapp>
6.81/3.42	             </rhs>
6.81/3.42	            </rule>
6.81/3.42	           </rules>
6.81/3.42	          </trs>
6.81/3.42	          <trsTerminationProof>
6.81/3.42	           <ruleRemoval>
6.81/3.42	            <orderingConstraintProof>
6.81/3.42	             <redPair>
6.81/3.42	              <interpretation>
6.81/3.42	               <type>
6.81/3.42	                <polynomial>
6.81/3.42	                 <domain>
6.81/3.42	                  <naturals/>
6.81/3.42	                 </domain>
6.81/3.42	                 <degree>1</degree>
6.81/3.42	                </polynomial>
6.81/3.42	               </type>
6.81/3.42	               <interpret>
6.81/3.42	                <name>U2</name>
6.81/3.42	                <arity>3</arity>
6.81/3.42	                <polynomial>
6.81/3.42	                 <sum>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <product>
6.81/3.42	                    <polynomial>
6.81/3.42	                     <coefficient>
6.81/3.42	                      <integer>1</integer>
6.81/3.42	                     </coefficient>
6.81/3.42	                    </polynomial>
6.81/3.42	                    <polynomial>
6.81/3.42	                     <variable>1</variable>
6.81/3.42	                    </polynomial>
6.81/3.42	                   </product>
6.81/3.42	                  </polynomial>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <product>
6.81/3.42	                    <polynomial>
6.81/3.42	                     <coefficient>
6.81/3.42	                      <integer>6</integer>
6.81/3.42	                     </coefficient>
6.81/3.42	                    </polynomial>
6.81/3.42	                    <polynomial>
6.81/3.42	                     <variable>2</variable>
6.81/3.42	                    </polynomial>
6.81/3.42	                   </product>
6.81/3.42	                  </polynomial>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <product>
6.81/3.42	                    <polynomial>
6.81/3.42	                     <coefficient>
6.81/3.42	                      <integer>2</integer>
6.81/3.42	                     </coefficient>
6.81/3.42	                    </polynomial>
6.81/3.42	                    <polynomial>
6.81/3.42	                     <variable>3</variable>
6.81/3.42	                    </polynomial>
6.81/3.42	                   </product>
6.81/3.42	                  </polynomial>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <coefficient>
6.81/3.42	                    <integer>4</integer>
6.81/3.42	                   </coefficient>
6.81/3.42	                  </polynomial>
6.81/3.42	                 </sum>
6.81/3.42	                </polynomial>
6.81/3.42	               </interpret>
6.81/3.42	               <interpret>
6.81/3.42	                <name>h</name>
6.81/3.42	                <arity>1</arity>
6.81/3.42	                <polynomial>
6.81/3.42	                 <sum>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <product>
6.81/3.42	                    <polynomial>
6.81/3.42	                     <coefficient>
6.81/3.42	                      <integer>1</integer>
6.81/3.42	                     </coefficient>
6.81/3.42	                    </polynomial>
6.81/3.42	                    <polynomial>
6.81/3.42	                     <variable>1</variable>
6.81/3.42	                    </polynomial>
6.81/3.42	                   </product>
6.81/3.42	                  </polynomial>
6.81/3.42	                  <polynomial>
6.81/3.42	                   <coefficient>
6.81/3.43	                    <integer>0</integer>
6.81/3.43	                   </coefficient>
6.81/3.43	                  </polynomial>
6.81/3.43	                 </sum>
6.81/3.43	                </polynomial>
6.81/3.43	               </interpret>
6.81/3.43	               <interpret>
6.81/3.43	                <name>c</name>
6.81/3.43	                <arity>1</arity>
6.81/3.43	                <polynomial>
6.81/3.43	                 <sum>
6.81/3.43	                  <polynomial>
6.81/3.43	                   <product>
6.81/3.43	                    <polynomial>
6.81/3.43	                     <coefficient>
6.81/3.43	                      <integer>1</integer>
6.81/3.43	                     </coefficient>
6.81/3.43	                    </polynomial>
6.81/3.43	                    <polynomial>
6.81/3.43	                     <variable>1</variable>
6.81/3.43	                    </polynomial>
6.81/3.43	                   </product>
6.81/3.43	                  </polynomial>
6.81/3.43	                  <polynomial>
6.81/3.43	                   <coefficient>
6.81/3.43	                    <integer>4</integer>
6.81/3.43	                   </coefficient>
6.81/3.43	                  </polynomial>
6.81/3.43	                 </sum>
6.81/3.43	                </polynomial>
6.81/3.43	               </interpret>
6.81/3.43	               <interpret>
6.81/3.43	                <name>f</name>
6.81/3.43	                <arity>2</arity>
6.81/3.43	                <polynomial>
6.81/3.43	                 <sum>
6.81/3.43	                  <polynomial>
6.81/3.43	                   <product>
6.81/3.43	                    <polynomial>
6.81/3.43	                     <coefficient>
6.81/3.43	                      <integer>7</integer>
6.81/3.43	                     </coefficient>
6.81/3.43	                    </polynomial>
6.81/3.43	                    <polynomial>
6.81/3.43	                     <variable>1</variable>
6.81/3.43	                    </polynomial>
6.81/3.43	                   </product>
6.81/3.43	                  </polynomial>
6.81/3.43	                  <polynomial>
6.81/3.43	                   <product>
6.81/3.43	                    <polynomial>
6.81/3.43	                     <coefficient>
6.81/3.43	                      <integer>4</integer>
6.81/3.43	                     </coefficient>
6.81/3.43	                    </polynomial>
6.81/3.43	                    <polynomial>
6.81/3.43	                     <variable>2</variable>
6.81/3.43	                    </polynomial>
6.81/3.43	                   </product>
6.81/3.43	                  </polynomial>
6.81/3.43	                  <polynomial>
6.81/3.43	                   <coefficient>
6.81/3.43	                    <integer>16</integer>
6.81/3.43	                   </coefficient>
6.81/3.43	                  </polynomial>
6.81/3.43	                 </sum>
6.81/3.43	                </polynomial>
6.81/3.43	               </interpret>
6.81/3.43	              </interpretation>
6.81/3.43	             </redPair>
6.81/3.43	            </orderingConstraintProof>
6.81/3.43	            <trs>
6.81/3.43	             <rules/>
6.81/3.43	            </trs>
6.81/3.43	            <trsTerminationProof>
6.81/3.43	             <rIsEmpty/>
6.81/3.43	            </trsTerminationProof>
6.81/3.43	           </ruleRemoval>
6.81/3.43	          </trsTerminationProof>
6.81/3.43	         </ruleRemoval>
6.81/3.43	        </trsTerminationProof>
6.81/3.43	       </ruleRemoval>
6.81/3.43	      </trsTerminationProof>
6.81/3.43	     </unraveling>
6.81/3.43	    </quasiReductiveProof>
6.81/3.43	    <contextJoinableCCPs>
6.81/3.43	     <contextJoinableCCP>
6.81/3.43	      <funapp>
6.81/3.43	       <name>h</name>
6.81/3.43	       <arg>
6.81/3.43	        <funapp>
6.81/3.43	         <name>s</name>
6.81/3.43	         <arg>
6.81/3.43	          <var>y'</var>
6.81/3.43	         </arg>
6.81/3.43	        </funapp>
6.81/3.43	       </arg>
6.81/3.43	      </funapp>
6.81/3.43	      <funapp>
6.81/3.43	       <name>g</name>
6.81/3.43	       <arg>
6.81/3.43	        <funapp>
6.81/3.43	         <name>s</name>
6.81/3.43	         <arg>
6.81/3.43	          <var>y'</var>
6.81/3.43	         </arg>
6.81/3.43	        </funapp>
6.81/3.43	       </arg>
6.81/3.43	      </funapp>
6.81/3.43	      <rules>
6.81/3.43	       <rule>
6.81/3.43	        <lhs>
6.81/3.43	         <funapp>
6.81/3.43	          <name>c</name>
6.81/3.43	          <arg>
6.81/3.43	           <funapp>
6.81/3.43	            <name>h</name>
6.81/3.43	            <arg>
6.81/3.43	             <var>y'</var>
6.81/3.43	            </arg>
6.81/3.43	           </funapp>
6.81/3.43	          </arg>
6.81/3.43	         </funapp>
6.81/3.43	        </lhs>
6.81/3.43	        <rhs>
6.81/3.43	         <funapp>
6.81/3.43	          <name>c</name>
6.81/3.43	          <arg>
6.81/3.43	           <funapp>
6.81/3.43	            <name>a</name>
6.81/3.43	           </funapp>
6.81/3.43	          </arg>
6.81/3.43	         </funapp>
6.81/3.43	        </rhs>
6.81/3.43	       </rule>
6.81/3.43	       <rule>
6.81/3.43	        <lhs>
6.81/3.43	         <funapp>
6.81/3.43	          <name>c</name>
6.81/3.43	          <arg>
6.81/3.43	           <funapp>
6.81/3.43	            <name>g</name>
6.81/3.43	            <arg>
6.81/3.43	             <var>y'</var>
6.81/3.43	            </arg>
6.81/3.43	           </funapp>
6.81/3.43	          </arg>
6.81/3.43	         </funapp>
6.81/3.43	        </lhs>
6.81/3.43	        <rhs>
6.81/3.43	         <funapp>
6.81/3.43	          <name>c</name>
6.81/3.43	          <arg>
6.81/3.43	           <funapp>
6.81/3.43	            <name>a</name>
6.81/3.43	           </funapp>
6.81/3.43	          </arg>
6.81/3.43	         </funapp>
6.81/3.43	        </rhs>
6.81/3.43	       </rule>
6.81/3.43	      </rules>
6.81/3.43	      <contextJoinabilityProof>
6.81/3.43	       <funapp>
6.81/3.43	        <name>?1</name>
6.81/3.43	       </funapp>
6.81/3.43	       <conditionalRewritingSequence>
6.81/3.43	        <conditionalRewriteStep>
6.81/3.43	         <conditionalRule>
6.81/3.43	          <rule>
6.81/3.43	           <lhs>
6.81/3.43	            <funapp>
6.81/3.43	             <name>h</name>
6.81/3.43	             <arg>
6.81/3.43	              <funapp>
6.81/3.43	               <name>s</name>
6.81/3.43	               <arg>
6.81/3.43	                <var>x</var>
6.81/3.43	               </arg>
6.81/3.43	              </funapp>
6.81/3.43	             </arg>
6.81/3.43	            </funapp>
6.81/3.43	           </lhs>
6.81/3.43	           <rhs>
6.81/3.43	            <var>x</var>
6.81/3.43	           </rhs>
6.81/3.43	          </rule>
6.81/3.43	         </conditionalRule>
6.81/3.43	         <positionInTerm></positionInTerm>
6.81/3.43	         <substitution>
6.81/3.43	          <substEntry>
6.81/3.43	           <var>x</var>
6.81/3.43	           <funapp>
6.81/3.43	            <name>?1</name>
6.81/3.43	           </funapp>
6.81/3.43	          </substEntry>
6.81/3.43	         </substitution>
6.81/3.43	         <source>
6.81/3.43	          <funapp>
6.81/3.43	           <name>h</name>
6.81/3.43	           <arg>
6.81/3.43	            <funapp>
6.81/3.43	             <name>s</name>
6.81/3.43	             <arg>
6.81/3.43	              <funapp>
6.81/3.43	               <name>?1</name>
6.81/3.43	              </funapp>
6.81/3.43	             </arg>
6.81/3.43	            </funapp>
6.81/3.43	           </arg>
6.81/3.43	          </funapp>
6.81/3.43	         </source>
6.81/3.43	         <target>
6.81/3.43	          <funapp>
6.81/3.43	           <name>?1</name>
6.81/3.43	          </funapp>
6.81/3.43	         </target>
6.81/3.43	         <conditions> </conditions>
6.81/3.43	        </conditionalRewriteStep>
6.81/3.43	       </conditionalRewritingSequence>
6.81/3.43	       <conditionalRewritingSequence>
6.81/3.43	        <conditionalRewriteStep>
6.81/3.43	         <conditionalRule>
6.81/3.43	          <rule>
6.81/3.43	           <lhs>
6.81/3.43	            <funapp>
6.81/3.43	             <name>g</name>
6.81/3.43	             <arg>
6.81/3.43	              <funapp>
6.81/3.43	               <name>s</name>
6.81/3.43	               <arg>
6.81/3.43	                <var>x</var>
6.81/3.43	               </arg>
6.81/3.43	              </funapp>
6.81/3.43	             </arg>
6.81/3.43	            </funapp>
6.81/3.43	           </lhs>
6.81/3.43	           <rhs>
6.81/3.43	            <var>x</var>
6.81/3.43	           </rhs>
6.81/3.43	          </rule>
6.81/3.43	         </conditionalRule>
6.81/3.43	         <positionInTerm></positionInTerm>
6.81/3.43	         <substitution>
6.81/3.43	          <substEntry>
6.81/3.43	           <var>x</var>
6.81/3.43	           <funapp>
6.81/3.43	            <name>?1</name>
6.81/3.43	           </funapp>
6.81/3.43	          </substEntry>
6.81/3.43	         </substitution>
6.81/3.43	         <source>
6.81/3.43	          <funapp>
6.81/3.43	           <name>g</name>
6.81/3.43	           <arg>
6.81/3.43	            <funapp>
6.81/3.43	             <name>s</name>
6.81/3.43	             <arg>
6.81/3.43	              <funapp>
6.81/3.43	               <name>?1</name>
6.81/3.43	              </funapp>
6.81/3.43	             </arg>
6.81/3.43	            </funapp>
6.81/3.43	           </arg>
6.81/3.43	          </funapp>
6.81/3.43	         </source>
6.81/3.43	         <target>
6.81/3.43	          <funapp>
6.81/3.43	           <name>?1</name>
6.81/3.43	          </funapp>
6.81/3.43	         </target>
6.81/3.43	         <conditions> </conditions>
6.81/3.43	        </conditionalRewriteStep>
6.81/3.43	       </conditionalRewritingSequence>
6.81/3.43	       <constMap>
6.81/3.43	        <entry>
6.81/3.43	         <symbol>
6.81/3.43	          <name>?1</name>
6.81/3.43	         </symbol>
6.81/3.43	         <const>y'</const>
6.81/3.43	        </entry>
6.81/3.43	       </constMap>
6.81/3.43	      </contextJoinabilityProof>
6.81/3.43	     </contextJoinableCCP>
6.81/3.43	     <contextJoinableCCP>
6.81/3.43	      <funapp>
6.81/3.43	       <name>g</name>
6.81/3.43	       <arg>
6.81/3.43	        <funapp>
6.81/3.43	         <name>s</name>
6.81/3.43	         <arg>
6.81/3.43	          <var>y'</var>
6.81/3.43	         </arg>
6.81/3.43	        </funapp>
6.81/3.43	       </arg>
6.81/3.43	      </funapp>
6.81/3.43	      <funapp>
6.81/3.43	       <name>h</name>
6.81/3.43	       <arg>
6.81/3.43	        <funapp>
6.81/3.43	         <name>s</name>
6.81/3.43	         <arg>
6.81/3.43	          <var>y'</var>
6.81/3.43	         </arg>
6.81/3.43	        </funapp>
6.81/3.43	       </arg>
6.81/3.43	      </funapp>
6.81/3.43	      <rules>
6.81/3.43	       <rule>
6.81/3.43	        <lhs>
6.81/3.43	         <funapp>
6.81/3.43	          <name>c</name>
6.81/3.43	          <arg>
6.81/3.43	           <funapp>
6.81/3.43	            <name>g</name>
6.81/3.43	            <arg>
6.81/3.43	             <var>y'</var>
6.81/3.43	            </arg>
6.81/3.43	           </funapp>
6.81/3.43	          </arg>
6.81/3.43	         </funapp>
6.81/3.43	        </lhs>
6.81/3.43	        <rhs>
6.81/3.43	         <funapp>
6.81/3.43	          <name>c</name>
6.81/3.43	          <arg>
6.81/3.43	           <funapp>
6.81/3.43	            <name>a</name>
6.81/3.43	           </funapp>
6.81/3.43	          </arg>
6.81/3.43	         </funapp>
6.81/3.43	        </rhs>
6.81/3.43	       </rule>
6.81/3.43	       <rule>
6.81/3.43	        <lhs>
6.81/3.43	         <funapp>
6.81/3.43	          <name>c</name>
6.81/3.43	          <arg>
6.81/3.43	           <funapp>
6.81/3.43	            <name>h</name>
6.81/3.43	            <arg>
6.81/3.43	             <var>y'</var>
6.81/3.43	            </arg>
6.81/3.43	           </funapp>
6.81/3.43	          </arg>
6.81/3.43	         </funapp>
6.81/3.43	        </lhs>
6.81/3.43	        <rhs>
6.81/3.43	         <funapp>
6.81/3.43	          <name>c</name>
6.81/3.43	          <arg>
6.81/3.43	           <funapp>
6.81/3.43	            <name>a</name>
6.81/3.43	           </funapp>
6.81/3.43	          </arg>
6.81/3.43	         </funapp>
6.81/3.43	        </rhs>
6.81/3.43	       </rule>
6.81/3.43	      </rules>
6.81/3.43	      <contextJoinabilityProof>
6.81/3.43	       <funapp>
6.81/3.43	        <name>?1</name>
6.81/3.43	       </funapp>
6.81/3.43	       <conditionalRewritingSequence>
6.81/3.43	        <conditionalRewriteStep>
6.81/3.43	         <conditionalRule>
6.81/3.43	          <rule>
6.81/3.43	           <lhs>
6.81/3.43	            <funapp>
6.81/3.43	             <name>g</name>
6.81/3.43	             <arg>
6.81/3.43	              <funapp>
6.81/3.43	               <name>s</name>
6.81/3.43	               <arg>
6.81/3.43	                <var>x</var>
6.81/3.43	               </arg>
6.81/3.43	              </funapp>
6.81/3.43	             </arg>
6.81/3.43	            </funapp>
6.81/3.43	           </lhs>
6.81/3.43	           <rhs>
6.81/3.43	            <var>x</var>
6.81/3.43	           </rhs>
6.81/3.43	          </rule>
6.81/3.43	         </conditionalRule>
6.81/3.43	         <positionInTerm></positionInTerm>
6.81/3.43	         <substitution>
6.81/3.43	          <substEntry>
6.81/3.43	           <var>x</var>
6.81/3.43	           <funapp>
6.81/3.43	            <name>?1</name>
6.81/3.43	           </funapp>
6.81/3.43	          </substEntry>
6.81/3.43	         </substitution>
6.81/3.43	         <source>
6.81/3.43	          <funapp>
6.81/3.43	           <name>g</name>
6.81/3.43	           <arg>
6.81/3.43	            <funapp>
6.81/3.43	             <name>s</name>
6.81/3.43	             <arg>
6.81/3.43	              <funapp>
6.81/3.43	               <name>?1</name>
6.81/3.43	              </funapp>
6.81/3.43	             </arg>
6.81/3.43	            </funapp>
6.81/3.43	           </arg>
6.81/3.43	          </funapp>
6.81/3.43	         </source>
6.81/3.43	         <target>
6.81/3.43	          <funapp>
6.81/3.43	           <name>?1</name>
6.81/3.43	          </funapp>
6.81/3.43	         </target>
6.81/3.43	         <conditions> </conditions>
6.81/3.43	        </conditionalRewriteStep>
6.81/3.43	       </conditionalRewritingSequence>
6.81/3.43	       <conditionalRewritingSequence>
6.81/3.43	        <conditionalRewriteStep>
6.81/3.43	         <conditionalRule>
6.81/3.43	          <rule>
6.81/3.43	           <lhs>
6.81/3.43	            <funapp>
6.81/3.43	             <name>h</name>
6.81/3.43	             <arg>
6.81/3.43	              <funapp>
6.81/3.43	               <name>s</name>
6.81/3.43	               <arg>
6.81/3.43	                <var>x</var>
6.81/3.43	               </arg>
6.81/3.43	              </funapp>
6.81/3.43	             </arg>
6.81/3.43	            </funapp>
6.81/3.43	           </lhs>
6.81/3.43	           <rhs>
6.81/3.43	            <var>x</var>
6.81/3.43	           </rhs>
6.81/3.43	          </rule>
6.81/3.43	         </conditionalRule>
6.81/3.43	         <positionInTerm></positionInTerm>
6.81/3.43	         <substitution>
6.81/3.43	          <substEntry>
6.81/3.43	           <var>x</var>
6.81/3.43	           <funapp>
6.81/3.43	            <name>?1</name>
6.81/3.43	           </funapp>
6.81/3.43	          </substEntry>
6.81/3.43	         </substitution>
6.81/3.43	         <source>
6.81/3.43	          <funapp>
6.81/3.43	           <name>h</name>
6.81/3.43	           <arg>
6.81/3.43	            <funapp>
6.81/3.43	             <name>s</name>
6.81/3.43	             <arg>
6.81/3.43	              <funapp>
6.81/3.43	               <name>?1</name>
6.81/3.43	              </funapp>
6.81/3.43	             </arg>
6.81/3.43	            </funapp>
6.81/3.43	           </arg>
6.81/3.43	          </funapp>
6.81/3.43	         </source>
6.81/3.43	         <target>
6.81/3.43	          <funapp>
6.81/3.43	           <name>?1</name>
6.81/3.43	          </funapp>
6.81/3.43	         </target>
6.81/3.43	         <conditions> </conditions>
6.81/3.43	        </conditionalRewriteStep>
6.81/3.43	       </conditionalRewritingSequence>
6.81/3.43	       <constMap>
6.81/3.43	        <entry>
6.81/3.43	         <symbol>
6.81/3.43	          <name>?1</name>
6.81/3.43	         </symbol>
6.81/3.43	         <const>y'</const>
6.81/3.43	        </entry>
6.81/3.43	       </constMap>
6.81/3.43	      </contextJoinabilityProof>
6.81/3.43	     </contextJoinableCCP>
6.81/3.43	    </contextJoinableCCPs>
6.81/3.43	    <infeasibleConditions/>
6.81/3.43	    <unfeasibleCCPs/>
6.81/3.43	   </al94>
6.81/3.43	  </conditionalCrProof>
6.81/3.43	 </proof>
6.81/3.43	 <origin>
6.81/3.43	  <proofOrigin>
6.81/3.43	   <tool>
6.81/3.43	    <name>ConCon</name>
6.81/3.43	    <version>concon 1.4.0.0</version>
6.81/3.43	    <strategy>concon -s --cert --conf A theBenchmark.trs 58</strategy>
6.81/3.43	   </tool>
6.81/3.43	  </proofOrigin>
6.81/3.43	 </origin>
6.81/3.43	</certificationProblem>
6.81/3.43	EOF