YES Problem 1: Infeasibility Problem: [(VAR vNonEmpty vNonEmpty) (STRATEGY CONTEXTSENSITIVE (a) (b) (c) (fSNonEmpty) ) (RULES a -> b a -> c b -> c | b ->* c ) ] Infeasibility Conditions: b ->* c Problem 1: Obtaining a model using Mace4: -> Usable Rules: b -> c | b ->* c -> Mace4 Output: ============================== Mace4 ================================= Mace4 (64) version 2009-11A, November 2009. Process 3355955 was started by sandbox2 on z002.star.cs.uiowa.edu, Tue Jul 30 09:32:55 2024 The command was "./mace4 -c -f /tmp/mace43355942-2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file /tmp/mace43355942-2.in assign(max_seconds,100). formulas(assumptions). ->*(b,c) -> ->(b,c) # label(replacement). ->*(x,x) # label(reflexivity). ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). end_of_list. formulas(goals). ->*(b,c) # label(goal). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 ->*(b,c) -> ->(b,c) # label(replacement) # label(non_clause). [assumption]. 2 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 3 ->*(b,c) # label(goal) # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== CLAUSES FOR SEARCH ==================== formulas(mace4_clauses). -->*(b,c) | ->(b,c) # label(replacement). ->*(x,x) # label(reflexivity). -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). -->*(b,c) # 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 ]), 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.01 seconds). Ground clauses: seen=12, kept=8. Selections=4, assignments=4, propagations=6, current_models=1. Rewrite_terms=6, rewrite_bools=12, indexes=2. Rules_from_neg_clauses=1, cross_offs=1. ============================== end of statistics ===================== User_CPU=0.01, System_CPU=0.00, Wall_clock=0. Exiting with 1 model. Process 3355955 exit (max_models) Tue Jul 30 09:32:55 2024 The process finished Tue Jul 30 09:32:55 2024 Mace4 cooked interpretation: % number = 1 % seconds = 0 % Interpretation of size 2 b = 0. c = 1. ->*(0,0). - ->*(0,1). - ->*(1,0). ->*(1,1). - ->(0,0). - ->(0,1). - ->(1,0). - ->(1,1). The problem is infeasible.