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

c(a(x)) -> c(c(x))
c(c(x)) -> a(b(x))
a(a(x)) -> b(c(x))
b(a(x)) -> c(c(x))
c(a(x)) -> b(a(x))
b(c(x)) -> a(b(x))
c(c(x)) -> a(b(x))
b(c(x)) -> c(a(x))

and
rewrite system:

c(b(x)) -> c(a(x))
b(c(x)) -> c(b(x))
a(b(x)) -> c(c(x))
a(a(x)) -> a(b(x))
a(c(x)) -> a(a(x))
c(c(x)) -> a(a(x))
a(a(x)) -> b(c(x))
b(b(x)) -> c(b(x))

the step from b(c(x)) to c(a(x)) via rule b(c(x)) -> c(a(x)) 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>c</name><funapp><name>b</name><var>x</var></funapp></funapp><funapp><name>c</name><funapp><name>a</name><var>x</var></funapp></funapp></rule></indexToRule><indexToRule><index>2</index><rule><funapp><name>b</name><funapp><name>c</name><var>x</var></funapp></funapp><funapp><name>c</name><funapp><name>b</name><var>x</var></funapp></funapp></rule></indexToRule><indexToRule><index>3</index><rule><funapp><name>a</name><funapp><name>b</name><var>x</var></funapp></funapp><funapp><name>c</name><funapp><name>c</name><var>x</var></funapp></funapp></rule></indexToRule><indexToRule><index>4</index><rule><funapp><name>a</name><funapp><name>a</name><var>x</var></funapp></funapp><funapp><name>a</name><funapp><name>b</name><var>x</var></funapp></funapp></rule></indexToRule><indexToRule><index>5</index><rule><funapp><name>a</name><funapp><name>c</name><var>x</var></funapp></funapp><funapp><name>a</name><funapp><name>a</name><var>x</var></funapp></funapp></rule></indexToRule><indexToRule><index>6</index><rule><funapp><name>c</name><funapp><name>c</name><var>x</var></funapp></funapp><funapp><name>a</name><funapp><name>a</name><var>x</var></funapp></funapp></rule></indexToRule><indexToRule><index>7</index><rule><funapp><name>a</name><funapp><name>a</name><var>x</var></funapp></funapp><funapp><name>b</name><funapp><name>c</name><var>x</var></funapp></funapp></rule></indexToRule><indexToRule><index>8</index><rule><funapp><name>b</name><funapp><name>b</name><var>x</var></funapp></funapp><funapp><name>c</name><funapp><name>b</name><var>x</var></funapp></funapp></rule></indexToRule><indexToRule><index>9</index><rule><funapp><name>c</name><funapp><name>a</name><var>x</var></funapp></funapp><funapp><name>c</name><funapp><name>c</name><var>x</var></funapp></funapp></rule></indexToRule><indexToRule><index>10</index><rule><funapp><name>c</name><funapp><name>c</name><var>x</var></funapp></funapp><funapp><name>a</name><funapp><name>b</name><var>x</var></funapp></funapp></rule></indexToRule><indexToRule><index>11</index><rule><funapp><name>b</name><funapp><name>a</name><var>x</var></funapp></funapp><funapp><name>c</name><funapp><name>c</name><var>x</var></funapp></funapp></rule></indexToRule><indexToRule><index>12</index><rule><funapp><name>c</name><funapp><name>a</name><var>x</var></funapp></funapp><funapp><name>b</name><funapp><name>a</name><var>x</var></funapp></funapp></rule></indexToRule><indexToRule><index>13</index><rule><funapp><name>b</name><funapp><name>c</name><var>x</var></funapp></funapp><funapp><name>a</name><funapp><name>b</name><var>x</var></funapp></funapp></rule></indexToRule><indexToRule><index>14</index><rule><funapp><name>b</name><funapp><name>c</name><var>x</var></funapp></funapp><funapp><name>c</name><funapp><name>a</name><var>x</var></funapp></funapp></rule></indexToRule></ruleTable></lookupTables><input><twoTrsWithSignature><signature><symbol><name>a</name><arity>1</arity></symbol><symbol><name>b</name><arity>1</arity></symbol><symbol><name>c</name><arity>1</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></rules></trs><trs><rules><ruleIndex>9</ruleIndex><ruleIndex>10</ruleIndex><ruleIndex>7</ruleIndex><ruleIndex>11</ruleIndex><ruleIndex>12</ruleIndex><ruleIndex>13</ruleIndex><ruleIndex>10</ruleIndex><ruleIndex>14</ruleIndex></rules></trs></twoTrsWithSignature></input><property><commutation/></property><answer><no/></answer><proof><comDisproof><nonJoinableFork><rewriteSequence><startTerm><funapp><name>b</name><funapp><name>c</name><var>x</var></funapp></funapp></startTerm><rewriteStep><positionInTerm/><ruleIndex>14</ruleIndex><funapp><name>c</name><funapp><name>a</name><var>x</var></funapp></funapp></rewriteStep></rewriteSequence><rewriteSequence><startTerm><funapp><name>b</name><funapp><name>c</name><var>x</var></funapp></funapp></startTerm><rewriteStep><positionInTerm/><ruleIndex>2</ruleIndex><funapp><name>c</name><funapp><name>b</name><var>x</var></funapp></funapp></rewriteStep></rewriteSequence><finitelyReachable/></nonJoinableFork></comDisproof></proof><metaInformation><toolInfos><toolInfo>ACP</toolInfo><toolInfo>version: 0.73</toolInfo></toolInfos></metaInformation></certificationProblem>