0.00/0.04 NO 0.00/0.04 (ignored inputs)COMMENT doi:10.1016/0890-5401 ( 90 ) 90015-A [24] Example 1 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama 0.00/0.04 Rewrite Rules: 0.00/0.04 [ a -> f(a,b), 0.00/0.04 f(a,b) -> f(b,a) ] 0.00/0.04 Apply Direct Methods... 0.00/0.04 Inner CPs: 0.00/0.04 [ f(f(a,b),b) = f(b,a) ] 0.00/0.04 Outer CPs: 0.00/0.04 [ ] 0.00/0.04 not Overlay, check Termination... 0.00/0.04 unknown/not Terminating 0.00/0.04 unknown Knuth & Bendix 0.00/0.04 Linear 0.00/0.04 unknown Development Closed 0.00/0.04 unknown Strongly Closed 0.00/0.04 unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow 0.00/0.04 inner CP cond (upside-parallel) 0.00/0.04 innter CP Cond (outside) 0.00/0.04 unknown Upside-Parallel-Closed/Outside-Closed 0.00/0.04 (inner) Parallel CPs: (not computed) 0.00/0.04 unknown Toyama (Parallel CPs) 0.00/0.04 Simultaneous CPs: 0.00/0.04 [ f(b,a) = f(f(a,b),b), 0.00/0.04 f(f(a,b),b) = f(b,a) ] 0.00/0.04 unknown Okui (Simultaneous CPs) 0.00/0.04 unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping 0.00/0.04 unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping 0.00/0.04 check Locally Decreasing Diagrams by Rule Labelling... 0.00/0.04 Critical Pair by Rules <0, 1> preceded by [(f,1)] 0.00/0.04 unknown Diagram Decreasing 0.00/0.04 check Non-Confluence... 0.00/0.04 obtain 10 rules by 3 steps unfolding 0.00/0.04 obtain 100 candidates for checking non-joinability 0.00/0.04 check by TCAP-Approximation (success) 0.00/0.04 Witness for Non-Confluence: f(b,a)> 0.00/0.04 Direct Methods: not CR 0.00/0.04 0.00/0.04 Combined result: not CR 0.00/0.04 /export/starexec/sandbox/benchmark/theBenchmark.trs: Success(not CR) 0.00/0.04 (8 msec.) 0.00/0.04 EOF