10.44/9.68	MAYBE
10.44/9.68	/export/starexec/sandbox2/benchmark/theBenchmark.trs
10.44/9.68	Input rules:
10.44/9.68	   [ g(f(a)) -> f(g(f(a))),
10.44/9.68	     g(f(a)) -> f(f(a)),
10.44/9.68	     f(f(a)) -> f(a) ]
10.44/9.68	Sorts having no ground terms: 
10.44/9.68	Rules applicable to ground terms:
10.44/9.68	   [ g(f(a)) -> f(g(f(a))),
10.44/9.68	     g(f(a)) -> f(f(a)),
10.44/9.68	     f(f(a)) -> f(a) ]
10.44/9.68	Constructor pattern: [g(?x_1),f(?x_1),a]
10.44/9.68	Defined pattern: []
10.44/9.68	Constructor subsystem:
10.44/9.68	   [ g(f(a)) -> f(g(f(a))),
10.44/9.68	     g(f(a)) -> f(f(a)),
10.44/9.68	     f(f(a)) -> f(a) ]
10.44/9.68	Modified Constructor subsystem:
10.44/9.68	   [ g(f(a)) -> f(g(f(a))),
10.44/9.68	     g(f(a)) -> f(f(a)),
10.44/9.68	     f(f(a)) -> f(a) ]
10.44/9.68	Find a quasi-ordering ...
10.44/9.68	order successfully found
10.44/9.68	Precedence:
10.44/9.68	 a : Mul;
10.44/9.68	 f : Mul,  g : Mul;
10.44/9.68	Rules:
10.44/9.68	   [ f(f(a)) -> f(a),
10.44/9.68	     g(f(a)) -> f(f(a)) ]
10.44/9.68	Check confluence of constructor subsystem...
10.44/9.68	Check Termination...
10.44/9.68	unknown Terminating, Linear, Oostrom: CR
10.44/9.68	Conjectures:
10.44/9.68	   [ g(f(a)) = f(g(f(a))) ]
10.44/9.68	STEP 0
10.44/9.68	ES:
10.44/9.68	   [ g(f(a)) = f(g(f(a))) ]
10.44/9.68	HS:
10.44/9.68	   [ ]
10.44/9.68	ES0:
10.44/9.68	   [ g(f(a)) = f(g(f(a))) ]
10.44/9.68	HS0:
10.44/9.68	   [ ]
10.44/9.68	ES1:
10.44/9.68	   [ g(f(a)) = f(g(f(a))) ]
10.44/9.68	HS1:
10.44/9.68	   [ ]
10.44/9.68	No equation to expand
10.44/9.68	check Non-Ground-Confluence...
10.44/9.69	ground constructor terms for instantiation: {a,g(a),f(a)}
10.44/9.69	ground terms for instantiation: {a:o,g(a):o,f(a):o}
10.44/9.69	obtain 10 rules by 3 steps unfolding
10.44/9.69	obtain 33 candidates for checking non-joinability
10.44/9.69	check by TCAP-Approximation (failure)
10.44/9.69	check by Ordering(rpo), check by Tree-Automata Approximation (failure)
10.44/9.69	check by Interpretation(mod2) (failure)
10.44/9.69	check by Descendants-Approximation, check by Ordering(poly) (failure)
10.44/9.69	: Failure(unknown)
10.44/9.69	(2071 msec.)
10.44/9.69	
10.44/9.69	=============================
10.44/9.69	Total: 0 Success, 1 Failure: 2072 millisec.
10.44/9.69	EOF