25.024/25.024 NO 25.024/25.024 25.024/25.024 Problem 1: 25.024/25.024 25.024/25.024 25.024/25.024 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.024/25.024 Confluence Problem: 25.024/25.024 (VAR vNonEmpty:S v:S w:S y:S z:S xs:S xs':S ys':S) 25.024/25.024 (STRATEGY CONTEXTSENSITIVE 25.024/25.024 (ssp 1 2) 25.024/25.024 (sub 1 2) 25.024/25.024 (0) 25.024/25.024 (cons 1 2) 25.024/25.024 (fSNonEmpty) 25.024/25.024 (nil) 25.024/25.024 (s 1) 25.024/25.024 ) 25.024/25.024 (RULES 25.024/25.024 ssp(cons(y:S,ys':S),v:S) -> cons(y:S,xs':S) | sub(v:S,y:S) ->* w:S, ssp(ys':S,w:S) ->* xs':S 25.024/25.024 ssp(cons(y:S,ys':S),v:S) -> xs:S | ssp(ys':S,v:S) ->* xs:S 25.024/25.024 ssp(nil,0) -> nil 25.024/25.024 sub(s(v:S),s(w:S)) -> z:S | sub(v:S,w:S) ->* z:S 25.024/25.024 sub(z:S,0) -> z:S 25.024/25.024 ) 25.024/25.024 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.024/25.024 25.024/25.024 25.024/25.024 Problem 1: 25.024/25.024 25.024/25.024 Inlining of Conditions Processor [STERN17]: 25.024/25.024 25.024/25.024 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.024/25.024 Confluence Problem: 25.024/25.024 (VAR vNonEmpty:S v:S w:S y:S z:S xs:S xs':S ys':S) 25.024/25.024 (STRATEGY CONTEXTSENSITIVE 25.024/25.024 (ssp 1 2) 25.024/25.024 (sub 1 2) 25.024/25.024 (0) 25.024/25.024 (cons 1 2) 25.024/25.024 (fSNonEmpty) 25.024/25.024 (nil) 25.024/25.024 (s 1) 25.024/25.024 ) 25.024/25.024 (RULES 25.024/25.024 ssp(cons(y:S,ys':S),v:S) -> ssp(ys':S,v:S) 25.024/25.024 ssp(cons(y:S,ys':S),v:S) -> cons(y:S,ssp(ys':S,sub(v:S,y:S))) 25.024/25.024 ssp(nil,0) -> nil 25.024/25.024 sub(s(v:S),s(w:S)) -> sub(v:S,w:S) 25.024/25.024 sub(z:S,0) -> z:S 25.024/25.024 ) 25.024/25.024 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.024/25.024 25.024/25.024 25.024/25.024 Problem 1: 25.024/25.024 25.024/25.024 Clean CTRS Processor: 25.024/25.024 25.024/25.024 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.024/25.024 Confluence Problem: 25.024/25.024 (VAR v:S w:S y:S z:S ys':S) 25.024/25.024 (STRATEGY CONTEXTSENSITIVE 25.024/25.024 (ssp 1 2) 25.024/25.024 (sub 1 2) 25.024/25.024 (0) 25.024/25.024 (cons 1 2) 25.024/25.024 (fSNonEmpty) 25.024/25.024 (nil) 25.024/25.024 (s 1) 25.024/25.024 ) 25.024/25.024 (RULES 25.024/25.024 ssp(cons(y:S,ys':S),v:S) -> ssp(ys':S,v:S) 25.024/25.024 ssp(cons(y:S,ys':S),v:S) -> cons(y:S,ssp(ys':S,sub(v:S,y:S))) 25.024/25.024 ssp(nil,0) -> nil 25.024/25.024 sub(s(v:S),s(w:S)) -> sub(v:S,w:S) 25.024/25.024 sub(z:S,0) -> z:S 25.024/25.024 ) 25.024/25.024 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.024/25.024 25.024/25.024 CRule InfChecker Info: 25.024/25.024 ssp(cons(y:S,ys':S),v:S) -> ssp(ys':S,v:S) 25.024/25.024 Rule remains 25.024/25.024 Proof: 25.024/25.024 NO_CONDS 25.024/25.024 25.024/25.024 CRule InfChecker Info: 25.024/25.024 ssp(cons(y:S,ys':S),v:S) -> cons(y:S,ssp(ys':S,sub(v:S,y:S))) 25.024/25.024 Rule remains 25.024/25.024 Proof: 25.024/25.024 NO_CONDS 25.024/25.024 25.024/25.024 CRule InfChecker Info: 25.024/25.024 ssp(nil,0) -> nil 25.024/25.024 Rule remains 25.024/25.024 Proof: 25.024/25.024 NO_CONDS 25.024/25.024 25.024/25.024 CRule InfChecker Info: 25.024/25.024 sub(s(v:S),s(w:S)) -> sub(v:S,w:S) 25.024/25.024 Rule remains 25.024/25.024 Proof: 25.024/25.024 NO_CONDS 25.024/25.024 25.024/25.024 CRule InfChecker Info: 25.024/25.024 sub(z:S,0) -> z:S 25.024/25.024 Rule remains 25.024/25.024 Proof: 25.024/25.024 NO_CONDS 25.024/25.024 25.024/25.024 Problem 1: 25.024/25.024 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.024/25.024 Confluence Problem: 25.024/25.024 (VAR v:S w:S y:S z:S ys':S) 25.024/25.024 (STRATEGY CONTEXTSENSITIVE 25.024/25.024 (ssp 1 2) 25.024/25.024 (sub 1 2) 25.024/25.024 (0) 25.024/25.024 (cons 1 2) 25.024/25.024 (fSNonEmpty) 25.024/25.024 (nil) 25.024/25.024 (s 1) 25.024/25.024 ) 25.024/25.024 (RULES 25.024/25.024 ssp(cons(y:S,ys':S),v:S) -> ssp(ys':S,v:S) 25.024/25.024 ssp(cons(y:S,ys':S),v:S) -> cons(y:S,ssp(ys':S,sub(v:S,y:S))) 25.024/25.024 ssp(nil,0) -> nil 25.024/25.024 sub(s(v:S),s(w:S)) -> sub(v:S,w:S) 25.024/25.024 sub(z:S,0) -> z:S 25.024/25.024 ) 25.024/25.024 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.024/25.024 25.024/25.024 Critical Pairs Processor: 25.024/25.024 -> Rules: 25.024/25.024 ssp(cons(y:S,ys':S),v:S) -> ssp(ys':S,v:S) 25.024/25.024 ssp(cons(y:S,ys':S),v:S) -> cons(y:S,ssp(ys':S,sub(v:S,y:S))) 25.024/25.024 ssp(nil,0) -> nil 25.024/25.024 sub(s(v:S),s(w:S)) -> sub(v:S,w:S) 25.024/25.024 sub(z:S,0) -> z:S 25.024/25.024 -> Vars: 25.024/25.024 "v", "y", "ys'", "v", "y", "ys'", "v", "w", "z" 25.024/25.024 -> FVars: 25.024/25.024 "x8", "x9", "x10", "x11", "x12", "x13", "x14", "x15", "x16" 25.024/25.024 -> PVars: 25.024/25.024 "v": ["x8", "x11", "x14"], "y": ["x9", "x12"], "ys'": ["x10", "x13"], "w": ["x15"], "z": ["x16"] 25.024/25.024 25.024/25.024 -> Rlps: 25.024/25.024 crule: ssp(cons(x9:S,x10:S),x8:S) -> ssp(x10:S,x8:S), id: 1, possubterms: ssp(cons(x9:S,x10:S),x8:S)-> [], cons(x9:S,x10:S)-> [1] 25.024/25.024 crule: ssp(cons(x12:S,x13:S),x11:S) -> cons(x12:S,ssp(x13:S,sub(x11:S,x12:S))), id: 2, possubterms: ssp(cons(x12:S,x13:S),x11:S)-> [], cons(x12:S,x13:S)-> [1] 25.024/25.024 crule: ssp(nil,0) -> nil, id: 3, possubterms: ssp(nil,0)-> [], nil-> [1], 0-> [2] 25.024/25.024 crule: sub(s(x14:S),s(x15:S)) -> sub(x14:S,x15:S), id: 4, possubterms: sub(s(x14:S),s(x15:S))-> [], s(x14:S)-> [1], s(x15:S)-> [2] 25.024/25.024 crule: sub(x16:S,0) -> x16:S, id: 5, possubterms: sub(x16:S,0)-> [], 0-> [2] 25.024/25.024 25.024/25.024 -> Unifications: 25.024/25.024 R2 unifies with R1 at p: [], l: ssp(cons(x12:S,x13:S),x11:S), lp: ssp(cons(x12:S,x13:S),x11:S), conds: {}, sig: {x11:S -> v:S,x12:S -> y:S,x13:S -> ys':S}, l': ssp(cons(y:S,ys':S),v:S), r: cons(x12:S,ssp(x13:S,sub(x11:S,x12:S))), r': ssp(ys':S,v:S) 25.024/25.024 25.024/25.024 -> Critical pairs info: 25.024/25.024 => Not trivial, Overlay, N1 25.024/25.024 25.024/25.024 -> Problem conclusions: 25.024/25.024 Left linear, Not right linear, Not linear 25.024/25.024 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 25.024/25.024 CTRS Type: 1 25.024/25.024 Deterministic, Strongly deterministic 25.024/25.024 Oriented CTRS, Properly oriented CTRS, Join CTRS 25.024/25.024 Maybe right-stable CTRS, Overlay CTRS 25.024/25.024 Normal CTRS, Almost normal CTRS 25.024/25.024 Maybe terminating CTRS, Maybe joinable CCPs 25.024/25.024 Maybe level confluent 25.024/25.024 Maybe confluent 25.024/25.024 25.024/25.024 Problem 1: 25.024/25.024 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.024/25.024 Confluence Problem: 25.024/25.024 (VAR v:S w:S y:S z:S ys':S) 25.024/25.024 (STRATEGY CONTEXTSENSITIVE 25.024/25.024 (ssp 1 2) 25.024/25.024 (sub 1 2) 25.024/25.024 (0) 25.024/25.024 (cons 1 2) 25.024/25.024 (fSNonEmpty) 25.024/25.024 (nil) 25.024/25.024 (s 1) 25.024/25.024 ) 25.024/25.024 (RULES 25.024/25.024 ssp(cons(y:S,ys':S),v:S) -> ssp(ys':S,v:S) 25.024/25.024 ssp(cons(y:S,ys':S),v:S) -> cons(y:S,ssp(ys':S,sub(v:S,y:S))) 25.024/25.024 ssp(nil,0) -> nil 25.024/25.024 sub(s(v:S),s(w:S)) -> sub(v:S,w:S) 25.024/25.024 sub(z:S,0) -> z:S 25.024/25.024 ) 25.024/25.024 Critical Pairs: 25.024/25.024 => Not trivial, Overlay, N1 25.024/25.024 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.024/25.024 25.024/25.024 Conditional Critical Pairs Distributor Processor 25.024/25.024 25.024/25.024 Problem 1: 25.024/25.024 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.024/25.024 Confluence Problem: 25.024/25.024 (VAR v:S w:S y:S z:S ys':S) 25.024/25.024 (STRATEGY CONTEXTSENSITIVE 25.024/25.024 (ssp 1 2) 25.024/25.024 (sub 1 2) 25.024/25.024 (0) 25.024/25.024 (cons 1 2) 25.024/25.024 (fSNonEmpty) 25.024/25.024 (nil) 25.024/25.024 (s 1) 25.024/25.024 ) 25.024/25.024 (RULES 25.024/25.024 ssp(cons(y:S,ys':S),v:S) -> ssp(ys':S,v:S) 25.024/25.024 ssp(cons(y:S,ys':S),v:S) -> cons(y:S,ssp(ys':S,sub(v:S,y:S))) 25.024/25.024 ssp(nil,0) -> nil 25.024/25.024 sub(s(v:S),s(w:S)) -> sub(v:S,w:S) 25.024/25.024 sub(z:S,0) -> z:S 25.024/25.024 ) 25.024/25.024 Critical Pairs: 25.024/25.024 => Not trivial, Overlay, N1 25.024/25.024 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.024/25.024 25.024/25.024 Infeasible Convergence No Conditions CCP Processor: 25.024/25.024 Infeasible convergence? 25.024/25.024 YES 25.024/25.024 25.024/25.024 Problem 1: 25.024/25.024 25.024/25.024 Infeasibility Problem: 25.024/25.024 [(VAR vNonEmpty:S v:S w:S y:S z:S ys1:S) 25.024/25.024 (STRATEGY CONTEXTSENSITIVE 25.024/25.024 (ssp 1 2) 25.024/25.024 (sub 1 2) 25.024/25.024 (0) 25.024/25.024 (cons 1 2) 25.024/25.024 (cv) 25.024/25.024 (cy) 25.024/25.024 (cys1) 25.024/25.024 (fSNonEmpty) 25.024/25.024 (nil) 25.024/25.024 (s 1) 25.024/25.024 ) 25.024/25.024 (RULES 25.024/25.024 ssp(cons(y:S,ys1:S),v:S) -> ssp(ys1:S,v:S) 25.024/25.024 ssp(cons(y:S,ys1:S),v:S) -> cons(y:S,ssp(ys1:S,sub(v:S,y:S))) 25.024/25.024 ssp(nil,0) -> nil 25.024/25.024 sub(s(v:S),s(w:S)) -> sub(v:S,w:S) 25.024/25.024 sub(z:S,0) -> z:S 25.024/25.024 )] 25.024/25.024 Infeasibility Conditions: 25.024/25.024 ssp(cys1,cv) ->* z:S, cons(cy,ssp(cys1,sub(cv,cy))) ->* z:S 25.024/25.024 25.024/25.024 Problem 1: 25.024/25.024 25.024/25.024 Obtaining a model using Mace4: 25.024/25.024 25.024/25.024 -> Usable Rules: 25.024/25.024 ssp(cons(y:S,ys1:S),v:S) -> ssp(ys1:S,v:S) 25.024/25.024 ssp(cons(y:S,ys1:S),v:S) -> cons(y:S,ssp(ys1:S,sub(v:S,y:S))) 25.024/25.024 ssp(nil,0) -> nil 25.024/25.024 sub(s(v:S),s(w:S)) -> sub(v:S,w:S) 25.024/25.024 sub(z:S,0) -> z:S 25.024/25.024 25.024/25.024 -> Mace4 Output: 25.024/25.024 ============================== Mace4 ================================= 25.024/25.024 Mace4 (64) version 2009-11A, November 2009. 25.024/25.024 Process 46130 was started by ubuntu on ubuntu, 25.024/25.024 Wed Jul 14 10:37:49 2021 25.024/25.024 The command was "./mace4 -c -f /tmp/mace446119-2.in". 25.024/25.024 ============================== end of head =========================== 25.024/25.024 25.024/25.024 ============================== INPUT ================================= 25.024/25.024 25.024/25.024 % Reading from file /tmp/mace446119-2.in 25.024/25.024 25.024/25.024 assign(max_seconds,20). 25.024/25.024 25.024/25.024 formulas(assumptions). 25.024/25.024 ->(x1,y) -> ->(ssp(x1,x2),ssp(y,x2)) # label(congruence). 25.024/25.024 ->(x2,y) -> ->(ssp(x1,x2),ssp(x1,y)) # label(congruence). 25.024/25.024 ->(x1,y) -> ->(sub(x1,x2),sub(y,x2)) # label(congruence). 25.024/25.024 ->(x2,y) -> ->(sub(x1,x2),sub(x1,y)) # label(congruence). 25.024/25.024 ->(x1,y) -> ->(cons(x1,x2),cons(y,x2)) # label(congruence). 25.024/25.024 ->(x2,y) -> ->(cons(x1,x2),cons(x1,y)) # label(congruence). 25.024/25.024 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence). 25.024/25.024 ->(ssp(cons(x3,x5),x1),ssp(x5,x1)) # label(replacement). 25.024/25.024 ->(ssp(cons(x3,x5),x1),cons(x3,ssp(x5,sub(x1,x3)))) # label(replacement). 25.024/25.024 ->(ssp(nil,0),nil) # label(replacement). 25.024/25.024 ->(sub(s(x1),s(x2)),sub(x1,x2)) # label(replacement). 25.024/25.024 ->(sub(x4,0),x4) # label(replacement). 25.024/25.024 ->*(x,x) # label(reflexivity). 25.024/25.024 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 25.024/25.024 end_of_list. 25.024/25.024 25.024/25.024 formulas(goals). 25.024/25.024 (exists x4 (->*(ssp(cys1,cv),x4) & ->*(cons(cy,ssp(cys1,sub(cv,cy))),x4))) # label(goal). 25.024/25.024 end_of_list. 25.024/25.024 25.024/25.024 ============================== end of input ========================== 25.024/25.024 25.024/25.024 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 25.024/25.024 25.024/25.024 % Formulas that are not ordinary clauses: 25.024/25.024 1 ->(x1,y) -> ->(ssp(x1,x2),ssp(y,x2)) # label(congruence) # label(non_clause). [assumption]. 25.024/25.024 2 ->(x2,y) -> ->(ssp(x1,x2),ssp(x1,y)) # label(congruence) # label(non_clause). [assumption]. 25.024/25.024 3 ->(x1,y) -> ->(sub(x1,x2),sub(y,x2)) # label(congruence) # label(non_clause). [assumption]. 25.024/25.024 4 ->(x2,y) -> ->(sub(x1,x2),sub(x1,y)) # label(congruence) # label(non_clause). [assumption]. 25.024/25.024 5 ->(x1,y) -> ->(cons(x1,x2),cons(y,x2)) # label(congruence) # label(non_clause). [assumption]. 25.024/25.024 6 ->(x2,y) -> ->(cons(x1,x2),cons(x1,y)) # label(congruence) # label(non_clause). [assumption]. 25.024/25.024 7 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 25.024/25.024 8 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 25.024/25.024 9 (exists x4 (->*(ssp(cys1,cv),x4) & ->*(cons(cy,ssp(cys1,sub(cv,cy))),x4))) # label(goal) # label(non_clause) # label(goal). [goal]. 25.024/25.024 25.024/25.024 ============================== end of process non-clausal formulas === 25.024/25.024 25.024/25.024 ============================== CLAUSES FOR SEARCH ==================== 25.024/25.024 25.024/25.024 formulas(mace4_clauses). 25.024/25.024 -->(x,y) | ->(ssp(x,z),ssp(y,z)) # label(congruence). 25.024/25.024 -->(x,y) | ->(ssp(z,x),ssp(z,y)) # label(congruence). 25.024/25.024 -->(x,y) | ->(sub(x,z),sub(y,z)) # label(congruence). 25.024/25.024 -->(x,y) | ->(sub(z,x),sub(z,y)) # label(congruence). 25.024/25.024 -->(x,y) | ->(cons(x,z),cons(y,z)) # label(congruence). 25.024/25.024 -->(x,y) | ->(cons(z,x),cons(z,y)) # label(congruence). 25.024/25.024 -->(x,y) | ->(s(x),s(y)) # label(congruence). 25.024/25.024 ->(ssp(cons(x,y),z),ssp(y,z)) # label(replacement). 25.024/25.024 ->(ssp(cons(x,y),z),cons(x,ssp(y,sub(z,x)))) # label(replacement). 25.024/25.024 ->(ssp(nil,0),nil) # label(replacement). 25.024/25.024 ->(sub(s(x),s(y)),sub(x,y)) # label(replacement). 25.024/25.024 ->(sub(x,0),x) # label(replacement). 25.024/25.024 ->*(x,x) # label(reflexivity). 25.024/25.024 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 25.024/25.024 -->*(ssp(cys1,cv),x) | -->*(cons(cy,ssp(cys1,sub(cv,cy))),x) # label(goal). 25.024/25.024 end_of_list. 25.024/25.024 25.024/25.024 ============================== end of clauses for search ============= 25.024/25.024 25.024/25.024 % There are no natural numbers in the input. 25.024/25.024 25.024/25.024 ============================== DOMAIN SIZE 2 ========================= 25.024/25.024 25.024/25.024 ============================== STATISTICS ============================ 25.024/25.024 25.024/25.024 For domain size 2. 25.024/25.024 25.024/25.024 Current CPU time: 0.00 seconds (total CPU time: 0.07 seconds). 25.024/25.024 Ground clauses: seen=87, kept=83. 25.024/25.024 Selections=15212, assignments=30423, propagations=25562, current_models=0. 25.024/25.024 Rewrite_terms=472689, rewrite_bools=249238, indexes=80006. 25.024/25.024 Rules_from_neg_clauses=13044, cross_offs=13044. 25.024/25.024 25.024/25.024 ============================== end of statistics ===================== 25.024/25.024 25.024/25.024 ============================== DOMAIN SIZE 3 ========================= 25.024/25.024 25.024/25.024 ============================== MODEL ================================= 25.024/25.024 25.024/25.024 interpretation( 3, [number=1, seconds=0], [ 25.024/25.024 25.024/25.024 function(nil, [ 0 ]), 25.024/25.024 25.024/25.024 function(0, [ 0 ]), 25.024/25.024 25.024/25.024 function(cv, [ 0 ]), 25.024/25.024 25.024/25.024 function(cy, [ 0 ]), 25.024/25.024 25.024/25.024 function(cys1, [ 0 ]), 25.024/25.024 25.024/25.024 function(s(_), [ 0, 1, 2 ]), 25.024/25.024 25.024/25.024 function(ssp(_,_), [ 25.024/25.024 0, 0, 0, 25.024/25.024 2, 2, 2, 25.024/25.024 2, 2, 2 ]), 25.024/25.024 25.024/25.024 function(sub(_,_), [ 25.024/25.024 0, 0, 0, 25.024/25.024 1, 0, 2, 25.024/25.024 2, 0, 2 ]), 25.024/25.024 25.024/25.024 function(cons(_,_), [ 25.024/25.024 1, 1, 1, 25.024/25.024 1, 1, 1, 25.024/25.024 1, 1, 1 ]), 25.024/25.024 25.024/25.024 relation(->*(_,_), [ 25.024/25.024 1, 0, 0, 25.024/25.024 0, 1, 0, 25.024/25.024 1, 1, 1 ]), 25.024/25.024 25.024/25.024 relation(->(_,_), [ 25.024/25.024 1, 0, 0, 25.024/25.024 0, 1, 0, 25.024/25.024 1, 1, 1 ]) 25.024/25.024 ]). 25.024/25.024 25.024/25.024 ============================== end of model ========================== 25.024/25.024 25.024/25.024 ============================== STATISTICS ============================ 25.024/25.024 25.024/25.024 For domain size 3. 25.024/25.024 25.024/25.024 Current CPU time: 0.00 seconds (total CPU time: 0.07 seconds). 25.024/25.024 Ground clauses: seen=271, kept=262. 25.024/25.024 Selections=314, assignments=908, propagations=206, current_models=1. 25.024/25.024 Rewrite_terms=14557, rewrite_bools=4928, indexes=537. 25.024/25.024 Rules_from_neg_clauses=190, cross_offs=493. 25.024/25.024 25.024/25.024 ============================== end of statistics ===================== 25.024/25.024 25.024/25.024 User_CPU=0.07, System_CPU=0.00, Wall_clock=0. 25.024/25.024 25.024/25.024 Exiting with 1 model. 25.024/25.024 25.024/25.024 Process 46130 exit (max_models) Wed Jul 14 10:37:49 2021 25.024/25.024 The process finished Wed Jul 14 10:37:49 2021 25.024/25.024 25.024/25.024 25.024/25.024 Mace4 cooked interpretation: 25.024/25.024 25.024/25.024 25.024/25.024 25.024/25.024 The problem is infeasible. 25.024/25.024 25.024/25.024 25.024/25.024 The problem is not joinable. 25.024/25.024 25.61user 0.43system 0:25.24elapsed 103%CPU (0avgtext+0avgdata 62416maxresident)k 25.024/25.024 0inputs+0outputs (0major+54189minor)pagefaults 0swaps