MAYBE
REJECTED
1.1: error when proving commutation by almost development closed criterion
the inner critical pair f(c) S<- . ->R c is not closed with multi-step over RSome (5)
hence the almost development closed check for the following TRSs could not be proven
R: rewrite system:

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


S: rewrite system:

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


Tool output
YES
<?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>f</name><funapp><name>a</name></funapp></funapp><funapp><name>c</name></funapp></rule></indexToRule><indexToRule><index>2</index><rule><funapp><name>b</name></funapp><funapp><name>c</name></funapp></rule></indexToRule><indexToRule><index>3</index><rule><funapp><name>b</name></funapp><funapp><name>a</name></funapp></rule></indexToRule><indexToRule><index>4</index><rule><funapp><name>c</name></funapp><funapp><name>f</name><funapp><name>c</name></funapp></funapp></rule></indexToRule><indexToRule><index>5</index><rule><funapp><name>c</name></funapp><funapp><name>c</name></funapp></rule></indexToRule><indexToRule><index>6</index><rule><funapp><name>f</name><funapp><name>a</name></funapp></funapp><funapp><name>b</name></funapp></rule></indexToRule><indexToRule><index>7</index><rule><funapp><name>a</name></funapp><funapp><name>c</name></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>f</name><arity>1</arity></symbol></signature><trs><rules><ruleIndex>1</ruleIndex><ruleIndex>2</ruleIndex><ruleIndex>3</ruleIndex></rules></trs><trs><rules><ruleIndex>4</ruleIndex><ruleIndex>5</ruleIndex><ruleIndex>6</ruleIndex><ruleIndex>7</ruleIndex></rules></trs></twoTrsWithSignature></input><property><commutation/></property><answer><yes/></answer><proof><comProof><swapTRSs><comProof><developmentClosed><joinAutoBfs>5</joinAutoBfs></developmentClosed></comProof></swapTRSs></comProof></proof><metaInformation><toolInfos><toolInfo>ACP</toolInfo><toolInfo>version: 0.73</toolInfo></toolInfos></metaInformation></certificationProblem>