2.90/1.81	YES
2.90/1.81	<?xml version="1.0"?><?xml-stylesheet type="text/xsl" href="cpfHTML.xsl"?>
2.90/1.81	<certificationProblem>
2.90/1.81	 <input>
2.90/1.81	  <ctrsInput>
2.90/1.81	   <conditionalRules>
2.90/1.81	    <conditionalRule>
2.90/1.81	     <rule>
2.90/1.81	      <lhs>
2.90/1.81	       <funapp>
2.90/1.81	        <name>f</name>
2.90/1.81	        <arg>
2.90/1.81	         <var>x</var>
2.90/1.81	        </arg>
2.90/1.81	       </funapp>
2.90/1.81	      </lhs>
2.90/1.81	      <rhs>
2.90/1.81	       <funapp>
2.90/1.81	        <name>a</name>
2.90/1.81	       </funapp>
2.90/1.81	      </rhs>
2.90/1.81	     </rule>
2.90/1.81	     <rule>
2.90/1.81	      <lhs>
2.90/1.81	       <var>x</var>
2.90/1.81	      </lhs>
2.90/1.81	      <rhs>
2.90/1.81	       <funapp>
2.90/1.81	        <name>b</name>
2.90/1.81	       </funapp>
2.90/1.81	      </rhs>
2.90/1.81	     </rule>
2.90/1.81	    </conditionalRule>
2.90/1.81	   </conditionalRules>
2.90/1.81	  </ctrsInput>
2.90/1.81	 </input>
2.90/1.81	 <cpfVersion>2.4</cpfVersion>
2.90/1.81	 <proof>
2.90/1.81	  <conditionalCrProof>
2.90/1.81	   <al94>
2.90/1.81	    <quasiReductiveProof>
2.90/1.81	     <unraveling>
2.90/1.81	      <unravelingInformation>
2.90/1.81	       <unravelingEntry>
2.90/1.81	        <conditionalRule>
2.90/1.81	         <rule>
2.90/1.81	          <lhs>
2.90/1.81	           <funapp>
2.90/1.81	            <name>f</name>
2.90/1.81	            <arg>
2.90/1.81	             <var>x</var>
2.90/1.81	            </arg>
2.90/1.81	           </funapp>
2.90/1.81	          </lhs>
2.90/1.81	          <rhs>
2.90/1.81	           <funapp>
2.90/1.81	            <name>a</name>
2.90/1.81	           </funapp>
2.90/1.81	          </rhs>
2.90/1.81	         </rule>
2.90/1.81	         <rule>
2.90/1.81	          <lhs>
2.90/1.81	           <var>x</var>
2.90/1.81	          </lhs>
2.90/1.81	          <rhs>
2.90/1.81	           <funapp>
2.90/1.81	            <name>b</name>
2.90/1.81	           </funapp>
2.90/1.81	          </rhs>
2.90/1.81	         </rule>
2.90/1.81	        </conditionalRule>
2.90/1.81	        <rule>
2.90/1.81	         <lhs>
2.90/1.81	          <funapp>
2.90/1.81	           <name>f</name>
2.90/1.81	           <arg>
2.90/1.81	            <var>x</var>
2.90/1.81	           </arg>
2.90/1.81	          </funapp>
2.90/1.81	         </lhs>
2.90/1.81	         <rhs>
2.90/1.81	          <funapp>
2.90/1.81	           <name>U1</name>
2.90/1.81	           <arg>
2.90/1.81	            <var>x</var>
2.90/1.81	           </arg>
2.90/1.81	           <arg>
2.90/1.81	            <var>x</var>
2.90/1.81	           </arg>
2.90/1.81	          </funapp>
2.90/1.81	         </rhs>
2.90/1.81	        </rule>
2.90/1.81	        <rule>
2.90/1.81	         <lhs>
2.90/1.81	          <funapp>
2.90/1.81	           <name>U1</name>
2.90/1.81	           <arg>
2.90/1.81	            <funapp>
2.90/1.81	             <name>b</name>
2.90/1.81	            </funapp>
2.90/1.81	           </arg>
2.90/1.81	           <arg>
2.90/1.81	            <var>x</var>
2.90/1.81	           </arg>
2.90/1.81	          </funapp>
2.90/1.81	         </lhs>
2.90/1.81	         <rhs>
2.90/1.81	          <funapp>
2.90/1.81	           <name>a</name>
2.90/1.81	          </funapp>
2.90/1.81	         </rhs>
2.90/1.81	        </rule>
2.90/1.81	       </unravelingEntry>
2.90/1.81	      </unravelingInformation>
2.90/1.81	      <trsTerminationProof>
2.90/1.81	       <ruleRemoval>
2.90/1.81	        <orderingConstraintProof>
2.90/1.81	         <redPair>
2.90/1.81	          <interpretation>
2.90/1.81	           <type>
2.90/1.81	            <polynomial>
2.90/1.81	             <domain>
2.90/1.81	              <matrices>
2.90/1.81	               <dimension>3</dimension>
2.90/1.81	               <strictDimension>1</strictDimension>
2.90/1.81	               <domain>
2.90/1.81	                <naturals/>
2.90/1.81	               </domain>
2.90/1.81	              </matrices>
2.90/1.81	             </domain>
2.90/1.81	             <degree>1</degree>
2.90/1.81	            </polynomial>
2.90/1.81	           </type>
2.90/1.81	           <interpret>
2.90/1.81	            <name>a</name>
2.90/1.81	            <arity>0</arity>
2.90/1.81	            <polynomial>
2.90/1.81	             <sum>
2.90/1.81	              <polynomial>
2.90/1.81	               <coefficient>
2.90/1.81	                <matrix>
2.90/1.81	                 <vector>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                 </vector>
2.90/1.81	                 <vector>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                 </vector>
2.90/1.81	                 <vector>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                 </vector>
2.90/1.81	                </matrix>
2.90/1.81	               </coefficient>
2.90/1.81	              </polynomial>
2.90/1.81	             </sum>
2.90/1.81	            </polynomial>
2.90/1.81	           </interpret>
2.90/1.81	           <interpret>
2.90/1.81	            <name>b</name>
2.90/1.81	            <arity>0</arity>
2.90/1.81	            <polynomial>
2.90/1.81	             <sum>
2.90/1.81	              <polynomial>
2.90/1.81	               <coefficient>
2.90/1.81	                <matrix>
2.90/1.81	                 <vector>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>2</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                 </vector>
2.90/1.81	                 <vector>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                 </vector>
2.90/1.81	                 <vector>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                 </vector>
2.90/1.81	                </matrix>
2.90/1.81	               </coefficient>
2.90/1.81	              </polynomial>
2.90/1.81	             </sum>
2.90/1.81	            </polynomial>
2.90/1.81	           </interpret>
2.90/1.81	           <interpret>
2.90/1.81	            <name>U1</name>
2.90/1.81	            <arity>2</arity>
2.90/1.81	            <polynomial>
2.90/1.81	             <sum>
2.90/1.81	              <polynomial>
2.90/1.81	               <product>
2.90/1.81	                <polynomial>
2.90/1.81	                 <coefficient>
2.90/1.81	                  <matrix>
2.90/1.81	                   <vector>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>1</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>0</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>0</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                   </vector>
2.90/1.81	                   <vector>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>0</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>0</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>0</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                   </vector>
2.90/1.81	                   <vector>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>0</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>0</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>0</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                   </vector>
2.90/1.81	                  </matrix>
2.90/1.81	                 </coefficient>
2.90/1.81	                </polynomial>
2.90/1.81	                <polynomial>
2.90/1.81	                 <variable>1</variable>
2.90/1.81	                </polynomial>
2.90/1.81	               </product>
2.90/1.81	              </polynomial>
2.90/1.81	              <polynomial>
2.90/1.81	               <product>
2.90/1.81	                <polynomial>
2.90/1.81	                 <coefficient>
2.90/1.81	                  <matrix>
2.90/1.81	                   <vector>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>2</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>0</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>0</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                   </vector>
2.90/1.81	                   <vector>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>0</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>0</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>0</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                   </vector>
2.90/1.81	                   <vector>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>0</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>0</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>0</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                   </vector>
2.90/1.81	                  </matrix>
2.90/1.81	                 </coefficient>
2.90/1.81	                </polynomial>
2.90/1.81	                <polynomial>
2.90/1.81	                 <variable>2</variable>
2.90/1.81	                </polynomial>
2.90/1.81	               </product>
2.90/1.81	              </polynomial>
2.90/1.81	              <polynomial>
2.90/1.81	               <coefficient>
2.90/1.81	                <matrix>
2.90/1.81	                 <vector>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>1</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                 </vector>
2.90/1.81	                 <vector>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                 </vector>
2.90/1.81	                 <vector>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                 </vector>
2.90/1.81	                </matrix>
2.90/1.81	               </coefficient>
2.90/1.81	              </polynomial>
2.90/1.81	             </sum>
2.90/1.81	            </polynomial>
2.90/1.81	           </interpret>
2.90/1.81	           <interpret>
2.90/1.81	            <name>f</name>
2.90/1.81	            <arity>1</arity>
2.90/1.81	            <polynomial>
2.90/1.81	             <sum>
2.90/1.81	              <polynomial>
2.90/1.81	               <product>
2.90/1.81	                <polynomial>
2.90/1.81	                 <coefficient>
2.90/1.81	                  <matrix>
2.90/1.81	                   <vector>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>3</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>0</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>0</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                   </vector>
2.90/1.81	                   <vector>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>0</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>0</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>0</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                   </vector>
2.90/1.81	                   <vector>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>0</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>0</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                    <coefficient>
2.90/1.81	                     <integer>0</integer>
2.90/1.81	                    </coefficient>
2.90/1.81	                   </vector>
2.90/1.81	                  </matrix>
2.90/1.81	                 </coefficient>
2.90/1.81	                </polynomial>
2.90/1.81	                <polynomial>
2.90/1.81	                 <variable>1</variable>
2.90/1.81	                </polynomial>
2.90/1.81	               </product>
2.90/1.81	              </polynomial>
2.90/1.81	              <polynomial>
2.90/1.81	               <coefficient>
2.90/1.81	                <matrix>
2.90/1.81	                 <vector>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>2</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                 </vector>
2.90/1.81	                 <vector>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                 </vector>
2.90/1.81	                 <vector>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                  <coefficient>
2.90/1.81	                   <integer>0</integer>
2.90/1.81	                  </coefficient>
2.90/1.81	                 </vector>
2.90/1.81	                </matrix>
2.90/1.81	               </coefficient>
2.90/1.81	              </polynomial>
2.90/1.81	             </sum>
2.90/1.81	            </polynomial>
2.90/1.81	           </interpret>
2.90/1.81	          </interpretation>
2.90/1.81	         </redPair>
2.90/1.81	        </orderingConstraintProof>
2.90/1.81	        <trs>
2.90/1.81	         <rules/>
2.90/1.82	        </trs>
2.90/1.82	        <trsTerminationProof>
2.90/1.82	         <rIsEmpty/>
2.90/1.82	        </trsTerminationProof>
2.90/1.82	       </ruleRemoval>
2.90/1.82	      </trsTerminationProof>
2.90/1.82	     </unraveling>
2.90/1.82	    </quasiReductiveProof>
2.90/1.82	    <contextJoinableCCPs/>
2.90/1.82	    <infeasibleConditions/>
2.90/1.82	    <unfeasibleCCPs/>
2.90/1.82	   </al94>
2.90/1.82	  </conditionalCrProof>
2.90/1.82	 </proof>
2.90/1.82	 <origin>
2.90/1.82	  <proofOrigin>
2.90/1.82	   <tool>
2.90/1.82	    <name>ConCon</name>
2.90/1.82	    <version>concon 1.4.0.0</version>
2.90/1.82	    <strategy>
2.90/1.82	     concon -s --cert --conf A --no-inlining theBenchmark.trs 58
2.90/1.82	    </strategy>
2.90/1.82	   </tool>
2.90/1.82	  </proofOrigin>
2.90/1.82	 </origin>
2.90/1.82	</certificationProblem>
2.90/1.82	EOF