6.45/2.81	YES
6.45/2.81	<?xml version="1.0"?><?xml-stylesheet type="text/xsl" href="cpfHTML.xsl"?>
6.45/2.81	<certificationProblem>
6.45/2.81	 <input>
6.45/2.81	  <ctrsInput>
6.45/2.81	   <conditionalRules>
6.45/2.81	    <conditionalRule>
6.45/2.81	     <rule>
6.45/2.81	      <lhs>
6.45/2.81	       <funapp>
6.45/2.81	        <name>isnoc</name>
6.45/2.81	        <arg>
6.45/2.81	         <funapp>
6.45/2.81	          <name>cons</name>
6.45/2.81	          <arg>
6.45/2.81	           <var>y</var>
6.45/2.81	          </arg>
6.45/2.81	          <arg>
6.45/2.81	           <funapp>
6.45/2.81	            <name>nil</name>
6.45/2.81	           </funapp>
6.45/2.81	          </arg>
6.45/2.81	         </funapp>
6.45/2.81	        </arg>
6.45/2.81	       </funapp>
6.45/2.81	      </lhs>
6.45/2.81	      <rhs>
6.45/2.81	       <funapp>
6.45/2.81	        <name>tp2</name>
6.45/2.81	        <arg>
6.45/2.81	         <funapp>
6.45/2.81	          <name>nil</name>
6.45/2.81	         </funapp>
6.45/2.81	        </arg>
6.45/2.81	        <arg>
6.45/2.81	         <var>y</var>
6.45/2.81	        </arg>
6.45/2.81	       </funapp>
6.45/2.81	      </rhs>
6.45/2.81	     </rule>
6.45/2.81	    </conditionalRule>
6.45/2.81	    <conditionalRule>
6.45/2.81	     <rule>
6.45/2.81	      <lhs>
6.45/2.81	       <funapp>
6.45/2.81	        <name>isnoc</name>
6.45/2.81	        <arg>
6.45/2.81	         <funapp>
6.45/2.81	          <name>cons</name>
6.45/2.81	          <arg>
6.45/2.81	           <var>x</var>
6.45/2.81	          </arg>
6.45/2.81	          <arg>
6.45/2.81	           <var>ys</var>
6.45/2.81	          </arg>
6.45/2.81	         </funapp>
6.45/2.81	        </arg>
6.45/2.81	       </funapp>
6.45/2.81	      </lhs>
6.45/2.81	      <rhs>
6.45/2.81	       <funapp>
6.45/2.81	        <name>tp2</name>
6.45/2.81	        <arg>
6.45/2.81	         <funapp>
6.45/2.81	          <name>cons</name>
6.45/2.81	          <arg>
6.45/2.81	           <var>x</var>
6.45/2.81	          </arg>
6.45/2.81	          <arg>
6.45/2.81	           <var>xs</var>
6.45/2.81	          </arg>
6.45/2.81	         </funapp>
6.45/2.81	        </arg>
6.45/2.81	        <arg>
6.45/2.81	         <var>y</var>
6.45/2.81	        </arg>
6.45/2.81	       </funapp>
6.45/2.81	      </rhs>
6.45/2.81	     </rule>
6.45/2.81	     <rule>
6.45/2.81	      <lhs>
6.45/2.81	       <funapp>
6.45/2.81	        <name>isnoc</name>
6.45/2.81	        <arg>
6.45/2.81	         <var>ys</var>
6.45/2.81	        </arg>
6.45/2.81	       </funapp>
6.45/2.81	      </lhs>
6.45/2.81	      <rhs>
6.45/2.81	       <funapp>
6.45/2.81	        <name>tp2</name>
6.45/2.81	        <arg>
6.45/2.81	         <var>xs</var>
6.45/2.81	        </arg>
6.45/2.81	        <arg>
6.45/2.81	         <var>y</var>
6.45/2.81	        </arg>
6.45/2.81	       </funapp>
6.45/2.81	      </rhs>
6.45/2.81	     </rule>
6.45/2.81	    </conditionalRule>
6.45/2.81	   </conditionalRules>
6.45/2.81	  </ctrsInput>
6.45/2.81	 </input>
6.45/2.81	 <cpfVersion>2.4</cpfVersion>
6.45/2.81	 <proof>
6.45/2.81	  <conditionalCrProof>
6.45/2.81	   <al94>
6.45/2.81	    <quasiReductiveProof>
6.45/2.81	     <unraveling>
6.45/2.81	      <unravelingInformation>
6.45/2.81	       <unravelingEntry>
6.45/2.81	        <conditionalRule>
6.45/2.81	         <rule>
6.45/2.81	          <lhs>
6.45/2.81	           <funapp>
6.45/2.81	            <name>isnoc</name>
6.45/2.81	            <arg>
6.45/2.81	             <funapp>
6.45/2.81	              <name>cons</name>
6.45/2.81	              <arg>
6.45/2.81	               <var>y</var>
6.45/2.81	              </arg>
6.45/2.81	              <arg>
6.45/2.81	               <funapp>
6.45/2.81	                <name>nil</name>
6.45/2.81	               </funapp>
6.45/2.81	              </arg>
6.45/2.81	             </funapp>
6.45/2.81	            </arg>
6.45/2.81	           </funapp>
6.45/2.81	          </lhs>
6.45/2.81	          <rhs>
6.45/2.81	           <funapp>
6.45/2.81	            <name>tp2</name>
6.45/2.81	            <arg>
6.45/2.81	             <funapp>
6.45/2.81	              <name>nil</name>
6.45/2.81	             </funapp>
6.45/2.81	            </arg>
6.45/2.81	            <arg>
6.45/2.81	             <var>y</var>
6.45/2.81	            </arg>
6.45/2.81	           </funapp>
6.45/2.81	          </rhs>
6.45/2.81	         </rule>
6.45/2.81	        </conditionalRule>
6.45/2.81	        <rule>
6.45/2.81	         <lhs>
6.45/2.81	          <funapp>
6.45/2.81	           <name>isnoc</name>
6.45/2.81	           <arg>
6.45/2.81	            <funapp>
6.45/2.81	             <name>cons</name>
6.45/2.81	             <arg>
6.45/2.81	              <var>y</var>
6.45/2.81	             </arg>
6.45/2.81	             <arg>
6.45/2.81	              <funapp>
6.45/2.81	               <name>nil</name>
6.45/2.81	              </funapp>
6.45/2.81	             </arg>
6.45/2.81	            </funapp>
6.45/2.81	           </arg>
6.45/2.81	          </funapp>
6.45/2.81	         </lhs>
6.45/2.81	         <rhs>
6.45/2.81	          <funapp>
6.45/2.81	           <name>tp2</name>
6.45/2.81	           <arg>
6.45/2.81	            <funapp>
6.45/2.81	             <name>nil</name>
6.45/2.81	            </funapp>
6.45/2.81	           </arg>
6.45/2.81	           <arg>
6.45/2.81	            <var>y</var>
6.45/2.81	           </arg>
6.45/2.81	          </funapp>
6.45/2.81	         </rhs>
6.45/2.81	        </rule>
6.45/2.81	       </unravelingEntry>
6.45/2.81	       <unravelingEntry>
6.45/2.81	        <conditionalRule>
6.45/2.81	         <rule>
6.45/2.81	          <lhs>
6.45/2.81	           <funapp>
6.45/2.81	            <name>isnoc</name>
6.45/2.81	            <arg>
6.45/2.81	             <funapp>
6.45/2.81	              <name>cons</name>
6.45/2.81	              <arg>
6.45/2.81	               <var>x</var>
6.45/2.81	              </arg>
6.45/2.81	              <arg>
6.45/2.81	               <var>ys</var>
6.45/2.81	              </arg>
6.45/2.81	             </funapp>
6.45/2.81	            </arg>
6.45/2.81	           </funapp>
6.45/2.81	          </lhs>
6.45/2.81	          <rhs>
6.45/2.81	           <funapp>
6.45/2.81	            <name>tp2</name>
6.45/2.81	            <arg>
6.45/2.81	             <funapp>
6.45/2.81	              <name>cons</name>
6.45/2.81	              <arg>
6.45/2.81	               <var>x</var>
6.45/2.81	              </arg>
6.45/2.81	              <arg>
6.45/2.81	               <var>xs</var>
6.45/2.81	              </arg>
6.45/2.81	             </funapp>
6.45/2.81	            </arg>
6.45/2.81	            <arg>
6.45/2.81	             <var>y</var>
6.45/2.81	            </arg>
6.45/2.81	           </funapp>
6.45/2.81	          </rhs>
6.45/2.81	         </rule>
6.45/2.81	         <rule>
6.45/2.81	          <lhs>
6.45/2.81	           <funapp>
6.45/2.81	            <name>isnoc</name>
6.45/2.81	            <arg>
6.45/2.81	             <var>ys</var>
6.45/2.81	            </arg>
6.45/2.81	           </funapp>
6.45/2.81	          </lhs>
6.45/2.81	          <rhs>
6.45/2.81	           <funapp>
6.45/2.81	            <name>tp2</name>
6.45/2.81	            <arg>
6.45/2.81	             <var>xs</var>
6.45/2.81	            </arg>
6.45/2.81	            <arg>
6.45/2.81	             <var>y</var>
6.45/2.81	            </arg>
6.45/2.81	           </funapp>
6.45/2.81	          </rhs>
6.45/2.81	         </rule>
6.45/2.81	        </conditionalRule>
6.45/2.81	        <rule>
6.45/2.81	         <lhs>
6.45/2.81	          <funapp>
6.45/2.81	           <name>isnoc</name>
6.45/2.81	           <arg>
6.45/2.81	            <funapp>
6.45/2.81	             <name>cons</name>
6.45/2.81	             <arg>
6.45/2.81	              <var>x</var>
6.45/2.81	             </arg>
6.45/2.81	             <arg>
6.45/2.81	              <var>ys</var>
6.45/2.81	             </arg>
6.45/2.81	            </funapp>
6.45/2.81	           </arg>
6.45/2.81	          </funapp>
6.45/2.81	         </lhs>
6.45/2.81	         <rhs>
6.45/2.81	          <funapp>
6.45/2.81	           <name>U1</name>
6.45/2.81	           <arg>
6.45/2.81	            <funapp>
6.45/2.81	             <name>isnoc</name>
6.45/2.81	             <arg>
6.45/2.81	              <var>ys</var>
6.45/2.81	             </arg>
6.45/2.81	            </funapp>
6.45/2.81	           </arg>
6.45/2.81	           <arg>
6.45/2.81	            <var>x</var>
6.45/2.81	           </arg>
6.45/2.81	           <arg>
6.45/2.81	            <var>ys</var>
6.45/2.81	           </arg>
6.45/2.81	          </funapp>
6.45/2.81	         </rhs>
6.45/2.81	        </rule>
6.45/2.81	        <rule>
6.45/2.81	         <lhs>
6.45/2.81	          <funapp>
6.45/2.81	           <name>U1</name>
6.45/2.81	           <arg>
6.45/2.81	            <funapp>
6.45/2.81	             <name>tp2</name>
6.45/2.81	             <arg>
6.45/2.81	              <var>xs</var>
6.45/2.81	             </arg>
6.45/2.81	             <arg>
6.45/2.81	              <var>y</var>
6.45/2.81	             </arg>
6.45/2.81	            </funapp>
6.45/2.81	           </arg>
6.45/2.81	           <arg>
6.45/2.81	            <var>x</var>
6.45/2.81	           </arg>
6.45/2.81	           <arg>
6.45/2.81	            <var>ys</var>
6.45/2.81	           </arg>
6.45/2.81	          </funapp>
6.45/2.81	         </lhs>
6.45/2.81	         <rhs>
6.45/2.81	          <funapp>
6.45/2.81	           <name>tp2</name>
6.45/2.81	           <arg>
6.45/2.81	            <funapp>
6.45/2.81	             <name>cons</name>
6.45/2.81	             <arg>
6.45/2.81	              <var>x</var>
6.45/2.81	             </arg>
6.45/2.81	             <arg>
6.45/2.81	              <var>xs</var>
6.45/2.81	             </arg>
6.45/2.81	            </funapp>
6.45/2.81	           </arg>
6.45/2.81	           <arg>
6.45/2.81	            <var>y</var>
6.45/2.81	           </arg>
6.45/2.81	          </funapp>
6.45/2.81	         </rhs>
6.45/2.81	        </rule>
6.45/2.81	       </unravelingEntry>
6.45/2.81	      </unravelingInformation>
6.45/2.81	      <trsTerminationProof>
6.45/2.81	       <ruleRemoval>
6.45/2.81	        <orderingConstraintProof>
6.45/2.81	         <redPair>
6.45/2.81	          <interpretation>
6.45/2.81	           <type>
6.45/2.81	            <polynomial>
6.45/2.81	             <domain>
6.45/2.81	              <matrices>
6.45/2.81	               <dimension>3</dimension>
6.45/2.81	               <strictDimension>1</strictDimension>
6.45/2.81	               <domain>
6.45/2.81	                <naturals/>
6.45/2.81	               </domain>
6.45/2.81	              </matrices>
6.45/2.81	             </domain>
6.45/2.81	             <degree>1</degree>
6.45/2.81	            </polynomial>
6.45/2.81	           </type>
6.45/2.81	           <interpret>
6.45/2.81	            <name>U1</name>
6.45/2.81	            <arity>3</arity>
6.45/2.81	            <polynomial>
6.45/2.81	             <sum>
6.45/2.81	              <polynomial>
6.45/2.81	               <product>
6.45/2.81	                <polynomial>
6.45/2.81	                 <coefficient>
6.45/2.81	                  <matrix>
6.45/2.81	                   <vector>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                   </vector>
6.45/2.81	                   <vector>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                   </vector>
6.45/2.81	                   <vector>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                   </vector>
6.45/2.81	                  </matrix>
6.45/2.81	                 </coefficient>
6.45/2.81	                </polynomial>
6.45/2.81	                <polynomial>
6.45/2.81	                 <variable>1</variable>
6.45/2.81	                </polynomial>
6.45/2.81	               </product>
6.45/2.81	              </polynomial>
6.45/2.81	              <polynomial>
6.45/2.81	               <product>
6.45/2.81	                <polynomial>
6.45/2.81	                 <coefficient>
6.45/2.81	                  <matrix>
6.45/2.81	                   <vector>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                   </vector>
6.45/2.81	                   <vector>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                   </vector>
6.45/2.81	                   <vector>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                   </vector>
6.45/2.81	                  </matrix>
6.45/2.81	                 </coefficient>
6.45/2.81	                </polynomial>
6.45/2.81	                <polynomial>
6.45/2.81	                 <variable>2</variable>
6.45/2.81	                </polynomial>
6.45/2.81	               </product>
6.45/2.81	              </polynomial>
6.45/2.81	              <polynomial>
6.45/2.81	               <product>
6.45/2.81	                <polynomial>
6.45/2.81	                 <coefficient>
6.45/2.81	                  <matrix>
6.45/2.81	                   <vector>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                   </vector>
6.45/2.81	                   <vector>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                   </vector>
6.45/2.81	                   <vector>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                   </vector>
6.45/2.81	                  </matrix>
6.45/2.81	                 </coefficient>
6.45/2.81	                </polynomial>
6.45/2.81	                <polynomial>
6.45/2.81	                 <variable>3</variable>
6.45/2.81	                </polynomial>
6.45/2.81	               </product>
6.45/2.81	              </polynomial>
6.45/2.81	              <polynomial>
6.45/2.81	               <coefficient>
6.45/2.81	                <matrix>
6.45/2.81	                 <vector>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>1</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                 </vector>
6.45/2.81	                 <vector>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                 </vector>
6.45/2.81	                 <vector>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                 </vector>
6.45/2.81	                </matrix>
6.45/2.81	               </coefficient>
6.45/2.81	              </polynomial>
6.45/2.81	             </sum>
6.45/2.81	            </polynomial>
6.45/2.81	           </interpret>
6.45/2.81	           <interpret>
6.45/2.81	            <name>tp2</name>
6.45/2.81	            <arity>2</arity>
6.45/2.81	            <polynomial>
6.45/2.81	             <sum>
6.45/2.81	              <polynomial>
6.45/2.81	               <product>
6.45/2.81	                <polynomial>
6.45/2.81	                 <coefficient>
6.45/2.81	                  <matrix>
6.45/2.81	                   <vector>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                   </vector>
6.45/2.81	                   <vector>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                   </vector>
6.45/2.81	                   <vector>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                   </vector>
6.45/2.81	                  </matrix>
6.45/2.81	                 </coefficient>
6.45/2.81	                </polynomial>
6.45/2.81	                <polynomial>
6.45/2.81	                 <variable>1</variable>
6.45/2.81	                </polynomial>
6.45/2.81	               </product>
6.45/2.81	              </polynomial>
6.45/2.81	              <polynomial>
6.45/2.81	               <product>
6.45/2.81	                <polynomial>
6.45/2.81	                 <coefficient>
6.45/2.81	                  <matrix>
6.45/2.81	                   <vector>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                   </vector>
6.45/2.81	                   <vector>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                   </vector>
6.45/2.81	                   <vector>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                   </vector>
6.45/2.81	                  </matrix>
6.45/2.81	                 </coefficient>
6.45/2.81	                </polynomial>
6.45/2.81	                <polynomial>
6.45/2.81	                 <variable>2</variable>
6.45/2.81	                </polynomial>
6.45/2.81	               </product>
6.45/2.81	              </polynomial>
6.45/2.81	              <polynomial>
6.45/2.81	               <coefficient>
6.45/2.81	                <matrix>
6.45/2.81	                 <vector>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                 </vector>
6.45/2.81	                 <vector>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                 </vector>
6.45/2.81	                 <vector>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                 </vector>
6.45/2.81	                </matrix>
6.45/2.81	               </coefficient>
6.45/2.81	              </polynomial>
6.45/2.81	             </sum>
6.45/2.81	            </polynomial>
6.45/2.81	           </interpret>
6.45/2.81	           <interpret>
6.45/2.81	            <name>isnoc</name>
6.45/2.81	            <arity>1</arity>
6.45/2.81	            <polynomial>
6.45/2.81	             <sum>
6.45/2.81	              <polynomial>
6.45/2.81	               <product>
6.45/2.81	                <polynomial>
6.45/2.81	                 <coefficient>
6.45/2.81	                  <matrix>
6.45/2.81	                   <vector>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                   </vector>
6.45/2.81	                   <vector>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                   </vector>
6.45/2.81	                   <vector>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                   </vector>
6.45/2.81	                  </matrix>
6.45/2.81	                 </coefficient>
6.45/2.81	                </polynomial>
6.45/2.81	                <polynomial>
6.45/2.81	                 <variable>1</variable>
6.45/2.81	                </polynomial>
6.45/2.81	               </product>
6.45/2.81	              </polynomial>
6.45/2.81	              <polynomial>
6.45/2.81	               <coefficient>
6.45/2.81	                <matrix>
6.45/2.81	                 <vector>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>1</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                 </vector>
6.45/2.81	                 <vector>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                 </vector>
6.45/2.81	                 <vector>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                 </vector>
6.45/2.81	                </matrix>
6.45/2.81	               </coefficient>
6.45/2.81	              </polynomial>
6.45/2.81	             </sum>
6.45/2.81	            </polynomial>
6.45/2.81	           </interpret>
6.45/2.81	           <interpret>
6.45/2.81	            <name>cons</name>
6.45/2.81	            <arity>2</arity>
6.45/2.81	            <polynomial>
6.45/2.81	             <sum>
6.45/2.81	              <polynomial>
6.45/2.81	               <product>
6.45/2.81	                <polynomial>
6.45/2.81	                 <coefficient>
6.45/2.81	                  <matrix>
6.45/2.81	                   <vector>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                   </vector>
6.45/2.81	                   <vector>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                   </vector>
6.45/2.81	                   <vector>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                   </vector>
6.45/2.81	                  </matrix>
6.45/2.81	                 </coefficient>
6.45/2.81	                </polynomial>
6.45/2.81	                <polynomial>
6.45/2.81	                 <variable>1</variable>
6.45/2.81	                </polynomial>
6.45/2.81	               </product>
6.45/2.81	              </polynomial>
6.45/2.81	              <polynomial>
6.45/2.81	               <product>
6.45/2.81	                <polynomial>
6.45/2.81	                 <coefficient>
6.45/2.81	                  <matrix>
6.45/2.81	                   <vector>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                   </vector>
6.45/2.81	                   <vector>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                   </vector>
6.45/2.81	                   <vector>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>0</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                    <coefficient>
6.45/2.81	                     <integer>1</integer>
6.45/2.81	                    </coefficient>
6.45/2.81	                   </vector>
6.45/2.81	                  </matrix>
6.45/2.81	                 </coefficient>
6.45/2.81	                </polynomial>
6.45/2.81	                <polynomial>
6.45/2.81	                 <variable>2</variable>
6.45/2.81	                </polynomial>
6.45/2.81	               </product>
6.45/2.81	              </polynomial>
6.45/2.81	              <polynomial>
6.45/2.81	               <coefficient>
6.45/2.81	                <matrix>
6.45/2.81	                 <vector>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>1</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                 </vector>
6.45/2.81	                 <vector>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                 </vector>
6.45/2.81	                 <vector>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                 </vector>
6.45/2.81	                </matrix>
6.45/2.81	               </coefficient>
6.45/2.81	              </polynomial>
6.45/2.81	             </sum>
6.45/2.81	            </polynomial>
6.45/2.81	           </interpret>
6.45/2.81	           <interpret>
6.45/2.81	            <name>nil</name>
6.45/2.81	            <arity>0</arity>
6.45/2.81	            <polynomial>
6.45/2.81	             <sum>
6.45/2.81	              <polynomial>
6.45/2.81	               <coefficient>
6.45/2.81	                <matrix>
6.45/2.81	                 <vector>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>1</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                 </vector>
6.45/2.81	                 <vector>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                 </vector>
6.45/2.81	                 <vector>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                  <coefficient>
6.45/2.81	                   <integer>0</integer>
6.45/2.81	                  </coefficient>
6.45/2.81	                 </vector>
6.45/2.81	                </matrix>
6.45/2.81	               </coefficient>
6.45/2.81	              </polynomial>
6.45/2.81	             </sum>
6.45/2.81	            </polynomial>
6.45/2.81	           </interpret>
6.45/2.81	          </interpretation>
6.45/2.81	         </redPair>
6.45/2.81	        </orderingConstraintProof>
6.45/2.81	        <trs>
6.45/2.81	         <rules>
6.45/2.81	          <rule>
6.45/2.81	           <lhs>
6.45/2.81	            <funapp>
6.45/2.81	             <name>U1</name>
6.45/2.81	             <arg>
6.45/2.81	              <funapp>
6.45/2.81	               <name>tp2</name>
6.45/2.81	               <arg>
6.45/2.81	                <var>xs</var>
6.45/2.81	               </arg>
6.45/2.81	               <arg>
6.45/2.81	                <var>y</var>
6.45/2.81	               </arg>
6.45/2.81	              </funapp>
6.45/2.81	             </arg>
6.45/2.81	             <arg>
6.45/2.81	              <var>x</var>
6.45/2.81	             </arg>
6.45/2.81	             <arg>
6.45/2.81	              <var>ys</var>
6.45/2.81	             </arg>
6.45/2.81	            </funapp>
6.45/2.81	           </lhs>
6.45/2.81	           <rhs>
6.45/2.81	            <funapp>
6.45/2.81	             <name>tp2</name>
6.45/2.81	             <arg>
6.45/2.81	              <funapp>
6.45/2.81	               <name>cons</name>
6.45/2.81	               <arg>
6.45/2.81	                <var>x</var>
6.45/2.81	               </arg>
6.45/2.81	               <arg>
6.45/2.81	                <var>xs</var>
6.45/2.81	               </arg>
6.45/2.81	              </funapp>
6.45/2.81	             </arg>
6.45/2.81	             <arg>
6.45/2.81	              <var>y</var>
6.45/2.81	             </arg>
6.45/2.81	            </funapp>
6.45/2.81	           </rhs>
6.45/2.81	          </rule>
6.45/2.81	         </rules>
6.45/2.81	        </trs>
6.45/2.81	        <trsTerminationProof>
6.45/2.81	         <ruleRemoval>
6.45/2.81	          <orderingConstraintProof>
6.45/2.81	           <redPair>
6.45/2.81	            <knuthBendixOrder>
6.45/2.81	             <w0>1</w0>
6.45/2.81	             <precedenceWeight>
6.45/2.81	              <precedenceWeightEntry>
6.45/2.81	               <name>U1</name>
6.45/2.81	               <arity>3</arity>
6.45/2.81	               <precedence>1</precedence>
6.45/2.81	               <weight>0</weight>
6.45/2.81	              </precedenceWeightEntry>
6.45/2.81	              <precedenceWeightEntry>
6.45/2.81	               <name>tp2</name>
6.45/2.81	               <arity>2</arity>
6.45/2.81	               <precedence>0</precedence>
6.45/2.81	               <weight>0</weight>
6.45/2.81	              </precedenceWeightEntry>
6.45/2.81	              <precedenceWeightEntry>
6.45/2.81	               <name>cons</name>
6.45/2.81	               <arity>2</arity>
6.45/2.81	               <precedence>0</precedence>
6.45/2.81	               <weight>1</weight>
6.45/2.81	              </precedenceWeightEntry>
6.45/2.81	             </precedenceWeight>
6.45/2.81	            </knuthBendixOrder>
6.45/2.81	           </redPair>
6.45/2.81	          </orderingConstraintProof>
6.45/2.81	          <trs>
6.45/2.81	           <rules/>
6.45/2.81	          </trs>
6.45/2.81	          <trsTerminationProof>
6.45/2.81	           <rIsEmpty/>
6.45/2.81	          </trsTerminationProof>
6.45/2.81	         </ruleRemoval>
6.45/2.81	        </trsTerminationProof>
6.45/2.81	       </ruleRemoval>
6.45/2.81	      </trsTerminationProof>
6.45/2.81	     </unraveling>
6.45/2.81	    </quasiReductiveProof>
6.45/2.81	    <contextJoinableCCPs/>
6.45/2.81	    <infeasibleConditions>
6.45/2.81	     <infeasibleCondition>
6.45/2.81	      <rules>
6.45/2.81	       <rule>
6.45/2.81	        <lhs>
6.45/2.81	         <funapp>
6.45/2.81	          <name>isnoc</name>
6.45/2.81	          <arg>
6.45/2.81	           <funapp>
6.45/2.81	            <name>nil</name>
6.45/2.81	           </funapp>
6.45/2.81	          </arg>
6.45/2.81	         </funapp>
6.45/2.81	        </lhs>
6.45/2.81	        <rhs>
6.45/2.81	         <funapp>
6.45/2.81	          <name>tp2</name>
6.45/2.81	          <arg>
6.45/2.81	           <var>x'</var>
6.45/2.81	          </arg>
6.45/2.81	          <arg>
6.45/2.81	           <var>y'</var>
6.45/2.81	          </arg>
6.45/2.81	         </funapp>
6.45/2.81	        </rhs>
6.45/2.81	       </rule>
6.45/2.81	      </rules>
6.45/2.81	      <infeasibilityProof>
6.45/2.81	       <infeasibleEquation>
6.45/2.81	        <rule>
6.45/2.81	         <lhs>
6.45/2.81	          <funapp>
6.45/2.81	           <name>isnoc</name>
6.45/2.81	           <arg>
6.45/2.81	            <funapp>
6.45/2.81	             <name>nil</name>
6.45/2.81	            </funapp>
6.45/2.81	           </arg>
6.45/2.81	          </funapp>
6.45/2.81	         </lhs>
6.45/2.81	         <rhs>
6.45/2.81	          <funapp>
6.45/2.81	           <name>tp2</name>
6.45/2.81	           <arg>
6.45/2.81	            <var>x'</var>
6.45/2.81	           </arg>
6.45/2.81	           <arg>
6.45/2.81	            <var>y'</var>
6.45/2.81	           </arg>
6.45/2.81	          </funapp>
6.45/2.81	         </rhs>
6.45/2.81	        </rule>
6.45/2.81	        <nonreachabilityProof>
6.45/2.81	         <nonreachableTcap/>
6.45/2.81	        </nonreachabilityProof>
6.45/2.81	       </infeasibleEquation>
6.45/2.81	      </infeasibilityProof>
6.45/2.81	     </infeasibleCondition>
6.45/2.81	     <infeasibleCondition>
6.45/2.81	      <rules>
6.45/2.81	       <rule>
6.45/2.81	        <lhs>
6.45/2.81	         <funapp>
6.45/2.81	          <name>isnoc</name>
6.45/2.81	          <arg>
6.45/2.81	           <funapp>
6.45/2.81	            <name>nil</name>
6.45/2.81	           </funapp>
6.45/2.81	          </arg>
6.45/2.81	         </funapp>
6.45/2.81	        </lhs>
6.45/2.81	        <rhs>
6.45/2.81	         <funapp>
6.45/2.81	          <name>tp2</name>
6.45/2.81	          <arg>
6.45/2.81	           <var>x'</var>
6.45/2.81	          </arg>
6.45/2.81	          <arg>
6.45/2.81	           <var>y'</var>
6.45/2.81	          </arg>
6.45/2.81	         </funapp>
6.45/2.81	        </rhs>
6.45/2.81	       </rule>
6.45/2.81	      </rules>
6.45/2.81	      <infeasibilityProof>
6.45/2.81	       <infeasibleEquation>
6.45/2.81	        <rule>
6.45/2.81	         <lhs>
6.45/2.81	          <funapp>
6.45/2.81	           <name>isnoc</name>
6.45/2.81	           <arg>
6.45/2.81	            <funapp>
6.45/2.81	             <name>nil</name>
6.45/2.81	            </funapp>
6.45/2.81	           </arg>
6.45/2.81	          </funapp>
6.45/2.81	         </lhs>
6.45/2.81	         <rhs>
6.45/2.81	          <funapp>
6.45/2.81	           <name>tp2</name>
6.45/2.81	           <arg>
6.45/2.81	            <var>x'</var>
6.45/2.81	           </arg>
6.45/2.81	           <arg>
6.45/2.81	            <var>y'</var>
6.45/2.81	           </arg>
6.45/2.81	          </funapp>
6.45/2.81	         </rhs>
6.45/2.81	        </rule>
6.45/2.81	        <nonreachabilityProof>
6.45/2.81	         <nonreachableTcap/>
6.45/2.81	        </nonreachabilityProof>
6.45/2.81	       </infeasibleEquation>
6.45/2.81	      </infeasibilityProof>
6.45/2.81	     </infeasibleCondition>
6.45/2.81	    </infeasibleConditions>
6.45/2.81	    <unfeasibleCCPs/>
6.45/2.81	   </al94>
6.45/2.81	  </conditionalCrProof>
6.45/2.81	 </proof>
6.45/2.81	 <origin>
6.45/2.81	  <proofOrigin>
6.45/2.81	   <tool>
6.45/2.81	    <name>ConCon</name>
6.45/2.81	    <version>concon 1.4.0.0</version>
6.45/2.81	    <strategy>
6.45/2.81	     concon -s --cert --conf A --no-inlining theBenchmark.trs 58
6.45/2.81	    </strategy>
6.45/2.81	   </tool>
6.45/2.81	  </proofOrigin>
6.45/2.81	 </origin>
6.45/2.81	</certificationProblem>
6.45/2.81	EOF