MAYBE
(ignored inputs)COMMENT R' from Example 3.1 from [F12-RTA]
Rewrite Rules:
   [ a -> b,
     a -> f(a),
     b -> f(f(b)),
     f(f(f(b))) -> b ]
Apply Direct Methods...
Inner CPs:
   [ f(f(f(f(f(b))))) = b ]
Outer CPs:
   [ b = f(a) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
Linear
unknown Development Closed
unknown Strongly Closed
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ f(a) = b,
     b = f(a),
     b = f(f(f(f(f(b))))),
     f(f(f(f(f(b))))) = b ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair <f(f(f(f(f(b))))), b> by Rules <2, 3> preceded by [(f,1),(f,1),(f,1)]
 joinable by a reduction of rules <[([(f,1),(f,1)],3)], [([],2)]>
Critical Pair <f(a), b> by Rules <1, 0> preceded by []
 joinable by a reduction of rules <[([(f,1)],1),([(f,1),(f,1)],0)], [([],2)]>
unknown Diagram Decreasing
check Non-Confluence...
obtain 14 rules by 3 steps unfolding
strenghten f(a) and b
strenghten f(b) and b
strenghten f(a) and f(b)
strenghten f(f(a)) and b
strenghten f(f(b)) and b
strenghten f(f(a)) and f(a)
strenghten f(f(a)) and f(b)
strenghten f(f(b)) and f(a)
strenghten f(f(b)) and f(b)
strenghten f(f(f(a))) and b
strenghten f(f(f(b))) and b
strenghten f(f(a)) and f(f(b))
strenghten f(f(f(f(b)))) and b
strenghten f(f(f(f(f(b))))) and b
obtain 100 candidates for checking non-joinability
check by TCAP-Approximation (failure)
check by Root-Approximation (failure)
check by Ordering(rpo), check by Tree-Automata Approximation (failure)
check by Interpretation(mod2) (failure)
check by Descendants-Approximation, check by Ordering(poly) (failure)
unknown Non-Confluence
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
failure(empty P)
unknown Reduction-Preserving Completion
Direct Methods: Can't judge

Try Persistent Decomposition for...
   [ a -> b,
     a -> f(a),
     b -> f(f(b)),
     f(f(f(b))) -> b ]
Sort Assignment:
 a : =>5
 b : =>5
 f : 5=>5
maximal types: {5}
Persistent Decomposition failed: Can't judge

Try Layer Preserving Decomposition for...
   [ a -> b,
     a -> f(a),
     b -> f(f(b)),
     f(f(f(b))) -> b ]
Layer Preserving Decomposition failed: Can't judge

Try Commutative Decomposition for...
   [ a -> b,
     a -> f(a),
     b -> f(f(b)),
     f(f(f(b))) -> b ]
Outside Critical Pair: <f(a), b> by Rules <1, 0>
develop reducts from lhs term...
<{1}, f(f(a))>
<{0}, f(b)>
<{}, f(a)>
develop reducts from rhs term...
<{2}, f(f(b))>
<{}, b>
Inside Critical Pair: <f(f(f(f(f(b))))), b> by Rules <2, 3>
develop reducts from lhs term...
<{3}, f(f(b))>
<{2}, f(f(f(f(f(f(f(b)))))))>
<{}, f(f(f(f(f(b)))))>
develop reducts from rhs term...
<{2}, f(f(b))>
<{}, b>
Try A Minimal Decomposition {0,1}{2,3}
{0,1}
(cm)Rewrite Rules:
   [ a -> b,
     a -> f(a) ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [ b = f(a) ]
Overlay, check Innermost Termination...
unknown Innermost Terminating
unknown Knuth & Bendix
Linear
unknown Development Closed
unknown Strongly Closed
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ f(a) = b,
     b = f(a) ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair <f(a), b> by Rules <1, 0> preceded by []
unknown Diagram Decreasing
check Non-Confluence...
obtain 12 rules by 3 steps unfolding
strenghten f(a) and b
strenghten f(b) and b
strenghten f(a) and f(b)
strenghten f(f(a)) and b
strenghten f(f(b)) and b
strenghten f(f(a)) and f(a)
strenghten f(f(a)) and f(b)
strenghten f(f(b)) and f(a)
strenghten f(f(b)) and f(b)
strenghten f(f(f(a))) and b
strenghten f(f(f(b))) and b
strenghten f(f(a)) and f(f(b))
strenghten f(f(f(a))) and f(a)
strenghten f(f(f(a))) and f(b)
strenghten f(f(f(b))) and f(a)
strenghten f(f(f(b))) and f(b)
strenghten f(f(f(f(a)))) and b
strenghten f(f(f(f(b)))) and b
obtain 64 candidates for checking non-joinability
check by TCAP-Approximation (success)
Witness for Non-Confluence: <f(a), b>
Direct Methods: not CR
{2,3}
(cm)Rewrite Rules:
   [ b -> f(f(b)),
     f(f(f(b))) -> b ]
Apply Direct Methods...
Inner CPs:
   [ f(f(f(f(f(b))))) = b ]
Outer CPs:
   [  ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
Linear
unknown Development Closed
Strongly Closed
Direct Methods: CR
Commutative Decomposition failed: Can't judge
No further decomposition possible


Final result: Can't judge
213.trs: Failure(unknown)
(2056 msec.)