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