35.021/35.021	NO
35.021/35.021	
35.021/35.021	Problem 1:
35.021/35.021	
35.021/35.021	
35.021/35.021	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
35.021/35.021	Confluence Problem:
35.021/35.021	(VAR vNonEmpty:S x:S)
35.021/35.021	(STRATEGY CONTEXTSENSITIVE
35.021/35.021	(p 1)
35.021/35.021	(q 1)
35.021/35.021	(r 1)
35.021/35.021	(s 1)
35.021/35.021	(0)
35.021/35.021	(1)
35.021/35.021	(fSNonEmpty)
35.021/35.021	(h 1)
35.021/35.021	)
35.021/35.021	(RULES
35.021/35.021	p(q(x:S)) -> p(r(x:S))
35.021/35.021	q(h(x:S)) -> r(x:S)
35.021/35.021	r(x:S) -> r(h(x:S)) | s(x:S) ->* 0
35.021/35.021	s(x:S) -> 1
35.021/35.021	)
35.021/35.021	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
35.021/35.021	
35.021/35.021	
35.021/35.021	Problem 1:
35.021/35.021	
35.021/35.021	Inlining of Conditions Processor [STERN17]:
35.021/35.021	
35.021/35.021	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
35.021/35.021	Confluence Problem:
35.021/35.021	(VAR vNonEmpty:S x:S)
35.021/35.021	(STRATEGY CONTEXTSENSITIVE
35.021/35.021	(p 1)
35.021/35.021	(q 1)
35.021/35.021	(r 1)
35.021/35.021	(s 1)
35.021/35.021	(0)
35.021/35.021	(1)
35.021/35.021	(fSNonEmpty)
35.021/35.021	(h 1)
35.021/35.021	)
35.021/35.021	(RULES
35.021/35.021	p(q(x:S)) -> p(r(x:S))
35.021/35.021	q(h(x:S)) -> r(x:S)
35.021/35.021	r(x:S) -> r(h(x:S)) | s(x:S) ->* 0
35.021/35.021	s(x:S) -> 1
35.021/35.021	)
35.021/35.021	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
35.021/35.021	
35.021/35.021	
35.021/35.021	Problem 1:
35.021/35.021	
35.021/35.021	Clean CTRS Processor:
35.021/35.021	
35.021/35.021	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
35.021/35.021	Confluence Problem:
35.021/35.021	(VAR x:S)
35.021/35.021	(STRATEGY CONTEXTSENSITIVE
35.021/35.021	(p 1)
35.021/35.021	(q 1)
35.021/35.021	(r 1)
35.021/35.021	(s 1)
35.021/35.021	(0)
35.021/35.021	(1)
35.021/35.021	(fSNonEmpty)
35.021/35.021	(h 1)
35.021/35.021	)
35.021/35.021	(RULES
35.021/35.021	p(q(x:S)) -> p(r(x:S))
35.021/35.021	q(h(x:S)) -> r(x:S)
35.021/35.021	s(x:S) -> 1
35.021/35.021	)
35.021/35.021	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
35.021/35.021	
35.021/35.021	CRule InfChecker Info:
35.021/35.021	p(q(x:S)) -> p(r(x:S))
35.021/35.021	Rule remains
35.021/35.021	Proof:
35.021/35.021	NO_CONDS
35.021/35.021	
35.021/35.021	CRule InfChecker Info:
35.021/35.021	q(h(x:S)) -> r(x:S)
35.021/35.021	Rule remains
35.021/35.021	Proof:
35.021/35.021	NO_CONDS
35.021/35.021	
35.021/35.021	CRule InfChecker Info:
35.021/35.021	r(x:S) -> r(h(x:S)) | s(x:S) ->* 0
35.021/35.021	Rule deleted
35.021/35.021	Proof:
35.021/35.021	YES
35.021/35.021	
35.021/35.021	Problem 1:
35.021/35.021	
35.021/35.021	Infeasibility Problem:
35.021/35.021	[(VAR vNonEmpty:S vNonEmpty:S:S x:S:S)
35.021/35.021	(STRATEGY CONTEXTSENSITIVE
35.021/35.021	(p 1)
35.021/35.021	(q 1)
35.021/35.021	(r 1)
35.021/35.021	(s 1)
35.021/35.021	(0)
35.021/35.021	(1)
35.021/35.021	(fSNonEmpty)
35.021/35.021	(h 1)
35.021/35.021	)
35.021/35.021	(RULES
35.021/35.021	p(q(x:S:S)) -> p(r(x:S:S))
35.021/35.021	q(h(x:S:S)) -> r(x:S:S)
35.021/35.021	r(x:S:S) -> r(h(x:S:S)) | s(x:S:S) ->* 0
35.021/35.021	s(x:S:S) -> 1
35.021/35.021	)]
35.021/35.021	
35.021/35.021	Infeasibility Conditions:
35.021/35.021	s(x:S:S) ->* 0
35.021/35.021	
35.021/35.021	Problem 1:
35.021/35.021	
35.021/35.021	Obtaining a model using Mace4:
35.021/35.021	
35.021/35.021	 -> Usable Rules:
35.021/35.021	p(q(x:S:S)) -> p(r(x:S:S))
35.021/35.021	q(h(x:S:S)) -> r(x:S:S)
35.021/35.021	r(x:S:S) -> r(h(x:S:S)) | s(x:S:S) ->* 0
35.021/35.021	s(x:S:S) -> 1
35.021/35.021	
35.021/35.021	 -> Mace4 Output:
35.021/35.021	============================== Mace4 =================================
35.021/35.021	Mace4 (64) version 2009-11A, November 2009.
35.021/35.021	Process 97879 was started by ubuntu on ubuntu,
35.021/35.021	Fri Jul 16 14:29:13 2021
35.021/35.021	The command was "./mace4 -c -f /tmp/mace497866-2.in".
35.021/35.021	============================== end of head ===========================
35.021/35.021	
35.021/35.021	============================== INPUT =================================
35.021/35.021	
35.021/35.021	% Reading from file /tmp/mace497866-2.in
35.021/35.021	
35.021/35.021	assign(max_seconds,10).
35.021/35.021	
35.021/35.021	formulas(assumptions).
35.021/35.021	->(x1,y) -> ->(p(x1),p(y)) # label(congruence).
35.021/35.021	->(x1,y) -> ->(q(x1),q(y)) # label(congruence).
35.021/35.021	->(x1,y) -> ->(r(x1),r(y)) # label(congruence).
35.021/35.021	->(x1,y) -> ->(s(x1),s(y)) # label(congruence).
35.021/35.021	->(x1,y) -> ->(h(x1),h(y)) # label(congruence).
35.021/35.021	->(p(q(x2)),p(r(x2))) # label(replacement).
35.021/35.021	->(q(h(x2)),r(x2)) # label(replacement).
35.021/35.021	->*(s(x2),0) -> ->(r(x2),r(h(x2))) # label(replacement).
35.021/35.021	->(s(x2),1) # label(replacement).
35.021/35.021	->*(x,x) # label(reflexivity).
35.021/35.021	->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity).
35.021/35.021	end_of_list.
35.021/35.021	
35.021/35.021	formulas(goals).
35.021/35.021	(exists x2 ->*(s(x2),0)) # label(goal).
35.021/35.021	end_of_list.
35.021/35.021	
35.021/35.021	============================== end of input ==========================
35.021/35.021	
35.021/35.021	============================== PROCESS NON-CLAUSAL FORMULAS ==========
35.021/35.021	
35.021/35.021	% Formulas that are not ordinary clauses:
35.021/35.021	1 ->(x1,y) -> ->(p(x1),p(y)) # label(congruence) # label(non_clause).  [assumption].
35.021/35.021	2 ->(x1,y) -> ->(q(x1),q(y)) # label(congruence) # label(non_clause).  [assumption].
35.021/35.021	3 ->(x1,y) -> ->(r(x1),r(y)) # label(congruence) # label(non_clause).  [assumption].
35.021/35.021	4 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause).  [assumption].
35.021/35.021	5 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence) # label(non_clause).  [assumption].
35.021/35.021	6 ->*(s(x2),0) -> ->(r(x2),r(h(x2))) # label(replacement) # label(non_clause).  [assumption].
35.021/35.021	7 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause).  [assumption].
35.021/35.021	8 (exists x2 ->*(s(x2),0)) # label(goal) # label(non_clause) # label(goal).  [goal].
35.021/35.021	
35.021/35.021	============================== end of process non-clausal formulas ===
35.021/35.021	
35.021/35.021	============================== CLAUSES FOR SEARCH ====================
35.021/35.021	
35.021/35.021	formulas(mace4_clauses).
35.021/35.021	-->(x,y) | ->(p(x),p(y)) # label(congruence).
35.021/35.021	-->(x,y) | ->(q(x),q(y)) # label(congruence).
35.021/35.021	-->(x,y) | ->(r(x),r(y)) # label(congruence).
35.021/35.021	-->(x,y) | ->(s(x),s(y)) # label(congruence).
35.021/35.021	-->(x,y) | ->(h(x),h(y)) # label(congruence).
35.021/35.021	->(p(q(x)),p(r(x))) # label(replacement).
35.021/35.021	->(q(h(x)),r(x)) # label(replacement).
35.021/35.021	-->*(s(x),0) | ->(r(x),r(h(x))) # label(replacement).
35.021/35.021	->(s(x),1) # label(replacement).
35.021/35.021	->*(x,x) # label(reflexivity).
35.021/35.021	-->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity).
35.021/35.021	-->*(s(x),0) # label(goal).
35.021/35.021	end_of_list.
35.021/35.021	
35.021/35.021	============================== end of clauses for search =============
35.021/35.021	
35.021/35.021	% There are no natural numbers in the input.
35.021/35.021	
35.021/35.021	============================== DOMAIN SIZE 2 =========================
35.021/35.021	
35.021/35.021	============================== MODEL =================================
35.021/35.021	
35.021/35.021	interpretation( 2, [number=1, seconds=0], [
35.021/35.021	
35.021/35.021	        function(0, [ 0 ]),
35.021/35.021	
35.021/35.021	        function(1, [ 1 ]),
35.021/35.021	
35.021/35.021	        function(p(_), [ 0, 0 ]),
35.021/35.021	
35.021/35.021	        function(q(_), [ 0, 0 ]),
35.021/35.021	
35.021/35.021	        function(r(_), [ 0, 0 ]),
35.021/35.021	
35.021/35.021	        function(s(_), [ 1, 1 ]),
35.021/35.021	
35.021/35.021	        function(h(_), [ 0, 0 ]),
35.021/35.021	
35.021/35.021	        relation(->*(_,_), [
35.021/35.021				   1, 0,
35.021/35.021				   0, 1 ]),
35.021/35.021	
35.021/35.021	        relation(->(_,_), [
35.021/35.021				   1, 0,
35.021/35.021				   0, 1 ])
35.021/35.021	]).
35.021/35.021	
35.021/35.021	============================== end of model ==========================
35.021/35.021	
35.021/35.021	============================== STATISTICS ============================
35.021/35.021	
35.021/35.021	For domain size 2.
35.021/35.021	
35.021/35.021	Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
35.021/35.021	Ground clauses: seen=40, kept=36.
35.021/35.021	Selections=10, assignments=10, propagations=10, current_models=1.
35.021/35.021	Rewrite_terms=72, rewrite_bools=47, indexes=6.
35.021/35.021	Rules_from_neg_clauses=3, cross_offs=3.
35.021/35.021	
35.021/35.021	============================== end of statistics =====================
35.021/35.021	
35.021/35.021	User_CPU=0.00, System_CPU=0.00, Wall_clock=0.
35.021/35.021	
35.021/35.021	Exiting with 1 model.
35.021/35.021	
35.021/35.021	Process 97879 exit (max_models) Fri Jul 16 14:29:13 2021
35.021/35.021	The process finished Fri Jul 16 14:29:13 2021
35.021/35.021	
35.021/35.021	
35.021/35.021	Mace4 cooked interpretation:
35.021/35.021	
35.021/35.021	
35.021/35.021	
35.021/35.021	The problem is infeasible.
35.021/35.021	
35.021/35.021	
35.021/35.021	CRule InfChecker Info:
35.021/35.021	s(x:S) -> 1
35.021/35.021	Rule remains
35.021/35.021	Proof:
35.021/35.021	NO_CONDS
35.021/35.021	
35.021/35.021	Problem 1:
35.021/35.021	
35.021/35.021	Transform No Conds CTRS Processor:
35.021/35.021	
35.021/35.021	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
35.021/35.021	Confluence Problem:
35.021/35.021	(VAR x:S)
35.021/35.021	(STRATEGY CONTEXTSENSITIVE
35.021/35.021	(p 1)
35.021/35.021	(q 1)
35.021/35.021	(r 1)
35.021/35.021	(s 1)
35.021/35.021	(0)
35.021/35.021	(1)
35.021/35.021	(fSNonEmpty)
35.021/35.021	(h 1)
35.021/35.021	)
35.021/35.021	(RULES
35.021/35.021	p(q(x:S)) -> p(r(x:S))
35.021/35.021	q(h(x:S)) -> r(x:S)
35.021/35.021	s(x:S) -> 1
35.021/35.021	)
35.021/35.021	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
35.021/35.021	Resulting R:
35.021/35.021	(VAR x:S)
35.021/35.021	(STRATEGY CONTEXTSENSITIVE
35.021/35.021	(p 1)
35.021/35.021	(q 1)
35.021/35.021	(r 1)
35.021/35.021	(s 1)
35.021/35.021	(0)
35.021/35.021	(1)
35.021/35.021	(fSNonEmpty)
35.021/35.021	(h 1)
35.021/35.021	)
35.021/35.021	(RULES
35.021/35.021	p(q(x:S)) -> p(r(x:S))
35.021/35.021	q(h(x:S)) -> r(x:S)
35.021/35.021	s(x:S) -> 1
35.021/35.021	)
35.021/35.021	
35.021/35.021	Problem 1:
35.021/35.021	
35.021/35.021	CleanTRS Processor:
35.021/35.021	
35.021/35.021	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
35.021/35.021	Confluence Problem:
35.021/35.021	(VAR x:S)
35.021/35.021	(STRATEGY CONTEXTSENSITIVE
35.021/35.021	(p 1)
35.021/35.021	(q 1)
35.021/35.021	(r 1)
35.021/35.021	(s 1)
35.021/35.021	(0)
35.021/35.021	(1)
35.021/35.021	(fSNonEmpty)
35.021/35.021	(h 1)
35.021/35.021	)
35.021/35.021	(RULES
35.021/35.021	p(q(x:S)) -> p(r(x:S))
35.021/35.021	q(h(x:S)) -> r(x:S)
35.021/35.021	s(x:S) -> 1
35.021/35.021	)
35.021/35.021	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
35.021/35.021	
35.021/35.021	
35.021/35.021	Problem 1:
35.021/35.021	
35.021/35.021	Modular Confluence Combinations Decomposition Processor:
35.021/35.021	
35.021/35.021	TRS combination:
35.021/35.021	{p(q(x:S)) -> p(r(x:S))
35.021/35.021	 q(h(x:S)) -> r(x:S)}
35.021/35.021	{s(x:S) -> 1}
35.021/35.021	Disjoint
35.021/35.021	Constructor-sharing
35.021/35.021	Left linear
35.021/35.021	Layer-preserving
35.021/35.021	TRS1
35.021/35.021	Just (VAR x:S)
35.021/35.021	(STRATEGY CONTEXTSENSITIVE
35.021/35.021	(p 1)
35.021/35.021	(q 1)
35.021/35.021	(r 1)
35.021/35.021	(h 1)
35.021/35.021	)
35.021/35.021	(RULES
35.021/35.021	p(q(x:S)) -> p(r(x:S))
35.021/35.021	q(h(x:S)) -> r(x:S)
35.021/35.021	)
35.021/35.021	
35.021/35.021	TRS2
35.021/35.021	Just (VAR x:S)
35.021/35.021	(STRATEGY CONTEXTSENSITIVE
35.021/35.021	(s 1)
35.021/35.021	(1)
35.021/35.021	)
35.021/35.021	(RULES
35.021/35.021	s(x:S) -> 1
35.021/35.021	)
35.021/35.021	
35.021/35.021	Problem 1:
35.021/35.021	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
35.021/35.021	Confluence Problem:
35.021/35.021	(VAR x:S)
35.021/35.021	(STRATEGY CONTEXTSENSITIVE
35.021/35.021	(p 1)
35.021/35.021	(q 1)
35.021/35.021	(r 1)
35.021/35.021	(h 1)
35.021/35.021	)
35.021/35.021	(RULES
35.021/35.021	p(q(x:S)) -> p(r(x:S))
35.021/35.021	q(h(x:S)) -> r(x:S)
35.021/35.021	)
35.021/35.021	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
35.021/35.021	
35.021/35.021	Huet Levy Processor:
35.021/35.021	-> Rules:
35.021/35.021	 p(q(x:S)) -> p(r(x:S))
35.021/35.021	 q(h(x:S)) -> r(x:S)
35.021/35.021	-> Vars:
35.021/35.021	 x, x
35.021/35.021	-> FVars:
35.021/35.021	 x2, x3
35.021/35.021	-> PVars:
35.021/35.021	 x: [x2, x3]
35.021/35.021	
35.021/35.021	-> Rlps:
35.021/35.021	 (rule: p(q(x2:S)) -> p(r(x2:S)), id: 1, possubterms: p(q(x2:S))->[], q(x2:S)->[1])
35.021/35.021	 (rule: q(h(x3:S)) -> r(x3:S), id: 2, possubterms: q(h(x3:S))->[], h(x3:S)->[1])
35.021/35.021	
35.021/35.021	-> Unifications:
35.021/35.021	(R1 unifies with R2 at p: [1], l: p(q(x2:S)), lp: q(x2:S), sig: {x2:S -> h(x:S)}, l': q(h(x:S)), r: p(r(x2:S)), r': r(x:S))
35.021/35.021	
35.021/35.021	-> Critical pairs info:
35.021/35.021	<p(r(x:S)),p(r(h(x:S)))>   =>  Not trivial, Not overlay, N1
35.021/35.021	
35.021/35.021	-> Problem conclusions:
35.021/35.021	 Left linear, Right linear, Linear
35.021/35.021	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
35.021/35.021	 Not Huet-Levy confluent, Not Newman confluent
35.021/35.021	 R is a TRS
35.021/35.021	
35.021/35.021	
35.021/35.021	Problem 1:
35.021/35.021	Different Normal CP Terms Processor:
35.021/35.021	<p(r(x:S)),p(r(h(x:S)))>   =>  Not trivial, Not overlay, N1, Normal and not trivial cp
35.021/35.021	
35.021/35.021	The problem is not joinable.
35.021/35.021	28.10user 0.58system 0:35.21elapsed 81%CPU (0avgtext+0avgdata 119372maxresident)k
35.021/35.021	6056inputs+0outputs (25major+71076minor)pagefaults 0swaps