3.58/2.35	YES
3.58/2.35	<?xml version="1.0"?><?xml-stylesheet type="text/xsl" href="cpfHTML.xsl"?>
3.58/2.35	<certificationProblem>
3.58/2.35	 <input>
3.58/2.35	  <ctrsInput>
3.58/2.35	   <rules>
3.58/2.35	    <rule>
3.58/2.35	     <lhs>
3.58/2.35	      <funapp>
3.58/2.35	       <name>f</name>
3.58/2.35	       <arg>
3.58/2.35	        <var>x</var>
3.58/2.35	       </arg>
3.58/2.35	       <arg>
3.58/2.35	        <var>x</var>
3.58/2.35	       </arg>
3.58/2.35	      </funapp>
3.58/2.35	     </lhs>
3.58/2.35	     <rhs>
3.58/2.35	      <funapp>
3.58/2.35	       <name>a</name>
3.58/2.35	      </funapp>
3.58/2.35	     </rhs>
3.58/2.35	     <conditions>
3.58/2.35	      <condition>
3.58/2.35	       <lhs>
3.58/2.35	        <funapp>
3.58/2.35	         <name>g</name>
3.58/2.35	         <arg>
3.58/2.35	          <var>x</var>
3.58/2.35	         </arg>
3.58/2.35	        </funapp>
3.58/2.35	       </lhs>
3.58/2.35	       <rhs>
3.58/2.35	        <funapp>
3.58/2.35	         <name>b</name>
3.58/2.35	        </funapp>
3.58/2.35	       </rhs>
3.58/2.35	      </condition>
3.58/2.35	     </conditions>
3.58/2.35	    </rule>
3.58/2.35	   </rules>
3.58/2.35	  </ctrsInput>
3.58/2.35	 </input>
3.58/2.35	 <cpfVersion>2.4</cpfVersion>
3.58/2.35	 <proof>
3.58/2.35	  <conditionalCrProof>
3.58/2.35	   <infeasibleRuleRemoval>
3.58/2.35	    <infeasibleRules>
3.58/2.35	     <infeasibleRule>
3.58/2.35	      <rule>
3.58/2.35	       <lhs>
3.58/2.35	        <funapp>
3.58/2.35	         <name>f</name>
3.58/2.35	         <arg>
3.58/2.35	          <var>x</var>
3.58/2.35	         </arg>
3.58/2.35	         <arg>
3.58/2.35	          <var>x</var>
3.58/2.35	         </arg>
3.58/2.35	        </funapp>
3.58/2.35	       </lhs>
3.58/2.35	       <rhs>
3.58/2.35	        <funapp>
3.58/2.35	         <name>a</name>
3.58/2.35	        </funapp>
3.58/2.35	       </rhs>
3.58/2.35	       <conditions>
3.58/2.35	        <condition>
3.58/2.35	         <lhs>
3.58/2.35	          <funapp>
3.58/2.35	           <name>g</name>
3.58/2.35	           <arg>
3.58/2.35	            <var>x</var>
3.58/2.35	           </arg>
3.58/2.35	          </funapp>
3.58/2.35	         </lhs>
3.58/2.35	         <rhs>
3.58/2.35	          <funapp>
3.58/2.35	           <name>b</name>
3.58/2.35	          </funapp>
3.58/2.35	         </rhs>
3.58/2.35	        </condition>
3.58/2.35	       </conditions>
3.58/2.35	      </rule>
3.58/2.35	      <infeasibilityProof>
3.58/2.35	       <infeasibleEquation>
3.58/2.35	        <rule>
3.58/2.35	         <lhs>
3.58/2.35	          <funapp>
3.58/2.35	           <name>g</name>
3.58/2.35	           <arg>
3.58/2.35	            <var>x</var>
3.58/2.35	           </arg>
3.58/2.35	          </funapp>
3.58/2.35	         </lhs>
3.58/2.35	         <rhs>
3.58/2.35	          <funapp>
3.58/2.35	           <name>b</name>
3.58/2.35	          </funapp>
3.58/2.35	         </rhs>
3.58/2.35	        </rule>
3.58/2.35	        <nonreachabilityProof>
3.58/2.35	         <nonreachableTcap/>
3.58/2.35	        </nonreachabilityProof>
3.58/2.35	       </infeasibleEquation>
3.58/2.35	      </infeasibilityProof>
3.58/2.35	     </infeasibleRule>
3.58/2.35	    </infeasibleRules>
3.58/2.35	    <conditionalCrProof>
3.58/2.35	     <almostOrthogonal/>
3.58/2.35	    </conditionalCrProof>
3.58/2.35	   </infeasibleRuleRemoval>
3.58/2.35	  </conditionalCrProof>
3.58/2.35	 </proof>
3.58/2.35	 <origin>
3.58/2.35	  <proofOrigin>
3.58/2.35	   <tool>
3.58/2.35	    <name>ConCon</name>
3.58/2.35	    <version>concon 1.10.0.0</version>
3.58/2.35	    <strategy>
3.58/2.35	     concon -s --inf 'tcap exeq oc etac' --cert theBenchmark.trs 58
3.58/2.35	    </strategy>
3.58/2.35	   </tool>
3.58/2.35	  </proofOrigin>
3.58/2.35	 </origin>
3.58/2.35	</certificationProblem>
3.58/2.35	EOF