0.00/0.04 NO 0.00/0.04 (ignored inputs)COMMENT [111] Example 1 0.00/0.04 input TRS: 0.00/0.04 [ a -> b, 0.00/0.04 f(?x,a) -> f(b,b), 0.00/0.04 f(b,?x) -> f(b,b), 0.00/0.04 f(f(?x,?y),?z) -> f(b,b) ] 0.00/0.04 Try persistent and layer-preserving decomposition... 0.00/0.04 Sort Assignment: 0.00/0.04 a : =>8 0.00/0.04 b : =>8 0.00/0.04 f : 8*8=>8 0.00/0.04 maximal types: {8} 0.00/0.04 ...decomposition failed. 0.00/0.04 TRS: 0.00/0.04 [ a -> b, 0.00/0.04 f(?x,a) -> f(b,b), 0.00/0.04 f(b,?x) -> f(b,b), 0.00/0.04 f(f(?x,?y),?z) -> f(b,b) ] 0.00/0.04 unknown Non-Omega-Overlapping 0.00/0.04 unknown Right-Reducible 0.00/0.04 Check distinct normal forms in critical pair closure 0.00/0.04 convertible distinct normal forms: f(?x,b) = f(?x_1,b) 0.00/0.04 /export/starexec/sandbox2/benchmark/theBenchmark.trs: Success(not UNC) 0.00/0.04 (1 msec.) 0.00/0.04 EOF