45.027/45.027 NO 45.027/45.027 45.027/45.027 Problem 1: 45.027/45.027 45.027/45.027 45.027/45.027 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.027/45.027 Confluence Problem: 45.027/45.027 (VAR vNonEmpty x y z) 45.027/45.027 (REPLACEMENT-MAP 45.027/45.027 (a 1) 45.027/45.027 (f 1, 2) 45.027/45.027 (b) 45.027/45.027 (c 1) 45.027/45.027 (fSNonEmpty) 45.027/45.027 ) 45.027/45.027 (RULES 45.027/45.027 a(x) -> f(x,x) 45.027/45.027 a(x) -> b 45.027/45.027 f(c(c(c(x))),y) -> a(y) | c(f(c(x),c(c(y)))) ->* c(a(a(b))) 45.027/45.027 f(c(x),c(c(y))) -> a(a(x)) | c(f(x,y)) ->* c(a(b)) 45.027/45.027 ) 45.027/45.027 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.027/45.027 45.027/45.027 45.027/45.027 Problem 1: 45.027/45.027 45.027/45.027 Inlining of Conditions Processor [STERN17]: 45.027/45.027 45.027/45.027 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.027/45.027 Confluence Problem: 45.027/45.027 (VAR vNonEmpty x y z) 45.027/45.027 (REPLACEMENT-MAP 45.027/45.027 (a 1) 45.027/45.027 (f 1, 2) 45.027/45.027 (b) 45.027/45.027 (c 1) 45.027/45.027 (fSNonEmpty) 45.027/45.027 ) 45.027/45.027 (RULES 45.027/45.027 a(x) -> f(x,x) 45.027/45.027 a(x) -> b 45.027/45.027 f(c(c(c(x))),y) -> a(y) | c(f(c(x),c(c(y)))) ->* c(a(a(b))) 45.027/45.027 f(c(x),c(c(y))) -> a(a(x)) | c(f(x,y)) ->* c(a(b)) 45.027/45.027 ) 45.027/45.027 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.027/45.027 45.027/45.027 45.027/45.027 Problem 1: 45.027/45.027 45.027/45.027 Clean CTRS Processor: 45.027/45.027 45.027/45.027 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.027/45.027 Confluence Problem: 45.027/45.027 (VAR x) 45.027/45.027 (REPLACEMENT-MAP 45.027/45.027 (a 1) 45.027/45.027 (f 1, 2) 45.027/45.027 (b) 45.027/45.027 (c 1) 45.027/45.027 (fSNonEmpty) 45.027/45.027 ) 45.027/45.027 (RULES 45.027/45.027 a(x) -> f(x,x) 45.027/45.027 a(x) -> b 45.027/45.027 ) 45.027/45.027 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.027/45.027 45.027/45.027 CRule InfChecker Info: 45.027/45.027 a(x) -> f(x,x) 45.027/45.027 Rule remains 45.027/45.027 Proof: 45.027/45.027 NO_CONDS 45.027/45.027 45.027/45.027 CRule InfChecker Info: 45.027/45.027 a(x) -> b 45.027/45.027 Rule remains 45.027/45.027 Proof: 45.027/45.027 NO_CONDS 45.027/45.027 45.027/45.027 CRule InfChecker Info: 45.027/45.027 f(c(c(c(x))),y) -> a(y) | c(f(c(x),c(c(y)))) ->* c(a(a(b))) 45.027/45.027 Rule deleted 45.027/45.027 Proof: 45.027/45.027 YES 45.027/45.027 45.027/45.027 Problem 1: 45.027/45.027 45.027/45.027 Infeasibility Problem: 45.027/45.027 [(VAR vNonEmpty x y z vNonEmpty x y) 45.027/45.027 (STRATEGY CONTEXTSENSITIVE 45.027/45.027 (a 1) 45.027/45.027 (f 1 2) 45.027/45.027 (b) 45.027/45.027 (c 1) 45.027/45.027 (fSNonEmpty) 45.027/45.027 ) 45.027/45.027 (RULES 45.027/45.027 a(x) -> f(x,x) 45.027/45.027 a(x) -> b 45.027/45.027 f(c(c(c(x))),y) -> a(y) | c(f(c(x),c(c(y)))) ->* c(a(a(b))) 45.027/45.027 f(c(x),c(c(y))) -> a(a(x)) | c(f(x,y)) ->* c(a(b)) 45.027/45.027 )] 45.027/45.027 45.027/45.027 Infeasibility Conditions: 45.027/45.027 c(f(c(x),c(c(y)))) ->* c(a(a(b))) 45.027/45.027 45.027/45.027 Problem 1: 45.027/45.027 45.027/45.027 Obtaining a model using Mace4: 45.027/45.027 45.027/45.027 -> Usable Rules: 45.027/45.027 a(x) -> f(x,x) 45.027/45.027 a(x) -> b 45.027/45.027 f(c(c(c(x))),y) -> a(y) | c(f(c(x),c(c(y)))) ->* c(a(a(b))) 45.027/45.027 f(c(x),c(c(y))) -> a(a(x)) | c(f(x,y)) ->* c(a(b)) 45.027/45.027 45.027/45.027 -> Mace4 Output: 45.027/45.027 ============================== Mace4 ================================= 45.027/45.027 Mace4 (64) version 2009-11A, November 2009. 45.027/45.027 Process 73784 was started by ubuntu on ubuntu, 45.027/45.027 Wed Mar 9 10:06:41 2022 45.027/45.027 The command was "./mace4 -c -f /tmp/mace473771-2.in". 45.027/45.027 ============================== end of head =========================== 45.027/45.027 45.027/45.027 ============================== INPUT ================================= 45.027/45.027 45.027/45.027 % Reading from file /tmp/mace473771-2.in 45.027/45.027 45.027/45.027 assign(max_seconds,20). 45.027/45.027 45.027/45.027 formulas(assumptions). 45.027/45.027 ->(x1,y) -> ->(a(x1),a(y)) # label(congruence). 45.027/45.027 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence). 45.027/45.027 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence). 45.027/45.027 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence). 45.027/45.027 ->(a(x1),f(x1,x1)) # label(replacement). 45.027/45.027 ->(a(x1),b) # label(replacement). 45.027/45.027 ->*(c(f(c(x1),c(c(x2)))),c(a(a(b)))) -> ->(f(c(c(c(x1))),x2),a(x2)) # label(replacement). 45.027/45.027 ->*(c(f(x1,x2)),c(a(b))) -> ->(f(c(x1),c(c(x2))),a(a(x1))) # label(replacement). 45.027/45.027 ->*(x,x) # label(reflexivity). 45.027/45.027 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 45.027/45.027 end_of_list. 45.027/45.027 45.027/45.027 formulas(goals). 45.027/45.027 (exists x5 exists x6 ->*(c(f(c(x5),c(c(x6)))),c(a(a(b))))) # label(goal). 45.027/45.027 end_of_list. 45.027/45.027 45.027/45.027 ============================== end of input ========================== 45.027/45.027 45.027/45.027 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 45.027/45.027 45.027/45.027 % Formulas that are not ordinary clauses: 45.027/45.027 1 ->(x1,y) -> ->(a(x1),a(y)) # label(congruence) # label(non_clause). [assumption]. 45.027/45.027 2 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 45.027/45.027 3 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 45.027/45.027 4 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence) # label(non_clause). [assumption]. 45.027/45.027 5 ->*(c(f(c(x1),c(c(x2)))),c(a(a(b)))) -> ->(f(c(c(c(x1))),x2),a(x2)) # label(replacement) # label(non_clause). [assumption]. 45.027/45.027 6 ->*(c(f(x1,x2)),c(a(b))) -> ->(f(c(x1),c(c(x2))),a(a(x1))) # label(replacement) # label(non_clause). [assumption]. 45.027/45.027 7 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 45.027/45.027 8 (exists x5 exists x6 ->*(c(f(c(x5),c(c(x6)))),c(a(a(b))))) # label(goal) # label(non_clause) # label(goal). [goal]. 45.027/45.027 45.027/45.027 ============================== end of process non-clausal formulas === 45.027/45.027 45.027/45.027 ============================== CLAUSES FOR SEARCH ==================== 45.027/45.027 45.027/45.027 formulas(mace4_clauses). 45.027/45.027 -->(x,y) | ->(a(x),a(y)) # label(congruence). 45.027/45.027 -->(x,y) | ->(f(x,z),f(y,z)) # label(congruence). 45.027/45.027 -->(x,y) | ->(f(z,x),f(z,y)) # label(congruence). 45.027/45.027 -->(x,y) | ->(c(x),c(y)) # label(congruence). 45.027/45.027 ->(a(x),f(x,x)) # label(replacement). 45.027/45.027 ->(a(x),b) # label(replacement). 45.027/45.027 -->*(c(f(c(x),c(c(y)))),c(a(a(b)))) | ->(f(c(c(c(x))),y),a(y)) # label(replacement). 45.027/45.027 -->*(c(f(x,y)),c(a(b))) | ->(f(c(x),c(c(y))),a(a(x))) # label(replacement). 45.027/45.027 ->*(x,x) # label(reflexivity). 45.027/45.027 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 45.027/45.027 -->*(c(f(c(x),c(c(y)))),c(a(a(b)))) # label(goal). 45.027/45.027 end_of_list. 45.027/45.027 45.027/45.027 ============================== end of clauses for search ============= 45.027/45.027 45.027/45.027 % There are no natural numbers in the input. 45.027/45.027 45.027/45.027 ============================== DOMAIN SIZE 2 ========================= 45.027/45.027 45.027/45.027 ============================== MODEL ================================= 45.027/45.027 45.027/45.027 interpretation( 2, [number=1, seconds=0], [ 45.027/45.027 45.027/45.027 function(b, [ 0 ]), 45.027/45.027 45.027/45.027 function(a(_), [ 0, 0 ]), 45.027/45.027 45.027/45.027 function(c(_), [ 0, 1 ]), 45.027/45.027 45.027/45.027 function(f(_,_), [ 45.027/45.027 1, 1, 45.027/45.027 1, 1 ]), 45.027/45.027 45.027/45.027 relation(->*(_,_), [ 45.027/45.027 1, 1, 45.027/45.027 0, 1 ]), 45.027/45.027 45.027/45.027 relation(->(_,_), [ 45.027/45.027 1, 1, 45.027/45.027 0, 1 ]) 45.027/45.027 ]). 45.027/45.027 45.027/45.027 ============================== end of model ========================== 45.027/45.027 45.027/45.027 ============================== STATISTICS ============================ 45.027/45.027 45.027/45.027 For domain size 2. 45.027/45.027 45.027/45.027 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 45.027/45.027 Ground clauses: seen=50, kept=46. 45.027/45.027 Selections=5, assignments=6, propagations=12, current_models=1. 45.027/45.027 Rewrite_terms=198, rewrite_bools=74, indexes=51. 45.027/45.027 Rules_from_neg_clauses=4, cross_offs=4. 45.027/45.027 45.027/45.027 ============================== end of statistics ===================== 45.027/45.027 45.027/45.027 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 45.027/45.027 45.027/45.027 Exiting with 1 model. 45.027/45.027 45.027/45.027 Process 73784 exit (max_models) Wed Mar 9 10:06:41 2022 45.027/45.027 The process finished Wed Mar 9 10:06:41 2022 45.027/45.027 45.027/45.027 45.027/45.027 Mace4 cooked interpretation: 45.027/45.027 45.027/45.027 45.027/45.027 45.027/45.027 The problem is infeasible. 45.027/45.027 45.027/45.027 45.027/45.027 CRule InfChecker Info: 45.027/45.027 f(c(x),c(c(y))) -> a(a(x)) | c(f(x,y)) ->* c(a(b)) 45.027/45.027 Rule deleted 45.027/45.027 Proof: 45.027/45.027 YES 45.027/45.027 45.027/45.027 Problem 1: 45.027/45.027 45.027/45.027 Infeasibility Problem: 45.027/45.027 [(VAR vNonEmpty x y vNonEmpty x y) 45.027/45.027 (STRATEGY CONTEXTSENSITIVE 45.027/45.027 (a 1) 45.027/45.027 (f 1 2) 45.027/45.027 (b) 45.027/45.027 (c 1) 45.027/45.027 (fSNonEmpty) 45.027/45.027 ) 45.027/45.027 (RULES 45.027/45.027 a(x) -> f(x,x) 45.027/45.027 a(x) -> b 45.027/45.027 f(c(x),c(c(y))) -> a(a(x)) | c(f(x,y)) ->* c(a(b)) 45.027/45.027 )] 45.027/45.027 45.027/45.027 Infeasibility Conditions: 45.027/45.027 c(f(x,y)) ->* c(a(b)) 45.027/45.027 45.027/45.027 Problem 1: 45.027/45.027 45.027/45.027 Obtaining a model using Mace4: 45.027/45.027 45.027/45.027 -> Usable Rules: 45.027/45.027 a(x) -> f(x,x) 45.027/45.027 a(x) -> b 45.027/45.027 f(c(x),c(c(y))) -> a(a(x)) | c(f(x,y)) ->* c(a(b)) 45.027/45.027 45.027/45.027 -> Mace4 Output: 45.027/45.027 ============================== Mace4 ================================= 45.027/45.027 Mace4 (64) version 2009-11A, November 2009. 45.027/45.027 Process 73817 was started by ubuntu on ubuntu, 45.027/45.027 Wed Mar 9 10:07:01 2022 45.027/45.027 The command was "./mace4 -c -f /tmp/mace473804-2.in". 45.027/45.027 ============================== end of head =========================== 45.027/45.027 45.027/45.027 ============================== INPUT ================================= 45.027/45.027 45.027/45.027 % Reading from file /tmp/mace473804-2.in 45.027/45.027 45.027/45.027 assign(max_seconds,20). 45.027/45.027 45.027/45.027 formulas(assumptions). 45.027/45.027 ->(x1,y) -> ->(a(x1),a(y)) # label(congruence). 45.027/45.027 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence). 45.027/45.027 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence). 45.027/45.027 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence). 45.027/45.027 ->(a(x1),f(x1,x1)) # label(replacement). 45.027/45.027 ->(a(x1),b) # label(replacement). 45.027/45.027 ->*(c(f(x1,x2)),c(a(b))) -> ->(f(c(x1),c(c(x2))),a(a(x1))) # label(replacement). 45.027/45.027 ->*(x,x) # label(reflexivity). 45.027/45.027 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 45.027/45.027 end_of_list. 45.027/45.027 45.027/45.027 formulas(goals). 45.027/45.027 (exists x4 exists x5 ->*(c(f(x4,x5)),c(a(b)))) # label(goal). 45.027/45.027 end_of_list. 45.027/45.027 45.027/45.027 ============================== end of input ========================== 45.027/45.027 45.027/45.027 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 45.027/45.027 45.027/45.027 % Formulas that are not ordinary clauses: 45.027/45.027 1 ->(x1,y) -> ->(a(x1),a(y)) # label(congruence) # label(non_clause). [assumption]. 45.027/45.027 2 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 45.027/45.027 3 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 45.027/45.027 4 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence) # label(non_clause). [assumption]. 45.027/45.027 5 ->*(c(f(x1,x2)),c(a(b))) -> ->(f(c(x1),c(c(x2))),a(a(x1))) # label(replacement) # label(non_clause). [assumption]. 45.027/45.027 6 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 45.027/45.027 7 (exists x4 exists x5 ->*(c(f(x4,x5)),c(a(b)))) # label(goal) # label(non_clause) # label(goal). [goal]. 45.027/45.027 45.027/45.027 ============================== end of process non-clausal formulas === 45.027/45.027 45.027/45.027 ============================== CLAUSES FOR SEARCH ==================== 45.027/45.027 45.027/45.027 formulas(mace4_clauses). 45.027/45.027 -->(x,y) | ->(a(x),a(y)) # label(congruence). 45.027/45.027 -->(x,y) | ->(f(x,z),f(y,z)) # label(congruence). 45.027/45.027 -->(x,y) | ->(f(z,x),f(z,y)) # label(congruence). 45.027/45.027 -->(x,y) | ->(c(x),c(y)) # label(congruence). 45.027/45.027 ->(a(x),f(x,x)) # label(replacement). 45.027/45.027 ->(a(x),b) # label(replacement). 45.027/45.027 -->*(c(f(x,y)),c(a(b))) | ->(f(c(x),c(c(y))),a(a(x))) # label(replacement). 45.027/45.027 ->*(x,x) # label(reflexivity). 45.027/45.027 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 45.027/45.027 -->*(c(f(x,y)),c(a(b))) # label(goal). 45.027/45.027 end_of_list. 45.027/45.027 45.027/45.027 ============================== end of clauses for search ============= 45.027/45.027 45.027/45.027 % There are no natural numbers in the input. 45.027/45.027 45.027/45.027 ============================== DOMAIN SIZE 2 ========================= 45.027/45.027 45.027/45.027 ============================== MODEL ================================= 45.027/45.027 45.027/45.027 interpretation( 2, [number=1, seconds=0], [ 45.027/45.027 45.027/45.027 function(b, [ 0 ]), 45.027/45.027 45.027/45.027 function(a(_), [ 0, 0 ]), 45.027/45.027 45.027/45.027 function(c(_), [ 0, 1 ]), 45.027/45.027 45.027/45.027 function(f(_,_), [ 45.027/45.027 1, 1, 45.027/45.027 1, 1 ]), 45.027/45.027 45.027/45.027 relation(->*(_,_), [ 45.027/45.027 1, 1, 45.027/45.027 0, 1 ]), 45.027/45.027 45.027/45.027 relation(->(_,_), [ 45.027/45.027 1, 1, 45.027/45.027 0, 1 ]) 45.027/45.027 ]). 45.027/45.027 45.027/45.027 ============================== end of model ========================== 45.027/45.027 45.027/45.027 ============================== STATISTICS ============================ 45.027/45.027 45.027/45.027 For domain size 2. 45.027/45.027 45.027/45.027 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 45.027/45.027 Ground clauses: seen=46, kept=42. 45.027/45.027 Selections=5, assignments=6, propagations=12, current_models=1. 45.027/45.027 Rewrite_terms=123, rewrite_bools=68, indexes=29. 45.027/45.027 Rules_from_neg_clauses=4, cross_offs=4. 45.027/45.027 45.027/45.027 ============================== end of statistics ===================== 45.027/45.027 45.027/45.027 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 45.027/45.027 45.027/45.027 Exiting with 1 model. 45.027/45.027 45.027/45.027 Process 73817 exit (max_models) Wed Mar 9 10:07:01 2022 45.027/45.027 The process finished Wed Mar 9 10:07:01 2022 45.027/45.027 45.027/45.027 45.027/45.027 Mace4 cooked interpretation: 45.027/45.027 45.027/45.027 45.027/45.027 45.027/45.027 The problem is infeasible. 45.027/45.027 45.027/45.027 45.027/45.027 Problem 1: 45.027/45.027 45.027/45.027 Transform No Conds CTRS Processor: 45.027/45.027 45.027/45.027 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.027/45.027 Confluence Problem: 45.027/45.027 (VAR x) 45.027/45.027 (REPLACEMENT-MAP 45.027/45.027 (a 1) 45.027/45.027 (f 1, 2) 45.027/45.027 (b) 45.027/45.027 (c 1) 45.027/45.027 (fSNonEmpty) 45.027/45.027 ) 45.027/45.027 (RULES 45.027/45.027 a(x) -> f(x,x) 45.027/45.027 a(x) -> b 45.027/45.027 ) 45.027/45.027 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.027/45.027 Resulting R: 45.027/45.027 (VAR x) 45.027/45.027 (STRATEGY CONTEXTSENSITIVE 45.027/45.027 (a 1) 45.027/45.027 (f 1 2) 45.027/45.027 (b) 45.027/45.027 (c 1) 45.027/45.027 (fSNonEmpty) 45.027/45.027 ) 45.027/45.027 (RULES 45.027/45.027 a(x) -> f(x,x) 45.027/45.027 a(x) -> b 45.027/45.027 ) 45.027/45.027 45.027/45.027 Problem 1: 45.027/45.027 45.027/45.027 CleanTRS Processor: 45.027/45.027 45.027/45.027 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.027/45.027 Confluence Problem: 45.027/45.027 (VAR x) 45.027/45.027 (REPLACEMENT-MAP 45.027/45.027 (a 1) 45.027/45.027 (f 1, 2) 45.027/45.027 (b) 45.027/45.027 (c 1) 45.027/45.027 (fSNonEmpty) 45.027/45.027 ) 45.027/45.027 (RULES 45.027/45.027 a(x) -> f(x,x) 45.027/45.027 a(x) -> b 45.027/45.027 ) 45.027/45.027 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.027/45.027 45.027/45.027 45.027/45.027 Problem 1: 45.027/45.027 45.027/45.027 Modular Confluence Combinations Decomposition Processor: 45.027/45.027 45.027/45.027 No usable combinations 45.027/45.027 45.027/45.027 Problem 1: 45.027/45.027 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.027/45.027 Confluence Problem: 45.027/45.027 (VAR x) 45.027/45.027 (REPLACEMENT-MAP 45.027/45.027 (a 1) 45.027/45.027 (f 1, 2) 45.027/45.027 (b) 45.027/45.027 (c 1) 45.027/45.027 (fSNonEmpty) 45.027/45.027 ) 45.027/45.027 (RULES 45.027/45.027 a(x) -> f(x,x) 45.027/45.027 a(x) -> b 45.027/45.027 ) 45.027/45.027 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.027/45.027 45.027/45.027 Huet Levy Processor: 45.027/45.027 -> Rules: 45.027/45.027 a(x) -> f(x,x) 45.027/45.027 a(x) -> b 45.027/45.027 -> Vars: 45.027/45.027 x, x 45.027/45.027 45.027/45.027 -> Rlps: 45.027/45.027 (rule: a(x) -> f(x,x), id: 1, possubterms: a(x)->[]) 45.027/45.027 (rule: a(x) -> b, id: 2, possubterms: a(x)->[]) 45.027/45.027 45.027/45.027 -> Unifications: 45.027/45.027 (R2 unifies with R1 at p: [], l: a(x), lp: a(x), sig: {x -> x'}, l': a(x'), r: b, r': f(x',x')) 45.027/45.027 45.027/45.027 -> Critical pairs info: 45.027/45.027 => Not trivial, Overlay, NW0, N1 45.027/45.027 45.027/45.027 -> Problem conclusions: 45.027/45.027 Left linear, Not right linear, Not linear 45.027/45.027 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 45.027/45.027 Not Huet-Levy confluent, Not Newman confluent 45.027/45.027 R is a TRS 45.027/45.027 45.027/45.027 45.027/45.027 Problem 1: 45.027/45.027 Different Normal CP Terms Processor: 45.027/45.027 => Not trivial, Overlay, NW0, N1, Normal and not trivial cp 45.027/45.027 45.027/45.027 The problem is not joinable. 45.027/45.027 48.37user 2.79system 0:45.27elapsed 113%CPU (0avgtext+0avgdata 128168maxresident)k 45.027/45.027 8inputs+0outputs (0major+117619minor)pagefaults 0swaps