30.01/20.26 NO 30.01/20.26 30.01/20.26 Problem 1: 30.01/20.26 30.01/20.26 30.01/20.26 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 30.01/20.26 Confluence Problem: 30.01/20.26 (VAR vNonEmpty) 30.01/20.26 (REPLACEMENT-MAP 30.01/20.26 (a) 30.01/20.26 (f 1, 2) 30.01/20.26 (b) 30.01/20.26 (fSNonEmpty) 30.01/20.26 ) 30.01/20.26 (RULES 30.01/20.26 a -> f(a,b) 30.01/20.26 f(a,b) -> f(b,a) 30.01/20.26 ) 30.01/20.26 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 30.01/20.26 30.01/20.26 30.01/20.26 Problem 1: 30.01/20.26 30.01/20.26 Problem 1: 30.01/20.26 Not CS-TRS Procedure: 30.01/20.26 R is not a CS-TRS 30.01/20.26 30.01/20.26 Problem 1: 30.01/20.26 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 30.01/20.26 Confluence Problem: 30.01/20.26 (VAR vNonEmpty) 30.01/20.26 (REPLACEMENT-MAP 30.01/20.26 (a) 30.01/20.26 (f 1, 2) 30.01/20.26 (b) 30.01/20.26 (fSNonEmpty) 30.01/20.26 ) 30.01/20.26 (RULES 30.01/20.26 a -> f(a,b) 30.01/20.26 f(a,b) -> f(b,a) 30.01/20.26 ) 30.01/20.26 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 30.01/20.26 30.01/20.26 Huet Levy Ordered by Num of Vars and Symbs Procedure: 30.01/20.26 -> Rules: 30.01/20.26 a -> f(a,b) 30.01/20.26 f(a,b) -> f(b,a) 30.01/20.26 -> Vars: 30.01/20.26 30.01/20.26 30.01/20.26 -> Rlps: 30.01/20.26 (rule: a -> f(a,b), id: 1, possubterms: a->[]) 30.01/20.26 (rule: f(a,b) -> f(b,a), id: 2, possubterms: f(a,b)->[], a->[1], b->[2]) 30.01/20.26 30.01/20.26 -> Unifications: 30.01/20.26 (R2 unifies with R1 at p: [1], l: f(a,b), lp: a, sig: {}, l': a, r: f(b,a), r': f(a,b)) 30.01/20.26 30.01/20.26 -> Critical pairs info: 30.01/20.26 => Not trivial, Not overlay, Proper, NW0, N1 30.01/20.26 30.01/20.26 -> Problem conclusions: 30.01/20.26 Left linear, Right linear, Linear 30.01/20.26 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 30.01/20.26 Not Huet-Levy confluent, Not Newman confluent 30.01/20.26 R is a TRS 30.01/20.26 30.01/20.26 30.01/20.26 Problem 1: 30.01/20.26 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 30.01/20.26 Confluence Problem: 30.01/20.26 (REPLACEMENT-MAP 30.01/20.26 (a) 30.01/20.26 (f 1, 2) 30.01/20.26 (b) 30.01/20.26 (fSNonEmpty) 30.01/20.26 ) 30.01/20.26 (RULES 30.01/20.26 a -> f(a,b) 30.01/20.26 f(a,b) -> f(b,a) 30.01/20.26 ) 30.01/20.26 Critical Pairs: 30.01/20.26 => Not trivial, Not overlay, Proper, NW0, N1 30.01/20.26 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 30.01/20.26 30.01/20.26 No Convergence InfChecker Procedure: 30.01/20.26 Infeasible convergence? 30.01/20.26 YES 30.01/20.26 30.01/20.26 Problem 1: 30.01/20.26 30.01/20.26 Infeasibility Problem: 30.01/20.26 [(VAR vNonEmpty vNonEmpty z0) 30.01/20.26 (STRATEGY CONTEXTSENSITIVE 30.01/20.26 (a) 30.01/20.26 (f 1 2) 30.01/20.26 (b) 30.01/20.26 (fSNonEmpty) 30.01/20.26 ) 30.01/20.26 (RULES 30.01/20.26 a -> f(a,b) 30.01/20.26 f(a,b) -> f(b,a) 30.01/20.26 )] 30.01/20.26 Infeasibility Conditions: 30.01/20.26 f(f(a,b),b) ->* z0, f(b,a) ->* z0 30.01/20.26 30.01/20.26 Problem 1: 30.01/20.26 30.01/20.26 Obtaining a model using Mace4: 30.01/20.26 30.01/20.26 -> Usable Rules: 30.01/20.26 a -> f(a,b) 30.01/20.26 f(a,b) -> f(b,a) 30.01/20.26 30.01/20.26 -> Mace4 Output: 30.01/20.26 ============================== Mace4 ================================= 30.01/20.26 Mace4 (64) version 2009-11A, November 2009. 30.01/20.26 Process 41047 was started by sandbox2 on n092.star.cs.uiowa.edu, 30.01/20.26 Wed Jul 13 07:23:45 2022 30.01/20.26 The command was "./mace4 -c -f /tmp/mace441033.in". 30.01/20.26 ============================== end of head =========================== 30.01/20.26 30.01/20.26 ============================== INPUT ================================= 30.01/20.26 30.01/20.26 % Reading from file /tmp/mace441033.in 30.01/20.26 30.01/20.26 assign(max_seconds,10). 30.01/20.26 30.01/20.26 formulas(assumptions). 30.01/20.26 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence). 30.01/20.26 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence). 30.01/20.26 ->(a,f(a,b)) # label(replacement). 30.01/20.26 ->(f(a,b),f(b,a)) # label(replacement). 30.01/20.26 ->*(x,x) # label(reflexivity). 30.01/20.26 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 30.01/20.26 end_of_list. 30.01/20.26 30.01/20.26 formulas(goals). 30.01/20.26 (exists x2 (->*(f(f(a,b),b),x2) & ->*(f(b,a),x2))) # label(goal). 30.01/20.26 end_of_list. 30.01/20.26 30.01/20.26 ============================== end of input ========================== 30.01/20.26 30.01/20.26 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 30.01/20.26 30.01/20.26 % Formulas that are not ordinary clauses: 30.01/20.26 1 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 30.01/20.26 2 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 30.01/20.26 3 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 30.01/20.26 4 (exists x2 (->*(f(f(a,b),b),x2) & ->*(f(b,a),x2))) # label(goal) # label(non_clause) # label(goal). [goal]. 30.01/20.26 30.01/20.26 ============================== end of process non-clausal formulas === 30.01/20.26 30.01/20.26 ============================== CLAUSES FOR SEARCH ==================== 30.01/20.26 30.01/20.26 formulas(mace4_clauses). 30.01/20.26 -->(x,y) | ->(f(x,z),f(y,z)) # label(congruence). 30.01/20.26 -->(x,y) | ->(f(z,x),f(z,y)) # label(congruence). 30.01/20.26 ->(a,f(a,b)) # label(replacement). 30.01/20.26 ->(f(a,b),f(b,a)) # label(replacement). 30.01/20.26 ->*(x,x) # label(reflexivity). 30.01/20.26 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 30.01/20.26 -->*(f(f(a,b),b),x) | -->*(f(b,a),x) # label(goal). 30.01/20.26 end_of_list. 30.01/20.26 30.01/20.26 ============================== end of clauses for search ============= 30.01/20.26 30.01/20.26 % There are no natural numbers in the input. 30.01/20.26 30.01/20.26 ============================== DOMAIN SIZE 2 ========================= 30.01/20.26 30.01/20.26 ============================== STATISTICS ============================ 30.01/20.26 30.01/20.26 For domain size 2. 30.01/20.26 30.01/20.26 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 30.01/20.26 Ground clauses: seen=30, kept=26. 30.01/20.26 Selections=11, assignments=21, propagations=42, current_models=0. 30.01/20.26 Rewrite_terms=246, rewrite_bools=149, indexes=70. 30.01/20.26 Rules_from_neg_clauses=12, cross_offs=12. 30.01/20.26 30.01/20.26 ============================== end of statistics ===================== 30.01/20.26 30.01/20.26 ============================== DOMAIN SIZE 3 ========================= 30.01/20.26 30.01/20.26 ============================== STATISTICS ============================ 30.01/20.26 30.01/20.26 For domain size 3. 30.01/20.26 30.01/20.26 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 30.01/20.26 Ground clauses: seen=89, kept=80. 30.01/20.26 Selections=32, assignments=89, propagations=310, current_models=0. 30.01/20.26 Rewrite_terms=1616, rewrite_bools=1158, indexes=490. 30.01/20.26 Rules_from_neg_clauses=41, cross_offs=105. 30.01/20.26 30.01/20.26 ============================== end of statistics ===================== 30.01/20.26 30.01/20.26 ============================== DOMAIN SIZE 4 ========================= 30.01/20.26 30.01/20.26 ============================== STATISTICS ============================ 30.01/20.26 30.01/20.26 For domain size 4. 30.01/20.26 30.01/20.26 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 30.01/20.26 Ground clauses: seen=202, kept=186. 30.01/20.26 Selections=114, assignments=425, propagations=1842, current_models=0. 30.01/20.26 Rewrite_terms=8274, rewrite_bools=10242, indexes=2587. 30.01/20.26 Rules_from_neg_clauses=142, cross_offs=755. 30.01/20.26 30.01/20.26 ============================== end of statistics ===================== 30.01/20.26 30.01/20.26 ============================== DOMAIN SIZE 5 ========================= 30.01/20.26 30.01/20.26 ============================== MODEL ================================= 30.01/20.26 30.01/20.26 interpretation( 5, [number=1, seconds=0], [ 30.01/20.26 30.01/20.26 function(a, [ 0 ]), 30.01/20.26 30.01/20.26 function(b, [ 1 ]), 30.01/20.26 30.01/20.26 function(f(_,_), [ 30.01/20.26 0, 2, 2, 2, 2, 30.01/20.26 3, 0, 3, 3, 3, 30.01/20.26 2, 4, 2, 2, 2, 30.01/20.26 2, 4, 2, 2, 2, 30.01/20.26 2, 4, 2, 2, 2 ]), 30.01/20.26 30.01/20.26 relation(->*(_,_), [ 30.01/20.26 1, 0, 1, 1, 1, 30.01/20.26 0, 1, 0, 0, 0, 30.01/20.26 0, 0, 1, 1, 1, 30.01/20.26 0, 0, 0, 1, 0, 30.01/20.26 0, 0, 0, 0, 1 ]), 30.01/20.26 30.01/20.26 relation(->(_,_), [ 30.01/20.26 0, 0, 1, 0, 0, 30.01/20.26 0, 0, 0, 0, 0, 30.01/20.26 0, 0, 1, 1, 1, 30.01/20.26 0, 0, 0, 1, 0, 30.01/20.26 0, 0, 0, 0, 1 ]) 30.01/20.26 ]). 30.01/20.26 30.01/20.26 ============================== end of model ========================== 30.01/20.26 30.01/20.26 ============================== STATISTICS ============================ 30.01/20.26 30.01/20.26 For domain size 5. 30.01/20.26 30.01/20.26 Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). 30.01/20.26 Ground clauses: seen=387, kept=362. 30.01/20.26 Selections=59, assignments=180, propagations=492, current_models=1. 30.01/20.26 Rewrite_terms=3116, rewrite_bools=3334, indexes=667. 30.01/20.26 Rules_from_neg_clauses=46, cross_offs=405. 30.01/20.26 30.01/20.26 ============================== end of statistics ===================== 30.01/20.26 30.01/20.26 User_CPU=0.01, System_CPU=0.00, Wall_clock=0. 30.01/20.26 30.01/20.26 Exiting with 1 model. 30.01/20.26 30.01/20.26 Process 41047 exit (max_models) Wed Jul 13 07:23:45 2022 30.01/20.26 The process finished Wed Jul 13 07:23:45 2022 30.01/20.26 30.01/20.26 30.01/20.26 Mace4 cooked interpretation: 30.01/20.26 30.01/20.26 30.01/20.26 30.01/20.26 The problem is infeasible. 30.01/20.26 30.01/20.26 30.01/20.26 The problem is not confluent. 30.01/20.26 EOF