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