25.006/25.006 YES 25.006/25.006 25.006/25.006 Problem 1: 25.006/25.006 25.006/25.006 25.006/25.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.006/25.006 Confluence Problem: 25.006/25.006 (VAR vNonEmpty:S x:S) 25.006/25.006 (STRATEGY CONTEXTSENSITIVE 25.006/25.006 (f 1) 25.006/25.006 (g 1 2) 25.006/25.006 (a) 25.006/25.006 (b) 25.006/25.006 (c) 25.006/25.006 (fSNonEmpty) 25.006/25.006 ) 25.006/25.006 (RULES 25.006/25.006 f(x:S) -> c | a ->* b 25.006/25.006 g(x:S,x:S) -> g(f(a),f(b)) 25.006/25.006 ) 25.006/25.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.006/25.006 25.006/25.006 25.006/25.006 Problem 1: 25.006/25.006 25.006/25.006 Inlining of Conditions Processor [STERN17]: 25.006/25.006 25.006/25.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.006/25.006 Confluence Problem: 25.006/25.006 (VAR vNonEmpty:S x:S) 25.006/25.006 (STRATEGY CONTEXTSENSITIVE 25.006/25.006 (f 1) 25.006/25.006 (g 1 2) 25.006/25.006 (a) 25.006/25.006 (b) 25.006/25.006 (c) 25.006/25.006 (fSNonEmpty) 25.006/25.006 ) 25.006/25.006 (RULES 25.006/25.006 f(x:S) -> c | a ->* b 25.006/25.006 g(x:S,x:S) -> g(f(a),f(b)) 25.006/25.006 ) 25.006/25.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.006/25.006 25.006/25.006 25.006/25.006 Problem 1: 25.006/25.006 25.006/25.006 Clean CTRS Processor: 25.006/25.006 25.006/25.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.006/25.006 Confluence Problem: 25.006/25.006 (VAR x:S) 25.006/25.006 (STRATEGY CONTEXTSENSITIVE 25.006/25.006 (f 1) 25.006/25.006 (g 1 2) 25.006/25.006 (a) 25.006/25.006 (b) 25.006/25.006 (c) 25.006/25.006 (fSNonEmpty) 25.006/25.006 ) 25.006/25.006 (RULES 25.006/25.006 g(x:S,x:S) -> g(f(a),f(b)) 25.006/25.006 ) 25.006/25.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.006/25.006 25.006/25.006 CRule InfChecker Info: 25.006/25.006 f(x:S) -> c | a ->* b 25.006/25.006 Rule deleted 25.006/25.006 Proof: 25.006/25.006 YES 25.006/25.006 25.006/25.006 Problem 1: 25.006/25.006 25.006/25.006 Infeasibility Problem: 25.006/25.006 [(VAR vNonEmpty:S vNonEmpty:S:S x:S:S) 25.006/25.006 (STRATEGY CONTEXTSENSITIVE 25.006/25.006 (f 1) 25.006/25.006 (g 1 2) 25.006/25.006 (a) 25.006/25.006 (b) 25.006/25.006 (c) 25.006/25.006 (fSNonEmpty) 25.006/25.006 ) 25.006/25.006 (RULES 25.006/25.006 f(x:S:S) -> c | a ->* b 25.006/25.006 g(x:S:S,x:S:S) -> g(f(a),f(b)) 25.006/25.006 )] 25.006/25.006 25.006/25.006 Infeasibility Conditions: 25.006/25.006 a ->* b 25.006/25.006 25.006/25.006 Problem 1: 25.006/25.006 25.006/25.006 Obtaining a model using Mace4: 25.006/25.006 25.006/25.006 -> Usable Rules: 25.006/25.006 Empty 25.006/25.006 25.006/25.006 -> Mace4 Output: 25.006/25.006 ============================== Mace4 ================================= 25.006/25.006 Mace4 (64) version 2009-11A, November 2009. 25.006/25.006 Process 108982 was started by ubuntu on ubuntu, 25.006/25.006 Fri Jul 16 15:02:37 2021 25.006/25.006 The command was "./mace4 -c -f /tmp/mace4108969-2.in". 25.006/25.006 ============================== end of head =========================== 25.006/25.006 25.006/25.006 ============================== INPUT ================================= 25.006/25.006 25.006/25.006 % Reading from file /tmp/mace4108969-2.in 25.006/25.006 25.006/25.006 assign(max_seconds,10). 25.006/25.006 25.006/25.006 formulas(assumptions). 25.006/25.006 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence). 25.006/25.006 ->(x1,y) -> ->(g(x1,x2),g(y,x2)) # label(congruence). 25.006/25.006 ->(x2,y) -> ->(g(x1,x2),g(x1,y)) # label(congruence). 25.006/25.006 ->*(x,x) # label(reflexivity). 25.006/25.006 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 25.006/25.006 end_of_list. 25.006/25.006 25.006/25.006 formulas(goals). 25.006/25.006 ->*(a,b) # label(goal). 25.006/25.006 end_of_list. 25.006/25.006 25.006/25.006 ============================== end of input ========================== 25.006/25.006 25.006/25.006 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 25.006/25.006 25.006/25.006 % Formulas that are not ordinary clauses: 25.006/25.006 1 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence) # label(non_clause). [assumption]. 25.006/25.006 2 ->(x1,y) -> ->(g(x1,x2),g(y,x2)) # label(congruence) # label(non_clause). [assumption]. 25.006/25.006 3 ->(x2,y) -> ->(g(x1,x2),g(x1,y)) # label(congruence) # label(non_clause). [assumption]. 25.006/25.006 4 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 25.006/25.006 5 ->*(a,b) # label(goal) # label(non_clause) # label(goal). [goal]. 25.006/25.006 25.006/25.006 ============================== end of process non-clausal formulas === 25.006/25.006 25.006/25.006 ============================== CLAUSES FOR SEARCH ==================== 25.006/25.006 25.006/25.006 formulas(mace4_clauses). 25.006/25.006 -->(x,y) | ->(f(x),f(y)) # label(congruence). 25.006/25.006 -->(x,y) | ->(g(x,z),g(y,z)) # label(congruence). 25.006/25.006 -->(x,y) | ->(g(z,x),g(z,y)) # label(congruence). 25.006/25.006 ->*(x,x) # label(reflexivity). 25.006/25.006 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 25.006/25.006 -->*(a,b) # label(goal). 25.006/25.006 end_of_list. 25.006/25.006 25.006/25.006 ============================== end of clauses for search ============= 25.006/25.006 25.006/25.006 % There are no natural numbers in the input. 25.006/25.006 25.006/25.006 ============================== DOMAIN SIZE 2 ========================= 25.006/25.006 25.006/25.006 ============================== MODEL ================================= 25.006/25.006 25.006/25.006 interpretation( 2, [number=1, seconds=0], [ 25.006/25.006 25.006/25.006 function(a, [ 0 ]), 25.006/25.006 25.006/25.006 function(b, [ 1 ]), 25.006/25.006 25.006/25.006 function(f(_), [ 0, 0 ]), 25.006/25.006 25.006/25.006 function(g(_,_), [ 25.006/25.006 0, 0, 25.006/25.006 0, 0 ]), 25.006/25.006 25.006/25.006 relation(->*(_,_), [ 25.006/25.006 1, 0, 25.006/25.006 0, 1 ]), 25.006/25.006 25.006/25.006 relation(->(_,_), [ 25.006/25.006 0, 0, 25.006/25.006 0, 0 ]) 25.006/25.006 ]). 25.006/25.006 25.006/25.006 ============================== end of model ========================== 25.006/25.006 25.006/25.006 ============================== STATISTICS ============================ 25.006/25.006 25.006/25.006 For domain size 2. 25.006/25.006 25.006/25.006 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 25.006/25.006 Ground clauses: seen=31, kept=27. 25.006/25.006 Selections=9, assignments=9, propagations=7, current_models=1. 25.006/25.006 Rewrite_terms=42, rewrite_bools=34, indexes=4. 25.006/25.006 Rules_from_neg_clauses=1, cross_offs=1. 25.006/25.006 25.006/25.006 ============================== end of statistics ===================== 25.006/25.006 25.006/25.006 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 25.006/25.006 25.006/25.006 Exiting with 1 model. 25.006/25.006 25.006/25.006 Process 108982 exit (max_models) Fri Jul 16 15:02:37 2021 25.006/25.006 The process finished Fri Jul 16 15:02:37 2021 25.006/25.006 25.006/25.006 25.006/25.006 Mace4 cooked interpretation: 25.006/25.006 25.006/25.006 25.006/25.006 25.006/25.006 The problem is infeasible. 25.006/25.006 25.006/25.006 25.006/25.006 CRule InfChecker Info: 25.006/25.006 g(x:S,x:S) -> g(f(a),f(b)) 25.006/25.006 Rule remains 25.006/25.006 Proof: 25.006/25.006 NO_CONDS 25.006/25.006 25.006/25.006 Problem 1: 25.006/25.006 25.006/25.006 Transform No Conds CTRS Processor: 25.006/25.006 25.006/25.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.006/25.006 Confluence Problem: 25.006/25.006 (VAR x:S) 25.006/25.006 (STRATEGY CONTEXTSENSITIVE 25.006/25.006 (f 1) 25.006/25.006 (g 1 2) 25.006/25.006 (a) 25.006/25.006 (b) 25.006/25.006 (c) 25.006/25.006 (fSNonEmpty) 25.006/25.006 ) 25.006/25.006 (RULES 25.006/25.006 g(x:S,x:S) -> g(f(a),f(b)) 25.006/25.006 ) 25.006/25.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.006/25.006 Resulting R: 25.006/25.006 (VAR x:S) 25.006/25.006 (STRATEGY CONTEXTSENSITIVE 25.006/25.006 (f 1) 25.006/25.006 (g 1 2) 25.006/25.006 (a) 25.006/25.006 (b) 25.006/25.006 (c) 25.006/25.006 (fSNonEmpty) 25.006/25.006 ) 25.006/25.006 (RULES 25.006/25.006 g(x:S,x:S) -> g(f(a),f(b)) 25.006/25.006 ) 25.006/25.006 25.006/25.006 Problem 1: 25.006/25.006 25.006/25.006 CleanTRS Processor: 25.006/25.006 25.006/25.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.006/25.006 Confluence Problem: 25.006/25.006 (VAR x:S) 25.006/25.006 (STRATEGY CONTEXTSENSITIVE 25.006/25.006 (f 1) 25.006/25.006 (g 1 2) 25.006/25.006 (a) 25.006/25.006 (b) 25.006/25.006 (c) 25.006/25.006 (fSNonEmpty) 25.006/25.006 ) 25.006/25.006 (RULES 25.006/25.006 g(x:S,x:S) -> g(f(a),f(b)) 25.006/25.006 ) 25.006/25.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.006/25.006 25.006/25.006 25.006/25.006 Problem 1: 25.006/25.006 25.006/25.006 Modular Confluence Combinations Decomposition Processor: 25.006/25.006 25.006/25.006 No usable combinations 25.006/25.006 25.006/25.006 Problem 1: 25.006/25.006 Termination Processor: 25.006/25.006 (STRATEGY CONTEXTSENSITIVE 25.006/25.006 (f 1) 25.006/25.006 (g 1 2) 25.006/25.006 (a) 25.006/25.006 (b) 25.006/25.006 (c) 25.006/25.006 (fSNonEmpty) 25.006/25.006 ) 25.006/25.006 Terminating? 25.006/25.006 YES 25.006/25.006 25.006/25.006 Problem 1: 25.006/25.006 25.006/25.006 (VAR vu95NonEmpty:S xu58S:S) 25.006/25.006 (STRATEGY CONTEXTSENSITIVE 25.006/25.006 (g 1 2) 25.006/25.006 (a) 25.006/25.006 (b) 25.006/25.006 (f 1) 25.006/25.006 (fSNonEmpty) 25.006/25.006 ) 25.006/25.006 (RULES 25.006/25.006 g(xu58S:S,xu58S:S) -> g(f(a),f(b)) 25.006/25.006 ) 25.006/25.006 25.006/25.006 Problem 1: 25.006/25.006 25.006/25.006 Dependency Pairs Processor: 25.006/25.006 -> Pairs: 25.006/25.006 Empty 25.006/25.006 -> Rules: 25.006/25.006 g(xu58S:S,xu58S:S) -> g(f(a),f(b)) 25.006/25.006 -> Unhiding Rules: 25.006/25.006 Empty 25.006/25.006 25.006/25.006 Problem 1: 25.006/25.006 25.006/25.006 Basic Processor: 25.006/25.006 -> Pairs: 25.006/25.006 Empty 25.006/25.006 -> Rules: 25.006/25.006 g(xu58S:S,xu58S:S) -> g(f(a),f(b)) 25.006/25.006 -> Unhiding rules: 25.006/25.006 Empty 25.006/25.006 -> Result: 25.006/25.006 Set P is empty 25.006/25.006 25.006/25.006 The problem is finite. 25.006/25.006 25.006/25.006 Problem 1.1: 25.006/25.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.006/25.006 Confluence Problem: 25.006/25.006 (VAR x:S) 25.006/25.006 (STRATEGY CONTEXTSENSITIVE 25.006/25.006 (f 1) 25.006/25.006 (g 1 2) 25.006/25.006 (a) 25.006/25.006 (b) 25.006/25.006 (c) 25.006/25.006 (fSNonEmpty) 25.006/25.006 ) 25.006/25.006 (RULES 25.006/25.006 g(x:S,x:S) -> g(f(a),f(b)) 25.006/25.006 ) 25.006/25.006 Terminating:"YES" 25.006/25.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.006/25.006 25.006/25.006 Huet Levy Processor: 25.006/25.006 -> Rules: 25.006/25.006 g(x:S,x:S) -> g(f(a),f(b)) 25.006/25.006 -> Vars: 25.006/25.006 x 25.006/25.006 -> FVars: 25.006/25.006 x2 25.006/25.006 -> PVars: 25.006/25.006 x: [x2] 25.006/25.006 25.006/25.006 -> Rlps: 25.006/25.006 (rule: g(x2:S,x2:S) -> g(f(a),f(b)), id: 1, possubterms: g(x2:S,x2:S)->[]) 25.006/25.006 25.006/25.006 -> Unifications: 25.006/25.006 25.006/25.006 25.006/25.006 -> Critical pairs info: 25.006/25.006 25.006/25.006 25.006/25.006 -> Problem conclusions: 25.006/25.006 Not left linear, Right linear, Not linear 25.006/25.006 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 25.006/25.006 Not Huet-Levy confluent, Newman confluent 25.006/25.006 R is a TRS 25.006/25.006 25.006/25.006 25.006/25.006 The problem is joinable. 25.006/25.006 21.86user 0.14system 0:25.06elapsed 87%CPU (0avgtext+0avgdata 44780maxresident)k 25.006/25.006 8inputs+0outputs (0major+35036minor)pagefaults 0swaps