3.99/2.17	YES
3.99/2.17	<?xml version="1.0"?><?xml-stylesheet type="text/xsl" href="cpfHTML.xsl"?>
3.99/2.17	<certificationProblem>
3.99/2.17	 <input>
3.99/2.17	  <ctrsInput>
3.99/2.17	   <conditionalRules>
3.99/2.17	    <conditionalRule>
3.99/2.17	     <rule>
3.99/2.17	      <lhs>
3.99/2.17	       <funapp>
3.99/2.17	        <name>not</name>
3.99/2.17	        <arg>
3.99/2.17	         <var>x</var>
3.99/2.17	        </arg>
3.99/2.17	       </funapp>
3.99/2.17	      </lhs>
3.99/2.17	      <rhs>
3.99/2.17	       <funapp>
3.99/2.17	        <name>false</name>
3.99/2.17	       </funapp>
3.99/2.17	      </rhs>
3.99/2.17	     </rule>
3.99/2.17	     <rule>
3.99/2.17	      <lhs>
3.99/2.17	       <var>x</var>
3.99/2.17	      </lhs>
3.99/2.17	      <rhs>
3.99/2.17	       <funapp>
3.99/2.17	        <name>true</name>
3.99/2.17	       </funapp>
3.99/2.17	      </rhs>
3.99/2.17	     </rule>
3.99/2.17	    </conditionalRule>
3.99/2.17	    <conditionalRule>
3.99/2.17	     <rule>
3.99/2.17	      <lhs>
3.99/2.17	       <funapp>
3.99/2.17	        <name>not</name>
3.99/2.17	        <arg>
3.99/2.17	         <var>x</var>
3.99/2.17	        </arg>
3.99/2.17	       </funapp>
3.99/2.17	      </lhs>
3.99/2.17	      <rhs>
3.99/2.17	       <funapp>
3.99/2.17	        <name>true</name>
3.99/2.17	       </funapp>
3.99/2.17	      </rhs>
3.99/2.17	     </rule>
3.99/2.17	     <rule>
3.99/2.17	      <lhs>
3.99/2.17	       <var>x</var>
3.99/2.17	      </lhs>
3.99/2.17	      <rhs>
3.99/2.17	       <funapp>
3.99/2.17	        <name>false</name>
3.99/2.17	       </funapp>
3.99/2.17	      </rhs>
3.99/2.17	     </rule>
3.99/2.17	    </conditionalRule>
3.99/2.17	   </conditionalRules>
3.99/2.17	  </ctrsInput>
3.99/2.17	 </input>
3.99/2.17	 <cpfVersion>2.4</cpfVersion>
3.99/2.17	 <proof>
3.99/2.17	  <conditionalCrProof>
3.99/2.17	   <al94>
3.99/2.17	    <quasiReductiveProof>
3.99/2.17	     <unraveling>
3.99/2.17	      <unravelingInformation>
3.99/2.17	       <unravelingEntry>
3.99/2.17	        <conditionalRule>
3.99/2.17	         <rule>
3.99/2.17	          <lhs>
3.99/2.17	           <funapp>
3.99/2.17	            <name>not</name>
3.99/2.17	            <arg>
3.99/2.17	             <var>x</var>
3.99/2.17	            </arg>
3.99/2.17	           </funapp>
3.99/2.17	          </lhs>
3.99/2.17	          <rhs>
3.99/2.17	           <funapp>
3.99/2.17	            <name>false</name>
3.99/2.17	           </funapp>
3.99/2.17	          </rhs>
3.99/2.17	         </rule>
3.99/2.17	         <rule>
3.99/2.17	          <lhs>
3.99/2.17	           <var>x</var>
3.99/2.17	          </lhs>
3.99/2.17	          <rhs>
3.99/2.17	           <funapp>
3.99/2.17	            <name>true</name>
3.99/2.17	           </funapp>
3.99/2.17	          </rhs>
3.99/2.17	         </rule>
3.99/2.17	        </conditionalRule>
3.99/2.17	        <rule>
3.99/2.17	         <lhs>
3.99/2.17	          <funapp>
3.99/2.17	           <name>not</name>
3.99/2.17	           <arg>
3.99/2.17	            <var>x</var>
3.99/2.17	           </arg>
3.99/2.17	          </funapp>
3.99/2.17	         </lhs>
3.99/2.17	         <rhs>
3.99/2.17	          <funapp>
3.99/2.17	           <name>U1</name>
3.99/2.17	           <arg>
3.99/2.17	            <var>x</var>
3.99/2.17	           </arg>
3.99/2.17	           <arg>
3.99/2.17	            <var>x</var>
3.99/2.17	           </arg>
3.99/2.17	          </funapp>
3.99/2.17	         </rhs>
3.99/2.17	        </rule>
3.99/2.17	        <rule>
3.99/2.17	         <lhs>
3.99/2.17	          <funapp>
3.99/2.17	           <name>U1</name>
3.99/2.17	           <arg>
3.99/2.17	            <funapp>
3.99/2.17	             <name>true</name>
3.99/2.17	            </funapp>
3.99/2.17	           </arg>
3.99/2.17	           <arg>
3.99/2.17	            <var>x</var>
3.99/2.17	           </arg>
3.99/2.17	          </funapp>
3.99/2.17	         </lhs>
3.99/2.17	         <rhs>
3.99/2.17	          <funapp>
3.99/2.17	           <name>false</name>
3.99/2.17	          </funapp>
3.99/2.17	         </rhs>
3.99/2.17	        </rule>
3.99/2.17	       </unravelingEntry>
3.99/2.17	       <unravelingEntry>
3.99/2.17	        <conditionalRule>
3.99/2.17	         <rule>
3.99/2.17	          <lhs>
3.99/2.17	           <funapp>
3.99/2.17	            <name>not</name>
3.99/2.17	            <arg>
3.99/2.17	             <var>x</var>
3.99/2.17	            </arg>
3.99/2.17	           </funapp>
3.99/2.17	          </lhs>
3.99/2.17	          <rhs>
3.99/2.17	           <funapp>
3.99/2.17	            <name>true</name>
3.99/2.17	           </funapp>
3.99/2.17	          </rhs>
3.99/2.17	         </rule>
3.99/2.17	         <rule>
3.99/2.17	          <lhs>
3.99/2.17	           <var>x</var>
3.99/2.17	          </lhs>
3.99/2.17	          <rhs>
3.99/2.17	           <funapp>
3.99/2.17	            <name>false</name>
3.99/2.17	           </funapp>
3.99/2.17	          </rhs>
3.99/2.17	         </rule>
3.99/2.17	        </conditionalRule>
3.99/2.17	        <rule>
3.99/2.17	         <lhs>
3.99/2.17	          <funapp>
3.99/2.17	           <name>not</name>
3.99/2.17	           <arg>
3.99/2.17	            <var>x</var>
3.99/2.17	           </arg>
3.99/2.17	          </funapp>
3.99/2.17	         </lhs>
3.99/2.17	         <rhs>
3.99/2.17	          <funapp>
3.99/2.17	           <name>U1</name>
3.99/2.17	           <arg>
3.99/2.17	            <var>x</var>
3.99/2.17	           </arg>
3.99/2.17	           <arg>
3.99/2.17	            <var>x</var>
3.99/2.17	           </arg>
3.99/2.17	          </funapp>
3.99/2.17	         </rhs>
3.99/2.17	        </rule>
3.99/2.17	        <rule>
3.99/2.17	         <lhs>
3.99/2.17	          <funapp>
3.99/2.17	           <name>U1</name>
3.99/2.17	           <arg>
3.99/2.17	            <funapp>
3.99/2.17	             <name>false</name>
3.99/2.17	            </funapp>
3.99/2.17	           </arg>
3.99/2.17	           <arg>
3.99/2.17	            <var>x</var>
3.99/2.17	           </arg>
3.99/2.17	          </funapp>
3.99/2.17	         </lhs>
3.99/2.17	         <rhs>
3.99/2.17	          <funapp>
3.99/2.17	           <name>true</name>
3.99/2.17	          </funapp>
3.99/2.17	         </rhs>
3.99/2.17	        </rule>
3.99/2.17	       </unravelingEntry>
3.99/2.17	      </unravelingInformation>
3.99/2.17	      <trsTerminationProof>
3.99/2.17	       <ruleRemoval>
3.99/2.17	        <orderingConstraintProof>
3.99/2.17	         <redPair>
3.99/2.17	          <interpretation>
3.99/2.17	           <type>
3.99/2.17	            <polynomial>
3.99/2.17	             <domain>
3.99/2.17	              <naturals/>
3.99/2.17	             </domain>
3.99/2.17	             <degree>1</degree>
3.99/2.17	            </polynomial>
3.99/2.17	           </type>
3.99/2.17	           <interpret>
3.99/2.17	            <name>false</name>
3.99/2.17	            <arity>0</arity>
3.99/2.17	            <polynomial>
3.99/2.17	             <sum>
3.99/2.17	              <polynomial>
3.99/2.17	               <coefficient>
3.99/2.17	                <integer>0</integer>
3.99/2.17	               </coefficient>
3.99/2.17	              </polynomial>
3.99/2.17	             </sum>
3.99/2.17	            </polynomial>
3.99/2.17	           </interpret>
3.99/2.17	           <interpret>
3.99/2.17	            <name>true</name>
3.99/2.17	            <arity>0</arity>
3.99/2.17	            <polynomial>
3.99/2.17	             <sum>
3.99/2.17	              <polynomial>
3.99/2.17	               <coefficient>
3.99/2.17	                <integer>15</integer>
3.99/2.17	               </coefficient>
3.99/2.17	              </polynomial>
3.99/2.17	             </sum>
3.99/2.17	            </polynomial>
3.99/2.17	           </interpret>
3.99/2.17	           <interpret>
3.99/2.17	            <name>U1</name>
3.99/2.17	            <arity>2</arity>
3.99/2.17	            <polynomial>
3.99/2.17	             <sum>
3.99/2.17	              <polynomial>
3.99/2.17	               <product>
3.99/2.17	                <polynomial>
3.99/2.17	                 <coefficient>
3.99/2.17	                  <integer>9</integer>
3.99/2.17	                 </coefficient>
3.99/2.17	                </polynomial>
3.99/2.17	                <polynomial>
3.99/2.17	                 <variable>1</variable>
3.99/2.17	                </polynomial>
3.99/2.17	               </product>
3.99/2.17	              </polynomial>
3.99/2.17	              <polynomial>
3.99/2.17	               <product>
3.99/2.17	                <polynomial>
3.99/2.17	                 <coefficient>
3.99/2.17	                  <integer>2</integer>
3.99/2.17	                 </coefficient>
3.99/2.17	                </polynomial>
3.99/2.17	                <polynomial>
3.99/2.17	                 <variable>2</variable>
3.99/2.17	                </polynomial>
3.99/2.17	               </product>
3.99/2.17	              </polynomial>
3.99/2.17	              <polynomial>
3.99/2.17	               <coefficient>
3.99/2.17	                <integer>15</integer>
3.99/2.17	               </coefficient>
3.99/2.17	              </polynomial>
3.99/2.17	             </sum>
3.99/2.17	            </polynomial>
3.99/2.17	           </interpret>
3.99/2.17	           <interpret>
3.99/2.17	            <name>not</name>
3.99/2.17	            <arity>1</arity>
3.99/2.17	            <polynomial>
3.99/2.17	             <sum>
3.99/2.17	              <polynomial>
3.99/2.17	               <product>
3.99/2.17	                <polynomial>
3.99/2.17	                 <coefficient>
3.99/2.17	                  <integer>11</integer>
3.99/2.17	                 </coefficient>
3.99/2.17	                </polynomial>
3.99/2.17	                <polynomial>
3.99/2.17	                 <variable>1</variable>
3.99/2.17	                </polynomial>
3.99/2.17	               </product>
3.99/2.17	              </polynomial>
3.99/2.17	              <polynomial>
3.99/2.17	               <coefficient>
3.99/2.17	                <integer>16</integer>
3.99/2.17	               </coefficient>
3.99/2.17	              </polynomial>
3.99/2.17	             </sum>
3.99/2.17	            </polynomial>
3.99/2.17	           </interpret>
3.99/2.17	          </interpretation>
3.99/2.17	         </redPair>
3.99/2.17	        </orderingConstraintProof>
3.99/2.17	        <trs>
3.99/2.17	         <rules>
3.99/2.17	          <rule>
3.99/2.17	           <lhs>
3.99/2.17	            <funapp>
3.99/2.17	             <name>U1</name>
3.99/2.17	             <arg>
3.99/2.17	              <funapp>
3.99/2.17	               <name>false</name>
3.99/2.17	              </funapp>
3.99/2.17	             </arg>
3.99/2.17	             <arg>
3.99/2.17	              <var>x</var>
3.99/2.17	             </arg>
3.99/2.17	            </funapp>
3.99/2.17	           </lhs>
3.99/2.17	           <rhs>
3.99/2.17	            <funapp>
3.99/2.17	             <name>true</name>
3.99/2.17	            </funapp>
3.99/2.17	           </rhs>
3.99/2.17	          </rule>
3.99/2.17	         </rules>
3.99/2.17	        </trs>
3.99/2.17	        <trsTerminationProof>
3.99/2.17	         <ruleRemoval>
3.99/2.17	          <orderingConstraintProof>
3.99/2.17	           <redPair>
3.99/2.17	            <knuthBendixOrder>
3.99/2.17	             <w0>1</w0>
3.99/2.17	             <precedenceWeight>
3.99/2.17	              <precedenceWeightEntry>
3.99/2.17	               <name>false</name>
3.99/2.17	               <arity>0</arity>
3.99/2.17	               <precedence>0</precedence>
3.99/2.17	               <weight>1</weight>
3.99/2.17	              </precedenceWeightEntry>
3.99/2.17	              <precedenceWeightEntry>
3.99/2.17	               <name>true</name>
3.99/2.17	               <arity>0</arity>
3.99/2.17	               <precedence>0</precedence>
3.99/2.17	               <weight>4</weight>
3.99/2.17	              </precedenceWeightEntry>
3.99/2.17	              <precedenceWeightEntry>
3.99/2.17	               <name>U1</name>
3.99/2.17	               <arity>2</arity>
3.99/2.17	               <precedence>1</precedence>
3.99/2.17	               <weight>2</weight>
3.99/2.17	              </precedenceWeightEntry>
3.99/2.17	             </precedenceWeight>
3.99/2.17	            </knuthBendixOrder>
3.99/2.17	           </redPair>
3.99/2.17	          </orderingConstraintProof>
3.99/2.17	          <trs>
3.99/2.17	           <rules/>
3.99/2.17	          </trs>
3.99/2.17	          <trsTerminationProof>
3.99/2.17	           <rIsEmpty/>
3.99/2.17	          </trsTerminationProof>
3.99/2.17	         </ruleRemoval>
3.99/2.17	        </trsTerminationProof>
3.99/2.17	       </ruleRemoval>
3.99/2.17	      </trsTerminationProof>
3.99/2.17	     </unraveling>
3.99/2.17	    </quasiReductiveProof>
3.99/2.17	    <contextJoinableCCPs/>
3.99/2.17	    <infeasibleConditions/>
3.99/2.17	    <unfeasibleCCPs>
3.99/2.17	     <unfeasibleCCP>
3.99/2.17	      <substitution>
3.99/2.17	       <substEntry>
3.99/2.17	        <var>y</var>
3.99/2.17	        <var>z</var>
3.99/2.17	       </substEntry>
3.99/2.17	      </substitution>
3.99/2.17	      <unfeasibilityProof>
3.99/2.17	       <terms>
3.99/2.17	        <funapp>
3.99/2.17	         <name>?1</name>
3.99/2.17	        </funapp>
3.99/2.17	        <funapp>
3.99/2.17	         <name>false</name>
3.99/2.17	        </funapp>
3.99/2.17	        <funapp>
3.99/2.17	         <name>true</name>
3.99/2.17	        </funapp>
3.99/2.17	       </terms>
3.99/2.17	       <conditionalRewritingSequence>
3.99/2.17	        <conditionalRewriteStep>
3.99/2.17	         <conditionalRule>
3.99/2.17	          <rule>
3.99/2.17	           <lhs>
3.99/2.17	            <funapp>
3.99/2.17	             <name>?1</name>
3.99/2.17	            </funapp>
3.99/2.17	           </lhs>
3.99/2.17	           <rhs>
3.99/2.17	            <funapp>
3.99/2.17	             <name>false</name>
3.99/2.17	            </funapp>
3.99/2.17	           </rhs>
3.99/2.17	          </rule>
3.99/2.17	         </conditionalRule>
3.99/2.17	         <positionInTerm></positionInTerm>
3.99/2.17	         <substitution> </substitution>
3.99/2.17	         <source>
3.99/2.17	          <funapp>
3.99/2.17	           <name>?1</name>
3.99/2.17	          </funapp>
3.99/2.17	         </source>
3.99/2.17	         <target>
3.99/2.17	          <funapp>
3.99/2.17	           <name>false</name>
3.99/2.17	          </funapp>
3.99/2.17	         </target>
3.99/2.17	         <conditions> </conditions>
3.99/2.17	        </conditionalRewriteStep>
3.99/2.17	       </conditionalRewritingSequence>
3.99/2.17	       <conditionalRewritingSequence>
3.99/2.17	        <conditionalRewriteStep>
3.99/2.17	         <conditionalRule>
3.99/2.17	          <rule>
3.99/2.17	           <lhs>
3.99/2.17	            <funapp>
3.99/2.17	             <name>?1</name>
3.99/2.17	            </funapp>
3.99/2.17	           </lhs>
3.99/2.17	           <rhs>
3.99/2.17	            <funapp>
3.99/2.17	             <name>true</name>
3.99/2.17	            </funapp>
3.99/2.17	           </rhs>
3.99/2.17	          </rule>
3.99/2.17	         </conditionalRule>
3.99/2.17	         <positionInTerm></positionInTerm>
3.99/2.17	         <substitution> </substitution>
3.99/2.17	         <source>
3.99/2.17	          <funapp>
3.99/2.17	           <name>?1</name>
3.99/2.17	          </funapp>
3.99/2.17	         </source>
3.99/2.17	         <target>
3.99/2.17	          <funapp>
3.99/2.17	           <name>true</name>
3.99/2.17	          </funapp>
3.99/2.17	         </target>
3.99/2.17	         <conditions> </conditions>
3.99/2.17	        </conditionalRewriteStep>
3.99/2.17	       </conditionalRewritingSequence>
3.99/2.17	       <rules>
3.99/2.17	        <conditionalRule>
3.99/2.17	         <rule>
3.99/2.17	          <lhs>
3.99/2.17	           <funapp>
3.99/2.17	            <name>not</name>
3.99/2.17	            <arg>
3.99/2.17	             <var>y</var>
3.99/2.17	            </arg>
3.99/2.17	           </funapp>
3.99/2.17	          </lhs>
3.99/2.17	          <rhs>
3.99/2.17	           <funapp>
3.99/2.17	            <name>true</name>
3.99/2.17	           </funapp>
3.99/2.17	          </rhs>
3.99/2.17	         </rule>
3.99/2.17	         <rule>
3.99/2.17	          <lhs>
3.99/2.17	           <var>y</var>
3.99/2.17	          </lhs>
3.99/2.17	          <rhs>
3.99/2.17	           <funapp>
3.99/2.17	            <name>false</name>
3.99/2.17	           </funapp>
3.99/2.17	          </rhs>
3.99/2.17	         </rule>
3.99/2.17	        </conditionalRule>
3.99/2.17	        <conditionalRule>
3.99/2.17	         <rule>
3.99/2.17	          <lhs>
3.99/2.17	           <funapp>
3.99/2.17	            <name>not</name>
3.99/2.17	            <arg>
3.99/2.17	             <var>z</var>
3.99/2.17	            </arg>
3.99/2.17	           </funapp>
3.99/2.17	          </lhs>
3.99/2.17	          <rhs>
3.99/2.17	           <funapp>
3.99/2.17	            <name>false</name>
3.99/2.17	           </funapp>
3.99/2.17	          </rhs>
3.99/2.17	         </rule>
3.99/2.17	         <rule>
3.99/2.17	          <lhs>
3.99/2.17	           <var>z</var>
3.99/2.17	          </lhs>
3.99/2.17	          <rhs>
3.99/2.17	           <funapp>
3.99/2.17	            <name>true</name>
3.99/2.17	           </funapp>
3.99/2.17	          </rhs>
3.99/2.17	         </rule>
3.99/2.17	        </conditionalRule>
3.99/2.17	       </rules>
3.99/2.17	       <constMap>
3.99/2.17	        <entry>
3.99/2.17	         <symbol>
3.99/2.17	          <name>?1</name>
3.99/2.17	         </symbol>
3.99/2.17	         <const>z</const>
3.99/2.17	        </entry>
3.99/2.17	       </constMap>
3.99/2.17	      </unfeasibilityProof>
3.99/2.17	     </unfeasibleCCP>
3.99/2.17	     <unfeasibleCCP>
3.99/2.17	      <substitution>
3.99/2.17	       <substEntry>
3.99/2.17	        <var>y</var>
3.99/2.17	        <var>z</var>
3.99/2.17	       </substEntry>
3.99/2.17	      </substitution>
3.99/2.17	      <unfeasibilityProof>
3.99/2.17	       <terms>
3.99/2.17	        <funapp>
3.99/2.17	         <name>?1</name>
3.99/2.17	        </funapp>
3.99/2.17	        <funapp>
3.99/2.17	         <name>true</name>
3.99/2.17	        </funapp>
3.99/2.17	        <funapp>
3.99/2.17	         <name>false</name>
3.99/2.17	        </funapp>
3.99/2.17	       </terms>
3.99/2.17	       <conditionalRewritingSequence>
3.99/2.17	        <conditionalRewriteStep>
3.99/2.17	         <conditionalRule>
3.99/2.17	          <rule>
3.99/2.17	           <lhs>
3.99/2.17	            <funapp>
3.99/2.17	             <name>?1</name>
3.99/2.17	            </funapp>
3.99/2.17	           </lhs>
3.99/2.17	           <rhs>
3.99/2.17	            <funapp>
3.99/2.17	             <name>true</name>
3.99/2.17	            </funapp>
3.99/2.17	           </rhs>
3.99/2.17	          </rule>
3.99/2.17	         </conditionalRule>
3.99/2.17	         <positionInTerm></positionInTerm>
3.99/2.17	         <substitution> </substitution>
3.99/2.17	         <source>
3.99/2.17	          <funapp>
3.99/2.17	           <name>?1</name>
3.99/2.17	          </funapp>
3.99/2.17	         </source>
3.99/2.17	         <target>
3.99/2.17	          <funapp>
3.99/2.17	           <name>true</name>
3.99/2.17	          </funapp>
3.99/2.17	         </target>
3.99/2.17	         <conditions> </conditions>
3.99/2.17	        </conditionalRewriteStep>
3.99/2.17	       </conditionalRewritingSequence>
3.99/2.17	       <conditionalRewritingSequence>
3.99/2.17	        <conditionalRewriteStep>
3.99/2.17	         <conditionalRule>
3.99/2.17	          <rule>
3.99/2.17	           <lhs>
3.99/2.17	            <funapp>
3.99/2.17	             <name>?1</name>
3.99/2.17	            </funapp>
3.99/2.17	           </lhs>
3.99/2.17	           <rhs>
3.99/2.17	            <funapp>
3.99/2.17	             <name>false</name>
3.99/2.17	            </funapp>
3.99/2.17	           </rhs>
3.99/2.17	          </rule>
3.99/2.17	         </conditionalRule>
3.99/2.17	         <positionInTerm></positionInTerm>
3.99/2.17	         <substitution> </substitution>
3.99/2.17	         <source>
3.99/2.17	          <funapp>
3.99/2.17	           <name>?1</name>
3.99/2.17	          </funapp>
3.99/2.17	         </source>
3.99/2.17	         <target>
3.99/2.17	          <funapp>
3.99/2.17	           <name>false</name>
3.99/2.17	          </funapp>
3.99/2.17	         </target>
3.99/2.17	         <conditions> </conditions>
3.99/2.17	        </conditionalRewriteStep>
3.99/2.17	       </conditionalRewritingSequence>
3.99/2.17	       <rules>
3.99/2.17	        <conditionalRule>
3.99/2.17	         <rule>
3.99/2.17	          <lhs>
3.99/2.17	           <funapp>
3.99/2.17	            <name>not</name>
3.99/2.17	            <arg>
3.99/2.17	             <var>y</var>
3.99/2.17	            </arg>
3.99/2.17	           </funapp>
3.99/2.17	          </lhs>
3.99/2.17	          <rhs>
3.99/2.17	           <funapp>
3.99/2.17	            <name>false</name>
3.99/2.17	           </funapp>
3.99/2.17	          </rhs>
3.99/2.17	         </rule>
3.99/2.17	         <rule>
3.99/2.17	          <lhs>
3.99/2.17	           <var>y</var>
3.99/2.17	          </lhs>
3.99/2.17	          <rhs>
3.99/2.17	           <funapp>
3.99/2.17	            <name>true</name>
3.99/2.17	           </funapp>
3.99/2.17	          </rhs>
3.99/2.17	         </rule>
3.99/2.17	        </conditionalRule>
3.99/2.17	        <conditionalRule>
3.99/2.17	         <rule>
3.99/2.17	          <lhs>
3.99/2.17	           <funapp>
3.99/2.17	            <name>not</name>
3.99/2.17	            <arg>
3.99/2.17	             <var>z</var>
3.99/2.17	            </arg>
3.99/2.17	           </funapp>
3.99/2.17	          </lhs>
3.99/2.17	          <rhs>
3.99/2.17	           <funapp>
3.99/2.17	            <name>true</name>
3.99/2.17	           </funapp>
3.99/2.17	          </rhs>
3.99/2.17	         </rule>
3.99/2.17	         <rule>
3.99/2.17	          <lhs>
3.99/2.17	           <var>z</var>
3.99/2.17	          </lhs>
3.99/2.17	          <rhs>
3.99/2.17	           <funapp>
3.99/2.17	            <name>false</name>
3.99/2.17	           </funapp>
3.99/2.17	          </rhs>
3.99/2.17	         </rule>
3.99/2.17	        </conditionalRule>
3.99/2.17	       </rules>
3.99/2.17	       <constMap>
3.99/2.17	        <entry>
3.99/2.17	         <symbol>
3.99/2.17	          <name>?1</name>
3.99/2.17	         </symbol>
3.99/2.17	         <const>z</const>
3.99/2.17	        </entry>
3.99/2.17	       </constMap>
3.99/2.17	      </unfeasibilityProof>
3.99/2.17	     </unfeasibleCCP>
3.99/2.17	    </unfeasibleCCPs>
3.99/2.17	   </al94>
3.99/2.17	  </conditionalCrProof>
3.99/2.17	 </proof>
3.99/2.17	 <origin>
3.99/2.17	  <proofOrigin>
3.99/2.17	   <tool>
3.99/2.17	    <name>ConCon</name>
3.99/2.17	    <version>concon 1.4.0.0</version>
3.99/2.17	    <strategy>
3.99/2.17	     concon -s --cert --conf A --no-inlining theBenchmark.trs 58
3.99/2.17	    </strategy>
3.99/2.17	   </tool>
3.99/2.17	  </proofOrigin>
3.99/2.17	 </origin>
3.99/2.17	</certificationProblem>
4.02/2.25	EOF