3.55/2.12	YES
3.55/2.12	<?xml version="1.0"?><?xml-stylesheet type="text/xsl" href="cpfHTML.xsl"?>
3.55/2.12	<certificationProblem>
3.55/2.12	 <input>
3.55/2.12	  <ctrsInput>
3.55/2.12	   <conditionalRules>
3.55/2.12	    <conditionalRule>
3.55/2.12	     <rule>
3.55/2.12	      <lhs>
3.55/2.12	       <funapp>
3.55/2.12	        <name>f</name>
3.55/2.12	        <arg>
3.55/2.12	         <var>x</var>
3.55/2.12	        </arg>
3.55/2.12	       </funapp>
3.55/2.12	      </lhs>
3.55/2.12	      <rhs>
3.55/2.12	       <var>x</var>
3.55/2.12	      </rhs>
3.55/2.12	     </rule>
3.55/2.12	     <rule>
3.55/2.12	      <lhs>
3.55/2.12	       <var>x</var>
3.55/2.12	      </lhs>
3.55/2.12	      <rhs>
3.55/2.12	       <funapp>
3.55/2.12	        <name>a</name>
3.55/2.12	       </funapp>
3.55/2.12	      </rhs>
3.55/2.12	     </rule>
3.55/2.12	    </conditionalRule>
3.55/2.12	    <conditionalRule>
3.55/2.12	     <rule>
3.55/2.12	      <lhs>
3.55/2.12	       <funapp>
3.55/2.12	        <name>g</name>
3.55/2.12	        <arg>
3.55/2.12	         <var>x</var>
3.55/2.12	        </arg>
3.55/2.12	       </funapp>
3.55/2.12	      </lhs>
3.55/2.12	      <rhs>
3.55/2.12	       <funapp>
3.55/2.12	        <name>h</name>
3.55/2.12	        <arg>
3.55/2.12	         <var>x</var>
3.55/2.12	        </arg>
3.55/2.12	        <arg>
3.55/2.12	         <var>x</var>
3.55/2.12	        </arg>
3.55/2.12	       </funapp>
3.55/2.12	      </rhs>
3.55/2.12	     </rule>
3.55/2.12	    </conditionalRule>
3.55/2.12	    <conditionalRule>
3.55/2.12	     <rule>
3.55/2.12	      <lhs>
3.55/2.12	       <funapp>
3.55/2.12	        <name>h</name>
3.55/2.12	        <arg>
3.55/2.12	         <var>x</var>
3.55/2.12	        </arg>
3.55/2.12	        <arg>
3.55/2.12	         <var>y</var>
3.55/2.12	        </arg>
3.55/2.12	       </funapp>
3.55/2.12	      </lhs>
3.55/2.12	      <rhs>
3.55/2.12	       <funapp>
3.55/2.12	        <name>i</name>
3.55/2.12	        <arg>
3.55/2.12	         <var>x</var>
3.55/2.12	        </arg>
3.55/2.12	       </funapp>
3.55/2.12	      </rhs>
3.55/2.12	     </rule>
3.55/2.12	    </conditionalRule>
3.55/2.12	   </conditionalRules>
3.55/2.12	  </ctrsInput>
3.55/2.12	 </input>
3.55/2.12	 <cpfVersion>2.4</cpfVersion>
3.55/2.12	 <proof>
3.55/2.12	  <conditionalCrProof>
3.55/2.12	   <al94>
3.55/2.12	    <quasiReductiveProof>
3.55/2.12	     <unraveling>
3.55/2.12	      <unravelingInformation>
3.55/2.12	       <unravelingEntry>
3.55/2.12	        <conditionalRule>
3.55/2.12	         <rule>
3.55/2.12	          <lhs>
3.55/2.12	           <funapp>
3.55/2.12	            <name>f</name>
3.55/2.12	            <arg>
3.55/2.12	             <var>x</var>
3.55/2.12	            </arg>
3.55/2.12	           </funapp>
3.55/2.12	          </lhs>
3.55/2.12	          <rhs>
3.55/2.12	           <var>x</var>
3.55/2.12	          </rhs>
3.55/2.12	         </rule>
3.55/2.12	         <rule>
3.55/2.12	          <lhs>
3.55/2.12	           <var>x</var>
3.55/2.12	          </lhs>
3.55/2.12	          <rhs>
3.55/2.12	           <funapp>
3.55/2.12	            <name>a</name>
3.55/2.12	           </funapp>
3.55/2.12	          </rhs>
3.55/2.12	         </rule>
3.55/2.12	        </conditionalRule>
3.55/2.12	        <rule>
3.55/2.12	         <lhs>
3.55/2.12	          <funapp>
3.55/2.12	           <name>f</name>
3.55/2.12	           <arg>
3.55/2.12	            <var>x</var>
3.55/2.12	           </arg>
3.55/2.12	          </funapp>
3.55/2.12	         </lhs>
3.55/2.12	         <rhs>
3.55/2.12	          <funapp>
3.55/2.12	           <name>U1</name>
3.55/2.12	           <arg>
3.55/2.12	            <var>x</var>
3.55/2.12	           </arg>
3.55/2.12	           <arg>
3.55/2.12	            <var>x</var>
3.55/2.12	           </arg>
3.55/2.12	          </funapp>
3.55/2.12	         </rhs>
3.55/2.12	        </rule>
3.55/2.12	        <rule>
3.55/2.12	         <lhs>
3.55/2.12	          <funapp>
3.55/2.12	           <name>U1</name>
3.55/2.12	           <arg>
3.55/2.12	            <funapp>
3.55/2.12	             <name>a</name>
3.55/2.12	            </funapp>
3.55/2.12	           </arg>
3.55/2.12	           <arg>
3.55/2.12	            <var>x</var>
3.55/2.12	           </arg>
3.55/2.12	          </funapp>
3.55/2.12	         </lhs>
3.55/2.12	         <rhs>
3.55/2.12	          <var>x</var>
3.55/2.12	         </rhs>
3.55/2.12	        </rule>
3.55/2.12	       </unravelingEntry>
3.55/2.12	       <unravelingEntry>
3.55/2.12	        <conditionalRule>
3.55/2.12	         <rule>
3.55/2.12	          <lhs>
3.55/2.12	           <funapp>
3.55/2.12	            <name>g</name>
3.55/2.12	            <arg>
3.55/2.12	             <var>x</var>
3.55/2.12	            </arg>
3.55/2.12	           </funapp>
3.55/2.12	          </lhs>
3.55/2.12	          <rhs>
3.55/2.12	           <funapp>
3.55/2.12	            <name>h</name>
3.55/2.12	            <arg>
3.55/2.12	             <var>x</var>
3.55/2.12	            </arg>
3.55/2.12	            <arg>
3.55/2.12	             <var>x</var>
3.55/2.12	            </arg>
3.55/2.12	           </funapp>
3.55/2.12	          </rhs>
3.55/2.12	         </rule>
3.55/2.12	        </conditionalRule>
3.55/2.12	        <rule>
3.55/2.12	         <lhs>
3.55/2.12	          <funapp>
3.55/2.12	           <name>g</name>
3.55/2.12	           <arg>
3.55/2.12	            <var>x</var>
3.55/2.12	           </arg>
3.55/2.12	          </funapp>
3.55/2.12	         </lhs>
3.55/2.12	         <rhs>
3.55/2.12	          <funapp>
3.55/2.12	           <name>h</name>
3.55/2.12	           <arg>
3.55/2.12	            <var>x</var>
3.55/2.12	           </arg>
3.55/2.12	           <arg>
3.55/2.12	            <var>x</var>
3.55/2.12	           </arg>
3.55/2.12	          </funapp>
3.55/2.12	         </rhs>
3.55/2.12	        </rule>
3.55/2.12	       </unravelingEntry>
3.55/2.12	       <unravelingEntry>
3.55/2.12	        <conditionalRule>
3.55/2.12	         <rule>
3.55/2.12	          <lhs>
3.55/2.12	           <funapp>
3.55/2.12	            <name>h</name>
3.55/2.12	            <arg>
3.55/2.12	             <var>x</var>
3.55/2.12	            </arg>
3.55/2.12	            <arg>
3.55/2.12	             <var>y</var>
3.55/2.12	            </arg>
3.55/2.12	           </funapp>
3.55/2.12	          </lhs>
3.55/2.12	          <rhs>
3.55/2.12	           <funapp>
3.55/2.12	            <name>i</name>
3.55/2.12	            <arg>
3.55/2.12	             <var>x</var>
3.55/2.12	            </arg>
3.55/2.12	           </funapp>
3.55/2.12	          </rhs>
3.55/2.12	         </rule>
3.55/2.12	        </conditionalRule>
3.55/2.12	        <rule>
3.55/2.12	         <lhs>
3.55/2.12	          <funapp>
3.55/2.12	           <name>h</name>
3.55/2.12	           <arg>
3.55/2.12	            <var>x</var>
3.55/2.12	           </arg>
3.55/2.12	           <arg>
3.55/2.12	            <var>y</var>
3.55/2.12	           </arg>
3.55/2.12	          </funapp>
3.55/2.12	         </lhs>
3.55/2.12	         <rhs>
3.55/2.12	          <funapp>
3.55/2.12	           <name>i</name>
3.55/2.12	           <arg>
3.55/2.12	            <var>x</var>
3.55/2.12	           </arg>
3.55/2.12	          </funapp>
3.55/2.12	         </rhs>
3.55/2.12	        </rule>
3.55/2.12	       </unravelingEntry>
3.55/2.12	      </unravelingInformation>
3.55/2.12	      <trsTerminationProof>
3.55/2.12	       <ruleRemoval>
3.55/2.12	        <orderingConstraintProof>
3.55/2.12	         <redPair>
3.55/2.12	          <interpretation>
3.55/2.12	           <type>
3.55/2.12	            <polynomial>
3.55/2.12	             <domain>
3.55/2.12	              <matrices>
3.55/2.12	               <dimension>3</dimension>
3.55/2.12	               <strictDimension>1</strictDimension>
3.55/2.12	               <domain>
3.55/2.12	                <naturals/>
3.55/2.12	               </domain>
3.55/2.12	              </matrices>
3.55/2.12	             </domain>
3.55/2.12	             <degree>1</degree>
3.55/2.12	            </polynomial>
3.55/2.12	           </type>
3.55/2.12	           <interpret>
3.55/2.12	            <name>i</name>
3.55/2.12	            <arity>1</arity>
3.55/2.12	            <polynomial>
3.55/2.12	             <sum>
3.55/2.12	              <polynomial>
3.55/2.12	               <product>
3.55/2.12	                <polynomial>
3.55/2.12	                 <coefficient>
3.55/2.12	                  <matrix>
3.55/2.12	                   <vector>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>2</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                   </vector>
3.55/2.12	                   <vector>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                   </vector>
3.55/2.12	                   <vector>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                   </vector>
3.55/2.12	                  </matrix>
3.55/2.12	                 </coefficient>
3.55/2.12	                </polynomial>
3.55/2.12	                <polynomial>
3.55/2.12	                 <variable>1</variable>
3.55/2.12	                </polynomial>
3.55/2.12	               </product>
3.55/2.12	              </polynomial>
3.55/2.12	              <polynomial>
3.55/2.12	               <coefficient>
3.55/2.12	                <matrix>
3.55/2.12	                 <vector>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                 </vector>
3.55/2.12	                 <vector>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                 </vector>
3.55/2.12	                 <vector>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                 </vector>
3.55/2.12	                </matrix>
3.55/2.12	               </coefficient>
3.55/2.12	              </polynomial>
3.55/2.12	             </sum>
3.55/2.12	            </polynomial>
3.55/2.12	           </interpret>
3.55/2.12	           <interpret>
3.55/2.12	            <name>h</name>
3.55/2.12	            <arity>2</arity>
3.55/2.12	            <polynomial>
3.55/2.12	             <sum>
3.55/2.12	              <polynomial>
3.55/2.12	               <product>
3.55/2.12	                <polynomial>
3.55/2.12	                 <coefficient>
3.55/2.12	                  <matrix>
3.55/2.12	                   <vector>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>2</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                   </vector>
3.55/2.12	                   <vector>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                   </vector>
3.55/2.12	                   <vector>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                   </vector>
3.55/2.12	                  </matrix>
3.55/2.12	                 </coefficient>
3.55/2.12	                </polynomial>
3.55/2.12	                <polynomial>
3.55/2.12	                 <variable>1</variable>
3.55/2.12	                </polynomial>
3.55/2.12	               </product>
3.55/2.12	              </polynomial>
3.55/2.12	              <polynomial>
3.55/2.12	               <product>
3.55/2.12	                <polynomial>
3.55/2.12	                 <coefficient>
3.55/2.12	                  <matrix>
3.55/2.12	                   <vector>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>1</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                   </vector>
3.55/2.12	                   <vector>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>2</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                   </vector>
3.55/2.12	                   <vector>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                   </vector>
3.55/2.12	                  </matrix>
3.55/2.12	                 </coefficient>
3.55/2.12	                </polynomial>
3.55/2.12	                <polynomial>
3.55/2.12	                 <variable>2</variable>
3.55/2.12	                </polynomial>
3.55/2.12	               </product>
3.55/2.12	              </polynomial>
3.55/2.12	              <polynomial>
3.55/2.12	               <coefficient>
3.55/2.12	                <matrix>
3.55/2.12	                 <vector>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                 </vector>
3.55/2.12	                 <vector>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                 </vector>
3.55/2.12	                 <vector>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                 </vector>
3.55/2.12	                </matrix>
3.55/2.12	               </coefficient>
3.55/2.12	              </polynomial>
3.55/2.12	             </sum>
3.55/2.12	            </polynomial>
3.55/2.12	           </interpret>
3.55/2.12	           <interpret>
3.55/2.12	            <name>g</name>
3.55/2.12	            <arity>1</arity>
3.55/2.12	            <polynomial>
3.55/2.12	             <sum>
3.55/2.12	              <polynomial>
3.55/2.12	               <product>
3.55/2.12	                <polynomial>
3.55/2.12	                 <coefficient>
3.55/2.12	                  <matrix>
3.55/2.12	                   <vector>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>3</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                   </vector>
3.55/2.12	                   <vector>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>2</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                   </vector>
3.55/2.12	                   <vector>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                   </vector>
3.55/2.12	                  </matrix>
3.55/2.12	                 </coefficient>
3.55/2.12	                </polynomial>
3.55/2.12	                <polynomial>
3.55/2.12	                 <variable>1</variable>
3.55/2.12	                </polynomial>
3.55/2.12	               </product>
3.55/2.12	              </polynomial>
3.55/2.12	              <polynomial>
3.55/2.12	               <coefficient>
3.55/2.12	                <matrix>
3.55/2.12	                 <vector>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>2</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                 </vector>
3.55/2.12	                 <vector>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                 </vector>
3.55/2.12	                 <vector>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                 </vector>
3.55/2.12	                </matrix>
3.55/2.12	               </coefficient>
3.55/2.12	              </polynomial>
3.55/2.12	             </sum>
3.55/2.12	            </polynomial>
3.55/2.12	           </interpret>
3.55/2.12	           <interpret>
3.55/2.12	            <name>a</name>
3.55/2.12	            <arity>0</arity>
3.55/2.12	            <polynomial>
3.55/2.12	             <sum>
3.55/2.12	              <polynomial>
3.55/2.12	               <coefficient>
3.55/2.12	                <matrix>
3.55/2.12	                 <vector>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>1</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>2</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>1</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                 </vector>
3.55/2.12	                 <vector>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                 </vector>
3.55/2.12	                 <vector>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                  <coefficient>
3.55/2.12	                   <integer>0</integer>
3.55/2.12	                  </coefficient>
3.55/2.12	                 </vector>
3.55/2.12	                </matrix>
3.55/2.12	               </coefficient>
3.55/2.12	              </polynomial>
3.55/2.12	             </sum>
3.55/2.12	            </polynomial>
3.55/2.12	           </interpret>
3.55/2.12	           <interpret>
3.55/2.12	            <name>U1</name>
3.55/2.12	            <arity>2</arity>
3.55/2.12	            <polynomial>
3.55/2.12	             <sum>
3.55/2.12	              <polynomial>
3.55/2.12	               <product>
3.55/2.12	                <polynomial>
3.55/2.12	                 <coefficient>
3.55/2.12	                  <matrix>
3.55/2.12	                   <vector>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>2</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>2</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                   </vector>
3.55/2.12	                   <vector>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>2</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>2</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                   </vector>
3.55/2.12	                   <vector>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>2</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>1</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                   </vector>
3.55/2.12	                  </matrix>
3.55/2.12	                 </coefficient>
3.55/2.12	                </polynomial>
3.55/2.12	                <polynomial>
3.55/2.12	                 <variable>1</variable>
3.55/2.12	                </polynomial>
3.55/2.12	               </product>
3.55/2.12	              </polynomial>
3.55/2.12	              <polynomial>
3.55/2.12	               <product>
3.55/2.12	                <polynomial>
3.55/2.12	                 <coefficient>
3.55/2.12	                  <matrix>
3.55/2.12	                   <vector>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>1</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>3</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                   </vector>
3.55/2.12	                   <vector>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>1</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>0</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                   </vector>
3.55/2.12	                   <vector>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>1</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>2</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                    <coefficient>
3.55/2.12	                     <integer>2</integer>
3.55/2.12	                    </coefficient>
3.55/2.12	                   </vector>
3.55/2.12	                  </matrix>
3.55/2.12	                 </coefficient>
3.55/2.12	                </polynomial>
3.55/2.12	                <polynomial>
3.55/2.12	                 <variable>2</variable>
3.55/2.12	                </polynomial>
3.55/2.12	               </product>
3.55/2.12	              </polynomial>
3.55/2.13	              <polynomial>
3.55/2.13	               <coefficient>
3.55/2.13	                <matrix>
3.55/2.13	                 <vector>
3.55/2.13	                  <coefficient>
3.55/2.13	                   <integer>3</integer>
3.55/2.13	                  </coefficient>
3.55/2.13	                  <coefficient>
3.55/2.13	                   <integer>0</integer>
3.55/2.13	                  </coefficient>
3.55/2.13	                  <coefficient>
3.55/2.13	                   <integer>1</integer>
3.55/2.13	                  </coefficient>
3.55/2.13	                 </vector>
3.55/2.13	                 <vector>
3.55/2.13	                  <coefficient>
3.55/2.13	                   <integer>0</integer>
3.55/2.13	                  </coefficient>
3.55/2.13	                  <coefficient>
3.55/2.13	                   <integer>0</integer>
3.55/2.13	                  </coefficient>
3.55/2.13	                  <coefficient>
3.55/2.13	                   <integer>0</integer>
3.55/2.13	                  </coefficient>
3.55/2.13	                 </vector>
3.55/2.13	                 <vector>
3.55/2.13	                  <coefficient>
3.55/2.13	                   <integer>0</integer>
3.55/2.13	                  </coefficient>
3.55/2.13	                  <coefficient>
3.55/2.13	                   <integer>0</integer>
3.55/2.13	                  </coefficient>
3.55/2.13	                  <coefficient>
3.55/2.13	                   <integer>0</integer>
3.55/2.13	                  </coefficient>
3.55/2.13	                 </vector>
3.55/2.13	                </matrix>
3.55/2.13	               </coefficient>
3.55/2.13	              </polynomial>
3.55/2.13	             </sum>
3.55/2.13	            </polynomial>
3.55/2.13	           </interpret>
3.55/2.13	           <interpret>
3.55/2.13	            <name>f</name>
3.55/2.13	            <arity>1</arity>
3.55/2.13	            <polynomial>
3.55/2.13	             <sum>
3.55/2.13	              <polynomial>
3.55/2.13	               <product>
3.55/2.13	                <polynomial>
3.55/2.13	                 <coefficient>
3.55/2.13	                  <matrix>
3.55/2.13	                   <vector>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>3</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>3</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>3</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                   </vector>
3.55/2.13	                   <vector>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>3</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>2</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                   </vector>
3.55/2.13	                   <vector>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>3</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>3</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>3</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                   </vector>
3.55/2.13	                  </matrix>
3.55/2.13	                 </coefficient>
3.55/2.13	                </polynomial>
3.55/2.13	                <polynomial>
3.55/2.13	                 <variable>1</variable>
3.55/2.13	                </polynomial>
3.55/2.13	               </product>
3.55/2.13	              </polynomial>
3.55/2.13	              <polynomial>
3.55/2.13	               <coefficient>
3.55/2.13	                <matrix>
3.55/2.13	                 <vector>
3.55/2.13	                  <coefficient>
3.55/2.13	                   <integer>3</integer>
3.55/2.13	                  </coefficient>
3.55/2.13	                  <coefficient>
3.55/2.13	                   <integer>2</integer>
3.55/2.13	                  </coefficient>
3.55/2.13	                  <coefficient>
3.55/2.13	                   <integer>1</integer>
3.55/2.13	                  </coefficient>
3.55/2.13	                 </vector>
3.55/2.13	                 <vector>
3.55/2.13	                  <coefficient>
3.55/2.13	                   <integer>0</integer>
3.55/2.13	                  </coefficient>
3.55/2.13	                  <coefficient>
3.55/2.13	                   <integer>0</integer>
3.55/2.13	                  </coefficient>
3.55/2.13	                  <coefficient>
3.55/2.13	                   <integer>0</integer>
3.55/2.13	                  </coefficient>
3.55/2.13	                 </vector>
3.55/2.13	                 <vector>
3.55/2.13	                  <coefficient>
3.55/2.13	                   <integer>0</integer>
3.55/2.13	                  </coefficient>
3.55/2.13	                  <coefficient>
3.55/2.13	                   <integer>0</integer>
3.55/2.13	                  </coefficient>
3.55/2.13	                  <coefficient>
3.55/2.13	                   <integer>0</integer>
3.55/2.13	                  </coefficient>
3.55/2.13	                 </vector>
3.55/2.13	                </matrix>
3.55/2.13	               </coefficient>
3.55/2.13	              </polynomial>
3.55/2.13	             </sum>
3.55/2.13	            </polynomial>
3.55/2.13	           </interpret>
3.55/2.13	          </interpretation>
3.55/2.13	         </redPair>
3.55/2.13	        </orderingConstraintProof>
3.55/2.13	        <trs>
3.55/2.13	         <rules>
3.55/2.13	          <rule>
3.55/2.13	           <lhs>
3.55/2.13	            <funapp>
3.55/2.13	             <name>f</name>
3.55/2.13	             <arg>
3.55/2.13	              <var>x</var>
3.55/2.13	             </arg>
3.55/2.13	            </funapp>
3.55/2.13	           </lhs>
3.55/2.13	           <rhs>
3.55/2.13	            <funapp>
3.55/2.13	             <name>U1</name>
3.55/2.13	             <arg>
3.55/2.13	              <var>x</var>
3.55/2.13	             </arg>
3.55/2.13	             <arg>
3.55/2.13	              <var>x</var>
3.55/2.13	             </arg>
3.55/2.13	            </funapp>
3.55/2.13	           </rhs>
3.55/2.13	          </rule>
3.55/2.13	          <rule>
3.55/2.13	           <lhs>
3.55/2.13	            <funapp>
3.55/2.13	             <name>h</name>
3.55/2.13	             <arg>
3.55/2.13	              <var>x</var>
3.55/2.13	             </arg>
3.55/2.13	             <arg>
3.55/2.13	              <var>y</var>
3.55/2.13	             </arg>
3.55/2.13	            </funapp>
3.55/2.13	           </lhs>
3.55/2.13	           <rhs>
3.55/2.13	            <funapp>
3.55/2.13	             <name>i</name>
3.55/2.13	             <arg>
3.55/2.13	              <var>x</var>
3.55/2.13	             </arg>
3.55/2.13	            </funapp>
3.55/2.13	           </rhs>
3.55/2.13	          </rule>
3.55/2.13	         </rules>
3.55/2.13	        </trs>
3.55/2.13	        <trsTerminationProof>
3.55/2.13	         <ruleRemoval>
3.55/2.13	          <orderingConstraintProof>
3.55/2.13	           <redPair>
3.55/2.13	            <interpretation>
3.55/2.13	             <type>
3.55/2.13	              <polynomial>
3.55/2.13	               <domain>
3.55/2.13	                <matrices>
3.55/2.13	                 <dimension>3</dimension>
3.55/2.13	                 <strictDimension>1</strictDimension>
3.55/2.13	                 <domain>
3.55/2.13	                  <naturals/>
3.55/2.13	                 </domain>
3.55/2.13	                </matrices>
3.55/2.13	               </domain>
3.55/2.13	               <degree>1</degree>
3.55/2.13	              </polynomial>
3.55/2.13	             </type>
3.55/2.13	             <interpret>
3.55/2.13	              <name>i</name>
3.55/2.13	              <arity>1</arity>
3.55/2.13	              <polynomial>
3.55/2.13	               <sum>
3.55/2.13	                <polynomial>
3.55/2.13	                 <product>
3.55/2.13	                  <polynomial>
3.55/2.13	                   <coefficient>
3.55/2.13	                    <matrix>
3.55/2.13	                     <vector>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>1</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                     </vector>
3.55/2.13	                     <vector>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                     </vector>
3.55/2.13	                     <vector>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                     </vector>
3.55/2.13	                    </matrix>
3.55/2.13	                   </coefficient>
3.55/2.13	                  </polynomial>
3.55/2.13	                  <polynomial>
3.55/2.13	                   <variable>1</variable>
3.55/2.13	                  </polynomial>
3.55/2.13	                 </product>
3.55/2.13	                </polynomial>
3.55/2.13	                <polynomial>
3.55/2.13	                 <coefficient>
3.55/2.13	                  <matrix>
3.55/2.13	                   <vector>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                   </vector>
3.55/2.13	                   <vector>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                   </vector>
3.55/2.13	                   <vector>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                   </vector>
3.55/2.13	                  </matrix>
3.55/2.13	                 </coefficient>
3.55/2.13	                </polynomial>
3.55/2.13	               </sum>
3.55/2.13	              </polynomial>
3.55/2.13	             </interpret>
3.55/2.13	             <interpret>
3.55/2.13	              <name>h</name>
3.55/2.13	              <arity>2</arity>
3.55/2.13	              <polynomial>
3.55/2.13	               <sum>
3.55/2.13	                <polynomial>
3.55/2.13	                 <product>
3.55/2.13	                  <polynomial>
3.55/2.13	                   <coefficient>
3.55/2.13	                    <matrix>
3.55/2.13	                     <vector>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>1</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                     </vector>
3.55/2.13	                     <vector>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                     </vector>
3.55/2.13	                     <vector>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>2</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                     </vector>
3.55/2.13	                    </matrix>
3.55/2.13	                   </coefficient>
3.55/2.13	                  </polynomial>
3.55/2.13	                  <polynomial>
3.55/2.13	                   <variable>1</variable>
3.55/2.13	                  </polynomial>
3.55/2.13	                 </product>
3.55/2.13	                </polynomial>
3.55/2.13	                <polynomial>
3.55/2.13	                 <product>
3.55/2.13	                  <polynomial>
3.55/2.13	                   <coefficient>
3.55/2.13	                    <matrix>
3.55/2.13	                     <vector>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>2</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                     </vector>
3.55/2.13	                     <vector>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                     </vector>
3.55/2.13	                     <vector>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                     </vector>
3.55/2.13	                    </matrix>
3.55/2.13	                   </coefficient>
3.55/2.13	                  </polynomial>
3.55/2.13	                  <polynomial>
3.55/2.13	                   <variable>2</variable>
3.55/2.13	                  </polynomial>
3.55/2.13	                 </product>
3.55/2.13	                </polynomial>
3.55/2.13	                <polynomial>
3.55/2.13	                 <coefficient>
3.55/2.13	                  <matrix>
3.55/2.13	                   <vector>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                   </vector>
3.55/2.13	                   <vector>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                   </vector>
3.55/2.13	                   <vector>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                   </vector>
3.55/2.13	                  </matrix>
3.55/2.13	                 </coefficient>
3.55/2.13	                </polynomial>
3.55/2.13	               </sum>
3.55/2.13	              </polynomial>
3.55/2.13	             </interpret>
3.55/2.13	             <interpret>
3.55/2.13	              <name>U1</name>
3.55/2.13	              <arity>2</arity>
3.55/2.13	              <polynomial>
3.55/2.13	               <sum>
3.55/2.13	                <polynomial>
3.55/2.13	                 <product>
3.55/2.13	                  <polynomial>
3.55/2.13	                   <coefficient>
3.55/2.13	                    <matrix>
3.55/2.13	                     <vector>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>2</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                     </vector>
3.55/2.13	                     <vector>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                     </vector>
3.55/2.13	                     <vector>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                     </vector>
3.55/2.13	                    </matrix>
3.55/2.13	                   </coefficient>
3.55/2.13	                  </polynomial>
3.55/2.13	                  <polynomial>
3.55/2.13	                   <variable>1</variable>
3.55/2.13	                  </polynomial>
3.55/2.13	                 </product>
3.55/2.13	                </polynomial>
3.55/2.13	                <polynomial>
3.55/2.13	                 <product>
3.55/2.13	                  <polynomial>
3.55/2.13	                   <coefficient>
3.55/2.13	                    <matrix>
3.55/2.13	                     <vector>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>1</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                     </vector>
3.55/2.13	                     <vector>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                     </vector>
3.55/2.13	                     <vector>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                     </vector>
3.55/2.13	                    </matrix>
3.55/2.13	                   </coefficient>
3.55/2.13	                  </polynomial>
3.55/2.13	                  <polynomial>
3.55/2.13	                   <variable>2</variable>
3.55/2.13	                  </polynomial>
3.55/2.13	                 </product>
3.55/2.13	                </polynomial>
3.55/2.13	                <polynomial>
3.55/2.13	                 <coefficient>
3.55/2.13	                  <matrix>
3.55/2.13	                   <vector>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                   </vector>
3.55/2.13	                   <vector>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                   </vector>
3.55/2.13	                   <vector>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                   </vector>
3.55/2.13	                  </matrix>
3.55/2.13	                 </coefficient>
3.55/2.13	                </polynomial>
3.55/2.13	               </sum>
3.55/2.13	              </polynomial>
3.55/2.13	             </interpret>
3.55/2.13	             <interpret>
3.55/2.13	              <name>f</name>
3.55/2.13	              <arity>1</arity>
3.55/2.13	              <polynomial>
3.55/2.13	               <sum>
3.55/2.13	                <polynomial>
3.55/2.13	                 <product>
3.55/2.13	                  <polynomial>
3.55/2.13	                   <coefficient>
3.55/2.13	                    <matrix>
3.55/2.13	                     <vector>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>3</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                     </vector>
3.55/2.13	                     <vector>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>1</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                     </vector>
3.55/2.13	                     <vector>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>1</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                      <coefficient>
3.55/2.13	                       <integer>0</integer>
3.55/2.13	                      </coefficient>
3.55/2.13	                     </vector>
3.55/2.13	                    </matrix>
3.55/2.13	                   </coefficient>
3.55/2.13	                  </polynomial>
3.55/2.13	                  <polynomial>
3.55/2.13	                   <variable>1</variable>
3.55/2.13	                  </polynomial>
3.55/2.13	                 </product>
3.55/2.13	                </polynomial>
3.55/2.13	                <polynomial>
3.55/2.13	                 <coefficient>
3.55/2.13	                  <matrix>
3.55/2.13	                   <vector>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>2</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                   </vector>
3.55/2.13	                   <vector>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                   </vector>
3.55/2.13	                   <vector>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                    <coefficient>
3.55/2.13	                     <integer>0</integer>
3.55/2.13	                    </coefficient>
3.55/2.13	                   </vector>
3.55/2.13	                  </matrix>
3.55/2.13	                 </coefficient>
3.55/2.13	                </polynomial>
3.55/2.13	               </sum>
3.55/2.13	              </polynomial>
3.55/2.13	             </interpret>
3.55/2.13	            </interpretation>
3.55/2.13	           </redPair>
3.55/2.13	          </orderingConstraintProof>
3.55/2.13	          <trs>
3.55/2.13	           <rules>
3.55/2.13	            <rule>
3.55/2.13	             <lhs>
3.55/2.13	              <funapp>
3.55/2.13	               <name>h</name>
3.55/2.13	               <arg>
3.55/2.13	                <var>x</var>
3.55/2.13	               </arg>
3.55/2.13	               <arg>
3.55/2.13	                <var>y</var>
3.55/2.13	               </arg>
3.55/2.13	              </funapp>
3.55/2.13	             </lhs>
3.55/2.13	             <rhs>
3.55/2.13	              <funapp>
3.55/2.13	               <name>i</name>
3.55/2.13	               <arg>
3.55/2.13	                <var>x</var>
3.55/2.13	               </arg>
3.55/2.13	              </funapp>
3.55/2.13	             </rhs>
3.55/2.13	            </rule>
3.55/2.13	           </rules>
3.55/2.13	          </trs>
3.55/2.13	          <trsTerminationProof>
3.55/2.13	           <ruleRemoval>
3.55/2.13	            <orderingConstraintProof>
3.55/2.13	             <redPair>
3.55/2.13	              <knuthBendixOrder>
3.55/2.13	               <w0>1</w0>
3.55/2.13	               <precedenceWeight>
3.55/2.13	                <precedenceWeightEntry>
3.55/2.13	                 <name>i</name>
3.55/2.13	                 <arity>1</arity>
3.55/2.13	                 <precedence>0</precedence>
3.55/2.13	                 <weight>1</weight>
3.55/2.13	                </precedenceWeightEntry>
3.55/2.13	                <precedenceWeightEntry>
3.55/2.13	                 <name>h</name>
3.55/2.13	                 <arity>2</arity>
3.55/2.13	                 <precedence>1</precedence>
3.55/2.13	                 <weight>0</weight>
3.55/2.13	                </precedenceWeightEntry>
3.55/2.13	               </precedenceWeight>
3.55/2.13	              </knuthBendixOrder>
3.55/2.13	             </redPair>
3.55/2.13	            </orderingConstraintProof>
3.55/2.13	            <trs>
3.55/2.13	             <rules/>
3.55/2.13	            </trs>
3.55/2.13	            <trsTerminationProof>
3.55/2.13	             <rIsEmpty/>
3.55/2.13	            </trsTerminationProof>
3.55/2.13	           </ruleRemoval>
3.55/2.13	          </trsTerminationProof>
3.55/2.13	         </ruleRemoval>
3.55/2.13	        </trsTerminationProof>
3.55/2.13	       </ruleRemoval>
3.55/2.13	      </trsTerminationProof>
3.55/2.13	     </unraveling>
3.55/2.13	    </quasiReductiveProof>
3.55/2.13	    <contextJoinableCCPs/>
3.55/2.13	    <infeasibleConditions/>
3.55/2.13	    <unfeasibleCCPs/>
3.55/2.13	   </al94>
3.55/2.13	  </conditionalCrProof>
3.55/2.13	 </proof>
3.55/2.13	 <origin>
3.55/2.13	  <proofOrigin>
3.55/2.13	   <tool>
3.55/2.13	    <name>ConCon</name>
3.55/2.13	    <version>concon 1.4.0.0</version>
3.55/2.13	    <strategy>
3.55/2.13	     concon -s --cert --conf A --no-inlining theBenchmark.trs 58
3.55/2.13	    </strategy>
3.55/2.13	   </tool>
3.55/2.13	  </proofOrigin>
3.55/2.13	 </origin>
3.55/2.13	</certificationProblem>
3.55/2.13	EOF