0.00/0.02	NO
0.00/0.02	(ignored inputs)COMMENT [11] Example 3.3.1 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama
0.00/0.02	input TRS:
0.00/0.02	   [ b -> a,
0.00/0.02	     b -> c,
0.00/0.02	     c -> b,
0.00/0.02	     c -> d ]
0.00/0.02	Try persistent and layer-preserving decomposition...
0.00/0.02	Sort Assignment:
0.00/0.02	 a : =>5
0.00/0.02	 b : =>5
0.00/0.02	 c : =>5
0.00/0.02	 d : =>5
0.00/0.02	maximal types: {5}
0.00/0.02	...decomposition failed.
0.00/0.02	TRS:
0.00/0.02	   [ b -> a,
0.00/0.02	     b -> c,
0.00/0.02	     c -> b,
0.00/0.02	     c -> d ]
0.00/0.02	Input:
0.00/0.02	   [ b -> a,
0.00/0.02	     b -> c,
0.00/0.02	     c -> b,
0.00/0.02	     c -> d ]
0.00/0.02	
0.00/0.02	Make it flat:
0.00/0.02	   [ b -> a,
0.00/0.02	     b -> c,
0.00/0.02	     c -> b,
0.00/0.02	     c -> d ]
0.00/0.02	Time: 0.000 [s]
0.00/0.02	
0.00/0.02	Make it Complete (R^):
0.00/0.02	   [ a = c,
0.00/0.02	     a = d,
0.00/0.02	     b = a,
0.00/0.02	     b = d,
0.00/0.02	     b = c,
0.00/0.02	     c = d ]
0.00/0.02	Time: 0.000 [s]
0.00/0.02	
0.00/0.02	CPNF:
0.00/0.02	   [ a … a,
0.00/0.02	     a … d ]
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	     a
0.00/0.02	<->* d
0.00/0.02	
0.00/0.02	proof:
0.00/0.02	     a
0.00/0.02	
0.00/0.02	     d
0.00/0.02	->R^ c
0.00/0.02	->R^ b
0.00/0.02	->R^ a
0.00/0.02	/export/starexec/sandbox2/benchmark/theBenchmark.trs: Success(not UNC)
0.00/0.02	(0 msec.)
0.00/0.02	EOF