MAYBE
REJECTED
1: error when disproving commutation of rewrite system:

f(a, b) -> c
a -> a'
b -> b'
c -> f(a', b)
c -> f(a, b')
c -> f(a, b)

and
rewrite system:

a -> b
a -> c
a -> e
b -> d
c -> a
d -> a
d -> e
g(x) -> h(a)
h(x) -> e

the step from f(a, b) to c via rule f(a, b) -> c at position empty is problematic


Tool output
NO
<?xml version="1.0"?>
<?xml-stylesheet type="text/xsl" href="cpf3HTML.xsl"?><certificationProblem xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:noNamespaceSchemaLocation="cpf3.xsd"><cpfVersion>3.0</cpfVersion><lookupTables><ruleTable><indexToRule><index>1</index><rule><funapp><name>a</name></funapp><funapp><name>b</name></funapp></rule></indexToRule><indexToRule><index>2</index><rule><funapp><name>a</name></funapp><funapp><name>c</name></funapp></rule></indexToRule><indexToRule><index>3</index><rule><funapp><name>a</name></funapp><funapp><name>e</name></funapp></rule></indexToRule><indexToRule><index>4</index><rule><funapp><name>b</name></funapp><funapp><name>d</name></funapp></rule></indexToRule><indexToRule><index>5</index><rule><funapp><name>c</name></funapp><funapp><name>a</name></funapp></rule></indexToRule><indexToRule><index>6</index><rule><funapp><name>d</name></funapp><funapp><name>a</name></funapp></rule></indexToRule><indexToRule><index>7</index><rule><funapp><name>d</name></funapp><funapp><name>e</name></funapp></rule></indexToRule><indexToRule><index>8</index><rule><funapp><name>g</name><var>x</var></funapp><funapp><name>h</name><funapp><name>a</name></funapp></funapp></rule></indexToRule><indexToRule><index>9</index><rule><funapp><name>h</name><var>x</var></funapp><funapp><name>e</name></funapp></rule></indexToRule><indexToRule><index>10</index><rule><funapp><name>f</name><funapp><name>a</name></funapp><funapp><name>b</name></funapp></funapp><funapp><name>c</name></funapp></rule></indexToRule><indexToRule><index>11</index><rule><funapp><name>a</name></funapp><funapp><name>a'</name></funapp></rule></indexToRule><indexToRule><index>12</index><rule><funapp><name>b</name></funapp><funapp><name>b'</name></funapp></rule></indexToRule><indexToRule><index>13</index><rule><funapp><name>c</name></funapp><funapp><name>f</name><funapp><name>a'</name></funapp><funapp><name>b</name></funapp></funapp></rule></indexToRule><indexToRule><index>14</index><rule><funapp><name>c</name></funapp><funapp><name>f</name><funapp><name>a</name></funapp><funapp><name>b'</name></funapp></funapp></rule></indexToRule><indexToRule><index>15</index><rule><funapp><name>c</name></funapp><funapp><name>f</name><funapp><name>a</name></funapp><funapp><name>b</name></funapp></funapp></rule></indexToRule></ruleTable></lookupTables><input><twoTrsWithSignature><signature><symbol><name>a</name><arity>0</arity></symbol><symbol><name>b</name><arity>0</arity></symbol><symbol><name>c</name><arity>0</arity></symbol><symbol><name>d</name><arity>0</arity></symbol><symbol><name>e</name><arity>0</arity></symbol><symbol><name>f</name><arity>2</arity></symbol><symbol><name>g</name><arity>1</arity></symbol><symbol><name>h</name><arity>1</arity></symbol><symbol><name>a'</name><arity>0</arity></symbol><symbol><name>b'</name><arity>0</arity></symbol></signature><trs><rules><ruleIndex>1</ruleIndex><ruleIndex>2</ruleIndex><ruleIndex>3</ruleIndex><ruleIndex>4</ruleIndex><ruleIndex>5</ruleIndex><ruleIndex>6</ruleIndex><ruleIndex>7</ruleIndex><ruleIndex>8</ruleIndex><ruleIndex>9</ruleIndex></rules></trs><trs><rules><ruleIndex>10</ruleIndex><ruleIndex>11</ruleIndex><ruleIndex>12</ruleIndex><ruleIndex>13</ruleIndex><ruleIndex>14</ruleIndex><ruleIndex>15</ruleIndex></rules></trs></twoTrsWithSignature></input><property><commutation/></property><answer><no/></answer><proof><comDisproof><nonJoinableFork><rewriteSequence><startTerm><funapp><name>f</name><funapp><name>a</name></funapp><funapp><name>b</name></funapp></funapp></startTerm><rewriteStep><positionInTerm/><ruleIndex>10</ruleIndex><funapp><name>c</name></funapp></rewriteStep></rewriteSequence><rewriteSequence><startTerm><funapp><name>f</name><funapp><name>a</name></funapp><funapp><name>b</name></funapp></funapp></startTerm><rewriteStep><positionInTerm><position>1</position></positionInTerm><ruleIndex>1</ruleIndex><funapp><name>f</name><funapp><name>b</name></funapp><funapp><name>b</name></funapp></funapp></rewriteStep></rewriteSequence><finitelyReachable/></nonJoinableFork></comDisproof></proof><metaInformation><toolInfos><toolInfo>ACP</toolInfo><toolInfo>version: 0.73</toolInfo></toolInfos></metaInformation></certificationProblem>