40.039/40.039 YES 40.039/40.039 40.039/40.039 Problem 1: 40.039/40.039 40.039/40.039 40.039/40.039 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.039/40.039 Confluence Problem: 40.039/40.039 (VAR vNonEmpty x y z) 40.039/40.039 (REPLACEMENT-MAP 40.039/40.039 (f 1, 2) 40.039/40.039 (h 1) 40.039/40.039 (a 1) 40.039/40.039 (b) 40.039/40.039 (c 1) 40.039/40.039 (fSNonEmpty) 40.039/40.039 ) 40.039/40.039 (RULES 40.039/40.039 f(c(c(c(x))),y) -> a(y) | c(f(c(x),c(c(y)))) ->* c(a(a(b))) 40.039/40.039 f(c(x),c(c(y))) -> a(a(x)) | c(f(x,y)) ->* c(a(b)) 40.039/40.039 h(a(a(x))) -> a(b) | h(x) ->* b 40.039/40.039 h(b) -> b 40.039/40.039 ) 40.039/40.039 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.039/40.039 40.039/40.039 40.039/40.039 Problem 1: 40.039/40.039 40.039/40.039 Inlining of Conditions Processor [STERN17]: 40.039/40.039 40.039/40.039 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.039/40.039 Confluence Problem: 40.039/40.039 (VAR vNonEmpty x y z) 40.039/40.039 (REPLACEMENT-MAP 40.039/40.039 (f 1, 2) 40.039/40.039 (h 1) 40.039/40.039 (a 1) 40.039/40.039 (b) 40.039/40.039 (c 1) 40.039/40.039 (fSNonEmpty) 40.039/40.039 ) 40.039/40.039 (RULES 40.039/40.039 f(c(c(c(x))),y) -> a(y) | c(f(c(x),c(c(y)))) ->* c(a(a(b))) 40.039/40.039 f(c(x),c(c(y))) -> a(a(x)) | c(f(x,y)) ->* c(a(b)) 40.039/40.039 h(a(a(x))) -> a(b) | h(x) ->* b 40.039/40.039 h(b) -> b 40.039/40.039 ) 40.039/40.039 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.039/40.039 40.039/40.039 40.039/40.039 Problem 1: 40.039/40.039 40.039/40.039 Clean CTRS Processor: 40.039/40.039 40.039/40.039 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.039/40.039 Confluence Problem: 40.039/40.039 (VAR x) 40.039/40.039 (REPLACEMENT-MAP 40.039/40.039 (f 1, 2) 40.039/40.039 (h 1) 40.039/40.039 (a 1) 40.039/40.039 (b) 40.039/40.039 (c 1) 40.039/40.039 (fSNonEmpty) 40.039/40.039 ) 40.039/40.039 (RULES 40.039/40.039 h(a(a(x))) -> a(b) | h(x) ->* b 40.039/40.039 h(b) -> b 40.039/40.039 ) 40.039/40.039 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.039/40.039 40.039/40.039 CRule InfChecker Info: 40.039/40.039 f(c(c(c(x))),y) -> a(y) | c(f(c(x),c(c(y)))) ->* c(a(a(b))) 40.039/40.039 Rule deleted 40.039/40.039 Proof: 40.039/40.039 YES 40.039/40.039 40.039/40.039 Problem 1: 40.039/40.039 40.039/40.039 Infeasibility Problem: 40.039/40.039 [(VAR vNonEmpty x y z vNonEmpty x y) 40.039/40.039 (STRATEGY CONTEXTSENSITIVE 40.039/40.039 (f 1 2) 40.039/40.039 (h 1) 40.039/40.039 (a 1) 40.039/40.039 (b) 40.039/40.039 (c 1) 40.039/40.039 (fSNonEmpty) 40.039/40.039 ) 40.039/40.039 (RULES 40.039/40.039 f(c(c(c(x))),y) -> a(y) | c(f(c(x),c(c(y)))) ->* c(a(a(b))) 40.039/40.039 f(c(x),c(c(y))) -> a(a(x)) | c(f(x,y)) ->* c(a(b)) 40.039/40.039 h(a(a(x))) -> a(b) | h(x) ->* b 40.039/40.039 h(b) -> b 40.039/40.039 )] 40.039/40.039 40.039/40.039 Infeasibility Conditions: 40.039/40.039 c(f(c(x),c(c(y)))) ->* c(a(a(b))) 40.039/40.039 40.039/40.039 Problem 1: 40.039/40.039 40.039/40.039 Obtaining a model using Mace4: 40.039/40.039 40.039/40.039 -> Usable Rules: 40.039/40.039 f(c(c(c(x))),y) -> a(y) | c(f(c(x),c(c(y)))) ->* c(a(a(b))) 40.039/40.039 f(c(x),c(c(y))) -> a(a(x)) | c(f(x,y)) ->* c(a(b)) 40.039/40.039 h(a(a(x))) -> a(b) | h(x) ->* b 40.039/40.039 h(b) -> b 40.039/40.039 40.039/40.039 -> Mace4 Output: 40.039/40.039 ============================== Mace4 ================================= 40.039/40.039 Mace4 (64) version 2009-11A, November 2009. 40.039/40.039 Process 73416 was started by ubuntu on ubuntu, 40.039/40.039 Wed Mar 9 10:05:36 2022 40.039/40.039 The command was "./mace4 -c -f /tmp/mace473405-2.in". 40.039/40.039 ============================== end of head =========================== 40.039/40.039 40.039/40.039 ============================== INPUT ================================= 40.039/40.039 40.039/40.039 % Reading from file /tmp/mace473405-2.in 40.039/40.039 40.039/40.039 assign(max_seconds,20). 40.039/40.039 40.039/40.039 formulas(assumptions). 40.039/40.039 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence). 40.039/40.039 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence). 40.039/40.039 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence). 40.039/40.039 ->(x1,y) -> ->(a(x1),a(y)) # label(congruence). 40.039/40.039 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence). 40.039/40.039 ->*(c(f(c(x1),c(c(x2)))),c(a(a(b)))) -> ->(f(c(c(c(x1))),x2),a(x2)) # label(replacement). 40.039/40.039 ->*(c(f(x1,x2)),c(a(b))) -> ->(f(c(x1),c(c(x2))),a(a(x1))) # label(replacement). 40.039/40.039 ->*(h(x1),b) -> ->(h(a(a(x1))),a(b)) # label(replacement). 40.039/40.039 ->(h(b),b) # label(replacement). 40.039/40.039 ->*(x,x) # label(reflexivity). 40.039/40.039 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 40.039/40.039 end_of_list. 40.039/40.039 40.039/40.039 formulas(goals). 40.039/40.039 (exists x5 exists x6 ->*(c(f(c(x5),c(c(x6)))),c(a(a(b))))) # label(goal). 40.039/40.039 end_of_list. 40.039/40.039 40.039/40.039 ============================== end of input ========================== 40.039/40.039 40.039/40.039 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 40.039/40.039 40.039/40.039 % Formulas that are not ordinary clauses: 40.039/40.039 1 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 40.039/40.039 2 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 40.039/40.039 3 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 40.039/40.039 4 ->(x1,y) -> ->(a(x1),a(y)) # label(congruence) # label(non_clause). [assumption]. 40.039/40.039 5 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence) # label(non_clause). [assumption]. 40.039/40.039 6 ->*(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]. 40.039/40.039 7 ->*(c(f(x1,x2)),c(a(b))) -> ->(f(c(x1),c(c(x2))),a(a(x1))) # label(replacement) # label(non_clause). [assumption]. 40.039/40.039 8 ->*(h(x1),b) -> ->(h(a(a(x1))),a(b)) # label(replacement) # label(non_clause). [assumption]. 40.039/40.039 9 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 40.039/40.039 10 (exists x5 exists x6 ->*(c(f(c(x5),c(c(x6)))),c(a(a(b))))) # label(goal) # label(non_clause) # label(goal). [goal]. 40.039/40.039 40.039/40.039 ============================== end of process non-clausal formulas === 40.039/40.039 40.039/40.039 ============================== CLAUSES FOR SEARCH ==================== 40.039/40.039 40.039/40.039 formulas(mace4_clauses). 40.039/40.039 -->(x,y) | ->(f(x,z),f(y,z)) # label(congruence). 40.039/40.039 -->(x,y) | ->(f(z,x),f(z,y)) # label(congruence). 40.039/40.039 -->(x,y) | ->(h(x),h(y)) # label(congruence). 40.039/40.039 -->(x,y) | ->(a(x),a(y)) # label(congruence). 40.039/40.039 -->(x,y) | ->(c(x),c(y)) # label(congruence). 40.039/40.039 -->*(c(f(c(x),c(c(y)))),c(a(a(b)))) | ->(f(c(c(c(x))),y),a(y)) # label(replacement). 40.039/40.039 -->*(c(f(x,y)),c(a(b))) | ->(f(c(x),c(c(y))),a(a(x))) # label(replacement). 40.039/40.039 -->*(h(x),b) | ->(h(a(a(x))),a(b)) # label(replacement). 40.039/40.039 ->(h(b),b) # label(replacement). 40.039/40.039 ->*(x,x) # label(reflexivity). 40.039/40.039 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 40.039/40.039 -->*(c(f(c(x),c(c(y)))),c(a(a(b)))) # label(goal). 40.039/40.039 end_of_list. 40.039/40.039 40.039/40.039 ============================== end of clauses for search ============= 40.039/40.039 40.039/40.039 % There are no natural numbers in the input. 40.039/40.039 40.039/40.039 ============================== DOMAIN SIZE 2 ========================= 40.039/40.039 40.039/40.039 ============================== MODEL ================================= 40.039/40.039 40.039/40.039 interpretation( 2, [number=1, seconds=0], [ 40.039/40.039 40.039/40.039 function(b, [ 0 ]), 40.039/40.039 40.039/40.039 function(h(_), [ 0, 0 ]), 40.039/40.039 40.039/40.039 function(a(_), [ 0, 0 ]), 40.039/40.039 40.039/40.039 function(c(_), [ 0, 1 ]), 40.039/40.039 40.039/40.039 function(f(_,_), [ 40.039/40.039 1, 1, 40.039/40.039 1, 1 ]), 40.039/40.039 40.039/40.039 relation(->*(_,_), [ 40.039/40.039 1, 0, 40.039/40.039 0, 1 ]), 40.039/40.039 40.039/40.039 relation(->(_,_), [ 40.039/40.039 1, 0, 40.039/40.039 0, 1 ]) 40.039/40.039 ]). 40.039/40.039 40.039/40.039 ============================== end of model ========================== 40.039/40.039 40.039/40.039 ============================== STATISTICS ============================ 40.039/40.039 40.039/40.039 For domain size 2. 40.039/40.039 40.039/40.039 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 40.039/40.039 Ground clauses: seen=53, kept=49. 40.039/40.039 Selections=11, assignments=15, propagations=8, current_models=1. 40.039/40.039 Rewrite_terms=232, rewrite_bools=90, indexes=54. 40.039/40.039 Rules_from_neg_clauses=1, cross_offs=1. 40.039/40.039 40.039/40.039 ============================== end of statistics ===================== 40.039/40.039 40.039/40.039 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 40.039/40.039 40.039/40.039 Exiting with 1 model. 40.039/40.039 40.039/40.039 Process 73416 exit (max_models) Wed Mar 9 10:05:36 2022 40.039/40.039 The process finished Wed Mar 9 10:05:36 2022 40.039/40.039 40.039/40.039 40.039/40.039 Mace4 cooked interpretation: 40.039/40.039 40.039/40.039 40.039/40.039 40.039/40.039 The problem is infeasible. 40.039/40.039 40.039/40.039 40.039/40.039 CRule InfChecker Info: 40.039/40.039 f(c(x),c(c(y))) -> a(a(x)) | c(f(x,y)) ->* c(a(b)) 40.039/40.039 Rule deleted 40.039/40.039 Proof: 40.039/40.039 YES 40.039/40.039 40.039/40.039 Problem 1: 40.039/40.039 40.039/40.039 Infeasibility Problem: 40.039/40.039 [(VAR vNonEmpty x y vNonEmpty x y) 40.039/40.039 (STRATEGY CONTEXTSENSITIVE 40.039/40.039 (f 1 2) 40.039/40.039 (h 1) 40.039/40.039 (a 1) 40.039/40.039 (b) 40.039/40.039 (c 1) 40.039/40.039 (fSNonEmpty) 40.039/40.039 ) 40.039/40.039 (RULES 40.039/40.039 f(c(x),c(c(y))) -> a(a(x)) | c(f(x,y)) ->* c(a(b)) 40.039/40.039 h(a(a(x))) -> a(b) | h(x) ->* b 40.039/40.039 h(b) -> b 40.039/40.039 )] 40.039/40.039 40.039/40.039 Infeasibility Conditions: 40.039/40.039 c(f(x,y)) ->* c(a(b)) 40.039/40.039 40.039/40.039 Problem 1: 40.039/40.039 40.039/40.039 Obtaining a model using Mace4: 40.039/40.039 40.039/40.039 -> Usable Rules: 40.039/40.039 f(c(x),c(c(y))) -> a(a(x)) | c(f(x,y)) ->* c(a(b)) 40.039/40.039 h(a(a(x))) -> a(b) | h(x) ->* b 40.039/40.039 h(b) -> b 40.039/40.039 40.039/40.039 -> Mace4 Output: 40.039/40.039 ============================== Mace4 ================================= 40.039/40.039 Mace4 (64) version 2009-11A, November 2009. 40.039/40.039 Process 73451 was started by ubuntu on ubuntu, 40.039/40.039 Wed Mar 9 10:05:56 2022 40.039/40.039 The command was "./mace4 -c -f /tmp/mace473438-2.in". 40.039/40.039 ============================== end of head =========================== 40.039/40.039 40.039/40.039 ============================== INPUT ================================= 40.039/40.039 40.039/40.039 % Reading from file /tmp/mace473438-2.in 40.039/40.039 40.039/40.039 assign(max_seconds,20). 40.039/40.039 40.039/40.039 formulas(assumptions). 40.039/40.039 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence). 40.039/40.039 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence). 40.039/40.039 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence). 40.039/40.039 ->(x1,y) -> ->(a(x1),a(y)) # label(congruence). 40.039/40.039 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence). 40.039/40.039 ->*(c(f(x1,x2)),c(a(b))) -> ->(f(c(x1),c(c(x2))),a(a(x1))) # label(replacement). 40.039/40.039 ->*(h(x1),b) -> ->(h(a(a(x1))),a(b)) # label(replacement). 40.039/40.039 ->(h(b),b) # label(replacement). 40.039/40.039 ->*(x,x) # label(reflexivity). 40.039/40.039 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 40.039/40.039 end_of_list. 40.039/40.039 40.039/40.039 formulas(goals). 40.039/40.039 (exists x4 exists x5 ->*(c(f(x4,x5)),c(a(b)))) # label(goal). 40.039/40.039 end_of_list. 40.039/40.039 40.039/40.039 ============================== end of input ========================== 40.039/40.039 40.039/40.039 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 40.039/40.039 40.039/40.039 % Formulas that are not ordinary clauses: 40.039/40.039 1 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 40.039/40.039 2 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 40.039/40.039 3 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 40.039/40.039 4 ->(x1,y) -> ->(a(x1),a(y)) # label(congruence) # label(non_clause). [assumption]. 40.039/40.039 5 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence) # label(non_clause). [assumption]. 40.039/40.039 6 ->*(c(f(x1,x2)),c(a(b))) -> ->(f(c(x1),c(c(x2))),a(a(x1))) # label(replacement) # label(non_clause). [assumption]. 40.039/40.039 7 ->*(h(x1),b) -> ->(h(a(a(x1))),a(b)) # label(replacement) # label(non_clause). [assumption]. 40.039/40.039 8 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 40.039/40.039 9 (exists x4 exists x5 ->*(c(f(x4,x5)),c(a(b)))) # label(goal) # label(non_clause) # label(goal). [goal]. 40.039/40.039 40.039/40.039 ============================== end of process non-clausal formulas === 40.039/40.039 40.039/40.039 ============================== CLAUSES FOR SEARCH ==================== 40.039/40.039 40.039/40.039 formulas(mace4_clauses). 40.039/40.039 -->(x,y) | ->(f(x,z),f(y,z)) # label(congruence). 40.039/40.039 -->(x,y) | ->(f(z,x),f(z,y)) # label(congruence). 40.039/40.039 -->(x,y) | ->(h(x),h(y)) # label(congruence). 40.039/40.039 -->(x,y) | ->(a(x),a(y)) # label(congruence). 40.039/40.039 -->(x,y) | ->(c(x),c(y)) # label(congruence). 40.039/40.039 -->*(c(f(x,y)),c(a(b))) | ->(f(c(x),c(c(y))),a(a(x))) # label(replacement). 40.039/40.039 -->*(h(x),b) | ->(h(a(a(x))),a(b)) # label(replacement). 40.039/40.039 ->(h(b),b) # label(replacement). 40.039/40.039 ->*(x,x) # label(reflexivity). 40.039/40.039 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 40.039/40.039 -->*(c(f(x,y)),c(a(b))) # label(goal). 40.039/40.039 end_of_list. 40.039/40.039 40.039/40.039 ============================== end of clauses for search ============= 40.039/40.039 40.039/40.039 % There are no natural numbers in the input. 40.039/40.039 40.039/40.039 ============================== DOMAIN SIZE 2 ========================= 40.039/40.039 40.039/40.039 ============================== MODEL ================================= 40.039/40.039 40.039/40.039 interpretation( 2, [number=1, seconds=0], [ 40.039/40.039 40.039/40.039 function(b, [ 0 ]), 40.039/40.039 40.039/40.039 function(h(_), [ 0, 0 ]), 40.039/40.039 40.039/40.039 function(a(_), [ 0, 0 ]), 40.039/40.039 40.039/40.039 function(c(_), [ 0, 1 ]), 40.039/40.039 40.039/40.039 function(f(_,_), [ 40.039/40.039 1, 1, 40.039/40.039 1, 1 ]), 40.039/40.039 40.039/40.039 relation(->*(_,_), [ 40.039/40.039 1, 0, 40.039/40.039 0, 1 ]), 40.039/40.039 40.039/40.039 relation(->(_,_), [ 40.039/40.039 1, 0, 40.039/40.039 0, 1 ]) 40.039/40.039 ]). 40.039/40.039 40.039/40.039 ============================== end of model ========================== 40.039/40.039 40.039/40.039 ============================== STATISTICS ============================ 40.039/40.039 40.039/40.039 For domain size 2. 40.039/40.039 40.039/40.039 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 40.039/40.039 Ground clauses: seen=49, kept=45. 40.039/40.039 Selections=11, assignments=15, propagations=8, current_models=1. 40.039/40.039 Rewrite_terms=149, rewrite_bools=79, indexes=32. 40.039/40.039 Rules_from_neg_clauses=1, cross_offs=1. 40.039/40.039 40.039/40.039 ============================== end of statistics ===================== 40.039/40.039 40.039/40.039 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 40.039/40.039 40.039/40.039 Exiting with 1 model. 40.039/40.039 40.039/40.039 Process 73451 exit (max_models) Wed Mar 9 10:05:56 2022 40.039/40.039 The process finished Wed Mar 9 10:05:56 2022 40.039/40.039 40.039/40.039 40.039/40.039 Mace4 cooked interpretation: 40.039/40.039 40.039/40.039 40.039/40.039 40.039/40.039 The problem is infeasible. 40.039/40.039 40.039/40.039 40.039/40.039 CRule InfChecker Info: 40.039/40.039 h(a(a(x))) -> a(b) | h(x) ->* b 40.039/40.039 Rule remains 40.039/40.039 Proof: 40.039/40.039 NO 40.039/40.039 40.039/40.039 Problem 1: 40.039/40.039 40.039/40.039 Infeasibility Problem: 40.039/40.039 [(VAR vNonEmpty x vNonEmpty x) 40.039/40.039 (STRATEGY CONTEXTSENSITIVE 40.039/40.039 (h 1) 40.039/40.039 (a 1) 40.039/40.039 (b) 40.039/40.039 (fSNonEmpty) 40.039/40.039 ) 40.039/40.039 (RULES 40.039/40.039 h(a(a(x))) -> a(b) | h(x) ->* b 40.039/40.039 h(b) -> b 40.039/40.039 )] 40.039/40.039 40.039/40.039 Infeasibility Conditions: 40.039/40.039 h(x) ->* b 40.039/40.039 40.039/40.039 Problem 1: 40.039/40.039 40.039/40.039 Obtaining a proof using Prover9: 40.039/40.039 40.039/40.039 -> Prover9 Output: 40.039/40.039 ============================== Prover9 =============================== 40.039/40.039 Prover9 (64) version 2009-11A, November 2009. 40.039/40.039 Process 73476 was started by ubuntu on ubuntu, 40.039/40.039 Wed Mar 9 10:06:16 2022 40.039/40.039 The command was "./prover9 -f /tmp/prover973467-0.in". 40.039/40.039 ============================== end of head =========================== 40.039/40.039 40.039/40.039 ============================== INPUT ================================= 40.039/40.039 40.039/40.039 % Reading from file /tmp/prover973467-0.in 40.039/40.039 40.039/40.039 assign(max_seconds,20). 40.039/40.039 40.039/40.039 formulas(assumptions). 40.039/40.039 ->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence). 40.039/40.039 ->_s0(x1,y) -> ->_s0(a(x1),a(y)) # label(congruence). 40.039/40.039 ->*_s0(h(x1),b) -> ->_s0(h(a(a(x1))),a(b)) # label(replacement). 40.039/40.039 ->_s0(h(b),b) # label(replacement). 40.039/40.039 ->*_s0(x,x) # label(reflexivity). 40.039/40.039 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 40.039/40.039 end_of_list. 40.039/40.039 40.039/40.039 formulas(goals). 40.039/40.039 (exists x3 ->*_s0(h(x3),b)) # label(goal). 40.039/40.039 end_of_list. 40.039/40.039 40.039/40.039 ============================== end of input ========================== 40.039/40.039 40.039/40.039 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 40.039/40.039 40.039/40.039 % Formulas that are not ordinary clauses: 40.039/40.039 1 ->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 40.039/40.039 2 ->_s0(x1,y) -> ->_s0(a(x1),a(y)) # label(congruence) # label(non_clause). [assumption]. 40.039/40.039 3 ->*_s0(h(x1),b) -> ->_s0(h(a(a(x1))),a(b)) # label(replacement) # label(non_clause). [assumption]. 40.039/40.039 4 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 40.039/40.039 5 (exists x3 ->*_s0(h(x3),b)) # label(goal) # label(non_clause) # label(goal). [goal]. 40.039/40.039 40.039/40.039 ============================== end of process non-clausal formulas === 40.039/40.039 40.039/40.039 ============================== PROCESS INITIAL CLAUSES =============== 40.039/40.039 40.039/40.039 % Clauses before input processing: 40.039/40.039 40.039/40.039 formulas(usable). 40.039/40.039 end_of_list. 40.039/40.039 40.039/40.039 formulas(sos). 40.039/40.039 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(1)]. 40.039/40.039 -->_s0(x,y) | ->_s0(a(x),a(y)) # label(congruence). [clausify(2)]. 40.039/40.039 -->*_s0(h(x),b) | ->_s0(h(a(a(x))),a(b)) # label(replacement). [clausify(3)]. 40.039/40.039 ->_s0(h(b),b) # label(replacement). [assumption]. 40.039/40.039 ->*_s0(x,x) # label(reflexivity). [assumption]. 40.039/40.039 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(4)]. 40.039/40.039 -->*_s0(h(x),b) # label(goal). [deny(5)]. 40.039/40.039 end_of_list. 40.039/40.039 40.039/40.039 formulas(demodulators). 40.039/40.039 end_of_list. 40.039/40.039 40.039/40.039 ============================== PREDICATE ELIMINATION ================= 40.039/40.039 40.039/40.039 No predicates eliminated. 40.039/40.039 40.039/40.039 ============================== end predicate elimination ============= 40.039/40.039 40.039/40.039 Auto_denials: 40.039/40.039 % copying label goal to answer in negative clause 40.039/40.039 40.039/40.039 Term ordering decisions: 40.039/40.039 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 40.039/40.039 Function symbol precedence: function_order([ b, h, a ]). 40.039/40.039 After inverse_order: (no changes). 40.039/40.039 Unfolding symbols: (none). 40.039/40.039 40.039/40.039 Auto_inference settings: 40.039/40.039 % set(neg_binary_resolution). % (HNE depth_diff=-4) 40.039/40.039 % clear(ordered_res). % (HNE depth_diff=-4) 40.039/40.039 % set(ur_resolution). % (HNE depth_diff=-4) 40.039/40.039 % set(ur_resolution) -> set(pos_ur_resolution). 40.039/40.039 % set(ur_resolution) -> set(neg_ur_resolution). 40.039/40.039 40.039/40.039 Auto_process settings: (no changes). 40.039/40.039 40.039/40.039 kept: 6 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(1)]. 40.039/40.039 kept: 7 -->_s0(x,y) | ->_s0(a(x),a(y)) # label(congruence). [clausify(2)]. 40.039/40.039 kept: 8 -->*_s0(h(x),b) | ->_s0(h(a(a(x))),a(b)) # label(replacement). [clausify(3)]. 40.039/40.039 kept: 9 ->_s0(h(b),b) # label(replacement). [assumption]. 40.039/40.039 kept: 10 ->*_s0(x,x) # label(reflexivity). [assumption]. 40.039/40.039 kept: 11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(4)]. 40.039/40.039 kept: 12 -->*_s0(h(x),b) # label(goal) # answer(goal). [deny(5)]. 40.039/40.039 40.039/40.039 ============================== end of process initial clauses ======== 40.039/40.039 40.039/40.039 ============================== CLAUSES FOR SEARCH ==================== 40.039/40.039 40.039/40.039 % Clauses after input processing: 40.039/40.039 40.039/40.039 formulas(usable). 40.039/40.039 end_of_list. 40.039/40.039 40.039/40.039 formulas(sos). 40.039/40.039 6 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(1)]. 40.039/40.039 7 -->_s0(x,y) | ->_s0(a(x),a(y)) # label(congruence). [clausify(2)]. 40.039/40.039 9 ->_s0(h(b),b) # label(replacement). [assumption]. 40.039/40.039 10 ->*_s0(x,x) # label(reflexivity). [assumption]. 40.039/40.039 11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(4)]. 40.039/40.039 12 -->*_s0(h(x),b) # label(goal) # answer(goal). [deny(5)]. 40.039/40.039 end_of_list. 40.039/40.039 40.039/40.039 formulas(demodulators). 40.039/40.039 end_of_list. 40.039/40.039 40.039/40.039 ============================== end of clauses for search ============= 40.039/40.039 40.039/40.039 ============================== SEARCH ================================ 40.039/40.039 40.039/40.039 % Starting search at 0.00 seconds. 40.039/40.039 40.039/40.039 given #1 (I,wt=8): 6 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(1)]. 40.039/40.039 40.039/40.039 given #2 (I,wt=8): 7 -->_s0(x,y) | ->_s0(a(x),a(y)) # label(congruence). [clausify(2)]. 40.039/40.039 40.039/40.039 given #3 (I,wt=4): 9 ->_s0(h(b),b) # label(replacement). [assumption]. 40.039/40.039 40.039/40.039 given #4 (I,wt=3): 10 ->*_s0(x,x) # label(reflexivity). [assumption]. 40.039/40.039 40.039/40.039 given #5 (I,wt=9): 11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(4)]. 40.039/40.039 40.039/40.039 ============================== PROOF ================================= 40.039/40.039 40.039/40.039 % Proof 1 at 0.00 (+ 0.00) seconds: goal. 40.039/40.039 % Length of proof is 8. 40.039/40.039 % Level of proof is 3. 40.039/40.039 % Maximum clause weight is 9.000. 40.039/40.039 % Given clauses 5. 40.039/40.039 40.039/40.039 4 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 40.039/40.039 5 (exists x3 ->*_s0(h(x3),b)) # label(goal) # label(non_clause) # label(goal). [goal]. 40.039/40.039 9 ->_s0(h(b),b) # label(replacement). [assumption]. 40.039/40.039 10 ->*_s0(x,x) # label(reflexivity). [assumption]. 40.039/40.039 11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(4)]. 40.039/40.039 12 -->*_s0(h(x),b) # label(goal) # answer(goal). [deny(5)]. 40.039/40.039 15 ->*_s0(h(b),b). [ur(11,a,9,a,b,10,a)]. 40.039/40.039 16 $F # answer(goal). [resolve(15,a,12,a)]. 40.039/40.039 40.039/40.039 ============================== end of proof ========================== 40.039/40.039 40.039/40.039 ============================== STATISTICS ============================ 40.039/40.039 40.039/40.039 Given=5. Generated=10. Kept=10. proofs=1. 40.039/40.039 Usable=5. Sos=3. Demods=0. Limbo=0, Disabled=8. Hints=0. 40.039/40.039 Kept_by_rule=0, Deleted_by_rule=0. 40.039/40.039 Forward_subsumed=0. Back_subsumed=1. 40.039/40.039 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 40.039/40.039 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 40.039/40.039 Demod_attempts=0. Demod_rewrites=0. 40.039/40.039 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 40.039/40.039 Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=6. 40.039/40.039 Megabytes=0.05. 40.039/40.039 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 40.039/40.039 40.039/40.039 ============================== end of statistics ===================== 40.039/40.039 40.039/40.039 ============================== end of search ========================= 40.039/40.039 40.039/40.039 THEOREM PROVED 40.039/40.039 40.039/40.039 Exiting with 1 proof. 40.039/40.039 40.039/40.039 Process 73476 exit (max_proofs) Wed Mar 9 10:06:16 2022 40.039/40.039 40.039/40.039 40.039/40.039 The problem is feasible. 40.039/40.039 40.039/40.039 40.039/40.039 CRule InfChecker Info: 40.039/40.039 h(b) -> b 40.039/40.039 Rule remains 40.039/40.039 Proof: 40.039/40.039 NO_CONDS 40.039/40.039 40.039/40.039 Problem 1: 40.039/40.039 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.039/40.039 Confluence Problem: 40.039/40.039 (VAR x) 40.039/40.039 (REPLACEMENT-MAP 40.039/40.039 (f 1, 2) 40.039/40.039 (h 1) 40.039/40.039 (a 1) 40.039/40.039 (b) 40.039/40.039 (c 1) 40.039/40.039 (fSNonEmpty) 40.039/40.039 ) 40.039/40.039 (RULES 40.039/40.039 h(a(a(x))) -> a(b) | h(x) ->* b 40.039/40.039 h(b) -> b 40.039/40.039 ) 40.039/40.039 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.039/40.039 40.039/40.039 Critical Pairs Processor: 40.039/40.039 -> Rules: 40.039/40.039 h(a(a(x))) -> a(b) | h(x) ->* b 40.039/40.039 h(b) -> b 40.039/40.039 -> Vars: 40.039/40.039 "x" 40.039/40.039 40.039/40.039 -> Rlps: 40.039/40.039 crule: h(a(a(x))) -> a(b) | h(x) ->* b, id: 1, possubterms: h(a(a(x)))-> [], a(a(x))-> [1], a(x)-> [1,1] 40.039/40.039 crule: h(b) -> b, id: 2, possubterms: h(b)-> [], b-> [1] 40.039/40.039 40.039/40.039 -> Unifications: 40.039/40.039 40.039/40.039 40.039/40.039 -> Critical pairs info: 40.039/40.039 40.039/40.039 40.039/40.039 -> Problem conclusions: 40.039/40.039 Left linear, Right linear, Linear 40.039/40.039 Weakly orthogonal, Almost orthogonal, Orthogonal 40.039/40.039 CTRS Type: 1 40.039/40.039 Deterministic, Strongly deterministic 40.039/40.039 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 40.039/40.039 Maybe right-stable CTRS, Overlay CTRS 40.039/40.039 Maybe normal CTRS, Maybe almost normal CTRS 40.039/40.039 Maybe terminating CTRS, Maybe operational terminating CTRS, Joinable CCPs 40.039/40.039 Maybe level confluent 40.039/40.039 Maybe confluent 40.039/40.039 40.039/40.039 Problem 1: 40.039/40.039 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.039/40.039 Confluence Problem: 40.039/40.039 (VAR x) 40.039/40.039 (REPLACEMENT-MAP 40.039/40.039 (f 1, 2) 40.039/40.039 (h 1) 40.039/40.039 (a 1) 40.039/40.039 (b) 40.039/40.039 (c 1) 40.039/40.039 (fSNonEmpty) 40.039/40.039 ) 40.039/40.039 (RULES 40.039/40.039 h(a(a(x))) -> a(b) | h(x) ->* b 40.039/40.039 h(b) -> b 40.039/40.039 ) 40.039/40.039 Critical Pairs: 40.039/40.039 40.039/40.039 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.039/40.039 40.039/40.039 Right Stable Processor: 40.039/40.039 Right-stable CTRS 40.039/40.039 Justification: 40.039/40.039 40.039/40.039 -> Term right-stability conditions: 40.039/40.039 Term: b 40.039/40.039 Right-stable term 40.039/40.039 Linear constructor form 40.039/40.039 Don't know if term is a ground normal form (not needed) 40.039/40.039 Right-stability condition achieved 40.039/40.039 A call to InfChecker wasn't needed 40.039/40.039 40.039/40.039 -> Problem conclusions: 40.039/40.039 Left linear, Right linear, Linear 40.039/40.039 Weakly orthogonal, Almost orthogonal, Orthogonal 40.039/40.039 CTRS Type: 1 40.039/40.039 Deterministic, Strongly deterministic 40.039/40.039 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 40.039/40.039 Right-stable CTRS, Overlay CTRS 40.039/40.039 Maybe normal CTRS, Almost normal CTRS 40.039/40.039 Maybe terminating CTRS, Maybe operational terminating CTRS, Joinable CCPs 40.039/40.039 Level confluent 40.039/40.039 Confluent 40.039/40.039 40.039/40.039 The problem is joinable. 40.039/40.039 56.31user 1.44system 0:40.39elapsed 142%CPU (0avgtext+0avgdata 169132maxresident)k 40.039/40.039 8inputs+0outputs (0major+105077minor)pagefaults 0swaps