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