80.033/80.033	NO
80.033/80.033	
80.033/80.033	Problem 1:
80.033/80.033	
80.033/80.033	
80.033/80.033	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
80.033/80.033	Confluence Problem:
80.033/80.033	(VAR vNonEmpty:S x:S)
80.033/80.033	(STRATEGY CONTEXTSENSITIVE
80.033/80.033	(e 1)
80.033/80.033	(o 1)
80.033/80.033	(0)
80.033/80.033	(fSNonEmpty)
80.033/80.033	(false)
80.033/80.033	(s 1)
80.033/80.033	(true)
80.033/80.033	)
80.033/80.033	(RULES
80.033/80.033	e(0) -> true
80.033/80.033	e(s(x:S)) -> false | e(x:S) ->* true
80.033/80.033	e(s(x:S)) -> true | o(x:S) ->* true
80.033/80.033	o(0) -> true
80.033/80.033	o(s(x:S)) -> false | o(x:S) ->* true
80.033/80.033	o(s(x:S)) -> true | e(x:S) ->* true
80.033/80.033	)
80.033/80.033	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
80.033/80.033	
80.033/80.033	
80.033/80.033	Problem 1:
80.033/80.033	
80.033/80.033	Inlining of Conditions Processor [STERN17]:
80.033/80.033	
80.033/80.033	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
80.033/80.033	Confluence Problem:
80.033/80.033	(VAR vNonEmpty:S x:S)
80.033/80.033	(STRATEGY CONTEXTSENSITIVE
80.033/80.033	(e 1)
80.033/80.033	(o 1)
80.033/80.033	(0)
80.033/80.033	(fSNonEmpty)
80.033/80.033	(false)
80.033/80.033	(s 1)
80.033/80.033	(true)
80.033/80.033	)
80.033/80.033	(RULES
80.033/80.033	e(0) -> true
80.033/80.033	e(s(x:S)) -> false | e(x:S) ->* true
80.033/80.033	e(s(x:S)) -> true | o(x:S) ->* true
80.033/80.033	o(0) -> true
80.033/80.033	o(s(x:S)) -> false | o(x:S) ->* true
80.033/80.033	o(s(x:S)) -> true | e(x:S) ->* true
80.033/80.033	)
80.033/80.033	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
80.033/80.033	
80.033/80.033	
80.033/80.033	Problem 1:
80.033/80.033	
80.033/80.033	Clean CTRS Processor:
80.033/80.033	
80.033/80.033	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
80.033/80.033	Confluence Problem:
80.033/80.033	(VAR x:S)
80.033/80.033	(STRATEGY CONTEXTSENSITIVE
80.033/80.033	(e 1)
80.033/80.033	(o 1)
80.033/80.033	(0)
80.033/80.033	(fSNonEmpty)
80.033/80.033	(false)
80.033/80.033	(s 1)
80.033/80.033	(true)
80.033/80.033	)
80.033/80.033	(RULES
80.033/80.033	e(0) -> true
80.033/80.033	e(s(x:S)) -> false | e(x:S) ->* true
80.033/80.033	e(s(x:S)) -> true | o(x:S) ->* true
80.033/80.033	o(0) -> true
80.033/80.033	o(s(x:S)) -> false | o(x:S) ->* true
80.033/80.033	o(s(x:S)) -> true | e(x:S) ->* true
80.033/80.033	)
80.033/80.033	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
80.033/80.033	
80.033/80.033	CRule InfChecker Info:
80.033/80.033	e(0) -> true
80.033/80.033	Rule remains
80.033/80.033	Proof:
80.033/80.033	NO_CONDS
80.033/80.033	
80.033/80.033	CRule InfChecker Info:
80.033/80.033	e(s(x:S)) -> false | e(x:S) ->* true
80.033/80.033	Rule remains
80.033/80.033	Proof:
80.033/80.033	NO
80.033/80.033	
80.033/80.033	Problem 1:
80.033/80.033	
80.033/80.033	Infeasibility Problem:
80.033/80.033	[(VAR vNonEmpty:S vNonEmpty:S:S x:S:S)
80.033/80.033	(STRATEGY CONTEXTSENSITIVE
80.033/80.033	(e 1)
80.033/80.033	(o 1)
80.033/80.033	(0)
80.033/80.033	(fSNonEmpty)
80.033/80.033	(false)
80.033/80.033	(s 1)
80.033/80.033	(true)
80.033/80.033	)
80.033/80.033	(RULES
80.033/80.033	e(0) -> true
80.033/80.033	e(s(x:S:S)) -> false | e(x:S:S) ->* true
80.033/80.033	e(s(x:S:S)) -> true | o(x:S:S) ->* true
80.033/80.033	o(0) -> true
80.033/80.033	o(s(x:S:S)) -> false | o(x:S:S) ->* true
80.033/80.033	o(s(x:S:S)) -> true | e(x:S:S) ->* true
80.033/80.033	)]
80.033/80.033	
80.033/80.033	Infeasibility Conditions:
80.033/80.033	e(x:S:S) ->* true
80.033/80.033	
80.033/80.033	Problem 1:
80.033/80.033	
80.033/80.033	Obtaining a proof using Prover9:
80.033/80.033	
80.033/80.033	 -> Prover9 Output:
80.033/80.033	============================== Prover9 ===============================
80.033/80.033	Prover9 (64) version 2009-11A, November 2009.
80.033/80.033	Process 52318 was started by ubuntu on ubuntu,
80.033/80.033	Wed Jul 14 11:02:48 2021
80.033/80.033	The command was "./prover9 -f /tmp/prover952308-0.in".
80.033/80.033	============================== end of head ===========================
80.033/80.033	
80.033/80.033	============================== INPUT =================================
80.033/80.033	
80.033/80.033	% Reading from file /tmp/prover952308-0.in
80.033/80.033	
80.033/80.033	assign(max_seconds,20).
80.033/80.033	
80.033/80.033	formulas(assumptions).
80.033/80.033	->*_s0(x,x) # label(reflexivity).
80.033/80.033	->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity).
80.033/80.033	->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence).
80.033/80.033	->_s0(x1,y) -> ->_s0(o(x1),o(y)) # label(congruence).
80.033/80.033	->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence).
80.033/80.033	->_s0(e(0),true) # label(replacement).
80.033/80.033	->*_s0(e(x2),true) -> ->_s0(e(s(x2)),false) # label(replacement).
80.033/80.033	->*_s0(o(x2),true) -> ->_s0(e(s(x2)),true) # label(replacement).
80.033/80.033	->_s0(o(0),true) # label(replacement).
80.033/80.033	->*_s0(o(x2),true) -> ->_s0(o(s(x2)),false) # label(replacement).
80.033/80.033	->*_s0(e(x2),true) -> ->_s0(o(s(x2)),true) # label(replacement).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(goals).
80.033/80.033	(exists x2 ->*_s0(e(x2),true)) # label(goal).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	============================== end of input ==========================
80.033/80.033	
80.033/80.033	============================== PROCESS NON-CLAUSAL FORMULAS ==========
80.033/80.033	
80.033/80.033	% Formulas that are not ordinary clauses:
80.033/80.033	1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
80.033/80.033	2 ->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence) # label(non_clause).  [assumption].
80.033/80.033	3 ->_s0(x1,y) -> ->_s0(o(x1),o(y)) # label(congruence) # label(non_clause).  [assumption].
80.033/80.033	4 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause).  [assumption].
80.033/80.033	5 ->*_s0(e(x2),true) -> ->_s0(e(s(x2)),false) # label(replacement) # label(non_clause).  [assumption].
80.033/80.033	6 ->*_s0(o(x2),true) -> ->_s0(e(s(x2)),true) # label(replacement) # label(non_clause).  [assumption].
80.033/80.033	7 ->*_s0(o(x2),true) -> ->_s0(o(s(x2)),false) # label(replacement) # label(non_clause).  [assumption].
80.033/80.033	8 ->*_s0(e(x2),true) -> ->_s0(o(s(x2)),true) # label(replacement) # label(non_clause).  [assumption].
80.033/80.033	9 (exists x2 ->*_s0(e(x2),true)) # label(goal) # label(non_clause) # label(goal).  [goal].
80.033/80.033	
80.033/80.033	============================== end of process non-clausal formulas ===
80.033/80.033	
80.033/80.033	============================== PROCESS INITIAL CLAUSES ===============
80.033/80.033	
80.033/80.033	% Clauses before input processing:
80.033/80.033	
80.033/80.033	formulas(usable).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(sos).
80.033/80.033	->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	-->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	-->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(2)].
80.033/80.033	-->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence).  [clausify(3)].
80.033/80.033	-->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(4)].
80.033/80.033	->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	-->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement).  [clausify(5)].
80.033/80.033	-->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement).  [clausify(6)].
80.033/80.033	->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	-->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement).  [clausify(7)].
80.033/80.033	-->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement).  [clausify(8)].
80.033/80.033	-->*_s0(e(x),true) # label(goal).  [deny(9)].
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(demodulators).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	============================== PREDICATE ELIMINATION =================
80.033/80.033	
80.033/80.033	No predicates eliminated.
80.033/80.033	
80.033/80.033	============================== end predicate elimination =============
80.033/80.033	
80.033/80.033	Auto_denials:
80.033/80.033	  % copying label goal to answer in negative clause
80.033/80.033	
80.033/80.033	Term ordering decisions:
80.033/80.033	Predicate symbol precedence:  predicate_order([ ->_s0, ->*_s0 ]).
80.033/80.033	Function symbol precedence:  function_order([ true, 0, false, e, o, s ]).
80.033/80.033	After inverse_order:  (no changes).
80.033/80.033	Unfolding symbols: (none).
80.033/80.033	
80.033/80.033	Auto_inference settings:
80.033/80.033	  % set(neg_binary_resolution).  % (HNE depth_diff=-7)
80.033/80.033	  % clear(ordered_res).  % (HNE depth_diff=-7)
80.033/80.033	  % set(ur_resolution).  % (HNE depth_diff=-7)
80.033/80.033	    % set(ur_resolution) -> set(pos_ur_resolution).
80.033/80.033	    % set(ur_resolution) -> set(neg_ur_resolution).
80.033/80.033	
80.033/80.033	Auto_process settings:  (no changes).
80.033/80.033	
80.033/80.033	kept:      10 ->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	kept:      11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	kept:      12 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(2)].
80.033/80.033	kept:      13 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence).  [clausify(3)].
80.033/80.033	kept:      14 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(4)].
80.033/80.033	kept:      15 ->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	kept:      16 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement).  [clausify(5)].
80.033/80.033	kept:      17 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement).  [clausify(6)].
80.033/80.033	kept:      18 ->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	kept:      19 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement).  [clausify(7)].
80.033/80.033	kept:      20 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement).  [clausify(8)].
80.033/80.033	kept:      21 -->*_s0(e(x),true) # label(goal) # answer(goal).  [deny(9)].
80.033/80.033	
80.033/80.033	============================== end of process initial clauses ========
80.033/80.033	
80.033/80.033	============================== CLAUSES FOR SEARCH ====================
80.033/80.033	
80.033/80.033	% Clauses after input processing:
80.033/80.033	
80.033/80.033	formulas(usable).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(sos).
80.033/80.033	10 ->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	12 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(2)].
80.033/80.033	13 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence).  [clausify(3)].
80.033/80.033	14 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(4)].
80.033/80.033	15 ->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	17 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement).  [clausify(6)].
80.033/80.033	18 ->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	19 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement).  [clausify(7)].
80.033/80.033	21 -->*_s0(e(x),true) # label(goal) # answer(goal).  [deny(9)].
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(demodulators).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	============================== end of clauses for search =============
80.033/80.033	
80.033/80.033	============================== SEARCH ================================
80.033/80.033	
80.033/80.033	% Starting search at 0.00 seconds.
80.033/80.033	
80.033/80.033	given #1 (I,wt=3): 10 ->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	
80.033/80.033	given #2 (I,wt=9): 11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	
80.033/80.033	given #3 (I,wt=8): 12 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(2)].
80.033/80.033	
80.033/80.033	given #4 (I,wt=8): 13 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence).  [clausify(3)].
80.033/80.033	
80.033/80.033	given #5 (I,wt=8): 14 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(4)].
80.033/80.033	
80.033/80.033	given #6 (I,wt=4): 15 ->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	
80.033/80.033	============================== PROOF =================================
80.033/80.033	
80.033/80.033	% Proof 1 at 0.00 (+ 0.00) seconds: goal.
80.033/80.033	% Length of proof is 8.
80.033/80.033	% Level of proof is 3.
80.033/80.033	% Maximum clause weight is 9.000.
80.033/80.033	% Given clauses 6.
80.033/80.033	
80.033/80.033	1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
80.033/80.033	9 (exists x2 ->*_s0(e(x2),true)) # label(goal) # label(non_clause) # label(goal).  [goal].
80.033/80.033	10 ->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	15 ->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	21 -->*_s0(e(x),true) # label(goal) # answer(goal).  [deny(9)].
80.033/80.033	25 ->*_s0(e(0),true).  [ur(11,a,15,a,b,10,a)].
80.033/80.033	26 $F # answer(goal).  [resolve(25,a,21,a)].
80.033/80.033	
80.033/80.033	============================== end of proof ==========================
80.033/80.033	
80.033/80.033	============================== STATISTICS ============================
80.033/80.033	
80.033/80.033	Given=6. Generated=16. Kept=16. proofs=1.
80.033/80.033	Usable=6. Sos=4. Demods=0. Limbo=3, Disabled=14. Hints=0.
80.033/80.033	Kept_by_rule=0, Deleted_by_rule=0.
80.033/80.033	Forward_subsumed=0. Back_subsumed=2.
80.033/80.033	Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
80.033/80.033	New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
80.033/80.033	Demod_attempts=0. Demod_rewrites=0.
80.033/80.033	Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
80.033/80.033	Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=11.
80.033/80.033	Megabytes=0.07.
80.033/80.033	User_CPU=0.00, System_CPU=0.00, Wall_clock=0.
80.033/80.033	
80.033/80.033	============================== end of statistics =====================
80.033/80.033	
80.033/80.033	============================== end of search =========================
80.033/80.033	
80.033/80.033	THEOREM PROVED
80.033/80.033	
80.033/80.033	Exiting with 1 proof.
80.033/80.033	
80.033/80.033	Process 52318 exit (max_proofs) Wed Jul 14 11:02:48 2021
80.033/80.033	
80.033/80.033	
80.033/80.033	The problem is feasible.
80.033/80.033	
80.033/80.033	
80.033/80.033	CRule InfChecker Info:
80.033/80.033	e(s(x:S)) -> true | o(x:S) ->* true
80.033/80.033	Rule remains
80.033/80.033	Proof:
80.033/80.033	NO
80.033/80.033	
80.033/80.033	Problem 1:
80.033/80.033	
80.033/80.033	Infeasibility Problem:
80.033/80.033	[(VAR vNonEmpty:S vNonEmpty:S:S x:S:S)
80.033/80.033	(STRATEGY CONTEXTSENSITIVE
80.033/80.033	(e 1)
80.033/80.033	(o 1)
80.033/80.033	(0)
80.033/80.033	(fSNonEmpty)
80.033/80.033	(false)
80.033/80.033	(s 1)
80.033/80.033	(true)
80.033/80.033	)
80.033/80.033	(RULES
80.033/80.033	e(0) -> true
80.033/80.033	e(s(x:S:S)) -> false | e(x:S:S) ->* true
80.033/80.033	e(s(x:S:S)) -> true | o(x:S:S) ->* true
80.033/80.033	o(0) -> true
80.033/80.033	o(s(x:S:S)) -> false | o(x:S:S) ->* true
80.033/80.033	o(s(x:S:S)) -> true | e(x:S:S) ->* true
80.033/80.033	)]
80.033/80.033	
80.033/80.033	Infeasibility Conditions:
80.033/80.033	o(x:S:S) ->* true
80.033/80.033	
80.033/80.033	Problem 1:
80.033/80.033	
80.033/80.033	Obtaining a proof using Prover9:
80.033/80.033	
80.033/80.033	 -> Prover9 Output:
80.033/80.033	============================== Prover9 ===============================
80.033/80.033	Prover9 (64) version 2009-11A, November 2009.
80.033/80.033	Process 52342 was started by ubuntu on ubuntu,
80.033/80.033	Wed Jul 14 11:02:48 2021
80.033/80.033	The command was "./prover9 -f /tmp/prover952330-0.in".
80.033/80.033	============================== end of head ===========================
80.033/80.033	
80.033/80.033	============================== INPUT =================================
80.033/80.033	
80.033/80.033	% Reading from file /tmp/prover952330-0.in
80.033/80.033	
80.033/80.033	assign(max_seconds,20).
80.033/80.033	
80.033/80.033	formulas(assumptions).
80.033/80.033	->*_s0(x,x) # label(reflexivity).
80.033/80.033	->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity).
80.033/80.033	->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence).
80.033/80.033	->_s0(x1,y) -> ->_s0(o(x1),o(y)) # label(congruence).
80.033/80.033	->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence).
80.033/80.033	->_s0(e(0),true) # label(replacement).
80.033/80.033	->*_s0(e(x2),true) -> ->_s0(e(s(x2)),false) # label(replacement).
80.033/80.033	->*_s0(o(x2),true) -> ->_s0(e(s(x2)),true) # label(replacement).
80.033/80.033	->_s0(o(0),true) # label(replacement).
80.033/80.033	->*_s0(o(x2),true) -> ->_s0(o(s(x2)),false) # label(replacement).
80.033/80.033	->*_s0(e(x2),true) -> ->_s0(o(s(x2)),true) # label(replacement).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(goals).
80.033/80.033	(exists x2 ->*_s0(o(x2),true)) # label(goal).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	============================== end of input ==========================
80.033/80.033	
80.033/80.033	============================== PROCESS NON-CLAUSAL FORMULAS ==========
80.033/80.033	
80.033/80.033	% Formulas that are not ordinary clauses:
80.033/80.033	1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
80.033/80.033	2 ->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence) # label(non_clause).  [assumption].
80.033/80.033	3 ->_s0(x1,y) -> ->_s0(o(x1),o(y)) # label(congruence) # label(non_clause).  [assumption].
80.033/80.033	4 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause).  [assumption].
80.033/80.033	5 ->*_s0(e(x2),true) -> ->_s0(e(s(x2)),false) # label(replacement) # label(non_clause).  [assumption].
80.033/80.033	6 ->*_s0(o(x2),true) -> ->_s0(e(s(x2)),true) # label(replacement) # label(non_clause).  [assumption].
80.033/80.033	7 ->*_s0(o(x2),true) -> ->_s0(o(s(x2)),false) # label(replacement) # label(non_clause).  [assumption].
80.033/80.033	8 ->*_s0(e(x2),true) -> ->_s0(o(s(x2)),true) # label(replacement) # label(non_clause).  [assumption].
80.033/80.033	9 (exists x2 ->*_s0(o(x2),true)) # label(goal) # label(non_clause) # label(goal).  [goal].
80.033/80.033	
80.033/80.033	============================== end of process non-clausal formulas ===
80.033/80.033	
80.033/80.033	============================== PROCESS INITIAL CLAUSES ===============
80.033/80.033	
80.033/80.033	% Clauses before input processing:
80.033/80.033	
80.033/80.033	formulas(usable).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(sos).
80.033/80.033	->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	-->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	-->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(2)].
80.033/80.033	-->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence).  [clausify(3)].
80.033/80.033	-->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(4)].
80.033/80.033	->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	-->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement).  [clausify(5)].
80.033/80.033	-->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement).  [clausify(6)].
80.033/80.033	->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	-->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement).  [clausify(7)].
80.033/80.033	-->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement).  [clausify(8)].
80.033/80.033	-->*_s0(o(x),true) # label(goal).  [deny(9)].
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(demodulators).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	============================== PREDICATE ELIMINATION =================
80.033/80.033	
80.033/80.033	No predicates eliminated.
80.033/80.033	
80.033/80.033	============================== end predicate elimination =============
80.033/80.033	
80.033/80.033	Auto_denials:
80.033/80.033	  % copying label goal to answer in negative clause
80.033/80.033	
80.033/80.033	Term ordering decisions:
80.033/80.033	Predicate symbol precedence:  predicate_order([ ->_s0, ->*_s0 ]).
80.033/80.033	Function symbol precedence:  function_order([ true, 0, false, e, o, s ]).
80.033/80.033	After inverse_order:  (no changes).
80.033/80.033	Unfolding symbols: (none).
80.033/80.033	
80.033/80.033	Auto_inference settings:
80.033/80.033	  % set(neg_binary_resolution).  % (HNE depth_diff=-7)
80.033/80.033	  % clear(ordered_res).  % (HNE depth_diff=-7)
80.033/80.033	  % set(ur_resolution).  % (HNE depth_diff=-7)
80.033/80.033	    % set(ur_resolution) -> set(pos_ur_resolution).
80.033/80.033	    % set(ur_resolution) -> set(neg_ur_resolution).
80.033/80.033	
80.033/80.033	Auto_process settings:  (no changes).
80.033/80.033	
80.033/80.033	kept:      10 ->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	kept:      11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	kept:      12 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(2)].
80.033/80.033	kept:      13 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence).  [clausify(3)].
80.033/80.033	kept:      14 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(4)].
80.033/80.033	kept:      15 ->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	kept:      16 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement).  [clausify(5)].
80.033/80.033	kept:      17 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement).  [clausify(6)].
80.033/80.033	kept:      18 ->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	kept:      19 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement).  [clausify(7)].
80.033/80.033	kept:      20 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement).  [clausify(8)].
80.033/80.033	kept:      21 -->*_s0(o(x),true) # label(goal) # answer(goal).  [deny(9)].
80.033/80.033	
80.033/80.033	============================== end of process initial clauses ========
80.033/80.033	
80.033/80.033	============================== CLAUSES FOR SEARCH ====================
80.033/80.033	
80.033/80.033	% Clauses after input processing:
80.033/80.033	
80.033/80.033	formulas(usable).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(sos).
80.033/80.033	10 ->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	12 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(2)].
80.033/80.033	13 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence).  [clausify(3)].
80.033/80.033	14 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(4)].
80.033/80.033	15 ->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	16 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement).  [clausify(5)].
80.033/80.033	18 ->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	20 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement).  [clausify(8)].
80.033/80.033	21 -->*_s0(o(x),true) # label(goal) # answer(goal).  [deny(9)].
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(demodulators).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	============================== end of clauses for search =============
80.033/80.033	
80.033/80.033	============================== SEARCH ================================
80.033/80.033	
80.033/80.033	% Starting search at 0.00 seconds.
80.033/80.033	
80.033/80.033	given #1 (I,wt=3): 10 ->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	
80.033/80.033	given #2 (I,wt=9): 11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	
80.033/80.033	given #3 (I,wt=8): 12 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(2)].
80.033/80.033	
80.033/80.033	given #4 (I,wt=8): 13 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence).  [clausify(3)].
80.033/80.033	
80.033/80.033	given #5 (I,wt=8): 14 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(4)].
80.033/80.033	
80.033/80.033	given #6 (I,wt=4): 15 ->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	
80.033/80.033	given #7 (I,wt=9): 16 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement).  [clausify(5)].
80.033/80.033	
80.033/80.033	given #8 (I,wt=4): 18 ->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	
80.033/80.033	============================== PROOF =================================
80.033/80.033	
80.033/80.033	% Proof 1 at 0.00 (+ 0.00) seconds: goal.
80.033/80.033	% Length of proof is 8.
80.033/80.033	% Level of proof is 3.
80.033/80.033	% Maximum clause weight is 9.000.
80.033/80.033	% Given clauses 8.
80.033/80.033	
80.033/80.033	1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
80.033/80.033	9 (exists x2 ->*_s0(o(x2),true)) # label(goal) # label(non_clause) # label(goal).  [goal].
80.033/80.033	10 ->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	18 ->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	21 -->*_s0(o(x),true) # label(goal) # answer(goal).  [deny(9)].
80.033/80.033	29 ->*_s0(o(0),true).  [ur(11,a,18,a,b,10,a)].
80.033/80.033	30 $F # answer(goal).  [resolve(29,a,21,a)].
80.033/80.033	
80.033/80.033	============================== end of proof ==========================
80.033/80.033	
80.033/80.033	============================== STATISTICS ============================
80.033/80.033	
80.033/80.033	Given=8. Generated=20. Kept=20. proofs=1.
80.033/80.033	Usable=8. Sos=6. Demods=0. Limbo=3, Disabled=14. Hints=0.
80.033/80.033	Kept_by_rule=0, Deleted_by_rule=0.
80.033/80.033	Forward_subsumed=0. Back_subsumed=2.
80.033/80.033	Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
80.033/80.033	New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
80.033/80.033	Demod_attempts=0. Demod_rewrites=0.
80.033/80.033	Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
80.033/80.033	Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=11.
80.033/80.033	Megabytes=0.07.
80.033/80.033	User_CPU=0.00, System_CPU=0.00, Wall_clock=0.
80.033/80.033	
80.033/80.033	============================== end of statistics =====================
80.033/80.033	
80.033/80.033	============================== end of search =========================
80.033/80.033	
80.033/80.033	THEOREM PROVED
80.033/80.033	
80.033/80.033	Exiting with 1 proof.
80.033/80.033	
80.033/80.033	Process 52342 exit (max_proofs) Wed Jul 14 11:02:48 2021
80.033/80.033	
80.033/80.033	
80.033/80.033	The problem is feasible.
80.033/80.033	
80.033/80.033	
80.033/80.033	CRule InfChecker Info:
80.033/80.033	o(0) -> true
80.033/80.033	Rule remains
80.033/80.033	Proof:
80.033/80.033	NO_CONDS
80.033/80.033	
80.033/80.033	CRule InfChecker Info:
80.033/80.033	o(s(x:S)) -> false | o(x:S) ->* true
80.033/80.033	Rule remains
80.033/80.033	Proof:
80.033/80.033	NO
80.033/80.033	
80.033/80.033	Problem 1:
80.033/80.033	
80.033/80.033	Infeasibility Problem:
80.033/80.033	[(VAR vNonEmpty:S vNonEmpty:S:S x:S:S)
80.033/80.033	(STRATEGY CONTEXTSENSITIVE
80.033/80.033	(e 1)
80.033/80.033	(o 1)
80.033/80.033	(0)
80.033/80.033	(fSNonEmpty)
80.033/80.033	(false)
80.033/80.033	(s 1)
80.033/80.033	(true)
80.033/80.033	)
80.033/80.033	(RULES
80.033/80.033	e(0) -> true
80.033/80.033	e(s(x:S:S)) -> false | e(x:S:S) ->* true
80.033/80.033	e(s(x:S:S)) -> true | o(x:S:S) ->* true
80.033/80.033	o(0) -> true
80.033/80.033	o(s(x:S:S)) -> false | o(x:S:S) ->* true
80.033/80.033	o(s(x:S:S)) -> true | e(x:S:S) ->* true
80.033/80.033	)]
80.033/80.033	
80.033/80.033	Infeasibility Conditions:
80.033/80.033	o(x:S:S) ->* true
80.033/80.033	
80.033/80.033	Problem 1:
80.033/80.033	
80.033/80.033	Obtaining a proof using Prover9:
80.033/80.033	
80.033/80.033	 -> Prover9 Output:
80.033/80.033	============================== Prover9 ===============================
80.033/80.033	Prover9 (64) version 2009-11A, November 2009.
80.033/80.033	Process 52363 was started by ubuntu on ubuntu,
80.033/80.033	Wed Jul 14 11:02:48 2021
80.033/80.033	The command was "./prover9 -f /tmp/prover952352-0.in".
80.033/80.033	============================== end of head ===========================
80.033/80.033	
80.033/80.033	============================== INPUT =================================
80.033/80.033	
80.033/80.033	% Reading from file /tmp/prover952352-0.in
80.033/80.033	
80.033/80.033	assign(max_seconds,20).
80.033/80.033	
80.033/80.033	formulas(assumptions).
80.033/80.033	->*_s0(x,x) # label(reflexivity).
80.033/80.033	->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity).
80.033/80.033	->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence).
80.033/80.033	->_s0(x1,y) -> ->_s0(o(x1),o(y)) # label(congruence).
80.033/80.033	->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence).
80.033/80.033	->_s0(e(0),true) # label(replacement).
80.033/80.033	->*_s0(e(x2),true) -> ->_s0(e(s(x2)),false) # label(replacement).
80.033/80.033	->*_s0(o(x2),true) -> ->_s0(e(s(x2)),true) # label(replacement).
80.033/80.033	->_s0(o(0),true) # label(replacement).
80.033/80.033	->*_s0(o(x2),true) -> ->_s0(o(s(x2)),false) # label(replacement).
80.033/80.033	->*_s0(e(x2),true) -> ->_s0(o(s(x2)),true) # label(replacement).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(goals).
80.033/80.033	(exists x2 ->*_s0(o(x2),true)) # label(goal).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	============================== end of input ==========================
80.033/80.033	
80.033/80.033	============================== PROCESS NON-CLAUSAL FORMULAS ==========
80.033/80.033	
80.033/80.033	% Formulas that are not ordinary clauses:
80.033/80.033	1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
80.033/80.033	2 ->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence) # label(non_clause).  [assumption].
80.033/80.033	3 ->_s0(x1,y) -> ->_s0(o(x1),o(y)) # label(congruence) # label(non_clause).  [assumption].
80.033/80.033	4 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause).  [assumption].
80.033/80.033	5 ->*_s0(e(x2),true) -> ->_s0(e(s(x2)),false) # label(replacement) # label(non_clause).  [assumption].
80.033/80.033	6 ->*_s0(o(x2),true) -> ->_s0(e(s(x2)),true) # label(replacement) # label(non_clause).  [assumption].
80.033/80.033	7 ->*_s0(o(x2),true) -> ->_s0(o(s(x2)),false) # label(replacement) # label(non_clause).  [assumption].
80.033/80.033	8 ->*_s0(e(x2),true) -> ->_s0(o(s(x2)),true) # label(replacement) # label(non_clause).  [assumption].
80.033/80.033	9 (exists x2 ->*_s0(o(x2),true)) # label(goal) # label(non_clause) # label(goal).  [goal].
80.033/80.033	
80.033/80.033	============================== end of process non-clausal formulas ===
80.033/80.033	
80.033/80.033	============================== PROCESS INITIAL CLAUSES ===============
80.033/80.033	
80.033/80.033	% Clauses before input processing:
80.033/80.033	
80.033/80.033	formulas(usable).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(sos).
80.033/80.033	->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	-->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	-->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(2)].
80.033/80.033	-->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence).  [clausify(3)].
80.033/80.033	-->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(4)].
80.033/80.033	->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	-->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement).  [clausify(5)].
80.033/80.033	-->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement).  [clausify(6)].
80.033/80.033	->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	-->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement).  [clausify(7)].
80.033/80.033	-->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement).  [clausify(8)].
80.033/80.033	-->*_s0(o(x),true) # label(goal).  [deny(9)].
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(demodulators).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	============================== PREDICATE ELIMINATION =================
80.033/80.033	
80.033/80.033	No predicates eliminated.
80.033/80.033	
80.033/80.033	============================== end predicate elimination =============
80.033/80.033	
80.033/80.033	Auto_denials:
80.033/80.033	  % copying label goal to answer in negative clause
80.033/80.033	
80.033/80.033	Term ordering decisions:
80.033/80.033	Predicate symbol precedence:  predicate_order([ ->_s0, ->*_s0 ]).
80.033/80.033	Function symbol precedence:  function_order([ true, 0, false, e, o, s ]).
80.033/80.033	After inverse_order:  (no changes).
80.033/80.033	Unfolding symbols: (none).
80.033/80.033	
80.033/80.033	Auto_inference settings:
80.033/80.033	  % set(neg_binary_resolution).  % (HNE depth_diff=-7)
80.033/80.033	  % clear(ordered_res).  % (HNE depth_diff=-7)
80.033/80.033	  % set(ur_resolution).  % (HNE depth_diff=-7)
80.033/80.033	    % set(ur_resolution) -> set(pos_ur_resolution).
80.033/80.033	    % set(ur_resolution) -> set(neg_ur_resolution).
80.033/80.033	
80.033/80.033	Auto_process settings:  (no changes).
80.033/80.033	
80.033/80.033	kept:      10 ->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	kept:      11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	kept:      12 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(2)].
80.033/80.033	kept:      13 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence).  [clausify(3)].
80.033/80.033	kept:      14 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(4)].
80.033/80.033	kept:      15 ->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	kept:      16 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement).  [clausify(5)].
80.033/80.033	kept:      17 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement).  [clausify(6)].
80.033/80.033	kept:      18 ->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	kept:      19 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement).  [clausify(7)].
80.033/80.033	kept:      20 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement).  [clausify(8)].
80.033/80.033	kept:      21 -->*_s0(o(x),true) # label(goal) # answer(goal).  [deny(9)].
80.033/80.033	
80.033/80.033	============================== end of process initial clauses ========
80.033/80.033	
80.033/80.033	============================== CLAUSES FOR SEARCH ====================
80.033/80.033	
80.033/80.033	% Clauses after input processing:
80.033/80.033	
80.033/80.033	formulas(usable).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(sos).
80.033/80.033	10 ->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	12 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(2)].
80.033/80.033	13 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence).  [clausify(3)].
80.033/80.033	14 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(4)].
80.033/80.033	15 ->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	16 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement).  [clausify(5)].
80.033/80.033	18 ->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	20 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement).  [clausify(8)].
80.033/80.033	21 -->*_s0(o(x),true) # label(goal) # answer(goal).  [deny(9)].
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(demodulators).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	============================== end of clauses for search =============
80.033/80.033	
80.033/80.033	============================== SEARCH ================================
80.033/80.033	
80.033/80.033	% Starting search at 0.00 seconds.
80.033/80.033	
80.033/80.033	given #1 (I,wt=3): 10 ->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	
80.033/80.033	given #2 (I,wt=9): 11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	
80.033/80.033	given #3 (I,wt=8): 12 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(2)].
80.033/80.033	
80.033/80.033	given #4 (I,wt=8): 13 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence).  [clausify(3)].
80.033/80.033	
80.033/80.033	given #5 (I,wt=8): 14 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(4)].
80.033/80.033	
80.033/80.033	given #6 (I,wt=4): 15 ->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	
80.033/80.033	given #7 (I,wt=9): 16 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement).  [clausify(5)].
80.033/80.033	
80.033/80.033	given #8 (I,wt=4): 18 ->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	
80.033/80.033	============================== PROOF =================================
80.033/80.033	
80.033/80.033	% Proof 1 at 0.00 (+ 0.00) seconds: goal.
80.033/80.033	% Length of proof is 8.
80.033/80.033	% Level of proof is 3.
80.033/80.033	% Maximum clause weight is 9.000.
80.033/80.033	% Given clauses 8.
80.033/80.033	
80.033/80.033	1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
80.033/80.033	9 (exists x2 ->*_s0(o(x2),true)) # label(goal) # label(non_clause) # label(goal).  [goal].
80.033/80.033	10 ->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	18 ->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	21 -->*_s0(o(x),true) # label(goal) # answer(goal).  [deny(9)].
80.033/80.033	29 ->*_s0(o(0),true).  [ur(11,a,18,a,b,10,a)].
80.033/80.033	30 $F # answer(goal).  [resolve(29,a,21,a)].
80.033/80.033	
80.033/80.033	============================== end of proof ==========================
80.033/80.033	
80.033/80.033	============================== STATISTICS ============================
80.033/80.033	
80.033/80.033	Given=8. Generated=20. Kept=20. proofs=1.
80.033/80.033	Usable=8. Sos=6. Demods=0. Limbo=3, Disabled=14. Hints=0.
80.033/80.033	Kept_by_rule=0, Deleted_by_rule=0.
80.033/80.033	Forward_subsumed=0. Back_subsumed=2.
80.033/80.033	Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
80.033/80.033	New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
80.033/80.033	Demod_attempts=0. Demod_rewrites=0.
80.033/80.033	Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
80.033/80.033	Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=11.
80.033/80.033	Megabytes=0.07.
80.033/80.033	User_CPU=0.00, System_CPU=0.00, Wall_clock=0.
80.033/80.033	
80.033/80.033	============================== end of statistics =====================
80.033/80.033	
80.033/80.033	============================== end of search =========================
80.033/80.033	
80.033/80.033	THEOREM PROVED
80.033/80.033	
80.033/80.033	Exiting with 1 proof.
80.033/80.033	
80.033/80.033	Process 52363 exit (max_proofs) Wed Jul 14 11:02:48 2021
80.033/80.033	
80.033/80.033	
80.033/80.033	The problem is feasible.
80.033/80.033	
80.033/80.033	
80.033/80.033	CRule InfChecker Info:
80.033/80.033	o(s(x:S)) -> true | e(x:S) ->* true
80.033/80.033	Rule remains
80.033/80.033	Proof:
80.033/80.033	NO
80.033/80.033	
80.033/80.033	Problem 1:
80.033/80.033	
80.033/80.033	Infeasibility Problem:
80.033/80.033	[(VAR vNonEmpty:S vNonEmpty:S:S x:S:S)
80.033/80.033	(STRATEGY CONTEXTSENSITIVE
80.033/80.033	(e 1)
80.033/80.033	(o 1)
80.033/80.033	(0)
80.033/80.033	(fSNonEmpty)
80.033/80.033	(false)
80.033/80.033	(s 1)
80.033/80.033	(true)
80.033/80.033	)
80.033/80.033	(RULES
80.033/80.033	e(0) -> true
80.033/80.033	e(s(x:S:S)) -> false | e(x:S:S) ->* true
80.033/80.033	e(s(x:S:S)) -> true | o(x:S:S) ->* true
80.033/80.033	o(0) -> true
80.033/80.033	o(s(x:S:S)) -> false | o(x:S:S) ->* true
80.033/80.033	o(s(x:S:S)) -> true | e(x:S:S) ->* true
80.033/80.033	)]
80.033/80.033	
80.033/80.033	Infeasibility Conditions:
80.033/80.033	e(x:S:S) ->* true
80.033/80.033	
80.033/80.033	Problem 1:
80.033/80.033	
80.033/80.033	Obtaining a proof using Prover9:
80.033/80.033	
80.033/80.033	 -> Prover9 Output:
80.033/80.033	============================== Prover9 ===============================
80.033/80.033	Prover9 (64) version 2009-11A, November 2009.
80.033/80.033	Process 52386 was started by ubuntu on ubuntu,
80.033/80.033	Wed Jul 14 11:02:48 2021
80.033/80.033	The command was "./prover9 -f /tmp/prover952373-0.in".
80.033/80.033	============================== end of head ===========================
80.033/80.033	
80.033/80.033	============================== INPUT =================================
80.033/80.033	
80.033/80.033	% Reading from file /tmp/prover952373-0.in
80.033/80.033	
80.033/80.033	assign(max_seconds,20).
80.033/80.033	
80.033/80.033	formulas(assumptions).
80.033/80.033	->*_s0(x,x) # label(reflexivity).
80.033/80.033	->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity).
80.033/80.033	->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence).
80.033/80.033	->_s0(x1,y) -> ->_s0(o(x1),o(y)) # label(congruence).
80.033/80.033	->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence).
80.033/80.033	->_s0(e(0),true) # label(replacement).
80.033/80.033	->*_s0(e(x2),true) -> ->_s0(e(s(x2)),false) # label(replacement).
80.033/80.033	->*_s0(o(x2),true) -> ->_s0(e(s(x2)),true) # label(replacement).
80.033/80.033	->_s0(o(0),true) # label(replacement).
80.033/80.033	->*_s0(o(x2),true) -> ->_s0(o(s(x2)),false) # label(replacement).
80.033/80.033	->*_s0(e(x2),true) -> ->_s0(o(s(x2)),true) # label(replacement).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(goals).
80.033/80.033	(exists x2 ->*_s0(e(x2),true)) # label(goal).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	============================== end of input ==========================
80.033/80.033	
80.033/80.033	============================== PROCESS NON-CLAUSAL FORMULAS ==========
80.033/80.033	
80.033/80.033	% Formulas that are not ordinary clauses:
80.033/80.033	1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
80.033/80.033	2 ->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence) # label(non_clause).  [assumption].
80.033/80.033	3 ->_s0(x1,y) -> ->_s0(o(x1),o(y)) # label(congruence) # label(non_clause).  [assumption].
80.033/80.033	4 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause).  [assumption].
80.033/80.033	5 ->*_s0(e(x2),true) -> ->_s0(e(s(x2)),false) # label(replacement) # label(non_clause).  [assumption].
80.033/80.033	6 ->*_s0(o(x2),true) -> ->_s0(e(s(x2)),true) # label(replacement) # label(non_clause).  [assumption].
80.033/80.033	7 ->*_s0(o(x2),true) -> ->_s0(o(s(x2)),false) # label(replacement) # label(non_clause).  [assumption].
80.033/80.033	8 ->*_s0(e(x2),true) -> ->_s0(o(s(x2)),true) # label(replacement) # label(non_clause).  [assumption].
80.033/80.033	9 (exists x2 ->*_s0(e(x2),true)) # label(goal) # label(non_clause) # label(goal).  [goal].
80.033/80.033	
80.033/80.033	============================== end of process non-clausal formulas ===
80.033/80.033	
80.033/80.033	============================== PROCESS INITIAL CLAUSES ===============
80.033/80.033	
80.033/80.033	% Clauses before input processing:
80.033/80.033	
80.033/80.033	formulas(usable).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(sos).
80.033/80.033	->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	-->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	-->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(2)].
80.033/80.033	-->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence).  [clausify(3)].
80.033/80.033	-->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(4)].
80.033/80.033	->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	-->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement).  [clausify(5)].
80.033/80.033	-->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement).  [clausify(6)].
80.033/80.033	->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	-->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement).  [clausify(7)].
80.033/80.033	-->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement).  [clausify(8)].
80.033/80.033	-->*_s0(e(x),true) # label(goal).  [deny(9)].
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(demodulators).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	============================== PREDICATE ELIMINATION =================
80.033/80.033	
80.033/80.033	No predicates eliminated.
80.033/80.033	
80.033/80.033	============================== end predicate elimination =============
80.033/80.033	
80.033/80.033	Auto_denials:
80.033/80.033	  % copying label goal to answer in negative clause
80.033/80.033	
80.033/80.033	Term ordering decisions:
80.033/80.033	Predicate symbol precedence:  predicate_order([ ->_s0, ->*_s0 ]).
80.033/80.033	Function symbol precedence:  function_order([ true, 0, false, e, o, s ]).
80.033/80.033	After inverse_order:  (no changes).
80.033/80.033	Unfolding symbols: (none).
80.033/80.033	
80.033/80.033	Auto_inference settings:
80.033/80.033	  % set(neg_binary_resolution).  % (HNE depth_diff=-7)
80.033/80.033	  % clear(ordered_res).  % (HNE depth_diff=-7)
80.033/80.033	  % set(ur_resolution).  % (HNE depth_diff=-7)
80.033/80.033	    % set(ur_resolution) -> set(pos_ur_resolution).
80.033/80.033	    % set(ur_resolution) -> set(neg_ur_resolution).
80.033/80.033	
80.033/80.033	Auto_process settings:  (no changes).
80.033/80.033	
80.033/80.033	kept:      10 ->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	kept:      11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	kept:      12 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(2)].
80.033/80.033	kept:      13 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence).  [clausify(3)].
80.033/80.033	kept:      14 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(4)].
80.033/80.033	kept:      15 ->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	kept:      16 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement).  [clausify(5)].
80.033/80.033	kept:      17 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement).  [clausify(6)].
80.033/80.033	kept:      18 ->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	kept:      19 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement).  [clausify(7)].
80.033/80.033	kept:      20 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement).  [clausify(8)].
80.033/80.033	kept:      21 -->*_s0(e(x),true) # label(goal) # answer(goal).  [deny(9)].
80.033/80.033	
80.033/80.033	============================== end of process initial clauses ========
80.033/80.033	
80.033/80.033	============================== CLAUSES FOR SEARCH ====================
80.033/80.033	
80.033/80.033	% Clauses after input processing:
80.033/80.033	
80.033/80.033	formulas(usable).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(sos).
80.033/80.033	10 ->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	12 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(2)].
80.033/80.033	13 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence).  [clausify(3)].
80.033/80.033	14 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(4)].
80.033/80.033	15 ->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	17 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement).  [clausify(6)].
80.033/80.033	18 ->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	19 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement).  [clausify(7)].
80.033/80.033	21 -->*_s0(e(x),true) # label(goal) # answer(goal).  [deny(9)].
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(demodulators).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	============================== end of clauses for search =============
80.033/80.033	
80.033/80.033	============================== SEARCH ================================
80.033/80.033	
80.033/80.033	% Starting search at 0.00 seconds.
80.033/80.033	
80.033/80.033	given #1 (I,wt=3): 10 ->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	
80.033/80.033	given #2 (I,wt=9): 11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	
80.033/80.033	given #3 (I,wt=8): 12 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(2)].
80.033/80.033	
80.033/80.033	given #4 (I,wt=8): 13 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence).  [clausify(3)].
80.033/80.033	
80.033/80.033	given #5 (I,wt=8): 14 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(4)].
80.033/80.033	
80.033/80.033	given #6 (I,wt=4): 15 ->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	
80.033/80.033	============================== PROOF =================================
80.033/80.033	
80.033/80.033	% Proof 1 at 0.00 (+ 0.00) seconds: goal.
80.033/80.033	% Length of proof is 8.
80.033/80.033	% Level of proof is 3.
80.033/80.033	% Maximum clause weight is 9.000.
80.033/80.033	% Given clauses 6.
80.033/80.033	
80.033/80.033	1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
80.033/80.033	9 (exists x2 ->*_s0(e(x2),true)) # label(goal) # label(non_clause) # label(goal).  [goal].
80.033/80.033	10 ->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	15 ->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	21 -->*_s0(e(x),true) # label(goal) # answer(goal).  [deny(9)].
80.033/80.033	25 ->*_s0(e(0),true).  [ur(11,a,15,a,b,10,a)].
80.033/80.033	26 $F # answer(goal).  [resolve(25,a,21,a)].
80.033/80.033	
80.033/80.033	============================== end of proof ==========================
80.033/80.033	
80.033/80.033	============================== STATISTICS ============================
80.033/80.033	
80.033/80.033	Given=6. Generated=16. Kept=16. proofs=1.
80.033/80.033	Usable=6. Sos=4. Demods=0. Limbo=3, Disabled=14. Hints=0.
80.033/80.033	Kept_by_rule=0, Deleted_by_rule=0.
80.033/80.033	Forward_subsumed=0. Back_subsumed=2.
80.033/80.033	Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
80.033/80.033	New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
80.033/80.033	Demod_attempts=0. Demod_rewrites=0.
80.033/80.033	Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
80.033/80.033	Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=11.
80.033/80.033	Megabytes=0.07.
80.033/80.033	User_CPU=0.00, System_CPU=0.00, Wall_clock=0.
80.033/80.033	
80.033/80.033	============================== end of statistics =====================
80.033/80.033	
80.033/80.033	============================== end of search =========================
80.033/80.033	
80.033/80.033	THEOREM PROVED
80.033/80.033	
80.033/80.033	Exiting with 1 proof.
80.033/80.033	
80.033/80.033	Process 52386 exit (max_proofs) Wed Jul 14 11:02:48 2021
80.033/80.033	
80.033/80.033	
80.033/80.033	The problem is feasible.
80.033/80.033	
80.033/80.033	
80.033/80.033	Problem 1:
80.033/80.033	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
80.033/80.033	Confluence Problem:
80.033/80.033	(VAR x:S)
80.033/80.033	(STRATEGY CONTEXTSENSITIVE
80.033/80.033	(e 1)
80.033/80.033	(o 1)
80.033/80.033	(0)
80.033/80.033	(fSNonEmpty)
80.033/80.033	(false)
80.033/80.033	(s 1)
80.033/80.033	(true)
80.033/80.033	)
80.033/80.033	(RULES
80.033/80.033	e(0) -> true
80.033/80.033	e(s(x:S)) -> false | e(x:S) ->* true
80.033/80.033	e(s(x:S)) -> true | o(x:S) ->* true
80.033/80.033	o(0) -> true
80.033/80.033	o(s(x:S)) -> false | o(x:S) ->* true
80.033/80.033	o(s(x:S)) -> true | e(x:S) ->* true
80.033/80.033	)
80.033/80.033	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
80.033/80.033	
80.033/80.033	Critical Pairs Processor:
80.033/80.033	-> Rules:
80.033/80.033	e(0) -> true
80.033/80.033	e(s(x:S)) -> false | e(x:S) ->* true
80.033/80.033	e(s(x:S)) -> true | o(x:S) ->* true
80.033/80.033	o(0) -> true
80.033/80.033	o(s(x:S)) -> false | o(x:S) ->* true
80.033/80.033	o(s(x:S)) -> true | e(x:S) ->* true
80.033/80.033	-> Vars:
80.033/80.033	"x", "x", "x", "x"
80.033/80.033	-> FVars:
80.033/80.033	"x2", "x3", "x4", "x5"
80.033/80.033	-> PVars:
80.033/80.033	"x": ["x2", "x3", "x4", "x5"]
80.033/80.033	
80.033/80.033	-> Rlps:
80.033/80.033	crule: e(0) -> true, id: 1, possubterms: e(0)-> [], 0-> [1]
80.033/80.033	crule: e(s(x2:S)) -> false | e(x2:S) ->* true, id: 2, possubterms: e(s(x2:S))-> [], s(x2:S)-> [1]
80.033/80.033	crule: e(s(x3:S)) -> true | o(x3:S) ->* true, id: 3, possubterms: e(s(x3:S))-> [], s(x3:S)-> [1]
80.033/80.033	crule: o(0) -> true, id: 4, possubterms: o(0)-> [], 0-> [1]
80.033/80.033	crule: o(s(x4:S)) -> false | o(x4:S) ->* true, id: 5, possubterms: o(s(x4:S))-> [], s(x4:S)-> [1]
80.033/80.033	crule: o(s(x5:S)) -> true | e(x5:S) ->* true, id: 6, possubterms: o(s(x5:S))-> [], s(x5:S)-> [1]
80.033/80.033	
80.033/80.033	-> Unifications:
80.033/80.033	R3 unifies with  R2 at  p: [], l: e(s(x3:S)), lp: e(s(x3:S)), conds: {o(x3:S) ->* true, e(x:S) ->* true}, sig: {x3:S -> x:S}, l': e(s(x:S)), r: true, r': false
80.033/80.033	R6 unifies with  R5 at  p: [], l: o(s(x5:S)), lp: o(s(x5:S)), conds: {e(x5:S) ->* true, o(x:S) ->* true}, sig: {x5:S -> x:S}, l': o(s(x:S)), r: true, r': false
80.033/80.033	
80.033/80.033	-> Critical pairs info:
80.033/80.033	<false,true> | e(x:S) ->* true, o(x:S) ->* true  =>  Not trivial, Overlay, N1
80.033/80.033	<false,true> | o(x:S) ->* true, e(x:S) ->* true  =>  Not trivial, Overlay, N2
80.033/80.033	
80.033/80.033	-> Problem conclusions:
80.033/80.033	 Left linear, Right linear, Linear
80.033/80.033	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
80.033/80.033	 CTRS Type: 1
80.033/80.033	 Deterministic, Strongly deterministic
80.033/80.033	 Oriented CTRS, Properly oriented CTRS, Not join CTRS
80.033/80.033	 Maybe right-stable CTRS, Overlay CTRS
80.033/80.033	 Maybe normal CTRS, Maybe almost normal CTRS
80.033/80.033	 Maybe terminating CTRS, Maybe joinable CCPs
80.033/80.033	 Maybe level confluent
80.033/80.033	 Maybe confluent
80.033/80.033	
80.033/80.033	Problem 1:
80.033/80.033	Clean Infeasible CCPs Processor:
80.033/80.033	Num of CPIs: 2
80.033/80.033	Timeout: 60
80.033/80.033	Timeout for each infeasibility problem: 60 s
80.033/80.033	<false,true> | e(x:S) ->* true, o(x:S) ->* true  =>  Not trivial, Overlay, Feasible conditions, N1
80.033/80.033	(PROBLEM INFEASIBILITY)
80.033/80.033	(VAR x)
80.033/80.033	(RULES
80.033/80.033	e(0) -> true
80.033/80.033	e(s(x)) -> false | e(x) ->* true
80.033/80.033	e(s(x)) -> true | o(x) ->* true
80.033/80.033	o(0) -> true
80.033/80.033	o(s(x)) -> false | o(x) ->* true
80.033/80.033	o(s(x)) -> true | e(x) ->* true)
80.033/80.033	(VAR x2)
80.033/80.033	(CONDITION e(x2) ->* true, o(x2) ->* true)
80.033/80.033	
80.033/80.033	Proof:
80.033/80.033	NO
80.033/80.033	
80.033/80.033	Problem 1:
80.033/80.033	
80.033/80.033	Infeasibility Problem:
80.033/80.033	[(VAR vNonEmpty:S x:S x2:S)
80.033/80.033	(STRATEGY CONTEXTSENSITIVE
80.033/80.033	(e 1)
80.033/80.033	(o 1)
80.033/80.033	(0)
80.033/80.033	(fSNonEmpty)
80.033/80.033	(false)
80.033/80.033	(s 1)
80.033/80.033	(true)
80.033/80.033	)
80.033/80.033	(RULES
80.033/80.033	e(0) -> true
80.033/80.033	e(s(x:S)) -> false | e(x:S) ->* true
80.033/80.033	e(s(x:S)) -> true | o(x:S) ->* true
80.033/80.033	o(0) -> true
80.033/80.033	o(s(x:S)) -> false | o(x:S) ->* true
80.033/80.033	o(s(x:S)) -> true | e(x:S) ->* true
80.033/80.033	)]
80.033/80.033	
80.033/80.033	Infeasibility Conditions:
80.033/80.033	e(x2:S) ->* true, o(x2:S) ->* true
80.033/80.033	
80.033/80.033	Problem 1:
80.033/80.033	
80.033/80.033	Obtaining a proof using Prover9:
80.033/80.033	
80.033/80.033	 -> Prover9 Output:
80.033/80.033	============================== Prover9 ===============================
80.033/80.033	Prover9 (64) version 2009-11A, November 2009.
80.033/80.033	Process 52425 was started by ubuntu on ubuntu,
80.033/80.033	Wed Jul 14 11:02:48 2021
80.033/80.033	The command was "./prover9 -f /tmp/prover952407-0.in".
80.033/80.033	============================== end of head ===========================
80.033/80.033	
80.033/80.033	============================== INPUT =================================
80.033/80.033	
80.033/80.033	% Reading from file /tmp/prover952407-0.in
80.033/80.033	
80.033/80.033	assign(max_seconds,20).
80.033/80.033	
80.033/80.033	formulas(assumptions).
80.033/80.033	->*_s0(x,x) # label(reflexivity).
80.033/80.033	->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity).
80.033/80.033	->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence).
80.033/80.033	->_s0(x1,y) -> ->_s0(o(x1),o(y)) # label(congruence).
80.033/80.033	->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence).
80.033/80.033	->_s0(e(0),true) # label(replacement).
80.033/80.033	->*_s0(e(x1),true) -> ->_s0(e(s(x1)),false) # label(replacement).
80.033/80.033	->*_s0(o(x1),true) -> ->_s0(e(s(x1)),true) # label(replacement).
80.033/80.033	->_s0(o(0),true) # label(replacement).
80.033/80.033	->*_s0(o(x1),true) -> ->_s0(o(s(x1)),false) # label(replacement).
80.033/80.033	->*_s0(e(x1),true) -> ->_s0(o(s(x1)),true) # label(replacement).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(goals).
80.033/80.033	(exists x2 (->*_s0(e(x2),true) & ->*_s0(o(x2),true))) # label(goal).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	============================== end of input ==========================
80.033/80.033	
80.033/80.033	============================== PROCESS NON-CLAUSAL FORMULAS ==========
80.033/80.033	
80.033/80.033	% Formulas that are not ordinary clauses:
80.033/80.033	1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
80.033/80.033	2 ->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence) # label(non_clause).  [assumption].
80.033/80.033	3 ->_s0(x1,y) -> ->_s0(o(x1),o(y)) # label(congruence) # label(non_clause).  [assumption].
80.033/80.033	4 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause).  [assumption].
80.033/80.033	5 ->*_s0(e(x1),true) -> ->_s0(e(s(x1)),false) # label(replacement) # label(non_clause).  [assumption].
80.033/80.033	6 ->*_s0(o(x1),true) -> ->_s0(e(s(x1)),true) # label(replacement) # label(non_clause).  [assumption].
80.033/80.033	7 ->*_s0(o(x1),true) -> ->_s0(o(s(x1)),false) # label(replacement) # label(non_clause).  [assumption].
80.033/80.033	8 ->*_s0(e(x1),true) -> ->_s0(o(s(x1)),true) # label(replacement) # label(non_clause).  [assumption].
80.033/80.033	9 (exists x2 (->*_s0(e(x2),true) & ->*_s0(o(x2),true))) # label(goal) # label(non_clause) # label(goal).  [goal].
80.033/80.033	
80.033/80.033	============================== end of process non-clausal formulas ===
80.033/80.033	
80.033/80.033	============================== PROCESS INITIAL CLAUSES ===============
80.033/80.033	
80.033/80.033	% Clauses before input processing:
80.033/80.033	
80.033/80.033	formulas(usable).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(sos).
80.033/80.033	->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	-->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	-->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(2)].
80.033/80.033	-->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence).  [clausify(3)].
80.033/80.033	-->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(4)].
80.033/80.033	->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	-->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement).  [clausify(5)].
80.033/80.033	-->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement).  [clausify(6)].
80.033/80.033	->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	-->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement).  [clausify(7)].
80.033/80.033	-->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement).  [clausify(8)].
80.033/80.033	-->*_s0(e(x),true) | -->*_s0(o(x),true) # label(goal).  [deny(9)].
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(demodulators).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	============================== PREDICATE ELIMINATION =================
80.033/80.033	
80.033/80.033	No predicates eliminated.
80.033/80.033	
80.033/80.033	============================== end predicate elimination =============
80.033/80.033	
80.033/80.033	Auto_denials:
80.033/80.033	  % copying label goal to answer in negative clause
80.033/80.033	
80.033/80.033	Term ordering decisions:
80.033/80.033	Predicate symbol precedence:  predicate_order([ ->_s0, ->*_s0 ]).
80.033/80.033	Function symbol precedence:  function_order([ true, 0, false, e, o, s ]).
80.033/80.033	After inverse_order:  (no changes).
80.033/80.033	Unfolding symbols: (none).
80.033/80.033	
80.033/80.033	Auto_inference settings:
80.033/80.033	  % set(neg_binary_resolution).  % (HNE depth_diff=-7)
80.033/80.033	  % clear(ordered_res).  % (HNE depth_diff=-7)
80.033/80.033	  % set(ur_resolution).  % (HNE depth_diff=-7)
80.033/80.033	    % set(ur_resolution) -> set(pos_ur_resolution).
80.033/80.033	    % set(ur_resolution) -> set(neg_ur_resolution).
80.033/80.033	
80.033/80.033	Auto_process settings:
80.033/80.033	  % set(unit_deletion).  % (Horn set with negative nonunits)
80.033/80.033	
80.033/80.033	kept:      10 ->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	kept:      11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	kept:      12 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(2)].
80.033/80.033	kept:      13 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence).  [clausify(3)].
80.033/80.033	kept:      14 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(4)].
80.033/80.033	kept:      15 ->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	kept:      16 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement).  [clausify(5)].
80.033/80.033	kept:      17 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement).  [clausify(6)].
80.033/80.033	kept:      18 ->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	kept:      19 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement).  [clausify(7)].
80.033/80.033	kept:      20 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement).  [clausify(8)].
80.033/80.033	kept:      21 -->*_s0(e(x),true) | -->*_s0(o(x),true) # label(goal) # answer(goal).  [deny(9)].
80.033/80.033	
80.033/80.033	============================== end of process initial clauses ========
80.033/80.033	
80.033/80.033	============================== CLAUSES FOR SEARCH ====================
80.033/80.033	
80.033/80.033	% Clauses after input processing:
80.033/80.033	
80.033/80.033	formulas(usable).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(sos).
80.033/80.033	10 ->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	12 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(2)].
80.033/80.033	13 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence).  [clausify(3)].
80.033/80.033	14 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(4)].
80.033/80.033	15 ->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	16 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement).  [clausify(5)].
80.033/80.033	17 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement).  [clausify(6)].
80.033/80.033	18 ->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	19 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement).  [clausify(7)].
80.033/80.033	20 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement).  [clausify(8)].
80.033/80.033	21 -->*_s0(e(x),true) | -->*_s0(o(x),true) # label(goal) # answer(goal).  [deny(9)].
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(demodulators).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	============================== end of clauses for search =============
80.033/80.033	
80.033/80.033	============================== SEARCH ================================
80.033/80.033	
80.033/80.033	% Starting search at 0.00 seconds.
80.033/80.033	
80.033/80.033	given #1 (I,wt=3): 10 ->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	
80.033/80.033	given #2 (I,wt=9): 11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	
80.033/80.033	given #3 (I,wt=8): 12 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(2)].
80.033/80.033	
80.033/80.033	given #4 (I,wt=8): 13 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence).  [clausify(3)].
80.033/80.033	
80.033/80.033	given #5 (I,wt=8): 14 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(4)].
80.033/80.033	
80.033/80.033	given #6 (I,wt=4): 15 ->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	
80.033/80.033	given #7 (I,wt=9): 16 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement).  [clausify(5)].
80.033/80.033	
80.033/80.033	given #8 (I,wt=9): 17 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement).  [clausify(6)].
80.033/80.033	
80.033/80.033	given #9 (I,wt=4): 18 ->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	
80.033/80.033	given #10 (I,wt=9): 19 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement).  [clausify(7)].
80.033/80.033	
80.033/80.033	given #11 (I,wt=9): 20 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement).  [clausify(8)].
80.033/80.033	
80.033/80.033	given #12 (I,wt=8): 21 -->*_s0(e(x),true) | -->*_s0(o(x),true) # label(goal) # answer(goal).  [deny(9)].
80.033/80.033	
80.033/80.033	given #13 (A,wt=6): 22 ->_s0(s(e(0)),s(true)).  [ur(14,a,15,a)].
80.033/80.033	
80.033/80.033	given #14 (F,wt=11): 30 -->*_s0(o(x),true) | -->_s0(e(x),y) | -->*_s0(y,true) # answer(goal).  [resolve(21,a,11,c)].
80.033/80.033	
80.033/80.033	============================== PROOF =================================
80.033/80.033	
80.033/80.033	% Proof 1 at 0.01 (+ 0.00) seconds: goal.
80.033/80.033	% Length of proof is 10.
80.033/80.033	% Level of proof is 3.
80.033/80.033	% Maximum clause weight is 11.000.
80.033/80.033	% Given clauses 14.
80.033/80.033	
80.033/80.033	1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
80.033/80.033	9 (exists x2 (->*_s0(e(x2),true) & ->*_s0(o(x2),true))) # label(goal) # label(non_clause) # label(goal).  [goal].
80.033/80.033	10 ->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	15 ->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	18 ->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	21 -->*_s0(e(x),true) | -->*_s0(o(x),true) # label(goal) # answer(goal).  [deny(9)].
80.033/80.033	29 ->*_s0(o(0),true).  [ur(11,a,18,a,b,10,a)].
80.033/80.033	30 -->*_s0(o(x),true) | -->_s0(e(x),y) | -->*_s0(y,true) # answer(goal).  [resolve(21,a,11,c)].
80.033/80.033	39 $F # answer(goal).  [resolve(30,b,15,a),unit_del(a,29),unit_del(b,10)].
80.033/80.033	
80.033/80.033	============================== end of proof ==========================
80.033/80.033	
80.033/80.033	============================== STATISTICS ============================
80.033/80.033	
80.033/80.033	Given=14. Generated=30. Kept=29. proofs=1.
80.033/80.033	Usable=14. Sos=12. Demods=0. Limbo=3, Disabled=12. Hints=0.
80.033/80.033	Kept_by_rule=0, Deleted_by_rule=0.
80.033/80.033	Forward_subsumed=0. Back_subsumed=0.
80.033/80.033	Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
80.033/80.033	New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
80.033/80.033	Demod_attempts=0. Demod_rewrites=0.
80.033/80.033	Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
80.033/80.033	Nonunit_fsub_feature_tests=7. Nonunit_bsub_feature_tests=14.
80.033/80.033	Megabytes=0.09.
80.033/80.033	User_CPU=0.01, System_CPU=0.00, Wall_clock=0.
80.033/80.033	
80.033/80.033	============================== end of statistics =====================
80.033/80.033	
80.033/80.033	============================== end of search =========================
80.033/80.033	
80.033/80.033	THEOREM PROVED
80.033/80.033	
80.033/80.033	Exiting with 1 proof.
80.033/80.033	
80.033/80.033	Process 52425 exit (max_proofs) Wed Jul 14 11:02:48 2021
80.033/80.033	
80.033/80.033	
80.033/80.033	The problem is feasible.
80.033/80.033	
80.033/80.033	
80.033/80.033	
80.033/80.033	
80.033/80.033	<false,true> | o(x:S) ->* true, e(x:S) ->* true  =>  Not trivial, Overlay, Feasible conditions, N2
80.033/80.033	(PROBLEM INFEASIBILITY)
80.033/80.033	(VAR x)
80.033/80.033	(RULES
80.033/80.033	e(0) -> true
80.033/80.033	e(s(x)) -> false | e(x) ->* true
80.033/80.033	e(s(x)) -> true | o(x) ->* true
80.033/80.033	o(0) -> true
80.033/80.033	o(s(x)) -> false | o(x) ->* true
80.033/80.033	o(s(x)) -> true | e(x) ->* true)
80.033/80.033	(VAR x2)
80.033/80.033	(CONDITION o(x2) ->* true, e(x2) ->* true)
80.033/80.033	
80.033/80.033	Proof:
80.033/80.033	NO
80.033/80.033	
80.033/80.033	Problem 1:
80.033/80.033	
80.033/80.033	Infeasibility Problem:
80.033/80.033	[(VAR vNonEmpty:S x:S x2:S)
80.033/80.033	(STRATEGY CONTEXTSENSITIVE
80.033/80.033	(e 1)
80.033/80.033	(o 1)
80.033/80.033	(0)
80.033/80.033	(fSNonEmpty)
80.033/80.033	(false)
80.033/80.033	(s 1)
80.033/80.033	(true)
80.033/80.033	)
80.033/80.033	(RULES
80.033/80.033	e(0) -> true
80.033/80.033	e(s(x:S)) -> false | e(x:S) ->* true
80.033/80.033	e(s(x:S)) -> true | o(x:S) ->* true
80.033/80.033	o(0) -> true
80.033/80.033	o(s(x:S)) -> false | o(x:S) ->* true
80.033/80.033	o(s(x:S)) -> true | e(x:S) ->* true
80.033/80.033	)]
80.033/80.033	
80.033/80.033	Infeasibility Conditions:
80.033/80.033	o(x2:S) ->* true, e(x2:S) ->* true
80.033/80.033	
80.033/80.033	Problem 1:
80.033/80.033	
80.033/80.033	Obtaining a proof using Prover9:
80.033/80.033	
80.033/80.033	 -> Prover9 Output:
80.033/80.033	============================== Prover9 ===============================
80.033/80.033	Prover9 (64) version 2009-11A, November 2009.
80.033/80.033	Process 52621 was started by ubuntu on ubuntu,
80.033/80.033	Wed Jul 14 11:04:03 2021
80.033/80.033	The command was "./prover9 -f /tmp/prover952612-0.in".
80.033/80.033	============================== end of head ===========================
80.033/80.033	
80.033/80.033	============================== INPUT =================================
80.033/80.033	
80.033/80.033	% Reading from file /tmp/prover952612-0.in
80.033/80.033	
80.033/80.033	assign(max_seconds,20).
80.033/80.033	
80.033/80.033	formulas(assumptions).
80.033/80.033	->*_s0(x,x) # label(reflexivity).
80.033/80.033	->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity).
80.033/80.033	->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence).
80.033/80.033	->_s0(x1,y) -> ->_s0(o(x1),o(y)) # label(congruence).
80.033/80.033	->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence).
80.033/80.033	->_s0(e(0),true) # label(replacement).
80.033/80.033	->*_s0(e(x1),true) -> ->_s0(e(s(x1)),false) # label(replacement).
80.033/80.033	->*_s0(o(x1),true) -> ->_s0(e(s(x1)),true) # label(replacement).
80.033/80.033	->_s0(o(0),true) # label(replacement).
80.033/80.033	->*_s0(o(x1),true) -> ->_s0(o(s(x1)),false) # label(replacement).
80.033/80.033	->*_s0(e(x1),true) -> ->_s0(o(s(x1)),true) # label(replacement).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(goals).
80.033/80.033	(exists x2 (->*_s0(o(x2),true) & ->*_s0(e(x2),true))) # label(goal).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	============================== end of input ==========================
80.033/80.033	
80.033/80.033	============================== PROCESS NON-CLAUSAL FORMULAS ==========
80.033/80.033	
80.033/80.033	% Formulas that are not ordinary clauses:
80.033/80.033	1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
80.033/80.033	2 ->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence) # label(non_clause).  [assumption].
80.033/80.033	3 ->_s0(x1,y) -> ->_s0(o(x1),o(y)) # label(congruence) # label(non_clause).  [assumption].
80.033/80.033	4 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause).  [assumption].
80.033/80.033	5 ->*_s0(e(x1),true) -> ->_s0(e(s(x1)),false) # label(replacement) # label(non_clause).  [assumption].
80.033/80.033	6 ->*_s0(o(x1),true) -> ->_s0(e(s(x1)),true) # label(replacement) # label(non_clause).  [assumption].
80.033/80.033	7 ->*_s0(o(x1),true) -> ->_s0(o(s(x1)),false) # label(replacement) # label(non_clause).  [assumption].
80.033/80.033	8 ->*_s0(e(x1),true) -> ->_s0(o(s(x1)),true) # label(replacement) # label(non_clause).  [assumption].
80.033/80.033	9 (exists x2 (->*_s0(o(x2),true) & ->*_s0(e(x2),true))) # label(goal) # label(non_clause) # label(goal).  [goal].
80.033/80.033	
80.033/80.033	============================== end of process non-clausal formulas ===
80.033/80.033	
80.033/80.033	============================== PROCESS INITIAL CLAUSES ===============
80.033/80.033	
80.033/80.033	% Clauses before input processing:
80.033/80.033	
80.033/80.033	formulas(usable).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(sos).
80.033/80.033	->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	-->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	-->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(2)].
80.033/80.033	-->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence).  [clausify(3)].
80.033/80.033	-->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(4)].
80.033/80.033	->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	-->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement).  [clausify(5)].
80.033/80.033	-->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement).  [clausify(6)].
80.033/80.033	->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	-->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement).  [clausify(7)].
80.033/80.033	-->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement).  [clausify(8)].
80.033/80.033	-->*_s0(o(x),true) | -->*_s0(e(x),true) # label(goal).  [deny(9)].
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(demodulators).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	============================== PREDICATE ELIMINATION =================
80.033/80.033	
80.033/80.033	No predicates eliminated.
80.033/80.033	
80.033/80.033	============================== end predicate elimination =============
80.033/80.033	
80.033/80.033	Auto_denials:
80.033/80.033	  % copying label goal to answer in negative clause
80.033/80.033	
80.033/80.033	Term ordering decisions:
80.033/80.033	Predicate symbol precedence:  predicate_order([ ->_s0, ->*_s0 ]).
80.033/80.033	Function symbol precedence:  function_order([ true, 0, false, e, o, s ]).
80.033/80.033	After inverse_order:  (no changes).
80.033/80.033	Unfolding symbols: (none).
80.033/80.033	
80.033/80.033	Auto_inference settings:
80.033/80.033	  % set(neg_binary_resolution).  % (HNE depth_diff=-7)
80.033/80.033	  % clear(ordered_res).  % (HNE depth_diff=-7)
80.033/80.033	  % set(ur_resolution).  % (HNE depth_diff=-7)
80.033/80.033	    % set(ur_resolution) -> set(pos_ur_resolution).
80.033/80.033	    % set(ur_resolution) -> set(neg_ur_resolution).
80.033/80.033	
80.033/80.033	Auto_process settings:
80.033/80.033	  % set(unit_deletion).  % (Horn set with negative nonunits)
80.033/80.033	
80.033/80.033	kept:      10 ->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	kept:      11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	kept:      12 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(2)].
80.033/80.033	kept:      13 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence).  [clausify(3)].
80.033/80.033	kept:      14 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(4)].
80.033/80.033	kept:      15 ->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	kept:      16 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement).  [clausify(5)].
80.033/80.033	kept:      17 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement).  [clausify(6)].
80.033/80.033	kept:      18 ->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	kept:      19 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement).  [clausify(7)].
80.033/80.033	kept:      20 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement).  [clausify(8)].
80.033/80.033	kept:      21 -->*_s0(o(x),true) | -->*_s0(e(x),true) # label(goal) # answer(goal).  [deny(9)].
80.033/80.033	
80.033/80.033	============================== end of process initial clauses ========
80.033/80.033	
80.033/80.033	============================== CLAUSES FOR SEARCH ====================
80.033/80.033	
80.033/80.033	% Clauses after input processing:
80.033/80.033	
80.033/80.033	formulas(usable).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(sos).
80.033/80.033	10 ->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	12 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(2)].
80.033/80.033	13 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence).  [clausify(3)].
80.033/80.033	14 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(4)].
80.033/80.033	15 ->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	16 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement).  [clausify(5)].
80.033/80.033	17 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement).  [clausify(6)].
80.033/80.033	18 ->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	19 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement).  [clausify(7)].
80.033/80.033	20 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement).  [clausify(8)].
80.033/80.033	21 -->*_s0(o(x),true) | -->*_s0(e(x),true) # label(goal) # answer(goal).  [deny(9)].
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(demodulators).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	============================== end of clauses for search =============
80.033/80.033	
80.033/80.033	============================== SEARCH ================================
80.033/80.033	
80.033/80.033	% Starting search at 0.00 seconds.
80.033/80.033	
80.033/80.033	given #1 (I,wt=3): 10 ->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	
80.033/80.033	given #2 (I,wt=9): 11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	
80.033/80.033	given #3 (I,wt=8): 12 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence).  [clausify(2)].
80.033/80.033	
80.033/80.033	given #4 (I,wt=8): 13 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence).  [clausify(3)].
80.033/80.033	
80.033/80.033	given #5 (I,wt=8): 14 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(4)].
80.033/80.033	
80.033/80.033	given #6 (I,wt=4): 15 ->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	
80.033/80.033	given #7 (I,wt=9): 16 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement).  [clausify(5)].
80.033/80.033	
80.033/80.033	given #8 (I,wt=9): 17 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement).  [clausify(6)].
80.033/80.033	
80.033/80.033	given #9 (I,wt=4): 18 ->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	
80.033/80.033	given #10 (I,wt=9): 19 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement).  [clausify(7)].
80.033/80.033	
80.033/80.033	given #11 (I,wt=9): 20 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement).  [clausify(8)].
80.033/80.033	
80.033/80.033	given #12 (I,wt=8): 21 -->*_s0(o(x),true) | -->*_s0(e(x),true) # label(goal) # answer(goal).  [deny(9)].
80.033/80.033	
80.033/80.033	given #13 (A,wt=6): 22 ->_s0(s(e(0)),s(true)).  [ur(14,a,15,a)].
80.033/80.033	
80.033/80.033	given #14 (F,wt=11): 30 -->*_s0(e(x),true) | -->_s0(o(x),y) | -->*_s0(y,true) # answer(goal).  [resolve(21,a,11,c)].
80.033/80.033	
80.033/80.033	============================== PROOF =================================
80.033/80.033	
80.033/80.033	% Proof 1 at 0.00 (+ 0.00) seconds: goal.
80.033/80.033	% Length of proof is 10.
80.033/80.033	% Level of proof is 3.
80.033/80.033	% Maximum clause weight is 11.000.
80.033/80.033	% Given clauses 14.
80.033/80.033	
80.033/80.033	1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
80.033/80.033	9 (exists x2 (->*_s0(o(x2),true) & ->*_s0(e(x2),true))) # label(goal) # label(non_clause) # label(goal).  [goal].
80.033/80.033	10 ->*_s0(x,x) # label(reflexivity).  [assumption].
80.033/80.033	11 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
80.033/80.033	15 ->_s0(e(0),true) # label(replacement).  [assumption].
80.033/80.033	18 ->_s0(o(0),true) # label(replacement).  [assumption].
80.033/80.033	21 -->*_s0(o(x),true) | -->*_s0(e(x),true) # label(goal) # answer(goal).  [deny(9)].
80.033/80.033	25 ->*_s0(e(0),true).  [ur(11,a,15,a,b,10,a)].
80.033/80.033	30 -->*_s0(e(x),true) | -->_s0(o(x),y) | -->*_s0(y,true) # answer(goal).  [resolve(21,a,11,c)].
80.033/80.033	39 $F # answer(goal).  [resolve(30,b,18,a),unit_del(a,25),unit_del(b,10)].
80.033/80.033	
80.033/80.033	============================== end of proof ==========================
80.033/80.033	
80.033/80.033	============================== STATISTICS ============================
80.033/80.033	
80.033/80.033	Given=14. Generated=30. Kept=29. proofs=1.
80.033/80.033	Usable=14. Sos=12. Demods=0. Limbo=3, Disabled=12. Hints=0.
80.033/80.033	Kept_by_rule=0, Deleted_by_rule=0.
80.033/80.033	Forward_subsumed=0. Back_subsumed=0.
80.033/80.033	Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
80.033/80.033	New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
80.033/80.033	Demod_attempts=0. Demod_rewrites=0.
80.033/80.033	Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
80.033/80.033	Nonunit_fsub_feature_tests=7. Nonunit_bsub_feature_tests=14.
80.033/80.033	Megabytes=0.09.
80.033/80.033	User_CPU=0.00, System_CPU=0.00, Wall_clock=0.
80.033/80.033	
80.033/80.033	============================== end of statistics =====================
80.033/80.033	
80.033/80.033	============================== end of search =========================
80.033/80.033	
80.033/80.033	THEOREM PROVED
80.033/80.033	
80.033/80.033	Exiting with 1 proof.
80.033/80.033	
80.033/80.033	Process 52621 exit (max_proofs) Wed Jul 14 11:04:03 2021
80.033/80.033	
80.033/80.033	
80.033/80.033	The problem is feasible.
80.033/80.033	
80.033/80.033	
80.033/80.033	
80.033/80.033	
80.033/80.033	-> Problem conclusions:
80.033/80.033	 Left linear, Right linear, Linear
80.033/80.033	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
80.033/80.033	 CTRS Type: 1
80.033/80.033	 Deterministic, Strongly deterministic
80.033/80.033	 Oriented CTRS, Properly oriented CTRS, Not join CTRS
80.033/80.033	 Maybe right-stable CTRS, Overlay CTRS
80.033/80.033	 Maybe normal CTRS, Maybe almost normal CTRS
80.033/80.033	 Maybe terminating CTRS, Maybe joinable CCPs
80.033/80.033	 Maybe level confluent
80.033/80.033	 Maybe confluent
80.033/80.033	
80.033/80.033	Resulting CCPs:
80.033/80.033	<false,true> | e(x:S) ->* true, o(x:S) ->* true  =>  Not trivial, Overlay, Feasible conditions, N1
80.033/80.033	<false,true> | o(x:S) ->* true, e(x:S) ->* true  =>  Not trivial, Overlay, Feasible conditions, N2
80.033/80.033	
80.033/80.033	Problem 1:
80.033/80.033	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
80.033/80.033	Confluence Problem:
80.033/80.033	(VAR x:S)
80.033/80.033	(STRATEGY CONTEXTSENSITIVE
80.033/80.033	(e 1)
80.033/80.033	(o 1)
80.033/80.033	(0)
80.033/80.033	(fSNonEmpty)
80.033/80.033	(false)
80.033/80.033	(s 1)
80.033/80.033	(true)
80.033/80.033	)
80.033/80.033	(RULES
80.033/80.033	e(0) -> true
80.033/80.033	e(s(x:S)) -> false | e(x:S) ->* true
80.033/80.033	e(s(x:S)) -> true | o(x:S) ->* true
80.033/80.033	o(0) -> true
80.033/80.033	o(s(x:S)) -> false | o(x:S) ->* true
80.033/80.033	o(s(x:S)) -> true | e(x:S) ->* true
80.033/80.033	)
80.033/80.033	Critical Pairs:
80.033/80.033	<false,true> | e(x:S) ->* true, o(x:S) ->* true  =>  Not trivial, Overlay, Feasible conditions, N1
80.033/80.033	<false,true> | o(x:S) ->* true, e(x:S) ->* true  =>  Not trivial, Overlay, Feasible conditions, N2
80.033/80.033	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
80.033/80.033	
80.033/80.033	Conditional Critical Pairs Distributor Processor
80.033/80.033	
80.033/80.033	Problem 1:
80.033/80.033	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
80.033/80.033	Confluence Problem:
80.033/80.033	(VAR x:S)
80.033/80.033	(STRATEGY CONTEXTSENSITIVE
80.033/80.033	(e 1)
80.033/80.033	(o 1)
80.033/80.033	(0)
80.033/80.033	(fSNonEmpty)
80.033/80.033	(false)
80.033/80.033	(s 1)
80.033/80.033	(true)
80.033/80.033	)
80.033/80.033	(RULES
80.033/80.033	e(0) -> true
80.033/80.033	e(s(x:S)) -> false | e(x:S) ->* true
80.033/80.033	e(s(x:S)) -> true | o(x:S) ->* true
80.033/80.033	o(0) -> true
80.033/80.033	o(s(x:S)) -> false | o(x:S) ->* true
80.033/80.033	o(s(x:S)) -> true | e(x:S) ->* true
80.033/80.033	)
80.033/80.033	Critical Pairs:
80.033/80.033	<false,true> | e(x:S) ->* true, o(x:S) ->* true  =>  Not trivial, Overlay, Feasible conditions, N1
80.033/80.033	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
80.033/80.033	
80.033/80.033	InfChecker Different Ground and Normal CCP Terms Processor:
80.033/80.033	Proof:
80.033/80.033	YES
80.033/80.033	
80.033/80.033	Problem 1:
80.033/80.033	
80.033/80.033	Infeasibility Problem:
80.033/80.033	[(VAR vNonEmpty:S x:S y:S)
80.033/80.033	(STRATEGY CONTEXTSENSITIVE
80.033/80.033	(e 1)
80.033/80.033	(o 1)
80.033/80.033	(0)
80.033/80.033	(fSNonEmpty)
80.033/80.033	(false)
80.033/80.033	(s 1)
80.033/80.033	(true)
80.033/80.033	)
80.033/80.033	(RULES
80.033/80.033	e(0) -> true
80.033/80.033	e(s(x:S)) -> false | e(x:S) ->* true
80.033/80.033	e(s(x:S)) -> true | o(x:S) ->* true
80.033/80.033	o(0) -> true
80.033/80.033	o(s(x:S)) -> false | o(x:S) ->* true
80.033/80.033	o(s(x:S)) -> true | e(x:S) ->* true
80.033/80.033	)]
80.033/80.033	
80.033/80.033	Infeasibility Conditions:
80.033/80.033	false -> y:S
80.033/80.033	
80.033/80.033	Problem 1:
80.033/80.033	
80.033/80.033	Obtaining a model using Mace4:
80.033/80.033	
80.033/80.033	 -> Usable Rules:
80.033/80.033	Empty
80.033/80.033	
80.033/80.033	 -> Mace4 Output:
80.033/80.033	============================== Mace4 =================================
80.033/80.033	Mace4 (64) version 2009-11A, November 2009.
80.033/80.033	Process 52563 was started by ubuntu on ubuntu,
80.033/80.033	Wed Jul 14 11:03:29 2021
80.033/80.033	The command was "./mace4 -c -f /tmp/mace452489-2.in".
80.033/80.033	============================== end of head ===========================
80.033/80.033	
80.033/80.033	============================== INPUT =================================
80.033/80.033	
80.033/80.033	% Reading from file /tmp/mace452489-2.in
80.033/80.033	
80.033/80.033	assign(max_seconds,6).
80.033/80.033	
80.033/80.033	formulas(assumptions).
80.033/80.033	->(x1,y) -> ->(e(x1),e(y)) # label(congruence).
80.033/80.033	->(x1,y) -> ->(o(x1),o(y)) # label(congruence).
80.033/80.033	->(x1,y) -> ->(s(x1),s(y)) # label(congruence).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(goals).
80.033/80.033	(exists x2 ->(false,x2)) # label(goal).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	============================== end of input ==========================
80.033/80.033	
80.033/80.033	============================== PROCESS NON-CLAUSAL FORMULAS ==========
80.033/80.033	
80.033/80.033	% Formulas that are not ordinary clauses:
80.033/80.033	1 ->(x1,y) -> ->(e(x1),e(y)) # label(congruence) # label(non_clause).  [assumption].
80.033/80.033	2 ->(x1,y) -> ->(o(x1),o(y)) # label(congruence) # label(non_clause).  [assumption].
80.033/80.033	3 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause).  [assumption].
80.033/80.033	4 (exists x2 ->(false,x2)) # label(goal) # label(non_clause) # label(goal).  [goal].
80.033/80.033	
80.033/80.033	============================== end of process non-clausal formulas ===
80.033/80.033	
80.033/80.033	============================== CLAUSES FOR SEARCH ====================
80.033/80.033	
80.033/80.033	formulas(mace4_clauses).
80.033/80.033	-->(x,y) | ->(e(x),e(y)) # label(congruence).
80.033/80.033	-->(x,y) | ->(o(x),o(y)) # label(congruence).
80.033/80.033	-->(x,y) | ->(s(x),s(y)) # label(congruence).
80.033/80.033	-->(false,x) # label(goal).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	============================== end of clauses for search =============
80.033/80.033	
80.033/80.033	% There are no natural numbers in the input.
80.033/80.033	
80.033/80.033	============================== DOMAIN SIZE 2 =========================
80.033/80.033	
80.033/80.033	============================== MODEL =================================
80.033/80.033	
80.033/80.033	interpretation( 2, [number=1, seconds=0], [
80.033/80.033	
80.033/80.033	        function(false, [ 0 ]),
80.033/80.033	
80.033/80.033	        function(e(_), [ 0, 0 ]),
80.033/80.033	
80.033/80.033	        function(o(_), [ 0, 0 ]),
80.033/80.033	
80.033/80.033	        function(s(_), [ 0, 0 ]),
80.033/80.033	
80.033/80.033	        relation(->(_,_), [
80.033/80.033				   0, 0,
80.033/80.033				   0, 0 ])
80.033/80.033	]).
80.033/80.033	
80.033/80.033	============================== end of model ==========================
80.033/80.033	
80.033/80.033	============================== STATISTICS ============================
80.033/80.033	
80.033/80.033	For domain size 2.
80.033/80.033	
80.033/80.033	Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
80.033/80.033	Ground clauses: seen=14, kept=14.
80.033/80.033	Selections=7, assignments=7, propagations=4, current_models=1.
80.033/80.033	Rewrite_terms=26, rewrite_bools=16, indexes=2.
80.033/80.033	Rules_from_neg_clauses=0, cross_offs=0.
80.033/80.033	
80.033/80.033	============================== end of statistics =====================
80.033/80.033	
80.033/80.033	User_CPU=0.00, System_CPU=0.00, Wall_clock=0.
80.033/80.033	
80.033/80.033	Exiting with 1 model.
80.033/80.033	
80.033/80.033	Process 52563 exit (max_models) Wed Jul 14 11:03:29 2021
80.033/80.033	The process finished Wed Jul 14 11:03:29 2021
80.033/80.033	
80.033/80.033	
80.033/80.033	Mace4 cooked interpretation:
80.033/80.033	
80.033/80.033	
80.033/80.033	
80.033/80.033	The problem is infeasible.
80.033/80.033	YES
80.033/80.033	
80.033/80.033	Problem 1:
80.033/80.033	
80.033/80.033	Infeasibility Problem:
80.033/80.033	[(VAR vNonEmpty:S x:S)
80.033/80.033	(STRATEGY CONTEXTSENSITIVE
80.033/80.033	(e 1)
80.033/80.033	(o 1)
80.033/80.033	(0)
80.033/80.033	(fSNonEmpty)
80.033/80.033	(false)
80.033/80.033	(s 1)
80.033/80.033	(true)
80.033/80.033	)
80.033/80.033	(RULES
80.033/80.033	e(0) -> true
80.033/80.033	e(s(x:S)) -> false | e(x:S) ->* true
80.033/80.033	e(s(x:S)) -> true | o(x:S) ->* true
80.033/80.033	o(0) -> true
80.033/80.033	o(s(x:S)) -> false | o(x:S) ->* true
80.033/80.033	o(s(x:S)) -> true | e(x:S) ->* true
80.033/80.033	)]
80.033/80.033	
80.033/80.033	Infeasibility Conditions:
80.033/80.033	true -> x:S
80.033/80.033	
80.033/80.033	Problem 1:
80.033/80.033	
80.033/80.033	Obtaining a model using Mace4:
80.033/80.033	
80.033/80.033	 -> Usable Rules:
80.033/80.033	Empty
80.033/80.033	
80.033/80.033	 -> Mace4 Output:
80.033/80.033	============================== Mace4 =================================
80.033/80.033	Mace4 (64) version 2009-11A, November 2009.
80.033/80.033	Process 52599 was started by ubuntu on ubuntu,
80.033/80.033	Wed Jul 14 11:03:47 2021
80.033/80.033	The command was "./mace4 -c -f /tmp/mace452586-2.in".
80.033/80.033	============================== end of head ===========================
80.033/80.033	
80.033/80.033	============================== INPUT =================================
80.033/80.033	
80.033/80.033	% Reading from file /tmp/mace452586-2.in
80.033/80.033	
80.033/80.033	assign(max_seconds,6).
80.033/80.033	
80.033/80.033	formulas(assumptions).
80.033/80.033	->(x1,y) -> ->(e(x1),e(y)) # label(congruence).
80.033/80.033	->(x1,y) -> ->(o(x1),o(y)) # label(congruence).
80.033/80.033	->(x1,y) -> ->(s(x1),s(y)) # label(congruence).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	formulas(goals).
80.033/80.033	(exists x1 ->(true,x1)) # label(goal).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	============================== end of input ==========================
80.033/80.033	
80.033/80.033	============================== PROCESS NON-CLAUSAL FORMULAS ==========
80.033/80.033	
80.033/80.033	% Formulas that are not ordinary clauses:
80.033/80.033	1 ->(x1,y) -> ->(e(x1),e(y)) # label(congruence) # label(non_clause).  [assumption].
80.033/80.033	2 ->(x1,y) -> ->(o(x1),o(y)) # label(congruence) # label(non_clause).  [assumption].
80.033/80.033	3 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause).  [assumption].
80.033/80.033	4 (exists x1 ->(true,x1)) # label(goal) # label(non_clause) # label(goal).  [goal].
80.033/80.033	
80.033/80.033	============================== end of process non-clausal formulas ===
80.033/80.033	
80.033/80.033	============================== CLAUSES FOR SEARCH ====================
80.033/80.033	
80.033/80.033	formulas(mace4_clauses).
80.033/80.033	-->(x,y) | ->(e(x),e(y)) # label(congruence).
80.033/80.033	-->(x,y) | ->(o(x),o(y)) # label(congruence).
80.033/80.033	-->(x,y) | ->(s(x),s(y)) # label(congruence).
80.033/80.033	-->(true,x) # label(goal).
80.033/80.033	end_of_list.
80.033/80.033	
80.033/80.033	============================== end of clauses for search =============
80.033/80.033	
80.033/80.033	% There are no natural numbers in the input.
80.033/80.033	
80.033/80.033	============================== DOMAIN SIZE 2 =========================
80.033/80.033	
80.033/80.033	============================== MODEL =================================
80.033/80.033	
80.033/80.033	interpretation( 2, [number=1, seconds=0], [
80.033/80.033	
80.033/80.033	        function(true, [ 0 ]),
80.033/80.033	
80.033/80.033	        function(e(_), [ 0, 0 ]),
80.033/80.033	
80.033/80.033	        function(o(_), [ 0, 0 ]),
80.033/80.033	
80.033/80.033	        function(s(_), [ 0, 0 ]),
80.033/80.033	
80.033/80.033	        relation(->(_,_), [
80.033/80.033				   0, 0,
80.033/80.033				   0, 0 ])
80.033/80.033	]).
80.033/80.033	
80.033/80.033	============================== end of model ==========================
80.033/80.033	
80.033/80.033	============================== STATISTICS ============================
80.033/80.033	
80.033/80.033	For domain size 2.
80.033/80.033	
80.033/80.033	Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
80.033/80.033	Ground clauses: seen=14, kept=14.
80.033/80.033	Selections=7, assignments=7, propagations=4, current_models=1.
80.033/80.033	Rewrite_terms=26, rewrite_bools=16, indexes=2.
80.033/80.033	Rules_from_neg_clauses=0, cross_offs=0.
80.033/80.033	
80.033/80.033	============================== end of statistics =====================
80.033/80.033	
80.033/80.033	User_CPU=0.00, System_CPU=0.00, Wall_clock=0.
80.033/80.033	
80.033/80.033	Exiting with 1 model.
80.033/80.033	
80.033/80.033	Process 52599 exit (max_models) Wed Jul 14 11:03:47 2021
80.033/80.033	The process finished Wed Jul 14 11:03:47 2021
80.033/80.033	
80.033/80.033	
80.033/80.033	Mace4 cooked interpretation:
80.033/80.033	
80.033/80.033	
80.033/80.033	
80.033/80.033	The problem is infeasible.
80.033/80.033	
80.033/80.033	
80.033/80.033	The problem is not joinable.
80.033/80.033	85.72user 4.19system 1:20.33elapsed 111%CPU (0avgtext+0avgdata 1960636maxresident)k
80.033/80.033	8inputs+0outputs (0major+1442314minor)pagefaults 0swaps