140.49/60.05	ages: Error (SolverSMTExt callToBarcelogicNIA'): (line 1, column 1):
140.49/60.05	unexpected "s"
140.49/60.05	expecting "sat", "unsat" or "unknown"
140.49/60.05	YES
140.49/60.05	
140.49/60.05	Problem 1: 
140.49/60.05	
140.49/60.05	Infeasibility Problem:
140.49/60.05	[(VAR vNonEmpty x vNonEmpty x)
140.49/60.05	(STRATEGY CONTEXTSENSITIVE
140.49/60.05	(f 1)
140.49/60.05	(g 1)
140.49/60.05	(h 1)
140.49/60.05	(fSNonEmpty)
140.49/60.05	)
140.49/60.05	(RULES
140.49/60.05	f(g(h(x))) -> g(f(h(g(x))))
140.49/60.05	f(x) -> x
140.49/60.05	g(x) -> x
140.49/60.05	h(x) -> x
140.49/60.05	)]
140.49/60.05	Infeasibility Conditions:
140.49/60.05	f(g(h(x))) ->* g(f(g(h(x))))
140.49/60.05	
140.49/60.05	Problem 1: 
140.49/60.05	
140.49/60.05	Obtaining a model using AGES:
140.49/60.05	
140.49/60.05	 -> Theory (Usable Rules):
140.49/60.05	f(g(h(x))) -> g(f(h(g(x))))
140.49/60.05	f(x) -> x
140.49/60.05	g(x) -> x
140.49/60.05	h(x) -> x
140.49/60.05	
140.49/60.05	 -> AGES Output:
140.49/60.05	
140.49/60.05	
140.49/60.05	
140.49/60.05	
140.49/60.05	The problem is infeasible.
140.49/60.05	EOF