0.009/0.009	YES
0.009/0.009	
0.009/0.009	Problem 1:
0.009/0.009	
0.009/0.009	
0.009/0.009	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.009/0.009	Confluence Problem:
0.009/0.009	(VAR vNonEmpty:S x:S x':S x'':S y:S)
0.009/0.009	(STRATEGY CONTEXTSENSITIVE
0.009/0.009	(f 1 2)
0.009/0.009	(h 1 2 3)
0.009/0.009	(c)
0.009/0.009	(fSNonEmpty)
0.009/0.009	(g 1 2)
0.009/0.009	)
0.009/0.009	(RULES
0.009/0.009	f(x:S,x':S) -> g(y:S,y:S) | x:S ->* y:S, x':S ->* y:S
0.009/0.009	h(x:S,x':S,x'':S) -> c | x:S ->* y:S, x':S ->* y:S, x'':S ->* y:S
0.009/0.009	)
0.009/0.009	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.009/0.009	
0.009/0.009	
0.009/0.009	Problem 1:
0.009/0.009	
0.009/0.009	Inlining of Conditions Processor [STERN17]:
0.009/0.009	
0.009/0.009	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.009/0.009	Confluence Problem:
0.009/0.009	(VAR vNonEmpty:S x:S x':S x'':S y:S)
0.009/0.009	(STRATEGY CONTEXTSENSITIVE
0.009/0.009	(f 1 2)
0.009/0.009	(h 1 2 3)
0.009/0.009	(c)
0.009/0.009	(fSNonEmpty)
0.009/0.009	(g 1 2)
0.009/0.009	)
0.009/0.009	(RULES
0.009/0.009	f(x:S,x':S) -> g(y:S,y:S) | x:S ->* y:S, x':S ->* y:S
0.009/0.009	h(x:S,x':S,x'':S) -> c | x:S ->* y:S, x':S ->* y:S, x'':S ->* y:S
0.009/0.009	)
0.009/0.009	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.009/0.009	
0.009/0.009	
0.009/0.009	Problem 1:
0.009/0.009	
0.009/0.009	Clean CTRS Processor:
0.009/0.009	
0.009/0.009	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.009/0.009	Confluence Problem:
0.009/0.009	(VAR x:S x':S x'':S y:S)
0.009/0.009	(STRATEGY CONTEXTSENSITIVE
0.009/0.009	(f 1 2)
0.009/0.009	(h 1 2 3)
0.009/0.009	(c)
0.009/0.009	(fSNonEmpty)
0.009/0.009	(g 1 2)
0.009/0.009	)
0.009/0.009	(RULES
0.009/0.009	f(x:S,x':S) -> g(y:S,y:S) | x:S ->* y:S, x':S ->* y:S
0.009/0.009	h(x:S,x':S,x'':S) -> c | x:S ->* y:S, x':S ->* y:S, x'':S ->* y:S
0.009/0.009	)
0.009/0.009	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.009/0.009	
0.009/0.009	CRule InfChecker Info:
0.009/0.009	f(x:S,x':S) -> g(y:S,y:S) | x:S ->* y:S, x':S ->* y:S
0.009/0.009	Rule remains
0.009/0.009	Proof:
0.009/0.009	NO
0.009/0.009	
0.009/0.009	Problem 1:
0.009/0.009	
0.009/0.009	Infeasibility Problem:
0.009/0.009	[(VAR vNonEmpty:S vNonEmpty:S:S x:S:S x':S:S x'':S:S y:S:S)
0.009/0.009	(STRATEGY CONTEXTSENSITIVE
0.009/0.009	(f 1 2)
0.009/0.009	(h 1 2 3)
0.009/0.009	(c)
0.009/0.009	(fSNonEmpty)
0.009/0.009	(g 1 2)
0.009/0.009	)
0.009/0.009	(RULES
0.009/0.009	f(x:S:S,x':S:S) -> g(y:S:S,y:S:S) | x:S:S ->* y:S:S, x':S:S ->* y:S:S
0.009/0.009	h(x:S:S,x':S:S,x'':S:S) -> c | x:S:S ->* y:S:S, x':S:S ->* y:S:S, x'':S:S ->* y:S:S
0.009/0.009	)]
0.009/0.009	
0.009/0.009	Infeasibility Conditions:
0.009/0.009	x:S:S ->* y:S:S, x':S:S ->* y:S:S
0.009/0.009	
0.009/0.009	Problem 1:
0.009/0.009	
0.009/0.009	Obtaining a proof using Prover9:
0.009/0.009	
0.009/0.009	 -> Prover9 Output:
0.009/0.009	============================== Prover9 ===============================
0.009/0.009	Prover9 (64) version 2009-11A, November 2009.
0.009/0.009	Process 106304 was started by ubuntu on ubuntu,
0.009/0.009	Fri Jul 16 14:54:42 2021
0.009/0.009	The command was "./prover9 -f /tmp/prover9106295-0.in".
0.009/0.009	============================== end of head ===========================
0.009/0.009	
0.009/0.009	============================== INPUT =================================
0.009/0.009	
0.009/0.009	% Reading from file /tmp/prover9106295-0.in
0.009/0.009	
0.009/0.009	assign(max_seconds,20).
0.009/0.009	
0.009/0.009	formulas(assumptions).
0.009/0.009	->*_s0(x,x) # label(reflexivity).
0.009/0.009	->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity).
0.009/0.009	->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence).
0.009/0.009	->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence).
0.009/0.009	->_s0(x1,y) -> ->_s0(h(x1,x2,x3),h(y,x2,x3)) # label(congruence).
0.009/0.009	->_s0(x2,y) -> ->_s0(h(x1,x2,x3),h(x1,y,x3)) # label(congruence).
0.009/0.009	->_s0(x3,y) -> ->_s0(h(x1,x2,x3),h(x1,x2,y)) # label(congruence).
0.009/0.009	->_s0(x1,y) -> ->_s0(g(x1,x2),g(y,x2)) # label(congruence).
0.009/0.009	->_s0(x2,y) -> ->_s0(g(x1,x2),g(x1,y)) # label(congruence).
0.009/0.009	->*_s0(x2,x5) & ->*_s0(x3,x5) -> ->_s0(f(x2,x3),g(x5,x5)) # label(replacement).
0.009/0.009	->*_s0(x2,x5) & ->*_s0(x3,x5) & ->*_s0(x4,x5) -> ->_s0(h(x2,x3,x4),c) # label(replacement).
0.009/0.009	end_of_list.
0.009/0.009	
0.009/0.009	formulas(goals).
0.009/0.009	(exists x2 exists x3 exists x5 (->*_s0(x2,x5) & ->*_s0(x3,x5))) # label(goal).
0.009/0.009	end_of_list.
0.009/0.009	
0.009/0.009	============================== end of input ==========================
0.009/0.009	
0.009/0.009	============================== PROCESS NON-CLAUSAL FORMULAS ==========
0.009/0.009	
0.009/0.009	% Formulas that are not ordinary clauses:
0.009/0.009	1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
0.009/0.009	2 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause).  [assumption].
0.009/0.009	3 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause).  [assumption].
0.009/0.009	4 ->_s0(x1,y) -> ->_s0(h(x1,x2,x3),h(y,x2,x3)) # label(congruence) # label(non_clause).  [assumption].
0.009/0.009	5 ->_s0(x2,y) -> ->_s0(h(x1,x2,x3),h(x1,y,x3)) # label(congruence) # label(non_clause).  [assumption].
0.009/0.009	6 ->_s0(x3,y) -> ->_s0(h(x1,x2,x3),h(x1,x2,y)) # label(congruence) # label(non_clause).  [assumption].
0.009/0.009	7 ->_s0(x1,y) -> ->_s0(g(x1,x2),g(y,x2)) # label(congruence) # label(non_clause).  [assumption].
0.009/0.009	8 ->_s0(x2,y) -> ->_s0(g(x1,x2),g(x1,y)) # label(congruence) # label(non_clause).  [assumption].
0.009/0.009	9 ->*_s0(x2,x5) & ->*_s0(x3,x5) -> ->_s0(f(x2,x3),g(x5,x5)) # label(replacement) # label(non_clause).  [assumption].
0.009/0.009	10 ->*_s0(x2,x5) & ->*_s0(x3,x5) & ->*_s0(x4,x5) -> ->_s0(h(x2,x3,x4),c) # label(replacement) # label(non_clause).  [assumption].
0.009/0.009	11 (exists x2 exists x3 exists x5 (->*_s0(x2,x5) & ->*_s0(x3,x5))) # label(goal) # label(non_clause) # label(goal).  [goal].
0.009/0.009	
0.009/0.009	============================== end of process non-clausal formulas ===
0.009/0.009	
0.009/0.009	============================== PROCESS INITIAL CLAUSES ===============
0.009/0.009	
0.009/0.009	% Clauses before input processing:
0.009/0.009	
0.009/0.009	formulas(usable).
0.009/0.009	end_of_list.
0.009/0.009	
0.009/0.009	formulas(sos).
0.009/0.009	->*_s0(x,x) # label(reflexivity).  [assumption].
0.009/0.009	-->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
0.009/0.009	-->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence).  [clausify(2)].
0.009/0.009	-->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence).  [clausify(3)].
0.009/0.009	-->_s0(x,y) | ->_s0(h(x,z,u),h(y,z,u)) # label(congruence).  [clausify(4)].
0.009/0.009	-->_s0(x,y) | ->_s0(h(z,x,u),h(z,y,u)) # label(congruence).  [clausify(5)].
0.009/0.009	-->_s0(x,y) | ->_s0(h(z,u,x),h(z,u,y)) # label(congruence).  [clausify(6)].
0.009/0.009	-->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence).  [clausify(7)].
0.009/0.009	-->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence).  [clausify(8)].
0.009/0.009	-->*_s0(x,y) | -->*_s0(z,y) | ->_s0(f(x,z),g(y,y)) # label(replacement).  [clausify(9)].
0.009/0.009	-->*_s0(x,y) | -->*_s0(z,y) | -->*_s0(u,y) | ->_s0(h(x,z,u),c) # label(replacement).  [clausify(10)].
0.009/0.009	-->*_s0(x,y) | -->*_s0(z,y) # label(goal).  [deny(11)].
0.009/0.009	end_of_list.
0.009/0.009	
0.009/0.009	formulas(demodulators).
0.009/0.009	end_of_list.
0.009/0.009	
0.009/0.009	============================== PREDICATE ELIMINATION =================
0.009/0.009	
0.009/0.009	No predicates eliminated.
0.009/0.009	
0.009/0.009	============================== end predicate elimination =============
0.009/0.009	
0.009/0.009	Auto_denials:
0.009/0.009	  % copying label goal to answer in negative clause
0.009/0.009	
0.009/0.009	Term ordering decisions:
0.009/0.009	Predicate symbol precedence:  predicate_order([ ->_s0, ->*_s0 ]).
0.009/0.009	Function symbol precedence:  function_order([ c, f, g, h ]).
0.009/0.009	After inverse_order:  (no changes).
0.009/0.009	Unfolding symbols: (none).
0.009/0.009	
0.009/0.009	Auto_inference settings:
0.009/0.009	  % set(neg_binary_resolution).  % (HNE depth_diff=-9)
0.009/0.009	  % clear(ordered_res).  % (HNE depth_diff=-9)
0.009/0.009	  % set(ur_resolution).  % (HNE depth_diff=-9)
0.009/0.009	    % set(ur_resolution) -> set(pos_ur_resolution).
0.009/0.009	    % set(ur_resolution) -> set(neg_ur_resolution).
0.009/0.009	
0.009/0.009	Auto_process settings:
0.009/0.009	  % set(unit_deletion).  % (Horn set with negative nonunits)
0.009/0.009	
0.009/0.009	kept:      12 ->*_s0(x,x) # label(reflexivity).  [assumption].
0.009/0.009	kept:      13 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
0.009/0.009	kept:      14 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence).  [clausify(2)].
0.009/0.009	kept:      15 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence).  [clausify(3)].
0.009/0.009	kept:      16 -->_s0(x,y) | ->_s0(h(x,z,u),h(y,z,u)) # label(congruence).  [clausify(4)].
0.009/0.009	kept:      17 -->_s0(x,y) | ->_s0(h(z,x,u),h(z,y,u)) # label(congruence).  [clausify(5)].
0.009/0.009	kept:      18 -->_s0(x,y) | ->_s0(h(z,u,x),h(z,u,y)) # label(congruence).  [clausify(6)].
0.009/0.009	kept:      19 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence).  [clausify(7)].
0.009/0.009	kept:      20 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence).  [clausify(8)].
0.009/0.009	kept:      21 -->*_s0(x,y) | -->*_s0(z,y) | ->_s0(f(x,z),g(y,y)) # label(replacement).  [clausify(9)].
0.009/0.009	kept:      22 -->*_s0(x,y) | -->*_s0(z,y) | -->*_s0(u,y) | ->_s0(h(x,z,u),c) # label(replacement).  [clausify(10)].
0.009/0.009	kept:      23 -->*_s0(x,y) | -->*_s0(z,y) # label(goal) # answer(goal).  [deny(11)].
0.009/0.009	
0.009/0.009	============================== end of process initial clauses ========
0.009/0.009	
0.009/0.009	============================== CLAUSES FOR SEARCH ====================
0.009/0.009	
0.009/0.009	% Clauses after input processing:
0.009/0.009	
0.009/0.009	formulas(usable).
0.009/0.009	end_of_list.
0.009/0.009	
0.009/0.009	formulas(sos).
0.009/0.009	12 ->*_s0(x,x) # label(reflexivity).  [assumption].
0.009/0.009	13 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
0.009/0.009	14 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence).  [clausify(2)].
0.009/0.009	15 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence).  [clausify(3)].
0.009/0.009	16 -->_s0(x,y) | ->_s0(h(x,z,u),h(y,z,u)) # label(congruence).  [clausify(4)].
0.009/0.009	17 -->_s0(x,y) | ->_s0(h(z,x,u),h(z,y,u)) # label(congruence).  [clausify(5)].
0.009/0.009	18 -->_s0(x,y) | ->_s0(h(z,u,x),h(z,u,y)) # label(congruence).  [clausify(6)].
0.009/0.009	19 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence).  [clausify(7)].
0.009/0.009	20 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence).  [clausify(8)].
0.009/0.009	23 -->*_s0(x,y) | -->*_s0(z,y) # label(goal) # answer(goal).  [deny(11)].
0.009/0.009	end_of_list.
0.009/0.009	
0.009/0.009	formulas(demodulators).
0.009/0.009	end_of_list.
0.009/0.009	
0.009/0.009	============================== end of clauses for search =============
0.009/0.009	
0.009/0.009	============================== SEARCH ================================
0.009/0.009	
0.009/0.009	% Starting search at 0.00 seconds.
0.009/0.009	
0.009/0.009	given #1 (I,wt=3): 12 ->*_s0(x,x) # label(reflexivity).  [assumption].
0.009/0.009	
0.009/0.009	given #2 (I,wt=9): 13 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
0.009/0.009	
0.009/0.009	given #3 (I,wt=10): 14 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence).  [clausify(2)].
0.009/0.009	
0.009/0.009	given #4 (I,wt=10): 15 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence).  [clausify(3)].
0.009/0.009	
0.009/0.009	given #5 (I,wt=12): 16 -->_s0(x,y) | ->_s0(h(x,z,u),h(y,z,u)) # label(congruence).  [clausify(4)].
0.009/0.009	
0.009/0.009	given #6 (I,wt=12): 17 -->_s0(x,y) | ->_s0(h(z,x,u),h(z,y,u)) # label(congruence).  [clausify(5)].
0.009/0.009	
0.009/0.009	given #7 (I,wt=12): 18 -->_s0(x,y) | ->_s0(h(z,u,x),h(z,u,y)) # label(congruence).  [clausify(6)].
0.009/0.009	
0.009/0.009	given #8 (I,wt=10): 19 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence).  [clausify(7)].
0.009/0.009	
0.009/0.009	given #9 (I,wt=10): 20 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence).  [clausify(8)].
0.009/0.009	
0.009/0.009	given #10 (I,wt=6): 23 -->*_s0(x,y) | -->*_s0(z,y) # label(goal) # answer(goal).  [deny(11)].
0.009/0.009	
0.009/0.009	============================== PROOF =================================
0.009/0.009	
0.009/0.009	% Proof 1 at 0.00 (+ 0.00) seconds: goal.
0.009/0.009	% Length of proof is 5.
0.009/0.009	% Level of proof is 3.
0.009/0.009	% Maximum clause weight is 6.000.
0.009/0.009	% Given clauses 10.
0.009/0.009	
0.009/0.009	11 (exists x2 exists x3 exists x5 (->*_s0(x2,x5) & ->*_s0(x3,x5))) # label(goal) # label(non_clause) # label(goal).  [goal].
0.009/0.009	12 ->*_s0(x,x) # label(reflexivity).  [assumption].
0.009/0.009	23 -->*_s0(x,y) | -->*_s0(z,y) # label(goal) # answer(goal).  [deny(11)].
0.009/0.009	24 -->*_s0(x,y) # answer(goal).  [resolve(23,a,12,a)].
0.009/0.009	25 $F # answer(goal).  [resolve(24,a,12,a)].
0.009/0.009	
0.009/0.009	============================== end of proof ==========================
0.009/0.009	
0.009/0.009	============================== STATISTICS ============================
0.009/0.009	
0.009/0.009	Given=10. Generated=14. Kept=13. proofs=1.
0.009/0.009	Usable=10. Sos=0. Demods=0. Limbo=0, Disabled=14. Hints=0.
0.009/0.009	Kept_by_rule=0, Deleted_by_rule=0.
0.009/0.009	Forward_subsumed=1. Back_subsumed=2.
0.009/0.009	Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
0.009/0.009	New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
0.009/0.009	Demod_attempts=0. Demod_rewrites=0.
0.009/0.009	Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
0.009/0.009	Nonunit_fsub_feature_tests=6. Nonunit_bsub_feature_tests=24.
0.009/0.009	Megabytes=0.07.
0.009/0.009	User_CPU=0.00, System_CPU=0.00, Wall_clock=0.
0.009/0.009	
0.009/0.009	============================== end of statistics =====================
0.009/0.009	
0.009/0.009	============================== end of search =========================
0.009/0.009	
0.009/0.009	THEOREM PROVED
0.009/0.009	
0.009/0.009	Exiting with 1 proof.
0.009/0.009	
0.009/0.009	Process 106304 exit (max_proofs) Fri Jul 16 14:54:42 2021
0.009/0.009	
0.009/0.009	
0.009/0.009	The problem is feasible.
0.009/0.009	
0.009/0.009	
0.009/0.009	CRule InfChecker Info:
0.009/0.009	h(x:S,x':S,x'':S) -> c | x:S ->* y:S, x':S ->* y:S, x'':S ->* y:S
0.009/0.009	Rule remains
0.009/0.009	Proof:
0.009/0.009	NO
0.009/0.009	
0.009/0.009	Problem 1:
0.009/0.009	
0.009/0.009	Infeasibility Problem:
0.009/0.009	[(VAR vNonEmpty:S vNonEmpty:S:S x:S:S x':S:S x'':S:S y:S:S)
0.009/0.009	(STRATEGY CONTEXTSENSITIVE
0.009/0.009	(f 1 2)
0.009/0.009	(h 1 2 3)
0.009/0.009	(c)
0.009/0.009	(fSNonEmpty)
0.009/0.009	(g 1 2)
0.009/0.009	)
0.009/0.009	(RULES
0.009/0.009	f(x:S:S,x':S:S) -> g(y:S:S,y:S:S) | x:S:S ->* y:S:S, x':S:S ->* y:S:S
0.009/0.009	h(x:S:S,x':S:S,x'':S:S) -> c | x:S:S ->* y:S:S, x':S:S ->* y:S:S, x'':S:S ->* y:S:S
0.009/0.009	)]
0.009/0.009	
0.009/0.009	Infeasibility Conditions:
0.009/0.009	x:S:S ->* y:S:S, x':S:S ->* y:S:S, x'':S:S ->* y:S:S
0.009/0.009	
0.009/0.009	Problem 1:
0.009/0.009	
0.009/0.009	Obtaining a proof using Prover9:
0.009/0.009	
0.009/0.009	 -> Prover9 Output:
0.009/0.009	============================== Prover9 ===============================
0.009/0.009	Prover9 (64) version 2009-11A, November 2009.
0.009/0.009	Process 106326 was started by ubuntu on ubuntu,
0.009/0.009	Fri Jul 16 14:54:42 2021
0.009/0.009	The command was "./prover9 -f /tmp/prover9106317-0.in".
0.009/0.009	============================== end of head ===========================
0.009/0.009	
0.009/0.009	============================== INPUT =================================
0.009/0.009	
0.009/0.009	% Reading from file /tmp/prover9106317-0.in
0.009/0.009	
0.009/0.009	assign(max_seconds,20).
0.009/0.009	
0.009/0.009	formulas(assumptions).
0.009/0.009	->*_s0(x,x) # label(reflexivity).
0.009/0.009	->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity).
0.009/0.009	->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence).
0.009/0.009	->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence).
0.009/0.009	->_s0(x1,y) -> ->_s0(h(x1,x2,x3),h(y,x2,x3)) # label(congruence).
0.009/0.009	->_s0(x2,y) -> ->_s0(h(x1,x2,x3),h(x1,y,x3)) # label(congruence).
0.009/0.009	->_s0(x3,y) -> ->_s0(h(x1,x2,x3),h(x1,x2,y)) # label(congruence).
0.009/0.009	->_s0(x1,y) -> ->_s0(g(x1,x2),g(y,x2)) # label(congruence).
0.009/0.009	->_s0(x2,y) -> ->_s0(g(x1,x2),g(x1,y)) # label(congruence).
0.009/0.009	->*_s0(x2,x5) & ->*_s0(x3,x5) -> ->_s0(f(x2,x3),g(x5,x5)) # label(replacement).
0.009/0.009	->*_s0(x2,x5) & ->*_s0(x3,x5) & ->*_s0(x4,x5) -> ->_s0(h(x2,x3,x4),c) # label(replacement).
0.009/0.009	end_of_list.
0.009/0.009	
0.009/0.009	formulas(goals).
0.009/0.009	(exists x2 exists x3 exists x4 exists x5 (->*_s0(x2,x5) & ->*_s0(x3,x5) & ->*_s0(x4,x5))) # label(goal).
0.009/0.009	end_of_list.
0.009/0.009	
0.009/0.009	============================== end of input ==========================
0.009/0.009	
0.009/0.009	============================== PROCESS NON-CLAUSAL FORMULAS ==========
0.009/0.009	
0.009/0.009	% Formulas that are not ordinary clauses:
0.009/0.009	1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
0.009/0.009	2 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause).  [assumption].
0.009/0.009	3 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause).  [assumption].
0.009/0.009	4 ->_s0(x1,y) -> ->_s0(h(x1,x2,x3),h(y,x2,x3)) # label(congruence) # label(non_clause).  [assumption].
0.009/0.009	5 ->_s0(x2,y) -> ->_s0(h(x1,x2,x3),h(x1,y,x3)) # label(congruence) # label(non_clause).  [assumption].
0.009/0.009	6 ->_s0(x3,y) -> ->_s0(h(x1,x2,x3),h(x1,x2,y)) # label(congruence) # label(non_clause).  [assumption].
0.009/0.009	7 ->_s0(x1,y) -> ->_s0(g(x1,x2),g(y,x2)) # label(congruence) # label(non_clause).  [assumption].
0.009/0.009	8 ->_s0(x2,y) -> ->_s0(g(x1,x2),g(x1,y)) # label(congruence) # label(non_clause).  [assumption].
0.009/0.009	9 ->*_s0(x2,x5) & ->*_s0(x3,x5) -> ->_s0(f(x2,x3),g(x5,x5)) # label(replacement) # label(non_clause).  [assumption].
0.009/0.009	10 ->*_s0(x2,x5) & ->*_s0(x3,x5) & ->*_s0(x4,x5) -> ->_s0(h(x2,x3,x4),c) # label(replacement) # label(non_clause).  [assumption].
0.009/0.009	11 (exists x2 exists x3 exists x4 exists x5 (->*_s0(x2,x5) & ->*_s0(x3,x5) & ->*_s0(x4,x5))) # label(goal) # label(non_clause) # label(goal).  [goal].
0.009/0.009	
0.009/0.009	============================== end of process non-clausal formulas ===
0.009/0.009	
0.009/0.009	============================== PROCESS INITIAL CLAUSES ===============
0.009/0.009	
0.009/0.009	% Clauses before input processing:
0.009/0.009	
0.009/0.009	formulas(usable).
0.009/0.009	end_of_list.
0.009/0.009	
0.009/0.009	formulas(sos).
0.009/0.009	->*_s0(x,x) # label(reflexivity).  [assumption].
0.009/0.009	-->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
0.009/0.009	-->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence).  [clausify(2)].
0.009/0.009	-->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence).  [clausify(3)].
0.009/0.009	-->_s0(x,y) | ->_s0(h(x,z,u),h(y,z,u)) # label(congruence).  [clausify(4)].
0.009/0.009	-->_s0(x,y) | ->_s0(h(z,x,u),h(z,y,u)) # label(congruence).  [clausify(5)].
0.009/0.009	-->_s0(x,y) | ->_s0(h(z,u,x),h(z,u,y)) # label(congruence).  [clausify(6)].
0.009/0.009	-->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence).  [clausify(7)].
0.009/0.009	-->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence).  [clausify(8)].
0.009/0.009	-->*_s0(x,y) | -->*_s0(z,y) | ->_s0(f(x,z),g(y,y)) # label(replacement).  [clausify(9)].
0.009/0.009	-->*_s0(x,y) | -->*_s0(z,y) | -->*_s0(u,y) | ->_s0(h(x,z,u),c) # label(replacement).  [clausify(10)].
0.009/0.009	-->*_s0(x,y) | -->*_s0(z,y) | -->*_s0(u,y) # label(goal).  [deny(11)].
0.009/0.009	end_of_list.
0.009/0.009	
0.009/0.009	formulas(demodulators).
0.009/0.009	end_of_list.
0.009/0.009	
0.009/0.009	============================== PREDICATE ELIMINATION =================
0.009/0.009	
0.009/0.009	No predicates eliminated.
0.009/0.009	
0.009/0.009	============================== end predicate elimination =============
0.009/0.009	
0.009/0.009	Auto_denials:
0.009/0.009	  % copying label goal to answer in negative clause
0.009/0.009	
0.009/0.009	Term ordering decisions:
0.009/0.009	Predicate symbol precedence:  predicate_order([ ->_s0, ->*_s0 ]).
0.009/0.009	Function symbol precedence:  function_order([ c, f, g, h ]).
0.009/0.009	After inverse_order:  (no changes).
0.009/0.009	Unfolding symbols: (none).
0.009/0.009	
0.009/0.009	Auto_inference settings:
0.009/0.009	  % set(neg_binary_resolution).  % (HNE depth_diff=-9)
0.009/0.009	  % clear(ordered_res).  % (HNE depth_diff=-9)
0.009/0.009	  % set(ur_resolution).  % (HNE depth_diff=-9)
0.009/0.009	    % set(ur_resolution) -> set(pos_ur_resolution).
0.009/0.009	    % set(ur_resolution) -> set(neg_ur_resolution).
0.009/0.009	
0.009/0.009	Auto_process settings:
0.009/0.009	  % set(unit_deletion).  % (Horn set with negative nonunits)
0.009/0.009	
0.009/0.009	kept:      12 ->*_s0(x,x) # label(reflexivity).  [assumption].
0.009/0.009	kept:      13 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
0.009/0.009	kept:      14 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence).  [clausify(2)].
0.009/0.009	kept:      15 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence).  [clausify(3)].
0.009/0.009	kept:      16 -->_s0(x,y) | ->_s0(h(x,z,u),h(y,z,u)) # label(congruence).  [clausify(4)].
0.009/0.009	kept:      17 -->_s0(x,y) | ->_s0(h(z,x,u),h(z,y,u)) # label(congruence).  [clausify(5)].
0.009/0.009	kept:      18 -->_s0(x,y) | ->_s0(h(z,u,x),h(z,u,y)) # label(congruence).  [clausify(6)].
0.009/0.009	kept:      19 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence).  [clausify(7)].
0.009/0.009	kept:      20 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence).  [clausify(8)].
0.009/0.009	kept:      21 -->*_s0(x,y) | -->*_s0(z,y) | ->_s0(f(x,z),g(y,y)) # label(replacement).  [clausify(9)].
0.009/0.009	kept:      22 -->*_s0(x,y) | -->*_s0(z,y) | -->*_s0(u,y) | ->_s0(h(x,z,u),c) # label(replacement).  [clausify(10)].
0.009/0.009	kept:      23 -->*_s0(x,y) | -->*_s0(z,y) | -->*_s0(u,y) # label(goal) # answer(goal).  [deny(11)].
0.009/0.009	
0.009/0.009	============================== end of process initial clauses ========
0.009/0.009	
0.009/0.009	============================== CLAUSES FOR SEARCH ====================
0.009/0.009	
0.009/0.009	% Clauses after input processing:
0.009/0.009	
0.009/0.009	formulas(usable).
0.009/0.009	end_of_list.
0.009/0.009	
0.009/0.009	formulas(sos).
0.009/0.009	12 ->*_s0(x,x) # label(reflexivity).  [assumption].
0.009/0.009	13 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
0.009/0.009	14 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence).  [clausify(2)].
0.009/0.009	15 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence).  [clausify(3)].
0.009/0.009	16 -->_s0(x,y) | ->_s0(h(x,z,u),h(y,z,u)) # label(congruence).  [clausify(4)].
0.009/0.009	17 -->_s0(x,y) | ->_s0(h(z,x,u),h(z,y,u)) # label(congruence).  [clausify(5)].
0.009/0.009	18 -->_s0(x,y) | ->_s0(h(z,u,x),h(z,u,y)) # label(congruence).  [clausify(6)].
0.009/0.009	19 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence).  [clausify(7)].
0.009/0.009	20 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence).  [clausify(8)].
0.009/0.009	21 -->*_s0(x,y) | -->*_s0(z,y) | ->_s0(f(x,z),g(y,y)) # label(replacement).  [clausify(9)].
0.009/0.009	23 -->*_s0(x,y) | -->*_s0(z,y) | -->*_s0(u,y) # label(goal) # answer(goal).  [deny(11)].
0.009/0.009	end_of_list.
0.009/0.009	
0.009/0.009	formulas(demodulators).
0.009/0.009	end_of_list.
0.009/0.009	
0.009/0.009	============================== end of clauses for search =============
0.009/0.009	
0.009/0.009	============================== SEARCH ================================
0.009/0.009	
0.009/0.009	% Starting search at 0.00 seconds.
0.009/0.009	
0.009/0.009	given #1 (I,wt=3): 12 ->*_s0(x,x) # label(reflexivity).  [assumption].
0.009/0.009	
0.009/0.009	given #2 (I,wt=9): 13 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
0.009/0.009	
0.009/0.009	given #3 (I,wt=10): 14 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence).  [clausify(2)].
0.009/0.009	
0.009/0.009	given #4 (I,wt=10): 15 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence).  [clausify(3)].
0.009/0.009	
0.009/0.009	given #5 (I,wt=12): 16 -->_s0(x,y) | ->_s0(h(x,z,u),h(y,z,u)) # label(congruence).  [clausify(4)].
0.009/0.009	
0.009/0.009	given #6 (I,wt=12): 17 -->_s0(x,y) | ->_s0(h(z,x,u),h(z,y,u)) # label(congruence).  [clausify(5)].
0.009/0.009	
0.009/0.009	given #7 (I,wt=12): 18 -->_s0(x,y) | ->_s0(h(z,u,x),h(z,u,y)) # label(congruence).  [clausify(6)].
0.009/0.009	
0.009/0.009	given #8 (I,wt=10): 19 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence).  [clausify(7)].
0.009/0.009	
0.009/0.009	given #9 (I,wt=10): 20 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence).  [clausify(8)].
0.009/0.009	
0.009/0.009	given #10 (I,wt=13): 21 -->*_s0(x,y) | -->*_s0(z,y) | ->_s0(f(x,z),g(y,y)) # label(replacement).  [clausify(9)].
0.009/0.009	
0.009/0.009	given #11 (I,wt=9): 23 -->*_s0(x,y) | -->*_s0(z,y) | -->*_s0(u,y) # label(goal) # answer(goal).  [deny(11)].
0.009/0.009	
0.009/0.009	============================== PROOF =================================
0.009/0.009	
0.009/0.009	% Proof 1 at 0.00 (+ 0.00) seconds: goal.
0.009/0.009	% Length of proof is 5.
0.009/0.009	% Level of proof is 3.
0.009/0.009	% Maximum clause weight is 9.000.
0.009/0.009	% Given clauses 11.
0.009/0.009	
0.009/0.009	11 (exists x2 exists x3 exists x4 exists x5 (->*_s0(x2,x5) & ->*_s0(x3,x5) & ->*_s0(x4,x5))) # label(goal) # label(non_clause) # label(goal).  [goal].
0.009/0.009	12 ->*_s0(x,x) # label(reflexivity).  [assumption].
0.009/0.009	23 -->*_s0(x,y) | -->*_s0(z,y) | -->*_s0(u,y) # label(goal) # answer(goal).  [deny(11)].
0.009/0.009	26 -->*_s0(x,y) # answer(goal).  [ur(23,b,12,a,c,12,a)].
0.009/0.009	27 $F # answer(goal).  [resolve(26,a,12,a)].
0.009/0.009	
0.009/0.009	============================== end of proof ==========================
0.009/0.009	
0.009/0.009	============================== STATISTICS ============================
0.009/0.009	
0.009/0.009	Given=11. Generated=20. Kept=15. proofs=1.
0.009/0.009	Usable=11. Sos=1. Demods=0. Limbo=1, Disabled=13. Hints=0.
0.009/0.009	Kept_by_rule=0, Deleted_by_rule=0.
0.009/0.009	Forward_subsumed=5. Back_subsumed=1.
0.009/0.009	Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
0.009/0.009	New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
0.009/0.009	Demod_attempts=0. Demod_rewrites=0.
0.009/0.009	Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
0.009/0.009	Nonunit_fsub_feature_tests=10. Nonunit_bsub_feature_tests=24.
0.009/0.009	Megabytes=0.08.
0.009/0.009	User_CPU=0.00, System_CPU=0.00, Wall_clock=0.
0.009/0.009	
0.009/0.009	============================== end of statistics =====================
0.009/0.009	
0.009/0.009	============================== end of search =========================
0.009/0.009	
0.009/0.009	THEOREM PROVED
0.009/0.009	
0.009/0.009	Exiting with 1 proof.
0.009/0.009	
0.009/0.009	Process 106326 exit (max_proofs) Fri Jul 16 14:54:42 2021
0.009/0.009	
0.009/0.009	
0.009/0.009	The problem is feasible.
0.009/0.009	
0.009/0.009	
0.009/0.009	Problem 1:
0.009/0.009	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.009/0.009	Confluence Problem:
0.009/0.009	(VAR x:S x':S x'':S y:S)
0.009/0.009	(STRATEGY CONTEXTSENSITIVE
0.009/0.009	(f 1 2)
0.009/0.009	(h 1 2 3)
0.009/0.009	(c)
0.009/0.009	(fSNonEmpty)
0.009/0.009	(g 1 2)
0.009/0.009	)
0.009/0.009	(RULES
0.009/0.009	f(x:S,x':S) -> g(y:S,y:S) | x:S ->* y:S, x':S ->* y:S
0.009/0.009	h(x:S,x':S,x'':S) -> c | x:S ->* y:S, x':S ->* y:S, x'':S ->* y:S
0.009/0.009	)
0.009/0.009	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.009/0.009	
0.009/0.009	Critical Pairs Processor:
0.009/0.009	-> Rules:
0.009/0.009	f(x:S,x':S) -> g(y:S,y:S) | x:S ->* y:S, x':S ->* y:S
0.009/0.009	h(x:S,x':S,x'':S) -> c | x:S ->* y:S, x':S ->* y:S, x'':S ->* y:S
0.009/0.009	-> Vars:
0.009/0.009	"x", "x'", "y", "x", "x'", "x''", "y"
0.009/0.009	-> FVars:
0.009/0.009	"x5", "x6", "x7", "x8", "x9", "x10", "x11"
0.009/0.009	-> PVars:
0.009/0.009	"x": ["x5", "x8"], "x'": ["x6", "x9"], "y": ["x7", "x11"], "x''": ["x10"]
0.009/0.009	
0.009/0.009	-> Rlps:
0.009/0.009	crule: f(x5:S,x6:S) -> g(x7:S,x7:S) | x5:S ->* x7:S, x6:S ->* x7:S, id: 1, possubterms: f(x5:S,x6:S)-> []
0.009/0.009	crule: h(x8:S,x9:S,x10:S) -> c | x8:S ->* x11:S, x9:S ->* x11:S, x10:S ->* x11:S, id: 2, possubterms: h(x8:S,x9:S,x10:S)-> []
0.009/0.009	
0.009/0.009	-> Unifications:
0.009/0.009	
0.009/0.009	
0.009/0.009	-> Critical pairs info:
0.009/0.009	
0.009/0.009	
0.009/0.009	-> Problem conclusions:
0.009/0.009	 Left linear, Not right linear, Not linear
0.009/0.009	 Weakly orthogonal, Almost orthogonal, Orthogonal
0.009/0.009	 CTRS Type: 3
0.009/0.009	 Deterministic, Strongly deterministic
0.009/0.009	 Oriented CTRS, Properly oriented CTRS, Not join CTRS
0.009/0.009	 Maybe right-stable CTRS, Overlay CTRS
0.009/0.009	 Maybe normal CTRS, Maybe almost normal CTRS
0.009/0.009	 Maybe terminating CTRS, Joinable CCPs
0.009/0.009	 Maybe level confluent
0.009/0.009	 Maybe confluent
0.009/0.009	
0.009/0.009	Problem 1:
0.009/0.009	Clean Infeasible CCPs Processor:
0.009/0.009	
0.009/0.009	
0.009/0.009	-> Problem conclusions:
0.009/0.009	 Left linear, Not right linear, Not linear
0.009/0.009	 Weakly orthogonal, Almost orthogonal, Orthogonal
0.009/0.009	 CTRS Type: 3
0.009/0.009	 Deterministic, Strongly deterministic
0.009/0.009	 Oriented CTRS, Properly oriented CTRS, Not join CTRS
0.009/0.009	 Maybe right-stable CTRS, Overlay CTRS
0.009/0.009	 Maybe normal CTRS, Maybe almost normal CTRS
0.009/0.009	 Maybe terminating CTRS, Joinable CCPs
0.009/0.009	 Maybe level confluent
0.009/0.009	 Maybe confluent
0.009/0.009	
0.009/0.009	Resulting CCPs:
0.009/0.009	No CCPs left
0.009/0.009	
0.009/0.009	Problem 1:
0.009/0.009	Operation Termination Processor:
0.009/0.009	Operational terminating?
0.009/0.009	YES
0.009/0.009	
0.009/0.009	Problem 1:
0.009/0.009	
0.009/0.009	(VAR vu95NonEmpty:S xu58S:S xu39u58S:S xu39u39u58S:S yu58S:S)
0.009/0.009	(RULES
0.009/0.009	f(xu58S:S,xu39u58S:S) -> g(yu58S:S,yu58S:S) | xu58S:S ->* yu58S:S, xu39u58S:S ->* yu58S:S
0.009/0.009	h(xu58S:S,xu39u58S:S,xu39u39u58S:S) -> c | xu58S:S ->* yu58S:S, xu39u58S:S ->* yu58S:S, xu39u39u58S:S ->* yu58S:S
0.009/0.009	)
0.009/0.009	
0.009/0.009	Problem 1:
0.009/0.009	Valid CTRS Processor:
0.009/0.009	-> Rules:
0.009/0.009	 f(xu58S:S,xu39u58S:S) -> g(yu58S:S,yu58S:S) | xu58S:S ->* yu58S:S, xu39u58S:S ->* yu58S:S
0.009/0.009	 h(xu58S:S,xu39u58S:S,xu39u39u58S:S) -> c | xu58S:S ->* yu58S:S, xu39u58S:S ->* yu58S:S, xu39u39u58S:S ->* yu58S:S
0.009/0.009	-> The system is a deterministic 3-CTRS.
0.009/0.009	
0.009/0.009	Problem 1:
0.009/0.009	
0.009/0.009	2D Dependency Pair Processor:
0.009/0.009	
0.009/0.009	Conditional Termination Problem 1:
0.009/0.009	-> Pairs:
0.009/0.009	 Empty
0.009/0.009	-> QPairs:
0.009/0.009	 Empty
0.009/0.009	-> Rules:
0.009/0.009	 f(xu58S:S,xu39u58S:S) -> g(yu58S:S,yu58S:S) | xu58S:S ->* yu58S:S, xu39u58S:S ->* yu58S:S
0.009/0.009	 h(xu58S:S,xu39u58S:S,xu39u39u58S:S) -> c | xu58S:S ->* yu58S:S, xu39u58S:S ->* yu58S:S, xu39u39u58S:S ->* yu58S:S
0.009/0.009	
0.009/0.009	Conditional Termination Problem 2:
0.009/0.009	-> Pairs:
0.009/0.009	 Empty
0.009/0.009	-> QPairs:
0.009/0.009	 Empty
0.009/0.009	-> Rules:
0.009/0.009	 f(xu58S:S,xu39u58S:S) -> g(yu58S:S,yu58S:S) | xu58S:S ->* yu58S:S, xu39u58S:S ->* yu58S:S
0.009/0.009	 h(xu58S:S,xu39u58S:S,xu39u39u58S:S) -> c | xu58S:S ->* yu58S:S, xu39u58S:S ->* yu58S:S, xu39u39u58S:S ->* yu58S:S
0.009/0.009	
0.009/0.009	
0.009/0.009	The problem is decomposed in 2 subproblems.
0.009/0.009	
0.009/0.009	Problem 1.1:
0.009/0.009	
0.009/0.009	SCC Processor:
0.009/0.009	-> Pairs:
0.009/0.009	 Empty
0.009/0.009	-> QPairs:
0.009/0.009	 Empty
0.009/0.009	-> Rules:
0.009/0.009	 f(xu58S:S,xu39u58S:S) -> g(yu58S:S,yu58S:S) | xu58S:S ->* yu58S:S, xu39u58S:S ->* yu58S:S
0.009/0.009	 h(xu58S:S,xu39u58S:S,xu39u39u58S:S) -> c | xu58S:S ->* yu58S:S, xu39u58S:S ->* yu58S:S, xu39u39u58S:S ->* yu58S:S
0.009/0.009	->Strongly Connected Components:
0.009/0.009	 There is no strongly connected component
0.009/0.009	
0.009/0.009	The problem is finite.
0.009/0.009	
0.009/0.009	Problem 1.2:
0.009/0.009	
0.009/0.009	SCC Processor:
0.009/0.009	-> Pairs:
0.009/0.009	 Empty
0.009/0.009	-> QPairs:
0.009/0.009	 Empty
0.009/0.009	-> Rules:
0.009/0.009	 f(xu58S:S,xu39u58S:S) -> g(yu58S:S,yu58S:S) | xu58S:S ->* yu58S:S, xu39u58S:S ->* yu58S:S
0.009/0.009	 h(xu58S:S,xu39u58S:S,xu39u39u58S:S) -> c | xu58S:S ->* yu58S:S, xu39u58S:S ->* yu58S:S, xu39u39u58S:S ->* yu58S:S
0.009/0.009	->Strongly Connected Components:
0.009/0.009	 There is no strongly connected component
0.009/0.009	
0.009/0.009	The problem is finite.
0.009/0.009	
0.009/0.009	
0.009/0.009	-> Problem conclusions:
0.009/0.009	 Left linear, Not right linear, Not linear
0.009/0.009	 Weakly orthogonal, Almost orthogonal, Orthogonal
0.009/0.009	 CTRS Type: 3
0.009/0.009	 Deterministic, Strongly deterministic
0.009/0.009	 Oriented CTRS, Properly oriented CTRS, Not join CTRS
0.009/0.009	 Maybe right-stable CTRS, Overlay CTRS
0.009/0.009	 Maybe normal CTRS, Maybe almost normal CTRS
0.009/0.009	 Terminating CTRS, Joinable CCPs
0.009/0.009	 Maybe level confluent
0.009/0.009	 Confluent
0.009/0.009	
0.009/0.009	The problem is joinable.
0.009/0.009	0.04user 0.04system 0:00.09elapsed 94%CPU (0avgtext+0avgdata 11864maxresident)k
0.009/0.009	8inputs+0outputs (0major+7733minor)pagefaults 0swaps