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