21.01/21.01	YES
21.01/21.01	
21.01/21.01	Problem 1:
21.01/21.01	
21.01/21.01	
21.01/21.01	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.01/21.01	Confluence Problem:
21.01/21.01	(VAR vNonEmpty:S)
21.01/21.01	(STRATEGY CONTEXTSENSITIVE
21.01/21.01	(a)
21.01/21.01	(f 1)
21.01/21.01	(b)
21.01/21.01	(c)
21.01/21.01	(fSNonEmpty)
21.01/21.01	)
21.01/21.01	(RULES
21.01/21.01	a -> c | f(a) ->* f(b)
21.01/21.01	f(b) -> b
21.01/21.01	)
21.01/21.01	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.01/21.01	
21.01/21.01	
21.01/21.01	Problem 1:
21.01/21.01	
21.01/21.01	Inlining of Conditions Processor [STERN17]:
21.01/21.01	
21.01/21.01	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.01/21.01	Confluence Problem:
21.01/21.01	(VAR vNonEmpty:S)
21.01/21.01	(STRATEGY CONTEXTSENSITIVE
21.01/21.01	(a)
21.01/21.01	(f 1)
21.01/21.01	(b)
21.01/21.01	(c)
21.01/21.01	(fSNonEmpty)
21.01/21.01	)
21.01/21.01	(RULES
21.01/21.01	a -> c | f(a) ->* f(b)
21.01/21.01	f(b) -> b
21.01/21.01	)
21.01/21.01	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.01/21.01	
21.01/21.01	
21.01/21.01	Problem 1:
21.01/21.01	
21.01/21.01	Clean CTRS Processor:
21.01/21.01	
21.01/21.01	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.01/21.01	Confluence Problem:
21.01/21.01	(STRATEGY CONTEXTSENSITIVE
21.01/21.01	(a)
21.01/21.01	(f 1)
21.01/21.01	(b)
21.01/21.01	(c)
21.01/21.01	(fSNonEmpty)
21.01/21.01	)
21.01/21.01	(RULES
21.01/21.01	f(b) -> b
21.01/21.01	)
21.01/21.01	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.01/21.01	
21.01/21.01	CRule InfChecker Info:
21.01/21.01	a -> c | f(a) ->* f(b)
21.01/21.01	Rule deleted
21.01/21.01	Proof:
21.01/21.01	YES
21.01/21.01	
21.01/21.01	Problem 1:
21.01/21.01	
21.01/21.01	Infeasibility Problem:
21.01/21.01	[(VAR vNonEmpty:S vNonEmpty:S:S)
21.01/21.01	(STRATEGY CONTEXTSENSITIVE
21.01/21.01	(a)
21.01/21.01	(f 1)
21.01/21.01	(b)
21.01/21.01	(c)
21.01/21.01	(fSNonEmpty)
21.01/21.01	)
21.01/21.01	(RULES
21.01/21.01	a -> c | f(a) ->* f(b)
21.01/21.01	f(b) -> b
21.01/21.01	)]
21.01/21.01	
21.01/21.01	Infeasibility Conditions:
21.01/21.01	f(a) ->* f(b)
21.01/21.01	
21.01/21.01	Problem 1:
21.01/21.01	
21.01/21.01	Obtaining a model using Mace4:
21.01/21.01	
21.01/21.01	 -> Usable Rules:
21.01/21.01	a -> c | f(a) ->* f(b)
21.01/21.01	f(b) -> b
21.01/21.01	
21.01/21.01	 -> Mace4 Output:
21.01/21.01	============================== Mace4 =================================
21.01/21.01	Mace4 (64) version 2009-11A, November 2009.
21.01/21.01	Process 63259 was started by ubuntu on ubuntu,
21.01/21.01	Wed Jul 14 11:42:22 2021
21.01/21.01	The command was "./mace4 -c -f /tmp/mace463244-2.in".
21.01/21.01	============================== end of head ===========================
21.01/21.01	
21.01/21.01	============================== INPUT =================================
21.01/21.01	
21.01/21.01	% Reading from file /tmp/mace463244-2.in
21.01/21.01	
21.01/21.01	assign(max_seconds,20).
21.01/21.01	
21.01/21.01	formulas(assumptions).
21.01/21.01	->(x1,y) -> ->(f(x1),f(y)) # label(congruence).
21.01/21.01	->*(f(a),f(b)) -> ->(a,c) # label(replacement).
21.01/21.01	->(f(b),b) # label(replacement).
21.01/21.01	->*(x,x) # label(reflexivity).
21.01/21.01	->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity).
21.01/21.01	end_of_list.
21.01/21.01	
21.01/21.01	formulas(goals).
21.01/21.01	->*(f(a),f(b)) # label(goal).
21.01/21.01	end_of_list.
21.01/21.01	
21.01/21.01	============================== end of input ==========================
21.01/21.01	
21.01/21.01	============================== PROCESS NON-CLAUSAL FORMULAS ==========
21.01/21.01	
21.01/21.01	% Formulas that are not ordinary clauses:
21.01/21.01	1 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence) # label(non_clause).  [assumption].
21.01/21.01	2 ->*(f(a),f(b)) -> ->(a,c) # label(replacement) # label(non_clause).  [assumption].
21.01/21.01	3 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause).  [assumption].
21.01/21.01	4 ->*(f(a),f(b)) # label(goal) # label(non_clause) # label(goal).  [goal].
21.01/21.01	
21.01/21.01	============================== end of process non-clausal formulas ===
21.01/21.01	
21.01/21.01	============================== CLAUSES FOR SEARCH ====================
21.01/21.01	
21.01/21.01	formulas(mace4_clauses).
21.01/21.01	-->(x,y) | ->(f(x),f(y)) # label(congruence).
21.01/21.01	-->*(f(a),f(b)) | ->(a,c) # label(replacement).
21.01/21.01	->(f(b),b) # label(replacement).
21.01/21.01	->*(x,x) # label(reflexivity).
21.01/21.01	-->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity).
21.01/21.01	-->*(f(a),f(b)) # label(goal).
21.01/21.01	end_of_list.
21.01/21.01	
21.01/21.01	============================== end of clauses for search =============
21.01/21.01	
21.01/21.01	% There are no natural numbers in the input.
21.01/21.01	
21.01/21.01	============================== DOMAIN SIZE 2 =========================
21.01/21.01	
21.01/21.01	============================== MODEL =================================
21.01/21.01	
21.01/21.01	interpretation( 2, [number=1, seconds=0], [
21.01/21.01	
21.01/21.01	        function(a, [ 0 ]),
21.01/21.01	
21.01/21.01	        function(b, [ 1 ]),
21.01/21.01	
21.01/21.01	        function(c, [ 0 ]),
21.01/21.01	
21.01/21.01	        function(f(_), [ 0, 1 ]),
21.01/21.01	
21.01/21.01	        relation(->*(_,_), [
21.01/21.01				   1, 0,
21.01/21.01				   0, 1 ]),
21.01/21.01	
21.01/21.01	        relation(->(_,_), [
21.01/21.01				   0, 0,
21.01/21.01				   0, 1 ])
21.01/21.01	]).
21.01/21.01	
21.01/21.01	============================== end of model ==========================
21.01/21.01	
21.01/21.01	============================== STATISTICS ============================
21.01/21.01	
21.01/21.01	For domain size 2.
21.01/21.01	
21.01/21.01	Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
21.01/21.01	Ground clauses: seen=17, kept=13.
21.01/21.01	Selections=9, assignments=13, propagations=14, current_models=1.
21.01/21.01	Rewrite_terms=47, rewrite_bools=29, indexes=21.
21.01/21.01	Rules_from_neg_clauses=1, cross_offs=1.
21.01/21.01	
21.01/21.01	============================== end of statistics =====================
21.01/21.01	
21.01/21.01	User_CPU=0.00, System_CPU=0.00, Wall_clock=0.
21.01/21.01	
21.01/21.01	Exiting with 1 model.
21.01/21.01	
21.01/21.01	Process 63259 exit (max_models) Wed Jul 14 11:42:22 2021
21.01/21.01	The process finished Wed Jul 14 11:42:22 2021
21.01/21.01	
21.01/21.01	
21.01/21.01	Mace4 cooked interpretation:
21.01/21.01	
21.01/21.01	
21.01/21.01	
21.01/21.01	The problem is infeasible.
21.01/21.01	
21.01/21.01	
21.01/21.01	CRule InfChecker Info:
21.01/21.01	f(b) -> b
21.01/21.01	Rule remains
21.01/21.01	Proof:
21.01/21.01	NO_CONDS
21.01/21.01	
21.01/21.01	Problem 1:
21.01/21.01	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.01/21.01	Confluence Problem:
21.01/21.01	(STRATEGY CONTEXTSENSITIVE
21.01/21.01	(a)
21.01/21.01	(f 1)
21.01/21.01	(b)
21.01/21.01	(c)
21.01/21.01	(fSNonEmpty)
21.01/21.01	)
21.01/21.01	(RULES
21.01/21.01	f(b) -> b
21.01/21.01	)
21.01/21.01	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.01/21.01	
21.01/21.01	Critical Pairs Processor:
21.01/21.01	-> Rules:
21.01/21.01	f(b) -> b
21.01/21.01	-> Vars:
21.01/21.01	
21.01/21.01	-> FVars:
21.01/21.01	
21.01/21.01	-> PVars:
21.01/21.01	
21.01/21.01	
21.01/21.01	-> Rlps:
21.01/21.01	crule: f(b) -> b, id: 1, possubterms: f(b)-> [], b-> [1]
21.01/21.01	
21.01/21.01	-> Unifications:
21.01/21.01	
21.01/21.01	
21.01/21.01	-> Critical pairs info:
21.01/21.01	
21.01/21.01	
21.01/21.01	-> Problem conclusions:
21.01/21.01	 Left linear, Right linear, Linear
21.01/21.01	 Weakly orthogonal, Almost orthogonal, Orthogonal
21.01/21.01	 CTRS Type: 1
21.01/21.01	 Deterministic, Strongly deterministic
21.01/21.01	 Oriented CTRS, Properly oriented CTRS, Join CTRS
21.01/21.01	 Maybe right-stable CTRS, Overlay CTRS
21.01/21.01	 Normal CTRS, Almost normal CTRS
21.01/21.01	 Maybe terminating CTRS, Joinable CCPs
21.01/21.01	 Level confluent
21.01/21.01	 Confluent
21.01/21.01	
21.01/21.01	The problem is joinable.
21.01/21.01	39.97user 2.44system 0:21.10elapsed 201%CPU (0avgtext+0avgdata 6068796maxresident)k
21.01/21.01	1252inputs+0outputs (10major+1538909minor)pagefaults 0swaps