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