10.00/3.83	YES
10.00/3.83	<?xml version="1.0"?><?xml-stylesheet type="text/xsl" href="cpfHTML.xsl"?>
10.00/3.83	<certificationProblem>
10.00/3.83	 <input>
10.00/3.83	  <ctrsInput>
10.00/3.83	   <conditionalRules>
10.00/3.83	    <conditionalRule>
10.00/3.83	     <rule>
10.00/3.83	      <lhs>
10.00/3.83	       <funapp>
10.00/3.83	        <name>lt</name>
10.00/3.83	        <arg>
10.00/3.83	         <var>x</var>
10.00/3.83	        </arg>
10.00/3.83	        <arg>
10.00/3.83	         <funapp>
10.00/3.83	          <name>0</name>
10.00/3.83	         </funapp>
10.00/3.83	        </arg>
10.00/3.83	       </funapp>
10.00/3.83	      </lhs>
10.00/3.83	      <rhs>
10.00/3.83	       <funapp>
10.00/3.83	        <name>false</name>
10.00/3.83	       </funapp>
10.00/3.83	      </rhs>
10.00/3.83	     </rule>
10.00/3.83	    </conditionalRule>
10.00/3.83	    <conditionalRule>
10.00/3.83	     <rule>
10.00/3.83	      <lhs>
10.00/3.83	       <funapp>
10.00/3.83	        <name>lt</name>
10.00/3.83	        <arg>
10.00/3.83	         <funapp>
10.00/3.83	          <name>0</name>
10.00/3.83	         </funapp>
10.00/3.83	        </arg>
10.00/3.83	        <arg>
10.00/3.83	         <funapp>
10.00/3.83	          <name>s</name>
10.00/3.83	          <arg>
10.00/3.83	           <var>x</var>
10.00/3.83	          </arg>
10.00/3.83	         </funapp>
10.00/3.83	        </arg>
10.00/3.83	       </funapp>
10.00/3.83	      </lhs>
10.00/3.83	      <rhs>
10.00/3.83	       <funapp>
10.00/3.83	        <name>true</name>
10.00/3.83	       </funapp>
10.00/3.83	      </rhs>
10.00/3.83	     </rule>
10.00/3.83	    </conditionalRule>
10.00/3.83	    <conditionalRule>
10.00/3.83	     <rule>
10.00/3.83	      <lhs>
10.00/3.83	       <funapp>
10.00/3.83	        <name>lt</name>
10.00/3.83	        <arg>
10.00/3.83	         <funapp>
10.00/3.83	          <name>s</name>
10.00/3.83	          <arg>
10.00/3.83	           <var>x</var>
10.00/3.83	          </arg>
10.00/3.83	         </funapp>
10.00/3.83	        </arg>
10.00/3.83	        <arg>
10.00/3.83	         <funapp>
10.00/3.83	          <name>s</name>
10.00/3.83	          <arg>
10.00/3.83	           <var>y</var>
10.00/3.83	          </arg>
10.00/3.83	         </funapp>
10.00/3.83	        </arg>
10.00/3.83	       </funapp>
10.00/3.83	      </lhs>
10.00/3.83	      <rhs>
10.00/3.83	       <funapp>
10.00/3.83	        <name>lt</name>
10.00/3.83	        <arg>
10.00/3.83	         <var>x</var>
10.00/3.83	        </arg>
10.00/3.83	        <arg>
10.00/3.83	         <var>y</var>
10.00/3.83	        </arg>
10.00/3.83	       </funapp>
10.00/3.83	      </rhs>
10.00/3.83	     </rule>
10.00/3.83	    </conditionalRule>
10.00/3.83	    <conditionalRule>
10.00/3.83	     <rule>
10.00/3.83	      <lhs>
10.00/3.83	       <funapp>
10.00/3.83	        <name>m</name>
10.00/3.83	        <arg>
10.00/3.83	         <funapp>
10.00/3.83	          <name>0</name>
10.00/3.83	         </funapp>
10.00/3.83	        </arg>
10.00/3.83	        <arg>
10.00/3.83	         <funapp>
10.00/3.83	          <name>s</name>
10.00/3.83	          <arg>
10.00/3.83	           <var>y</var>
10.00/3.83	          </arg>
10.00/3.83	         </funapp>
10.00/3.83	        </arg>
10.00/3.83	       </funapp>
10.00/3.83	      </lhs>
10.00/3.83	      <rhs>
10.00/3.83	       <funapp>
10.00/3.83	        <name>0</name>
10.00/3.83	       </funapp>
10.00/3.84	      </rhs>
10.00/3.84	     </rule>
10.00/3.84	    </conditionalRule>
10.00/3.84	    <conditionalRule>
10.00/3.84	     <rule>
10.00/3.84	      <lhs>
10.00/3.84	       <funapp>
10.00/3.84	        <name>m</name>
10.00/3.84	        <arg>
10.00/3.84	         <var>x</var>
10.00/3.84	        </arg>
10.00/3.84	        <arg>
10.00/3.84	         <funapp>
10.00/3.84	          <name>0</name>
10.00/3.84	         </funapp>
10.00/3.84	        </arg>
10.00/3.84	       </funapp>
10.00/3.84	      </lhs>
10.00/3.84	      <rhs>
10.00/3.84	       <var>x</var>
10.00/3.84	      </rhs>
10.00/3.84	     </rule>
10.00/3.84	    </conditionalRule>
10.00/3.84	    <conditionalRule>
10.00/3.84	     <rule>
10.00/3.84	      <lhs>
10.00/3.84	       <funapp>
10.00/3.84	        <name>m</name>
10.00/3.84	        <arg>
10.00/3.84	         <funapp>
10.00/3.84	          <name>s</name>
10.00/3.84	          <arg>
10.00/3.84	           <var>x</var>
10.00/3.84	          </arg>
10.00/3.84	         </funapp>
10.00/3.84	        </arg>
10.00/3.84	        <arg>
10.00/3.84	         <funapp>
10.00/3.84	          <name>s</name>
10.00/3.84	          <arg>
10.00/3.84	           <var>y</var>
10.00/3.84	          </arg>
10.00/3.84	         </funapp>
10.00/3.84	        </arg>
10.00/3.84	       </funapp>
10.00/3.84	      </lhs>
10.00/3.84	      <rhs>
10.00/3.84	       <funapp>
10.00/3.84	        <name>m</name>
10.00/3.84	        <arg>
10.00/3.84	         <var>x</var>
10.00/3.84	        </arg>
10.00/3.84	        <arg>
10.00/3.84	         <var>y</var>
10.00/3.84	        </arg>
10.00/3.84	       </funapp>
10.00/3.84	      </rhs>
10.00/3.84	     </rule>
10.00/3.84	    </conditionalRule>
10.00/3.84	    <conditionalRule>
10.00/3.84	     <rule>
10.00/3.84	      <lhs>
10.00/3.84	       <funapp>
10.00/3.84	        <name>div</name>
10.00/3.84	        <arg>
10.00/3.84	         <funapp>
10.00/3.84	          <name>0</name>
10.00/3.84	         </funapp>
10.00/3.84	        </arg>
10.00/3.84	        <arg>
10.00/3.84	         <funapp>
10.00/3.84	          <name>s</name>
10.00/3.84	          <arg>
10.00/3.84	           <var>x</var>
10.00/3.84	          </arg>
10.00/3.84	         </funapp>
10.00/3.84	        </arg>
10.00/3.84	       </funapp>
10.00/3.84	      </lhs>
10.00/3.84	      <rhs>
10.00/3.84	       <funapp>
10.00/3.84	        <name>pair</name>
10.00/3.84	        <arg>
10.00/3.84	         <funapp>
10.00/3.84	          <name>0</name>
10.00/3.84	         </funapp>
10.00/3.84	        </arg>
10.00/3.84	        <arg>
10.00/3.84	         <funapp>
10.00/3.84	          <name>0</name>
10.00/3.84	         </funapp>
10.00/3.84	        </arg>
10.00/3.84	       </funapp>
10.00/3.84	      </rhs>
10.00/3.84	     </rule>
10.00/3.84	    </conditionalRule>
10.00/3.84	    <conditionalRule>
10.00/3.84	     <rule>
10.00/3.84	      <lhs>
10.00/3.84	       <funapp>
10.00/3.84	        <name>div</name>
10.00/3.84	        <arg>
10.00/3.84	         <funapp>
10.00/3.84	          <name>s</name>
10.00/3.84	          <arg>
10.00/3.84	           <var>x</var>
10.00/3.84	          </arg>
10.00/3.84	         </funapp>
10.00/3.84	        </arg>
10.00/3.84	        <arg>
10.00/3.84	         <funapp>
10.00/3.84	          <name>s</name>
10.00/3.84	          <arg>
10.00/3.84	           <var>y</var>
10.00/3.84	          </arg>
10.00/3.84	         </funapp>
10.00/3.84	        </arg>
10.00/3.84	       </funapp>
10.00/3.84	      </lhs>
10.00/3.84	      <rhs>
10.00/3.84	       <funapp>
10.00/3.84	        <name>pair</name>
10.00/3.84	        <arg>
10.00/3.84	         <funapp>
10.00/3.84	          <name>0</name>
10.00/3.84	         </funapp>
10.00/3.84	        </arg>
10.00/3.84	        <arg>
10.00/3.84	         <funapp>
10.00/3.84	          <name>s</name>
10.00/3.84	          <arg>
10.00/3.84	           <var>x</var>
10.00/3.84	          </arg>
10.00/3.84	         </funapp>
10.00/3.84	        </arg>
10.00/3.84	       </funapp>
10.00/3.84	      </rhs>
10.00/3.84	     </rule>
10.00/3.84	     <rule>
10.00/3.84	      <lhs>
10.00/3.84	       <funapp>
10.00/3.84	        <name>lt</name>
10.00/3.84	        <arg>
10.00/3.84	         <var>x</var>
10.00/3.84	        </arg>
10.00/3.84	        <arg>
10.00/3.84	         <var>y</var>
10.00/3.84	        </arg>
10.00/3.84	       </funapp>
10.00/3.84	      </lhs>
10.00/3.84	      <rhs>
10.00/3.84	       <funapp>
10.00/3.84	        <name>true</name>
10.00/3.84	       </funapp>
10.00/3.84	      </rhs>
10.00/3.84	     </rule>
10.00/3.84	    </conditionalRule>
10.00/3.84	    <conditionalRule>
10.00/3.84	     <rule>
10.00/3.84	      <lhs>
10.00/3.84	       <funapp>
10.00/3.84	        <name>div</name>
10.00/3.84	        <arg>
10.00/3.84	         <funapp>
10.00/3.84	          <name>s</name>
10.00/3.84	          <arg>
10.00/3.84	           <var>x</var>
10.00/3.84	          </arg>
10.00/3.84	         </funapp>
10.00/3.84	        </arg>
10.00/3.84	        <arg>
10.00/3.84	         <funapp>
10.00/3.84	          <name>s</name>
10.00/3.84	          <arg>
10.00/3.84	           <var>y</var>
10.00/3.84	          </arg>
10.00/3.84	         </funapp>
10.00/3.84	        </arg>
10.00/3.84	       </funapp>
10.00/3.84	      </lhs>
10.00/3.84	      <rhs>
10.00/3.84	       <funapp>
10.00/3.84	        <name>pair</name>
10.00/3.84	        <arg>
10.00/3.84	         <funapp>
10.00/3.84	          <name>s</name>
10.00/3.84	          <arg>
10.00/3.84	           <var>q</var>
10.00/3.84	          </arg>
10.00/3.84	         </funapp>
10.00/3.84	        </arg>
10.00/3.84	        <arg>
10.00/3.84	         <var>r</var>
10.00/3.84	        </arg>
10.00/3.84	       </funapp>
10.00/3.84	      </rhs>
10.00/3.84	     </rule>
10.00/3.84	     <rule>
10.00/3.84	      <lhs>
10.00/3.84	       <funapp>
10.00/3.84	        <name>lt</name>
10.00/3.84	        <arg>
10.00/3.84	         <var>x</var>
10.00/3.84	        </arg>
10.00/3.84	        <arg>
10.00/3.84	         <var>y</var>
10.00/3.84	        </arg>
10.00/3.84	       </funapp>
10.00/3.84	      </lhs>
10.00/3.84	      <rhs>
10.00/3.84	       <funapp>
10.00/3.84	        <name>false</name>
10.00/3.84	       </funapp>
10.00/3.84	      </rhs>
10.00/3.84	     </rule>
10.00/3.84	     <rule>
10.00/3.84	      <lhs>
10.00/3.84	       <funapp>
10.00/3.84	        <name>div</name>
10.00/3.84	        <arg>
10.00/3.84	         <funapp>
10.00/3.84	          <name>m</name>
10.00/3.84	          <arg>
10.00/3.84	           <var>x</var>
10.00/3.84	          </arg>
10.00/3.84	          <arg>
10.00/3.84	           <var>y</var>
10.00/3.84	          </arg>
10.00/3.84	         </funapp>
10.00/3.84	        </arg>
10.00/3.84	        <arg>
10.00/3.84	         <funapp>
10.00/3.84	          <name>s</name>
10.00/3.84	          <arg>
10.00/3.84	           <var>y</var>
10.00/3.84	          </arg>
10.00/3.84	         </funapp>
10.00/3.84	        </arg>
10.00/3.84	       </funapp>
10.00/3.84	      </lhs>
10.00/3.84	      <rhs>
10.00/3.84	       <funapp>
10.00/3.84	        <name>pair</name>
10.00/3.84	        <arg>
10.00/3.84	         <var>q</var>
10.00/3.84	        </arg>
10.00/3.84	        <arg>
10.00/3.84	         <var>r</var>
10.00/3.84	        </arg>
10.00/3.84	       </funapp>
10.00/3.84	      </rhs>
10.00/3.84	     </rule>
10.00/3.84	    </conditionalRule>
10.00/3.84	   </conditionalRules>
10.00/3.84	  </ctrsInput>
10.00/3.84	 </input>
10.00/3.84	 <cpfVersion>2.4</cpfVersion>
10.00/3.84	 <proof>
10.00/3.84	  <conditionalCrProof>
10.00/3.84	   <al94>
10.00/3.84	    <quasiReductiveProof>
10.00/3.84	     <unraveling>
10.00/3.84	      <unravelingInformation>
10.00/3.84	       <unravelingEntry>
10.00/3.84	        <conditionalRule>
10.00/3.84	         <rule>
10.00/3.84	          <lhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>m</name>
10.00/3.84	            <arg>
10.00/3.84	             <var>x</var>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>0</name>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </lhs>
10.00/3.84	          <rhs>
10.00/3.84	           <var>x</var>
10.00/3.84	          </rhs>
10.00/3.84	         </rule>
10.00/3.84	        </conditionalRule>
10.00/3.84	        <rule>
10.00/3.84	         <lhs>
10.00/3.84	          <funapp>
10.00/3.84	           <name>m</name>
10.00/3.84	           <arg>
10.00/3.84	            <var>x</var>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>0</name>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	          </funapp>
10.00/3.84	         </lhs>
10.00/3.84	         <rhs>
10.00/3.84	          <var>x</var>
10.00/3.84	         </rhs>
10.00/3.84	        </rule>
10.00/3.84	       </unravelingEntry>
10.00/3.84	       <unravelingEntry>
10.00/3.84	        <conditionalRule>
10.00/3.84	         <rule>
10.00/3.84	          <lhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>m</name>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>x</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>y</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </lhs>
10.00/3.84	          <rhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>m</name>
10.00/3.84	            <arg>
10.00/3.84	             <var>x</var>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <var>y</var>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </rhs>
10.00/3.84	         </rule>
10.00/3.84	        </conditionalRule>
10.00/3.84	        <rule>
10.00/3.84	         <lhs>
10.00/3.84	          <funapp>
10.00/3.84	           <name>m</name>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>s</name>
10.00/3.84	             <arg>
10.00/3.84	              <var>x</var>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>s</name>
10.00/3.84	             <arg>
10.00/3.84	              <var>y</var>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	          </funapp>
10.00/3.84	         </lhs>
10.00/3.84	         <rhs>
10.00/3.84	          <funapp>
10.00/3.84	           <name>m</name>
10.00/3.84	           <arg>
10.00/3.84	            <var>x</var>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <var>y</var>
10.00/3.84	           </arg>
10.00/3.84	          </funapp>
10.00/3.84	         </rhs>
10.00/3.84	        </rule>
10.00/3.84	       </unravelingEntry>
10.00/3.84	       <unravelingEntry>
10.00/3.84	        <conditionalRule>
10.00/3.84	         <rule>
10.00/3.84	          <lhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>lt</name>
10.00/3.84	            <arg>
10.00/3.84	             <var>x</var>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>0</name>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </lhs>
10.00/3.84	          <rhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>false</name>
10.00/3.84	           </funapp>
10.00/3.84	          </rhs>
10.00/3.84	         </rule>
10.00/3.84	        </conditionalRule>
10.00/3.84	        <rule>
10.00/3.84	         <lhs>
10.00/3.84	          <funapp>
10.00/3.84	           <name>lt</name>
10.00/3.84	           <arg>
10.00/3.84	            <var>x</var>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>0</name>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	          </funapp>
10.00/3.84	         </lhs>
10.00/3.84	         <rhs>
10.00/3.84	          <funapp>
10.00/3.84	           <name>false</name>
10.00/3.84	          </funapp>
10.00/3.84	         </rhs>
10.00/3.84	        </rule>
10.00/3.84	       </unravelingEntry>
10.00/3.84	       <unravelingEntry>
10.00/3.84	        <conditionalRule>
10.00/3.84	         <rule>
10.00/3.84	          <lhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>div</name>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>0</name>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>x</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </lhs>
10.00/3.84	          <rhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>pair</name>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>0</name>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>0</name>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </rhs>
10.00/3.84	         </rule>
10.00/3.84	        </conditionalRule>
10.00/3.84	        <rule>
10.00/3.84	         <lhs>
10.00/3.84	          <funapp>
10.00/3.84	           <name>div</name>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>0</name>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>s</name>
10.00/3.84	             <arg>
10.00/3.84	              <var>x</var>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	          </funapp>
10.00/3.84	         </lhs>
10.00/3.84	         <rhs>
10.00/3.84	          <funapp>
10.00/3.84	           <name>pair</name>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>0</name>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>0</name>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	          </funapp>
10.00/3.84	         </rhs>
10.00/3.84	        </rule>
10.00/3.84	       </unravelingEntry>
10.00/3.84	       <unravelingEntry>
10.00/3.84	        <conditionalRule>
10.00/3.84	         <rule>
10.00/3.84	          <lhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>div</name>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>x</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>y</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </lhs>
10.00/3.84	          <rhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>pair</name>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>q</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <var>r</var>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </rhs>
10.00/3.84	         </rule>
10.00/3.84	         <rule>
10.00/3.84	          <lhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>lt</name>
10.00/3.84	            <arg>
10.00/3.84	             <var>x</var>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <var>y</var>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </lhs>
10.00/3.84	          <rhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>false</name>
10.00/3.84	           </funapp>
10.00/3.84	          </rhs>
10.00/3.84	         </rule>
10.00/3.84	         <rule>
10.00/3.84	          <lhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>div</name>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>m</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>x</var>
10.00/3.84	              </arg>
10.00/3.84	              <arg>
10.00/3.84	               <var>y</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>y</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </lhs>
10.00/3.84	          <rhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>pair</name>
10.00/3.84	            <arg>
10.00/3.84	             <var>q</var>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <var>r</var>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </rhs>
10.00/3.84	         </rule>
10.00/3.84	        </conditionalRule>
10.00/3.84	        <rule>
10.00/3.84	         <lhs>
10.00/3.84	          <funapp>
10.00/3.84	           <name>div</name>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>s</name>
10.00/3.84	             <arg>
10.00/3.84	              <var>x</var>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>s</name>
10.00/3.84	             <arg>
10.00/3.84	              <var>y</var>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	          </funapp>
10.00/3.84	         </lhs>
10.00/3.84	         <rhs>
10.00/3.84	          <funapp>
10.00/3.84	           <name>U1</name>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>lt</name>
10.00/3.84	             <arg>
10.00/3.84	              <var>x</var>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <var>y</var>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <var>x</var>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <var>y</var>
10.00/3.84	           </arg>
10.00/3.84	          </funapp>
10.00/3.84	         </rhs>
10.00/3.84	        </rule>
10.00/3.84	        <rule>
10.00/3.84	         <lhs>
10.00/3.84	          <funapp>
10.00/3.84	           <name>U1</name>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>false</name>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <var>x</var>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <var>y</var>
10.00/3.84	           </arg>
10.00/3.84	          </funapp>
10.00/3.84	         </lhs>
10.00/3.84	         <rhs>
10.00/3.84	          <funapp>
10.00/3.84	           <name>U2</name>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>div</name>
10.00/3.84	             <arg>
10.00/3.84	              <funapp>
10.00/3.84	               <name>m</name>
10.00/3.84	               <arg>
10.00/3.84	                <var>x</var>
10.00/3.84	               </arg>
10.00/3.84	               <arg>
10.00/3.84	                <var>y</var>
10.00/3.84	               </arg>
10.00/3.84	              </funapp>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <funapp>
10.00/3.84	               <name>s</name>
10.00/3.84	               <arg>
10.00/3.84	                <var>y</var>
10.00/3.84	               </arg>
10.00/3.84	              </funapp>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <var>x</var>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <var>y</var>
10.00/3.84	           </arg>
10.00/3.84	          </funapp>
10.00/3.84	         </rhs>
10.00/3.84	        </rule>
10.00/3.84	        <rule>
10.00/3.84	         <lhs>
10.00/3.84	          <funapp>
10.00/3.84	           <name>U2</name>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>pair</name>
10.00/3.84	             <arg>
10.00/3.84	              <var>q</var>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <var>r</var>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <var>x</var>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <var>y</var>
10.00/3.84	           </arg>
10.00/3.84	          </funapp>
10.00/3.84	         </lhs>
10.00/3.84	         <rhs>
10.00/3.84	          <funapp>
10.00/3.84	           <name>pair</name>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>s</name>
10.00/3.84	             <arg>
10.00/3.84	              <var>q</var>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <var>r</var>
10.00/3.84	           </arg>
10.00/3.84	          </funapp>
10.00/3.84	         </rhs>
10.00/3.84	        </rule>
10.00/3.84	       </unravelingEntry>
10.00/3.84	       <unravelingEntry>
10.00/3.84	        <conditionalRule>
10.00/3.84	         <rule>
10.00/3.84	          <lhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>lt</name>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>x</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>y</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </lhs>
10.00/3.84	          <rhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>lt</name>
10.00/3.84	            <arg>
10.00/3.84	             <var>x</var>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <var>y</var>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </rhs>
10.00/3.84	         </rule>
10.00/3.84	        </conditionalRule>
10.00/3.84	        <rule>
10.00/3.84	         <lhs>
10.00/3.84	          <funapp>
10.00/3.84	           <name>lt</name>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>s</name>
10.00/3.84	             <arg>
10.00/3.84	              <var>x</var>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>s</name>
10.00/3.84	             <arg>
10.00/3.84	              <var>y</var>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	          </funapp>
10.00/3.84	         </lhs>
10.00/3.84	         <rhs>
10.00/3.84	          <funapp>
10.00/3.84	           <name>lt</name>
10.00/3.84	           <arg>
10.00/3.84	            <var>x</var>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <var>y</var>
10.00/3.84	           </arg>
10.00/3.84	          </funapp>
10.00/3.84	         </rhs>
10.00/3.84	        </rule>
10.00/3.84	       </unravelingEntry>
10.00/3.84	       <unravelingEntry>
10.00/3.84	        <conditionalRule>
10.00/3.84	         <rule>
10.00/3.84	          <lhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>div</name>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>x</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>y</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </lhs>
10.00/3.84	          <rhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>pair</name>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>0</name>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>x</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </rhs>
10.00/3.84	         </rule>
10.00/3.84	         <rule>
10.00/3.84	          <lhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>lt</name>
10.00/3.84	            <arg>
10.00/3.84	             <var>x</var>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <var>y</var>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </lhs>
10.00/3.84	          <rhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>true</name>
10.00/3.84	           </funapp>
10.00/3.84	          </rhs>
10.00/3.84	         </rule>
10.00/3.84	        </conditionalRule>
10.00/3.84	        <rule>
10.00/3.84	         <lhs>
10.00/3.84	          <funapp>
10.00/3.84	           <name>div</name>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>s</name>
10.00/3.84	             <arg>
10.00/3.84	              <var>x</var>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>s</name>
10.00/3.84	             <arg>
10.00/3.84	              <var>y</var>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	          </funapp>
10.00/3.84	         </lhs>
10.00/3.84	         <rhs>
10.00/3.84	          <funapp>
10.00/3.84	           <name>U1</name>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>lt</name>
10.00/3.84	             <arg>
10.00/3.84	              <var>x</var>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <var>y</var>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <var>x</var>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <var>y</var>
10.00/3.84	           </arg>
10.00/3.84	          </funapp>
10.00/3.84	         </rhs>
10.00/3.84	        </rule>
10.00/3.84	        <rule>
10.00/3.84	         <lhs>
10.00/3.84	          <funapp>
10.00/3.84	           <name>U1</name>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>true</name>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <var>x</var>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <var>y</var>
10.00/3.84	           </arg>
10.00/3.84	          </funapp>
10.00/3.84	         </lhs>
10.00/3.84	         <rhs>
10.00/3.84	          <funapp>
10.00/3.84	           <name>pair</name>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>0</name>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>s</name>
10.00/3.84	             <arg>
10.00/3.84	              <var>x</var>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	          </funapp>
10.00/3.84	         </rhs>
10.00/3.84	        </rule>
10.00/3.84	       </unravelingEntry>
10.00/3.84	       <unravelingEntry>
10.00/3.84	        <conditionalRule>
10.00/3.84	         <rule>
10.00/3.84	          <lhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>lt</name>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>0</name>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>x</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </lhs>
10.00/3.84	          <rhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>true</name>
10.00/3.84	           </funapp>
10.00/3.84	          </rhs>
10.00/3.84	         </rule>
10.00/3.84	        </conditionalRule>
10.00/3.84	        <rule>
10.00/3.84	         <lhs>
10.00/3.84	          <funapp>
10.00/3.84	           <name>lt</name>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>0</name>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>s</name>
10.00/3.84	             <arg>
10.00/3.84	              <var>x</var>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	          </funapp>
10.00/3.84	         </lhs>
10.00/3.84	         <rhs>
10.00/3.84	          <funapp>
10.00/3.84	           <name>true</name>
10.00/3.84	          </funapp>
10.00/3.84	         </rhs>
10.00/3.84	        </rule>
10.00/3.84	       </unravelingEntry>
10.00/3.84	       <unravelingEntry>
10.00/3.84	        <conditionalRule>
10.00/3.84	         <rule>
10.00/3.84	          <lhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>m</name>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>0</name>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>y</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </lhs>
10.00/3.84	          <rhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>0</name>
10.00/3.84	           </funapp>
10.00/3.84	          </rhs>
10.00/3.84	         </rule>
10.00/3.84	        </conditionalRule>
10.00/3.84	        <rule>
10.00/3.84	         <lhs>
10.00/3.84	          <funapp>
10.00/3.84	           <name>m</name>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>0</name>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>s</name>
10.00/3.84	             <arg>
10.00/3.84	              <var>y</var>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	          </funapp>
10.00/3.84	         </lhs>
10.00/3.84	         <rhs>
10.00/3.84	          <funapp>
10.00/3.84	           <name>0</name>
10.00/3.84	          </funapp>
10.00/3.84	         </rhs>
10.00/3.84	        </rule>
10.00/3.84	       </unravelingEntry>
10.00/3.84	      </unravelingInformation>
10.00/3.84	      <trsTerminationProof>
10.00/3.84	       <dpTrans>
10.00/3.84	        <dps>
10.00/3.84	         <rules>
10.00/3.84	          <rule>
10.00/3.84	           <lhs>
10.00/3.84	            <funapp>
10.00/3.84	             <sharp>
10.00/3.84	              <name>m</name>
10.00/3.84	             </sharp>
10.00/3.84	             <arg>
10.00/3.84	              <funapp>
10.00/3.84	               <name>s</name>
10.00/3.84	               <arg>
10.00/3.84	                <var>x</var>
10.00/3.84	               </arg>
10.00/3.84	              </funapp>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <funapp>
10.00/3.84	               <name>s</name>
10.00/3.84	               <arg>
10.00/3.84	                <var>y</var>
10.00/3.84	               </arg>
10.00/3.84	              </funapp>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </lhs>
10.00/3.84	           <rhs>
10.00/3.84	            <funapp>
10.00/3.84	             <sharp>
10.00/3.84	              <name>m</name>
10.00/3.84	             </sharp>
10.00/3.84	             <arg>
10.00/3.84	              <var>x</var>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <var>y</var>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </rhs>
10.00/3.84	          </rule>
10.00/3.84	          <rule>
10.00/3.84	           <lhs>
10.00/3.84	            <funapp>
10.00/3.84	             <sharp>
10.00/3.84	              <name>div</name>
10.00/3.84	             </sharp>
10.00/3.84	             <arg>
10.00/3.84	              <funapp>
10.00/3.84	               <name>s</name>
10.00/3.84	               <arg>
10.00/3.84	                <var>x</var>
10.00/3.84	               </arg>
10.00/3.84	              </funapp>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <funapp>
10.00/3.84	               <name>s</name>
10.00/3.84	               <arg>
10.00/3.84	                <var>y</var>
10.00/3.84	               </arg>
10.00/3.84	              </funapp>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </lhs>
10.00/3.84	           <rhs>
10.00/3.84	            <funapp>
10.00/3.84	             <sharp>
10.00/3.84	              <name>lt</name>
10.00/3.84	             </sharp>
10.00/3.84	             <arg>
10.00/3.84	              <var>x</var>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <var>y</var>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </rhs>
10.00/3.84	          </rule>
10.00/3.84	          <rule>
10.00/3.84	           <lhs>
10.00/3.84	            <funapp>
10.00/3.84	             <sharp>
10.00/3.84	              <name>div</name>
10.00/3.84	             </sharp>
10.00/3.84	             <arg>
10.00/3.84	              <funapp>
10.00/3.84	               <name>s</name>
10.00/3.84	               <arg>
10.00/3.84	                <var>x</var>
10.00/3.84	               </arg>
10.00/3.84	              </funapp>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <funapp>
10.00/3.84	               <name>s</name>
10.00/3.84	               <arg>
10.00/3.84	                <var>y</var>
10.00/3.84	               </arg>
10.00/3.84	              </funapp>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </lhs>
10.00/3.84	           <rhs>
10.00/3.84	            <funapp>
10.00/3.84	             <sharp>
10.00/3.84	              <name>U1</name>
10.00/3.84	             </sharp>
10.00/3.84	             <arg>
10.00/3.84	              <funapp>
10.00/3.84	               <name>lt</name>
10.00/3.84	               <arg>
10.00/3.84	                <var>x</var>
10.00/3.84	               </arg>
10.00/3.84	               <arg>
10.00/3.84	                <var>y</var>
10.00/3.84	               </arg>
10.00/3.84	              </funapp>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <var>x</var>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <var>y</var>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </rhs>
10.00/3.84	          </rule>
10.00/3.84	          <rule>
10.00/3.84	           <lhs>
10.00/3.84	            <funapp>
10.00/3.84	             <sharp>
10.00/3.84	              <name>U1</name>
10.00/3.84	             </sharp>
10.00/3.84	             <arg>
10.00/3.84	              <funapp>
10.00/3.84	               <name>false</name>
10.00/3.84	              </funapp>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <var>x</var>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <var>y</var>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </lhs>
10.00/3.84	           <rhs>
10.00/3.84	            <funapp>
10.00/3.84	             <sharp>
10.00/3.84	              <name>m</name>
10.00/3.84	             </sharp>
10.00/3.84	             <arg>
10.00/3.84	              <var>x</var>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <var>y</var>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </rhs>
10.00/3.84	          </rule>
10.00/3.84	          <rule>
10.00/3.84	           <lhs>
10.00/3.84	            <funapp>
10.00/3.84	             <sharp>
10.00/3.84	              <name>U1</name>
10.00/3.84	             </sharp>
10.00/3.84	             <arg>
10.00/3.84	              <funapp>
10.00/3.84	               <name>false</name>
10.00/3.84	              </funapp>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <var>x</var>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <var>y</var>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </lhs>
10.00/3.84	           <rhs>
10.00/3.84	            <funapp>
10.00/3.84	             <sharp>
10.00/3.84	              <name>div</name>
10.00/3.84	             </sharp>
10.00/3.84	             <arg>
10.00/3.84	              <funapp>
10.00/3.84	               <name>m</name>
10.00/3.84	               <arg>
10.00/3.84	                <var>x</var>
10.00/3.84	               </arg>
10.00/3.84	               <arg>
10.00/3.84	                <var>y</var>
10.00/3.84	               </arg>
10.00/3.84	              </funapp>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <funapp>
10.00/3.84	               <name>s</name>
10.00/3.84	               <arg>
10.00/3.84	                <var>y</var>
10.00/3.84	               </arg>
10.00/3.84	              </funapp>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </rhs>
10.00/3.84	          </rule>
10.00/3.84	          <rule>
10.00/3.84	           <lhs>
10.00/3.84	            <funapp>
10.00/3.84	             <sharp>
10.00/3.84	              <name>U1</name>
10.00/3.84	             </sharp>
10.00/3.84	             <arg>
10.00/3.84	              <funapp>
10.00/3.84	               <name>false</name>
10.00/3.84	              </funapp>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <var>x</var>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <var>y</var>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </lhs>
10.00/3.84	           <rhs>
10.00/3.84	            <funapp>
10.00/3.84	             <sharp>
10.00/3.84	              <name>U2</name>
10.00/3.84	             </sharp>
10.00/3.84	             <arg>
10.00/3.84	              <funapp>
10.00/3.84	               <name>div</name>
10.00/3.84	               <arg>
10.00/3.84	                <funapp>
10.00/3.84	                 <name>m</name>
10.00/3.84	                 <arg>
10.00/3.84	                  <var>x</var>
10.00/3.84	                 </arg>
10.00/3.84	                 <arg>
10.00/3.84	                  <var>y</var>
10.00/3.84	                 </arg>
10.00/3.84	                </funapp>
10.00/3.84	               </arg>
10.00/3.84	               <arg>
10.00/3.84	                <funapp>
10.00/3.84	                 <name>s</name>
10.00/3.84	                 <arg>
10.00/3.84	                  <var>y</var>
10.00/3.84	                 </arg>
10.00/3.84	                </funapp>
10.00/3.84	               </arg>
10.00/3.84	              </funapp>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <var>x</var>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <var>y</var>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </rhs>
10.00/3.84	          </rule>
10.00/3.84	          <rule>
10.00/3.84	           <lhs>
10.00/3.84	            <funapp>
10.00/3.84	             <sharp>
10.00/3.84	              <name>lt</name>
10.00/3.84	             </sharp>
10.00/3.84	             <arg>
10.00/3.84	              <funapp>
10.00/3.84	               <name>s</name>
10.00/3.84	               <arg>
10.00/3.84	                <var>x</var>
10.00/3.84	               </arg>
10.00/3.84	              </funapp>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <funapp>
10.00/3.84	               <name>s</name>
10.00/3.84	               <arg>
10.00/3.84	                <var>y</var>
10.00/3.84	               </arg>
10.00/3.84	              </funapp>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </lhs>
10.00/3.84	           <rhs>
10.00/3.84	            <funapp>
10.00/3.84	             <sharp>
10.00/3.84	              <name>lt</name>
10.00/3.84	             </sharp>
10.00/3.84	             <arg>
10.00/3.84	              <var>x</var>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <var>y</var>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </rhs>
10.00/3.84	          </rule>
10.00/3.84	         </rules>
10.00/3.84	        </dps>
10.00/3.84	        <markedSymbols>true</markedSymbols>
10.00/3.84	        <dpProof>
10.00/3.84	         <depGraphProc>
10.00/3.84	          <component>
10.00/3.84	           <dps>
10.00/3.84	            <rules>
10.00/3.84	             <rule>
10.00/3.84	              <lhs>
10.00/3.84	               <funapp>
10.00/3.84	                <sharp>
10.00/3.84	                 <name>U1</name>
10.00/3.84	                </sharp>
10.00/3.84	                <arg>
10.00/3.84	                 <funapp>
10.00/3.84	                  <name>false</name>
10.00/3.84	                 </funapp>
10.00/3.84	                </arg>
10.00/3.84	                <arg>
10.00/3.84	                 <var>x</var>
10.00/3.84	                </arg>
10.00/3.84	                <arg>
10.00/3.84	                 <var>y</var>
10.00/3.84	                </arg>
10.00/3.84	               </funapp>
10.00/3.84	              </lhs>
10.00/3.84	              <rhs>
10.00/3.84	               <funapp>
10.00/3.84	                <sharp>
10.00/3.84	                 <name>div</name>
10.00/3.84	                </sharp>
10.00/3.84	                <arg>
10.00/3.84	                 <funapp>
10.00/3.84	                  <name>m</name>
10.00/3.84	                  <arg>
10.00/3.84	                   <var>x</var>
10.00/3.84	                  </arg>
10.00/3.84	                  <arg>
10.00/3.84	                   <var>y</var>
10.00/3.84	                  </arg>
10.00/3.84	                 </funapp>
10.00/3.84	                </arg>
10.00/3.84	                <arg>
10.00/3.84	                 <funapp>
10.00/3.84	                  <name>s</name>
10.00/3.84	                  <arg>
10.00/3.84	                   <var>y</var>
10.00/3.84	                  </arg>
10.00/3.84	                 </funapp>
10.00/3.84	                </arg>
10.00/3.84	               </funapp>
10.00/3.84	              </rhs>
10.00/3.84	             </rule>
10.00/3.84	             <rule>
10.00/3.84	              <lhs>
10.00/3.84	               <funapp>
10.00/3.84	                <sharp>
10.00/3.84	                 <name>div</name>
10.00/3.84	                </sharp>
10.00/3.84	                <arg>
10.00/3.84	                 <funapp>
10.00/3.84	                  <name>s</name>
10.00/3.84	                  <arg>
10.00/3.84	                   <var>x</var>
10.00/3.84	                  </arg>
10.00/3.84	                 </funapp>
10.00/3.84	                </arg>
10.00/3.84	                <arg>
10.00/3.84	                 <funapp>
10.00/3.84	                  <name>s</name>
10.00/3.84	                  <arg>
10.00/3.84	                   <var>y</var>
10.00/3.84	                  </arg>
10.00/3.84	                 </funapp>
10.00/3.84	                </arg>
10.00/3.84	               </funapp>
10.00/3.84	              </lhs>
10.00/3.84	              <rhs>
10.00/3.84	               <funapp>
10.00/3.84	                <sharp>
10.00/3.84	                 <name>U1</name>
10.00/3.84	                </sharp>
10.00/3.84	                <arg>
10.00/3.84	                 <funapp>
10.00/3.84	                  <name>lt</name>
10.00/3.84	                  <arg>
10.00/3.84	                   <var>x</var>
10.00/3.84	                  </arg>
10.00/3.84	                  <arg>
10.00/3.84	                   <var>y</var>
10.00/3.84	                  </arg>
10.00/3.84	                 </funapp>
10.00/3.84	                </arg>
10.00/3.84	                <arg>
10.00/3.84	                 <var>x</var>
10.00/3.84	                </arg>
10.00/3.84	                <arg>
10.00/3.84	                 <var>y</var>
10.00/3.84	                </arg>
10.00/3.84	               </funapp>
10.00/3.84	              </rhs>
10.00/3.84	             </rule>
10.00/3.84	            </rules>
10.00/3.84	           </dps>
10.00/3.84	           <realScc>true</realScc>
10.00/3.84	           <arcs>
10.00/3.84	            <forwardArc>1</forwardArc>
10.00/3.84	            <forwardArc>3</forwardArc>
10.00/3.84	            <forwardArc>5</forwardArc>
10.00/3.84	           </arcs>
10.00/3.84	           <dpProof>
10.00/3.84	            <subtermProc>
10.00/3.84	             <multisetArgumentFilter>
10.00/3.84	              <multisetArgumentFilterEntry>
10.00/3.84	               <sharp>
10.00/3.84	                <name>U1</name>
10.00/3.84	               </sharp>
10.00/3.84	               <arity>3</arity>
10.00/3.84	               <status>
10.00/3.84	                <position>2</position>
10.00/3.84	               </status>
10.00/3.84	              </multisetArgumentFilterEntry>
10.00/3.84	              <multisetArgumentFilterEntry>
10.00/3.84	               <sharp>
10.00/3.84	                <name>div</name>
10.00/3.84	               </sharp>
10.00/3.84	               <arity>2</arity>
10.00/3.84	               <status>
10.00/3.84	                <position>1</position>
10.00/3.84	               </status>
10.00/3.84	              </multisetArgumentFilterEntry>
10.00/3.84	              <multisetArgumentFilterEntry>
10.00/3.84	               <name>m</name>
10.00/3.84	               <arity>2</arity>
10.00/3.84	               <status>
10.00/3.84	                <position>1</position>
10.00/3.84	               </status>
10.00/3.84	              </multisetArgumentFilterEntry>
10.00/3.84	             </multisetArgumentFilter>
10.00/3.84	             <dps>
10.00/3.84	              <rules>
10.00/3.84	               <rule>
10.00/3.84	                <lhs>
10.00/3.84	                 <funapp>
10.00/3.84	                  <sharp>
10.00/3.84	                   <name>div</name>
10.00/3.84	                  </sharp>
10.00/3.84	                  <arg>
10.00/3.84	                   <funapp>
10.00/3.84	                    <name>s</name>
10.00/3.84	                    <arg>
10.00/3.84	                     <var>x</var>
10.00/3.84	                    </arg>
10.00/3.84	                   </funapp>
10.00/3.84	                  </arg>
10.00/3.84	                  <arg>
10.00/3.84	                   <funapp>
10.00/3.84	                    <name>s</name>
10.00/3.84	                    <arg>
10.00/3.84	                     <var>y</var>
10.00/3.84	                    </arg>
10.00/3.84	                   </funapp>
10.00/3.84	                  </arg>
10.00/3.84	                 </funapp>
10.00/3.84	                </lhs>
10.00/3.84	                <rhs>
10.00/3.84	                 <funapp>
10.00/3.84	                  <sharp>
10.00/3.84	                   <name>U1</name>
10.00/3.84	                  </sharp>
10.00/3.84	                  <arg>
10.00/3.84	                   <funapp>
10.00/3.84	                    <name>lt</name>
10.00/3.84	                    <arg>
10.00/3.84	                     <var>x</var>
10.00/3.84	                    </arg>
10.00/3.84	                    <arg>
10.00/3.84	                     <var>y</var>
10.00/3.84	                    </arg>
10.00/3.84	                   </funapp>
10.00/3.84	                  </arg>
10.00/3.84	                  <arg>
10.00/3.84	                   <var>x</var>
10.00/3.84	                  </arg>
10.00/3.84	                  <arg>
10.00/3.84	                   <var>y</var>
10.00/3.84	                  </arg>
10.00/3.84	                 </funapp>
10.00/3.84	                </rhs>
10.00/3.84	               </rule>
10.00/3.84	              </rules>
10.00/3.84	             </dps>
10.00/3.84	             <dpProof>
10.00/3.84	              <depGraphProc>
10.00/3.84	               <component>
10.00/3.84	                <dps>
10.00/3.84	                 <rules>
10.00/3.84	                  <rule>
10.00/3.84	                   <lhs>
10.00/3.84	                    <funapp>
10.00/3.84	                     <sharp>
10.00/3.84	                      <name>U1</name>
10.00/3.84	                     </sharp>
10.00/3.84	                     <arg>
10.00/3.84	                      <funapp>
10.00/3.84	                       <name>false</name>
10.00/3.84	                      </funapp>
10.00/3.84	                     </arg>
10.00/3.84	                     <arg>
10.00/3.84	                      <var>x</var>
10.00/3.84	                     </arg>
10.00/3.84	                     <arg>
10.00/3.84	                      <var>y</var>
10.00/3.84	                     </arg>
10.00/3.84	                    </funapp>
10.00/3.84	                   </lhs>
10.00/3.84	                   <rhs>
10.00/3.84	                    <funapp>
10.00/3.84	                     <sharp>
10.00/3.84	                      <name>div</name>
10.00/3.84	                     </sharp>
10.00/3.84	                     <arg>
10.00/3.84	                      <funapp>
10.00/3.84	                       <name>m</name>
10.00/3.84	                       <arg>
10.00/3.84	                        <var>x</var>
10.00/3.84	                       </arg>
10.00/3.84	                       <arg>
10.00/3.84	                        <var>y</var>
10.00/3.84	                       </arg>
10.00/3.84	                      </funapp>
10.00/3.84	                     </arg>
10.00/3.84	                     <arg>
10.00/3.84	                      <funapp>
10.00/3.84	                       <name>s</name>
10.00/3.84	                       <arg>
10.00/3.84	                        <var>y</var>
10.00/3.84	                       </arg>
10.00/3.84	                      </funapp>
10.00/3.84	                     </arg>
10.00/3.84	                    </funapp>
10.00/3.84	                   </rhs>
10.00/3.84	                  </rule>
10.00/3.84	                 </rules>
10.00/3.84	                </dps>
10.00/3.84	                <realScc>false</realScc>
10.00/3.84	                <arcs/>
10.00/3.84	               </component>
10.00/3.84	              </depGraphProc>
10.00/3.84	             </dpProof>
10.00/3.84	            </subtermProc>
10.00/3.84	           </dpProof>
10.00/3.84	          </component>
10.00/3.84	          <component>
10.00/3.84	           <dps>
10.00/3.84	            <rules>
10.00/3.84	             <rule>
10.00/3.84	              <lhs>
10.00/3.84	               <funapp>
10.00/3.84	                <sharp>
10.00/3.84	                 <name>U1</name>
10.00/3.84	                </sharp>
10.00/3.84	                <arg>
10.00/3.84	                 <funapp>
10.00/3.84	                  <name>false</name>
10.00/3.84	                 </funapp>
10.00/3.84	                </arg>
10.00/3.84	                <arg>
10.00/3.84	                 <var>x</var>
10.00/3.84	                </arg>
10.00/3.84	                <arg>
10.00/3.84	                 <var>y</var>
10.00/3.84	                </arg>
10.00/3.84	               </funapp>
10.00/3.84	              </lhs>
10.00/3.84	              <rhs>
10.00/3.84	               <funapp>
10.00/3.84	                <sharp>
10.00/3.84	                 <name>m</name>
10.00/3.84	                </sharp>
10.00/3.84	                <arg>
10.00/3.84	                 <var>x</var>
10.00/3.84	                </arg>
10.00/3.84	                <arg>
10.00/3.84	                 <var>y</var>
10.00/3.84	                </arg>
10.00/3.84	               </funapp>
10.00/3.84	              </rhs>
10.00/3.84	             </rule>
10.00/3.84	            </rules>
10.00/3.84	           </dps>
10.00/3.84	           <realScc>false</realScc>
10.00/3.84	           <arcs>
10.00/3.84	            <forwardArc>1</forwardArc>
10.00/3.84	           </arcs>
10.00/3.84	          </component>
10.00/3.84	          <component>
10.00/3.84	           <dps>
10.00/3.84	            <rules>
10.00/3.84	             <rule>
10.00/3.84	              <lhs>
10.00/3.84	               <funapp>
10.00/3.84	                <sharp>
10.00/3.84	                 <name>m</name>
10.00/3.84	                </sharp>
10.00/3.84	                <arg>
10.00/3.84	                 <funapp>
10.00/3.84	                  <name>s</name>
10.00/3.84	                  <arg>
10.00/3.84	                   <var>x</var>
10.00/3.84	                  </arg>
10.00/3.84	                 </funapp>
10.00/3.84	                </arg>
10.00/3.84	                <arg>
10.00/3.84	                 <funapp>
10.00/3.84	                  <name>s</name>
10.00/3.84	                  <arg>
10.00/3.84	                   <var>y</var>
10.00/3.84	                  </arg>
10.00/3.84	                 </funapp>
10.00/3.84	                </arg>
10.00/3.84	               </funapp>
10.00/3.84	              </lhs>
10.00/3.84	              <rhs>
10.00/3.84	               <funapp>
10.00/3.84	                <sharp>
10.00/3.84	                 <name>m</name>
10.00/3.84	                </sharp>
10.00/3.84	                <arg>
10.00/3.84	                 <var>x</var>
10.00/3.84	                </arg>
10.00/3.84	                <arg>
10.00/3.84	                 <var>y</var>
10.00/3.84	                </arg>
10.00/3.84	               </funapp>
10.00/3.84	              </rhs>
10.00/3.84	             </rule>
10.00/3.84	            </rules>
10.00/3.84	           </dps>
10.00/3.84	           <realScc>true</realScc>
10.00/3.84	           <arcs/>
10.00/3.84	           <dpProof>
10.00/3.84	            <sizeChangeProc>
10.00/3.84	             <subtermCriterion/>
10.00/3.84	             <sizeChangeGraph>
10.00/3.84	              <rule>
10.00/3.84	               <lhs>
10.00/3.84	                <funapp>
10.00/3.84	                 <sharp>
10.00/3.84	                  <name>m</name>
10.00/3.84	                 </sharp>
10.00/3.84	                 <arg>
10.00/3.84	                  <funapp>
10.00/3.84	                   <name>s</name>
10.00/3.84	                   <arg>
10.00/3.84	                    <var>x</var>
10.00/3.84	                   </arg>
10.00/3.84	                  </funapp>
10.00/3.84	                 </arg>
10.00/3.84	                 <arg>
10.00/3.84	                  <funapp>
10.00/3.84	                   <name>s</name>
10.00/3.84	                   <arg>
10.00/3.84	                    <var>y</var>
10.00/3.84	                   </arg>
10.00/3.84	                  </funapp>
10.00/3.84	                 </arg>
10.00/3.84	                </funapp>
10.00/3.84	               </lhs>
10.00/3.84	               <rhs>
10.00/3.84	                <funapp>
10.00/3.84	                 <sharp>
10.00/3.84	                  <name>m</name>
10.00/3.84	                 </sharp>
10.00/3.84	                 <arg>
10.00/3.84	                  <var>x</var>
10.00/3.84	                 </arg>
10.00/3.84	                 <arg>
10.00/3.84	                  <var>y</var>
10.00/3.84	                 </arg>
10.00/3.84	                </funapp>
10.00/3.84	               </rhs>
10.00/3.84	              </rule>
10.00/3.84	              <edge>
10.00/3.84	               <position>2</position>
10.00/3.84	               <strict>true</strict>
10.00/3.84	               <position>2</position>
10.00/3.84	              </edge>
10.00/3.84	              <edge>
10.00/3.84	               <position>1</position>
10.00/3.84	               <strict>true</strict>
10.00/3.84	               <position>1</position>
10.00/3.84	              </edge>
10.00/3.84	             </sizeChangeGraph>
10.00/3.84	            </sizeChangeProc>
10.00/3.84	           </dpProof>
10.00/3.84	          </component>
10.00/3.84	          <component>
10.00/3.84	           <dps>
10.00/3.84	            <rules>
10.00/3.84	             <rule>
10.00/3.84	              <lhs>
10.00/3.84	               <funapp>
10.00/3.84	                <sharp>
10.00/3.84	                 <name>div</name>
10.00/3.84	                </sharp>
10.00/3.84	                <arg>
10.00/3.84	                 <funapp>
10.00/3.84	                  <name>s</name>
10.00/3.84	                  <arg>
10.00/3.84	                   <var>x</var>
10.00/3.84	                  </arg>
10.00/3.84	                 </funapp>
10.00/3.84	                </arg>
10.00/3.84	                <arg>
10.00/3.84	                 <funapp>
10.00/3.84	                  <name>s</name>
10.00/3.84	                  <arg>
10.00/3.84	                   <var>y</var>
10.00/3.84	                  </arg>
10.00/3.84	                 </funapp>
10.00/3.84	                </arg>
10.00/3.84	               </funapp>
10.00/3.84	              </lhs>
10.00/3.84	              <rhs>
10.00/3.84	               <funapp>
10.00/3.84	                <sharp>
10.00/3.84	                 <name>lt</name>
10.00/3.84	                </sharp>
10.00/3.84	                <arg>
10.00/3.84	                 <var>x</var>
10.00/3.84	                </arg>
10.00/3.84	                <arg>
10.00/3.84	                 <var>y</var>
10.00/3.84	                </arg>
10.00/3.84	               </funapp>
10.00/3.84	              </rhs>
10.00/3.84	             </rule>
10.00/3.84	            </rules>
10.00/3.84	           </dps>
10.00/3.84	           <realScc>false</realScc>
10.00/3.84	           <arcs>
10.00/3.84	            <forwardArc>1</forwardArc>
10.00/3.84	           </arcs>
10.00/3.84	          </component>
10.00/3.84	          <component>
10.00/3.84	           <dps>
10.00/3.84	            <rules>
10.00/3.84	             <rule>
10.00/3.84	              <lhs>
10.00/3.84	               <funapp>
10.00/3.84	                <sharp>
10.00/3.84	                 <name>lt</name>
10.00/3.84	                </sharp>
10.00/3.84	                <arg>
10.00/3.84	                 <funapp>
10.00/3.84	                  <name>s</name>
10.00/3.84	                  <arg>
10.00/3.84	                   <var>x</var>
10.00/3.84	                  </arg>
10.00/3.84	                 </funapp>
10.00/3.84	                </arg>
10.00/3.84	                <arg>
10.00/3.84	                 <funapp>
10.00/3.84	                  <name>s</name>
10.00/3.84	                  <arg>
10.00/3.84	                   <var>y</var>
10.00/3.84	                  </arg>
10.00/3.84	                 </funapp>
10.00/3.84	                </arg>
10.00/3.84	               </funapp>
10.00/3.84	              </lhs>
10.00/3.84	              <rhs>
10.00/3.84	               <funapp>
10.00/3.84	                <sharp>
10.00/3.84	                 <name>lt</name>
10.00/3.84	                </sharp>
10.00/3.84	                <arg>
10.00/3.84	                 <var>x</var>
10.00/3.84	                </arg>
10.00/3.84	                <arg>
10.00/3.84	                 <var>y</var>
10.00/3.84	                </arg>
10.00/3.84	               </funapp>
10.00/3.84	              </rhs>
10.00/3.84	             </rule>
10.00/3.84	            </rules>
10.00/3.84	           </dps>
10.00/3.84	           <realScc>true</realScc>
10.00/3.84	           <arcs/>
10.00/3.84	           <dpProof>
10.00/3.84	            <sizeChangeProc>
10.00/3.84	             <subtermCriterion/>
10.00/3.84	             <sizeChangeGraph>
10.00/3.84	              <rule>
10.00/3.84	               <lhs>
10.00/3.84	                <funapp>
10.00/3.84	                 <sharp>
10.00/3.84	                  <name>lt</name>
10.00/3.84	                 </sharp>
10.00/3.84	                 <arg>
10.00/3.84	                  <funapp>
10.00/3.84	                   <name>s</name>
10.00/3.84	                   <arg>
10.00/3.84	                    <var>x</var>
10.00/3.84	                   </arg>
10.00/3.84	                  </funapp>
10.00/3.84	                 </arg>
10.00/3.84	                 <arg>
10.00/3.84	                  <funapp>
10.00/3.84	                   <name>s</name>
10.00/3.84	                   <arg>
10.00/3.84	                    <var>y</var>
10.00/3.84	                   </arg>
10.00/3.84	                  </funapp>
10.00/3.84	                 </arg>
10.00/3.84	                </funapp>
10.00/3.84	               </lhs>
10.00/3.84	               <rhs>
10.00/3.84	                <funapp>
10.00/3.84	                 <sharp>
10.00/3.84	                  <name>lt</name>
10.00/3.84	                 </sharp>
10.00/3.84	                 <arg>
10.00/3.84	                  <var>x</var>
10.00/3.84	                 </arg>
10.00/3.84	                 <arg>
10.00/3.84	                  <var>y</var>
10.00/3.84	                 </arg>
10.00/3.84	                </funapp>
10.00/3.84	               </rhs>
10.00/3.84	              </rule>
10.00/3.84	              <edge>
10.00/3.84	               <position>2</position>
10.00/3.84	               <strict>true</strict>
10.00/3.84	               <position>2</position>
10.00/3.84	              </edge>
10.00/3.84	              <edge>
10.00/3.84	               <position>1</position>
10.00/3.84	               <strict>true</strict>
10.00/3.84	               <position>1</position>
10.00/3.84	              </edge>
10.00/3.84	             </sizeChangeGraph>
10.00/3.84	            </sizeChangeProc>
10.00/3.84	           </dpProof>
10.00/3.84	          </component>
10.00/3.84	          <component>
10.00/3.84	           <dps>
10.00/3.84	            <rules>
10.00/3.84	             <rule>
10.00/3.84	              <lhs>
10.00/3.84	               <funapp>
10.00/3.84	                <sharp>
10.00/3.84	                 <name>U1</name>
10.00/3.84	                </sharp>
10.00/3.84	                <arg>
10.00/3.84	                 <funapp>
10.00/3.84	                  <name>false</name>
10.00/3.84	                 </funapp>
10.00/3.84	                </arg>
10.00/3.84	                <arg>
10.00/3.84	                 <var>x</var>
10.00/3.84	                </arg>
10.00/3.84	                <arg>
10.00/3.84	                 <var>y</var>
10.00/3.84	                </arg>
10.00/3.84	               </funapp>
10.00/3.84	              </lhs>
10.00/3.84	              <rhs>
10.00/3.84	               <funapp>
10.00/3.84	                <sharp>
10.00/3.84	                 <name>U2</name>
10.00/3.84	                </sharp>
10.00/3.84	                <arg>
10.00/3.84	                 <funapp>
10.00/3.84	                  <name>div</name>
10.00/3.84	                  <arg>
10.00/3.84	                   <funapp>
10.00/3.84	                    <name>m</name>
10.00/3.84	                    <arg>
10.00/3.84	                     <var>x</var>
10.00/3.84	                    </arg>
10.00/3.84	                    <arg>
10.00/3.84	                     <var>y</var>
10.00/3.84	                    </arg>
10.00/3.84	                   </funapp>
10.00/3.84	                  </arg>
10.00/3.84	                  <arg>
10.00/3.84	                   <funapp>
10.00/3.84	                    <name>s</name>
10.00/3.84	                    <arg>
10.00/3.84	                     <var>y</var>
10.00/3.84	                    </arg>
10.00/3.84	                   </funapp>
10.00/3.84	                  </arg>
10.00/3.84	                 </funapp>
10.00/3.84	                </arg>
10.00/3.84	                <arg>
10.00/3.84	                 <var>x</var>
10.00/3.84	                </arg>
10.00/3.84	                <arg>
10.00/3.84	                 <var>y</var>
10.00/3.84	                </arg>
10.00/3.84	               </funapp>
10.00/3.84	              </rhs>
10.00/3.84	             </rule>
10.00/3.84	            </rules>
10.00/3.84	           </dps>
10.00/3.84	           <realScc>false</realScc>
10.00/3.84	           <arcs/>
10.00/3.84	          </component>
10.00/3.84	         </depGraphProc>
10.00/3.84	        </dpProof>
10.00/3.84	       </dpTrans>
10.00/3.84	      </trsTerminationProof>
10.00/3.84	     </unraveling>
10.00/3.84	    </quasiReductiveProof>
10.00/3.84	    <contextJoinableCCPs/>
10.00/3.84	    <infeasibleConditions/>
10.00/3.84	    <unfeasibleCCPs>
10.00/3.84	     <unfeasibleCCP>
10.00/3.84	      <substitution>
10.00/3.84	       <substEntry>
10.00/3.84	        <var>y'</var>
10.00/3.84	        <var>$1</var>
10.00/3.84	       </substEntry>
10.00/3.84	       <substEntry>
10.00/3.84	        <var>z'</var>
10.00/3.84	        <var>$2</var>
10.00/3.84	       </substEntry>
10.00/3.84	      </substitution>
10.00/3.84	      <unfeasibilityProof>
10.00/3.84	       <terms>
10.00/3.84	        <funapp>
10.00/3.84	         <name>lt</name>
10.00/3.84	         <arg>
10.00/3.84	          <funapp>
10.00/3.84	           <name>?1</name>
10.00/3.84	          </funapp>
10.00/3.84	         </arg>
10.00/3.84	         <arg>
10.00/3.84	          <funapp>
10.00/3.84	           <name>?2</name>
10.00/3.84	          </funapp>
10.00/3.84	         </arg>
10.00/3.84	        </funapp>
10.00/3.84	        <funapp>
10.00/3.84	         <name>false</name>
10.00/3.84	        </funapp>
10.00/3.84	        <funapp>
10.00/3.84	         <name>true</name>
10.00/3.84	        </funapp>
10.00/3.84	       </terms>
10.00/3.84	       <conditionalRewritingSequence>
10.00/3.84	        <conditionalRewriteStep>
10.00/3.84	         <conditionalRule>
10.00/3.84	          <rule>
10.00/3.84	           <lhs>
10.00/3.84	            <funapp>
10.00/3.84	             <name>lt</name>
10.00/3.84	             <arg>
10.00/3.84	              <funapp>
10.00/3.84	               <name>?1</name>
10.00/3.84	              </funapp>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <funapp>
10.00/3.84	               <name>?2</name>
10.00/3.84	              </funapp>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </lhs>
10.00/3.84	           <rhs>
10.00/3.84	            <funapp>
10.00/3.84	             <name>false</name>
10.00/3.84	            </funapp>
10.00/3.84	           </rhs>
10.00/3.84	          </rule>
10.00/3.84	         </conditionalRule>
10.00/3.84	         <positionInTerm></positionInTerm>
10.00/3.84	         <substitution> </substitution>
10.00/3.84	         <source>
10.00/3.84	          <funapp>
10.00/3.84	           <name>lt</name>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>?1</name>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>?2</name>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	          </funapp>
10.00/3.84	         </source>
10.00/3.84	         <target>
10.00/3.84	          <funapp>
10.00/3.84	           <name>false</name>
10.00/3.84	          </funapp>
10.00/3.84	         </target>
10.00/3.84	         <conditions> </conditions>
10.00/3.84	        </conditionalRewriteStep>
10.00/3.84	       </conditionalRewritingSequence>
10.00/3.84	       <conditionalRewritingSequence>
10.00/3.84	        <conditionalRewriteStep>
10.00/3.84	         <conditionalRule>
10.00/3.84	          <rule>
10.00/3.84	           <lhs>
10.00/3.84	            <funapp>
10.00/3.84	             <name>lt</name>
10.00/3.84	             <arg>
10.00/3.84	              <funapp>
10.00/3.84	               <name>?1</name>
10.00/3.84	              </funapp>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <funapp>
10.00/3.84	               <name>?2</name>
10.00/3.84	              </funapp>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </lhs>
10.00/3.84	           <rhs>
10.00/3.84	            <funapp>
10.00/3.84	             <name>true</name>
10.00/3.84	            </funapp>
10.00/3.84	           </rhs>
10.00/3.84	          </rule>
10.00/3.84	         </conditionalRule>
10.00/3.84	         <positionInTerm></positionInTerm>
10.00/3.84	         <substitution> </substitution>
10.00/3.84	         <source>
10.00/3.84	          <funapp>
10.00/3.84	           <name>lt</name>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>?1</name>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>?2</name>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	          </funapp>
10.00/3.84	         </source>
10.00/3.84	         <target>
10.00/3.84	          <funapp>
10.00/3.84	           <name>true</name>
10.00/3.84	          </funapp>
10.00/3.84	         </target>
10.00/3.84	         <conditions> </conditions>
10.00/3.84	        </conditionalRewriteStep>
10.00/3.84	       </conditionalRewritingSequence>
10.00/3.84	       <rules>
10.00/3.84	        <conditionalRule>
10.00/3.84	         <rule>
10.00/3.84	          <lhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>div</name>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>y'</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>z'</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </lhs>
10.00/3.84	          <rhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>pair</name>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>z</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <var>x'</var>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </rhs>
10.00/3.84	         </rule>
10.00/3.84	         <rule>
10.00/3.84	          <lhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>lt</name>
10.00/3.84	            <arg>
10.00/3.84	             <var>y'</var>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <var>z'</var>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </lhs>
10.00/3.84	          <rhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>false</name>
10.00/3.84	           </funapp>
10.00/3.84	          </rhs>
10.00/3.84	         </rule>
10.00/3.84	         <rule>
10.00/3.84	          <lhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>div</name>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>m</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>y'</var>
10.00/3.84	              </arg>
10.00/3.84	              <arg>
10.00/3.84	               <var>z'</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>z'</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </lhs>
10.00/3.84	          <rhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>pair</name>
10.00/3.84	            <arg>
10.00/3.84	             <var>z</var>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <var>x'</var>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </rhs>
10.00/3.84	         </rule>
10.00/3.84	        </conditionalRule>
10.00/3.84	        <conditionalRule>
10.00/3.84	         <rule>
10.00/3.84	          <lhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>div</name>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>$1</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>$2</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </lhs>
10.00/3.84	          <rhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>pair</name>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>0</name>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>$1</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </rhs>
10.00/3.84	         </rule>
10.00/3.84	         <rule>
10.00/3.84	          <lhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>lt</name>
10.00/3.84	            <arg>
10.00/3.84	             <var>$1</var>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <var>$2</var>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </lhs>
10.00/3.84	          <rhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>true</name>
10.00/3.84	           </funapp>
10.00/3.84	          </rhs>
10.00/3.84	         </rule>
10.00/3.84	        </conditionalRule>
10.00/3.84	       </rules>
10.00/3.84	       <constMap>
10.00/3.84	        <entry>
10.00/3.84	         <symbol>
10.00/3.84	          <name>?1</name>
10.00/3.84	         </symbol>
10.00/3.84	         <const>$1</const>
10.00/3.84	        </entry>
10.00/3.84	        <entry>
10.00/3.84	         <symbol>
10.00/3.84	          <name>?2</name>
10.00/3.84	         </symbol>
10.00/3.84	         <const>$2</const>
10.00/3.84	        </entry>
10.00/3.84	        <entry>
10.00/3.84	         <symbol>
10.00/3.84	          <name>?3</name>
10.00/3.84	         </symbol>
10.00/3.84	         <const>x'</const>
10.00/3.84	        </entry>
10.00/3.84	        <entry>
10.00/3.84	         <symbol>
10.00/3.84	          <name>?4</name>
10.00/3.84	         </symbol>
10.00/3.84	         <const>z</const>
10.00/3.84	        </entry>
10.00/3.84	       </constMap>
10.00/3.84	      </unfeasibilityProof>
10.00/3.84	     </unfeasibleCCP>
10.00/3.84	     <unfeasibleCCP>
10.00/3.84	      <substitution>
10.00/3.84	       <substEntry>
10.00/3.84	        <var>z</var>
10.00/3.84	        <var>$1</var>
10.00/3.84	       </substEntry>
10.00/3.84	       <substEntry>
10.00/3.84	        <var>x'</var>
10.00/3.84	        <var>$2</var>
10.00/3.84	       </substEntry>
10.00/3.84	      </substitution>
10.00/3.84	      <unfeasibilityProof>
10.00/3.84	       <terms>
10.00/3.84	        <funapp>
10.00/3.84	         <name>lt</name>
10.00/3.84	         <arg>
10.00/3.84	          <funapp>
10.00/3.84	           <name>?1</name>
10.00/3.84	          </funapp>
10.00/3.84	         </arg>
10.00/3.84	         <arg>
10.00/3.84	          <funapp>
10.00/3.84	           <name>?2</name>
10.00/3.84	          </funapp>
10.00/3.84	         </arg>
10.00/3.84	        </funapp>
10.00/3.84	        <funapp>
10.00/3.84	         <name>true</name>
10.00/3.84	        </funapp>
10.00/3.84	        <funapp>
10.00/3.84	         <name>false</name>
10.00/3.84	        </funapp>
10.00/3.84	       </terms>
10.00/3.84	       <conditionalRewritingSequence>
10.00/3.84	        <conditionalRewriteStep>
10.00/3.84	         <conditionalRule>
10.00/3.84	          <rule>
10.00/3.84	           <lhs>
10.00/3.84	            <funapp>
10.00/3.84	             <name>lt</name>
10.00/3.84	             <arg>
10.00/3.84	              <funapp>
10.00/3.84	               <name>?1</name>
10.00/3.84	              </funapp>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <funapp>
10.00/3.84	               <name>?2</name>
10.00/3.84	              </funapp>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </lhs>
10.00/3.84	           <rhs>
10.00/3.84	            <funapp>
10.00/3.84	             <name>true</name>
10.00/3.84	            </funapp>
10.00/3.84	           </rhs>
10.00/3.84	          </rule>
10.00/3.84	         </conditionalRule>
10.00/3.84	         <positionInTerm></positionInTerm>
10.00/3.84	         <substitution> </substitution>
10.00/3.84	         <source>
10.00/3.84	          <funapp>
10.00/3.84	           <name>lt</name>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>?1</name>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>?2</name>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	          </funapp>
10.00/3.84	         </source>
10.00/3.84	         <target>
10.00/3.84	          <funapp>
10.00/3.84	           <name>true</name>
10.00/3.84	          </funapp>
10.00/3.84	         </target>
10.00/3.84	         <conditions> </conditions>
10.00/3.84	        </conditionalRewriteStep>
10.00/3.84	       </conditionalRewritingSequence>
10.00/3.84	       <conditionalRewritingSequence>
10.00/3.84	        <conditionalRewriteStep>
10.00/3.84	         <conditionalRule>
10.00/3.84	          <rule>
10.00/3.84	           <lhs>
10.00/3.84	            <funapp>
10.00/3.84	             <name>lt</name>
10.00/3.84	             <arg>
10.00/3.84	              <funapp>
10.00/3.84	               <name>?1</name>
10.00/3.84	              </funapp>
10.00/3.84	             </arg>
10.00/3.84	             <arg>
10.00/3.84	              <funapp>
10.00/3.84	               <name>?2</name>
10.00/3.84	              </funapp>
10.00/3.84	             </arg>
10.00/3.84	            </funapp>
10.00/3.84	           </lhs>
10.00/3.84	           <rhs>
10.00/3.84	            <funapp>
10.00/3.84	             <name>false</name>
10.00/3.84	            </funapp>
10.00/3.84	           </rhs>
10.00/3.84	          </rule>
10.00/3.84	         </conditionalRule>
10.00/3.84	         <positionInTerm></positionInTerm>
10.00/3.84	         <substitution> </substitution>
10.00/3.84	         <source>
10.00/3.84	          <funapp>
10.00/3.84	           <name>lt</name>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>?1</name>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	           <arg>
10.00/3.84	            <funapp>
10.00/3.84	             <name>?2</name>
10.00/3.84	            </funapp>
10.00/3.84	           </arg>
10.00/3.84	          </funapp>
10.00/3.84	         </source>
10.00/3.84	         <target>
10.00/3.84	          <funapp>
10.00/3.84	           <name>false</name>
10.00/3.84	          </funapp>
10.00/3.84	         </target>
10.00/3.84	         <conditions> </conditions>
10.00/3.84	        </conditionalRewriteStep>
10.00/3.84	       </conditionalRewritingSequence>
10.00/3.84	       <rules>
10.00/3.84	        <conditionalRule>
10.00/3.84	         <rule>
10.00/3.84	          <lhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>div</name>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>z</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>x'</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </lhs>
10.00/3.84	          <rhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>pair</name>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>0</name>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>z</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </rhs>
10.00/3.84	         </rule>
10.00/3.84	         <rule>
10.00/3.84	          <lhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>lt</name>
10.00/3.84	            <arg>
10.00/3.84	             <var>z</var>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <var>x'</var>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </lhs>
10.00/3.84	          <rhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>true</name>
10.00/3.84	           </funapp>
10.00/3.84	          </rhs>
10.00/3.84	         </rule>
10.00/3.84	        </conditionalRule>
10.00/3.84	        <conditionalRule>
10.00/3.84	         <rule>
10.00/3.84	          <lhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>div</name>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>$1</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>$2</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </lhs>
10.00/3.84	          <rhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>pair</name>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>y'</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <var>z'</var>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </rhs>
10.00/3.84	         </rule>
10.00/3.84	         <rule>
10.00/3.84	          <lhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>lt</name>
10.00/3.84	            <arg>
10.00/3.84	             <var>$1</var>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <var>$2</var>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </lhs>
10.00/3.84	          <rhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>false</name>
10.00/3.84	           </funapp>
10.00/3.84	          </rhs>
10.00/3.84	         </rule>
10.00/3.84	         <rule>
10.00/3.84	          <lhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>div</name>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>m</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>$1</var>
10.00/3.84	              </arg>
10.00/3.84	              <arg>
10.00/3.84	               <var>$2</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <funapp>
10.00/3.84	              <name>s</name>
10.00/3.84	              <arg>
10.00/3.84	               <var>$2</var>
10.00/3.84	              </arg>
10.00/3.84	             </funapp>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </lhs>
10.00/3.84	          <rhs>
10.00/3.84	           <funapp>
10.00/3.84	            <name>pair</name>
10.00/3.84	            <arg>
10.00/3.84	             <var>y'</var>
10.00/3.84	            </arg>
10.00/3.84	            <arg>
10.00/3.84	             <var>z'</var>
10.00/3.84	            </arg>
10.00/3.84	           </funapp>
10.00/3.84	          </rhs>
10.00/3.84	         </rule>
10.00/3.84	        </conditionalRule>
10.00/3.84	       </rules>
10.00/3.84	       <constMap>
10.00/3.84	        <entry>
10.00/3.84	         <symbol>
10.00/3.84	          <name>?1</name>
10.00/3.84	         </symbol>
10.00/3.84	         <const>$1</const>
10.00/3.84	        </entry>
10.00/3.84	        <entry>
10.00/3.84	         <symbol>
10.00/3.84	          <name>?2</name>
10.00/3.84	         </symbol>
10.00/3.84	         <const>$2</const>
10.00/3.84	        </entry>
10.00/3.84	        <entry>
10.00/3.84	         <symbol>
10.00/3.84	          <name>?3</name>
10.00/3.84	         </symbol>
10.00/3.84	         <const>y'</const>
10.00/3.84	        </entry>
10.00/3.84	        <entry>
10.00/3.84	         <symbol>
10.00/3.84	          <name>?4</name>
10.00/3.84	         </symbol>
10.00/3.84	         <const>z'</const>
10.00/3.84	        </entry>
10.00/3.84	       </constMap>
10.00/3.84	      </unfeasibilityProof>
10.00/3.84	     </unfeasibleCCP>
10.00/3.84	    </unfeasibleCCPs>
10.00/3.84	   </al94>
10.00/3.84	  </conditionalCrProof>
10.00/3.84	 </proof>
10.00/3.84	 <origin>
10.00/3.84	  <proofOrigin>
10.00/3.84	   <tool>
10.00/3.84	    <name>ConCon</name>
10.00/3.84	    <version>concon 1.4.0.0</version>
10.00/3.84	    <strategy>concon -s --cert --conf A theBenchmark.trs 58</strategy>
10.00/3.84	   </tool>
10.00/3.84	  </proofOrigin>
10.00/3.84	 </origin>
10.00/3.84	</certificationProblem>
10.00/3.84	EOF