3.92/2.10	YES
3.92/2.10	<?xml version="1.0"?><?xml-stylesheet type="text/xsl" href="cpfHTML.xsl"?>
3.92/2.10	<certificationProblem>
3.92/2.10	 <input>
3.92/2.10	  <ctrsInput>
3.92/2.10	   <conditionalRules>
3.92/2.10	    <conditionalRule>
3.92/2.10	     <rule>
3.92/2.10	      <lhs>
3.92/2.10	       <funapp>
3.92/2.10	        <name>add</name>
3.92/2.10	        <arg>
3.92/2.10	         <var>x</var>
3.92/2.10	        </arg>
3.92/2.10	        <arg>
3.92/2.10	         <funapp>
3.92/2.10	          <name>0</name>
3.92/2.10	         </funapp>
3.92/2.10	        </arg>
3.92/2.10	       </funapp>
3.92/2.10	      </lhs>
3.92/2.10	      <rhs>
3.92/2.10	       <var>x</var>
3.92/2.10	      </rhs>
3.92/2.10	     </rule>
3.92/2.10	    </conditionalRule>
3.92/2.10	    <conditionalRule>
3.92/2.10	     <rule>
3.92/2.10	      <lhs>
3.92/2.10	       <funapp>
3.92/2.10	        <name>add</name>
3.92/2.10	        <arg>
3.92/2.10	         <var>x</var>
3.92/2.10	        </arg>
3.92/2.10	        <arg>
3.92/2.10	         <funapp>
3.92/2.10	          <name>s</name>
3.92/2.10	          <arg>
3.92/2.10	           <var>y</var>
3.92/2.10	          </arg>
3.92/2.10	         </funapp>
3.92/2.10	        </arg>
3.92/2.10	       </funapp>
3.92/2.10	      </lhs>
3.92/2.10	      <rhs>
3.92/2.10	       <funapp>
3.92/2.10	        <name>s</name>
3.92/2.10	        <arg>
3.92/2.10	         <var>z</var>
3.92/2.10	        </arg>
3.92/2.10	       </funapp>
3.92/2.10	      </rhs>
3.92/2.10	     </rule>
3.92/2.10	     <rule>
3.92/2.10	      <lhs>
3.92/2.10	       <funapp>
3.92/2.10	        <name>add</name>
3.92/2.10	        <arg>
3.92/2.10	         <var>x</var>
3.92/2.10	        </arg>
3.92/2.10	        <arg>
3.92/2.10	         <var>y</var>
3.92/2.10	        </arg>
3.92/2.10	       </funapp>
3.92/2.10	      </lhs>
3.92/2.10	      <rhs>
3.92/2.10	       <var>z</var>
3.92/2.10	      </rhs>
3.92/2.10	     </rule>
3.92/2.10	    </conditionalRule>
3.92/2.10	   </conditionalRules>
3.92/2.10	  </ctrsInput>
3.92/2.10	 </input>
3.92/2.10	 <cpfVersion>2.4</cpfVersion>
3.92/2.10	 <proof>
3.92/2.10	  <conditionalCrProof>
3.92/2.10	   <al94>
3.92/2.10	    <quasiReductiveProof>
3.92/2.10	     <unraveling>
3.92/2.10	      <unravelingInformation>
3.92/2.10	       <unravelingEntry>
3.92/2.10	        <conditionalRule>
3.92/2.10	         <rule>
3.92/2.10	          <lhs>
3.92/2.10	           <funapp>
3.92/2.10	            <name>add</name>
3.92/2.10	            <arg>
3.92/2.10	             <var>x</var>
3.92/2.10	            </arg>
3.92/2.10	            <arg>
3.92/2.10	             <funapp>
3.92/2.10	              <name>0</name>
3.92/2.10	             </funapp>
3.92/2.10	            </arg>
3.92/2.10	           </funapp>
3.92/2.10	          </lhs>
3.92/2.10	          <rhs>
3.92/2.10	           <var>x</var>
3.92/2.10	          </rhs>
3.92/2.10	         </rule>
3.92/2.10	        </conditionalRule>
3.92/2.10	        <rule>
3.92/2.10	         <lhs>
3.92/2.10	          <funapp>
3.92/2.10	           <name>add</name>
3.92/2.10	           <arg>
3.92/2.10	            <var>x</var>
3.92/2.10	           </arg>
3.92/2.10	           <arg>
3.92/2.10	            <funapp>
3.92/2.10	             <name>0</name>
3.92/2.10	            </funapp>
3.92/2.10	           </arg>
3.92/2.10	          </funapp>
3.92/2.10	         </lhs>
3.92/2.10	         <rhs>
3.92/2.10	          <var>x</var>
3.92/2.10	         </rhs>
3.92/2.10	        </rule>
3.92/2.10	       </unravelingEntry>
3.92/2.10	       <unravelingEntry>
3.92/2.10	        <conditionalRule>
3.92/2.10	         <rule>
3.92/2.10	          <lhs>
3.92/2.10	           <funapp>
3.92/2.10	            <name>add</name>
3.92/2.10	            <arg>
3.92/2.10	             <var>x</var>
3.92/2.10	            </arg>
3.92/2.10	            <arg>
3.92/2.10	             <funapp>
3.92/2.10	              <name>s</name>
3.92/2.10	              <arg>
3.92/2.10	               <var>y</var>
3.92/2.10	              </arg>
3.92/2.10	             </funapp>
3.92/2.10	            </arg>
3.92/2.10	           </funapp>
3.92/2.10	          </lhs>
3.92/2.10	          <rhs>
3.92/2.10	           <funapp>
3.92/2.10	            <name>s</name>
3.92/2.10	            <arg>
3.92/2.10	             <var>z</var>
3.92/2.10	            </arg>
3.92/2.10	           </funapp>
3.92/2.10	          </rhs>
3.92/2.10	         </rule>
3.92/2.10	         <rule>
3.92/2.10	          <lhs>
3.92/2.10	           <funapp>
3.92/2.10	            <name>add</name>
3.92/2.10	            <arg>
3.92/2.10	             <var>x</var>
3.92/2.10	            </arg>
3.92/2.10	            <arg>
3.92/2.10	             <var>y</var>
3.92/2.10	            </arg>
3.92/2.10	           </funapp>
3.92/2.10	          </lhs>
3.92/2.10	          <rhs>
3.92/2.10	           <var>z</var>
3.92/2.10	          </rhs>
3.92/2.10	         </rule>
3.92/2.10	        </conditionalRule>
3.92/2.10	        <rule>
3.92/2.10	         <lhs>
3.92/2.10	          <funapp>
3.92/2.10	           <name>add</name>
3.92/2.10	           <arg>
3.92/2.10	            <var>x</var>
3.92/2.10	           </arg>
3.92/2.10	           <arg>
3.92/2.10	            <funapp>
3.92/2.10	             <name>s</name>
3.92/2.10	             <arg>
3.92/2.10	              <var>y</var>
3.92/2.10	             </arg>
3.92/2.10	            </funapp>
3.92/2.10	           </arg>
3.92/2.10	          </funapp>
3.92/2.10	         </lhs>
3.92/2.10	         <rhs>
3.92/2.10	          <funapp>
3.92/2.10	           <name>U1</name>
3.92/2.10	           <arg>
3.92/2.10	            <funapp>
3.92/2.10	             <name>add</name>
3.92/2.10	             <arg>
3.92/2.10	              <var>x</var>
3.92/2.10	             </arg>
3.92/2.10	             <arg>
3.92/2.10	              <var>y</var>
3.92/2.10	             </arg>
3.92/2.10	            </funapp>
3.92/2.10	           </arg>
3.92/2.10	           <arg>
3.92/2.10	            <var>x</var>
3.92/2.10	           </arg>
3.92/2.10	           <arg>
3.92/2.10	            <var>y</var>
3.92/2.10	           </arg>
3.92/2.10	          </funapp>
3.92/2.10	         </rhs>
3.92/2.10	        </rule>
3.92/2.10	        <rule>
3.92/2.10	         <lhs>
3.92/2.10	          <funapp>
3.92/2.10	           <name>U1</name>
3.92/2.10	           <arg>
3.92/2.10	            <var>z</var>
3.92/2.10	           </arg>
3.92/2.10	           <arg>
3.92/2.10	            <var>x</var>
3.92/2.10	           </arg>
3.92/2.10	           <arg>
3.92/2.10	            <var>y</var>
3.92/2.10	           </arg>
3.92/2.10	          </funapp>
3.92/2.10	         </lhs>
3.92/2.10	         <rhs>
3.92/2.10	          <funapp>
3.92/2.10	           <name>s</name>
3.92/2.10	           <arg>
3.92/2.10	            <var>z</var>
3.92/2.10	           </arg>
3.92/2.10	          </funapp>
3.92/2.10	         </rhs>
3.92/2.10	        </rule>
3.92/2.10	       </unravelingEntry>
3.92/2.10	      </unravelingInformation>
3.92/2.10	      <trsTerminationProof>
3.92/2.10	       <dpTrans>
3.92/2.10	        <dps>
3.92/2.10	         <rules>
3.92/2.10	          <rule>
3.92/2.10	           <lhs>
3.92/2.10	            <funapp>
3.92/2.10	             <sharp>
3.92/2.10	              <name>add</name>
3.92/2.10	             </sharp>
3.92/2.10	             <arg>
3.92/2.10	              <var>x</var>
3.92/2.10	             </arg>
3.92/2.10	             <arg>
3.92/2.10	              <funapp>
3.92/2.10	               <name>s</name>
3.92/2.10	               <arg>
3.92/2.10	                <var>y</var>
3.92/2.10	               </arg>
3.92/2.10	              </funapp>
3.92/2.10	             </arg>
3.92/2.10	            </funapp>
3.92/2.10	           </lhs>
3.92/2.10	           <rhs>
3.92/2.10	            <funapp>
3.92/2.10	             <sharp>
3.92/2.10	              <name>add</name>
3.92/2.10	             </sharp>
3.92/2.10	             <arg>
3.92/2.10	              <var>x</var>
3.92/2.10	             </arg>
3.92/2.10	             <arg>
3.92/2.10	              <var>y</var>
3.92/2.10	             </arg>
3.92/2.10	            </funapp>
3.92/2.10	           </rhs>
3.92/2.10	          </rule>
3.92/2.10	          <rule>
3.92/2.10	           <lhs>
3.92/2.10	            <funapp>
3.92/2.10	             <sharp>
3.92/2.10	              <name>add</name>
3.92/2.10	             </sharp>
3.92/2.10	             <arg>
3.92/2.10	              <var>x</var>
3.92/2.10	             </arg>
3.92/2.10	             <arg>
3.92/2.10	              <funapp>
3.92/2.10	               <name>s</name>
3.92/2.10	               <arg>
3.92/2.10	                <var>y</var>
3.92/2.10	               </arg>
3.92/2.10	              </funapp>
3.92/2.10	             </arg>
3.92/2.10	            </funapp>
3.92/2.10	           </lhs>
3.92/2.10	           <rhs>
3.92/2.10	            <funapp>
3.92/2.10	             <sharp>
3.92/2.10	              <name>U1</name>
3.92/2.10	             </sharp>
3.92/2.10	             <arg>
3.92/2.10	              <funapp>
3.92/2.10	               <name>add</name>
3.92/2.10	               <arg>
3.92/2.10	                <var>x</var>
3.92/2.10	               </arg>
3.92/2.10	               <arg>
3.92/2.10	                <var>y</var>
3.92/2.10	               </arg>
3.92/2.10	              </funapp>
3.92/2.10	             </arg>
3.92/2.10	             <arg>
3.92/2.10	              <var>x</var>
3.92/2.10	             </arg>
3.92/2.10	             <arg>
3.92/2.10	              <var>y</var>
3.92/2.10	             </arg>
3.92/2.10	            </funapp>
3.92/2.10	           </rhs>
3.92/2.10	          </rule>
3.92/2.10	         </rules>
3.92/2.10	        </dps>
3.92/2.10	        <markedSymbols>true</markedSymbols>
3.92/2.10	        <dpProof>
3.92/2.10	         <depGraphProc>
3.92/2.10	          <component>
3.92/2.10	           <dps>
3.92/2.10	            <rules>
3.92/2.10	             <rule>
3.92/2.10	              <lhs>
3.92/2.10	               <funapp>
3.92/2.10	                <sharp>
3.92/2.10	                 <name>add</name>
3.92/2.10	                </sharp>
3.92/2.10	                <arg>
3.92/2.10	                 <var>x</var>
3.92/2.10	                </arg>
3.92/2.10	                <arg>
3.92/2.10	                 <funapp>
3.92/2.10	                  <name>s</name>
3.92/2.10	                  <arg>
3.92/2.10	                   <var>y</var>
3.92/2.10	                  </arg>
3.92/2.10	                 </funapp>
3.92/2.10	                </arg>
3.92/2.10	               </funapp>
3.92/2.10	              </lhs>
3.92/2.10	              <rhs>
3.92/2.10	               <funapp>
3.92/2.10	                <sharp>
3.92/2.10	                 <name>add</name>
3.92/2.10	                </sharp>
3.92/2.10	                <arg>
3.92/2.10	                 <var>x</var>
3.92/2.10	                </arg>
3.92/2.10	                <arg>
3.92/2.10	                 <var>y</var>
3.92/2.10	                </arg>
3.92/2.10	               </funapp>
3.92/2.10	              </rhs>
3.92/2.10	             </rule>
3.92/2.10	            </rules>
3.92/2.10	           </dps>
3.92/2.10	           <realScc>true</realScc>
3.92/2.10	           <arcs>
3.92/2.10	            <forwardArc>1</forwardArc>
3.92/2.10	           </arcs>
3.92/2.10	           <dpProof>
3.92/2.10	            <sizeChangeProc>
3.92/2.10	             <subtermCriterion/>
3.92/2.10	             <sizeChangeGraph>
3.92/2.10	              <rule>
3.92/2.10	               <lhs>
3.92/2.10	                <funapp>
3.92/2.10	                 <sharp>
3.92/2.10	                  <name>add</name>
3.92/2.10	                 </sharp>
3.92/2.10	                 <arg>
3.92/2.10	                  <var>x</var>
3.92/2.10	                 </arg>
3.92/2.10	                 <arg>
3.92/2.10	                  <funapp>
3.92/2.10	                   <name>s</name>
3.92/2.10	                   <arg>
3.92/2.10	                    <var>y</var>
3.92/2.10	                   </arg>
3.92/2.10	                  </funapp>
3.92/2.10	                 </arg>
3.92/2.10	                </funapp>
3.92/2.10	               </lhs>
3.92/2.10	               <rhs>
3.92/2.10	                <funapp>
3.92/2.10	                 <sharp>
3.92/2.10	                  <name>add</name>
3.92/2.10	                 </sharp>
3.92/2.10	                 <arg>
3.92/2.10	                  <var>x</var>
3.92/2.10	                 </arg>
3.92/2.10	                 <arg>
3.92/2.10	                  <var>y</var>
3.92/2.10	                 </arg>
3.92/2.10	                </funapp>
3.92/2.10	               </rhs>
3.92/2.10	              </rule>
3.92/2.10	              <edge>
3.92/2.10	               <position>2</position>
3.92/2.10	               <strict>true</strict>
3.92/2.10	               <position>2</position>
3.92/2.10	              </edge>
3.92/2.10	              <edge>
3.92/2.10	               <position>1</position>
3.92/2.10	               <strict>false</strict>
3.92/2.10	               <position>1</position>
3.92/2.10	              </edge>
3.92/2.10	             </sizeChangeGraph>
3.92/2.10	            </sizeChangeProc>
3.92/2.10	           </dpProof>
3.92/2.10	          </component>
3.92/2.10	          <component>
3.92/2.10	           <dps>
3.92/2.10	            <rules>
3.92/2.10	             <rule>
3.92/2.10	              <lhs>
3.92/2.10	               <funapp>
3.92/2.10	                <sharp>
3.92/2.10	                 <name>add</name>
3.92/2.10	                </sharp>
3.92/2.10	                <arg>
3.92/2.10	                 <var>x</var>
3.92/2.10	                </arg>
3.92/2.10	                <arg>
3.92/2.10	                 <funapp>
3.92/2.10	                  <name>s</name>
3.92/2.10	                  <arg>
3.92/2.10	                   <var>y</var>
3.92/2.10	                  </arg>
3.92/2.10	                 </funapp>
3.92/2.10	                </arg>
3.92/2.10	               </funapp>
3.92/2.10	              </lhs>
3.92/2.10	              <rhs>
3.92/2.10	               <funapp>
3.92/2.10	                <sharp>
3.92/2.10	                 <name>U1</name>
3.92/2.10	                </sharp>
3.92/2.10	                <arg>
3.92/2.10	                 <funapp>
3.92/2.10	                  <name>add</name>
3.92/2.10	                  <arg>
3.92/2.10	                   <var>x</var>
3.92/2.10	                  </arg>
3.92/2.10	                  <arg>
3.92/2.10	                   <var>y</var>
3.92/2.10	                  </arg>
3.92/2.10	                 </funapp>
3.92/2.10	                </arg>
3.92/2.10	                <arg>
3.92/2.10	                 <var>x</var>
3.92/2.10	                </arg>
3.92/2.10	                <arg>
3.92/2.10	                 <var>y</var>
3.92/2.10	                </arg>
3.92/2.10	               </funapp>
3.92/2.10	              </rhs>
3.92/2.10	             </rule>
3.92/2.10	            </rules>
3.92/2.10	           </dps>
3.92/2.10	           <realScc>false</realScc>
3.92/2.10	           <arcs/>
3.92/2.10	          </component>
3.92/2.10	         </depGraphProc>
3.92/2.10	        </dpProof>
3.92/2.10	       </dpTrans>
3.92/2.10	      </trsTerminationProof>
3.92/2.10	     </unraveling>
3.92/2.10	    </quasiReductiveProof>
3.92/2.10	    <contextJoinableCCPs/>
3.92/2.10	    <infeasibleConditions/>
3.92/2.10	    <unfeasibleCCPs/>
3.92/2.10	   </al94>
3.92/2.10	  </conditionalCrProof>
3.92/2.10	 </proof>
3.92/2.10	 <origin>
3.92/2.10	  <proofOrigin>
3.92/2.10	   <tool>
3.92/2.10	    <name>ConCon</name>
3.92/2.10	    <version>concon 1.4.0.0</version>
3.92/2.10	    <strategy>
3.92/2.10	     concon -s --cert --conf A --no-inlining theBenchmark.trs 58
3.92/2.10	    </strategy>
3.92/2.10	   </tool>
3.92/2.10	  </proofOrigin>
3.92/2.10	 </origin>
3.92/2.10	</certificationProblem>
3.92/2.13	EOF