0.00/0.03 YES 0.00/0.03 (ignored inputs)COMMENT doi:10.1007/s10817-011-9238-x [33] Example 8 0.00/0.03 input TRS: 0.00/0.03 [ f(a,a) -> c, 0.00/0.03 f(b,?x) -> f(?x,?x), 0.00/0.03 f(?x,b) -> f(?x,?x), 0.00/0.03 a -> b ] 0.00/0.03 Try persistent and layer-preserving decomposition... 0.00/0.03 Sort Assignment: 0.00/0.03 a : =>9 0.00/0.03 b : =>9 0.00/0.03 c : =>10 0.00/0.03 f : 9*9=>10 0.00/0.03 maximal types: {9,10} 0.00/0.03 ...decomposition failed. 0.00/0.03 TRS: 0.00/0.03 [ f(a,a) -> c, 0.00/0.03 f(b,?x) -> f(?x,?x), 0.00/0.03 f(?x,b) -> f(?x,?x), 0.00/0.03 a -> b ] 0.00/0.03 Input: 0.00/0.03 [ f(a,a) -> c, 0.00/0.03 f(b,?x) -> f(?x,?x), 0.00/0.03 f(?x,b) -> f(?x,?x), 0.00/0.03 a -> b ] 0.00/0.03 0.00/0.03 Make it flat: 0.00/0.03 [ f(a,a) -> c, 0.00/0.03 f(b,?x) -> f(?x,?x), 0.00/0.03 f(?x,b) -> f(?x,?x), 0.00/0.03 a -> b ] 0.00/0.03 Time: 0.000 [s] 0.00/0.03 0.00/0.03 Make it Complete (R^): 0.00/0.03 [ f(a,b) = c, 0.00/0.03 f(b,a) = c, 0.00/0.03 c = f(b,b), 0.00/0.03 f(a,a) = c, 0.00/0.03 f(a,?x) = f(?x,?x), 0.00/0.03 f(b,?x) = f(?x,b), 0.00/0.03 f(?x,b) = f(a,?x), 0.00/0.03 f(a,?x) = f(b,?x), 0.00/0.03 f(a,?x) = f(?x,a), 0.00/0.03 f(b,?x) = f(?x,a), 0.00/0.03 f(b,?x) = f(?x,?x), 0.00/0.03 f(?x,a) = f(?x,b), 0.00/0.03 f(b,a) = f(b,b), 0.00/0.03 f(b,b) = f(a,a), 0.00/0.03 f(a,a) = f(b,a), 0.00/0.03 f(b,b) = f(a,b), 0.00/0.03 f(b,a) = f(a,b), 0.00/0.03 f(a,a) = f(a,b), 0.00/0.03 f(?x,a) = f(?x,?x), 0.00/0.03 f(?x,b) = f(?x,?x), 0.00/0.03 a = b ] 0.00/0.03 Time: 0.008 [s] 0.00/0.03 0.00/0.03 CPNF: 0.00/0.03 [ c … c, 0.00/0.03 a … b ] 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 (8 msec.) 0.00/0.03 EOF