0.00/0.14	YES
0.00/0.14	(ignored inputs)COMMENT doi:10.1007/978-3-642-12251-4_20 [32] Example 3.2
0.00/0.14	input TRS:
0.00/0.14	   [ a -> b,
0.00/0.14	     a -> c,
0.00/0.14	     a -> e,
0.00/0.14	     b -> d,
0.00/0.14	     c -> a,
0.00/0.14	     d -> a,
0.00/0.14	     d -> e,
0.00/0.14	     g(?x) -> h(a),
0.00/0.14	     h(?x) -> e ]
0.00/0.14	Try persistent and layer-preserving decomposition...
0.00/0.14	Sort Assignment:
0.00/0.14	 a : =>12
0.00/0.14	 b : =>12
0.00/0.14	 c : =>12
0.00/0.14	 d : =>12
0.00/0.14	 e : =>12
0.00/0.14	 g : 8=>12
0.00/0.14	 h : 12=>12
0.00/0.14	maximal types: {8,12}
0.00/0.14	...decomposition failed.
0.00/0.14	TRS:
0.00/0.14	   [ a -> b,
0.00/0.14	     a -> c,
0.00/0.14	     a -> e,
0.00/0.14	     b -> d,
0.00/0.14	     c -> a,
0.00/0.14	     d -> a,
0.00/0.14	     d -> e,
0.00/0.14	     g(?x) -> h(a),
0.00/0.14	     h(?x) -> e ]
0.00/0.14	Input:
0.00/0.14	   [ a -> b,
0.00/0.14	     a -> c,
0.00/0.14	     a -> e,
0.00/0.14	     b -> d,
0.00/0.14	     c -> a,
0.00/0.14	     d -> a,
0.00/0.14	     d -> e,
0.00/0.14	     g(?x) -> h(a),
0.00/0.14	     h(?x) -> e ]
0.00/0.14	
0.00/0.14	Make it flat:
0.00/0.14	   [ a -> b,
0.00/0.14	     a -> c,
0.00/0.14	     a -> e,
0.00/0.14	     b -> d,
0.00/0.14	     c -> a,
0.00/0.14	     d -> a,
0.00/0.14	     d -> e,
0.00/0.14	     g(?x) -> h(a),
0.00/0.14	     h(?x) -> e ]
0.00/0.14	Time: 0.000 [s]
0.00/0.14	
0.00/0.14	Make it Complete (R^):
0.00/0.14	   [ a = b,
0.00/0.14	     h(c) = g(?x),
0.00/0.14	     h(c) = h(?x_1),
0.00/0.14	     h(c) = e,
0.00/0.14	     h(c) = d,
0.00/0.14	     c = d,
0.00/0.14	     c = h(?x),
0.00/0.14	     h(c) = a,
0.00/0.14	     c = h(a),
0.00/0.14	     c = h(d),
0.00/0.14	     h(c) = h(d),
0.00/0.14	     h(c) = h(e),
0.00/0.14	     c = h(e),
0.00/0.14	     c = g(?x),
0.00/0.14	     h(c) = h(b),
0.00/0.14	     c = h(b),
0.00/0.14	     c = h(c),
0.00/0.14	     h(c) = b,
0.00/0.14	     h(c) = h(a),
0.00/0.14	     c = b,
0.00/0.14	     c = e,
0.00/0.14	     a = c,
0.00/0.14	     a = e,
0.00/0.14	     b = e,
0.00/0.14	     b = g(?x),
0.00/0.14	     b = h(a),
0.00/0.14	     b = h(?x),
0.00/0.14	     h(b) = a,
0.00/0.14	     h(b) = h(a),
0.00/0.14	     b = h(e),
0.00/0.14	     h(b) = h(e),
0.00/0.14	     b = h(d),
0.00/0.14	     b = h(b),
0.00/0.14	     h(b) = d,
0.00/0.14	     h(b) = e,
0.00/0.14	     h(b) = h(?x_1),
0.00/0.14	     h(b) = h(d),
0.00/0.14	     h(b) = g(?x),
0.00/0.14	     b = d,
0.00/0.14	     h(d) = g(?x),
0.00/0.14	     h(d) = h(?x_1),
0.00/0.14	     h(d) = e,
0.00/0.14	     h(d) = d,
0.00/0.14	     a = g(?x),
0.00/0.14	     h(e) = a,
0.00/0.14	     h(d) = h(e),
0.00/0.14	     h(e) = e,
0.00/0.14	     h(e) = h(?x_1),
0.00/0.14	     h(e) = g(?x_1),
0.00/0.14	     h(e) = d,
0.00/0.14	     h(e) = h(a),
0.00/0.14	     h(d) = h(a),
0.00/0.14	     h(d) = a,
0.00/0.14	     a = h(a),
0.00/0.14	     a = h(?x),
0.00/0.14	     d = a,
0.00/0.14	     d = h(?x),
0.00/0.14	     d = h(a),
0.00/0.14	     d = g(?x),
0.00/0.14	     d = e,
0.00/0.14	     g(?x) = e,
0.00/0.14	     h(a) = e,
0.00/0.14	     h(?x_1) = h(a),
0.00/0.14	     g(?x) = h(?x_1),
0.00/0.14	     g(?x) = g(?x_1),
0.00/0.14	     g(?x) = h(a),
0.00/0.14	     h(?x) = h(?x_1),
0.00/0.14	     h(?x) = e ]
0.00/0.14	Time: 0.093 [s]
0.00/0.14	
0.00/0.14	CPNF:
0.00/0.14	   [ a … e ]
0.00/0.14	Time: 0.000 [s]
0.00/0.14	
0.00/0.14	Now checking all the pairs in CW...
0.00/0.14	
0.00/0.14	Time to check pairs: 0.000 [s]
0.00/0.14	
0.00/0.14	The TRS has Uniqueness of Normal Forms.
0.00/0.14	/export/starexec/sandbox/benchmark/theBenchmark.trs: Success(UNC)
0.00/0.14	(91 msec.)
0.00/0.14	EOF