65.012/65.012	YES
65.012/65.012	
65.012/65.012	Problem 1:
65.012/65.012	
65.012/65.012	
65.012/65.012	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
65.012/65.012	Confluence Problem:
65.012/65.012	(VAR vNonEmpty x y z)
65.012/65.012	(REPLACEMENT-MAP
65.012/65.012	(F 1, 2, 3)
65.012/65.012	(G 1)
65.012/65.012	(e 1)
65.012/65.012	(f 1, 2)
65.012/65.012	(A)
65.012/65.012	(B)
65.012/65.012	(fSNonEmpty)
65.012/65.012	)
65.012/65.012	(RULES
65.012/65.012	F(x,y,z) -> G(z) | x ->*<- y
65.012/65.012	G(A) -> F(A,B,A)
65.012/65.012	e(x) -> f(x,x)
65.012/65.012	f(x,y) -> x
65.012/65.012	)
65.012/65.012	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
65.012/65.012	
65.012/65.012	
65.012/65.012	Problem 1:
65.012/65.012	
65.012/65.012	Inlining of Conditions Processor [STERN17]:
65.012/65.012	
65.012/65.012	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
65.012/65.012	Confluence Problem:
65.012/65.012	(VAR vNonEmpty x y z)
65.012/65.012	(REPLACEMENT-MAP
65.012/65.012	(F 1, 2, 3)
65.012/65.012	(G 1)
65.012/65.012	(e 1)
65.012/65.012	(f 1, 2)
65.012/65.012	(A)
65.012/65.012	(B)
65.012/65.012	(fSNonEmpty)
65.012/65.012	)
65.012/65.012	(RULES
65.012/65.012	F(x,y,z) -> G(z) | x ->*<- y
65.012/65.012	G(A) -> F(A,B,A)
65.012/65.012	e(x) -> f(x,x)
65.012/65.012	f(x,y) -> x
65.012/65.012	)
65.012/65.012	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
65.012/65.012	
65.012/65.012	
65.012/65.012	Problem 1:
65.012/65.012	
65.012/65.012	Clean CTRS Processor:
65.012/65.012	
65.012/65.012	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
65.012/65.012	Confluence Problem:
65.012/65.012	(VAR x y z)
65.012/65.012	(REPLACEMENT-MAP
65.012/65.012	(F 1, 2, 3)
65.012/65.012	(G 1)
65.012/65.012	(e 1)
65.012/65.012	(f 1, 2)
65.012/65.012	(A)
65.012/65.012	(B)
65.012/65.012	(fSNonEmpty)
65.012/65.012	)
65.012/65.012	(RULES
65.012/65.012	F(x,y,z) -> G(z) | x ->*<- y
65.012/65.012	G(A) -> F(A,B,A)
65.012/65.012	e(x) -> f(x,x)
65.012/65.012	f(x,y) -> x
65.012/65.012	)
65.012/65.012	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
65.012/65.012	
65.012/65.012	CRule InfChecker Info:
65.012/65.012	F(x,y,z) -> G(z) | x ->*<- y
65.012/65.012	Rule remains
65.012/65.012	Proof:
65.012/65.012	NO
65.012/65.012	
65.012/65.012	Problem 1:
65.012/65.012	
65.012/65.012	Infeasibility Problem:
65.012/65.012	[(VAR vNonEmpty x y z vNonEmpty x y)
65.012/65.012	(STRATEGY CONTEXTSENSITIVE
65.012/65.012	(F 1 2 3)
65.012/65.012	(G 1)
65.012/65.012	(e 1)
65.012/65.012	(f 1 2)
65.012/65.012	(A)
65.012/65.012	(B)
65.012/65.012	(fSNonEmpty)
65.012/65.012	)
65.012/65.012	(RULES
65.012/65.012	F(x,y,z) -> G(z) | x ->*<- y
65.012/65.012	G(A) -> F(A,B,A)
65.012/65.012	e(x) -> f(x,x)
65.012/65.012	f(x,y) -> x
65.012/65.012	)]
65.012/65.012	
65.012/65.012	Infeasibility Conditions:
65.012/65.012	x ->*<- y
65.012/65.012	
65.012/65.012	Problem 1:
65.012/65.012	
65.012/65.012	Obtaining a proof using Prover9:
65.012/65.012	
65.012/65.012	 -> Prover9 Output:
65.012/65.012	============================== Prover9 ===============================
65.012/65.012	Prover9 (64) version 2009-11A, November 2009.
65.012/65.012	Process 86088 was started by ubuntu on ubuntu,
65.012/65.012	Wed Mar  9 10:48:27 2022
65.012/65.012	The command was "./prover9 -f /tmp/prover986079-0.in".
65.012/65.012	============================== end of head ===========================
65.012/65.012	
65.012/65.012	============================== INPUT =================================
65.012/65.012	
65.012/65.012	% Reading from file /tmp/prover986079-0.in
65.012/65.012	
65.012/65.012	assign(max_seconds,20).
65.012/65.012	
65.012/65.012	formulas(assumptions).
65.012/65.012	->_s0(x1,y) -> ->_s0(F(x1,x2,x3),F(y,x2,x3)) # label(congruence).
65.012/65.012	->_s0(x2,y) -> ->_s0(F(x1,x2,x3),F(x1,y,x3)) # label(congruence).
65.012/65.012	->_s0(x3,y) -> ->_s0(F(x1,x2,x3),F(x1,x2,y)) # label(congruence).
65.012/65.012	->_s0(x1,y) -> ->_s0(G(x1),G(y)) # label(congruence).
65.012/65.012	->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence).
65.012/65.012	->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence).
65.012/65.012	->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence).
65.012/65.012	->*<-_s0(x1,x2) -> ->_s0(F(x1,x2,x3),G(x3)) # label(replacement).
65.012/65.012	->_s0(G(A),F(A,B,A)) # label(replacement).
65.012/65.012	->_s0(e(x1),f(x1,x1)) # label(replacement).
65.012/65.012	->_s0(f(x1,x2),x1) # label(replacement).
65.012/65.012	->*_s0(x,x) # label(reflexivity).
65.012/65.012	->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity).
65.012/65.012	->*_s0(x,y) & ->*_s0(z,y) -> ->*<-_s0(x,z) # label(joinability).
65.012/65.012	end_of_list.
65.012/65.012	
65.012/65.012	formulas(goals).
65.012/65.012	(exists x5 exists x6 ->*<-_s0(x5,x6)) # label(goal).
65.012/65.012	end_of_list.
65.012/65.012	
65.012/65.012	============================== end of input ==========================
65.012/65.012	
65.012/65.012	============================== PROCESS NON-CLAUSAL FORMULAS ==========
65.012/65.012	
65.012/65.012	% Formulas that are not ordinary clauses:
65.012/65.012	1 ->_s0(x1,y) -> ->_s0(F(x1,x2,x3),F(y,x2,x3)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	2 ->_s0(x2,y) -> ->_s0(F(x1,x2,x3),F(x1,y,x3)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	3 ->_s0(x3,y) -> ->_s0(F(x1,x2,x3),F(x1,x2,y)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	4 ->_s0(x1,y) -> ->_s0(G(x1),G(y)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	5 ->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	6 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	7 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	8 ->*<-_s0(x1,x2) -> ->_s0(F(x1,x2,x3),G(x3)) # label(replacement) # label(non_clause).  [assumption].
65.012/65.012	9 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
65.012/65.012	10 ->*_s0(x,y) & ->*_s0(z,y) -> ->*<-_s0(x,z) # label(joinability) # label(non_clause).  [assumption].
65.012/65.012	11 (exists x5 exists x6 ->*<-_s0(x5,x6)) # label(goal) # label(non_clause) # label(goal).  [goal].
65.012/65.012	
65.012/65.012	============================== end of process non-clausal formulas ===
65.012/65.012	
65.012/65.012	============================== PROCESS INITIAL CLAUSES ===============
65.012/65.012	
65.012/65.012	% Clauses before input processing:
65.012/65.012	
65.012/65.012	formulas(usable).
65.012/65.012	end_of_list.
65.012/65.012	
65.012/65.012	formulas(sos).
65.012/65.012	-->_s0(x,y) | ->_s0(F(x,z,u),F(y,z,u)) # label(congruence).  [clausify(1)].
65.012/65.012	-->_s0(x,y) | ->_s0(F(z,x,u),F(z,y,u)) # label(congruence).  [clausify(2)].
65.012/65.012	-->_s0(x,y) | ->_s0(F(z,u,x),F(z,u,y)) # label(congruence).  [clausify(3)].
65.012/65.012	-->_s0(x,y) | ->_s0(G(x),G(y)) # label(congruence).  [clausify(4)].
65.012/65.012	-->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(5)].
65.012/65.012	-->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence).  [clausify(6)].
65.012/65.012	-->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence).  [clausify(7)].
65.012/65.012	-->*<-_s0(x,y) | ->_s0(F(x,y,z),G(z)) # label(replacement).  [clausify(8)].
65.012/65.012	->_s0(G(A),F(A,B,A)) # label(replacement).  [assumption].
65.012/65.012	->_s0(e(x),f(x,x)) # label(replacement).  [assumption].
65.012/65.012	->_s0(f(x,y),x) # label(replacement).  [assumption].
65.012/65.012	->*_s0(x,x) # label(reflexivity).  [assumption].
65.012/65.012	-->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(9)].
65.012/65.012	-->*_s0(x,y) | -->*_s0(z,y) | ->*<-_s0(x,z) # label(joinability).  [clausify(10)].
65.012/65.012	-->*<-_s0(x,y) # label(goal).  [deny(11)].
65.012/65.012	end_of_list.
65.012/65.012	
65.012/65.012	formulas(demodulators).
65.012/65.012	end_of_list.
65.012/65.012	
65.012/65.012	============================== PREDICATE ELIMINATION =================
65.012/65.012	
65.012/65.012	Eliminating ->*<-_s0/2
65.012/65.012	12 -->*_s0(x,y) | -->*_s0(z,y) | ->*<-_s0(x,z) # label(joinability).  [clausify(10)].
65.012/65.012	13 -->*<-_s0(x,y) | ->_s0(F(x,y,z),G(z)) # label(replacement).  [clausify(8)].
65.012/65.012	Derived: -->*_s0(x,y) | -->*_s0(z,y) | ->_s0(F(x,z,u),G(u)).  [resolve(12,c,13,a)].
65.012/65.012	14 -->*<-_s0(x,y) # label(goal).  [deny(11)].
65.012/65.012	Derived: -->*_s0(x,y) | -->*_s0(z,y).  [resolve(14,a,12,c)].
65.012/65.012	
65.012/65.012	============================== end predicate elimination =============
65.012/65.012	
65.012/65.012	Auto_denials:  (no changes).
65.012/65.012	
65.012/65.012	Term ordering decisions:
65.012/65.012	Predicate symbol precedence:  predicate_order([ ->_s0, ->*_s0 ]).
65.012/65.012	Function symbol precedence:  function_order([ A, B, f, G, e, F ]).
65.012/65.012	After inverse_order:  (no changes).
65.012/65.012	Unfolding symbols: (none).
65.012/65.012	
65.012/65.012	Auto_inference settings:
65.012/65.012	  % set(neg_binary_resolution).  % (HNE depth_diff=-8)
65.012/65.012	  % clear(ordered_res).  % (HNE depth_diff=-8)
65.012/65.012	  % set(ur_resolution).  % (HNE depth_diff=-8)
65.012/65.012	    % set(ur_resolution) -> set(pos_ur_resolution).
65.012/65.012	    % set(ur_resolution) -> set(neg_ur_resolution).
65.012/65.012	
65.012/65.012	Auto_process settings:
65.012/65.012	  % set(unit_deletion).  % (Horn set with negative nonunits)
65.012/65.012	
65.012/65.012	kept:      15 -->_s0(x,y) | ->_s0(F(x,z,u),F(y,z,u)) # label(congruence).  [clausify(1)].
65.012/65.012	kept:      16 -->_s0(x,y) | ->_s0(F(z,x,u),F(z,y,u)) # label(congruence).  [clausify(2)].
65.012/65.012	kept:      17 -->_s0(x,y) | ->_s0(F(z,u,x),F(z,u,y)) # label(congruence).  [clausify(3)].
65.012/65.012	kept:      18 -->_s0(x,y) | ->_s0(G(x),G(y)) # label(congruence).  [clausify(4)].
65.012/65.012	kept:      19 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(5)].
65.012/65.012	kept:      20 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence).  [clausify(6)].
65.012/65.012	kept:      21 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence).  [clausify(7)].
65.012/65.012	kept:      22 ->_s0(G(A),F(A,B,A)) # label(replacement).  [assumption].
65.012/65.012	kept:      23 ->_s0(e(x),f(x,x)) # label(replacement).  [assumption].
65.012/65.012	kept:      24 ->_s0(f(x,y),x) # label(replacement).  [assumption].
65.012/65.012	kept:      25 ->*_s0(x,x) # label(reflexivity).  [assumption].
65.012/65.012	kept:      26 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(9)].
65.012/65.012	kept:      27 -->*_s0(x,y) | -->*_s0(z,y) | ->_s0(F(x,z,u),G(u)).  [resolve(12,c,13,a)].
65.012/65.012	kept:      28 -->*_s0(x,y) | -->*_s0(z,y).  [resolve(14,a,12,c)].
65.012/65.012	
65.012/65.012	============================== end of process initial clauses ========
65.012/65.012	
65.012/65.012	============================== CLAUSES FOR SEARCH ====================
65.012/65.012	
65.012/65.012	% Clauses after input processing:
65.012/65.012	
65.012/65.012	formulas(usable).
65.012/65.012	end_of_list.
65.012/65.012	
65.012/65.012	formulas(sos).
65.012/65.012	15 -->_s0(x,y) | ->_s0(F(x,z,u),F(y,z,u)) # label(congruence).  [clausify(1)].
65.012/65.012	16 -->_s0(x,y) | ->_s0(F(z,x,u),F(z,y,u)) # label(congruence).  [clausify(2)].
65.012/65.012	17 -->_s0(x,y) | ->_s0(F(z,u,x),F(z,u,y)) # label(congruence).  [clausify(3)].
65.012/65.012	18 -->_s0(x,y) | ->_s0(G(x),G(y)) # label(congruence).  [clausify(4)].
65.012/65.012	19 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(5)].
65.012/65.012	20 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence).  [clausify(6)].
65.012/65.012	21 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence).  [clausify(7)].
65.012/65.012	22 ->_s0(G(A),F(A,B,A)) # label(replacement).  [assumption].
65.012/65.012	23 ->_s0(e(x),f(x,x)) # label(replacement).  [assumption].
65.012/65.012	24 ->_s0(f(x,y),x) # label(replacement).  [assumption].
65.012/65.012	25 ->*_s0(x,x) # label(reflexivity).  [assumption].
65.012/65.012	26 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(9)].
65.012/65.012	28 -->*_s0(x,y) | -->*_s0(z,y).  [resolve(14,a,12,c)].
65.012/65.012	end_of_list.
65.012/65.012	
65.012/65.012	formulas(demodulators).
65.012/65.012	end_of_list.
65.012/65.012	
65.012/65.012	============================== end of clauses for search =============
65.012/65.012	
65.012/65.012	============================== SEARCH ================================
65.012/65.012	
65.012/65.012	% Starting search at 0.00 seconds.
65.012/65.012	
65.012/65.012	given #1 (I,wt=12): 15 -->_s0(x,y) | ->_s0(F(x,z,u),F(y,z,u)) # label(congruence).  [clausify(1)].
65.012/65.012	
65.012/65.012	given #2 (I,wt=12): 16 -->_s0(x,y) | ->_s0(F(z,x,u),F(z,y,u)) # label(congruence).  [clausify(2)].
65.012/65.012	
65.012/65.012	given #3 (I,wt=12): 17 -->_s0(x,y) | ->_s0(F(z,u,x),F(z,u,y)) # label(congruence).  [clausify(3)].
65.012/65.012	
65.012/65.012	given #4 (I,wt=8): 18 -->_s0(x,y) | ->_s0(G(x),G(y)) # label(congruence).  [clausify(4)].
65.012/65.012	
65.012/65.012	given #5 (I,wt=8): 19 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(5)].
65.012/65.012	
65.012/65.012	given #6 (I,wt=10): 20 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence).  [clausify(6)].
65.012/65.012	
65.012/65.012	given #7 (I,wt=10): 21 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence).  [clausify(7)].
65.012/65.012	
65.012/65.012	given #8 (I,wt=7): 22 ->_s0(G(A),F(A,B,A)) # label(replacement).  [assumption].
65.012/65.012	
65.012/65.012	given #9 (I,wt=6): 23 ->_s0(e(x),f(x,x)) # label(replacement).  [assumption].
65.012/65.012	
65.012/65.012	given #10 (I,wt=5): 24 ->_s0(f(x,y),x) # label(replacement).  [assumption].
65.012/65.012	
65.012/65.012	given #11 (I,wt=3): 25 ->*_s0(x,x) # label(reflexivity).  [assumption].
65.012/65.012	
65.012/65.012	given #12 (I,wt=9): 26 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(9)].
65.012/65.012	
65.012/65.012	given #13 (I,wt=6): 28 -->*_s0(x,y) | -->*_s0(z,y).  [resolve(14,a,12,c)].
65.012/65.012	
65.012/65.012	============================== PROOF =================================
65.012/65.012	
65.012/65.012	% Proof 1 at 0.00 (+ 0.00) seconds.
65.012/65.012	% Length of proof is 12.
65.012/65.012	% Level of proof is 4.
65.012/65.012	% Maximum clause weight is 9.000.
65.012/65.012	% Given clauses 13.
65.012/65.012	
65.012/65.012	9 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
65.012/65.012	10 ->*_s0(x,y) & ->*_s0(z,y) -> ->*<-_s0(x,z) # label(joinability) # label(non_clause).  [assumption].
65.012/65.012	11 (exists x5 exists x6 ->*<-_s0(x5,x6)) # label(goal) # label(non_clause) # label(goal).  [goal].
65.012/65.012	12 -->*_s0(x,y) | -->*_s0(z,y) | ->*<-_s0(x,z) # label(joinability).  [clausify(10)].
65.012/65.012	14 -->*<-_s0(x,y) # label(goal).  [deny(11)].
65.012/65.012	22 ->_s0(G(A),F(A,B,A)) # label(replacement).  [assumption].
65.012/65.012	25 ->*_s0(x,x) # label(reflexivity).  [assumption].
65.012/65.012	26 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(9)].
65.012/65.012	28 -->*_s0(x,y) | -->*_s0(z,y).  [resolve(14,a,12,c)].
65.012/65.012	52 ->*_s0(G(A),F(A,B,A)).  [ur(26,a,22,a,b,25,a)].
65.012/65.012	53 -->*_s0(x,y).  [resolve(28,a,25,a)].
65.012/65.012	54 $F.  [resolve(53,a,52,a)].
65.012/65.012	
65.012/65.012	============================== end of proof ==========================
65.012/65.012	
65.012/65.012	============================== STATISTICS ============================
65.012/65.012	
65.012/65.012	Given=13. Generated=40. Kept=39. proofs=1.
65.012/65.012	Usable=13. Sos=24. Demods=0. Limbo=0, Disabled=18. Hints=0.
65.012/65.012	Kept_by_rule=0, Deleted_by_rule=0.
65.012/65.012	Forward_subsumed=1. Back_subsumed=1.
65.012/65.012	Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
65.012/65.012	New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
65.012/65.012	Demod_attempts=0. Demod_rewrites=0.
65.012/65.012	Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
65.012/65.012	Nonunit_fsub_feature_tests=5. Nonunit_bsub_feature_tests=22.
65.012/65.012	Megabytes=0.12.
65.012/65.012	User_CPU=0.01, System_CPU=0.00, Wall_clock=0.
65.012/65.012	
65.012/65.012	============================== end of statistics =====================
65.012/65.012	
65.012/65.012	============================== end of search =========================
65.012/65.012	
65.012/65.012	THEOREM PROVED
65.012/65.012	
65.012/65.012	Exiting with 1 proof.
65.012/65.012	
65.012/65.012	Process 86088 exit (max_proofs) Wed Mar  9 10:48:27 2022
65.012/65.012	
65.012/65.012	
65.012/65.012	The problem is feasible.
65.012/65.012	
65.012/65.012	
65.012/65.012	CRule InfChecker Info:
65.012/65.012	G(A) -> F(A,B,A)
65.012/65.012	Rule remains
65.012/65.012	Proof:
65.012/65.012	NO_CONDS
65.012/65.012	
65.012/65.012	CRule InfChecker Info:
65.012/65.012	e(x) -> f(x,x)
65.012/65.012	Rule remains
65.012/65.012	Proof:
65.012/65.012	NO_CONDS
65.012/65.012	
65.012/65.012	CRule InfChecker Info:
65.012/65.012	f(x,y) -> x
65.012/65.012	Rule remains
65.012/65.012	Proof:
65.012/65.012	NO_CONDS
65.012/65.012	
65.012/65.012	Problem 1:
65.012/65.012	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
65.012/65.012	Confluence Problem:
65.012/65.012	(VAR x y z)
65.012/65.012	(REPLACEMENT-MAP
65.012/65.012	(F 1, 2, 3)
65.012/65.012	(G 1)
65.012/65.012	(e 1)
65.012/65.012	(f 1, 2)
65.012/65.012	(A)
65.012/65.012	(B)
65.012/65.012	(fSNonEmpty)
65.012/65.012	)
65.012/65.012	(RULES
65.012/65.012	F(x,y,z) -> G(z) | x ->*<- y
65.012/65.012	G(A) -> F(A,B,A)
65.012/65.012	e(x) -> f(x,x)
65.012/65.012	f(x,y) -> x
65.012/65.012	)
65.012/65.012	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
65.012/65.012	
65.012/65.012	Critical Pairs Processor:
65.012/65.012	-> Rules:
65.012/65.012	F(x,y,z) -> G(z) | x ->*<- y
65.012/65.012	G(A) -> F(A,B,A)
65.012/65.012	e(x) -> f(x,x)
65.012/65.012	f(x,y) -> x
65.012/65.012	-> Vars:
65.012/65.012	"x", "y", "z"
65.012/65.012	
65.012/65.012	-> Rlps:
65.012/65.012	crule: F(x,y,z) -> G(z) | x ->*<- y, id: 1, possubterms: F(x,y,z)-> []
65.012/65.012	crule: G(A) -> F(A,B,A), id: 2, possubterms: G(A)-> [], A-> [1]
65.012/65.012	crule: e(x) -> f(x,x), id: 3, possubterms: e(x)-> []
65.012/65.012	crule: f(x,y) -> x, id: 4, possubterms: f(x,y)-> []
65.012/65.012	
65.012/65.012	-> Unifications:
65.012/65.012	
65.012/65.012	
65.012/65.012	-> Critical pairs info:
65.012/65.012	
65.012/65.012	
65.012/65.012	-> Problem conclusions:
65.012/65.012	 Left linear, Not right linear, Not linear
65.012/65.012	 Weakly orthogonal, Almost orthogonal, Orthogonal
65.012/65.012	 CTRS Type: 1
65.012/65.012	 Deterministic, Strongly deterministic
65.012/65.012	 Not oriented CTRS, Not properly oriented CTRS, Join CTRS, Not semiequational CTRS
65.012/65.012	 Maybe right-stable CTRS, Overlay CTRS
65.012/65.012	 Maybe normal CTRS, Maybe almost normal CTRS
65.012/65.012	 Maybe terminating CTRS, Maybe operational terminating CTRS, Joinable CCPs
65.012/65.012	 Maybe level confluent
65.012/65.012	 Maybe confluent
65.012/65.012	
65.012/65.012	Problem 1:
65.012/65.012	Clean Infeasible CCPs Processor:
65.012/65.012	
65.012/65.012	
65.012/65.012	-> Problem conclusions:
65.012/65.012	 Left linear, Not right linear, Not linear
65.012/65.012	 Weakly orthogonal, Almost orthogonal, Orthogonal
65.012/65.012	 CTRS Type: 1
65.012/65.012	 Deterministic, Strongly deterministic
65.012/65.012	 Not oriented CTRS, Not properly oriented CTRS, Join CTRS, Not semiequational CTRS
65.012/65.012	 Maybe right-stable CTRS, Overlay CTRS
65.012/65.012	 Maybe normal CTRS, Maybe almost normal CTRS
65.012/65.012	 Maybe terminating CTRS, Maybe operational terminating CTRS, Joinable CCPs
65.012/65.012	 Maybe level confluent
65.012/65.012	 Maybe confluent
65.012/65.012	
65.012/65.012	Resulting CCPs:
65.012/65.012	No CCPs left
65.012/65.012	
65.012/65.012	Problem 1:
65.012/65.012	Operation Termination Processor:
65.012/65.012	Operational terminating?
65.012/65.012	YES
65.012/65.012	
65.012/65.012	Problem 1:
65.012/65.012	
65.012/65.012	(VAR vu95NonEmpty z1 x y z)
65.012/65.012	(RULES
65.012/65.012	F(x,y,z) -> G(z) | x ->* z1, y ->* z1
65.012/65.012	G(A) -> F(A,B,A)
65.012/65.012	e(x) -> f(x,x)
65.012/65.012	f(x,y) -> x
65.012/65.012	)
65.012/65.012	
65.012/65.012	Problem 1:
65.012/65.012	Valid CTRS Processor:
65.012/65.012	-> Rules:
65.012/65.012	 F(x,y,z) -> G(z) | x ->* z1, y ->* z1
65.012/65.012	 G(A) -> F(A,B,A)
65.012/65.012	 e(x) -> f(x,x)
65.012/65.012	 f(x,y) -> x
65.012/65.012	-> The system is a deterministic 3-CTRS.
65.012/65.012	
65.012/65.012	Problem 1:
65.012/65.012	
65.012/65.012	2D Dependency Pair Processor:
65.012/65.012	
65.012/65.012	Conditional Termination Problem 1:
65.012/65.012	-> Pairs:
65.012/65.012	 FSharp(x,y,z) -> GSharp(z) | x ->* z1, y ->* z1
65.012/65.012	 GSharp(A) -> FSharp(A,B,A)
65.012/65.012	 E(x) -> fSharp(x,x)
65.012/65.012	-> QPairs:
65.012/65.012	 Empty
65.012/65.012	-> Rules:
65.012/65.012	 F(x,y,z) -> G(z) | x ->* z1, y ->* z1
65.012/65.012	 G(A) -> F(A,B,A)
65.012/65.012	 e(x) -> f(x,x)
65.012/65.012	 f(x,y) -> x
65.012/65.012	
65.012/65.012	Conditional Termination Problem 2:
65.012/65.012	-> Pairs:
65.012/65.012	 Empty
65.012/65.012	-> QPairs:
65.012/65.012	 Empty
65.012/65.012	-> Rules:
65.012/65.012	 F(x,y,z) -> G(z) | x ->* z1, y ->* z1
65.012/65.012	 G(A) -> F(A,B,A)
65.012/65.012	 e(x) -> f(x,x)
65.012/65.012	 f(x,y) -> x
65.012/65.012	
65.012/65.012	
65.012/65.012	The problem is decomposed in 2 subproblems.
65.012/65.012	
65.012/65.012	Problem 1.1:
65.012/65.012	
65.012/65.012	SCC Processor:
65.012/65.012	-> Pairs:
65.012/65.012	 FSharp(x,y,z) -> GSharp(z) | x ->* z1, y ->* z1
65.012/65.012	 GSharp(A) -> FSharp(A,B,A)
65.012/65.012	 E(x) -> fSharp(x,x)
65.012/65.012	-> QPairs:
65.012/65.012	 Empty
65.012/65.012	-> Rules:
65.012/65.012	 F(x,y,z) -> G(z) | x ->* z1, y ->* z1
65.012/65.012	 G(A) -> F(A,B,A)
65.012/65.012	 e(x) -> f(x,x)
65.012/65.012	 f(x,y) -> x
65.012/65.012	->Strongly Connected Components:
65.012/65.012	->->Cycle:
65.012/65.012	->->-> Pairs:
65.012/65.012	 FSharp(x,y,z) -> GSharp(z) | x ->* z1, y ->* z1
65.012/65.012	 GSharp(A) -> FSharp(A,B,A)
65.012/65.012	-> QPairs:
65.012/65.012	 Empty
65.012/65.012	->->-> Rules:
65.012/65.012	 F(x,y,z) -> G(z) | x ->* z1, y ->* z1
65.012/65.012	 G(A) -> F(A,B,A)
65.012/65.012	 e(x) -> f(x,x)
65.012/65.012	 f(x,y) -> x
65.012/65.012	
65.012/65.012	Problem 1.1:
65.012/65.012	
65.012/65.012	Semantic Removal Triple Processor:
65.012/65.012	-> Pairs:
65.012/65.012	 FSharp(x,y,z) -> GSharp(z) | x ->* z1, y ->* z1
65.012/65.012	 GSharp(A) -> FSharp(A,B,A)
65.012/65.012	-> Rules:
65.012/65.012	 F(x,y,z) -> G(z) | x ->* z1, y ->* z1
65.012/65.012	 G(A) -> F(A,B,A)
65.012/65.012	 e(x) -> f(x,x)
65.012/65.012	 f(x,y) -> x
65.012/65.012	-> Needed rules:
65.012/65.012	 Empty
65.012/65.012	-> Usable rules:
65.012/65.012	 Empty
65.012/65.012	->Mace4 Output:
65.012/65.012	 ============================== Mace4 =================================
65.012/65.012	Mace4 (64) version 2009-11A, November 2009.
65.012/65.012	Process 86221 was started by ubuntu on ubuntu,
65.012/65.012	Wed Mar  9 10:48:27 2022
65.012/65.012	The command was "./mace4 -c -f /tmp/mace486132-4.in".
65.012/65.012	============================== end of head ===========================
65.012/65.012	
65.012/65.012	============================== INPUT =================================
65.012/65.012	
65.012/65.012	% Reading from file /tmp/mace486132-4.in
65.012/65.012	
65.012/65.012	assign(max_seconds,20).
65.012/65.012	
65.012/65.012	formulas(assumptions).
65.012/65.012	arrowStar_s0(x,x) # label(reflexivity).
65.012/65.012	arrow_s0(x,y) & arrowStar_s0(y,z) -> arrowStar_s0(x,z) # label(compatibility).
65.012/65.012	gtrsim_s0(x,y) & sqsupset_s0(y,z) -> sqsupset_s0(x,z) # label(compatibility).
65.012/65.012	succeq_s0(x,y) & sqsupset_s0(y,z) -> sqsupset_s0(x,z) # label(compatibility).
65.012/65.012	gtrsim_s0(x,y) & succeq_s0(y,z) -> gtrsim_s0(x,z) # label(compatibility).
65.012/65.012	arrow_s0(x1,y) -> arrow_s0(f2(x1,x2,x3),f2(y,x2,x3)) # label(congruence).
65.012/65.012	arrow_s0(x2,y) -> arrow_s0(f2(x1,x2,x3),f2(x1,y,x3)) # label(congruence).
65.012/65.012	arrow_s0(x3,y) -> arrow_s0(f2(x1,x2,x3),f2(x1,x2,y)) # label(congruence).
65.012/65.012	arrow_s0(x1,y) -> arrow_s0(f3(x1),f3(y)) # label(congruence).
65.012/65.012	arrow_s0(x1,y) -> arrow_s0(f4(x1),f4(y)) # label(congruence).
65.012/65.012	arrow_s0(x1,y) -> arrow_s0(f5(x1,x2),f5(y,x2)) # label(congruence).
65.012/65.012	arrow_s0(x2,y) -> arrow_s0(f5(x1,x2),f5(x1,y)) # label(congruence).
65.012/65.012	arrow_s0(x1,y) -> arrow_s0(f15(x1,x2),f15(y,x2)) # label(congruence).
65.012/65.012	arrow_s0(x2,y) -> arrow_s0(f15(x1,x2),f15(x1,y)) # label(congruence).
65.012/65.012	arrowN_s0(x1,y) -> arrowN_s0(f2(x1,x2,x3),f2(y,x2,x3)) # label(congruence).
65.012/65.012	arrowN_s0(x2,y) -> arrowN_s0(f2(x1,x2,x3),f2(x1,y,x3)) # label(congruence).
65.012/65.012	arrowN_s0(x3,y) -> arrowN_s0(f2(x1,x2,x3),f2(x1,x2,y)) # label(congruence).
65.012/65.012	arrowN_s0(x1,y) -> arrowN_s0(f3(x1),f3(y)) # label(congruence).
65.012/65.012	arrowN_s0(x1,y) -> arrowN_s0(f4(x1),f4(y)) # label(congruence).
65.012/65.012	arrowN_s0(x1,y) -> arrowN_s0(f5(x1,x2),f5(y,x2)) # label(congruence).
65.012/65.012	arrowN_s0(x2,y) -> arrowN_s0(f5(x1,x2),f5(x1,y)) # label(congruence).
65.012/65.012	arrowN_s0(x1,y) -> arrowN_s0(f11(x1,x2,x3),f11(y,x2,x3)) # label(congruence).
65.012/65.012	arrowN_s0(x2,y) -> arrowN_s0(f11(x1,x2,x3),f11(x1,y,x3)) # label(congruence).
65.012/65.012	arrowN_s0(x3,y) -> arrowN_s0(f11(x1,x2,x3),f11(x1,x2,y)) # label(congruence).
65.012/65.012	arrowN_s0(x1,y) -> arrowN_s0(f12(x1),f12(y)) # label(congruence).
65.012/65.012	arrowN_s0(x1,y) -> arrowN_s0(f13(x1),f13(y)) # label(congruence).
65.012/65.012	arrowN_s0(x1,y) -> arrowN_s0(f14(x1,x2),f14(y,x2)) # label(congruence).
65.012/65.012	arrowN_s0(x2,y) -> arrowN_s0(f14(x1,x2),f14(x1,y)) # label(congruence).
65.012/65.012	arrowN_s0(x1,y) -> arrowN_s0(f15(x1,x2),f15(y,x2)) # label(congruence).
65.012/65.012	arrowN_s0(x2,y) -> arrowN_s0(f15(x1,x2),f15(x1,y)) # label(congruence).
65.012/65.012	arrow_s0(f15(x5,x6),x5) # label(replacement).
65.012/65.012	arrow_s0(f15(x5,x6),x6) # label(replacement).
65.012/65.012	arrowN_s0(f15(x5,x6),x5) # label(replacement).
65.012/65.012	arrowN_s0(f15(x5,x6),x6) # label(replacement).
65.012/65.012	arrowN_s0(x,y) -> gtrsim_s0(x,y) # label(inclusion).
65.012/65.012	arrowStar_s0(x2,x1) & arrowStar_s0(x3,x1) -> sqsupset_s0(f11(x2,x3,x4),f12(x4)) # label(replacement).
65.012/65.012	succeq_s0(f12(f6),f11(f6,f7,f6)) # label(replacement).
65.012/65.012	sqsupset_s0(x,y) -> sqsupsetStar_s0(x,y) # label(inclusion).
65.012/65.012	sqsupset_s0(x,y) & sqsupsetStar_s0(y,z) -> sqsupsetStar_s0(x,z) # label(compatibility).
65.012/65.012	end_of_list.
65.012/65.012	
65.012/65.012	formulas(goals).
65.012/65.012	(exists x sqsupsetStar_s0(x,x)) # label(wellfoundedness).
65.012/65.012	end_of_list.
65.012/65.012	
65.012/65.012	============================== end of input ==========================
65.012/65.012	
65.012/65.012	============================== PROCESS NON-CLAUSAL FORMULAS ==========
65.012/65.012	
65.012/65.012	% Formulas that are not ordinary clauses:
65.012/65.012	1 arrow_s0(x,y) & arrowStar_s0(y,z) -> arrowStar_s0(x,z) # label(compatibility) # label(non_clause).  [assumption].
65.012/65.012	2 gtrsim_s0(x,y) & sqsupset_s0(y,z) -> sqsupset_s0(x,z) # label(compatibility) # label(non_clause).  [assumption].
65.012/65.012	3 succeq_s0(x,y) & sqsupset_s0(y,z) -> sqsupset_s0(x,z) # label(compatibility) # label(non_clause).  [assumption].
65.012/65.012	4 gtrsim_s0(x,y) & succeq_s0(y,z) -> gtrsim_s0(x,z) # label(compatibility) # label(non_clause).  [assumption].
65.012/65.012	5 arrow_s0(x1,y) -> arrow_s0(f2(x1,x2,x3),f2(y,x2,x3)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	6 arrow_s0(x2,y) -> arrow_s0(f2(x1,x2,x3),f2(x1,y,x3)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	7 arrow_s0(x3,y) -> arrow_s0(f2(x1,x2,x3),f2(x1,x2,y)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	8 arrow_s0(x1,y) -> arrow_s0(f3(x1),f3(y)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	9 arrow_s0(x1,y) -> arrow_s0(f4(x1),f4(y)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	10 arrow_s0(x1,y) -> arrow_s0(f5(x1,x2),f5(y,x2)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	11 arrow_s0(x2,y) -> arrow_s0(f5(x1,x2),f5(x1,y)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	12 arrow_s0(x1,y) -> arrow_s0(f15(x1,x2),f15(y,x2)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	13 arrow_s0(x2,y) -> arrow_s0(f15(x1,x2),f15(x1,y)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	14 arrowN_s0(x1,y) -> arrowN_s0(f2(x1,x2,x3),f2(y,x2,x3)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	15 arrowN_s0(x2,y) -> arrowN_s0(f2(x1,x2,x3),f2(x1,y,x3)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	16 arrowN_s0(x3,y) -> arrowN_s0(f2(x1,x2,x3),f2(x1,x2,y)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	17 arrowN_s0(x1,y) -> arrowN_s0(f3(x1),f3(y)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	18 arrowN_s0(x1,y) -> arrowN_s0(f4(x1),f4(y)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	19 arrowN_s0(x1,y) -> arrowN_s0(f5(x1,x2),f5(y,x2)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	20 arrowN_s0(x2,y) -> arrowN_s0(f5(x1,x2),f5(x1,y)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	21 arrowN_s0(x1,y) -> arrowN_s0(f11(x1,x2,x3),f11(y,x2,x3)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	22 arrowN_s0(x2,y) -> arrowN_s0(f11(x1,x2,x3),f11(x1,y,x3)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	23 arrowN_s0(x3,y) -> arrowN_s0(f11(x1,x2,x3),f11(x1,x2,y)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	24 arrowN_s0(x1,y) -> arrowN_s0(f12(x1),f12(y)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	25 arrowN_s0(x1,y) -> arrowN_s0(f13(x1),f13(y)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	26 arrowN_s0(x1,y) -> arrowN_s0(f14(x1,x2),f14(y,x2)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	27 arrowN_s0(x2,y) -> arrowN_s0(f14(x1,x2),f14(x1,y)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	28 arrowN_s0(x1,y) -> arrowN_s0(f15(x1,x2),f15(y,x2)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	29 arrowN_s0(x2,y) -> arrowN_s0(f15(x1,x2),f15(x1,y)) # label(congruence) # label(non_clause).  [assumption].
65.012/65.012	30 arrowN_s0(x,y) -> gtrsim_s0(x,y) # label(inclusion) # label(non_clause).  [assumption].
65.012/65.012	31 arrowStar_s0(x2,x1) & arrowStar_s0(x3,x1) -> sqsupset_s0(f11(x2,x3,x4),f12(x4)) # label(replacement) # label(non_clause).  [assumption].
65.012/65.012	32 sqsupset_s0(x,y) -> sqsupsetStar_s0(x,y) # label(inclusion) # label(non_clause).  [assumption].
65.012/65.012	33 sqsupset_s0(x,y) & sqsupsetStar_s0(y,z) -> sqsupsetStar_s0(x,z) # label(compatibility) # label(non_clause).  [assumption].
65.012/65.012	34 (exists x sqsupsetStar_s0(x,x)) # label(wellfoundedness) # label(non_clause) # label(goal).  [goal].
65.012/65.012	
65.012/65.012	============================== end of process non-clausal formulas ===
65.012/65.012	
65.012/65.012	============================== CLAUSES FOR SEARCH ====================
65.012/65.012	
65.012/65.012	formulas(mace4_clauses).
65.012/65.012	arrowStar_s0(x,x) # label(reflexivity).
65.012/65.012	-arrow_s0(x,y) | -arrowStar_s0(y,z) | arrowStar_s0(x,z) # label(compatibility).
65.012/65.012	-gtrsim_s0(x,y) | -sqsupset_s0(y,z) | sqsupset_s0(x,z) # label(compatibility).
65.012/65.012	-succeq_s0(x,y) | -sqsupset_s0(y,z) | sqsupset_s0(x,z) # label(compatibility).
65.012/65.012	-gtrsim_s0(x,y) | -succeq_s0(y,z) | gtrsim_s0(x,z) # label(compatibility).
65.012/65.012	-arrow_s0(x,y) | arrow_s0(f2(x,z,u),f2(y,z,u)) # label(congruence).
65.012/65.012	-arrow_s0(x,y) | arrow_s0(f2(z,x,u),f2(z,y,u)) # label(congruence).
65.012/65.012	-arrow_s0(x,y) | arrow_s0(f2(z,u,x),f2(z,u,y)) # label(congruence).
65.012/65.012	-arrow_s0(x,y) | arrow_s0(f3(x),f3(y)) # label(congruence).
65.012/65.012	-arrow_s0(x,y) | arrow_s0(f4(x),f4(y)) # label(congruence).
65.012/65.012	-arrow_s0(x,y) | arrow_s0(f5(x,z),f5(y,z)) # label(congruence).
65.012/65.012	-arrow_s0(x,y) | arrow_s0(f5(z,x),f5(z,y)) # label(congruence).
65.012/65.012	-arrow_s0(x,y) | arrow_s0(f15(x,z),f15(y,z)) # label(congruence).
65.012/65.012	-arrow_s0(x,y) | arrow_s0(f15(z,x),f15(z,y)) # label(congruence).
65.012/65.012	-arrowN_s0(x,y) | arrowN_s0(f2(x,z,u),f2(y,z,u)) # label(congruence).
65.012/65.012	-arrowN_s0(x,y) | arrowN_s0(f2(z,x,u),f2(z,y,u)) # label(congruence).
65.012/65.012	-arrowN_s0(x,y) | arrowN_s0(f2(z,u,x),f2(z,u,y)) # label(congruence).
65.012/65.012	-arrowN_s0(x,y) | arrowN_s0(f3(x),f3(y)) # label(congruence).
65.012/65.012	-arrowN_s0(x,y) | arrowN_s0(f4(x),f4(y)) # label(congruence).
65.012/65.012	-arrowN_s0(x,y) | arrowN_s0(f5(x,z),f5(y,z)) # label(congruence).
65.012/65.012	-arrowN_s0(x,y) | arrowN_s0(f5(z,x),f5(z,y)) # label(congruence).
65.012/65.012	-arrowN_s0(x,y) | arrowN_s0(f11(x,z,u),f11(y,z,u)) # label(congruence).
65.012/65.012	-arrowN_s0(x,y) | arrowN_s0(f11(z,x,u),f11(z,y,u)) # label(congruence).
65.012/65.012	-arrowN_s0(x,y) | arrowN_s0(f11(z,u,x),f11(z,u,y)) # label(congruence).
65.012/65.012	-arrowN_s0(x,y) | arrowN_s0(f12(x),f12(y)) # label(congruence).
65.012/65.012	-arrowN_s0(x,y) | arrowN_s0(f13(x),f13(y)) # label(congruence).
65.012/65.012	-arrowN_s0(x,y) | arrowN_s0(f14(x,z),f14(y,z)) # label(congruence).
65.012/65.012	-arrowN_s0(x,y) | arrowN_s0(f14(z,x),f14(z,y)) # label(congruence).
65.012/65.012	-arrowN_s0(x,y) | arrowN_s0(f15(x,z),f15(y,z)) # label(congruence).
65.012/65.012	-arrowN_s0(x,y) | arrowN_s0(f15(z,x),f15(z,y)) # label(congruence).
65.012/65.012	arrow_s0(f15(x,y),x) # label(replacement).
65.012/65.012	arrow_s0(f15(x,y),y) # label(replacement).
65.012/65.012	arrowN_s0(f15(x,y),x) # label(replacement).
65.012/65.012	arrowN_s0(f15(x,y),y) # label(replacement).
65.012/65.012	-arrowN_s0(x,y) | gtrsim_s0(x,y) # label(inclusion).
65.012/65.012	-arrowStar_s0(x,y) | -arrowStar_s0(z,y) | sqsupset_s0(f11(x,z,u),f12(u)) # label(replacement).
65.012/65.012	succeq_s0(f12(f6),f11(f6,f7,f6)) # label(replacement).
65.012/65.012	-sqsupset_s0(x,y) | sqsupsetStar_s0(x,y) # label(inclusion).
65.012/65.012	-sqsupset_s0(x,y) | -sqsupsetStar_s0(y,z) | sqsupsetStar_s0(x,z) # label(compatibility).
65.012/65.012	-sqsupsetStar_s0(x,x) # label(wellfoundedness).
65.012/65.012	end_of_list.
65.012/65.012	
65.012/65.012	============================== end of clauses for search =============
65.012/65.012	
65.012/65.012	% There are no natural numbers in the input.
65.012/65.012	
65.012/65.012	============================== DOMAIN SIZE 2 =========================
65.012/65.012	
65.012/65.012	============================== STATISTICS ============================
65.012/65.012	
65.012/65.012	For domain size 2.
65.012/65.012	
65.012/65.012	Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
65.012/65.012	Ground clauses: seen=333, kept=329.
65.012/65.012	Selections=4, assignments=7, propagations=48, current_models=0.
65.012/65.012	Rewrite_terms=157, rewrite_bools=274, indexes=37.
65.012/65.012	Rules_from_neg_clauses=12, cross_offs=12.
65.012/65.012	
65.012/65.012	============================== end of statistics =====================
65.012/65.012	
65.012/65.012	============================== DOMAIN SIZE 3 =========================
65.012/65.012	
65.012/65.012	============================== MODEL =================================
65.012/65.012	
65.012/65.012	interpretation( 3, [number=1, seconds=0], [
65.012/65.012	
65.012/65.012	        function(f6, [ 0 ]),
65.012/65.012	
65.012/65.012	        function(f7, [ 1 ]),
65.012/65.012	
65.012/65.012	        function(f12(_), [ 0, 0, 0 ]),
65.012/65.012	
65.012/65.012	        function(f13(_), [ 0, 0, 0 ]),
65.012/65.012	
65.012/65.012	        function(f3(_), [ 0, 0, 0 ]),
65.012/65.012	
65.012/65.012	        function(f4(_), [ 0, 0, 0 ]),
65.012/65.012	
65.012/65.012	        function(f14(_,_), [
65.012/65.012				   0, 0, 0,
65.012/65.012				   0, 0, 0,
65.012/65.012				   0, 0, 0 ]),
65.012/65.012	
65.012/65.012	        function(f15(_,_), [
65.012/65.012				   0, 2, 2,
65.012/65.012				   2, 1, 2,
65.012/65.012				   2, 2, 2 ]),
65.012/65.012	
65.012/65.012	        function(f5(_,_), [
65.012/65.012				   0, 0, 0,
65.012/65.012				   0, 0, 0,
65.012/65.012				   0, 0, 0 ]),
65.012/65.012	
65.012/65.012	        function(f11(_,_,_), [
65.012/65.012				   1, 1, 1,
65.012/65.012				   0, 0, 0,
65.012/65.012				   2, 2, 2,
65.012/65.012				   1, 1, 1,
65.012/65.012				   1, 1, 1,
65.012/65.012				   1, 1, 1,
65.012/65.012				   1, 1, 1,
65.012/65.012				   2, 2, 2,
65.012/65.012				   2, 2, 2 ]),
65.012/65.012	
65.012/65.012	        function(f2(_,_,_), [
65.012/65.012				   0, 0, 0,
65.012/65.012				   0, 0, 0,
65.012/65.012				   0, 0, 0,
65.012/65.012				   0, 0, 0,
65.012/65.012				   0, 0, 0,
65.012/65.012				   0, 0, 0,
65.012/65.012				   0, 0, 0,
65.012/65.012				   0, 0, 0,
65.012/65.012				   0, 0, 0 ]),
65.012/65.012	
65.012/65.012	        relation(arrowN_s0(_,_), [
65.012/65.012				   1, 0, 0,
65.012/65.012				   0, 1, 0,
65.012/65.012				   1, 1, 1 ]),
65.012/65.012	
65.012/65.012	        relation(arrowStar_s0(_,_), [
65.012/65.012				   1, 0, 0,
65.012/65.012				   0, 1, 0,
65.012/65.012				   1, 1, 1 ]),
65.012/65.012	
65.012/65.012	        relation(arrow_s0(_,_), [
65.012/65.012				   1, 0, 0,
65.012/65.012				   0, 1, 0,
65.012/65.012				   1, 1, 1 ]),
65.012/65.012	
65.012/65.012	        relation(gtrsim_s0(_,_), [
65.012/65.012				   1, 0, 0,
65.012/65.012				   0, 1, 0,
65.012/65.012				   1, 1, 1 ]),
65.012/65.012	
65.012/65.012	        relation(sqsupsetStar_s0(_,_), [
65.012/65.012				   0, 0, 0,
65.012/65.012				   1, 0, 0,
65.012/65.012				   1, 0, 0 ]),
65.012/65.012	
65.012/65.012	        relation(sqsupset_s0(_,_), [
65.012/65.012				   0, 0, 0,
65.012/65.012				   1, 0, 0,
65.012/65.012				   1, 0, 0 ]),
65.012/65.012	
65.012/65.012	        relation(succeq_s0(_,_), [
65.012/65.012				   1, 0, 0,
65.012/65.012				   0, 0, 0,
65.012/65.012				   0, 0, 0 ])
65.012/65.012	]).
65.012/65.012	
65.012/65.012	============================== end of model ==========================
65.012/65.012	
65.012/65.012	============================== STATISTICS ============================
65.012/65.012	
65.012/65.012	For domain size 3.
65.012/65.012	
65.012/65.012	Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
65.012/65.012	Ground clauses: seen=1330, kept=1321.
65.012/65.012	Selections=71, assignments=92, propagations=131, current_models=1.
65.012/65.012	Rewrite_terms=2542, rewrite_bools=2147, indexes=68.
65.012/65.012	Rules_from_neg_clauses=38, cross_offs=130.
65.012/65.012	
65.012/65.012	============================== end of statistics =====================
65.012/65.012	
65.012/65.012	User_CPU=0.01, System_CPU=0.00, Wall_clock=0.
65.012/65.012	
65.012/65.012	Exiting with 1 model.
65.012/65.012	
65.012/65.012	Process 86221 exit (max_models) Wed Mar  9 10:48:27 2022
65.012/65.012	The process finished Wed Mar  9 10:48:27 2022
65.012/65.012	
65.012/65.012	
65.012/65.012	Mace4 cooked interpretation:
65.012/65.012	
65.012/65.012	
65.012/65.012	
65.012/65.012	Problem 1.1:
65.012/65.012	
65.012/65.012	SCC Processor:
65.012/65.012	-> Pairs:
65.012/65.012	 GSharp(A) -> FSharp(A,B,A)
65.012/65.012	-> QPairs:
65.012/65.012	 Empty
65.012/65.012	-> Rules:
65.012/65.012	 F(x,y,z) -> G(z) | x ->* z1, y ->* z1
65.012/65.012	 G(A) -> F(A,B,A)
65.012/65.012	 e(x) -> f(x,x)
65.012/65.012	 f(x,y) -> x
65.012/65.012	->Strongly Connected Components:
65.012/65.012	 There is no strongly connected component
65.012/65.012	
65.012/65.012	The problem is finite.
65.012/65.012	
65.012/65.012	Problem 1.2:
65.012/65.012	
65.012/65.012	SCC Processor:
65.012/65.012	-> Pairs:
65.012/65.012	 Empty
65.012/65.012	-> QPairs:
65.012/65.012	 Empty
65.012/65.012	-> Rules:
65.012/65.012	 F(x,y,z) -> G(z) | x ->* z1, y ->* z1
65.012/65.012	 G(A) -> F(A,B,A)
65.012/65.012	 e(x) -> f(x,x)
65.012/65.012	 f(x,y) -> x
65.012/65.012	->Strongly Connected Components:
65.012/65.012	 There is no strongly connected component
65.012/65.012	
65.012/65.012	The problem is finite.
65.012/65.012	
65.012/65.012	
65.012/65.012	-> Problem conclusions:
65.012/65.012	 Left linear, Not right linear, Not linear
65.012/65.012	 Weakly orthogonal, Almost orthogonal, Orthogonal
65.012/65.012	 CTRS Type: 1
65.012/65.012	 Deterministic, Strongly deterministic
65.012/65.012	 Not oriented CTRS, Not properly oriented CTRS, Join CTRS, Not semiequational CTRS
65.012/65.012	 Maybe right-stable CTRS, Overlay CTRS
65.012/65.012	 Maybe normal CTRS, Maybe almost normal CTRS
65.012/65.012	 Terminating CTRS, Operational terminating CTRS, Joinable CCPs
65.012/65.012	 Maybe level confluent
65.012/65.012	 Confluent
65.012/65.012	
65.012/65.012	The problem is joinable.
65.012/65.012	30.12user 0.74system 1:05.12elapsed 47%CPU (0avgtext+0avgdata 116892maxresident)k
65.012/65.012	0inputs+0outputs (0major+82374minor)pagefaults 0swaps