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