65.058/65.058 NO 65.058/65.058 65.058/65.058 Problem 1: 65.058/65.058 65.058/65.058 65.058/65.058 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 65.058/65.058 Confluence Problem: 65.058/65.058 (VAR vNonEmpty:S x:S y:S z:S) 65.058/65.058 (STRATEGY CONTEXTSENSITIVE 65.058/65.058 (a 1) 65.058/65.058 (f 1 2) 65.058/65.058 (b) 65.058/65.058 (c 1) 65.058/65.058 (fSNonEmpty) 65.058/65.058 ) 65.058/65.058 (RULES 65.058/65.058 a(x:S) -> f(x:S,x:S) 65.058/65.058 a(x:S) -> b 65.058/65.058 f(c(c(c(x:S))),y:S) -> a(y:S) | c(f(c(x:S),c(c(y:S)))) ->* c(a(a(b))) 65.058/65.058 f(c(x:S),c(c(y:S))) -> a(a(x:S)) | c(f(x:S,y:S)) ->* c(a(b)) 65.058/65.058 ) 65.058/65.058 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 65.058/65.058 65.058/65.058 65.058/65.058 Problem 1: 65.058/65.058 65.058/65.058 Inlining of Conditions Processor [STERN17]: 65.058/65.058 65.058/65.058 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 65.058/65.058 Confluence Problem: 65.058/65.058 (VAR vNonEmpty:S x:S y:S z:S) 65.058/65.058 (STRATEGY CONTEXTSENSITIVE 65.058/65.058 (a 1) 65.058/65.058 (f 1 2) 65.058/65.058 (b) 65.058/65.058 (c 1) 65.058/65.058 (fSNonEmpty) 65.058/65.058 ) 65.058/65.058 (RULES 65.058/65.058 a(x:S) -> f(x:S,x:S) 65.058/65.058 a(x:S) -> b 65.058/65.058 f(c(c(c(x:S))),y:S) -> a(y:S) | c(f(c(x:S),c(c(y:S)))) ->* c(a(a(b))) 65.058/65.058 f(c(x:S),c(c(y:S))) -> a(a(x:S)) | c(f(x:S,y:S)) ->* c(a(b)) 65.058/65.058 ) 65.058/65.058 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 65.058/65.058 65.058/65.058 65.058/65.058 Problem 1: 65.058/65.058 65.058/65.058 Clean CTRS Processor: 65.058/65.058 65.058/65.058 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 65.058/65.058 Confluence Problem: 65.058/65.058 (VAR x:S) 65.058/65.058 (STRATEGY CONTEXTSENSITIVE 65.058/65.058 (a 1) 65.058/65.058 (f 1 2) 65.058/65.058 (b) 65.058/65.058 (c 1) 65.058/65.058 (fSNonEmpty) 65.058/65.058 ) 65.058/65.058 (RULES 65.058/65.058 a(x:S) -> f(x:S,x:S) 65.058/65.058 a(x:S) -> b 65.058/65.058 ) 65.058/65.058 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 65.058/65.058 65.058/65.058 CRule InfChecker Info: 65.058/65.058 a(x:S) -> f(x:S,x:S) 65.058/65.058 Rule remains 65.058/65.058 Proof: 65.058/65.058 NO_CONDS 65.058/65.058 65.058/65.058 CRule InfChecker Info: 65.058/65.058 a(x:S) -> b 65.058/65.058 Rule remains 65.058/65.058 Proof: 65.058/65.058 NO_CONDS 65.058/65.058 65.058/65.058 CRule InfChecker Info: 65.058/65.058 f(c(c(c(x:S))),y:S) -> a(y:S) | c(f(c(x:S),c(c(y:S)))) ->* c(a(a(b))) 65.058/65.058 Rule deleted 65.058/65.058 Proof: 65.058/65.058 YES 65.058/65.058 65.058/65.058 Problem 1: 65.058/65.058 65.058/65.058 Infeasibility Problem: 65.058/65.058 [(VAR vNonEmpty:S vNonEmpty:S:S x:S:S y:S:S z:S:S) 65.058/65.058 (STRATEGY CONTEXTSENSITIVE 65.058/65.058 (a 1) 65.058/65.058 (f 1 2) 65.058/65.058 (b) 65.058/65.058 (c 1) 65.058/65.058 (fSNonEmpty) 65.058/65.058 ) 65.058/65.058 (RULES 65.058/65.058 a(x:S:S) -> f(x:S:S,x:S:S) 65.058/65.058 a(x:S:S) -> b 65.058/65.058 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))) 65.058/65.058 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)) 65.058/65.058 )] 65.058/65.058 65.058/65.058 Infeasibility Conditions: 65.058/65.058 c(f(c(x:S:S),c(c(y:S:S)))) ->* c(a(a(b))) 65.058/65.058 65.058/65.058 Problem 1: 65.058/65.058 65.058/65.058 Obtaining a model using Mace4: 65.058/65.058 65.058/65.058 -> Usable Rules: 65.058/65.058 a(x:S:S) -> f(x:S:S,x:S:S) 65.058/65.058 a(x:S:S) -> b 65.058/65.058 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))) 65.058/65.058 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)) 65.058/65.058 65.058/65.058 -> Mace4 Output: 65.058/65.058 ============================== Mace4 ================================= 65.058/65.058 Mace4 (64) version 2009-11A, November 2009. 65.058/65.058 Process 56349 was started by ubuntu on ubuntu, 65.058/65.058 Wed Jul 14 11:19:12 2021 65.058/65.058 The command was "./mace4 -c -f /tmp/mace456336-2.in". 65.058/65.058 ============================== end of head =========================== 65.058/65.058 65.058/65.058 ============================== INPUT ================================= 65.058/65.058 65.058/65.058 % Reading from file /tmp/mace456336-2.in 65.058/65.058 65.058/65.058 assign(max_seconds,20). 65.058/65.058 65.058/65.058 formulas(assumptions). 65.058/65.058 ->(x1,y) -> ->(a(x1),a(y)) # label(congruence). 65.058/65.058 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence). 65.058/65.058 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence). 65.058/65.058 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence). 65.058/65.058 ->(a(x2),f(x2,x2)) # label(replacement). 65.058/65.058 ->(a(x2),b) # label(replacement). 65.058/65.058 ->*(c(f(c(x2),c(c(x3)))),c(a(a(b)))) -> ->(f(c(c(c(x2))),x3),a(x3)) # label(replacement). 65.058/65.058 ->*(c(f(x2,x3)),c(a(b))) -> ->(f(c(x2),c(c(x3))),a(a(x2))) # label(replacement). 65.058/65.058 ->*(x,x) # label(reflexivity). 65.058/65.058 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 65.058/65.058 end_of_list. 65.058/65.058 65.058/65.058 formulas(goals). 65.058/65.058 (exists x2 exists x3 ->*(c(f(c(x2),c(c(x3)))),c(a(a(b))))) # label(goal). 65.058/65.058 end_of_list. 65.058/65.058 65.058/65.058 ============================== end of input ========================== 65.058/65.058 65.058/65.058 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 65.058/65.058 65.058/65.058 % Formulas that are not ordinary clauses: 65.058/65.058 1 ->(x1,y) -> ->(a(x1),a(y)) # label(congruence) # label(non_clause). [assumption]. 65.058/65.058 2 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 65.058/65.058 3 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 65.058/65.058 4 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence) # label(non_clause). [assumption]. 65.058/65.058 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]. 65.058/65.058 6 ->*(c(f(x2,x3)),c(a(b))) -> ->(f(c(x2),c(c(x3))),a(a(x2))) # label(replacement) # label(non_clause). [assumption]. 65.058/65.058 7 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 65.058/65.058 8 (exists x2 exists x3 ->*(c(f(c(x2),c(c(x3)))),c(a(a(b))))) # label(goal) # label(non_clause) # label(goal). [goal]. 65.058/65.058 65.058/65.058 ============================== end of process non-clausal formulas === 65.058/65.058 65.058/65.058 ============================== CLAUSES FOR SEARCH ==================== 65.058/65.058 65.058/65.058 formulas(mace4_clauses). 65.058/65.058 -->(x,y) | ->(a(x),a(y)) # label(congruence). 65.058/65.058 -->(x,y) | ->(f(x,z),f(y,z)) # label(congruence). 65.058/65.058 -->(x,y) | ->(f(z,x),f(z,y)) # label(congruence). 65.058/65.058 -->(x,y) | ->(c(x),c(y)) # label(congruence). 65.058/65.058 ->(a(x),f(x,x)) # label(replacement). 65.058/65.058 ->(a(x),b) # label(replacement). 65.058/65.058 -->*(c(f(c(x),c(c(y)))),c(a(a(b)))) | ->(f(c(c(c(x))),y),a(y)) # label(replacement). 65.058/65.058 -->*(c(f(x,y)),c(a(b))) | ->(f(c(x),c(c(y))),a(a(x))) # label(replacement). 65.058/65.058 ->*(x,x) # label(reflexivity). 65.058/65.058 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 65.058/65.058 -->*(c(f(c(x),c(c(y)))),c(a(a(b)))) # label(goal). 65.058/65.058 end_of_list. 65.058/65.058 65.058/65.058 ============================== end of clauses for search ============= 65.058/65.058 65.058/65.058 % There are no natural numbers in the input. 65.058/65.058 65.058/65.058 ============================== DOMAIN SIZE 2 ========================= 65.058/65.058 65.058/65.058 ============================== MODEL ================================= 65.058/65.058 65.058/65.058 interpretation( 2, [number=1, seconds=0], [ 65.058/65.058 65.058/65.058 function(b, [ 0 ]), 65.058/65.058 65.058/65.058 function(a(_), [ 0, 0 ]), 65.058/65.058 65.058/65.058 function(c(_), [ 0, 1 ]), 65.058/65.058 65.058/65.058 function(f(_,_), [ 65.058/65.058 1, 1, 65.058/65.058 1, 1 ]), 65.058/65.058 65.058/65.058 relation(->*(_,_), [ 65.058/65.058 1, 1, 65.058/65.058 0, 1 ]), 65.058/65.058 65.058/65.058 relation(->(_,_), [ 65.058/65.058 1, 1, 65.058/65.058 0, 1 ]) 65.058/65.058 ]). 65.058/65.058 65.058/65.058 ============================== end of model ========================== 65.058/65.058 65.058/65.058 ============================== STATISTICS ============================ 65.058/65.058 65.058/65.058 For domain size 2. 65.058/65.058 65.058/65.058 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 65.058/65.058 Ground clauses: seen=50, kept=46. 65.058/65.058 Selections=5, assignments=6, propagations=12, current_models=1. 65.058/65.058 Rewrite_terms=198, rewrite_bools=74, indexes=51. 65.058/65.058 Rules_from_neg_clauses=4, cross_offs=4. 65.058/65.058 65.058/65.058 ============================== end of statistics ===================== 65.058/65.058 65.058/65.058 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 65.058/65.058 65.058/65.058 Exiting with 1 model. 65.058/65.058 65.058/65.058 Process 56349 exit (max_models) Wed Jul 14 11:19:12 2021 65.058/65.058 The process finished Wed Jul 14 11:19:12 2021 65.058/65.058 65.058/65.058 65.058/65.058 Mace4 cooked interpretation: 65.058/65.058 65.058/65.058 65.058/65.058 65.058/65.058 The problem is infeasible. 65.058/65.058 65.058/65.058 65.058/65.058 CRule InfChecker Info: 65.058/65.058 f(c(x:S),c(c(y:S))) -> a(a(x:S)) | c(f(x:S,y:S)) ->* c(a(b)) 65.058/65.058 Rule deleted 65.058/65.058 Proof: 65.058/65.058 YES 65.058/65.058 65.058/65.058 Problem 1: 65.058/65.058 65.058/65.058 Infeasibility Problem: 65.058/65.058 [(VAR vNonEmpty:S x:S:S y:S:S) 65.058/65.058 (STRATEGY CONTEXTSENSITIVE 65.058/65.058 (a 1) 65.058/65.058 (f 1 2) 65.058/65.058 (b) 65.058/65.058 (c 1) 65.058/65.058 (fSNonEmpty) 65.058/65.058 ) 65.058/65.058 (RULES 65.058/65.058 a(x:S:S) -> f(x:S:S,x:S:S) 65.058/65.058 a(x:S:S) -> b 65.058/65.058 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)) 65.058/65.058 )] 65.058/65.058 65.058/65.058 Infeasibility Conditions: 65.058/65.058 c(f(x:S:S,y:S:S)) ->* c(a(b)) 65.058/65.058 65.058/65.058 Problem 1: 65.058/65.058 65.058/65.058 Obtaining a model using Mace4: 65.058/65.058 65.058/65.058 -> Usable Rules: 65.058/65.058 a(x:S:S) -> f(x:S:S,x:S:S) 65.058/65.058 a(x:S:S) -> b 65.058/65.058 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)) 65.058/65.058 65.058/65.058 -> Mace4 Output: 65.058/65.058 ============================== Mace4 ================================= 65.058/65.058 Mace4 (64) version 2009-11A, November 2009. 65.058/65.058 Process 56381 was started by ubuntu on ubuntu, 65.058/65.058 Wed Jul 14 11:19:33 2021 65.058/65.058 The command was "./mace4 -c -f /tmp/mace456368-2.in". 65.058/65.058 ============================== end of head =========================== 65.058/65.058 65.058/65.058 ============================== INPUT ================================= 65.058/65.058 65.058/65.058 % Reading from file /tmp/mace456368-2.in 65.058/65.058 65.058/65.058 assign(max_seconds,20). 65.058/65.058 65.058/65.058 formulas(assumptions). 65.058/65.058 ->(x1,y) -> ->(a(x1),a(y)) # label(congruence). 65.058/65.058 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence). 65.058/65.058 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence). 65.058/65.058 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence). 65.058/65.058 ->(a(x1),f(x1,x1)) # label(replacement). 65.058/65.058 ->(a(x1),b) # label(replacement). 65.058/65.058 ->*(c(f(x1,x2)),c(a(b))) -> ->(f(c(x1),c(c(x2))),a(a(x1))) # label(replacement). 65.058/65.058 ->*(x,x) # label(reflexivity). 65.058/65.058 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 65.058/65.058 end_of_list. 65.058/65.058 65.058/65.058 formulas(goals). 65.058/65.058 (exists x1 exists x2 ->*(c(f(x1,x2)),c(a(b)))) # label(goal). 65.058/65.058 end_of_list. 65.058/65.058 65.058/65.058 ============================== end of input ========================== 65.058/65.058 65.058/65.058 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 65.058/65.058 65.058/65.058 % Formulas that are not ordinary clauses: 65.058/65.058 1 ->(x1,y) -> ->(a(x1),a(y)) # label(congruence) # label(non_clause). [assumption]. 65.058/65.058 2 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 65.058/65.058 3 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 65.058/65.058 4 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence) # label(non_clause). [assumption]. 65.058/65.058 5 ->*(c(f(x1,x2)),c(a(b))) -> ->(f(c(x1),c(c(x2))),a(a(x1))) # label(replacement) # label(non_clause). [assumption]. 65.058/65.058 6 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 65.058/65.058 7 (exists x1 exists x2 ->*(c(f(x1,x2)),c(a(b)))) # label(goal) # label(non_clause) # label(goal). [goal]. 65.058/65.058 65.058/65.058 ============================== end of process non-clausal formulas === 65.058/65.058 65.058/65.058 ============================== CLAUSES FOR SEARCH ==================== 65.058/65.058 65.058/65.058 formulas(mace4_clauses). 65.058/65.058 -->(x,y) | ->(a(x),a(y)) # label(congruence). 65.058/65.058 -->(x,y) | ->(f(x,z),f(y,z)) # label(congruence). 65.058/65.058 -->(x,y) | ->(f(z,x),f(z,y)) # label(congruence). 65.058/65.058 -->(x,y) | ->(c(x),c(y)) # label(congruence). 65.058/65.058 ->(a(x),f(x,x)) # label(replacement). 65.058/65.058 ->(a(x),b) # label(replacement). 65.058/65.058 -->*(c(f(x,y)),c(a(b))) | ->(f(c(x),c(c(y))),a(a(x))) # label(replacement). 65.058/65.058 ->*(x,x) # label(reflexivity). 65.058/65.058 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 65.058/65.058 -->*(c(f(x,y)),c(a(b))) # label(goal). 65.058/65.058 end_of_list. 65.058/65.058 65.058/65.058 ============================== end of clauses for search ============= 65.058/65.058 65.058/65.058 % There are no natural numbers in the input. 65.058/65.058 65.058/65.058 ============================== DOMAIN SIZE 2 ========================= 65.058/65.058 65.058/65.058 ============================== MODEL ================================= 65.058/65.058 65.058/65.058 interpretation( 2, [number=1, seconds=0], [ 65.058/65.058 65.058/65.058 function(b, [ 0 ]), 65.058/65.058 65.058/65.058 function(a(_), [ 0, 0 ]), 65.058/65.058 65.058/65.058 function(c(_), [ 0, 1 ]), 65.058/65.058 65.058/65.058 function(f(_,_), [ 65.058/65.058 1, 1, 65.058/65.058 1, 1 ]), 65.058/65.058 65.058/65.058 relation(->*(_,_), [ 65.058/65.058 1, 1, 65.058/65.058 0, 1 ]), 65.058/65.058 65.058/65.058 relation(->(_,_), [ 65.058/65.058 1, 1, 65.058/65.058 0, 1 ]) 65.058/65.058 ]). 65.058/65.058 65.058/65.058 ============================== end of model ========================== 65.058/65.058 65.058/65.058 ============================== STATISTICS ============================ 65.058/65.058 65.058/65.058 For domain size 2. 65.058/65.058 65.058/65.058 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 65.058/65.058 Ground clauses: seen=46, kept=42. 65.058/65.058 Selections=5, assignments=6, propagations=12, current_models=1. 65.058/65.058 Rewrite_terms=123, rewrite_bools=68, indexes=29. 65.058/65.058 Rules_from_neg_clauses=4, cross_offs=4. 65.058/65.058 65.058/65.058 ============================== end of statistics ===================== 65.058/65.058 65.058/65.058 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 65.058/65.058 65.058/65.058 Exiting with 1 model. 65.058/65.058 65.058/65.058 Process 56381 exit (max_models) Wed Jul 14 11:19:33 2021 65.058/65.058 The process finished Wed Jul 14 11:19:33 2021 65.058/65.058 65.058/65.058 65.058/65.058 Mace4 cooked interpretation: 65.058/65.058 65.058/65.058 65.058/65.058 65.058/65.058 The problem is infeasible. 65.058/65.058 65.058/65.058 65.058/65.058 Problem 1: 65.058/65.058 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 65.058/65.058 Confluence Problem: 65.058/65.058 (VAR x:S) 65.058/65.058 (STRATEGY CONTEXTSENSITIVE 65.058/65.058 (a 1) 65.058/65.058 (f 1 2) 65.058/65.058 (b) 65.058/65.058 (c 1) 65.058/65.058 (fSNonEmpty) 65.058/65.058 ) 65.058/65.058 (RULES 65.058/65.058 a(x:S) -> f(x:S,x:S) 65.058/65.058 a(x:S) -> b 65.058/65.058 ) 65.058/65.058 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 65.058/65.058 65.058/65.058 Critical Pairs Processor: 65.058/65.058 -> Rules: 65.058/65.058 a(x:S) -> f(x:S,x:S) 65.058/65.058 a(x:S) -> b 65.058/65.058 -> Vars: 65.058/65.058 "x", "x" 65.058/65.058 -> FVars: 65.058/65.058 "x2", "x3" 65.058/65.058 -> PVars: 65.058/65.058 "x": ["x2", "x3"] 65.058/65.058 65.058/65.058 -> Rlps: 65.058/65.058 crule: a(x2:S) -> f(x2:S,x2:S), id: 1, possubterms: a(x2:S)-> [] 65.058/65.058 crule: a(x3:S) -> b, id: 2, possubterms: a(x3:S)-> [] 65.058/65.058 65.058/65.058 -> Unifications: 65.058/65.058 R2 unifies with R1 at p: [], l: a(x3:S), lp: a(x3:S), conds: {}, sig: {x3:S -> x:S}, l': a(x:S), r: b, r': f(x:S,x:S) 65.058/65.058 65.058/65.058 -> Critical pairs info: 65.058/65.058 => Not trivial, Overlay, N1 65.058/65.058 65.058/65.058 -> Problem conclusions: 65.058/65.058 Left linear, Not right linear, Not linear 65.058/65.058 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 65.058/65.058 CTRS Type: 1 65.058/65.058 Deterministic, Strongly deterministic 65.058/65.058 Oriented CTRS, Properly oriented CTRS, Join CTRS 65.058/65.058 Maybe right-stable CTRS, Overlay CTRS 65.058/65.058 Normal CTRS, Almost normal CTRS 65.058/65.058 Maybe terminating CTRS, Maybe joinable CCPs 65.058/65.058 Maybe level confluent 65.058/65.058 Maybe confluent 65.058/65.058 65.058/65.058 Problem 1: 65.058/65.058 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 65.058/65.058 Confluence Problem: 65.058/65.058 (VAR x:S) 65.058/65.058 (STRATEGY CONTEXTSENSITIVE 65.058/65.058 (a 1) 65.058/65.058 (f 1 2) 65.058/65.058 (b) 65.058/65.058 (c 1) 65.058/65.058 (fSNonEmpty) 65.058/65.058 ) 65.058/65.058 (RULES 65.058/65.058 a(x:S) -> f(x:S,x:S) 65.058/65.058 a(x:S) -> b 65.058/65.058 ) 65.058/65.058 Critical Pairs: 65.058/65.058 => Not trivial, Overlay, N1 65.058/65.058 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 65.058/65.058 65.058/65.058 Conditional Critical Pairs Distributor Processor 65.058/65.058 65.058/65.058 Problem 1: 65.058/65.058 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 65.058/65.058 Confluence Problem: 65.058/65.058 (VAR x:S) 65.058/65.058 (STRATEGY CONTEXTSENSITIVE 65.058/65.058 (a 1) 65.058/65.058 (f 1 2) 65.058/65.058 (b) 65.058/65.058 (c 1) 65.058/65.058 (fSNonEmpty) 65.058/65.058 ) 65.058/65.058 (RULES 65.058/65.058 a(x:S) -> f(x:S,x:S) 65.058/65.058 a(x:S) -> b 65.058/65.058 ) 65.058/65.058 Critical Pairs: 65.058/65.058 => Not trivial, Overlay, N1 65.058/65.058 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 65.058/65.058 65.058/65.058 Infeasible Convergence No Conditions CCP Processor: 65.058/65.058 Infeasible convergence? 65.058/65.058 YES 65.058/65.058 65.058/65.058 Problem 1: 65.058/65.058 65.058/65.058 Infeasibility Problem: 65.058/65.058 [(VAR vNonEmpty:S x:S z:S) 65.058/65.058 (STRATEGY CONTEXTSENSITIVE 65.058/65.058 (a 1) 65.058/65.058 (b) 65.058/65.058 (cx) 65.058/65.058 (f 1 2) 65.058/65.058 (fSNonEmpty) 65.058/65.058 ) 65.058/65.058 (RULES 65.058/65.058 a(x:S) -> b 65.058/65.058 a(x:S) -> f(x:S,x:S) 65.058/65.058 )] 65.058/65.058 Infeasibility Conditions: 65.058/65.058 f(cx,cx) ->* z:S, b ->* z:S 65.058/65.058 65.058/65.058 Problem 1: 65.058/65.058 65.058/65.058 Obtaining a model using Mace4: 65.058/65.058 65.058/65.058 -> Usable Rules: 65.058/65.058 Empty 65.058/65.058 65.058/65.058 -> Mace4 Output: 65.058/65.058 ============================== Mace4 ================================= 65.058/65.058 Mace4 (64) version 2009-11A, November 2009. 65.058/65.058 Process 56407 was started by ubuntu on ubuntu, 65.058/65.058 Wed Jul 14 11:19:53 2021 65.058/65.058 The command was "./mace4 -c -f /tmp/mace456394-2.in". 65.058/65.058 ============================== end of head =========================== 65.058/65.058 65.058/65.058 ============================== INPUT ================================= 65.058/65.058 65.058/65.058 % Reading from file /tmp/mace456394-2.in 65.058/65.058 65.058/65.058 assign(max_seconds,20). 65.058/65.058 65.058/65.058 formulas(assumptions). 65.058/65.058 ->(x1,y) -> ->(a(x1),a(y)) # label(congruence). 65.058/65.058 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence). 65.058/65.058 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence). 65.058/65.058 ->*(x,x) # label(reflexivity). 65.058/65.058 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 65.058/65.058 end_of_list. 65.058/65.058 65.058/65.058 formulas(goals). 65.058/65.058 (exists x2 (->*(f(cx,cx),x2) & ->*(b,x2))) # label(goal). 65.058/65.058 end_of_list. 65.058/65.058 65.058/65.058 ============================== end of input ========================== 65.058/65.058 65.058/65.058 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 65.058/65.058 65.058/65.058 % Formulas that are not ordinary clauses: 65.058/65.058 1 ->(x1,y) -> ->(a(x1),a(y)) # label(congruence) # label(non_clause). [assumption]. 65.058/65.058 2 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 65.058/65.058 3 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 65.058/65.058 4 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 65.058/65.058 5 (exists x2 (->*(f(cx,cx),x2) & ->*(b,x2))) # label(goal) # label(non_clause) # label(goal). [goal]. 65.058/65.058 65.058/65.058 ============================== end of process non-clausal formulas === 65.058/65.058 65.058/65.058 ============================== CLAUSES FOR SEARCH ==================== 65.058/65.058 65.058/65.058 formulas(mace4_clauses). 65.058/65.058 -->(x,y) | ->(a(x),a(y)) # label(congruence). 65.058/65.058 -->(x,y) | ->(f(x,z),f(y,z)) # label(congruence). 65.058/65.058 -->(x,y) | ->(f(z,x),f(z,y)) # label(congruence). 65.058/65.058 ->*(x,x) # label(reflexivity). 65.058/65.058 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 65.058/65.058 -->*(f(cx,cx),x) | -->*(b,x) # label(goal). 65.058/65.058 end_of_list. 65.058/65.058 65.058/65.058 ============================== end of clauses for search ============= 65.058/65.058 65.058/65.058 % There are no natural numbers in the input. 65.058/65.058 65.058/65.058 ============================== DOMAIN SIZE 2 ========================= 65.058/65.058 65.058/65.058 ============================== MODEL ================================= 65.058/65.058 65.058/65.058 interpretation( 2, [number=1, seconds=0], [ 65.058/65.058 65.058/65.058 function(b, [ 0 ]), 65.058/65.058 65.058/65.058 function(cx, [ 0 ]), 65.058/65.058 65.058/65.058 function(a(_), [ 0, 0 ]), 65.058/65.058 65.058/65.058 function(f(_,_), [ 65.058/65.058 1, 0, 65.058/65.058 0, 0 ]), 65.058/65.058 65.058/65.058 relation(->*(_,_), [ 65.058/65.058 1, 0, 65.058/65.058 0, 1 ]), 65.058/65.058 65.058/65.058 relation(->(_,_), [ 65.058/65.058 0, 0, 65.058/65.058 0, 0 ]) 65.058/65.058 ]). 65.058/65.058 65.058/65.058 ============================== end of model ========================== 65.058/65.058 65.058/65.058 ============================== STATISTICS ============================ 65.058/65.058 65.058/65.058 For domain size 2. 65.058/65.058 65.058/65.058 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 65.058/65.058 Ground clauses: seen=32, kept=28. 65.058/65.058 Selections=8, assignments=8, propagations=8, current_models=1. 65.058/65.058 Rewrite_terms=48, rewrite_bools=36, indexes=7. 65.058/65.058 Rules_from_neg_clauses=1, cross_offs=1. 65.058/65.058 65.058/65.058 ============================== end of statistics ===================== 65.058/65.058 65.058/65.058 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 65.058/65.058 65.058/65.058 Exiting with 1 model. 65.058/65.058 65.058/65.058 Process 56407 exit (max_models) Wed Jul 14 11:19:53 2021 65.058/65.058 The process finished Wed Jul 14 11:19:53 2021 65.058/65.058 65.058/65.058 65.058/65.058 Mace4 cooked interpretation: 65.058/65.058 65.058/65.058 65.058/65.058 65.058/65.058 The problem is infeasible. 65.058/65.058 65.058/65.058 65.058/65.058 The problem is not joinable. 65.058/65.058 78.85user 3.15system 1:05.58elapsed 125%CPU (0avgtext+0avgdata 115020maxresident)k 65.058/65.058 8inputs+0outputs (0major+156306minor)pagefaults 0swaps