YES Problem 1: Infeasibility Problem: [(VAR vNonEmpty x y z w vNonEmpty) (STRATEGY CONTEXTSENSITIVE (f 1 2) (a) (b) (fSNonEmpty) ) (RULES f(f(x,y),f(z,w)) -> f(f(x,z),f(y,w)) f(f(x,y),x) -> x ) ] Infeasibility Conditions: f(b,a) <-->* f(a,b) Problem 1: Obtaining a model using Mace4: -> Usable Rules: f(f(x,y),f(z,w)) -> f(f(x,z),f(y,w)) f(f(x,y),x) -> x -> Mace4 Output: ============================== Mace4 ================================= Mace4 (64) version 2009-11A, November 2009. Process 3365057 was started by sandbox on z010.star.cs.uiowa.edu, Tue Jul 30 09:26:40 2024 The command was "./mace4 -c -f /tmp/mace43365043-2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file /tmp/mace43365043-2.in assign(max_seconds,100). formulas(assumptions). ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence). ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence). ->(f(f(x1,x2),f(x3,x4)),f(f(x1,x3),f(x2,x4))) # label(replacement). ->(f(f(x1,x2),x1),x1) # label(replacement). ->(x,y) | ->(y,x) -> <-->(x,y) # label(convertibility). <-->*(x,x) # label(covertibility). <-->(x,y) & <-->*(y,z) -> <-->*(x,z) # label(convertibility). end_of_list. formulas(goals). <-->*(f(b,a),f(a,b)) # label(goal). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 2 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 3 ->(x,y) | ->(y,x) -> <-->(x,y) # label(convertibility) # label(non_clause). [assumption]. 4 <-->(x,y) & <-->*(y,z) -> <-->*(x,z) # label(convertibility) # label(non_clause). [assumption]. 5 <-->*(f(b,a),f(a,b)) # label(goal) # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== CLAUSES FOR SEARCH ==================== formulas(mace4_clauses). -->(x,y) | ->(f(x,z),f(y,z)) # label(congruence). -->(x,y) | ->(f(z,x),f(z,y)) # label(congruence). ->(f(f(x,y),f(z,u)),f(f(x,z),f(y,u))) # label(replacement). ->(f(f(x,y),x),x) # label(replacement). -->(x,y) | <-->(x,y) # label(convertibility). -->(x,y) | <-->(y,x) # label(convertibility). <-->*(x,x) # label(covertibility). -<-->(x,y) | -<-->*(y,z) | <-->*(x,z) # label(convertibility). -<-->*(f(b,a),f(a,b)) # 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(a, [ 0 ]), function(b, [ 1 ]), function(f(_,_), [ 0, 0, 1, 1 ]), relation(->(_,_), [ 1, 0, 0, 1 ]), relation(<-->*(_,_), [ 1, 0, 0, 1 ]), relation(<-->(_,_), [ 1, 0, 0, 1 ]) ]). ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 2. Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). Ground clauses: seen=55, kept=51. Selections=6, assignments=8, propagations=13, current_models=1. Rewrite_terms=148, rewrite_bools=71, indexes=12. 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 3365057 exit (max_models) Tue Jul 30 09:26:40 2024 The process finished Tue Jul 30 09:26:40 2024 Mace4 cooked interpretation: % number = 1 % seconds = 0 % Interpretation of size 2 a = 0. b = 1. f(0,0) = 0. f(0,1) = 0. f(1,0) = 1. f(1,1) = 1. ->(0,0). - ->(0,1). - ->(1,0). ->(1,1). <-->*(0,0). - <-->*(0,1). - <-->*(1,0). <-->*(1,1). <-->(0,0). - <-->(0,1). - <-->(1,0). <-->(1,1). The problem is infeasible.