11.94/23.28	NO
11.94/23.28	
11.94/23.28	Problem 1: 
11.94/23.28	
11.94/23.28	
11.94/23.28	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
11.94/23.28	Confluence Problem:
11.94/23.28	(VAR vNonEmpty:S x:S)
11.94/23.28	(STRATEGY CONTEXTSENSITIVE
11.94/23.28	(a 1)
11.94/23.28	(b 1)
11.94/23.28	(c 1)
11.94/23.28	(fSNonEmpty)
11.94/23.28	)
11.94/23.28	(RULES
11.94/23.28	a(b(x:S)) -> a(b(x:S))
11.94/23.28	a(b(x:S)) -> b(c(x:S))
11.94/23.28	a(c(x:S)) -> c(a(x:S))
11.94/23.28	b(b(x:S)) -> a(c(x:S))
11.94/23.28	c(b(x:S)) -> b(c(x:S))
11.94/23.28	c(b(x:S)) -> c(c(x:S))
11.94/23.28	c(c(x:S)) -> c(b(x:S))
11.94/23.28	)
11.94/23.28	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
11.94/23.28	
11.94/23.28	
11.94/23.28	Problem 1: 
11.94/23.28	
11.94/23.28	CleanTRS Processor:
11.94/23.28	
11.94/23.28	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
11.94/23.28	Confluence Problem:
11.94/23.28	(VAR vNonEmpty:S x:S)
11.94/23.28	(STRATEGY CONTEXTSENSITIVE
11.94/23.28	(a 1)
11.94/23.28	(b 1)
11.94/23.28	(c 1)
11.94/23.28	(fSNonEmpty)
11.94/23.28	)
11.94/23.28	(RULES
11.94/23.28	a(b(x:S)) -> b(c(x:S))
11.94/23.28	a(c(x:S)) -> c(a(x:S))
11.94/23.28	b(b(x:S)) -> a(c(x:S))
11.94/23.28	c(b(x:S)) -> b(c(x:S))
11.94/23.28	c(b(x:S)) -> c(c(x:S))
11.94/23.28	c(c(x:S)) -> c(b(x:S))
11.94/23.28	)
11.94/23.28	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
11.94/23.28	
11.94/23.28	
11.94/23.28	Problem 1: 
11.94/23.28	
11.94/23.28	Modular Confluence Combinations Decomposition Processor:
11.94/23.28	
11.94/23.28	No usable combinations
11.94/23.28	
11.94/23.28	Problem 1: 
11.94/23.28	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
11.94/23.28	Confluence Problem:
11.94/23.28	(VAR vNonEmpty:S x:S)
11.94/23.28	(STRATEGY CONTEXTSENSITIVE
11.94/23.28	(a 1)
11.94/23.28	(b 1)
11.94/23.28	(c 1)
11.94/23.28	(fSNonEmpty)
11.94/23.28	)
11.94/23.28	(RULES
11.94/23.28	a(b(x:S)) -> b(c(x:S))
11.94/23.28	a(c(x:S)) -> c(a(x:S))
11.94/23.28	b(b(x:S)) -> a(c(x:S))
11.94/23.28	c(b(x:S)) -> b(c(x:S))
11.94/23.28	c(b(x:S)) -> c(c(x:S))
11.94/23.28	c(c(x:S)) -> c(b(x:S))
11.94/23.28	)
11.94/23.28	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
11.94/23.28	
11.94/23.28	Huet Levy Processor:
11.94/23.28	-> Rules:
11.94/23.28	 a(b(x:S)) -> b(c(x:S))
11.94/23.28	 a(c(x:S)) -> c(a(x:S))
11.94/23.28	 b(b(x:S)) -> a(c(x:S))
11.94/23.28	 c(b(x:S)) -> b(c(x:S))
11.94/23.28	 c(b(x:S)) -> c(c(x:S))
11.94/23.28	 c(c(x:S)) -> c(b(x:S))
11.94/23.28	-> Vars:
11.94/23.28	 x, x, x, x, x, x
11.94/23.28	-> FVars:
11.94/23.28	 x2, x3, x4, x5, x6, x7
11.94/23.28	-> PVars:
11.94/23.28	 x: [x2, x3, x4, x5, x6, x7]
11.94/23.28	
11.94/23.28	-> Rlps:
11.94/23.28	 (rule: a(b(x2:S)) -> b(c(x2:S)), id: 1, possubterms: a(b(x2:S))->[], b(x2:S)->[1])
11.94/23.28	 (rule: a(c(x3:S)) -> c(a(x3:S)), id: 2, possubterms: a(c(x3:S))->[], c(x3:S)->[1])
11.94/23.28	 (rule: b(b(x4:S)) -> a(c(x4:S)), id: 3, possubterms: b(b(x4:S))->[], b(x4:S)->[1])
11.94/23.28	 (rule: c(b(x5:S)) -> b(c(x5:S)), id: 4, possubterms: c(b(x5:S))->[], b(x5:S)->[1])
11.94/23.28	 (rule: c(b(x6:S)) -> c(c(x6:S)), id: 5, possubterms: c(b(x6:S))->[], b(x6:S)->[1])
11.94/23.28	 (rule: c(c(x7:S)) -> c(b(x7:S)), id: 6, possubterms: c(c(x7:S))->[], c(x7:S)->[1])
11.94/23.28	
11.94/23.28	-> Unifications:
11.94/23.28	(R1 unifies with R3 at p: [1], l: a(b(x2:S)), lp: b(x2:S), sig: {x2:S -> b(x:S)}, l': b(b(x:S)), r: b(c(x2:S)), r': a(c(x:S)))
11.94/23.28	(R2 unifies with R4 at p: [1], l: a(c(x3:S)), lp: c(x3:S), sig: {x3:S -> b(x:S)}, l': c(b(x:S)), r: c(a(x3:S)), r': b(c(x:S)))
11.94/23.28	(R2 unifies with R5 at p: [1], l: a(c(x3:S)), lp: c(x3:S), sig: {x3:S -> b(x:S)}, l': c(b(x:S)), r: c(a(x3:S)), r': c(c(x:S)))
11.94/23.28	(R2 unifies with R6 at p: [1], l: a(c(x3:S)), lp: c(x3:S), sig: {x3:S -> c(x:S)}, l': c(c(x:S)), r: c(a(x3:S)), r': c(b(x:S)))
11.94/23.28	(R3 unifies with R3 at p: [1], l: b(b(x4:S)), lp: b(x4:S), sig: {x4:S -> b(x:S)}, l': b(b(x:S)), r: a(c(x4:S)), r': a(c(x:S)))
11.94/23.28	(R4 unifies with R3 at p: [1], l: c(b(x5:S)), lp: b(x5:S), sig: {x5:S -> b(x:S)}, l': b(b(x:S)), r: b(c(x5:S)), r': a(c(x:S)))
11.94/23.28	(R5 unifies with R4 at p: [], l: c(b(x6:S)), lp: c(b(x6:S)), sig: {x6:S -> x:S}, l': c(b(x:S)), r: c(c(x6:S)), r': b(c(x:S)))
11.94/23.28	(R5 unifies with R3 at p: [1], l: c(b(x6:S)), lp: b(x6:S), sig: {x6:S -> b(x:S)}, l': b(b(x:S)), r: c(c(x6:S)), r': a(c(x:S)))
11.94/23.28	(R6 unifies with R4 at p: [1], l: c(c(x7:S)), lp: c(x7:S), sig: {x7:S -> b(x:S)}, l': c(b(x:S)), r: c(b(x7:S)), r': b(c(x:S)))
11.94/23.28	(R6 unifies with R5 at p: [1], l: c(c(x7:S)), lp: c(x7:S), sig: {x7:S -> b(x:S)}, l': c(b(x:S)), r: c(b(x7:S)), r': c(c(x:S)))
11.94/23.28	(R6 unifies with R6 at p: [1], l: c(c(x7:S)), lp: c(x7:S), sig: {x7:S -> c(x:S)}, l': c(c(x:S)), r: c(b(x7:S)), r': c(b(x:S)))
11.94/23.28	
11.94/23.28	-> Critical pairs info:
11.94/23.28	<c(c(c(x:S))),c(b(b(x:S)))>   =>  Not trivial, Not overlay, N1
11.94/23.28	<c(c(b(x:S))),c(b(c(x:S)))>   =>  Not trivial, Not overlay, N2
11.94/23.28	<c(b(c(x:S))),c(b(b(x:S)))>   =>  Not trivial, Not overlay, N3
11.94/23.28	<c(a(c(x:S))),c(c(b(x:S)))>   =>  Not trivial, Not overlay, N4
11.94/23.28	<c(a(c(x:S))),b(c(b(x:S)))>   =>  Not trivial, Not overlay, N5
11.94/23.28	<b(c(x:S)),c(c(x:S))>   =>  Not trivial, Overlay, N6
11.94/23.28	<b(a(c(x:S))),a(c(b(x:S)))>   =>  Not trivial, Not overlay, N7
11.94/23.28	<a(c(c(x:S))),c(a(b(x:S)))>   =>  Not trivial, Not overlay, N8
11.94/23.28	<a(c(b(x:S))),c(a(c(x:S)))>   =>  Not trivial, Not overlay, N9
11.94/23.28	<a(b(c(x:S))),c(a(b(x:S)))>   =>  Not trivial, Not overlay, N10
11.94/23.28	<a(a(c(x:S))),b(c(b(x:S)))>   =>  Not trivial, Not overlay, N11
11.94/23.28	
11.94/23.28	-> Problem conclusions:
11.94/23.28	 Left linear, Right linear, Linear
11.94/23.28	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
11.94/23.28	 Not Huet-Levy confluent, Not Newman confluent
11.94/23.28	 R is a TRS 
11.94/23.28	
11.94/23.28	
11.94/23.28	Problem 1: 
11.94/23.28	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
11.94/23.28	Confluence Problem:
11.94/23.28	(VAR vNonEmpty:S x:S)
11.94/23.28	(STRATEGY CONTEXTSENSITIVE
11.94/23.28	(a 1)
11.94/23.28	(b 1)
11.94/23.28	(c 1)
11.94/23.28	(fSNonEmpty)
11.94/23.28	)
11.94/23.28	(RULES
11.94/23.28	a(b(x:S)) -> b(c(x:S))
11.94/23.28	a(c(x:S)) -> c(a(x:S))
11.94/23.28	b(b(x:S)) -> a(c(x:S))
11.94/23.28	c(b(x:S)) -> b(c(x:S))
11.94/23.28	c(b(x:S)) -> c(c(x:S))
11.94/23.28	c(c(x:S)) -> c(b(x:S))
11.94/23.28	)
11.94/23.28	Critical Pairs:
11.94/23.28	<a(a(c(x:S))),b(c(b(x:S)))>   =>  Not trivial, Not overlay, N11
11.94/23.28	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
11.94/23.28	
11.94/23.28	No Convergence InfChecker Processor:
11.94/23.28	Infeasible convergence?
11.94/23.28	YES
11.94/23.28	
11.94/23.28	Problem 1: 
11.94/23.28	
11.94/23.28	Infeasibility Problem:
11.94/23.28	[(VAR vNonEmpty:S vNonEmpty:S:S x:S:S x:S)
11.94/23.28	(STRATEGY CONTEXTSENSITIVE
11.94/23.28	(a 1)
11.94/23.28	(b 1)
11.94/23.28	(c 1)
11.94/23.28	(cx)
11.94/23.28	(fSNonEmpty)
11.94/23.28	)
11.94/23.28	(RULES
11.94/23.28	a(b(x:S:S)) -> b(c(x:S:S))
11.94/23.28	a(c(x:S:S)) -> c(a(x:S:S))
11.94/23.28	b(b(x:S:S)) -> a(c(x:S:S))
11.94/23.28	c(b(x:S:S)) -> b(c(x:S:S))
11.94/23.28	c(b(x:S:S)) -> c(c(x:S:S))
11.94/23.28	c(c(x:S:S)) -> c(b(x:S:S))
11.94/23.28	)]
11.94/23.28	Infeasibility Conditions:
11.94/23.28	a(a(c(cx))) ->* x:S, b(c(b(cx))) ->* x:S
11.94/23.28	
11.94/23.28	Problem 1: 
11.94/23.28	
11.94/23.28	Obtaining a model using Mace4:
11.94/23.28	
11.94/23.28	 -> Usable Rules:
11.94/23.28	a(b(x:S:S)) -> b(c(x:S:S))
11.94/23.28	a(c(x:S:S)) -> c(a(x:S:S))
11.94/23.28	b(b(x:S:S)) -> a(c(x:S:S))
11.94/23.28	c(b(x:S:S)) -> b(c(x:S:S))
11.94/23.28	c(b(x:S:S)) -> c(c(x:S:S))
11.94/23.28	c(c(x:S:S)) -> c(b(x:S:S))
11.94/23.28	
11.94/23.28	 -> Mace4 Output:
11.94/23.28	============================== Mace4 =================================
11.94/23.28	Mace4 (64) version 2009-11A, November 2009.
11.94/23.28	Process 9766 was started by sandbox on n187.star.cs.uiowa.edu,
11.94/23.28	Tue Jul  6 10:42:21 2021
11.94/23.28	The command was "./mace4 -c -f /tmp/mace49749.in".
11.94/23.28	============================== end of head ===========================
11.94/23.28	
11.94/23.28	============================== INPUT =================================
11.94/23.28	
11.94/23.28	% Reading from file /tmp/mace49749.in
11.94/23.28	
11.94/23.28	assign(max_seconds,10).
11.94/23.28	
11.94/23.28	formulas(assumptions).
11.94/23.28	->(x1,y) -> ->(a(x1),a(y)) # label(congruence).
11.94/23.28	->(x1,y) -> ->(b(x1),b(y)) # label(congruence).
11.94/23.28	->(x1,y) -> ->(c(x1),c(y)) # label(congruence).
11.94/23.28	->(a(b(x2)),b(c(x2))) # label(replacement).
11.94/23.28	->(a(c(x2)),c(a(x2))) # label(replacement).
11.94/23.28	->(b(b(x2)),a(c(x2))) # label(replacement).
11.94/23.28	->(c(b(x2)),b(c(x2))) # label(replacement).
11.94/23.28	->(c(b(x2)),c(c(x2))) # label(replacement).
11.94/23.28	->(c(c(x2)),c(b(x2))) # label(replacement).
11.94/23.28	->*(x,x) # label(reflexivity).
11.94/23.28	->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity).
11.94/23.28	end_of_list.
11.94/23.28	
11.94/23.28	formulas(goals).
11.94/23.28	(exists x3 (->*(a(a(c(cx))),x3) & ->*(b(c(b(cx))),x3))) # label(goal).
11.94/23.28	end_of_list.
11.94/23.28	
11.94/23.28	============================== end of input ==========================
11.94/23.28	
11.94/23.28	============================== PROCESS NON-CLAUSAL FORMULAS ==========
11.94/23.28	
11.94/23.28	% Formulas that are not ordinary clauses:
11.94/23.28	1 ->(x1,y) -> ->(a(x1),a(y)) # label(congruence) # label(non_clause).  [assumption].
11.94/23.28	2 ->(x1,y) -> ->(b(x1),b(y)) # label(congruence) # label(non_clause).  [assumption].
11.94/23.28	3 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence) # label(non_clause).  [assumption].
11.94/23.28	4 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause).  [assumption].
11.94/23.28	5 (exists x3 (->*(a(a(c(cx))),x3) & ->*(b(c(b(cx))),x3))) # label(goal) # label(non_clause) # label(goal).  [goal].
11.94/23.28	
11.94/23.28	============================== end of process non-clausal formulas ===
11.94/23.28	
11.94/23.28	============================== CLAUSES FOR SEARCH ====================
11.94/23.28	
11.94/23.28	formulas(mace4_clauses).
11.94/23.28	-->(x,y) | ->(a(x),a(y)) # label(congruence).
11.94/23.28	-->(x,y) | ->(b(x),b(y)) # label(congruence).
11.94/23.28	-->(x,y) | ->(c(x),c(y)) # label(congruence).
11.94/23.28	->(a(b(x)),b(c(x))) # label(replacement).
11.94/23.28	->(a(c(x)),c(a(x))) # label(replacement).
11.94/23.28	->(b(b(x)),a(c(x))) # label(replacement).
11.94/23.28	->(c(b(x)),b(c(x))) # label(replacement).
11.94/23.28	->(c(b(x)),c(c(x))) # label(replacement).
11.94/23.28	->(c(c(x)),c(b(x))) # label(replacement).
11.94/23.28	->*(x,x) # label(reflexivity).
11.94/23.28	-->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity).
11.94/23.28	-->*(a(a(c(cx))),x) | -->*(b(c(b(cx))),x) # label(goal).
11.94/23.28	end_of_list.
11.94/23.28	
11.94/23.28	============================== end of clauses for search =============
11.94/23.28	
11.94/23.28	% There are no natural numbers in the input.
11.94/23.28	
11.94/23.28	============================== DOMAIN SIZE 2 =========================
11.94/23.28	
11.94/23.28	============================== STATISTICS ============================
11.94/23.28	
11.94/23.28	For domain size 2.
11.94/23.28	
11.94/23.28	Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
11.94/23.28	Ground clauses: seen=36, kept=32.
11.94/23.28	Selections=50, assignments=99, propagations=120, current_models=0.
11.94/23.28	Rewrite_terms=1167, rewrite_bools=563, indexes=244.
11.94/23.28	Rules_from_neg_clauses=12, cross_offs=12.
11.94/23.28	
11.94/23.28	============================== end of statistics =====================
11.94/23.28	
11.94/23.28	============================== DOMAIN SIZE 3 =========================
11.94/23.28	
11.94/23.28	============================== STATISTICS ============================
11.94/23.28	
11.94/23.28	For domain size 3.
11.94/23.28	
11.94/23.28	Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds).
11.94/23.28	Ground clauses: seen=78, kept=69.
11.94/23.28	Selections=4207, assignments=11834, propagations=13512, current_models=0.
11.94/23.28	Rewrite_terms=134637, rewrite_bools=92269, indexes=16514.
11.94/23.28	Rules_from_neg_clauses=1176, cross_offs=3791.
11.94/23.28	
11.94/23.28	============================== end of statistics =====================
11.94/23.28	
11.94/23.28	============================== DOMAIN SIZE 4 =========================
11.94/23.28	
11.94/23.28	============================== MODEL =================================
11.94/23.28	
11.94/23.28	interpretation( 4, [number=1, seconds=0], [
11.94/23.28	
11.94/23.28	        function(cx, [ 0 ]),
11.94/23.28	
11.94/23.28	        function(a(_), [ 0, 1, 2, 3 ]),
11.94/23.28	
11.94/23.28	        function(b(_), [ 1, 1, 3, 3 ]),
11.94/23.28	
11.94/23.28	        function(c(_), [ 2, 3, 3, 3 ]),
11.94/23.28	
11.94/23.28	        relation(->*(_,_), [
11.94/23.28				   1, 0, 0, 0,
11.94/23.28				   0, 1, 1, 1,
11.94/23.28				   0, 0, 1, 0,
11.94/23.28				   0, 0, 0, 1 ]),
11.94/23.28	
11.94/23.28	        relation(->(_,_), [
11.94/23.28				   0, 0, 0, 0,
11.94/23.28				   0, 0, 1, 1,
11.94/23.28				   0, 0, 1, 0,
11.94/23.28				   0, 0, 0, 1 ])
11.94/23.28	]).
11.94/23.28	
11.94/23.28	============================== end of model ==========================
11.94/23.28	
11.94/23.28	============================== STATISTICS ============================
11.94/23.28	
11.94/23.28	For domain size 4.
11.94/23.28	
11.94/23.28	Current CPU time: 0.00 seconds (total CPU time: 0.04 seconds).
11.94/23.28	Ground clauses: seen=144, kept=128.
11.94/23.28	Selections=736, assignments=2646, propagations=5856, current_models=1.
11.94/23.29	Rewrite_terms=36976, rewrite_bools=28109, indexes=8538.
11.94/23.29	Rules_from_neg_clauses=894, cross_offs=3204.
11.94/23.29	
11.94/23.29	============================== end of statistics =====================
11.94/23.29	
11.94/23.29	User_CPU=0.04, System_CPU=0.00, Wall_clock=0.
11.94/23.29	
11.94/23.29	Exiting with 1 model.
11.94/23.29	
11.94/23.29	Process 9766 exit (max_models) Tue Jul  6 10:42:21 2021
11.94/23.29	The process finished Tue Jul  6 10:42:21 2021
11.94/23.29	
11.94/23.29	
11.94/23.29	Mace4 cooked interpretation:
11.94/23.29	
11.94/23.29	% number = 1
11.94/23.29	% seconds = 0
11.94/23.29	
11.94/23.29	% Interpretation of size 4
11.94/23.29	
11.94/23.29	cx = 0.
11.94/23.29	
11.94/23.29	a(0) = 0.
11.94/23.29	a(1) = 1.
11.94/23.29	a(2) = 2.
11.94/23.29	a(3) = 3.
11.94/23.29	
11.94/23.29	b(0) = 1.
11.94/23.29	b(1) = 1.
11.94/23.29	b(2) = 3.
11.94/23.29	b(3) = 3.
11.94/23.29	
11.94/23.29	c(0) = 2.
11.94/23.29	c(1) = 3.
11.94/23.29	c(2) = 3.
11.94/23.29	c(3) = 3.
11.94/23.29	
11.94/23.29	  ->*(0,0).
11.94/23.29	- ->*(0,1).
11.94/23.29	- ->*(0,2).
11.94/23.29	- ->*(0,3).
11.94/23.29	- ->*(1,0).
11.94/23.29	  ->*(1,1).
11.94/23.29	  ->*(1,2).
11.94/23.29	  ->*(1,3).
11.94/23.29	- ->*(2,0).
11.94/23.29	- ->*(2,1).
11.94/23.29	  ->*(2,2).
11.94/23.29	- ->*(2,3).
11.94/23.29	- ->*(3,0).
11.94/23.29	- ->*(3,1).
11.94/23.29	- ->*(3,2).
11.94/23.29	  ->*(3,3).
11.94/23.29	
11.94/23.29	- ->(0,0).
11.94/23.29	- ->(0,1).
11.94/23.29	- ->(0,2).
11.94/23.29	- ->(0,3).
11.94/23.29	- ->(1,0).
11.94/23.29	- ->(1,1).
11.94/23.29	  ->(1,2).
11.94/23.29	  ->(1,3).
11.94/23.29	- ->(2,0).
11.94/23.29	- ->(2,1).
11.94/23.29	  ->(2,2).
11.94/23.29	- ->(2,3).
11.94/23.29	- ->(3,0).
11.94/23.29	- ->(3,1).
11.94/23.29	- ->(3,2).
11.94/23.29	  ->(3,3).
11.94/23.29	
11.94/23.29	
11.94/23.29	The problem is infeasible.
11.94/23.29	
11.94/23.29	
11.94/23.29	The problem is not joinable.
11.94/36.11	EOF