YES
CERTIFIED

Tool output:
YES
<?xml version='1.0' ?><certificationProblem xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:noNamespaceSchemaLocation="cpf3.xsd"><cpfVersion>3.0</cpfVersion><lookupTables /><input><infeasibilityInput><ctrs><conditionType><oriented /></conditionType><rules><rule><funapp><name>g</name><funapp><name>h</name><var>x</var></funapp><var>y</var></funapp><funapp><name>g</name><var>x</var><funapp><name>h</name><var>y</var></funapp></funapp><conditions /></rule><rule><funapp><name>f</name><var>x</var><funapp><name>a</name></funapp></funapp><funapp><name>f</name><var>x</var><funapp><name>g</name><var>x</var><funapp><name>b</name></funapp></funapp></funapp><conditions /></rule><rule><funapp><name>g</name><funapp><name>a</name></funapp><var>y</var></funapp><var>y</var><conditions /></rule></rules></ctrs><infeasibilityQuery><rule><funapp><name>F</name><var>x</var><funapp><name>g</name><var>x</var><funapp><name>b</name></funapp></funapp></funapp><funapp><name>F</name><var>y</var><funapp><name>a</name></funapp></funapp></rule></infeasibilityQuery></infeasibilityInput></input><property><infeasibility /></property><answer><yes /></answer><proof><infeasibilityProof><infeasibleGoalLifting><name>true__</name><name>false__</name><infeasibilityProof><rightInlineConditions><rules><rule><funapp><name>g</name><funapp><name>h</name><var>x</var></funapp><var>y</var></funapp><funapp><name>g</name><var>x</var><funapp><name>h</name><var>y</var></funapp></funapp><conditions /></rule><rule><funapp><name>f</name><var>x</var><funapp><name>a</name></funapp></funapp><funapp><name>f</name><var>x</var><funapp><name>g</name><var>x</var><funapp><name>b</name></funapp></funapp></funapp><conditions /></rule><rule><funapp><name>g</name><funapp><name>a</name></funapp><var>y</var></funapp><var>y</var><conditions /></rule><rule><funapp><name>true__</name></funapp><funapp><name>false__</name></funapp><conditions><condition><funapp><name>F</name><var>x</var><funapp><name>g</name><var>x</var><funapp><name>b</name></funapp></funapp></funapp><funapp><name>F</name><var>y</var><funapp><name>a</name></funapp></funapp></condition></conditions></rule></rules><inlinedRules /><infeasibilityProof><infeasibleSplitIf><splitIfInformation><funapp><name>true__</name></funapp><funapp><name>false__</name></funapp><normalUnravelingEntry><rule><funapp><name>true__</name></funapp><funapp><name>false__</name></funapp><conditions><condition><funapp><name>F</name><var>x</var><funapp><name>g</name><var>x</var><funapp><name>b</name></funapp></funapp></funapp><funapp><name>F</name><var>y</var><funapp><name>a</name></funapp></funapp></condition></conditions></rule><name>c1</name><var>y</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>c1</name><funapp><name>F</name><var>y</var><funapp><name>a</name></funapp></funapp><var>y</var></funapp><funapp><name>false__</name></funapp></rule><rule><funapp><name>f</name><var>x</var><funapp><name>b</name></funapp></funapp><funapp><name>f</name><var>x</var><funapp><name>a</name></funapp></funapp></rule><rule><funapp><name>c1</name><funapp><name>F</name><var>x</var><funapp><name>b</name></funapp></funapp><var>y</var></funapp><funapp><name>true__</name></funapp></rule><rule><funapp><name>g</name><var>x0</var><var>x1</var></funapp><var>x1</var></rule><rule><funapp><name>h</name><var>x0</var></funapp><var>x0</var></rule></rules></trs><approxCompletionProof><wcrProof><joinAutoNF /></wcrProof><trsTerminationProof><ruleRemoval><recursivePathOrder><statusPrecedence><statusPrecedenceEntry><name>true__</name><arity>0</arity><precedence>0</precedence><lex /></statusPrecedenceEntry><statusPrecedenceEntry><name>false__</name><arity>0</arity><precedence>1</precedence><lex /></statusPrecedenceEntry><statusPrecedenceEntry><name>h</name><arity>1</arity><precedence>2</precedence><lex /></statusPrecedenceEntry><statusPrecedenceEntry><name>g</name><arity>2</arity><precedence>3</precedence><lex /></statusPrecedenceEntry><statusPrecedenceEntry><name>f</name><arity>2</arity><precedence>4</precedence><lex /></statusPrecedenceEntry><statusPrecedenceEntry><name>a</name><arity>0</arity><precedence>5</precedence><lex /></statusPrecedenceEntry><statusPrecedenceEntry><name>b</name><arity>0</arity><precedence>6</precedence><lex /></statusPrecedenceEntry><statusPrecedenceEntry><name>c1</name><arity>2</arity><precedence>7</precedence><lex /></statusPrecedenceEntry><statusPrecedenceEntry><name>F</name><arity>2</arity><precedence>8</precedence><lex /></statusPrecedenceEntry><statusPrecedenceEntry><name>c2</name><arity>1</arity><precedence>9</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>c1</name><funapp><name>F</name><var>y</var><funapp><name>a</name></funapp></funapp><var>y</var></funapp><funapp><name>false__</name></funapp></rule><rule><funapp><name>f</name><var>x</var><funapp><name>b</name></funapp></funapp><funapp><name>f</name><var>x</var><funapp><name>a</name></funapp></funapp></rule><rule><funapp><name>c1</name><funapp><name>F</name><var>x</var><funapp><name>b</name></funapp></funapp><var>y</var></funapp><funapp><name>true__</name></funapp></rule><rule><funapp><name>g</name><var>x0</var><var>x1</var></funapp><var>x1</var></rule><rule><funapp><name>h</name><var>x0</var></funapp><var>x0</var></rule></rules></trs><trsTerminationProof><rIsEmpty /></trsTerminationProof></ruleRemoval></trsTerminationProof></approxCompletionProof></approxAndCompletionAndNormalization></equationalDisproof></nonreachableEquationalDisproof></nonreachabilityProof></infeasibleSplitIf></infeasibilityProof></rightInlineConditions></infeasibilityProof></infeasibleGoalLifting></infeasibilityProof></proof></certificationProblem>