NO Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty) (REPLACEMENT-MAP (a) (h 1, 2) (b) (c) (f 1) (fSNonEmpty) ) (RULES a -> f(f(h(a,c))) h(h(h(c,f(h(f(h(h(c,c),c)),b))),h(h(a,c),h(f(a),h(f(f(c)),h(c,b))))),h(f(a),c)) -> c ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty) (REPLACEMENT-MAP (a) (h 1, 2) (b) (c) (f 1) (fSNonEmpty) ) (RULES a -> f(f(h(a,c))) h(h(h(c,f(h(f(h(h(c,c),c)),b))),h(h(a,c),h(f(a),h(f(f(c)),h(c,b))))),h(f(a),c)) -> c ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Ordered by Num of Vars and Symbs Procedure: -> Rules: a -> f(f(h(a,c))) h(h(h(c,f(h(f(h(h(c,c),c)),b))),h(h(a,c),h(f(a),h(f(f(c)),h(c,b))))),h(f(a),c)) -> c -> Vars: -> Rlps: (rule: a -> f(f(h(a,c))), id: 1, possubterms: a->[]) (rule: h(h(h(c,f(h(f(h(h(c,c),c)),b))),h(h(a,c),h(f(a),h(f(f(c)),h(c,b))))),h(f(a),c)) -> c, id: 2, possubterms: h(h(h(c,f(h(f(h(h(c,c),c)),b))),h(h(a,c),h(f(a),h(f(f(c)),h(c,b))))),h(f(a),c))->[], h(h(c,f(h(f(h(h(c,c),c)),b))),h(h(a,c),h(f(a),h(f(f(c)),h(c,b)))))->[1], h(c,f(h(f(h(h(c,c),c)),b)))->[1, 1], c->[1, 1, 1], f(h(f(h(h(c,c),c)),b))->[1, 1, 2], h(f(h(h(c,c),c)),b)->[1, 1, 2, 1], f(h(h(c,c),c))->[1, 1, 2, 1, 1], h(h(c,c),c)->[1, 1, 2, 1, 1, 1], h(c,c)->[1, 1, 2, 1, 1, 1, 1], c->[1, 1, 2, 1, 1, 1, 1, 1], c->[1, 1, 2, 1, 1, 1, 1, 2], c->[1, 1, 2, 1, 1, 1, 2], b->[1, 1, 2, 1, 2], h(h(a,c),h(f(a),h(f(f(c)),h(c,b))))->[1, 2], h(a,c)->[1, 2, 1], a->[1, 2, 1, 1], c->[1, 2, 1, 2], h(f(a),h(f(f(c)),h(c,b)))->[1, 2, 2], f(a)->[1, 2, 2, 1], a->[1, 2, 2, 1, 1], h(f(f(c)),h(c,b))->[1, 2, 2, 2], f(f(c))->[1, 2, 2, 2, 1], f(c)->[1, 2, 2, 2, 1, 1], c->[1, 2, 2, 2, 1, 1, 1], h(c,b)->[1, 2, 2, 2, 2], c->[1, 2, 2, 2, 2, 1], b->[1, 2, 2, 2, 2, 2], h(f(a),c)->[2], f(a)->[2, 1], a->[2, 1, 1], c->[2, 2]) -> Unifications: (R2 unifies with R1 at p: [1,2,1,1], l: h(h(h(c,f(h(f(h(h(c,c),c)),b))),h(h(a,c),h(f(a),h(f(f(c)),h(c,b))))),h(f(a),c)), lp: a, sig: {}, l': a, r: c, r': f(f(h(a,c)))) (R2 unifies with R1 at p: [1,2,2,1,1], l: h(h(h(c,f(h(f(h(h(c,c),c)),b))),h(h(a,c),h(f(a),h(f(f(c)),h(c,b))))),h(f(a),c)), lp: a, sig: {}, l': a, r: c, r': f(f(h(a,c)))) (R2 unifies with R1 at p: [2,1,1], l: h(h(h(c,f(h(f(h(h(c,c),c)),b))),h(h(a,c),h(f(a),h(f(f(c)),h(c,b))))),h(f(a),c)), lp: a, sig: {}, l': a, r: c, r': f(f(h(a,c)))) -> Critical pairs info: => Not trivial, Not 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: (REPLACEMENT-MAP (a) (h 1, 2) (b) (c) (f 1) (fSNonEmpty) ) (RULES a -> f(f(h(a,c))) h(h(h(c,f(h(f(h(h(c,c),c)),b))),h(h(a,c),h(f(a),h(f(f(c)),h(c,b))))),h(f(a),c)) -> c ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N1 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: No Convergence InfChecker Procedure: Infeasible convergence? YES Problem 1: Infeasibility Problem: [(VAR vNonEmpty vNonEmpty z0) (STRATEGY CONTEXTSENSITIVE (a) (h 1 2) (b) (c) (f 1) (fSNonEmpty) ) (RULES a -> f(f(h(a,c))) h(h(h(c,f(h(f(h(h(c,c),c)),b))),h(h(a,c),h(f(a),h(f(f(c)),h(c,b))))),h(f(a),c)) -> c )] Infeasibility Conditions: h(h(h(c,f(h(f(h(h(c,c),c)),b))),h(h(a,c),h(f(f(f(h(a,c)))),h(f(f(c)),h(c,b))))),h(f(a),c)) ->* z0, c ->* z0 Problem 1: Obtaining a model using Mace4: -> Usable Rules: a -> f(f(h(a,c))) h(h(h(c,f(h(f(h(h(c,c),c)),b))),h(h(a,c),h(f(a),h(f(f(c)),h(c,b))))),h(f(a),c)) -> c -> Mace4 Output: ============================== Mace4 ================================= Mace4 (64) version 2009-11A, November 2009. Process 2791739 was started by shintani on shintani-XPS-13-9310, Fri Jun 9 17:34:33 2023 The command was "./mace4 -c -f /tmp/mace42791710-2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file /tmp/mace42791710-2.in assign(max_seconds,10). formulas(assumptions). ->(x1,y) -> ->(h(x1,x2),h(y,x2)) # label(congruence). ->(x2,y) -> ->(h(x1,x2),h(x1,y)) # label(congruence). ->(x1,y) -> ->(f(x1),f(y)) # label(congruence). ->(a,f(f(h(a,c)))) # label(replacement). ->(h(h(h(c,f(h(f(h(h(c,c),c)),b))),h(h(a,c),h(f(a),h(f(f(c)),h(c,b))))),h(f(a),c)),c) # label(replacement). ->*(x,x) # label(reflexivity). ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). end_of_list. formulas(goals). (exists x2 (->*(h(h(h(c,f(h(f(h(h(c,c),c)),b))),h(h(a,c),h(f(f(f(h(a,c)))),h(f(f(c)),h(c,b))))),h(f(a),c)),x2) & ->*(c,x2))) # label(goal). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 ->(x1,y) -> ->(h(x1,x2),h(y,x2)) # label(congruence) # label(non_clause). [assumption]. 2 ->(x2,y) -> ->(h(x1,x2),h(x1,y)) # label(congruence) # label(non_clause). [assumption]. 3 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence) # label(non_clause). [assumption]. 4 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 5 (exists x2 (->*(h(h(h(c,f(h(f(h(h(c,c),c)),b))),h(h(a,c),h(f(f(f(h(a,c)))),h(f(f(c)),h(c,b))))),h(f(a),c)),x2) & ->*(c,x2))) # label(goal) # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== CLAUSES FOR SEARCH ==================== formulas(mace4_clauses). -->(x,y) | ->(h(x,z),h(y,z)) # label(congruence). -->(x,y) | ->(h(z,x),h(z,y)) # label(congruence). -->(x,y) | ->(f(x),f(y)) # label(congruence). ->(a,f(f(h(a,c)))) # label(replacement). ->(h(h(h(c,f(h(f(h(h(c,c),c)),b))),h(h(a,c),h(f(a),h(f(f(c)),h(c,b))))),h(f(a),c)),c) # label(replacement). ->*(x,x) # label(reflexivity). -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). -->*(h(h(h(c,f(h(f(h(h(c,c),c)),b))),h(h(a,c),h(f(f(f(h(a,c)))),h(f(f(c)),h(c,b))))),h(f(a),c)),x) | -->*(c,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=34, kept=30. Selections=291, assignments=581, propagations=373, current_models=0. Rewrite_terms=10826, rewrite_bools=2514, indexes=940. Rules_from_neg_clauses=27, cross_offs=27. ============================== end of statistics ===================== ============================== DOMAIN SIZE 3 ========================= ============================== MODEL ================================= interpretation( 3, [number=1, seconds=0], [ function(a, [ 0 ]), function(b, [ 0 ]), function(c, [ 1 ]), function(f(_), [ 0, 1, 2 ]), function(h(_,_), [ 0, 2, 0, 2, 2, 2, 0, 2, 2 ]), relation(->*(_,_), [ 1, 1, 1, 0, 1, 0, 0, 0, 1 ]), relation(->(_,_), [ 1, 1, 1, 0, 0, 0, 0, 0, 1 ]) ]). ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 3. Current CPU time: 0.00 seconds (total CPU time: 0.31 seconds). Ground clauses: seen=98, kept=89. Selections=133500, assignments=397406, propagations=158906, current_models=1. Rewrite_terms=4118349, rewrite_bools=1652578, indexes=321712. Rules_from_neg_clauses=15807, cross_offs=46981. ============================== end of statistics ===================== User_CPU=0.31, System_CPU=0.03, Wall_clock=0. Exiting with 1 model. Process 2791739 exit (max_models) Fri Jun 9 17:34:33 2023 The process finished Fri Jun 9 17:34:33 2023 Mace4 cooked interpretation: The problem is infeasible. The problem is not confluent.