45.054/45.054 NO 45.054/45.054 45.054/45.054 Problem 1: 45.054/45.054 45.054/45.054 45.054/45.054 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.054/45.054 Confluence Problem: 45.054/45.054 (VAR vNonEmpty:S x:S y:S z:S) 45.054/45.054 (STRATEGY CONTEXTSENSITIVE 45.054/45.054 (a) 45.054/45.054 (f 1 2) 45.054/45.054 (g 1 2) 45.054/45.054 (k 1) 45.054/45.054 (b) 45.054/45.054 (fSNonEmpty) 45.054/45.054 (h 1) 45.054/45.054 ) 45.054/45.054 (RULES 45.054/45.054 a -> b 45.054/45.054 f(k(a),h(a)) -> k(x:S) | a ->* x:S 45.054/45.054 f(k(z:S),a) -> g(x:S,x:S) | h(z:S) ->* x:S, x:S ->* b 45.054/45.054 g(x:S,x:S) -> a 45.054/45.054 k(x:S) -> a 45.054/45.054 k(x:S) -> b 45.054/45.054 k(x:S) -> h(x:S) 45.054/45.054 ) 45.054/45.054 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.054/45.054 45.054/45.054 45.054/45.054 Problem 1: 45.054/45.054 45.054/45.054 Inlining of Conditions Processor [STERN17]: 45.054/45.054 45.054/45.054 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.054/45.054 Confluence Problem: 45.054/45.054 (VAR vNonEmpty:S x:S y:S z:S) 45.054/45.054 (STRATEGY CONTEXTSENSITIVE 45.054/45.054 (a) 45.054/45.054 (f 1 2) 45.054/45.054 (g 1 2) 45.054/45.054 (k 1) 45.054/45.054 (b) 45.054/45.054 (fSNonEmpty) 45.054/45.054 (h 1) 45.054/45.054 ) 45.054/45.054 (RULES 45.054/45.054 a -> b 45.054/45.054 f(k(a),h(a)) -> k(a) 45.054/45.054 f(k(z:S),a) -> g(h(z:S),h(z:S)) | h(z:S) ->* b 45.054/45.054 g(x:S,x:S) -> a 45.054/45.054 k(x:S) -> a 45.054/45.054 k(x:S) -> b 45.054/45.054 k(x:S) -> h(x:S) 45.054/45.054 ) 45.054/45.054 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.054/45.054 45.054/45.054 45.054/45.054 Problem 1: 45.054/45.054 45.054/45.054 Clean CTRS Processor: 45.054/45.054 45.054/45.054 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.054/45.054 Confluence Problem: 45.054/45.054 (VAR x:S) 45.054/45.054 (STRATEGY CONTEXTSENSITIVE 45.054/45.054 (a) 45.054/45.054 (f 1 2) 45.054/45.054 (g 1 2) 45.054/45.054 (k 1) 45.054/45.054 (b) 45.054/45.054 (fSNonEmpty) 45.054/45.054 (h 1) 45.054/45.054 ) 45.054/45.054 (RULES 45.054/45.054 a -> b 45.054/45.054 f(k(a),h(a)) -> k(a) 45.054/45.054 g(x:S,x:S) -> a 45.054/45.054 k(x:S) -> a 45.054/45.054 k(x:S) -> b 45.054/45.054 k(x:S) -> h(x:S) 45.054/45.054 ) 45.054/45.054 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.054/45.054 45.054/45.054 CRule InfChecker Info: 45.054/45.054 a -> b 45.054/45.054 Rule remains 45.054/45.054 Proof: 45.054/45.054 NO_CONDS 45.054/45.054 45.054/45.054 CRule InfChecker Info: 45.054/45.054 f(k(a),h(a)) -> k(a) 45.054/45.054 Rule remains 45.054/45.054 Proof: 45.054/45.054 NO_CONDS 45.054/45.054 45.054/45.054 CRule InfChecker Info: 45.054/45.054 f(k(z:S),a) -> g(h(z:S),h(z:S)) | h(z:S) ->* b 45.054/45.054 Rule deleted 45.054/45.054 Proof: 45.054/45.054 YES 45.054/45.054 45.054/45.054 Problem 1: 45.054/45.054 45.054/45.054 Infeasibility Problem: 45.054/45.054 [(VAR vNonEmpty:S vNonEmpty:S:S x:S:S y:S:S z:S:S) 45.054/45.054 (STRATEGY CONTEXTSENSITIVE 45.054/45.054 (a) 45.054/45.054 (f 1 2) 45.054/45.054 (g 1 2) 45.054/45.054 (k 1) 45.054/45.054 (b) 45.054/45.054 (fSNonEmpty) 45.054/45.054 (h 1) 45.054/45.054 ) 45.054/45.054 (RULES 45.054/45.054 a -> b 45.054/45.054 f(k(a),h(a)) -> k(a) 45.054/45.054 f(k(z:S:S),a) -> g(h(z:S:S),h(z:S:S)) | h(z:S:S) ->* b 45.054/45.054 g(x:S:S,x:S:S) -> a 45.054/45.054 k(x:S:S) -> a 45.054/45.054 k(x:S:S) -> b 45.054/45.054 k(x:S:S) -> h(x:S:S) 45.054/45.054 )] 45.054/45.054 45.054/45.054 Infeasibility Conditions: 45.054/45.054 h(z:S:S) ->* b 45.054/45.054 45.054/45.054 Problem 1: 45.054/45.054 45.054/45.054 Obtaining a model using Mace4: 45.054/45.054 45.054/45.054 -> Usable Rules: 45.054/45.054 a -> b 45.054/45.054 f(k(a),h(a)) -> k(a) 45.054/45.054 f(k(z:S:S),a) -> g(h(z:S:S),h(z:S:S)) | h(z:S:S) ->* b 45.054/45.054 g(x:S:S,x:S:S) -> a 45.054/45.054 k(x:S:S) -> a 45.054/45.054 k(x:S:S) -> b 45.054/45.054 k(x:S:S) -> h(x:S:S) 45.054/45.054 45.054/45.054 -> Mace4 Output: 45.054/45.054 ============================== Mace4 ================================= 45.054/45.054 Mace4 (64) version 2009-11A, November 2009. 45.054/45.054 Process 66307 was started by ubuntu on ubuntu, 45.054/45.054 Wed Jul 14 11:52:30 2021 45.054/45.054 The command was "./mace4 -c -f /tmp/mace466296-2.in". 45.054/45.054 ============================== end of head =========================== 45.054/45.054 45.054/45.054 ============================== INPUT ================================= 45.054/45.054 45.054/45.054 % Reading from file /tmp/mace466296-2.in 45.054/45.054 45.054/45.054 assign(max_seconds,20). 45.054/45.054 45.054/45.054 formulas(assumptions). 45.054/45.054 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence). 45.054/45.054 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence). 45.054/45.054 ->(x1,y) -> ->(g(x1,x2),g(y,x2)) # label(congruence). 45.054/45.054 ->(x2,y) -> ->(g(x1,x2),g(x1,y)) # label(congruence). 45.054/45.054 ->(x1,y) -> ->(k(x1),k(y)) # label(congruence). 45.054/45.054 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence). 45.054/45.054 ->(a,b) # label(replacement). 45.054/45.054 ->(f(k(a),h(a)),k(a)) # label(replacement). 45.054/45.054 ->*(h(x4),b) -> ->(f(k(x4),a),g(h(x4),h(x4))) # label(replacement). 45.054/45.054 ->(g(x2,x2),a) # label(replacement). 45.054/45.054 ->(k(x2),a) # label(replacement). 45.054/45.054 ->(k(x2),b) # label(replacement). 45.054/45.054 ->(k(x2),h(x2)) # label(replacement). 45.054/45.054 ->*(x,x) # label(reflexivity). 45.054/45.054 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 45.054/45.054 end_of_list. 45.054/45.054 45.054/45.054 formulas(goals). 45.054/45.054 (exists x4 ->*(h(x4),b)) # label(goal). 45.054/45.054 end_of_list. 45.054/45.054 45.054/45.054 ============================== end of input ========================== 45.054/45.054 45.054/45.054 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 45.054/45.054 45.054/45.054 % Formulas that are not ordinary clauses: 45.054/45.054 1 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 45.054/45.054 2 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 45.054/45.054 3 ->(x1,y) -> ->(g(x1,x2),g(y,x2)) # label(congruence) # label(non_clause). [assumption]. 45.054/45.054 4 ->(x2,y) -> ->(g(x1,x2),g(x1,y)) # label(congruence) # label(non_clause). [assumption]. 45.054/45.054 5 ->(x1,y) -> ->(k(x1),k(y)) # label(congruence) # label(non_clause). [assumption]. 45.054/45.054 6 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 45.054/45.054 7 ->*(h(x4),b) -> ->(f(k(x4),a),g(h(x4),h(x4))) # label(replacement) # label(non_clause). [assumption]. 45.054/45.054 8 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 45.054/45.054 9 (exists x4 ->*(h(x4),b)) # label(goal) # label(non_clause) # label(goal). [goal]. 45.054/45.054 45.054/45.054 ============================== end of process non-clausal formulas === 45.054/45.054 45.054/45.054 ============================== CLAUSES FOR SEARCH ==================== 45.054/45.054 45.054/45.054 formulas(mace4_clauses). 45.054/45.054 -->(x,y) | ->(f(x,z),f(y,z)) # label(congruence). 45.054/45.054 -->(x,y) | ->(f(z,x),f(z,y)) # label(congruence). 45.054/45.054 -->(x,y) | ->(g(x,z),g(y,z)) # label(congruence). 45.054/45.054 -->(x,y) | ->(g(z,x),g(z,y)) # label(congruence). 45.054/45.054 -->(x,y) | ->(k(x),k(y)) # label(congruence). 45.054/45.054 -->(x,y) | ->(h(x),h(y)) # label(congruence). 45.054/45.054 ->(a,b) # label(replacement). 45.054/45.054 ->(f(k(a),h(a)),k(a)) # label(replacement). 45.054/45.054 -->*(h(x),b) | ->(f(k(x),a),g(h(x),h(x))) # label(replacement). 45.054/45.054 ->(g(x,x),a) # label(replacement). 45.054/45.054 ->(k(x),a) # label(replacement). 45.054/45.054 ->(k(x),b) # label(replacement). 45.054/45.054 ->(k(x),h(x)) # label(replacement). 45.054/45.054 ->*(x,x) # label(reflexivity). 45.054/45.054 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 45.054/45.054 -->*(h(x),b) # label(goal). 45.054/45.054 end_of_list. 45.054/45.054 45.054/45.054 ============================== end of clauses for search ============= 45.054/45.054 45.054/45.054 % There are no natural numbers in the input. 45.054/45.054 45.054/45.054 ============================== DOMAIN SIZE 2 ========================= 45.054/45.054 45.054/45.054 ============================== MODEL ================================= 45.054/45.054 45.054/45.054 interpretation( 2, [number=1, seconds=0], [ 45.054/45.054 45.054/45.054 function(a, [ 0 ]), 45.054/45.054 45.054/45.054 function(b, [ 0 ]), 45.054/45.054 45.054/45.054 function(k(_), [ 0, 0 ]), 45.054/45.054 45.054/45.054 function(h(_), [ 1, 1 ]), 45.054/45.054 45.054/45.054 function(f(_,_), [ 45.054/45.054 0, 0, 45.054/45.054 0, 0 ]), 45.054/45.054 45.054/45.054 function(g(_,_), [ 45.054/45.054 0, 0, 45.054/45.054 0, 0 ]), 45.054/45.054 45.054/45.054 relation(->*(_,_), [ 45.054/45.054 1, 1, 45.054/45.054 0, 1 ]), 45.054/45.054 45.054/45.054 relation(->(_,_), [ 45.054/45.054 1, 1, 45.054/45.054 0, 1 ]) 45.054/45.054 ]). 45.054/45.054 45.054/45.054 ============================== end of model ========================== 45.054/45.054 45.054/45.054 ============================== STATISTICS ============================ 45.054/45.054 45.054/45.054 For domain size 2. 45.054/45.054 45.054/45.054 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 45.054/45.054 Ground clauses: seen=64, kept=60. 45.054/45.054 Selections=4, assignments=4, propagations=18, current_models=1. 45.054/45.054 Rewrite_terms=125, rewrite_bools=94, indexes=11. 45.054/45.054 Rules_from_neg_clauses=10, cross_offs=10. 45.054/45.054 45.054/45.054 ============================== end of statistics ===================== 45.054/45.054 45.054/45.054 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 45.054/45.054 45.054/45.054 Exiting with 1 model. 45.054/45.054 45.054/45.054 Process 66307 exit (max_models) Wed Jul 14 11:52:30 2021 45.054/45.054 The process finished Wed Jul 14 11:52:30 2021 45.054/45.054 45.054/45.054 45.054/45.054 Mace4 cooked interpretation: 45.054/45.054 45.054/45.054 45.054/45.054 45.054/45.054 The problem is infeasible. 45.054/45.054 45.054/45.054 45.054/45.054 CRule InfChecker Info: 45.054/45.054 g(x:S,x:S) -> a 45.054/45.054 Rule remains 45.054/45.054 Proof: 45.054/45.054 NO_CONDS 45.054/45.054 45.054/45.054 CRule InfChecker Info: 45.054/45.054 k(x:S) -> a 45.054/45.054 Rule remains 45.054/45.054 Proof: 45.054/45.054 NO_CONDS 45.054/45.054 45.054/45.054 CRule InfChecker Info: 45.054/45.054 k(x:S) -> b 45.054/45.054 Rule remains 45.054/45.054 Proof: 45.054/45.054 NO_CONDS 45.054/45.054 45.054/45.054 CRule InfChecker Info: 45.054/45.054 k(x:S) -> h(x:S) 45.054/45.054 Rule remains 45.054/45.054 Proof: 45.054/45.054 NO_CONDS 45.054/45.054 45.054/45.054 Problem 1: 45.054/45.054 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.054/45.054 Confluence Problem: 45.054/45.054 (VAR x:S) 45.054/45.054 (STRATEGY CONTEXTSENSITIVE 45.054/45.054 (a) 45.054/45.054 (f 1 2) 45.054/45.054 (g 1 2) 45.054/45.054 (k 1) 45.054/45.054 (b) 45.054/45.054 (fSNonEmpty) 45.054/45.054 (h 1) 45.054/45.054 ) 45.054/45.054 (RULES 45.054/45.054 a -> b 45.054/45.054 f(k(a),h(a)) -> k(a) 45.054/45.054 g(x:S,x:S) -> a 45.054/45.054 k(x:S) -> a 45.054/45.054 k(x:S) -> b 45.054/45.054 k(x:S) -> h(x:S) 45.054/45.054 ) 45.054/45.054 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.054/45.054 45.054/45.054 Critical Pairs Processor: 45.054/45.054 -> Rules: 45.054/45.054 a -> b 45.054/45.054 f(k(a),h(a)) -> k(a) 45.054/45.054 g(x:S,x:S) -> a 45.054/45.054 k(x:S) -> a 45.054/45.054 k(x:S) -> b 45.054/45.054 k(x:S) -> h(x:S) 45.054/45.054 -> Vars: 45.054/45.054 "x", "x", "x", "x" 45.054/45.054 -> FVars: 45.054/45.054 "x2", "x3", "x4", "x5" 45.054/45.054 -> PVars: 45.054/45.054 "x": ["x2", "x3", "x4", "x5"] 45.054/45.054 45.054/45.054 -> Rlps: 45.054/45.054 crule: a -> b, id: 1, possubterms: a-> [] 45.054/45.054 crule: f(k(a),h(a)) -> k(a), id: 2, possubterms: f(k(a),h(a))-> [], k(a)-> [1], a-> [1,1], h(a)-> [2], a-> [2,1] 45.054/45.054 crule: g(x2:S,x2:S) -> a, id: 3, possubterms: g(x2:S,x2:S)-> [] 45.054/45.054 crule: k(x3:S) -> a, id: 4, possubterms: k(x3:S)-> [] 45.054/45.054 crule: k(x4:S) -> b, id: 5, possubterms: k(x4:S)-> [] 45.054/45.054 crule: k(x5:S) -> h(x5:S), id: 6, possubterms: k(x5:S)-> [] 45.054/45.054 45.054/45.054 -> Unifications: 45.054/45.054 R2 unifies with R4 at p: [1], l: f(k(a),h(a)), lp: k(a), conds: {}, sig: {x:S -> a}, l': k(x:S), r: k(a), r': a 45.054/45.054 R2 unifies with R5 at p: [1], l: f(k(a),h(a)), lp: k(a), conds: {}, sig: {x:S -> a}, l': k(x:S), r: k(a), r': b 45.054/45.054 R2 unifies with R6 at p: [1], l: f(k(a),h(a)), lp: k(a), conds: {}, sig: {x:S -> a}, l': k(x:S), r: k(a), r': h(x:S) 45.054/45.054 R2 unifies with R1 at p: [1,1], l: f(k(a),h(a)), lp: a, conds: {}, sig: {}, l': a, r: k(a), r': b 45.054/45.054 R2 unifies with R1 at p: [2,1], l: f(k(a),h(a)), lp: a, conds: {}, sig: {}, l': a, r: k(a), r': b 45.054/45.054 R5 unifies with R4 at p: [], l: k(x4:S), lp: k(x4:S), conds: {}, sig: {x4:S -> x:S}, l': k(x:S), r: b, r': a 45.054/45.054 R6 unifies with R4 at p: [], l: k(x5:S), lp: k(x5:S), conds: {}, sig: {x5:S -> x:S}, l': k(x:S), r: h(x5:S), r': a 45.054/45.054 R6 unifies with R5 at p: [], l: k(x5:S), lp: k(x5:S), conds: {}, sig: {x5:S -> x:S}, l': k(x:S), r: h(x5:S), r': b 45.054/45.054 45.054/45.054 -> Critical pairs info: 45.054/45.054 => Not trivial, Overlay, N1 45.054/45.054 => Not trivial, Not overlay, N2 45.054/45.054 => Not trivial, Not overlay, N3 45.054/45.054 => Not trivial, Not overlay, N4 45.054/45.054 => Not trivial, Not overlay, N5 45.054/45.054 => Not trivial, Not overlay, N6 45.054/45.054 => Not trivial, Overlay, N7 45.054/45.054 => Not trivial, Overlay, N8 45.054/45.054 45.054/45.054 -> Problem conclusions: 45.054/45.054 Not left linear, Right linear, Not linear 45.054/45.054 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 45.054/45.054 CTRS Type: 1 45.054/45.054 Deterministic, Strongly deterministic 45.054/45.054 Oriented CTRS, Properly oriented CTRS, Join CTRS 45.054/45.054 Maybe right-stable CTRS, Not overlay CTRS 45.054/45.054 Normal CTRS, Almost normal CTRS 45.054/45.054 Maybe terminating CTRS, Maybe joinable CCPs 45.054/45.054 Maybe level confluent 45.054/45.054 Maybe confluent 45.054/45.054 45.054/45.054 Problem 1: 45.054/45.054 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.054/45.054 Confluence Problem: 45.054/45.054 (VAR x:S) 45.054/45.054 (STRATEGY CONTEXTSENSITIVE 45.054/45.054 (a) 45.054/45.054 (f 1 2) 45.054/45.054 (g 1 2) 45.054/45.054 (k 1) 45.054/45.054 (b) 45.054/45.054 (fSNonEmpty) 45.054/45.054 (h 1) 45.054/45.054 ) 45.054/45.054 (RULES 45.054/45.054 a -> b 45.054/45.054 f(k(a),h(a)) -> k(a) 45.054/45.054 g(x:S,x:S) -> a 45.054/45.054 k(x:S) -> a 45.054/45.054 k(x:S) -> b 45.054/45.054 k(x:S) -> h(x:S) 45.054/45.054 ) 45.054/45.054 Critical Pairs: 45.054/45.054 => Not trivial, Overlay, N1 45.054/45.054 => Not trivial, Not overlay, N2 45.054/45.054 => Not trivial, Not overlay, N3 45.054/45.054 => Not trivial, Not overlay, N4 45.054/45.054 => Not trivial, Not overlay, N5 45.054/45.054 => Not trivial, Not overlay, N6 45.054/45.054 => Not trivial, Overlay, N7 45.054/45.054 => Not trivial, Overlay, N8 45.054/45.054 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.054/45.054 45.054/45.054 Conditional Critical Pairs Distributor Processor 45.054/45.054 45.054/45.054 Problem 1: 45.054/45.054 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.054/45.054 Confluence Problem: 45.054/45.054 (VAR x:S) 45.054/45.054 (STRATEGY CONTEXTSENSITIVE 45.054/45.054 (a) 45.054/45.054 (f 1 2) 45.054/45.054 (g 1 2) 45.054/45.054 (k 1) 45.054/45.054 (b) 45.054/45.054 (fSNonEmpty) 45.054/45.054 (h 1) 45.054/45.054 ) 45.054/45.054 (RULES 45.054/45.054 a -> b 45.054/45.054 f(k(a),h(a)) -> k(a) 45.054/45.054 g(x:S,x:S) -> a 45.054/45.054 k(x:S) -> a 45.054/45.054 k(x:S) -> b 45.054/45.054 k(x:S) -> h(x:S) 45.054/45.054 ) 45.054/45.054 Critical Pairs: 45.054/45.054 => Not trivial, Not overlay, N2 45.054/45.054 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.054/45.054 45.054/45.054 Infeasible Convergence No Conditions CCP Processor: 45.054/45.054 Infeasible convergence? 45.054/45.054 YES 45.054/45.054 45.054/45.054 Problem 1: 45.054/45.054 45.054/45.054 Infeasibility Problem: 45.054/45.054 [(VAR vNonEmpty:S x:S z:S) 45.054/45.054 (STRATEGY CONTEXTSENSITIVE 45.054/45.054 (a) 45.054/45.054 (f 1 2) 45.054/45.054 (g 1 2) 45.054/45.054 (k 1) 45.054/45.054 (b) 45.054/45.054 (fSNonEmpty) 45.054/45.054 (h 1) 45.054/45.054 ) 45.054/45.054 (RULES 45.054/45.054 a -> b 45.054/45.054 f(k(a),h(a)) -> k(a) 45.054/45.054 g(x:S,x:S) -> a 45.054/45.054 k(x:S) -> a 45.054/45.054 k(x:S) -> b 45.054/45.054 k(x:S) -> h(x:S) 45.054/45.054 )] 45.054/45.054 Infeasibility Conditions: 45.054/45.054 f(k(a),h(b)) ->* z:S, k(a) ->* z:S 45.054/45.054 45.054/45.054 Problem 1: 45.054/45.054 45.054/45.054 Obtaining a model using Mace4: 45.054/45.054 45.054/45.054 -> Usable Rules: 45.054/45.054 a -> b 45.054/45.054 f(k(a),h(a)) -> k(a) 45.054/45.054 k(x:S) -> a 45.054/45.054 k(x:S) -> b 45.054/45.054 k(x:S) -> h(x:S) 45.054/45.054 45.054/45.054 -> Mace4 Output: 45.054/45.054 ============================== Mace4 ================================= 45.054/45.054 Mace4 (64) version 2009-11A, November 2009. 45.054/45.054 Process 66401 was started by ubuntu on ubuntu, 45.054/45.054 Wed Jul 14 11:52:51 2021 45.054/45.054 The command was "./mace4 -c -f /tmp/mace466370-2.in". 45.054/45.054 ============================== end of head =========================== 45.054/45.054 45.054/45.054 ============================== INPUT ================================= 45.054/45.054 45.054/45.054 % Reading from file /tmp/mace466370-2.in 45.054/45.054 45.054/45.054 assign(max_seconds,20). 45.054/45.054 45.054/45.054 formulas(assumptions). 45.054/45.054 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence). 45.054/45.054 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence). 45.054/45.054 ->(x1,y) -> ->(g(x1,x2),g(y,x2)) # label(congruence). 45.054/45.054 ->(x2,y) -> ->(g(x1,x2),g(x1,y)) # label(congruence). 45.054/45.054 ->(x1,y) -> ->(k(x1),k(y)) # label(congruence). 45.054/45.054 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence). 45.054/45.054 ->(a,b) # label(replacement). 45.054/45.054 ->(f(k(a),h(a)),k(a)) # label(replacement). 45.054/45.054 ->(k(x1),a) # label(replacement). 45.054/45.054 ->(k(x1),b) # label(replacement). 45.054/45.054 ->(k(x1),h(x1)) # label(replacement). 45.054/45.054 ->*(x,x) # label(reflexivity). 45.054/45.054 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 45.054/45.054 end_of_list. 45.054/45.054 45.054/45.054 formulas(goals). 45.054/45.054 (exists x2 (->*(f(k(a),h(b)),x2) & ->*(k(a),x2))) # label(goal). 45.054/45.054 end_of_list. 45.054/45.054 45.054/45.054 ============================== end of input ========================== 45.054/45.054 45.054/45.054 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 45.054/45.054 45.054/45.054 % Formulas that are not ordinary clauses: 45.054/45.054 1 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 45.054/45.054 2 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 45.054/45.054 3 ->(x1,y) -> ->(g(x1,x2),g(y,x2)) # label(congruence) # label(non_clause). [assumption]. 45.054/45.054 4 ->(x2,y) -> ->(g(x1,x2),g(x1,y)) # label(congruence) # label(non_clause). [assumption]. 45.054/45.054 5 ->(x1,y) -> ->(k(x1),k(y)) # label(congruence) # label(non_clause). [assumption]. 45.054/45.054 6 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 45.054/45.054 7 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 45.054/45.054 8 (exists x2 (->*(f(k(a),h(b)),x2) & ->*(k(a),x2))) # label(goal) # label(non_clause) # label(goal). [goal]. 45.054/45.054 45.054/45.054 ============================== end of process non-clausal formulas === 45.054/45.054 45.054/45.054 ============================== CLAUSES FOR SEARCH ==================== 45.054/45.054 45.054/45.054 formulas(mace4_clauses). 45.054/45.054 -->(x,y) | ->(f(x,z),f(y,z)) # label(congruence). 45.054/45.054 -->(x,y) | ->(f(z,x),f(z,y)) # label(congruence). 45.054/45.054 -->(x,y) | ->(g(x,z),g(y,z)) # label(congruence). 45.054/45.054 -->(x,y) | ->(g(z,x),g(z,y)) # label(congruence). 45.054/45.054 -->(x,y) | ->(k(x),k(y)) # label(congruence). 45.054/45.054 -->(x,y) | ->(h(x),h(y)) # label(congruence). 45.054/45.054 ->(a,b) # label(replacement). 45.054/45.054 ->(f(k(a),h(a)),k(a)) # label(replacement). 45.054/45.054 ->(k(x),a) # label(replacement). 45.054/45.054 ->(k(x),b) # label(replacement). 45.054/45.054 ->(k(x),h(x)) # label(replacement). 45.054/45.054 ->*(x,x) # label(reflexivity). 45.054/45.054 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 45.054/45.054 -->*(f(k(a),h(b)),x) | -->*(k(a),x) # label(goal). 45.054/45.054 end_of_list. 45.054/45.054 45.054/45.054 ============================== end of clauses for search ============= 45.054/45.054 45.054/45.054 % There are no natural numbers in the input. 45.054/45.054 45.054/45.054 ============================== DOMAIN SIZE 2 ========================= 45.054/45.054 45.054/45.054 ============================== STATISTICS ============================ 45.054/45.054 45.054/45.054 For domain size 2. 45.054/45.054 45.054/45.054 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 45.054/45.054 Ground clauses: seen=60, kept=56. 45.054/45.054 Selections=84, assignments=167, propagations=124, current_models=0. 45.054/45.054 Rewrite_terms=1111, rewrite_bools=904, indexes=192. 45.054/45.054 Rules_from_neg_clauses=80, cross_offs=80. 45.054/45.054 45.054/45.054 ============================== end of statistics ===================== 45.054/45.054 45.054/45.054 ============================== DOMAIN SIZE 3 ========================= 45.054/45.054 45.054/45.054 ============================== STATISTICS ============================ 45.054/45.054 45.054/45.054 For domain size 3. 45.054/45.054 45.054/45.054 Current CPU time: 0.00 seconds (total CPU time: 0.05 seconds). 45.054/45.054 Ground clauses: seen=170, kept=161. 45.054/45.054 Selections=5482, assignments=16386, propagations=12778, current_models=0. 45.054/45.054 Rewrite_terms=135851, rewrite_bools=116078, indexes=24684. 45.054/45.054 Rules_from_neg_clauses=5890, cross_offs=12181. 45.054/45.054 45.054/45.054 ============================== end of statistics ===================== 45.054/45.054 45.054/45.054 ============================== DOMAIN SIZE 4 ========================= 45.054/45.054 45.054/45.054 ============================== MODEL ================================= 45.054/45.054 45.054/45.054 interpretation( 4, [number=1, seconds=0], [ 45.054/45.054 45.054/45.054 function(a, [ 0 ]), 45.054/45.054 45.054/45.054 function(b, [ 1 ]), 45.054/45.054 45.054/45.054 function(k(_), [ 0, 0, 0, 0 ]), 45.054/45.054 45.054/45.054 function(h(_), [ 0, 1, 0, 0 ]), 45.054/45.054 45.054/45.054 function(f(_,_), [ 45.054/45.054 2, 3, 2, 0, 45.054/45.054 2, 3, 2, 0, 45.054/45.054 2, 2, 2, 0, 45.054/45.054 0, 0, 0, 0 ]), 45.054/45.054 45.054/45.054 function(g(_,_), [ 45.054/45.054 0, 0, 0, 0, 45.054/45.054 0, 0, 0, 0, 45.054/45.054 0, 0, 0, 0, 45.054/45.054 0, 0, 0, 0 ]), 45.054/45.054 45.054/45.054 relation(->*(_,_), [ 45.054/45.054 1, 1, 0, 0, 45.054/45.054 0, 1, 0, 0, 45.054/45.054 1, 1, 1, 1, 45.054/45.054 0, 0, 0, 1 ]), 45.054/45.054 45.054/45.054 relation(->(_,_), [ 45.054/45.054 1, 1, 0, 0, 45.054/45.054 0, 0, 0, 0, 45.054/45.054 1, 0, 1, 1, 45.054/45.054 0, 0, 0, 1 ]) 45.054/45.054 ]). 45.054/45.054 45.054/45.054 ============================== end of model ========================== 45.054/45.054 45.054/45.054 ============================== STATISTICS ============================ 45.054/45.054 45.054/45.054 For domain size 4. 45.054/45.054 45.054/45.054 Current CPU time: 0.00 seconds (total CPU time: 0.06 seconds). 45.054/45.054 Ground clauses: seen=374, kept=358. 45.054/45.054 Selections=79, assignments=196, propagations=652, current_models=1. 45.054/45.054 Rewrite_terms=3049, rewrite_bools=4123, indexes=810. 45.054/45.054 Rules_from_neg_clauses=56, cross_offs=234. 45.054/45.054 45.054/45.054 ============================== end of statistics ===================== 45.054/45.054 45.054/45.054 User_CPU=0.06, System_CPU=0.00, Wall_clock=0. 45.054/45.054 45.054/45.054 Exiting with 1 model. 45.054/45.054 45.054/45.054 Process 66401 exit (max_models) Wed Jul 14 11:52:51 2021 45.054/45.054 The process finished Wed Jul 14 11:52:51 2021 45.054/45.054 45.054/45.054 45.054/45.054 Mace4 cooked interpretation: 45.054/45.054 45.054/45.054 45.054/45.054 45.054/45.054 The problem is infeasible. 45.054/45.054 45.054/45.054 45.054/45.054 The problem is not joinable. 45.054/45.054 38.41user 2.59system 0:45.54elapsed 90%CPU (0avgtext+0avgdata 116712maxresident)k 45.054/45.054 8inputs+0outputs (0major+76123minor)pagefaults 0swaps