NO Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (f 1) (fSNonEmpty) (g 1) ) (RULES f(f(x)) -> f(g(f(f(x)))) f(x) -> x ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (f 1) (fSNonEmpty) (g 1) ) (RULES f(f(x)) -> f(g(f(f(x)))) f(x) -> x ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Ordered by Num of Vars and Symbs Procedure: -> Rules: f(f(x)) -> f(g(f(f(x)))) f(x) -> x -> Vars: x, x -> Rlps: (rule: f(f(x)) -> f(g(f(f(x)))), id: 1, possubterms: f(f(x))->[], f(x)->[1]) (rule: f(x) -> x, id: 2, possubterms: f(x)->[]) -> Unifications: (R1 unifies with R1 at p: [1], l: f(f(x)), lp: f(x), sig: {x -> f(x')}, l': f(f(x')), r: f(g(f(f(x)))), r': f(g(f(f(x'))))) (R1 unifies with R2 at p: [1], l: f(f(x)), lp: f(x), sig: {x -> x'}, l': f(x'), r: f(g(f(f(x)))), r': x') (R2 unifies with R1 at p: [], l: f(x), lp: f(x), sig: {x -> f(x')}, l': f(f(x')), r: x, r': f(g(f(f(x'))))) -> Critical pairs info: => Not trivial, Overlay, Proper, NW0, N1 => Not trivial, Not overlay, Proper, NW0, N2 => Not trivial, Not overlay, Proper, NW0, N3 -> Problem conclusions: Left linear, Right linear, Linear Not weakly orthogonal, Not almost orthogonal, Not orthogonal Not Huet-Levy confluent, Not Newman confluent R is a TRS Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (f 1) (fSNonEmpty) (g 1) ) (RULES f(f(x)) -> f(g(f(f(x)))) f(x) -> x ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N2 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: No Convergence InfChecker Procedure: Infeasible convergence? YES Problem 1: Infeasibility Problem: [(VAR vNonEmpty x x1 vNonEmpty z0) (STRATEGY CONTEXTSENSITIVE (f 1) (c_x1) (fSNonEmpty) (g 1) ) (RULES f(f(x)) -> f(g(f(f(x)))) f(x) -> x )] Infeasibility Conditions: f(c_x1) ->* z0, f(g(f(f(c_x1)))) ->* z0 Problem 1: Obtaining a model using Mace4: -> Usable Rules: f(f(x)) -> f(g(f(f(x)))) f(x) -> x -> Mace4 Output: ============================== Mace4 ================================= Mace4 (64) version 2009-11A, November 2009. Process 2883353 was started by shintani on shintani-XPS-13-9310, Fri Jun 9 18:56:10 2023 The command was "./mace4 -c -f /tmp/mace42883335-2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file /tmp/mace42883335-2.in assign(max_seconds,10). formulas(assumptions). ->(x1,y) -> ->(f(x1),f(y)) # label(congruence). ->(x1,y) -> ->(g(x1),g(y)) # label(congruence). ->(f(f(x1)),f(g(f(f(x1))))) # label(replacement). ->(f(x1),x1) # label(replacement). ->*(x,x) # label(reflexivity). ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). end_of_list. formulas(goals). (exists x4 (->*(f(c_x1),x4) & ->*(f(g(f(f(c_x1)))),x4))) # label(goal). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence) # label(non_clause). [assumption]. 2 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 3 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 4 (exists x4 (->*(f(c_x1),x4) & ->*(f(g(f(f(c_x1)))),x4))) # label(goal) # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== CLAUSES FOR SEARCH ==================== formulas(mace4_clauses). -->(x,y) | ->(f(x),f(y)) # label(congruence). -->(x,y) | ->(g(x),g(y)) # label(congruence). ->(f(f(x)),f(g(f(f(x))))) # label(replacement). ->(f(x),x) # label(replacement). ->*(x,x) # label(reflexivity). -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). -->*(f(c_x1),x) | -->*(f(g(f(f(c_x1)))),x) # label(goal). end_of_list. ============================== end of clauses for search ============= % There are no natural numbers in the input. ============================== DOMAIN SIZE 2 ========================= ============================== STATISTICS ============================ For domain size 2. Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). Ground clauses: seen=24, kept=20. Selections=13, assignments=25, propagations=18, current_models=0. Rewrite_terms=165, rewrite_bools=79, indexes=46. Rules_from_neg_clauses=2, cross_offs=2. ============================== end of statistics ===================== ============================== DOMAIN SIZE 3 ========================= ============================== STATISTICS ============================ For domain size 3. Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). Ground clauses: seen=57, kept=48. Selections=185, assignments=517, propagations=311, current_models=0. Rewrite_terms=3391, rewrite_bools=2304, indexes=521. Rules_from_neg_clauses=25, cross_offs=91. ============================== end of statistics ===================== ============================== DOMAIN SIZE 4 ========================= ============================== MODEL ================================= interpretation( 4, [number=1, seconds=0], [ function(c_x1, [ 0 ]), function(f(_), [ 1, 3, 2, 3 ]), function(g(_), [ 2, 2, 2, 2 ]), relation(->*(_,_), [ 1, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 0, 1, 1, 1, 1 ]), relation(->(_,_), [ 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0, 1, 1, 1 ]) ]). ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 4. Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=112, kept=96. Selections=857, assignments=3089, propagations=2438, current_models=1. Rewrite_terms=22267, rewrite_bools=16584, indexes=3986. Rules_from_neg_clauses=214, cross_offs=916. ============================== end of statistics ===================== User_CPU=0.01, System_CPU=0.00, Wall_clock=0. Exiting with 1 model. Process 2883353 exit (max_models) Fri Jun 9 18:56:10 2023 The process finished Fri Jun 9 18:56:10 2023 Mace4 cooked interpretation: The problem is infeasible. The problem is not confluent.