6.57/2.91	YES
6.57/2.91	<?xml version="1.0"?><?xml-stylesheet type="text/xsl" href="cpfHTML.xsl"?>
6.57/2.91	<certificationProblem>
6.57/2.91	 <input>
6.57/2.91	  <ctrsInput>
6.57/2.91	   <conditionalRules>
6.57/2.91	    <conditionalRule>
6.57/2.91	     <rule>
6.57/2.91	      <lhs>
6.57/2.91	       <funapp>
6.57/2.91	        <name>size</name>
6.57/2.91	        <arg>
6.57/2.91	         <funapp>
6.57/2.91	          <name>empty</name>
6.57/2.91	         </funapp>
6.57/2.91	        </arg>
6.57/2.91	       </funapp>
6.57/2.91	      </lhs>
6.57/2.91	      <rhs>
6.57/2.91	       <funapp>
6.57/2.91	        <name>0</name>
6.57/2.91	       </funapp>
6.57/2.91	      </rhs>
6.57/2.91	     </rule>
6.57/2.91	    </conditionalRule>
6.57/2.91	    <conditionalRule>
6.57/2.91	     <rule>
6.57/2.91	      <lhs>
6.57/2.91	       <funapp>
6.57/2.91	        <name>size</name>
6.57/2.91	        <arg>
6.57/2.91	         <funapp>
6.57/2.91	          <name>push</name>
6.57/2.91	          <arg>
6.57/2.91	           <var>x</var>
6.57/2.91	          </arg>
6.57/2.91	          <arg>
6.57/2.91	           <var>y</var>
6.57/2.91	          </arg>
6.57/2.91	         </funapp>
6.57/2.91	        </arg>
6.57/2.91	       </funapp>
6.57/2.91	      </lhs>
6.57/2.91	      <rhs>
6.57/2.91	       <funapp>
6.57/2.91	        <name>s</name>
6.57/2.91	        <arg>
6.57/2.91	         <funapp>
6.57/2.91	          <name>size</name>
6.57/2.91	          <arg>
6.57/2.91	           <var>x</var>
6.57/2.91	          </arg>
6.57/2.91	         </funapp>
6.57/2.91	        </arg>
6.57/2.91	       </funapp>
6.57/2.91	      </rhs>
6.57/2.91	     </rule>
6.57/2.91	    </conditionalRule>
6.57/2.91	    <conditionalRule>
6.57/2.91	     <rule>
6.57/2.91	      <lhs>
6.57/2.91	       <funapp>
6.57/2.91	        <name>m</name>
6.57/2.91	       </funapp>
6.57/2.91	      </lhs>
6.57/2.91	      <rhs>
6.57/2.91	       <funapp>
6.57/2.91	        <name>s</name>
6.57/2.91	        <arg>
6.57/2.91	         <funapp>
6.57/2.91	          <name>s</name>
6.57/2.91	          <arg>
6.57/2.91	           <funapp>
6.57/2.91	            <name>s</name>
6.57/2.91	            <arg>
6.57/2.91	             <funapp>
6.57/2.91	              <name>s</name>
6.57/2.91	              <arg>
6.57/2.91	               <funapp>
6.57/2.91	                <name>0</name>
6.57/2.91	               </funapp>
6.57/2.91	              </arg>
6.57/2.91	             </funapp>
6.57/2.91	            </arg>
6.57/2.91	           </funapp>
6.57/2.91	          </arg>
6.57/2.91	         </funapp>
6.57/2.91	        </arg>
6.57/2.91	       </funapp>
6.57/2.91	      </rhs>
6.57/2.91	     </rule>
6.57/2.91	    </conditionalRule>
6.57/2.91	    <conditionalRule>
6.57/2.91	     <rule>
6.57/2.91	      <lhs>
6.57/2.91	       <funapp>
6.57/2.91	        <name>pop</name>
6.57/2.91	        <arg>
6.57/2.91	         <funapp>
6.57/2.91	          <name>empty</name>
6.57/2.91	         </funapp>
6.57/2.91	        </arg>
6.57/2.91	       </funapp>
6.57/2.91	      </lhs>
6.57/2.91	      <rhs>
6.57/2.91	       <funapp>
6.57/2.91	        <name>empty</name>
6.57/2.91	       </funapp>
6.57/2.91	      </rhs>
6.57/2.91	     </rule>
6.57/2.91	    </conditionalRule>
6.57/2.91	    <conditionalRule>
6.57/2.91	     <rule>
6.57/2.91	      <lhs>
6.57/2.91	       <funapp>
6.57/2.91	        <name>pop</name>
6.57/2.91	        <arg>
6.57/2.91	         <funapp>
6.57/2.91	          <name>push</name>
6.57/2.91	          <arg>
6.57/2.91	           <var>x</var>
6.57/2.91	          </arg>
6.57/2.91	          <arg>
6.57/2.91	           <var>y</var>
6.57/2.91	          </arg>
6.57/2.91	         </funapp>
6.57/2.91	        </arg>
6.57/2.91	       </funapp>
6.57/2.91	      </lhs>
6.57/2.91	      <rhs>
6.57/2.91	       <var>x</var>
6.57/2.91	      </rhs>
6.57/2.91	     </rule>
6.57/2.91	     <rule>
6.57/2.91	      <lhs>
6.57/2.91	       <funapp>
6.57/2.91	        <name>le</name>
6.57/2.91	        <arg>
6.57/2.91	         <funapp>
6.57/2.91	          <name>size</name>
6.57/2.91	          <arg>
6.57/2.91	           <var>x</var>
6.57/2.91	          </arg>
6.57/2.91	         </funapp>
6.57/2.91	        </arg>
6.57/2.91	        <arg>
6.57/2.91	         <funapp>
6.57/2.91	          <name>m</name>
6.57/2.91	         </funapp>
6.57/2.91	        </arg>
6.57/2.91	       </funapp>
6.57/2.91	      </lhs>
6.57/2.91	      <rhs>
6.57/2.91	       <funapp>
6.57/2.91	        <name>true</name>
6.57/2.91	       </funapp>
6.57/2.91	      </rhs>
6.57/2.91	     </rule>
6.57/2.91	    </conditionalRule>
6.57/2.91	    <conditionalRule>
6.57/2.91	     <rule>
6.57/2.91	      <lhs>
6.57/2.91	       <funapp>
6.57/2.91	        <name>top</name>
6.57/2.91	        <arg>
6.57/2.91	         <funapp>
6.57/2.91	          <name>empty</name>
6.57/2.91	         </funapp>
6.57/2.91	        </arg>
6.57/2.91	       </funapp>
6.57/2.91	      </lhs>
6.57/2.91	      <rhs>
6.57/2.91	       <funapp>
6.57/2.91	        <name>eentry</name>
6.57/2.91	       </funapp>
6.57/2.91	      </rhs>
6.57/2.91	     </rule>
6.57/2.91	    </conditionalRule>
6.57/2.91	    <conditionalRule>
6.57/2.91	     <rule>
6.57/2.91	      <lhs>
6.57/2.91	       <funapp>
6.57/2.91	        <name>top</name>
6.57/2.91	        <arg>
6.57/2.91	         <funapp>
6.57/2.91	          <name>push</name>
6.57/2.91	          <arg>
6.57/2.91	           <var>x</var>
6.57/2.91	          </arg>
6.57/2.91	          <arg>
6.57/2.91	           <var>y</var>
6.57/2.91	          </arg>
6.57/2.91	         </funapp>
6.57/2.91	        </arg>
6.57/2.91	       </funapp>
6.57/2.91	      </lhs>
6.57/2.91	      <rhs>
6.57/2.91	       <var>y</var>
6.57/2.91	      </rhs>
6.57/2.91	     </rule>
6.57/2.91	     <rule>
6.57/2.91	      <lhs>
6.57/2.91	       <funapp>
6.57/2.91	        <name>le</name>
6.57/2.91	        <arg>
6.57/2.91	         <funapp>
6.57/2.91	          <name>size</name>
6.57/2.91	          <arg>
6.57/2.91	           <var>x</var>
6.57/2.91	          </arg>
6.57/2.91	         </funapp>
6.57/2.91	        </arg>
6.57/2.91	        <arg>
6.57/2.91	         <funapp>
6.57/2.91	          <name>m</name>
6.57/2.91	         </funapp>
6.57/2.91	        </arg>
6.57/2.91	       </funapp>
6.57/2.91	      </lhs>
6.57/2.91	      <rhs>
6.57/2.91	       <funapp>
6.57/2.91	        <name>true</name>
6.57/2.91	       </funapp>
6.57/2.91	      </rhs>
6.57/2.91	     </rule>
6.57/2.91	    </conditionalRule>
6.57/2.91	    <conditionalRule>
6.57/2.91	     <rule>
6.57/2.91	      <lhs>
6.57/2.91	       <funapp>
6.57/2.91	        <name>le</name>
6.57/2.91	        <arg>
6.57/2.91	         <var>x</var>
6.57/2.91	        </arg>
6.57/2.91	        <arg>
6.57/2.91	         <funapp>
6.57/2.91	          <name>0</name>
6.57/2.91	         </funapp>
6.57/2.91	        </arg>
6.57/2.91	       </funapp>
6.57/2.91	      </lhs>
6.57/2.91	      <rhs>
6.57/2.91	       <funapp>
6.57/2.91	        <name>false</name>
6.57/2.91	       </funapp>
6.57/2.91	      </rhs>
6.57/2.91	     </rule>
6.57/2.91	    </conditionalRule>
6.57/2.91	    <conditionalRule>
6.57/2.91	     <rule>
6.57/2.91	      <lhs>
6.57/2.91	       <funapp>
6.57/2.91	        <name>le</name>
6.57/2.91	        <arg>
6.57/2.91	         <funapp>
6.57/2.91	          <name>0</name>
6.57/2.91	         </funapp>
6.57/2.91	        </arg>
6.57/2.91	        <arg>
6.57/2.91	         <funapp>
6.57/2.91	          <name>s</name>
6.57/2.91	          <arg>
6.57/2.91	           <var>x</var>
6.57/2.91	          </arg>
6.57/2.91	         </funapp>
6.57/2.91	        </arg>
6.57/2.91	       </funapp>
6.57/2.91	      </lhs>
6.57/2.91	      <rhs>
6.57/2.91	       <funapp>
6.57/2.91	        <name>true</name>
6.57/2.91	       </funapp>
6.57/2.91	      </rhs>
6.57/2.91	     </rule>
6.57/2.91	    </conditionalRule>
6.57/2.91	    <conditionalRule>
6.57/2.91	     <rule>
6.57/2.91	      <lhs>
6.57/2.91	       <funapp>
6.57/2.91	        <name>le</name>
6.57/2.91	        <arg>
6.57/2.91	         <funapp>
6.57/2.91	          <name>s</name>
6.57/2.91	          <arg>
6.57/2.91	           <var>x</var>
6.57/2.91	          </arg>
6.57/2.91	         </funapp>
6.57/2.91	        </arg>
6.57/2.91	        <arg>
6.57/2.91	         <funapp>
6.57/2.91	          <name>s</name>
6.57/2.91	          <arg>
6.57/2.91	           <var>y</var>
6.57/2.91	          </arg>
6.57/2.91	         </funapp>
6.57/2.91	        </arg>
6.57/2.91	       </funapp>
6.57/2.91	      </lhs>
6.57/2.91	      <rhs>
6.57/2.91	       <funapp>
6.57/2.91	        <name>le</name>
6.57/2.91	        <arg>
6.57/2.91	         <var>x</var>
6.57/2.91	        </arg>
6.57/2.91	        <arg>
6.57/2.91	         <var>y</var>
6.57/2.91	        </arg>
6.57/2.91	       </funapp>
6.57/2.91	      </rhs>
6.57/2.91	     </rule>
6.57/2.91	    </conditionalRule>
6.57/2.91	   </conditionalRules>
6.57/2.91	  </ctrsInput>
6.57/2.91	 </input>
6.57/2.91	 <cpfVersion>2.4</cpfVersion>
6.57/2.91	 <proof>
6.57/2.91	  <conditionalCrProof>
6.57/2.91	   <al94>
6.57/2.91	    <quasiReductiveProof>
6.57/2.91	     <unraveling>
6.57/2.91	      <unravelingInformation>
6.57/2.91	       <unravelingEntry>
6.57/2.91	        <conditionalRule>
6.57/2.91	         <rule>
6.57/2.91	          <lhs>
6.57/2.91	           <funapp>
6.57/2.91	            <name>pop</name>
6.57/2.91	            <arg>
6.57/2.91	             <funapp>
6.57/2.91	              <name>empty</name>
6.57/2.91	             </funapp>
6.57/2.91	            </arg>
6.57/2.91	           </funapp>
6.57/2.91	          </lhs>
6.57/2.91	          <rhs>
6.57/2.91	           <funapp>
6.57/2.91	            <name>empty</name>
6.57/2.91	           </funapp>
6.57/2.91	          </rhs>
6.57/2.91	         </rule>
6.57/2.91	        </conditionalRule>
6.57/2.91	        <rule>
6.57/2.91	         <lhs>
6.57/2.91	          <funapp>
6.57/2.91	           <name>pop</name>
6.57/2.91	           <arg>
6.57/2.91	            <funapp>
6.57/2.91	             <name>empty</name>
6.57/2.91	            </funapp>
6.57/2.91	           </arg>
6.57/2.91	          </funapp>
6.57/2.91	         </lhs>
6.57/2.91	         <rhs>
6.57/2.91	          <funapp>
6.57/2.91	           <name>empty</name>
6.57/2.91	          </funapp>
6.57/2.91	         </rhs>
6.57/2.91	        </rule>
6.57/2.91	       </unravelingEntry>
6.57/2.91	       <unravelingEntry>
6.57/2.91	        <conditionalRule>
6.57/2.91	         <rule>
6.57/2.91	          <lhs>
6.57/2.91	           <funapp>
6.57/2.91	            <name>le</name>
6.57/2.91	            <arg>
6.57/2.91	             <funapp>
6.57/2.91	              <name>0</name>
6.57/2.91	             </funapp>
6.57/2.91	            </arg>
6.57/2.91	            <arg>
6.57/2.91	             <funapp>
6.57/2.91	              <name>s</name>
6.57/2.91	              <arg>
6.57/2.91	               <var>x</var>
6.57/2.91	              </arg>
6.57/2.91	             </funapp>
6.57/2.91	            </arg>
6.57/2.91	           </funapp>
6.57/2.91	          </lhs>
6.57/2.91	          <rhs>
6.57/2.91	           <funapp>
6.57/2.91	            <name>true</name>
6.57/2.91	           </funapp>
6.57/2.91	          </rhs>
6.57/2.91	         </rule>
6.57/2.91	        </conditionalRule>
6.57/2.91	        <rule>
6.57/2.91	         <lhs>
6.57/2.91	          <funapp>
6.57/2.91	           <name>le</name>
6.57/2.91	           <arg>
6.57/2.91	            <funapp>
6.57/2.91	             <name>0</name>
6.57/2.91	            </funapp>
6.57/2.91	           </arg>
6.57/2.91	           <arg>
6.57/2.91	            <funapp>
6.57/2.91	             <name>s</name>
6.57/2.91	             <arg>
6.57/2.91	              <var>x</var>
6.57/2.91	             </arg>
6.57/2.91	            </funapp>
6.57/2.91	           </arg>
6.57/2.91	          </funapp>
6.57/2.91	         </lhs>
6.57/2.91	         <rhs>
6.57/2.91	          <funapp>
6.57/2.91	           <name>true</name>
6.57/2.91	          </funapp>
6.57/2.91	         </rhs>
6.57/2.91	        </rule>
6.57/2.91	       </unravelingEntry>
6.57/2.91	       <unravelingEntry>
6.57/2.91	        <conditionalRule>
6.57/2.91	         <rule>
6.57/2.91	          <lhs>
6.57/2.91	           <funapp>
6.57/2.91	            <name>top</name>
6.57/2.91	            <arg>
6.57/2.91	             <funapp>
6.57/2.91	              <name>push</name>
6.57/2.91	              <arg>
6.57/2.91	               <var>x</var>
6.57/2.91	              </arg>
6.57/2.91	              <arg>
6.57/2.91	               <var>y</var>
6.57/2.91	              </arg>
6.57/2.91	             </funapp>
6.57/2.91	            </arg>
6.57/2.91	           </funapp>
6.57/2.91	          </lhs>
6.57/2.91	          <rhs>
6.57/2.91	           <var>y</var>
6.57/2.91	          </rhs>
6.57/2.91	         </rule>
6.57/2.91	         <rule>
6.57/2.91	          <lhs>
6.57/2.91	           <funapp>
6.57/2.91	            <name>le</name>
6.57/2.91	            <arg>
6.57/2.91	             <funapp>
6.57/2.91	              <name>size</name>
6.57/2.91	              <arg>
6.57/2.91	               <var>x</var>
6.57/2.91	              </arg>
6.57/2.91	             </funapp>
6.57/2.91	            </arg>
6.57/2.91	            <arg>
6.57/2.91	             <funapp>
6.57/2.91	              <name>m</name>
6.57/2.91	             </funapp>
6.57/2.91	            </arg>
6.57/2.91	           </funapp>
6.57/2.91	          </lhs>
6.57/2.91	          <rhs>
6.57/2.91	           <funapp>
6.57/2.91	            <name>true</name>
6.57/2.91	           </funapp>
6.57/2.91	          </rhs>
6.57/2.91	         </rule>
6.57/2.91	        </conditionalRule>
6.57/2.91	        <rule>
6.57/2.91	         <lhs>
6.57/2.91	          <funapp>
6.57/2.91	           <name>top</name>
6.57/2.91	           <arg>
6.57/2.91	            <funapp>
6.57/2.91	             <name>push</name>
6.57/2.91	             <arg>
6.57/2.91	              <var>x</var>
6.57/2.91	             </arg>
6.57/2.91	             <arg>
6.57/2.91	              <var>y</var>
6.57/2.91	             </arg>
6.57/2.91	            </funapp>
6.57/2.91	           </arg>
6.57/2.91	          </funapp>
6.57/2.91	         </lhs>
6.57/2.91	         <rhs>
6.57/2.91	          <funapp>
6.57/2.91	           <name>U2</name>
6.57/2.91	           <arg>
6.57/2.91	            <funapp>
6.57/2.91	             <name>le</name>
6.57/2.91	             <arg>
6.57/2.91	              <funapp>
6.57/2.91	               <name>size</name>
6.57/2.91	               <arg>
6.57/2.91	                <var>x</var>
6.57/2.91	               </arg>
6.57/2.91	              </funapp>
6.57/2.91	             </arg>
6.57/2.91	             <arg>
6.57/2.91	              <funapp>
6.57/2.91	               <name>m</name>
6.57/2.91	              </funapp>
6.57/2.91	             </arg>
6.57/2.91	            </funapp>
6.57/2.91	           </arg>
6.57/2.91	           <arg>
6.57/2.91	            <var>x</var>
6.57/2.91	           </arg>
6.57/2.91	           <arg>
6.57/2.91	            <var>y</var>
6.57/2.91	           </arg>
6.57/2.91	          </funapp>
6.57/2.91	         </rhs>
6.57/2.91	        </rule>
6.57/2.91	        <rule>
6.57/2.91	         <lhs>
6.57/2.91	          <funapp>
6.57/2.91	           <name>U2</name>
6.57/2.91	           <arg>
6.57/2.91	            <funapp>
6.57/2.91	             <name>true</name>
6.57/2.91	            </funapp>
6.57/2.91	           </arg>
6.57/2.91	           <arg>
6.57/2.91	            <var>x</var>
6.57/2.91	           </arg>
6.57/2.91	           <arg>
6.57/2.91	            <var>y</var>
6.57/2.91	           </arg>
6.57/2.91	          </funapp>
6.57/2.91	         </lhs>
6.57/2.91	         <rhs>
6.57/2.91	          <var>y</var>
6.57/2.91	         </rhs>
6.57/2.91	        </rule>
6.57/2.91	       </unravelingEntry>
6.57/2.91	       <unravelingEntry>
6.57/2.91	        <conditionalRule>
6.57/2.91	         <rule>
6.57/2.92	          <lhs>
6.57/2.92	           <funapp>
6.57/2.92	            <name>le</name>
6.57/2.92	            <arg>
6.57/2.92	             <funapp>
6.57/2.92	              <name>s</name>
6.57/2.92	              <arg>
6.57/2.92	               <var>x</var>
6.57/2.92	              </arg>
6.57/2.92	             </funapp>
6.57/2.92	            </arg>
6.57/2.92	            <arg>
6.57/2.92	             <funapp>
6.57/2.92	              <name>s</name>
6.57/2.92	              <arg>
6.57/2.92	               <var>y</var>
6.57/2.92	              </arg>
6.57/2.92	             </funapp>
6.57/2.92	            </arg>
6.57/2.92	           </funapp>
6.57/2.92	          </lhs>
6.57/2.92	          <rhs>
6.57/2.92	           <funapp>
6.57/2.92	            <name>le</name>
6.57/2.92	            <arg>
6.57/2.92	             <var>x</var>
6.57/2.92	            </arg>
6.57/2.92	            <arg>
6.57/2.92	             <var>y</var>
6.57/2.92	            </arg>
6.57/2.92	           </funapp>
6.57/2.92	          </rhs>
6.57/2.92	         </rule>
6.57/2.92	        </conditionalRule>
6.57/2.92	        <rule>
6.57/2.92	         <lhs>
6.57/2.92	          <funapp>
6.57/2.92	           <name>le</name>
6.57/2.92	           <arg>
6.57/2.92	            <funapp>
6.57/2.92	             <name>s</name>
6.57/2.92	             <arg>
6.57/2.92	              <var>x</var>
6.57/2.92	             </arg>
6.57/2.92	            </funapp>
6.57/2.92	           </arg>
6.57/2.92	           <arg>
6.57/2.92	            <funapp>
6.57/2.92	             <name>s</name>
6.57/2.92	             <arg>
6.57/2.92	              <var>y</var>
6.57/2.92	             </arg>
6.57/2.92	            </funapp>
6.57/2.92	           </arg>
6.57/2.92	          </funapp>
6.57/2.92	         </lhs>
6.57/2.92	         <rhs>
6.57/2.92	          <funapp>
6.57/2.92	           <name>le</name>
6.57/2.92	           <arg>
6.57/2.92	            <var>x</var>
6.57/2.92	           </arg>
6.57/2.92	           <arg>
6.57/2.92	            <var>y</var>
6.57/2.92	           </arg>
6.57/2.92	          </funapp>
6.57/2.92	         </rhs>
6.57/2.92	        </rule>
6.57/2.92	       </unravelingEntry>
6.57/2.92	       <unravelingEntry>
6.57/2.92	        <conditionalRule>
6.57/2.92	         <rule>
6.57/2.92	          <lhs>
6.57/2.92	           <funapp>
6.57/2.92	            <name>size</name>
6.57/2.92	            <arg>
6.57/2.92	             <funapp>
6.57/2.92	              <name>push</name>
6.57/2.92	              <arg>
6.57/2.92	               <var>x</var>
6.57/2.92	              </arg>
6.57/2.92	              <arg>
6.57/2.92	               <var>y</var>
6.57/2.92	              </arg>
6.57/2.92	             </funapp>
6.57/2.92	            </arg>
6.57/2.92	           </funapp>
6.57/2.92	          </lhs>
6.57/2.92	          <rhs>
6.57/2.92	           <funapp>
6.57/2.92	            <name>s</name>
6.57/2.92	            <arg>
6.57/2.92	             <funapp>
6.57/2.92	              <name>size</name>
6.57/2.92	              <arg>
6.57/2.92	               <var>x</var>
6.57/2.92	              </arg>
6.57/2.92	             </funapp>
6.57/2.92	            </arg>
6.57/2.92	           </funapp>
6.57/2.92	          </rhs>
6.57/2.92	         </rule>
6.57/2.92	        </conditionalRule>
6.57/2.92	        <rule>
6.57/2.92	         <lhs>
6.57/2.92	          <funapp>
6.57/2.92	           <name>size</name>
6.57/2.92	           <arg>
6.57/2.92	            <funapp>
6.57/2.92	             <name>push</name>
6.57/2.92	             <arg>
6.57/2.92	              <var>x</var>
6.57/2.92	             </arg>
6.57/2.92	             <arg>
6.57/2.92	              <var>y</var>
6.57/2.92	             </arg>
6.57/2.92	            </funapp>
6.57/2.92	           </arg>
6.57/2.92	          </funapp>
6.57/2.92	         </lhs>
6.57/2.92	         <rhs>
6.57/2.92	          <funapp>
6.57/2.92	           <name>s</name>
6.57/2.92	           <arg>
6.57/2.92	            <funapp>
6.57/2.92	             <name>size</name>
6.57/2.92	             <arg>
6.57/2.92	              <var>x</var>
6.57/2.92	             </arg>
6.57/2.92	            </funapp>
6.57/2.92	           </arg>
6.57/2.92	          </funapp>
6.57/2.92	         </rhs>
6.57/2.92	        </rule>
6.57/2.92	       </unravelingEntry>
6.57/2.92	       <unravelingEntry>
6.57/2.92	        <conditionalRule>
6.57/2.92	         <rule>
6.57/2.92	          <lhs>
6.57/2.92	           <funapp>
6.57/2.92	            <name>size</name>
6.57/2.92	            <arg>
6.57/2.92	             <funapp>
6.57/2.92	              <name>empty</name>
6.57/2.92	             </funapp>
6.57/2.92	            </arg>
6.57/2.92	           </funapp>
6.57/2.92	          </lhs>
6.57/2.92	          <rhs>
6.57/2.92	           <funapp>
6.57/2.92	            <name>0</name>
6.57/2.92	           </funapp>
6.57/2.92	          </rhs>
6.57/2.92	         </rule>
6.57/2.92	        </conditionalRule>
6.57/2.92	        <rule>
6.57/2.92	         <lhs>
6.57/2.92	          <funapp>
6.57/2.92	           <name>size</name>
6.57/2.92	           <arg>
6.57/2.92	            <funapp>
6.57/2.92	             <name>empty</name>
6.57/2.92	            </funapp>
6.57/2.92	           </arg>
6.57/2.92	          </funapp>
6.57/2.92	         </lhs>
6.57/2.92	         <rhs>
6.57/2.92	          <funapp>
6.57/2.92	           <name>0</name>
6.57/2.92	          </funapp>
6.57/2.92	         </rhs>
6.57/2.92	        </rule>
6.57/2.92	       </unravelingEntry>
6.57/2.92	       <unravelingEntry>
6.57/2.92	        <conditionalRule>
6.57/2.92	         <rule>
6.57/2.92	          <lhs>
6.57/2.92	           <funapp>
6.57/2.92	            <name>le</name>
6.57/2.92	            <arg>
6.57/2.92	             <var>x</var>
6.57/2.92	            </arg>
6.57/2.92	            <arg>
6.57/2.92	             <funapp>
6.57/2.92	              <name>0</name>
6.57/2.92	             </funapp>
6.57/2.92	            </arg>
6.57/2.92	           </funapp>
6.57/2.92	          </lhs>
6.57/2.92	          <rhs>
6.57/2.92	           <funapp>
6.57/2.92	            <name>false</name>
6.57/2.92	           </funapp>
6.57/2.92	          </rhs>
6.57/2.92	         </rule>
6.57/2.92	        </conditionalRule>
6.57/2.92	        <rule>
6.57/2.92	         <lhs>
6.57/2.92	          <funapp>
6.57/2.92	           <name>le</name>
6.57/2.92	           <arg>
6.57/2.92	            <var>x</var>
6.57/2.92	           </arg>
6.57/2.92	           <arg>
6.57/2.92	            <funapp>
6.57/2.92	             <name>0</name>
6.57/2.92	            </funapp>
6.57/2.92	           </arg>
6.57/2.92	          </funapp>
6.57/2.92	         </lhs>
6.57/2.92	         <rhs>
6.57/2.92	          <funapp>
6.57/2.92	           <name>false</name>
6.57/2.92	          </funapp>
6.57/2.92	         </rhs>
6.57/2.92	        </rule>
6.57/2.92	       </unravelingEntry>
6.57/2.92	       <unravelingEntry>
6.57/2.92	        <conditionalRule>
6.57/2.92	         <rule>
6.57/2.92	          <lhs>
6.57/2.92	           <funapp>
6.57/2.92	            <name>pop</name>
6.57/2.92	            <arg>
6.57/2.92	             <funapp>
6.57/2.92	              <name>push</name>
6.57/2.92	              <arg>
6.57/2.92	               <var>x</var>
6.57/2.92	              </arg>
6.57/2.92	              <arg>
6.57/2.92	               <var>y</var>
6.57/2.92	              </arg>
6.57/2.92	             </funapp>
6.57/2.92	            </arg>
6.57/2.92	           </funapp>
6.57/2.92	          </lhs>
6.57/2.92	          <rhs>
6.57/2.92	           <var>x</var>
6.57/2.92	          </rhs>
6.57/2.92	         </rule>
6.57/2.92	         <rule>
6.57/2.92	          <lhs>
6.57/2.92	           <funapp>
6.57/2.92	            <name>le</name>
6.57/2.92	            <arg>
6.57/2.92	             <funapp>
6.57/2.92	              <name>size</name>
6.57/2.92	              <arg>
6.57/2.92	               <var>x</var>
6.57/2.92	              </arg>
6.57/2.92	             </funapp>
6.57/2.92	            </arg>
6.57/2.92	            <arg>
6.57/2.92	             <funapp>
6.57/2.92	              <name>m</name>
6.57/2.92	             </funapp>
6.57/2.92	            </arg>
6.57/2.92	           </funapp>
6.57/2.92	          </lhs>
6.57/2.92	          <rhs>
6.57/2.92	           <funapp>
6.57/2.92	            <name>true</name>
6.57/2.92	           </funapp>
6.57/2.92	          </rhs>
6.57/2.92	         </rule>
6.57/2.92	        </conditionalRule>
6.57/2.92	        <rule>
6.57/2.92	         <lhs>
6.57/2.92	          <funapp>
6.57/2.92	           <name>pop</name>
6.57/2.92	           <arg>
6.57/2.92	            <funapp>
6.57/2.92	             <name>push</name>
6.57/2.92	             <arg>
6.57/2.92	              <var>x</var>
6.57/2.92	             </arg>
6.57/2.92	             <arg>
6.57/2.92	              <var>y</var>
6.57/2.92	             </arg>
6.57/2.92	            </funapp>
6.57/2.92	           </arg>
6.57/2.92	          </funapp>
6.57/2.92	         </lhs>
6.57/2.92	         <rhs>
6.57/2.92	          <funapp>
6.57/2.92	           <name>U1</name>
6.57/2.92	           <arg>
6.57/2.92	            <funapp>
6.57/2.92	             <name>le</name>
6.57/2.92	             <arg>
6.57/2.92	              <funapp>
6.57/2.92	               <name>size</name>
6.57/2.92	               <arg>
6.57/2.92	                <var>x</var>
6.57/2.92	               </arg>
6.57/2.92	              </funapp>
6.57/2.92	             </arg>
6.57/2.92	             <arg>
6.57/2.92	              <funapp>
6.57/2.92	               <name>m</name>
6.57/2.92	              </funapp>
6.57/2.92	             </arg>
6.57/2.92	            </funapp>
6.57/2.92	           </arg>
6.57/2.92	           <arg>
6.57/2.92	            <var>x</var>
6.57/2.92	           </arg>
6.57/2.92	           <arg>
6.57/2.92	            <var>y</var>
6.57/2.92	           </arg>
6.57/2.92	          </funapp>
6.57/2.92	         </rhs>
6.57/2.92	        </rule>
6.57/2.92	        <rule>
6.57/2.92	         <lhs>
6.57/2.92	          <funapp>
6.57/2.92	           <name>U1</name>
6.57/2.92	           <arg>
6.57/2.92	            <funapp>
6.57/2.92	             <name>true</name>
6.57/2.92	            </funapp>
6.57/2.92	           </arg>
6.57/2.92	           <arg>
6.57/2.92	            <var>x</var>
6.57/2.92	           </arg>
6.57/2.92	           <arg>
6.57/2.92	            <var>y</var>
6.57/2.92	           </arg>
6.57/2.92	          </funapp>
6.57/2.92	         </lhs>
6.57/2.92	         <rhs>
6.57/2.92	          <var>x</var>
6.57/2.92	         </rhs>
6.57/2.92	        </rule>
6.57/2.92	       </unravelingEntry>
6.57/2.92	       <unravelingEntry>
6.57/2.92	        <conditionalRule>
6.57/2.92	         <rule>
6.57/2.92	          <lhs>
6.57/2.92	           <funapp>
6.57/2.92	            <name>m</name>
6.57/2.92	           </funapp>
6.57/2.92	          </lhs>
6.57/2.92	          <rhs>
6.57/2.92	           <funapp>
6.57/2.92	            <name>s</name>
6.57/2.92	            <arg>
6.57/2.92	             <funapp>
6.57/2.92	              <name>s</name>
6.57/2.92	              <arg>
6.57/2.92	               <funapp>
6.57/2.92	                <name>s</name>
6.57/2.92	                <arg>
6.57/2.92	                 <funapp>
6.57/2.92	                  <name>s</name>
6.57/2.92	                  <arg>
6.57/2.92	                   <funapp>
6.57/2.92	                    <name>0</name>
6.57/2.92	                   </funapp>
6.57/2.92	                  </arg>
6.57/2.92	                 </funapp>
6.57/2.92	                </arg>
6.57/2.92	               </funapp>
6.57/2.92	              </arg>
6.57/2.92	             </funapp>
6.57/2.92	            </arg>
6.57/2.92	           </funapp>
6.57/2.92	          </rhs>
6.57/2.92	         </rule>
6.57/2.92	        </conditionalRule>
6.57/2.92	        <rule>
6.57/2.92	         <lhs>
6.57/2.92	          <funapp>
6.57/2.92	           <name>m</name>
6.57/2.92	          </funapp>
6.57/2.92	         </lhs>
6.57/2.92	         <rhs>
6.57/2.92	          <funapp>
6.57/2.92	           <name>s</name>
6.57/2.92	           <arg>
6.57/2.92	            <funapp>
6.57/2.92	             <name>s</name>
6.57/2.92	             <arg>
6.57/2.92	              <funapp>
6.57/2.92	               <name>s</name>
6.57/2.92	               <arg>
6.57/2.92	                <funapp>
6.57/2.92	                 <name>s</name>
6.57/2.92	                 <arg>
6.57/2.92	                  <funapp>
6.57/2.92	                   <name>0</name>
6.57/2.92	                  </funapp>
6.57/2.92	                 </arg>
6.57/2.92	                </funapp>
6.57/2.92	               </arg>
6.57/2.92	              </funapp>
6.57/2.92	             </arg>
6.57/2.92	            </funapp>
6.57/2.92	           </arg>
6.57/2.92	          </funapp>
6.57/2.92	         </rhs>
6.57/2.92	        </rule>
6.57/2.92	       </unravelingEntry>
6.57/2.92	       <unravelingEntry>
6.57/2.92	        <conditionalRule>
6.57/2.92	         <rule>
6.57/2.92	          <lhs>
6.57/2.92	           <funapp>
6.57/2.92	            <name>top</name>
6.57/2.92	            <arg>
6.57/2.92	             <funapp>
6.57/2.92	              <name>empty</name>
6.57/2.92	             </funapp>
6.57/2.92	            </arg>
6.57/2.92	           </funapp>
6.57/2.92	          </lhs>
6.57/2.92	          <rhs>
6.57/2.92	           <funapp>
6.57/2.92	            <name>eentry</name>
6.57/2.92	           </funapp>
6.57/2.92	          </rhs>
6.57/2.92	         </rule>
6.57/2.92	        </conditionalRule>
6.57/2.92	        <rule>
6.57/2.92	         <lhs>
6.57/2.92	          <funapp>
6.57/2.92	           <name>top</name>
6.57/2.92	           <arg>
6.57/2.92	            <funapp>
6.57/2.92	             <name>empty</name>
6.57/2.92	            </funapp>
6.57/2.92	           </arg>
6.57/2.92	          </funapp>
6.57/2.92	         </lhs>
6.57/2.92	         <rhs>
6.57/2.92	          <funapp>
6.57/2.92	           <name>eentry</name>
6.57/2.92	          </funapp>
6.57/2.92	         </rhs>
6.57/2.92	        </rule>
6.57/2.92	       </unravelingEntry>
6.57/2.92	      </unravelingInformation>
6.57/2.92	      <trsTerminationProof>
6.57/2.92	       <ruleRemoval>
6.57/2.92	        <orderingConstraintProof>
6.57/2.92	         <redPair>
6.57/2.92	          <interpretation>
6.57/2.92	           <type>
6.57/2.92	            <polynomial>
6.57/2.92	             <domain>
6.57/2.92	              <matrices>
6.57/2.92	               <dimension>3</dimension>
6.57/2.92	               <strictDimension>1</strictDimension>
6.57/2.92	               <domain>
6.57/2.92	                <naturals/>
6.57/2.92	               </domain>
6.57/2.92	              </matrices>
6.57/2.92	             </domain>
6.57/2.92	             <degree>1</degree>
6.57/2.92	            </polynomial>
6.57/2.92	           </type>
6.57/2.92	           <interpret>
6.57/2.92	            <name>eentry</name>
6.57/2.92	            <arity>0</arity>
6.57/2.92	            <polynomial>
6.57/2.92	             <sum>
6.57/2.92	              <polynomial>
6.57/2.92	               <coefficient>
6.57/2.92	                <matrix>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                </matrix>
6.57/2.92	               </coefficient>
6.57/2.92	              </polynomial>
6.57/2.92	             </sum>
6.57/2.92	            </polynomial>
6.57/2.92	           </interpret>
6.57/2.92	           <interpret>
6.57/2.92	            <name>U1</name>
6.57/2.92	            <arity>3</arity>
6.57/2.92	            <polynomial>
6.57/2.92	             <sum>
6.57/2.92	              <polynomial>
6.57/2.92	               <product>
6.57/2.92	                <polynomial>
6.57/2.92	                 <coefficient>
6.57/2.92	                  <matrix>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                  </matrix>
6.57/2.92	                 </coefficient>
6.57/2.92	                </polynomial>
6.57/2.92	                <polynomial>
6.57/2.92	                 <variable>1</variable>
6.57/2.92	                </polynomial>
6.57/2.92	               </product>
6.57/2.92	              </polynomial>
6.57/2.92	              <polynomial>
6.57/2.92	               <product>
6.57/2.92	                <polynomial>
6.57/2.92	                 <coefficient>
6.57/2.92	                  <matrix>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                  </matrix>
6.57/2.92	                 </coefficient>
6.57/2.92	                </polynomial>
6.57/2.92	                <polynomial>
6.57/2.92	                 <variable>2</variable>
6.57/2.92	                </polynomial>
6.57/2.92	               </product>
6.57/2.92	              </polynomial>
6.57/2.92	              <polynomial>
6.57/2.92	               <product>
6.57/2.92	                <polynomial>
6.57/2.92	                 <coefficient>
6.57/2.92	                  <matrix>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                  </matrix>
6.57/2.92	                 </coefficient>
6.57/2.92	                </polynomial>
6.57/2.92	                <polynomial>
6.57/2.92	                 <variable>3</variable>
6.57/2.92	                </polynomial>
6.57/2.92	               </product>
6.57/2.92	              </polynomial>
6.57/2.92	              <polynomial>
6.57/2.92	               <coefficient>
6.57/2.92	                <matrix>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                </matrix>
6.57/2.92	               </coefficient>
6.57/2.92	              </polynomial>
6.57/2.92	             </sum>
6.57/2.92	            </polynomial>
6.57/2.92	           </interpret>
6.57/2.92	           <interpret>
6.57/2.92	            <name>false</name>
6.57/2.92	            <arity>0</arity>
6.57/2.92	            <polynomial>
6.57/2.92	             <sum>
6.57/2.92	              <polynomial>
6.57/2.92	               <coefficient>
6.57/2.92	                <matrix>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>1</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                </matrix>
6.57/2.92	               </coefficient>
6.57/2.92	              </polynomial>
6.57/2.92	             </sum>
6.57/2.92	            </polynomial>
6.57/2.92	           </interpret>
6.57/2.92	           <interpret>
6.57/2.92	            <name>U2</name>
6.57/2.92	            <arity>3</arity>
6.57/2.92	            <polynomial>
6.57/2.92	             <sum>
6.57/2.92	              <polynomial>
6.57/2.92	               <product>
6.57/2.92	                <polynomial>
6.57/2.92	                 <coefficient>
6.57/2.92	                  <matrix>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                  </matrix>
6.57/2.92	                 </coefficient>
6.57/2.92	                </polynomial>
6.57/2.92	                <polynomial>
6.57/2.92	                 <variable>1</variable>
6.57/2.92	                </polynomial>
6.57/2.92	               </product>
6.57/2.92	              </polynomial>
6.57/2.92	              <polynomial>
6.57/2.92	               <product>
6.57/2.92	                <polynomial>
6.57/2.92	                 <coefficient>
6.57/2.92	                  <matrix>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                  </matrix>
6.57/2.92	                 </coefficient>
6.57/2.92	                </polynomial>
6.57/2.92	                <polynomial>
6.57/2.92	                 <variable>2</variable>
6.57/2.92	                </polynomial>
6.57/2.92	               </product>
6.57/2.92	              </polynomial>
6.57/2.92	              <polynomial>
6.57/2.92	               <product>
6.57/2.92	                <polynomial>
6.57/2.92	                 <coefficient>
6.57/2.92	                  <matrix>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                  </matrix>
6.57/2.92	                 </coefficient>
6.57/2.92	                </polynomial>
6.57/2.92	                <polynomial>
6.57/2.92	                 <variable>3</variable>
6.57/2.92	                </polynomial>
6.57/2.92	               </product>
6.57/2.92	              </polynomial>
6.57/2.92	              <polynomial>
6.57/2.92	               <coefficient>
6.57/2.92	                <matrix>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                </matrix>
6.57/2.92	               </coefficient>
6.57/2.92	              </polynomial>
6.57/2.92	             </sum>
6.57/2.92	            </polynomial>
6.57/2.92	           </interpret>
6.57/2.92	           <interpret>
6.57/2.92	            <name>m</name>
6.57/2.92	            <arity>0</arity>
6.57/2.92	            <polynomial>
6.57/2.92	             <sum>
6.57/2.92	              <polynomial>
6.57/2.92	               <coefficient>
6.57/2.92	                <matrix>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>1</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                </matrix>
6.57/2.92	               </coefficient>
6.57/2.92	              </polynomial>
6.57/2.92	             </sum>
6.57/2.92	            </polynomial>
6.57/2.92	           </interpret>
6.57/2.92	           <interpret>
6.57/2.92	            <name>size</name>
6.57/2.92	            <arity>1</arity>
6.57/2.92	            <polynomial>
6.57/2.92	             <sum>
6.57/2.92	              <polynomial>
6.57/2.92	               <product>
6.57/2.92	                <polynomial>
6.57/2.92	                 <coefficient>
6.57/2.92	                  <matrix>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                  </matrix>
6.57/2.92	                 </coefficient>
6.57/2.92	                </polynomial>
6.57/2.92	                <polynomial>
6.57/2.92	                 <variable>1</variable>
6.57/2.92	                </polynomial>
6.57/2.92	               </product>
6.57/2.92	              </polynomial>
6.57/2.92	              <polynomial>
6.57/2.92	               <coefficient>
6.57/2.92	                <matrix>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>1</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                </matrix>
6.57/2.92	               </coefficient>
6.57/2.92	              </polynomial>
6.57/2.92	             </sum>
6.57/2.92	            </polynomial>
6.57/2.92	           </interpret>
6.57/2.92	           <interpret>
6.57/2.92	            <name>top</name>
6.57/2.92	            <arity>1</arity>
6.57/2.92	            <polynomial>
6.57/2.92	             <sum>
6.57/2.92	              <polynomial>
6.57/2.92	               <product>
6.57/2.92	                <polynomial>
6.57/2.92	                 <coefficient>
6.57/2.92	                  <matrix>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                  </matrix>
6.57/2.92	                 </coefficient>
6.57/2.92	                </polynomial>
6.57/2.92	                <polynomial>
6.57/2.92	                 <variable>1</variable>
6.57/2.92	                </polynomial>
6.57/2.92	               </product>
6.57/2.92	              </polynomial>
6.57/2.92	              <polynomial>
6.57/2.92	               <coefficient>
6.57/2.92	                <matrix>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>1</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                </matrix>
6.57/2.92	               </coefficient>
6.57/2.92	              </polynomial>
6.57/2.92	             </sum>
6.57/2.92	            </polynomial>
6.57/2.92	           </interpret>
6.57/2.92	           <interpret>
6.57/2.92	            <name>push</name>
6.57/2.92	            <arity>2</arity>
6.57/2.92	            <polynomial>
6.57/2.92	             <sum>
6.57/2.92	              <polynomial>
6.57/2.92	               <product>
6.57/2.92	                <polynomial>
6.57/2.92	                 <coefficient>
6.57/2.92	                  <matrix>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                  </matrix>
6.57/2.92	                 </coefficient>
6.57/2.92	                </polynomial>
6.57/2.92	                <polynomial>
6.57/2.92	                 <variable>1</variable>
6.57/2.92	                </polynomial>
6.57/2.92	               </product>
6.57/2.92	              </polynomial>
6.57/2.92	              <polynomial>
6.57/2.92	               <product>
6.57/2.92	                <polynomial>
6.57/2.92	                 <coefficient>
6.57/2.92	                  <matrix>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                  </matrix>
6.57/2.92	                 </coefficient>
6.57/2.92	                </polynomial>
6.57/2.92	                <polynomial>
6.57/2.92	                 <variable>2</variable>
6.57/2.92	                </polynomial>
6.57/2.92	               </product>
6.57/2.92	              </polynomial>
6.57/2.92	              <polynomial>
6.57/2.92	               <coefficient>
6.57/2.92	                <matrix>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>1</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>1</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>1</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                </matrix>
6.57/2.92	               </coefficient>
6.57/2.92	              </polynomial>
6.57/2.92	             </sum>
6.57/2.92	            </polynomial>
6.57/2.92	           </interpret>
6.57/2.92	           <interpret>
6.57/2.92	            <name>true</name>
6.57/2.92	            <arity>0</arity>
6.57/2.92	            <polynomial>
6.57/2.92	             <sum>
6.57/2.92	              <polynomial>
6.57/2.92	               <coefficient>
6.57/2.92	                <matrix>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                </matrix>
6.57/2.92	               </coefficient>
6.57/2.92	              </polynomial>
6.57/2.92	             </sum>
6.57/2.92	            </polynomial>
6.57/2.92	           </interpret>
6.57/2.92	           <interpret>
6.57/2.92	            <name>le</name>
6.57/2.92	            <arity>2</arity>
6.57/2.92	            <polynomial>
6.57/2.92	             <sum>
6.57/2.92	              <polynomial>
6.57/2.92	               <product>
6.57/2.92	                <polynomial>
6.57/2.92	                 <coefficient>
6.57/2.92	                  <matrix>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                  </matrix>
6.57/2.92	                 </coefficient>
6.57/2.92	                </polynomial>
6.57/2.92	                <polynomial>
6.57/2.92	                 <variable>1</variable>
6.57/2.92	                </polynomial>
6.57/2.92	               </product>
6.57/2.92	              </polynomial>
6.57/2.92	              <polynomial>
6.57/2.92	               <product>
6.57/2.92	                <polynomial>
6.57/2.92	                 <coefficient>
6.57/2.92	                  <matrix>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                  </matrix>
6.57/2.92	                 </coefficient>
6.57/2.92	                </polynomial>
6.57/2.92	                <polynomial>
6.57/2.92	                 <variable>2</variable>
6.57/2.92	                </polynomial>
6.57/2.92	               </product>
6.57/2.92	              </polynomial>
6.57/2.92	              <polynomial>
6.57/2.92	               <coefficient>
6.57/2.92	                <matrix>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>1</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                </matrix>
6.57/2.92	               </coefficient>
6.57/2.92	              </polynomial>
6.57/2.92	             </sum>
6.57/2.92	            </polynomial>
6.57/2.92	           </interpret>
6.57/2.92	           <interpret>
6.57/2.92	            <name>s</name>
6.57/2.92	            <arity>1</arity>
6.57/2.92	            <polynomial>
6.57/2.92	             <sum>
6.57/2.92	              <polynomial>
6.57/2.92	               <product>
6.57/2.92	                <polynomial>
6.57/2.92	                 <coefficient>
6.57/2.92	                  <matrix>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                  </matrix>
6.57/2.92	                 </coefficient>
6.57/2.92	                </polynomial>
6.57/2.92	                <polynomial>
6.57/2.92	                 <variable>1</variable>
6.57/2.92	                </polynomial>
6.57/2.92	               </product>
6.57/2.92	              </polynomial>
6.57/2.92	              <polynomial>
6.57/2.92	               <coefficient>
6.57/2.92	                <matrix>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                </matrix>
6.57/2.92	               </coefficient>
6.57/2.92	              </polynomial>
6.57/2.92	             </sum>
6.57/2.92	            </polynomial>
6.57/2.92	           </interpret>
6.57/2.92	           <interpret>
6.57/2.92	            <name>0</name>
6.57/2.92	            <arity>0</arity>
6.57/2.92	            <polynomial>
6.57/2.92	             <sum>
6.57/2.92	              <polynomial>
6.57/2.92	               <coefficient>
6.57/2.92	                <matrix>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>1</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                </matrix>
6.57/2.92	               </coefficient>
6.57/2.92	              </polynomial>
6.57/2.92	             </sum>
6.57/2.92	            </polynomial>
6.57/2.92	           </interpret>
6.57/2.92	           <interpret>
6.57/2.92	            <name>pop</name>
6.57/2.92	            <arity>1</arity>
6.57/2.92	            <polynomial>
6.57/2.92	             <sum>
6.57/2.92	              <polynomial>
6.57/2.92	               <product>
6.57/2.92	                <polynomial>
6.57/2.92	                 <coefficient>
6.57/2.92	                  <matrix>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                  </matrix>
6.57/2.92	                 </coefficient>
6.57/2.92	                </polynomial>
6.57/2.92	                <polynomial>
6.57/2.92	                 <variable>1</variable>
6.57/2.92	                </polynomial>
6.57/2.92	               </product>
6.57/2.92	              </polynomial>
6.57/2.92	              <polynomial>
6.57/2.92	               <coefficient>
6.57/2.92	                <matrix>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>1</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                </matrix>
6.57/2.92	               </coefficient>
6.57/2.92	              </polynomial>
6.57/2.92	             </sum>
6.57/2.92	            </polynomial>
6.57/2.92	           </interpret>
6.57/2.92	           <interpret>
6.57/2.92	            <name>empty</name>
6.57/2.92	            <arity>0</arity>
6.57/2.92	            <polynomial>
6.57/2.92	             <sum>
6.57/2.92	              <polynomial>
6.57/2.92	               <coefficient>
6.57/2.92	                <matrix>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>1</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                 <vector>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                  <coefficient>
6.57/2.92	                   <integer>0</integer>
6.57/2.92	                  </coefficient>
6.57/2.92	                 </vector>
6.57/2.92	                </matrix>
6.57/2.92	               </coefficient>
6.57/2.92	              </polynomial>
6.57/2.92	             </sum>
6.57/2.92	            </polynomial>
6.57/2.92	           </interpret>
6.57/2.92	          </interpretation>
6.57/2.92	         </redPair>
6.57/2.92	        </orderingConstraintProof>
6.57/2.92	        <trs>
6.57/2.92	         <rules>
6.57/2.92	          <rule>
6.57/2.92	           <lhs>
6.57/2.92	            <funapp>
6.57/2.92	             <name>le</name>
6.57/2.92	             <arg>
6.57/2.92	              <funapp>
6.57/2.92	               <name>0</name>
6.57/2.92	              </funapp>
6.57/2.92	             </arg>
6.57/2.92	             <arg>
6.57/2.92	              <funapp>
6.57/2.92	               <name>s</name>
6.57/2.92	               <arg>
6.57/2.92	                <var>x</var>
6.57/2.92	               </arg>
6.57/2.92	              </funapp>
6.57/2.92	             </arg>
6.57/2.92	            </funapp>
6.57/2.92	           </lhs>
6.57/2.92	           <rhs>
6.57/2.92	            <funapp>
6.57/2.92	             <name>true</name>
6.57/2.92	            </funapp>
6.57/2.92	           </rhs>
6.57/2.92	          </rule>
6.57/2.92	          <rule>
6.57/2.92	           <lhs>
6.57/2.92	            <funapp>
6.57/2.92	             <name>U2</name>
6.57/2.92	             <arg>
6.57/2.92	              <funapp>
6.57/2.92	               <name>true</name>
6.57/2.92	              </funapp>
6.57/2.92	             </arg>
6.57/2.92	             <arg>
6.57/2.92	              <var>x</var>
6.57/2.92	             </arg>
6.57/2.92	             <arg>
6.57/2.92	              <var>y</var>
6.57/2.92	             </arg>
6.57/2.92	            </funapp>
6.57/2.92	           </lhs>
6.57/2.92	           <rhs>
6.57/2.92	            <var>y</var>
6.57/2.92	           </rhs>
6.57/2.92	          </rule>
6.57/2.92	          <rule>
6.57/2.92	           <lhs>
6.57/2.92	            <funapp>
6.57/2.92	             <name>le</name>
6.57/2.92	             <arg>
6.57/2.92	              <funapp>
6.57/2.92	               <name>s</name>
6.57/2.92	               <arg>
6.57/2.92	                <var>x</var>
6.57/2.92	               </arg>
6.57/2.92	              </funapp>
6.57/2.92	             </arg>
6.57/2.92	             <arg>
6.57/2.92	              <funapp>
6.57/2.92	               <name>s</name>
6.57/2.92	               <arg>
6.57/2.92	                <var>y</var>
6.57/2.92	               </arg>
6.57/2.92	              </funapp>
6.57/2.92	             </arg>
6.57/2.92	            </funapp>
6.57/2.92	           </lhs>
6.57/2.92	           <rhs>
6.57/2.92	            <funapp>
6.57/2.92	             <name>le</name>
6.57/2.92	             <arg>
6.57/2.92	              <var>x</var>
6.57/2.92	             </arg>
6.57/2.92	             <arg>
6.57/2.92	              <var>y</var>
6.57/2.92	             </arg>
6.57/2.92	            </funapp>
6.57/2.92	           </rhs>
6.57/2.92	          </rule>
6.57/2.92	          <rule>
6.57/2.92	           <lhs>
6.57/2.92	            <funapp>
6.57/2.92	             <name>le</name>
6.57/2.92	             <arg>
6.57/2.92	              <var>x</var>
6.57/2.92	             </arg>
6.57/2.92	             <arg>
6.57/2.92	              <funapp>
6.57/2.92	               <name>0</name>
6.57/2.92	              </funapp>
6.57/2.92	             </arg>
6.57/2.92	            </funapp>
6.57/2.92	           </lhs>
6.57/2.92	           <rhs>
6.57/2.92	            <funapp>
6.57/2.92	             <name>false</name>
6.57/2.92	            </funapp>
6.57/2.92	           </rhs>
6.57/2.92	          </rule>
6.57/2.92	          <rule>
6.57/2.92	           <lhs>
6.57/2.92	            <funapp>
6.57/2.92	             <name>pop</name>
6.57/2.92	             <arg>
6.57/2.92	              <funapp>
6.57/2.92	               <name>push</name>
6.57/2.92	               <arg>
6.57/2.92	                <var>x</var>
6.57/2.92	               </arg>
6.57/2.92	               <arg>
6.57/2.92	                <var>y</var>
6.57/2.92	               </arg>
6.57/2.92	              </funapp>
6.57/2.92	             </arg>
6.57/2.92	            </funapp>
6.57/2.92	           </lhs>
6.57/2.92	           <rhs>
6.57/2.92	            <funapp>
6.57/2.92	             <name>U1</name>
6.57/2.92	             <arg>
6.57/2.92	              <funapp>
6.57/2.92	               <name>le</name>
6.57/2.92	               <arg>
6.57/2.92	                <funapp>
6.57/2.92	                 <name>size</name>
6.57/2.92	                 <arg>
6.57/2.92	                  <var>x</var>
6.57/2.92	                 </arg>
6.57/2.92	                </funapp>
6.57/2.92	               </arg>
6.57/2.92	               <arg>
6.57/2.92	                <funapp>
6.57/2.92	                 <name>m</name>
6.57/2.92	                </funapp>
6.57/2.92	               </arg>
6.57/2.92	              </funapp>
6.57/2.92	             </arg>
6.57/2.92	             <arg>
6.57/2.92	              <var>x</var>
6.57/2.92	             </arg>
6.57/2.92	             <arg>
6.57/2.92	              <var>y</var>
6.57/2.92	             </arg>
6.57/2.92	            </funapp>
6.57/2.92	           </rhs>
6.57/2.92	          </rule>
6.57/2.92	          <rule>
6.57/2.92	           <lhs>
6.57/2.92	            <funapp>
6.57/2.92	             <name>U1</name>
6.57/2.92	             <arg>
6.57/2.92	              <funapp>
6.57/2.92	               <name>true</name>
6.57/2.92	              </funapp>
6.57/2.92	             </arg>
6.57/2.92	             <arg>
6.57/2.92	              <var>x</var>
6.57/2.92	             </arg>
6.57/2.92	             <arg>
6.57/2.92	              <var>y</var>
6.57/2.92	             </arg>
6.57/2.92	            </funapp>
6.57/2.92	           </lhs>
6.57/2.92	           <rhs>
6.57/2.92	            <var>x</var>
6.57/2.92	           </rhs>
6.57/2.92	          </rule>
6.57/2.92	          <rule>
6.57/2.92	           <lhs>
6.57/2.92	            <funapp>
6.57/2.92	             <name>m</name>
6.57/2.92	            </funapp>
6.57/2.92	           </lhs>
6.57/2.92	           <rhs>
6.57/2.92	            <funapp>
6.57/2.92	             <name>s</name>
6.57/2.92	             <arg>
6.57/2.92	              <funapp>
6.57/2.92	               <name>s</name>
6.57/2.92	               <arg>
6.57/2.92	                <funapp>
6.57/2.92	                 <name>s</name>
6.57/2.92	                 <arg>
6.57/2.92	                  <funapp>
6.57/2.92	                   <name>s</name>
6.57/2.92	                   <arg>
6.57/2.92	                    <funapp>
6.57/2.92	                     <name>0</name>
6.57/2.92	                    </funapp>
6.57/2.92	                   </arg>
6.57/2.92	                  </funapp>
6.57/2.92	                 </arg>
6.57/2.92	                </funapp>
6.57/2.92	               </arg>
6.57/2.92	              </funapp>
6.57/2.92	             </arg>
6.57/2.92	            </funapp>
6.57/2.92	           </rhs>
6.57/2.92	          </rule>
6.57/2.92	         </rules>
6.57/2.92	        </trs>
6.57/2.92	        <trsTerminationProof>
6.57/2.92	         <ruleRemoval>
6.57/2.92	          <orderingConstraintProof>
6.57/2.92	           <redPair>
6.57/2.92	            <interpretation>
6.57/2.92	             <type>
6.57/2.92	              <polynomial>
6.57/2.92	               <domain>
6.57/2.92	                <matrices>
6.57/2.92	                 <dimension>3</dimension>
6.57/2.92	                 <strictDimension>1</strictDimension>
6.57/2.92	                 <domain>
6.57/2.92	                  <naturals/>
6.57/2.92	                 </domain>
6.57/2.92	                </matrices>
6.57/2.92	               </domain>
6.57/2.92	               <degree>1</degree>
6.57/2.92	              </polynomial>
6.57/2.92	             </type>
6.57/2.92	             <interpret>
6.57/2.92	              <name>U1</name>
6.57/2.92	              <arity>3</arity>
6.57/2.92	              <polynomial>
6.57/2.92	               <sum>
6.57/2.92	                <polynomial>
6.57/2.92	                 <product>
6.57/2.92	                  <polynomial>
6.57/2.92	                   <coefficient>
6.57/2.92	                    <matrix>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>1</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                    </matrix>
6.57/2.92	                   </coefficient>
6.57/2.92	                  </polynomial>
6.57/2.92	                  <polynomial>
6.57/2.92	                   <variable>1</variable>
6.57/2.92	                  </polynomial>
6.57/2.92	                 </product>
6.57/2.92	                </polynomial>
6.57/2.92	                <polynomial>
6.57/2.92	                 <product>
6.57/2.92	                  <polynomial>
6.57/2.92	                   <coefficient>
6.57/2.92	                    <matrix>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>1</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>1</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>1</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>1</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                    </matrix>
6.57/2.92	                   </coefficient>
6.57/2.92	                  </polynomial>
6.57/2.92	                  <polynomial>
6.57/2.92	                   <variable>2</variable>
6.57/2.92	                  </polynomial>
6.57/2.92	                 </product>
6.57/2.92	                </polynomial>
6.57/2.92	                <polynomial>
6.57/2.92	                 <product>
6.57/2.92	                  <polynomial>
6.57/2.92	                   <coefficient>
6.57/2.92	                    <matrix>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>1</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>1</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                    </matrix>
6.57/2.92	                   </coefficient>
6.57/2.92	                  </polynomial>
6.57/2.92	                  <polynomial>
6.57/2.92	                   <variable>3</variable>
6.57/2.92	                  </polynomial>
6.57/2.92	                 </product>
6.57/2.92	                </polynomial>
6.57/2.92	                <polynomial>
6.57/2.92	                 <coefficient>
6.57/2.92	                  <matrix>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                  </matrix>
6.57/2.92	                 </coefficient>
6.57/2.92	                </polynomial>
6.57/2.92	               </sum>
6.57/2.92	              </polynomial>
6.57/2.92	             </interpret>
6.57/2.92	             <interpret>
6.57/2.92	              <name>false</name>
6.57/2.92	              <arity>0</arity>
6.57/2.92	              <polynomial>
6.57/2.92	               <sum>
6.57/2.92	                <polynomial>
6.57/2.92	                 <coefficient>
6.57/2.92	                  <matrix>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                  </matrix>
6.57/2.92	                 </coefficient>
6.57/2.92	                </polynomial>
6.57/2.92	               </sum>
6.57/2.92	              </polynomial>
6.57/2.92	             </interpret>
6.57/2.92	             <interpret>
6.57/2.92	              <name>U2</name>
6.57/2.92	              <arity>3</arity>
6.57/2.92	              <polynomial>
6.57/2.92	               <sum>
6.57/2.92	                <polynomial>
6.57/2.92	                 <product>
6.57/2.92	                  <polynomial>
6.57/2.92	                   <coefficient>
6.57/2.92	                    <matrix>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>1</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                    </matrix>
6.57/2.92	                   </coefficient>
6.57/2.92	                  </polynomial>
6.57/2.92	                  <polynomial>
6.57/2.92	                   <variable>1</variable>
6.57/2.92	                  </polynomial>
6.57/2.92	                 </product>
6.57/2.92	                </polynomial>
6.57/2.92	                <polynomial>
6.57/2.92	                 <product>
6.57/2.92	                  <polynomial>
6.57/2.92	                   <coefficient>
6.57/2.92	                    <matrix>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>1</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                    </matrix>
6.57/2.92	                   </coefficient>
6.57/2.92	                  </polynomial>
6.57/2.92	                  <polynomial>
6.57/2.92	                   <variable>2</variable>
6.57/2.92	                  </polynomial>
6.57/2.92	                 </product>
6.57/2.92	                </polynomial>
6.57/2.92	                <polynomial>
6.57/2.92	                 <product>
6.57/2.92	                  <polynomial>
6.57/2.92	                   <coefficient>
6.57/2.92	                    <matrix>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>1</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>1</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>1</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                    </matrix>
6.57/2.92	                   </coefficient>
6.57/2.92	                  </polynomial>
6.57/2.92	                  <polynomial>
6.57/2.92	                   <variable>3</variable>
6.57/2.92	                  </polynomial>
6.57/2.92	                 </product>
6.57/2.92	                </polynomial>
6.57/2.92	                <polynomial>
6.57/2.92	                 <coefficient>
6.57/2.92	                  <matrix>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                  </matrix>
6.57/2.92	                 </coefficient>
6.57/2.92	                </polynomial>
6.57/2.92	               </sum>
6.57/2.92	              </polynomial>
6.57/2.92	             </interpret>
6.57/2.92	             <interpret>
6.57/2.92	              <name>m</name>
6.57/2.92	              <arity>0</arity>
6.57/2.92	              <polynomial>
6.57/2.92	               <sum>
6.57/2.92	                <polynomial>
6.57/2.92	                 <coefficient>
6.57/2.92	                  <matrix>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                  </matrix>
6.57/2.92	                 </coefficient>
6.57/2.92	                </polynomial>
6.57/2.92	               </sum>
6.57/2.92	              </polynomial>
6.57/2.92	             </interpret>
6.57/2.92	             <interpret>
6.57/2.92	              <name>size</name>
6.57/2.92	              <arity>1</arity>
6.57/2.92	              <polynomial>
6.57/2.92	               <sum>
6.57/2.92	                <polynomial>
6.57/2.92	                 <product>
6.57/2.92	                  <polynomial>
6.57/2.92	                   <coefficient>
6.57/2.92	                    <matrix>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>1</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                    </matrix>
6.57/2.92	                   </coefficient>
6.57/2.92	                  </polynomial>
6.57/2.92	                  <polynomial>
6.57/2.92	                   <variable>1</variable>
6.57/2.92	                  </polynomial>
6.57/2.92	                 </product>
6.57/2.92	                </polynomial>
6.57/2.92	                <polynomial>
6.57/2.92	                 <coefficient>
6.57/2.92	                  <matrix>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                  </matrix>
6.57/2.92	                 </coefficient>
6.57/2.92	                </polynomial>
6.57/2.92	               </sum>
6.57/2.92	              </polynomial>
6.57/2.92	             </interpret>
6.57/2.92	             <interpret>
6.57/2.92	              <name>push</name>
6.57/2.92	              <arity>2</arity>
6.57/2.92	              <polynomial>
6.57/2.92	               <sum>
6.57/2.92	                <polynomial>
6.57/2.92	                 <product>
6.57/2.92	                  <polynomial>
6.57/2.92	                   <coefficient>
6.57/2.92	                    <matrix>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>1</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>1</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>1</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>1</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                    </matrix>
6.57/2.92	                   </coefficient>
6.57/2.92	                  </polynomial>
6.57/2.92	                  <polynomial>
6.57/2.92	                   <variable>1</variable>
6.57/2.92	                  </polynomial>
6.57/2.92	                 </product>
6.57/2.92	                </polynomial>
6.57/2.92	                <polynomial>
6.57/2.92	                 <product>
6.57/2.92	                  <polynomial>
6.57/2.92	                   <coefficient>
6.57/2.92	                    <matrix>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>1</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>1</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                    </matrix>
6.57/2.92	                   </coefficient>
6.57/2.92	                  </polynomial>
6.57/2.92	                  <polynomial>
6.57/2.92	                   <variable>2</variable>
6.57/2.92	                  </polynomial>
6.57/2.92	                 </product>
6.57/2.92	                </polynomial>
6.57/2.92	                <polynomial>
6.57/2.92	                 <coefficient>
6.57/2.92	                  <matrix>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>1</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                  </matrix>
6.57/2.92	                 </coefficient>
6.57/2.92	                </polynomial>
6.57/2.92	               </sum>
6.57/2.92	              </polynomial>
6.57/2.92	             </interpret>
6.57/2.92	             <interpret>
6.57/2.92	              <name>true</name>
6.57/2.92	              <arity>0</arity>
6.57/2.92	              <polynomial>
6.57/2.92	               <sum>
6.57/2.92	                <polynomial>
6.57/2.92	                 <coefficient>
6.57/2.92	                  <matrix>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                   <vector>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                    <coefficient>
6.57/2.92	                     <integer>0</integer>
6.57/2.92	                    </coefficient>
6.57/2.92	                   </vector>
6.57/2.92	                  </matrix>
6.57/2.92	                 </coefficient>
6.57/2.92	                </polynomial>
6.57/2.92	               </sum>
6.57/2.92	              </polynomial>
6.57/2.92	             </interpret>
6.57/2.92	             <interpret>
6.57/2.92	              <name>le</name>
6.57/2.92	              <arity>2</arity>
6.57/2.92	              <polynomial>
6.57/2.92	               <sum>
6.57/2.92	                <polynomial>
6.57/2.92	                 <product>
6.57/2.92	                  <polynomial>
6.57/2.92	                   <coefficient>
6.57/2.92	                    <matrix>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>1</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                     </vector>
6.57/2.92	                     <vector>
6.57/2.92	                      <coefficient>
6.57/2.92	                       <integer>0</integer>
6.57/2.92	                      </coefficient>
6.57/2.92	                      <coefficient>
6.57/2.93	                       <integer>0</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>0</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                     </vector>
6.57/2.93	                     <vector>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>0</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>0</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>0</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                     </vector>
6.57/2.93	                    </matrix>
6.57/2.93	                   </coefficient>
6.57/2.93	                  </polynomial>
6.57/2.93	                  <polynomial>
6.57/2.93	                   <variable>1</variable>
6.57/2.93	                  </polynomial>
6.57/2.93	                 </product>
6.57/2.93	                </polynomial>
6.57/2.93	                <polynomial>
6.57/2.93	                 <product>
6.57/2.93	                  <polynomial>
6.57/2.93	                   <coefficient>
6.57/2.93	                    <matrix>
6.57/2.93	                     <vector>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>1</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>0</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>0</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                     </vector>
6.57/2.93	                     <vector>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>0</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>0</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>0</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                     </vector>
6.57/2.93	                     <vector>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>0</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>0</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>0</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                     </vector>
6.57/2.93	                    </matrix>
6.57/2.93	                   </coefficient>
6.57/2.93	                  </polynomial>
6.57/2.93	                  <polynomial>
6.57/2.93	                   <variable>2</variable>
6.57/2.93	                  </polynomial>
6.57/2.93	                 </product>
6.57/2.93	                </polynomial>
6.57/2.93	                <polynomial>
6.57/2.93	                 <coefficient>
6.57/2.93	                  <matrix>
6.57/2.93	                   <vector>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                   </vector>
6.57/2.93	                   <vector>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                   </vector>
6.57/2.93	                   <vector>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                   </vector>
6.57/2.93	                  </matrix>
6.57/2.93	                 </coefficient>
6.57/2.93	                </polynomial>
6.57/2.93	               </sum>
6.57/2.93	              </polynomial>
6.57/2.93	             </interpret>
6.57/2.93	             <interpret>
6.57/2.93	              <name>s</name>
6.57/2.93	              <arity>1</arity>
6.57/2.93	              <polynomial>
6.57/2.93	               <sum>
6.57/2.93	                <polynomial>
6.57/2.93	                 <product>
6.57/2.93	                  <polynomial>
6.57/2.93	                   <coefficient>
6.57/2.93	                    <matrix>
6.57/2.93	                     <vector>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>1</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>0</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>0</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                     </vector>
6.57/2.93	                     <vector>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>0</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>0</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>1</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                     </vector>
6.57/2.93	                     <vector>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>0</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>0</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>0</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                     </vector>
6.57/2.93	                    </matrix>
6.57/2.93	                   </coefficient>
6.57/2.93	                  </polynomial>
6.57/2.93	                  <polynomial>
6.57/2.93	                   <variable>1</variable>
6.57/2.93	                  </polynomial>
6.57/2.93	                 </product>
6.57/2.93	                </polynomial>
6.57/2.93	                <polynomial>
6.57/2.93	                 <coefficient>
6.57/2.93	                  <matrix>
6.57/2.93	                   <vector>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                   </vector>
6.57/2.93	                   <vector>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                   </vector>
6.57/2.93	                   <vector>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                   </vector>
6.57/2.93	                  </matrix>
6.57/2.93	                 </coefficient>
6.57/2.93	                </polynomial>
6.57/2.93	               </sum>
6.57/2.93	              </polynomial>
6.57/2.93	             </interpret>
6.57/2.93	             <interpret>
6.57/2.93	              <name>0</name>
6.57/2.93	              <arity>0</arity>
6.57/2.93	              <polynomial>
6.57/2.93	               <sum>
6.57/2.93	                <polynomial>
6.57/2.93	                 <coefficient>
6.57/2.93	                  <matrix>
6.57/2.93	                   <vector>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>1</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                   </vector>
6.57/2.93	                   <vector>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                   </vector>
6.57/2.93	                   <vector>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                   </vector>
6.57/2.93	                  </matrix>
6.57/2.93	                 </coefficient>
6.57/2.93	                </polynomial>
6.57/2.93	               </sum>
6.57/2.93	              </polynomial>
6.57/2.93	             </interpret>
6.57/2.93	             <interpret>
6.57/2.93	              <name>pop</name>
6.57/2.93	              <arity>1</arity>
6.57/2.93	              <polynomial>
6.57/2.93	               <sum>
6.57/2.93	                <polynomial>
6.57/2.93	                 <product>
6.57/2.93	                  <polynomial>
6.57/2.93	                   <coefficient>
6.57/2.93	                    <matrix>
6.57/2.93	                     <vector>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>1</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>0</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>1</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                     </vector>
6.57/2.93	                     <vector>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>1</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>0</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>0</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                     </vector>
6.57/2.93	                     <vector>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>0</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>1</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                      <coefficient>
6.57/2.93	                       <integer>1</integer>
6.57/2.93	                      </coefficient>
6.57/2.93	                     </vector>
6.57/2.93	                    </matrix>
6.57/2.93	                   </coefficient>
6.57/2.93	                  </polynomial>
6.57/2.93	                  <polynomial>
6.57/2.93	                   <variable>1</variable>
6.57/2.93	                  </polynomial>
6.57/2.93	                 </product>
6.57/2.93	                </polynomial>
6.57/2.93	                <polynomial>
6.57/2.93	                 <coefficient>
6.57/2.93	                  <matrix>
6.57/2.93	                   <vector>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>1</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>1</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                   </vector>
6.57/2.93	                   <vector>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                   </vector>
6.57/2.93	                   <vector>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                    <coefficient>
6.57/2.93	                     <integer>0</integer>
6.57/2.93	                    </coefficient>
6.57/2.93	                   </vector>
6.57/2.93	                  </matrix>
6.57/2.93	                 </coefficient>
6.57/2.93	                </polynomial>
6.57/2.93	               </sum>
6.57/2.93	              </polynomial>
6.57/2.93	             </interpret>
6.57/2.93	            </interpretation>
6.57/2.93	           </redPair>
6.57/2.93	          </orderingConstraintProof>
6.57/2.93	          <trs>
6.57/2.93	           <rules>
6.57/2.93	            <rule>
6.57/2.93	             <lhs>
6.57/2.93	              <funapp>
6.57/2.93	               <name>le</name>
6.57/2.93	               <arg>
6.57/2.93	                <funapp>
6.57/2.93	                 <name>0</name>
6.57/2.93	                </funapp>
6.57/2.93	               </arg>
6.57/2.93	               <arg>
6.57/2.93	                <funapp>
6.57/2.93	                 <name>s</name>
6.57/2.93	                 <arg>
6.57/2.93	                  <var>x</var>
6.57/2.93	                 </arg>
6.57/2.93	                </funapp>
6.57/2.93	               </arg>
6.57/2.93	              </funapp>
6.57/2.93	             </lhs>
6.57/2.93	             <rhs>
6.57/2.93	              <funapp>
6.57/2.93	               <name>true</name>
6.57/2.93	              </funapp>
6.57/2.93	             </rhs>
6.57/2.93	            </rule>
6.57/2.93	            <rule>
6.57/2.93	             <lhs>
6.57/2.93	              <funapp>
6.57/2.93	               <name>U2</name>
6.57/2.93	               <arg>
6.57/2.93	                <funapp>
6.57/2.93	                 <name>true</name>
6.57/2.93	                </funapp>
6.57/2.93	               </arg>
6.57/2.93	               <arg>
6.57/2.93	                <var>x</var>
6.57/2.93	               </arg>
6.57/2.93	               <arg>
6.57/2.93	                <var>y</var>
6.57/2.93	               </arg>
6.57/2.93	              </funapp>
6.57/2.93	             </lhs>
6.57/2.93	             <rhs>
6.57/2.93	              <var>y</var>
6.57/2.93	             </rhs>
6.57/2.93	            </rule>
6.57/2.93	            <rule>
6.57/2.93	             <lhs>
6.57/2.93	              <funapp>
6.57/2.93	               <name>le</name>
6.57/2.93	               <arg>
6.57/2.93	                <funapp>
6.57/2.93	                 <name>s</name>
6.57/2.93	                 <arg>
6.57/2.93	                  <var>x</var>
6.57/2.93	                 </arg>
6.57/2.93	                </funapp>
6.57/2.93	               </arg>
6.57/2.93	               <arg>
6.57/2.93	                <funapp>
6.57/2.93	                 <name>s</name>
6.57/2.93	                 <arg>
6.57/2.93	                  <var>y</var>
6.57/2.93	                 </arg>
6.57/2.93	                </funapp>
6.57/2.93	               </arg>
6.57/2.93	              </funapp>
6.57/2.93	             </lhs>
6.57/2.93	             <rhs>
6.57/2.93	              <funapp>
6.57/2.93	               <name>le</name>
6.57/2.93	               <arg>
6.57/2.93	                <var>x</var>
6.57/2.93	               </arg>
6.57/2.93	               <arg>
6.57/2.93	                <var>y</var>
6.57/2.93	               </arg>
6.57/2.93	              </funapp>
6.57/2.93	             </rhs>
6.57/2.93	            </rule>
6.57/2.93	            <rule>
6.57/2.93	             <lhs>
6.57/2.93	              <funapp>
6.57/2.93	               <name>le</name>
6.57/2.93	               <arg>
6.57/2.93	                <var>x</var>
6.57/2.93	               </arg>
6.57/2.93	               <arg>
6.57/2.93	                <funapp>
6.57/2.93	                 <name>0</name>
6.57/2.93	                </funapp>
6.57/2.93	               </arg>
6.57/2.93	              </funapp>
6.57/2.93	             </lhs>
6.57/2.93	             <rhs>
6.57/2.93	              <funapp>
6.57/2.93	               <name>false</name>
6.57/2.93	              </funapp>
6.57/2.93	             </rhs>
6.57/2.93	            </rule>
6.57/2.93	            <rule>
6.57/2.93	             <lhs>
6.57/2.93	              <funapp>
6.57/2.93	               <name>U1</name>
6.57/2.93	               <arg>
6.57/2.93	                <funapp>
6.57/2.93	                 <name>true</name>
6.57/2.93	                </funapp>
6.57/2.93	               </arg>
6.57/2.93	               <arg>
6.57/2.93	                <var>x</var>
6.57/2.93	               </arg>
6.57/2.93	               <arg>
6.57/2.93	                <var>y</var>
6.57/2.93	               </arg>
6.57/2.93	              </funapp>
6.57/2.93	             </lhs>
6.57/2.93	             <rhs>
6.57/2.93	              <var>x</var>
6.57/2.93	             </rhs>
6.57/2.93	            </rule>
6.57/2.93	            <rule>
6.57/2.93	             <lhs>
6.57/2.93	              <funapp>
6.57/2.93	               <name>m</name>
6.57/2.93	              </funapp>
6.57/2.93	             </lhs>
6.57/2.93	             <rhs>
6.57/2.93	              <funapp>
6.57/2.93	               <name>s</name>
6.57/2.93	               <arg>
6.57/2.93	                <funapp>
6.57/2.93	                 <name>s</name>
6.57/2.93	                 <arg>
6.57/2.93	                  <funapp>
6.57/2.93	                   <name>s</name>
6.57/2.93	                   <arg>
6.57/2.93	                    <funapp>
6.57/2.93	                     <name>s</name>
6.57/2.93	                     <arg>
6.57/2.93	                      <funapp>
6.57/2.93	                       <name>0</name>
6.57/2.93	                      </funapp>
6.57/2.93	                     </arg>
6.57/2.93	                    </funapp>
6.57/2.93	                   </arg>
6.57/2.93	                  </funapp>
6.57/2.93	                 </arg>
6.57/2.93	                </funapp>
6.57/2.93	               </arg>
6.57/2.93	              </funapp>
6.57/2.93	             </rhs>
6.57/2.93	            </rule>
6.57/2.93	           </rules>
6.57/2.93	          </trs>
6.57/2.93	          <trsTerminationProof>
6.57/2.93	           <ruleRemoval>
6.57/2.93	            <orderingConstraintProof>
6.57/2.93	             <redPair>
6.57/2.93	              <knuthBendixOrder>
6.57/2.93	               <w0>1</w0>
6.57/2.93	               <precedenceWeight>
6.57/2.93	                <precedenceWeightEntry>
6.57/2.93	                 <name>U1</name>
6.57/2.93	                 <arity>3</arity>
6.57/2.93	                 <precedence>0</precedence>
6.57/2.93	                 <weight>0</weight>
6.57/2.93	                </precedenceWeightEntry>
6.57/2.93	                <precedenceWeightEntry>
6.57/2.93	                 <name>false</name>
6.57/2.93	                 <arity>0</arity>
6.57/2.93	                 <precedence>0</precedence>
6.57/2.93	                 <weight>2</weight>
6.57/2.93	                </precedenceWeightEntry>
6.57/2.93	                <precedenceWeightEntry>
6.57/2.93	                 <name>U2</name>
6.57/2.93	                 <arity>3</arity>
6.57/2.93	                 <precedence>0</precedence>
6.57/2.93	                 <weight>0</weight>
6.57/2.93	                </precedenceWeightEntry>
6.57/2.93	                <precedenceWeightEntry>
6.57/2.93	                 <name>m</name>
6.57/2.93	                 <arity>0</arity>
6.57/2.93	                 <precedence>1</precedence>
6.57/2.93	                 <weight>5</weight>
6.57/2.93	                </precedenceWeightEntry>
6.57/2.93	                <precedenceWeightEntry>
6.57/2.93	                 <name>true</name>
6.57/2.93	                 <arity>0</arity>
6.57/2.93	                 <precedence>0</precedence>
6.57/2.93	                 <weight>1</weight>
6.57/2.93	                </precedenceWeightEntry>
6.57/2.93	                <precedenceWeightEntry>
6.57/2.93	                 <name>le</name>
6.57/2.93	                 <arity>2</arity>
6.57/2.93	                 <precedence>0</precedence>
6.57/2.93	                 <weight>1</weight>
6.57/2.93	                </precedenceWeightEntry>
6.57/2.93	                <precedenceWeightEntry>
6.57/2.93	                 <name>s</name>
6.57/2.93	                 <arity>1</arity>
6.57/2.93	                 <precedence>0</precedence>
6.57/2.93	                 <weight>1</weight>
6.57/2.93	                </precedenceWeightEntry>
6.57/2.93	                <precedenceWeightEntry>
6.57/2.93	                 <name>0</name>
6.57/2.93	                 <arity>0</arity>
6.57/2.93	                 <precedence>0</precedence>
6.57/2.93	                 <weight>1</weight>
6.57/2.93	                </precedenceWeightEntry>
6.57/2.93	               </precedenceWeight>
6.57/2.93	              </knuthBendixOrder>
6.57/2.93	             </redPair>
6.57/2.93	            </orderingConstraintProof>
6.57/2.93	            <trs>
6.57/2.93	             <rules/>
6.57/2.93	            </trs>
6.57/2.93	            <trsTerminationProof>
6.57/2.93	             <rIsEmpty/>
6.57/2.93	            </trsTerminationProof>
6.57/2.93	           </ruleRemoval>
6.57/2.93	          </trsTerminationProof>
6.57/2.93	         </ruleRemoval>
6.57/2.93	        </trsTerminationProof>
6.57/2.93	       </ruleRemoval>
6.57/2.93	      </trsTerminationProof>
6.57/2.93	     </unraveling>
6.57/2.93	    </quasiReductiveProof>
6.57/2.93	    <contextJoinableCCPs/>
6.57/2.93	    <infeasibleConditions/>
6.57/2.93	    <unfeasibleCCPs/>
6.57/2.93	   </al94>
6.57/2.93	  </conditionalCrProof>
6.57/2.93	 </proof>
6.57/2.93	 <origin>
6.57/2.93	  <proofOrigin>
6.57/2.93	   <tool>
6.57/2.93	    <name>ConCon</name>
6.57/2.93	    <version>concon 1.4.0.0</version>
6.57/2.93	    <strategy>concon -s --cert --conf A theBenchmark.trs 58</strategy>
6.57/2.93	   </tool>
6.57/2.93	  </proofOrigin>
6.57/2.93	 </origin>
6.57/2.93	</certificationProblem>
6.57/2.93	EOF