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