0.00/0.02 NO 0.00/0.02 (ignored inputs)COMMENT doi:10.1007/11538363_37 [41] Example 1 0.00/0.02 input TRS: 0.00/0.02 [ f(a) -> b, 0.00/0.02 a -> a', 0.00/0.02 f(b) -> c ] 0.00/0.02 Try persistent and layer-preserving decomposition... 0.00/0.02 Sort Assignment: 0.00/0.02 a : =>8 0.00/0.02 b : =>8 0.00/0.02 c : =>8 0.00/0.02 f : 8=>8 0.00/0.02 a' : =>8 0.00/0.02 maximal types: {8} 0.00/0.02 ...decomposition failed. 0.00/0.02 TRS: 0.00/0.02 [ f(a) -> b, 0.00/0.02 a -> a', 0.00/0.02 f(b) -> c ] 0.00/0.02 Input: 0.00/0.02 [ f(a) -> b, 0.00/0.02 a -> a', 0.00/0.02 f(b) -> c ] 0.00/0.02 0.00/0.02 Make it flat: 0.00/0.02 [ f(a) -> b, 0.00/0.02 a -> a', 0.00/0.02 f(b) -> c ] 0.00/0.02 Time: 0.000 [s] 0.00/0.02 0.00/0.02 Make it Complete (R^): 0.00/0.02 [ f(a') = f(a), 0.00/0.02 f(a') = b, 0.00/0.02 f(a) = b, 0.00/0.02 a = a', 0.00/0.02 f(b) = c ] 0.00/0.02 Time: 0.000 [s] 0.00/0.02 0.00/0.02 CPNF: 0.00/0.02 [ b … f(a'), 0.00/0.02 a … a', 0.00/0.02 b … b, 0.00/0.02 c … c ] 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 f(a') 0.00/0.02 <->* b 0.00/0.02 0.00/0.02 proof: 0.00/0.02 f(a') 0.00/0.02 ->R^ f(a) 0.00/0.02 ->R^ b 0.00/0.02 0.00/0.02 b 0.00/0.02 /export/starexec/sandbox/benchmark/theBenchmark.trs: Success(not UNC) 0.00/0.02 (0 msec.) 0.00/0.02 EOF