NO Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (a 1) (b 1) (c 1) (fSNonEmpty) ) (RULES a(x) -> b(x) b(b(c(x))) -> c(a(c(a(a(x))))) c(c(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 (a 1) (b 1) (c 1) (fSNonEmpty) ) (RULES a(x) -> b(x) b(b(c(x))) -> c(a(c(a(a(x))))) c(c(x)) -> x ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Ordered by Num of Vars and Symbs Procedure: -> Rules: a(x) -> b(x) b(b(c(x))) -> c(a(c(a(a(x))))) c(c(x)) -> x -> Vars: x, x, x -> Rlps: (rule: a(x) -> b(x), id: 1, possubterms: a(x)->[]) (rule: b(b(c(x))) -> c(a(c(a(a(x))))), id: 2, possubterms: b(b(c(x)))->[], b(c(x))->[1], c(x)->[1, 1]) (rule: c(c(x)) -> x, id: 3, possubterms: c(c(x))->[], c(x)->[1]) -> Unifications: (R2 unifies with R3 at p: [1,1], l: b(b(c(x))), lp: c(x), sig: {x -> c(x')}, l': c(c(x')), r: c(a(c(a(a(x))))), r': x') (R3 unifies with R3 at p: [1], l: c(c(x)), lp: c(x), sig: {x -> c(x')}, l': c(c(x')), r: x, r': x') -> Critical pairs info: => Trivial, Not overlay, Proper, NW0, N1 => Not trivial, Not overlay, Proper, NW0, N2 -> 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 (a 1) (b 1) (c 1) (fSNonEmpty) ) (RULES a(x) -> b(x) b(b(c(x))) -> c(a(c(a(a(x))))) c(c(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 (a 1) (b 1) (c 1) (c_x1) (fSNonEmpty) ) (RULES a(x) -> b(x) b(b(c(x))) -> c(a(c(a(a(x))))) c(c(x)) -> x )] Infeasibility Conditions: b(b(c_x1)) ->* z0, c(a(c(a(a(c(c_x1)))))) ->* z0 Problem 1: Obtaining a model using Mace4: -> Usable Rules: a(x) -> b(x) b(b(c(x))) -> c(a(c(a(a(x))))) c(c(x)) -> x -> Mace4 Output: ============================== Mace4 ================================= Mace4 (64) version 2009-11A, November 2009. Process 2804045 was started by shintani on shintani-XPS-13-9310, Fri Jun 9 18:20:45 2023 The command was "./mace4 -c -f /tmp/mace42804026-2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file /tmp/mace42804026-2.in assign(max_seconds,10). formulas(assumptions). ->(x1,y) -> ->(a(x1),a(y)) # label(congruence). ->(x1,y) -> ->(b(x1),b(y)) # label(congruence). ->(x1,y) -> ->(c(x1),c(y)) # label(congruence). ->(a(x1),b(x1)) # label(replacement). ->(b(b(c(x1))),c(a(c(a(a(x1)))))) # label(replacement). ->(c(c(x1)),x1) # label(replacement). ->*(x,x) # label(reflexivity). ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). end_of_list. formulas(goals). (exists x4 (->*(b(b(c_x1)),x4) & ->*(c(a(c(a(a(c(c_x1)))))),x4))) # label(goal). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 ->(x1,y) -> ->(a(x1),a(y)) # label(congruence) # label(non_clause). [assumption]. 2 ->(x1,y) -> ->(b(x1),b(y)) # label(congruence) # label(non_clause). [assumption]. 3 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence) # label(non_clause). [assumption]. 4 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 5 (exists x4 (->*(b(b(c_x1)),x4) & ->*(c(a(c(a(a(c(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) | ->(a(x),a(y)) # label(congruence). -->(x,y) | ->(b(x),b(y)) # label(congruence). -->(x,y) | ->(c(x),c(y)) # label(congruence). ->(a(x),b(x)) # label(replacement). ->(b(b(c(x))),c(a(c(a(a(x)))))) # label(replacement). ->(c(c(x)),x) # label(replacement). ->*(x,x) # label(reflexivity). -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). -->*(b(b(c_x1)),x) | -->*(c(a(c(a(a(c(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=30, kept=26. Selections=44, assignments=87, propagations=89, current_models=0. Rewrite_terms=924, rewrite_bools=410, indexes=158. Rules_from_neg_clauses=13, cross_offs=13. ============================== end of statistics ===================== ============================== DOMAIN SIZE 3 ========================= ============================== STATISTICS ============================ For domain size 3. Current CPU time: 0.00 seconds (total CPU time: 0.02 seconds). Ground clauses: seen=69, kept=60. Selections=4072, assignments=11517, propagations=8078, current_models=0. Rewrite_terms=112769, rewrite_bools=57412, indexes=11012. Rules_from_neg_clauses=1044, cross_offs=3359. ============================== end of statistics ===================== ============================== DOMAIN SIZE 4 ========================= ============================== MODEL ================================= interpretation( 4, [number=1, seconds=0], [ function(c_x1, [ 0 ]), function(a(_), [ 0, 2, 2, 3 ]), function(b(_), [ 0, 2, 2, 3 ]), function(c(_), [ 1, 3, 2, 1 ]), relation(->*(_,_), [ 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 1, 0, 1, 0, 1, 1 ]), relation(->(_,_), [ 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 1, 0, 1, 0, 1, 1 ]) ]). ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 4. Current CPU time: 0.00 seconds (total CPU time: 0.04 seconds). Ground clauses: seen=132, kept=116. Selections=9185, assignments=35304, propagations=18445, current_models=1. Rewrite_terms=281998, rewrite_bools=149946, indexes=19315. Rules_from_neg_clauses=473, cross_offs=4521. ============================== end of statistics ===================== User_CPU=0.04, System_CPU=0.01, Wall_clock=0. Exiting with 1 model. Process 2804045 exit (max_models) Fri Jun 9 18:20:45 2023 The process finished Fri Jun 9 18:20:45 2023 Mace4 cooked interpretation: The problem is infeasible. The problem is not confluent.