Created
January 10, 2024 15:13
-
-
Save saitouena/be65074055d4114dcd82968b684e2bcb to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
<?xml version="1.0"?> | |
<certificationProblem noNamespaceSchemaLocation="cpf3.xsd" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"> | |
<cpfVersion>3.0</cpfVersion> | |
<lookupTables/> | |
<input> | |
<infeasibilityInput> | |
<ctrs> | |
<conditionType> | |
<oriented/> | |
</conditionType> | |
<rules> | |
<rule> | |
<funapp> | |
<name>-</name> | |
<funapp> | |
<name>0</name> | |
</funapp> | |
<var>x</var> | |
</funapp> | |
<funapp> | |
<name>0</name> | |
</funapp> | |
<conditions/> | |
</rule> | |
<rule> | |
<funapp> | |
<name>-</name> | |
<var>x</var> | |
<funapp> | |
<name>0</name> | |
</funapp> | |
</funapp> | |
<var>x</var> | |
<conditions/> | |
</rule> | |
<rule> | |
<funapp> | |
<name>-</name> | |
<funapp> | |
<name>s</name> | |
<var>x</var> | |
</funapp> | |
<funapp> | |
<name>s</name> | |
<var>y</var> | |
</funapp> | |
</funapp> | |
<funapp> | |
<name>-</name> | |
<var>x</var> | |
<var>y</var> | |
</funapp> | |
<conditions/> | |
</rule> | |
</rules> | |
</ctrs> | |
<infeasibilityQuery> | |
<rule> | |
<funapp> | |
<name>-</name> | |
<var>x</var> | |
<var>x</var> | |
</funapp> | |
<funapp> | |
<name>s</name> | |
<var>x</var> | |
</funapp> | |
</rule> | |
</infeasibilityQuery> | |
</infeasibilityInput> | |
</input> | |
<property> | |
<infeasibility/> | |
</property> | |
<answer> | |
<yes/> | |
</answer> | |
<proof> | |
<infeasibilityProof> | |
<infeasibleSplitIf> | |
<splitIfInformation> | |
<name>true__</name> | |
<name>false__</name> | |
<normalUnravelingEntry> | |
<rule> | |
<funapp> | |
<name>true__</name> | |
</funapp> | |
<funapp> | |
<name>false__</name> | |
</funapp> | |
<conditions> | |
<condition> | |
<funapp> | |
<name>-</name> | |
<var>x</var> | |
<var>x</var> | |
</funapp> | |
<funapp> | |
<name>s</name> | |
<var>x</var> | |
</funapp> | |
</condition> | |
</conditions> | |
</rule> | |
<name>c1</name> | |
<var>x</var> | |
</normalUnravelingEntry> | |
<normalUnravelingEntry> | |
<rule> | |
<funapp> | |
<name>false__</name> | |
</funapp> | |
<funapp> | |
<name>true__</name> | |
</funapp> | |
<conditions> | |
<condition> | |
<funapp> | |
<name>true__</name> | |
</funapp> | |
<funapp> | |
<name>false__</name> | |
</funapp> | |
</condition> | |
</conditions> | |
</rule> | |
<name>c2</name> | |
</normalUnravelingEntry> | |
</splitIfInformation> | |
<nonreachabilityProof> | |
<nonreachableEquationalDisproof> | |
<equationalDisproof> | |
<approxAndCompletionAndNormalization> | |
<trs> | |
<rules> | |
<rule> | |
<funapp> | |
<name>c2</name> | |
<funapp> | |
<name>false__</name> | |
</funapp> | |
</funapp> | |
<funapp> | |
<name>true__</name> | |
</funapp> | |
</rule> | |
<rule> | |
<funapp> | |
<name>c2</name> | |
<funapp> | |
<name>true__</name> | |
</funapp> | |
</funapp> | |
<funapp> | |
<name>false__</name> | |
</funapp> | |
</rule> | |
<rule> | |
<funapp> | |
<name>-</name> | |
<funapp> | |
<name>0</name> | |
</funapp> | |
<var>x</var> | |
</funapp> | |
<funapp> | |
<name>0</name> | |
</funapp> | |
</rule> | |
<rule> | |
<funapp> | |
<name>-</name> | |
<var>x</var> | |
<funapp> | |
<name>0</name> | |
</funapp> | |
</funapp> | |
<var>x</var> | |
</rule> | |
<rule> | |
<funapp> | |
<name>c1</name> | |
<funapp> | |
<name>0</name> | |
</funapp> | |
<funapp> | |
<name>0</name> | |
</funapp> | |
</funapp> | |
<funapp> | |
<name>true__</name> | |
</funapp> | |
</rule> | |
<rule> | |
<funapp> | |
<name>c1</name> | |
<funapp> | |
<name>s</name> | |
<var>x</var> | |
</funapp> | |
<var>x</var> | |
</funapp> | |
<funapp> | |
<name>false__</name> | |
</funapp> | |
</rule> | |
<rule> | |
<funapp> | |
<name>c1</name> | |
<funapp> | |
<name>-</name> | |
<var>x</var> | |
<var>x</var> | |
</funapp> | |
<var>x</var> | |
</funapp> | |
<funapp> | |
<name>true__</name> | |
</funapp> | |
</rule> | |
<rule> | |
<funapp> | |
<name>c1</name> | |
<funapp> | |
<name>0</name> | |
</funapp> | |
<funapp> | |
<name>s</name> | |
<var>Y1</var> | |
</funapp> | |
</funapp> | |
<funapp> | |
<name>c1</name> | |
<funapp> | |
<name>0</name> | |
</funapp> | |
<var>Y1</var> | |
</funapp> | |
</rule> | |
<rule> | |
<funapp> | |
<name>-</name> | |
<funapp> | |
<name>s</name> | |
<var>x</var> | |
</funapp> | |
<funapp> | |
<name>s</name> | |
<var>y</var> | |
</funapp> | |
</funapp> | |
<funapp> | |
<name>-</name> | |
<var>x</var> | |
<var>y</var> | |
</funapp> | |
</rule> | |
<rule> | |
<funapp> | |
<name>c1</name> | |
<funapp> | |
<name>-</name> | |
<var>X0</var> | |
<var>X0</var> | |
</funapp> | |
<funapp> | |
<name>s</name> | |
<var>W1</var> | |
</funapp> | |
</funapp> | |
<funapp> | |
<name>c1</name> | |
<funapp> | |
<name>-</name> | |
<var>X0</var> | |
<var>X0</var> | |
</funapp> | |
<var>W1</var> | |
</funapp> | |
</rule> | |
</rules> | |
</trs> | |
<approxCompletionProof> | |
<wcrProof> | |
<joinAutoNF/> | |
</wcrProof> | |
<trsTerminationProof> | |
<ruleRemoval> | |
<recursivePathOrder> | |
<statusPrecedence> | |
<statusPrecedenceEntry> | |
<name>false__</name> | |
<arity>0</arity> | |
<precedence>0</precedence> | |
<lex/> | |
</statusPrecedenceEntry> | |
<statusPrecedenceEntry> | |
<name>true__</name> | |
<arity>0</arity> | |
<precedence>1</precedence> | |
<lex/> | |
</statusPrecedenceEntry> | |
<statusPrecedenceEntry> | |
<name>c2</name> | |
<arity>1</arity> | |
<precedence>2</precedence> | |
<lex/> | |
</statusPrecedenceEntry> | |
<statusPrecedenceEntry> | |
<name>-</name> | |
<arity>2</arity> | |
<precedence>3</precedence> | |
<lex/> | |
</statusPrecedenceEntry> | |
<statusPrecedenceEntry> | |
<name>0</name> | |
<arity>0</arity> | |
<precedence>4</precedence> | |
<lex/> | |
</statusPrecedenceEntry> | |
<statusPrecedenceEntry> | |
<name>c1</name> | |
<arity>2</arity> | |
<precedence>5</precedence> | |
<lex/> | |
</statusPrecedenceEntry> | |
<statusPrecedenceEntry> | |
<name>s</name> | |
<arity>1</arity> | |
<precedence>6</precedence> | |
<lex/> | |
</statusPrecedenceEntry> | |
</statusPrecedence> | |
</recursivePathOrder> | |
<trs> | |
<rules> | |
<rule> | |
<funapp> | |
<name>c2</name> | |
<funapp> | |
<name>false__</name> | |
</funapp> | |
</funapp> | |
<funapp> | |
<name>true__</name> | |
</funapp> | |
</rule> | |
<rule> | |
<funapp> | |
<name>c2</name> | |
<funapp> | |
<name>true__</name> | |
</funapp> | |
</funapp> | |
<funapp> | |
<name>false__</name> | |
</funapp> | |
</rule> | |
<rule> | |
<funapp> | |
<name>-</name> | |
<funapp> | |
<name>0</name> | |
</funapp> | |
<var>x</var> | |
</funapp> | |
<funapp> | |
<name>0</name> | |
</funapp> | |
</rule> | |
<rule> | |
<funapp> | |
<name>-</name> | |
<var>x</var> | |
<funapp> | |
<name>0</name> | |
</funapp> | |
</funapp> | |
<var>x</var> | |
</rule> | |
<rule> | |
<funapp> | |
<name>c1</name> | |
<funapp> | |
<name>0</name> | |
</funapp> | |
<funapp> | |
<name>0</name> | |
</funapp> | |
</funapp> | |
<funapp> | |
<name>true__</name> | |
</funapp> | |
</rule> | |
<rule> | |
<funapp> | |
<name>c1</name> | |
<funapp> | |
<name>s</name> | |
<var>x</var> | |
</funapp> | |
<var>x</var> | |
</funapp> | |
<funapp> | |
<name>false__</name> | |
</funapp> | |
</rule> | |
<rule> | |
<funapp> | |
<name>c1</name> | |
<funapp> | |
<name>-</name> | |
<var>x</var> | |
<var>x</var> | |
</funapp> | |
<var>x</var> | |
</funapp> | |
<funapp> | |
<name>true__</name> | |
</funapp> | |
</rule> | |
<rule> | |
<funapp> | |
<name>c1</name> | |
<funapp> | |
<name>0</name> | |
</funapp> | |
<funapp> | |
<name>s</name> | |
<var>Y1</var> | |
</funapp> | |
</funapp> | |
<funapp> | |
<name>c1</name> | |
<funapp> | |
<name>0</name> | |
</funapp> | |
<var>Y1</var> | |
</funapp> | |
</rule> | |
<rule> | |
<funapp> | |
<name>-</name> | |
<funapp> | |
<name>s</name> | |
<var>x</var> | |
</funapp> | |
<funapp> | |
<name>s</name> | |
<var>y</var> | |
</funapp> | |
</funapp> | |
<funapp> | |
<name>-</name> | |
<var>x</var> | |
<var>y</var> | |
</funapp> | |
</rule> | |
<rule> | |
<funapp> | |
<name>c1</name> | |
<funapp> | |
<name>-</name> | |
<var>X0</var> | |
<var>X0</var> | |
</funapp> | |
<funapp> | |
<name>s</name> | |
<var>W1</var> | |
</funapp> | |
</funapp> | |
<funapp> | |
<name>c1</name> | |
<funapp> | |
<name>-</name> | |
<var>X0</var> | |
<var>X0</var> | |
</funapp> | |
<var>W1</var> | |
</funapp> | |
</rule> | |
</rules> | |
</trs> | |
<trsTerminationProof> | |
<rIsEmpty/> | |
</trsTerminationProof> | |
</ruleRemoval> | |
</trsTerminationProof> | |
</approxCompletionProof> | |
</approxAndCompletionAndNormalization> | |
</equationalDisproof> | |
</nonreachableEquationalDisproof> | |
</nonreachabilityProof> | |
</infeasibleSplitIf> | |
</infeasibilityProof> | |
</proof> | |
</certificationProblem> |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment