42.017/42.017 YES 42.017/42.017 42.017/42.017 Problem 1: 42.017/42.017 42.017/42.017 42.017/42.017 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 42.017/42.017 Confluence Problem: 42.017/42.017 (VAR vNonEmpty x y) 42.017/42.017 (REPLACEMENT-MAP 42.017/42.017 (f 1, 2) 42.017/42.017 (fSNonEmpty) 42.017/42.017 (g 1) 42.017/42.017 (s 1) 42.017/42.017 ) 42.017/42.017 (RULES 42.017/42.017 f(x,y) -> x | g(x) ->*<- y, g(g(x)) ->*<- s(y) 42.017/42.017 f(x,y) -> y | g(y) ->*<- s(x), g(g(y)) ->*<- x 42.017/42.017 ) 42.017/42.017 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 42.017/42.017 42.017/42.017 42.017/42.017 Problem 1: 42.017/42.017 42.017/42.017 Inlining of Conditions Processor [STERN17]: 42.017/42.017 42.017/42.017 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 42.017/42.017 Confluence Problem: 42.017/42.017 (VAR vNonEmpty x y) 42.017/42.017 (REPLACEMENT-MAP 42.017/42.017 (f 1, 2) 42.017/42.017 (fSNonEmpty) 42.017/42.017 (g 1) 42.017/42.017 (s 1) 42.017/42.017 ) 42.017/42.017 (RULES 42.017/42.017 f(x,y) -> x | g(x) ->*<- y, g(g(x)) ->*<- s(y) 42.017/42.017 f(x,y) -> y | g(y) ->*<- s(x), g(g(y)) ->*<- x 42.017/42.017 ) 42.017/42.017 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 42.017/42.017 42.017/42.017 42.017/42.017 Problem 1: 42.017/42.017 42.017/42.017 Clean CTRS Processor: 42.017/42.017 42.017/42.017 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 42.017/42.017 Confluence Problem: 42.017/42.017 (REPLACEMENT-MAP 42.017/42.017 (f 1, 2) 42.017/42.017 (fSNonEmpty) 42.017/42.017 (g 1) 42.017/42.017 (s 1) 42.017/42.017 ) 42.017/42.017 (RULES 42.017/42.017 ) 42.017/42.017 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 42.017/42.017 42.017/42.017 CRule InfChecker Info: 42.017/42.017 f(x,y) -> x | g(x) ->*<- y, g(g(x)) ->*<- s(y) 42.017/42.017 Rule deleted 42.017/42.017 Proof: 42.017/42.017 YES 42.017/42.017 42.017/42.017 Problem 1: 42.017/42.017 42.017/42.017 Infeasibility Problem: 42.017/42.017 [(VAR vNonEmpty x y vNonEmpty x y) 42.017/42.017 (STRATEGY CONTEXTSENSITIVE 42.017/42.017 (f 1 2) 42.017/42.017 (fSNonEmpty) 42.017/42.017 (g 1) 42.017/42.017 (s 1) 42.017/42.017 ) 42.017/42.017 (RULES 42.017/42.017 f(x,y) -> x | g(x) ->*<- y, g(g(x)) ->*<- s(y) 42.017/42.017 f(x,y) -> y | g(y) ->*<- s(x), g(g(y)) ->*<- x 42.017/42.017 )] 42.017/42.017 42.017/42.017 Infeasibility Conditions: 42.017/42.017 g(x) ->*<- y, g(g(x)) ->*<- s(y) 42.017/42.017 42.017/42.017 Problem 1: 42.017/42.017 42.017/42.017 Obtaining a model using Mace4: 42.017/42.017 42.017/42.017 -> Usable Rules: 42.017/42.017 f(x,y) -> x | g(x) ->*<- y, g(g(x)) ->*<- s(y) 42.017/42.017 f(x,y) -> y | g(y) ->*<- s(x), g(g(y)) ->*<- x 42.017/42.017 42.017/42.017 -> Mace4 Output: 42.017/42.017 ============================== Mace4 ================================= 42.017/42.017 Mace4 (64) version 2009-11A, November 2009. 42.017/42.017 Process 85282 was started by ubuntu on ubuntu, 42.017/42.017 Wed Mar 9 10:46:12 2022 42.017/42.017 The command was "./mace4 -c -f /tmp/mace485269-2.in". 42.017/42.017 ============================== end of head =========================== 42.017/42.017 42.017/42.017 ============================== INPUT ================================= 42.017/42.017 42.017/42.017 % Reading from file /tmp/mace485269-2.in 42.017/42.017 42.017/42.017 assign(max_seconds,20). 42.017/42.017 42.017/42.017 formulas(assumptions). 42.017/42.017 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence). 42.017/42.017 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence). 42.017/42.017 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence). 42.017/42.017 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence). 42.017/42.017 ->*<-(g(x1),x2) & ->*<-(g(g(x1)),s(x2)) -> ->(f(x1,x2),x1) # label(replacement). 42.017/42.017 ->*<-(g(x2),s(x1)) & ->*<-(g(g(x2)),x1) -> ->(f(x1,x2),x2) # label(replacement). 42.017/42.017 ->*(x,x) # label(reflexivity). 42.017/42.017 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 42.017/42.017 ->*(x,y) & ->*(z,y) -> ->*<-(x,z) # label(joinability). 42.017/42.017 end_of_list. 42.017/42.017 42.017/42.017 formulas(goals). 42.017/42.017 (exists x4 exists x5 (->*<-(g(x4),x5) & ->*<-(g(g(x4)),s(x5)))) # label(goal). 42.017/42.017 end_of_list. 42.017/42.017 42.017/42.017 ============================== end of input ========================== 42.017/42.017 42.017/42.017 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 42.017/42.017 42.017/42.017 % Formulas that are not ordinary clauses: 42.017/42.017 1 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 42.017/42.017 2 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 42.017/42.017 3 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 42.017/42.017 4 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 42.017/42.017 5 ->*<-(g(x1),x2) & ->*<-(g(g(x1)),s(x2)) -> ->(f(x1,x2),x1) # label(replacement) # label(non_clause). [assumption]. 42.017/42.017 6 ->*<-(g(x2),s(x1)) & ->*<-(g(g(x2)),x1) -> ->(f(x1,x2),x2) # label(replacement) # label(non_clause). [assumption]. 42.017/42.017 7 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 42.017/42.017 8 ->*(x,y) & ->*(z,y) -> ->*<-(x,z) # label(joinability) # label(non_clause). [assumption]. 42.017/42.017 9 (exists x4 exists x5 (->*<-(g(x4),x5) & ->*<-(g(g(x4)),s(x5)))) # label(goal) # label(non_clause) # label(goal). [goal]. 42.017/42.017 42.017/42.017 ============================== end of process non-clausal formulas === 42.017/42.017 42.017/42.017 ============================== CLAUSES FOR SEARCH ==================== 42.017/42.017 42.017/42.017 formulas(mace4_clauses). 42.017/42.017 -->(x,y) | ->(f(x,z),f(y,z)) # label(congruence). 42.017/42.017 -->(x,y) | ->(f(z,x),f(z,y)) # label(congruence). 42.017/42.017 -->(x,y) | ->(g(x),g(y)) # label(congruence). 42.017/42.017 -->(x,y) | ->(s(x),s(y)) # label(congruence). 42.017/42.017 -->*<-(g(x),y) | -->*<-(g(g(x)),s(y)) | ->(f(x,y),x) # label(replacement). 42.017/42.017 -->*<-(g(x),s(y)) | -->*<-(g(g(x)),y) | ->(f(y,x),x) # label(replacement). 42.017/42.017 ->*(x,x) # label(reflexivity). 42.017/42.017 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 42.017/42.017 -->*(x,y) | -->*(z,y) | ->*<-(x,z) # label(joinability). 42.017/42.017 -->*<-(g(x),y) | -->*<-(g(g(x)),s(y)) # label(goal). 42.017/42.017 end_of_list. 42.017/42.017 42.017/42.017 ============================== end of clauses for search ============= 42.017/42.017 42.017/42.017 % There are no natural numbers in the input. 42.017/42.017 42.017/42.017 ============================== DOMAIN SIZE 2 ========================= 42.017/42.017 42.017/42.017 ============================== MODEL ================================= 42.017/42.017 42.017/42.017 interpretation( 2, [number=1, seconds=0], [ 42.017/42.017 42.017/42.017 function(g(_), [ 0, 0 ]), 42.017/42.017 42.017/42.017 function(s(_), [ 1, 0 ]), 42.017/42.017 42.017/42.017 function(f(_,_), [ 42.017/42.017 0, 0, 42.017/42.017 0, 0 ]), 42.017/42.017 42.017/42.017 relation(->*(_,_), [ 42.017/42.017 1, 0, 42.017/42.017 0, 1 ]), 42.017/42.017 42.017/42.017 relation(->(_,_), [ 42.017/42.017 0, 0, 42.017/42.017 0, 0 ]), 42.017/42.017 42.017/42.017 relation(->*<-(_,_), [ 42.017/42.017 1, 0, 42.017/42.017 0, 1 ]) 42.017/42.017 ]). 42.017/42.017 42.017/42.017 ============================== end of model ========================== 42.017/42.017 42.017/42.017 ============================== STATISTICS ============================ 42.017/42.017 42.017/42.017 For domain size 2. 42.017/42.017 42.017/42.017 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 42.017/42.017 Ground clauses: seen=54, kept=49. 42.017/42.017 Selections=9, assignments=9, propagations=11, current_models=1. 42.017/42.017 Rewrite_terms=104, rewrite_bools=63, indexes=10. 42.017/42.017 Rules_from_neg_clauses=1, cross_offs=1. 42.017/42.017 42.017/42.017 ============================== end of statistics ===================== 42.017/42.017 42.017/42.017 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 42.017/42.017 42.017/42.017 Exiting with 1 model. 42.017/42.017 42.017/42.017 Process 85282 exit (max_models) Wed Mar 9 10:46:12 2022 42.017/42.017 The process finished Wed Mar 9 10:46:12 2022 42.017/42.017 42.017/42.017 42.017/42.017 Mace4 cooked interpretation: 42.017/42.017 42.017/42.017 42.017/42.017 42.017/42.017 The problem is infeasible. 42.017/42.017 42.017/42.017 42.017/42.017 CRule InfChecker Info: 42.017/42.017 f(x,y) -> y | g(y) ->*<- s(x), g(g(y)) ->*<- x 42.017/42.017 Rule deleted 42.017/42.017 Proof: 42.017/42.017 YES 42.017/42.017 42.017/42.017 Problem 1: 42.017/42.017 42.017/42.017 Infeasibility Problem: 42.017/42.017 [(VAR vNonEmpty x y vNonEmpty x y) 42.017/42.017 (STRATEGY CONTEXTSENSITIVE 42.017/42.017 (f 1 2) 42.017/42.017 (fSNonEmpty) 42.017/42.017 (g 1) 42.017/42.017 (s 1) 42.017/42.017 ) 42.017/42.017 (RULES 42.017/42.017 f(x,y) -> y | g(y) ->*<- s(x), g(g(y)) ->*<- x 42.017/42.017 )] 42.017/42.017 42.017/42.017 Infeasibility Conditions: 42.017/42.017 g(y) ->*<- s(x), g(g(y)) ->*<- x 42.017/42.017 42.017/42.017 Problem 1: 42.017/42.017 42.017/42.017 Obtaining a model using Mace4: 42.017/42.017 42.017/42.017 -> Usable Rules: 42.017/42.017 f(x,y) -> y | g(y) ->*<- s(x), g(g(y)) ->*<- x 42.017/42.017 42.017/42.017 -> Mace4 Output: 42.017/42.017 ============================== Mace4 ================================= 42.017/42.017 Mace4 (64) version 2009-11A, November 2009. 42.017/42.017 Process 85312 was started by ubuntu on ubuntu, 42.017/42.017 Wed Mar 9 10:46:33 2022 42.017/42.017 The command was "./mace4 -c -f /tmp/mace485299-2.in". 42.017/42.017 ============================== end of head =========================== 42.017/42.017 42.017/42.017 ============================== INPUT ================================= 42.017/42.017 42.017/42.017 % Reading from file /tmp/mace485299-2.in 42.017/42.017 42.017/42.017 assign(max_seconds,20). 42.017/42.017 42.017/42.017 formulas(assumptions). 42.017/42.017 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence). 42.017/42.017 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence). 42.017/42.017 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence). 42.017/42.017 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence). 42.017/42.017 ->*<-(g(x2),s(x1)) & ->*<-(g(g(x2)),x1) -> ->(f(x1,x2),x2) # label(replacement). 42.017/42.017 ->*(x,x) # label(reflexivity). 42.017/42.017 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 42.017/42.017 ->*(x,y) & ->*(z,y) -> ->*<-(x,z) # label(joinability). 42.017/42.017 end_of_list. 42.017/42.017 42.017/42.017 formulas(goals). 42.017/42.017 (exists x4 exists x5 (->*<-(g(x5),s(x4)) & ->*<-(g(g(x5)),x4))) # label(goal). 42.017/42.017 end_of_list. 42.017/42.017 42.017/42.017 ============================== end of input ========================== 42.017/42.017 42.017/42.017 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 42.017/42.017 42.017/42.017 % Formulas that are not ordinary clauses: 42.017/42.017 1 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 42.017/42.017 2 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 42.017/42.017 3 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 42.017/42.017 4 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 42.017/42.017 5 ->*<-(g(x2),s(x1)) & ->*<-(g(g(x2)),x1) -> ->(f(x1,x2),x2) # label(replacement) # label(non_clause). [assumption]. 42.017/42.017 6 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 42.017/42.017 7 ->*(x,y) & ->*(z,y) -> ->*<-(x,z) # label(joinability) # label(non_clause). [assumption]. 42.017/42.017 8 (exists x4 exists x5 (->*<-(g(x5),s(x4)) & ->*<-(g(g(x5)),x4))) # label(goal) # label(non_clause) # label(goal). [goal]. 42.017/42.017 42.017/42.017 ============================== end of process non-clausal formulas === 42.017/42.017 42.017/42.017 ============================== CLAUSES FOR SEARCH ==================== 42.017/42.017 42.017/42.017 formulas(mace4_clauses). 42.017/42.017 -->(x,y) | ->(f(x,z),f(y,z)) # label(congruence). 42.017/42.017 -->(x,y) | ->(f(z,x),f(z,y)) # label(congruence). 42.017/42.017 -->(x,y) | ->(g(x),g(y)) # label(congruence). 42.017/42.017 -->(x,y) | ->(s(x),s(y)) # label(congruence). 42.017/42.017 -->*<-(g(x),s(y)) | -->*<-(g(g(x)),y) | ->(f(y,x),x) # label(replacement). 42.017/42.017 ->*(x,x) # label(reflexivity). 42.017/42.017 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 42.017/42.017 -->*(x,y) | -->*(z,y) | ->*<-(x,z) # label(joinability). 42.017/42.017 -->*<-(g(x),s(y)) | -->*<-(g(g(x)),y) # label(goal). 42.017/42.017 end_of_list. 42.017/42.017 42.017/42.017 ============================== end of clauses for search ============= 42.017/42.017 42.017/42.017 % There are no natural numbers in the input. 42.017/42.017 42.017/42.017 ============================== DOMAIN SIZE 2 ========================= 42.017/42.017 42.017/42.017 ============================== MODEL ================================= 42.017/42.017 42.017/42.017 interpretation( 2, [number=1, seconds=0], [ 42.017/42.017 42.017/42.017 function(g(_), [ 0, 0 ]), 42.017/42.017 42.017/42.017 function(s(_), [ 1, 0 ]), 42.017/42.017 42.017/42.017 function(f(_,_), [ 42.017/42.017 0, 0, 42.017/42.017 0, 0 ]), 42.017/42.017 42.017/42.017 relation(->*(_,_), [ 42.017/42.017 1, 0, 42.017/42.017 0, 1 ]), 42.017/42.017 42.017/42.017 relation(->(_,_), [ 42.017/42.017 0, 0, 42.017/42.017 0, 0 ]), 42.017/42.017 42.017/42.017 relation(->*<-(_,_), [ 42.017/42.017 1, 0, 42.017/42.017 0, 1 ]) 42.017/42.017 ]). 42.017/42.017 42.017/42.017 ============================== end of model ========================== 42.017/42.017 42.017/42.017 ============================== STATISTICS ============================ 42.017/42.017 42.017/42.017 For domain size 2. 42.017/42.017 42.017/42.017 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 42.017/42.017 Ground clauses: seen=50, kept=45. 42.017/42.017 Selections=9, assignments=9, propagations=11, current_models=1. 42.017/42.017 Rewrite_terms=84, rewrite_bools=59, indexes=8. 42.017/42.017 Rules_from_neg_clauses=1, cross_offs=1. 42.017/42.017 42.017/42.017 ============================== end of statistics ===================== 42.017/42.017 42.017/42.017 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 42.017/42.017 42.017/42.017 Exiting with 1 model. 42.017/42.017 42.017/42.017 Process 85312 exit (max_models) Wed Mar 9 10:46:33 2022 42.017/42.017 The process finished Wed Mar 9 10:46:33 2022 42.017/42.017 42.017/42.017 42.017/42.017 Mace4 cooked interpretation: 42.017/42.017 42.017/42.017 42.017/42.017 42.017/42.017 The problem is infeasible. 42.017/42.017 42.017/42.017 42.017/42.017 Problem 1: 42.017/42.017 42.017/42.017 Transform No Conds CTRS Processor: 42.017/42.017 42.017/42.017 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 42.017/42.017 Confluence Problem: 42.017/42.017 (REPLACEMENT-MAP 42.017/42.017 (f 1, 2) 42.017/42.017 (fSNonEmpty) 42.017/42.017 (g 1) 42.017/42.017 (s 1) 42.017/42.017 ) 42.017/42.017 (RULES 42.017/42.017 ) 42.017/42.017 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 42.017/42.017 Resulting R: 42.017/42.017 (STRATEGY CONTEXTSENSITIVE 42.017/42.017 (f 1 2) 42.017/42.017 (fSNonEmpty) 42.017/42.017 (g 1) 42.017/42.017 (s 1) 42.017/42.017 ) 42.017/42.017 (RULES 42.017/42.017 ) 42.017/42.017 42.017/42.017 Problem 1: 42.017/42.017 42.017/42.017 CleanTRS Processor: 42.017/42.017 42.017/42.017 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 42.017/42.017 Confluence Problem: 42.017/42.017 (REPLACEMENT-MAP 42.017/42.017 (f 1, 2) 42.017/42.017 (fSNonEmpty) 42.017/42.017 (g 1) 42.017/42.017 (s 1) 42.017/42.017 ) 42.017/42.017 (RULES 42.017/42.017 ) 42.017/42.017 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 42.017/42.017 42.017/42.017 42.017/42.017 Problem 1: 42.017/42.017 42.017/42.017 Modular Confluence Combinations Decomposition Processor: 42.017/42.017 42.017/42.017 No usable combinations 42.017/42.017 42.017/42.017 Problem 1: 42.017/42.017 Linearity Processor: 42.017/42.017 Linear? 42.017/42.017 YES 42.017/42.017 Problem 1.1: 42.017/42.017 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 42.017/42.017 Confluence Problem: 42.017/42.017 (REPLACEMENT-MAP 42.017/42.017 (f 1, 2) 42.017/42.017 (fSNonEmpty) 42.017/42.017 (g 1) 42.017/42.017 (s 1) 42.017/42.017 ) 42.017/42.017 (RULES 42.017/42.017 ) 42.017/42.017 Linear:YES 42.017/42.017 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 42.017/42.017 42.017/42.017 Huet Levy Processor: 42.017/42.017 -> Rules: 42.017/42.017 42.017/42.017 -> Vars: 42.017/42.017 42.017/42.017 42.017/42.017 -> Rlps: 42.017/42.017 42.017/42.017 42.017/42.017 -> Unifications: 42.017/42.017 42.017/42.017 42.017/42.017 -> Critical pairs info: 42.017/42.017 42.017/42.017 42.017/42.017 -> Problem conclusions: 42.017/42.017 Left linear, Right linear, Linear 42.017/42.017 Weakly orthogonal, Almost orthogonal, Orthogonal 42.017/42.017 Huet-Levy confluent, Not Newman confluent 42.017/42.017 R is a TRS 42.017/42.017 42.017/42.017 42.017/42.017 The problem is joinable. 42.017/42.017 49.43user 1.03system 0:42.17elapsed 119%CPU (0avgtext+0avgdata 436024maxresident)k 42.017/42.017 0inputs+0outputs (0major+288912minor)pagefaults 0swaps