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