21.011/21.011	YES
21.011/21.011	
21.011/21.011	Problem 1:
21.011/21.011	
21.011/21.011	
21.011/21.011	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.011/21.011	Confluence Problem:
21.011/21.011	(VAR vNonEmpty x)
21.011/21.011	(REPLACEMENT-MAP
21.011/21.011	(A)
21.011/21.011	(e)
21.011/21.011	(d)
21.011/21.011	(f 1)
21.011/21.011	(fSNonEmpty)
21.011/21.011	(h 1, 2)
21.011/21.011	(l)
21.011/21.011	)
21.011/21.011	(RULES
21.011/21.011	A -> h(x,x)
21.011/21.011	e -> f(x) | l ->* d
21.011/21.011	)
21.011/21.011	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.011/21.011	
21.011/21.011	
21.011/21.011	Problem 1:
21.011/21.011	
21.011/21.011	Inlining of Conditions Processor [STERN17]:
21.011/21.011	
21.011/21.011	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.011/21.011	Confluence Problem:
21.011/21.011	(VAR vNonEmpty x)
21.011/21.011	(REPLACEMENT-MAP
21.011/21.011	(A)
21.011/21.011	(e)
21.011/21.011	(d)
21.011/21.011	(f 1)
21.011/21.011	(fSNonEmpty)
21.011/21.011	(h 1, 2)
21.011/21.011	(l)
21.011/21.011	)
21.011/21.011	(RULES
21.011/21.011	A -> h(x,x)
21.011/21.011	e -> f(x) | l ->* d
21.011/21.011	)
21.011/21.011	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.011/21.011	
21.011/21.011	
21.011/21.011	Problem 1:
21.011/21.011	
21.011/21.011	Clean CTRS Processor:
21.011/21.011	
21.011/21.011	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.011/21.011	Confluence Problem:
21.011/21.011	(VAR x)
21.011/21.011	(REPLACEMENT-MAP
21.011/21.011	(A)
21.011/21.011	(e)
21.011/21.011	(d)
21.011/21.011	(f 1)
21.011/21.011	(fSNonEmpty)
21.011/21.011	(h 1, 2)
21.011/21.011	(l)
21.011/21.011	)
21.011/21.011	(RULES
21.011/21.011	A -> h(x,x)
21.011/21.011	)
21.011/21.011	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.011/21.011	
21.011/21.011	CRule InfChecker Info:
21.011/21.011	A -> h(x,x)
21.011/21.011	Rule remains
21.011/21.011	Proof:
21.011/21.011	NO_CONDS
21.011/21.011	
21.011/21.011	CRule InfChecker Info:
21.011/21.011	e -> f(x) | l ->* d
21.011/21.011	Rule deleted
21.011/21.011	Proof:
21.011/21.011	YES
21.011/21.011	
21.011/21.011	Problem 1:
21.011/21.011	
21.011/21.011	Infeasibility Problem:
21.011/21.011	[(VAR vNonEmpty x vNonEmpty)
21.011/21.011	(STRATEGY CONTEXTSENSITIVE
21.011/21.011	(A)
21.011/21.011	(e)
21.011/21.011	(d)
21.011/21.011	(f 1)
21.011/21.011	(fSNonEmpty)
21.011/21.011	(h 1 2)
21.011/21.011	(l)
21.011/21.011	)
21.011/21.011	(RULES
21.011/21.011	A -> h(x,x)
21.011/21.011	e -> f(x) | l ->* d
21.011/21.011	)]
21.011/21.011	
21.011/21.011	Infeasibility Conditions:
21.011/21.011	l ->* d
21.011/21.011	
21.011/21.011	Problem 1:
21.011/21.011	
21.011/21.011	Obtaining a model using Mace4:
21.011/21.011	
21.011/21.011	 -> Usable Rules:
21.011/21.011	Empty
21.011/21.011	
21.011/21.011	 -> Mace4 Output:
21.011/21.011	============================== Mace4 =================================
21.011/21.011	Mace4 (64) version 2009-11A, November 2009.
21.011/21.011	Process 11640 was started by ubuntu on ubuntu,
21.011/21.011	Wed Mar  9 09:17:20 2022
21.011/21.011	The command was "./mace4 -c -f /tmp/mace411627-2.in".
21.011/21.011	============================== end of head ===========================
21.011/21.011	
21.011/21.011	============================== INPUT =================================
21.011/21.011	
21.011/21.011	% Reading from file /tmp/mace411627-2.in
21.011/21.011	
21.011/21.011	assign(max_seconds,20).
21.011/21.011	
21.011/21.011	formulas(assumptions).
21.011/21.011	->(x1,y) -> ->(f(x1),f(y)) # label(congruence).
21.011/21.011	->(x1,y) -> ->(h(x1,x2),h(y,x2)) # label(congruence).
21.011/21.011	->(x2,y) -> ->(h(x1,x2),h(x1,y)) # label(congruence).
21.011/21.011	->*(x,x) # label(reflexivity).
21.011/21.011	->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity).
21.011/21.011	end_of_list.
21.011/21.011	
21.011/21.011	formulas(goals).
21.011/21.011	->*(l,d) # label(goal).
21.011/21.011	end_of_list.
21.011/21.011	
21.011/21.011	============================== end of input ==========================
21.011/21.011	
21.011/21.011	============================== PROCESS NON-CLAUSAL FORMULAS ==========
21.011/21.011	
21.011/21.011	% Formulas that are not ordinary clauses:
21.011/21.011	1 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence) # label(non_clause).  [assumption].
21.011/21.011	2 ->(x1,y) -> ->(h(x1,x2),h(y,x2)) # label(congruence) # label(non_clause).  [assumption].
21.011/21.011	3 ->(x2,y) -> ->(h(x1,x2),h(x1,y)) # label(congruence) # label(non_clause).  [assumption].
21.011/21.011	4 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause).  [assumption].
21.011/21.011	5 ->*(l,d) # label(goal) # label(non_clause) # label(goal).  [goal].
21.011/21.011	
21.011/21.011	============================== end of process non-clausal formulas ===
21.011/21.011	
21.011/21.011	============================== CLAUSES FOR SEARCH ====================
21.011/21.011	
21.011/21.011	formulas(mace4_clauses).
21.011/21.011	-->(x,y) | ->(f(x),f(y)) # label(congruence).
21.011/21.011	-->(x,y) | ->(h(x,z),h(y,z)) # label(congruence).
21.011/21.011	-->(x,y) | ->(h(z,x),h(z,y)) # label(congruence).
21.011/21.011	->*(x,x) # label(reflexivity).
21.011/21.011	-->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity).
21.011/21.011	-->*(l,d) # label(goal).
21.011/21.011	end_of_list.
21.011/21.011	
21.011/21.011	============================== end of clauses for search =============
21.011/21.011	
21.011/21.011	% There are no natural numbers in the input.
21.011/21.011	
21.011/21.011	============================== DOMAIN SIZE 2 =========================
21.011/21.011	
21.011/21.011	============================== MODEL =================================
21.011/21.011	
21.011/21.011	interpretation( 2, [number=1, seconds=0], [
21.011/21.011	
21.011/21.011	        function(d, [ 0 ]),
21.011/21.011	
21.011/21.011	        function(l, [ 1 ]),
21.011/21.011	
21.011/21.011	        function(f(_), [ 0, 0 ]),
21.011/21.011	
21.011/21.011	        function(h(_,_), [
21.011/21.011				   0, 0,
21.011/21.011				   0, 0 ]),
21.011/21.011	
21.011/21.011	        relation(->*(_,_), [
21.011/21.011				   1, 0,
21.011/21.011				   0, 1 ]),
21.011/21.011	
21.011/21.011	        relation(->(_,_), [
21.011/21.011				   0, 0,
21.011/21.011				   0, 0 ])
21.011/21.011	]).
21.011/21.011	
21.011/21.011	============================== end of model ==========================
21.011/21.011	
21.011/21.011	============================== STATISTICS ============================
21.011/21.011	
21.011/21.011	For domain size 2.
21.011/21.011	
21.011/21.011	Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
21.011/21.011	Ground clauses: seen=31, kept=27.
21.011/21.011	Selections=9, assignments=9, propagations=7, current_models=1.
21.011/21.011	Rewrite_terms=42, rewrite_bools=34, indexes=4.
21.011/21.011	Rules_from_neg_clauses=1, cross_offs=1.
21.011/21.011	
21.011/21.011	============================== end of statistics =====================
21.011/21.011	
21.011/21.011	User_CPU=0.00, System_CPU=0.00, Wall_clock=0.
21.011/21.011	
21.011/21.011	Exiting with 1 model.
21.011/21.011	
21.011/21.011	Process 11640 exit (max_models) Wed Mar  9 09:17:20 2022
21.011/21.011	The process finished Wed Mar  9 09:17:20 2022
21.011/21.011	
21.011/21.011	
21.011/21.011	Mace4 cooked interpretation:
21.011/21.011	
21.011/21.011	
21.011/21.011	
21.011/21.011	The problem is infeasible.
21.011/21.011	
21.011/21.011	
21.011/21.011	Problem 1:
21.011/21.011	
21.011/21.011	Transform No Conds CTRS Processor:
21.011/21.011	
21.011/21.011	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.011/21.011	Confluence Problem:
21.011/21.011	(VAR x)
21.011/21.011	(REPLACEMENT-MAP
21.011/21.011	(A)
21.011/21.011	(e)
21.011/21.011	(d)
21.011/21.011	(f 1)
21.011/21.011	(fSNonEmpty)
21.011/21.011	(h 1, 2)
21.011/21.011	(l)
21.011/21.011	)
21.011/21.011	(RULES
21.011/21.011	A -> h(x,x)
21.011/21.011	)
21.011/21.011	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.011/21.011	Resulting R:
21.011/21.011	(VAR x)
21.011/21.011	(STRATEGY CONTEXTSENSITIVE
21.011/21.011	(A)
21.011/21.011	(e)
21.011/21.011	(d)
21.011/21.011	(f 1)
21.011/21.011	(fSNonEmpty)
21.011/21.011	(h 1 2)
21.011/21.011	(l)
21.011/21.011	)
21.011/21.011	(RULES
21.011/21.011	A -> h(x,x)
21.011/21.011	)
21.011/21.011	
21.011/21.011	Problem 1:
21.011/21.011	
21.011/21.011	CleanTRS Processor:
21.011/21.011	
21.011/21.011	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.011/21.011	Confluence Problem:
21.011/21.011	(VAR x)
21.011/21.011	(REPLACEMENT-MAP
21.011/21.011	(A)
21.011/21.011	(e)
21.011/21.011	(d)
21.011/21.011	(f 1)
21.011/21.011	(fSNonEmpty)
21.011/21.011	(h 1, 2)
21.011/21.011	(l)
21.011/21.011	)
21.011/21.011	(RULES
21.011/21.011	A -> h(x,x)
21.011/21.011	)
21.011/21.011	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.011/21.011	
21.011/21.011	
21.011/21.011	Problem 1:
21.011/21.011	
21.011/21.011	Modular Confluence Combinations Decomposition Processor:
21.011/21.011	
21.011/21.011	No usable combinations
21.011/21.011	
21.011/21.011	Problem 1:
21.011/21.011	Linearity Processor:
21.011/21.011	Linear?
21.011/21.011	NO
21.011/21.011	Problem 1.1:
21.011/21.011	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.011/21.011	Confluence Problem:
21.011/21.011	(VAR x)
21.011/21.011	(REPLACEMENT-MAP
21.011/21.011	(A)
21.011/21.011	(e)
21.011/21.011	(d)
21.011/21.011	(f 1)
21.011/21.011	(fSNonEmpty)
21.011/21.011	(h 1, 2)
21.011/21.011	(l)
21.011/21.011	)
21.011/21.011	(RULES
21.011/21.011	A -> h(x,x)
21.011/21.011	)
21.011/21.011	Linear:NO
21.011/21.011	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.011/21.011	
21.011/21.011	Huet Levy Processor:
21.011/21.011	-> Rules:
21.011/21.011	 A -> h(x,x)
21.011/21.011	-> Vars:
21.011/21.011	 x
21.011/21.011	
21.011/21.011	-> Rlps:
21.011/21.011	 (rule: A -> h(x,x), id: 1, possubterms: A->[])
21.011/21.011	
21.011/21.011	-> Unifications:
21.011/21.011	
21.011/21.011	
21.011/21.011	-> Critical pairs info:
21.011/21.011	
21.011/21.011	
21.011/21.011	-> Problem conclusions:
21.011/21.011	 Left linear, Not right linear, Not linear
21.011/21.011	 Weakly orthogonal, Almost orthogonal, Orthogonal
21.011/21.011	 Huet-Levy confluent, Not Newman confluent
21.011/21.011	 R is a TRS
21.011/21.011	
21.011/21.011	
21.011/21.011	The problem is joinable.
21.011/21.011	21.75user 0.49system 0:21.11elapsed 105%CPU (0avgtext+0avgdata 511892maxresident)k
21.011/21.011	8inputs+0outputs (0major+156630minor)pagefaults 0swaps