MAYBE
(ignored inputs)COMMENT reduction failed
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 11 rules by 3 steps unfolding
obtain 100 candidates for checking non-joinability
check by TCAP-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
check by Ordered Rewriting...
remove redundants rules and split
R-part:
   [ a -> b,
     a -> f(a),
     b -> f(f(b)),
     f(f(f(b))) -> b ]
E-part:
   [ ]
...failed to find a suitable LPO.
unknown Confluence by Ordered Rewriting
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 10 rules by 3 steps unfolding
obtain 64 candidates for checking non-joinability
check by TCAP-Approximation (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (failure)
check by Ordering(rpo), check by Tree-Automata Approximation (success)
Witness for Non-Confluence: <f(a) <- 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


Combined result: Can't judge
/tmp/fileybyG0k.trs: Failure(unknown CR)
(850 msec.)