0.00/0.00	MAYBE
0.00/0.00	
0.00/0.00	Succeeded in reading "/export/starexec/sandbox/benchmark/theBenchmark.trs".
0.00/0.00	    (CONDITIONTYPE ORIENTED)
0.00/0.00	    (VAR x)
0.00/0.00	    (RULES
0.00/0.00	      f(g(h(x))) -> g(f(h(g(x))))
0.00/0.00	      f(x) -> x
0.00/0.00	      g(x) -> x
0.00/0.00	      h(x) -> x
0.00/0.00	    )
0.00/0.00	    (COMMENT COPS 1651)
0.00/0.00	    (COMMENT submitted by: Akihisa Yamada)
0.00/0.00	
0.00/0.00	No "->="-rules.
0.00/0.00	
0.00/0.00	Decomposed conditions and removed infeasible rules if possible.
0.00/0.00	    (VAR x)
0.00/0.00	    (RULES
0.00/0.00	      f(g(h(x))) -> g(f(h(g(x))))
0.00/0.00	      f(x) -> x
0.00/0.00	      g(x) -> x
0.00/0.00	      h(x) -> x
0.00/0.00	    )
0.00/0.00	    (COMMENT COPS 1651)
0.00/0.00	    (COMMENT submitted by: Akihisa Yamada)
0.00/0.00	
0.00/0.00	(VAR x)
0.00/0.00	(CONDITION 
0.00/0.00	f(g(h(x))) == g(f(g(h(x))))
0.00/0.00	)
0.00/0.00	
0.00/0.00	Optimized the infeasibility problem if possible.
0.00/0.00	
0.00/0.00	(VAR x)
0.00/0.00	(CONDITION 
0.00/0.00	f(g(h(x))) == g(f(g(h(x))))
0.00/0.00	)
0.00/0.00	
0.00/0.00	This is ultra-RL and deterministic.
0.00/0.00	
0.00/0.00	This is not operationally terminating and confluent.
0.00/0.00	
0.00/0.00	Failed to prove infeasibility of the linearized conditions by means of narrowing trees.
0.00/0.00	
0.00/0.00	This is not ultra-RL and deterministic.
0.00/0.00	
0.00/0.00	
0.00/0.00	MAYBE
0.00/0.00	EOF