0.00/0.03 YES 0.00/0.03 (ignored inputs)COMMENT doi:10.1007/11805618_6 [7] Example 3 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama 0.00/0.03 input TRS: 0.00/0.03 [ b -> a, 0.00/0.03 b -> c, 0.00/0.03 c -> h(b), 0.00/0.03 c -> d, 0.00/0.03 a -> h(a), 0.00/0.03 d -> h(d) ] 0.00/0.03 Try persistent and layer-preserving decomposition... 0.00/0.03 Sort Assignment: 0.00/0.03 a : =>7 0.00/0.03 b : =>7 0.00/0.03 c : =>7 0.00/0.03 d : =>7 0.00/0.03 h : 7=>7 0.00/0.03 maximal types: {7} 0.00/0.03 ...decomposition failed. 0.00/0.03 TRS: 0.00/0.03 [ b -> a, 0.00/0.03 b -> c, 0.00/0.03 c -> h(b), 0.00/0.03 c -> d, 0.00/0.03 a -> h(a), 0.00/0.03 d -> h(d) ] 0.00/0.03 Input: 0.00/0.03 [ b -> a, 0.00/0.03 b -> c, 0.00/0.03 c -> h(b), 0.00/0.03 c -> d, 0.00/0.03 a -> h(a), 0.00/0.03 d -> h(d) ] 0.00/0.03 0.00/0.03 Make it flat: 0.00/0.03 [ b -> a, 0.00/0.03 b -> c, 0.00/0.03 c -> h(b), 0.00/0.03 c -> d, 0.00/0.03 a -> h(a), 0.00/0.03 d -> h(d) ] 0.00/0.03 Time: 0.000 [s] 0.00/0.03 0.00/0.03 Make it Complete (R^): 0.00/0.03 [ h(b) = a, 0.00/0.03 b = h(a), 0.00/0.03 h(a) = c, 0.00/0.03 h(a) = h(c), 0.00/0.03 h(a) = h(d), 0.00/0.03 h(a) = d, 0.00/0.03 a = c, 0.00/0.03 a = h(c), 0.00/0.03 a = h(d), 0.00/0.03 h(a) = h(b), 0.00/0.03 a = d, 0.00/0.03 b = a, 0.00/0.03 b = d, 0.00/0.03 b = h(d), 0.00/0.03 b = h(c), 0.00/0.03 b = h(b), 0.00/0.03 b = c, 0.00/0.03 d = h(b), 0.00/0.03 h(b) = h(d), 0.00/0.03 h(b) = h(c), 0.00/0.03 c = h(b), 0.00/0.03 h(c) = d, 0.00/0.03 h(c) = h(d), 0.00/0.03 h(c) = c, 0.00/0.03 c = h(d), 0.00/0.03 c = d, 0.00/0.03 a = h(a), 0.00/0.03 d = h(d) ] 0.00/0.03 Time: 0.006 [s] 0.00/0.03 0.00/0.03 CPNF: 0.00/0.03 [ ] 0.00/0.03 Time: 0.000 [s] 0.00/0.03 0.00/0.03 Now checking all the pairs in CW... 0.00/0.03 0.00/0.03 Time to check pairs: 0.000 [s] 0.00/0.03 0.00/0.03 The TRS has Uniqueness of Normal Forms. 0.00/0.03 /export/starexec/sandbox2/benchmark/theBenchmark.trs: Success(UNC) 0.00/0.03 (6 msec.) 0.00/0.03 EOF