21.045/21.045	NO
21.045/21.045	
21.045/21.045	Problem 1:
21.045/21.045	
21.045/21.045	
21.045/21.045	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.045/21.045	Confluence Problem:
21.045/21.045	(VAR vNonEmpty x y z)
21.045/21.045	(REPLACEMENT-MAP
21.045/21.045	(gcd 1, 2)
21.045/21.045	(iadd 1)
21.045/21.045	(0)
21.045/21.045	(add 1, 2)
21.045/21.045	(fSNonEmpty)
21.045/21.045	(s 1)
21.045/21.045	(tp2 1, 2)
21.045/21.045	)
21.045/21.045	(RULES
21.045/21.045	gcd(0,x) -> x
21.045/21.045	gcd(x,0) -> x
21.045/21.045	gcd(y,z) -> gcd(x,y) | iadd(z) ->* tp2(x,y)
21.045/21.045	gcd(z,y) -> gcd(x,y) | iadd(z) ->* tp2(x,y)
21.045/21.045	iadd(add(x,y)) -> tp2(x,y)
21.045/21.045	iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y)
21.045/21.045	iadd(y) -> tp2(0,y)
21.045/21.045	)
21.045/21.045	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.045/21.045	
21.045/21.045	
21.045/21.045	Problem 1:
21.045/21.045	
21.045/21.045	Inlining of Conditions Processor [STERN17]:
21.045/21.045	
21.045/21.045	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.045/21.045	Confluence Problem:
21.045/21.045	(VAR vNonEmpty x y z)
21.045/21.045	(REPLACEMENT-MAP
21.045/21.045	(gcd 1, 2)
21.045/21.045	(iadd 1)
21.045/21.045	(0)
21.045/21.045	(add 1, 2)
21.045/21.045	(fSNonEmpty)
21.045/21.045	(s 1)
21.045/21.045	(tp2 1, 2)
21.045/21.045	)
21.045/21.045	(RULES
21.045/21.045	gcd(0,x) -> x
21.045/21.045	gcd(x,0) -> x
21.045/21.045	gcd(y,z) -> gcd(x,y) | iadd(z) ->* tp2(x,y)
21.045/21.045	gcd(z,y) -> gcd(x,y) | iadd(z) ->* tp2(x,y)
21.045/21.045	iadd(add(x,y)) -> tp2(x,y)
21.045/21.045	iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y)
21.045/21.045	iadd(y) -> tp2(0,y)
21.045/21.045	)
21.045/21.045	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.045/21.045	
21.045/21.045	
21.045/21.045	Problem 1:
21.045/21.045	
21.045/21.045	Clean CTRS Processor:
21.045/21.045	
21.045/21.045	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.045/21.045	Confluence Problem:
21.045/21.045	(VAR x y z)
21.045/21.045	(REPLACEMENT-MAP
21.045/21.045	(gcd 1, 2)
21.045/21.045	(iadd 1)
21.045/21.045	(0)
21.045/21.045	(add 1, 2)
21.045/21.045	(fSNonEmpty)
21.045/21.045	(s 1)
21.045/21.045	(tp2 1, 2)
21.045/21.045	)
21.045/21.045	(RULES
21.045/21.045	gcd(0,x) -> x
21.045/21.045	gcd(x,0) -> x
21.045/21.045	gcd(y,z) -> gcd(x,y) | iadd(z) ->* tp2(x,y)
21.045/21.045	gcd(z,y) -> gcd(x,y) | iadd(z) ->* tp2(x,y)
21.045/21.045	iadd(add(x,y)) -> tp2(x,y)
21.045/21.045	iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y)
21.045/21.045	iadd(y) -> tp2(0,y)
21.045/21.045	)
21.045/21.045	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.045/21.045	
21.045/21.045	CRule InfChecker Info:
21.045/21.045	gcd(0,x) -> x
21.045/21.045	Rule remains
21.045/21.045	Proof:
21.045/21.045	NO_CONDS
21.045/21.045	
21.045/21.045	CRule InfChecker Info:
21.045/21.045	gcd(x,0) -> x
21.045/21.045	Rule remains
21.045/21.045	Proof:
21.045/21.045	NO_CONDS
21.045/21.045	
21.045/21.045	CRule InfChecker Info:
21.045/21.045	gcd(y,z) -> gcd(x,y) | iadd(z) ->* tp2(x,y)
21.045/21.045	Rule remains
21.045/21.045	Proof:
21.045/21.045	NO
21.045/21.045	
21.045/21.045	Problem 1:
21.045/21.045	
21.045/21.045	Infeasibility Problem:
21.045/21.045	[(VAR vNonEmpty x y z vNonEmpty x y z)
21.045/21.045	(STRATEGY CONTEXTSENSITIVE
21.045/21.045	(gcd 1 2)
21.045/21.045	(iadd 1)
21.045/21.045	(0)
21.045/21.045	(add 1 2)
21.045/21.045	(fSNonEmpty)
21.045/21.045	(s 1)
21.045/21.045	(tp2 1 2)
21.045/21.045	)
21.045/21.045	(RULES
21.045/21.045	gcd(0,x) -> x
21.045/21.045	gcd(x,0) -> x
21.045/21.045	gcd(y,z) -> gcd(x,y) | iadd(z) ->* tp2(x,y)
21.045/21.045	gcd(z,y) -> gcd(x,y) | iadd(z) ->* tp2(x,y)
21.045/21.045	iadd(add(x,y)) -> tp2(x,y)
21.045/21.045	iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y)
21.045/21.045	iadd(y) -> tp2(0,y)
21.045/21.045	)]
21.045/21.045	
21.045/21.045	Infeasibility Conditions:
21.045/21.045	iadd(z) ->* tp2(x,y)
21.045/21.045	
21.045/21.045	Problem 1:
21.045/21.045	
21.045/21.045	Obtaining a proof using Prover9:
21.045/21.045	
21.045/21.045	 -> Prover9 Output:
21.045/21.045	============================== Prover9 ===============================
21.045/21.045	Prover9 (64) version 2009-11A, November 2009.
21.045/21.045	Process 10632 was started by ubuntu on ubuntu,
21.045/21.045	Wed Mar  9 09:14:16 2022
21.045/21.045	The command was "./prover9 -f /tmp/prover910625-0.in".
21.045/21.045	============================== end of head ===========================
21.045/21.045	
21.045/21.045	============================== INPUT =================================
21.045/21.045	
21.045/21.045	% Reading from file /tmp/prover910625-0.in
21.045/21.045	
21.045/21.045	assign(max_seconds,20).
21.045/21.045	
21.045/21.045	formulas(assumptions).
21.045/21.045	->_s0(x1,y) -> ->_s0(gcd(x1,x2),gcd(y,x2)) # label(congruence).
21.045/21.045	->_s0(x2,y) -> ->_s0(gcd(x1,x2),gcd(x1,y)) # label(congruence).
21.045/21.045	->_s0(x1,y) -> ->_s0(iadd(x1),iadd(y)) # label(congruence).
21.045/21.045	->_s0(x1,y) -> ->_s0(add(x1,x2),add(y,x2)) # label(congruence).
21.045/21.045	->_s0(x2,y) -> ->_s0(add(x1,x2),add(x1,y)) # label(congruence).
21.045/21.045	->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence).
21.045/21.045	->_s0(x1,y) -> ->_s0(tp2(x1,x2),tp2(y,x2)) # label(congruence).
21.045/21.045	->_s0(x2,y) -> ->_s0(tp2(x1,x2),tp2(x1,y)) # label(congruence).
21.045/21.045	->_s0(gcd(0,x1),x1) # label(replacement).
21.045/21.045	->_s0(gcd(x1,0),x1) # label(replacement).
21.045/21.045	->*_s0(iadd(x3),tp2(x1,x2)) -> ->_s0(gcd(x2,x3),gcd(x1,x2)) # label(replacement).
21.045/21.045	->*_s0(iadd(x3),tp2(x1,x2)) -> ->_s0(gcd(x3,x2),gcd(x1,x2)) # label(replacement).
21.045/21.045	->_s0(iadd(add(x1,x2)),tp2(x1,x2)) # label(replacement).
21.045/21.045	->*_s0(iadd(x3),tp2(x1,x2)) -> ->_s0(iadd(s(x3)),tp2(s(x1),x2)) # label(replacement).
21.045/21.045	->_s0(iadd(x2),tp2(0,x2)) # label(replacement).
21.045/21.045	->*_s0(x,x) # label(reflexivity).
21.045/21.045	->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity).
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	formulas(goals).
21.045/21.045	(exists x5 exists x6 exists x7 ->*_s0(iadd(x7),tp2(x5,x6))) # label(goal).
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	============================== end of input ==========================
21.045/21.045	
21.045/21.045	============================== PROCESS NON-CLAUSAL FORMULAS ==========
21.045/21.045	
21.045/21.045	% Formulas that are not ordinary clauses:
21.045/21.045	1 ->_s0(x1,y) -> ->_s0(gcd(x1,x2),gcd(y,x2)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	2 ->_s0(x2,y) -> ->_s0(gcd(x1,x2),gcd(x1,y)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	3 ->_s0(x1,y) -> ->_s0(iadd(x1),iadd(y)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	4 ->_s0(x1,y) -> ->_s0(add(x1,x2),add(y,x2)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	5 ->_s0(x2,y) -> ->_s0(add(x1,x2),add(x1,y)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	6 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	7 ->_s0(x1,y) -> ->_s0(tp2(x1,x2),tp2(y,x2)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	8 ->_s0(x2,y) -> ->_s0(tp2(x1,x2),tp2(x1,y)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	9 ->*_s0(iadd(x3),tp2(x1,x2)) -> ->_s0(gcd(x2,x3),gcd(x1,x2)) # label(replacement) # label(non_clause).  [assumption].
21.045/21.045	10 ->*_s0(iadd(x3),tp2(x1,x2)) -> ->_s0(gcd(x3,x2),gcd(x1,x2)) # label(replacement) # label(non_clause).  [assumption].
21.045/21.045	11 ->*_s0(iadd(x3),tp2(x1,x2)) -> ->_s0(iadd(s(x3)),tp2(s(x1),x2)) # label(replacement) # label(non_clause).  [assumption].
21.045/21.045	12 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
21.045/21.045	13 (exists x5 exists x6 exists x7 ->*_s0(iadd(x7),tp2(x5,x6))) # label(goal) # label(non_clause) # label(goal).  [goal].
21.045/21.045	
21.045/21.045	============================== end of process non-clausal formulas ===
21.045/21.045	
21.045/21.045	============================== PROCESS INITIAL CLAUSES ===============
21.045/21.045	
21.045/21.045	% Clauses before input processing:
21.045/21.045	
21.045/21.045	formulas(usable).
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	formulas(sos).
21.045/21.045	-->_s0(x,y) | ->_s0(gcd(x,z),gcd(y,z)) # label(congruence).  [clausify(1)].
21.045/21.045	-->_s0(x,y) | ->_s0(gcd(z,x),gcd(z,y)) # label(congruence).  [clausify(2)].
21.045/21.045	-->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(3)].
21.045/21.045	-->_s0(x,y) | ->_s0(add(x,z),add(y,z)) # label(congruence).  [clausify(4)].
21.045/21.045	-->_s0(x,y) | ->_s0(add(z,x),add(z,y)) # label(congruence).  [clausify(5)].
21.045/21.045	-->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(6)].
21.045/21.045	-->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.045/21.045	-->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.045/21.045	->_s0(gcd(0,x),x) # label(replacement).  [assumption].
21.045/21.045	->_s0(gcd(x,0),x) # label(replacement).  [assumption].
21.045/21.045	-->*_s0(iadd(x),tp2(y,z)) | ->_s0(gcd(z,x),gcd(y,z)) # label(replacement).  [clausify(9)].
21.045/21.045	-->*_s0(iadd(x),tp2(y,z)) | ->_s0(gcd(x,z),gcd(y,z)) # label(replacement).  [clausify(10)].
21.045/21.045	->_s0(iadd(add(x,y)),tp2(x,y)) # label(replacement).  [assumption].
21.045/21.045	-->*_s0(iadd(x),tp2(y,z)) | ->_s0(iadd(s(x)),tp2(s(y),z)) # label(replacement).  [clausify(11)].
21.045/21.045	->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.045/21.045	->*_s0(x,x) # label(reflexivity).  [assumption].
21.045/21.045	-->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(12)].
21.045/21.045	-->*_s0(iadd(x),tp2(y,z)) # label(goal).  [deny(13)].
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	formulas(demodulators).
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	============================== PREDICATE ELIMINATION =================
21.045/21.045	
21.045/21.045	No predicates eliminated.
21.045/21.045	
21.045/21.045	============================== end predicate elimination =============
21.045/21.045	
21.045/21.045	Auto_denials:
21.045/21.045	  % copying label goal to answer in negative clause
21.045/21.045	
21.045/21.045	Term ordering decisions:
21.045/21.045	Predicate symbol precedence:  predicate_order([ ->_s0, ->*_s0 ]).
21.045/21.045	Function symbol precedence:  function_order([ 0, gcd, tp2, add, iadd, s ]).
21.045/21.045	After inverse_order:  (no changes).
21.045/21.045	Unfolding symbols: (none).
21.045/21.045	
21.045/21.045	Auto_inference settings:
21.045/21.045	  % set(neg_binary_resolution).  % (HNE depth_diff=-9)
21.045/21.045	  % clear(ordered_res).  % (HNE depth_diff=-9)
21.045/21.045	  % set(ur_resolution).  % (HNE depth_diff=-9)
21.045/21.045	    % set(ur_resolution) -> set(pos_ur_resolution).
21.045/21.045	    % set(ur_resolution) -> set(neg_ur_resolution).
21.045/21.045	
21.045/21.045	Auto_process settings:  (no changes).
21.045/21.045	
21.045/21.045	kept:      14 -->_s0(x,y) | ->_s0(gcd(x,z),gcd(y,z)) # label(congruence).  [clausify(1)].
21.045/21.045	kept:      15 -->_s0(x,y) | ->_s0(gcd(z,x),gcd(z,y)) # label(congruence).  [clausify(2)].
21.045/21.045	kept:      16 -->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(3)].
21.045/21.045	kept:      17 -->_s0(x,y) | ->_s0(add(x,z),add(y,z)) # label(congruence).  [clausify(4)].
21.045/21.045	kept:      18 -->_s0(x,y) | ->_s0(add(z,x),add(z,y)) # label(congruence).  [clausify(5)].
21.045/21.045	kept:      19 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(6)].
21.045/21.045	kept:      20 -->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.045/21.045	kept:      21 -->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.045/21.045	kept:      22 ->_s0(gcd(0,x),x) # label(replacement).  [assumption].
21.045/21.045	kept:      23 ->_s0(gcd(x,0),x) # label(replacement).  [assumption].
21.045/21.045	kept:      24 -->*_s0(iadd(x),tp2(y,z)) | ->_s0(gcd(z,x),gcd(y,z)) # label(replacement).  [clausify(9)].
21.045/21.045	kept:      25 -->*_s0(iadd(x),tp2(y,z)) | ->_s0(gcd(x,z),gcd(y,z)) # label(replacement).  [clausify(10)].
21.045/21.045	kept:      26 ->_s0(iadd(add(x,y)),tp2(x,y)) # label(replacement).  [assumption].
21.045/21.045	kept:      27 -->*_s0(iadd(x),tp2(y,z)) | ->_s0(iadd(s(x)),tp2(s(y),z)) # label(replacement).  [clausify(11)].
21.045/21.045	kept:      28 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.045/21.045	kept:      29 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.045/21.045	kept:      30 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(12)].
21.045/21.045	kept:      31 -->*_s0(iadd(x),tp2(y,z)) # label(goal) # answer(goal).  [deny(13)].
21.045/21.045	
21.045/21.045	============================== end of process initial clauses ========
21.045/21.045	
21.045/21.045	============================== CLAUSES FOR SEARCH ====================
21.045/21.045	
21.045/21.045	% Clauses after input processing:
21.045/21.045	
21.045/21.045	formulas(usable).
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	formulas(sos).
21.045/21.045	14 -->_s0(x,y) | ->_s0(gcd(x,z),gcd(y,z)) # label(congruence).  [clausify(1)].
21.045/21.045	15 -->_s0(x,y) | ->_s0(gcd(z,x),gcd(z,y)) # label(congruence).  [clausify(2)].
21.045/21.045	16 -->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(3)].
21.045/21.045	17 -->_s0(x,y) | ->_s0(add(x,z),add(y,z)) # label(congruence).  [clausify(4)].
21.045/21.045	18 -->_s0(x,y) | ->_s0(add(z,x),add(z,y)) # label(congruence).  [clausify(5)].
21.045/21.045	19 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(6)].
21.045/21.045	20 -->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.045/21.045	21 -->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.045/21.045	22 ->_s0(gcd(0,x),x) # label(replacement).  [assumption].
21.045/21.045	23 ->_s0(gcd(x,0),x) # label(replacement).  [assumption].
21.045/21.045	26 ->_s0(iadd(add(x,y)),tp2(x,y)) # label(replacement).  [assumption].
21.045/21.045	28 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.045/21.045	29 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.045/21.045	30 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(12)].
21.045/21.045	31 -->*_s0(iadd(x),tp2(y,z)) # label(goal) # answer(goal).  [deny(13)].
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	formulas(demodulators).
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	============================== end of clauses for search =============
21.045/21.045	
21.045/21.045	============================== SEARCH ================================
21.045/21.045	
21.045/21.045	% Starting search at 0.00 seconds.
21.045/21.045	
21.045/21.045	given #1 (I,wt=10): 14 -->_s0(x,y) | ->_s0(gcd(x,z),gcd(y,z)) # label(congruence).  [clausify(1)].
21.045/21.045	
21.045/21.045	given #2 (I,wt=10): 15 -->_s0(x,y) | ->_s0(gcd(z,x),gcd(z,y)) # label(congruence).  [clausify(2)].
21.045/21.045	
21.045/21.045	given #3 (I,wt=8): 16 -->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(3)].
21.045/21.045	
21.045/21.045	given #4 (I,wt=10): 17 -->_s0(x,y) | ->_s0(add(x,z),add(y,z)) # label(congruence).  [clausify(4)].
21.045/21.045	
21.045/21.045	given #5 (I,wt=10): 18 -->_s0(x,y) | ->_s0(add(z,x),add(z,y)) # label(congruence).  [clausify(5)].
21.045/21.045	
21.045/21.045	given #6 (I,wt=8): 19 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(6)].
21.045/21.045	
21.045/21.045	given #7 (I,wt=10): 20 -->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.045/21.045	
21.045/21.045	given #8 (I,wt=10): 21 -->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.045/21.045	
21.045/21.045	given #9 (I,wt=5): 22 ->_s0(gcd(0,x),x) # label(replacement).  [assumption].
21.045/21.045	
21.045/21.045	given #10 (I,wt=5): 23 ->_s0(gcd(x,0),x) # label(replacement).  [assumption].
21.045/21.045	
21.045/21.045	given #11 (I,wt=8): 26 ->_s0(iadd(add(x,y)),tp2(x,y)) # label(replacement).  [assumption].
21.045/21.045	
21.045/21.045	given #12 (I,wt=6): 28 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.045/21.045	
21.045/21.045	given #13 (I,wt=3): 29 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.045/21.045	
21.045/21.045	given #14 (I,wt=9): 30 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(12)].
21.045/21.045	
21.045/21.045	============================== PROOF =================================
21.045/21.045	
21.045/21.045	% Proof 1 at 0.00 (+ 0.00) seconds: goal.
21.045/21.045	% Length of proof is 8.
21.045/21.045	% Level of proof is 3.
21.045/21.045	% Maximum clause weight is 9.000.
21.045/21.045	% Given clauses 14.
21.045/21.045	
21.045/21.045	12 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
21.045/21.045	13 (exists x5 exists x6 exists x7 ->*_s0(iadd(x7),tp2(x5,x6))) # label(goal) # label(non_clause) # label(goal).  [goal].
21.045/21.045	28 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.045/21.045	29 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.045/21.045	30 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(12)].
21.045/21.045	31 -->*_s0(iadd(x),tp2(y,z)) # label(goal) # answer(goal).  [deny(13)].
21.045/21.045	64 ->*_s0(iadd(x),tp2(0,x)).  [ur(30,a,28,a,b,29,a)].
21.045/21.045	65 $F # answer(goal).  [resolve(64,a,31,a)].
21.045/21.045	
21.045/21.045	============================== end of proof ==========================
21.045/21.045	
21.045/21.045	============================== STATISTICS ============================
21.045/21.045	
21.045/21.045	Given=14. Generated=51. Kept=51. proofs=1.
21.045/21.045	Usable=14. Sos=33. Demods=0. Limbo=0, Disabled=21. Hints=0.
21.045/21.045	Kept_by_rule=0, Deleted_by_rule=0.
21.045/21.045	Forward_subsumed=0. Back_subsumed=3.
21.045/21.045	Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
21.045/21.045	New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
21.045/21.045	Demod_attempts=0. Demod_rewrites=0.
21.045/21.045	Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
21.045/21.045	Nonunit_fsub_feature_tests=4. Nonunit_bsub_feature_tests=24.
21.045/21.045	Megabytes=0.14.
21.045/21.045	User_CPU=0.00, System_CPU=0.00, Wall_clock=0.
21.045/21.045	
21.045/21.045	============================== end of statistics =====================
21.045/21.045	
21.045/21.045	============================== end of search =========================
21.045/21.045	
21.045/21.045	THEOREM PROVED
21.045/21.045	
21.045/21.045	Exiting with 1 proof.
21.045/21.045	
21.045/21.045	Process 10632 exit (max_proofs) Wed Mar  9 09:14:16 2022
21.045/21.045	
21.045/21.045	
21.045/21.045	The problem is feasible.
21.045/21.045	
21.045/21.045	
21.045/21.045	CRule InfChecker Info:
21.045/21.045	gcd(z,y) -> gcd(x,y) | iadd(z) ->* tp2(x,y)
21.045/21.045	Rule remains
21.045/21.045	Proof:
21.045/21.045	NO
21.045/21.045	
21.045/21.045	Problem 1:
21.045/21.045	
21.045/21.045	Infeasibility Problem:
21.045/21.045	[(VAR vNonEmpty x y z vNonEmpty x y z)
21.045/21.045	(STRATEGY CONTEXTSENSITIVE
21.045/21.045	(gcd 1 2)
21.045/21.045	(iadd 1)
21.045/21.045	(0)
21.045/21.045	(add 1 2)
21.045/21.045	(fSNonEmpty)
21.045/21.045	(s 1)
21.045/21.045	(tp2 1 2)
21.045/21.045	)
21.045/21.045	(RULES
21.045/21.045	gcd(0,x) -> x
21.045/21.045	gcd(x,0) -> x
21.045/21.045	gcd(y,z) -> gcd(x,y) | iadd(z) ->* tp2(x,y)
21.045/21.045	gcd(z,y) -> gcd(x,y) | iadd(z) ->* tp2(x,y)
21.045/21.045	iadd(add(x,y)) -> tp2(x,y)
21.045/21.045	iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y)
21.045/21.045	iadd(y) -> tp2(0,y)
21.045/21.045	)]
21.045/21.045	
21.045/21.045	Infeasibility Conditions:
21.045/21.045	iadd(z) ->* tp2(x,y)
21.045/21.045	
21.045/21.045	Problem 1:
21.045/21.045	
21.045/21.045	Obtaining a proof using Prover9:
21.045/21.045	
21.045/21.045	 -> Prover9 Output:
21.045/21.045	============================== Prover9 ===============================
21.045/21.045	Prover9 (64) version 2009-11A, November 2009.
21.045/21.045	Process 10655 was started by ubuntu on ubuntu,
21.045/21.045	Wed Mar  9 09:14:16 2022
21.045/21.045	The command was "./prover9 -f /tmp/prover910647-0.in".
21.045/21.045	============================== end of head ===========================
21.045/21.045	
21.045/21.045	============================== INPUT =================================
21.045/21.045	
21.045/21.045	% Reading from file /tmp/prover910647-0.in
21.045/21.045	
21.045/21.045	assign(max_seconds,20).
21.045/21.045	
21.045/21.045	formulas(assumptions).
21.045/21.045	->_s0(x1,y) -> ->_s0(gcd(x1,x2),gcd(y,x2)) # label(congruence).
21.045/21.045	->_s0(x2,y) -> ->_s0(gcd(x1,x2),gcd(x1,y)) # label(congruence).
21.045/21.045	->_s0(x1,y) -> ->_s0(iadd(x1),iadd(y)) # label(congruence).
21.045/21.045	->_s0(x1,y) -> ->_s0(add(x1,x2),add(y,x2)) # label(congruence).
21.045/21.045	->_s0(x2,y) -> ->_s0(add(x1,x2),add(x1,y)) # label(congruence).
21.045/21.045	->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence).
21.045/21.045	->_s0(x1,y) -> ->_s0(tp2(x1,x2),tp2(y,x2)) # label(congruence).
21.045/21.045	->_s0(x2,y) -> ->_s0(tp2(x1,x2),tp2(x1,y)) # label(congruence).
21.045/21.045	->_s0(gcd(0,x1),x1) # label(replacement).
21.045/21.045	->_s0(gcd(x1,0),x1) # label(replacement).
21.045/21.045	->*_s0(iadd(x3),tp2(x1,x2)) -> ->_s0(gcd(x2,x3),gcd(x1,x2)) # label(replacement).
21.045/21.045	->*_s0(iadd(x3),tp2(x1,x2)) -> ->_s0(gcd(x3,x2),gcd(x1,x2)) # label(replacement).
21.045/21.045	->_s0(iadd(add(x1,x2)),tp2(x1,x2)) # label(replacement).
21.045/21.045	->*_s0(iadd(x3),tp2(x1,x2)) -> ->_s0(iadd(s(x3)),tp2(s(x1),x2)) # label(replacement).
21.045/21.045	->_s0(iadd(x2),tp2(0,x2)) # label(replacement).
21.045/21.045	->*_s0(x,x) # label(reflexivity).
21.045/21.045	->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity).
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	formulas(goals).
21.045/21.045	(exists x5 exists x6 exists x7 ->*_s0(iadd(x7),tp2(x5,x6))) # label(goal).
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	============================== end of input ==========================
21.045/21.045	
21.045/21.045	============================== PROCESS NON-CLAUSAL FORMULAS ==========
21.045/21.045	
21.045/21.045	% Formulas that are not ordinary clauses:
21.045/21.045	1 ->_s0(x1,y) -> ->_s0(gcd(x1,x2),gcd(y,x2)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	2 ->_s0(x2,y) -> ->_s0(gcd(x1,x2),gcd(x1,y)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	3 ->_s0(x1,y) -> ->_s0(iadd(x1),iadd(y)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	4 ->_s0(x1,y) -> ->_s0(add(x1,x2),add(y,x2)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	5 ->_s0(x2,y) -> ->_s0(add(x1,x2),add(x1,y)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	6 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	7 ->_s0(x1,y) -> ->_s0(tp2(x1,x2),tp2(y,x2)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	8 ->_s0(x2,y) -> ->_s0(tp2(x1,x2),tp2(x1,y)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	9 ->*_s0(iadd(x3),tp2(x1,x2)) -> ->_s0(gcd(x2,x3),gcd(x1,x2)) # label(replacement) # label(non_clause).  [assumption].
21.045/21.045	10 ->*_s0(iadd(x3),tp2(x1,x2)) -> ->_s0(gcd(x3,x2),gcd(x1,x2)) # label(replacement) # label(non_clause).  [assumption].
21.045/21.045	11 ->*_s0(iadd(x3),tp2(x1,x2)) -> ->_s0(iadd(s(x3)),tp2(s(x1),x2)) # label(replacement) # label(non_clause).  [assumption].
21.045/21.045	12 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
21.045/21.045	13 (exists x5 exists x6 exists x7 ->*_s0(iadd(x7),tp2(x5,x6))) # label(goal) # label(non_clause) # label(goal).  [goal].
21.045/21.045	
21.045/21.045	============================== end of process non-clausal formulas ===
21.045/21.045	
21.045/21.045	============================== PROCESS INITIAL CLAUSES ===============
21.045/21.045	
21.045/21.045	% Clauses before input processing:
21.045/21.045	
21.045/21.045	formulas(usable).
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	formulas(sos).
21.045/21.045	-->_s0(x,y) | ->_s0(gcd(x,z),gcd(y,z)) # label(congruence).  [clausify(1)].
21.045/21.045	-->_s0(x,y) | ->_s0(gcd(z,x),gcd(z,y)) # label(congruence).  [clausify(2)].
21.045/21.045	-->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(3)].
21.045/21.045	-->_s0(x,y) | ->_s0(add(x,z),add(y,z)) # label(congruence).  [clausify(4)].
21.045/21.045	-->_s0(x,y) | ->_s0(add(z,x),add(z,y)) # label(congruence).  [clausify(5)].
21.045/21.045	-->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(6)].
21.045/21.045	-->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.045/21.045	-->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.045/21.045	->_s0(gcd(0,x),x) # label(replacement).  [assumption].
21.045/21.045	->_s0(gcd(x,0),x) # label(replacement).  [assumption].
21.045/21.045	-->*_s0(iadd(x),tp2(y,z)) | ->_s0(gcd(z,x),gcd(y,z)) # label(replacement).  [clausify(9)].
21.045/21.045	-->*_s0(iadd(x),tp2(y,z)) | ->_s0(gcd(x,z),gcd(y,z)) # label(replacement).  [clausify(10)].
21.045/21.045	->_s0(iadd(add(x,y)),tp2(x,y)) # label(replacement).  [assumption].
21.045/21.045	-->*_s0(iadd(x),tp2(y,z)) | ->_s0(iadd(s(x)),tp2(s(y),z)) # label(replacement).  [clausify(11)].
21.045/21.045	->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.045/21.045	->*_s0(x,x) # label(reflexivity).  [assumption].
21.045/21.045	-->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(12)].
21.045/21.045	-->*_s0(iadd(x),tp2(y,z)) # label(goal).  [deny(13)].
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	formulas(demodulators).
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	============================== PREDICATE ELIMINATION =================
21.045/21.045	
21.045/21.045	No predicates eliminated.
21.045/21.045	
21.045/21.045	============================== end predicate elimination =============
21.045/21.045	
21.045/21.045	Auto_denials:
21.045/21.045	  % copying label goal to answer in negative clause
21.045/21.045	
21.045/21.045	Term ordering decisions:
21.045/21.045	Predicate symbol precedence:  predicate_order([ ->_s0, ->*_s0 ]).
21.045/21.045	Function symbol precedence:  function_order([ 0, gcd, tp2, add, iadd, s ]).
21.045/21.045	After inverse_order:  (no changes).
21.045/21.045	Unfolding symbols: (none).
21.045/21.045	
21.045/21.045	Auto_inference settings:
21.045/21.045	  % set(neg_binary_resolution).  % (HNE depth_diff=-9)
21.045/21.045	  % clear(ordered_res).  % (HNE depth_diff=-9)
21.045/21.045	  % set(ur_resolution).  % (HNE depth_diff=-9)
21.045/21.045	    % set(ur_resolution) -> set(pos_ur_resolution).
21.045/21.045	    % set(ur_resolution) -> set(neg_ur_resolution).
21.045/21.045	
21.045/21.045	Auto_process settings:  (no changes).
21.045/21.045	
21.045/21.045	kept:      14 -->_s0(x,y) | ->_s0(gcd(x,z),gcd(y,z)) # label(congruence).  [clausify(1)].
21.045/21.045	kept:      15 -->_s0(x,y) | ->_s0(gcd(z,x),gcd(z,y)) # label(congruence).  [clausify(2)].
21.045/21.045	kept:      16 -->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(3)].
21.045/21.045	kept:      17 -->_s0(x,y) | ->_s0(add(x,z),add(y,z)) # label(congruence).  [clausify(4)].
21.045/21.045	kept:      18 -->_s0(x,y) | ->_s0(add(z,x),add(z,y)) # label(congruence).  [clausify(5)].
21.045/21.045	kept:      19 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(6)].
21.045/21.045	kept:      20 -->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.045/21.045	kept:      21 -->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.045/21.045	kept:      22 ->_s0(gcd(0,x),x) # label(replacement).  [assumption].
21.045/21.045	kept:      23 ->_s0(gcd(x,0),x) # label(replacement).  [assumption].
21.045/21.045	kept:      24 -->*_s0(iadd(x),tp2(y,z)) | ->_s0(gcd(z,x),gcd(y,z)) # label(replacement).  [clausify(9)].
21.045/21.045	kept:      25 -->*_s0(iadd(x),tp2(y,z)) | ->_s0(gcd(x,z),gcd(y,z)) # label(replacement).  [clausify(10)].
21.045/21.045	kept:      26 ->_s0(iadd(add(x,y)),tp2(x,y)) # label(replacement).  [assumption].
21.045/21.045	kept:      27 -->*_s0(iadd(x),tp2(y,z)) | ->_s0(iadd(s(x)),tp2(s(y),z)) # label(replacement).  [clausify(11)].
21.045/21.045	kept:      28 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.045/21.045	kept:      29 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.045/21.045	kept:      30 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(12)].
21.045/21.045	kept:      31 -->*_s0(iadd(x),tp2(y,z)) # label(goal) # answer(goal).  [deny(13)].
21.045/21.045	
21.045/21.045	============================== end of process initial clauses ========
21.045/21.045	
21.045/21.045	============================== CLAUSES FOR SEARCH ====================
21.045/21.045	
21.045/21.045	% Clauses after input processing:
21.045/21.045	
21.045/21.045	formulas(usable).
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	formulas(sos).
21.045/21.045	14 -->_s0(x,y) | ->_s0(gcd(x,z),gcd(y,z)) # label(congruence).  [clausify(1)].
21.045/21.045	15 -->_s0(x,y) | ->_s0(gcd(z,x),gcd(z,y)) # label(congruence).  [clausify(2)].
21.045/21.045	16 -->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(3)].
21.045/21.045	17 -->_s0(x,y) | ->_s0(add(x,z),add(y,z)) # label(congruence).  [clausify(4)].
21.045/21.045	18 -->_s0(x,y) | ->_s0(add(z,x),add(z,y)) # label(congruence).  [clausify(5)].
21.045/21.045	19 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(6)].
21.045/21.045	20 -->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.045/21.045	21 -->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.045/21.045	22 ->_s0(gcd(0,x),x) # label(replacement).  [assumption].
21.045/21.045	23 ->_s0(gcd(x,0),x) # label(replacement).  [assumption].
21.045/21.045	26 ->_s0(iadd(add(x,y)),tp2(x,y)) # label(replacement).  [assumption].
21.045/21.045	28 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.045/21.045	29 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.045/21.045	30 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(12)].
21.045/21.045	31 -->*_s0(iadd(x),tp2(y,z)) # label(goal) # answer(goal).  [deny(13)].
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	formulas(demodulators).
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	============================== end of clauses for search =============
21.045/21.045	
21.045/21.045	============================== SEARCH ================================
21.045/21.045	
21.045/21.045	% Starting search at 0.00 seconds.
21.045/21.045	
21.045/21.045	given #1 (I,wt=10): 14 -->_s0(x,y) | ->_s0(gcd(x,z),gcd(y,z)) # label(congruence).  [clausify(1)].
21.045/21.045	
21.045/21.045	given #2 (I,wt=10): 15 -->_s0(x,y) | ->_s0(gcd(z,x),gcd(z,y)) # label(congruence).  [clausify(2)].
21.045/21.045	
21.045/21.045	given #3 (I,wt=8): 16 -->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(3)].
21.045/21.045	
21.045/21.045	given #4 (I,wt=10): 17 -->_s0(x,y) | ->_s0(add(x,z),add(y,z)) # label(congruence).  [clausify(4)].
21.045/21.045	
21.045/21.045	given #5 (I,wt=10): 18 -->_s0(x,y) | ->_s0(add(z,x),add(z,y)) # label(congruence).  [clausify(5)].
21.045/21.045	
21.045/21.045	given #6 (I,wt=8): 19 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(6)].
21.045/21.045	
21.045/21.045	given #7 (I,wt=10): 20 -->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.045/21.045	
21.045/21.045	given #8 (I,wt=10): 21 -->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.045/21.045	
21.045/21.045	given #9 (I,wt=5): 22 ->_s0(gcd(0,x),x) # label(replacement).  [assumption].
21.045/21.045	
21.045/21.045	given #10 (I,wt=5): 23 ->_s0(gcd(x,0),x) # label(replacement).  [assumption].
21.045/21.045	
21.045/21.045	given #11 (I,wt=8): 26 ->_s0(iadd(add(x,y)),tp2(x,y)) # label(replacement).  [assumption].
21.045/21.045	
21.045/21.045	given #12 (I,wt=6): 28 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.045/21.045	
21.045/21.045	given #13 (I,wt=3): 29 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.045/21.045	
21.045/21.045	given #14 (I,wt=9): 30 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(12)].
21.045/21.045	
21.045/21.045	============================== PROOF =================================
21.045/21.045	
21.045/21.045	% Proof 1 at 0.00 (+ 0.00) seconds: goal.
21.045/21.045	% Length of proof is 8.
21.045/21.045	% Level of proof is 3.
21.045/21.045	% Maximum clause weight is 9.000.
21.045/21.045	% Given clauses 14.
21.045/21.045	
21.045/21.045	12 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
21.045/21.045	13 (exists x5 exists x6 exists x7 ->*_s0(iadd(x7),tp2(x5,x6))) # label(goal) # label(non_clause) # label(goal).  [goal].
21.045/21.045	28 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.045/21.045	29 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.045/21.045	30 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(12)].
21.045/21.045	31 -->*_s0(iadd(x),tp2(y,z)) # label(goal) # answer(goal).  [deny(13)].
21.045/21.045	64 ->*_s0(iadd(x),tp2(0,x)).  [ur(30,a,28,a,b,29,a)].
21.045/21.045	65 $F # answer(goal).  [resolve(64,a,31,a)].
21.045/21.045	
21.045/21.045	============================== end of proof ==========================
21.045/21.045	
21.045/21.045	============================== STATISTICS ============================
21.045/21.045	
21.045/21.045	Given=14. Generated=51. Kept=51. proofs=1.
21.045/21.045	Usable=14. Sos=33. Demods=0. Limbo=0, Disabled=21. Hints=0.
21.045/21.045	Kept_by_rule=0, Deleted_by_rule=0.
21.045/21.045	Forward_subsumed=0. Back_subsumed=3.
21.045/21.045	Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
21.045/21.045	New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
21.045/21.045	Demod_attempts=0. Demod_rewrites=0.
21.045/21.045	Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
21.045/21.045	Nonunit_fsub_feature_tests=4. Nonunit_bsub_feature_tests=24.
21.045/21.045	Megabytes=0.14.
21.045/21.045	User_CPU=0.00, System_CPU=0.00, Wall_clock=0.
21.045/21.045	
21.045/21.045	============================== end of statistics =====================
21.045/21.045	
21.045/21.045	============================== end of search =========================
21.045/21.045	
21.045/21.045	THEOREM PROVED
21.045/21.045	
21.045/21.045	Exiting with 1 proof.
21.045/21.045	
21.045/21.045	Process 10655 exit (max_proofs) Wed Mar  9 09:14:16 2022
21.045/21.045	
21.045/21.045	
21.045/21.045	The problem is feasible.
21.045/21.045	
21.045/21.045	
21.045/21.045	CRule InfChecker Info:
21.045/21.045	iadd(add(x,y)) -> tp2(x,y)
21.045/21.045	Rule remains
21.045/21.045	Proof:
21.045/21.045	NO_CONDS
21.045/21.045	
21.045/21.045	CRule InfChecker Info:
21.045/21.045	iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y)
21.045/21.045	Rule remains
21.045/21.045	Proof:
21.045/21.045	NO
21.045/21.045	
21.045/21.045	Problem 1:
21.045/21.045	
21.045/21.045	Infeasibility Problem:
21.045/21.045	[(VAR vNonEmpty x y z vNonEmpty x y z)
21.045/21.045	(STRATEGY CONTEXTSENSITIVE
21.045/21.045	(gcd 1 2)
21.045/21.045	(iadd 1)
21.045/21.045	(0)
21.045/21.045	(add 1 2)
21.045/21.045	(fSNonEmpty)
21.045/21.045	(s 1)
21.045/21.045	(tp2 1 2)
21.045/21.045	)
21.045/21.045	(RULES
21.045/21.045	gcd(0,x) -> x
21.045/21.045	gcd(x,0) -> x
21.045/21.045	gcd(y,z) -> gcd(x,y) | iadd(z) ->* tp2(x,y)
21.045/21.045	gcd(z,y) -> gcd(x,y) | iadd(z) ->* tp2(x,y)
21.045/21.045	iadd(add(x,y)) -> tp2(x,y)
21.045/21.045	iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y)
21.045/21.045	iadd(y) -> tp2(0,y)
21.045/21.045	)]
21.045/21.045	
21.045/21.045	Infeasibility Conditions:
21.045/21.045	iadd(z) ->* tp2(x,y)
21.045/21.045	
21.045/21.045	Problem 1:
21.045/21.045	
21.045/21.045	Obtaining a proof using Prover9:
21.045/21.045	
21.045/21.045	 -> Prover9 Output:
21.045/21.045	============================== Prover9 ===============================
21.045/21.045	Prover9 (64) version 2009-11A, November 2009.
21.045/21.045	Process 10679 was started by ubuntu on ubuntu,
21.045/21.045	Wed Mar  9 09:14:16 2022
21.045/21.045	The command was "./prover9 -f /tmp/prover910670-0.in".
21.045/21.045	============================== end of head ===========================
21.045/21.045	
21.045/21.045	============================== INPUT =================================
21.045/21.045	
21.045/21.045	% Reading from file /tmp/prover910670-0.in
21.045/21.045	
21.045/21.045	assign(max_seconds,20).
21.045/21.045	
21.045/21.045	formulas(assumptions).
21.045/21.045	->_s0(x1,y) -> ->_s0(gcd(x1,x2),gcd(y,x2)) # label(congruence).
21.045/21.045	->_s0(x2,y) -> ->_s0(gcd(x1,x2),gcd(x1,y)) # label(congruence).
21.045/21.045	->_s0(x1,y) -> ->_s0(iadd(x1),iadd(y)) # label(congruence).
21.045/21.045	->_s0(x1,y) -> ->_s0(add(x1,x2),add(y,x2)) # label(congruence).
21.045/21.045	->_s0(x2,y) -> ->_s0(add(x1,x2),add(x1,y)) # label(congruence).
21.045/21.045	->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence).
21.045/21.045	->_s0(x1,y) -> ->_s0(tp2(x1,x2),tp2(y,x2)) # label(congruence).
21.045/21.045	->_s0(x2,y) -> ->_s0(tp2(x1,x2),tp2(x1,y)) # label(congruence).
21.045/21.045	->_s0(gcd(0,x1),x1) # label(replacement).
21.045/21.045	->_s0(gcd(x1,0),x1) # label(replacement).
21.045/21.045	->*_s0(iadd(x3),tp2(x1,x2)) -> ->_s0(gcd(x2,x3),gcd(x1,x2)) # label(replacement).
21.045/21.045	->*_s0(iadd(x3),tp2(x1,x2)) -> ->_s0(gcd(x3,x2),gcd(x1,x2)) # label(replacement).
21.045/21.045	->_s0(iadd(add(x1,x2)),tp2(x1,x2)) # label(replacement).
21.045/21.045	->*_s0(iadd(x3),tp2(x1,x2)) -> ->_s0(iadd(s(x3)),tp2(s(x1),x2)) # label(replacement).
21.045/21.045	->_s0(iadd(x2),tp2(0,x2)) # label(replacement).
21.045/21.045	->*_s0(x,x) # label(reflexivity).
21.045/21.045	->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity).
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	formulas(goals).
21.045/21.045	(exists x5 exists x6 exists x7 ->*_s0(iadd(x7),tp2(x5,x6))) # label(goal).
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	============================== end of input ==========================
21.045/21.045	
21.045/21.045	============================== PROCESS NON-CLAUSAL FORMULAS ==========
21.045/21.045	
21.045/21.045	% Formulas that are not ordinary clauses:
21.045/21.045	1 ->_s0(x1,y) -> ->_s0(gcd(x1,x2),gcd(y,x2)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	2 ->_s0(x2,y) -> ->_s0(gcd(x1,x2),gcd(x1,y)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	3 ->_s0(x1,y) -> ->_s0(iadd(x1),iadd(y)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	4 ->_s0(x1,y) -> ->_s0(add(x1,x2),add(y,x2)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	5 ->_s0(x2,y) -> ->_s0(add(x1,x2),add(x1,y)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	6 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	7 ->_s0(x1,y) -> ->_s0(tp2(x1,x2),tp2(y,x2)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	8 ->_s0(x2,y) -> ->_s0(tp2(x1,x2),tp2(x1,y)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	9 ->*_s0(iadd(x3),tp2(x1,x2)) -> ->_s0(gcd(x2,x3),gcd(x1,x2)) # label(replacement) # label(non_clause).  [assumption].
21.045/21.045	10 ->*_s0(iadd(x3),tp2(x1,x2)) -> ->_s0(gcd(x3,x2),gcd(x1,x2)) # label(replacement) # label(non_clause).  [assumption].
21.045/21.045	11 ->*_s0(iadd(x3),tp2(x1,x2)) -> ->_s0(iadd(s(x3)),tp2(s(x1),x2)) # label(replacement) # label(non_clause).  [assumption].
21.045/21.045	12 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
21.045/21.045	13 (exists x5 exists x6 exists x7 ->*_s0(iadd(x7),tp2(x5,x6))) # label(goal) # label(non_clause) # label(goal).  [goal].
21.045/21.045	
21.045/21.045	============================== end of process non-clausal formulas ===
21.045/21.045	
21.045/21.045	============================== PROCESS INITIAL CLAUSES ===============
21.045/21.045	
21.045/21.045	% Clauses before input processing:
21.045/21.045	
21.045/21.045	formulas(usable).
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	formulas(sos).
21.045/21.045	-->_s0(x,y) | ->_s0(gcd(x,z),gcd(y,z)) # label(congruence).  [clausify(1)].
21.045/21.045	-->_s0(x,y) | ->_s0(gcd(z,x),gcd(z,y)) # label(congruence).  [clausify(2)].
21.045/21.045	-->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(3)].
21.045/21.045	-->_s0(x,y) | ->_s0(add(x,z),add(y,z)) # label(congruence).  [clausify(4)].
21.045/21.045	-->_s0(x,y) | ->_s0(add(z,x),add(z,y)) # label(congruence).  [clausify(5)].
21.045/21.045	-->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(6)].
21.045/21.045	-->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.045/21.045	-->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.045/21.045	->_s0(gcd(0,x),x) # label(replacement).  [assumption].
21.045/21.045	->_s0(gcd(x,0),x) # label(replacement).  [assumption].
21.045/21.045	-->*_s0(iadd(x),tp2(y,z)) | ->_s0(gcd(z,x),gcd(y,z)) # label(replacement).  [clausify(9)].
21.045/21.045	-->*_s0(iadd(x),tp2(y,z)) | ->_s0(gcd(x,z),gcd(y,z)) # label(replacement).  [clausify(10)].
21.045/21.045	->_s0(iadd(add(x,y)),tp2(x,y)) # label(replacement).  [assumption].
21.045/21.045	-->*_s0(iadd(x),tp2(y,z)) | ->_s0(iadd(s(x)),tp2(s(y),z)) # label(replacement).  [clausify(11)].
21.045/21.045	->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.045/21.045	->*_s0(x,x) # label(reflexivity).  [assumption].
21.045/21.045	-->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(12)].
21.045/21.045	-->*_s0(iadd(x),tp2(y,z)) # label(goal).  [deny(13)].
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	formulas(demodulators).
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	============================== PREDICATE ELIMINATION =================
21.045/21.045	
21.045/21.045	No predicates eliminated.
21.045/21.045	
21.045/21.045	============================== end predicate elimination =============
21.045/21.045	
21.045/21.045	Auto_denials:
21.045/21.045	  % copying label goal to answer in negative clause
21.045/21.045	
21.045/21.045	Term ordering decisions:
21.045/21.045	Predicate symbol precedence:  predicate_order([ ->_s0, ->*_s0 ]).
21.045/21.045	Function symbol precedence:  function_order([ 0, gcd, tp2, add, iadd, s ]).
21.045/21.045	After inverse_order:  (no changes).
21.045/21.045	Unfolding symbols: (none).
21.045/21.045	
21.045/21.045	Auto_inference settings:
21.045/21.045	  % set(neg_binary_resolution).  % (HNE depth_diff=-9)
21.045/21.045	  % clear(ordered_res).  % (HNE depth_diff=-9)
21.045/21.045	  % set(ur_resolution).  % (HNE depth_diff=-9)
21.045/21.045	    % set(ur_resolution) -> set(pos_ur_resolution).
21.045/21.045	    % set(ur_resolution) -> set(neg_ur_resolution).
21.045/21.045	
21.045/21.045	Auto_process settings:  (no changes).
21.045/21.045	
21.045/21.045	kept:      14 -->_s0(x,y) | ->_s0(gcd(x,z),gcd(y,z)) # label(congruence).  [clausify(1)].
21.045/21.045	kept:      15 -->_s0(x,y) | ->_s0(gcd(z,x),gcd(z,y)) # label(congruence).  [clausify(2)].
21.045/21.045	kept:      16 -->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(3)].
21.045/21.045	kept:      17 -->_s0(x,y) | ->_s0(add(x,z),add(y,z)) # label(congruence).  [clausify(4)].
21.045/21.045	kept:      18 -->_s0(x,y) | ->_s0(add(z,x),add(z,y)) # label(congruence).  [clausify(5)].
21.045/21.045	kept:      19 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(6)].
21.045/21.045	kept:      20 -->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.045/21.045	kept:      21 -->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.045/21.045	kept:      22 ->_s0(gcd(0,x),x) # label(replacement).  [assumption].
21.045/21.045	kept:      23 ->_s0(gcd(x,0),x) # label(replacement).  [assumption].
21.045/21.045	kept:      24 -->*_s0(iadd(x),tp2(y,z)) | ->_s0(gcd(z,x),gcd(y,z)) # label(replacement).  [clausify(9)].
21.045/21.045	kept:      25 -->*_s0(iadd(x),tp2(y,z)) | ->_s0(gcd(x,z),gcd(y,z)) # label(replacement).  [clausify(10)].
21.045/21.045	kept:      26 ->_s0(iadd(add(x,y)),tp2(x,y)) # label(replacement).  [assumption].
21.045/21.045	kept:      27 -->*_s0(iadd(x),tp2(y,z)) | ->_s0(iadd(s(x)),tp2(s(y),z)) # label(replacement).  [clausify(11)].
21.045/21.045	kept:      28 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.045/21.045	kept:      29 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.045/21.045	kept:      30 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(12)].
21.045/21.045	kept:      31 -->*_s0(iadd(x),tp2(y,z)) # label(goal) # answer(goal).  [deny(13)].
21.045/21.045	
21.045/21.045	============================== end of process initial clauses ========
21.045/21.045	
21.045/21.045	============================== CLAUSES FOR SEARCH ====================
21.045/21.045	
21.045/21.045	% Clauses after input processing:
21.045/21.045	
21.045/21.045	formulas(usable).
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	formulas(sos).
21.045/21.045	14 -->_s0(x,y) | ->_s0(gcd(x,z),gcd(y,z)) # label(congruence).  [clausify(1)].
21.045/21.045	15 -->_s0(x,y) | ->_s0(gcd(z,x),gcd(z,y)) # label(congruence).  [clausify(2)].
21.045/21.045	16 -->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(3)].
21.045/21.045	17 -->_s0(x,y) | ->_s0(add(x,z),add(y,z)) # label(congruence).  [clausify(4)].
21.045/21.045	18 -->_s0(x,y) | ->_s0(add(z,x),add(z,y)) # label(congruence).  [clausify(5)].
21.045/21.045	19 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(6)].
21.045/21.045	20 -->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.045/21.045	21 -->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.045/21.045	22 ->_s0(gcd(0,x),x) # label(replacement).  [assumption].
21.045/21.045	23 ->_s0(gcd(x,0),x) # label(replacement).  [assumption].
21.045/21.045	26 ->_s0(iadd(add(x,y)),tp2(x,y)) # label(replacement).  [assumption].
21.045/21.045	28 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.045/21.045	29 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.045/21.045	30 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(12)].
21.045/21.045	31 -->*_s0(iadd(x),tp2(y,z)) # label(goal) # answer(goal).  [deny(13)].
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	formulas(demodulators).
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	============================== end of clauses for search =============
21.045/21.045	
21.045/21.045	============================== SEARCH ================================
21.045/21.045	
21.045/21.045	% Starting search at 0.00 seconds.
21.045/21.045	
21.045/21.045	given #1 (I,wt=10): 14 -->_s0(x,y) | ->_s0(gcd(x,z),gcd(y,z)) # label(congruence).  [clausify(1)].
21.045/21.045	
21.045/21.045	given #2 (I,wt=10): 15 -->_s0(x,y) | ->_s0(gcd(z,x),gcd(z,y)) # label(congruence).  [clausify(2)].
21.045/21.045	
21.045/21.045	given #3 (I,wt=8): 16 -->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(3)].
21.045/21.045	
21.045/21.045	given #4 (I,wt=10): 17 -->_s0(x,y) | ->_s0(add(x,z),add(y,z)) # label(congruence).  [clausify(4)].
21.045/21.045	
21.045/21.045	given #5 (I,wt=10): 18 -->_s0(x,y) | ->_s0(add(z,x),add(z,y)) # label(congruence).  [clausify(5)].
21.045/21.045	
21.045/21.045	given #6 (I,wt=8): 19 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(6)].
21.045/21.045	
21.045/21.045	given #7 (I,wt=10): 20 -->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.045/21.045	
21.045/21.045	given #8 (I,wt=10): 21 -->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.045/21.045	
21.045/21.045	given #9 (I,wt=5): 22 ->_s0(gcd(0,x),x) # label(replacement).  [assumption].
21.045/21.045	
21.045/21.045	given #10 (I,wt=5): 23 ->_s0(gcd(x,0),x) # label(replacement).  [assumption].
21.045/21.045	
21.045/21.045	given #11 (I,wt=8): 26 ->_s0(iadd(add(x,y)),tp2(x,y)) # label(replacement).  [assumption].
21.045/21.045	
21.045/21.045	given #12 (I,wt=6): 28 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.045/21.045	
21.045/21.045	given #13 (I,wt=3): 29 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.045/21.045	
21.045/21.045	given #14 (I,wt=9): 30 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(12)].
21.045/21.045	
21.045/21.045	============================== PROOF =================================
21.045/21.045	
21.045/21.045	% Proof 1 at 0.01 (+ 0.00) seconds: goal.
21.045/21.045	% Length of proof is 8.
21.045/21.045	% Level of proof is 3.
21.045/21.045	% Maximum clause weight is 9.000.
21.045/21.045	% Given clauses 14.
21.045/21.045	
21.045/21.045	12 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
21.045/21.045	13 (exists x5 exists x6 exists x7 ->*_s0(iadd(x7),tp2(x5,x6))) # label(goal) # label(non_clause) # label(goal).  [goal].
21.045/21.045	28 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.045/21.045	29 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.045/21.045	30 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(12)].
21.045/21.045	31 -->*_s0(iadd(x),tp2(y,z)) # label(goal) # answer(goal).  [deny(13)].
21.045/21.045	64 ->*_s0(iadd(x),tp2(0,x)).  [ur(30,a,28,a,b,29,a)].
21.045/21.045	65 $F # answer(goal).  [resolve(64,a,31,a)].
21.045/21.045	
21.045/21.045	============================== end of proof ==========================
21.045/21.045	
21.045/21.045	============================== STATISTICS ============================
21.045/21.045	
21.045/21.045	Given=14. Generated=51. Kept=51. proofs=1.
21.045/21.045	Usable=14. Sos=33. Demods=0. Limbo=0, Disabled=21. Hints=0.
21.045/21.045	Kept_by_rule=0, Deleted_by_rule=0.
21.045/21.045	Forward_subsumed=0. Back_subsumed=3.
21.045/21.045	Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
21.045/21.045	New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
21.045/21.045	Demod_attempts=0. Demod_rewrites=0.
21.045/21.045	Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
21.045/21.045	Nonunit_fsub_feature_tests=4. Nonunit_bsub_feature_tests=24.
21.045/21.045	Megabytes=0.14.
21.045/21.045	User_CPU=0.01, System_CPU=0.00, Wall_clock=0.
21.045/21.045	
21.045/21.045	============================== end of statistics =====================
21.045/21.045	
21.045/21.045	============================== end of search =========================
21.045/21.045	
21.045/21.045	THEOREM PROVED
21.045/21.045	
21.045/21.045	Exiting with 1 proof.
21.045/21.045	
21.045/21.045	Process 10679 exit (max_proofs) Wed Mar  9 09:14:16 2022
21.045/21.045	
21.045/21.045	
21.045/21.045	The problem is feasible.
21.045/21.045	
21.045/21.045	
21.045/21.045	CRule InfChecker Info:
21.045/21.045	iadd(y) -> tp2(0,y)
21.045/21.045	Rule remains
21.045/21.045	Proof:
21.045/21.045	NO_CONDS
21.045/21.045	
21.045/21.045	Problem 1:
21.045/21.045	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.045/21.045	Confluence Problem:
21.045/21.045	(VAR x y z)
21.045/21.045	(REPLACEMENT-MAP
21.045/21.045	(gcd 1, 2)
21.045/21.045	(iadd 1)
21.045/21.045	(0)
21.045/21.045	(add 1, 2)
21.045/21.045	(fSNonEmpty)
21.045/21.045	(s 1)
21.045/21.045	(tp2 1, 2)
21.045/21.045	)
21.045/21.045	(RULES
21.045/21.045	gcd(0,x) -> x
21.045/21.045	gcd(x,0) -> x
21.045/21.045	gcd(y,z) -> gcd(x,y) | iadd(z) ->* tp2(x,y)
21.045/21.045	gcd(z,y) -> gcd(x,y) | iadd(z) ->* tp2(x,y)
21.045/21.045	iadd(add(x,y)) -> tp2(x,y)
21.045/21.045	iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y)
21.045/21.045	iadd(y) -> tp2(0,y)
21.045/21.045	)
21.045/21.045	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.045/21.045	
21.045/21.045	Critical Pairs Processor:
21.045/21.045	-> Rules:
21.045/21.045	gcd(0,x) -> x
21.045/21.045	gcd(x,0) -> x
21.045/21.045	gcd(y,z) -> gcd(x,y) | iadd(z) ->* tp2(x,y)
21.045/21.045	gcd(z,y) -> gcd(x,y) | iadd(z) ->* tp2(x,y)
21.045/21.045	iadd(add(x,y)) -> tp2(x,y)
21.045/21.045	iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y)
21.045/21.045	iadd(y) -> tp2(0,y)
21.045/21.045	-> Vars:
21.045/21.045	"x", "y", "z"
21.045/21.045	
21.045/21.045	-> Rlps:
21.045/21.045	crule: gcd(0,x) -> x, id: 1, possubterms: gcd(0,x)-> [], 0-> [1]
21.045/21.045	crule: gcd(x,0) -> x, id: 2, possubterms: gcd(x,0)-> [], 0-> [2]
21.045/21.045	crule: gcd(y,z) -> gcd(x,y) | iadd(z) ->* tp2(x,y), id: 3, possubterms: gcd(y,z)-> []
21.045/21.045	crule: gcd(z,y) -> gcd(x,y) | iadd(z) ->* tp2(x,y), id: 4, possubterms: gcd(z,y)-> []
21.045/21.045	crule: iadd(add(x,y)) -> tp2(x,y), id: 5, possubterms: iadd(add(x,y))-> [], add(x,y)-> [1]
21.045/21.045	crule: iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y), id: 6, possubterms: iadd(s(z))-> [], s(z)-> [1]
21.045/21.045	crule: iadd(y) -> tp2(0,y), id: 7, possubterms: iadd(y)-> []
21.045/21.045	
21.045/21.045	-> Unifications:
21.045/21.045	R2 unifies with  R1 at  p: [], l: gcd(x,0), lp: gcd(x,0), conds: {}, sig: {x -> 0,x' -> 0}, l': gcd(0,x'), r: x, r': x'
21.045/21.045	R3 unifies with  R1 at  p: [], l: gcd(y,z), lp: gcd(y,z), conds: {iadd(z) ->* tp2(x,y)}, sig: {y -> 0,z -> x'}, l': gcd(0,x'), r: gcd(x,y), r': x'
21.045/21.045	R3 unifies with  R2 at  p: [], l: gcd(y,z), lp: gcd(y,z), conds: {iadd(z) ->* tp2(x,y)}, sig: {y -> x',z -> 0}, l': gcd(x',0), r: gcd(x,y), r': x'
21.045/21.045	R4 unifies with  R1 at  p: [], l: gcd(z,y), lp: gcd(z,y), conds: {iadd(z) ->* tp2(x,y)}, sig: {y -> x',z -> 0}, l': gcd(0,x'), r: gcd(x,y), r': x'
21.045/21.045	R4 unifies with  R2 at  p: [], l: gcd(z,y), lp: gcd(z,y), conds: {iadd(z) ->* tp2(x,y)}, sig: {y -> 0,z -> x'}, l': gcd(x',0), r: gcd(x,y), r': x'
21.045/21.045	R4 unifies with  R3 at  p: [], l: gcd(z,y), lp: gcd(z,y), conds: {iadd(z) ->* tp2(x,y), iadd(z') ->* tp2(x',y')}, sig: {y -> z',z -> y'}, l': gcd(y',z'), r: gcd(x,y), r': gcd(x',y')
21.045/21.045	R7 unifies with  R5 at  p: [], l: iadd(y), lp: iadd(y), conds: {}, sig: {y -> add(x,y')}, l': iadd(add(x,y')), r: tp2(0,y), r': tp2(x,y')
21.045/21.045	R7 unifies with  R6 at  p: [], l: iadd(y), lp: iadd(y), conds: {iadd(z) ->* tp2(x,y')}, sig: {y -> s(z)}, l': iadd(s(z)), r: tp2(0,y), r': tp2(s(x),y')
21.045/21.045	
21.045/21.045	-> Critical pairs info:
21.045/21.045	<tp2(s(x),y'),tp2(0,s(z))> | iadd(z) ->* tp2(x,y')  =>  Not trivial, Overlay, NW2, N1
21.045/21.045	<0,0>   =>  Trivial, Overlay, NW2, N2
21.045/21.045	<tp2(x,y'),tp2(0,add(x,y'))>   =>  Not trivial, Overlay, NW2, N3
21.045/21.045	<x',gcd(x,x')> | iadd(0) ->* tp2(x,x')  =>  Not trivial, Overlay, NW1, N4
21.045/21.045	<x',gcd(x,0)> | iadd(x') ->* tp2(x,0)  =>  Not trivial, Overlay, NW1, N5
21.045/21.045	<gcd(x',y'),gcd(x,z')> | iadd(y') ->* tp2(x,z'), iadd(z') ->* tp2(x',y')  =>  Not trivial, Overlay, NW0, N6
21.045/21.045	
21.045/21.045	-> Problem conclusions:
21.045/21.045	 Left linear, Right linear, Linear
21.045/21.045	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
21.045/21.045	 CTRS Type: 3
21.045/21.045	 Deterministic, Strongly deterministic
21.045/21.045	 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS
21.045/21.045	 Maybe right-stable CTRS, Overlay CTRS
21.045/21.045	 Maybe normal CTRS, Maybe almost normal CTRS
21.045/21.045	 Maybe terminating CTRS, Maybe operational terminating CTRS, Maybe joinable CCPs
21.045/21.045	 Maybe level confluent
21.045/21.045	 Maybe confluent
21.045/21.045	
21.045/21.045	Problem 1:
21.045/21.045	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.045/21.045	Confluence Problem:
21.045/21.045	(VAR x y z x y' z)
21.045/21.045	(REPLACEMENT-MAP
21.045/21.045	(gcd 1, 2)
21.045/21.045	(iadd 1)
21.045/21.045	(0)
21.045/21.045	(add 1, 2)
21.045/21.045	(fSNonEmpty)
21.045/21.045	(s 1)
21.045/21.045	(tp2 1, 2)
21.045/21.045	)
21.045/21.045	(RULES
21.045/21.045	gcd(0,x) -> x
21.045/21.045	gcd(x,0) -> x
21.045/21.045	gcd(y,z) -> gcd(x,y) | iadd(z) ->* tp2(x,y)
21.045/21.045	gcd(z,y) -> gcd(x,y) | iadd(z) ->* tp2(x,y)
21.045/21.045	iadd(add(x,y)) -> tp2(x,y)
21.045/21.045	iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y)
21.045/21.045	iadd(y) -> tp2(0,y)
21.045/21.045	)
21.045/21.045	Critical Pairs:
21.045/21.045	<tp2(s(x),y'),tp2(0,s(z))> | iadd(z) ->* tp2(x,y')  =>  Not trivial, Overlay, NW2, N1
21.045/21.045	<tp2(x,y'),tp2(0,add(x,y'))>   =>  Not trivial, Overlay, NW2, N3
21.045/21.045	<x',gcd(x,x')> | iadd(0) ->* tp2(x,x')  =>  Not trivial, Overlay, NW1, N4
21.045/21.045	<x',gcd(x,0)> | iadd(x') ->* tp2(x,0)  =>  Not trivial, Overlay, NW1, N5
21.045/21.045	<gcd(x',y'),gcd(x,z')> | iadd(y') ->* tp2(x,z'), iadd(z') ->* tp2(x',y')  =>  Not trivial, Overlay, NW0, N6
21.045/21.045	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.045/21.045	
21.045/21.045	Conditional Critical Pairs Distributor Processor
21.045/21.045	
21.045/21.045	Problem 1:
21.045/21.045	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.045/21.045	Confluence Problem:
21.045/21.045	(VAR x y z x y' z)
21.045/21.045	(REPLACEMENT-MAP
21.045/21.045	(gcd 1, 2)
21.045/21.045	(iadd 1)
21.045/21.045	(0)
21.045/21.045	(add 1, 2)
21.045/21.045	(fSNonEmpty)
21.045/21.045	(s 1)
21.045/21.045	(tp2 1, 2)
21.045/21.045	)
21.045/21.045	(RULES
21.045/21.045	gcd(0,x) -> x
21.045/21.045	gcd(x,0) -> x
21.045/21.045	gcd(y,z) -> gcd(x,y) | iadd(z) ->* tp2(x,y)
21.045/21.045	gcd(z,y) -> gcd(x,y) | iadd(z) ->* tp2(x,y)
21.045/21.045	iadd(add(x,y)) -> tp2(x,y)
21.045/21.045	iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y)
21.045/21.045	iadd(y) -> tp2(0,y)
21.045/21.045	)
21.045/21.045	Critical Pairs:
21.045/21.045	<tp2(x,y'),tp2(0,add(x,y'))>   =>  Not trivial, Overlay, NW2, N3
21.045/21.045	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.045/21.045	
21.045/21.045	Infeasible Convergence No Conditions CCP Processor:
21.045/21.045	Infeasible convergence?
21.045/21.045	YES
21.045/21.045	
21.045/21.045	Problem 1:
21.045/21.045	
21.045/21.045	Infeasibility Problem:
21.045/21.045	[(VAR vNonEmpty x y z y1 vNonEmpty z)
21.045/21.045	(STRATEGY CONTEXTSENSITIVE
21.045/21.045	(gcd 1 2)
21.045/21.045	(iadd 1)
21.045/21.045	(0)
21.045/21.045	(add 1 2)
21.045/21.045	(c_x)
21.045/21.045	(c_y1)
21.045/21.045	(fSNonEmpty)
21.045/21.045	(s 1)
21.045/21.045	(tp2 1 2)
21.045/21.045	)
21.045/21.045	(RULES
21.045/21.045	gcd(0,x) -> x
21.045/21.045	gcd(x,0) -> x
21.045/21.045	gcd(y,z) -> gcd(x,y) | iadd(z) ->* tp2(x,y)
21.045/21.045	gcd(z,y) -> gcd(x,y) | iadd(z) ->* tp2(x,y)
21.045/21.045	iadd(add(x,y)) -> tp2(x,y)
21.045/21.045	iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y)
21.045/21.045	iadd(y) -> tp2(0,y)
21.045/21.045	)]
21.045/21.045	
21.045/21.045	Infeasibility Conditions:
21.045/21.045	tp2(c_x,c_y1) ->* z, tp2(0,add(c_x,c_y1)) ->* z
21.045/21.045	
21.045/21.045	Problem 1:
21.045/21.045	
21.045/21.045	Obtaining a model using Mace4:
21.045/21.045	
21.045/21.045	 -> Usable Rules:
21.045/21.045	Empty
21.045/21.045	
21.045/21.045	 -> Mace4 Output:
21.045/21.045	============================== Mace4 =================================
21.045/21.045	Mace4 (64) version 2009-11A, November 2009.
21.045/21.045	Process 10709 was started by ubuntu on ubuntu,
21.045/21.045	Wed Mar  9 09:14:16 2022
21.045/21.045	The command was "./mace4 -c -f /tmp/mace410694-2.in".
21.045/21.045	============================== end of head ===========================
21.045/21.045	
21.045/21.045	============================== INPUT =================================
21.045/21.045	
21.045/21.045	% Reading from file /tmp/mace410694-2.in
21.045/21.045	
21.045/21.045	assign(max_seconds,20).
21.045/21.045	
21.045/21.045	formulas(assumptions).
21.045/21.045	->(x1,y) -> ->(gcd(x1,x2),gcd(y,x2)) # label(congruence).
21.045/21.045	->(x2,y) -> ->(gcd(x1,x2),gcd(x1,y)) # label(congruence).
21.045/21.045	->(x1,y) -> ->(iadd(x1),iadd(y)) # label(congruence).
21.045/21.045	->(x1,y) -> ->(add(x1,x2),add(y,x2)) # label(congruence).
21.045/21.045	->(x2,y) -> ->(add(x1,x2),add(x1,y)) # label(congruence).
21.045/21.045	->(x1,y) -> ->(s(x1),s(y)) # label(congruence).
21.045/21.045	->(x1,y) -> ->(tp2(x1,x2),tp2(y,x2)) # label(congruence).
21.045/21.045	->(x2,y) -> ->(tp2(x1,x2),tp2(x1,y)) # label(congruence).
21.045/21.045	->*(x,x) # label(reflexivity).
21.045/21.045	->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity).
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	formulas(goals).
21.045/21.045	(exists x6 (->*(tp2(c_x,c_y1),x6) & ->*(tp2(0,add(c_x,c_y1)),x6))) # label(goal).
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	============================== end of input ==========================
21.045/21.045	
21.045/21.045	============================== PROCESS NON-CLAUSAL FORMULAS ==========
21.045/21.045	
21.045/21.045	% Formulas that are not ordinary clauses:
21.045/21.045	1 ->(x1,y) -> ->(gcd(x1,x2),gcd(y,x2)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	2 ->(x2,y) -> ->(gcd(x1,x2),gcd(x1,y)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	3 ->(x1,y) -> ->(iadd(x1),iadd(y)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	4 ->(x1,y) -> ->(add(x1,x2),add(y,x2)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	5 ->(x2,y) -> ->(add(x1,x2),add(x1,y)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	6 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	7 ->(x1,y) -> ->(tp2(x1,x2),tp2(y,x2)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	8 ->(x2,y) -> ->(tp2(x1,x2),tp2(x1,y)) # label(congruence) # label(non_clause).  [assumption].
21.045/21.045	9 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause).  [assumption].
21.045/21.045	10 (exists x6 (->*(tp2(c_x,c_y1),x6) & ->*(tp2(0,add(c_x,c_y1)),x6))) # label(goal) # label(non_clause) # label(goal).  [goal].
21.045/21.045	
21.045/21.045	============================== end of process non-clausal formulas ===
21.045/21.045	
21.045/21.045	============================== CLAUSES FOR SEARCH ====================
21.045/21.045	
21.045/21.045	formulas(mace4_clauses).
21.045/21.045	-->(x,y) | ->(gcd(x,z),gcd(y,z)) # label(congruence).
21.045/21.045	-->(x,y) | ->(gcd(z,x),gcd(z,y)) # label(congruence).
21.045/21.045	-->(x,y) | ->(iadd(x),iadd(y)) # label(congruence).
21.045/21.045	-->(x,y) | ->(add(x,z),add(y,z)) # label(congruence).
21.045/21.045	-->(x,y) | ->(add(z,x),add(z,y)) # label(congruence).
21.045/21.045	-->(x,y) | ->(s(x),s(y)) # label(congruence).
21.045/21.045	-->(x,y) | ->(tp2(x,z),tp2(y,z)) # label(congruence).
21.045/21.045	-->(x,y) | ->(tp2(z,x),tp2(z,y)) # label(congruence).
21.045/21.045	->*(x,x) # label(reflexivity).
21.045/21.045	-->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity).
21.045/21.045	-->*(tp2(c_x,c_y1),x) | -->*(tp2(0,add(c_x,c_y1)),x) # label(goal).
21.045/21.045	end_of_list.
21.045/21.045	
21.045/21.045	============================== end of clauses for search =============
21.045/21.045	
21.045/21.045	% There are no natural numbers in the input.
21.045/21.045	
21.045/21.045	============================== DOMAIN SIZE 2 =========================
21.045/21.045	
21.045/21.045	============================== MODEL =================================
21.045/21.045	
21.045/21.045	interpretation( 2, [number=1, seconds=0], [
21.045/21.045	
21.045/21.045	        function(0, [ 0 ]),
21.045/21.045	
21.045/21.045	        function(c_x, [ 0 ]),
21.045/21.045	
21.045/21.045	        function(c_y1, [ 0 ]),
21.045/21.045	
21.045/21.045	        function(iadd(_), [ 0, 0 ]),
21.045/21.045	
21.045/21.045	        function(s(_), [ 0, 0 ]),
21.045/21.045	
21.045/21.045	        function(tp2(_,_), [
21.045/21.045				   0, 1,
21.045/21.045				   0, 0 ]),
21.045/21.045	
21.045/21.045	        function(gcd(_,_), [
21.045/21.045				   0, 0,
21.045/21.045				   0, 0 ]),
21.045/21.045	
21.045/21.045	        function(add(_,_), [
21.045/21.045				   1, 0,
21.045/21.045				   0, 0 ]),
21.045/21.045	
21.045/21.045	        relation(->*(_,_), [
21.045/21.045				   1, 0,
21.045/21.045				   0, 1 ]),
21.045/21.045	
21.045/21.045	        relation(->(_,_), [
21.045/21.045				   0, 0,
21.045/21.045				   0, 0 ])
21.045/21.045	]).
21.045/21.045	
21.045/21.045	============================== end of model ==========================
21.045/21.045	
21.045/21.045	============================== STATISTICS ============================
21.045/21.045	
21.045/21.045	For domain size 2.
21.045/21.045	
21.045/21.045	Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
21.045/21.045	Ground clauses: seen=68, kept=64.
21.045/21.045	Selections=19, assignments=20, propagations=8, current_models=1.
21.045/21.045	Rewrite_terms=130, rewrite_bools=81, indexes=20.
21.045/21.045	Rules_from_neg_clauses=1, cross_offs=1.
21.045/21.045	
21.045/21.045	============================== end of statistics =====================
21.045/21.045	
21.045/21.045	User_CPU=0.00, System_CPU=0.00, Wall_clock=0.
21.045/21.045	
21.045/21.045	Exiting with 1 model.
21.045/21.045	
21.045/21.045	Process 10709 exit (max_models) Wed Mar  9 09:14:16 2022
21.045/21.045	The process finished Wed Mar  9 09:14:16 2022
21.045/21.045	
21.045/21.045	
21.045/21.045	Mace4 cooked interpretation:
21.045/21.045	
21.045/21.045	
21.045/21.045	
21.045/21.045	The problem is infeasible.
21.045/21.045	
21.045/21.045	
21.045/21.045	The problem is not joinable.
21.045/21.045	29.50user 1.07system 0:21.45elapsed 142%CPU (0avgtext+0avgdata 445384maxresident)k
21.045/21.045	8inputs+0outputs (0major+163140minor)pagefaults 0swaps