55.08/55.08 NO 55.08/55.08 55.08/55.08 Problem 1: 55.08/55.08 55.08/55.08 55.08/55.08 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 55.08/55.08 Confluence Problem: 55.08/55.08 (VAR vNonEmpty:S x:S y:S) 55.08/55.08 (STRATEGY CONTEXTSENSITIVE 55.08/55.08 (f 1 2 3) 55.08/55.08 (g 1) 55.08/55.08 (h 1) 55.08/55.08 (a) 55.08/55.08 (b) 55.08/55.08 (c 1) 55.08/55.08 (d) 55.08/55.08 (fSNonEmpty) 55.08/55.08 (k 1) 55.08/55.08 ) 55.08/55.08 (RULES 55.08/55.08 f(k(a),k(b),x:S) -> f(x:S,x:S,x:S) 55.08/55.08 g(x:S) -> k(y:S) | h(x:S) ->* d, h(x:S) ->* c(y:S) 55.08/55.08 h(d) -> c(a) 55.08/55.08 h(d) -> c(b) 55.08/55.08 ) 55.08/55.08 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 55.08/55.08 55.08/55.08 55.08/55.08 Problem 1: 55.08/55.08 55.08/55.08 Inlining of Conditions Processor [STERN17]: 55.08/55.08 55.08/55.08 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 55.08/55.08 Confluence Problem: 55.08/55.08 (VAR vNonEmpty:S x:S y:S) 55.08/55.08 (STRATEGY CONTEXTSENSITIVE 55.08/55.08 (f 1 2 3) 55.08/55.08 (g 1) 55.08/55.08 (h 1) 55.08/55.08 (a) 55.08/55.08 (b) 55.08/55.08 (c 1) 55.08/55.08 (d) 55.08/55.08 (fSNonEmpty) 55.08/55.08 (k 1) 55.08/55.08 ) 55.08/55.08 (RULES 55.08/55.08 f(k(a),k(b),x:S) -> f(x:S,x:S,x:S) 55.08/55.08 g(x:S) -> k(y:S) | h(x:S) ->* c(y:S), h(x:S) ->* d 55.08/55.08 h(d) -> c(a) 55.08/55.08 h(d) -> c(b) 55.08/55.08 ) 55.08/55.08 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 55.08/55.08 55.08/55.08 55.08/55.08 Problem 1: 55.08/55.08 55.08/55.08 Clean CTRS Processor: 55.08/55.08 55.08/55.08 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 55.08/55.08 Confluence Problem: 55.08/55.08 (VAR x:S) 55.08/55.08 (STRATEGY CONTEXTSENSITIVE 55.08/55.08 (f 1 2 3) 55.08/55.08 (g 1) 55.08/55.08 (h 1) 55.08/55.08 (a) 55.08/55.08 (b) 55.08/55.08 (c 1) 55.08/55.08 (d) 55.08/55.08 (fSNonEmpty) 55.08/55.08 (k 1) 55.08/55.08 ) 55.08/55.08 (RULES 55.08/55.08 f(k(a),k(b),x:S) -> f(x:S,x:S,x:S) 55.08/55.08 h(d) -> c(a) 55.08/55.08 h(d) -> c(b) 55.08/55.08 ) 55.08/55.08 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 55.08/55.08 55.08/55.08 CRule InfChecker Info: 55.08/55.08 f(k(a),k(b),x:S) -> f(x:S,x:S,x:S) 55.08/55.08 Rule remains 55.08/55.08 Proof: 55.08/55.08 NO_CONDS 55.08/55.08 55.08/55.08 CRule InfChecker Info: 55.08/55.08 g(x:S) -> k(y:S) | h(x:S) ->* c(y:S), h(x:S) ->* d 55.08/55.08 Rule deleted 55.08/55.08 Proof: 55.08/55.08 YES 55.08/55.08 55.08/55.08 Problem 1: 55.08/55.08 55.08/55.08 Infeasibility Problem: 55.08/55.08 [(VAR vNonEmpty:S vNonEmpty:S:S x:S:S y:S:S) 55.08/55.08 (STRATEGY CONTEXTSENSITIVE 55.08/55.08 (f 1 2 3) 55.08/55.08 (g 1) 55.08/55.08 (h 1) 55.08/55.08 (a) 55.08/55.08 (b) 55.08/55.08 (c 1) 55.08/55.08 (d) 55.08/55.08 (fSNonEmpty) 55.08/55.08 (k 1) 55.08/55.08 ) 55.08/55.08 (RULES 55.08/55.08 f(k(a),k(b),x:S:S) -> f(x:S:S,x:S:S,x:S:S) 55.08/55.08 g(x:S:S) -> k(y:S:S) | h(x:S:S) ->* c(y:S:S), h(x:S:S) ->* d 55.08/55.08 h(d) -> c(a) 55.08/55.08 h(d) -> c(b) 55.08/55.08 )] 55.08/55.08 55.08/55.08 Infeasibility Conditions: 55.08/55.08 h(x:S:S) ->* c(y:S:S), h(x:S:S) ->* d 55.08/55.08 55.08/55.08 Problem 1: 55.08/55.08 55.08/55.08 Obtaining a model using Mace4: 55.08/55.08 55.08/55.08 -> Usable Rules: 55.08/55.08 f(k(a),k(b),x:S:S) -> f(x:S:S,x:S:S,x:S:S) 55.08/55.08 g(x:S:S) -> k(y:S:S) | h(x:S:S) ->* c(y:S:S), h(x:S:S) ->* d 55.08/55.08 h(d) -> c(a) 55.08/55.08 h(d) -> c(b) 55.08/55.08 55.08/55.08 -> Mace4 Output: 55.08/55.08 ============================== Mace4 ================================= 55.08/55.08 Mace4 (64) version 2009-11A, November 2009. 55.08/55.08 Process 47081 was started by ubuntu on ubuntu, 55.08/55.08 Wed Jul 14 10:40:41 2021 55.08/55.08 The command was "./mace4 -c -f /tmp/mace447068-2.in". 55.08/55.08 ============================== end of head =========================== 55.08/55.08 55.08/55.08 ============================== INPUT ================================= 55.08/55.08 55.08/55.08 % Reading from file /tmp/mace447068-2.in 55.08/55.08 55.08/55.08 assign(max_seconds,20). 55.08/55.08 55.08/55.08 formulas(assumptions). 55.08/55.08 ->(x1,y) -> ->(f(x1,x2,x3),f(y,x2,x3)) # label(congruence). 55.08/55.08 ->(x2,y) -> ->(f(x1,x2,x3),f(x1,y,x3)) # label(congruence). 55.08/55.08 ->(x3,y) -> ->(f(x1,x2,x3),f(x1,x2,y)) # label(congruence). 55.08/55.08 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence). 55.08/55.08 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence). 55.08/55.08 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence). 55.08/55.08 ->(x1,y) -> ->(k(x1),k(y)) # label(congruence). 55.08/55.08 ->(f(k(a),k(b),x2),f(x2,x2,x2)) # label(replacement). 55.08/55.08 ->*(h(x2),c(x3)) & ->*(h(x2),d) -> ->(g(x2),k(x3)) # label(replacement). 55.08/55.08 ->(h(d),c(a)) # label(replacement). 55.08/55.08 ->(h(d),c(b)) # label(replacement). 55.08/55.08 ->*(x,x) # label(reflexivity). 55.08/55.08 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 55.08/55.08 end_of_list. 55.08/55.08 55.08/55.08 formulas(goals). 55.08/55.08 (exists x2 exists x3 (->*(h(x2),c(x3)) & ->*(h(x2),d))) # label(goal). 55.08/55.08 end_of_list. 55.08/55.08 55.08/55.08 ============================== end of input ========================== 55.08/55.08 55.08/55.08 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 55.08/55.08 55.08/55.08 % Formulas that are not ordinary clauses: 55.08/55.08 1 ->(x1,y) -> ->(f(x1,x2,x3),f(y,x2,x3)) # label(congruence) # label(non_clause). [assumption]. 55.08/55.08 2 ->(x2,y) -> ->(f(x1,x2,x3),f(x1,y,x3)) # label(congruence) # label(non_clause). [assumption]. 55.08/55.08 3 ->(x3,y) -> ->(f(x1,x2,x3),f(x1,x2,y)) # label(congruence) # label(non_clause). [assumption]. 55.08/55.08 4 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 55.08/55.08 5 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 55.08/55.08 6 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence) # label(non_clause). [assumption]. 55.08/55.08 7 ->(x1,y) -> ->(k(x1),k(y)) # label(congruence) # label(non_clause). [assumption]. 55.08/55.08 8 ->*(h(x2),c(x3)) & ->*(h(x2),d) -> ->(g(x2),k(x3)) # label(replacement) # label(non_clause). [assumption]. 55.08/55.08 9 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 55.08/55.08 10 (exists x2 exists x3 (->*(h(x2),c(x3)) & ->*(h(x2),d))) # label(goal) # label(non_clause) # label(goal). [goal]. 55.08/55.08 55.08/55.08 ============================== end of process non-clausal formulas === 55.08/55.08 55.08/55.08 ============================== CLAUSES FOR SEARCH ==================== 55.08/55.08 55.08/55.08 formulas(mace4_clauses). 55.08/55.08 -->(x,y) | ->(f(x,z,u),f(y,z,u)) # label(congruence). 55.08/55.08 -->(x,y) | ->(f(z,x,u),f(z,y,u)) # label(congruence). 55.08/55.08 -->(x,y) | ->(f(z,u,x),f(z,u,y)) # label(congruence). 55.08/55.08 -->(x,y) | ->(g(x),g(y)) # label(congruence). 55.08/55.08 -->(x,y) | ->(h(x),h(y)) # label(congruence). 55.08/55.08 -->(x,y) | ->(c(x),c(y)) # label(congruence). 55.08/55.08 -->(x,y) | ->(k(x),k(y)) # label(congruence). 55.08/55.08 ->(f(k(a),k(b),x),f(x,x,x)) # label(replacement). 55.08/55.08 -->*(h(x),c(y)) | -->*(h(x),d) | ->(g(x),k(y)) # label(replacement). 55.08/55.08 ->(h(d),c(a)) # label(replacement). 55.08/55.08 ->(h(d),c(b)) # label(replacement). 55.08/55.08 ->*(x,x) # label(reflexivity). 55.08/55.08 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 55.08/55.08 -->*(h(x),c(y)) | -->*(h(x),d) # label(goal). 55.08/55.08 end_of_list. 55.08/55.08 55.08/55.08 ============================== end of clauses for search ============= 55.08/55.08 55.08/55.08 % There are no natural numbers in the input. 55.08/55.08 55.08/55.08 ============================== DOMAIN SIZE 2 ========================= 55.08/55.08 55.08/55.08 ============================== MODEL ================================= 55.08/55.08 55.08/55.08 interpretation( 2, [number=1, seconds=0], [ 55.08/55.08 55.08/55.08 function(a, [ 0 ]), 55.08/55.08 55.08/55.08 function(b, [ 0 ]), 55.08/55.08 55.08/55.08 function(d, [ 0 ]), 55.08/55.08 55.08/55.08 function(k(_), [ 0, 0 ]), 55.08/55.08 55.08/55.08 function(g(_), [ 0, 0 ]), 55.08/55.08 55.08/55.08 function(h(_), [ 1, 0 ]), 55.08/55.08 55.08/55.08 function(c(_), [ 1, 1 ]), 55.08/55.08 55.08/55.08 function(f(_,_,_), [ 55.08/55.08 0, 0, 55.08/55.08 0, 0, 55.08/55.08 0, 0, 55.08/55.08 0, 0 ]), 55.08/55.08 55.08/55.08 relation(->*(_,_), [ 55.08/55.08 1, 0, 55.08/55.08 0, 1 ]), 55.08/55.08 55.08/55.08 relation(->(_,_), [ 55.08/55.08 1, 0, 55.08/55.08 0, 1 ]) 55.08/55.08 ]). 55.08/55.08 55.08/55.08 ============================== end of model ========================== 55.08/55.08 55.08/55.08 ============================== STATISTICS ============================ 55.08/55.08 55.08/55.08 For domain size 2. 55.08/55.08 55.08/55.08 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 55.08/55.08 Ground clauses: seen=86, kept=82. 55.08/55.08 Selections=17, assignments=19, propagations=15, current_models=1. 55.08/55.08 Rewrite_terms=222, rewrite_bools=145, indexes=30. 55.08/55.08 Rules_from_neg_clauses=3, cross_offs=3. 55.08/55.08 55.08/55.08 ============================== end of statistics ===================== 55.08/55.08 55.08/55.08 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 55.08/55.08 55.08/55.08 Exiting with 1 model. 55.08/55.08 55.08/55.08 Process 47081 exit (max_models) Wed Jul 14 10:40:41 2021 55.08/55.08 The process finished Wed Jul 14 10:40:41 2021 55.08/55.08 55.08/55.08 55.08/55.08 Mace4 cooked interpretation: 55.08/55.08 55.08/55.08 55.08/55.08 55.08/55.08 The problem is infeasible. 55.08/55.08 55.08/55.08 55.08/55.08 CRule InfChecker Info: 55.08/55.08 h(d) -> c(a) 55.08/55.08 Rule remains 55.08/55.08 Proof: 55.08/55.08 NO_CONDS 55.08/55.08 55.08/55.08 CRule InfChecker Info: 55.08/55.08 h(d) -> c(b) 55.08/55.08 Rule remains 55.08/55.08 Proof: 55.08/55.08 NO_CONDS 55.08/55.08 55.08/55.08 Problem 1: 55.08/55.08 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 55.08/55.08 Confluence Problem: 55.08/55.08 (VAR x:S) 55.08/55.08 (STRATEGY CONTEXTSENSITIVE 55.08/55.08 (f 1 2 3) 55.08/55.08 (g 1) 55.08/55.08 (h 1) 55.08/55.08 (a) 55.08/55.08 (b) 55.08/55.08 (c 1) 55.08/55.08 (d) 55.08/55.08 (fSNonEmpty) 55.08/55.08 (k 1) 55.08/55.08 ) 55.08/55.08 (RULES 55.08/55.08 f(k(a),k(b),x:S) -> f(x:S,x:S,x:S) 55.08/55.08 h(d) -> c(a) 55.08/55.08 h(d) -> c(b) 55.08/55.08 ) 55.08/55.08 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 55.08/55.08 55.08/55.08 Critical Pairs Processor: 55.08/55.08 -> Rules: 55.08/55.08 f(k(a),k(b),x:S) -> f(x:S,x:S,x:S) 55.08/55.08 h(d) -> c(a) 55.08/55.08 h(d) -> c(b) 55.08/55.08 -> Vars: 55.08/55.08 "x" 55.08/55.08 -> FVars: 55.08/55.08 "x2" 55.08/55.08 -> PVars: 55.08/55.08 "x": ["x2"] 55.08/55.08 55.08/55.08 -> Rlps: 55.08/55.08 crule: f(k(a),k(b),x2:S) -> f(x2:S,x2:S,x2:S), id: 1, possubterms: f(k(a),k(b),x2:S)-> [], k(a)-> [1], a-> [1,1], k(b)-> [2], b-> [2,1] 55.08/55.08 crule: h(d) -> c(a), id: 2, possubterms: h(d)-> [], d-> [1] 55.08/55.08 crule: h(d) -> c(b), id: 3, possubterms: h(d)-> [], d-> [1] 55.08/55.08 55.08/55.08 -> Unifications: 55.08/55.08 R3 unifies with R2 at p: [], l: h(d), lp: h(d), conds: {}, sig: {}, l': h(d), r: c(b), r': c(a) 55.08/55.08 55.08/55.08 -> Critical pairs info: 55.08/55.08 => Not trivial, Overlay, N1 55.08/55.08 55.08/55.08 -> Problem conclusions: 55.08/55.08 Left linear, Not right linear, Not linear 55.08/55.08 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 55.08/55.08 CTRS Type: 1 55.08/55.08 Deterministic, Strongly deterministic 55.08/55.08 Oriented CTRS, Properly oriented CTRS, Join CTRS 55.08/55.08 Maybe right-stable CTRS, Overlay CTRS 55.08/55.08 Normal CTRS, Almost normal CTRS 55.08/55.08 Maybe terminating CTRS, Maybe joinable CCPs 55.08/55.08 Maybe level confluent 55.08/55.08 Maybe confluent 55.08/55.08 55.08/55.08 Problem 1: 55.08/55.08 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 55.08/55.08 Confluence Problem: 55.08/55.08 (VAR x:S) 55.08/55.08 (STRATEGY CONTEXTSENSITIVE 55.08/55.08 (f 1 2 3) 55.08/55.08 (g 1) 55.08/55.08 (h 1) 55.08/55.08 (a) 55.08/55.08 (b) 55.08/55.08 (c 1) 55.08/55.08 (d) 55.08/55.08 (fSNonEmpty) 55.08/55.08 (k 1) 55.08/55.08 ) 55.08/55.08 (RULES 55.08/55.08 f(k(a),k(b),x:S) -> f(x:S,x:S,x:S) 55.08/55.08 h(d) -> c(a) 55.08/55.08 h(d) -> c(b) 55.08/55.08 ) 55.08/55.08 Critical Pairs: 55.08/55.08 => Not trivial, Overlay, N1 55.08/55.08 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 55.08/55.08 55.08/55.08 Conditional Critical Pairs Distributor Processor 55.08/55.08 55.08/55.08 Problem 1: 55.08/55.08 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 55.08/55.08 Confluence Problem: 55.08/55.08 (VAR x:S) 55.08/55.08 (STRATEGY CONTEXTSENSITIVE 55.08/55.08 (f 1 2 3) 55.08/55.08 (g 1) 55.08/55.08 (h 1) 55.08/55.08 (a) 55.08/55.08 (b) 55.08/55.08 (c 1) 55.08/55.08 (d) 55.08/55.08 (fSNonEmpty) 55.08/55.08 (k 1) 55.08/55.08 ) 55.08/55.08 (RULES 55.08/55.08 f(k(a),k(b),x:S) -> f(x:S,x:S,x:S) 55.08/55.08 h(d) -> c(a) 55.08/55.08 h(d) -> c(b) 55.08/55.08 ) 55.08/55.08 Critical Pairs: 55.08/55.08 => Not trivial, Overlay, N1 55.08/55.08 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 55.08/55.08 55.08/55.08 InfChecker Different Ground and Normal No Conditions CCP Terms Processor: 55.08/55.08 Proof: 55.08/55.08 YES 55.08/55.08 55.08/55.08 Problem 1: 55.08/55.08 55.08/55.08 Infeasibility Problem: 55.08/55.08 [(VAR vNonEmpty:S x:S y:S) 55.08/55.08 (STRATEGY CONTEXTSENSITIVE 55.08/55.08 (f 1 2 3) 55.08/55.08 (h 1) 55.08/55.08 (a) 55.08/55.08 (b) 55.08/55.08 (c 1) 55.08/55.08 (d) 55.08/55.08 (fSNonEmpty) 55.08/55.08 (k 1) 55.08/55.08 ) 55.08/55.08 (RULES 55.08/55.08 f(k(a),k(b),x:S) -> f(x:S,x:S,x:S) 55.08/55.08 h(d) -> c(a) 55.08/55.08 h(d) -> c(b) 55.08/55.08 )] 55.08/55.08 Infeasibility Conditions: 55.08/55.08 c(a) -> y:S 55.08/55.08 55.08/55.08 Problem 1: 55.08/55.08 55.08/55.08 Obtaining a model using Mace4: 55.08/55.08 55.08/55.08 -> Usable Rules: 55.08/55.08 Empty 55.08/55.08 55.08/55.08 -> Mace4 Output: 55.08/55.08 ============================== Mace4 ================================= 55.08/55.08 Mace4 (64) version 2009-11A, November 2009. 55.08/55.08 Process 47127 was started by ubuntu on ubuntu, 55.08/55.08 Wed Jul 14 10:41:01 2021 55.08/55.08 The command was "./mace4 -c -f /tmp/mace447101-2.in". 55.08/55.08 ============================== end of head =========================== 55.08/55.08 55.08/55.08 ============================== INPUT ================================= 55.08/55.08 55.08/55.08 % Reading from file /tmp/mace447101-2.in 55.08/55.08 55.08/55.08 assign(max_seconds,6). 55.08/55.08 55.08/55.08 formulas(assumptions). 55.08/55.08 ->(x1,y) -> ->(f(x1,x2,x3),f(y,x2,x3)) # label(congruence). 55.08/55.08 ->(x2,y) -> ->(f(x1,x2,x3),f(x1,y,x3)) # label(congruence). 55.08/55.08 ->(x3,y) -> ->(f(x1,x2,x3),f(x1,x2,y)) # label(congruence). 55.08/55.08 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence). 55.08/55.08 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence). 55.08/55.08 ->(x1,y) -> ->(k(x1),k(y)) # label(congruence). 55.08/55.08 end_of_list. 55.08/55.08 55.08/55.08 formulas(goals). 55.08/55.08 (exists x2 ->(c(a),x2)) # label(goal). 55.08/55.08 end_of_list. 55.08/55.08 55.08/55.08 ============================== end of input ========================== 55.08/55.08 55.08/55.08 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 55.08/55.08 55.08/55.08 % Formulas that are not ordinary clauses: 55.08/55.08 1 ->(x1,y) -> ->(f(x1,x2,x3),f(y,x2,x3)) # label(congruence) # label(non_clause). [assumption]. 55.08/55.08 2 ->(x2,y) -> ->(f(x1,x2,x3),f(x1,y,x3)) # label(congruence) # label(non_clause). [assumption]. 55.08/55.08 3 ->(x3,y) -> ->(f(x1,x2,x3),f(x1,x2,y)) # label(congruence) # label(non_clause). [assumption]. 55.08/55.08 4 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 55.08/55.08 5 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence) # label(non_clause). [assumption]. 55.08/55.08 6 ->(x1,y) -> ->(k(x1),k(y)) # label(congruence) # label(non_clause). [assumption]. 55.08/55.08 7 (exists x2 ->(c(a),x2)) # label(goal) # label(non_clause) # label(goal). [goal]. 55.08/55.08 55.08/55.08 ============================== end of process non-clausal formulas === 55.08/55.08 55.08/55.08 ============================== CLAUSES FOR SEARCH ==================== 55.08/55.08 55.08/55.08 formulas(mace4_clauses). 55.08/55.08 -->(x,y) | ->(f(x,z,u),f(y,z,u)) # label(congruence). 55.08/55.08 -->(x,y) | ->(f(z,x,u),f(z,y,u)) # label(congruence). 55.08/55.08 -->(x,y) | ->(f(z,u,x),f(z,u,y)) # label(congruence). 55.08/55.08 -->(x,y) | ->(h(x),h(y)) # label(congruence). 55.08/55.08 -->(x,y) | ->(c(x),c(y)) # label(congruence). 55.08/55.08 -->(x,y) | ->(k(x),k(y)) # label(congruence). 55.08/55.08 -->(c(a),x) # label(goal). 55.08/55.08 end_of_list. 55.08/55.08 55.08/55.08 ============================== end of clauses for search ============= 55.08/55.08 55.08/55.08 % There are no natural numbers in the input. 55.08/55.08 55.08/55.08 ============================== DOMAIN SIZE 2 ========================= 55.08/55.08 55.08/55.08 ============================== MODEL ================================= 55.08/55.08 55.08/55.08 interpretation( 2, [number=1, seconds=0], [ 55.08/55.08 55.08/55.08 function(a, [ 0 ]), 55.08/55.08 55.08/55.08 function(h(_), [ 0, 0 ]), 55.08/55.08 55.08/55.08 function(c(_), [ 0, 0 ]), 55.08/55.08 55.08/55.08 function(k(_), [ 0, 0 ]), 55.08/55.08 55.08/55.08 function(f(_,_,_), [ 55.08/55.08 0, 0, 55.08/55.08 0, 0, 55.08/55.08 0, 0, 55.08/55.08 0, 0 ]), 55.08/55.08 55.08/55.08 relation(->(_,_), [ 55.08/55.08 0, 0, 55.08/55.08 0, 0 ]) 55.08/55.08 ]). 55.08/55.08 55.08/55.08 ============================== end of model ========================== 55.08/55.08 55.08/55.08 ============================== STATISTICS ============================ 55.08/55.08 55.08/55.08 For domain size 2. 55.08/55.08 55.08/55.08 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 55.08/55.08 Ground clauses: seen=62, kept=62. 55.08/55.08 Selections=15, assignments=15, propagations=4, current_models=1. 55.08/55.08 Rewrite_terms=124, rewrite_bools=66, indexes=5. 55.08/55.08 Rules_from_neg_clauses=0, cross_offs=0. 55.08/55.08 55.08/55.08 ============================== end of statistics ===================== 55.08/55.08 55.08/55.08 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 55.08/55.08 55.08/55.08 Exiting with 1 model. 55.08/55.08 55.08/55.08 Process 47127 exit (max_models) Wed Jul 14 10:41:01 2021 55.08/55.08 The process finished Wed Jul 14 10:41:01 2021 55.08/55.08 55.08/55.08 55.08/55.08 Mace4 cooked interpretation: 55.08/55.08 55.08/55.08 55.08/55.08 55.08/55.08 The problem is infeasible. 55.08/55.08 YES 55.08/55.08 55.08/55.08 Problem 1: 55.08/55.08 55.08/55.08 Infeasibility Problem: 55.08/55.08 [(VAR vNonEmpty:S x:S) 55.08/55.08 (STRATEGY CONTEXTSENSITIVE 55.08/55.08 (f 1 2 3) 55.08/55.08 (h 1) 55.08/55.08 (a) 55.08/55.08 (b) 55.08/55.08 (c 1) 55.08/55.08 (d) 55.08/55.08 (fSNonEmpty) 55.08/55.08 (k 1) 55.08/55.08 ) 55.08/55.08 (RULES 55.08/55.08 f(k(a),k(b),x:S) -> f(x:S,x:S,x:S) 55.08/55.08 h(d) -> c(a) 55.08/55.08 h(d) -> c(b) 55.08/55.08 )] 55.08/55.08 Infeasibility Conditions: 55.08/55.08 c(b) -> x:S 55.08/55.08 55.08/55.08 Problem 1: 55.08/55.08 55.08/55.08 Obtaining a model using Mace4: 55.08/55.08 55.08/55.08 -> Usable Rules: 55.08/55.08 Empty 55.08/55.08 55.08/55.08 -> Mace4 Output: 55.08/55.08 ============================== Mace4 ================================= 55.08/55.08 Mace4 (64) version 2009-11A, November 2009. 55.08/55.08 Process 47164 was started by ubuntu on ubuntu, 55.08/55.08 Wed Jul 14 10:41:20 2021 55.08/55.08 The command was "./mace4 -c -f /tmp/mace447151-2.in". 55.08/55.08 ============================== end of head =========================== 55.08/55.08 55.08/55.08 ============================== INPUT ================================= 55.08/55.08 55.08/55.08 % Reading from file /tmp/mace447151-2.in 55.08/55.08 55.08/55.08 assign(max_seconds,6). 55.08/55.08 55.08/55.08 formulas(assumptions). 55.08/55.08 ->(x1,y) -> ->(f(x1,x2,x3),f(y,x2,x3)) # label(congruence). 55.08/55.08 ->(x2,y) -> ->(f(x1,x2,x3),f(x1,y,x3)) # label(congruence). 55.08/55.08 ->(x3,y) -> ->(f(x1,x2,x3),f(x1,x2,y)) # label(congruence). 55.08/55.08 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence). 55.08/55.08 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence). 55.08/55.08 ->(x1,y) -> ->(k(x1),k(y)) # label(congruence). 55.08/55.08 end_of_list. 55.08/55.08 55.08/55.08 formulas(goals). 55.08/55.08 (exists x1 ->(c(b),x1)) # label(goal). 55.08/55.08 end_of_list. 55.08/55.08 55.08/55.08 ============================== end of input ========================== 55.08/55.08 55.08/55.08 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 55.08/55.08 55.08/55.08 % Formulas that are not ordinary clauses: 55.08/55.08 1 ->(x1,y) -> ->(f(x1,x2,x3),f(y,x2,x3)) # label(congruence) # label(non_clause). [assumption]. 55.08/55.08 2 ->(x2,y) -> ->(f(x1,x2,x3),f(x1,y,x3)) # label(congruence) # label(non_clause). [assumption]. 55.08/55.08 3 ->(x3,y) -> ->(f(x1,x2,x3),f(x1,x2,y)) # label(congruence) # label(non_clause). [assumption]. 55.08/55.08 4 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 55.08/55.08 5 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence) # label(non_clause). [assumption]. 55.08/55.08 6 ->(x1,y) -> ->(k(x1),k(y)) # label(congruence) # label(non_clause). [assumption]. 55.08/55.08 7 (exists x1 ->(c(b),x1)) # label(goal) # label(non_clause) # label(goal). [goal]. 55.08/55.08 55.08/55.08 ============================== end of process non-clausal formulas === 55.08/55.08 55.08/55.08 ============================== CLAUSES FOR SEARCH ==================== 55.08/55.08 55.08/55.08 formulas(mace4_clauses). 55.08/55.08 -->(x,y) | ->(f(x,z,u),f(y,z,u)) # label(congruence). 55.08/55.08 -->(x,y) | ->(f(z,x,u),f(z,y,u)) # label(congruence). 55.08/55.08 -->(x,y) | ->(f(z,u,x),f(z,u,y)) # label(congruence). 55.08/55.08 -->(x,y) | ->(h(x),h(y)) # label(congruence). 55.08/55.08 -->(x,y) | ->(c(x),c(y)) # label(congruence). 55.08/55.08 -->(x,y) | ->(k(x),k(y)) # label(congruence). 55.08/55.08 -->(c(b),x) # label(goal). 55.08/55.08 end_of_list. 55.08/55.08 55.08/55.08 ============================== end of clauses for search ============= 55.08/55.08 55.08/55.08 % There are no natural numbers in the input. 55.08/55.08 55.08/55.08 ============================== DOMAIN SIZE 2 ========================= 55.08/55.08 55.08/55.08 ============================== MODEL ================================= 55.08/55.08 55.08/55.08 interpretation( 2, [number=1, seconds=0], [ 55.08/55.08 55.08/55.08 function(b, [ 0 ]), 55.08/55.08 55.08/55.08 function(h(_), [ 0, 0 ]), 55.08/55.08 55.08/55.08 function(c(_), [ 0, 0 ]), 55.08/55.08 55.08/55.08 function(k(_), [ 0, 0 ]), 55.08/55.08 55.08/55.08 function(f(_,_,_), [ 55.08/55.08 0, 0, 55.08/55.08 0, 0, 55.08/55.08 0, 0, 55.08/55.08 0, 0 ]), 55.08/55.08 55.08/55.08 relation(->(_,_), [ 55.08/55.08 0, 0, 55.08/55.08 0, 0 ]) 55.08/55.08 ]). 55.08/55.08 55.08/55.08 ============================== end of model ========================== 55.08/55.08 55.08/55.08 ============================== STATISTICS ============================ 55.08/55.08 55.08/55.08 For domain size 2. 55.08/55.08 55.08/55.08 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 55.08/55.08 Ground clauses: seen=62, kept=62. 55.08/55.08 Selections=15, assignments=15, propagations=4, current_models=1. 55.08/55.08 Rewrite_terms=124, rewrite_bools=66, indexes=5. 55.08/55.08 Rules_from_neg_clauses=0, cross_offs=0. 55.08/55.08 55.08/55.08 ============================== end of statistics ===================== 55.08/55.08 55.08/55.08 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 55.08/55.08 55.08/55.08 Exiting with 1 model. 55.08/55.08 55.08/55.08 Process 47164 exit (max_models) Wed Jul 14 10:41:20 2021 55.08/55.08 The process finished Wed Jul 14 10:41:20 2021 55.08/55.08 55.08/55.08 55.08/55.08 Mace4 cooked interpretation: 55.08/55.08 55.08/55.08 55.08/55.08 55.08/55.08 The problem is infeasible. 55.08/55.08 55.08/55.08 55.08/55.08 The problem is not joinable. 55.08/55.08 75.83user 4.37system 0:55.80elapsed 143%CPU (0avgtext+0avgdata 1974268maxresident)k 55.08/55.08 0inputs+0outputs (0major+1365097minor)pagefaults 0swaps