5.006/5.006 YES 5.006/5.006 5.006/5.006 Problem 1: 5.006/5.006 5.006/5.006 5.006/5.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.006/5.006 Confluence Problem: 5.006/5.006 (VAR vNonEmpty x) 5.006/5.006 (REPLACEMENT-MAP 5.006/5.006 (a) 5.006/5.006 (b) 5.006/5.006 (c) 5.006/5.006 (d) 5.006/5.006 (e) 5.006/5.006 (fSNonEmpty) 5.006/5.006 ) 5.006/5.006 (RULES 5.006/5.006 a -> a | b ->* x, c ->* x 5.006/5.006 b -> d | d ->* x, e ->* x 5.006/5.006 c -> d | d ->* x, e ->* x 5.006/5.006 ) 5.006/5.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.006/5.006 5.006/5.006 5.006/5.006 Problem 1: 5.006/5.006 5.006/5.006 Inlining of Conditions Processor [STERN17]: 5.006/5.006 5.006/5.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.006/5.006 Confluence Problem: 5.006/5.006 (VAR vNonEmpty x) 5.006/5.006 (REPLACEMENT-MAP 5.006/5.006 (a) 5.006/5.006 (b) 5.006/5.006 (c) 5.006/5.006 (d) 5.006/5.006 (e) 5.006/5.006 (fSNonEmpty) 5.006/5.006 ) 5.006/5.006 (RULES 5.006/5.006 a -> a | b ->* x, c ->* x 5.006/5.006 b -> d | d ->* x, e ->* x 5.006/5.006 c -> d | d ->* x, e ->* x 5.006/5.006 ) 5.006/5.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.006/5.006 5.006/5.006 5.006/5.006 Problem 1: 5.006/5.006 5.006/5.006 Clean CTRS Processor: 5.006/5.006 5.006/5.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.006/5.006 Confluence Problem: 5.006/5.006 (REPLACEMENT-MAP 5.006/5.006 (a) 5.006/5.006 (b) 5.006/5.006 (c) 5.006/5.006 (d) 5.006/5.006 (e) 5.006/5.006 (fSNonEmpty) 5.006/5.006 ) 5.006/5.006 (RULES 5.006/5.006 ) 5.006/5.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.006/5.006 5.006/5.006 CRule InfChecker Info: 5.006/5.006 a -> a | b ->* x, c ->* x 5.006/5.006 Rule deleted 5.006/5.006 Proof: 5.006/5.006 SAME_LHS_AND_RHS 5.006/5.006 5.006/5.006 CRule InfChecker Info: 5.006/5.006 b -> d | d ->* x, e ->* x 5.006/5.006 Rule deleted 5.006/5.006 Proof: 5.006/5.006 YES 5.006/5.006 5.006/5.006 Problem 1: 5.006/5.006 5.006/5.006 Infeasibility Problem: 5.006/5.006 [(VAR vNonEmpty x vNonEmpty x) 5.006/5.006 (STRATEGY CONTEXTSENSITIVE 5.006/5.006 (b) 5.006/5.006 (c) 5.006/5.006 (d) 5.006/5.006 (e) 5.006/5.006 (fSNonEmpty) 5.006/5.006 ) 5.006/5.006 (RULES 5.006/5.006 b -> d | d ->* x, e ->* x 5.006/5.006 c -> d | d ->* x, e ->* x 5.006/5.006 )] 5.006/5.006 5.006/5.006 Infeasibility Conditions: 5.006/5.006 d ->* x, e ->* x 5.006/5.006 5.006/5.006 Problem 1: 5.006/5.006 5.006/5.006 Obtaining a model using Mace4: 5.006/5.006 5.006/5.006 -> Usable Rules: 5.006/5.006 Empty 5.006/5.006 5.006/5.006 -> Mace4 Output: 5.006/5.006 ============================== Mace4 ================================= 5.006/5.006 Mace4 (64) version 2009-11A, November 2009. 5.006/5.006 Process 80991 was started by ubuntu on ubuntu, 5.006/5.006 Wed Mar 9 10:27:22 2022 5.006/5.006 The command was "./mace4 -c -f /tmp/mace480978-2.in". 5.006/5.006 ============================== end of head =========================== 5.006/5.006 5.006/5.006 ============================== INPUT ================================= 5.006/5.006 5.006/5.006 % Reading from file /tmp/mace480978-2.in 5.006/5.006 5.006/5.006 assign(max_seconds,20). 5.006/5.006 5.006/5.006 formulas(assumptions). 5.006/5.006 ->*(x,x) # label(reflexivity). 5.006/5.006 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 5.006/5.006 end_of_list. 5.006/5.006 5.006/5.006 formulas(goals). 5.006/5.006 (exists x3 (->*(d,x3) & ->*(e,x3))) # label(goal). 5.006/5.006 end_of_list. 5.006/5.006 5.006/5.006 ============================== end of input ========================== 5.006/5.006 5.006/5.006 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 5.006/5.006 5.006/5.006 % Formulas that are not ordinary clauses: 5.006/5.006 1 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 5.006/5.006 2 (exists x3 (->*(d,x3) & ->*(e,x3))) # label(goal) # label(non_clause) # label(goal). [goal]. 5.006/5.006 5.006/5.006 ============================== end of process non-clausal formulas === 5.006/5.006 5.006/5.006 ============================== CLAUSES FOR SEARCH ==================== 5.006/5.006 5.006/5.006 formulas(mace4_clauses). 5.006/5.006 ->*(x,x) # label(reflexivity). 5.006/5.006 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 5.006/5.006 -->*(d,x) | -->*(e,x) # label(goal). 5.006/5.006 end_of_list. 5.006/5.006 5.006/5.006 ============================== end of clauses for search ============= 5.006/5.006 5.006/5.006 % There are no natural numbers in the input. 5.006/5.006 5.006/5.006 ============================== DOMAIN SIZE 2 ========================= 5.006/5.006 5.006/5.006 ============================== MODEL ================================= 5.006/5.006 5.006/5.006 interpretation( 2, [number=1, seconds=0], [ 5.006/5.006 5.006/5.006 function(d, [ 0 ]), 5.006/5.006 5.006/5.006 function(e, [ 1 ]), 5.006/5.006 5.006/5.006 relation(->*(_,_), [ 5.006/5.006 1, 0, 5.006/5.006 0, 1 ]), 5.006/5.006 5.006/5.006 relation(->(_,_), [ 5.006/5.006 0, 0, 5.006/5.006 0, 0 ]) 5.006/5.006 ]). 5.006/5.006 5.006/5.006 ============================== end of model ========================== 5.006/5.006 5.006/5.006 ============================== STATISTICS ============================ 5.006/5.006 5.006/5.006 For domain size 2. 5.006/5.006 5.006/5.006 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 5.006/5.006 Ground clauses: seen=12, kept=8. 5.006/5.006 Selections=3, assignments=3, propagations=7, current_models=1. 5.006/5.006 Rewrite_terms=4, rewrite_bools=14, indexes=2. 5.006/5.006 Rules_from_neg_clauses=1, cross_offs=1. 5.006/5.006 5.006/5.006 ============================== end of statistics ===================== 5.006/5.006 5.006/5.006 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 5.006/5.006 5.006/5.006 Exiting with 1 model. 5.006/5.006 5.006/5.006 Process 80991 exit (max_models) Wed Mar 9 10:27:22 2022 5.006/5.006 The process finished Wed Mar 9 10:27:22 2022 5.006/5.006 5.006/5.006 5.006/5.006 Mace4 cooked interpretation: 5.006/5.006 5.006/5.006 5.006/5.006 5.006/5.006 The problem is infeasible. 5.006/5.006 5.006/5.006 5.006/5.006 CRule InfChecker Info: 5.006/5.006 c -> d | d ->* x, e ->* x 5.006/5.006 Rule deleted 5.006/5.006 Proof: 5.006/5.006 YES 5.006/5.006 5.006/5.006 Problem 1: 5.006/5.006 5.006/5.006 Infeasibility Problem: 5.006/5.006 [(VAR vNonEmpty x vNonEmpty x) 5.006/5.006 (STRATEGY CONTEXTSENSITIVE 5.006/5.006 (c) 5.006/5.006 (d) 5.006/5.006 (e) 5.006/5.006 (fSNonEmpty) 5.006/5.006 ) 5.006/5.006 (RULES 5.006/5.006 c -> d | d ->* x, e ->* x 5.006/5.006 )] 5.006/5.006 5.006/5.006 Infeasibility Conditions: 5.006/5.006 d ->* x, e ->* x 5.006/5.006 5.006/5.006 Problem 1: 5.006/5.006 5.006/5.006 Obtaining a model using Mace4: 5.006/5.006 5.006/5.006 -> Usable Rules: 5.006/5.006 Empty 5.006/5.006 5.006/5.006 -> Mace4 Output: 5.006/5.006 ============================== Mace4 ================================= 5.006/5.006 Mace4 (64) version 2009-11A, November 2009. 5.006/5.006 Process 81017 was started by ubuntu on ubuntu, 5.006/5.006 Wed Mar 9 10:27:22 2022 5.006/5.006 The command was "./mace4 -c -f /tmp/mace481002-2.in". 5.006/5.006 ============================== end of head =========================== 5.006/5.006 5.006/5.006 ============================== INPUT ================================= 5.006/5.006 5.006/5.006 % Reading from file /tmp/mace481002-2.in 5.006/5.006 5.006/5.006 assign(max_seconds,20). 5.006/5.006 5.006/5.006 formulas(assumptions). 5.006/5.006 ->*(x,x) # label(reflexivity). 5.006/5.006 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 5.006/5.006 end_of_list. 5.006/5.006 5.006/5.006 formulas(goals). 5.006/5.006 (exists x3 (->*(d,x3) & ->*(e,x3))) # label(goal). 5.006/5.006 end_of_list. 5.006/5.006 5.006/5.006 ============================== end of input ========================== 5.006/5.006 5.006/5.006 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 5.006/5.006 5.006/5.006 % Formulas that are not ordinary clauses: 5.006/5.006 1 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 5.006/5.006 2 (exists x3 (->*(d,x3) & ->*(e,x3))) # label(goal) # label(non_clause) # label(goal). [goal]. 5.006/5.006 5.006/5.006 ============================== end of process non-clausal formulas === 5.006/5.006 5.006/5.006 ============================== CLAUSES FOR SEARCH ==================== 5.006/5.006 5.006/5.006 formulas(mace4_clauses). 5.006/5.006 ->*(x,x) # label(reflexivity). 5.006/5.006 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 5.006/5.006 -->*(d,x) | -->*(e,x) # label(goal). 5.006/5.006 end_of_list. 5.006/5.006 5.006/5.006 ============================== end of clauses for search ============= 5.006/5.006 5.006/5.006 % There are no natural numbers in the input. 5.006/5.006 5.006/5.006 ============================== DOMAIN SIZE 2 ========================= 5.006/5.006 5.006/5.006 ============================== MODEL ================================= 5.006/5.006 5.006/5.006 interpretation( 2, [number=1, seconds=0], [ 5.006/5.006 5.006/5.006 function(d, [ 0 ]), 5.006/5.006 5.006/5.006 function(e, [ 1 ]), 5.006/5.006 5.006/5.006 relation(->*(_,_), [ 5.006/5.006 1, 0, 5.006/5.006 0, 1 ]), 5.006/5.006 5.006/5.006 relation(->(_,_), [ 5.006/5.006 0, 0, 5.006/5.006 0, 0 ]) 5.006/5.006 ]). 5.006/5.006 5.006/5.006 ============================== end of model ========================== 5.006/5.006 5.006/5.006 ============================== STATISTICS ============================ 5.006/5.006 5.006/5.006 For domain size 2. 5.006/5.006 5.006/5.006 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 5.006/5.006 Ground clauses: seen=12, kept=8. 5.006/5.006 Selections=3, assignments=3, propagations=7, current_models=1. 5.006/5.006 Rewrite_terms=4, rewrite_bools=14, indexes=2. 5.006/5.006 Rules_from_neg_clauses=1, cross_offs=1. 5.006/5.006 5.006/5.006 ============================== end of statistics ===================== 5.006/5.006 5.006/5.006 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 5.006/5.006 5.006/5.006 Exiting with 1 model. 5.006/5.006 5.006/5.006 Process 81017 exit (max_models) Wed Mar 9 10:27:22 2022 5.006/5.006 The process finished Wed Mar 9 10:27:22 2022 5.006/5.006 5.006/5.006 5.006/5.006 Mace4 cooked interpretation: 5.006/5.006 5.006/5.006 5.006/5.006 5.006/5.006 The problem is infeasible. 5.006/5.006 5.006/5.006 5.006/5.006 Problem 1: 5.006/5.006 5.006/5.006 Transform No Conds CTRS Processor: 5.006/5.006 5.006/5.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.006/5.006 Confluence Problem: 5.006/5.006 (REPLACEMENT-MAP 5.006/5.006 (a) 5.006/5.006 (b) 5.006/5.006 (c) 5.006/5.006 (d) 5.006/5.006 (e) 5.006/5.006 (fSNonEmpty) 5.006/5.006 ) 5.006/5.006 (RULES 5.006/5.006 ) 5.006/5.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.006/5.006 Resulting R: 5.006/5.006 (STRATEGY CONTEXTSENSITIVE 5.006/5.006 (a) 5.006/5.006 (b) 5.006/5.006 (c) 5.006/5.006 (d) 5.006/5.006 (e) 5.006/5.006 (fSNonEmpty) 5.006/5.006 ) 5.006/5.006 (RULES 5.006/5.006 ) 5.006/5.006 5.006/5.006 Problem 1: 5.006/5.006 5.006/5.006 CleanTRS Processor: 5.006/5.006 5.006/5.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.006/5.006 Confluence Problem: 5.006/5.006 (REPLACEMENT-MAP 5.006/5.006 (a) 5.006/5.006 (b) 5.006/5.006 (c) 5.006/5.006 (d) 5.006/5.006 (e) 5.006/5.006 (fSNonEmpty) 5.006/5.006 ) 5.006/5.006 (RULES 5.006/5.006 ) 5.006/5.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.006/5.006 5.006/5.006 5.006/5.006 Problem 1: 5.006/5.006 5.006/5.006 Modular Confluence Combinations Decomposition Processor: 5.006/5.006 5.006/5.006 No usable combinations 5.006/5.006 5.006/5.006 Problem 1: 5.006/5.006 Linearity Processor: 5.006/5.006 Linear? 5.006/5.006 YES 5.006/5.006 Problem 1.1: 5.006/5.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.006/5.006 Confluence Problem: 5.006/5.006 (REPLACEMENT-MAP 5.006/5.006 (a) 5.006/5.006 (b) 5.006/5.006 (c) 5.006/5.006 (d) 5.006/5.006 (e) 5.006/5.006 (fSNonEmpty) 5.006/5.006 ) 5.006/5.006 (RULES 5.006/5.006 ) 5.006/5.006 Linear:YES 5.006/5.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.006/5.006 5.006/5.006 Huet Levy Processor: 5.006/5.006 -> Rules: 5.006/5.006 5.006/5.006 -> Vars: 5.006/5.006 5.006/5.006 5.006/5.006 -> Rlps: 5.006/5.006 5.006/5.006 5.006/5.006 -> Unifications: 5.006/5.006 5.006/5.006 5.006/5.006 -> Critical pairs info: 5.006/5.006 5.006/5.006 5.006/5.006 -> Problem conclusions: 5.006/5.006 Left linear, Right linear, Linear 5.006/5.006 Weakly orthogonal, Almost orthogonal, Orthogonal 5.006/5.006 Huet-Levy confluent, Not Newman confluent 5.006/5.006 R is a TRS 5.006/5.006 5.006/5.006 5.006/5.006 The problem is joinable. 5.006/5.006 0.07user 0.02system 0:05.06elapsed 2%CPU (0avgtext+0avgdata 13008maxresident)k 5.006/5.006 8inputs+0outputs (0major+9768minor)pagefaults 0swaps