0.00/0.09	NO
0.00/0.09	(ignored inputs)COMMENT Cops #647 - #721: generated ground TRSs; evenly distributed in the UNR/UNC/NFP/CR hierarchy submitted by: Bertram Felgenhauer
0.00/0.09	input TRS:
0.00/0.09	   [ a -> f(b),
0.00/0.09	     h(b,f(c)) -> c,
0.00/0.09	     b -> f(b),
0.00/0.09	     b -> f(c),
0.00/0.09	     h(c,c) -> c ]
0.00/0.09	unknown Strongly Non-Overlapping
0.00/0.09	unknown Right-Reducible
0.00/0.09	Call a UNC decision procedure for shallow TRSs...
0.00/0.09	Input:
0.00/0.09	   [ a -> f(b),
0.00/0.09	     h(b,f(c)) -> c,
0.00/0.09	     b -> f(b),
0.00/0.09	     b -> f(c),
0.00/0.09	     h(c,c) -> c ]
0.00/0.09	
0.00/0.09	Make it flat:
0.00/0.09	   [ h(b,!cl_0) -> c,
0.00/0.09	     a -> f(b),
0.00/0.09	     f(c) -> !cl_0,
0.00/0.09	     h(c,c) -> c,
0.00/0.09	     b -> f(c),
0.00/0.09	     b -> f(b) ]
0.00/0.09	Time: 0.000 [s]
0.00/0.09	
0.00/0.09	Make it Complete (R^):
0.00/0.09	   [ h(!cl_0,!cl_0) = c,
0.00/0.09	     h(b,b) = c,
0.00/0.09	     h(b,a) = c,
0.00/0.09	     h(a,!cl_0) = c,
0.00/0.09	     h(!cl_0,!cl_0) = h(c,c),
0.00/0.09	     h(b,b) = h(c,c),
0.00/0.09	     h(b,a) = h(c,c),
0.00/0.09	     h(a,b) = h(c,c),
0.00/0.09	     h(a,a) = h(c,c),
0.00/0.09	     h(!cl_0,!cl_0) = h(a,!cl_0),
0.00/0.09	     h(b,b) = h(a,!cl_0),
0.00/0.09	     h(b,a) = h(a,!cl_0),
0.00/0.09	     h(a,b) = h(b,!cl_0),
0.00/0.09	     h(a,a) = h(b,!cl_0),
0.00/0.09	     h(b,b) = h(!cl_0,!cl_0),
0.00/0.09	     h(b,a) = h(!cl_0,!cl_0),
0.00/0.09	     h(!cl_0,b) = h(b,!cl_0),
0.00/0.09	     h(!cl_0,!cl_0) = h(!cl_0,a),
0.00/0.09	     h(b,b) = h(!cl_0,a),
0.00/0.09	     h(b,a) = h(!cl_0,a),
0.00/0.09	     h(a,!cl_0) = h(!cl_0,a),
0.00/0.09	     h(b,a) = h(b,!cl_0),
0.00/0.09	     h(!cl_0,a) = c,
0.00/0.09	     h(a,b) = c,
0.00/0.09	     c = h(a,a),
0.00/0.09	     h(!cl_0,b) = c,
0.00/0.09	     h(!cl_0,b) = h(a,!cl_0),
0.00/0.09	     h(b,a) = h(!cl_0,b),
0.00/0.09	     h(a,a) = h(!cl_0,b),
0.00/0.09	     h(!cl_0,!cl_0) = h(!cl_0,b),
0.00/0.09	     h(b,a) = h(a,b),
0.00/0.09	     h(a,a) = h(a,b),
0.00/0.09	     h(!cl_0,!cl_0) = h(a,b),
0.00/0.09	     h(!cl_0,b) = h(a,b),
0.00/0.09	     h(!cl_0,b) = h(b,b),
0.00/0.09	     h(a,b) = h(b,b),
0.00/0.09	     h(b,!cl_0) = h(b,b),
0.00/0.09	     h(b,a) = h(b,b),
0.00/0.09	     h(b,b) = h(a,a),
0.00/0.09	     h(b,a) = h(a,a),
0.00/0.09	     h(a,b) = h(a,!cl_0),
0.00/0.09	     h(a,!cl_0) = h(a,a),
0.00/0.09	     h(!cl_0,!cl_0) = h(a,a),
0.00/0.09	     h(a,a) = h(!cl_0,a),
0.00/0.09	     h(a,b) = h(!cl_0,a),
0.00/0.09	     h(!cl_0,b) = h(!cl_0,a),
0.00/0.09	     h(!cl_0,b) = h(c,c),
0.00/0.09	     h(!cl_0,a) = h(c,c),
0.00/0.09	     h(!cl_0,a) = h(b,!cl_0),
0.00/0.09	     h(!cl_0,!cl_0) = h(b,!cl_0),
0.00/0.09	     h(a,!cl_0) = h(b,!cl_0),
0.00/0.09	     h(a,!cl_0) = h(c,c),
0.00/0.09	     h(b,!cl_0) = h(c,c),
0.00/0.09	     h(b,!cl_0) = c,
0.00/0.09	     f(!cl_0) = a,
0.00/0.09	     a = b,
0.00/0.09	     a = f(c),
0.00/0.09	     f(a) = !cl_0,
0.00/0.09	     f(a) = a,
0.00/0.09	     f(a) = f(b),
0.00/0.09	     f(a) = f(c),
0.00/0.09	     f(a) = f(!cl_0),
0.00/0.09	     f(a) = b,
0.00/0.09	     a = !cl_0,
0.00/0.09	     a = f(b),
0.00/0.09	     f(!cl_0) = b,
0.00/0.09	     f(!cl_0) = f(c),
0.00/0.09	     f(!cl_0) = f(b),
0.00/0.09	     f(!cl_0) = !cl_0,
0.00/0.09	     !cl_0 = b,
0.00/0.09	     !cl_0 = f(b),
0.00/0.09	     f(c) = !cl_0,
0.00/0.09	     h(c,c) = c,
0.00/0.09	     f(c) = f(b),
0.00/0.09	     b = f(c),
0.00/0.09	     b = f(b) ]
0.00/0.09	Time: 0.047 [s]
0.00/0.09	
0.00/0.09	CPNF:
0.00/0.09	   [ !cl_0 … f(!cl_0),
0.00/0.09	     !cl_0 … !cl_0,
0.00/0.09	     c … c ]
0.00/0.09	Time: 0.000 [s]
0.00/0.09	
0.00/0.09	The TRS doesn't have Uniqueness of Normal Forms.
0.00/0.09	Counter Example: 
0.00/0.09	     f(!cl_0)
0.00/0.09	<->* !cl_0
0.00/0.09	
0.00/0.09	proof:
0.00/0.09	     f(!cl_0)
0.00/0.09	->R^ !cl_0
0.00/0.09	
0.00/0.09	     !cl_0
0.00/0.09	Total Time: 0.048 [s]
0.00/0.09	
0.00/0.09	...Not UNC found by the decision procedure.
0.00/0.09	Check distinct normal forms in critical pair closure
0.00/0.09	distinct normal forms of a term: f(f(c)) = f(f(f(c)))
0.00/0.09	/export/starexec/sandbox/benchmark/theBenchmark.trs: Success(not UNR)
0.00/0.09	(47 msec.)
0.00/0.09	EOF