0.00/0.04	YES
0.00/0.04	
0.00/0.04	Problem 1: 
0.00/0.04	
0.00/0.04	
0.00/0.04	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.04	Confluence Problem:
0.00/0.04	(VAR vNonEmpty x)
0.00/0.04	(REPLACEMENT-MAP
0.00/0.04	(a)
0.00/0.04	(f 1)
0.00/0.04	(b)
0.00/0.04	(fSNonEmpty)
0.00/0.04	)
0.00/0.04	(RULES
0.00/0.04	a -> b
0.00/0.04	f(x) -> x | x ->* b
0.00/0.04	)
0.00/0.04	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.04	
0.00/0.04	
0.00/0.04	Problem 1: 
0.00/0.04	
0.00/0.04	Problem 1: 
0.00/0.04	
0.00/0.04	Clean CTRS Procedure:
0.00/0.04	
0.00/0.04	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.04	Confluence Problem:
0.00/0.04	(VAR x)
0.00/0.04	(REPLACEMENT-MAP
0.00/0.04	(a)
0.00/0.04	(f 1)
0.00/0.04	(b)
0.00/0.04	(fSNonEmpty)
0.00/0.04	)
0.00/0.04	(RULES
0.00/0.04	a -> b
0.00/0.04	f(x) -> x | x ->* b
0.00/0.04	)
0.00/0.04	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.04	
0.00/0.04	CRule InfChecker Info:
0.00/0.04	a -> b
0.00/0.04	Rule remains
0.00/0.04	Proof:
0.00/0.04	NO_CONDS
0.00/0.04	
0.00/0.04	CRule InfChecker Info:
0.00/0.04	f(x) -> x | x ->* b
0.00/0.04	Rule remains
0.00/0.04	Proof:
0.00/0.04	NO
0.00/0.04	
0.00/0.04	Problem 1: 
0.00/0.04	
0.00/0.04	Infeasibility Problem:
0.00/0.04	[(VAR vNonEmpty x vNonEmpty x)
0.00/0.04	(STRATEGY CONTEXTSENSITIVE
0.00/0.04	(a)
0.00/0.04	(f 1)
0.00/0.04	(b)
0.00/0.04	(fSNonEmpty)
0.00/0.04	)
0.00/0.04	(RULES
0.00/0.04	a -> b
0.00/0.04	f(x) -> x | x ->* b
0.00/0.04	)]
0.00/0.04	
0.00/0.04	Infeasibility Conditions:
0.00/0.04	x ->* b
0.00/0.04	
0.00/0.04	Problem 1: 
0.00/0.04	
0.00/0.04	Obtaining a proof using Prover9:
0.00/0.04	
0.00/0.04	 -> Prover9 Output:
0.00/0.04	============================== Prover9 ===============================
0.00/0.04	Prover9 (64) version 2009-11A, November 2009.
0.00/0.04	Process 50855 was started by sandbox2 on n085.star.cs.uiowa.edu,
0.00/0.04	Wed Jul 13 08:28:00 2022
0.00/0.04	The command was "./prover9 -f /tmp/prover950844.in".
0.00/0.04	============================== end of head ===========================
0.00/0.04	
0.00/0.04	============================== INPUT =================================
0.00/0.04	
0.00/0.04	% Reading from file /tmp/prover950844.in
0.00/0.04	
0.00/0.04	assign(max_seconds,20).
0.00/0.04	
0.00/0.04	formulas(assumptions).
0.00/0.04	->_s0(x1,y) -> ->_s0(f(x1),f(y)) # label(congruence).
0.00/0.04	->_s0(a,b) # label(replacement).
0.00/0.04	->*_s0(x1,b) -> ->_s0(f(x1),x1) # label(replacement).
0.00/0.04	->*_s0(x,x) # label(reflexivity).
0.00/0.04	->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity).
0.00/0.04	end_of_list.
0.00/0.04	
0.00/0.04	formulas(goals).
0.00/0.04	(exists x3 ->*_s0(x3,b)) # label(goal).
0.00/0.04	end_of_list.
0.00/0.04	
0.00/0.04	============================== end of input ==========================
0.00/0.04	
0.00/0.04	============================== PROCESS NON-CLAUSAL FORMULAS ==========
0.00/0.04	
0.00/0.04	% Formulas that are not ordinary clauses:
0.00/0.04	1 ->_s0(x1,y) -> ->_s0(f(x1),f(y)) # label(congruence) # label(non_clause).  [assumption].
0.00/0.04	2 ->*_s0(x1,b) -> ->_s0(f(x1),x1) # label(replacement) # label(non_clause).  [assumption].
0.00/0.04	3 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
0.00/0.04	4 (exists x3 ->*_s0(x3,b)) # label(goal) # label(non_clause) # label(goal).  [goal].
0.00/0.04	
0.00/0.04	============================== end of process non-clausal formulas ===
0.00/0.04	
0.00/0.04	============================== PROCESS INITIAL CLAUSES ===============
0.00/0.04	
0.00/0.04	% Clauses before input processing:
0.00/0.04	
0.00/0.04	formulas(usable).
0.00/0.04	end_of_list.
0.00/0.04	
0.00/0.04	formulas(sos).
0.00/0.04	-->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence).  [clausify(1)].
0.00/0.04	->_s0(a,b) # label(replacement).  [assumption].
0.00/0.04	-->*_s0(x,b) | ->_s0(f(x),x) # label(replacement).  [clausify(2)].
0.00/0.04	->*_s0(x,x) # label(reflexivity).  [assumption].
0.00/0.04	-->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(3)].
0.00/0.04	-->*_s0(x,b) # label(goal).  [deny(4)].
0.00/0.04	end_of_list.
0.00/0.04	
0.00/0.04	formulas(demodulators).
0.00/0.04	end_of_list.
0.00/0.04	
0.00/0.04	============================== PREDICATE ELIMINATION =================
0.00/0.04	
0.00/0.04	No predicates eliminated.
0.00/0.04	
0.00/0.04	============================== end predicate elimination =============
0.00/0.04	
0.00/0.04	Auto_denials:
0.00/0.04	  % copying label goal to answer in negative clause
0.00/0.04	
0.00/0.04	Term ordering decisions:
0.00/0.04	Predicate symbol precedence:  predicate_order([ ->_s0, ->*_s0 ]).
0.00/0.04	Function symbol precedence:  function_order([ b, a, f ]).
0.00/0.04	After inverse_order:  (no changes).
0.00/0.04	Unfolding symbols: (none).
0.00/0.04	
0.00/0.04	Auto_inference settings:
0.00/0.04	  % set(neg_binary_resolution).  % (HNE depth_diff=-2)
0.00/0.04	  % clear(ordered_res).  % (HNE depth_diff=-2)
0.00/0.04	  % set(ur_resolution).  % (HNE depth_diff=-2)
0.00/0.04	    % set(ur_resolution) -> set(pos_ur_resolution).
0.00/0.04	    % set(ur_resolution) -> set(neg_ur_resolution).
0.00/0.04	
0.00/0.04	Auto_process settings:  (no changes).
0.00/0.04	
0.00/0.04	kept:      5 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence).  [clausify(1)].
0.00/0.04	kept:      6 ->_s0(a,b) # label(replacement).  [assumption].
0.00/0.04	kept:      7 -->*_s0(x,b) | ->_s0(f(x),x) # label(replacement).  [clausify(2)].
0.00/0.04	kept:      8 ->*_s0(x,x) # label(reflexivity).  [assumption].
0.00/0.04	kept:      9 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(3)].
0.00/0.04	kept:      10 -->*_s0(x,b) # label(goal) # answer(goal).  [deny(4)].
0.00/0.04	
0.00/0.04	============================== PROOF =================================
0.00/0.04	
0.00/0.04	% Proof 1 at 0.00 (+ 0.00) seconds: goal.
0.00/0.04	% Length of proof is 4.
0.00/0.04	% Level of proof is 2.
0.00/0.04	% Maximum clause weight is 3.000.
0.00/0.04	% Given clauses 0.
0.00/0.04	
0.00/0.04	4 (exists x3 ->*_s0(x3,b)) # label(goal) # label(non_clause) # label(goal).  [goal].
0.00/0.04	8 ->*_s0(x,x) # label(reflexivity).  [assumption].
0.00/0.04	10 -->*_s0(x,b) # label(goal) # answer(goal).  [deny(4)].
0.00/0.04	11 $F # answer(goal).  [resolve(10,a,8,a)].
0.00/0.04	
0.00/0.04	============================== end of proof ==========================
0.00/0.04	
0.00/0.04	============================== STATISTICS ============================
0.00/0.04	
0.00/0.04	Given=0. Generated=6. Kept=6. proofs=1.
0.00/0.04	Usable=0. Sos=0. Demods=0. Limbo=5, Disabled=6. Hints=0.
0.00/0.04	Kept_by_rule=0, Deleted_by_rule=0.
0.00/0.04	Forward_subsumed=0. Back_subsumed=0.
0.00/0.04	Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
0.00/0.04	New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
0.00/0.04	Demod_attempts=0. Demod_rewrites=0.
0.00/0.04	Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
0.00/0.04	Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.
0.00/0.04	Megabytes=0.03.
0.00/0.04	User_CPU=0.00, System_CPU=0.00, Wall_clock=0.
0.00/0.04	
0.00/0.04	============================== end of statistics =====================
0.00/0.04	
0.00/0.04	============================== end of search =========================
0.00/0.04	
0.00/0.04	THEOREM PROVED
0.00/0.04	
0.00/0.04	Exiting with 1 proof.
0.00/0.04	
0.00/0.04	Process 50855 exit (max_proofs) Wed Jul 13 08:28:00 2022
0.00/0.04	
0.00/0.04	
0.00/0.04	The problem is feasible.
0.00/0.04	
0.00/0.04	
0.00/0.04	Problem 1: 
0.00/0.04	
0.00/0.04	Problem 1: 
0.00/0.04	
0.00/0.04	U_conf Transform CTRS Procedure:
0.00/0.04	
0.00/0.04	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.04	Confluence Problem:
0.00/0.04	(VAR x)
0.00/0.04	(REPLACEMENT-MAP
0.00/0.04	(a)
0.00/0.04	(f 1)
0.00/0.04	(b)
0.00/0.04	(fSNonEmpty)
0.00/0.04	)
0.00/0.04	(RULES
0.00/0.04	a -> b
0.00/0.04	f(x) -> x | x ->* b
0.00/0.04	)
0.00/0.04	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.04	Resulting U_conf(R):
0.00/0.04	(VAR x)
0.00/0.04	(STRATEGY CONTEXTSENSITIVE
0.00/0.04	(a)
0.00/0.04	(f 1)
0.00/0.04	(b)
0.00/0.04	(fSNonEmpty)
0.00/0.04	(U1 1 2)
0.00/0.04	)
0.00/0.04	(RULES
0.00/0.04	a -> b
0.00/0.04	f(x) -> U1(x,x)
0.00/0.04	U1(b,x) -> x
0.00/0.04	)
0.00/0.04	UAlphas (debugging):
0.00/0.04	[{f(x) | x}]
0.00/0.04	
0.00/0.04	Problem 1: 
0.00/0.04	
0.00/0.04	
0.00/0.04	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.04	Confluence Problem:
0.00/0.04	(VAR x)
0.00/0.04	(REPLACEMENT-MAP
0.00/0.04	(a)
0.00/0.04	(f 1)
0.00/0.04	(b)
0.00/0.04	(fSNonEmpty)
0.00/0.04	(U1 1, 2)
0.00/0.04	)
0.00/0.04	(RULES
0.00/0.04	a -> b
0.00/0.04	f(x) -> U1(x,x)
0.00/0.04	U1(b,x) -> x
0.00/0.04	)
0.00/0.04	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.04	
0.00/0.04	
0.00/0.04	Problem 1: 
0.00/0.04	
0.00/0.04	Problem 1: 
0.00/0.04	Not CS-TRS Procedure:
0.00/0.04	R is not a CS-TRS
0.00/0.04	
0.00/0.04	Problem 1: 
0.00/0.04	Linearity Procedure:
0.00/0.04	Linear?
0.00/0.04	NO
0.00/0.04	
0.00/0.04	Problem 1: 
0.00/0.04	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.04	Confluence Problem:
0.00/0.04	(VAR x)
0.00/0.04	(REPLACEMENT-MAP
0.00/0.04	(a)
0.00/0.04	(f 1)
0.00/0.04	(b)
0.00/0.04	(fSNonEmpty)
0.00/0.04	(U1 1, 2)
0.00/0.04	)
0.00/0.04	(RULES
0.00/0.04	a -> b
0.00/0.04	f(x) -> U1(x,x)
0.00/0.04	U1(b,x) -> x
0.00/0.04	)
0.00/0.04	Linear:NO
0.00/0.04	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.04	
0.00/0.04	Huet Levy Procedure:
0.00/0.04	-> Rules:
0.00/0.04	 a -> b
0.00/0.04	 f(x) -> U1(x,x)
0.00/0.04	 U1(b,x) -> x
0.00/0.04	-> Vars:
0.00/0.04	 x, x
0.00/0.04	
0.00/0.04	-> Rlps:
0.00/0.04	 (rule: a -> b, id: 1, possubterms: a->[])
0.00/0.04	 (rule: f(x) -> U1(x,x), id: 2, possubterms: f(x)->[])
0.00/0.04	 (rule: U1(b,x) -> x, id: 3, possubterms: U1(b,x)->[], b->[1])
0.00/0.04	
0.00/0.04	-> Unifications:
0.00/0.04	
0.00/0.04	
0.00/0.04	-> Critical pairs info:
0.00/0.04	
0.00/0.04	
0.00/0.04	-> Problem conclusions:
0.00/0.04	 Left linear, Not right linear, Not linear
0.00/0.04	 Weakly orthogonal, Almost orthogonal, Orthogonal
0.00/0.04	 Huet-Levy confluent, Not Newman confluent
0.00/0.04	 R is a TRS 
0.00/0.04	
0.00/0.04	
0.00/0.04	The problem is confluent.
0.00/10.11	EOF