0.00/0.02 NO 0.00/0.02 (ignored inputs)COMMENT [11] Example 3.3.1 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama 0.00/0.02 input TRS: 0.00/0.02 [ b -> a, 0.00/0.02 b -> c, 0.00/0.02 c -> b, 0.00/0.02 c -> d ] 0.00/0.02 Try persistent and layer-preserving decomposition... 0.00/0.02 Sort Assignment: 0.00/0.02 a : =>5 0.00/0.02 b : =>5 0.00/0.02 c : =>5 0.00/0.02 d : =>5 0.00/0.02 maximal types: {5} 0.00/0.02 ...decomposition failed. 0.00/0.02 TRS: 0.00/0.02 [ b -> a, 0.00/0.02 b -> c, 0.00/0.02 c -> b, 0.00/0.02 c -> d ] 0.00/0.02 Input: 0.00/0.02 [ b -> a, 0.00/0.02 b -> c, 0.00/0.02 c -> b, 0.00/0.02 c -> d ] 0.00/0.02 0.00/0.02 Make it flat: 0.00/0.02 [ b -> a, 0.00/0.02 b -> c, 0.00/0.02 c -> b, 0.00/0.02 c -> d ] 0.00/0.02 Time: 0.000 [s] 0.00/0.02 0.00/0.02 Make it Complete (R^): 0.00/0.02 [ a = c, 0.00/0.02 a = d, 0.00/0.02 b = a, 0.00/0.02 b = d, 0.00/0.02 b = c, 0.00/0.02 c = d ] 0.00/0.02 Time: 0.000 [s] 0.00/0.02 0.00/0.02 CPNF: 0.00/0.02 [ a … a, 0.00/0.02 a … d ] 0.00/0.02 Time: 0.000 [s] 0.00/0.02 0.00/0.02 The TRS doesn't have Uniqueness of Normal Forms. 0.00/0.02 Counter Example: 0.00/0.02 a 0.00/0.02 <->* d 0.00/0.02 0.00/0.02 proof: 0.00/0.02 a 0.00/0.02 0.00/0.02 d 0.00/0.02 ->R^ c 0.00/0.02 ->R^ b 0.00/0.02 ->R^ a 0.00/0.02 /export/starexec/sandbox2/benchmark/theBenchmark.trs: Success(not UNC) 0.00/0.02 (0 msec.) 0.00/0.02 EOF