NO Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x y) (REPLACEMENT-MAP (c) (f 1, 2) (h 1, 2) (d) (fSNonEmpty) (g 1) ) (RULES c -> f(c,d) c -> h(c,d) f(x,y) -> f(g(y),x) h(x,y) -> h(g(y),x) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x y) (REPLACEMENT-MAP (c) (f 1, 2) (h 1, 2) (d) (fSNonEmpty) (g 1) ) (RULES c -> f(c,d) c -> h(c,d) f(x,y) -> f(g(y),x) h(x,y) -> h(g(y),x) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Ordered by Num of Vars and Symbs Procedure: -> Rules: c -> f(c,d) c -> h(c,d) f(x,y) -> f(g(y),x) h(x,y) -> h(g(y),x) -> Vars: x, y, x, y -> Rlps: (rule: c -> f(c,d), id: 1, possubterms: c->[]) (rule: c -> h(c,d), id: 2, possubterms: c->[]) (rule: f(x,y) -> f(g(y),x), id: 3, possubterms: f(x,y)->[]) (rule: h(x,y) -> h(g(y),x), id: 4, possubterms: h(x,y)->[]) -> Unifications: (R2 unifies with R1 at p: [], l: c, lp: c, sig: {}, l': c, r: h(c,d), r': f(c,d)) -> Critical pairs info: => Not trivial, Overlay, Proper, NW0, N1 -> 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 y) (REPLACEMENT-MAP (c) (f 1, 2) (h 1, 2) (d) (fSNonEmpty) (g 1) ) (RULES c -> f(c,d) c -> h(c,d) f(x,y) -> f(g(y),x) h(x,y) -> h(g(y),x) ) Critical Pairs: => Not trivial, Overlay, Proper, NW0, N1 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: No Convergence InfChecker Procedure: Infeasible convergence? YES Problem 1: Infeasibility Problem: [(VAR vNonEmpty x y vNonEmpty z0) (STRATEGY CONTEXTSENSITIVE (c) (f 1 2) (h 1 2) (d) (fSNonEmpty) (g 1) ) (RULES c -> f(c,d) c -> h(c,d) f(x,y) -> f(g(y),x) h(x,y) -> h(g(y),x) )] Infeasibility Conditions: f(c,d) ->* z0, h(c,d) ->* z0 Problem 1: Obtaining a model using Mace4: -> Usable Rules: c -> f(c,d) c -> h(c,d) f(x,y) -> f(g(y),x) h(x,y) -> h(g(y),x) -> Mace4 Output: ============================== Mace4 ================================= Mace4 (64) version 2009-11A, November 2009. Process 2776893 was started by shintani on shintani-XPS-13-9310, Fri Jun 9 16:36:19 2023 The command was "./mace4 -c -f /tmp/mace42776877-2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file /tmp/mace42776877-2.in assign(max_seconds,10). formulas(assumptions). ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence). ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence). ->(x1,y) -> ->(h(x1,x2),h(y,x2)) # label(congruence). ->(x2,y) -> ->(h(x1,x2),h(x1,y)) # label(congruence). ->(x1,y) -> ->(g(x1),g(y)) # label(congruence). ->(c,f(c,d)) # label(replacement). ->(c,h(c,d)) # label(replacement). ->(f(x1,x2),f(g(x2),x1)) # label(replacement). ->(h(x1,x2),h(g(x2),x1)) # label(replacement). ->*(x,x) # label(reflexivity). ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). end_of_list. formulas(goals). (exists x4 (->*(f(c,d),x4) & ->*(h(c,d),x4))) # label(goal). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 2 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 3 ->(x1,y) -> ->(h(x1,x2),h(y,x2)) # label(congruence) # label(non_clause). [assumption]. 4 ->(x2,y) -> ->(h(x1,x2),h(x1,y)) # label(congruence) # label(non_clause). [assumption]. 5 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 6 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 7 (exists x4 (->*(f(c,d),x4) & ->*(h(c,d),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,z),f(y,z)) # label(congruence). -->(x,y) | ->(f(z,x),f(z,y)) # label(congruence). -->(x,y) | ->(h(x,z),h(y,z)) # label(congruence). -->(x,y) | ->(h(z,x),h(z,y)) # label(congruence). -->(x,y) | ->(g(x),g(y)) # label(congruence). ->(c,f(c,d)) # label(replacement). ->(c,h(c,d)) # label(replacement). ->(f(x,y),f(g(y),x)) # label(replacement). ->(h(x,y),h(g(y),x)) # label(replacement). ->*(x,x) # label(reflexivity). -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). -->*(f(c,d),x) | -->*(h(c,d),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=58, kept=54. Selections=41, assignments=81, propagations=189, current_models=0. Rewrite_terms=1223, rewrite_bools=835, indexes=287. Rules_from_neg_clauses=50, cross_offs=50. ============================== end of statistics ===================== ============================== DOMAIN SIZE 3 ========================= ============================== MODEL ================================= interpretation( 3, [number=1, seconds=0], [ function(c, [ 0 ]), function(d, [ 0 ]), function(g(_), [ 0, 1, 1 ]), function(f(_,_), [ 1, 1, 1, 1, 1, 1, 1, 1, 1 ]), function(h(_,_), [ 2, 2, 2, 2, 2, 2, 2, 2, 2 ]), relation(->*(_,_), [ 1, 1, 1, 0, 1, 0, 0, 0, 1 ]), relation(->(_,_), [ 0, 1, 1, 0, 1, 0, 0, 0, 1 ]) ]). ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 3. Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). Ground clauses: seen=170, kept=161. Selections=10, assignments=14, propagations=37, current_models=1. Rewrite_terms=383, rewrite_bools=290, indexes=30. Rules_from_neg_clauses=17, cross_offs=37. ============================== end of statistics ===================== User_CPU=0.00, System_CPU=0.00, Wall_clock=0. Exiting with 1 model. Process 2776893 exit (max_models) Fri Jun 9 16:36:19 2023 The process finished Fri Jun 9 16:36:19 2023 Mace4 cooked interpretation: The problem is infeasible. The problem is not confluent.