Categories – INF
The INF category deals with infeasibility problems.
Format
The input is an infeasibility problem specified in the ARI
INF format. The question to be answered is
whether the condition contained in the problem is infeasible:
YES
if no satisfying substitution exists, NO
if a satisfying substitution exists. The equality sign in the condition is
interpreted as reachability if the rewrite system contained in the problem
is a TRS or an oriented CTRS. For semiequational (join) CTRSs the equality
sign is interpreted as conversion (joinability).
Examples

; origin COPS 547 (format CTRS oriented :problem infeasibility) (fun a 0) (fun b 0) (fun f 1) (rule (f x) a (= x a)) (rule (f x) b (= x b)) (infeasible? (= x a) (= x b))
The correct answer isYES
. 
; origin COPS 47 (format TRS :problem infeasibility) (fun A 0) (fun C 0) (fun F 2) (fun G 1) (rule (F x x) A) (rule (G x) (F x (G x))) (rule C (G C)) (infeasible? (= (G A) A))
The correct answer isYES
.
Problem Selection
Problems are selected from those in the ARI database with the 'infeasibility' tag.