0.00/0.03	YES
0.00/0.03	(ignored inputs)COMMENT doi:10.1007/11805618_6 [7] Example 3 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama
0.00/0.03	input TRS:
0.00/0.03	   [ b -> a,
0.00/0.03	     b -> c,
0.00/0.03	     c -> h(b),
0.00/0.03	     c -> d,
0.00/0.03	     a -> h(a),
0.00/0.03	     d -> h(d) ]
0.00/0.03	Try persistent and layer-preserving decomposition...
0.00/0.03	Sort Assignment:
0.00/0.03	 a : =>7
0.00/0.03	 b : =>7
0.00/0.03	 c : =>7
0.00/0.03	 d : =>7
0.00/0.03	 h : 7=>7
0.00/0.03	maximal types: {7}
0.00/0.03	...decomposition failed.
0.00/0.03	TRS:
0.00/0.03	   [ b -> a,
0.00/0.03	     b -> c,
0.00/0.03	     c -> h(b),
0.00/0.03	     c -> d,
0.00/0.03	     a -> h(a),
0.00/0.03	     d -> h(d) ]
0.00/0.03	Input:
0.00/0.03	   [ b -> a,
0.00/0.03	     b -> c,
0.00/0.03	     c -> h(b),
0.00/0.03	     c -> d,
0.00/0.03	     a -> h(a),
0.00/0.03	     d -> h(d) ]
0.00/0.03	
0.00/0.03	Make it flat:
0.00/0.03	   [ b -> a,
0.00/0.03	     b -> c,
0.00/0.03	     c -> h(b),
0.00/0.03	     c -> d,
0.00/0.03	     a -> h(a),
0.00/0.03	     d -> h(d) ]
0.00/0.03	Time: 0.000 [s]
0.00/0.03	
0.00/0.03	Make it Complete (R^):
0.00/0.03	   [ h(b) = a,
0.00/0.03	     b = h(a),
0.00/0.03	     h(a) = c,
0.00/0.03	     h(a) = h(c),
0.00/0.03	     h(a) = h(d),
0.00/0.03	     h(a) = d,
0.00/0.03	     a = c,
0.00/0.03	     a = h(c),
0.00/0.03	     a = h(d),
0.00/0.03	     h(a) = h(b),
0.00/0.03	     a = d,
0.00/0.03	     b = a,
0.00/0.03	     b = d,
0.00/0.03	     b = h(d),
0.00/0.03	     b = h(c),
0.00/0.03	     b = h(b),
0.00/0.03	     b = c,
0.00/0.03	     d = h(b),
0.00/0.03	     h(b) = h(d),
0.00/0.03	     h(b) = h(c),
0.00/0.03	     c = h(b),
0.00/0.03	     h(c) = d,
0.00/0.03	     h(c) = h(d),
0.00/0.03	     h(c) = c,
0.00/0.03	     c = h(d),
0.00/0.03	     c = d,
0.00/0.03	     a = h(a),
0.00/0.03	     d = h(d) ]
0.00/0.03	Time: 0.006 [s]
0.00/0.03	
0.00/0.03	CPNF:
0.00/0.03	   [  ]
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	(6 msec.)
0.00/0.03	EOF