62.037/62.037 NO 62.037/62.037 62.037/62.037 Problem 1: 62.037/62.037 62.037/62.037 62.037/62.037 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 62.037/62.037 Confluence Problem: 62.037/62.037 (VAR vNonEmpty:S x:S y:S) 62.037/62.037 (STRATEGY CONTEXTSENSITIVE 62.037/62.037 (a) 62.037/62.037 (f 1) 62.037/62.037 (g 1) 62.037/62.037 (b) 62.037/62.037 (c 1 2) 62.037/62.037 (fSNonEmpty) 62.037/62.037 (h 1) 62.037/62.037 ) 62.037/62.037 (RULES 62.037/62.037 a -> b 62.037/62.037 f(x:S) -> c(x:S,y:S) | g(x:S) ->* y:S, y:S ->* h(x:S) 62.037/62.037 g(a) -> h(b) 62.037/62.037 ) 62.037/62.037 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 62.037/62.037 62.037/62.037 62.037/62.037 Problem 1: 62.037/62.037 62.037/62.037 Inlining of Conditions Processor [STERN17]: 62.037/62.037 62.037/62.037 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 62.037/62.037 Confluence Problem: 62.037/62.037 (VAR vNonEmpty:S x:S y:S) 62.037/62.037 (STRATEGY CONTEXTSENSITIVE 62.037/62.037 (a) 62.037/62.037 (f 1) 62.037/62.037 (g 1) 62.037/62.037 (b) 62.037/62.037 (c 1 2) 62.037/62.037 (fSNonEmpty) 62.037/62.037 (h 1) 62.037/62.037 ) 62.037/62.037 (RULES 62.037/62.037 a -> b 62.037/62.037 f(x:S) -> c(x:S,g(x:S)) | g(x:S) ->* h(x:S) 62.037/62.037 g(a) -> h(b) 62.037/62.037 ) 62.037/62.037 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 62.037/62.037 62.037/62.037 62.037/62.037 Problem 1: 62.037/62.037 62.037/62.037 Clean CTRS Processor: 62.037/62.037 62.037/62.037 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 62.037/62.037 Confluence Problem: 62.037/62.037 (STRATEGY CONTEXTSENSITIVE 62.037/62.037 (a) 62.037/62.037 (f 1) 62.037/62.037 (g 1) 62.037/62.037 (b) 62.037/62.037 (c 1 2) 62.037/62.037 (fSNonEmpty) 62.037/62.037 (h 1) 62.037/62.037 ) 62.037/62.037 (RULES 62.037/62.037 a -> b 62.037/62.037 g(a) -> h(b) 62.037/62.037 ) 62.037/62.037 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 62.037/62.037 62.037/62.037 CRule InfChecker Info: 62.037/62.037 a -> b 62.037/62.037 Rule remains 62.037/62.037 Proof: 62.037/62.037 NO_CONDS 62.037/62.037 62.037/62.037 CRule InfChecker Info: 62.037/62.037 f(x:S) -> c(x:S,g(x:S)) | g(x:S) ->* h(x:S) 62.037/62.037 Rule deleted 62.037/62.037 Proof: 62.037/62.037 YES 62.037/62.037 62.037/62.037 Problem 1: 62.037/62.037 62.037/62.037 Infeasibility Problem: 62.037/62.037 [(VAR vNonEmpty:S vNonEmpty:S:S x:S:S y:S:S) 62.037/62.037 (STRATEGY CONTEXTSENSITIVE 62.037/62.037 (a) 62.037/62.037 (f 1) 62.037/62.037 (g 1) 62.037/62.037 (b) 62.037/62.037 (c 1 2) 62.037/62.037 (fSNonEmpty) 62.037/62.037 (h 1) 62.037/62.037 ) 62.037/62.037 (RULES 62.037/62.037 a -> b 62.037/62.037 f(x:S:S) -> c(x:S:S,g(x:S:S)) | g(x:S:S) ->* h(x:S:S) 62.037/62.037 g(a) -> h(b) 62.037/62.037 )] 62.037/62.037 62.037/62.037 Infeasibility Conditions: 62.037/62.037 g(x:S:S) ->* h(x:S:S) 62.037/62.037 62.037/62.037 Problem 1: 62.037/62.037 62.037/62.037 Obtaining a model using Mace4: 62.037/62.037 62.037/62.037 -> Usable Rules: 62.037/62.037 a -> b 62.037/62.037 f(x:S:S) -> c(x:S:S,g(x:S:S)) | g(x:S:S) ->* h(x:S:S) 62.037/62.037 g(a) -> h(b) 62.037/62.037 62.037/62.037 -> Mace4 Output: 62.037/62.037 ============================== Mace4 ================================= 62.037/62.037 Mace4 (64) version 2009-11A, November 2009. 62.037/62.037 Process 40416 was started by ubuntu on ubuntu, 62.037/62.037 Wed Jul 14 10:16:15 2021 62.037/62.037 The command was "./mace4 -c -f /tmp/mace440403-2.in". 62.037/62.037 ============================== end of head =========================== 62.037/62.037 62.037/62.037 ============================== INPUT ================================= 62.037/62.037 62.037/62.037 % Reading from file /tmp/mace440403-2.in 62.037/62.037 62.037/62.037 assign(max_seconds,20). 62.037/62.037 62.037/62.037 formulas(assumptions). 62.037/62.037 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence). 62.037/62.037 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence). 62.037/62.037 ->(x1,y) -> ->(c(x1,x2),c(y,x2)) # label(congruence). 62.037/62.037 ->(x2,y) -> ->(c(x1,x2),c(x1,y)) # label(congruence). 62.037/62.037 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence). 62.037/62.037 ->(a,b) # label(replacement). 62.037/62.037 ->*(g(x2),h(x2)) -> ->(f(x2),c(x2,g(x2))) # label(replacement). 62.037/62.037 ->(g(a),h(b)) # label(replacement). 62.037/62.037 ->*(x,x) # label(reflexivity). 62.037/62.037 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 62.037/62.037 end_of_list. 62.037/62.037 62.037/62.037 formulas(goals). 62.037/62.037 (exists x2 ->*(g(x2),h(x2))) # label(goal). 62.037/62.037 end_of_list. 62.037/62.037 62.037/62.037 ============================== end of input ========================== 62.037/62.037 62.037/62.037 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 62.037/62.037 62.037/62.037 % Formulas that are not ordinary clauses: 62.037/62.037 1 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence) # label(non_clause). [assumption]. 62.037/62.037 2 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 62.037/62.037 3 ->(x1,y) -> ->(c(x1,x2),c(y,x2)) # label(congruence) # label(non_clause). [assumption]. 62.037/62.037 4 ->(x2,y) -> ->(c(x1,x2),c(x1,y)) # label(congruence) # label(non_clause). [assumption]. 62.037/62.037 5 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 62.037/62.037 6 ->*(g(x2),h(x2)) -> ->(f(x2),c(x2,g(x2))) # label(replacement) # label(non_clause). [assumption]. 62.037/62.037 7 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 62.037/62.037 8 (exists x2 ->*(g(x2),h(x2))) # label(goal) # label(non_clause) # label(goal). [goal]. 62.037/62.037 62.037/62.037 ============================== end of process non-clausal formulas === 62.037/62.037 62.037/62.037 ============================== CLAUSES FOR SEARCH ==================== 62.037/62.037 62.037/62.037 formulas(mace4_clauses). 62.037/62.037 -->(x,y) | ->(f(x),f(y)) # label(congruence). 62.037/62.037 -->(x,y) | ->(g(x),g(y)) # label(congruence). 62.037/62.037 -->(x,y) | ->(c(x,z),c(y,z)) # label(congruence). 62.037/62.037 -->(x,y) | ->(c(z,x),c(z,y)) # label(congruence). 62.037/62.037 -->(x,y) | ->(h(x),h(y)) # label(congruence). 62.037/62.037 ->(a,b) # label(replacement). 62.037/62.037 -->*(g(x),h(x)) | ->(f(x),c(x,g(x))) # label(replacement). 62.037/62.037 ->(g(a),h(b)) # label(replacement). 62.037/62.037 ->*(x,x) # label(reflexivity). 62.037/62.037 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 62.037/62.037 -->*(g(x),h(x)) # label(goal). 62.037/62.037 end_of_list. 62.037/62.037 62.037/62.037 ============================== end of clauses for search ============= 62.037/62.037 62.037/62.037 % There are no natural numbers in the input. 62.037/62.037 62.037/62.037 ============================== DOMAIN SIZE 2 ========================= 62.037/62.037 62.037/62.037 ============================== STATISTICS ============================ 62.037/62.037 62.037/62.037 For domain size 2. 62.037/62.037 62.037/62.037 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 62.037/62.037 Ground clauses: seen=44, kept=40. 62.037/62.037 Selections=8, assignments=15, propagations=35, current_models=0. 62.037/62.037 Rewrite_terms=149, rewrite_bools=113, indexes=38. 62.037/62.037 Rules_from_neg_clauses=13, cross_offs=13. 62.037/62.037 62.037/62.037 ============================== end of statistics ===================== 62.037/62.037 62.037/62.037 ============================== DOMAIN SIZE 3 ========================= 62.037/62.037 62.037/62.037 ============================== MODEL ================================= 62.037/62.037 62.037/62.037 interpretation( 3, [number=1, seconds=0], [ 62.037/62.037 62.037/62.037 function(a, [ 0 ]), 62.037/62.037 62.037/62.037 function(b, [ 1 ]), 62.037/62.037 62.037/62.037 function(f(_), [ 0, 0, 0 ]), 62.037/62.037 62.037/62.037 function(g(_), [ 0, 1, 0 ]), 62.037/62.037 62.037/62.037 function(h(_), [ 2, 0, 2 ]), 62.037/62.037 62.037/62.037 function(c(_,_), [ 62.037/62.037 0, 0, 0, 62.037/62.037 0, 0, 0, 62.037/62.037 0, 0, 0 ]), 62.037/62.037 62.037/62.037 relation(->*(_,_), [ 62.037/62.037 1, 1, 0, 62.037/62.037 0, 1, 0, 62.037/62.037 1, 1, 1 ]), 62.037/62.037 62.037/62.037 relation(->(_,_), [ 62.037/62.037 1, 1, 0, 62.037/62.037 0, 0, 0, 62.037/62.037 1, 0, 1 ]) 62.037/62.037 ]). 62.037/62.037 62.037/62.037 ============================== end of model ========================== 62.037/62.037 62.037/62.037 ============================== STATISTICS ============================ 62.037/62.037 62.037/62.037 For domain size 3. 62.037/62.037 62.037/62.037 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 62.037/62.037 Ground clauses: seen=119, kept=110. 62.037/62.037 Selections=24, assignments=39, propagations=49, current_models=1. 62.037/62.037 Rewrite_terms=355, rewrite_bools=323, indexes=50. 62.037/62.037 Rules_from_neg_clauses=7, cross_offs=27. 62.037/62.037 62.037/62.037 ============================== end of statistics ===================== 62.037/62.037 62.037/62.037 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 62.037/62.037 62.037/62.037 Exiting with 1 model. 62.037/62.037 62.037/62.037 Process 40416 exit (max_models) Wed Jul 14 10:16:15 2021 62.037/62.037 The process finished Wed Jul 14 10:16:15 2021 62.037/62.037 62.037/62.037 62.037/62.037 Mace4 cooked interpretation: 62.037/62.037 62.037/62.037 62.037/62.037 62.037/62.037 The problem is infeasible. 62.037/62.037 62.037/62.037 62.037/62.037 CRule InfChecker Info: 62.037/62.037 g(a) -> h(b) 62.037/62.037 Rule remains 62.037/62.037 Proof: 62.037/62.037 NO_CONDS 62.037/62.037 62.037/62.037 Problem 1: 62.037/62.037 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 62.037/62.037 Confluence Problem: 62.037/62.037 (STRATEGY CONTEXTSENSITIVE 62.037/62.037 (a) 62.037/62.037 (f 1) 62.037/62.037 (g 1) 62.037/62.037 (b) 62.037/62.037 (c 1 2) 62.037/62.037 (fSNonEmpty) 62.037/62.037 (h 1) 62.037/62.037 ) 62.037/62.037 (RULES 62.037/62.037 a -> b 62.037/62.037 g(a) -> h(b) 62.037/62.037 ) 62.037/62.037 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 62.037/62.037 62.037/62.037 Critical Pairs Processor: 62.037/62.037 -> Rules: 62.037/62.037 a -> b 62.037/62.037 g(a) -> h(b) 62.037/62.037 -> Vars: 62.037/62.037 62.037/62.037 -> FVars: 62.037/62.037 62.037/62.037 -> PVars: 62.037/62.037 62.037/62.037 62.037/62.037 -> Rlps: 62.037/62.037 crule: a -> b, id: 1, possubterms: a-> [] 62.037/62.037 crule: g(a) -> h(b), id: 2, possubterms: g(a)-> [], a-> [1] 62.037/62.037 62.037/62.037 -> Unifications: 62.037/62.037 R2 unifies with R1 at p: [1], l: g(a), lp: a, conds: {}, sig: {}, l': a, r: h(b), r': b 62.037/62.037 62.037/62.037 -> Critical pairs info: 62.037/62.037 => Not trivial, Not overlay, N1 62.037/62.037 62.037/62.037 -> Problem conclusions: 62.037/62.037 Left linear, Right linear, Linear 62.037/62.037 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 62.037/62.037 CTRS Type: 1 62.037/62.037 Deterministic, Strongly deterministic 62.037/62.037 Oriented CTRS, Properly oriented CTRS, Join CTRS 62.037/62.037 Maybe right-stable CTRS, Not overlay CTRS 62.037/62.037 Normal CTRS, Almost normal CTRS 62.037/62.037 Maybe terminating CTRS, Maybe joinable CCPs 62.037/62.037 Maybe level confluent 62.037/62.037 Maybe confluent 62.037/62.037 62.037/62.037 Problem 1: 62.037/62.037 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 62.037/62.037 Confluence Problem: 62.037/62.037 (STRATEGY CONTEXTSENSITIVE 62.037/62.037 (a) 62.037/62.037 (f 1) 62.037/62.037 (g 1) 62.037/62.037 (b) 62.037/62.037 (c 1 2) 62.037/62.037 (fSNonEmpty) 62.037/62.037 (h 1) 62.037/62.037 ) 62.037/62.037 (RULES 62.037/62.037 a -> b 62.037/62.037 g(a) -> h(b) 62.037/62.037 ) 62.037/62.037 Critical Pairs: 62.037/62.037 => Not trivial, Not overlay, N1 62.037/62.037 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 62.037/62.037 62.037/62.037 Conditional Critical Pairs Distributor Processor 62.037/62.037 62.037/62.037 Problem 1: 62.037/62.037 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 62.037/62.037 Confluence Problem: 62.037/62.037 (STRATEGY CONTEXTSENSITIVE 62.037/62.037 (a) 62.037/62.037 (f 1) 62.037/62.037 (g 1) 62.037/62.037 (b) 62.037/62.037 (c 1 2) 62.037/62.037 (fSNonEmpty) 62.037/62.037 (h 1) 62.037/62.037 ) 62.037/62.037 (RULES 62.037/62.037 a -> b 62.037/62.037 g(a) -> h(b) 62.037/62.037 ) 62.037/62.037 Critical Pairs: 62.037/62.037 => Not trivial, Not overlay, N1 62.037/62.037 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 62.037/62.037 62.037/62.037 InfChecker Different Ground and Normal No Conditions CCP Terms Processor: 62.037/62.037 Proof: 62.037/62.037 YES 62.037/62.037 62.037/62.037 Problem 1: 62.037/62.037 62.037/62.037 Infeasibility Problem: 62.037/62.037 [(VAR vNonEmpty:S y:S) 62.037/62.037 (STRATEGY CONTEXTSENSITIVE 62.037/62.037 (a) 62.037/62.037 (g 1) 62.037/62.037 (b) 62.037/62.037 (fSNonEmpty) 62.037/62.037 (h 1) 62.037/62.037 ) 62.037/62.037 (RULES 62.037/62.037 a -> b 62.037/62.037 g(a) -> h(b) 62.037/62.037 )] 62.037/62.037 Infeasibility Conditions: 62.037/62.037 g(b) -> y:S 62.037/62.037 62.037/62.037 Problem 1: 62.037/62.037 62.037/62.037 Obtaining a model using Mace4: 62.037/62.037 62.037/62.037 -> Usable Rules: 62.037/62.037 g(a) -> h(b) 62.037/62.037 62.037/62.037 -> Mace4 Output: 62.037/62.037 ============================== Mace4 ================================= 62.037/62.037 Mace4 (64) version 2009-11A, November 2009. 62.037/62.037 Process 40460 was started by ubuntu on ubuntu, 62.037/62.037 Wed Jul 14 10:16:35 2021 62.037/62.037 The command was "./mace4 -c -f /tmp/mace440434-2.in". 62.037/62.037 ============================== end of head =========================== 62.037/62.037 62.037/62.037 ============================== INPUT ================================= 62.037/62.037 62.037/62.037 % Reading from file /tmp/mace440434-2.in 62.037/62.037 62.037/62.037 assign(max_seconds,6). 62.037/62.037 62.037/62.037 formulas(assumptions). 62.037/62.037 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence). 62.037/62.037 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence). 62.037/62.037 ->(g(a),h(b)) # label(replacement). 62.037/62.037 end_of_list. 62.037/62.037 62.037/62.037 formulas(goals). 62.037/62.037 (exists x1 ->(g(b),x1)) # label(goal). 62.037/62.037 end_of_list. 62.037/62.037 62.037/62.037 ============================== end of input ========================== 62.037/62.037 62.037/62.037 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 62.037/62.037 62.037/62.037 % Formulas that are not ordinary clauses: 62.037/62.037 1 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 62.037/62.037 2 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 62.037/62.037 3 (exists x1 ->(g(b),x1)) # label(goal) # label(non_clause) # label(goal). [goal]. 62.037/62.037 62.037/62.037 ============================== end of process non-clausal formulas === 62.037/62.037 62.037/62.037 ============================== CLAUSES FOR SEARCH ==================== 62.037/62.037 62.037/62.037 formulas(mace4_clauses). 62.037/62.037 -->(x,y) | ->(g(x),g(y)) # label(congruence). 62.037/62.037 -->(x,y) | ->(h(x),h(y)) # label(congruence). 62.037/62.037 ->(g(a),h(b)) # label(replacement). 62.037/62.037 -->(g(b),x) # label(goal). 62.037/62.037 end_of_list. 62.037/62.037 62.037/62.037 ============================== end of clauses for search ============= 62.037/62.037 62.037/62.037 % There are no natural numbers in the input. 62.037/62.037 62.037/62.037 ============================== DOMAIN SIZE 2 ========================= 62.037/62.037 62.037/62.037 ============================== MODEL ================================= 62.037/62.037 62.037/62.037 interpretation( 2, [number=1, seconds=0], [ 62.037/62.037 62.037/62.037 function(a, [ 0 ]), 62.037/62.037 62.037/62.037 function(b, [ 1 ]), 62.037/62.037 62.037/62.037 function(g(_), [ 0, 1 ]), 62.037/62.037 62.037/62.037 function(h(_), [ 0, 1 ]), 62.037/62.037 62.037/62.037 relation(->(_,_), [ 62.037/62.037 0, 1, 62.037/62.037 0, 0 ]) 62.037/62.037 ]). 62.037/62.037 62.037/62.037 ============================== end of model ========================== 62.037/62.037 62.037/62.037 ============================== STATISTICS ============================ 62.037/62.037 62.037/62.037 For domain size 2. 62.037/62.037 62.037/62.037 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 62.037/62.037 Ground clauses: seen=11, kept=11. 62.037/62.037 Selections=6, assignments=8, propagations=12, current_models=1. 62.037/62.037 Rewrite_terms=41, rewrite_bools=22, indexes=18. 62.037/62.037 Rules_from_neg_clauses=4, cross_offs=4. 62.037/62.037 62.037/62.037 ============================== end of statistics ===================== 62.037/62.037 62.037/62.037 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 62.037/62.037 62.037/62.037 Exiting with 1 model. 62.037/62.037 62.037/62.037 Process 40460 exit (max_models) Wed Jul 14 10:16:35 2021 62.037/62.037 The process finished Wed Jul 14 10:16:35 2021 62.037/62.037 62.037/62.037 62.037/62.037 Mace4 cooked interpretation: 62.037/62.037 62.037/62.037 62.037/62.037 62.037/62.037 The problem is infeasible. 62.037/62.037 YES 62.037/62.037 62.037/62.037 Problem 1: 62.037/62.037 62.037/62.037 Infeasibility Problem: 62.037/62.037 [(VAR vNonEmpty:S x:S) 62.037/62.037 (STRATEGY CONTEXTSENSITIVE 62.037/62.037 (a) 62.037/62.037 (g 1) 62.037/62.037 (b) 62.037/62.037 (fSNonEmpty) 62.037/62.037 (h 1) 62.037/62.037 ) 62.037/62.037 (RULES 62.037/62.037 a -> b 62.037/62.037 g(a) -> h(b) 62.037/62.037 )] 62.037/62.037 Infeasibility Conditions: 62.037/62.037 h(b) -> x:S 62.037/62.037 62.037/62.037 Problem 1: 62.037/62.037 62.037/62.037 Obtaining a model using Mace4: 62.037/62.037 62.037/62.037 -> Usable Rules: 62.037/62.037 Empty 62.037/62.037 62.037/62.037 -> Mace4 Output: 62.037/62.037 ============================== Mace4 ================================= 62.037/62.037 Mace4 (64) version 2009-11A, November 2009. 62.037/62.037 Process 40497 was started by ubuntu on ubuntu, 62.037/62.037 Wed Jul 14 10:16:55 2021 62.037/62.037 The command was "./mace4 -c -f /tmp/mace440484-2.in". 62.037/62.037 ============================== end of head =========================== 62.037/62.037 62.037/62.037 ============================== INPUT ================================= 62.037/62.037 62.037/62.037 % Reading from file /tmp/mace440484-2.in 62.037/62.037 62.037/62.037 assign(max_seconds,6). 62.037/62.037 62.037/62.037 formulas(assumptions). 62.037/62.037 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence). 62.037/62.037 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence). 62.037/62.037 end_of_list. 62.037/62.037 62.037/62.037 formulas(goals). 62.037/62.037 (exists x1 ->(h(b),x1)) # label(goal). 62.037/62.037 end_of_list. 62.037/62.037 62.037/62.037 ============================== end of input ========================== 62.037/62.037 62.037/62.037 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 62.037/62.037 62.037/62.037 % Formulas that are not ordinary clauses: 62.037/62.037 1 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 62.037/62.037 2 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 62.037/62.037 3 (exists x1 ->(h(b),x1)) # label(goal) # label(non_clause) # label(goal). [goal]. 62.037/62.037 62.037/62.037 ============================== end of process non-clausal formulas === 62.037/62.037 62.037/62.037 ============================== CLAUSES FOR SEARCH ==================== 62.037/62.037 62.037/62.037 formulas(mace4_clauses). 62.037/62.037 -->(x,y) | ->(g(x),g(y)) # label(congruence). 62.037/62.037 -->(x,y) | ->(h(x),h(y)) # label(congruence). 62.037/62.037 -->(h(b),x) # label(goal). 62.037/62.037 end_of_list. 62.037/62.037 62.037/62.037 ============================== end of clauses for search ============= 62.037/62.037 62.037/62.037 % There are no natural numbers in the input. 62.037/62.037 62.037/62.037 ============================== DOMAIN SIZE 2 ========================= 62.037/62.037 62.037/62.037 ============================== MODEL ================================= 62.037/62.037 62.037/62.037 interpretation( 2, [number=1, seconds=0], [ 62.037/62.037 62.037/62.037 function(b, [ 0 ]), 62.037/62.037 62.037/62.037 function(g(_), [ 0, 0 ]), 62.037/62.037 62.037/62.037 function(h(_), [ 0, 0 ]), 62.037/62.037 62.037/62.037 relation(->(_,_), [ 62.037/62.037 0, 0, 62.037/62.037 0, 0 ]) 62.037/62.037 ]). 62.037/62.037 62.037/62.037 ============================== end of model ========================== 62.037/62.037 62.037/62.037 ============================== STATISTICS ============================ 62.037/62.037 62.037/62.037 For domain size 2. 62.037/62.037 62.037/62.037 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 62.037/62.037 Ground clauses: seen=10, kept=10. 62.037/62.037 Selections=5, assignments=5, propagations=4, current_models=1. 62.037/62.037 Rewrite_terms=20, rewrite_bools=14, indexes=5. 62.037/62.037 Rules_from_neg_clauses=0, cross_offs=0. 62.037/62.037 62.037/62.037 ============================== end of statistics ===================== 62.037/62.037 62.037/62.037 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 62.037/62.037 62.037/62.037 Exiting with 1 model. 62.037/62.037 62.037/62.037 Process 40497 exit (max_models) Wed Jul 14 10:16:55 2021 62.037/62.037 The process finished Wed Jul 14 10:16:55 2021 62.037/62.037 62.037/62.037 62.037/62.037 Mace4 cooked interpretation: 62.037/62.037 62.037/62.037 62.037/62.037 62.037/62.037 The problem is infeasible. 62.037/62.037 62.037/62.037 62.037/62.037 The problem is not joinable. 62.037/62.037 78.51user 4.94system 1:02.37elapsed 133%CPU (0avgtext+0avgdata 3773384maxresident)k 62.037/62.037 0inputs+0outputs (0major+2329869minor)pagefaults 0swaps