NO Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (a 1) (b 1) (c 1) (fSNonEmpty) ) (RULES a(a(x)) -> c(a(x)) a(c(x)) -> a(b(x)) b(a(x)) -> a(a(x)) b(c(x)) -> a(a(x)) c(a(x)) -> b(a(x)) c(a(x)) -> b(c(x)) c(b(x)) -> a(c(x)) c(c(x)) -> a(a(x)) c(c(x)) -> c(c(x)) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: CleanTRS Procedure: R was updated by simple cleaning of the TRS ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (a 1) (b 1) (c 1) (fSNonEmpty) ) (RULES a(a(x)) -> c(a(x)) a(c(x)) -> a(b(x)) b(a(x)) -> a(a(x)) b(c(x)) -> a(a(x)) c(a(x)) -> b(a(x)) c(a(x)) -> b(c(x)) c(b(x)) -> a(c(x)) c(c(x)) -> a(a(x)) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 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(a(x)) -> c(a(x)) a(c(x)) -> a(b(x)) b(a(x)) -> a(a(x)) b(c(x)) -> a(a(x)) c(a(x)) -> b(a(x)) c(a(x)) -> b(c(x)) c(b(x)) -> a(c(x)) c(c(x)) -> a(a(x)) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Ordered by Num of Vars and Symbs Procedure: -> Rules: a(a(x)) -> c(a(x)) a(c(x)) -> a(b(x)) b(a(x)) -> a(a(x)) b(c(x)) -> a(a(x)) c(a(x)) -> b(a(x)) c(a(x)) -> b(c(x)) c(b(x)) -> a(c(x)) c(c(x)) -> a(a(x)) -> Vars: x, x, x, x, x, x, x, x -> Rlps: (rule: a(a(x)) -> c(a(x)), id: 1, possubterms: a(a(x))->[], a(x)->[1]) (rule: a(c(x)) -> a(b(x)), id: 2, possubterms: a(c(x))->[], c(x)->[1]) (rule: b(a(x)) -> a(a(x)), id: 3, possubterms: b(a(x))->[], a(x)->[1]) (rule: b(c(x)) -> a(a(x)), id: 4, possubterms: b(c(x))->[], c(x)->[1]) (rule: c(a(x)) -> b(a(x)), id: 5, possubterms: c(a(x))->[], a(x)->[1]) (rule: c(a(x)) -> b(c(x)), id: 6, possubterms: c(a(x))->[], a(x)->[1]) (rule: c(b(x)) -> a(c(x)), id: 7, possubterms: c(b(x))->[], b(x)->[1]) (rule: c(c(x)) -> a(a(x)), id: 8, possubterms: c(c(x))->[], c(x)->[1]) -> Unifications: (R1 unifies with R1 at p: [1], l: a(a(x)), lp: a(x), sig: {x -> a(x')}, l': a(a(x')), r: c(a(x)), r': c(a(x'))) (R1 unifies with R2 at p: [1], l: a(a(x)), lp: a(x), sig: {x -> c(x')}, l': a(c(x')), r: c(a(x)), r': a(b(x'))) (R2 unifies with R5 at p: [1], l: a(c(x)), lp: c(x), sig: {x -> a(x')}, l': c(a(x')), r: a(b(x)), r': b(a(x'))) (R2 unifies with R6 at p: [1], l: a(c(x)), lp: c(x), sig: {x -> a(x')}, l': c(a(x')), r: a(b(x)), r': b(c(x'))) (R2 unifies with R7 at p: [1], l: a(c(x)), lp: c(x), sig: {x -> b(x')}, l': c(b(x')), r: a(b(x)), r': a(c(x'))) (R2 unifies with R8 at p: [1], l: a(c(x)), lp: c(x), sig: {x -> c(x')}, l': c(c(x')), r: a(b(x)), r': a(a(x'))) (R3 unifies with R1 at p: [1], l: b(a(x)), lp: a(x), sig: {x -> a(x')}, l': a(a(x')), r: a(a(x)), r': c(a(x'))) (R3 unifies with R2 at p: [1], l: b(a(x)), lp: a(x), sig: {x -> c(x')}, l': a(c(x')), r: a(a(x)), r': a(b(x'))) (R4 unifies with R5 at p: [1], l: b(c(x)), lp: c(x), sig: {x -> a(x')}, l': c(a(x')), r: a(a(x)), r': b(a(x'))) (R4 unifies with R6 at p: [1], l: b(c(x)), lp: c(x), sig: {x -> a(x')}, l': c(a(x')), r: a(a(x)), r': b(c(x'))) (R4 unifies with R7 at p: [1], l: b(c(x)), lp: c(x), sig: {x -> b(x')}, l': c(b(x')), r: a(a(x)), r': a(c(x'))) (R4 unifies with R8 at p: [1], l: b(c(x)), lp: c(x), sig: {x -> c(x')}, l': c(c(x')), r: a(a(x)), r': a(a(x'))) (R5 unifies with R1 at p: [1], l: c(a(x)), lp: a(x), sig: {x -> a(x')}, l': a(a(x')), r: b(a(x)), r': c(a(x'))) (R5 unifies with R2 at p: [1], l: c(a(x)), lp: a(x), sig: {x -> c(x')}, l': a(c(x')), r: b(a(x)), r': a(b(x'))) (R6 unifies with R5 at p: [], l: c(a(x)), lp: c(a(x)), sig: {x -> x'}, l': c(a(x')), r: b(c(x)), r': b(a(x'))) (R6 unifies with R1 at p: [1], l: c(a(x)), lp: a(x), sig: {x -> a(x')}, l': a(a(x')), r: b(c(x)), r': c(a(x'))) (R6 unifies with R2 at p: [1], l: c(a(x)), lp: a(x), sig: {x -> c(x')}, l': a(c(x')), r: b(c(x)), r': a(b(x'))) (R7 unifies with R3 at p: [1], l: c(b(x)), lp: b(x), sig: {x -> a(x')}, l': b(a(x')), r: a(c(x)), r': a(a(x'))) (R7 unifies with R4 at p: [1], l: c(b(x)), lp: b(x), sig: {x -> c(x')}, l': b(c(x')), r: a(c(x)), r': a(a(x'))) (R8 unifies with R5 at p: [1], l: c(c(x)), lp: c(x), sig: {x -> a(x')}, l': c(a(x')), r: a(a(x)), r': b(a(x'))) (R8 unifies with R6 at p: [1], l: c(c(x)), lp: c(x), sig: {x -> a(x')}, l': c(a(x')), r: a(a(x)), r': b(c(x'))) (R8 unifies with R7 at p: [1], l: c(c(x)), lp: c(x), sig: {x -> b(x')}, l': c(b(x')), r: a(a(x)), r': a(c(x'))) (R8 unifies with R8 at p: [1], l: c(c(x)), lp: c(x), sig: {x -> c(x')}, l': c(c(x')), r: a(a(x)), r': a(a(x'))) -> Critical pairs info: => Not trivial, Not overlay, Proper, NW0, N1 => Not trivial, Not overlay, Proper, NW0, N2 => Not trivial, Not overlay, Proper, NW0, N3 => Not trivial, Not overlay, Proper, NW0, N4 => Not trivial, Not overlay, Proper, NW0, N5 => Trivial, Not overlay, Proper, NW0, N6 => Not trivial, Not overlay, Proper, NW0, N7 => Not trivial, Not overlay, Proper, NW0, N8 => Not trivial, Not overlay, Proper, NW0, N9 => Not trivial, Not overlay, Proper, NW0, N10 => Not trivial, Not overlay, Proper, NW0, N11 => Not trivial, Not overlay, Proper, NW0, N12 => Not trivial, Not overlay, Proper, NW0, N13 => Not trivial, Not overlay, Proper, NW0, N14 => Not trivial, Not overlay, Proper, NW0, N15 => Not trivial, Not overlay, Proper, NW0, N16 => Not trivial, Not overlay, Proper, NW0, N17 => Not trivial, Overlay, Proper, NW0, N18 => Not trivial, Not overlay, Proper, NW0, N19 => Not trivial, Not overlay, Proper, NW0, N20 => Not trivial, Not overlay, Proper, NW0, N21 => Not trivial, Not overlay, Proper, NW0, N22 => Not trivial, Not overlay, Proper, NW0, N23 -> 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(a(x)) -> c(a(x)) a(c(x)) -> a(b(x)) b(a(x)) -> a(a(x)) b(c(x)) -> a(a(x)) c(a(x)) -> b(a(x)) c(a(x)) -> b(c(x)) c(b(x)) -> a(c(x)) c(c(x)) -> a(a(x)) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N8 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 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(a(x)) -> c(a(x)) a(c(x)) -> a(b(x)) b(a(x)) -> a(a(x)) b(c(x)) -> a(a(x)) c(a(x)) -> b(a(x)) c(a(x)) -> b(c(x)) c(b(x)) -> a(c(x)) c(c(x)) -> a(a(x)) )] Infeasibility Conditions: a(a(c(c_x1))) ->* z0, a(b(b(c_x1))) ->* z0 Problem 1: Obtaining a model using Mace4: -> Usable Rules: a(a(x)) -> c(a(x)) a(c(x)) -> a(b(x)) b(a(x)) -> a(a(x)) b(c(x)) -> a(a(x)) c(a(x)) -> b(a(x)) c(a(x)) -> b(c(x)) c(b(x)) -> a(c(x)) c(c(x)) -> a(a(x)) -> Mace4 Output: ============================== Mace4 ================================= Mace4 (64) version 2009-11A, November 2009. Process 2874661 was started by shintani on shintani-XPS-13-9310, Fri Jun 9 18:37:37 2023 The command was "./mace4 -c -f /tmp/mace42874643-2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file /tmp/mace42874643-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(a(x1)),c(a(x1))) # label(replacement). ->(a(c(x1)),a(b(x1))) # label(replacement). ->(b(a(x1)),a(a(x1))) # label(replacement). ->(b(c(x1)),a(a(x1))) # label(replacement). ->(c(a(x1)),b(a(x1))) # label(replacement). ->(c(a(x1)),b(c(x1))) # label(replacement). ->(c(b(x1)),a(c(x1))) # label(replacement). ->(c(c(x1)),a(a(x1))) # label(replacement). ->*(x,x) # label(reflexivity). ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). end_of_list. formulas(goals). (exists x4 (->*(a(a(c(c_x1))),x4) & ->*(a(b(b(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 (->*(a(a(c(c_x1))),x4) & ->*(a(b(b(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(a(x)),c(a(x))) # label(replacement). ->(a(c(x)),a(b(x))) # label(replacement). ->(b(a(x)),a(a(x))) # label(replacement). ->(b(c(x)),a(a(x))) # label(replacement). ->(c(a(x)),b(a(x))) # label(replacement). ->(c(a(x)),b(c(x))) # label(replacement). ->(c(b(x)),a(c(x))) # label(replacement). ->(c(c(x)),a(a(x))) # label(replacement). ->*(x,x) # label(reflexivity). -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). -->*(a(a(c(c_x1))),x) | -->*(a(b(b(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=40, kept=36. Selections=30, assignments=59, propagations=50, current_models=0. Rewrite_terms=658, rewrite_bools=323, indexes=142. Rules_from_neg_clauses=6, cross_offs=6. ============================== 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=84, kept=75. Selections=2548, assignments=7034, propagations=4524, current_models=0. Rewrite_terms=67856, rewrite_bools=43392, indexes=6871. Rules_from_neg_clauses=186, cross_offs=1598. ============================== end of statistics ===================== ============================== DOMAIN SIZE 4 ========================= ============================== STATISTICS ============================ For domain size 4. Current CPU time: 0.00 seconds (total CPU time: 1.33 seconds). Ground clauses: seen=152, kept=136. Selections=241043, assignments=834076, propagations=507447, current_models=0. Rewrite_terms=8250580, rewrite_bools=5840470, indexes=708866. Rules_from_neg_clauses=13286, cross_offs=193078. ============================== end of statistics ===================== ============================== DOMAIN SIZE 5 ========================= ============================== MODEL ================================= interpretation( 5, [number=1, seconds=4], [ function(c_x1, [ 0 ]), function(a(_), [ 1, 3, 4, 3, 3 ]), function(b(_), [ 0, 3, 3, 3, 3 ]), function(c(_), [ 2, 3, 3, 3, 3 ]), relation(->*(_,_), [ 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 1, 0, 0, 1, 0, 1, 1 ]), relation(->(_,_), [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 1, 0, 1, 0 ]) ]). ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 5. Current CPU time: 0.00 seconds (total CPU time: 4.70 seconds). Ground clauses: seen=250, kept=225. Selections=404345, assignments=1738082, propagations=1973700, current_models=1. Rewrite_terms=20971238, rewrite_bools=17088150, indexes=2202481. Rules_from_neg_clauses=86504, cross_offs=551006. ============================== end of statistics ===================== User_CPU=4.70, System_CPU=0.25, Wall_clock=6. Exiting with 1 model. Process 2874661 exit (max_models) Fri Jun 9 18:37:43 2023 The process finished Fri Jun 9 18:37:43 2023 Mace4 cooked interpretation: The problem is infeasible. The problem is not confluent.