20.017/20.017	NO
20.017/20.017	
20.017/20.017	Problem 1:
20.017/20.017	
20.017/20.017	
20.017/20.017	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
20.017/20.017	Confluence Problem:
20.017/20.017	(VAR vNonEmpty x y)
20.017/20.017	(REPLACEMENT-MAP
20.017/20.017	(f 1, 2, 3)
20.017/20.017	(g 1)
20.017/20.017	(h 1)
20.017/20.017	(a)
20.017/20.017	(b)
20.017/20.017	(c 1)
20.017/20.017	(d)
20.017/20.017	(fSNonEmpty)
20.017/20.017	(k 1)
20.017/20.017	)
20.017/20.017	(RULES
20.017/20.017	f(k(a),k(b),x) -> f(x,x,x)
20.017/20.017	g(x) -> k(y) | h(x) ->* d, h(x) ->* c(y)
20.017/20.017	h(d) -> c(a)
20.017/20.017	h(d) -> c(b)
20.017/20.017	)
20.017/20.017	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
20.017/20.017	
20.017/20.017	
20.017/20.017	Problem 1:
20.017/20.017	
20.017/20.017	Inlining of Conditions Processor [STERN17]:
20.017/20.017	
20.017/20.017	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
20.017/20.017	Confluence Problem:
20.017/20.017	(VAR vNonEmpty x y)
20.017/20.017	(REPLACEMENT-MAP
20.017/20.017	(f 1, 2, 3)
20.017/20.017	(g 1)
20.017/20.017	(h 1)
20.017/20.017	(a)
20.017/20.017	(b)
20.017/20.017	(c 1)
20.017/20.017	(d)
20.017/20.017	(fSNonEmpty)
20.017/20.017	(k 1)
20.017/20.017	)
20.017/20.017	(RULES
20.017/20.017	f(k(a),k(b),x) -> f(x,x,x)
20.017/20.017	g(x) -> k(y) | h(x) ->* c(y), h(x) ->* d
20.017/20.017	h(d) -> c(a)
20.017/20.017	h(d) -> c(b)
20.017/20.017	)
20.017/20.017	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
20.017/20.017	
20.017/20.017	
20.017/20.017	Problem 1:
20.017/20.017	
20.017/20.017	Clean CTRS Processor:
20.017/20.017	
20.017/20.017	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
20.017/20.017	Confluence Problem:
20.017/20.017	(VAR x)
20.017/20.017	(REPLACEMENT-MAP
20.017/20.017	(f 1, 2, 3)
20.017/20.017	(g 1)
20.017/20.017	(h 1)
20.017/20.017	(a)
20.017/20.017	(b)
20.017/20.017	(c 1)
20.017/20.017	(d)
20.017/20.017	(fSNonEmpty)
20.017/20.017	(k 1)
20.017/20.017	)
20.017/20.017	(RULES
20.017/20.017	f(k(a),k(b),x) -> f(x,x,x)
20.017/20.017	h(d) -> c(a)
20.017/20.017	h(d) -> c(b)
20.017/20.017	)
20.017/20.017	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
20.017/20.017	
20.017/20.017	CRule InfChecker Info:
20.017/20.017	f(k(a),k(b),x) -> f(x,x,x)
20.017/20.017	Rule remains
20.017/20.017	Proof:
20.017/20.017	NO_CONDS
20.017/20.017	
20.017/20.017	CRule InfChecker Info:
20.017/20.017	g(x) -> k(y) | h(x) ->* c(y), h(x) ->* d
20.017/20.017	Rule deleted
20.017/20.017	Proof:
20.017/20.017	YES
20.017/20.017	
20.017/20.017	Problem 1:
20.017/20.017	
20.017/20.017	Infeasibility Problem:
20.017/20.017	[(VAR vNonEmpty x y vNonEmpty x y)
20.017/20.017	(STRATEGY CONTEXTSENSITIVE
20.017/20.017	(f 1 2 3)
20.017/20.017	(g 1)
20.017/20.017	(h 1)
20.017/20.017	(a)
20.017/20.017	(b)
20.017/20.017	(c 1)
20.017/20.017	(d)
20.017/20.017	(fSNonEmpty)
20.017/20.017	(k 1)
20.017/20.017	)
20.017/20.017	(RULES
20.017/20.017	f(k(a),k(b),x) -> f(x,x,x)
20.017/20.017	g(x) -> k(y) | h(x) ->* c(y), h(x) ->* d
20.017/20.017	h(d) -> c(a)
20.017/20.017	h(d) -> c(b)
20.017/20.017	)]
20.017/20.017	
20.017/20.017	Infeasibility Conditions:
20.017/20.017	h(x) ->* c(y), h(x) ->* d
20.017/20.017	
20.017/20.017	Problem 1:
20.017/20.017	
20.017/20.017	Obtaining a model using Mace4:
20.017/20.017	
20.017/20.017	 -> Usable Rules:
20.017/20.017	f(k(a),k(b),x) -> f(x,x,x)
20.017/20.017	g(x) -> k(y) | h(x) ->* c(y), h(x) ->* d
20.017/20.017	h(d) -> c(a)
20.017/20.017	h(d) -> c(b)
20.017/20.017	
20.017/20.017	 -> Mace4 Output:
20.017/20.017	============================== Mace4 =================================
20.017/20.017	Mace4 (64) version 2009-11A, November 2009.
20.017/20.017	Process 58837 was started by ubuntu on ubuntu,
20.017/20.017	Wed Mar  9 09:37:52 2022
20.017/20.017	The command was "./mace4 -c -f /tmp/mace458824-2.in".
20.017/20.017	============================== end of head ===========================
20.017/20.017	
20.017/20.017	============================== INPUT =================================
20.017/20.017	
20.017/20.017	% Reading from file /tmp/mace458824-2.in
20.017/20.017	
20.017/20.017	assign(max_seconds,20).
20.017/20.017	
20.017/20.017	formulas(assumptions).
20.017/20.017	->(x1,y) -> ->(f(x1,x2,x3),f(y,x2,x3)) # label(congruence).
20.017/20.017	->(x2,y) -> ->(f(x1,x2,x3),f(x1,y,x3)) # label(congruence).
20.017/20.017	->(x3,y) -> ->(f(x1,x2,x3),f(x1,x2,y)) # label(congruence).
20.017/20.017	->(x1,y) -> ->(g(x1),g(y)) # label(congruence).
20.017/20.017	->(x1,y) -> ->(h(x1),h(y)) # label(congruence).
20.017/20.017	->(x1,y) -> ->(c(x1),c(y)) # label(congruence).
20.017/20.017	->(x1,y) -> ->(k(x1),k(y)) # label(congruence).
20.017/20.017	->(f(k(a),k(b),x1),f(x1,x1,x1)) # label(replacement).
20.017/20.017	->*(h(x1),c(x2)) & ->*(h(x1),d) -> ->(g(x1),k(x2)) # label(replacement).
20.017/20.017	->(h(d),c(a)) # label(replacement).
20.017/20.017	->(h(d),c(b)) # label(replacement).
20.017/20.017	->*(x,x) # label(reflexivity).
20.017/20.017	->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity).
20.017/20.017	end_of_list.
20.017/20.017	
20.017/20.017	formulas(goals).
20.017/20.017	(exists x4 exists x5 (->*(h(x4),c(x5)) & ->*(h(x4),d))) # label(goal).
20.017/20.017	end_of_list.
20.017/20.017	
20.017/20.017	============================== end of input ==========================
20.017/20.017	
20.017/20.017	============================== PROCESS NON-CLAUSAL FORMULAS ==========
20.017/20.017	
20.017/20.017	% Formulas that are not ordinary clauses:
20.017/20.017	1 ->(x1,y) -> ->(f(x1,x2,x3),f(y,x2,x3)) # label(congruence) # label(non_clause).  [assumption].
20.017/20.017	2 ->(x2,y) -> ->(f(x1,x2,x3),f(x1,y,x3)) # label(congruence) # label(non_clause).  [assumption].
20.017/20.017	3 ->(x3,y) -> ->(f(x1,x2,x3),f(x1,x2,y)) # label(congruence) # label(non_clause).  [assumption].
20.017/20.017	4 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence) # label(non_clause).  [assumption].
20.017/20.017	5 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence) # label(non_clause).  [assumption].
20.017/20.017	6 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence) # label(non_clause).  [assumption].
20.017/20.017	7 ->(x1,y) -> ->(k(x1),k(y)) # label(congruence) # label(non_clause).  [assumption].
20.017/20.017	8 ->*(h(x1),c(x2)) & ->*(h(x1),d) -> ->(g(x1),k(x2)) # label(replacement) # label(non_clause).  [assumption].
20.017/20.017	9 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause).  [assumption].
20.017/20.017	10 (exists x4 exists x5 (->*(h(x4),c(x5)) & ->*(h(x4),d))) # label(goal) # label(non_clause) # label(goal).  [goal].
20.017/20.017	
20.017/20.017	============================== end of process non-clausal formulas ===
20.017/20.017	
20.017/20.017	============================== CLAUSES FOR SEARCH ====================
20.017/20.017	
20.017/20.017	formulas(mace4_clauses).
20.017/20.017	-->(x,y) | ->(f(x,z,u),f(y,z,u)) # label(congruence).
20.017/20.017	-->(x,y) | ->(f(z,x,u),f(z,y,u)) # label(congruence).
20.017/20.017	-->(x,y) | ->(f(z,u,x),f(z,u,y)) # label(congruence).
20.017/20.017	-->(x,y) | ->(g(x),g(y)) # label(congruence).
20.017/20.017	-->(x,y) | ->(h(x),h(y)) # label(congruence).
20.017/20.017	-->(x,y) | ->(c(x),c(y)) # label(congruence).
20.017/20.017	-->(x,y) | ->(k(x),k(y)) # label(congruence).
20.017/20.017	->(f(k(a),k(b),x),f(x,x,x)) # label(replacement).
20.017/20.017	-->*(h(x),c(y)) | -->*(h(x),d) | ->(g(x),k(y)) # label(replacement).
20.017/20.017	->(h(d),c(a)) # label(replacement).
20.017/20.017	->(h(d),c(b)) # label(replacement).
20.017/20.017	->*(x,x) # label(reflexivity).
20.017/20.017	-->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity).
20.017/20.017	-->*(h(x),c(y)) | -->*(h(x),d) # label(goal).
20.017/20.017	end_of_list.
20.017/20.017	
20.017/20.017	============================== end of clauses for search =============
20.017/20.017	
20.017/20.017	% There are no natural numbers in the input.
20.017/20.017	
20.017/20.017	============================== DOMAIN SIZE 2 =========================
20.017/20.017	
20.017/20.017	============================== MODEL =================================
20.017/20.017	
20.017/20.017	interpretation( 2, [number=1, seconds=0], [
20.017/20.017	
20.017/20.017	        function(a, [ 0 ]),
20.017/20.017	
20.017/20.017	        function(b, [ 0 ]),
20.017/20.017	
20.017/20.017	        function(d, [ 0 ]),
20.017/20.017	
20.017/20.017	        function(k(_), [ 0, 0 ]),
20.017/20.017	
20.017/20.017	        function(g(_), [ 0, 0 ]),
20.017/20.017	
20.017/20.017	        function(h(_), [ 1, 0 ]),
20.017/20.017	
20.017/20.017	        function(c(_), [ 1, 1 ]),
20.017/20.017	
20.017/20.017	        function(f(_,_,_), [
20.017/20.017				   0, 0,
20.017/20.017				   0, 0,
20.017/20.017				   0, 0,
20.017/20.017				   0, 0 ]),
20.017/20.017	
20.017/20.017	        relation(->*(_,_), [
20.017/20.017				   1, 0,
20.017/20.017				   0, 1 ]),
20.017/20.017	
20.017/20.017	        relation(->(_,_), [
20.017/20.017				   1, 0,
20.017/20.017				   0, 1 ])
20.017/20.017	]).
20.017/20.017	
20.017/20.017	============================== end of model ==========================
20.017/20.017	
20.017/20.017	============================== STATISTICS ============================
20.017/20.017	
20.017/20.017	For domain size 2.
20.017/20.017	
20.017/20.017	Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
20.017/20.017	Ground clauses: seen=86, kept=82.
20.017/20.017	Selections=17, assignments=19, propagations=15, current_models=1.
20.017/20.017	Rewrite_terms=222, rewrite_bools=145, indexes=30.
20.017/20.017	Rules_from_neg_clauses=3, cross_offs=3.
20.017/20.017	
20.017/20.017	============================== end of statistics =====================
20.017/20.017	
20.017/20.017	User_CPU=0.01, System_CPU=0.00, Wall_clock=0.
20.017/20.017	
20.017/20.017	Exiting with 1 model.
20.017/20.017	
20.017/20.017	Process 58837 exit (max_models) Wed Mar  9 09:37:52 2022
20.017/20.017	The process finished Wed Mar  9 09:37:52 2022
20.017/20.017	
20.017/20.017	
20.017/20.017	Mace4 cooked interpretation:
20.017/20.017	
20.017/20.017	
20.017/20.017	
20.017/20.017	The problem is infeasible.
20.017/20.017	
20.017/20.017	
20.017/20.017	CRule InfChecker Info:
20.017/20.017	h(d) -> c(a)
20.017/20.017	Rule remains
20.017/20.017	Proof:
20.017/20.017	NO_CONDS
20.017/20.017	
20.017/20.017	CRule InfChecker Info:
20.017/20.017	h(d) -> c(b)
20.017/20.017	Rule remains
20.017/20.017	Proof:
20.017/20.017	NO_CONDS
20.017/20.017	
20.017/20.017	Problem 1:
20.017/20.017	
20.017/20.017	Transform No Conds CTRS Processor:
20.017/20.017	
20.017/20.017	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
20.017/20.017	Confluence Problem:
20.017/20.017	(VAR x)
20.017/20.017	(REPLACEMENT-MAP
20.017/20.017	(f 1, 2, 3)
20.017/20.017	(g 1)
20.017/20.017	(h 1)
20.017/20.017	(a)
20.017/20.017	(b)
20.017/20.017	(c 1)
20.017/20.017	(d)
20.017/20.017	(fSNonEmpty)
20.017/20.017	(k 1)
20.017/20.017	)
20.017/20.017	(RULES
20.017/20.017	f(k(a),k(b),x) -> f(x,x,x)
20.017/20.017	h(d) -> c(a)
20.017/20.017	h(d) -> c(b)
20.017/20.017	)
20.017/20.017	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
20.017/20.017	Resulting R:
20.017/20.017	(VAR x)
20.017/20.017	(STRATEGY CONTEXTSENSITIVE
20.017/20.017	(f 1 2 3)
20.017/20.017	(g 1)
20.017/20.017	(h 1)
20.017/20.017	(a)
20.017/20.017	(b)
20.017/20.017	(c 1)
20.017/20.017	(d)
20.017/20.017	(fSNonEmpty)
20.017/20.017	(k 1)
20.017/20.017	)
20.017/20.017	(RULES
20.017/20.017	f(k(a),k(b),x) -> f(x,x,x)
20.017/20.017	h(d) -> c(a)
20.017/20.017	h(d) -> c(b)
20.017/20.017	)
20.017/20.017	
20.017/20.017	Problem 1:
20.017/20.017	
20.017/20.017	CleanTRS Processor:
20.017/20.017	
20.017/20.017	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
20.017/20.017	Confluence Problem:
20.017/20.017	(VAR x)
20.017/20.017	(REPLACEMENT-MAP
20.017/20.017	(f 1, 2, 3)
20.017/20.017	(g 1)
20.017/20.017	(h 1)
20.017/20.017	(a)
20.017/20.017	(b)
20.017/20.017	(c 1)
20.017/20.017	(d)
20.017/20.017	(fSNonEmpty)
20.017/20.017	(k 1)
20.017/20.017	)
20.017/20.017	(RULES
20.017/20.017	f(k(a),k(b),x) -> f(x,x,x)
20.017/20.017	h(d) -> c(a)
20.017/20.017	h(d) -> c(b)
20.017/20.017	)
20.017/20.017	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
20.017/20.017	
20.017/20.017	
20.017/20.017	Problem 1:
20.017/20.017	
20.017/20.017	Modular Confluence Combinations Decomposition Processor:
20.017/20.017	
20.017/20.017	TRS combination:
20.017/20.017	{f(k(a),k(b),x) -> f(x,x,x)}
20.017/20.017	{h(d) -> c(a)
20.017/20.017	 h(d) -> c(b)}
20.017/20.017	Not disjoint
20.017/20.017	Constructor-sharing
20.017/20.017	Left linear
20.017/20.017	Layer-preserving
20.017/20.017	TRS1
20.017/20.017	Just (VAR x)
20.017/20.017	(STRATEGY CONTEXTSENSITIVE
20.017/20.017	(f 1 2 3)
20.017/20.017	(a)
20.017/20.017	(b)
20.017/20.017	(k 1)
20.017/20.017	)
20.017/20.017	(RULES
20.017/20.017	f(k(a),k(b),x) -> f(x,x,x)
20.017/20.017	)
20.017/20.017	
20.017/20.017	TRS2
20.017/20.017	Just (STRATEGY CONTEXTSENSITIVE
20.017/20.017	(h 1)
20.017/20.017	(a)
20.017/20.017	(b)
20.017/20.017	(c 1)
20.017/20.017	(d)
20.017/20.017	)
20.017/20.017	(RULES
20.017/20.017	h(d) -> c(a)
20.017/20.017	h(d) -> c(b)
20.017/20.017	)
20.017/20.017	
20.017/20.017	Problem 1:
20.017/20.017	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
20.017/20.017	Confluence Problem:
20.017/20.017	(REPLACEMENT-MAP
20.017/20.017	(h 1)
20.017/20.017	(a)
20.017/20.017	(b)
20.017/20.017	(c 1)
20.017/20.017	(d)
20.017/20.017	)
20.017/20.017	(RULES
20.017/20.017	h(d) -> c(a)
20.017/20.017	h(d) -> c(b)
20.017/20.017	)
20.017/20.017	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
20.017/20.017	
20.017/20.017	Huet Levy Processor:
20.017/20.017	-> Rules:
20.017/20.017	 h(d) -> c(a)
20.017/20.017	 h(d) -> c(b)
20.017/20.017	-> Vars:
20.017/20.017	
20.017/20.017	
20.017/20.017	-> Rlps:
20.017/20.017	 (rule: h(d) -> c(a), id: 1, possubterms: h(d)->[], d->[1])
20.017/20.017	 (rule: h(d) -> c(b), id: 2, possubterms: h(d)->[], d->[1])
20.017/20.017	
20.017/20.017	-> Unifications:
20.017/20.017	(R2 unifies with R1 at p: [], l: h(d), lp: h(d), sig: {}, l': h(d), r: c(b), r': c(a))
20.017/20.017	
20.017/20.017	-> Critical pairs info:
20.017/20.017	<c(a),c(b)>   =>  Not trivial, Overlay, NW0, N1
20.017/20.017	
20.017/20.017	-> Problem conclusions:
20.017/20.017	 Left linear, Right linear, Linear
20.017/20.017	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
20.017/20.017	 Not Huet-Levy confluent, Not Newman confluent
20.017/20.017	 R is a TRS
20.017/20.017	
20.017/20.017	
20.017/20.017	Problem 1:
20.017/20.017	Different Normal CP Terms Processor:
20.017/20.017	<c(a),c(b)>   =>  Not trivial, Overlay, NW0, N1, Normal and not trivial cp
20.017/20.017	
20.017/20.017	The problem is not joinable.
20.017/20.017	19.97user 0.39system 0:20.17elapsed 100%CPU (0avgtext+0avgdata 62256maxresident)k
20.017/20.017	8inputs+0outputs (0major+29629minor)pagefaults 0swaps