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