45.047/45.047 NO 45.047/45.047 45.047/45.047 Problem 1: 45.047/45.047 45.047/45.047 45.047/45.047 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.047/45.047 Confluence Problem: 45.047/45.047 (VAR vNonEmpty:S x:S) 45.047/45.047 (STRATEGY CONTEXTSENSITIVE 45.047/45.047 (p 1) 45.047/45.047 (q 1) 45.047/45.047 (r 1) 45.047/45.047 (s 1) 45.047/45.047 (0) 45.047/45.047 (1) 45.047/45.047 (fSNonEmpty) 45.047/45.047 (h 1) 45.047/45.047 ) 45.047/45.047 (RULES 45.047/45.047 p(q(x:S)) -> p(r(x:S)) 45.047/45.047 q(h(x:S)) -> r(x:S) 45.047/45.047 r(x:S) -> r(h(x:S)) | s(x:S) ->* 0 45.047/45.047 s(x:S) -> 1 45.047/45.047 ) 45.047/45.047 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.047/45.047 45.047/45.047 45.047/45.047 Problem 1: 45.047/45.047 45.047/45.047 Inlining of Conditions Processor [STERN17]: 45.047/45.047 45.047/45.047 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.047/45.047 Confluence Problem: 45.047/45.047 (VAR vNonEmpty:S x:S) 45.047/45.047 (STRATEGY CONTEXTSENSITIVE 45.047/45.047 (p 1) 45.047/45.047 (q 1) 45.047/45.047 (r 1) 45.047/45.047 (s 1) 45.047/45.047 (0) 45.047/45.047 (1) 45.047/45.047 (fSNonEmpty) 45.047/45.047 (h 1) 45.047/45.047 ) 45.047/45.047 (RULES 45.047/45.047 p(q(x:S)) -> p(r(x:S)) 45.047/45.047 q(h(x:S)) -> r(x:S) 45.047/45.047 r(x:S) -> r(h(x:S)) | s(x:S) ->* 0 45.047/45.047 s(x:S) -> 1 45.047/45.047 ) 45.047/45.047 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.047/45.047 45.047/45.047 45.047/45.047 Problem 1: 45.047/45.047 45.047/45.047 Clean CTRS Processor: 45.047/45.047 45.047/45.047 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.047/45.047 Confluence Problem: 45.047/45.047 (VAR x:S) 45.047/45.047 (STRATEGY CONTEXTSENSITIVE 45.047/45.047 (p 1) 45.047/45.047 (q 1) 45.047/45.047 (r 1) 45.047/45.047 (s 1) 45.047/45.047 (0) 45.047/45.047 (1) 45.047/45.047 (fSNonEmpty) 45.047/45.047 (h 1) 45.047/45.047 ) 45.047/45.047 (RULES 45.047/45.047 p(q(x:S)) -> p(r(x:S)) 45.047/45.047 q(h(x:S)) -> r(x:S) 45.047/45.047 s(x:S) -> 1 45.047/45.047 ) 45.047/45.047 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.047/45.047 45.047/45.047 CRule InfChecker Info: 45.047/45.047 p(q(x:S)) -> p(r(x:S)) 45.047/45.047 Rule remains 45.047/45.047 Proof: 45.047/45.047 NO_CONDS 45.047/45.047 45.047/45.047 CRule InfChecker Info: 45.047/45.047 q(h(x:S)) -> r(x:S) 45.047/45.047 Rule remains 45.047/45.047 Proof: 45.047/45.047 NO_CONDS 45.047/45.047 45.047/45.047 CRule InfChecker Info: 45.047/45.047 r(x:S) -> r(h(x:S)) | s(x:S) ->* 0 45.047/45.047 Rule deleted 45.047/45.047 Proof: 45.047/45.047 YES 45.047/45.047 45.047/45.047 Problem 1: 45.047/45.047 45.047/45.047 Infeasibility Problem: 45.047/45.047 [(VAR vNonEmpty:S vNonEmpty:S:S x:S:S) 45.047/45.047 (STRATEGY CONTEXTSENSITIVE 45.047/45.047 (p 1) 45.047/45.047 (q 1) 45.047/45.047 (r 1) 45.047/45.047 (s 1) 45.047/45.047 (0) 45.047/45.047 (1) 45.047/45.047 (fSNonEmpty) 45.047/45.047 (h 1) 45.047/45.047 ) 45.047/45.047 (RULES 45.047/45.047 p(q(x:S:S)) -> p(r(x:S:S)) 45.047/45.047 q(h(x:S:S)) -> r(x:S:S) 45.047/45.047 r(x:S:S) -> r(h(x:S:S)) | s(x:S:S) ->* 0 45.047/45.047 s(x:S:S) -> 1 45.047/45.047 )] 45.047/45.047 45.047/45.047 Infeasibility Conditions: 45.047/45.047 s(x:S:S) ->* 0 45.047/45.047 45.047/45.047 Problem 1: 45.047/45.047 45.047/45.047 Obtaining a model using Mace4: 45.047/45.047 45.047/45.047 -> Usable Rules: 45.047/45.047 p(q(x:S:S)) -> p(r(x:S:S)) 45.047/45.047 q(h(x:S:S)) -> r(x:S:S) 45.047/45.047 r(x:S:S) -> r(h(x:S:S)) | s(x:S:S) ->* 0 45.047/45.047 s(x:S:S) -> 1 45.047/45.047 45.047/45.047 -> Mace4 Output: 45.047/45.047 ============================== Mace4 ================================= 45.047/45.047 Mace4 (64) version 2009-11A, November 2009. 45.047/45.047 Process 34504 was started by ubuntu on ubuntu, 45.047/45.047 Wed Jul 14 09:53:04 2021 45.047/45.047 The command was "./mace4 -c -f /tmp/mace434491-2.in". 45.047/45.047 ============================== end of head =========================== 45.047/45.047 45.047/45.047 ============================== INPUT ================================= 45.047/45.047 45.047/45.047 % Reading from file /tmp/mace434491-2.in 45.047/45.047 45.047/45.047 assign(max_seconds,20). 45.047/45.047 45.047/45.047 formulas(assumptions). 45.047/45.047 ->(x1,y) -> ->(p(x1),p(y)) # label(congruence). 45.047/45.047 ->(x1,y) -> ->(q(x1),q(y)) # label(congruence). 45.047/45.047 ->(x1,y) -> ->(r(x1),r(y)) # label(congruence). 45.047/45.047 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence). 45.047/45.047 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence). 45.047/45.047 ->(p(q(x2)),p(r(x2))) # label(replacement). 45.047/45.047 ->(q(h(x2)),r(x2)) # label(replacement). 45.047/45.047 ->*(s(x2),0) -> ->(r(x2),r(h(x2))) # label(replacement). 45.047/45.047 ->(s(x2),1) # label(replacement). 45.047/45.047 ->*(x,x) # label(reflexivity). 45.047/45.047 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 45.047/45.047 end_of_list. 45.047/45.047 45.047/45.047 formulas(goals). 45.047/45.047 (exists x2 ->*(s(x2),0)) # label(goal). 45.047/45.047 end_of_list. 45.047/45.047 45.047/45.047 ============================== end of input ========================== 45.047/45.047 45.047/45.047 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 45.047/45.047 45.047/45.047 % Formulas that are not ordinary clauses: 45.047/45.047 1 ->(x1,y) -> ->(p(x1),p(y)) # label(congruence) # label(non_clause). [assumption]. 45.047/45.047 2 ->(x1,y) -> ->(q(x1),q(y)) # label(congruence) # label(non_clause). [assumption]. 45.047/45.047 3 ->(x1,y) -> ->(r(x1),r(y)) # label(congruence) # label(non_clause). [assumption]. 45.047/45.047 4 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 45.047/45.047 5 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 45.047/45.047 6 ->*(s(x2),0) -> ->(r(x2),r(h(x2))) # label(replacement) # label(non_clause). [assumption]. 45.047/45.047 7 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 45.047/45.047 8 (exists x2 ->*(s(x2),0)) # label(goal) # label(non_clause) # label(goal). [goal]. 45.047/45.047 45.047/45.047 ============================== end of process non-clausal formulas === 45.047/45.047 45.047/45.047 ============================== CLAUSES FOR SEARCH ==================== 45.047/45.047 45.047/45.047 formulas(mace4_clauses). 45.047/45.047 -->(x,y) | ->(p(x),p(y)) # label(congruence). 45.047/45.047 -->(x,y) | ->(q(x),q(y)) # label(congruence). 45.047/45.047 -->(x,y) | ->(r(x),r(y)) # label(congruence). 45.047/45.047 -->(x,y) | ->(s(x),s(y)) # label(congruence). 45.047/45.047 -->(x,y) | ->(h(x),h(y)) # label(congruence). 45.047/45.047 ->(p(q(x)),p(r(x))) # label(replacement). 45.047/45.047 ->(q(h(x)),r(x)) # label(replacement). 45.047/45.047 -->*(s(x),0) | ->(r(x),r(h(x))) # label(replacement). 45.047/45.047 ->(s(x),1) # label(replacement). 45.047/45.047 ->*(x,x) # label(reflexivity). 45.047/45.047 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 45.047/45.047 -->*(s(x),0) # label(goal). 45.047/45.047 end_of_list. 45.047/45.047 45.047/45.047 ============================== end of clauses for search ============= 45.047/45.047 45.047/45.047 % There are no natural numbers in the input. 45.047/45.047 45.047/45.047 ============================== DOMAIN SIZE 2 ========================= 45.047/45.047 45.047/45.047 ============================== MODEL ================================= 45.047/45.047 45.047/45.047 interpretation( 2, [number=1, seconds=0], [ 45.047/45.047 45.047/45.047 function(0, [ 0 ]), 45.047/45.047 45.047/45.047 function(1, [ 1 ]), 45.047/45.047 45.047/45.047 function(p(_), [ 0, 0 ]), 45.047/45.047 45.047/45.047 function(q(_), [ 0, 0 ]), 45.047/45.047 45.047/45.047 function(r(_), [ 0, 0 ]), 45.047/45.047 45.047/45.047 function(s(_), [ 1, 1 ]), 45.047/45.047 45.047/45.047 function(h(_), [ 0, 0 ]), 45.047/45.047 45.047/45.047 relation(->*(_,_), [ 45.047/45.047 1, 0, 45.047/45.047 0, 1 ]), 45.047/45.047 45.047/45.047 relation(->(_,_), [ 45.047/45.047 1, 0, 45.047/45.047 0, 1 ]) 45.047/45.047 ]). 45.047/45.047 45.047/45.047 ============================== end of model ========================== 45.047/45.047 45.047/45.047 ============================== STATISTICS ============================ 45.047/45.047 45.047/45.047 For domain size 2. 45.047/45.047 45.047/45.047 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 45.047/45.047 Ground clauses: seen=40, kept=36. 45.047/45.047 Selections=10, assignments=10, propagations=10, current_models=1. 45.047/45.047 Rewrite_terms=72, rewrite_bools=47, indexes=6. 45.047/45.047 Rules_from_neg_clauses=3, cross_offs=3. 45.047/45.047 45.047/45.047 ============================== end of statistics ===================== 45.047/45.047 45.047/45.047 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 45.047/45.047 45.047/45.047 Exiting with 1 model. 45.047/45.047 45.047/45.047 Process 34504 exit (max_models) Wed Jul 14 09:53:04 2021 45.047/45.047 The process finished Wed Jul 14 09:53:04 2021 45.047/45.047 45.047/45.047 45.047/45.047 Mace4 cooked interpretation: 45.047/45.047 45.047/45.047 45.047/45.047 45.047/45.047 The problem is infeasible. 45.047/45.047 45.047/45.047 45.047/45.047 CRule InfChecker Info: 45.047/45.047 s(x:S) -> 1 45.047/45.047 Rule remains 45.047/45.047 Proof: 45.047/45.047 NO_CONDS 45.047/45.047 45.047/45.047 Problem 1: 45.047/45.047 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.047/45.047 Confluence Problem: 45.047/45.047 (VAR x:S) 45.047/45.047 (STRATEGY CONTEXTSENSITIVE 45.047/45.047 (p 1) 45.047/45.047 (q 1) 45.047/45.047 (r 1) 45.047/45.047 (s 1) 45.047/45.047 (0) 45.047/45.047 (1) 45.047/45.047 (fSNonEmpty) 45.047/45.047 (h 1) 45.047/45.047 ) 45.047/45.047 (RULES 45.047/45.047 p(q(x:S)) -> p(r(x:S)) 45.047/45.047 q(h(x:S)) -> r(x:S) 45.047/45.047 s(x:S) -> 1 45.047/45.047 ) 45.047/45.047 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.047/45.047 45.047/45.047 Critical Pairs Processor: 45.047/45.047 -> Rules: 45.047/45.047 p(q(x:S)) -> p(r(x:S)) 45.047/45.047 q(h(x:S)) -> r(x:S) 45.047/45.047 s(x:S) -> 1 45.047/45.047 -> Vars: 45.047/45.047 "x", "x", "x" 45.047/45.047 -> FVars: 45.047/45.047 "x2", "x3", "x4" 45.047/45.047 -> PVars: 45.047/45.047 "x": ["x2", "x3", "x4"] 45.047/45.047 45.047/45.047 -> Rlps: 45.047/45.047 crule: p(q(x2:S)) -> p(r(x2:S)), id: 1, possubterms: p(q(x2:S))-> [], q(x2:S)-> [1] 45.047/45.047 crule: q(h(x3:S)) -> r(x3:S), id: 2, possubterms: q(h(x3:S))-> [], h(x3:S)-> [1] 45.047/45.047 crule: s(x4:S) -> 1, id: 3, possubterms: s(x4:S)-> [] 45.047/45.047 45.047/45.047 -> Unifications: 45.047/45.047 R1 unifies with R2 at p: [1], l: p(q(x2:S)), lp: q(x2:S), conds: {}, sig: {x2:S -> h(x:S)}, l': q(h(x:S)), r: p(r(x2:S)), r': r(x:S) 45.047/45.047 45.047/45.047 -> Critical pairs info: 45.047/45.047 => Not trivial, Not overlay, N1 45.047/45.047 45.047/45.047 -> Problem conclusions: 45.047/45.047 Left linear, Right linear, Linear 45.047/45.047 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 45.047/45.047 CTRS Type: 1 45.047/45.047 Deterministic, Strongly deterministic 45.047/45.047 Oriented CTRS, Properly oriented CTRS, Join CTRS 45.047/45.047 Maybe right-stable CTRS, Not overlay CTRS 45.047/45.047 Normal CTRS, Almost normal CTRS 45.047/45.047 Maybe terminating CTRS, Maybe joinable CCPs 45.047/45.047 Maybe level confluent 45.047/45.047 Maybe confluent 45.047/45.047 45.047/45.047 Problem 1: 45.047/45.047 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.047/45.047 Confluence Problem: 45.047/45.047 (VAR x:S) 45.047/45.047 (STRATEGY CONTEXTSENSITIVE 45.047/45.047 (p 1) 45.047/45.047 (q 1) 45.047/45.047 (r 1) 45.047/45.047 (s 1) 45.047/45.047 (0) 45.047/45.047 (1) 45.047/45.047 (fSNonEmpty) 45.047/45.047 (h 1) 45.047/45.047 ) 45.047/45.047 (RULES 45.047/45.047 p(q(x:S)) -> p(r(x:S)) 45.047/45.047 q(h(x:S)) -> r(x:S) 45.047/45.047 s(x:S) -> 1 45.047/45.047 ) 45.047/45.047 Critical Pairs: 45.047/45.047 => Not trivial, Not overlay, N1 45.047/45.047 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.047/45.047 45.047/45.047 Conditional Critical Pairs Distributor Processor 45.047/45.047 45.047/45.047 Problem 1: 45.047/45.047 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.047/45.047 Confluence Problem: 45.047/45.047 (VAR x:S) 45.047/45.047 (STRATEGY CONTEXTSENSITIVE 45.047/45.047 (p 1) 45.047/45.047 (q 1) 45.047/45.047 (r 1) 45.047/45.047 (s 1) 45.047/45.047 (0) 45.047/45.047 (1) 45.047/45.047 (fSNonEmpty) 45.047/45.047 (h 1) 45.047/45.047 ) 45.047/45.047 (RULES 45.047/45.047 p(q(x:S)) -> p(r(x:S)) 45.047/45.047 q(h(x:S)) -> r(x:S) 45.047/45.047 s(x:S) -> 1 45.047/45.047 ) 45.047/45.047 Critical Pairs: 45.047/45.047 => Not trivial, Not overlay, N1 45.047/45.047 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.047/45.047 45.047/45.047 Infeasible Convergence No Conditions CCP Processor: 45.047/45.047 Infeasible convergence? 45.047/45.047 YES 45.047/45.047 45.047/45.047 Problem 1: 45.047/45.047 45.047/45.047 Infeasibility Problem: 45.047/45.047 [(VAR vNonEmpty:S x:S z:S) 45.047/45.047 (STRATEGY CONTEXTSENSITIVE 45.047/45.047 (p 1) 45.047/45.047 (q 1) 45.047/45.047 (s 1) 45.047/45.047 (1) 45.047/45.047 (cx) 45.047/45.047 (fSNonEmpty) 45.047/45.047 (h 1) 45.047/45.047 (r 1) 45.047/45.047 ) 45.047/45.047 (RULES 45.047/45.047 p(q(x:S)) -> p(r(x:S)) 45.047/45.047 q(h(x:S)) -> r(x:S) 45.047/45.047 s(x:S) -> 1 45.047/45.047 )] 45.047/45.047 Infeasibility Conditions: 45.047/45.047 p(r(cx)) ->* z:S, p(r(h(cx))) ->* z:S 45.047/45.047 45.047/45.047 Problem 1: 45.047/45.047 45.047/45.047 Obtaining a model using Mace4: 45.047/45.047 45.047/45.047 -> Usable Rules: 45.047/45.047 p(q(x:S)) -> p(r(x:S)) 45.047/45.047 45.047/45.047 -> Mace4 Output: 45.047/45.047 ============================== Mace4 ================================= 45.047/45.047 Mace4 (64) version 2009-11A, November 2009. 45.047/45.047 Process 34533 was started by ubuntu on ubuntu, 45.047/45.047 Wed Jul 14 09:53:24 2021 45.047/45.047 The command was "./mace4 -c -f /tmp/mace434520-2.in". 45.047/45.047 ============================== end of head =========================== 45.047/45.047 45.047/45.047 ============================== INPUT ================================= 45.047/45.047 45.047/45.047 % Reading from file /tmp/mace434520-2.in 45.047/45.047 45.047/45.047 assign(max_seconds,20). 45.047/45.047 45.047/45.047 formulas(assumptions). 45.047/45.047 ->(x1,y) -> ->(p(x1),p(y)) # label(congruence). 45.047/45.047 ->(x1,y) -> ->(q(x1),q(y)) # label(congruence). 45.047/45.047 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence). 45.047/45.047 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence). 45.047/45.047 ->(x1,y) -> ->(r(x1),r(y)) # label(congruence). 45.047/45.047 ->(p(q(x1)),p(r(x1))) # label(replacement). 45.047/45.047 ->*(x,x) # label(reflexivity). 45.047/45.047 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 45.047/45.047 end_of_list. 45.047/45.047 45.047/45.047 formulas(goals). 45.047/45.047 (exists x2 (->*(p(r(cx)),x2) & ->*(p(r(h(cx))),x2))) # label(goal). 45.047/45.047 end_of_list. 45.047/45.047 45.047/45.047 ============================== end of input ========================== 45.047/45.047 45.047/45.047 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 45.047/45.047 45.047/45.047 % Formulas that are not ordinary clauses: 45.047/45.047 1 ->(x1,y) -> ->(p(x1),p(y)) # label(congruence) # label(non_clause). [assumption]. 45.047/45.047 2 ->(x1,y) -> ->(q(x1),q(y)) # label(congruence) # label(non_clause). [assumption]. 45.047/45.047 3 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 45.047/45.047 4 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 45.047/45.047 5 ->(x1,y) -> ->(r(x1),r(y)) # label(congruence) # label(non_clause). [assumption]. 45.047/45.047 6 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 45.047/45.047 7 (exists x2 (->*(p(r(cx)),x2) & ->*(p(r(h(cx))),x2))) # label(goal) # label(non_clause) # label(goal). [goal]. 45.047/45.047 45.047/45.047 ============================== end of process non-clausal formulas === 45.047/45.047 45.047/45.047 ============================== CLAUSES FOR SEARCH ==================== 45.047/45.047 45.047/45.047 formulas(mace4_clauses). 45.047/45.047 -->(x,y) | ->(p(x),p(y)) # label(congruence). 45.047/45.047 -->(x,y) | ->(q(x),q(y)) # label(congruence). 45.047/45.047 -->(x,y) | ->(s(x),s(y)) # label(congruence). 45.047/45.047 -->(x,y) | ->(h(x),h(y)) # label(congruence). 45.047/45.047 -->(x,y) | ->(r(x),r(y)) # label(congruence). 45.047/45.047 ->(p(q(x)),p(r(x))) # label(replacement). 45.047/45.047 ->*(x,x) # label(reflexivity). 45.047/45.047 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 45.047/45.047 -->*(p(r(cx)),x) | -->*(p(r(h(cx))),x) # label(goal). 45.047/45.047 end_of_list. 45.047/45.047 45.047/45.047 ============================== end of clauses for search ============= 45.047/45.047 45.047/45.047 % There are no natural numbers in the input. 45.047/45.047 45.047/45.047 ============================== DOMAIN SIZE 2 ========================= 45.047/45.047 45.047/45.047 ============================== MODEL ================================= 45.047/45.047 45.047/45.047 interpretation( 2, [number=1, seconds=0], [ 45.047/45.047 45.047/45.047 function(cx, [ 0 ]), 45.047/45.047 45.047/45.047 function(p(_), [ 0, 1 ]), 45.047/45.047 45.047/45.047 function(q(_), [ 0, 1 ]), 45.047/45.047 45.047/45.047 function(s(_), [ 0, 0 ]), 45.047/45.047 45.047/45.047 function(h(_), [ 1, 0 ]), 45.047/45.047 45.047/45.047 function(r(_), [ 0, 1 ]), 45.047/45.047 45.047/45.047 relation(->*(_,_), [ 45.047/45.047 1, 0, 45.047/45.047 0, 1 ]), 45.047/45.047 45.047/45.047 relation(->(_,_), [ 45.047/45.047 1, 0, 45.047/45.047 0, 1 ]) 45.047/45.047 ]). 45.047/45.047 45.047/45.047 ============================== end of model ========================== 45.047/45.047 45.047/45.047 ============================== STATISTICS ============================ 45.047/45.047 45.047/45.047 For domain size 2. 45.047/45.047 45.047/45.047 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 45.047/45.047 Ground clauses: seen=34, kept=30. 45.047/45.047 Selections=36, assignments=65, propagations=24, current_models=1. 45.047/45.047 Rewrite_terms=315, rewrite_bools=177, indexes=91. 45.047/45.047 Rules_from_neg_clauses=1, cross_offs=1. 45.047/45.047 45.047/45.047 ============================== end of statistics ===================== 45.047/45.047 45.047/45.047 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 45.047/45.047 45.047/45.047 Exiting with 1 model. 45.047/45.047 45.047/45.047 Process 34533 exit (max_models) Wed Jul 14 09:53:24 2021 45.047/45.047 The process finished Wed Jul 14 09:53:24 2021 45.047/45.047 45.047/45.047 45.047/45.047 Mace4 cooked interpretation: 45.047/45.047 45.047/45.047 45.047/45.047 45.047/45.047 The problem is infeasible. 45.047/45.047 45.047/45.047 45.047/45.047 The problem is not joinable. 45.047/45.047 62.29user 1.38system 0:45.47elapsed 140%CPU (0avgtext+0avgdata 135944maxresident)k 45.047/45.047 0inputs+0outputs (0major+143383minor)pagefaults 0swaps