3.63/2.06	YES
3.63/2.06	<?xml version="1.0"?><?xml-stylesheet type="text/xsl" href="cpfHTML.xsl"?>
3.63/2.06	<certificationProblem>
3.63/2.06	 <input>
3.63/2.06	  <ctrsInput>
3.63/2.06	   <conditionalRules>
3.63/2.06	    <conditionalRule>
3.63/2.06	     <rule>
3.63/2.06	      <lhs>
3.63/2.06	       <funapp>
3.63/2.06	        <name>f</name>
3.63/2.06	        <arg>
3.63/2.06	         <var>x</var>
3.63/2.06	        </arg>
3.63/2.06	       </funapp>
3.63/2.06	      </lhs>
3.63/2.06	      <rhs>
3.63/2.06	       <funapp>
3.63/2.06	        <name>a</name>
3.63/2.06	       </funapp>
3.63/2.06	      </rhs>
3.63/2.06	     </rule>
3.63/2.06	     <rule>
3.63/2.06	      <lhs>
3.63/2.06	       <funapp>
3.63/2.06	        <name>a</name>
3.63/2.06	       </funapp>
3.63/2.06	      </lhs>
3.63/2.06	      <rhs>
3.63/2.06	       <var>x</var>
3.63/2.06	      </rhs>
3.63/2.06	     </rule>
3.63/2.06	    </conditionalRule>
3.63/2.06	    <conditionalRule>
3.63/2.06	     <rule>
3.63/2.06	      <lhs>
3.63/2.06	       <funapp>
3.63/2.06	        <name>f</name>
3.63/2.06	        <arg>
3.63/2.06	         <var>x</var>
3.63/2.06	        </arg>
3.63/2.06	       </funapp>
3.63/2.06	      </lhs>
3.63/2.06	      <rhs>
3.63/2.06	       <funapp>
3.63/2.06	        <name>b</name>
3.63/2.06	       </funapp>
3.63/2.06	      </rhs>
3.63/2.06	     </rule>
3.63/2.06	     <rule>
3.63/2.06	      <lhs>
3.63/2.06	       <funapp>
3.63/2.06	        <name>b</name>
3.63/2.06	       </funapp>
3.63/2.06	      </lhs>
3.63/2.06	      <rhs>
3.63/2.06	       <var>x</var>
3.63/2.06	      </rhs>
3.63/2.06	     </rule>
3.63/2.06	    </conditionalRule>
3.63/2.06	   </conditionalRules>
3.63/2.06	  </ctrsInput>
3.63/2.06	 </input>
3.63/2.06	 <cpfVersion>2.4</cpfVersion>
3.63/2.06	 <proof>
3.63/2.06	  <conditionalCrProof>
3.63/2.06	   <al94>
3.63/2.06	    <quasiReductiveProof>
3.63/2.06	     <unraveling>
3.63/2.06	      <unravelingInformation>
3.63/2.06	       <unravelingEntry>
3.63/2.06	        <conditionalRule>
3.63/2.06	         <rule>
3.63/2.06	          <lhs>
3.63/2.06	           <funapp>
3.63/2.06	            <name>f</name>
3.63/2.06	            <arg>
3.63/2.06	             <var>x</var>
3.63/2.06	            </arg>
3.63/2.06	           </funapp>
3.63/2.06	          </lhs>
3.63/2.06	          <rhs>
3.63/2.06	           <funapp>
3.63/2.06	            <name>a</name>
3.63/2.06	           </funapp>
3.63/2.06	          </rhs>
3.63/2.06	         </rule>
3.63/2.06	         <rule>
3.63/2.06	          <lhs>
3.63/2.06	           <funapp>
3.63/2.06	            <name>a</name>
3.63/2.06	           </funapp>
3.63/2.06	          </lhs>
3.63/2.06	          <rhs>
3.63/2.06	           <var>x</var>
3.63/2.06	          </rhs>
3.63/2.06	         </rule>
3.63/2.06	        </conditionalRule>
3.63/2.06	        <rule>
3.63/2.06	         <lhs>
3.63/2.06	          <funapp>
3.63/2.06	           <name>f</name>
3.63/2.06	           <arg>
3.63/2.06	            <var>x</var>
3.63/2.06	           </arg>
3.63/2.06	          </funapp>
3.63/2.06	         </lhs>
3.63/2.06	         <rhs>
3.63/2.06	          <funapp>
3.63/2.06	           <name>U1</name>
3.63/2.06	           <arg>
3.63/2.06	            <funapp>
3.63/2.06	             <name>a</name>
3.63/2.06	            </funapp>
3.63/2.06	           </arg>
3.63/2.06	           <arg>
3.63/2.06	            <var>x</var>
3.63/2.06	           </arg>
3.63/2.06	          </funapp>
3.63/2.06	         </rhs>
3.63/2.06	        </rule>
3.63/2.06	        <rule>
3.63/2.06	         <lhs>
3.63/2.06	          <funapp>
3.63/2.06	           <name>U1</name>
3.63/2.06	           <arg>
3.63/2.06	            <var>x</var>
3.63/2.06	           </arg>
3.63/2.06	           <arg>
3.63/2.06	            <var>x</var>
3.63/2.06	           </arg>
3.63/2.06	          </funapp>
3.63/2.06	         </lhs>
3.63/2.06	         <rhs>
3.63/2.06	          <funapp>
3.63/2.06	           <name>a</name>
3.63/2.06	          </funapp>
3.63/2.06	         </rhs>
3.63/2.06	        </rule>
3.63/2.06	       </unravelingEntry>
3.63/2.06	       <unravelingEntry>
3.63/2.06	        <conditionalRule>
3.63/2.06	         <rule>
3.63/2.06	          <lhs>
3.63/2.06	           <funapp>
3.63/2.06	            <name>f</name>
3.63/2.06	            <arg>
3.63/2.06	             <var>x</var>
3.63/2.06	            </arg>
3.63/2.06	           </funapp>
3.63/2.06	          </lhs>
3.63/2.06	          <rhs>
3.63/2.06	           <funapp>
3.63/2.06	            <name>b</name>
3.63/2.06	           </funapp>
3.63/2.06	          </rhs>
3.63/2.06	         </rule>
3.63/2.06	         <rule>
3.63/2.06	          <lhs>
3.63/2.06	           <funapp>
3.63/2.06	            <name>b</name>
3.63/2.06	           </funapp>
3.63/2.06	          </lhs>
3.63/2.06	          <rhs>
3.63/2.06	           <var>x</var>
3.63/2.06	          </rhs>
3.63/2.06	         </rule>
3.63/2.06	        </conditionalRule>
3.63/2.06	        <rule>
3.63/2.06	         <lhs>
3.63/2.06	          <funapp>
3.63/2.06	           <name>f</name>
3.63/2.06	           <arg>
3.63/2.06	            <var>x</var>
3.63/2.06	           </arg>
3.63/2.06	          </funapp>
3.63/2.06	         </lhs>
3.63/2.06	         <rhs>
3.63/2.06	          <funapp>
3.63/2.06	           <name>U2</name>
3.63/2.06	           <arg>
3.63/2.06	            <funapp>
3.63/2.06	             <name>b</name>
3.63/2.06	            </funapp>
3.63/2.06	           </arg>
3.63/2.06	           <arg>
3.63/2.06	            <var>x</var>
3.63/2.06	           </arg>
3.63/2.06	          </funapp>
3.63/2.06	         </rhs>
3.63/2.06	        </rule>
3.63/2.06	        <rule>
3.63/2.06	         <lhs>
3.63/2.06	          <funapp>
3.63/2.06	           <name>U2</name>
3.63/2.06	           <arg>
3.63/2.06	            <var>x</var>
3.63/2.06	           </arg>
3.63/2.06	           <arg>
3.63/2.06	            <var>x</var>
3.63/2.06	           </arg>
3.63/2.06	          </funapp>
3.63/2.06	         </lhs>
3.63/2.06	         <rhs>
3.63/2.06	          <funapp>
3.63/2.06	           <name>b</name>
3.63/2.06	          </funapp>
3.63/2.06	         </rhs>
3.63/2.06	        </rule>
3.63/2.06	       </unravelingEntry>
3.63/2.06	      </unravelingInformation>
3.63/2.06	      <trsTerminationProof>
3.63/2.06	       <ruleRemoval>
3.63/2.06	        <orderingConstraintProof>
3.63/2.06	         <redPair>
3.63/2.06	          <knuthBendixOrder>
3.63/2.06	           <w0>1</w0>
3.63/2.06	           <precedenceWeight>
3.63/2.06	            <precedenceWeightEntry>
3.63/2.06	             <name>U2</name>
3.63/2.06	             <arity>2</arity>
3.63/2.06	             <precedence>2</precedence>
3.63/2.06	             <weight>2</weight>
3.63/2.06	            </precedenceWeightEntry>
3.63/2.06	            <precedenceWeightEntry>
3.63/2.06	             <name>b</name>
3.63/2.06	             <arity>0</arity>
3.63/2.06	             <precedence>0</precedence>
3.63/2.06	             <weight>4</weight>
3.63/2.06	            </precedenceWeightEntry>
3.63/2.06	            <precedenceWeightEntry>
3.63/2.06	             <name>U1</name>
3.63/2.06	             <arity>2</arity>
3.63/2.06	             <precedence>4</precedence>
3.63/2.06	             <weight>2</weight>
3.63/2.06	            </precedenceWeightEntry>
3.63/2.06	            <precedenceWeightEntry>
3.63/2.06	             <name>a</name>
3.63/2.06	             <arity>0</arity>
3.63/2.06	             <precedence>0</precedence>
3.63/2.06	             <weight>4</weight>
3.63/2.06	            </precedenceWeightEntry>
3.63/2.06	            <precedenceWeightEntry>
3.63/2.06	             <name>f</name>
3.63/2.06	             <arity>1</arity>
3.63/2.06	             <precedence>7</precedence>
3.63/2.06	             <weight>6</weight>
3.63/2.06	            </precedenceWeightEntry>
3.63/2.06	           </precedenceWeight>
3.63/2.06	          </knuthBendixOrder>
3.63/2.06	         </redPair>
3.63/2.06	        </orderingConstraintProof>
3.63/2.06	        <trs>
3.63/2.06	         <rules/>
3.63/2.06	        </trs>
3.63/2.06	        <trsTerminationProof>
3.63/2.06	         <rIsEmpty/>
3.63/2.06	        </trsTerminationProof>
3.63/2.06	       </ruleRemoval>
3.63/2.06	      </trsTerminationProof>
3.63/2.06	     </unraveling>
3.63/2.06	    </quasiReductiveProof>
3.63/2.06	    <contextJoinableCCPs>
3.63/2.06	     <contextJoinableCCP>
3.63/2.06	      <funapp>
3.63/2.06	       <name>b</name>
3.63/2.06	      </funapp>
3.63/2.06	      <funapp>
3.63/2.06	       <name>a</name>
3.63/2.06	      </funapp>
3.63/2.06	      <rules>
3.63/2.06	       <rule>
3.63/2.06	        <lhs>
3.63/2.06	         <funapp>
3.63/2.06	          <name>b</name>
3.63/2.06	         </funapp>
3.63/2.06	        </lhs>
3.63/2.06	        <rhs>
3.63/2.06	         <var>z</var>
3.63/2.06	        </rhs>
3.63/2.06	       </rule>
3.63/2.06	       <rule>
3.63/2.06	        <lhs>
3.63/2.06	         <funapp>
3.63/2.06	          <name>a</name>
3.63/2.06	         </funapp>
3.63/2.06	        </lhs>
3.63/2.06	        <rhs>
3.63/2.06	         <var>z</var>
3.63/2.06	        </rhs>
3.63/2.06	       </rule>
3.63/2.06	      </rules>
3.63/2.06	      <contextJoinabilityProof>
3.63/2.06	       <funapp>
3.63/2.06	        <name>?1</name>
3.63/2.06	       </funapp>
3.63/2.06	       <conditionalRewritingSequence>
3.63/2.06	        <conditionalRewriteStep>
3.63/2.06	         <conditionalRule>
3.63/2.06	          <rule>
3.63/2.06	           <lhs>
3.63/2.06	            <funapp>
3.63/2.06	             <name>b</name>
3.63/2.06	            </funapp>
3.63/2.06	           </lhs>
3.63/2.06	           <rhs>
3.63/2.06	            <funapp>
3.63/2.06	             <name>?1</name>
3.63/2.06	            </funapp>
3.63/2.06	           </rhs>
3.63/2.06	          </rule>
3.63/2.06	         </conditionalRule>
3.63/2.06	         <positionInTerm></positionInTerm>
3.63/2.06	         <substitution> </substitution>
3.63/2.06	         <source>
3.63/2.06	          <funapp>
3.63/2.06	           <name>b</name>
3.63/2.06	          </funapp>
3.63/2.06	         </source>
3.63/2.06	         <target>
3.63/2.06	          <funapp>
3.63/2.06	           <name>?1</name>
3.63/2.06	          </funapp>
3.63/2.06	         </target>
3.63/2.06	         <conditions> </conditions>
3.63/2.06	        </conditionalRewriteStep>
3.63/2.06	       </conditionalRewritingSequence>
3.63/2.06	       <conditionalRewritingSequence>
3.63/2.06	        <conditionalRewriteStep>
3.63/2.06	         <conditionalRule>
3.63/2.06	          <rule>
3.63/2.06	           <lhs>
3.63/2.06	            <funapp>
3.63/2.06	             <name>a</name>
3.63/2.06	            </funapp>
3.63/2.06	           </lhs>
3.63/2.06	           <rhs>
3.63/2.06	            <funapp>
3.63/2.06	             <name>?1</name>
3.63/2.06	            </funapp>
3.63/2.06	           </rhs>
3.63/2.06	          </rule>
3.63/2.06	         </conditionalRule>
3.63/2.06	         <positionInTerm></positionInTerm>
3.63/2.06	         <substitution> </substitution>
3.63/2.06	         <source>
3.63/2.06	          <funapp>
3.63/2.06	           <name>a</name>
3.63/2.06	          </funapp>
3.63/2.06	         </source>
3.63/2.06	         <target>
3.63/2.06	          <funapp>
3.63/2.06	           <name>?1</name>
3.63/2.06	          </funapp>
3.63/2.06	         </target>
3.63/2.06	         <conditions> </conditions>
3.63/2.06	        </conditionalRewriteStep>
3.63/2.06	       </conditionalRewritingSequence>
3.63/2.06	       <constMap>
3.63/2.06	        <entry>
3.63/2.06	         <symbol>
3.63/2.06	          <name>?1</name>
3.63/2.06	         </symbol>
3.63/2.06	         <const>z</const>
3.63/2.06	        </entry>
3.63/2.06	       </constMap>
3.63/2.06	      </contextJoinabilityProof>
3.63/2.06	     </contextJoinableCCP>
3.63/2.06	     <contextJoinableCCP>
3.63/2.06	      <funapp>
3.63/2.06	       <name>a</name>
3.63/2.06	      </funapp>
3.63/2.06	      <funapp>
3.63/2.06	       <name>b</name>
3.63/2.06	      </funapp>
3.63/2.06	      <rules>
3.63/2.06	       <rule>
3.63/2.06	        <lhs>
3.63/2.06	         <funapp>
3.63/2.06	          <name>a</name>
3.63/2.06	         </funapp>
3.63/2.06	        </lhs>
3.63/2.06	        <rhs>
3.63/2.06	         <var>z</var>
3.63/2.06	        </rhs>
3.63/2.06	       </rule>
3.63/2.06	       <rule>
3.63/2.06	        <lhs>
3.63/2.06	         <funapp>
3.63/2.06	          <name>b</name>
3.63/2.06	         </funapp>
3.63/2.06	        </lhs>
3.63/2.06	        <rhs>
3.63/2.06	         <var>z</var>
3.63/2.06	        </rhs>
3.63/2.06	       </rule>
3.63/2.06	      </rules>
3.63/2.06	      <contextJoinabilityProof>
3.63/2.06	       <funapp>
3.63/2.06	        <name>?1</name>
3.63/2.06	       </funapp>
3.63/2.06	       <conditionalRewritingSequence>
3.63/2.06	        <conditionalRewriteStep>
3.63/2.06	         <conditionalRule>
3.63/2.06	          <rule>
3.63/2.06	           <lhs>
3.63/2.06	            <funapp>
3.63/2.06	             <name>a</name>
3.63/2.06	            </funapp>
3.63/2.06	           </lhs>
3.63/2.06	           <rhs>
3.63/2.06	            <funapp>
3.63/2.06	             <name>?1</name>
3.63/2.06	            </funapp>
3.63/2.06	           </rhs>
3.63/2.06	          </rule>
3.63/2.06	         </conditionalRule>
3.63/2.06	         <positionInTerm></positionInTerm>
3.63/2.06	         <substitution> </substitution>
3.63/2.06	         <source>
3.63/2.06	          <funapp>
3.63/2.06	           <name>a</name>
3.63/2.06	          </funapp>
3.63/2.06	         </source>
3.63/2.06	         <target>
3.63/2.06	          <funapp>
3.63/2.06	           <name>?1</name>
3.63/2.06	          </funapp>
3.63/2.06	         </target>
3.63/2.06	         <conditions> </conditions>
3.63/2.06	        </conditionalRewriteStep>
3.63/2.06	       </conditionalRewritingSequence>
3.63/2.06	       <conditionalRewritingSequence>
3.63/2.06	        <conditionalRewriteStep>
3.63/2.06	         <conditionalRule>
3.63/2.06	          <rule>
3.63/2.06	           <lhs>
3.63/2.06	            <funapp>
3.63/2.06	             <name>b</name>
3.63/2.06	            </funapp>
3.63/2.06	           </lhs>
3.63/2.06	           <rhs>
3.63/2.06	            <funapp>
3.63/2.06	             <name>?1</name>
3.63/2.06	            </funapp>
3.63/2.06	           </rhs>
3.63/2.06	          </rule>
3.63/2.06	         </conditionalRule>
3.63/2.06	         <positionInTerm></positionInTerm>
3.63/2.06	         <substitution> </substitution>
3.63/2.06	         <source>
3.63/2.06	          <funapp>
3.63/2.06	           <name>b</name>
3.63/2.06	          </funapp>
3.63/2.06	         </source>
3.63/2.06	         <target>
3.63/2.06	          <funapp>
3.63/2.06	           <name>?1</name>
3.63/2.06	          </funapp>
3.63/2.06	         </target>
3.63/2.06	         <conditions> </conditions>
3.63/2.06	        </conditionalRewriteStep>
3.63/2.06	       </conditionalRewritingSequence>
3.63/2.06	       <constMap>
3.63/2.06	        <entry>
3.63/2.06	         <symbol>
3.63/2.06	          <name>?1</name>
3.63/2.06	         </symbol>
3.63/2.06	         <const>z</const>
3.63/2.06	        </entry>
3.63/2.06	       </constMap>
3.63/2.06	      </contextJoinabilityProof>
3.63/2.06	     </contextJoinableCCP>
3.63/2.06	    </contextJoinableCCPs>
3.63/2.06	    <infeasibleConditions/>
3.63/2.06	    <unfeasibleCCPs/>
3.63/2.06	   </al94>
3.63/2.06	  </conditionalCrProof>
3.63/2.06	 </proof>
3.63/2.06	 <origin>
3.63/2.06	  <proofOrigin>
3.63/2.06	   <tool>
3.63/2.06	    <name>ConCon</name>
3.63/2.06	    <version>concon 1.4.0.0</version>
3.63/2.06	    <strategy>
3.63/2.06	     concon -s --cert --conf A --no-inlining theBenchmark.trs 58
3.63/2.06	    </strategy>
3.63/2.06	   </tool>
3.63/2.06	  </proofOrigin>
3.63/2.06	 </origin>
3.63/2.06	</certificationProblem>
3.63/2.07	EOF