YES Problem 1: Infeasibility Problem: [(VAR vNonEmpty x vNonEmpty x) (STRATEGY CONTEXTSENSITIVE (a) (b) (c) (d) (e) (fSNonEmpty) ) (RULES a -> a | b ->* x, c ->* x b -> d | d ->* x, e ->* x c -> d | d ->* x, e ->* x ) ] Infeasibility Conditions: b ->* x, c ->* x Problem 1: Obtaining a model using Mace4: -> Usable Rules: b -> d | d ->* x, e ->* x c -> d | d ->* x, e ->* x -> Mace4 Output: ============================== Mace4 ================================= Mace4 (64) version 2009-11A, November 2009. Process 3121388 was started by sandbox on z001.star.cs.uiowa.edu, Tue Jul 30 08:22:40 2024 The command was "./mace4 -c -f /tmp/mace43121373-2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file /tmp/mace43121373-2.in assign(max_seconds,100). formulas(assumptions). ->*(d,x1) & ->*(e,x1) -> ->(b,d) # label(replacement). ->*(d,x1) & ->*(e,x1) -> ->(c,d) # label(replacement). ->*(x,x) # label(reflexivity). ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). end_of_list. formulas(goals). (exists x3 (->*(b,x3) & ->*(c,x3))) # label(goal). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 ->*(d,x1) & ->*(e,x1) -> ->(b,d) # label(replacement) # label(non_clause). [assumption]. 2 ->*(d,x1) & ->*(e,x1) -> ->(c,d) # label(replacement) # label(non_clause). [assumption]. 3 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 4 (exists x3 (->*(b,x3) & ->*(c,x3))) # label(goal) # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== CLAUSES FOR SEARCH ==================== formulas(mace4_clauses). -->*(d,x) | -->*(e,x) | ->(b,d) # label(replacement). -->*(d,x) | -->*(e,x) | ->(c,d) # label(replacement). ->*(x,x) # label(reflexivity). -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). -->*(b,x) | -->*(c,x) # label(goal). end_of_list. ============================== end of clauses for search ============= % There are no natural numbers in the input. ============================== DOMAIN SIZE 2 ========================= ============================== MODEL ================================= interpretation( 2, [number=1, seconds=0], [ function(b, [ 0 ]), function(c, [ 1 ]), function(d, [ 0 ]), function(e, [ 1 ]), relation(->*(_,_), [ 1, 0, 0, 1 ]), relation(->(_,_), [ 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 2. Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). Ground clauses: seen=16, kept=12. Selections=4, assignments=4, propagations=8, current_models=1. Rewrite_terms=20, rewrite_bools=22, indexes=4. Rules_from_neg_clauses=2, cross_offs=2. ============================== end of statistics ===================== User_CPU=0.00, System_CPU=0.00, Wall_clock=0. Exiting with 1 model. Process 3121388 exit (max_models) Tue Jul 30 08:22:40 2024 The process finished Tue Jul 30 08:22:40 2024 Mace4 cooked interpretation: % number = 1 % seconds = 0 % Interpretation of size 2 b = 0. c = 1. d = 0. e = 1. ->*(0,0). - ->*(0,1). - ->*(1,0). ->*(1,1). - ->(0,0). - ->(0,1). - ->(1,0). - ->(1,1). The problem is infeasible.