21.05/21.05	YES
21.05/21.05	
21.05/21.05	Problem 1:
21.05/21.05	
21.05/21.05	
21.05/21.05	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.05/21.05	Confluence Problem:
21.05/21.05	(VAR vNonEmpty:S)
21.05/21.05	(STRATEGY CONTEXTSENSITIVE
21.05/21.05	(a)
21.05/21.05	(f 1)
21.05/21.05	(b)
21.05/21.05	(c)
21.05/21.05	(fSNonEmpty)
21.05/21.05	)
21.05/21.05	(RULES
21.05/21.05	a -> c | f(a) ->* f(b)
21.05/21.05	f(b) -> b
21.05/21.05	)
21.05/21.05	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.05/21.05	
21.05/21.05	
21.05/21.05	Problem 1:
21.05/21.05	
21.05/21.05	Inlining of Conditions Processor [STERN17]:
21.05/21.05	
21.05/21.05	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.05/21.05	Confluence Problem:
21.05/21.05	(VAR vNonEmpty:S)
21.05/21.05	(STRATEGY CONTEXTSENSITIVE
21.05/21.05	(a)
21.05/21.05	(f 1)
21.05/21.05	(b)
21.05/21.05	(c)
21.05/21.05	(fSNonEmpty)
21.05/21.05	)
21.05/21.05	(RULES
21.05/21.05	a -> c | f(a) ->* f(b)
21.05/21.05	f(b) -> b
21.05/21.05	)
21.05/21.05	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.05/21.05	
21.05/21.05	
21.05/21.05	Problem 1:
21.05/21.05	
21.05/21.05	Clean CTRS Processor:
21.05/21.05	
21.05/21.05	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.05/21.05	Confluence Problem:
21.05/21.05	(STRATEGY CONTEXTSENSITIVE
21.05/21.05	(a)
21.05/21.05	(f 1)
21.05/21.05	(b)
21.05/21.05	(c)
21.05/21.05	(fSNonEmpty)
21.05/21.05	)
21.05/21.05	(RULES
21.05/21.05	f(b) -> b
21.05/21.05	)
21.05/21.05	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.05/21.05	
21.05/21.05	CRule InfChecker Info:
21.05/21.05	a -> c | f(a) ->* f(b)
21.05/21.05	Rule deleted
21.05/21.05	Proof:
21.05/21.05	YES
21.05/21.05	
21.05/21.05	Problem 1:
21.05/21.05	
21.05/21.05	Infeasibility Problem:
21.05/21.05	[(VAR vNonEmpty:S vNonEmpty:S:S)
21.05/21.05	(STRATEGY CONTEXTSENSITIVE
21.05/21.05	(a)
21.05/21.05	(f 1)
21.05/21.05	(b)
21.05/21.05	(c)
21.05/21.05	(fSNonEmpty)
21.05/21.05	)
21.05/21.05	(RULES
21.05/21.05	a -> c | f(a) ->* f(b)
21.05/21.05	f(b) -> b
21.05/21.05	)]
21.05/21.05	
21.05/21.05	Infeasibility Conditions:
21.05/21.05	f(a) ->* f(b)
21.05/21.05	
21.05/21.05	Problem 1:
21.05/21.05	
21.05/21.05	Obtaining a model using Mace4:
21.05/21.05	
21.05/21.05	 -> Usable Rules:
21.05/21.05	a -> c | f(a) ->* f(b)
21.05/21.05	f(b) -> b
21.05/21.05	
21.05/21.05	 -> Mace4 Output:
21.05/21.05	============================== Mace4 =================================
21.05/21.05	Mace4 (64) version 2009-11A, November 2009.
21.05/21.05	Process 121973 was started by ubuntu on ubuntu,
21.05/21.05	Fri Jul 16 15:42:37 2021
21.05/21.05	The command was "./mace4 -c -f /tmp/mace4121961-2.in".
21.05/21.05	============================== end of head ===========================
21.05/21.05	
21.05/21.05	============================== INPUT =================================
21.05/21.05	
21.05/21.05	% Reading from file /tmp/mace4121961-2.in
21.05/21.05	
21.05/21.05	assign(max_seconds,10).
21.05/21.05	
21.05/21.05	formulas(assumptions).
21.05/21.05	->(x1,y) -> ->(f(x1),f(y)) # label(congruence).
21.05/21.05	->*(f(a),f(b)) -> ->(a,c) # label(replacement).
21.05/21.05	->(f(b),b) # label(replacement).
21.05/21.05	->*(x,x) # label(reflexivity).
21.05/21.05	->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity).
21.05/21.05	end_of_list.
21.05/21.05	
21.05/21.05	formulas(goals).
21.05/21.05	->*(f(a),f(b)) # label(goal).
21.05/21.05	end_of_list.
21.05/21.05	
21.05/21.05	============================== end of input ==========================
21.05/21.05	
21.05/21.05	============================== PROCESS NON-CLAUSAL FORMULAS ==========
21.05/21.05	
21.05/21.05	% Formulas that are not ordinary clauses:
21.05/21.05	1 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence) # label(non_clause).  [assumption].
21.05/21.05	2 ->*(f(a),f(b)) -> ->(a,c) # label(replacement) # label(non_clause).  [assumption].
21.05/21.05	3 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause).  [assumption].
21.05/21.05	4 ->*(f(a),f(b)) # label(goal) # label(non_clause) # label(goal).  [goal].
21.05/21.05	
21.05/21.05	============================== end of process non-clausal formulas ===
21.05/21.05	
21.05/21.05	============================== CLAUSES FOR SEARCH ====================
21.05/21.05	
21.05/21.05	formulas(mace4_clauses).
21.05/21.05	-->(x,y) | ->(f(x),f(y)) # label(congruence).
21.05/21.05	-->*(f(a),f(b)) | ->(a,c) # label(replacement).
21.05/21.05	->(f(b),b) # label(replacement).
21.05/21.05	->*(x,x) # label(reflexivity).
21.05/21.05	-->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity).
21.05/21.05	-->*(f(a),f(b)) # label(goal).
21.05/21.05	end_of_list.
21.05/21.05	
21.05/21.05	============================== end of clauses for search =============
21.05/21.05	
21.05/21.05	% There are no natural numbers in the input.
21.05/21.05	
21.05/21.05	============================== DOMAIN SIZE 2 =========================
21.05/21.05	
21.05/21.05	============================== MODEL =================================
21.05/21.05	
21.05/21.05	interpretation( 2, [number=1, seconds=0], [
21.05/21.05	
21.05/21.05	        function(a, [ 0 ]),
21.05/21.05	
21.05/21.05	        function(b, [ 1 ]),
21.05/21.05	
21.05/21.05	        function(c, [ 0 ]),
21.05/21.05	
21.05/21.05	        function(f(_), [ 0, 1 ]),
21.05/21.05	
21.05/21.05	        relation(->*(_,_), [
21.05/21.05				   1, 0,
21.05/21.05				   0, 1 ]),
21.05/21.05	
21.05/21.05	        relation(->(_,_), [
21.05/21.05				   0, 0,
21.05/21.05				   0, 1 ])
21.05/21.05	]).
21.05/21.05	
21.05/21.05	============================== end of model ==========================
21.05/21.05	
21.05/21.05	============================== STATISTICS ============================
21.05/21.05	
21.05/21.05	For domain size 2.
21.05/21.05	
21.05/21.05	Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
21.05/21.05	Ground clauses: seen=17, kept=13.
21.05/21.05	Selections=9, assignments=13, propagations=14, current_models=1.
21.05/21.05	Rewrite_terms=47, rewrite_bools=29, indexes=21.
21.05/21.05	Rules_from_neg_clauses=1, cross_offs=1.
21.05/21.05	
21.05/21.05	============================== end of statistics =====================
21.05/21.05	
21.05/21.05	User_CPU=0.00, System_CPU=0.00, Wall_clock=0.
21.05/21.05	
21.05/21.05	Exiting with 1 model.
21.05/21.05	
21.05/21.05	Process 121973 exit (max_models) Fri Jul 16 15:42:37 2021
21.05/21.05	The process finished Fri Jul 16 15:42:37 2021
21.05/21.05	
21.05/21.05	
21.05/21.05	Mace4 cooked interpretation:
21.05/21.05	
21.05/21.05	
21.05/21.05	
21.05/21.05	The problem is infeasible.
21.05/21.05	
21.05/21.05	
21.05/21.05	CRule InfChecker Info:
21.05/21.05	f(b) -> b
21.05/21.05	Rule remains
21.05/21.05	Proof:
21.05/21.05	NO_CONDS
21.05/21.05	
21.05/21.05	Problem 1:
21.05/21.05	
21.05/21.05	Transform No Conds CTRS Processor:
21.05/21.05	
21.05/21.05	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.05/21.05	Confluence Problem:
21.05/21.05	(STRATEGY CONTEXTSENSITIVE
21.05/21.05	(a)
21.05/21.05	(f 1)
21.05/21.05	(b)
21.05/21.05	(c)
21.05/21.05	(fSNonEmpty)
21.05/21.05	)
21.05/21.05	(RULES
21.05/21.05	f(b) -> b
21.05/21.05	)
21.05/21.05	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.05/21.05	Resulting R:
21.05/21.05	(STRATEGY CONTEXTSENSITIVE
21.05/21.05	(a)
21.05/21.05	(f 1)
21.05/21.05	(b)
21.05/21.05	(c)
21.05/21.05	(fSNonEmpty)
21.05/21.05	)
21.05/21.05	(RULES
21.05/21.05	f(b) -> b
21.05/21.05	)
21.05/21.05	
21.05/21.05	Problem 1:
21.05/21.05	
21.05/21.05	CleanTRS Processor:
21.05/21.05	
21.05/21.05	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.05/21.05	Confluence Problem:
21.05/21.05	(STRATEGY CONTEXTSENSITIVE
21.05/21.05	(a)
21.05/21.05	(f 1)
21.05/21.05	(b)
21.05/21.05	(c)
21.05/21.05	(fSNonEmpty)
21.05/21.05	)
21.05/21.05	(RULES
21.05/21.05	f(b) -> b
21.05/21.05	)
21.05/21.05	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.05/21.05	
21.05/21.05	
21.05/21.05	Problem 1:
21.05/21.05	
21.05/21.05	Modular Confluence Combinations Decomposition Processor:
21.05/21.05	
21.05/21.05	No usable combinations
21.05/21.05	
21.05/21.05	Problem 1:
21.05/21.05	Linearity Processor:
21.05/21.05	Linear?
21.05/21.05	YES
21.05/21.05	Problem 1.1:
21.05/21.05	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.05/21.05	Confluence Problem:
21.05/21.05	(STRATEGY CONTEXTSENSITIVE
21.05/21.05	(a)
21.05/21.05	(f 1)
21.05/21.05	(b)
21.05/21.05	(c)
21.05/21.05	(fSNonEmpty)
21.05/21.05	)
21.05/21.05	(RULES
21.05/21.05	f(b) -> b
21.05/21.05	)
21.05/21.05	Linear:YES
21.05/21.05	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.05/21.05	
21.05/21.05	Huet Levy Processor:
21.05/21.05	-> Rules:
21.05/21.05	 f(b) -> b
21.05/21.05	-> Vars:
21.05/21.05	
21.05/21.05	-> FVars:
21.05/21.05	
21.05/21.05	-> PVars:
21.05/21.05	
21.05/21.05	
21.05/21.05	-> Rlps:
21.05/21.05	 (rule: f(b) -> b, id: 1, possubterms: f(b)->[], b->[1])
21.05/21.05	
21.05/21.05	-> Unifications:
21.05/21.05	
21.05/21.05	
21.05/21.05	-> Critical pairs info:
21.05/21.05	
21.05/21.05	
21.05/21.05	-> Problem conclusions:
21.05/21.05	 Left linear, Right linear, Linear
21.05/21.05	 Weakly orthogonal, Almost orthogonal, Orthogonal
21.05/21.05	 Huet-Levy confluent, Not Newman confluent
21.05/21.05	 R is a TRS
21.05/21.05	
21.05/21.05	
21.05/21.05	The problem is joinable.
21.05/21.05	40.16user 2.36system 0:21.50elapsed 197%CPU (0avgtext+0avgdata 6819428maxresident)k
21.05/21.05	1850inputs+0outputs (13major+1726753minor)pagefaults 0swaps