140.29/60.11	ages: Error (SolverSMTExt callToBarcelogicNIA'): (line 1, column 1):
140.29/60.11	unexpected "s"
140.29/60.11	expecting "sat", "unsat" or "unknown"
140.29/60.11	YES
140.29/60.11	
140.29/60.11	Problem 1: 
140.29/60.11	
140.29/60.11	Infeasibility Problem:
140.29/60.11	[(VAR vNonEmpty m n l vNonEmpty x1 x3)
140.29/60.11	(STRATEGY CONTEXTSENSITIVE
140.29/60.11	(insert 1 2)
140.29/60.11	(lte 1 2)
140.29/60.11	(ordered 1)
140.29/60.11	(0)
140.29/60.11	(cons 1 2)
140.29/60.11	(fSNonEmpty)
140.29/60.11	(false)
140.29/60.11	(nil)
140.29/60.11	(s 1)
140.29/60.11	(true)
140.29/60.11	)
140.29/60.11	(RULES
140.29/60.11	insert(cons(n,l),m) -> cons(m,cons(n,l)) | lte(m,n) ->* true
140.29/60.11	insert(cons(n,l),m) -> cons(n,insert(l,m)) | lte(m,n) ->* false
140.29/60.11	insert(nil,m) -> cons(m,nil)
140.29/60.11	lte(0,n) -> true
140.29/60.11	lte(s(m),0) -> false
140.29/60.11	lte(s(m),s(n)) -> lte(m,n)
140.29/60.11	ordered(cons(m,cons(n,l))) -> ordered(cons(n,l)) | lte(m,n) ->* true
140.29/60.11	ordered(cons(m,cons(n,l))) -> false | lte(m,n) ->* false
140.29/60.11	ordered(cons(m,nil)) -> true
140.29/60.11	ordered(nil) -> true
140.29/60.11	)]
140.29/60.11	
140.29/60.11	Infeasibility Conditions:
140.29/60.11	lte(x3,x1) ->* true, lte(x3,x1) ->* false
140.29/60.11	
140.29/60.11	Problem 1: 
140.29/60.11	
140.29/60.11	Obtaining a model using AGES:
140.29/60.11	
140.29/60.11	 -> Usable Rules:
140.29/60.11	
140.29/60.11	insert(cons(n,l),m) -> cons(m,cons(n,l)) | lte(m,n) ->* true
140.29/60.11	insert(cons(n,l),m) -> cons(n,insert(l,m)) | lte(m,n) ->* false
140.29/60.11	insert(nil,m) -> cons(m,nil)
140.29/60.11	lte(0,n) -> true
140.29/60.11	lte(s(m),0) -> false
140.29/60.11	lte(s(m),s(n)) -> lte(m,n)
140.29/60.11	ordered(cons(m,cons(n,l))) -> ordered(cons(n,l)) | lte(m,n) ->* true
140.29/60.11	ordered(cons(m,cons(n,l))) -> false | lte(m,n) ->* false
140.29/60.11	ordered(cons(m,nil)) -> true
140.29/60.11	ordered(nil) -> true
140.29/60.11	
140.29/60.11	 -> AGES Output:
140.29/60.11	
140.29/60.11	
140.29/60.11	
140.29/60.11	
140.29/60.11	The problem is infeasible.
140.29/60.12	EOF