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